GaloisInc/macaw
1
1
Fork 0
mirror of https://github.com/GaloisInc/macaw.git synced 2024-12-01 17:26:45 +03:00
Code Issues Projects Releases Wiki Activity

x86-syntax: Use upstream register indices

Browse Source
This commit is contained in:
Langston Barrett 2024-08-15 16:13:23 -04:00
parent 97751b0895
commit 69f63302f8
2 changed files with 1 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
macaw-x86-syntax/macaw-x86-syntax.cabal
View File

@ -95,7 +95,6 @@ library
base >= 4.13, base >= 4.13,
containers, containers,
crucible, crucible,
crucible-llvm,
crucible-syntax, crucible-syntax,
macaw-base, macaw-base,
macaw-symbolic, macaw-symbolic,

7
macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
View File

@ -33,7 +33,6 @@ import Data.Parameterized.Some (Some(..))
import Lang.Crucible.CFG.Expr as Expr import Lang.Crucible.CFG.Expr as Expr
import Lang.Crucible.CFG.Reg (Atom, Stmt) import Lang.Crucible.CFG.Reg (Atom, Stmt)
import Lang.Crucible.CFG.Reg qualified as Reg import Lang.Crucible.CFG.Reg qualified as Reg
import Lang.Crucible.LLVM.MemModel.Pointer qualified as Mem
import Lang.Crucible.Syntax.Atoms qualified as LCSA import Lang.Crucible.Syntax.Atoms qualified as LCSA
import Lang.Crucible.Syntax.Concrete qualified as LCSC import Lang.Crucible.Syntax.Concrete qualified as LCSC
import Lang.Crucible.Syntax.Monad qualified as LCSM import Lang.Crucible.Syntax.Monad qualified as LCSM
@ -95,13 +94,9 @@ parseReg =
LCSM.describe "an x86_64 register" $ do LCSM.describe "an x86_64 register" $ do
name <- LCSC.atomName name <- LCSC.atomName
case name of case name of
LCSA.AtomName "rip" -> LCSA.AtomName "rip" -> pure (Some X86.ip)
pure (Some ripIndex)
LCSA.AtomName _ -> empty LCSA.AtomName _ -> empty
ripIndex :: Ctx.Index (DMS.MacawCrucibleRegTypes X86.X86_64) (Mem.LLVMPointerType 64)
ripIndex = Ctx.extendIndex @(Ctx.EmptyCtx Ctx.::> Mem.LLVMPointerType 64) @(DMS.MacawCrucibleRegTypes X86.X86_64) Ctx.baseIndex
x86AtomParser :: x86AtomParser ::
( LCSM.MonadSyntax LCSA.Atomic m ( LCSM.MonadSyntax LCSA.Atomic m
, MonadIO m , MonadIO m