From 7171888446d3d4b47765cc21d982eb2045cd00cd Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 4 Apr 2019 16:27:52 +0200 Subject: some more progress on select --- mppa_k1c/Op.v | 15 ++-------- mppa_k1c/SelectOp.vp | 4 +-- mppa_k1c/SelectOpproof.v | 53 ++++++++++++++++++------------------ mppa_k1c/ValueAOp.v | 71 +++++++++++++++++++++++++++++++++++------------- 4 files changed, 84 insertions(+), 59 deletions(-) diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index c3ea4baf..e619b2f5 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -283,18 +283,9 @@ Definition eval_condition0 (cond: condition0) (v1: val) (m: mem): option bool := end. Definition eval_select (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := - match v0 with - | Vint i0 => - match v1 with - | Vint i1 => - match (eval_condition0 cond vselect m) with - | Some bval => - Vint (if bval then i1 else i0) - | None => Vundef - end - | _ => Vundef - end - | _ => Vundef + match v0, v1, (eval_condition0 cond vselect m) with + | Vint i0, Vint i1, Some bval => Vint (if bval then i1 else i0) + | _,_,_ => Vundef end. Definition eval_selectl (v0 : val) (v1 : val) (vselect : val) : val := diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 6d61e674..31e81093 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -283,7 +283,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then Eop Oselect (v0:::v1:::y0:::Enil) + then Eop (Oselect (Ccomp0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oor (e1:::e2:::Enil) | (Eop Oand ((Eop Oneg ((Eop (Ocmp (Ccompuimm Ceq zero0)) (y0:::Enil)):::Enil)):::v0:::Enil)), @@ -292,7 +292,7 @@ Nondetfunction or (e1: expr) (e2: expr) := if same_expr_pure y0 y1 && Int.eq zero0 Int.zero && Int.eq zero1 Int.zero - then Eop Oselect (v0:::v1:::y0:::Enil) + then Eop (Oselect (Ccompu0 Cne)) (v0:::v1:::y0:::Enil) else Eop Oor (e1:::e2:::Enil) | _, _ => Eop Oor (e1:::e2:::Enil) end. diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 20ba74a1..4af5ccfa 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -582,22 +582,22 @@ Proof. inv H2. inv H5. replace v8 with v4 in * by congruence. rename v4 into vselect. - destruct vselect; simpl; trivial. - rewrite (Val.and_commut _ v5). - destruct v5; simpl; trivial. - rewrite (Val.and_commut _ v9). - rewrite Val.or_commut. - destruct v9; simpl; trivial. - rewrite int_eq_commut. - destruct (Int.eq i1 Int.zero); simpl. - + rewrite Int.and_zero. - rewrite Int.or_commut. - rewrite Int.or_zero. + destruct vselect; simpl; trivial; + destruct v5; simpl; trivial; destruct v9; simpl; trivial; + destruct (Int.eq i1 Int.zero); simpl; trivial. + + rewrite Int.neg_zero. + rewrite Int.and_commut. rewrite Int.and_mone. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_zero. reflexivity. - + rewrite Int.and_mone. - rewrite Int.neg_zero. + + rewrite Int.neg_zero. + rewrite Int.and_commut. rewrite Int.and_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.or_commut. rewrite Int.or_zero. reflexivity. - (* select unsigned *) @@ -620,22 +620,23 @@ Proof. inv H2. inv H5. replace v8 with v4 in * by congruence. rename v4 into vselect. - destruct vselect; simpl; trivial. - rewrite (Val.and_commut _ v5). - destruct v5; simpl; trivial. - rewrite (Val.and_commut _ v9). - rewrite Val.or_commut. - destruct v9; simpl; trivial. - rewrite int_eq_commut. - destruct (Int.eq i1 Int.zero); simpl. - + rewrite Int.and_zero. - rewrite Int.or_commut. - rewrite Int.or_zero. + destruct vselect; simpl; trivial; + destruct v5; simpl; trivial; + destruct v9; simpl; trivial; + destruct (Int.eq i1 Int.zero); simpl; trivial. + + rewrite Int.neg_zero. + rewrite Int.and_commut. rewrite Int.and_mone. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_zero. reflexivity. - + rewrite Int.and_mone. - rewrite Int.neg_zero. + + rewrite Int.neg_zero. + rewrite Int.and_commut. rewrite Int.and_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.or_commut. rewrite Int.or_zero. reflexivity. - apply DEFAULT. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 122249a4..af685a5e 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -42,16 +42,36 @@ Definition eval_static_addressing (addr: addressing) (vl: list aval): aval := | _, _ => Vbot end. -Definition select (v0 v1 vselect : aval) : aval := - match vselect with - | I iselect => - if Int.eq Int.zero iselect - then binop_int (fun x0 x1 => x0) v0 v1 - else binop_int (fun x0 x1 => x1) v0 v1 +Definition eval_static_condition0 (cond : condition0) (v : aval) : abool := + match cond with + | Ccomp0 c => cmp_bool c v (I Int.zero) + | Ccompu0 c => cmpu_bool c v (I Int.zero) + | Ccompl0 c => cmpl_bool c v (L Int64.zero) + | Ccomplu0 c => cmplu_bool c v (L Int64.zero) + end. + +Definition eval_static_select (cond : condition0) (v0 v1 vselect : aval) : aval := + match eval_static_condition0 cond vselect with + | Just b => binop_int (fun x0 x1 => if b then x1 else x0) v0 v1 | _ => Vtop end. -Definition selectl (v0 v1 vselect : aval) : aval := +Definition eval_select2 (cond : condition0) (v0 : val) (v1 : val) (vselect : val) (m: mem) : val := + match (eval_condition0 cond vselect m), v0, v1 with + | Some bval, Vint i0, Vint i1 => Vint (if bval then i1 else i0) + | _,_,_ => Vundef + end. + +Lemma eval_select_to2: forall cond v0 v1 vselect m, + (eval_select cond v0 v1 vselect m) = + (eval_select2 cond v0 v1 vselect m). +Proof. + intros. + unfold eval_select2. + destruct v0; destruct v1; simpl; destruct (eval_condition0 cond vselect m); simpl; reflexivity. +Qed. + +Definition eval_static_selectl (v0 v1 vselect : aval) : aval := match vselect with | I iselect => if Int.eq Int.zero iselect @@ -60,7 +80,7 @@ Definition selectl (v0 v1 vselect : aval) : aval := | _ => Vtop end. -Definition selectf (v0 v1 vselect : aval) : aval := +Definition eval_static_selectf (v0 v1 vselect : aval) : aval := match vselect with | I iselect => if Int.eq Int.zero iselect @@ -69,7 +89,7 @@ Definition selectf (v0 v1 vselect : aval) : aval := | _ => Vtop end. -Definition selectfs (v0 v1 vselect : aval) : aval := +Definition eval_static_selectfs (v0 v1 vselect : aval) : aval := match vselect with | I iselect => if Int.eq Int.zero iselect @@ -202,10 +222,10 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoflong, v1::nil => singleoflong v1 | Osingleoflongu, v1::nil => singleoflongu v1 | Ocmp c, _ => of_optbool (eval_static_condition c vl) - | Oselect, v0::v1::vselect::nil => select v0 v1 vselect - | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect - | Oselectf, v0::v1::vselect::nil => selectf v0 v1 vselect - | Oselectfs, v0::v1::vselect::nil => selectfs v0 v1 vselect + | (Oselect cond), v0::v1::vselect::nil => eval_static_select cond v0 v1 vselect + | Oselectl, v0::v1::vselect::nil => eval_static_selectl v0 v1 vselect + | Oselectf, v0::v1::vselect::nil => eval_static_selectf v0 v1 vselect + | Oselectfs, v0::v1::vselect::nil => eval_static_selectfs v0 v1 vselect | _, _ => Vbot end. @@ -231,6 +251,15 @@ Proof. destruct cond; auto with va. Qed. +Theorem eval_static_condition0_sound: + forall cond varg m aarg, + vmatch bc varg aarg -> + cmatch (eval_condition0 cond varg m) (eval_static_condition0 cond aarg). +Proof. + intros until aarg; intro VM. + destruct cond; simpl; eauto with va. +Qed. + Lemma symbol_address_sound: forall id ofs, vmatch bc (Genv.symbol_address ge id ofs) (Ptr (Gl id ofs)). @@ -276,18 +305,22 @@ Theorem eval_static_operation_sound: list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_operation op aargs). Proof. - unfold eval_operation, eval_static_operation; intros; + unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros; destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. (* select *) - - inv H2; simpl; try constructor. - + destruct (Int.eq _ _); apply binop_int_sound; trivial. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption). + rewrite eval_select_to2. + unfold eval_select2. + inv Hcond; trivial; try constructor. + + apply binop_int_sound; assumption. + + destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_i. + + destruct (eval_condition0 cond a2 m); destruct a1; destruct a0; try apply vmatch_ifptr_undef. + apply vmatch_ifptr_i. (* selectl *) - inv H2; simpl; try constructor. + destruct (Int.eq _ _); apply binop_long_sound; trivial. -- cgit