From 66199370095cb23faa1febc752c2722d22bf4bde Mon Sep 17 00:00:00 2001 From: Nicholas Coughlin Date: Tue, 24 Dec 2024 08:54:31 +1000 Subject: [PATCH] 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. --- libASL/scala_backend.ml | 2 +- libASL/symbolic.ml | 4 ++++ libASL/symbolic_lifter.ml | 6 +++--- .../aslp-lifter-llvm/include/aslp/llvm_interface.hpp | 1 + .../subprojects/aslp-lifter/include/aslp/interface.hpp | 1 + offlineASL-scala/lifter/src/interface.scala | 1 + offlineASL-scala/main/src/NoneLifter.scala | 1 + offlineASL/offline_utils.ml | 2 ++ 8 files changed, 14 insertions(+), 4 deletions(-) diff --git a/libASL/scala_backend.ml b/libASL/scala_backend.ml index 981316b2..4aac7eba 100644 --- 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 index a904fcfb..a999a19c 100644 --- 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 index 86dd03b4..4a37306c 100644 --- 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 index 526454b2..49cd1345 100644 --- 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_interfaceCreateLoad(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 index b8593419..e93410c2 100644 --- 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 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 index 5a363fa2..006cacd2 100644 --- 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 index 1b2f61af..30b47a15 100644 --- 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 index 74e84992..0130a5d7 100644 --- 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 =