Extend offline to handle new reachable constructs

UQ-PAC · Dec 23, 2024 · 0becc26 · 0becc26
1 parent 38e7d42
commit 0becc26
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 1 deletion.
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,12 @@ module RemoveUnsupported = struct
       | Stmt_Dep_ImpDef (_, loc)
       | Stmt_See (_, loc)
       | Stmt_Throw (_, loc)
+      | Stmt_Repeat(_, _, loc)
+      | Stmt_Try(_, _, _, _, loc)
       | Stmt_DecodeExecute (_, _, loc) -> ChangeTo (assert_false loc)
 
-      | _ -> failwith @@ "Unknown stmt: " ^ (pp_stmt e))
+      )
+
   end
 
   let run unsupported env body =

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 et x =
+  failwith "MemTag_read unsupported"
 
 (* Prim bool ops *)
 let f_gen_and_bool e1 e2 =