From 5eaa318878162e14dfd6eac6cc49ac505593bb10 Mon Sep 17 00:00:00 2001 From: Ferinko Date: Thu, 9 Mar 2023 13:19:53 +0100 Subject: [PATCH] add docs, implement refactorings * The optimisation of splitting on preconditions is no longer optional, because we rely on existential instantation for logical variables in posts of modules that optimise pres - the original way of dealing with existentials via checkpoints has been completely removed due to its error proneness. * Added inline and haddock toplevel docstrings for various functions. --- src/Horus/CFGBuild.hs | 101 ++++++++++++++++++++++--------- src/Horus/CFGBuild/Runner.hs | 5 ++ src/Horus/CairoSemantics.hs | 99 +++++++++++++++++-------------- src/Horus/Global.hs | 11 ++-- src/Horus/Module.hs | 112 ++++++++++++++++++++++++++--------- 5 files changed, 221 insertions(+), 107 deletions(-) diff --git a/src/Horus/CFGBuild.hs b/src/Horus/CFGBuild.hs index 2dda756a..36112a65 100644 --- a/src/Horus/CFGBuild.hs +++ b/src/Horus/CFGBuild.hs @@ -125,8 +125,8 @@ liftF' = CFGBuildL . liftF addVertex :: Label -> CFGBuildL Vertex addVertex l = liftF' (AddVertex l Nothing id) -addOptimizingVertex :: Label -> ScopedFunction -> CFGBuildL Vertex -addOptimizingVertex l f = liftF' (AddVertex l (Just f) id) +addOptimisingVertex :: Label -> ScopedFunction -> CFGBuildL Vertex +addOptimisingVertex l f = liftF' (AddVertex l (Just f) id) addArc :: Vertex -> Vertex -> [LabeledInst] -> ArcCondition -> FInfo -> CFGBuildL () addArc vFrom vTo insts test f = liftF' (AddArc vFrom vTo insts test f ()) @@ -155,11 +155,16 @@ getSvarSpecs = liftF' (GetSvarSpecs id) getVerts :: Label -> CFGBuildL [Vertex] getVerts l = liftF' (GetVerts l id) --- It is enforced that for any one PC, one can add at most a single salient vertex +{- | Saliant vertices can be thought of as 'main' vertices of the CFG, meaning that +if one wants to reason about flow control of the program, one should query salient vertices. + +Certain program transformations and optimisations can add various additional nodes into the CFG, +whose primary purpose is not to reason about control flow. + +It is enforced that for any one PC, one can add at most a single salient vertex. -} getSalientVertex :: Label -> CFGBuildL Vertex getSalientVertex l = do verts <- filter (not . isOptimising) <$> getVerts l - -- This can be at most one, so len <> 1 implies there are no vertices case verts of [vert] -> pure vert _ -> throw $ "No vertex with label: " <> tShow l @@ -192,9 +197,13 @@ segmentInsts (Segment ne) = toList ne buildFrame :: Set ScopedFunction -> [LabeledInst] -> Program -> CFGBuildL () buildFrame inlinables rows prog = do let segments = breakIntoSegments (programLabels rows $ p_identifiers prog) rows + -- It is necessary to add all vertices prior to calling `addArcsFrom`. segmentsWithVerts <- for segments $ \s -> addVertex (segmentLabel s) <&> (s,) - for_ segmentsWithVerts $ \(s, v) -> addArcsFrom inlinables prog rows s v True + for_ segmentsWithVerts . uncurry $ addArcsFrom inlinables prog rows +{- | A simple procedure for splitting a stream of instructions into nonempty Segments based +on program labels, which more-or-less correspond with changes in control flow in the program. +We thus obtain linear segments of instructions without control flow. -} breakIntoSegments :: [Label] -> [LabeledInst] -> [Segment] breakIntoSegments _ [] = [] breakIntoSegments ls_ (i_ : is_) = coerce (go [] (i_ :| []) ls_ is_) @@ -209,29 +218,24 @@ breakIntoSegments ls_ (i_ : is_) = coerce (go [] (i_ :| []) ls_ is_) addArc' :: Vertex -> Vertex -> [LabeledInst] -> CFGBuildL () addArc' lFrom lTo insts = addArc lFrom lTo insts ACNone Nothing -addArcsFrom :: Set ScopedFunction -> Program -> [LabeledInst] -> Segment -> Vertex -> Bool -> CFGBuildL () -addArcsFrom inlinables prog rows seg@(Segment s) vFrom optimiseWithSplit +{- | This function adds arcs (edges) into the CFG and labels them with instructions that are +to be executed when traversing from one vertex to another. + +Currently, we do not have an optimisation post-processing pass in Horus and we therefore +also include an optimisation here that generates an extra vertex in order to implement +separate checking of preconditions for abstracted functions.-} +addArcsFrom :: Set ScopedFunction -> Program -> [LabeledInst] -> Segment -> Vertex -> CFGBuildL () +addArcsFrom inlinables prog rows seg@(Segment s) vFrom | Call <- i_opCode endInst = - let callee = uncheckedScopedFOfPc (p_identifiers prog) (uncheckedCallDestination lInst) - in do - if callee `Set.member` inlinables - then do - salientCalleeV <- getSalientVertex (sf_pc callee) - addArc vFrom salientCalleeV insts ACNone . Just $ ArcCall endPc (sf_pc callee) - else do - salientLinearV <- getSalientVertex (nextSegmentLabel seg) - addArc' vFrom salientLinearV insts - svarSpecs <- getSvarSpecs - when (optimiseWithSplit && sf_scopedName callee `Set.notMember` svarSpecs) $ do - -- Suppose F calls G where G has a precondition. We synthesize an extra module - -- Pre(F) -> Pre(G) to check whether Pre(G) holds. The standard module for F - -- is then Pre(F) -> Post(F) (conceptually, unless there's a split in the middle, etc.), - -- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have - -- been checked by the module induced by the ghost vertex. - ghostV <- addOptimizingVertex (nextSegmentLabel seg) callee - pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee - addAssertion ghostV $ quantifyEx pre - addArc' vFrom ghostV insts + -- An inlined call pretends as though the stream of instructions continues without breaking + -- through the function being inlined. + + -- An abstracted call does not break control flow and CONCEPTUALLY asserts 'pre implies post'. + -- Conceptually is the operative word here because due to the way that APs 'flow' + -- in the program thus making the actual implication unnecessary plus the existance + -- of the optimisation in optimiseCheckingOfPre makes it such that the pre is checked + -- in a separate module. + if callee `Set.member` inlinables then beginInlining else abstractOver | Ret <- i_opCode endInst = -- Find the function corresponding to `endPc` and lookup its label. If we -- found the label, add arcs for each caller. @@ -256,6 +260,45 @@ addArcsFrom inlinables prog rows seg@(Segment s) vFrom optimiseWithSplit insts = segmentInsts seg inlinableLabels = Set.map sf_pc inlinables + callee = uncheckedScopedFOfPc (p_identifiers prog) (uncheckedCallDestination lInst) + + beginInlining = do + salientCalleeV <- getSalientVertex (sf_pc callee) + addArc vFrom salientCalleeV insts ACNone . Just $ ArcCall endPc (sf_pc callee) + + optimiseCheckingOfPre = do + -- Suppose F calls G where G has a precondition. We synthesize an extra module + -- Pre(F) -> Pre(G) to check whether Pre(G) holds. The standard module for F + -- is then Pre(F) -> Post(F) (conceptually, unless there's a split in the middle, etc.), + -- in which Pre(G) is assumed to hold at the PC of the G call site, as it will have + -- been checked by the module induced by the ghost vertex. + ghostV <- addOptimisingVertex (nextSegmentLabel seg) callee + pre <- maybe (mkPre Expr.True) mkPre . fs'_pre <$> getFuncSpec callee + + -- Important note on the way we deal with logical variables. These are @declare-d and + -- their values can be bound in preconditions. They generate existentials which only occur + -- in our models here and require special treatment, in addition to being somewhat + -- difficult for SMT checkers to deal with. + + -- First note that these preconditions now become optimising-module postconditions. + -- We existentially quantify all logical variables present in the expression, thus in the + -- following example: + -- func foo: + -- call bar // where bar refers to $my_logical_var + -- We get an optimising module along the lines of: + -- Pre(foo) -> Pre(bar) where Pre(bar) contains \exists my_logical_var, ... + -- We can then check whether this instantiation exists in the optimising module exclusively. + -- The module that then considers that pre holds as a fact now has the luxury of not having + -- to deal with existential quantifiers, as it can simply 'declare' them as free variables. + addAssertion ghostV $ quantifyEx pre + addArc' vFrom ghostV insts + + abstractOver = do + salientLinearV <- getSalientVertex (nextSegmentLabel seg) + addArc' vFrom salientLinearV insts + svarSpecs <- getSvarSpecs + when (sf_scopedName callee `Set.notMember` svarSpecs) optimiseCheckingOfPre + addRetArc :: Label -> CFGBuildL () addRetArc pc = do retV <- getSalientVertex endPc @@ -274,6 +317,8 @@ addArcsFrom inlinables prog rows seg@(Segment s) vFrom optimiseWithSplit let lvars = gatherLogicalVariables expr in foldr Expr.ExistsFelt expr lvars +{- | This function labels appropriate vertices (at 'ret'urns) with their respective postconditions. +-} addAssertions :: Set ScopedFunction -> Identifiers -> CFGBuildL () addAssertions inlinables identifiers = do for_ (Map.toList identifiers) $ \(idName, def) -> case def of @@ -284,6 +329,8 @@ addAssertions inlinables identifiers = do post <- fs'_post <$> getFuncSpec func retVs <- mapM getSalientVertex =<< getRets idName case (pre, post) of + -- (Nothing, Nothing) means the function has no pre nor post. We refrain from + -- adding Pre := True and Post := True in case the function can be inlined. (Nothing, Nothing) -> when (fu_pc f `Set.notMember` Set.map sf_pc inlinables) $ for_ retVs (`addAssertion` mkPost Expr.True) diff --git a/src/Horus/CFGBuild/Runner.hs b/src/Horus/CFGBuild/Runner.hs index 8ccd2e50..a27a4e70 100644 --- a/src/Horus/CFGBuild/Runner.hs +++ b/src/Horus/CFGBuild/Runner.hs @@ -27,6 +27,11 @@ import Horus.FunctionAnalysis (FInfo) type Impl = ReaderT ContractInfo (ExceptT Text (State CFG)) +{- | This represents a quasi Control Flow Graph. + +Normally, they store instructions in nodes and edges represent flow control / jumps. +In our case, we store instructions in edges and nodes represent points of program +with associated logical assertions - preconditions, postconditions and invariants. -} data CFG = CFG { cfg_vertices :: [Vertex] , cfg_arcs :: Map Vertex [(Vertex, [LabeledInst], ArcCondition, FInfo)] diff --git a/src/Horus/CairoSemantics.hs b/src/Horus/CairoSemantics.hs index 1e518ee8..dbee7e7b 100644 --- a/src/Horus/CairoSemantics.hs +++ b/src/Horus/CairoSemantics.hs @@ -28,7 +28,6 @@ import Lens.Micro ((^.), _1) import Horus.CallStack as CS (CallEntry, CallStack) import Horus.Expr (Cast (..), Expr ((:+)), Ty (..), (.&&), (./=), (.<), (.<=), (.==), (.=>), (.||)) import Horus.Expr qualified as Expr -import Horus.Expr qualified as TSMT import Horus.Expr.Util (gatherLogicalVariables, suffixLogicalVariables) import Horus.Expr.Vars ( builtinAligned @@ -57,7 +56,7 @@ import Horus.Instruction , uncheckedCallDestination ) import Horus.Label (Label (..), tShowLabel) -import Horus.Module (Module (..), ModuleSpec (..), PlainSpec (..), isOptimising, richToPlainSpec) +import Horus.Module (Module (..), ModuleSpec (..), PlainSpec (..), isOptimising, richToPlainSpec, ModuleData (ModuleData, md_prog, md_lastPc, md_spec), moduleData, moduleOptimisesPreForF) import Horus.Program (ApTracking (..)) import Horus.SW.Builtin (Builtin, BuiltinOffsets (..)) import Horus.SW.Builtin qualified as Builtin (name) @@ -105,7 +104,8 @@ data CairoSemanticsF a | UpdateStorage Storage a | GetStorage (Storage -> a) | Throw Text - deriving stock (Functor) + +deriving instance Functor CairoSemanticsF type CairoSemanticsL = F CairoSemanticsF @@ -273,17 +273,21 @@ getFp :: CairoSemanticsL (Expr TFelt) getFp = getFp' Nothing moduleStartAp :: Module -> CairoSemanticsL (Expr TFelt) -moduleStartAp Module{m_prog = []} = getStackTraceDescr <&> Expr.const . ("ap!" <>) -moduleStartAp Module{m_prog = (pc0, _) : _} = getAp pc0 +moduleStartAp mdl = + case md_prog (moduleData mdl) of + [] -> getStackTraceDescr <&> Expr.const . ("ap!" <>) + (pc0, _) : _ -> getAp pc0 moduleEndAp :: Module -> CairoSemanticsL (Expr TFelt) -moduleEndAp Module{m_prog = []} = getStackTraceDescr <&> Expr.const . ("ap!" <>) -moduleEndAp m@Module{m_prog = _} = getAp' (Just callstack) pc where (callstack, pc) = m_lastPc m +moduleEndAp mdl = + case md_prog (moduleData mdl) of + [] -> getStackTraceDescr <&> Expr.const . ("ap!" <>) + _ -> getAp' (Just callstack) pc where (callstack, pc) = md_lastPc (moduleData mdl) encodeModule :: Module -> CairoSemanticsL () -encodeModule m@Module{..} = case m_spec of - MSRich spec -> encodeRichSpec m spec - MSPlain spec -> encodePlainSpec m spec +encodeModule mdl = case md_spec (moduleData mdl) of + MSRich spec -> encodeRichSpec mdl spec + MSPlain spec -> encodePlainSpec mdl spec {- | Gather the assertions and other state (in the `ConstraintsState` contained in `CairoSemanticsL`) associated with a function specification that contains @@ -316,11 +320,8 @@ encodePlainSpec mdl PlainSpec{..} = do assert (fp .<= apStart) assertPre =<< prepare' apStart fp ps_pre - let instrs = m_prog mdl - -- The last FP might be influenced in the optimizing case, we need to grab it as propagated -- by the encoding of the semantics of the call. - lastFp <- fromMaybe fp . join . safeLast <$> for @@ -329,13 +330,13 @@ encodePlainSpec mdl PlainSpec{..} = do mkInstructionConstraints instr (getNextPcInlinedWithFallback instrs idx) - (m_optimisesF mdl) - (m_jnzOracle mdl) + (moduleOptimisesPreForF mdl) + oracle ) expect =<< preparePost apEnd lastFp ps_post (isOptimising mdl) - whenJust (nonEmpty (m_prog mdl)) $ \neInsts -> do + whenJust (nonEmpty instrs) $ \neInsts -> do -- Normally, 'call's are accompanied by 'ret's for inlined functions. With the optimisation -- that splits modules on pre of every non-inlined function, some modules 'finish' their -- enconding without actually reaching a subsequent 'ret' for every inlined 'call', thus @@ -347,7 +348,9 @@ encodePlainSpec mdl PlainSpec{..} = do resetStack mkApConstraints apEnd neInsts resetStack - mkBuiltinConstraints apEnd neInsts (m_optimisesF mdl) + mkBuiltinConstraints apEnd neInsts (moduleOptimisesPreForF mdl) + where + (ModuleData _ instrs oracle _ _) = moduleData mdl exMemoryRemoval :: Expr TBool -> CairoSemanticsL ([MemoryVariable] -> Expr TBool) exMemoryRemoval expr = do @@ -445,6 +448,8 @@ mkInstructionConstraints lInst@(pc, Instruction{..}) nextPc optimisingF jnzOracl Nothing -> pure Nothing Ret -> pop $> Nothing +{- | A particular case of mkInstructionConstraints for the instruction 'call'. +-} mkCallConstraints :: Label -> Label -> @@ -457,44 +462,46 @@ mkCallConstraints pc nextPc fp optimisingF f = do nextAp <- prepare pc calleeFp (Vars.fp .== Vars.ap + 2) saveOldFp <- prepare pc fp (memory Vars.ap .== Vars.fp) setNextPc <- prepare pc fp (memory (Vars.ap + 1) .== fromIntegral (unLabel nextPc)) - assert (TSMT.and [nextAp, saveOldFp, setNextPc]) + assert (Expr.and [nextAp, saveOldFp, setNextPc]) push stackFrame - -- We need only a part of the call instruction's semantics for optimizing modules. -- Considering we have already pushed the stackFrame by now, we need to make sure that either -- the function is inlinable and we'll encounter a 'ret', or we need to pop right away -- once we encode semantics of the function. - -- Determine whether the current function matches the function being optimised exactly - - -- this necessitates comparing execution traces. - executionContext <- getStackTraceDescr - optimisedFExecutionContext <- getStackTraceDescr' ((^. _1) <$> optimisingF) - if isJust optimisingF && executionContext == optimisedFExecutionContext - then Just <$> getFp <* pop - else do - -- This is reachable unless the module is optimizing, in which case the precondition - -- of the function is necessarily the last thing being checked; as such, the semantics - -- of the function being invoked must not be considered. - canInline <- isInlinable f - if canInline - then pure Nothing -- An inlined function will have a 'ret' at some point, do not pop here. - else do - (FuncSpec pre post storage) <- getFuncSpec f <&> toFuncSpec - let pre' = suffixLogicalVariables lvarSuffix pre - post' = suffixLogicalVariables lvarSuffix post - preparedPre <- prepare nextPc calleeFp =<< storageRemoval pre' - -- Grab the state of all storage variables prior to executing the function body. - precedingStorage <- getStorage - updateStorage =<< traverseStorage (prepare nextPc calleeFp) storage - pop - -- Dereference storage variable reads with respect to `precedingStorage`. - preparedPost <- prepare nextPc calleeFp =<< storageRemoval' (Just precedingStorage) post' - assert preparedPre - assert preparedPost - pure Nothing + -- We need only a part of the call instruction's semantics for optimizing modules. + guardWith isModuleCheckingPre (Just <$> getFp <* pop) $ do + -- This is reachable unless the module is optimizing, in which case the precondition + -- of the function is necessarily the last thing being checked; as such, the semantics + -- of the function being invoked must not be considered. + guardWith (isInlinable f) (pure Nothing) $ do -- An inlined function will have a 'ret' at some point, do not pop here. + (FuncSpec pre post storage) <- getFuncSpec f <&> toFuncSpec + let pre' = suffixLogicalVariables lvarSuffix pre + post' = suffixLogicalVariables lvarSuffix post + preparedPre <- prepare nextPc calleeFp =<< storageRemoval pre' + -- Grab the state of all storage variables prior to executing the function body. + precedingStorage <- getStorage + updateStorage =<< traverseStorage (prepare nextPc calleeFp) storage + pop + -- Dereference storage variable reads with respect to `precedingStorage`. + preparedPost <- prepare nextPc calleeFp =<< storageRemoval' (Just precedingStorage) post' + -- One would normally expect to see assert (pre -> post). + -- However, pre will be checked in a separate 'optimising' module and we can therefore simply + -- assert it holds here. If it does not, the corresponding pre-checking module will fail, + -- thus failing the judgement for the entire function. + assert preparedPre + assert preparedPost + pure Nothing where lvarSuffix = "+" <> tShowLabel pc calleePc = sf_pc f stackFrame = (pc, calleePc) + -- Determine whether the current function matches the function being optimised exactly - + -- this necessitates comparing execution traces. + isModuleCheckingPre = do + executionContext <- getStackTraceDescr + optimisedFExecutionContext <- getStackTraceDescr' ((^. _1) <$> optimisingF) + pure (isJust optimisingF && executionContext == optimisedFExecutionContext) + guardWith condM val cont = do cond <- condM; if cond then val else cont traverseStorage :: (forall a. Expr a -> CairoSemanticsL (Expr a)) -> Storage -> CairoSemanticsL Storage traverseStorage preparer = traverse prepareWrites diff --git a/src/Horus/Global.hs b/src/Horus/Global.hs index 9ac57adf..82e0245e 100644 --- a/src/Horus/Global.hs +++ b/src/Horus/Global.hs @@ -39,7 +39,7 @@ import Horus.Expr qualified as Expr import Horus.Expr.Util (gatherLogicalVariables) import Horus.FunctionAnalysis (ScopedFunction (ScopedFunction, sf_pc), isWrapper) import Horus.Logger qualified as L (LogL, logDebug, logError, logInfo, logWarning) -import Horus.Module (Module (..), ModuleL, gatherModules, getModuleNameParts) +import Horus.Module (Module (..), ModuleL, gatherModules, getModuleNameParts, moduleData, ModuleData (md_calledF, md_prog), moduleOptimisesPreForF) import Horus.Preprocessor (HorusResult (..), PreprocessorL, SolverResult (..), goalListToTextList, optimizeQuery, solve) import Horus.Preprocessor.Runner (PreprocessorEnv (..)) import Horus.Preprocessor.Solvers (Solver, SolverSettings, filterMathsat, includesMathsat, isEmptySolver) @@ -159,7 +159,8 @@ makeModules (cfg, allow) = =<< getSources extractConstraints :: Module -> GlobalL ConstraintsState -extractConstraints mdl = runCairoSemanticsL (initialWithFunc $ m_calledF mdl) (encodeModule mdl) +extractConstraints mdl = + runCairoSemanticsL (initialWithFunc . md_calledF . moduleData $ mdl) (encodeModule mdl) data SolvingInfo = SolvingInfo { si_moduleName :: Text @@ -196,7 +197,7 @@ solveModule m = do identifiers <- getIdentifiers let (qualifiedFuncName, labelsSummary, oracleSuffix, optimisesF) = getModuleNameParts identifiers m moduleName = mkLabeledFuncName qualifiedFuncName labelsSummary <> oracleSuffix <> optimisesF - inlinable = m_calledF m `elem` Set.map sf_pc inlinables + inlinable = md_calledF (moduleData m) `elem` Set.map sf_pc inlinables result <- removeMathSAT m (mkResult moduleName) pure SolvingInfo @@ -204,7 +205,7 @@ solveModule m = do , si_funcName = qualifiedFuncName , si_result = result , si_inlinable = inlinable - , si_optimisesF = m_optimisesF m + , si_optimisesF = moduleOptimisesPreForF m } where mkResult :: Text -> GlobalL HorusResult @@ -253,7 +254,7 @@ removeMathSAT :: Module -> GlobalL a -> GlobalL a removeMathSAT m run = do conf <- getConfig let solver = cfg_solver conf - usesLvars <- or <$> traverse instUsesLvars (m_prog m) + usesLvars <- or <$> traverse instUsesLvars (md_prog (moduleData m)) if includesMathsat solver && usesLvars then do let solver' = filterMathsat solver diff --git a/src/Horus/Module.hs b/src/Horus/Module.hs index 0f08fdbe..1c839d80 100644 --- a/src/Horus/Module.hs +++ b/src/Horus/Module.hs @@ -10,6 +10,9 @@ module Horus.Module , richToPlainSpec , isOptimising , dropMain + , moduleData + , ModuleData (..) + , moduleOptimisesPreForF ) where @@ -21,7 +24,6 @@ import Data.Foldable (for_, traverse_) import Data.List.NonEmpty (NonEmpty) import Data.Map (Map) import Data.Map qualified as Map (elems, empty, insert, map, null, toList) -import Data.Maybe (isJust) import Data.Text (Text) import Data.Text qualified as Text (concat, intercalate) import Lens.Micro (ix, (^.)) @@ -43,14 +45,17 @@ import Horus.SW.FuncSpec (FuncSpec (..)) import Horus.SW.Identifier (Function (..), getFunctionPc, getLabelPc) import Horus.SW.ScopedName (ScopedName (..), toText) -data Module = Module - { m_spec :: ModuleSpec - , m_prog :: [LabeledInst] - , m_jnzOracle :: Map (NonEmpty Label, Label) Bool - , m_calledF :: Label - , m_lastPc :: (CallStack, Label) - , m_optimisesF :: Maybe (CallStack, ScopedFunction) - } +data ModuleData = ModuleData + { md_spec :: ModuleSpec + , md_prog :: [LabeledInst] + , md_jnzOracle :: Map (NonEmpty Label, Label) Bool + , md_calledF :: Label + , md_lastPc :: (CallStack, Label) +} deriving stock (Show) + +data Module = + StandardModule ModuleData + | OptimisingModule ModuleData (CallStack, ScopedFunction) deriving stock (Show) data ModuleSpec = MSRich FuncSpec | MSPlain PlainSpec @@ -59,8 +64,17 @@ data ModuleSpec = MSRich FuncSpec | MSPlain PlainSpec data PlainSpec = PlainSpec {ps_pre :: Expr TBool, ps_post :: Expr TBool} deriving stock (Show) +moduleData :: Module -> ModuleData +moduleData (StandardModule md) = md +moduleData (OptimisingModule md _) = md + +moduleOptimisesPreForF :: Module -> Maybe (CallStack, ScopedFunction) +moduleOptimisesPreForF (StandardModule _) = Nothing +moduleOptimisesPreForF (OptimisingModule _ f) = Just f + isOptimising :: Module -> Bool -isOptimising = isJust . m_optimisesF +isOptimising (StandardModule _) = False +isOptimising (OptimisingModule _ _) = True richToPlainSpec :: FuncSpec -> PlainSpec richToPlainSpec FuncSpec{..} = PlainSpec{ps_pre = fs_pre .&& ap .== fp, ps_post = fs_post} @@ -193,7 +207,7 @@ descrOfOracle oracle = it does not contain the rest of the labels. -} getModuleNameParts :: Identifiers -> Module -> (Text, Text, Text, Text) -getModuleNameParts idents (Module spec prog oracle calledF _ optimisesF) = +getModuleNameParts idents mdl = case beginOfModule prog of Nothing -> ("", "empty: " <> pprExpr post, "", "") Just label -> @@ -202,13 +216,14 @@ getModuleNameParts idents (Module spec prog oracle calledF _ optimisesF) = (prefix, labelsSummary) = normalizedName scopedNames isFloatingLabel in (prefix, labelsSummary, descrOfOracle oracle, optimisingSuffix) where + (ModuleData spec prog oracle calledF _) = moduleData mdl post = case spec of MSRich fs -> fs_post fs; MSPlain ps -> ps_post ps - optimisingSuffix = case optimisesF of - Nothing -> "" - Just (callstack, f) -> + optimisingSuffix = case mdl of + StandardModule _ -> "" + OptimisingModule _ (callstack, f) -> let fName = toText . ScopedName . dropMain . sn_path . sf_scopedName $ f stack = digestOfCallStack (Map.map sf_scopedName (pcToFun idents)) callstack - in " Pre<" <> fName <> "|" <> stack <> ">" + in " Pre<" <> fName <> "|" <> stack <> ">" data Error = ELoopNoInvariant Label @@ -245,8 +260,7 @@ emitModule m = liftF' (EmitModule m ()) as visited. 'm' additionally takes a parameter that tells whether 'l' has been -visited before. --} +visited before. -} visiting :: (NonEmpty Label, Map (NonEmpty Label, Label) Bool, Vertex) -> (Bool -> ModuleL b) -> ModuleL b visiting vertexDesc action = liftF' (Visiting vertexDesc action id) @@ -266,12 +280,51 @@ extractPlainBuilder fs@(FuncSpec _pre _post state) gatherModules :: CFG -> [(Function, ScopedName, FuncSpec)] -> ModuleL () gatherModules cfg = traverse_ $ \(f, _, spec) -> gatherFromSource cfg f spec +{- | This function represents a depth first search through the CFG that uses as sentinels +(for where to begin and where to end) assertions in nodes, such that nodes that are not annotated +are traversed without stopping the search, gathering labels from respective edges that +represent instructions and concatenating them into final Modules, that are subsequently +transformed into actual *.smt2 queries. + +Thus, a module can comprise of 0 to several segments, where the precondition of the module +is the annotation of the node 'begin' that begins the first segment, the postcondition of the module +is the annotation of the node 'end' that ends the last segment and instructions of the module +are a concatenation of edge labels for the given path through the graph from 'begin' to 'end'. + +Note that NO node with an annotation can be encountered in the middle of one such path, +because annotated nodes are sentinels and the search would terminate. + +We distinguish between plain and rich modules. +A plain module is a self-contained 'sub-program' with its own semantics that is referentially pure +in the sense that it has no side-effects on the environment, i.e. does not access storage variables. + +A rich module is very much like a plain module except it allows side effects, +i.e. accesses to storage variables. -} gatherFromSource :: CFG -> Function -> FuncSpec -> ModuleL () gatherFromSource cfg function fSpec = do let verticesAtFuPc = verticesLabelledBy cfg $ fu_pc function for_ verticesAtFuPc $ \v -> visit Map.empty (initialWithFunc (fu_pc function)) [] SBRich v ACNone Nothing where + {- Revisiting nodes (thus looping) within the CFG is verboten in all cases but one, + specifically when we are jumping back to a label that is annotated with an invariant 'inv'. + In this case, we pretend that the 'begin' and 'end' is the same node, both of which + annotated with 'inv'. + + Thus, visit needs a way to keep track of nodes that have already been visited. However, + it is important to note that it is not sufficient to keep track of which program counters + we have touched in the CFG, as there are several ways to 'validly' revisit the same PC + without loopy behaviour, most prominently stemming from existence of ifs that converge + on the same path and presence of inlining where the same function can be called multiple times. + + In order to distinguish valid nodes in this context, we need the oracle for ifs as described in + the docs of getModuleNameParts and we need the callstack which keeps track of inlined functions + in very much the same way as 'normal' callstacks work, thus allowing us to identify + whether the execution of the current function is unique, or being revisited through + a 'wrong' path through the CFG. + + Oracles need a bit of extra information about which booltest passed - in the form of ArcCondition + and CallStack needs a bit of extra information about when call/ret are called, in the form of FInfo. -} visit :: Map (NonEmpty Label, Label) Bool -> CallStack -> @@ -309,20 +362,21 @@ gatherFromSource cfg function fSpec = do oracle' = updateOracle arcCond callstack' oracle assertions = map snd (cfg_assertions cfg ^. ix v) onFinalNode = null (cfg_arcs cfg ^. ix v) - emitPlain pre post = emit . MSPlain $ PlainSpec pre post - emitRich pre post = emit . MSRich . FuncSpec pre post $ fs_storage fSpec - - emit spec = - emitModule - ( Module spec acc oracle' (fu_pc function) (callstack', l) executionContextOfOptimisedF - ) - where - optimisingStackFrame = (fCallerPc, fCalledF) - where + + optimisingStackFrame = (fCallerPc, fCalledF) + where laballedCall@(fCallerPc, _) = last acc fCalledF = uncheckedCallDestination laballedCall - executionContextOfOptimisedF = - (push optimisingStackFrame callstack',) <$> v_optimisesF v + optimContext = + (push optimisingStackFrame callstack',) <$> v_optimisesF v + + emitPlain pre post = emit optimContext . MSPlain $ PlainSpec pre post + emitRich pre post = emit optimContext . MSRich . FuncSpec pre post $ fs_storage fSpec + + emit mbTrace spec = case mbTrace of + Nothing -> emitModule (StandardModule md) + Just trace -> emitModule (OptimisingModule md trace) + where md = ModuleData spec acc oracle' (fu_pc function) (callstack', l) visitArcs newOracle acc' pre v' = do let outArcs = cfg_arcs cfg ^. ix v'