Bump Crucible submodule, adapt to crucible-syntax changes

GaloisInc · Dec 8, 2023 · 20f35cd · 20f35cd
1 parent 2c540f8
commit 20f35cd
Show file tree

Hide file tree

Showing 8 changed files with 74 additions and 70 deletions.
diff --git a/stubs-common/src/Stubs/Diagnostic.hs b/stubs-common/src/Stubs/Diagnostic.hs
@@ -36,7 +36,6 @@ import qualified Lang.Crucible.Backend as LCB
 import qualified Lang.Crucible.CFG.Reg as LCCR
 import qualified Lang.Crucible.FunctionHandle as LCF
 import qualified Lang.Crucible.Simulator.SimError as LCSS
-import qualified Lang.Crucible.Syntax.Concrete as LCSC
 import qualified Stubs.Style as STY
 
 data Diagnostic where
@@ -73,7 +72,7 @@ data Diagnostic where
   -- | Setting up the goals for the given property
   AssertingGoalsForProperty :: T.Text -> Maybe T.Text -> Diagnostic
   -- | Executing a user override test
-  ExecutingOverrideTest :: LCSC.ACFG ext -> FilePath -> Diagnostic
+  ExecutingOverrideTest :: LCCR.AnyCFG ext -> FilePath -> Diagnostic
   -- | Reporting a symbolic branch
   SymbolicBranch :: Maybe WP.ProgramLoc -> Diagnostic
   -- | Invoking a function call in the simulator
@@ -146,7 +145,7 @@ ppDiagnostic d =
     AssertingGoalsForProperty name mdesc ->
       let desc = maybe mempty ((PP.line <>) . PP.pretty) mdesc
       in PP.pretty "Asserting goals for property " <> PP.pretty name <> desc <> PP.line
-    ExecutingOverrideTest (LCSC.ACFG _ _ g) path ->
+    ExecutingOverrideTest (LCCR.AnyCFG g) path ->
           PP.pretty "Executing override test '"
       <> PP.pretty (LCF.handleName (LCCR.cfgHandle g))
       <> PP.pretty "' in '"

diff --git a/stubs-common/src/Stubs/FunctionOverride/Extension.hs b/stubs-common/src/Stubs/FunctionOverride/Extension.hs
@@ -41,7 +41,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 What4.Interface as WI
 import qualified What4.ProgramLoc as WP
@@ -55,7 +55,7 @@ allTypeAliases = [minBound .. maxBound]
 
 -- | Parser for type extensions to crucible syntax
 extensionTypeParser
-  :: (LCSE.MonadSyntax LCSA.Atomic m)
+  :: (LCSM.MonadSyntax LCSA.Atomic m)
   => Map.Map LCSA.AtomName (Some LCT.TypeRepr)
   -- ^ A mapping from additional type names to the crucible types they
   -- represent
@@ -157,14 +157,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 =
@@ -175,8 +175,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 =
@@ -187,7 +187,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))
@@ -197,9 +197,9 @@ extensionParser wrappers hooks =
         -- name and length arguments separately due to their need to be
         -- concrete, and we must parse the type argument separately before we
         -- can know the return type.
-        LCSE.depCons LCSC.string $ \nmPrefix ->
-          LCSE.depCons LCSC.isType $ \(Some tp) ->
-            LCSE.depCons LCSC.nat $ \len ->
+        LCSM.depCons LCSC.string $ \nmPrefix ->
+          LCSM.depCons LCSC.isType $ \(Some tp) ->
+            LCSM.depCons LCSC.nat $ \len ->
             go (SomeExtensionWrapper (buildFreshVecWrapper nmPrefix tp len))
       _ ->
         case Map.lookup name wrappers of
@@ -210,7 +210,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

diff --git a/stubs-common/src/Stubs/FunctionOverride/Extension/Types.hs b/stubs-common/src/Stubs/FunctionOverride/Extension/Types.hs
@@ -31,7 +31,7 @@ import qualified Lang.Crucible.CFG.Extension as LCCE
 import qualified Lang.Crucible.CFG.Reg as LCCR
 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 What4.ProgramLoc as WP
 
@@ -47,7 +47,7 @@ data TypeAlias = Byte | Int | Long | PidT | Pointer | Short | SizeT | UidT
 newtype TypeLookup = TypeLookup (TypeAlias -> (Some LCT.TypeRepr))
 
 -- | 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

diff --git a/stubs-translator/src/Stubs/Translate.hs b/stubs-translator/src/Stubs/Translate.hs
@@ -54,7 +54,6 @@ import Control.Monad.IO.Class (MonadIO(liftIO))
 import Control.Monad.RWS (gets, modify)
 import Control.Monad.Reader (ReaderT (runReaderT))
 import Lang.Crucible.CFG.Core (StringInfoRepr(UnicodeRepr))
-import qualified Lang.Crucible.Syntax.Concrete as LCSC
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Map as Map
 import qualified Stubs.AST as SA
@@ -80,7 +79,7 @@ import Control.Monad.Catch (throwM)
 -- | A translated Program. Several fields are taken from crucible-syntax's ParsedProgram, for easy conversion
 data CrucibleProgram arch = CrucibleProgram {
   -- | The generated CFGs
-  crCFGs :: [LCSC.ACFG (DMS.MacawExt arch)],
+  crCFGs :: [LCCR.AnyCFG (DMS.MacawExt arch)],
   crGlobals :: Map.Map LCSA.GlobalName (Some LCCC.GlobalVar),
   crExterns :: Map.Map LCSA.GlobalName (Some LCCC.GlobalVar),
   crFwdDecs :: Map.Map WF.FunctionName LCF.SomeHandle,
@@ -97,7 +96,7 @@ data CrucibleProgram arch = CrucibleProgram {
 -- | A translated library / module. This is the result of translating a StubsLibrary
 data CrucibleLibrary arch = CrucibleLibrary {
     -- | Generated CFGs
-    crLibCFGs :: [LCSC.ACFG (DMS.MacawExt arch)],
+    crLibCFGs :: [LCCR.AnyCFG (DMS.MacawExt arch)],
     -- | Signature and Handle information for defined CFGs, for linking
     crExportedHandles :: [(String,STC.SomeHandle arch)]
 }
@@ -298,15 +297,13 @@ translateFn :: forall args ret s arch m. (DMS.SymArchConstraints arch, LCCE.IsSy
                 StubHandle arch args ret ->
                 STC.StubsEnv arch ->
                 MapF.MapF SA.CrucibleVar (STC.CrucibleGlobal arch) ->
-                SA.StubsFunction args ret ->  m (LCSC.ACFG (DMS.MacawExt arch))
+                SA.StubsFunction args ret ->  m (LCCR.AnyCFG (DMS.MacawExt arch))
 translateFn ng _ handles hdl env gmap SA.StubsFunction{SA.stubFnSig=SA.StubsSignature{SA.sigFnArgTys=argtys, SA.sigFnRetTy=retty},SA.stubFnBody=body}= do
     -- CFG needs crucible type info
-    args <- runReaderT (toCrucibleTyCtx argtys) env
-    cret <- runReaderT (toCrucibleTy retty) env
     let StubHandle _ _ handle = hdl
     (LCCR.SomeCFG cfg, _) <- liftIO $ LCCG.defineFunction WF.InternalPos (Some ng) handle $ \crucArgs -> (StubsState env retty MapF.empty MapF.empty (translateFnArgs crucArgs argtys) handles gmap,
                                                                                                      translateStmts @arch @_ @ret body >> LCCG.reportError (LCCR.App $ LCCE.StringEmpty UnicodeRepr))
-    return $ LCSC.ACFG args cret cfg
+    return $ LCCR.AnyCFG cfg
 
 -- | Translate all declarations from a StubsLibrary
 translateDecls :: forall arch s m . (STC.StubsArch arch, SPR.Preamble arch, LCCE.IsSyntaxExtension (DMS.MacawExt arch), StubsTranslator m) =>
@@ -318,7 +315,7 @@ translateDecls :: forall arch s m . (STC.StubsArch arch, SPR.Preamble arch, LCCE
         MapF.MapF SA.CrucibleVar (STC.CrucibleGlobal arch) ->
         [(String, SomeWrappedOverride arch)] ->
         [SA.SomeStubsFunction] -> -- Functions to translate
-        m [(LCSC.ACFG (DMS.MacawExt arch), (String,SomeHandle arch))]
+        m [(LCCR.AnyCFG (DMS.MacawExt arch), (String,SomeHandle arch))]
 translateDecls ng hAlloc preMap prevHdls env gmap ovMap fns = do
 
     -- get handles for all functions before hand, for linking.

diff --git a/stubs-wrapper/src/Stubs/Wrapper.hs b/stubs-wrapper/src/Stubs/Wrapper.hs
@@ -27,6 +27,7 @@ import qualified What4.Interface as WI
 
 import qualified Lang.Crucible.Syntax.Concrete as LCSC
 import qualified Lang.Crucible.FunctionHandle as LCF
+import qualified Lang.Crucible.CFG.Extension as LCCE
 import qualified Lang.Crucible.Simulator as LCS
 import qualified Lang.Crucible.CFG.SSAConversion as LCCS
 import qualified Lang.Crucible.CFG.Core as LCCC
@@ -60,7 +61,7 @@ import qualified Stubs.AST as SA
 import qualified Stubs.Common as SC
 
 -- | Inherited from Ambient : Turn crucible-syntax Parsed Programs into overrides
-loadParsedPrograms :: forall ext sym arch w . (ext ~ DMS.MacawExt arch, DMM.MemWidth w) => [(FilePath,LCSC.ParsedProgram ext)] -> [WF.FunctionName] -> [(FilePath, Word64,WF.FunctionName)] -> IO (SFT.CrucibleSyntaxOverrides w () sym arch)
+loadParsedPrograms :: forall ext sym arch w . (ext ~ DMS.MacawExt arch, DMM.MemWidth w, LCCE.IsSyntaxExtension ext) => [(FilePath,LCSC.ParsedProgram ext)] -> [WF.FunctionName] -> [(FilePath, Word64,WF.FunctionName)] -> IO (SFT.CrucibleSyntaxOverrides w () sym arch)
 loadParsedPrograms pathProgs startupOverrides funAddrOverrides = do
   overrides <- traverse (uncurry parsedProgToFunctionOverride) pathProgs
   let ovmap = Map.fromList $ map (\sov@(SF.SomeFunctionOverride ov) -> (SF.functionName ov, sov)) overrides
@@ -108,7 +109,9 @@ crucibleProgramToFunctionOverride sym prog = do
 
     -- Get entry point of override
     case List.partition (isEntryPoint (ST.crEntry prog)) (ST.crCFGs prog) of
-      ([LCSC.ACFG argTypes retType cfg], aux) -> do
+      ([LCCR.AnyCFG cfg], aux) -> do
+              let argTypes = LCCR.cfgArgTypes cfg
+              let retType = LCCR.cfgReturnType cfg
               let e = WF.functionNameFromText $ DT.pack $ ST.crEntry prog
               let argMap = SFA.bitvectorArgumentMapping argTypes
                   (ptrTypes, ptrTypeMapping) = SFA.pointerArgumentMappping argMap
@@ -151,27 +154,29 @@ genInitOvHooks sym prog = do
     let (inits, _) = List.partition (isInitOv (ST.crOvInits prog)) (ST.crOvHandleMap prog)
     mapM (wrappedOverrideToInitOv sym) inits
 
-acfgToInitOverride ::  (STC.StubsArch arch, SPR.Preamble arch) =>  [LCS.FnBinding p sym (DMS.MacawExt arch)] -> [LCS.FnBinding p sym (DMS.MacawExt arch)] -> LCSC.ACFG (DMS.MacawExt arch) -> IO  (SF.FunctionOverride p sym Ctx.EmptyCtx arch LCT.UnitType)
-acfgToInitOverride preambleBindings ovBindings (LCSC.ACFG Ctx.Empty LCT.UnitRepr cfg) = do
-  let name = LCF.handleName (LCCR.cfgHandle cfg)
-  let argMap = SFA.bitvectorArgumentMapping Ctx.Empty
-      (ptrTypes, ptrTypeMapping) = SFA.pointerArgumentMappping argMap
-      retRepr = SFA.promoteBVToPtr LCT.UnitRepr
-  case LCCS.toSSA cfg of
-                LCCC.SomeCFG ssaCFG -> return $ (SF.FunctionOverride {
-                    SF.functionName=name,
-                    SF.functionGlobals=mempty,
-                    SF.functionExterns=mempty,
-                    SF.functionArgTypes=ptrTypes,
-                    SF.functionReturnType=retRepr,
-                    SF.functionAuxiliaryFnBindings=preambleBindings++ovBindings, --Should have preamble + overrides here
-                    SF.functionForwardDeclarations=mempty,
-                    SF.functionOverride= \bak args _ _ -> do
-                        pointerArgs <- liftIO $ SFA.buildFunctionOverrideArgs bak argMap ptrTypeMapping args
-                        userRes <- LCS.callCFG ssaCFG (LCS.RegMap pointerArgs)
-                        SF.OverrideResult [] . LCS.regValue <$> liftIO (SFA.convertBitvector bak retRepr userRes)
-                  })
-acfgToInitOverride _ _ (LCSC.ACFG _ _ cfg)= fail ("Attempted to generate init override with invalid signature: " ++ show (LCCR.cfgHandle cfg))
+acfgToInitOverride ::  (STC.StubsArch arch, SPR.Preamble arch) =>  [LCS.FnBinding p sym (DMS.MacawExt arch)] -> [LCS.FnBinding p sym (DMS.MacawExt arch)] -> LCCR.AnyCFG (DMS.MacawExt arch) -> IO  (SF.FunctionOverride p sym Ctx.EmptyCtx arch LCT.UnitType)
+acfgToInitOverride preambleBindings ovBindings (LCCR.AnyCFG cfg) =
+  case (LCCR.cfgArgTypes cfg, LCCR.cfgReturnType cfg) of
+    (Ctx.Empty, LCT.UnitRepr) -> do
+      let name = LCF.handleName (LCCR.cfgHandle cfg)
+      let argMap = SFA.bitvectorArgumentMapping Ctx.Empty
+          (ptrTypes, ptrTypeMapping) = SFA.pointerArgumentMappping argMap
+          retRepr = SFA.promoteBVToPtr LCT.UnitRepr
+      case LCCS.toSSA cfg of
+                    LCCC.SomeCFG ssaCFG -> return $ (SF.FunctionOverride {
+                        SF.functionName=name,
+                        SF.functionGlobals=mempty,
+                        SF.functionExterns=mempty,
+                        SF.functionArgTypes=ptrTypes,
+                        SF.functionReturnType=retRepr,
+                        SF.functionAuxiliaryFnBindings=preambleBindings++ovBindings, --Should have preamble + overrides here
+                        SF.functionForwardDeclarations=mempty,
+                        SF.functionOverride= \bak args _ _ -> do
+                            pointerArgs <- liftIO $ SFA.buildFunctionOverrideArgs bak argMap ptrTypeMapping args
+                            userRes <- LCS.callCFG ssaCFG (LCS.RegMap pointerArgs)
+                            SF.OverrideResult [] . LCS.regValue <$> liftIO (SFA.convertBitvector bak retRepr userRes)
+                      })
+    _ -> fail ("Attempted to generate init override with invalid signature: " ++ show (LCCR.cfgHandle cfg))
 
 wrappedOverrideToInitOv :: (STC.StubsArch arch, SPR.Preamble arch) => SC.Sym sym -> ST.SomeWrappedOverride arch -> IO  (SF.FunctionOverride p sym Ctx.EmptyCtx arch LCT.UnitType)
 wrappedOverrideToInitOv sym (ST.SomeWrappedOverride (ST.WrappedOverride ovf (STC.StubHandle Ctx.Empty SA.StubsUnitRepr n))) = do
@@ -198,7 +203,7 @@ wrappedOverrideToInitOv _ (ST.SomeWrappedOverride (ST.WrappedOverride _ (STC.Stu
 -- | Convert a 'LCSC.ParsedProgram' at a the given 'FilePath' to a function
 -- override.
 parsedProgToFunctionOverride ::
-  ( ext ~ DMS.MacawExt arch ) =>
+  ( ext ~ DMS.MacawExt arch, LCCE.IsSyntaxExtension ext ) =>
   String ->
   LCSC.ParsedProgram ext ->
   IO (SF.SomeFunctionOverride () sym arch)
@@ -220,36 +225,38 @@ parsedProgToFunctionOverride path parsedProg = do
 
 -- | Does a function have the same name as the @.cbl@ file in which it is
 -- defined?
-isEntryPoint :: String -> LCSC.ACFG ext -> Bool
+isEntryPoint :: String -> LCCR.AnyCFG ext -> Bool
 isEntryPoint path acfg =
   acfgHandleName acfg == DS.fromString path
 
-isInitPoint :: [String] -> LCSC.ACFG ext -> Bool
+isInitPoint :: [String] -> LCCR.AnyCFG ext -> Bool
 isInitPoint initNames acfg = show (acfgHandleName acfg) `elem` initNames
 
 isInitOv :: [String] -> ST.SomeWrappedOverride arch -> Bool
 isInitOv initNames (ST.SomeWrappedOverride (ST.WrappedOverride _ (STC.StubHandle _ _ hdl) )) = show (LCF.handleName hdl) `elem` initNames
 
--- | Retrieve the 'WF.FunctionName' in the handle in a 'LCSC.ACFG'.
-acfgHandleName :: LCSC.ACFG ext -> WF.FunctionName
-acfgHandleName (LCSC.ACFG _ _ g) = LCF.handleName (LCCR.cfgHandle g)
+-- | Retrieve the 'WF.FunctionName' in the handle in a 'LCCR.AnyCFG'.
+acfgHandleName :: LCCR.AnyCFG ext -> WF.FunctionName
+acfgHandleName (LCCR.AnyCFG g) = LCF.handleName (LCCR.cfgHandle g)
 
 -- Convert an ACFG to a FunctionOverride
 acfgToFunctionOverride
-  :: ( ext ~ DMS.MacawExt arch )
+  :: ( ext ~ DMS.MacawExt arch, LCCE.IsSyntaxExtension ext )
   => WF.FunctionName
   -> Map.Map LCSA.GlobalName (Some LCS.GlobalVar)
   -- ^ GlobalVars used in function override
   -> Map.Map LCSA.GlobalName (Some LCS.GlobalVar)
   -- ^ Externs declared in the override
   -> Map.Map WF.FunctionName LCF.SomeHandle
   -- ^ Forward declarations declared in the override
-  -> [LCSC.ACFG ext]
+  -> [LCCR.AnyCFG ext]
   -- ^ The ACFGs for auxiliary functions
-  -> LCSC.ACFG ext
+  -> LCCR.AnyCFG ext
   -> SF.SomeFunctionOverride () sym arch
-acfgToFunctionOverride name globals externs fwdDecs auxCFGs (LCSC.ACFG argTypes retType cfg) =
-  let argMap = SFA.bitvectorArgumentMapping argTypes
+acfgToFunctionOverride name globals externs fwdDecs auxCFGs (LCCR.AnyCFG cfg) =
+  let argTypes = LCCR.cfgArgTypes cfg
+      retType = LCCR.cfgReturnType cfg
+      argMap = SFA.bitvectorArgumentMapping argTypes
       (ptrTypes, ptrTypeMapping) = SFA.pointerArgumentMappping argMap
       retRepr = SFA.promoteBVToPtr retType
   in case LCCS.toSSA cfg of
@@ -275,9 +282,9 @@ acfgToFunctionOverride name globals externs fwdDecs auxCFGs (LCSC.ACFG argTypes
              SF.OverrideResult [] . LCS.regValue <$> liftIO (SFA.convertBitvector bak retRepr userRes)
          }
 
--- | Convert an 'LCSC.ACFG' to a 'LCS.FnBinding'.
-acfgToFnBinding :: forall sym ext p. LCSC.ACFG ext -> LCS.FnBinding p sym ext
-acfgToFnBinding (LCSC.ACFG _ _ g) =
+-- | Convert an 'LCCR.AnyCFG' to a 'LCS.FnBinding'.
+acfgToFnBinding :: forall sym ext p. LCCE.IsSyntaxExtension ext => LCCR.AnyCFG ext -> LCS.FnBinding p sym ext
+acfgToFnBinding (LCCR.AnyCFG g) =
   case LCCS.toSSA g of
     LCCC.SomeCFG ssa ->
       LCS.FnBinding (LCCR.cfgHandle g)

diff --git a/submodules/crucible b/submodules/crucible
diff --git a/tests/Infrastructure.hs b/tests/Infrastructure.hs
@@ -28,7 +28,6 @@ import qualified Stubs.EnvVar as AEnv
 
 import qualified Stubs.Memory as AM
 import qualified Stubs.Solver as AS
-import qualified Lang.Crucible.Syntax.Concrete as LCSC
 import qualified Data.Macaw.Symbolic as DMS
 
 import           Data.Macaw.BinaryLoader.X86 ()
@@ -45,6 +44,7 @@ import qualified Lang.Crucible.Simulator.GlobalState as LCSG
 import qualified Lang.Crucible.LLVM.SymIO as LCLS
 import qualified System.IO as IO
 import qualified Lang.Crucible.CFG.Core as LCCC
+import qualified Lang.Crucible.CFG.Reg as LCCR
 import qualified Lang.Crucible.Analysis.Postdom as LCAP
 import qualified Lang.Crucible.CFG.SSAConversion as LCSSA
 import qualified Lang.Crucible.Types as LCT
@@ -193,7 +193,7 @@ symexec bak halloc prog cfg args retRepr check ovs = do --todo link ovs
                     LCS.regValue <$> LCS.callCFG cfg (LCS.RegMap args)
 
   let cfgs = ST.crCFGs prog
-  let hdlMap = foldr (\(LCSC.ACFG _ _ icfg) acc -> case LCSSA.toSSA icfg of
+  let hdlMap = foldr (\(LCCR.AnyCFG icfg) acc -> case LCSSA.toSSA icfg of
             (LCCC.SomeCFG ccfg) -> LCF.insertHandleMap (LCCC.cfgHandle ccfg)
                                        (LCS.UseCFG ccfg (LCAP.postdomInfo ccfg))
                                        acc