x86-syntax: Use upstream register indices

GaloisInc · Aug 15, 2024 · d2a304f · d2a304f
1 parent 4ad8a70
commit d2a304f
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 7 deletions.
diff --git a/macaw-x86-syntax/macaw-x86-syntax.cabal b/macaw-x86-syntax/macaw-x86-syntax.cabal
@@ -95,7 +95,6 @@ library
     base >= 4.13,
     containers,
     crucible,
-    crucible-llvm,
     crucible-syntax,
     macaw-base,
     macaw-symbolic,

diff --git a/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs b/macaw-x86-syntax/src/Data/Macaw/X86/Symbolic/Syntax.hs
@@ -33,7 +33,6 @@ import Data.Parameterized.Some (Some(..))
 import Lang.Crucible.CFG.Expr as Expr
 import Lang.Crucible.CFG.Reg (Atom, Stmt)
 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.Concrete qualified as LCSC
 import Lang.Crucible.Syntax.Monad qualified as LCSM
@@ -95,13 +94,9 @@ parseReg =
   LCSM.describe "an x86_64 register" $ do
     name <- LCSC.atomName
     case name of
-      LCSA.AtomName "rip" ->
-        pure (Some ripIndex)
+      LCSA.AtomName "rip" -> pure (Some X86.ip)
       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 ::
   ( LCSM.MonadSyntax LCSA.Atomic m
   , MonadIO m