aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ValueAOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/ValueAOp.v')
-rw-r--r--riscV/ValueAOp.v98
1 files changed, 47 insertions, 51 deletions
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 3ba2732d..d29180e4 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -22,12 +22,11 @@ Definition zero64 := (L Int64.zero).
(** 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 :=
+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 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 :=
@@ -68,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 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)
+ | 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.
@@ -223,35 +222,34 @@ 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)
- | 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))
+ | 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, nil => shl (I n) (I (Int.repr 12))
- | 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)
+ | 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 (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))
+ | 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, 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 (Ifptr Ptop)
- | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack)
+ | 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)
@@ -418,8 +416,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 Vundef)
- (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))).
+ 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 optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -433,8 +431,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 Vundef))
- (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))).
+ Op.zero64))
+ (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)).
Proof.
intros.
destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -444,8 +442,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 Vundef)
- (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))).
+ 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 optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -456,8 +454,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 Vundef))
- (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))).
+ (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 optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -482,18 +480,16 @@ Proof.
unfold Val.cmp; apply of_optbool_sound; eauto with va.
unfold Val.cmpu; apply of_optbool_sound; 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. }
+ { 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;
- InvHyps; eauto with va;
- destruct Archi.ptr64 eqn:A; simpl;
- inv H1; simpl; try rewrite A; simpl; eauto with va. }
+ 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;
generated by cgit (git 2.34.1) at 2024-05-20 03:34:55 +0000