expect operation

3 files changed, 41 insertions, 33 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 9f2c4604..902a5c5d 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -900,6 +900,14 @@ let rec convertExpr env e =
   | C.ECompound(ty1, ie) ->
       unsupported "compound literals"; ezero
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_expect"}}, args) ->
+     (match args with
+      | [e1; e2] ->
+         ewrap (Ctyping.ebinop Cop.Oexpect (convertExpr env e1) (convertExpr env e2))
+      | _ -> 
+       error "__builtin_expect wants two arguments";
+       ezero)
+
   | C.ECall({edesc = C.EVar {name = "__builtin_debug"}}, args) when List.length args < 2 ->
       error "too few arguments to function call, expected at least 2, have 0";
       ezero
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index e7d57a1c..95e3957c 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -770,53 +770,53 @@ Proof.
 (* val *)
   simpl in H. destruct v; monadInv H; exists (@nil ident); split; auto with gensym.
 Opaque makeif.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
-  intros. destruct dst; simpl in *; inv H2.
+- intros. destruct dst; simpl in *; inv H2.
     constructor. auto. intros; constructor.
     constructor.
     constructor. auto. intros; constructor.
 (* var *)
-  monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
+- monadInv H; econstructor; split; auto with gensym. UseFinish. constructor.
 (* field *)
-  monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. auto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* valof *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   exploit transl_valof_meets_spec; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
 (* deref *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* addrof *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. econstructor; eauto.
 (* unop *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* binop *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]]. UseFinish.
   exists (tmp1 ++ tmp2); split.
   intros; apply tr_expr_add_dest. econstructor; eauto with gensym.
   eauto with gensym.
 (* cast *)
-  monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
+- monadInv H0. exploit H; eauto. intros [tmp [A B]]. UseFinish.
   econstructor; split; eauto. intros; apply tr_expr_add_dest. constructor; auto.
 (* seqand *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
@@ -840,7 +840,7 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* seqor *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
@@ -864,7 +864,7 @@ Opaque makeif.
   apply list_disjoint_cons_r; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* condition *)
-  monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H2. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0.
   (* for value *)
   exploit H0; eauto with gensym. intros [tmp2 [C D]].
@@ -896,13 +896,13 @@ Opaque makeif.
   apply contained_app; eauto with gensym.
   apply contained_app; eauto with gensym.
 (* sizeof *)
-  monadInv H. UseFinish.
+- monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
 (* alignof *)
-  monadInv H. UseFinish.
+- monadInv H. UseFinish.
   exists (@nil ident); split; auto with gensym. constructor.
 (* assign *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
@@ -921,7 +921,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* assignop *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exploit transl_valof_meets_spec; eauto. intros [tmp3 [E F]].
   destruct dst; monadInv EQ3; simpl add_dest in *.
@@ -941,7 +941,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* postincr *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
   (* for value *)
   exists (x0 :: tmp1); split.
@@ -958,7 +958,7 @@ Opaque makeif.
   econstructor; eauto with gensym.
   apply contained_cons; eauto with gensym.
 (* comma *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto with gensym. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
@@ -968,7 +968,7 @@ Opaque makeif.
   destruct dst; simpl; auto with gensym.
   apply contained_app; eauto with gensym.
 (* call *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   destruct dst; monadInv EQ2; simpl add_dest in *.
   (* for value *)
@@ -986,7 +986,7 @@ Opaque makeif.
   apply contained_cons. eauto with gensym.
   apply contained_app; eauto with gensym.
 (* builtin *)
-  monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H0. exploit H; eauto. intros [tmp1 [A B]].
   destruct dst; monadInv EQ0; simpl add_dest in *.
   (* for value *)
   exists (x0 :: tmp1); split.
@@ -1001,13 +1001,13 @@ Opaque makeif.
   repeat rewrite app_ass. econstructor; eauto with gensym. congruence.
   apply contained_cons; eauto with gensym.
 (* loc *)
-  monadInv H.
+- monadInv H.
 (* paren *)
-  monadInv H0.
+- monadInv H0.
 (* nil *)
-  monadInv H; exists (@nil ident); split; auto with gensym. constructor.
+- monadInv H; exists (@nil ident); split; auto with gensym. constructor.
 (* cons *)
-  monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
+- monadInv H1. exploit H; eauto. intros [tmp1 [A B]].
   exploit H0; eauto. intros [tmp2 [Csyntax D]].
   exists (tmp1 ++ tmp2); split.
   econstructor; eauto with gensym.
diff --git a/common/Builtins0.v b/common/Builtins0.v
index a3215545..f72febf8 100644
--- a/common/Builtins0.v
+++ b/common/Builtins0.v
@@ -337,7 +337,7 @@ Inductive standard_builtin : Type :=
   | BI_addl
   | BI_subl
   | BI_mull
-  | BI_expect
+(*  | BI_expect *)
   | BI_i16_bswap
   | BI_i32_bswap
   | BI_i64_bswap
@@ -370,7 +370,7 @@ Definition standard_builtin_table : list (string * standard_builtin) :=
  :: ("__builtin_addl", BI_addl)
  :: ("__builtin_subl", BI_subl)
  :: ("__builtin_mull", BI_mull)
- :: ("__builtin_expect", BI_expect)
+(* :: ("__builtin_expect", BI_expect) *)
  :: ("__builtin_bswap16", BI_i16_bswap)
  :: ("__builtin_bswap", BI_i32_bswap)
  :: ("__builtin_bswap32", BI_i32_bswap)
@@ -405,8 +405,8 @@ Definition standard_builtin_sig (b: standard_builtin) : signature :=
       mksignature (Tlong :: Tlong :: nil) Tlong cc_default
   | BI_mull =>
       mksignature (Tint :: Tint :: nil) Tlong cc_default
-  | BI_expect =>
-    mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+(*  | BI_expect =>
+    mksignature (Tlong :: Tlong :: nil) Tlong cc_default *)
   | BI_i32_bswap =>
       mksignature (Tint :: nil) Tint cc_default
   | BI_i64_bswap =>
@@ -437,8 +437,8 @@ Program Definition standard_builtin_sem (b: standard_builtin) : builtin_sem (sig
   | 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_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)))))