Now a more general way to perform imm operations

1 files changed, 18 insertions, 13 deletions

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index 82291f9c..b64040e1 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -51,6 +51,12 @@ Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
       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
@@ -220,6 +226,7 @@ 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 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)
@@ -231,7 +238,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | 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
-  | OEaddiwr0 n, nil => add (I n) zero32
   | OEandiw n, v1::nil => and (I n) v1
   | OEoriw n, v1::nil => or (I n) v1
   | OEseql optR0, v1::v2::nil => of_optbool (apply_bin_r0 optR0 (cmpl_bool Ceq) v1 v2 zero64)
@@ -247,7 +253,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | 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
-  | OEaddilr0 n, nil => addl (L n) zero64
   | 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)
@@ -472,36 +477,36 @@ 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.
-  
+
+  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. }
-  { unfold zero32; 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. }
-  10: { fold (Val.andl (Vlong n) a1); eauto with va. }
-  10: { fold (Val.orl (Vlong n) a1); eauto with va. }
-  10: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
+  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.
-  2:
+  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.
   
-  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. }
+  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.