From d5b6999b75c93e02e6aba3e4f897e0c905883e2b Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Thu, 7 Dec 2023 12:41:37 -0500 Subject: [PATCH] crucible: Introduce a helper to bind CFGs to their handles --- crucible/src/Lang/Crucible/Simulator/OverrideSim.hs | 7 +++++++ crux-mir/src/Mir/Overrides.hs | 3 +-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs b/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs index 459ae8309..130a98159 100644 --- 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 index 1a3e3ded3..f99325b23 100644 --- 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 ++