From c420bc8d3b87d71c38209b5ab8bca22875466362 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 25 Sep 2019 21:31:57 +0200
Subject: __builtin_expect defined as its first argument

---
 backend/Selection.v               | 3 ++-
 backend/Selectionproof.v          | 7 +++++++
 cfrontend/C2C.ml                  | 5 +++--
 common/Builtins0.v                | 8 +++++++-
 runtime/include/ccomp_k1c_fixes.h | 2 +-
 5 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/backend/Selection.v b/backend/Selection.v
index 4ab3331e..7ba8fe92 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -243,7 +243,8 @@ Definition sel_builtin_res (optid: option ident) : builtin_res ident :=
 Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
   match bf, args with
   | BI_platform b, _ =>
-      SelectOp.platform_builtin b args
+    SelectOp.platform_builtin b args
+  | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1
   | BI_standard (BI_select ty), a1 ::: a2 ::: a3 ::: Enil =>
       Some (sel_select ty a1 a2 a3)
   | BI_standard BI_fabs, a1 ::: Enil =>
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 8a827af2..0be96167 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -395,6 +395,13 @@ Proof.
   inv ARGS; try discriminate. inv H0; try discriminate.
   inv SEL.  
   simpl in SEM; inv SEM. apply eval_absf; auto.
++ (* expect *)
+  inv ARGS; try discriminate.
+  inv H0; try discriminate.
+  inv H2; try discriminate.
+  simpl in SEM. inv SEM. inv SEL.
+  destruct v1; destruct v0.
+  all: econstructor; split; eauto.
 - eapply eval_platform_builtin; eauto.
 Qed.
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index dc25b516..421c4b07 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -157,9 +157,10 @@ let ais_annot_functions =
 let builtins_generic = {
   builtin_typedefs = [];
   builtin_functions =
-    ais_annot_functions
-      @
+    ais_annot_functions @
     [
+    "__builtin_expect",
+    (TInt(ILong, []), [TInt(ILong, []); TInt(ILong, [])], false);
     (* Integer arithmetic *)
     "__builtin_bswap64",
     (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
diff --git a/common/Builtins0.v b/common/Builtins0.v
index b78006dd..5061bf43 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -337,6 +337,7 @@ Inductive standard_builtin : Type :=
   | BI_addl
   | BI_subl
   | BI_mull
+  | BI_expect
   | BI_i16_bswap
   | BI_i32_bswap
   | BI_i64_bswap
@@ -373,6 +374,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_expect", BI_expect)
  :: ("__compcert_i64_umulh", BI_i64_umulh)
  :: ("__compcert_i64_smulh", BI_i64_smulh)
  :: ("__compcert_i64_sdiv", BI_i64_sdiv)
@@ -402,7 +404,9 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
   | BI_i64_sdiv | BI_i64_udiv | BI_i64_smod | BI_i64_umod =>
       mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
   | BI_mull =>
-      mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+    mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default
+  | BI_expect =>
+    mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default
   | BI_i32_bswap =>
       mksignature (Tint :: nil) (Some Tint) cc_default
   | BI_i64_bswap =>
@@ -433,6 +437,8 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (pro
   | BI_addl => mkbuiltin_v2t Tlong Val.addl _ _ 
   | BI_subl => mkbuiltin_v2t Tlong Val.subl _ _
   | BI_mull => mkbuiltin_v2t Tlong Val.mull' _ _
+  | BI_expect =>
+    mkbuiltin_n2t Tlong Tlong Tlong (fun x _ => x)
   | BI_i16_bswap =>
     mkbuiltin_n1t Tint Tint
                   (fun n => Int.repr (decode_int (List.rev (encode_int 2%nat (Int.unsigned n)))))
diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h
index 718ac3e5..f3fa11fe 100644
--- a/runtime/include/ccomp_k1c_fixes.h
+++ b/runtime/include/ccomp_k1c_fixes.h
@@ -25,6 +25,6 @@ extern long long __compcert_afaddd(void *address, unsigned long long incr);
 extern int __compcert_afaddw(void *address, unsigned int incr);
 #endif
 
-#define __builtin_expect(x, y) (x)
+/* #define __builtin_expect(x, y) (x) */
 #define __builtin_ctz(x) __builtin_k1_ctzw(x)
 #define __builtin_clz(x) __builtin_k1_clzw(x)
-- 
cgit