diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-06 23:37:22 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-06 23:37:22 +0200 |
commit | dd4767e17235adb5de922626ed1fea15f4eb9e3b (patch) | |
tree | 37843b101add33cf6ea56e055ddae2df96c6dc67 /riscV/ValueAOp.v | |
parent | df9aab806ae8d20393b56e4175e210ed6cff1ef1 (diff) | |
download | compcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.tar.gz compcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.zip |
Important commit on expansions' mini CSE, and a draft for addptrofs
Diffstat (limited to 'riscV/ValueAOp.v')
-rw-r--r-- | riscV/ValueAOp.v | 133 |
1 files changed, 68 insertions, 65 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v index e48c4a5b..3ba2732d 100644 --- a/riscV/ValueAOp.v +++ b/riscV/ValueAOp.v @@ -19,44 +19,41 @@ Require Import Zbits. Definition zero32 := (I Int.zero). Definition zero64 := (L Int64.zero). - -Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B := + +(** Functions to select a special register (see Op.v) *) + +Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B := match optR with | None => sem v1 v2 | Some X0_L => sem vz v1 | Some X0_R => sem v1 vz + | Some SP_S => sem v1 sp end. Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval := match mu with - | MUint => match v1 with - | I _ => v2 - | _ => Ifptr Ptop + | MUint => match v1, v2 with + | I _, I _ => v2 + | _, _ => Ifptr Ptop end - | MUlong => match v1 with - | L _ => v2 - | _ => Ifptr Ptop + | MUlong => match v1, v2 with + | L _, I _ => v2 + | _, _ => Ifptr Ptop end | MUshrx i => - match v1 with - | I _ => - if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + 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 with - | L _ => - if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop - | _ => Ifptr Ptop + match v1, v2 with + | L _, L _ => + if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop + | _, _ => Ifptr Ptop end end. -Definition eval_opimmR0 (opi: opimm): aval := - match opi with - | OPimmADD i => add (I i) zero32 - | OPimmADDL i => addl (L i) zero64 - end. - Definition eval_static_condition (cond: condition) (vl: list aval): abool := match cond, vl with | Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2 @@ -71,22 +68,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 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 + | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop) + | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop) + | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop) + | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop) + | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop) + | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop) + | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop) + | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop) + | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop) | _, _ => Bnone end. @@ -226,33 +223,35 @@ 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) - | OEimmR0 opi, nil => eval_opimmR0 opi - | 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) + | OEmoveSP, nil => Ptr Stack + | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)) + | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)) + | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)) + | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)) | 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, nil => shl (I n) (I (Int.repr 12)) - | OEaddiw n, v1::nil => add (I n) v1 + | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop) + | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | 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) + | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)) + | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)) + | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)) + | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)) | 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, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12))) - | OEaddil n, v1::nil => addl (L n) v1 + | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop) + | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack) | 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) @@ -419,8 +418,8 @@ 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_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)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -434,8 +433,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m, vmatch bc (Val.maketotal (Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0 - Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)). + Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -445,8 +444,8 @@ Qed. Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp, vmatch bc a1 b1 -> vmatch bc a0 b0 -> - 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)). + vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef) + (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -457,8 +456,8 @@ 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_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64)) - (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)). + (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef)) + (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))). Proof. intros. destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg; @@ -478,19 +477,23 @@ Proof. rewrite Ptrofs.add_zero_l; eauto with va. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. - unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64; - destruct opi; eauto with va. 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. - { fold (Val.add (Vint n) a1); eauto with va. } + { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; 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: { fold (Val.addl (Vlong n) a1); eauto with va. } + 9: { destruct optR as [[]|]; simpl; eauto with va; + InvHyps; eauto with va; + destruct Archi.ptr64 eqn:A; simpl; + inv H1; simpl; try rewrite A; simpl; 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; |