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 1816d77
Show file tree
Hide file tree
Showing 2 changed files with 7 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

0 comments on commit 1816d77

Please sign in to comment.