start implementing expect as expr

7 files changed, 52 insertions, 43 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 91a4c104..dcebbb86 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -77,6 +77,7 @@ Inductive unary_operation : Type :=
   | Osingleoflongu: unary_operation.       (**r unsigned long to float32 *)
 
 Inductive binary_operation : Type :=
+  | Oexpect: typ -> binary_operation       (**r first value, second is expected*)
   | Oadd: binary_operation                 (**r integer addition *)
   | Osub: binary_operation                 (**r integer subtraction *)
   | Omul: binary_operation                 (**r integer multiplication *)
@@ -301,6 +302,7 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
 Definition eval_binop
             (op: binary_operation) (arg1 arg2: val) (m: mem): option val :=
   match op with
+  | Oexpect ty => Some (Val.normalize arg1 ty)
   | Oadd => Some (Val.add arg1 arg2)
   | Osub => Some (Val.sub arg1 arg2)
   | Omul => Some (Val.mul arg1 arg2)
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index 92ec45f2..8945cecf 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -64,6 +64,7 @@ Definition type_binop (op: binary_operation) : typ * typ * typ :=
   | Ocmpf _ => (Tfloat, Tfloat, Tint)
   | Ocmpfs _ => (Tsingle, Tsingle, Tint)
   | Ocmpl _ | Ocmplu _ => (Tlong, Tlong, Tint)
+  | Oexpect ty => (ty, ty, ty)
   end.
 
 Module RTLtypes <: TYPE_ALGEBRA.
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index c9a6d399..051225a4 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -34,6 +34,7 @@ let precedence = function
   | Ebinop((Oadd|Osub|Oaddf|Osubf|Oaddfs|Osubfs|Oaddl|Osubl), _, _) -> (12, LtoR)
   | Ebinop((Oshl|Oshr|Oshru|Oshll|Oshrl|Oshrlu), _, _) -> (11, LtoR)
   | Ebinop((Ocmp _|Ocmpu _|Ocmpf _|Ocmpfs _|Ocmpl _|Ocmplu _), _, _) -> (10, LtoR)
+  | Ebinop((Oexpect _), _, _) -> (9, LtoR)
   | Ebinop((Oand|Oandl), _, _) -> (8, LtoR)
   | Ebinop((Oxor|Oxorl), _, _) -> (7, LtoR)
   | Ebinop((Oor|Oorl), _, _) -> (6, LtoR)
@@ -89,6 +90,7 @@ let comparison_name = function
   | Cge -> ">="
 
 let name_of_binop = function
+  | Oexpect _ -> "expect"
   | Oadd -> "+"
   | Osub -> "-"
   | Omul -> "*"
diff --git a/backend/Selection.v b/backend/Selection.v
index 7ba8fe92..fcb14127 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -120,6 +120,7 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
 
 Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
   match op with
+  | Cminor.Oexpect ty => arg1
   | Cminor.Oadd => add arg1 arg2
   | Cminor.Osub => sub arg1 arg2
   | Cminor.Omul => mul arg1 arg2
@@ -244,7 +245,7 @@ Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
   match bf, args with
   | BI_platform b, _ =>
     SelectOp.platform_builtin b args
-  | BI_standard BI_expect, a1 ::: a2 ::: Enil => Some a1
+(*  | 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/Selectionaux.ml b/backend/Selectionaux.ml
index 26a79fd7..5a8bde8c 100644
--- a/backend/Selectionaux.ml
+++ b/backend/Selectionaux.ml
@@ -39,6 +39,7 @@ let cost_unop = function
   | Osingleoflong | Osingleoflongu -> assert false
 
 let cost_binop = function
+  | Oexpect _ -> 0
   | Oadd  | Osub -> 1
   | Omul -> 2
   | Odiv  | Odivu | Omod  | Omodu -> assert false
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 9e0f22cc..53600c7a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -310,46 +310,47 @@ Lemma eval_sel_binop:
   exists v', eval_expr tge sp e m le (sel_binop op a1 a2) v' /\ Val.lessdef v v'.
 Proof.
   destruct op; simpl; intros; FuncInv; try subst v.
-  apply eval_add; auto.
-  apply eval_sub; auto.
-  apply eval_mul; auto.
-  eapply eval_divs; eauto.
-  eapply eval_divu; eauto.
-  eapply eval_mods; eauto.
-  eapply eval_modu; eauto.
-  apply eval_and; auto.
-  apply eval_or; auto.
-  apply eval_xor; auto.
-  apply eval_shl; auto.
-  apply eval_shr; auto.
-  apply eval_shru; auto.
-  apply eval_addf; auto.
-  apply eval_subf; auto.
-  apply eval_mulf; auto.
-  apply eval_divf; auto.
-  apply eval_addfs; auto.
-  apply eval_subfs; auto.
-  apply eval_mulfs; auto.
-  apply eval_divfs; auto.
-  eapply eval_addl; eauto.
-  eapply eval_subl; eauto.
-  eapply eval_mull; eauto.
-  eapply eval_divls; eauto.
-  eapply eval_divlu; eauto.
-  eapply eval_modls; eauto.
-  eapply eval_modlu; eauto.
-  eapply eval_andl; eauto.
-  eapply eval_orl; eauto.
-  eapply eval_xorl; eauto.
-  eapply eval_shll; eauto.
-  eapply eval_shrl; eauto.
-  eapply eval_shrlu; eauto.
-  apply eval_comp; auto.
-  apply eval_compu; auto.
-  apply eval_compf; auto.
-  apply eval_compfs; auto.
-  exists v; split; auto. eapply eval_cmpl; eauto.
-  exists v; split; auto. eapply eval_cmplu; eauto.
+  - exists v1; split; trivial. apply Val.lessdef_normalize.
+  - apply eval_add; auto.
+  - apply eval_sub; auto.
+  - apply eval_mul; auto.
+  - eapply eval_divs; eauto.
+  - eapply eval_divu; eauto.
+  - eapply eval_mods; eauto.
+  - eapply eval_modu; eauto.
+  - apply eval_and; auto.
+  - apply eval_or; auto.
+  - apply eval_xor; auto.
+  - apply eval_shl; auto.
+  - apply eval_shr; auto.
+  - apply eval_shru; auto.
+  - apply eval_addf; auto.
+  - apply eval_subf; auto.
+  - apply eval_mulf; auto.
+  - apply eval_divf; auto.
+  - apply eval_addfs; auto.
+  - apply eval_subfs; auto.
+  - apply eval_mulfs; auto.
+  - apply eval_divfs; auto.
+  - eapply eval_addl; eauto.
+  - eapply eval_subl; eauto.
+  - eapply eval_mull; eauto.
+  - eapply eval_divls; eauto.
+  - eapply eval_divlu; eauto.
+  - eapply eval_modls; eauto.
+  - eapply eval_modlu; eauto.
+  - eapply eval_andl; eauto.
+  - eapply eval_orl; eauto.
+  - eapply eval_xorl; eauto.
+  - eapply eval_shll; eauto.
+  - eapply eval_shrl; eauto.
+  - eapply eval_shrlu; eauto.
+  - apply eval_comp; auto.
+  - apply eval_compu; auto.
+  - apply eval_compf; auto.
+  - apply eval_compfs; auto.
+  - exists v; split; auto. eapply eval_cmpl; eauto.
+  - exists v; split; auto. eapply eval_cmplu; eauto.
 Qed.
 
 Lemma eval_sel_select:
@@ -395,13 +396,13 @@ Proof.
   inv ARGS; try discriminate. inv H0; try discriminate.
   inv SEL.  
   simpl in SEM; inv SEM. apply eval_absf; auto.
-+ (* expect *)
+  (* + (* 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.
+  all: econstructor; split; eauto. *)
 - eapply eval_platform_builtin; eauto.
 Qed.
 
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.