Skip to content

Commit

Permalink
Offline fixes for new reachable code
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
ncough committed Dec 23, 2024
1 parent ca497c6 commit b1b7d26
Show file tree
Hide file tree
Showing 3 changed files with 9 additions and 3 deletions.
4 changes: 4 additions & 0 deletions libASL/symbolic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions libASL/symbolic_lifter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down
2 changes: 2 additions & 0 deletions offlineASL/offline_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down

0 comments on commit b1b7d26

Please sign in to comment.