GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-11-22 05:45:51 +03:00
Code Issues Projects Releases Wiki Activity

Bump Crucible submodule, adapt to crucible-syntax changes

Browse Source
This commit is contained in:
Langston Barrett 2023-12-07 17:09:21 -05:00
parent 9e09fc86e7
commit 35b5fcd732
2 changed files with 16 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
deps/crucible vendored

@ -1 +1 @@
Subproject commit 6fad4300d50c15ad926eedab7a98109bb36caa90
Subproject commit 459e8db323b164ad48f52fb232a6a3331e99be69

30
symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
View File

@ -42,7 +42,7 @@ import qualified Lang.Crucible.CFG.Reg as LCCR
import qualified Lang.Crucible.LLVM.MemModel as LCLM
import qualified Lang.Crucible.Syntax.Atoms as LCSA
import qualified Lang.Crucible.Syntax.Concrete as LCSC
import qualified Lang.Crucible.Syntax.ExprParse as LCSE
import qualified Lang.Crucible.Syntax.Monad as LCSM
import qualified Lang.Crucible.Types as LCT
import qualified Lang.Crucible.LLVM.Syntax as LCLS
@ -50,7 +50,7 @@ import qualified What4.Interface as WI
import qualified What4.ProgramLoc as WP
-- | The constraints on the abstract parser monad
type ExtensionParser m ext s = ( LCSE.MonadSyntax LCSA.Atomic m
type ExtensionParser m ext s = ( LCSM.MonadSyntax LCSA.Atomic m
, MonadWriter [WP.Posd (LCCR.Stmt ext s)] m
, MonadState (LCSC.SyntaxState s) m
, MonadIO m
@ -169,14 +169,14 @@ extensionParser :: forall s m ext arch w
-- ^ A pair containing a result type and an atom of that type
extensionParser wrappers hooks =
let ?parserHooks = hooks in
LCSE.depCons LCSC.atomName $ \name ->
LCSM.depCons LCSC.atomName $ \name ->
case name of
LCSA.AtomName "pointer-read" -> do
-- Pointer reads are a special case because we must parse the type of
-- the value to read as well as the endianness of the read before
-- parsing the additional arguments as Atoms.
LCSE.depCons LCSC.isType $ \(Some tp) ->
LCSE.depCons LCSC.atomName $ \endiannessName ->
LCSM.depCons LCSC.isType $ \(Some tp) ->
LCSM.depCons LCSC.atomName $ \endiannessName ->
case endiannessFromAtomName endiannessName of
Just endianness ->
let readWrapper =
@ -187,8 +187,8 @@ extensionParser wrappers hooks =
-- Pointer writes are a special case because we must parse the type of
-- the value to write out as well as the endianness of the write before
-- parsing the additional arguments as Atoms.
LCSE.depCons LCSC.isType $ \(Some tp) ->
LCSE.depCons LCSC.atomName $ \endiannessName ->
LCSM.depCons LCSC.isType $ \(Some tp) ->
LCSM.depCons LCSC.atomName $ \endiannessName ->
case endiannessFromAtomName endiannessName of
Just endianness ->
let writeWrapper =
@ -199,7 +199,7 @@ extensionParser wrappers hooks =
-- Bitvector literals with a type argument are a special case. We must
-- parse the type argument separately before parsing the remaining
-- argument as an Atom.
LCSE.depCons LCSC.isType $ \(Some tp) ->
LCSM.depCons LCSC.isType $ \(Some tp) ->
case tp of
LCT.BVRepr{} ->
go (SomeExtensionWrapper (buildBvTypedLitWrapper tp))
@ -213,7 +213,7 @@ extensionParser wrappers hooks =
=> SomeExtensionWrapper arch
-> m (Some (LCCR.Atom s))
go (SomeExtensionWrapper wrapper) = do
loc <- LCSE.position
loc <- LCSM.position
-- Generate atoms for the arguments to this extension
operandAtoms <- LCSC.operands (extArgTypes wrapper)
-- Pass these atoms to the extension wrapper and return an atom for the
@ -518,8 +518,8 @@ extensionWrappers = Map.fromList
, (LCSA.AtomName "pointer-make-null", SomeExtensionWrapper wrapMakeNull)
]
ptrTypeParser :: LCSE.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)
ptrTypeParser = LCSE.describe "Pointer type" $ do
ptrTypeParser :: LCSM.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)
ptrTypeParser = LCSM.describe "Pointer type" $ do
LCSC.BoundedNat n <- LCLS.pointerTypeParser
pure (Some (LCLM.LLVMPointerRepr n))
@ -534,10 +534,10 @@ machineCodeParserHooks
machineCodeParserHooks proxy hooks =
LCSC.ParserHooks
{ LCSC.extensionTypeParser =
LCSE.describe "Macaw type" $
LCSE.call (ptrTypeParser <|> LCSC.extensionTypeParser hooks)
LCSM.describe "Macaw type" $
LCSM.call (ptrTypeParser <|> LCSC.extensionTypeParser hooks)
, LCSC.extensionParser =
LCSE.describe "Macaw operation" $ do
LCSM.describe "Macaw operation" $ do
let extParser = extensionParser extensionWrappers (machineCodeParserHooks proxy hooks)
LCSE.call (extParser <|> LCSC.extensionParser hooks)
LCSM.call (extParser <|> LCSC.extensionParser hooks)
}