Skip to content

Commit

Permalink
x86-symbolic: Create an exception type for missing semantics
Browse files Browse the repository at this point in the history
This is an exception that consumers might want to catch.
  • Loading branch information
langston-barrett committed Jan 23, 2024
1 parent e1d0846 commit a946c34
Showing 1 changed file with 16 additions and 5 deletions.
21 changes: 16 additions & 5 deletions x86_symbolic/src/Data/Macaw/X86/Crucible.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ module Data.Macaw.X86.Crucible
SymFuns(..), newSymFuns

-- * Instruction interpretation
, MissingSemantics(..)
, funcSemantics
, stmtSemantics
, termSemantics
Expand Down Expand Up @@ -129,6 +130,13 @@ withConcreteCountAndDir state val_size wrapped_count _wrapped_dir func =
return ((), res_crux_state)
Nothing -> error $ "Unsupported symbolic count in rep stmt: "

data MissingSemantics
= MissingStmtSemantics String
| MissingTermSemantics String
deriving Show

instance Exception MissingSemantics

stmtSemantics
:: (IsSymInterface sym, HasLLVMAnn sym, ?memOpts :: MemOptions)
=> SymFuns sym
Expand Down Expand Up @@ -169,9 +177,10 @@ stmtSemantics _sym_funs global_var_mem globals stmt state =
afterWriteMem <- doWriteMem bak mem M.Addr64 mem_repr resolvedDestPtr (regValue val)
-- Update the final state
pure $! setMem acc_state global_var_mem afterWriteMem
_ -> error $
"Symbolic execution semantics for x86 statement are not implemented yet: "
<> (show $ MC.ppArchStmt (liftAtomIn (pretty . regType)) stmt)
_ ->
let msg = "Symbolic execution semantics for x86 statement are not implemented yet: "
++ show (MC.ppArchStmt (liftAtomIn (pretty . regType)) stmt)
in throw (MissingStmtSemantics msg)

-- | Dynamic semantics for x86-specific arch terminators
--
Expand All @@ -182,8 +191,10 @@ termSemantics :: (IsSymInterface sym)
-> M.X86TermStmt (AtomWrapper (RegEntry sym))
-> S p sym rtp bs r ctx
-> IO (RegValue sym UnitType, S p sym rtp bs r ctx)
termSemantics _fs x _s = error ("Symbolic execution semantics for x86 terminators are not implemented yet: " <>
show (MC.ppArchTermStmt (error "Can't print RegEntry") x))
termSemantics _fs x _s =
let msg = "Symbolic execution semantics for x86 terminators are not implemented yet: "
++ show (MC.ppArchTermStmt (error "Can't print RegEntry") x)
in throw (MissingTermSemantics msg)

data Sym s bak =
Sym { symBackend :: bak
Expand Down

0 comments on commit a946c34

Please sign in to comment.