GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-24 00:42:28 +03:00
Code Issues Projects Releases Wiki Activity

[x86_symbolic] updates for crucible nonce change from (ST h) to IO

Browse Source 
Changes for compatibility with Crucible pull request
285 (https://github.com/GaloisInc/crucible/pull/285) and the
corresponding changes in macaw symbolic.
This commit is contained in:
Kevin Quick 2019-07-19 13:15:44 -07:00
parent 48c3ba1fed
commit 40eff5802c
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
2 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
View File

@ -276,27 +276,27 @@ instance TraversableFC X86StmtExtension where
type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension
crucGenX86Fn :: forall ids h s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp
-> CrucGen M.X86_64 ids h s (C.Atom s (ToCrucibleType tp))
crucGenX86Fn :: forall ids s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp
-> CrucGen M.X86_64 ids s (C.Atom s (ToCrucibleType tp))
crucGenX86Fn fn = do
let f :: M.Value arch ids a -> CrucGen arch ids h s (AtomWrapper (C.Atom s) a)
let f :: M.Value arch ids a -> CrucGen arch ids s (AtomWrapper (C.Atom s) a)
f x = AtomWrapper <$> valueToCrucible x
r <- traverseFC f fn
evalArchStmt (X86PrimFn r)
crucGenX86Stmt :: forall ids h s
crucGenX86Stmt :: forall ids s
. M.X86Stmt (M.Value M.X86_64 ids)
-> CrucGen M.X86_64 ids h s ()
-> CrucGen M.X86_64 ids s ()
crucGenX86Stmt stmt = do
let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids h s (AtomWrapper (C.Atom s) a)
let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids s (AtomWrapper (C.Atom s) a)
f x = AtomWrapper <$> valueToCrucible x
stmt' <- traverseF f stmt
void (evalArchStmt (X86PrimStmt stmt'))
crucGenX86TermStmt :: M.X86TermStmt ids
-> M.RegState M.X86Reg (M.Value M.X86_64 ids)
-> CrucGen M.X86_64 ids h s ()
-> CrucGen M.X86_64 ids s ()
crucGenX86TermStmt tstmt _regs =
void (evalArchStmt (X86PrimTerm tstmt))

4
x86_symbolic/tests/Main.hs
View File

@ -95,7 +95,7 @@ main = do
[] -> fail "Could not find add function"
_ -> fail "Found multiple add functions"
memBaseVar <- stToIO $ C.freshGlobalVar halloc "add_mem_base" C.knownRepr
memBaseVar <- C.freshGlobalVar halloc "add_mem_base" C.knownRepr
let memBaseVarMap :: MS.MemSegmentMap 64
memBaseVarMap = Map.singleton 1 memBaseVar
@ -113,7 +113,7 @@ main = do
putStrLn $ "Analyzing " ++ show addr
(_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0
C.SomeCFG g <- stToIO $ MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo
C.SomeCFG g <- MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo
regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)