aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ValueAOp.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/ValueAOp.v')
-rw-r--r--riscV/ValueAOp.v133
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;
generated by cgit (git 2.34.1) at 2024-05-20 03:03:29 +0000