crucible: Introduce a helper to bind CFGs to their handles (#1151)

GaloisInc · Dec 7, 2023 · 501623d · 501623d
1 parent 96343bf
commit 501623d
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs
@@ -31,6 +31,7 @@ module Lang.Crucible.Simulator.OverrideSim
   , getSymInterface
   , ovrWithBackend
   , bindFnHandle
+  , bindCFG
   , exitExecution
   , getOverrideArgs
   , overrideError
@@ -246,6 +247,12 @@ bindFnHandle ::
 bindFnHandle h s =
   stateContext . functionBindings %= FnBindings . insertHandleMap h s . fnBindings
 
+-- | Bind a CFG to its handle.
+--
+-- Computes postdominator information.
+bindCFG :: CFG ext blocks args ret -> OverrideSim p sym ext rtp a r ()
+bindCFG c = bindFnHandle (cfgHandle c) (UseCFG c (postdomInfo c))
+
 ------------------------------------------------------------------------
 -- Mutable variables
 

diff --git a/crux-mir/src/Mir/Overrides.hs b/crux-mir/src/Mir/Overrides.hs
@@ -440,8 +440,7 @@ bindFn _symOnline _cs fn cfg =
   ovrWithBackend $ \bak ->
   let s = backendGetSym bak in
   case Map.lookup (textIdKey fn) (overrides bak) of
-    Nothing ->
-      bindFnHandle (cfgHandle cfg) $ UseCFG cfg (postdomInfo cfg)
+    Nothing -> bindCFG cfg
     Just (SomeTypedOverride o@(TypedOverride f argTys retTy)) ->
       case (,) <$> testEquality (cfgReturnType cfg) retTy <*> testEquality (cfgArgTypes cfg) argTys of
         Nothing -> error $ "Mismatching override type for " ++ Text.unpack fn ++