Also support Val_bool in eval_exp'

rems-project · Mar 6, 2024 · 8434160 · 8434160
1 parent 895426c
commit 8434160
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 1 deletion.
diff --git a/examples/ite_test.v b/examples/ite_test.v
@@ -69,7 +69,13 @@ Definition instr_ite : isla_trace :=
                                ] Mk_annot)
                           (Val (Val_Bits (BV 64%N 0%Z)) Mk_annot)
                           (Val (Val_Symbolic 1%Z) Mk_annot) Mk_annot)) Mk_annot :t:
+  Smt (DefineConst 4%Z (Unop Not (Ite (Manyop And [
+     Binop Eq (Val (Val_Symbolic 1%Z) Mk_annot) (Val (Val_Bits (BV 64%N 0%Z)) Mk_annot) Mk_annot
+                               ] Mk_annot)
+                          (Val (Val_Bool true) Mk_annot)
+                          (Val (Val_Bool false) Mk_annot) Mk_annot) Mk_annot)) Mk_annot :t:
   WriteReg "R0" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
+  WriteReg "R1" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
   Smt (DeclareConst 10%Z (Ty_BitVec 64%N)) Mk_annot :t:
   ReadReg "_PC" [] (RegVal_Base (Val_Symbolic 10%Z)) Mk_annot :t:
   Smt (DefineConst 11%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 10%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
@@ -83,7 +89,7 @@ Definition spec `{!islaG Σ} `{!threadG} a : iProp Σ :=
   "R2" ↦ᵣ RVal_Bits v2 ∗
   "R0" ↦ᵣ RVal_Bits vold ∗
   instr_pre a (
-    "R1" ↦ᵣ RVal_Bits v1 ∗
+    "R1" ↦ᵣ RVal_Bool (negb (ite (bool_decide (v1 = 0%bv)) true false)) ∗
     "R2" ↦ᵣ RVal_Bits v2 ∗
     "R0" ↦ᵣ RVal_Bits (ite (bool_decide (v1 = 0%bv) && bool_decide (v2 = 1%bv)) 0%bv v1) ∗
     True).

diff --git a/theories/automation.v b/theories/automation.v
@@ -327,6 +327,8 @@ Fixpoint eval_exp' (e : exp) : option base_val :=
         | Val_Bits b2, Val_Bits b3 =>
             b3' ← bvn_to_bv b2.(bvn_n) b3;
             Some (Val_Bits (ite b b2.(bvn_val) b3'))
+        | Val_Bool b2, Val_Bool b3 =>
+            Some (Val_Bool (ite b b2 b3))
         | _, _ => Some (ite b v2 v3)
         end
     | _ => None