diff options
Diffstat (limited to 'riscV/ValueAOp.v')
| -rw-r--r-- | riscV/ValueAOp.v | 197 |
1 files changed, 113 insertions, 84 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index ca0834db..e0314c6a 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -19,30 +19,38 @@ Require Import Zbits Lia. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). - -Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := - match optR0 with + +(** Functions to select a special register (see Op.v) *) + +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + match optR with | None => sem v1 v2 - | Some true => sem vz v1 - | Some false => sem v1 vz + | Some X0_L => sem vz v1 + | Some X0_R => sem v1 vz end. -Definition may_undef_int (is_long: bool) (sem: aval -> aval -> aval) (v1 vimm vz: aval): aval := - if negb is_long then - match v1 with - | I _ => sem vimm vz - | _ => Ifptr Ptop - end - else - match v1 with - | L _ => sem vimm vz - | _ => Ifptr Ptop - end. - -Definition may_undef_luil (v1: aval) (n: int64): aval := - match v1 with - | L _ => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | _ => Ifptr Ptop +Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := + match mu with + | MUint => match v1, v2 with + | I _, I _ => v2 + | _, _ => Ifptr Ptop + end + | MUlong => match v1, v2 with + | L _, I _ => v2 + | _, _ => Ifptr Ptop + end + | MUshrx i => + match v1, v2 with + | I _, I _ => + if Int.ltu i (Int.repr 31) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop + end + | MUshrxl i => + match v1, v2 with + | L _, L _ => + if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop + end end. Definition eval_static_condition (cond: condition) (vl: list aval): abool := @@ -59,22 +67,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool := | Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2) | Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2 | Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2) - | CEbeqw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32 - | CEbnew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32 - | CEbequw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32 - | CEbneuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32 - | CEbltw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32 - | CEbltuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32 - | CEbgew optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmp_bool Cge) v1 v2 zero32 - | CEbgeuw optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpu_bool Cge) v1 v2 zero32 - | CEbeql optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64 - | CEbnel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64 - | CEbequl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64 - | CEbneul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64 - | CEbltl optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64 - | CEbltul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64 - | CEbgel optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmpl_bool Cge) v1 v2 zero64 - | CEbgeul optR0, v1 :: v2 :: nil => apply_bin_r0 optR0 (cmplu_bool Cge) v1 v2 zero64 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 | _, _ => Bnone end. @@ -214,29 +222,36 @@ 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) - | OEseqw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Ceq) v1 v2 zero32) - | OEsnew optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Cne) v1 v2 zero32) - | OEsequw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Ceq) v1 v2 zero32) - | OEsneuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Cne) v1 v2 zero32) - | OEsltw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmp_bool Clt) v1 v2 zero32) - | OEsltuw optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpu_bool Clt) v1 v2 zero32) + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32) | OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n)) | OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n)) | OExoriw n, v1::nil => xor v1 (I n) - | OEluiw n is_long, v1::nil => may_undef_int is_long shl v1 (I n) (I (Int.repr 12)) - | OEaddiwr0 n is_long, v1::nil => may_undef_int is_long add v1 (I n) zero32 - | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64) - | OEsnel optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Cne) v1 v2 zero64) - | OEsequl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Ceq) v1 v2 zero64) - | OEsneul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Cne) v1 v2 zero64) - | OEsltl optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Clt) v1 v2 zero64) - | OEsltul optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmplu_bool Clt) v1 v2 zero64) + | OEluiw n, nil => shl (I n) (I (Int.repr 12)) + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (I n) (Ifptr Ptop) + | OEandiw n, v1::nil => and (I n) v1 + | OEoriw n, v1::nil => or (I n) v1 + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64) | OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n)) | OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n)) + | OEandil n, v1::nil => andl (L n) v1 + | OEoril n, v1::nil => orl (L n) v1 | OExoril n, v1::nil => xorl v1 (L n) - | OEluil n, v1::nil => may_undef_luil v1 n - | OEaddilr0 n, v1::nil => may_undef_int true addl v1 (L n) zero64 + | OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (L n) (Ifptr Ptop) | OEloadli n, nil => L (n) + | OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2 | OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2) | OEfltd, v1::v2::nil => of_optbool (cmpf_bool Clt v1 v2) | OEfled, v1::v2::nil => of_optbool (cmpf_bool Cle v1 v2) @@ -340,7 +355,7 @@ Proof. inv H2. destruct cond; simpl; eauto with va. 17: destruct cond; simpl; eauto with va. - all: destruct optR0 as [[]|]; unfold apply_bin_r0, Op.apply_bin_r0; + all: destruct optR as [[]|]; unfold apply_bin_oreg, Op.apply_bin_oreg; unfold zero32, Op.zero32, zero64, Op.zero64; eauto with va. Qed. @@ -397,53 +412,53 @@ Proof. inv H; auto. simpl. destruct b; constructor. Qed. -Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmpu_bool c) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR0 m, +Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, c = Ceq \/ c = Cne \/ c = Clt-> vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc (Val.maketotal - (Op.apply_bin_r0 optR0 (Val.cmplu (Mem.valid_pointer m) c) a1 a0 + (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmplu_bool c) b1 b0 zero64)). + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. -Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - vmatch bc (Op.apply_bin_r0 optR0 (Val.cmp cmp) a1 a0 Op.zero32) - (of_optbool (apply_bin_r0 optR0 (cmp_bool cmp) b1 b0 zero32)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_sound; unfold Op.zero32, zero32; eauto with va. Qed. -Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR0 cmp, +Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> vmatch bc - (Val.maketotal (Op.apply_bin_r0 optR0 (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_r0 optR0 (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). Proof. intros. - destruct optR0 as [[]|]; unfold Op.apply_bin_r0, apply_bin_r0; + destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; apply of_optbool_maketotal_sound; unfold Op.zero64, zero64; eauto with va. Qed. @@ -459,24 +474,38 @@ Proof. destruct (propagate_float_constants tt); constructor. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - + 3,4,6: apply eval_cmpu_sound; auto. 1,2,3: apply eval_cmp_sound; auto. unfold Val.cmp; apply of_optbool_sound; eauto with va. unfold Val.cmpu; apply of_optbool_sound; eauto with va. - unfold zero32; simpl; eauto with va. - - 1,2,11,12: - try unfold Op.may_undef_int, may_undef_int, Op.zero32, zero32, Op.zero64, zero64; - try unfold Op.may_undef_luil, may_undef_luil; simpl; unfold ntop1; - inv H1; try destruct is_long; simpl; try destruct (Int.ltu _ _); eauto with va; - try apply vmatch_ifptr_i; try apply vmatch_ifptr_l. - - 3,4,6: apply eval_cmplu_sound; auto. - 1,2,3: apply eval_cmpl_sound; auto. - unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. - unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. - unfold zero64; simpl; eauto with va. + + { destruct optR as [[]|]; simpl; eauto with va. } + { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } + { fold (Val.and (Vint n) a1); eauto with va. } + { fold (Val.or (Vint n) a1); eauto with va. } + { simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1; + try apply vmatch_ifptr_undef. } + 9: { destruct optR as [[]|]; simpl; eauto with va. } + 9: { destruct optR as [[]|]; + unfold apply_bin_oreg, Op.apply_bin_oreg; eauto with va. } + 9: { fold (Val.andl (Vlong n) a1); eauto with va. } + 9: { fold (Val.orl (Vlong n) a1); eauto with va. } + 9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl; + apply vmatch_ifptr_l. } + + 1,10: simpl; eauto with va. + 10: + unfold Op.eval_may_undef, eval_may_undef; destruct mu; + inv H1; inv H0; eauto with va; + try destruct (Int.ltu _ _); simpl; + try eapply vmatch_ifptr_p, pmatch_top'; eauto with va. + + 4,5,7: apply eval_cmplu_sound; auto. + 1,3,4: apply eval_cmpl_sound; auto. + 2: { unfold Val.cmpl; apply of_optbool_maketotal_sound; eauto with va. } + 2: { unfold Val.cmplu; apply of_optbool_maketotal_sound; eauto with va. } all: unfold Val.cmpf; apply of_optbool_sound; eauto with va. Qed. |