diff options
Diffstat (limited to 'arm')
-rw-r--r-- | arm/ConstpropOp.vp | 14 | ||||
-rw-r--r-- | arm/ConstpropOpproof.v | 28 | ||||
-rw-r--r-- | arm/ValueAOp.v | 4 |
3 files changed, 23 insertions, 23 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp index 4f4bf5aa..872493a6 100644 --- a/arm/ConstpropOp.vp +++ b/arm/ConstpropOp.vp @@ -96,12 +96,12 @@ Definition make_cmp_base (c: condition) (args: list reg) (vl: list aval) := Nondetfunction make_cmp (c: condition) (args: list reg) (vl: list aval) := match c, args, vl with | Ccompimm Ceq n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | Ccompimm Cne n, r1 :: nil, v1 :: nil => - if Int.eq_dec n Int.zero && vincl v1 (Uns 1) then (Omove, r1 :: nil) - else if Int.eq_dec n Int.one && vincl v1 (Uns 1) then (Oxorimm Int.one, r1 :: nil) + if Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1) then (Omove, r1 :: nil) + else if Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1) then (Oxorimm Int.one, r1 :: nil) else make_cmp_base c args vl | _, _, _ => make_cmp_base c args vl @@ -164,7 +164,7 @@ Definition make_divuimm (n: int) (r1 r2: reg) := Definition make_andimm (n: int) (r: reg) (a: aval) := if Int.eq n Int.zero then (Ointconst Int.zero, nil) else if Int.eq n Int.mone then (Omove, r :: nil) - else if match a with Uns m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero + else if match a with Uns _ m => Int.eq (Int.zero_ext m (Int.not n)) Int.zero | _ => false end then (Omove, r :: nil) else (Oandimm n, r :: nil). @@ -190,9 +190,9 @@ Definition make_mulfsimm (n: float32) (r r1 r2: reg) := else (Omulfs, r1 :: r2 :: nil). Definition make_cast8signed (r: reg) (a: aval) := - if vincl a (Sgn 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). + if vincl a (Sgn Ptop 8) then (Omove, r :: nil) else (Ocast8signed, r :: nil). Definition make_cast16signed (r: reg) (a: aval) := - if vincl a (Sgn 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). + if vincl a (Sgn Ptop 16) then (Omove, r :: nil) else (Ocast16signed, r :: nil). Nondetfunction op_strength_reduction (op: operation) (args: list reg) (vl: list aval) := diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index 597c9602..fa20d17e 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -163,24 +163,24 @@ Lemma make_cmp_correct: /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. - assert (Y: forall r, vincl (AE.get r ae) (Uns 1) = true -> + assert (Y: forall r, vincl (AE.get r ae) (Uns Ptop 1) = true -> rs#r = Vundef \/ rs#r = Vint Int.zero \/ rs#r = Vint Int.one). - { intros. apply vmatch_Uns_1 with bc. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } + { intros. apply vmatch_Uns_1 with bc Ptop. eapply vmatch_ge. eapply vincl_ge; eauto. apply MATCH. } unfold make_cmp. case (make_cmp_match c args vl); intros. -- destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. +- destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. + destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. apply make_cmp_base_correct; auto. -- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns 1)) eqn:E0. +- destruct (Int.eq_dec n Int.zero && vincl v1 (Uns Ptop 1)) eqn:E0. simpl in H; inv H. InvBooleans. subst n. exists (rs#r1); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. - destruct (Int.eq_dec n Int.one && vincl v1 (Uns 1)) eqn:E1. + destruct (Int.eq_dec n Int.one && vincl v1 (Uns Ptop 1)) eqn:E1. simpl in H; inv H. InvBooleans. subst n. exists (Val.xor rs#r1 (Vint Int.one)); split; auto. simpl. exploit Y; eauto. intros [A | [A | A]]; rewrite A; simpl; auto. @@ -302,7 +302,7 @@ Proof. subst n. exists (Vint Int.zero); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_zero; auto. predSpec Int.eq Int.eq_spec n Int.mone; intros. subst n. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.and_mone; auto. - destruct (match x with Uns k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero + destruct (match x with Uns _ k => Int.eq (Int.zero_ext k (Int.not n)) Int.zero | _ => false end) eqn:UNS. destruct x; try congruence. exists (rs#r); split; auto. @@ -313,7 +313,7 @@ Proof. rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. - rewrite H5 by auto. auto. + rewrite H6 by auto. auto. econstructor; split; eauto. auto. Qed. @@ -404,11 +404,11 @@ Lemma make_cast8signed_correct: let (op, args) := make_cast8signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. - intros; unfold make_cast8signed. destruct (vincl x (Sgn 8)) eqn:INCL. + intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 8)). + assert (V: vmatch bc rs#r (Sgn Ptop 8)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. @@ -418,11 +418,11 @@ Lemma make_cast16signed_correct: let (op, args) := make_cast16signed r x in exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. - intros; unfold make_cast16signed. destruct (vincl x (Sgn 16)) eqn:INCL. + intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. - assert (V: vmatch bc rs#r (Sgn 16)). + assert (V: vmatch bc rs#r (Sgn Ptop 16)). { eapply vmatch_ge; eauto. apply vincl_ge; auto. } - inv V; simpl; auto. rewrite is_sgn_sign_ext in H3 by auto. rewrite H3; auto. + inv V; simpl; auto. rewrite is_sgn_sign_ext in H4 by auto. rewrite H4; auto. econstructor; split; simpl; eauto. Qed. diff --git a/arm/ValueAOp.v b/arm/ValueAOp.v index a14d6b98..b388bf12 100644 --- a/arm/ValueAOp.v +++ b/arm/ValueAOp.v @@ -64,8 +64,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with | Omove, v1::nil => v1 | Ointconst n, nil => I n - | Ofloatconst n, nil => if propagate_float_constants tt then F n else ftop - | Osingleconst n, nil => if propagate_float_constants tt then FS n else ftop + | Ofloatconst n, nil => if propagate_float_constants tt then F n else ntop + | Osingleconst n, nil => if propagate_float_constants tt then FS n else ntop | Oaddrsymbol id ofs, nil => Ptr (Gl id ofs) | Oaddrstack ofs, nil => Ptr (Stk ofs) | Ocast8signed, v1 :: nil => sign_ext 8 v1 |