From 249482aed76d209ff203f9afeeb3f10db004e8c0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 7 Apr 2020 21:34:14 +0200 Subject: start implementing expect as expr --- backend/Cminor.v | 2 ++ backend/Cminortyping.v | 1 + backend/PrintCminor.ml | 2 ++ backend/Selection.v | 3 +- backend/Selectionaux.ml | 1 + backend/Selectionproof.v | 85 +++++++++++++++++++++++----------------------- cfrontend/Cminorgenproof.v | 1 + 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. -- cgit