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

Update macaw-symbolic with changes to string literals in what4

Browse Source
This commit is contained in:
Rob Dockins 2019-11-15 14:39:38 -08:00
parent 3da105d44e
commit 13aefd82f2
3 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit a657820d9d730fa00bae4cb8929c3a3f41136472
Subproject commit 1afe71bc094793f623ca30780ef0a56424692163

3
symbolic/src/Data/Macaw/Symbolic.hs
View File

@ -126,6 +126,7 @@ import What4.Interface
import What4.InterpretedFloatingPoint as C
import qualified What4.ProgramLoc as C
import What4.Symbol (userSymbol)
import qualified What4.Utils.StringLiteral as C
import qualified Lang.Crucible.Analysis.Postdom as C
import Lang.Crucible.Backend
@ -529,7 +530,7 @@ mkBlockPathRegCFG arch_fns halloc pos_fn blocks =
block_ptr <- evalMacawStmt $
MacawGlobalPtr arch_width $ M.segoffAddr block_addr
cond <- evalMacawStmt $ PtrEq arch_width ip_reg_val block_ptr
msg <- appAtom $ C.TextLit
msg <- appAtom $ C.StringLit $ C.UnicodeLiteral
"the current block follows the previous block in the path"
addStmt $ CR.Assume cond msg

13
symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
View File

@ -111,6 +111,7 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>), width)
import What4.ProgramLoc as C
import qualified What4.Symbol as C
import qualified What4.Utils.StringLiteral as C
import qualified Lang.Crucible.CFG.Expr as C
import qualified Lang.Crucible.CFG.Extension.Safety as C
@ -1256,7 +1257,7 @@ addMacawTermStmt tstmt =
fns <- translateFns <$> get
crucGenArchTermStmt fns ts regs
M.TranslateError _regs msg -> do
cmsg <- crucibleValue (C.TextLit msg)
cmsg <- crucibleValue (C.StringLit (C.UnicodeLiteral msg))
addTermStmt (CR.ErrorStmt cmsg)
-----------------
@ -1416,15 +1417,15 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
-- an X86 HLT instruction. TODO: We may want to do something
-- else for an exit syscall, since that's a normal outcome.
Nothing -> do
msgVal <- crucibleValue (C.TextLit "Halting")
msgVal <- crucibleValue (C.StringLit (C.UnicodeLiteral "Halting"))
addTermStmt $ CR.ErrorStmt msgVal
M.PLTStub{} ->
error "Do not support translating PLT stubs"
M.ParsedTranslateError msg -> do
msgVal <- crucibleValue (C.TextLit msg)
msgVal <- crucibleValue (C.StringLit (C.UnicodeLiteral msg))
addTermStmt $ CR.ErrorStmt msgVal
M.ClassifyFailure _regs _failureReasons -> do
msgVal <- crucibleValue $ C.TextLit $ Text.pack $ "Could not identify block at " ++ show thisAddr
msgVal <- crucibleValue $ C.StringLit $ C.UnicodeLiteral $ Text.pack $ "Could not identify block at " ++ show thisAddr
addTermStmt $ CR.ErrorStmt msgVal
addSwitch :: forall arch s ids
@ -1501,9 +1502,9 @@ addSwitch blockLabelMap idx possibleAddrs = do
, CR.Br eqAtom thnLbl elsLbl
)
errAtom <- mkAtom C.StringRepr
errAtom <- mkAtom (C.StringRepr C.UnicodeRepr)
let finalStmts =
[ CR.DefineAtom errAtom $ CR.EvalApp $ C.TextLit $
[ CR.DefineAtom errAtom $ CR.EvalApp $ C.StringLit $ C.UnicodeLiteral
"Index not in lookup table"
]
let finalTermStmt = CR.ErrorStmt errAtom