Offline fixes for new reachable code

Calls without bodies are left in the partial eval result. This is a little unexpected, leading to offline issues. Also fix some sanity tests to handle failure consistently.
UQ-PAC · Dec 24, 2024 · 6619937 · 6619937
1 parent ca497c6
commit 6619937
Show file tree

Hide file tree

Showing 8 changed files with 14 additions and 4 deletions.
diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml
@@ -60,7 +60,7 @@ module StringSet = Set.Make(String)
         "f_gen_lsr_bits"; "f_gen_mul_bits"; "f_gen_ne_bits"; "f_gen_not_bits";
         "f_gen_not_bool"; "f_gen_or_bits"; "f_gen_or_bool"; "f_gen_sdiv_bits";
         "f_gen_sle_bits"; "f_gen_slt_bits"; "f_gen_sub_bits";
-        "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice";
+        "f_gen_AArch64_MemTag_read"; "f_gen_AArch64_MemTag_set"; "f_gen_Mem_read"; "f_gen_slice";
         "f_gen_replicate_bits"; "f_gen_append_bits"; "f_gen_array_load";
         "f_gen_array_store"; "f_gen_Mem_set"; "f_gen_assert";
         "f_switch_context"; "f_true_branch"; "f_false_branch"; "f_merge_branch"])

diff --git a/libASL/symbolic.ml b/libASL/symbolic.ml
@@ -990,6 +990,10 @@ let prims_impure () =
     FIdent("AtomicEnd",0);
     FIdent("AArch64.MemTag.read",0);
     FIdent("AArch64.MemTag.set",0);
+    FIdent("SetTagCheckedInstruction",0);
+    FIdent("SpeculativeStoreBypassBarrierToPA",0);
+    FIdent("SpeculationBarrier",0);
+    FIdent("SpeculativeStoreBypassBarrierToVA",0);
   ]
 
 (** Test if an expression is only over constants, variables and pure operations. Does not

diff --git a/libASL/symbolic_lifter.ml b/libASL/symbolic_lifter.ml
@@ -135,9 +135,9 @@ module RemoveUnsupported = struct
       | Stmt_Dep_ImpDef (_, loc)
       | Stmt_See (_, loc)
       | Stmt_Throw (_, loc)
-      | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc)
-
-      | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e))
+      | Stmt_DecodeExecute (_, _, loc)
+      | Stmt_Try (_, _, _, _, loc)
+      | Stmt_Repeat (_, _, loc) -> ChangeTo (assert_false loc))
   end
 
   let run unsupported env body =

diff --git a/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter-llvm/include/aslp/llvm_interface.hpp
@@ -340,6 +340,7 @@ class llvm_run_time_interface : virtual public lifter_interface<llvm_lifter_trai
     return builder->CreateLoad(intty(int_expr(width)), ptr);
   }
   void f_gen_AArch64_MemTag_set(rt_expr address, rt_expr acctype, rt_expr value) override { assert(0); }
+  void f_gen_AArch64_MemTag_read(rt_expr address, rt_expr acctype) override { assert(0); }
 
   void f_AtomicStart() override { assert(0); }
   void f_AtomicEnd() override { assert(0); }

diff --git a/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp b/offlineASL-cpp/subprojects/aslp-lifter/include/aslp/interface.hpp
@@ -111,6 +111,7 @@ template <typename Traits> class lifter_interface : public Traits {
                                  rt_expr acctype) = 0;
   virtual void f_gen_AArch64_MemTag_set(rt_expr address, rt_expr acctype,
                                         rt_expr value) = 0;
+  virtual rt_expr f_gen_AArch64_MemTag_read(rt_expr address, rt_expr acctype) = 0;
 
   virtual void f_AtomicStart() = 0;
   virtual void f_AtomicEnd() = 0;

diff --git a/offlineASL-scala/lifter/src/interface.scala b/offlineASL-scala/lifter/src/interface.scala
@@ -95,6 +95,7 @@ trait LiftState[RTSym, RTLabel, BV <: RTSym] {
   def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_AArch64_MemTag_set(arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym
+  def f_gen_AArch64_MemTag_read(arg0: RTSym, arg1: RTSym): RTSym
   def f_gen_Mem_read(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym
   def f_gen_slice(e: RTSym, lo: BigInt, wd: BigInt): RTSym
   def f_gen_replicate_bits(targ0: BigInt, targ1: BigInt, arg0: RTSym, arg1: BV): RTSym

diff --git a/offlineASL-scala/main/src/NoneLifter.scala b/offlineASL-scala/main/src/NoneLifter.scala
@@ -106,6 +106,7 @@ class NotImplementedLifter extends LiftState[RExpr, String, BitVec] {
   def f_gen_slt_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_sub_bits(targ0: BigInt, arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_AArch64_MemTag_set(arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError()
+  def f_gen_AArch64_MemTag_read(arg0: RTSym, arg1: RTSym): RTSym = throw NotImplementedError()
   def f_gen_Mem_read(targ0: BigInt, arg0: RTSym, arg1: RTSym, arg2: RTSym): RTSym = throw NotImplementedError()
   def f_gen_slice(e: RTSym, lo: BigInt, wd: BigInt): RTSym = throw NotImplementedError()
   def f_gen_replicate_bits(targ0: BigInt, targ1: BigInt, arg0: RTSym, arg1: BV): RTSym = throw NotImplementedError()

diff --git a/offlineASL/offline_utils.ml b/offlineASL/offline_utils.ml
@@ -191,6 +191,8 @@ let f_AtomicEnd () =
   push_stmt (Stmt_TCall (FIdent ("AtomicEnd", 0), [], [], Unknown))
 let f_gen_AArch64_MemTag_set x y z: unit =
   failwith "MemTag_set unsupported"
+let f_gen_AArch64_MemTag_read x y =
+  failwith "MemTag_read unsupported"
 
 (* Prim bool ops *)
 let f_gen_and_bool e1 e2 =