Merge remote-tracking branch 'origin/mppa-expect3' into mppa-work

9 files changed, 86 insertions, 45 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index f637b5e4..75f5eb3e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -181,9 +181,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);
@@ -912,6 +913,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/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 5acb996d..744df818 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1335,6 +1335,7 @@ Lemma eval_binop_compat:
   /\ Val.inject f v tv.
 Proof.
   destruct op; simpl; intros; inv H.
+- TrivialExists. apply Val.normalize_inject; auto.
 - TrivialExists. apply Val.add_inject; auto.
 - TrivialExists. apply Val.sub_inject; auto.
 - TrivialExists. inv H0; inv H1; constructor.
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 143e87a3..47a02851 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -33,6 +33,7 @@ Inductive unary_operation : Type :=
   | Oabsfloat : unary_operation.        (**r floating-point absolute value *)
 
 Inductive binary_operation : Type :=
+  | Oexpect : binary_operation          (**r return first argument *)
   | Oadd : binary_operation             (**r addition (binary [+]) *)
   | Osub : binary_operation             (**r subtraction (binary [-]) *)
   | Omul : binary_operation             (**r multiplication (binary [*]) *)
@@ -763,6 +764,14 @@ Definition sem_mul (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :
     (fun n1 n2 => Some(Vsingle(Float32.mul n1 n2)))
     v1 t1 v2 t2 m.
 
+Definition sem_expect (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
+  sem_binarith
+    (fun sg n1 n2 => Some(Vint n1))
+    (fun sg n1 n2 => Some(Vlong n1))
+    (fun n1 n2 => Some(Vfloat n1))
+    (fun n1 n2 => Some(Vsingle n1))
+    v1 t1 v2 t2 m.
+
 Definition sem_div (v1:val) (t1:type) (v2: val) (t2:type) (m:mem) : option val :=
   sem_binarith
     (fun sg n1 n2 =>
@@ -1050,6 +1059,7 @@ Definition sem_binary_operation
     (v1: val) (t1: type) (v2: val) (t2:type)
     (m: mem): option val :=
   match op with
+  | Oexpect => sem_expect v1 t1 v2 t2 m
   | Oadd => sem_add cenv v1 t1 v2 t2 m
   | Osub => sem_sub cenv v1 t1 v2 t2 m
   | Omul => sem_mul v1 t1 v2 t2 m
@@ -1290,6 +1300,9 @@ Lemma sem_binary_operation_inj:
   exists tv, sem_binary_operation cenv op tv1 ty1 tv2 ty2 m' = Some tv /\ Val.inject f v tv.
 Proof.
   unfold sem_binary_operation; intros; destruct op.
+- (* expect *)
+  unfold sem_expect in *.
+  eapply sem_binarith_inject; eauto; intros; exact I.
 - (* add *)
   assert (A: forall cenv ty si v1' v2' tv1' tv2',
              Val.inject f v1' tv1' -> Val.inject f v2' tv2' ->
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 5bd12d00..f78b52ae 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -259,6 +259,11 @@ Definition make_add_ptr_long (ce: composite_env) (ty: type) (e1 e2: expr) :=
     let n := make_intconst (Int.repr sz) in
     OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2))).
 
+Definition make_expect (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  make_binarith (Oexpect AST.Tint) (Oexpect AST.Tint)
+                (Oexpect AST.Tfloat) (Oexpect AST.Tsingle)
+                (Oexpect AST.Tlong) (Oexpect AST.Tlong) e1 ty1 e2 ty2.
+
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
   | add_case_pi ty si => make_add_ptr_int ce ty si e1 e2
@@ -421,6 +426,7 @@ Definition transl_binop (ce: composite_env)
                         (a: expr) (ta: type)
                         (b: expr) (tb: type) : res expr :=
   match op with
+  | Cop.Oexpect => make_expect a ta b tb
   | Cop.Oadd => make_add ce a ta b tb
   | Cop.Osub => make_sub ce a ta b tb
   | Cop.Omul => make_mul a ta b tb
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1ceb8e4d..c5ba19d5 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -619,6 +619,11 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
+Lemma make_expect_correct: binary_constructor_correct make_expect sem_expect.
+Proof.
+  apply make_binarith_correct; intros; auto.
+Qed.
+
 Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
   assert (A: forall ty si a b c e le m va vb v,
@@ -922,22 +927,23 @@ Lemma transl_binop_correct:
   eval_expr ge e le m c v.
 Proof.
   intros. destruct op; simpl in *.
-  eapply make_add_correct; eauto.
-  eapply make_sub_correct; eauto.
-  eapply make_mul_correct; eauto.
-  eapply make_div_correct; eauto.
-  eapply make_mod_correct; eauto.
-  eapply make_and_correct; eauto.
-  eapply make_or_correct; eauto.
-  eapply make_xor_correct; eauto.
-  eapply make_shl_correct; eauto.
-  eapply make_shr_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
-  eapply make_cmp_correct; eauto.
+- eapply make_expect_correct; eauto.
+- eapply make_add_correct; eauto.
+- eapply make_sub_correct; eauto.
+- eapply make_mul_correct; eauto.
+- eapply make_div_correct; eauto.
+- eapply make_mod_correct; eauto.
+- eapply make_and_correct; eauto.
+- eapply make_or_correct; eauto.
+- eapply make_xor_correct; eauto.
+- eapply make_shl_correct; eauto.
+- eapply make_shr_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
+- eapply make_cmp_correct; eauto.
 Qed.
 
 Lemma make_load_correct:
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index 00fcf8ab..bde4001f 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -111,6 +111,7 @@ Definition comparison_type (ty1 ty2: type) (m: string): res type :=
 
 Definition type_binop (op: binary_operation) (ty1 ty2: type) : res type :=
   match op with
+  | Oexpect => binarith_type ty1 ty2 "__builtin_expect"
   | Oadd =>
       match classify_add ty1 ty2 with
       | add_case_pi ty _ | add_case_ip _ ty
@@ -1546,6 +1547,8 @@ Lemma pres_sem_binop:
 Proof.
   intros until m; intros TY SEM WT1 WT2.
   destruct op; simpl in TY; simpl in SEM.
+- (* expect *)
+  unfold sem_expect in SEM. eapply pres_sem_binarith; eauto; intros; exact I.    
 - (* add *)
   unfold sem_add, sem_add_ptr_int, sem_add_ptr_long in SEM; DestructCases; auto with ty.
   eapply pres_sem_binarith; eauto; intros; exact I.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 0e735d2d..0aefde31 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -62,6 +62,7 @@ let precedence = function
   | Ebinop(Oand, _, _, _) -> (8, LtoR)
   | Ebinop(Oxor, _, _, _) -> (7, LtoR)
   | Ebinop(Oor, _, _, _) -> (6, LtoR)
+  | Ebinop(Oexpect, _, _, _) -> (5, LtoR)
 
 (* Expressions *)
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 03dc5837..beca056f 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -30,6 +30,7 @@ let name_unop = function
   | Oabsfloat -> "__builtin_fabs"
 
 let name_binop = function
+  | Oexpect -> "expect"
   | Oadd -> "+"
   | Osub -> "-"
   | Omul -> "*"
@@ -158,6 +159,7 @@ let rec precedence = function
   | Ebinop(Oand, _, _, _) -> (8, LtoR)
   | Ebinop(Oxor, _, _, _) -> (7, LtoR)
   | Ebinop(Oor, _, _, _) -> (6, LtoR)
+  | Ebinop(Oexpect, _, _, _) -> (5, LtoR) (* fixme *)
   | Eseqand _ -> (5, LtoR)
   | Eseqor _ -> (4, LtoR)
   | Econdition _ -> (3, RtoL)
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.