Minimal support for __builtin_unreachable and for __builtin_expect

aarch64/Asmexpand.ml

@@ -355,8 +355,12 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Byte swap *)
   | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
      emit (Prev(W, res, a1))

arm/Asmexpand.ml

@@ -407,8 +407,12 @@ let expand_builtin_inline name args res =
   (* Vararg stuff *)
   | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))

cfrontend/C2C.ml

@@ -268,6 +268,11 @@ let builtins_generic = {
         (TPtr(TVoid [], []),
           [TPtr(TVoid [], []); TInt(IULong, [])],
           false);
+  (* Optimization hints *)
+    "__builtin_unreachable",
+        (TVoid [], [], false);
+    "__builtin_expect",
+        (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
   (* Helper functions for int64 arithmetic *)
     "__compcert_i64_dtos",
         (TInt(ILongLong, []),
@@ -989,6 +994,9 @@ let rec convertExpr env e =
       ewrap (Ctyping.eselection (convertExpr env arg1)
                                 (convertExpr env arg2) (convertExpr env arg3))
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, [arg1; arg2]) ->
+      convertExpr env arg1
+
   | C.ECall({edesc = C.EVar {name = "printf"}}, args)
     when !Clflags.option_interp ->
       let targs = convertTypArgs env [] args

common/Builtins0.v

@@ -341,6 +341,7 @@ Inductive standard_builtin : Type :=
   | BI_i16_bswap
   | BI_i32_bswap
   | BI_i64_bswap
+  | BI_unreachable
   | BI_i64_umulh
   | BI_i64_smulh
   | BI_i64_sdiv
@@ -376,6 +377,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
  :: ("__builtin_bswap", BI_i32_bswap)
  :: ("__builtin_bswap32", BI_i32_bswap)
  :: ("__builtin_bswap64", BI_i64_bswap)
+ :: ("__builtin_unreachable", BI_unreachable)
  :: ("__compcert_i64_umulh", BI_i64_umulh)
  :: ("__compcert_i64_smulh", BI_i64_smulh)
  :: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -414,6 +416,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
       mksignature (Tlong :: nil) Tlong cc_default
   | BI_i16_bswap =>
       mksignature (Tint :: nil) Tint cc_default
+  | BI_unreachable =>
+      mksignature nil Tvoid cc_default
   | BI_i64_shl  | BI_i64_shr | BI_i64_sar =>
       mksignature (Tlong :: Tint :: nil) Tlong cc_default
   | BI_i64_dtos | BI_i64_dtou =>
@@ -448,6 +452,7 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
   | BI_i64_bswap =>
     mkbuiltin_n1t Tlong Tlong
                   (fun n => Int64.repr (decode_int (List.rev (encode_int 8%nat (Int64.unsigned n)))))
+  | BI_unreachable => mkbuiltin Tvoid (fun vargs => None) _ _
   | BI_i64_umulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
   | BI_i64_smulh => mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
   | BI_i64_sdiv => mkbuiltin_v2p Tlong Val.divls _ _

cparser/Cflow.ml

@@ -23,8 +23,12 @@ open Cutil
 module StringSet = Set.Make(String)
 
 (* Functions declared noreturn by the standard *)
+(* We also add our own "__builtin_unreachable" function because, currently,
+   it is difficult to attach attributes to a built-in function. *)
+
 let std_noreturn_functions =
-   ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit"]
+   ["longjmp";"exit";"_exit";"abort";"_Exit";"quick_exit";"thrd_exit";
+    "__builtin_unreachable"]
 
 (* Statements are abstracted as "flow transformers":
    functions from possible inputs to possible outcomes.

powerpc/Asmexpand.ml

@@ -793,6 +793,9 @@ let expand_builtin_inline name args res =
   (* no operation *)
   | "__builtin_nop", [], _ ->
       emit (Pori (GPR0, GPR0, Cint _0))
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* atomic operations *)
   | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
       (* Register constraints imposed by Machregs.v *)

riscV/Asmexpand.ml

@@ -646,8 +646,12 @@ let expand_builtin_inline name args res =
                         (fun rl ->
                           emit (Pmulw (rl, X a, X b));
                           emit (Pmulhuw (rh, X a, X b)))
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))

x86/Asmexpand.ml

@@ -487,9 +487,12 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
-  (* no operation *)
+  (* No operation *)
   | "__builtin_nop", [], _ ->
      emit Pnop
+  (* Optimization hint *)
+  | "__builtin_unreachable", [], _ ->
+     ()
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))