From 0d98d7fec937d3a9a2324f1731b041cfbf16dcbe Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Tue, 30 Mar 2021 10:11:01 +0200
Subject: Refactoring the mayundef OP to be more general...

---
 riscV/ValueAOp.v | 67 +++++++++++++++++++-------------------------------------
 1 file changed, 23 insertions(+), 44 deletions(-)

(limited to 'riscV/ValueAOp.v')

diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index fe519921..82291f9c 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -27,42 +27,28 @@ Definition apply_bin_r0 {B} (optR0: option bool) (sem: aval -> aval -> B) (v1 v2
   | Some false => sem v1 vz
   end.
 
-Definition may_undef_int (is_long: bool) (v1 v2: aval): aval :=
-  if negb is_long then
-    match v1 with
-    | I _ => v2
-    | _ => Ifptr Ptop
-    end
-  else
-    match v1 with
-    | L _ => v2
-    | _ => Ifptr Ptop
-    end.
-
-Definition shrx_imm_undef (v1 v2: aval): aval :=
-  match v1 with
-  | I n1 =>
-      match v2 with
-      | I n2 =>
-          if Int.ltu n2 (Int.repr 31)
-          then I n1
-          else Ifptr Ptop
+Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
+  match mu with
+  | MUint => match v1 with
+             | I _ => v2
+             | _ => Ifptr Ptop
+             end
+  | MUlong => match v1 with
+              | L _ => v2
+              | _ => Ifptr Ptop
+              end
+  | MUshrx i =>
+      match v1 with
+      | I _ =>
+          if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop
       | _ => Ifptr Ptop
       end
-  | _ => Ifptr Ptop
-  end.
-
-Definition shrxl_imm_undef (v1 v2: aval): aval :=
-  match v1 with
-  | L n1 =>
-      match v2 with
-      | I n2 =>
-          if Int.ltu n2 (Int.repr 63)
-          then L n1
-          else Ifptr Ptop
+  | MUshrxl i =>
+      match v1 with
+      | L _ =>
+          if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop
       | _ => Ifptr Ptop
       end
-  | _ => Ifptr Ptop
   end.
 
 Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
@@ -263,9 +249,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | OEaddil n, v1::nil => addl (L n) v1
   | OEaddilr0 n, nil => addl (L n) zero64
   | OEloadli n, nil => L (n)
-  | OEmayundef is_long, v1::v2::nil => may_undef_int is_long v1 v2
-  | OEshrxundef n, v1::nil => shrx_imm_undef v1 (I n)
-  | OEshrxlundef n, v1::nil => shrxl_imm_undef v1 (I 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)
@@ -508,21 +492,16 @@ Proof.
   
   1,10: simpl; eauto with va.
   2:
-    unfold Op.may_undef_int, may_undef_int; destruct is_long;
-    simpl; inv H0; inv H1; eauto with va; inv H;
-    apply vmatch_ifptr_p; eauto with va.
+    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. }
-  { unfold Op.shrx_imm_undef, shrx_imm_undef.
-    simpl; inv H1; eauto with va;
-    destruct (Int.ltu _ _); simpl; eauto with va. }
-  { unfold Op.shrxl_imm_undef, shrxl_imm_undef.
-    simpl; inv H1; eauto with va;
-    destruct (Int.ltu _ _); simpl; eauto with va. }
   all: unfold Val.cmpf; apply of_optbool_sound; eauto with va.
 Qed.
 
-- 
cgit