From b5cf203353fb92a0951b6af59e3aa14a625348ab Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 14 May 2024 12:37:05 -0700 Subject: [PATCH 01/26] add missing JSON serialization for ChoiceTree fixes issue where GUI would hang when trying to navigate to display a choice tree (i.e. prompt) --- src/Pate/TraceTree.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index 36b58624..4fdc60da 100644 --- a/src/Pate/TraceTree.hs +++ b/src/Pate/TraceTree.hs @@ -805,6 +805,9 @@ data ChoiceHeader k (nm_choice :: Symbol) a = data SomeChoiceHeader k = forall nm_choice nm_ret. SomeChoiceHeader (ChoiceHeader k nm_choice nm_ret) +instance JSON.ToJSON (SomeChoiceHeader k) where + toJSON (SomeChoiceHeader ch) = JSON.toJSON (symbolRepr $ choiceType ch) + instance IsTraceNode k "choiceTree" where type TraceNodeType k "choiceTree" = SomeChoiceHeader k type TraceNodeLabel "choiceTree" = String @@ -814,6 +817,8 @@ instance IsTraceNode k "choiceTree" where ,(Simplified_Detail, \nm _ -> PP.pretty nm) ,(Simplified, \nm _ -> PP.pretty nm) ] + jsonNode _ = nodeToJSON @k @"choiceTree" + data Choice k (nm_choice :: Symbol) a = Choice { choiceHeader :: ChoiceHeader k nm_choice a From 7e8dc31008825c24526df973fe904b07b084549d Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 14 May 2024 12:39:24 -0700 Subject: [PATCH 02/26] add utility functions for PairGraphM --- src/Pate/Monad/PairGraph.hs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Pate/Monad/PairGraph.hs b/src/Pate/Monad/PairGraph.hs index 5a2897b2..c970d52c 100644 --- a/src/Pate/Monad/PairGraph.hs +++ b/src/Pate/Monad/PairGraph.hs @@ -10,8 +10,10 @@ -- EquivM operations on a PairGraph module Pate.Monad.PairGraph ( withPG + , evalPG , withPG_ , liftPG + , liftPartEqM_ , catchPG , liftEqM , liftEqM_ @@ -60,6 +62,12 @@ withPG :: EquivM sym arch (a, PairGraph sym arch) withPG pg f = runStateT f pg +evalPG :: + PairGraph sym arch -> + PairGraphM sym arch a -> + EquivM sym arch a +evalPG pg f = fst <$> (withPG pg $ liftPG f) + withPG_ :: PairGraph sym arch -> StateT (PairGraph sym arch) (EquivM_ sym arch) a -> @@ -89,6 +97,13 @@ liftEqM_ :: StateT (PairGraph sym arch) (EquivM_ sym arch) () liftEqM_ f = liftEqM $ \pg -> ((),) <$> (f pg) +liftPartEqM_ :: + (PairGraph sym arch -> EquivM_ sym arch (Maybe (PairGraph sym arch))) -> + StateT (PairGraph sym arch) (EquivM_ sym arch) Bool +liftPartEqM_ f = liftEqM $ \pg -> f pg >>= \case + Just pg' -> return (True, pg') + Nothing -> return (False, pg) + liftEqM :: (PairGraph sym arch -> EquivM_ sym arch (a, PairGraph sym arch)) -> StateT (PairGraph sym arch) (EquivM_ sym arch) a From d7243dd04ddf5fba139b9377f0df771e3f897e84 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 14 May 2024 12:43:05 -0700 Subject: [PATCH 03/26] retain divergence information for sync nodes this is a forward-looking change to support more expressive control flow synchronization --- src/Pate/Verification/PairGraph.hs | 12 +++--- src/Pate/Verification/PairGraph/Node.hs | 52 +++++++++++++++++++++---- 2 files changed, 49 insertions(+), 15 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 87a1a4ac..2d8f2110 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -159,7 +159,7 @@ import qualified Pate.Equivalence.Error as PEE import qualified Pate.SimState as PS -import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, NodeReturn, nodeBlocks, nodeFuns, graphNodeBlocks, getDivergePoint, divergePoint, mkNodeEntry, mkNodeReturn, nodeContext, isSingleNodeEntry, isSingleReturn ) +import Pate.Verification.PairGraph.Node import Pate.Verification.StrongestPosts.CounterExample ( TotalityCounterexample(..), ObservableCounterexample(..) ) import qualified Pate.Verification.AbstractDomain as PAD @@ -973,20 +973,18 @@ combineNodes node1 node2 = do -- it only makes sense to combine nodes that share a divergence point, -- where that divergence point will be used as the calling context for the -- merged point - GraphNode divergeO <- divergePoint $ nodeContext nodeO - GraphNode divergeP <- divergePoint $ nodeContext nodeP + divergeO <- divergePoint $ nodeContext nodeO + divergeP <- divergePoint $ nodeContext nodeP guard $ divergeO == divergeP case (nodeO, nodeP) of (GraphNode nodeO', GraphNode nodeP') -> do blocksO <- PPa.get PBi.OriginalRepr (nodeBlocks nodeO') blocksP <- PPa.get PBi.PatchedRepr (nodeBlocks nodeP') - -- FIXME: retain calling context? - return $ GraphNode $ mkNodeEntry divergeO (PPa.PatchPair blocksO blocksP) + return $ GraphNode $ mkMergedNodeEntry divergeO blocksO blocksP (ReturnNode nodeO', ReturnNode nodeP') -> do fnsO <- PPa.get PBi.OriginalRepr (nodeFuns nodeO') fnsP <- PPa.get PBi.PatchedRepr (nodeFuns nodeP') - -- FIXME: retain calling context? - return $ ReturnNode $ mkNodeReturn divergeO (PPa.PatchPair fnsO fnsP) + return $ ReturnNode $ mkMergedNodeReturn divergeO fnsO fnsP _ -> Nothing singleNodeRepr :: GraphNode arch -> Maybe (Some (PBi.WhichBinaryRepr)) diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 28d3991e..9869d151 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -9,6 +9,7 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE OverloadedStrings #-} @@ -46,6 +47,8 @@ module Pate.Verification.PairGraph.Node ( , splitGraphNode , getDivergePoint , eqUptoDivergePoint + , mkMergedNodeEntry + , mkMergedNodeReturn ) where import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) @@ -150,15 +153,43 @@ addContext newCtx ne@(NodeEntry (CallingContext ctx d) blks) = True -> ne False -> NodeEntry (CallingContext (newCtx:ctx) d) blks +-- Strip diverge points from two-sided nodes. This is used so that +-- merged nodes (which are two-sided) can meaningfully retain their +-- diverge point, but it will be stripped on any subsequent nodes. +mkNextContext :: PPa.PatchPair a -> CallingContext arch -> CallingContext arch +mkNextContext (PPa.PatchPair{}) cctx = dropDivergePoint cctx +mkNextContext _ cctx = cctx + +dropDivergePoint :: CallingContext arch -> CallingContext arch +dropDivergePoint (CallingContext cctx _) = CallingContext cctx Nothing + mkNodeEntry :: NodeEntry arch -> PB.BlockPair arch -> NodeEntry arch -mkNodeEntry node pPair = NodeEntry (graphNodeContext node) pPair +mkNodeEntry node pPair = NodeEntry (mkNextContext pPair (graphNodeContext node)) pPair mkNodeEntry' :: GraphNode arch -> PB.BlockPair arch -> NodeEntry arch -mkNodeEntry' (GraphNode node) pPair = NodeEntry (graphNodeContext node) pPair -mkNodeEntry' (ReturnNode node) pPair = NodeEntry (returnNodeContext node) pPair +mkNodeEntry' (GraphNode ne) pPair = mkNodeEntry ne pPair +mkNodeEntry' (ReturnNode node) pPair = NodeEntry (mkNextContext pPair (returnNodeContext node)) pPair mkNodeReturn :: NodeEntry arch -> PB.FunPair arch -> NodeReturn arch -mkNodeReturn node fPair = NodeReturn (graphNodeContext node) fPair +mkNodeReturn node fPair = NodeReturn (mkNextContext fPair (graphNodeContext node)) fPair + +mkMergedNodeEntry :: + GraphNode arch -> + PB.ConcreteBlock arch PB.Original -> + PB.ConcreteBlock arch PB.Patched -> + NodeEntry arch +mkMergedNodeEntry nd blkO blkP = NodeEntry (CallingContext cctx (Just nd)) (PPa.PatchPair blkO blkP) + where + CallingContext cctx _ = nodeContext nd + +mkMergedNodeReturn :: + GraphNode arch -> + PB.FunctionEntry arch PB.Original -> + PB.FunctionEntry arch PB.Patched -> + NodeReturn arch +mkMergedNodeReturn nd fnO fnP = NodeReturn (CallingContext cctx (Just nd)) (PPa.PatchPair fnO fnP) + where + CallingContext cctx _ = nodeContext nd -- | Project the given 'NodeReturn' into a singleton node for the given binary toSingleReturn :: PPa.PatchPairM m => PB.WhichBinaryRepr bin -> GraphNode arch -> NodeReturn arch -> m (NodeReturn arch) @@ -228,16 +259,16 @@ splitGraphNode nd = do -- | Get the node corresponding to the entry point for the function returnToEntry :: NodeReturn arch -> NodeEntry arch -returnToEntry (NodeReturn ctx fns) = NodeEntry ctx (TF.fmapF PB.functionEntryToConcreteBlock fns) +returnToEntry (NodeReturn ctx fns) = NodeEntry (mkNextContext fns ctx) (TF.fmapF PB.functionEntryToConcreteBlock fns) -- | Get the return node that this entry would return to returnOfEntry :: NodeEntry arch -> NodeReturn arch -returnOfEntry (NodeEntry ctx blks) = NodeReturn ctx (TF.fmapF PB.blockFunctionEntry blks) +returnOfEntry (NodeEntry ctx blks) = NodeReturn (mkNextContext blks ctx) (TF.fmapF PB.blockFunctionEntry blks) -- | For an intermediate entry point in a function, find the entry point -- corresponding to the function start functionEntryOf :: NodeEntry arch -> NodeEntry arch -functionEntryOf (NodeEntry ctx blks) = NodeEntry ctx (TF.fmapF (PB.functionEntryToConcreteBlock . PB.blockFunctionEntry) blks) +functionEntryOf (NodeEntry ctx blks) = NodeEntry (mkNextContext blks ctx) (TF.fmapF (PB.functionEntryToConcreteBlock . PB.blockFunctionEntry) blks) instance PA.ValidArch arch => Show (CallingContext arch) where show c = show (pretty c) @@ -308,7 +339,12 @@ instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "node" w type TraceNodeType '(sym, arch) "node" = GraphNode arch type TraceNodeLabel "node" = String prettyNode msg nd = tracePrettyNode nd msg - nodeTags = mkTags @'(sym,arch) @"node" [Simplified, Summary] + nodeTags = mkTags @'(sym,arch) @"node" [Simplified, Summary] + ++ [("debug", \lbl v -> tracePrettyNode v lbl <+> case divergePoint (nodeContext v) of + Just dp -> "diverged: (" <> tracePrettyNode dp "" <> ")" + Nothing -> "" + ) + ] jsonNode _ = nodeToJSON @'(sym,arch) @"node" instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "entrynode" where From 2412b87793924287a2fd1b5d9378e1717a7efc91 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 20 Mar 2024 09:43:44 -0700 Subject: [PATCH 04/26] add 'filter' function to RevMap --- src/Data/RevMap.hs | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/Data/RevMap.hs b/src/Data/RevMap.hs index f271b107..310674cb 100644 --- a/src/Data/RevMap.hs +++ b/src/Data/RevMap.hs @@ -1,4 +1,6 @@ {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} {-| Module : Data.RevMap Copyright : (c) Galois, Inc 2023 @@ -19,9 +21,10 @@ module Data.RevMap , alter , insertWith , findFirst + , filter ) where -import Prelude hiding (lookup) +import Prelude hiding (lookup, filter) import qualified Data.Set as Set import Data.Set (Set) @@ -76,6 +79,13 @@ delete a m@(RevMap a_to_b b_to_a) = case Map.lookup a a_to_b of Just b -> reverseAdjust b (Set.delete a) (RevMap (Map.delete a a_to_b) b_to_a) Nothing -> m +filter :: forall a b. (a -> b -> Bool) -> RevMap a b -> RevMap a b +filter f (RevMap a_to_b b_to_a) = + RevMap (Map.filterWithKey f a_to_b) (Map.mapMaybeWithKey g b_to_a) + where + g :: b -> Set a -> Maybe (Set a) + g b as = let as' = Set.filter (\a -> f a b) as + in if Set.null as' then Nothing else Just as' alter :: (Ord a, Ord b) => (Maybe b -> Maybe b) -> a -> RevMap a b -> RevMap a b alter f a m@(RevMap a_to_b b_to_as) = case Map.lookup a a_to_b of From ac18ddd4e3d8f6a6b5b7d39ce5c8f5c91b539eb5 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 20 Mar 2024 11:34:55 -0700 Subject: [PATCH 05/26] wrap PairGraph worklist elements in WorkItem datatype this is an intermediate step in adding additional ways that a node can be queued to be processed - in particular, handling node merge logic via the scheduler --- src/Pate/Verification/PairGraph.hs | 60 ++++++++++++------------- src/Pate/Verification/StrongestPosts.hs | 20 +++------ 2 files changed, 36 insertions(+), 44 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 2d8f2110..7a1cdce8 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -34,10 +34,8 @@ module Pate.Verification.PairGraph , hasWorkLeft , pairGraphWorklist , pairGraphObservableReports - , popWorkItem , updateDomain , updateDomain' - , dropWorkItem , addReturnVector , getReturnVectors , getEdgesFrom @@ -75,6 +73,8 @@ module Pate.Verification.PairGraph , combineNodes , NodePriority(..) , addToWorkList + , WorkItem + , workItemNode , getQueuedPriority , queueAncestors , queueNode @@ -233,7 +233,7 @@ data PairGraph sym arch = -- be revisited, and here we record all such nodes that must be examinied. -- -- This is a mapping from nodes to their queue priority. - , pairGraphWorklist :: !(RevMap (GraphNode arch) NodePriority) + , pairGraphWorklist :: !(WorkList arch) -- | The set of blocks where this function may return to. Whenever we see a function -- call to the given FunPair, we record the program point pair where the function -- returns to here. This is used to tell us where we need to propagate abstract domain @@ -293,7 +293,17 @@ data PairGraph sym arch = !(Map (GraphNode arch) [DomainRefinement sym arch]) } +type WorkList arch = RevMap (WorkItem arch) NodePriority +-- | Operations that can be a scheduled and handled +-- at the top-level. +data WorkItem arch = + -- | Handle all normal node processing logic + ProcessNode (GraphNode arch) + deriving (Eq, Ord) + +workItemNode :: WorkItem arch -> GraphNode arch +workItemNode (ProcessNode nd) = nd newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a } deriving (Functor @@ -615,9 +625,9 @@ dropDomain nd priority pg = case getCurrentDomain pg nd of pg' = case Set.null (getBackEdgesFrom pg nd) of -- don't drop the domain for a toplevel entrypoint, but mark it for -- re-analysis - True -> pg { pairGraphWorklist = RevMap.insertWith (min) nd priority (pairGraphWorklist pg) } + True -> pg { pairGraphWorklist = RevMap.insertWith (min) (ProcessNode nd) priority (pairGraphWorklist pg) } False -> pg { pairGraphDomains = Map.delete nd (pairGraphDomains pg), - pairGraphWorklist = RevMap.delete nd (pairGraphWorklist pg) + pairGraphWorklist = dropNodeFromWorkList nd (pairGraphWorklist pg) } pg'' = Set.foldl' (\pg_ nd' -> dropDomain nd' priority pg_) pg' (getEdgesFrom pg nd) pg3 = dropObservableReports nd pg'' @@ -776,25 +786,13 @@ pairGraphComputeVerdict gr = else PE.Inequivalent -popWorkItem :: - PA.ValidArch arch => - PairGraph sym arch -> - GraphNode arch -> - (PairGraph sym arch, GraphNode arch, AbstractDomainSpec sym arch) -popWorkItem gr nd = case Map.lookup nd (pairGraphDomains gr) of - Nothing -> panic Verifier "popWorkItem" ["Could not find domain corresponding to block pair", show nd] - Just d -> - let wl = RevMap.delete nd (pairGraphWorklist gr) - in (gr{ pairGraphWorklist = wl }, nd, d) - -- | Drop the given node from the work queue if it is queued. -- Otherwise do nothing. -dropWorkItem :: - PA.ValidArch arch => +dropNodeFromWorkList :: GraphNode arch -> - PairGraph sym arch -> - PairGraph sym arch -dropWorkItem nd gr = gr { pairGraphWorklist = RevMap.delete nd (pairGraphWorklist gr) } + WorkList arch -> + WorkList arch +dropNodeFromWorkList nd wl = RevMap.filter (\wi _ -> workItemNode wi == nd) wl hasWorkLeft :: PairGraph sym arch -> Bool @@ -808,15 +806,15 @@ hasWorkLeft pg = case RevMap.minView_value (pairGraphWorklist pg) of chooseWorkItem :: PA.ValidArch arch => PairGraph sym arch -> - Maybe (NodePriority, PairGraph sym arch, GraphNode arch, AbstractDomainSpec sym arch) + Maybe (NodePriority, PairGraph sym arch, WorkItem arch, AbstractDomainSpec sym arch) chooseWorkItem gr = -- choose the smallest pair from the worklist. This is a pretty brain-dead -- heuristic. Perhaps we should do something more clever. case RevMap.minView_value (pairGraphWorklist gr) of Nothing -> Nothing - Just (nd, p, wl) -> case Map.lookup nd (pairGraphDomains gr) of - Nothing -> panic Verifier "chooseWorkItem" ["Could not find domain corresponding to block pair", show nd] - Just d -> Just (p, gr{ pairGraphWorklist = wl }, nd, d) + Just (wi, p, wl) -> case Map.lookup (workItemNode wi) (pairGraphDomains gr) of + Nothing -> panic Verifier "chooseWorkItem" ["Could not find domain corresponding to block pair", show (workItemNode wi)] + Just d -> Just (p, gr{ pairGraphWorklist = wl }, wi, d) -- | Update the abstract domain for the target graph node, -- decreasing the gas parameter as necessary. @@ -857,7 +855,7 @@ updateDomain' :: PairGraph sym arch updateDomain' gr pFrom pTo d priority = markEdge pFrom pTo $ gr { pairGraphDomains = Map.insert pTo d (pairGraphDomains gr) - , pairGraphWorklist = RevMap.insertWith (min) pTo priority (pairGraphWorklist gr) + , pairGraphWorklist = RevMap.insertWith (min) (ProcessNode pTo) priority (pairGraphWorklist gr) , pairGraphEdges = Map.insertWith Set.union pFrom (Set.singleton pTo) (pairGraphEdges gr) , pairGraphBackEdges = Map.insertWith Set.union pTo (Set.singleton pFrom) (pairGraphBackEdges gr) } @@ -913,7 +911,7 @@ addReturnVector gr funPair retPair priority = f Nothing = Just (Set.singleton retPair) f (Just s) = Just (Set.insert retPair s) - wl = RevMap.insertWith (min) (ReturnNode funPair) priority (pairGraphWorklist gr) + wl = RevMap.insertWith (min) (ProcessNode (ReturnNode funPair)) priority (pairGraphWorklist gr) pgMaybe :: String -> Maybe a -> PairGraphM sym arch a pgMaybe _ (Just a) = return a @@ -1035,12 +1033,14 @@ addToWorkList :: PairGraph sym arch -> Maybe (PairGraph sym arch) addToWorkList nd priority gr = case getCurrentDomain gr nd of - Just{} -> Just $ gr { pairGraphWorklist = RevMap.insertWith (min) nd priority (pairGraphWorklist gr) } + Just{} -> Just $ gr { pairGraphWorklist = RevMap.insertWith (min) (ProcessNode nd) priority (pairGraphWorklist gr) } Nothing -> Nothing +-- | Return the priority of the given 'GraphNode' if it is queued for +-- normal processing getQueuedPriority :: GraphNode arch -> PairGraph sym arch -> Maybe NodePriority -getQueuedPriority nd pg = RevMap.lookup nd (pairGraphWorklist pg) +getQueuedPriority nd pg = RevMap.lookup (ProcessNode nd) (pairGraphWorklist pg) emptyWorkList :: PairGraph sym arch -> PairGraph sym arch emptyWorkList pg = pg { pairGraphWorklist = RevMap.empty } @@ -1055,7 +1055,7 @@ freshDomain :: PairGraph sym arch freshDomain gr pTo priority d = gr{ pairGraphDomains = Map.insert pTo d (pairGraphDomains gr) - , pairGraphWorklist = RevMap.insertWith (min) pTo priority (pairGraphWorklist gr) + , pairGraphWorklist = RevMap.insertWith (min) (ProcessNode pTo) priority (pairGraphWorklist gr) } initDomain :: diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index a6f5df72..5512cca4 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -745,32 +745,23 @@ withWorkItem :: PA.ValidArch arch => PSo.ValidSym sym => PairGraph sym arch -> - ((NodePriority, PairGraph sym arch, GraphNode arch, PAD.AbstractDomainSpec sym arch) -> EquivM_ sym arch a) -> + ((NodePriority, PairGraph sym arch, WorkItem arch, PAD.AbstractDomainSpec sym arch) -> EquivM_ sym arch a) -> NodeBuilderT '(sym,arch) "node" (EquivM_ sym arch) (Maybe a) withWorkItem gr0 f = do gr0' <- lift $ queuePendingNodes gr0 case chooseWorkItem gr0' of Nothing -> return Nothing - Just (priority, gr1, nd, spec) -> do + Just (priority, gr1, wi, spec) -> do + let nd = workItemNode wi res <- subTraceLabel @"node" (printPriorityKind priority) nd $ startTimer $ atPriority priority Nothing $ PS.viewSpec spec $ \scope d -> do runPendingActions refineActions nd (TupleF2 scope d) gr1 >>= \case Just gr2 -> return $ Left gr2 - Nothing -> Right <$> f (priority, gr1, nd, spec) + Nothing -> Right <$> f (priority, gr1, wi, spec) case res of Left gr2 -> withWorkItem gr2 f Right a -> return $ Just a -{- - let nodes = Set.toList $ pairGraphWorklist gr - case nodes of - [] -> return Nothing - [node] -> return (Just $ popWorkItem gr node) - _ -> - _ -> choose @"node" "chooseWorkItem" $ \choice -> forM_ nodes $ \nd -> - choice "" nd $ return (Just $ popWorkItem gr nd) --} - -- | Execute the forward dataflow fixpoint algorithm. -- Visit nodes and compute abstract domains until we propagate information -- to all reachable positions in the program graph and we reach stability, @@ -782,7 +773,8 @@ pairGraphComputeFixpoint :: pairGraphComputeFixpoint entries gr_init = do let go (gr0 :: PairGraph sym arch) = do - mgr4 <- withWorkItem gr0 $ \(priority, gr1, nd, preSpec) -> do + mgr4 <- withWorkItem gr0 $ \(priority, gr1, wi, preSpec) -> do + let nd = workItemNode wi shouldProcessNode nd >>= \case False -> do emitWarning $ PEE.SkippedInequivalentBlocks (graphNodeBlocks nd) From 483b7df5b940688f71316cbc26d23ab7fdc92275 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 4 Apr 2024 13:19:40 -0700 Subject: [PATCH 06/26] add SingleNodeEntry datatype to represent explicitly single-sided nodes This clears up some of the ambiguity in the SyncPoint data which otherwise had lots of implicit assumptions about the run-time contents of the NodeEntry for each sync point A SingleNodeEntry is functionally equivalent to a NodeEntry that's annotated with the fact that it's single-sided --- src/Data/Parameterized/SetF.hs | 10 +++ src/Pate/PatchPair.hs | 18 ++++ src/Pate/Verification/PairGraph.hs | 58 +++++------- src/Pate/Verification/PairGraph/Node.hs | 115 +++++++++++++++++++++--- src/Pate/Verification/StrongestPosts.hs | 38 ++++---- 5 files changed, 176 insertions(+), 63 deletions(-) diff --git a/src/Data/Parameterized/SetF.hs b/src/Data/Parameterized/SetF.hs index 665b8533..32c471d5 100644 --- a/src/Data/Parameterized/SetF.hs +++ b/src/Data/Parameterized/SetF.hs @@ -43,6 +43,7 @@ module Data.Parameterized.SetF , union , unions , null + , toSet , ppSetF ) where @@ -55,6 +56,7 @@ import Prettyprinter ( (<+>) ) import Data.Set (Set) import qualified Data.Set as S +import Unsafe.Coerce (unsafeCoerce) newtype AsOrd f tp where AsOrd :: { unAsOrd :: f tp } -> AsOrd f tp @@ -130,6 +132,14 @@ null :: SetF f tp -> Bool null (SetF es) = S.null es +-- | Convert a 'SetF' to a 'Set', under the assumption +-- that the 'OrdF' and 'Ord' instances are consistent. +-- This uses coercion rather than re-building the set, +-- which is sound given the above assumption. +toSet :: + (OrdF f, Ord (f tp)) => SetF f tp -> Set (f tp) +toSet (SetF s) = unsafeCoerce s + ppSetF :: (f tp -> PP.Doc a) -> SetF f tp -> diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index 0d2ef51e..a2378d30 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -41,6 +41,7 @@ module Pate.PatchPair ( , ppPatchPair' , forBins , update + , insertWith , forBinsC , catBins , get @@ -332,6 +333,23 @@ update src f = do (PatchPair _ b, PatchPairOriginal a) -> return $ PatchPair a b (PatchPair a _, PatchPairPatched b) -> return $ PatchPair a b +-- | Add a value to a 'PatchPair', combining it with an existing entry if +-- present using the given function (i.e. similar to Map.insertWith) +insertWith :: + PB.WhichBinaryRepr bin -> + f bin -> + (f bin -> f bin -> f bin) -> + PatchPair f -> + PatchPair f +insertWith bin v f = \case + PatchPair vO vP | PB.OriginalRepr <- bin -> PatchPair (f v vO) vP + PatchPair vO vP | PB.PatchedRepr <- bin -> PatchPair vO (f v vP) + PatchPairSingle bin' v' -> case (bin, bin') of + (PB.OriginalRepr, PB.OriginalRepr) -> PatchPairSingle bin (f v v') + (PB.PatchedRepr, PB.PatchedRepr) -> PatchPairSingle bin (f v v') + (PB.PatchedRepr, PB.OriginalRepr) -> PatchPair v' v + ( PB.OriginalRepr, PB.PatchedRepr) -> PatchPair v v' + -- | Specialization of 'PatchPair' to types which are not indexed on 'PB.WhichBinary' type PatchPairC tp = PatchPair (Const tp) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 7a1cdce8..28376187 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -173,6 +173,8 @@ import qualified Pate.Location as PL import qualified Pate.Address as PAd import Data.Foldable (find) import Data.Parameterized.PairF +import Data.Parameterized.SetF (SetF) +import qualified Data.Parameterized.SetF as SetF -- | Gas is used to ensure that our fixpoint computation terminates -- in a reasonable amount of time. Gas is expended each time @@ -476,7 +478,7 @@ data SyncPoint arch = -- The "merge" nodes are the cross product of these, since we -- must assume that any combination of exits is possible -- during the single-sided analysis - { syncStartNodes :: PPa.PatchPairC (Set (GraphNode arch)) + { syncStartNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) , syncCutAddresses :: PPa.PatchPairC (PAd.ConcreteAddress arch) } @@ -921,10 +923,10 @@ getSyncPoints :: forall sym arch bin. PBi.WhichBinaryRepr bin -> GraphNode arch -> - PairGraphM sym arch (Set (GraphNode arch)) + PairGraphM sym arch (Set (SingleNodeEntry arch bin)) getSyncPoints bin nd = do (SyncPoint syncPair _) <- lookupPairGraph @sym pairGraphSyncPoints nd - PPa.getC bin syncPair + SetF.toSet <$> PPa.get bin syncPair getSyncAddress :: forall sym arch bin. @@ -950,12 +952,12 @@ updateSyncPoint nd f = do getCombinedSyncPoints :: forall sym arch. GraphNode arch -> - PairGraphM sym arch ([((GraphNode arch, GraphNode arch), GraphNode arch)], SyncPoint arch) + PairGraphM sym arch ([((SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched), GraphNode arch)], SyncPoint arch) getCombinedSyncPoints ndDiv = do sync@(SyncPoint syncSet _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv case syncSet of - PPa.PatchPairC ndsO ndsP -> do - all_pairs <- forM (Set.toList $ Set.cartesianProduct ndsO ndsP) $ \(ndO, ndP) -> do + PPa.PatchPair ndsO ndsP -> do + all_pairs <- forM (Set.toList $ Set.cartesianProduct (SetF.toSet ndsO) (SetF.toSet ndsP)) $ \(ndO, ndP) -> do combined <- pgMaybe "failed to combine nodes" $ combineNodes ndO ndP return $ ((ndO, ndP), combined) return (all_pairs, sync) @@ -963,27 +965,18 @@ getCombinedSyncPoints ndDiv = do -- | Compute a merged node for two diverging nodes -- FIXME: do we need to support mismatched node kinds here? -combineNodes :: GraphNode arch -> GraphNode arch -> Maybe (GraphNode arch) +combineNodes :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (GraphNode arch) combineNodes node1 node2 = do - (nodeO, nodeP) <- case PPa.get PBi.OriginalRepr (graphNodeBlocks node1) of - Just{} -> return (node1, node2) - Nothing -> return (node2, node1) + let ndPair = PPa.mkPair (singleEntryBin node1) node1 node2 + nodeO <- PPa.get PBi.OriginalRepr ndPair + nodeP <- PPa.get PBi.PatchedRepr ndPair -- it only makes sense to combine nodes that share a divergence point, -- where that divergence point will be used as the calling context for the -- merged point - divergeO <- divergePoint $ nodeContext nodeO - divergeP <- divergePoint $ nodeContext nodeP + let divergeO = singleNodeDivergence nodeO + let divergeP = singleNodeDivergence nodeP guard $ divergeO == divergeP - case (nodeO, nodeP) of - (GraphNode nodeO', GraphNode nodeP') -> do - blocksO <- PPa.get PBi.OriginalRepr (nodeBlocks nodeO') - blocksP <- PPa.get PBi.PatchedRepr (nodeBlocks nodeP') - return $ GraphNode $ mkMergedNodeEntry divergeO blocksO blocksP - (ReturnNode nodeO', ReturnNode nodeP') -> do - fnsO <- PPa.get PBi.OriginalRepr (nodeFuns nodeO') - fnsP <- PPa.get PBi.PatchedRepr (nodeFuns nodeP') - return $ ReturnNode $ mkMergedNodeReturn divergeO fnsO fnsP - _ -> Nothing + return $ GraphNode $ mkMergedNodeEntry divergeO (singleNodeBlock nodeO) (singleNodeBlock nodeP) singleNodeRepr :: GraphNode arch -> Maybe (Some (PBi.WhichBinaryRepr)) singleNodeRepr nd = case graphNodeBlocks nd of @@ -993,17 +986,12 @@ singleNodeRepr nd = case graphNodeBlocks nd of addSyncNode :: forall sym arch. GraphNode arch {- ^ The divergent node -} -> - GraphNode arch {- ^ the sync node -} -> + NodeEntry arch {- ^ the sync node -} -> PairGraphM sym arch () addSyncNode ndDiv ndSync = do - Pair bin _ <- PPa.asSingleton (graphNodeBlocks ndSync) - let ndSync' = PPa.PatchPairSingle bin (Const ndSync) + Some nd <- asSingleNodeEntry ndSync (SyncPoint sp addrs) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv - sp' <- PPa.update sp $ \bin' -> do - s <- PPa.getC bin' ndSync' - case PPa.getC bin' sp of - Nothing -> return $ (Const (Set.singleton s)) - Just s' -> return $ (Const (Set.insert s s')) + let sp' = PPa.insertWith (singleEntryBin nd) (SetF.singleton nd) SetF.union sp modify $ \pg -> pg { pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp' addrs) (pairGraphSyncPoints pg) } tryPG :: PairGraphM sym arch a -> PairGraphM sym arch (Maybe a) @@ -1022,7 +1010,7 @@ setSyncAddress ndDiv bin syncAddr = do addrs' <- PPa.update addrs $ \bin' -> PPa.get bin' syncAddr' modify $ \pg -> pg{ pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp addrs') (pairGraphSyncPoints pg) } Nothing -> do - let sp = PPa.mkPair bin (Const Set.empty) (Const Set.empty) + let sp = PPa.mkPair bin SetF.empty SetF.empty modify $ \pg -> pg{pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp syncAddr') (pairGraphSyncPoints pg) } -- | Add a node back to the worklist to be re-analyzed if there is @@ -1178,15 +1166,15 @@ checkForNodeSync :: [(PPa.PatchPair (PB.BlockTarget arch))] -> PairGraphM sym arch Bool checkForNodeSync ne targets_pairs = fmap (fromMaybe False) $ tryPG $ do - Just (Some bin) <- return $ isSingleNodeEntry ne - - Just dp <- return $ getDivergePoint (GraphNode ne) + Some sne <- asSingleNodeEntry ne + let bin = singleEntryBin sne + let dp = singleNodeDivergence sne syncPoints <- getSyncPoints bin dp syncAddr <- getSyncAddress bin dp thisAddr <- fmap PB.concreteAddress $ PPa.get bin (nodeBlocks ne) -- if this node is already defined as sync point then we don't -- have to check anything else - if | Set.member (GraphNode ne) syncPoints -> return True + if | Set.member sne syncPoints -> return True -- similarly if this is exactly the sync address then we should -- stop the single-sided analysis | thisAddr == syncAddr -> return True diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 9869d151..454d005b 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -25,6 +25,7 @@ module Pate.Verification.PairGraph.Node ( , pattern GraphNodeEntry , pattern GraphNodeReturn , nodeContext + , graphNodeContext , divergePoint , graphNodeBlocks , mkNodeEntry @@ -49,6 +50,13 @@ module Pate.Verification.PairGraph.Node ( , eqUptoDivergePoint , mkMergedNodeEntry , mkMergedNodeReturn + , SingleNodeEntry + , singleEntryBin + , asSingleNodeEntry + , singleToNodeEntry + , combineSingleEntries + , singleNodeBlock + , singleNodeDivergence ) where import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) @@ -64,6 +72,9 @@ import qualified Pate.Binary as PB import qualified Prettyprinter as PP import Data.Parameterized (Some(..), Pair (..)) import qualified What4.JSON as W4S +import Control.Monad (guard) +import Data.Parameterized.Classes +import Pate.Panic -- | Nodes in the program graph consist either of a pair of -- program points (GraphNode), or a synthetic node representing @@ -91,28 +102,48 @@ instance PA.ValidArch arch => W4S.W4Serializable sym (GraphNode arch) where instance PA.ValidArch arch => W4S.W4Serializable sym (NodeEntry arch) where w4Serialize r = return $ JSON.toJSON r --- A frozen binary -data NodeEntry arch = - NodeEntry { graphNodeContext :: CallingContext arch, nodeBlocks :: PB.BlockPair arch } +data NodeContent arch e = + NodeContent { nodeContentCtx :: CallingContext arch, nodeContent :: e } deriving (Eq, Ord) -data NodeReturn arch = - NodeReturn { returnNodeContext :: CallingContext arch, nodeFuns :: PB.FunPair arch } - deriving (Eq, Ord) +type NodeEntry arch = NodeContent arch (PB.BlockPair arch) + +pattern NodeEntry :: CallingContext arch -> PB.BlockPair arch -> NodeEntry arch +pattern NodeEntry ctx bp = NodeContent ctx bp +{-# COMPLETE NodeEntry #-} + + +nodeBlocks :: NodeEntry arch -> PB.BlockPair arch +nodeBlocks = nodeContent + +graphNodeContext :: NodeEntry arch -> CallingContext arch +graphNodeContext = nodeContentCtx + +type NodeReturn arch = NodeContent arch (PB.FunPair arch) + +nodeFuns :: NodeReturn arch -> PB.FunPair arch +nodeFuns = nodeContent + +returnNodeContext :: NodeReturn arch -> CallingContext arch +returnNodeContext = nodeContentCtx + +pattern NodeReturn :: CallingContext arch -> PB.FunPair arch -> NodeReturn arch +pattern NodeReturn ctx bp = NodeContent ctx bp +{-# COMPLETE NodeReturn #-} graphNodeBlocks :: GraphNode arch -> PB.BlockPair arch graphNodeBlocks (GraphNode ne) = nodeBlocks ne graphNodeBlocks (ReturnNode ret) = TF.fmapF PB.functionEntryToConcreteBlock (nodeFuns ret) nodeContext :: GraphNode arch -> CallingContext arch -nodeContext (GraphNode nd) = graphNodeContext nd -nodeContext (ReturnNode ret) = returnNodeContext ret +nodeContext (GraphNode nd) = nodeContentCtx nd +nodeContext (ReturnNode ret) = nodeContentCtx ret pattern GraphNodeEntry :: PB.BlockPair arch -> GraphNode arch -pattern GraphNodeEntry blks <- (GraphNode (NodeEntry _ blks)) +pattern GraphNodeEntry blks <- (GraphNode (NodeContent _ blks)) pattern GraphNodeReturn :: PB.FunPair arch -> GraphNode arch -pattern GraphNodeReturn blks <- (ReturnNode (NodeReturn _ blks)) +pattern GraphNodeReturn blks <- (ReturnNode (NodeContent _ blks)) {-# COMPLETE GraphNodeEntry, GraphNodeReturn #-} @@ -191,6 +222,7 @@ mkMergedNodeReturn nd fnO fnP = NodeReturn (CallingContext cctx (Just nd)) (PPa. where CallingContext cctx _ = nodeContext nd + -- | Project the given 'NodeReturn' into a singleton node for the given binary toSingleReturn :: PPa.PatchPairM m => PB.WhichBinaryRepr bin -> GraphNode arch -> NodeReturn arch -> m (NodeReturn arch) toSingleReturn bin divergedAt (NodeReturn ctx fPair) = do @@ -352,3 +384,66 @@ instance forall sym arch. PA.ValidArch arch => IsTraceNode '(sym, arch) "entryno prettyNode () = pretty nodeTags = mkTags @'(sym,arch) @"entrynode" [Simplified, Summary] jsonNode _ = nodeToJSON @'(sym,arch) @"entrynode" + +-- | Equivalent to a 'NodeEntry' but necessarily a single-sided node. +-- Converting a 'SingleNodeEntry' to a 'NodeEntry' is always defined, +-- while converting a 'NodeEntry' to a 'SingleNodeEntry' is partial. +data SingleNodeEntry arch bin = + SingleNodeEntry + { singleEntryBin :: PB.WhichBinaryRepr bin + , _singleEntry :: NodeContent arch (PB.ConcreteBlock arch bin) + } + +instance TestEquality (SingleNodeEntry arch) where + testEquality se1 se2 | EQF <- compareF se1 se2 = Just Refl + testEquality _ _ = Nothing + +instance Eq (SingleNodeEntry arch bin) where + se1 == se2 = compare se1 se2 == EQ + +instance Ord (SingleNodeEntry arch bin) where + compare (SingleNodeEntry _ se1) (SingleNodeEntry _ se2) = compare se1 se2 + +instance OrdF (SingleNodeEntry arch) where + compareF (SingleNodeEntry bin1 se1) (SingleNodeEntry bin2 se2) = + lexCompareF bin1 bin2 $ fromOrdering (compare se1 se2) + +instance PA.ValidArch arch => Show (SingleNodeEntry arch bin) where + show e = show (singleToNodeEntry e) + +asSingleNodeEntry :: PPa.PatchPairM m => NodeEntry arch -> m (Some (SingleNodeEntry arch)) +asSingleNodeEntry (NodeEntry cctx bPair) = do + Pair bin blk <- PPa.asSingleton bPair + case divergePoint cctx of + Just{} -> return $ Some (SingleNodeEntry bin (NodeContent cctx blk)) + Nothing -> PPa.throwPairErr + +singleToNodeEntry :: SingleNodeEntry arch bin -> NodeEntry arch +singleToNodeEntry (SingleNodeEntry bin (NodeContent cctx v)) = + NodeEntry cctx (PPa.PatchPairSingle bin v) + +singleNodeBlock :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin +singleNodeBlock (SingleNodeEntry _ (NodeContent _ blk)) = blk + +singleNodeDivergence :: SingleNodeEntry arch bin -> GraphNode arch +singleNodeDivergence (SingleNodeEntry _ (NodeContent cctx _)) = case divergePoint cctx of + Just dp -> dp + Nothing -> panic Verifier "singleNodeDivergence" ["Unexpected missing divergence point"] + +-- | Create a combined two-sided 'NodeEntry' based on +-- a pair of single-sided entries. The given entries +-- must have the same diverge point (returns 'Nothing' otherwise), +-- and the calling context of the resulting node is inherited from +-- that point (i.e. any additional context accumulated during +-- the either single-sided analysis is discarded) +combineSingleEntries :: + SingleNodeEntry arch PB.Original -> + SingleNodeEntry arch PB.Patched -> + Maybe (NodeEntry arch) +combineSingleEntries (SingleNodeEntry _ eO) (SingleNodeEntry _ eP) = do + GraphNode divergeO <- divergePoint $ nodeContentCtx eO + GraphNode divergeP <- divergePoint $ nodeContentCtx eP + guard $ divergeO == divergeP + let blksO = nodeContent eO + let blksP = nodeContent eP + return $ mkNodeEntry divergeO (PPa.PatchPair blksO blksP) \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 5512cca4..11af1665 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -117,7 +117,7 @@ import qualified Pate.Verification.ConditionalEquiv as PVC import qualified Pate.Verification.Simplify as PSi import Pate.Verification.PairGraph -import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, NodeReturn (nodeFuns), toSingleReturn, rootEntry, rootReturn, getDivergePoint, toSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, toSingleGraphNode, isSingleNodeEntry, divergePoint, isSingleReturn ) +import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, nodeFuns, toSingleReturn, rootEntry, rootReturn, getDivergePoint, toSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, toSingleGraphNode, isSingleNodeEntry, divergePoint, isSingleReturn, NodeReturn, singleToNodeEntry, SingleNodeEntry, singleNodeBlock ) import Pate.Verification.Widening import qualified Pate.Verification.AbstractDomain as PAD import Data.Monoid (All(..), Any (..)) @@ -382,12 +382,12 @@ handleDanglingReturns fnPairs pg = do handleSyncPoint :: - GraphNode arch -> + NodeEntry arch -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) handleSyncPoint nd pg = withTracing @"message" "End of single-sided analysis" $ withPG_ pg $ do divergeNode <- liftPG $ do - Just divergeNode <- return $ getDivergePoint nd + Just divergeNode <- return $ getDivergePoint (GraphNode nd) addSyncNode divergeNode nd return divergeNode liftEqM_ $ updateCombinedSyncPoint divergeNode @@ -589,8 +589,8 @@ updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do syncsP_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.PatchedRepr divergeNode -- collect all sync points that have been found and that have a pre-domain - syncsO <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM nd) syncsO_ - syncsP <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM nd) syncsP_ + syncsO <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM (GraphNode (singleToNodeEntry nd))) syncsO_ + syncsP <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM (GraphNode (singleToNodeEntry nd))) syncsP_ case syncsO of -- We have not completed a single-sided analysis for the @@ -606,7 +606,7 @@ updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO -- also re-queue the ancestors of any known sync points that are missing domains forM_ syncsO_ $ \syncO -> do - modify $ queueAncestors (priority PriorityHandleDesync) syncO + modify $ queueAncestors (priority PriorityHandleDesync) (GraphNode (singleToNodeEntry syncO)) -- We have at least one completed one-sided analysis for the Original binary. -- The convention is that we find at least one Original sync point before -- moving on to the Patched one-sided analysis. @@ -623,9 +623,9 @@ updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do bundle <- lift $ noopBundle scope (graphNodeBlocks divergeNodeY) forM_ syncsO $ \(syncO, _) -> do liftPG $ (void $ getCurrentDomainM divergeNodeY) - <|> (modify $ \pg -> updateDomain' pg syncO divergeNodeY (PS.mkSimSpec scope domP) (priority PriorityWidening)) + <|> (modify $ \pg -> updateDomain' pg (GraphNode (singleToNodeEntry syncO)) divergeNodeY (PS.mkSimSpec scope domP) (priority PriorityWidening)) liftEqM_ $ \pg -> withPredomain scope bundle domP $ withConditionsAssumed scope bundle dom divergeNode pg $ - widenAlongEdge scope bundle syncO domP pg divergeNodeY + widenAlongEdge scope bundle (GraphNode (singleToNodeEntry syncO)) domP pg divergeNodeY -- Finally, if we have any Patched one-sided results, we take all combinations -- of Original and Patched sync points and connect them to a "combined" two-sided node @@ -637,8 +637,8 @@ updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do Just combinedNode <- return $ combineNodes syncO syncP return combinedNode withTracingLabel @"node" "Merge Node" combinedNode $ do - emitTrace @"node" syncO - emitTrace @"node" syncP + emitTrace @"node" (GraphNode (singleToNodeEntry syncO)) + emitTrace @"node" (GraphNode (singleToNodeEntry syncO)) liftEqM_ $ mergeDualNodes syncO syncP domO_spec domP_spec combinedNode @@ -716,15 +716,17 @@ addImmediateEqDomRefinementChoice nd preD gr0 = do mapM_ go [minBound..maxBound] mergeDualNodes :: - GraphNode arch {- ^ first program node -} -> - GraphNode arch {- ^ second program node -} -> - PAD.AbstractDomainSpec sym arch {- ^ first node domain -} -> - PAD.AbstractDomainSpec sym arch {- ^ second node domain -} -> + SingleNodeEntry arch PBi.Original {- ^ original program node -} -> + SingleNodeEntry arch PBi.Patched {- ^ patched program node -} -> + PAD.AbstractDomainSpec sym arch {- ^ original node domain -} -> + PAD.AbstractDomainSpec sym arch {- ^ patched node domain -} -> GraphNode arch {- ^ combined sync node -} -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -mergeDualNodes in1 in2 spec1 spec2 syncNode gr0 = fnTrace "mergeDualNodes" $ withSym $ \sym -> do +mergeDualNodes in1_single in2_single spec1 spec2 syncNode gr0 = fnTrace "mergeDualNodes" $ withSym $ \sym -> do let gr2 = gr0 + let in1 = GraphNode $ singleToNodeEntry in1_single + let in2 = GraphNode $ singleToNodeEntry in2_single let blkPair1 = graphNodeBlocks in1 let blkPair2 = graphNodeBlocks in2 @@ -1361,7 +1363,7 @@ visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 = -- node as a merge point withPG_ gr2 $ do (liftPG $ checkForNodeSync node exitPairs) >>= \case - True -> liftEqM_ $ handleSyncPoint (GraphNode node) + True -> liftEqM_ $ handleSyncPoint node False -> liftEqM_ $ \pg -> do handleSplitAnalysis scope node d pg >>= \case Just pg' -> return pg' @@ -1425,9 +1427,9 @@ visitNode scope (ReturnNode fPair) d gr0 = do liftEqM_ $ checkObservables scope node bundle d liftEqM_ $ \pg -> widenAlongEdge scope bundle (ReturnNode fPair) d pg (GraphNode node) (liftPG $ checkForReturnSync fPair node) >>= \case - True -> liftEqM_ $ handleSyncPoint (GraphNode node) + True -> liftEqM_ $ handleSyncPoint node False -> return () - + -- | Construct a "dummy" simulation bundle that basically just -- immediately returns the prestate as the poststate. -- This is used to compute widenings that propagate abstract domain From 4b8532ea180c7f2e0bbf44f3cf02c8d19ff960df Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 5 Apr 2024 08:44:28 -0700 Subject: [PATCH 07/26] add map to SetF --- src/Data/Parameterized/SetF.hs | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/Data/Parameterized/SetF.hs b/src/Data/Parameterized/SetF.hs index 32c471d5..d7d87723 100644 --- a/src/Data/Parameterized/SetF.hs +++ b/src/Data/Parameterized/SetF.hs @@ -44,10 +44,12 @@ module Data.Parameterized.SetF , unions , null , toSet + , map , ppSetF ) where -import Prelude hiding (filter, null) +import Prelude hiding (filter, null, map) +import qualified Data.List as List import Data.Parameterized.Classes import qualified Data.Foldable as Foldable @@ -93,13 +95,13 @@ insert e (SetF es) = SetF (S.insert (AsOrd e) es) toList :: SetF f tp -> [f tp] -toList (SetF es) = map unAsOrd $ S.toList es +toList (SetF es) = List.map unAsOrd $ S.toList es fromList :: OrdF f => [f tp] -> SetF f tp -fromList es = SetF $ S.fromList (map AsOrd es) +fromList es = SetF $ S.fromList (List.map AsOrd es) member :: OrdF f => @@ -140,6 +142,10 @@ toSet :: (OrdF f, Ord (f tp)) => SetF f tp -> Set (f tp) toSet (SetF s) = unsafeCoerce s +map :: + (OrdF g) => (f tp -> g tp) -> SetF f tp -> SetF g tp +map f (SetF s) = SetF (S.map (\(AsOrd v) -> AsOrd (f v)) s) + ppSetF :: (f tp -> PP.Doc a) -> SetF f tp -> From 1c072adc0ab74765af770b1f77d999a72fb51964 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 5 Apr 2024 08:45:05 -0700 Subject: [PATCH 08/26] add WithBin datatype to PatchPair for annotating data with original or patched this is essentially the same as Const, but useful for cases where we want to establish OrdF or TestEquality --- src/Pate/PatchPair.hs | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index a2378d30..536216dc 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -72,6 +72,7 @@ module Pate.PatchPair ( , zip , jsonPatchPair , w4SerializePair + , WithBin(..) ) where import Prelude hiding (zip) @@ -126,6 +127,27 @@ pattern PatchPairPatched a = PatchPairSingle PB.PatchedRepr a {-# COMPLETE PatchPair, PatchPairSingle #-} {-# COMPLETE PatchPair, PatchPairOriginal, PatchPairPatched #-} +-- | Tag any type with a 'PB.WhichBinary' +data WithBin f (bin :: PB.WhichBinary) = + WithBin { withBinRepr :: PB.WhichBinaryRepr bin, withBinValue :: f } + +instance Eq f => TestEquality (WithBin f) where + testEquality (WithBin bin1 f1) (WithBin bin2 f2) + | Just Refl <- testEquality bin1 bin2 + , f1 == f2 + = Just Refl + testEquality _ _ = Nothing + +instance Ord f => OrdF (WithBin f) where + compareF (WithBin bin1 f1) (WithBin bin2 f2) = + lexCompareF bin1 bin2 $ fromOrdering (compare f1 f2) + +instance Eq f => Eq (WithBin f bin) where + (WithBin _ f1) == (WithBin _ f2) = f1 == f2 + +instance Ord f => Ord (WithBin f bin) where + compare (WithBin _ f1) (WithBin _ f2) = compare f1 f2 + -- | Select the value from the 'PatchPair' according to the given 'PB.WhichBinaryRepr' -- Returns 'Nothing' if the given 'PatchPair' does not contain a value for the given binary -- (i.e. it is a singleton 'PatchPair' and the opposite binary repr is given) From 7ea5e60684c6c22940b9134194f168da193efa70 Mon Sep 17 00:00:00 2001 From: Zarigis Date: Tue, 14 May 2024 13:25:17 -0700 Subject: [PATCH 09/26] WIP --- src/Data/Parameterized/PairF.hs | 11 + src/Pate/Equivalence/Error.hs | 1 + src/Pate/Monad/Environment.hs | 7 + src/Pate/Monad/PairGraph.hs | 17 +- src/Pate/Verification/PairGraph.hs | 498 +++++++++++++++++------- src/Pate/Verification/PairGraph/Node.hs | 57 ++- src/Pate/Verification/StrongestPosts.hs | 356 +++++++---------- 7 files changed, 574 insertions(+), 373 deletions(-) diff --git a/src/Data/Parameterized/PairF.hs b/src/Data/Parameterized/PairF.hs index 3450274f..92962ea4 100644 --- a/src/Data/Parameterized/PairF.hs +++ b/src/Data/Parameterized/PairF.hs @@ -15,6 +15,7 @@ module Data.Parameterized.PairF ) where import Data.Kind (Type) +import Data.Parameterized.Classes data PairF tp1 tp2 k = PairF (tp1 k) (tp2 k) @@ -26,6 +27,16 @@ type instance TupleF '(a,b,c,d) = PairF a (PairF b (PairF c d)) pattern TupleF2 :: a k -> b k -> TupleF '(a,b) k pattern TupleF2 a b = PairF a b +instance (TestEquality a, TestEquality b) => TestEquality (PairF a b) where + testEquality (PairF a1 b1) (PairF a2 b2) = + case (testEquality a1 a2, testEquality b1 b2) of + (Just Refl, Just Refl) -> Just Refl + _ -> Nothing + +instance (OrdF a, OrdF b) => OrdF (PairF a b) where + compareF (PairF a1 b1) (PairF a2 b2) = + lexCompareF a1 a2 $ compareF b1 b2 + {-# COMPLETE TupleF2 #-} pattern TupleF3 :: a k -> b k -> c k -> TupleF '(a,b,c) k diff --git a/src/Pate/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs index f27a7a8a..06587b78 100644 --- a/src/Pate/Equivalence/Error.hs +++ b/src/Pate/Equivalence/Error.hs @@ -170,6 +170,7 @@ data InnerEquivalenceError arch | RequiresInvalidPointerOps | PairGraphError PairGraphErr | forall e. X.Exception e => UnhandledException e + | IncompatibleSingletonNodes (PB.ConcreteBlock arch PBi.Original) (PB.ConcreteBlock arch PBi.Patched) | SolverError X.SomeException errShortName :: MS.SymArchConstraints arch => InnerEquivalenceError arch -> String diff --git a/src/Pate/Monad/Environment.hs b/src/Pate/Monad/Environment.hs index cbf92d5c..e8ef0d4e 100644 --- a/src/Pate/Monad/Environment.hs +++ b/src/Pate/Monad/Environment.hs @@ -134,6 +134,8 @@ data NodePriorityK = | PriorityDeferredPropagation | PriorityDomainRefresh | PriorityHandleReturn + | PriorityHandleMerge + | PriorityFinalizeDivergence | PriorityMiscCleanup | PriorityDeferred deriving (Eq, Ord) @@ -153,8 +155,13 @@ printPriorityKind (NodePriority pk _ _ ) = case pk of PriorityDeferredPropagation -> "Propagating Deferred Conditions" PriorityDomainRefresh -> "Re-checking Equivalence Domains" PriorityHandleReturn -> "Handling Function Return" + PriorityHandleMerge -> "Handling Control Flow Merge" PriorityMiscCleanup -> "Proof Cleanup" PriorityDeferred -> "Handling Deferred Decisions" + -- this should be lowest priority since we want to defer this + -- until any other analysis is complete + PriorityFinalizeDivergence -> "Finalizing Control Flow Divergence" + instance IsTraceNode k "priority" where type TraceNodeType k "priority" = NodePriority diff --git a/src/Pate/Monad/PairGraph.hs b/src/Pate/Monad/PairGraph.hs index c970d52c..c5db1557 100644 --- a/src/Pate/Monad/PairGraph.hs +++ b/src/Pate/Monad/PairGraph.hs @@ -13,7 +13,6 @@ module Pate.Monad.PairGraph , evalPG , withPG_ , liftPG - , liftPartEqM_ , catchPG , liftEqM , liftEqM_ @@ -25,6 +24,8 @@ module Pate.Monad.PairGraph , considerDesyncEvent , addLazyAction , queuePendingNodes + , runPG + , liftPartEqM_ ) where import Control.Monad.State.Strict @@ -54,9 +55,11 @@ import qualified Pate.Equivalence.Condition as PEC import qualified Data.Macaw.CFG as MM import qualified Data.Map as Map import qualified Pate.Equivalence.Error as PEE +import GHC.Stack (HasCallStack) withPG :: + HasCallStack => PairGraph sym arch -> StateT (PairGraph sym arch) (EquivM_ sym arch) a -> EquivM sym arch (a, PairGraph sym arch) @@ -69,12 +72,13 @@ evalPG :: evalPG pg f = fst <$> (withPG pg $ liftPG f) withPG_ :: + HasCallStack => PairGraph sym arch -> StateT (PairGraph sym arch) (EquivM_ sym arch) a -> EquivM sym arch (PairGraph sym arch) withPG_ pg f = execStateT f pg -liftPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a +liftPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a liftPG f = do pg <- get case runPairGraphM pg f of @@ -83,7 +87,12 @@ liftPG f = do put pg' return a -catchPG :: PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a) +runPG :: HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM_ sym arch (a, PairGraph sym arch) +runPG pg f = case runPairGraphM pg f of + Left err -> throwHere $ PEE.PairGraphError err + Right a -> return a + +catchPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a) catchPG f = do pg <- get case runPairGraphM pg f of @@ -93,6 +102,7 @@ catchPG f = do return $ Just a liftEqM_ :: + HasCallStack => (PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch)) -> StateT (PairGraph sym arch) (EquivM_ sym arch) () liftEqM_ f = liftEqM $ \pg -> ((),) <$> (f pg) @@ -105,6 +115,7 @@ liftPartEqM_ f = liftEqM $ \pg -> f pg >>= \case Nothing -> return (False, pg) liftEqM :: + HasCallStack => (PairGraph sym arch -> EquivM_ sym arch (a, PairGraph sym arch)) -> StateT (PairGraph sym arch) (EquivM_ sym arch) a liftEqM f = do diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 28376187..511cae08 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -68,13 +68,14 @@ module Pate.Verification.PairGraph , markEdge , getSyncPoints , getBackEdgesFrom - , addSyncNode , getCombinedSyncPoints , combineNodes , NodePriority(..) , addToWorkList - , WorkItem + , WorkItem(FinalizeDivergence, ProcessNode) + , pattern ProcessMerge , workItemNode + , singleSidedReturns , getQueuedPriority , queueAncestors , queueNode @@ -107,18 +108,20 @@ module Pate.Verification.PairGraph , propagateOnce , getPropagationKind , propagateAction - , getSyncAddress - , setSyncAddress - , checkForNodeSync - , checkForReturnSync + , getSyncAddresses + , addSyncAddress + -- , filterSyncExits , pairGraphComputeVerdict -- FIXME: remove this and have modules import this directly , module Data.Parameterized.PairF + , handleSingleSidedReturnTo + , filterSyncExits + , isDivergeNode ) where import Prettyprinter -import Control.Monad (guard, forM) +import Control.Monad (guard, forM, forM_, filterM, unless) import Control.Monad.IO.Class import Control.Monad.State.Strict (MonadState (..), modify, State, gets) import Control.Monad.Except (ExceptT, MonadError (..)) @@ -132,7 +135,7 @@ import Data.Kind (Type) import qualified Data.Foldable as F import Data.Map (Map) import qualified Data.Map as Map -import Data.Maybe (fromMaybe) +import Data.Maybe (fromMaybe, catMaybes) import Data.Parameterized.Classes import Data.Set (Set) import qualified Data.Set as Set @@ -175,6 +178,7 @@ import Data.Foldable (find) import Data.Parameterized.PairF import Data.Parameterized.SetF (SetF) import qualified Data.Parameterized.SetF as SetF +import GHC.Stack (HasCallStack) -- | Gas is used to ensure that our fixpoint computation terminates -- in a reasonable amount of time. Gas is expended each time @@ -301,11 +305,125 @@ type WorkList arch = RevMap (WorkItem arch) NodePriority -- at the top-level. data WorkItem arch = -- | Handle all normal node processing logic - ProcessNode (GraphNode arch) + ProcessNode (GraphNode arch) + -- | Handle merging two single-sided analyses (both nodes must share a diverge point) + | ProcessMergeCtor + (SingleNodeEntry arch PBi.Original) + (SingleNodeEntry arch PBi.Patched) + | FinalizeDivergence (GraphNode arch) deriving (Eq, Ord) +-- Use mkProcessMerge as a partial smart constructor, but +-- export this pattern so we can match on it +pattern ProcessMerge :: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch +pattern ProcessMerge sneO sneP <- ProcessMergeCtor sneO sneP + +{-# COMPLETE ProcessNode, ProcessMerge, FinalizeDivergence #-} + +-- TODO: After some refactoring I'm not sure if we actually need edge actions anymore, so this potentially can be simplified +data ActionQueue sym arch = + ActionQueue + { _edgeActions :: Map (GraphNode arch, GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, PS.SimBundle sym arch, AbstractDomain sym arch, AbstractDomain sym arch))] + , _nodeActions :: Map (GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, PS.SimBundle sym arch, AbstractDomain sym arch))] + , _refineActions :: Map (GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, AbstractDomain sym arch))] + , _queueActions :: Map () [PendingAction sym arch (Const ())] + , _latestPendingId :: Int + } + +data PendingAction sym arch (f :: PS.VarScope -> Type) = + PendingAction { pactIdent :: Int, pactAction :: LazyIOAction (EquivEnv sym arch, Some f, PairGraph sym arch) (PairGraph sym arch)} + +data DomainRefinementKind = + RefineUsingIntraBlockPaths + | RefineUsingExactEquality + +data DomainRefinement sym arch = + LocationRefinement ConditionKind DomainRefinementKind (PL.SomeLocation sym arch -> Bool) + | PruneBranch ConditionKind + | AlignControlFlowRefinment ConditionKind + +data ConditionKind = + ConditionAsserted + | ConditionAssumed + -- ^ flag is true if this assumption should be propagated to ancestor nodes. + -- After propagation, this is set to false so that it only propagates once. + -- See 'nextCondition' + | ConditionEquiv + -- ^ a separate category for equivalence conditions, which should be shown + -- to the user once the analysis is complete + deriving (Eq,Ord, Enum, Bounded) + +data PropagateKind = + PropagateFull + | PropagateFullNoPaths + | PropagateOnce + | PropagateNone + deriving (Eq,Ord, Enum, Bounded) + +-- | Defines the data structure for tracking how to re-synchronize +-- control flow for a given diverge point. +-- Each diverge node yields two single-sided analyses, which +-- terminate (i.e. sync back with the normal two-sided analysis) +-- when they reach a defined sync point. A sync point is defined +-- as a single-sided GraphNode, paired with a "cut" address +-- indicating a particular exit from that node. +-- Cut addresses are provided at the start of the split analysis, +-- and the merge nodes are discovered during the single-sided analysis +-- when a node is determined to be able to exit to a cut point. +-- Note that, for a given divergence, we need to take the product +-- of Original sync point vs. every Patched sync point +-- In practice this is still reasonably small, since there are usually +-- only 2-3 cut addresses on each side (i.e. 4-9 merge cases to consider) +data SyncPoint arch = + SyncPoint + { + -- | During single-sided analysis, if we encounter an edge + -- that ends in a cut point, we + -- mark it here as a node that needs to be considered for merging + _syncMergeNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) + -- | Instruction addresses that, if reached during single-sided + -- analysis (from the corresponding diverge point), + -- should trigger a merge back into a two-sided analysis + , _syncCutAddresses :: PPa.PatchPair (SetF (PPa.WithBin (PAd.ConcreteAddress arch))) + -- | Defines exceptions for exits that would otherwise be considered sync points. + -- In these cases, the single-sided analysis continues instead, with the intention + -- that another sync point is encountered after additional instructions are executed + , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch))) + -- | The single-sided nodes that were + -- introduced when a single-sided analysis of a function returned + -- exactly to a cut point. + , _syncReturnTargets :: PPa.PatchPair (SetF (SingleNodeEntry arch)) + + } + +$(L.makeLenses ''SyncPoint) +$(L.makeLenses ''ActionQueue) + +type ActionQueueLens sym arch k v = L.Lens' (ActionQueue sym arch) (Map k [PendingAction sym arch v]) + +-- | Combine two single-sided nodes into a 'WorkItem' to process their +-- merge. Returns 'Nothing' if the two single-sided nodes have different +-- divergence points. +mkProcessMerge :: + SingleNodeEntry arch bin -> + SingleNodeEntry arch (PBi.OtherBinary bin) -> + Maybe (WorkItem arch) +mkProcessMerge sne1 sne2 + | dp1 <- singleNodeDivergePoint sne1 + , dp2 <- singleNodeDivergePoint sne2 + , dp1 == dp2 = case singleEntryBin sne1 of + PBi.OriginalRepr -> Just $ ProcessMergeCtor sne1 sne2 + PBi.PatchedRepr -> Just $ ProcessMergeCtor sne2 sne1 +mkProcessMerge _ _ = Nothing + workItemNode :: WorkItem arch -> GraphNode arch -workItemNode (ProcessNode nd) = nd +workItemNode = \case + ProcessNode nd -> nd + ProcessMerge sneO sneP -> case combineSingleEntries sneO sneP of + Just merged -> GraphNode merged + Nothing -> panic Verifier "workItemNode" ["Unexpected mismatched single-sided nodes"] + FinalizeDivergence dp -> dp + newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a } deriving (Functor @@ -345,6 +463,7 @@ evalPairGraphM pg f = case runPairGraphM pg f of lookupPairGraph :: forall sym arch b. + HasCallStack => (PairGraph sym arch -> Map (GraphNode arch) b) -> GraphNode arch -> PairGraphM sym arch b @@ -352,24 +471,6 @@ lookupPairGraph f node = do m <- gets f pgMaybe "missing node entry" $ Map.lookup node m -data ConditionKind = - ConditionAsserted - | ConditionAssumed - -- ^ flag is true if this assumption should be propagated to ancestor nodes. - -- After propagation, this is set to false so that it only propagates once. - -- See 'nextCondition' - | ConditionEquiv - -- ^ a separate category for equivalence conditions, which should be shown - -- to the user once the analysis is complete - deriving (Eq,Ord, Enum, Bounded) - -data PropagateKind = - PropagateFull - | PropagateFullNoPaths - | PropagateOnce - | PropagateNone - deriving (Eq,Ord, Enum, Bounded) - propagateAction :: PropagateKind -> String propagateAction = \case @@ -423,18 +524,6 @@ conditionAction = \case ConditionAssumed{} -> "Assume" ConditionEquiv{} -> "Assume as equivalence condition" - -data DomainRefinementKind = - RefineUsingIntraBlockPaths - | RefineUsingExactEquality - - - -data DomainRefinement sym arch = - LocationRefinement ConditionKind DomainRefinementKind (PL.SomeLocation sym arch -> Bool) - | PruneBranch ConditionKind - | AlignControlFlowRefinment ConditionKind - addDomainRefinement :: GraphNode arch -> DomainRefinement sym arch -> @@ -455,33 +544,6 @@ getNextDomainRefinement nd pg = case Map.lookup nd (pairGraphDomainRefinements p Just (refine:rest) -> Just (refine, pg {pairGraphDomainRefinements = Map.insert nd rest (pairGraphDomainRefinements pg)}) _ -> Nothing - -data PendingAction sym arch (f :: PS.VarScope -> Type) = - PendingAction { pactIdent :: Int, pactAction :: LazyIOAction (EquivEnv sym arch, Some f, PairGraph sym arch) (PairGraph sym arch)} - --- TODO: After some refactoring I'm not sure if we actually need edge actions anymore, so this potentially can be simplified -data ActionQueue sym arch = - ActionQueue - { _edgeActions :: Map (GraphNode arch, GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, PS.SimBundle sym arch, AbstractDomain sym arch, AbstractDomain sym arch))] - , _nodeActions :: Map (GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, PS.SimBundle sym arch, AbstractDomain sym arch))] - , _refineActions :: Map (GraphNode arch) [PendingAction sym arch (TupleF '(PS.SimScope sym arch, AbstractDomain sym arch))] - , _queueActions :: Map () [PendingAction sym arch (Const ())] - , _latestPendingId :: Int - } - - -data SyncPoint arch = - SyncPoint - -- each side of the analysis independently defines a set of - -- graph nodes, representing CFARs that can terminate - -- respectively on the cut addresses - -- The "merge" nodes are the cross product of these, since we - -- must assume that any combination of exits is possible - -- during the single-sided analysis - { syncStartNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) - , syncCutAddresses :: PPa.PatchPairC (PAd.ConcreteAddress arch) - } - ppProgramDomains :: forall sym arch a. ( PA.ValidArch arch @@ -654,6 +716,10 @@ queueAncestors priority nd pg = queueNode :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGraph sym arch queueNode priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) +queueWorkItem :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGraph sym arch +queueWorkItem priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) + + -- | Adds a node to the work list. If it doesn't have a domain, queue its ancestors. -- Takes a set of nodes that have already been considerd, and returns all considered nodes queueNode' :: NodePriority -> GraphNode arch -> (Set (GraphNode arch), PairGraph sym arch) -> (Set (GraphNode arch), PairGraph sym arch) @@ -802,21 +868,49 @@ hasWorkLeft pg = case RevMap.minView_value (pairGraphWorklist pg) of Nothing -> False Just{} -> True +isDivergeNode :: + GraphNode arch -> PairGraph sym arch -> Bool +isDivergeNode nd pg = Map.member nd (pairGraphSyncPoints pg) + -- | Given a pair graph, chose the next node in the graph to visit -- from the work list, updating the necessary bookeeping. If the -- work list is empty, return Nothing, indicating that we are done. chooseWorkItem :: PA.ValidArch arch => PairGraph sym arch -> - Maybe (NodePriority, PairGraph sym arch, WorkItem arch, AbstractDomainSpec sym arch) -chooseWorkItem gr = - -- choose the smallest pair from the worklist. This is a pretty brain-dead - -- heuristic. Perhaps we should do something more clever. + Maybe (NodePriority, PairGraph sym arch, WorkItem arch) +chooseWorkItem gr = case runPairGraphM gr chooseWorkItem' of + Left err -> panic Verifier "chooseWorkItem" ["Unexpected PairGraphM error", show err] + Right (Just (np,wi),gr1) -> Just (np,gr1,wi) + Right (Nothing, _) -> Nothing + +chooseWorkItem' :: + PA.ValidArch arch => + PairGraphM sym arch (Maybe (NodePriority, WorkItem arch)) +chooseWorkItem' = do + gr <- get case RevMap.minView_value (pairGraphWorklist gr) of - Nothing -> Nothing - Just (wi, p, wl) -> case Map.lookup (workItemNode wi) (pairGraphDomains gr) of - Nothing -> panic Verifier "chooseWorkItem" ["Could not find domain corresponding to block pair", show (workItemNode wi)] - Just d -> Just (p, gr{ pairGraphWorklist = wl }, wi, d) + Nothing -> return Nothing + Just (wi, p, wl) -> do + modify $ \gr_ -> gr_ { pairGraphWorklist = wl } + case wi of + ProcessNode (GraphNode ne) | Just (Some sne) <- asSingleNodeEntry ne -> do + let bin = singleEntryBin sne + let sne_addr = PB.concreteAddress $ singleNodeBlock sne + (exceptEdges, _) <- getSingleNodeSync syncExceptions sne + (cutAddrs, _) <- getSingleNodeSync syncCutAddresses sne + let isCutAddr = SetF.member (PPa.WithBin bin sne_addr) cutAddrs + let excepts = SetF.map (\(TupleF2 sne_ _) -> sne_) exceptEdges + let isExcepted = SetF.member sne excepts + case (isCutAddr, isExcepted) of + -- special case where we ignore single-sided nodes + -- that are exactly at the cut point, since this should + -- be handled as part of merging any nodes that reach this + (True, False) -> chooseWorkItem' + _ -> return $ Just (p,wi) + -- FIXME: handle diverge node? + + _ -> return $ Just (p,wi) -- | Update the abstract domain for the target graph node, -- decreasing the gas parameter as necessary. @@ -921,21 +1015,23 @@ pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg getSyncPoints :: forall sym arch bin. + HasCallStack => PBi.WhichBinaryRepr bin -> GraphNode arch -> PairGraphM sym arch (Set (SingleNodeEntry arch bin)) getSyncPoints bin nd = do - (SyncPoint syncPair _) <- lookupPairGraph @sym pairGraphSyncPoints nd + (SyncPoint syncPair _ _ _) <- lookupPairGraph @sym pairGraphSyncPoints nd SetF.toSet <$> PPa.get bin syncPair -getSyncAddress :: +getSyncAddresses :: forall sym arch bin. + HasCallStack => PBi.WhichBinaryRepr bin -> GraphNode arch -> - PairGraphM sym arch (PAd.ConcreteAddress arch) -getSyncAddress bin nd = do - (SyncPoint _ addrPair) <- lookupPairGraph @sym pairGraphSyncPoints nd - PPa.getC bin addrPair + PairGraphM sym arch (Set (PAd.ConcreteAddress arch)) +getSyncAddresses bin nd = fmap (fromMaybe Set.empty) $ tryPG $ do + (SyncPoint _ addrPair _ _) <- lookupPairGraph @sym pairGraphSyncPoints nd + (Set.map PPa.withBinValue . SetF.toSet) <$> PPa.get bin addrPair updateSyncPoint :: forall sym arch. @@ -951,10 +1047,11 @@ updateSyncPoint nd f = do -- | Returns all discovered merge points from the given diverge point getCombinedSyncPoints :: forall sym arch. + HasCallStack => GraphNode arch -> PairGraphM sym arch ([((SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched), GraphNode arch)], SyncPoint arch) getCombinedSyncPoints ndDiv = do - sync@(SyncPoint syncSet _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv + sync@(SyncPoint syncSet _ _ _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv case syncSet of PPa.PatchPair ndsO ndsP -> do all_pairs <- forM (Set.toList $ Set.cartesianProduct (SetF.toSet ndsO) (SetF.toSet ndsP)) $ \(ndO, ndP) -> do @@ -983,35 +1080,74 @@ singleNodeRepr nd = case graphNodeBlocks nd of PPa.PatchPairSingle bin _ -> return $ Some bin PPa.PatchPair{} -> Nothing -addSyncNode :: - forall sym arch. - GraphNode arch {- ^ The divergent node -} -> - NodeEntry arch {- ^ the sync node -} -> - PairGraphM sym arch () -addSyncNode ndDiv ndSync = do - Some nd <- asSingleNodeEntry ndSync - (SyncPoint sp addrs) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv - let sp' = PPa.insertWith (singleEntryBin nd) (SetF.singleton nd) SetF.union sp - modify $ \pg -> pg { pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp' addrs) (pairGraphSyncPoints pg) } tryPG :: PairGraphM sym arch a -> PairGraphM sym arch (Maybe a) tryPG f = catchError (Just <$> f) (\_ -> return Nothing) -setSyncAddress :: +getSyncPoint :: + forall sym arch x bin. + HasCallStack => + L.Lens' (SyncPoint arch) (PPa.PatchPair x) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + PairGraphM sym arch (x bin) +getSyncPoint lens bin nd = do + sp <- lookupPairGraph @sym pairGraphSyncPoints nd + let x = sp ^. lens + PPa.get bin x + +-- | Retrive the 'SyncPoint' fields corresponding to +-- the divergence point of the given single-sided node +getSingleNodeSync :: + forall sym arch x bin. + HasCallStack => + L.Lens' (SyncPoint arch) (PPa.PatchPair x) -> + SingleNodeEntry arch bin -> + PairGraphM sym arch (x bin, x (PBi.OtherBinary bin)) +getSingleNodeSync lens sne = do + let bin = singleEntryBin sne + let nd = singleNodeDivergePoint sne + sp <- lookupPairGraph @sym pairGraphSyncPoints nd + let x = sp ^. lens + v1 <- PPa.get bin x + v2 <- PPa.get (PBi.flipRepr bin) x + return (v1, v2) + +-- | Initialize an empty sync point entry for the given node, if +-- one doesn't already exist +initSyncPoint :: GraphNode arch -> PairGraphM sym arch () +initSyncPoint nd = do + pg <- get + case Map.member nd (pairGraphSyncPoints pg) of + True -> return () + False -> do + let sp = SyncPoint (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) + modify $ \pg_ -> pg_{ pairGraphSyncPoints = Map.insert nd sp (pairGraphSyncPoints pg) } + +addToSyncPoint :: + forall sym arch x bin. + OrdF x => + HasCallStack => + L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + x bin -> + PairGraphM sym arch () +addToSyncPoint lens bin nd x = do + initSyncPoint nd + sp <- lookupPairGraph @sym pairGraphSyncPoints nd + let sp' = sp & lens %~ PPa.insertWith bin (SetF.singleton x) SetF.union + -- make sure the other side has an empty set so that 'getSyncPoint' always succeeds + let sp'' = sp' & lens %~ PPa.insertWith (PBi.flipRepr bin) SetF.empty SetF.union + modify $ \pg -> pg{ pairGraphSyncPoints = Map.insert nd sp'' (pairGraphSyncPoints pg) } + +addSyncAddress :: forall sym arch bin. GraphNode arch {- ^ The divergent node -} -> PBi.WhichBinaryRepr bin -> PAd.ConcreteAddress arch -> PairGraphM sym arch () -setSyncAddress ndDiv bin syncAddr = do - let syncAddr' = PPa.PatchPairSingle bin (Const syncAddr) - tryPG (lookupPairGraph @sym pairGraphSyncPoints ndDiv) >>= \case - Just (SyncPoint sp addrs) -> do - addrs' <- PPa.update addrs $ \bin' -> PPa.get bin' syncAddr' - modify $ \pg -> pg{ pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp addrs') (pairGraphSyncPoints pg) } - Nothing -> do - let sp = PPa.mkPair bin SetF.empty SetF.empty - modify $ \pg -> pg{pairGraphSyncPoints = Map.insert ndDiv (SyncPoint sp syncAddr') (pairGraphSyncPoints pg) } +addSyncAddress nd bin syncAddr = addToSyncPoint syncCutAddresses bin nd (PPa.WithBin bin syncAddr) -- | Add a node back to the worklist to be re-analyzed if there is -- an existing abstract domain for it. Otherwise return Nothing. @@ -1021,9 +1157,17 @@ addToWorkList :: PairGraph sym arch -> Maybe (PairGraph sym arch) addToWorkList nd priority gr = case getCurrentDomain gr nd of - Just{} -> Just $ gr { pairGraphWorklist = RevMap.insertWith (min) (ProcessNode nd) priority (pairGraphWorklist gr) } + Just{} -> Just $ addItemToWorkList (ProcessNode nd) priority gr Nothing -> Nothing +-- | Add a work item to the worklist to be processed +addItemToWorkList :: + WorkItem arch -> + NodePriority -> + PairGraph sym arch -> + PairGraph sym arch +addItemToWorkList wi priority gr = gr { pairGraphWorklist = RevMap.insertWith (min) wi priority (pairGraphWorklist gr) } + -- | Return the priority of the given 'GraphNode' if it is queued for -- normal processing getQueuedPriority :: @@ -1105,12 +1249,6 @@ getOrphanedReturns gr = do let rets = (Map.keysSet (pairGraphReturnVectors gr)) Set.\\ (pairGraphTerminalNodes gr) Set.filter (\ret -> not (Map.member (ReturnNode ret) (pairGraphDomains gr))) rets - - -$(L.makeLenses ''ActionQueue) - -type ActionQueueLens sym arch k v = L.Lens' (ActionQueue sym arch) (Map k [PendingAction sym arch v]) - dropActId' :: Int -> ActionQueue sym arch -> @@ -1153,47 +1291,105 @@ getPendingActions lens = do pg <- get return $ (pairGraphPendingActs pg) ^. lens --- If the given node is single-sided, check if any of the exits --- match the given synchronization point for the diverge point of this node. --- --- We can restrict our search to just the block exits because we already --- defined the synchronization point as a cut point for code discovery. --- This means that any CFAR which can reach the sync point will necessarily --- have one block exit that jumps to it, regardless of where it is --- in a basic block. -checkForNodeSync :: - NodeEntry arch -> - [(PPa.PatchPair (PB.BlockTarget arch))] -> - PairGraphM sym arch Bool -checkForNodeSync ne targets_pairs = fmap (fromMaybe False) $ tryPG $ do - Some sne <- asSingleNodeEntry ne + +isSyncExit :: + SingleNodeEntry arch bin -> + PB.BlockTarget arch bin -> + PairGraphM sym arch (Maybe (PB.ConcreteBlock arch bin)) +isSyncExit sne blkt@(PB.BlockTarget{}) = do + let dp = singleNodeDivergePoint sne let bin = singleEntryBin sne - let dp = singleNodeDivergence sne - syncPoints <- getSyncPoints bin dp - syncAddr <- getSyncAddress bin dp - thisAddr <- fmap PB.concreteAddress $ PPa.get bin (nodeBlocks ne) - -- if this node is already defined as sync point then we don't - -- have to check anything else - if | Set.member sne syncPoints -> return True - -- similarly if this is exactly the sync address then we should - -- stop the single-sided analysis - | thisAddr == syncAddr -> return True - | otherwise -> do - targets <- mapM (PPa.get bin) targets_pairs - let matchTarget btgt = case btgt of - PB.BlockTarget{} -> PB.targetRawPC btgt == syncAddr - _ -> False - return $ isJust $ find matchTarget targets - --- Same as 'checkForNodeSync' but considers a single outgoing edge from --- a function return. -checkForReturnSync :: - NodeReturn arch -> + cuts <- getSyncPoint syncCutAddresses bin dp + excepts <- getSyncPoint syncExceptions bin dp + let isExcept = SetF.member (TupleF2 sne blkt) excepts + case (not isExcept) && + SetF.member (PPa.WithBin bin (PB.targetRawPC blkt)) cuts of + True -> return $ Just (PB.targetCall blkt) + False -> return Nothing +isSyncExit _ _ = return Nothing + +-- | Get all possible merge targets from the given node +-- (i.e. all merge nodes for diverge point of the given +-- entry) +otherMergeNodes :: + SingleNodeEntry arch bin -> + PairGraphM sym arch [SingleNodeEntry arch (PBi.OtherBinary bin)] +otherMergeNodes sne = do + let bin = singleEntryBin sne + let dp = singleNodeDivergePoint sne + merges <- getSyncPoint syncMergeNodes (PBi.flipRepr bin) dp + return $ SetF.toList merges + + +singleSidedReturns :: + GraphNode arch -> + PairGraphM sym arch [(SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched)] +singleSidedReturns nd = do + retsO <- getSyncPoint syncReturnTargets PBi.OriginalRepr nd + retsP <- getSyncPoint syncReturnTargets PBi.PatchedRepr nd + return $ [ (retO,retP) | retO <- SetF.toList retsO, retP <- SetF.toList retsP ] + +-- | Filter a list of reachable block exits to +-- only those that should be handled for the given 'WorkItem' +-- For a 'ProcessNode' item, this is all exits for a +-- two-sided node and all non-merge exits for a single-sided node. +-- For a single-sided node, any merge exits are paired with all +-- possible merge nodes from the other side of the analysis and +-- queued as a 'ProcessMerge' work item. +filterSyncExits :: + (NodePriorityK -> NodePriority) -> {- ^ priority to queue new work items at -} + WorkItem arch -> + [PPa.PatchPair (PB.BlockTarget arch)] -> + PairGraphM sym arch [PPa.PatchPair (PB.BlockTarget arch)] +filterSyncExits _priority (FinalizeDivergence{}) _ = fail "Unexpected FinalizeDivergence work item" +filterSyncExits _priority (ProcessNode (ReturnNode{})) _ = fail "Unexpected ReturnNode work item" +filterSyncExits _priority (ProcessMerge sneO sneP) blktPairs = do + let isSyncExitPair blktPair = do + blktO <- PPa.get PBi.OriginalRepr blktPair + blktP <- PPa.get PBi.PatchedRepr blktPair + x <- isSyncExit sneO blktO + y <- isSyncExit sneP blktP + return $ isJust x && isJust y + filterM isSyncExitPair blktPairs +filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of + Nothing -> return blktPairs + Just (Some sne) -> do + let dp = singleNodeDivergePoint sne + let bin = singleEntryBin sne + blkts <- mapM (PPa.get bin) blktPairs + exitBlks <- catMaybes <$> mapM (isSyncExit sne) blkts + forM_ exitBlks $ \blk -> do + let nextNode = mkSingleNodeEntry ne blk + addToSyncPoint syncReturnTargets bin dp nextNode + unless (null exitBlks) $ do + -- if any of the exits from this node are sync exits, + -- then we need to queue up processing this node as + -- a merge against all known merge points + addToSyncPoint syncMergeNodes bin dp sne + -- make sure that the divergence itself is finalized after all + -- other processing is done + modify $ addItemToWorkList (FinalizeDivergence dp) (priority PriorityFinalizeDivergence) + return blktPairs + +-- | For a given return -> entry transition, return a list of +-- entry nodes for all possible ways that control flow could +-- re-sync at the entry. i.e. if the given entry point is single-sided +-- but a sync address, then pair it with all possible merge nodes +-- from the other binary for the divergence point. +handleSingleSidedReturnTo :: + (NodePriorityK -> NodePriority) -> {- ^ priority to queue new work items at -} NodeEntry arch -> - PairGraphM sym arch Bool -checkForReturnSync nr ne = fmap (fromMaybe False) $ tryPG $ do - Just (Some bin) <- return $ isSingleReturn nr - Just dp <- return $ getDivergePoint (ReturnNode nr) - syncAddr <- getSyncAddress bin dp - blk <- PPa.get bin (nodeBlocks ne) - return $ PB.concreteAddress blk == syncAddr \ No newline at end of file + PairGraphM sym arch () +handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of + Just (Some sne) -> do + let bin = singleEntryBin sne + let dp = singleNodeDivergePoint sne + syncAddrs <- getSyncPoint syncCutAddresses bin dp + let blk = singleNodeBlock sne + case SetF.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of + True -> do + addToSyncPoint syncReturnTargets bin dp sne + -- need to re-check this as part of finalization + modify $ addItemToWorkList (FinalizeDivergence dp) (priority PriorityFinalizeDivergence) + False -> return () + Nothing -> return () diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 454d005b..792893e7 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -30,6 +30,7 @@ module Pate.Verification.PairGraph.Node ( , graphNodeBlocks , mkNodeEntry , mkNodeEntry' + , mkSingleNodeEntry , addContext , mkNodeReturn , rootEntry @@ -52,11 +53,14 @@ module Pate.Verification.PairGraph.Node ( , mkMergedNodeReturn , SingleNodeEntry , singleEntryBin + , singleNodeDivergePoint , asSingleNodeEntry , singleToNodeEntry + , singleNodeBlock , combineSingleEntries , singleNodeBlock , singleNodeDivergence + , toSingleNodeEntry ) where import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) @@ -394,6 +398,9 @@ data SingleNodeEntry arch bin = , _singleEntry :: NodeContent arch (PB.ConcreteBlock arch bin) } +mkSingleNodeEntry :: NodeEntry arch -> PB.ConcreteBlock arch bin -> SingleNodeEntry arch bin +mkSingleNodeEntry node blk = SingleNodeEntry (PB.blockBinRepr blk) (NodeContent (graphNodeContext node) blk) + instance TestEquality (SingleNodeEntry arch) where testEquality se1 se2 | EQF <- compareF se1 se2 = Just Refl testEquality _ _ = Nothing @@ -411,6 +418,11 @@ instance OrdF (SingleNodeEntry arch) where instance PA.ValidArch arch => Show (SingleNodeEntry arch bin) where show e = show (singleToNodeEntry e) +singleNodeDivergePoint :: SingleNodeEntry arch bin -> GraphNode arch +singleNodeDivergePoint (SingleNodeEntry _ (NodeContent cctx _)) = case divergePoint cctx of + Just dp -> dp + Nothing -> panic Verifier "singleNodeDivergePoint" ["missing diverge point for SingleNodeEntry"] + asSingleNodeEntry :: PPa.PatchPairM m => NodeEntry arch -> m (Some (SingleNodeEntry arch)) asSingleNodeEntry (NodeEntry cctx bPair) = do Pair bin blk <- PPa.asSingleton bPair @@ -418,32 +430,53 @@ asSingleNodeEntry (NodeEntry cctx bPair) = do Just{} -> return $ Some (SingleNodeEntry bin (NodeContent cctx blk)) Nothing -> PPa.throwPairErr +singleNodeBlock :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin +singleNodeBlock (SingleNodeEntry _ (NodeContent _ blk)) = blk + +-- | Returns a 'SingleNodeEntry' for a given 'NodeEntry' if it has an entry +-- for the given 'bin'. +-- Note that, in contrast to +-- 'asSingleNodeEntry' this does not require the given 'NodeEntry' to be a singleton +toSingleNodeEntry :: + PPa.PatchPairM m => + PB.WhichBinaryRepr bin -> + NodeEntry arch -> + m (SingleNodeEntry arch bin) +toSingleNodeEntry bin (NodeEntry cctx bPair) = do + blk <- PPa.get bin bPair + return $ SingleNodeEntry bin (NodeContent cctx blk) + singleToNodeEntry :: SingleNodeEntry arch bin -> NodeEntry arch singleToNodeEntry (SingleNodeEntry bin (NodeContent cctx v)) = NodeEntry cctx (PPa.PatchPairSingle bin v) -singleNodeBlock :: SingleNodeEntry arch bin -> PB.ConcreteBlock arch bin -singleNodeBlock (SingleNodeEntry _ (NodeContent _ blk)) = blk - singleNodeDivergence :: SingleNodeEntry arch bin -> GraphNode arch singleNodeDivergence (SingleNodeEntry _ (NodeContent cctx _)) = case divergePoint cctx of Just dp -> dp Nothing -> panic Verifier "singleNodeDivergence" ["Unexpected missing divergence point"] --- | Create a combined two-sided 'NodeEntry' based on --- a pair of single-sided entries. The given entries --- must have the same diverge point (returns 'Nothing' otherwise), --- and the calling context of the resulting node is inherited from --- that point (i.e. any additional context accumulated during --- the either single-sided analysis is discarded) -combineSingleEntries :: +combineSingleEntries' :: SingleNodeEntry arch PB.Original -> SingleNodeEntry arch PB.Patched -> Maybe (NodeEntry arch) -combineSingleEntries (SingleNodeEntry _ eO) (SingleNodeEntry _ eP) = do +combineSingleEntries' (SingleNodeEntry _ eO) (SingleNodeEntry _ eP) = do GraphNode divergeO <- divergePoint $ nodeContentCtx eO GraphNode divergeP <- divergePoint $ nodeContentCtx eP guard $ divergeO == divergeP let blksO = nodeContent eO let blksP = nodeContent eP - return $ mkNodeEntry divergeO (PPa.PatchPair blksO blksP) \ No newline at end of file + return $ mkNodeEntry divergeO (PPa.PatchPair blksO blksP) + +-- | Create a combined two-sided 'NodeEntry' based on +-- a pair of single-sided entries. The given entries +-- must have the same diverge point (returns 'Nothing' otherwise), +-- and the calling context of the resulting node is inherited from +-- that point (i.e. any additional context accumulated during +-- the either single-sided analysis is discarded) +combineSingleEntries :: + SingleNodeEntry arch bin -> + SingleNodeEntry arch (PB.OtherBinary bin) -> + Maybe (NodeEntry arch) +combineSingleEntries sne1 sne2 = case singleEntryBin sne1 of + PB.OriginalRepr -> combineSingleEntries' sne1 sne2 + PB.PatchedRepr -> combineSingleEntries' sne2 sne1 \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 11af1665..0d00becc 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -117,7 +117,7 @@ import qualified Pate.Verification.ConditionalEquiv as PVC import qualified Pate.Verification.Simplify as PSi import Pate.Verification.PairGraph -import Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, mkNodeEntry, mkNodeReturn, nodeBlocks, addContext, returnToEntry, graphNodeBlocks, returnOfEntry, nodeFuns, toSingleReturn, rootEntry, rootReturn, getDivergePoint, toSingleNode, mkNodeEntry', functionEntryOf, eqUptoDivergePoint, toSingleGraphNode, isSingleNodeEntry, divergePoint, isSingleReturn, NodeReturn, singleToNodeEntry, SingleNodeEntry, singleNodeBlock ) +import Pate.Verification.PairGraph.Node import Pate.Verification.Widening import qualified Pate.Verification.AbstractDomain as PAD import Data.Monoid (All(..), Any (..)) @@ -366,13 +366,6 @@ handleDanglingReturns fnPairs pg = do _ -> Nothing) single_rets case duals of [] -> return pg0 - {- - [dual] -> do - Just dom1 <- return $ getCurrentDomain pg0 (ReturnNode ret) - Just dom2 <- return $ getCurrentDomain pg0 (ReturnNode dual) - Just combined <- return $ combineNodes (ReturnNode ret) (ReturnNode dual) - mergeDualNodes (ReturnNode ret) (ReturnNode dual) dom1 dom2 combined pg0 - -} _ -> do let fn_single_ = PPa.mkSingle (PB.functionBinRepr fn_single) fn_single err <- emitError' (PEE.OrphanedSingletonAnalysis fn_single_) @@ -381,17 +374,6 @@ handleDanglingReturns fnPairs pg = do foldM go pg single_rets -handleSyncPoint :: - NodeEntry arch -> - PairGraph sym arch -> - EquivM sym arch (PairGraph sym arch) -handleSyncPoint nd pg = withTracing @"message" "End of single-sided analysis" $ withPG_ pg $ do - divergeNode <- liftPG $ do - Just divergeNode <- return $ getDivergePoint (GraphNode nd) - addSyncNode divergeNode nd - return divergeNode - liftEqM_ $ updateCombinedSyncPoint divergeNode - addressOfNode :: GraphNode arch -> EquivM sym arch (PPa.PatchPairC (MM.ArchSegmentOff arch)) @@ -452,14 +434,25 @@ chooseSyncPoint nd pg0 = do addr <- PB.concreteAddress <$> PPa.get syncBin (nodeBlocks sync) withPG_ pg0 $ do - liftPG $ setSyncAddress nd syncBin addr + liftPG $ addSyncAddress nd syncBin addr diverge <- PPa.getC otherBin divergePair syncOther <- lift $ fst <$> pickCutPoint syncMsg [diverge] addrOther <- PB.concreteAddress <$> PPa.get otherBin (nodeBlocks syncOther) - liftPG $ setSyncAddress nd otherBin addrOther + liftPG $ addSyncAddress nd otherBin addrOther + where syncMsg = "Choose a synchronization point:" +{- +queueSplitAnalysis :: + GraphNode arch -> + PairGraph sym arch -> + EquivM sym arch (PairGraph sym arch) +queueSplitAnalysis nd pg = do + -- we always start the split analysis + divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode + case getCurrentDomain pg ndO +-} {- guessDivergence :: @@ -543,157 +536,6 @@ cutAfterAddress addr blk = do True -> makeCut addr_next False -> go (addr_next:addrs) -{- -handleSyncPoint _ (GraphNode{}) _ = return Nothing -handleSyncPoint pg (ReturnNode nd) spec = case nodeFuns nd of - PPa.PatchPair{} -> do - ndO <- asSingleReturn PBi.OriginalRepr nd - ndP <- asSingleReturn PBi.PatchedRepr nd - -- if both single-sided cases have finished processing, then we can process - -- the return as usual - case (getCurrentDomain pg (ReturnNode ndO), getCurrentDomain pg (ReturnNode ndP)) of - (Just{}, Just{}) -> return Nothing - -- if either single-sided is not finished, we pop this return from the work - -- list under the assumption that it will be handled later - _ -> return $ Just pg - PPa.PatchPair{} -> return Nothing - PPa.PatchPairSingle bin _ -> case getSyncPoint pg nd of - Just syncs -> do - let go gr' nd' = case asSingleReturn (PBi.flipRepr bin) nd' of - Just nd_other -> case getCurrentDomain pg (ReturnNode nd_other) of - -- dual node has a spec, so we can merge them and add the result to the graph - -- as the sync point - Just{} | PPa.PatchPairC ndO ndP <- PPa.mkPair bin (Const nd) (Const nd') -> - chooseSyncPoint (ReturnNode ndO) (ReturnNode ndP) pg - -- if the dual node is not present in the graph, we assume it will - -- be handled when the dual case is pushed through the verifier, so - -- we drop it here - _ -> return gr' - Nothing -> PPa.throwPairErr - Just <$> foldM go pg (Set.elems syncs) - Nothing -> return Nothing --} - --- Connects the terminal nodes of any single-sided analysis to "merge" nodes --- Notably a single divergence may give rise to multiple synchronization points, --- since multiple CFARs may terminate at the provided address --- To address this we take the cartesian product of all original vs. patched sync points --- and create merge nodes for all of them -updateCombinedSyncPoint :: - GraphNode arch {- ^ diverging node -} -> - PairGraph sym arch -> - EquivM sym arch (PairGraph sym arch) -updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do - priority <- lift $ thisPriority - syncsO_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.OriginalRepr divergeNode - syncsP_ <- fmap Set.toList $ liftPG $ getSyncPoints PBi.PatchedRepr divergeNode - - -- collect all sync points that have been found and that have a pre-domain - syncsO <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM (GraphNode (singleToNodeEntry nd))) syncsO_ - syncsP <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM (GraphNode (singleToNodeEntry nd))) syncsP_ - - case syncsO of - -- We have not completed a single-sided analysis for the - -- Original binary. - -- We re-schedule the diverge node and any ancestors of discovered Original sync points. - -- This is needed to handle cases where the single-sided nodes have been dropped from - -- the graph as a result of some other operation (e.g. introducing an assertion). - -- In the case where the first Original single-sided node is dropped, this ensures that it is - -- re-scheduled by re-processing the divergence point. - [] -> do - divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode - liftPG $ do - modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO - -- also re-queue the ancestors of any known sync points that are missing domains - forM_ syncsO_ $ \syncO -> do - modify $ queueAncestors (priority PriorityHandleDesync) (GraphNode (singleToNodeEntry syncO)) - -- We have at least one completed one-sided analysis for the Original binary. - -- The convention is that we find at least one Original sync point before - -- moving on to the Patched one-sided analysis. - -- We artifically connect the post-domain of each Original one-sided analysis to the - -- pre-domain of the start of the Patched one-sided analysis. This ensures that any - -- assertions are carried forward to the Patched analysis. - _:_ -> do - (catchPG $ getCurrentDomainM divergeNode) >>= \case - Nothing -> liftPG $ modify $ queueNode (priority PriorityHandleDesync) divergeNode - Just dom_spec -> do - divergeNodeY <- toSingleGraphNode PBi.PatchedRepr divergeNode - fmap (\x -> PS.viewSpecBody x PS.unWS) $ PS.forSpec dom_spec $ \scope dom -> fmap PS.WithScope $ do - domP <- lift $ PAD.singletonDomain PBi.PatchedRepr dom - bundle <- lift $ noopBundle scope (graphNodeBlocks divergeNodeY) - forM_ syncsO $ \(syncO, _) -> do - liftPG $ (void $ getCurrentDomainM divergeNodeY) - <|> (modify $ \pg -> updateDomain' pg (GraphNode (singleToNodeEntry syncO)) divergeNodeY (PS.mkSimSpec scope domP) (priority PriorityWidening)) - liftEqM_ $ \pg -> withPredomain scope bundle domP $ withConditionsAssumed scope bundle dom divergeNode pg $ - widenAlongEdge scope bundle (GraphNode (singleToNodeEntry syncO)) domP pg divergeNodeY - - -- Finally, if we have any Patched one-sided results, we take all combinations - -- of Original and Patched sync points and connect them to a "combined" two-sided node - -- that contains the intersection of their pre-domains. - -- From this combined node, normal two-sided analysis can continue. - let syncPairs = [ (x,y) | x <- syncsO, y <- syncsP ] - forM_ syncPairs $ \((syncO, domO_spec), (syncP, domP_spec)) -> do - combinedNode <- liftPG $ do - Just combinedNode <- return $ combineNodes syncO syncP - return combinedNode - withTracingLabel @"node" "Merge Node" combinedNode $ do - emitTrace @"node" (GraphNode (singleToNodeEntry syncO)) - emitTrace @"node" (GraphNode (singleToNodeEntry syncO)) - liftEqM_ $ mergeDualNodes syncO syncP domO_spec domP_spec combinedNode - - -{- -fnTrace "updateCombinedSyncPoint" $ do - runMaybeT $ do - getCombinedSyncPoint divergeNode - - case getCombinedSyncPoint pg divergeNode of - Nothing -> do - emitTrace @"message" ("No sync node found for: " ++ show divergeNode) - return pg - Just (combinedNode, _) -> do - PPa.PatchPairC (syncO, mdomO) (syncP, mdomP) <- - PPa.forBinsC $ \bin -> do - Just sync <- return $ getSyncPoint pg bin divergeNode - mdom <- return $ getCurrentDomain pg sync - return $ (sync, mdom) - case (mdomO, mdomP) of - -- if we have finished analyzing the original program up to the sync point, - -- then we need to attach this to the divergence point of the patched program - (Just{}, Nothing) -> do - priority <- thisPriority - case getCurrentDomain pg divergeNode of - Nothing -> return $ queueNode (priority PriorityHandleDesync) divergeNode pg - Just dom_spec -> do - fmap (\x -> PS.viewSpecBody x PS.unWS) $ PS.forSpec dom_spec $ \scope dom -> fmap PS.WithScope $ do - domP <- PAD.singletonDomain PBi.PatchedRepr dom - divergeNodeP <- toSingleGraphNode PBi.PatchedRepr divergeNode - bundle <- noopBundle scope (graphNodeBlocks divergeNodeP) - pg1 <- case getCurrentDomain pg divergeNodeP of - Nothing -> return $ updateDomain' pg syncO divergeNodeP (PS.mkSimSpec scope domP) (priority PriorityWidening) - Just{} -> return pg - withPredomain scope bundle domP $ withConditionsAssumed scope syncO pg1 $ - widenAlongEdge scope bundle syncO domP pg1 divergeNodeP - (Just domO_spec, Just domP_spec) -> do - -- similarly if we've finished analyzing the patched program, then by convention - -- we connect the post-domain of the to the merged sync point - mergeDualNodes syncO syncP domO_spec domP_spec combinedNode pg - _ -> withTracing @"message" "Missing domain(s) for sync points" $ do - priority <- thisPriority - divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode - return $ queueNode (priority PriorityDomainRefresh) divergeNodeO $ queueAncestors (priority PriorityHandleDesync) syncO pg --} - -{- --- | Connect two nodes with a no-op -atomicJump :: - (GraphNode arch, GraphNode arch) -> - PAD.AbstractDomainSpec sym arch -> - PairGraph sym arch -> - EquivM sym arch (PairGraph sym arch) -atomicJump (from,to) domSpec gr0 = withSym $ \sym -> do --} - addImmediateEqDomRefinementChoice :: GraphNode arch -> PAD.AbstractDomain sym arch v -> @@ -715,6 +557,114 @@ addImmediateEqDomRefinementChoice nd preD gr0 = do choice ("No refinements") () $ return gr1 mapM_ go [minBound..maxBound] +{- +initSingleSidedDomain :: + GraphNode arch -> + WhichBinaryRepr bin -> + PairGraph sym arch -> + EquivM sym arch (PairGraph sym arch) +initSingleSidedDomain nd bin pg = do + nd_single <- toSingleGraphNode bin nd + case getCurrentDomain nd pg of + Just dom_spec -> do + + case getCurrentDomain nd_single pg of + Just{} -> return pg + Nothing -> do +-} + +workItemDomainSpec :: + WorkItem arch -> + PairGraph sym arch -> + EquivM sym arch (Maybe (GraphNode arch, PAD.AbstractDomainSpec sym arch), PairGraph sym arch) +workItemDomainSpec wi pg = withPG pg $ case wi of + FinalizeDivergence dp -> do + snePairs <- liftPG $ singleSidedReturns dp + forM_ snePairs $ \(sneO, sneP) -> do + void $ liftEqM $ mergeSingletons sneO sneP + return Nothing + ProcessNode nd -> do + dom_spec <- liftPG $ getCurrentDomainM nd + case isDivergeNode nd pg of + True -> do + priority <- lift $ thisPriority + divergeNodeO <- toSingleGraphNode PBi.OriginalRepr nd + case getCurrentDomain pg divergeNodeO of + Just{} -> liftPG $ modify $ queueNode (priority PriorityHandleDesync) divergeNodeO + Nothing -> error "TODO" + False -> error "TODO" + + return $ Just (nd, dom_spec) + ProcessMerge sneO sneP -> do + let + ndO = GraphNode $ singleToNodeEntry sneO + ndP = GraphNode $ singleToNodeEntry sneP + divergeNode = singleNodeDivergePoint sneO + priority <- lift $ thisPriority + case getCurrentDomain pg divergeNode of + Nothing -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode + return Nothing + Just diverge_dom_spec -> do + case (getCurrentDomain pg ndO, getCurrentDomain pg ndP) of + (Just{}, Just{}) -> do + syncNode <- liftEqM $ mergeSingletons sneO sneP + dom_spec <- liftPG $ getCurrentDomainM (GraphNode syncNode) + return $ Just (GraphNode syncNode, dom_spec) + (Just ndO_dom_spec, Nothing) -> do + divergeNodeP <- toSingleGraphNode PBi.PatchedRepr divergeNode + _ <- PS.forSpec diverge_dom_spec $ \scope diverge_dom -> do + diverge_domP <- lift $ PAD.singletonDomain PBi.PatchedRepr diverge_dom + bundle <- lift $ noopBundle scope (graphNodeBlocks divergeNodeP) + -- if the current domain for the patched variant of the diverge node + -- doesn't exist, then we initialize it as the "singletonDomain" + -- otherwise we leave it unmodified, as it's potentially been widened + liftPG $ (void $ getCurrentDomainM divergeNodeP) + <|> (modify $ \pg_ -> updateDomain' pg_ ndO divergeNodeP (PS.mkSimSpec scope diverge_domP) (priority PriorityWidening)) + liftEqM_ $ \pg_ -> withPredomain scope bundle diverge_domP $ withConditionsAssumed scope bundle diverge_dom divergeNode pg_ $ + widenAlongEdge scope bundle ndO diverge_domP pg_ divergeNodeP + return (PS.WithScope ()) + return Nothing + (Nothing, _) -> do + divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO + return Nothing + +mergeSingletons :: + SingleNodeEntry arch PBi.Original -> + SingleNodeEntry arch PBi.Patched -> + PairGraph sym arch -> + EquivM sym arch (NodeEntry arch, PairGraph sym arch) +mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do + let + blkO = singleNodeBlock sneO + blkP = singleNodeBlock sneP + ndO = GraphNode $ singleToNodeEntry sneO + ndP = GraphNode $ singleToNodeEntry sneP + blkPairO = PPa.PatchPairSingle PBi.OriginalRepr blkO + blkPairP = PPa.PatchPairSingle PBi.PatchedRepr blkP + blkPair = PPa.PatchPair blkO blkP + + syncNode <- case combineSingleEntries sneO sneP of + Just ne -> return ne + Nothing -> throwHere $ PEE.IncompatibleSingletonNodes blkO blkP + + specO <- evalPG pg $ getCurrentDomainM ndO + specP <- evalPG pg $ getCurrentDomainM ndP + + pg1 <- fmap (\x -> PS.viewSpecBody x PS.unWS) $ withFreshScope blkPair $ \scope -> fmap PS.WithScope $ + withValidInit scope blkPairO $ withValidInit scope blkPairP $ do + (_, domO) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) specO + (_, domP) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) specP + dom <- PAD.zipSingletonDomains sym domO domP + bundle <- noopBundle scope (nodeBlocks syncNode) + withPredomain scope bundle dom $ withConditionsAssumed scope bundle domP ndP pg $ do + withTracing @"node" ndP $ do + emitTraceLabel @"domain" PAD.Predomain (Some dom) + widenAlongEdge scope bundle ndP dom pg (GraphNode syncNode) + return (syncNode, pg1) + + mergeDualNodes :: SingleNodeEntry arch PBi.Original {- ^ original program node -} -> SingleNodeEntry arch PBi.Patched {- ^ patched program node -} -> @@ -753,16 +703,17 @@ withWorkItem gr0 f = do gr0' <- lift $ queuePendingNodes gr0 case chooseWorkItem gr0' of Nothing -> return Nothing - Just (priority, gr1, wi, spec) -> do - let nd = workItemNode wi - res <- subTraceLabel @"node" (printPriorityKind priority) nd $ startTimer $ - atPriority priority Nothing $ PS.viewSpec spec $ \scope d -> do - runPendingActions refineActions nd (TupleF2 scope d) gr1 >>= \case - Just gr2 -> return $ Left gr2 - Nothing -> Right <$> f (priority, gr1, wi, spec) - case res of - Left gr2 -> withWorkItem gr2 f - Right a -> return $ Just a + Just (priority, gr0'', wi) -> (lift $ workItemDomainSpec wi gr0'') >>= \case + (Nothing, gr1) -> withWorkItem gr1 f + (Just (nd, spec), gr1) -> do + res <- subTraceLabel @"node" (printPriorityKind priority) nd $ startTimer $ + atPriority priority Nothing $ PS.viewSpec spec $ \scope d -> do + runPendingActions refineActions nd (TupleF2 scope d) gr1 >>= \case + Just gr2 -> return $ Left gr2 + Nothing -> Right <$> f (priority, gr1, wi, spec) + case res of + Left gr2 -> withWorkItem gr2 f + Right a -> return $ Just a -- | Execute the forward dataflow fixpoint algorithm. -- Visit nodes and compute abstract domains until we propagate information @@ -790,7 +741,7 @@ pairGraphComputeFixpoint entries gr_init = do False -> return d withAssumptionSet (PS.scopeAsm scope) $ do gr2 <- addRefinementChoice nd gr1 - gr3 <- visitNode scope nd d' gr2 + gr3 <- visitNode scope wi d' gr2 emitEvent $ PE.VisitedNode nd return gr3 case mgr4 of @@ -1338,11 +1289,11 @@ checkParsedBlocks pPair = PPa.catBins $ \bin -> do visitNode :: forall sym arch v. HasCallStack => PS.SimScope sym arch v -> - GraphNode arch -> + WorkItem arch -> AbstractDomain sym arch v -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 = +visitNode scope wi@(workItemNode -> (GraphNode node@(nodeBlocks -> bPair))) d gr0 = withAbsDomain node d gr0 $ do checkParsedBlocks bPair withValidInit scope bPair $ do @@ -1358,20 +1309,11 @@ visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 = return $ queueNode (priority PriorityHandleActions) (GraphNode node) gr3 Nothing -> withConditionsAssumed scope bundle d (GraphNode node) gr0 $ do exitPairs <- PD.discoverPairs bundle - -- if a sync point is reachable then we don't want to do - -- further analysis, since we want to instead treat this - -- node as a merge point - withPG_ gr2 $ do - (liftPG $ checkForNodeSync node exitPairs) >>= \case - True -> liftEqM_ $ handleSyncPoint node - False -> liftEqM_ $ \pg -> do - handleSplitAnalysis scope node d pg >>= \case - Just pg' -> return pg' - Nothing -> do - pg' <- processBundle scope node bundle d exitPairs pg - fromMaybe pg' <$> handleSplitAnalysis scope node d pg' - -visitNode scope (ReturnNode fPair) d gr0 = do + priority <- thisPriority + (filteredPairs, gr3) <- runPG gr2 $ filterSyncExits priority wi exitPairs + processBundle scope node bundle d filteredPairs gr3 + +visitNode scope (workItemNode -> (ReturnNode fPair)) d gr0 = do -- propagate the abstract domain of the return node to -- all of the known call sites of this function. let rets = getReturnVectors gr0 fPair @@ -1403,6 +1345,7 @@ visitNode scope (ReturnNode fPair) d gr0 = do processReturn gr0' node@(nodeBlocks -> ret) = do + priority <- thisPriority let vars = PS.scopeVars scope varsSt = TF.fmapF PS.simVarState vars @@ -1412,7 +1355,6 @@ visitNode scope (ReturnNode fPair) d gr0 = do withAssumptionSet asm $ withPredomain scope bundle d $ do runPendingActions nodeActions (ReturnNode fPair) (TupleF3 scope bundle d) gr0' >>= \case Just gr1 -> do - priority <- thisPriority return $ queueNode (priority PriorityHandleActions) (ReturnNode fPair) gr1 Nothing -> withConditionsAssumed scope bundle d (ReturnNode fPair) gr0 $ do traceBundle bundle "Processing return edge" @@ -1426,9 +1368,7 @@ visitNode scope (ReturnNode fPair) d gr0 = do withPG_ gr0' $ do liftEqM_ $ checkObservables scope node bundle d liftEqM_ $ \pg -> widenAlongEdge scope bundle (ReturnNode fPair) d pg (GraphNode node) - (liftPG $ checkForReturnSync fPair node) >>= \case - True -> liftEqM_ $ handleSyncPoint node - False -> return () + liftPG $ handleSingleSidedReturnTo priority node -- | Construct a "dummy" simulation bundle that basically just -- immediately returns the prestate as the poststate. @@ -2584,6 +2524,9 @@ singletonBundle :: singletonBundle bin (SimBundle in_ out_) = SimBundle <$> PPa.toSingleton bin in_ <*> PPa.toSingleton bin out_ + + +{- -- | Check if the given node has defined sync addresses. If so, -- connect it to the one-sided Original version of the node and -- queue it in the worklist. @@ -2597,8 +2540,8 @@ handleSplitAnalysis :: EquivM sym arch (Maybe (PairGraph sym arch)) handleSplitAnalysis scope node dom pg = do let syncAddrs = evalPairGraphM pg $ do - syncO <- getSyncAddress PBi.OriginalRepr (GraphNode node) - syncP <- getSyncAddress PBi.PatchedRepr (GraphNode node) + syncO <- getSyncAddresses PBi.OriginalRepr (GraphNode node) + syncP <- getSyncAddresses PBi.PatchedRepr (GraphNode node) return (syncO, syncP) case syncAddrs of Right (syncO, syncP) -> do @@ -2619,6 +2562,7 @@ handleSplitAnalysis scope node dom pg = do emitTraceLabel @"address" "Synchronization Address" syncP return $ Just pg' Left{} -> return Nothing +-} handleDivergingPaths :: HasCallStack => @@ -2654,9 +2598,7 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi -- leave block exit as unhandled AdmitNonTotal -> return st' ChooseSyncPoint -> do - -- re-queuing for sync points happens at the toplevel pg1 <- chooseSyncPoint divergeNode pg - -- pg2 <- updateCombinedSyncPoint divergeNode pg1 return $ st'{ branchGraph = pg1 } -- handleDivergingPaths scope bundle currBlock (st'{ branchGraph = pg2 }) dom blkt ChooseDesyncPoint -> do From c95d70f49e0f560577f7c51b87fbec981312b3dc Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 15 May 2024 14:56:43 -0700 Subject: [PATCH 10/26] cherry-pick changes from dm/diverge-fix2 this now builds, and changes the control flow synchronization to occur as a first-class operation that is explicitly scheduled this provides some flexibility for handling additional cases for mismatched control flow, but this is still work in progress --- src/Data/Parameterized/PairF.hs | 6 + src/Data/Parameterized/SetF.hs | 8 + src/Pate/Binary.hs | 8 + src/Pate/PatchPair.hs | 42 ++-- src/Pate/Verification/PairGraph.hs | 268 ++++++++++++------------ src/Pate/Verification/StrongestPosts.hs | 78 +++---- src/Pate/Verification/Widening.hs | 48 +---- 7 files changed, 201 insertions(+), 257 deletions(-) diff --git a/src/Data/Parameterized/PairF.hs b/src/Data/Parameterized/PairF.hs index 92962ea4..f5d03ab1 100644 --- a/src/Data/Parameterized/PairF.hs +++ b/src/Data/Parameterized/PairF.hs @@ -37,6 +37,12 @@ instance (OrdF a, OrdF b) => OrdF (PairF a b) where compareF (PairF a1 b1) (PairF a2 b2) = lexCompareF a1 a2 $ compareF b1 b2 +instance (Eq (a tp), Eq (b tp)) => Eq ((PairF a b) tp) where + (PairF a1 b1) == (PairF a2 b2) = a1 == a2 && b1 == b2 + +instance (Ord (a tp), Ord (b tp)) => Ord ((PairF a b) tp) where + compare (PairF a1 b1) (PairF a2 b2) = compare a1 a2 <> compare b1 b2 + {-# COMPLETE TupleF2 #-} pattern TupleF3 :: a k -> b k -> c k -> TupleF '(a,b,c) k diff --git a/src/Data/Parameterized/SetF.hs b/src/Data/Parameterized/SetF.hs index d7d87723..950a1a26 100644 --- a/src/Data/Parameterized/SetF.hs +++ b/src/Data/Parameterized/SetF.hs @@ -44,6 +44,7 @@ module Data.Parameterized.SetF , unions , null , toSet + , fromSet , map , ppSetF ) where @@ -142,6 +143,13 @@ toSet :: (OrdF f, Ord (f tp)) => SetF f tp -> Set (f tp) toSet (SetF s) = unsafeCoerce s +-- | Convert a 'Set' to a 'SetF', under the assumption +-- that the 'OrdF' and 'Ord' instances are consistent. +-- This uses coercion rather than re-building the set, +-- which is sound given the above assumption. +fromSet :: (OrdF f, Ord (f tp)) => Set (f tp) -> SetF f tp +fromSet s = SetF (unsafeCoerce s) + map :: (OrdF g) => (f tp -> g tp) -> SetF f tp -> SetF g tp map f (SetF s) = SetF (S.map (\(AsOrd v) -> AsOrd (f v)) s) diff --git a/src/Pate/Binary.hs b/src/Pate/Binary.hs index 943f1e82..5b809bfb 100644 --- a/src/Pate/Binary.hs +++ b/src/Pate/Binary.hs @@ -29,6 +29,7 @@ module Pate.Binary , Patched , WhichBinaryRepr(..) , OtherBinary + , binCases , flipRepr , short) where @@ -60,6 +61,13 @@ flipRepr = \case OriginalRepr -> PatchedRepr PatchedRepr -> OriginalRepr +binCases :: WhichBinaryRepr bin1 -> WhichBinaryRepr bin2 -> Either (bin1 :~: bin2) ('(bin1, bin2) :~: '(OtherBinary bin2, OtherBinary bin1)) +binCases bin1 bin2 = case (bin1, bin2) of + (OriginalRepr, OriginalRepr) -> Left Refl + (OriginalRepr, PatchedRepr) -> Right Refl + (PatchedRepr, PatchedRepr) -> Left Refl + (PatchedRepr, OriginalRepr) -> Right Refl + short :: WhichBinaryRepr bin -> String short OriginalRepr = "O" short PatchedRepr = "P" diff --git a/src/Pate/PatchPair.hs b/src/Pate/PatchPair.hs index 536216dc..41a8b102 100644 --- a/src/Pate/PatchPair.hs +++ b/src/Pate/PatchPair.hs @@ -148,6 +148,22 @@ instance Eq f => Eq (WithBin f bin) where instance Ord f => Ord (WithBin f bin) where compare (WithBin _ f1) (WithBin _ f2) = compare f1 f2 +-- NB: not a Monoid because we don't have an empty value for <> +instance (forall bin. Semigroup (f bin)) => Semigroup (PatchPair f) where + p1 <> p2 = case (p1,p2) of + (PatchPair a1 b1, PatchPair a2 b2) -> PatchPair (a1 <> a2) (b1 <> b2) + (PatchPairSingle bin1 v1, PatchPair a2 b2) -> case bin1 of + PB.OriginalRepr -> PatchPair (v1 <> a2) b2 + PB.PatchedRepr -> PatchPair a2 (v1 <> b2) + (PatchPair a1 b1, PatchPairSingle bin2 v2) -> case bin2 of + PB.OriginalRepr -> PatchPair (a1 <> v2) b1 + PB.PatchedRepr -> PatchPair a1 (b1 <> v2) + (PatchPairSingle bin1 v1, PatchPairSingle bin2 v2) -> case (bin1, bin2) of + (PB.OriginalRepr, PB.PatchedRepr) -> PatchPair v1 v2 + (PB.OriginalRepr, PB.OriginalRepr) -> PatchPairSingle bin1 (v1 <> v2) + (PB.PatchedRepr, PB.OriginalRepr) -> PatchPair v2 v1 + (PB.PatchedRepr, PB.PatchedRepr) ->PatchPairSingle bin1 (v1 <> v2) + -- | Select the value from the 'PatchPair' according to the given 'PB.WhichBinaryRepr' -- Returns 'Nothing' if the given 'PatchPair' does not contain a value for the given binary -- (i.e. it is a singleton 'PatchPair' and the opposite binary repr is given) @@ -159,19 +175,6 @@ getPair repr pPair = case pPair of PatchPairSingle repr' a | Just Refl <- testEquality repr repr' -> Just a _ -> Nothing --- | Set the value in the given 'PatchPair' according to the given 'PB.WhichBinaryRepr' --- Returns 'Nothing' if the given 'PatchPair' does not contain a value for the given binary. --- (n.b. this will not convert a singleton 'PatchPair' into a full 'PatchPair') -setPair :: PB.WhichBinaryRepr bin -> (forall tp. PatchPair tp -> tp bin -> Maybe (PatchPair tp)) -setPair PB.OriginalRepr pPair a = case pPair of - PatchPair _ patched -> Just $ PatchPair a patched - PatchPairOriginal _ -> Just $ PatchPairOriginal a - PatchPairPatched _ -> Nothing -setPair PB.PatchedRepr pPair a = case pPair of - PatchPair orig _ -> Just $ PatchPair orig a - PatchPairPatched _ -> Just $ PatchPairPatched a - PatchPairOriginal _ -> Nothing - -- {-# DEPRECATED handleSingletonStub "Missing implementation for handling singleton PatchPair values" #-} handleSingletonStub :: HasCallStack => a handleSingletonStub = error "Missing implementation for handling singleton PatchPair values" @@ -246,11 +249,14 @@ fromMaybes = \case (Nothing, Nothing) -> throwPairErr - --- | Set the value in the given 'PatchPair' according to the given 'PB.WhichBinaryRepr' --- Raises 'pairErr' if the given 'PatchPair' does not contain a value for the given binary. -set :: HasCallStack => PatchPairM m => PB.WhichBinaryRepr bin -> (forall tp. PatchPair tp -> tp bin -> m (PatchPair tp)) -set repr pPair a = liftPairErr (setPair repr pPair a) +set :: PB.WhichBinaryRepr bin -> tp bin -> PatchPair tp -> PatchPair tp +set repr v pPair = case pPair of + PatchPair a b -> case repr of + PB.OriginalRepr -> PatchPair v b + PB.PatchedRepr -> PatchPair a v + PatchPairSingle repr' v' -> case PB.binCases repr' repr of + Left Refl -> PatchPairSingle repr v + Right Refl -> mkPair repr v v' data InconsistentPatchPairAccess = InconsistentPatchPairAccess deriving (Show) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 511cae08..0453c221 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -66,22 +66,24 @@ module Pate.Verification.PairGraph , dropReturns , dropPostDomains , markEdge - , getSyncPoints , getBackEdgesFrom , getCombinedSyncPoints , combineNodes , NodePriority(..) , addToWorkList - , WorkItem(FinalizeDivergence, ProcessNode) + , WorkItem(ProcessNode) , pattern ProcessMerge , workItemNode - , singleSidedReturns , getQueuedPriority , queueAncestors , queueNode , emptyWorkList - , SyncPoint(..) - , updateSyncPoint + , SyncPoint + , getSyncPoint + , modifySyncPoint + , syncMergeExitNodes + , syncCutAddresses + , syncExceptions , singleNodeRepr , edgeActions , nodeActions @@ -108,7 +110,6 @@ module Pate.Verification.PairGraph , propagateOnce , getPropagationKind , propagateAction - , getSyncAddresses , addSyncAddress -- , filterSyncExits , pairGraphComputeVerdict @@ -117,6 +118,8 @@ module Pate.Verification.PairGraph , handleSingleSidedReturnTo , filterSyncExits , isDivergeNode + , mkProcessMerge + , dropWorkItem ) where import Prettyprinter @@ -310,7 +313,6 @@ data WorkItem arch = | ProcessMergeCtor (SingleNodeEntry arch PBi.Original) (SingleNodeEntry arch PBi.Patched) - | FinalizeDivergence (GraphNode arch) deriving (Eq, Ord) -- Use mkProcessMerge as a partial smart constructor, but @@ -318,7 +320,7 @@ data WorkItem arch = pattern ProcessMerge :: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch pattern ProcessMerge sneO sneP <- ProcessMergeCtor sneO sneP -{-# COMPLETE ProcessNode, ProcessMerge, FinalizeDivergence #-} +{-# COMPLETE ProcessNode, ProcessMerge #-} -- TODO: After some refactoring I'm not sure if we actually need edge actions anymore, so this potentially can be simplified data ActionQueue sym arch = @@ -380,7 +382,7 @@ data SyncPoint arch = -- | During single-sided analysis, if we encounter an edge -- that ends in a cut point, we -- mark it here as a node that needs to be considered for merging - _syncMergeNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) + _syncMergeExitNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) -- | Instruction addresses that, if reached during single-sided -- analysis (from the corresponding diverge point), -- should trigger a merge back into a two-sided analysis @@ -389,18 +391,79 @@ data SyncPoint arch = -- In these cases, the single-sided analysis continues instead, with the intention -- that another sync point is encountered after additional instructions are executed , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch))) - -- | The single-sided nodes that were - -- introduced when a single-sided analysis of a function returned - -- exactly to a cut point. - , _syncReturnTargets :: PPa.PatchPair (SetF (SingleNodeEntry arch)) - } + + +instance Semigroup (SyncPoint arch) where + (SyncPoint a1 b1 c1) <> (SyncPoint a2 b2 c2) = (SyncPoint (a1 <> a2) (b1 <> b2) (c1 <> c2)) + + +instance Monoid (SyncPoint arch) where + mempty = SyncPoint + (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) + (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) + (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) + $(L.makeLenses ''SyncPoint) $(L.makeLenses ''ActionQueue) type ActionQueueLens sym arch k v = L.Lens' (ActionQueue sym arch) (Map k [PendingAction sym arch v]) +getSyncPoint :: + forall sym arch x bin. + HasCallStack => + (OrdF x, Ord (x bin)) => + L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + PairGraphM sym arch (Set (x bin)) +getSyncPoint lens bin nd = do + sp <- lookupPairGraph @sym pairGraphSyncPoints nd + let x = sp ^. lens + -- should be redundant, but no harm in checking + case PPa.get bin x of + Just x' -> return $ SetF.toSet x' + Nothing -> return Set.empty + +modifySyncPoint :: + forall sym arch x bin. + HasCallStack => + (OrdF x, Ord (x bin)) => + L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch -> + (Set (x bin) -> Set (x bin)) -> + PairGraphM sym arch () +modifySyncPoint lens bin dp f = do + msp <- tryPG $ lookupPairGraph pairGraphSyncPoints dp + let f' = \x -> SetF.fromSet (f (SetF.toSet x)) + let sp' = case msp of + Nothing -> mempty & lens .~ (PPa.mkSingle bin (f' SetF.empty)) + Just sp -> sp & lens %~ + (\x -> PPa.set bin (f' $ fromMaybe SetF.empty (PPa.get bin x)) x) + modify $ \pg -> + pg { pairGraphSyncPoints = Map.insert dp sp' (pairGraphSyncPoints pg)} + +addToSyncPoint :: + forall sym arch x bin. + (OrdF x, Ord (x bin)) => + HasCallStack => + L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + x bin -> + PairGraphM sym arch () +addToSyncPoint lens bin nd x = modifySyncPoint lens bin nd (Set.insert x) + +addSyncAddress :: + forall sym arch bin. + GraphNode arch {- ^ The divergent node -} -> + PBi.WhichBinaryRepr bin -> + PAd.ConcreteAddress arch -> + PairGraphM sym arch () +addSyncAddress nd bin syncAddr = addToSyncPoint syncCutAddresses bin nd (PPa.WithBin bin syncAddr) + -- | Combine two single-sided nodes into a 'WorkItem' to process their -- merge. Returns 'Nothing' if the two single-sided nodes have different -- divergence points. @@ -422,8 +485,6 @@ workItemNode = \case ProcessMerge sneO sneP -> case combineSingleEntries sneO sneP of Just merged -> GraphNode merged Nothing -> panic Verifier "workItemNode" ["Unexpected mismatched single-sided nodes"] - FinalizeDivergence dp -> dp - newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a } deriving (Functor @@ -716,8 +777,23 @@ queueAncestors priority nd pg = queueNode :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGraph sym arch queueNode priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) -queueWorkItem :: NodePriority -> GraphNode arch -> PairGraph sym arch -> PairGraph sym arch -queueWorkItem priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) +-- | Calls 'queueNode' for 'ProcessNode' work items. +-- For 'ProcessMerge' work items, queues up the merge if +-- there exist domains for both single-sided nodes. +-- Otherwise, queues up the single-sided nodes with missing domains. +queueWorkItem :: NodePriority -> WorkItem arch -> PairGraph sym arch -> PairGraph sym arch +queueWorkItem priority wi pg = case wi of + ProcessNode nd -> queueNode priority nd pg + ProcessMerge sneO sneP -> + let + neO = GraphNode (singleToNodeEntry sneO) + neP = GraphNode (singleToNodeEntry sneP) + in case (getCurrentDomain pg neO, getCurrentDomain pg neP) of + (Just{},Just{}) -> addItemToWorkList wi priority pg + (Just{}, Nothing) -> queueNode priority neP pg + (Nothing, Just{}) -> queueNode priority neO pg + (Nothing, Nothing) -> + queueNode priority neP (queueNode priority neO pg) -- | Adds a node to the work list. If it doesn't have a domain, queue its ancestors. @@ -1013,37 +1089,6 @@ pgMaybe :: String -> Maybe a -> PairGraphM sym arch a pgMaybe _ (Just a) = return a pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg -getSyncPoints :: - forall sym arch bin. - HasCallStack => - PBi.WhichBinaryRepr bin -> - GraphNode arch -> - PairGraphM sym arch (Set (SingleNodeEntry arch bin)) -getSyncPoints bin nd = do - (SyncPoint syncPair _ _ _) <- lookupPairGraph @sym pairGraphSyncPoints nd - SetF.toSet <$> PPa.get bin syncPair - -getSyncAddresses :: - forall sym arch bin. - HasCallStack => - PBi.WhichBinaryRepr bin -> - GraphNode arch -> - PairGraphM sym arch (Set (PAd.ConcreteAddress arch)) -getSyncAddresses bin nd = fmap (fromMaybe Set.empty) $ tryPG $ do - (SyncPoint _ addrPair _ _) <- lookupPairGraph @sym pairGraphSyncPoints nd - (Set.map PPa.withBinValue . SetF.toSet) <$> PPa.get bin addrPair - -updateSyncPoint :: - forall sym arch. - GraphNode arch -> - (SyncPoint arch -> SyncPoint arch) -> - PairGraphM sym arch () -updateSyncPoint nd f = do - dp <- pgMaybe "missing diverge point" $ getDivergePoint nd - sp <- lookupPairGraph pairGraphSyncPoints dp - modify $ \pg -> - pg { pairGraphSyncPoints = Map.insert dp (f sp) (pairGraphSyncPoints pg)} - -- | Returns all discovered merge points from the given diverge point getCombinedSyncPoints :: forall sym arch. @@ -1051,7 +1096,7 @@ getCombinedSyncPoints :: GraphNode arch -> PairGraphM sym arch ([((SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched), GraphNode arch)], SyncPoint arch) getCombinedSyncPoints ndDiv = do - sync@(SyncPoint syncSet _ _ _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv + sync@(SyncPoint syncSet _ _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv case syncSet of PPa.PatchPair ndsO ndsP -> do all_pairs <- forM (Set.toList $ Set.cartesianProduct (SetF.toSet ndsO) (SetF.toSet ndsP)) $ \(ndO, ndP) -> do @@ -1084,17 +1129,6 @@ singleNodeRepr nd = case graphNodeBlocks nd of tryPG :: PairGraphM sym arch a -> PairGraphM sym arch (Maybe a) tryPG f = catchError (Just <$> f) (\_ -> return Nothing) -getSyncPoint :: - forall sym arch x bin. - HasCallStack => - L.Lens' (SyncPoint arch) (PPa.PatchPair x) -> - PBi.WhichBinaryRepr bin -> - GraphNode arch {- ^ The divergent node -} -> - PairGraphM sym arch (x bin) -getSyncPoint lens bin nd = do - sp <- lookupPairGraph @sym pairGraphSyncPoints nd - let x = sp ^. lens - PPa.get bin x -- | Retrive the 'SyncPoint' fields corresponding to -- the divergence point of the given single-sided node @@ -1113,41 +1147,7 @@ getSingleNodeSync lens sne = do v2 <- PPa.get (PBi.flipRepr bin) x return (v1, v2) --- | Initialize an empty sync point entry for the given node, if --- one doesn't already exist -initSyncPoint :: GraphNode arch -> PairGraphM sym arch () -initSyncPoint nd = do - pg <- get - case Map.member nd (pairGraphSyncPoints pg) of - True -> return () - False -> do - let sp = SyncPoint (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) (PPa.PatchPair SetF.empty SetF.empty) - modify $ \pg_ -> pg_{ pairGraphSyncPoints = Map.insert nd sp (pairGraphSyncPoints pg) } -addToSyncPoint :: - forall sym arch x bin. - OrdF x => - HasCallStack => - L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> - PBi.WhichBinaryRepr bin -> - GraphNode arch {- ^ The divergent node -} -> - x bin -> - PairGraphM sym arch () -addToSyncPoint lens bin nd x = do - initSyncPoint nd - sp <- lookupPairGraph @sym pairGraphSyncPoints nd - let sp' = sp & lens %~ PPa.insertWith bin (SetF.singleton x) SetF.union - -- make sure the other side has an empty set so that 'getSyncPoint' always succeeds - let sp'' = sp' & lens %~ PPa.insertWith (PBi.flipRepr bin) SetF.empty SetF.union - modify $ \pg -> pg{ pairGraphSyncPoints = Map.insert nd sp'' (pairGraphSyncPoints pg) } - -addSyncAddress :: - forall sym arch bin. - GraphNode arch {- ^ The divergent node -} -> - PBi.WhichBinaryRepr bin -> - PAd.ConcreteAddress arch -> - PairGraphM sym arch () -addSyncAddress nd bin syncAddr = addToSyncPoint syncCutAddresses bin nd (PPa.WithBin bin syncAddr) -- | Add a node back to the worklist to be re-analyzed if there is -- an existing abstract domain for it. Otherwise return Nothing. @@ -1168,6 +1168,14 @@ addItemToWorkList :: PairGraph sym arch addItemToWorkList wi priority gr = gr { pairGraphWorklist = RevMap.insertWith (min) wi priority (pairGraphWorklist gr) } +-- | Drop a work item. Should only be used in cases where we are certain +-- the work item is going to be handled after it is dropped. +dropWorkItem :: + WorkItem arch -> + PairGraph sym arch -> + PairGraph sym arch +dropWorkItem wi gr = gr { pairGraphWorklist = RevMap.delete wi (pairGraphWorklist gr) } + -- | Return the priority of the given 'GraphNode' if it is queued for -- normal processing getQueuedPriority :: @@ -1301,33 +1309,13 @@ isSyncExit sne blkt@(PB.BlockTarget{}) = do let bin = singleEntryBin sne cuts <- getSyncPoint syncCutAddresses bin dp excepts <- getSyncPoint syncExceptions bin dp - let isExcept = SetF.member (TupleF2 sne blkt) excepts + let isExcept = Set.member (TupleF2 sne blkt) excepts case (not isExcept) && - SetF.member (PPa.WithBin bin (PB.targetRawPC blkt)) cuts of + Set.member (PPa.WithBin bin (PB.targetRawPC blkt)) cuts of True -> return $ Just (PB.targetCall blkt) False -> return Nothing isSyncExit _ _ = return Nothing --- | Get all possible merge targets from the given node --- (i.e. all merge nodes for diverge point of the given --- entry) -otherMergeNodes :: - SingleNodeEntry arch bin -> - PairGraphM sym arch [SingleNodeEntry arch (PBi.OtherBinary bin)] -otherMergeNodes sne = do - let bin = singleEntryBin sne - let dp = singleNodeDivergePoint sne - merges <- getSyncPoint syncMergeNodes (PBi.flipRepr bin) dp - return $ SetF.toList merges - - -singleSidedReturns :: - GraphNode arch -> - PairGraphM sym arch [(SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched)] -singleSidedReturns nd = do - retsO <- getSyncPoint syncReturnTargets PBi.OriginalRepr nd - retsP <- getSyncPoint syncReturnTargets PBi.PatchedRepr nd - return $ [ (retO,retP) | retO <- SetF.toList retsO, retP <- SetF.toList retsP ] -- | Filter a list of reachable block exits to -- only those that should be handled for the given 'WorkItem' @@ -1337,13 +1325,12 @@ singleSidedReturns nd = do -- possible merge nodes from the other side of the analysis and -- queued as a 'ProcessMerge' work item. filterSyncExits :: - (NodePriorityK -> NodePriority) -> {- ^ priority to queue new work items at -} + (NodePriorityK -> NodePriority) -> WorkItem arch -> [PPa.PatchPair (PB.BlockTarget arch)] -> PairGraphM sym arch [PPa.PatchPair (PB.BlockTarget arch)] -filterSyncExits _priority (FinalizeDivergence{}) _ = fail "Unexpected FinalizeDivergence work item" -filterSyncExits _priority (ProcessNode (ReturnNode{})) _ = fail "Unexpected ReturnNode work item" -filterSyncExits _priority (ProcessMerge sneO sneP) blktPairs = do +filterSyncExits _ (ProcessNode (ReturnNode{})) _ = fail "Unexpected ReturnNode work item" +filterSyncExits _ (ProcessMerge sneO sneP) blktPairs = do let isSyncExitPair blktPair = do blktO <- PPa.get PBi.OriginalRepr blktPair blktP <- PPa.get PBi.PatchedRepr blktPair @@ -1358,26 +1345,30 @@ filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleN let bin = singleEntryBin sne blkts <- mapM (PPa.get bin) blktPairs exitBlks <- catMaybes <$> mapM (isSyncExit sne) blkts - forM_ exitBlks $ \blk -> do - let nextNode = mkSingleNodeEntry ne blk - addToSyncPoint syncReturnTargets bin dp nextNode unless (null exitBlks) $ do -- if any of the exits from this node are sync exits, -- then we need to queue up processing this node as -- a merge against all known merge points - addToSyncPoint syncMergeNodes bin dp sne - -- make sure that the divergence itself is finalized after all - -- other processing is done - modify $ addItemToWorkList (FinalizeDivergence dp) (priority PriorityFinalizeDivergence) + addToSyncPoint syncMergeExitNodes bin dp sne + queueMerges priority sne return blktPairs --- | For a given return -> entry transition, return a list of --- entry nodes for all possible ways that control flow could --- re-sync at the entry. i.e. if the given entry point is single-sided --- but a sync address, then pair it with all possible merge nodes --- from the other binary for the divergence point. +queueMerges :: + (NodePriorityK -> NodePriority) -> + SingleNodeEntry arch bin -> + PairGraphM sym arch () +queueMerges priority sne = do + let dp = singleNodeDivergePoint sne + otherExits <- getSyncPoint syncMergeExitNodes (PBi.flipRepr (singleEntryBin sne)) dp + forM_ otherExits $ \otherExit -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge sne otherExit + modify $ queueWorkItem (priority PriorityHandleMerge) wi + +-- | This handles the special case where the sync point +-- is the return site for a function. +-- This will be handled specially handleSingleSidedReturnTo :: - (NodePriorityK -> NodePriority) -> {- ^ priority to queue new work items at -} + (NodePriorityK -> NodePriority) -> NodeEntry arch -> PairGraphM sym arch () handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of @@ -1386,10 +1377,9 @@ handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of let dp = singleNodeDivergePoint sne syncAddrs <- getSyncPoint syncCutAddresses bin dp let blk = singleNodeBlock sne - case SetF.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of + case Set.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of True -> do - addToSyncPoint syncReturnTargets bin dp sne - -- need to re-check this as part of finalization - modify $ addItemToWorkList (FinalizeDivergence dp) (priority PriorityFinalizeDivergence) + addToSyncPoint syncMergeExitNodes bin dp sne + queueMerges priority sne False -> return () - Nothing -> return () + Nothing -> return () \ No newline at end of file diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 0d00becc..a9631ea4 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -557,44 +557,42 @@ addImmediateEqDomRefinementChoice nd preD gr0 = do choice ("No refinements") () $ return gr1 mapM_ go [minBound..maxBound] -{- + initSingleSidedDomain :: GraphNode arch -> - WhichBinaryRepr bin -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -initSingleSidedDomain nd bin pg = do +initSingleSidedDomain nd pg0 = withPG_ pg0 $ do + priority <- lift $ thisPriority + let bin = PBi.OriginalRepr nd_single <- toSingleGraphNode bin nd - case getCurrentDomain nd pg of - Just dom_spec -> do - - case getCurrentDomain nd_single pg of - Just{} -> return pg - Nothing -> do --} + dom_spec <- liftPG $ getCurrentDomainM nd + PS.forSpec dom_spec $ \scope dom -> do + case getCurrentDomain pg0 nd_single of + Just{} -> return () + Nothing -> do + dom_single <- PAD.singletonDomain bin dom + let dom_single_spec = PS.mkSimSpec scope dom_single + liftPG $ modify $ \pg -> initDomain pg nd nd_single (priority PriorityHandleDesync) dom_single_spec + bundle <- lift $ noopBundle scope (graphNodeBlocks nd) + liftEqM_ $ \pg -> widenAlongEdge scope bundle nd dom pg nd_single + return (PS.WithScope ()) workItemDomainSpec :: WorkItem arch -> PairGraph sym arch -> EquivM sym arch (Maybe (GraphNode arch, PAD.AbstractDomainSpec sym arch), PairGraph sym arch) workItemDomainSpec wi pg = withPG pg $ case wi of - FinalizeDivergence dp -> do - snePairs <- liftPG $ singleSidedReturns dp - forM_ snePairs $ \(sneO, sneP) -> do - void $ liftEqM $ mergeSingletons sneO sneP - return Nothing ProcessNode nd -> do - dom_spec <- liftPG $ getCurrentDomainM nd case isDivergeNode nd pg of True -> do - priority <- lift $ thisPriority - divergeNodeO <- toSingleGraphNode PBi.OriginalRepr nd - case getCurrentDomain pg divergeNodeO of - Just{} -> liftPG $ modify $ queueNode (priority PriorityHandleDesync) divergeNodeO - Nothing -> error "TODO" - False -> error "TODO" - - return $ Just (nd, dom_spec) + liftEqM_ $ initSingleSidedDomain nd + -- single-sided node has been queued, so we skip + -- any further analysis here + return Nothing + False -> do + dom <- liftPG $ getCurrentDomainM nd + return $ Just (nd, dom) ProcessMerge sneO sneP -> do let ndO = GraphNode $ singleToNodeEntry sneO @@ -611,7 +609,7 @@ workItemDomainSpec wi pg = withPG pg $ case wi of syncNode <- liftEqM $ mergeSingletons sneO sneP dom_spec <- liftPG $ getCurrentDomainM (GraphNode syncNode) return $ Just (GraphNode syncNode, dom_spec) - (Just ndO_dom_spec, Nothing) -> do + (Just{}, Nothing) -> do divergeNodeP <- toSingleGraphNode PBi.PatchedRepr divergeNode _ <- PS.forSpec diverge_dom_spec $ \scope diverge_dom -> do diverge_domP <- lift $ PAD.singletonDomain PBi.PatchedRepr diverge_dom @@ -619,6 +617,8 @@ workItemDomainSpec wi pg = withPG pg $ case wi of -- if the current domain for the patched variant of the diverge node -- doesn't exist, then we initialize it as the "singletonDomain" -- otherwise we leave it unmodified, as it's potentially been widened + -- any updates that propagate from before this divergence will eventually + -- be propagated here via the Original single-sided analysis liftPG $ (void $ getCurrentDomainM divergeNodeP) <|> (modify $ \pg_ -> updateDomain' pg_ ndO divergeNodeP (PS.mkSimSpec scope diverge_domP) (priority PriorityWidening)) liftEqM_ $ \pg_ -> withPredomain scope bundle diverge_domP $ withConditionsAssumed scope bundle diverge_dom divergeNode pg_ $ @@ -664,34 +664,6 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do widenAlongEdge scope bundle ndP dom pg (GraphNode syncNode) return (syncNode, pg1) - -mergeDualNodes :: - SingleNodeEntry arch PBi.Original {- ^ original program node -} -> - SingleNodeEntry arch PBi.Patched {- ^ patched program node -} -> - PAD.AbstractDomainSpec sym arch {- ^ original node domain -} -> - PAD.AbstractDomainSpec sym arch {- ^ patched node domain -} -> - GraphNode arch {- ^ combined sync node -} -> - PairGraph sym arch -> - EquivM sym arch (PairGraph sym arch) -mergeDualNodes in1_single in2_single spec1 spec2 syncNode gr0 = fnTrace "mergeDualNodes" $ withSym $ \sym -> do - let gr2 = gr0 - let in1 = GraphNode $ singleToNodeEntry in1_single - let in2 = GraphNode $ singleToNodeEntry in2_single - - let blkPair1 = graphNodeBlocks in1 - let blkPair2 = graphNodeBlocks in2 - - fmap (\x -> PS.viewSpecBody x PS.unWS) $ withFreshScope (graphNodeBlocks syncNode) $ \scope -> fmap PS.WithScope $ - withValidInit scope blkPair1 $ withValidInit scope blkPair2 $ do - (_, dom1) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) spec1 - (_, dom2) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) spec2 - dom <- PAD.zipSingletonDomains sym dom1 dom2 - bundle <- noopBundle scope (graphNodeBlocks syncNode) - withPredomain scope bundle dom $ withConditionsAssumed scope bundle dom2 in2 gr2 $ do - withTracing @"node" in2 $ do - emitTraceLabel @"domain" PAD.Predomain (Some dom) - widenAlongEdge scope bundle in2 dom gr2 syncNode - -- | Choose some work item (optionally interactively) withWorkItem :: PA.ValidArch arch => diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index d55d3998..f22ec509 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -599,52 +599,6 @@ domainToEquivCondition scope bundle preD postD refine = withSym $ \sym -> do False -> return $ W4.truePred sym True -> return eqPred -{- --- | After widening an edge, insert an equivalence condition --- into the pairgraph for candidate functions -initializeCondition :: - PS.SimScope sym arch v -> - SimBundle sym arch v -> - AbstractDomain sym arch v {- ^ incoming source predomain -} -> - AbstractDomain sym arch v {- ^ resulting target postdomain -} -> - GraphNode arch {- ^ from -} -> - GraphNode arch {- ^ to -} -> - PairGraph sym arch -> - EquivM sym arch (PairGraph sym arch) -initializeCondition scope bundle preD postD from to gr = do - let edge = (from,to) - addLazyAction edge gr "Post-process equivalence domain?" $ \choice -> - choice "Refine and generate equivalence condition" (\x y -> refineEqDomainForEdge edge x y) - - - eqCondFns <- CMR.asks envEqCondFns - (mlocFilter, gr1) <- if - | Just sync <- asSyncPoint gr to -> case syncTerminal sync of - Just True -> do - locFilter <- refineEquivalenceDomain postD - return (Just locFilter, gr) - Just False -> return (Nothing, gr) - Nothing -> do - emitTraceLabel @"domain" PAD.ExternalPostDomain (Some postD) - chooseBool "Continue analysis after resynchronization?" >>= \case - True -> return (Nothing, updateSyncPoint gr to (\sync' -> sync'{syncTerminal = Just False})) - False -> do - locFilter <- refineEquivalenceDomain postD - return (Just locFilter, updateSyncPoint gr to (\sync' -> sync'{syncTerminal = Just True})) - | ReturnNode ret <- to - , Just locFilter <- Map.lookup (nodeFuns ret) eqCondFns -> - return $ (Just locFilter, gr) - | otherwise -> return (Nothing, gr) - case mlocFilter of - Just locFilter -> do - eqCond <- computeEquivCondition scope bundle preD postD (\l -> locFilter (PL.SomeLocation l)) - pathCond <- CMR.asks envPathCondition >>= PAs.toPred sym - eqCond' <- PEC.mux sym pathCond eqCond (PEC.universal sym) - let gr2 = setEquivCondition to (PS.mkSimSpec scope eqCond') gr1 - return $ dropDomain to (markEdge from to gr2) - Nothing -> return gr1 --} - data PickManyChoice sym arch = forall tp. PickRegister (MM.ArchReg arch tp) | forall w. PickStack (PMc.MemCell sym arch w) @@ -1676,7 +1630,7 @@ dropValueLoc wb loc postD = do PL.Unit -> vals _ -> error "unsupported location" locs = WidenLocs (Set.singleton (PL.SomeLocation loc)) - vals' <- PPa.set wb (PAD.absDomVals postD) v + let vals' = PPa.set wb v (PAD.absDomVals postD) return $ Widen WidenValue locs (postD { PAD.absDomVals = vals' }) widenCells :: From fe6c108434cf500345b3aed983e9fcb6465340e6 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 17 May 2024 14:15:24 -0700 Subject: [PATCH 11/26] distinguish entry vs. exit sync points so they can be appropriately merged --- src/Pate/Binary.hs | 14 +- src/Pate/Monad/Environment.hs | 5 - src/Pate/Verification/PairGraph.hs | 242 ++++++++++++++---------- src/Pate/Verification/PairGraph/Node.hs | 1 - 4 files changed, 147 insertions(+), 115 deletions(-) diff --git a/src/Pate/Binary.hs b/src/Pate/Binary.hs index 5b809bfb..1f03307c 100644 --- a/src/Pate/Binary.hs +++ b/src/Pate/Binary.hs @@ -31,7 +31,9 @@ module Pate.Binary , OtherBinary , binCases , flipRepr - , short) + , short + , otherInvolutive + ) where import Data.Parameterized.WithRepr @@ -51,10 +53,14 @@ data WhichBinaryRepr (bin :: WhichBinary) where OriginalRepr :: WhichBinaryRepr 'Original PatchedRepr :: WhichBinaryRepr 'Patched -type family OtherBinary (bin :: WhichBinary) :: WhichBinary +type family OtherBinary (bin :: WhichBinary) :: WhichBinary where + OtherBinary Original = Patched + OtherBinary Patched = Original -type instance OtherBinary Original = Patched -type instance OtherBinary Patched = Original +otherInvolutive :: WhichBinaryRepr bin -> (OtherBinary (OtherBinary bin) :~: bin) +otherInvolutive bin = case binCases bin (flipRepr bin) of + Left Refl -> Refl + Right Refl -> Refl flipRepr :: WhichBinaryRepr bin -> WhichBinaryRepr (OtherBinary bin) flipRepr = \case diff --git a/src/Pate/Monad/Environment.hs b/src/Pate/Monad/Environment.hs index e8ef0d4e..022f7d39 100644 --- a/src/Pate/Monad/Environment.hs +++ b/src/Pate/Monad/Environment.hs @@ -135,7 +135,6 @@ data NodePriorityK = | PriorityDomainRefresh | PriorityHandleReturn | PriorityHandleMerge - | PriorityFinalizeDivergence | PriorityMiscCleanup | PriorityDeferred deriving (Eq, Ord) @@ -158,10 +157,6 @@ printPriorityKind (NodePriority pk _ _ ) = case pk of PriorityHandleMerge -> "Handling Control Flow Merge" PriorityMiscCleanup -> "Proof Cleanup" PriorityDeferred -> "Handling Deferred Decisions" - -- this should be lowest priority since we want to defer this - -- until any other analysis is complete - PriorityFinalizeDivergence -> "Finalizing Control Flow Divergence" - instance IsTraceNode k "priority" where type TraceNodeType k "priority" = NodePriority diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 0453c221..4401cad7 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -19,6 +19,7 @@ {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE ViewPatterns #-} module Pate.Verification.PairGraph ( Gas(..) @@ -67,7 +68,6 @@ module Pate.Verification.PairGraph , dropPostDomains , markEdge , getBackEdgesFrom - , getCombinedSyncPoints , combineNodes , NodePriority(..) , addToWorkList @@ -78,10 +78,11 @@ module Pate.Verification.PairGraph , queueAncestors , queueNode , emptyWorkList - , SyncPoint - , getSyncPoint - , modifySyncPoint - , syncMergeExitNodes + , SyncData + , SyncPoint(..) + , getSyncData + , modifySyncData + , syncPoints , syncCutAddresses , syncExceptions , singleNodeRepr @@ -296,7 +297,7 @@ data PairGraph sym arch = -- | Mapping from singleton nodes to their "synchronization" point, representing -- the case where two independent program analysis steps have occurred and now -- their control-flows have re-synchronized - , pairGraphSyncPoints :: !(Map (GraphNode arch) (SyncPoint arch)) + , pairGraphSyncData :: !(Map (GraphNode arch) (SyncData arch)) , pairGraphPendingActs :: ActionQueue sym arch , pairGraphDomainRefinements :: !(Map (GraphNode arch) [DomainRefinement sym arch]) @@ -310,16 +311,32 @@ data WorkItem arch = -- | Handle all normal node processing logic ProcessNode (GraphNode arch) -- | Handle merging two single-sided analyses (both nodes must share a diverge point) - | ProcessMergeCtor + | ProcessMergeAtExitsCtor + (SingleNodeEntry arch PBi.Original) + (SingleNodeEntry arch PBi.Patched) + | ProcessMergeAtEntryCtor (SingleNodeEntry arch PBi.Original) (SingleNodeEntry arch PBi.Patched) deriving (Eq, Ord) +processMergeSinglePair :: WorkItem arch -> Maybe (SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched) +processMergeSinglePair wi = case wi of + ProcessMergeAtExits sne1 sne2 -> Just (sne1,sne2) + ProcessMergeAtEntry sne1 sne2 -> Just (sne1, sne2) + ProcessNode{} -> Nothing + -- Use mkProcessMerge as a partial smart constructor, but -- export this pattern so we can match on it -pattern ProcessMerge :: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch -pattern ProcessMerge sneO sneP <- ProcessMergeCtor sneO sneP +pattern ProcessMergeAtExits :: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch +pattern ProcessMergeAtExits sneO sneP <- ProcessMergeAtExitsCtor sneO sneP +pattern ProcessMergeAtEntry :: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch +pattern ProcessMergeAtEntry sneO sneP <- ProcessMergeAtEntryCtor sneO sneP + +pattern ProcessMerge:: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch +pattern ProcessMerge sneO sneP <- (processMergeSinglePair -> Just (sneO, sneP)) + +{-# COMPLETE ProcessNode, ProcessMergeAtExits, ProcessMergeAtEntry #-} {-# COMPLETE ProcessNode, ProcessMerge #-} -- TODO: After some refactoring I'm not sure if we actually need edge actions anymore, so this potentially can be simplified @@ -376,13 +393,13 @@ data PropagateKind = -- of Original sync point vs. every Patched sync point -- In practice this is still reasonably small, since there are usually -- only 2-3 cut addresses on each side (i.e. 4-9 merge cases to consider) -data SyncPoint arch = - SyncPoint +data SyncData arch = + SyncData { -- | During single-sided analysis, if we encounter an edge -- that ends in a cut point, we -- mark it here as a node that needs to be considered for merging - _syncMergeExitNodes :: PPa.PatchPair (SetF (SingleNodeEntry arch)) + _syncPoints :: PPa.PatchPair (SetF (SyncPoint arch)) -- | Instruction addresses that, if reached during single-sided -- analysis (from the corresponding diverge point), -- should trigger a merge back into a two-sided analysis @@ -393,68 +410,93 @@ data SyncPoint arch = , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch))) } +data SyncPoint arch bin = + SyncAtExits { syncPointNode :: SingleNodeEntry arch bin , _syncPointExits :: Set (SingleNodeEntry arch bin) } + | SyncAtStart { syncPointNode :: SingleNodeEntry arch bin } + deriving (Eq, Ord) +syncPointBin :: SyncPoint arch bin -> PBi.WhichBinaryRepr bin +syncPointBin sp = singleEntryBin $ syncPointNode sp -instance Semigroup (SyncPoint arch) where - (SyncPoint a1 b1 c1) <> (SyncPoint a2 b2 c2) = (SyncPoint (a1 <> a2) (b1 <> b2) (c1 <> c2)) +instance TestEquality (SyncPoint arch) where + testEquality e1 e2 = testEquality (syncPointNode e1) (syncPointNode e2) +instance OrdF (SyncPoint arch) where + compareF sp1 sp2 = lexCompareF (syncPointBin sp1) (syncPointBin sp2) $ + fromOrdering (compare sp1 sp2) -instance Monoid (SyncPoint arch) where - mempty = SyncPoint +instance Semigroup (SyncData arch) where + (SyncData a1 b1 c1) <> (SyncData a2 b2 c2) = (SyncData (a1 <> a2) (b1 <> b2) (c1 <> c2)) + + +instance Monoid (SyncData arch) where + mempty = SyncData (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) -$(L.makeLenses ''SyncPoint) +$(L.makeLenses ''SyncData) $(L.makeLenses ''ActionQueue) type ActionQueueLens sym arch k v = L.Lens' (ActionQueue sym arch) (Map k [PendingAction sym arch v]) -getSyncPoint :: +getSyncData :: forall sym arch x bin. HasCallStack => (OrdF x, Ord (x bin)) => - L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> PBi.WhichBinaryRepr bin -> GraphNode arch {- ^ The divergent node -} -> PairGraphM sym arch (Set (x bin)) -getSyncPoint lens bin nd = do - sp <- lookupPairGraph @sym pairGraphSyncPoints nd +getSyncData lens bin nd = do + sp <- lookupPairGraph @sym pairGraphSyncData nd let x = sp ^. lens -- should be redundant, but no harm in checking case PPa.get bin x of Just x' -> return $ SetF.toSet x' Nothing -> return Set.empty -modifySyncPoint :: +getSingleNodeData :: + forall sym arch x bin. + HasCallStack => + (OrdF x, Ord (x bin)) => + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> + SingleNodeEntry arch bin -> + PairGraphM sym arch (Set (x bin)) +getSingleNodeData lens sne = do + let dp = singleNodeDivergePoint sne + let bin = singleEntryBin sne + getSyncData lens bin dp + +modifySyncData :: forall sym arch x bin. HasCallStack => (OrdF x, Ord (x bin)) => - L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> PBi.WhichBinaryRepr bin -> GraphNode arch -> (Set (x bin) -> Set (x bin)) -> PairGraphM sym arch () -modifySyncPoint lens bin dp f = do - msp <- tryPG $ lookupPairGraph pairGraphSyncPoints dp +modifySyncData lens bin dp f = do + msp <- tryPG $ lookupPairGraph pairGraphSyncData dp let f' = \x -> SetF.fromSet (f (SetF.toSet x)) let sp' = case msp of Nothing -> mempty & lens .~ (PPa.mkSingle bin (f' SetF.empty)) Just sp -> sp & lens %~ (\x -> PPa.set bin (f' $ fromMaybe SetF.empty (PPa.get bin x)) x) modify $ \pg -> - pg { pairGraphSyncPoints = Map.insert dp sp' (pairGraphSyncPoints pg)} + pg { pairGraphSyncData = Map.insert dp sp' (pairGraphSyncData pg)} -addToSyncPoint :: +addToSyncData :: forall sym arch x bin. (OrdF x, Ord (x bin)) => HasCallStack => - L.Lens' (SyncPoint arch) (PPa.PatchPair (SetF x)) -> + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> PBi.WhichBinaryRepr bin -> GraphNode arch {- ^ The divergent node -} -> x bin -> PairGraphM sym arch () -addToSyncPoint lens bin nd x = modifySyncPoint lens bin nd (Set.insert x) +addToSyncData lens bin nd x = modifySyncData lens bin nd (Set.insert x) addSyncAddress :: forall sym arch bin. @@ -462,27 +504,32 @@ addSyncAddress :: PBi.WhichBinaryRepr bin -> PAd.ConcreteAddress arch -> PairGraphM sym arch () -addSyncAddress nd bin syncAddr = addToSyncPoint syncCutAddresses bin nd (PPa.WithBin bin syncAddr) +addSyncAddress nd bin syncAddr = addToSyncData syncCutAddresses bin nd (PPa.WithBin bin syncAddr) -- | Combine two single-sided nodes into a 'WorkItem' to process their -- merge. Returns 'Nothing' if the two single-sided nodes have different -- divergence points. -mkProcessMerge :: +mkProcessMerge :: + Bool -> SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (WorkItem arch) -mkProcessMerge sne1 sne2 +mkProcessMerge syncAtExits sne1 sne2 | dp1 <- singleNodeDivergePoint sne1 , dp2 <- singleNodeDivergePoint sne2 , dp1 == dp2 = case singleEntryBin sne1 of - PBi.OriginalRepr -> Just $ ProcessMergeCtor sne1 sne2 - PBi.PatchedRepr -> Just $ ProcessMergeCtor sne2 sne1 -mkProcessMerge _ _ = Nothing + PBi.OriginalRepr -> case syncAtExits of + True -> Just $ ProcessMergeAtExitsCtor sne1 sne2 + False -> Just $ ProcessMergeAtEntryCtor sne1 sne2 + PBi.PatchedRepr -> case syncAtExits of + True -> Just $ ProcessMergeAtExitsCtor sne2 sne1 + False -> Just $ ProcessMergeAtEntryCtor sne2 sne1 +mkProcessMerge _ _ _ = Nothing workItemNode :: WorkItem arch -> GraphNode arch workItemNode = \case ProcessNode nd -> nd - ProcessMerge sneO sneP -> case combineSingleEntries sneO sneP of + ProcessMerge spO spP -> case combineSingleEntries spO spP of Just merged -> GraphNode merged Nothing -> panic Verifier "workItemNode" ["Unexpected mismatched single-sided nodes"] @@ -640,7 +687,7 @@ emptyPairGraph = , pairGraphConditions = mempty , pairGraphEdges = mempty , pairGraphBackEdges = mempty - , pairGraphSyncPoints = mempty + , pairGraphSyncData = mempty , pairGraphPendingActs = ActionQueue Map.empty Map.empty Map.empty Map.empty 0 , pairGraphDomainRefinements = mempty } @@ -784,10 +831,10 @@ queueNode priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) queueWorkItem :: NodePriority -> WorkItem arch -> PairGraph sym arch -> PairGraph sym arch queueWorkItem priority wi pg = case wi of ProcessNode nd -> queueNode priority nd pg - ProcessMerge sneO sneP -> + ProcessMerge spO spP -> let - neO = GraphNode (singleToNodeEntry sneO) - neP = GraphNode (singleToNodeEntry sneP) + neO = GraphNode (singleToNodeEntry spO) + neP = GraphNode (singleToNodeEntry spP) in case (getCurrentDomain pg neO, getCurrentDomain pg neP) of (Just{},Just{}) -> addItemToWorkList wi priority pg (Just{}, Nothing) -> queueNode priority neP pg @@ -946,7 +993,7 @@ hasWorkLeft pg = case RevMap.minView_value (pairGraphWorklist pg) of isDivergeNode :: GraphNode arch -> PairGraph sym arch -> Bool -isDivergeNode nd pg = Map.member nd (pairGraphSyncPoints pg) +isDivergeNode nd pg = Map.member nd (pairGraphSyncData pg) -- | Given a pair graph, chose the next node in the graph to visit -- from the work list, updating the necessary bookeeping. If the @@ -973,11 +1020,11 @@ chooseWorkItem' = do ProcessNode (GraphNode ne) | Just (Some sne) <- asSingleNodeEntry ne -> do let bin = singleEntryBin sne let sne_addr = PB.concreteAddress $ singleNodeBlock sne - (exceptEdges, _) <- getSingleNodeSync syncExceptions sne - (cutAddrs, _) <- getSingleNodeSync syncCutAddresses sne - let isCutAddr = SetF.member (PPa.WithBin bin sne_addr) cutAddrs - let excepts = SetF.map (\(TupleF2 sne_ _) -> sne_) exceptEdges - let isExcepted = SetF.member sne excepts + exceptEdges <- getSingleNodeData syncExceptions sne + cutAddrs <- getSingleNodeData syncCutAddresses sne + let isCutAddr = Set.member (PPa.WithBin bin sne_addr) cutAddrs + let excepts = Set.map (\(TupleF2 sne_ _) -> sne_) exceptEdges + let isExcepted = Set.member sne excepts case (isCutAddr, isExcepted) of -- special case where we ignore single-sided nodes -- that are exactly at the cut point, since this should @@ -1089,21 +1136,7 @@ pgMaybe :: String -> Maybe a -> PairGraphM sym arch a pgMaybe _ (Just a) = return a pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg --- | Returns all discovered merge points from the given diverge point -getCombinedSyncPoints :: - forall sym arch. - HasCallStack => - GraphNode arch -> - PairGraphM sym arch ([((SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched), GraphNode arch)], SyncPoint arch) -getCombinedSyncPoints ndDiv = do - sync@(SyncPoint syncSet _ _) <- lookupPairGraph @sym pairGraphSyncPoints ndDiv - case syncSet of - PPa.PatchPair ndsO ndsP -> do - all_pairs <- forM (Set.toList $ Set.cartesianProduct (SetF.toSet ndsO) (SetF.toSet ndsP)) $ \(ndO, ndP) -> do - combined <- pgMaybe "failed to combine nodes" $ combineNodes ndO ndP - return $ ((ndO, ndP), combined) - return (all_pairs, sync) - _ -> return ([], sync) + -- | Compute a merged node for two diverging nodes -- FIXME: do we need to support mismatched node kinds here? @@ -1130,25 +1163,6 @@ tryPG :: PairGraphM sym arch a -> PairGraphM sym arch (Maybe a) tryPG f = catchError (Just <$> f) (\_ -> return Nothing) --- | Retrive the 'SyncPoint' fields corresponding to --- the divergence point of the given single-sided node -getSingleNodeSync :: - forall sym arch x bin. - HasCallStack => - L.Lens' (SyncPoint arch) (PPa.PatchPair x) -> - SingleNodeEntry arch bin -> - PairGraphM sym arch (x bin, x (PBi.OtherBinary bin)) -getSingleNodeSync lens sne = do - let bin = singleEntryBin sne - let nd = singleNodeDivergePoint sne - sp <- lookupPairGraph @sym pairGraphSyncPoints nd - let x = sp ^. lens - v1 <- PPa.get bin x - v2 <- PPa.get (PBi.flipRepr bin) x - return (v1, v2) - - - -- | Add a node back to the worklist to be re-analyzed if there is -- an existing abstract domain for it. Otherwise return Nothing. addToWorkList :: @@ -1301,22 +1315,20 @@ getPendingActions lens = do isSyncExit :: + forall sym arch bin. SingleNodeEntry arch bin -> PB.BlockTarget arch bin -> - PairGraphM sym arch (Maybe (PB.ConcreteBlock arch bin)) + PairGraphM sym arch (Maybe (SingleNodeEntry arch bin)) isSyncExit sne blkt@(PB.BlockTarget{}) = do - let dp = singleNodeDivergePoint sne - let bin = singleEntryBin sne - cuts <- getSyncPoint syncCutAddresses bin dp - excepts <- getSyncPoint syncExceptions bin dp + cuts <- getSingleNodeData syncCutAddresses sne + excepts <- getSingleNodeData syncExceptions sne let isExcept = Set.member (TupleF2 sne blkt) excepts case (not isExcept) && - Set.member (PPa.WithBin bin (PB.targetRawPC blkt)) cuts of - True -> return $ Just (PB.targetCall blkt) + Set.member (PPa.WithBin (singleEntryBin sne) (PB.targetRawPC blkt)) cuts of + True -> return $ Just (mkSingleNodeEntry (singleToNodeEntry sne) (PB.targetCall blkt)) False -> return Nothing isSyncExit _ _ = return Nothing - -- | Filter a list of reachable block exits to -- only those that should be handled for the given 'WorkItem' -- For a 'ProcessNode' item, this is all exits for a @@ -1330,7 +1342,7 @@ filterSyncExits :: [PPa.PatchPair (PB.BlockTarget arch)] -> PairGraphM sym arch [PPa.PatchPair (PB.BlockTarget arch)] filterSyncExits _ (ProcessNode (ReturnNode{})) _ = fail "Unexpected ReturnNode work item" -filterSyncExits _ (ProcessMerge sneO sneP) blktPairs = do +filterSyncExits _ (ProcessMergeAtExits sneO sneP) blktPairs = do let isSyncExitPair blktPair = do blktO <- PPa.get PBi.OriginalRepr blktPair blktP <- PPa.get PBi.PatchedRepr blktPair @@ -1338,31 +1350,53 @@ filterSyncExits _ (ProcessMerge sneO sneP) blktPairs = do y <- isSyncExit sneP blktP return $ isJust x && isJust y filterM isSyncExitPair blktPairs +-- nothing to do for a merge at entry, since we're considering all exits +-- to be synchronized +filterSyncExits _ (ProcessMergeAtEntry{}) blktPairs = return blktPairs filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of Nothing -> return blktPairs Just (Some sne) -> do - let dp = singleNodeDivergePoint sne let bin = singleEntryBin sne blkts <- mapM (PPa.get bin) blktPairs - exitBlks <- catMaybes <$> mapM (isSyncExit sne) blkts - unless (null exitBlks) $ do + syncExits <- catMaybes <$> mapM (isSyncExit sne) blkts + unless (null syncExits) $ do -- if any of the exits from this node are sync exits, -- then we need to queue up processing this node as -- a merge against all known merge points - addToSyncPoint syncMergeExitNodes bin dp sne - queueMerges priority sne + queueExitMerges priority (SyncAtExits sne (Set.fromList syncExits)) return blktPairs -queueMerges :: + +queueSyncPoints :: (NodePriorityK -> NodePriority) -> - SingleNodeEntry arch bin -> + SyncPoint arch bin -> + SyncPoint arch (PBi.OtherBinary bin) -> PairGraphM sym arch () -queueMerges priority sne = do - let dp = singleNodeDivergePoint sne - otherExits <- getSyncPoint syncMergeExitNodes (PBi.flipRepr (singleEntryBin sne)) dp - forM_ otherExits $ \otherExit -> do - wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge sne otherExit +queueSyncPoints priority sp1 sp2 = case (sp1, sp2) of + (SyncAtExits _ exits1, SyncAtStart sne2) -> forM_ exits1 $ \exit1 -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge True exit1 sne2 + modify $ queueWorkItem (priority PriorityHandleMerge) wi + (SyncAtStart{}, SyncAtExits{}) | Refl <- PBi.otherInvolutive bin -> queueSyncPoints priority sp2 sp1 + (SyncAtExits{}, SyncAtExits{}) -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge True (syncPointNode sp1) (syncPointNode sp2) modify $ queueWorkItem (priority PriorityHandleMerge) wi + (SyncAtStart{}, SyncAtStart{}) -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge False (syncPointNode sp1) (syncPointNode sp2) + modify $ queueWorkItem (priority PriorityHandleMerge) wi + where + bin = syncPointBin sp1 + +queueExitMerges :: + (NodePriorityK -> NodePriority) -> + SyncPoint arch bin -> + PairGraphM sym arch () +queueExitMerges priority sp = do + let sne = syncPointNode sp + let dp = singleNodeDivergePoint sne + addToSyncData syncPoints (singleEntryBin sne) dp sp + otherExits <- getSyncData syncPoints (PBi.flipRepr (singleEntryBin sne)) dp + forM_ otherExits $ \syncOther -> queueSyncPoints priority sp syncOther + -- | This handles the special case where the sync point -- is the return site for a function. @@ -1375,11 +1409,9 @@ handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of Just (Some sne) -> do let bin = singleEntryBin sne let dp = singleNodeDivergePoint sne - syncAddrs <- getSyncPoint syncCutAddresses bin dp + syncAddrs <- getSyncData syncCutAddresses bin dp let blk = singleNodeBlock sne case Set.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of - True -> do - addToSyncPoint syncMergeExitNodes bin dp sne - queueMerges priority sne + True -> queueExitMerges priority (SyncAtStart sne) False -> return () Nothing -> return () \ No newline at end of file diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 792893e7..2af7caae 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -58,7 +58,6 @@ module Pate.Verification.PairGraph.Node ( , singleToNodeEntry , singleNodeBlock , combineSingleEntries - , singleNodeBlock , singleNodeDivergence , toSingleNodeEntry ) where From c883edf870ff8005484a272d909b696ebd94a81b Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 31 May 2024 13:03:54 -0700 Subject: [PATCH 12/26] add simple logging to PairGraph operations --- src/Pate/Monad/PairGraph.hs | 54 ++++++++++++++++++++++------- src/Pate/Verification/PairGraph.hs | 55 +++++++++++++++++++++++++----- 2 files changed, 88 insertions(+), 21 deletions(-) diff --git a/src/Pate/Monad/PairGraph.hs b/src/Pate/Monad/PairGraph.hs index c5db1557..0bee0597 100644 --- a/src/Pate/Monad/PairGraph.hs +++ b/src/Pate/Monad/PairGraph.hs @@ -6,6 +6,12 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE PolyKinds #-} -- EquivM operations on a PairGraph module Pate.Monad.PairGraph @@ -56,7 +62,17 @@ import qualified Data.Macaw.CFG as MM import qualified Data.Map as Map import qualified Pate.Equivalence.Error as PEE import GHC.Stack (HasCallStack) +import qualified Prettyprinter as PP + + +instance IsTraceNode (k :: l) "pg_trace" where + type TraceNodeType k "pg_trace" = [String] + prettyNode () msgs = PP.vsep (map PP.viaShow msgs) + nodeTags = mkTags @k @"pg_trace" [Custom "debug"] +emitPGTrace :: [String] -> EquivM sym arch () +emitPGTrace [] = return () +emitPGTrace l = emitTrace @"pg_trace" l withPG :: HasCallStack => @@ -81,25 +97,37 @@ withPG_ pg f = execStateT f pg liftPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) a liftPG f = do pg <- get - case runPairGraphM pg f of - Left err -> lift $ throwHere $ PEE.PairGraphError err - Right (a,pg') -> do - put pg' - return a + env <- lift $ ask + withValidEnv env $ + case runPairGraphMLog pg f of + (l, Left err) -> do + lift $ emitPGTrace l + lift $ throwHere $ PEE.PairGraphError err + (l, Right (a,pg')) -> do + lift $ emitPGTrace l + put pg' + return a runPG :: HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM_ sym arch (a, PairGraph sym arch) -runPG pg f = case runPairGraphM pg f of - Left err -> throwHere $ PEE.PairGraphError err - Right a -> return a +runPG pg f = withValid $ case runPairGraphMLog pg f of + (l, Left err) -> do + emitPGTrace l + throwHere $ PEE.PairGraphError err + (l, Right a) -> do + emitPGTrace l + return a catchPG :: HasCallStack => PairGraphM sym arch a -> StateT (PairGraph sym arch) (EquivM_ sym arch) (Maybe a) catchPG f = do pg <- get - case runPairGraphM pg f of - Left{} -> return Nothing - Right (a,pg') -> do - put pg' - return $ Just a + env <- lift $ ask + withValidEnv env $ + case runPairGraphMLog pg f of + (l, Left{}) -> (lift $ emitPGTrace l) >> return Nothing + (l, Right (a,pg')) -> do + lift $ emitPGTrace l + put pg' + return $ Just a liftEqM_ :: HasCallStack => diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 4401cad7..f7d4059d 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -27,6 +27,7 @@ module Pate.Verification.PairGraph , PairGraph , PairGraphM , runPairGraphM + , runPairGraphMLog , execPairGraphM , evalPairGraphM , maybeUpdate @@ -131,6 +132,8 @@ import Control.Monad.State.Strict (MonadState (..), modify, State, get import Control.Monad.Except (ExceptT, MonadError (..)) import Control.Monad.Trans.Except (runExceptT) import Control.Monad.Trans.State.Strict (runState) +import Control.Monad.Trans.Writer hiding (tell) +import Control.Monad.Writer import qualified Control.Lens as L import Control.Lens ( (&), (.~), (^.), (%~) ) @@ -183,6 +186,8 @@ import Data.Parameterized.PairF import Data.Parameterized.SetF (SetF) import qualified Data.Parameterized.SetF as SetF import GHC.Stack (HasCallStack) +import Control.Monad.Reader + -- | Gas is used to ensure that our fixpoint computation terminates -- in a reasonable amount of time. Gas is expended each time @@ -526,19 +531,37 @@ mkProcessMerge syncAtExits sne1 sne2 False -> Just $ ProcessMergeAtEntryCtor sne2 sne1 mkProcessMerge _ _ _ = Nothing +-- | Can only mark a single node entry as a split if it is equal to +-- its own divergence point +mkProcessSplit :: SingleNodeEntry arch bin -> Maybe (WorkItem arch) +mkProcessSplit sne = do + GraphNode dp_ne <- return $ singleNodeDivergePoint sne + sne_dp <- toSingleNodeEntry (singleEntryBin sne) dp_ne + guard (sne_dp == sne) + return (ProcessSplitCtor (Some sne)) + + workItemNode :: WorkItem arch -> GraphNode arch workItemNode = \case ProcessNode nd -> nd ProcessMerge spO spP -> case combineSingleEntries spO spP of Just merged -> GraphNode merged Nothing -> panic Verifier "workItemNode" ["Unexpected mismatched single-sided nodes"] + ProcessSplit sne -> GraphNode (singleToNodeEntry sne) + +type PairGraphLog = [String] + +data PairGraphEnv sym arch where + PairGraphEnv :: forall sym arch. (PA.ValidArch arch) => PairGraphEnv sym arch -newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a } +newtype PairGraphM sym arch a = PairGraphM + { unpgM ::(ExceptT PEE.PairGraphErr (WriterT PairGraphLog (ReaderT (PairGraphEnv sym arch) (State (PairGraph sym arch))))) a } deriving (Functor , Applicative , Monad , MonadState (PairGraph sym arch) , MonadError PEE.PairGraphErr + , MonadWriter PairGraphLog ) instance PPa.PatchPairM (PairGraphM sym arch) where @@ -552,19 +575,35 @@ instance Alternative (PairGraphM sym arch) where empty = throwError $ PEE.PairGraphErr "No more alternatives" instance MonadFail (PairGraphM sym arch) where - fail msg = throwError $ PEE.PairGraphErr ("fail: " ++ msg) + fail msg = do + logPG $ "fail: " ++ msg + throwError $ PEE.PairGraphErr ("fail: " ++ msg) + +logPG :: String -> PairGraphM sym arch () +logPG msg = tell [msg] + +pgValid :: (PA.ValidArch arch => PairGraphM sym arch a) -> PairGraphM sym arch a +pgValid f = do + PairGraphEnv <- PairGraphM ask + f + +runPairGraphMLog :: + forall sym arch a. + PA.ValidArch arch => PairGraph sym arch -> PairGraphM sym arch a -> (PairGraphLog, Either PEE.PairGraphErr (a, PairGraph sym arch)) +runPairGraphMLog pg f = case runState (runReaderT (runWriterT (runExceptT (unpgM f))) (PairGraphEnv @sym @arch)) pg of + ((Left err,l), _) -> (l, Left err) + ((Right a,l), pg') -> (l, Right (a, pg')) + -runPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (a, PairGraph sym arch) -runPairGraphM pg f = case runState (runExceptT (unpgT f)) pg of - (Left err, _) -> Left err - (Right a, pg') -> Right (a, pg') +runPairGraphM :: PA.ValidArch arch => PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (a, PairGraph sym arch) +runPairGraphM pg f = snd $ runPairGraphMLog pg f -execPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (PairGraph sym arch) +execPairGraphM :: PA.ValidArch arch => PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (PairGraph sym arch) execPairGraphM pg f = case runPairGraphM pg f of Left err -> Left err Right (_,pg') -> Right pg' -evalPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr a +evalPairGraphM :: PA.ValidArch arch => PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr a evalPairGraphM pg f = case runPairGraphM pg f of Left err -> Left err Right (a,_) -> Right a From d4b30e175fd1db118a188e966086a7e5eb07bcf5 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 31 May 2024 13:08:47 -0700 Subject: [PATCH 13/26] add ProcessSplit as top-level work queue action this allows us to handle the "zero step" sync case explicitly, where one of the sides of the analysis takes no steps before re-synchronizing control flow --- src/Pate/Verification/PairGraph.hs | 112 ++++++++- src/Pate/Verification/PairGraph/Node.hs | 9 +- src/Pate/Verification/StrongestPosts.hs | 301 ++++++++++++++---------- 3 files changed, 288 insertions(+), 134 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index f7d4059d..e94529d1 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -72,7 +72,7 @@ module Pate.Verification.PairGraph , combineNodes , NodePriority(..) , addToWorkList - , WorkItem(ProcessNode) + , WorkItem(ProcessNode, ProcessSplit) , pattern ProcessMerge , workItemNode , getQueuedPriority @@ -122,6 +122,9 @@ module Pate.Verification.PairGraph , isDivergeNode , mkProcessMerge , dropWorkItem + , addDesyncExits + , queueSplitAnalysis + , handleKnownDesync ) where import Prettyprinter @@ -322,13 +325,23 @@ data WorkItem arch = | ProcessMergeAtEntryCtor (SingleNodeEntry arch PBi.Original) (SingleNodeEntry arch PBi.Patched) + -- | Handle starting a split analysis from a diverging node. + | ProcessSplitCtor (Some (SingleNodeEntry arch)) deriving (Eq, Ord) +instance PA.ValidArch arch => Show (WorkItem arch) where + show = \case + ProcessNode nd -> "ProcessNode " ++ show nd + ProcessMergeAtEntry sneO sneP -> "ProcessMergeAtEntry " ++ show sneO ++ " vs. " ++ show sneP + ProcessMergeAtExits sneO sneP -> "ProcessMergeAtExits " ++ show sneO ++ " vs. " ++ show sneP + ProcessSplit sne -> "ProcessSplit " ++ show sne + processMergeSinglePair :: WorkItem arch -> Maybe (SingleNodeEntry arch PBi.Original, SingleNodeEntry arch PBi.Patched) processMergeSinglePair wi = case wi of ProcessMergeAtExits sne1 sne2 -> Just (sne1,sne2) ProcessMergeAtEntry sne1 sne2 -> Just (sne1, sne2) ProcessNode{} -> Nothing + ProcessSplit{} -> Nothing -- Use mkProcessMerge as a partial smart constructor, but -- export this pattern so we can match on it @@ -341,8 +354,12 @@ pattern ProcessMergeAtEntry sneO sneP <- ProcessMergeAtEntryCtor sneO sneP pattern ProcessMerge:: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch PBi.Patched -> WorkItem arch pattern ProcessMerge sneO sneP <- (processMergeSinglePair -> Just (sneO, sneP)) -{-# COMPLETE ProcessNode, ProcessMergeAtExits, ProcessMergeAtEntry #-} -{-# COMPLETE ProcessNode, ProcessMerge #-} +pattern ProcessSplit :: SingleNodeEntry arch bin -> WorkItem arch +pattern ProcessSplit sne <- ProcessSplitCtor (Some sne) + + +{-# COMPLETE ProcessNode, ProcessMergeAtExits, ProcessMergeAtEntry, ProcessSplit #-} +{-# COMPLETE ProcessNode, ProcessMerge, ProcessSplit #-} -- TODO: After some refactoring I'm not sure if we actually need edge actions anymore, so this potentially can be simplified data ActionQueue sym arch = @@ -413,6 +430,8 @@ data SyncData arch = -- In these cases, the single-sided analysis continues instead, with the intention -- that another sync point is encountered after additional instructions are executed , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch))) + -- Exits from the corresponding desync node that start the single-sided analysis + , _syncDesyncExits :: PPa.PatchPair (SetF (PB.BlockTarget arch)) } data SyncPoint arch bin = @@ -431,7 +450,7 @@ instance OrdF (SyncPoint arch) where fromOrdering (compare sp1 sp2) instance Semigroup (SyncData arch) where - (SyncData a1 b1 c1) <> (SyncData a2 b2 c2) = (SyncData (a1 <> a2) (b1 <> b2) (c1 <> c2)) + (SyncData a1 b1 c1 d1) <> (SyncData a2 b2 c2 d2) = (SyncData (a1 <> a2) (b1 <> b2) (c1 <> c2) (d1 <> d2)) instance Monoid (SyncData arch) where @@ -439,6 +458,7 @@ instance Monoid (SyncData arch) where (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) + (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) $(L.makeLenses ''SyncData) $(L.makeLenses ''ActionQueue) @@ -511,6 +531,33 @@ addSyncAddress :: PairGraphM sym arch () addSyncAddress nd bin syncAddr = addToSyncData syncCutAddresses bin nd (PPa.WithBin bin syncAddr) +addDesyncExits :: + forall sym arch. + GraphNode arch {- ^ The divergent node -} -> + PPa.PatchPair (PB.BlockTarget arch) -> + PairGraphM sym arch () +addDesyncExits dp blktPair = do + PPa.catBins $ \bin -> do + blkt <- PPa.get bin blktPair + modifySyncData syncDesyncExits bin dp (Set.insert blkt) + +handleKnownDesync :: + (NodePriorityK -> NodePriority) -> + NodeEntry arch -> + PPa.PatchPair (PB.BlockTarget arch) -> + PairGraphM sym arch Bool +handleKnownDesync priority ne blktPair = fmap (fromMaybe False) $ tryPG $ do + let dp = GraphNode ne + blktO <- PPa.get PBi.OriginalRepr blktPair + blktP <- PPa.get PBi.PatchedRepr blktPair + knownDesyncsO <- getSyncData syncDesyncExits PBi.OriginalRepr dp + knownDesyncsP <- getSyncData syncDesyncExits PBi.PatchedRepr dp + case Set.member blktO knownDesyncsO && Set.member blktP knownDesyncsP of + True -> do + queueSplitAnalysis (priority PriorityHandleDesync) ne + return True + False -> return False + -- | Combine two single-sided nodes into a 'WorkItem' to process their -- merge. Returns 'Nothing' if the two single-sided nodes have different -- divergence points. @@ -867,6 +914,8 @@ queueNode priority nd__ pg__ = snd $ queueNode' priority nd__ (Set.empty, pg__) -- For 'ProcessMerge' work items, queues up the merge if -- there exist domains for both single-sided nodes. -- Otherwise, queues up the single-sided nodes with missing domains. +-- For 'ProcessSplit' work items, queues the given single-sided node if +-- it has a domain, otherwise queues the source (two-sided) diverging node. queueWorkItem :: NodePriority -> WorkItem arch -> PairGraph sym arch -> PairGraph sym arch queueWorkItem priority wi pg = case wi of ProcessNode nd -> queueNode priority nd pg @@ -880,7 +929,18 @@ queueWorkItem priority wi pg = case wi of (Nothing, Just{}) -> queueNode priority neO pg (Nothing, Nothing) -> queueNode priority neP (queueNode priority neO pg) - + ProcessSplit sne -> case getCurrentDomain pg (singleNodeDivergence sne) of + Just{} -> addItemToWorkList wi priority pg + Nothing -> queueNode priority (singleNodeDivergence sne) pg + +queueSplitAnalysis :: NodePriority -> NodeEntry arch -> PairGraphM sym arch () +queueSplitAnalysis priority ne = do + sneO <- toSingleNodeEntry PBi.OriginalRepr ne + sneP <- toSingleNodeEntry PBi.PatchedRepr ne + wiO <- pgMaybe "invalid original split" $ mkProcessSplit sneO + wiP <- pgMaybe "invalid patched split" $ mkProcessSplit sneP + modify $ queueWorkItem priority wiO + modify $ queueWorkItem priority wiP -- | Adds a node to the work list. If it doesn't have a domain, queue its ancestors. -- Takes a set of nodes that have already been considerd, and returns all considered nodes @@ -1229,11 +1289,11 @@ dropWorkItem :: PairGraph sym arch dropWorkItem wi gr = gr { pairGraphWorklist = RevMap.delete wi (pairGraphWorklist gr) } --- | Return the priority of the given 'GraphNode' if it is queued for --- normal processing +-- | Return the priority of the given 'WorkItem' getQueuedPriority :: - GraphNode arch -> PairGraph sym arch -> Maybe NodePriority -getQueuedPriority nd pg = RevMap.lookup (ProcessNode nd) (pairGraphWorklist pg) + WorkItem arch -> PairGraph sym arch -> Maybe NodePriority +getQueuedPriority wi pg = RevMap.lookup wi (pairGraphWorklist pg) + emptyWorkList :: PairGraph sym arch -> PairGraph sym arch emptyWorkList pg = pg { pairGraphWorklist = RevMap.empty } @@ -1368,6 +1428,18 @@ isSyncExit sne blkt@(PB.BlockTarget{}) = do False -> return Nothing isSyncExit _ _ = return Nothing +-- | True if the given node starts at exactly a sync point +isZeroStepSync :: + forall sym arch bin. + SingleNodeEntry arch bin -> + PairGraphM sym arch Bool +isZeroStepSync sne = do + cuts <- getSingleNodeData syncCutAddresses sne + logPG $ "isZeroStepSync cuts:" ++ show (Set.map PPa.withBinValue cuts) + let addr = PB.concreteAddress $ singleNodeBlock sne + logPG $ "isZeroStepSync addr:" ++ show addr + return $ Set.member (PPa.WithBin (singleEntryBin sne) addr) cuts + -- | Filter a list of reachable block exits to -- only those that should be handled for the given 'WorkItem' -- For a 'ProcessNode' item, this is all exits for a @@ -1392,6 +1464,23 @@ filterSyncExits _ (ProcessMergeAtExits sneO sneP) blktPairs = do -- nothing to do for a merge at entry, since we're considering all exits -- to be synchronized filterSyncExits _ (ProcessMergeAtEntry{}) blktPairs = return blktPairs +filterSyncExits priority (ProcessSplit sne) blktPairs = pgValid $ do + logPG $ "filterSyncExits (ProcessSplit):" ++ show sne + isZeroStepSync sne >>= \case + True -> do + queueExitMerges priority (SyncAtStart sne) + return [] + False -> do + let bin = singleEntryBin sne + desyncExits <- getSingleNodeData syncDesyncExits sne + logPG $ "allExits: " ++ show (pretty blktPairs) + logPG $ "desyncExits: " ++ show desyncExits + let isDesyncExitPair blktPair = do + blkt <- PPa.get bin blktPair + return $ Set.member blkt desyncExits + x <- filterM isDesyncExitPair blktPairs + logPG $ "result: " ++ show (pretty x) + return x filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of Nothing -> return blktPairs Just (Some sne) -> do @@ -1446,11 +1535,14 @@ handleSingleSidedReturnTo :: PairGraphM sym arch () handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of Just (Some sne) -> do + logPG $ "handleSingleSidedReturnTo" let bin = singleEntryBin sne let dp = singleNodeDivergePoint sne syncAddrs <- getSyncData syncCutAddresses bin dp let blk = singleNodeBlock sne case Set.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of - True -> queueExitMerges priority (SyncAtStart sne) + True -> do + logPG $ "queueExitMerges" + queueExitMerges priority (SyncAtStart sne) False -> return () Nothing -> return () \ No newline at end of file diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 2af7caae..2b1156af 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -441,9 +441,12 @@ toSingleNodeEntry :: PB.WhichBinaryRepr bin -> NodeEntry arch -> m (SingleNodeEntry arch bin) -toSingleNodeEntry bin (NodeEntry cctx bPair) = do - blk <- PPa.get bin bPair - return $ SingleNodeEntry bin (NodeContent cctx blk) +toSingleNodeEntry bin ne = do + case toSingleNode bin ne of + Just (NodeEntry cctx bPair) -> do + blk <- PPa.get bin bPair + return $ SingleNodeEntry bin (NodeContent cctx blk) + _ -> PPa.throwPairErr singleToNodeEntry :: SingleNodeEntry arch bin -> NodeEntry arch singleToNodeEntry (SingleNodeEntry bin (NodeContent cctx v)) = diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index a9631ea4..ec461a01 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -35,7 +35,7 @@ import Control.Monad.IO.Class import qualified Control.Monad.IO.Unlift as IO import Control.Monad.Reader (asks, local) import Control.Monad.Except (catchError, throwError) -import Control.Monad.State.Strict (get, StateT, runStateT, put, execStateT, modify) +import Control.Monad.State.Strict (get, gets, StateT, runStateT, put, execStateT, modify) import Control.Monad.Trans (lift) import Numeric (showHex) import Prettyprinter @@ -45,7 +45,7 @@ import qualified Data.ByteString as BS import qualified Data.ByteString.Char8 as BSC import qualified Data.Map as Map import qualified Data.Set as Set -import Data.List (findIndex, find) +import Data.List (findIndex, find, (\\)) import Data.Maybe (mapMaybe, catMaybes) import Data.Proxy import Data.Functor.Const @@ -557,15 +557,18 @@ addImmediateEqDomRefinementChoice nd preD gr0 = do choice ("No refinements") () $ return gr1 mapM_ go [minBound..maxBound] - +-- | Connect the divergence point to the start of the single-sided analysis +-- If there is no single-sided domain, then it is initialized to be the split +-- version of the two-sided analysis. initSingleSidedDomain :: - GraphNode arch -> + SingleNodeEntry arch bin -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -initSingleSidedDomain nd pg0 = withPG_ pg0 $ do +initSingleSidedDomain sne pg0 = withPG_ pg0 $ do priority <- lift $ thisPriority - let bin = PBi.OriginalRepr - nd_single <- toSingleGraphNode bin nd + let bin = singleEntryBin sne + let nd = singleNodeDivergence sne + let nd_single = GraphNode (singleToNodeEntry sne) dom_spec <- liftPG $ getCurrentDomainM nd PS.forSpec dom_spec $ \scope dom -> do case getCurrentDomain pg0 nd_single of @@ -578,21 +581,67 @@ initSingleSidedDomain nd pg0 = withPG_ pg0 $ do liftEqM_ $ \pg -> widenAlongEdge scope bundle nd dom pg nd_single return (PS.WithScope ()) +handleProcessSplit :: + SingleNodeEntry arch bin -> + PairGraph sym arch -> + EquivM sym arch (Maybe (GraphNode arch), PairGraph sym arch) +handleProcessSplit sne pg = withPG pg $ do + let divergeNode = singleNodeDivergePoint sne + priority <- lift $ thisPriority + case getCurrentDomain pg divergeNode of + Nothing -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode + return Nothing + Just{} -> do + let nd = GraphNode (singleToNodeEntry sne) + liftEqM_ $ initSingleSidedDomain sne + return $ Just nd + +handleProcessMerge :: + SingleNodeEntry arch PBi.Original -> + SingleNodeEntry arch PBi.Patched -> + PairGraph sym arch -> + EquivM sym arch (Maybe (GraphNode arch), PairGraph sym arch) +handleProcessMerge sneO sneP pg = withPG pg $ do + let + ndO = GraphNode $ singleToNodeEntry sneO + ndP = GraphNode $ singleToNodeEntry sneP + divergeNode = singleNodeDivergePoint sneO + priority <- lift $ thisPriority + case getCurrentDomain pg divergeNode of + Nothing -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode + return Nothing + Just{} -> do + case (getCurrentDomain pg ndO, getCurrentDomain pg ndP) of + (Just{}, Just{}) -> do + syncNode <- liftEqM $ mergeSingletons sneO sneP + return $ Just $ GraphNode syncNode + _ -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode + return Nothing +{- workItemDomainSpec :: WorkItem arch -> PairGraph sym arch -> EquivM sym arch (Maybe (GraphNode arch, PAD.AbstractDomainSpec sym arch), PairGraph sym arch) workItemDomainSpec wi pg = withPG pg $ case wi of ProcessNode nd -> do - case isDivergeNode nd pg of - True -> do - liftEqM_ $ initSingleSidedDomain nd - -- single-sided node has been queued, so we skip - -- any further analysis here + dom <- liftPG $ getCurrentDomainM nd + return $ Just (nd, dom) + ProcessSplit sne -> do + let divergeNode = singleNodeDivergePoint sne + priority <- lift $ thisPriority + case getCurrentDomain pg divergeNode of + Nothing -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode return Nothing - False -> do + Just{} -> do + liftEqM_ $ initSingleSidedDomain sne + let nd = GraphNode (singleToNodeEntry sne) dom <- liftPG $ getCurrentDomainM nd return $ Just (nd, dom) + ProcessMerge sneO sneP -> do let ndO = GraphNode $ singleToNodeEntry sneO @@ -603,32 +652,16 @@ workItemDomainSpec wi pg = withPG pg $ case wi of Nothing -> do liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode return Nothing - Just diverge_dom_spec -> do + Just{} -> do case (getCurrentDomain pg ndO, getCurrentDomain pg ndP) of (Just{}, Just{}) -> do syncNode <- liftEqM $ mergeSingletons sneO sneP dom_spec <- liftPG $ getCurrentDomainM (GraphNode syncNode) return $ Just (GraphNode syncNode, dom_spec) - (Just{}, Nothing) -> do - divergeNodeP <- toSingleGraphNode PBi.PatchedRepr divergeNode - _ <- PS.forSpec diverge_dom_spec $ \scope diverge_dom -> do - diverge_domP <- lift $ PAD.singletonDomain PBi.PatchedRepr diverge_dom - bundle <- lift $ noopBundle scope (graphNodeBlocks divergeNodeP) - -- if the current domain for the patched variant of the diverge node - -- doesn't exist, then we initialize it as the "singletonDomain" - -- otherwise we leave it unmodified, as it's potentially been widened - -- any updates that propagate from before this divergence will eventually - -- be propagated here via the Original single-sided analysis - liftPG $ (void $ getCurrentDomainM divergeNodeP) - <|> (modify $ \pg_ -> updateDomain' pg_ ndO divergeNodeP (PS.mkSimSpec scope diverge_domP) (priority PriorityWidening)) - liftEqM_ $ \pg_ -> withPredomain scope bundle diverge_domP $ withConditionsAssumed scope bundle diverge_dom divergeNode pg_ $ - widenAlongEdge scope bundle ndO diverge_domP pg_ divergeNodeP - return (PS.WithScope ()) - return Nothing - (Nothing, _) -> do - divergeNodeO <- toSingleGraphNode PBi.OriginalRepr divergeNode - liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNodeO + _ -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode return Nothing +-} mergeSingletons :: SingleNodeEntry arch PBi.Original -> @@ -675,17 +708,28 @@ withWorkItem gr0 f = do gr0' <- lift $ queuePendingNodes gr0 case chooseWorkItem gr0' of Nothing -> return Nothing - Just (priority, gr0'', wi) -> (lift $ workItemDomainSpec wi gr0'') >>= \case - (Nothing, gr1) -> withWorkItem gr1 f - (Just (nd, spec), gr1) -> do - res <- subTraceLabel @"node" (printPriorityKind priority) nd $ startTimer $ - atPriority priority Nothing $ PS.viewSpec spec $ \scope d -> do - runPendingActions refineActions nd (TupleF2 scope d) gr1 >>= \case - Just gr2 -> return $ Left gr2 - Nothing -> Right <$> f (priority, gr1, wi, spec) - case res of - Left gr2 -> withWorkItem gr2 f - Right a -> return $ Just a + Just (priority, gr1, wi) -> do + let nd = workItemNode wi + res <- subTraceLabel @"node" (printPriorityKind priority) nd $ atPriority priority Nothing $ do + (mnext, gr2) <- case wi of + ProcessNode nd' -> do + spec <- evalPG gr1 $ getCurrentDomainM nd + PS.viewSpec spec $ \scope d -> do + runPendingActions refineActions nd' (TupleF2 scope d) gr1 >>= \case + Just gr2 -> return $ (Nothing, gr2) + Nothing -> return $ (Just nd', gr1) + ProcessSplit sne -> handleProcessSplit sne gr1 + ProcessMerge sneO sneP -> handleProcessMerge sneO sneP gr1 + case (mnext, getCurrentDomain gr2 nd) of + (Just next, Just spec) | next == nd -> fmap Right $ f (priority, gr2, wi, spec) + _ -> return $ Left (mnext, gr2) + case res of + (Left ((Just next), gr2)) -> subTraceLabel @"node" (printPriorityKind priority) next $ do + spec <- evalPG gr2 $ getCurrentDomainM next + atPriority priority Nothing $ (Just <$> (f (priority, gr2, wi, spec))) + Left (Nothing, gr2) -> withWorkItem gr2 f + Right a -> return $ Just a + -- | Execute the forward dataflow fixpoint algorithm. -- Visit nodes and compute abstract domains until we propagate information @@ -1136,13 +1180,17 @@ accM b ta f = foldM f b ta processBundle :: forall sym arch v. PS.SimScope sym arch v -> + WorkItem arch -> NodeEntry arch -> SimBundle sym arch v -> AbstractDomain sym arch v -> [(PPa.PatchPair (PB.BlockTarget arch))] -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -processBundle scope node bundle d exitPairs gr0 = withSym $ \sym -> do +processBundle scope wi node bundle d exitPairs gr0_ = withSym $ \sym -> do + priority <- thisPriority + (filteredPairs, gr0) <- runPG gr0_ $ filterSyncExits priority wi exitPairs + gr1 <- checkObservables scope node bundle d gr0 paths <- withTracing @"message" "All Instruction Paths" $ do paths <- bundleToInstrTraces bundle @@ -1152,19 +1200,22 @@ processBundle scope node bundle d exitPairs gr0 = withSym $ \sym -> do -- Follow all the exit pairs we found let initBranchState = BranchState { branchGraph = gr1, branchDesyncChoice = Nothing, branchHandled = []} - st <- subTree @"blocktarget" "Block Exits" $ accM initBranchState (zip [0 ..] exitPairs) $ \st0 (idx,tgt) -> do + st <- subTree @"blocktarget" "Block Exits" $ accM initBranchState (zip [0 ..] filteredPairs) $ \st0 (idx,tgt) -> do pg1 <- lift $ queuePendingNodes (branchGraph st0) let st1 = st0 { branchGraph = pg1 } - case checkNodeRequeued st1 node of + case checkNodeRequeued st1 wi of True -> return st1 False -> subTrace tgt $ followExit scope bundle paths node d st1 (idx,tgt) -- confirm that all handled exits cover the set of possible exits - let allHandled = length (branchHandled st) == length exitPairs + let allHandled = length (branchHandled st) == length filteredPairs let anyNonTotal = branchDesyncChoice st == Just AdmitNonTotal - case allHandled || anyNonTotal of + case (allHandled || anyNonTotal) of -- we've handled all outstanding block exits, so we should now check -- that the result is total - True -> checkTotality node scope bundle d (branchHandled st) (branchGraph st) + True -> do + -- consider any filtered out pairs as being handled + let handled = branchHandled st ++ (exitPairs \\ filteredPairs) + checkTotality node scope bundle d handled (branchGraph st) -- some block exits have been intentially skipped, -- since we'll be revisiting this node we can skip the totality check as well False -> return $ branchGraph st @@ -1280,10 +1331,8 @@ visitNode scope wi@(workItemNode -> (GraphNode node@(nodeBlocks -> bPair))) d gr priority <- thisPriority return $ queueNode (priority PriorityHandleActions) (GraphNode node) gr3 Nothing -> withConditionsAssumed scope bundle d (GraphNode node) gr0 $ do - exitPairs <- PD.discoverPairs bundle - priority <- thisPriority - (filteredPairs, gr3) <- runPG gr2 $ filterSyncExits priority wi exitPairs - processBundle scope node bundle d filteredPairs gr3 + exitPairs <- PD.discoverPairs bundle + processBundle scope wi node bundle d exitPairs gr2 visitNode scope (workItemNode -> (ReturnNode fPair)) d gr0 = do -- propagate the abstract domain of the return node to @@ -2000,12 +2049,12 @@ updateBranchGraph st blkt pg = st {branchGraph = pg, branchHandled = blkt : bran checkNodeRequeued :: BranchState sym arch -> - NodeEntry arch -> + WorkItem arch -> Bool -checkNodeRequeued st node = fromMaybe False $ do +checkNodeRequeued st wi = fromMaybe False $ do bc <- branchDesyncChoice st return $ choiceRequiresRequeue bc - <|> (getQueuedPriority (GraphNode node) (branchGraph st) >> return True) + <|> (getQueuedPriority wi (branchGraph st) >> return True) followExit :: PS.SimScope sym arch v -> @@ -2551,70 +2600,79 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi priority <- thisPriority currBlockO <- toSingleNode PBi.OriginalRepr currBlock currBlockP <- toSingleNode PBi.PatchedRepr currBlock - let divergeNode = GraphNode currBlock - let pg = gr0 - let msg = "Control flow desynchronization found at: " ++ show divergeNode - a <- case mchoice of - Just bc | choiceRequiresRequeue bc -> return bc - _ -> do - () <- withTracing @"message" "Equivalence Counter-example" $ withSym $ \sym -> do - -- we've already introduced the path condition here, so we just want to see how we got here - res <- getSomeGroundTrace scope bundle dom Nothing - emitTrace @"trace_events" res - return () - choose @"()" msg $ \choice -> forM_ [minBound..maxBound] $ \bc -> - choice (show bc) () $ return bc - emitTrace @"message" $ "Resolved control flow desynchronization with: " ++ show a - let st' = st { branchDesyncChoice = Just a } - case a of - -- leave block exit as unhandled - AdmitNonTotal -> return st' - ChooseSyncPoint -> do - pg1 <- chooseSyncPoint divergeNode pg - return $ st'{ branchGraph = pg1 } - -- handleDivergingPaths scope bundle currBlock (st'{ branchGraph = pg2 }) dom blkt - ChooseDesyncPoint -> do - pg1 <- chooseDesyncPoint divergeNode pg - -- drop domains from any outgoing edges, since the set of outgoing edges - -- from this node will likely change - let pg2 = dropPostDomains divergeNode (priority PriorityDomainRefresh) pg1 - -- re-queue the node after picking a de-synchronization point - let pg3 = queueNode (priority PriorityHandleActions) divergeNode pg2 - return $ st'{ branchGraph = pg3 } - IsInfeasible condK -> do - gr2 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockO) condK pg - gr3 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockP) condK gr2 - return $ st'{ branchGraph = gr3 } - DeferDecision -> do - -- add this back to the work list at a low priority - -- this allows, for example, the analysis to determine - -- that this is unreachable (potentially after refinements) and therefore - -- doesn't need synchronization - Just pg1 <- return $ addToWorkList divergeNode (priority PriorityDeferred) pg - return $ st'{ branchGraph = pg1 } - AlignControlFlow condK -> withSym $ \sym -> do - traces <- bundleToInstrTraces bundle - pg2 <- case traces of - PPa.PatchPairC traceO traceP -> do - -- NOTE: this predicate is not satisfiable in the current assumption - -- context: we are assuming a branch condition that leads to - -- a control flow divergence, and this predicate states exact control - -- flow equality. - -- Given this, it can't be simplified using the solver here. - -- It can be simplified later outside of this context, once it has been - -- added to the assumptions for the node - traces_eq_ <- compareSymSeq sym traceO traceP $ \evO evP -> - return $ W4.backendPred sym (ET.instrDisassembled evO == ET.instrDisassembled evP) - -- if-then-else expressions for booleans are a bit clumsy and don't work well - -- with simplification, but the sequence comparison introduces them - -- at each branch point, so we convert them into implications - traces_eq <- IO.liftIO $ WEH.iteToImp sym traces_eq_ - pg1 <- addToEquivCondition scope (GraphNode currBlock) condK traces_eq pg - -- drop all post domains from this node since they all need to be re-computed - -- under this additional assumption/assertion - return $ dropPostDomains (GraphNode currBlock) (priority PriorityDomainRefresh) pg1 - _ -> return pg - return $ st'{ branchGraph = pg2 } + (handled, gr1) <- runPG gr0 $ handleKnownDesync priority currBlock blkt + case handled of + True -> do + emitTrace @"message" $ "Known desynchronization point. Queue split analysis." + return $ st{ branchGraph = gr1 } + False -> do + let divergeNode = GraphNode currBlock + let pg = gr1 + let msg = "Control flow desynchronization found at: " ++ show divergeNode + a <- case mchoice of + Just bc | choiceRequiresRequeue bc -> return bc + _ -> do + () <- withTracing @"message" "Equivalence Counter-example" $ withSym $ \sym -> do + -- we've already introduced the path condition here, so we just want to see how we got here + res <- getSomeGroundTrace scope bundle dom Nothing + emitTrace @"trace_events" res + return () + choose @"()" msg $ \choice -> forM_ [minBound..maxBound] $ \bc -> + choice (show bc) () $ return bc + emitTrace @"message" $ "Resolved control flow desynchronization with: " ++ show a + let st' = st { branchDesyncChoice = Just a } + case a of + -- leave block exit as unhandled + AdmitNonTotal -> return st' + ChooseSyncPoint -> do + pg1 <- withPG_ pg $ do + liftEqM_ $ chooseSyncPoint divergeNode + liftPG $ addDesyncExits divergeNode blkt + liftPG $ queueSplitAnalysis (priority PriorityHandleDesync) currBlock + return $ st'{ branchGraph = pg1 } + -- handleDivergingPaths scope bundle currBlock (st'{ branchGraph = pg2 }) dom blkt + ChooseDesyncPoint -> do + pg1 <- chooseDesyncPoint divergeNode pg + -- drop domains from any outgoing edges, since the set of outgoing edges + -- from this node will likely change + let pg2 = dropPostDomains divergeNode (priority PriorityDomainRefresh) pg1 + -- re-queue the node after picking a de-synchronization point + let pg3 = queueNode (priority PriorityHandleActions) divergeNode pg2 + return $ st'{ branchGraph = pg3 } + IsInfeasible condK -> do + gr2 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockO) condK pg + gr3 <- pruneCurrentBranch scope (divergeNode, GraphNode currBlockP) condK gr2 + return $ st'{ branchGraph = gr3 } + DeferDecision -> do + -- add this back to the work list at a low priority + -- this allows, for example, the analysis to determine + -- that this is unreachable (potentially after refinements) and therefore + -- doesn't need synchronization + Just pg1 <- return $ addToWorkList divergeNode (priority PriorityDeferred) pg + return $ st'{ branchGraph = pg1 } + AlignControlFlow condK -> withSym $ \sym -> do + traces <- bundleToInstrTraces bundle + pg2 <- case traces of + PPa.PatchPairC traceO traceP -> do + -- NOTE: this predicate is not satisfiable in the current assumption + -- context: we are assuming a branch condition that leads to + -- a control flow divergence, and this predicate states exact control + -- flow equality. + -- Given this, it can't be simplified using the solver here. + -- It can be simplified later outside of this context, once it has been + -- added to the assumptions for the node + traces_eq_ <- compareSymSeq sym traceO traceP $ \evO evP -> + return $ W4.backendPred sym (ET.instrDisassembled evO == ET.instrDisassembled evP) + -- if-then-else expressions for booleans are a bit clumsy and don't work well + -- with simplification, but the sequence comparison introduces them + -- at each branch point, so we convert them into implications + traces_eq <- IO.liftIO $ WEH.iteToImp sym traces_eq_ + pg1 <- addToEquivCondition scope (GraphNode currBlock) condK traces_eq pg + -- drop all post domains from this node since they all need to be re-computed + -- under this additional assumption/assertion + return $ dropPostDomains (GraphNode currBlock) (priority PriorityDomainRefresh) pg1 + _ -> return pg + return $ st'{ branchGraph = pg2 } ppMux :: (f -> PP.Doc a) -> MT.MuxTree sym f -> PP.Doc a ppMux ppf mt = case MT.viewMuxTree mt of @@ -2675,6 +2733,7 @@ instance Show DesyncChoice where choiceRequiresRequeue :: DesyncChoice -> Bool choiceRequiresRequeue = \case AdmitNonTotal -> False + ChooseSyncPoint -> False _ -> True handleStub :: From 9269e67256e070175ca26c14859d50da057b1f48 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 31 May 2024 13:10:52 -0700 Subject: [PATCH 14/26] clean up logging --- src/Pate/Verification/PairGraph.hs | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index e94529d1..a247b2f7 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -1435,9 +1435,7 @@ isZeroStepSync :: PairGraphM sym arch Bool isZeroStepSync sne = do cuts <- getSingleNodeData syncCutAddresses sne - logPG $ "isZeroStepSync cuts:" ++ show (Set.map PPa.withBinValue cuts) let addr = PB.concreteAddress $ singleNodeBlock sne - logPG $ "isZeroStepSync addr:" ++ show addr return $ Set.member (PPa.WithBin (singleEntryBin sne) addr) cuts -- | Filter a list of reachable block exits to @@ -1465,7 +1463,6 @@ filterSyncExits _ (ProcessMergeAtExits sneO sneP) blktPairs = do -- to be synchronized filterSyncExits _ (ProcessMergeAtEntry{}) blktPairs = return blktPairs filterSyncExits priority (ProcessSplit sne) blktPairs = pgValid $ do - logPG $ "filterSyncExits (ProcessSplit):" ++ show sne isZeroStepSync sne >>= \case True -> do queueExitMerges priority (SyncAtStart sne) @@ -1473,13 +1470,10 @@ filterSyncExits priority (ProcessSplit sne) blktPairs = pgValid $ do False -> do let bin = singleEntryBin sne desyncExits <- getSingleNodeData syncDesyncExits sne - logPG $ "allExits: " ++ show (pretty blktPairs) - logPG $ "desyncExits: " ++ show desyncExits let isDesyncExitPair blktPair = do blkt <- PPa.get bin blktPair return $ Set.member blkt desyncExits x <- filterM isDesyncExitPair blktPairs - logPG $ "result: " ++ show (pretty x) return x filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of Nothing -> return blktPairs @@ -1535,14 +1529,11 @@ handleSingleSidedReturnTo :: PairGraphM sym arch () handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of Just (Some sne) -> do - logPG $ "handleSingleSidedReturnTo" let bin = singleEntryBin sne let dp = singleNodeDivergePoint sne syncAddrs <- getSyncData syncCutAddresses bin dp let blk = singleNodeBlock sne case Set.member (PPa.WithBin bin (PB.concreteAddress blk)) syncAddrs of - True -> do - logPG $ "queueExitMerges" - queueExitMerges priority (SyncAtStart sne) + True -> queueExitMerges priority (SyncAtStart sne) False -> return () Nothing -> return () \ No newline at end of file From 61bd5ff3e6d1f47bff08dd76727ba4470e7d049a Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 5 Jun 2024 11:17:26 -0700 Subject: [PATCH 15/26] add execPG to Monad.PairGraph --- src/Pate/Monad/PairGraph.hs | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Pate/Monad/PairGraph.hs b/src/Pate/Monad/PairGraph.hs index 0bee0597..36e1c556 100644 --- a/src/Pate/Monad/PairGraph.hs +++ b/src/Pate/Monad/PairGraph.hs @@ -31,6 +31,7 @@ module Pate.Monad.PairGraph , addLazyAction , queuePendingNodes , runPG + , execPG , liftPartEqM_ ) where @@ -82,11 +83,15 @@ withPG :: withPG pg f = runStateT f pg evalPG :: + HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM sym arch a evalPG pg f = fst <$> (withPG pg $ liftPG f) +execPG :: HasCallStack => PairGraph sym arch -> PairGraphM sym arch a -> EquivM_ sym arch (PairGraph sym arch) +execPG pg f = snd <$> runPG pg f + withPG_ :: HasCallStack => PairGraph sym arch -> From b0b35f96bc1dd9283e7ed054c18429f350e5405b Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 5 Jun 2024 11:19:31 -0700 Subject: [PATCH 16/26] support stubs returning to sync points --- src/Pate/Verification/PairGraph.hs | 53 +++++++--- src/Pate/Verification/StrongestPosts.hs | 123 ++++++++++++++++-------- src/Pate/Verification/Widening.hs | 43 +++++---- 3 files changed, 149 insertions(+), 70 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index a247b2f7..387a5486 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -78,6 +78,7 @@ module Pate.Verification.PairGraph , getQueuedPriority , queueAncestors , queueNode + , queueWorkItem , emptyWorkList , SyncData , SyncPoint(..) @@ -125,6 +126,7 @@ module Pate.Verification.PairGraph , addDesyncExits , queueSplitAnalysis , handleKnownDesync + , addReturnPointSync ) where import Prettyprinter @@ -437,7 +439,7 @@ data SyncData arch = data SyncPoint arch bin = SyncAtExits { syncPointNode :: SingleNodeEntry arch bin , _syncPointExits :: Set (SingleNodeEntry arch bin) } | SyncAtStart { syncPointNode :: SingleNodeEntry arch bin } - deriving (Eq, Ord) + deriving (Eq, Ord, Show) syncPointBin :: SyncPoint arch bin -> PBi.WhichBinaryRepr bin syncPointBin sp = singleEntryBin $ syncPointNode sp @@ -541,19 +543,21 @@ addDesyncExits dp blktPair = do blkt <- PPa.get bin blktPair modifySyncData syncDesyncExits bin dp (Set.insert blkt) +-- | If this node is a known divergence point, queue a split +-- analysis starting here, marking this as a diverging exit, and return True +-- Otherwise do nothing and return handleKnownDesync :: (NodePriorityK -> NodePriority) -> NodeEntry arch -> PPa.PatchPair (PB.BlockTarget arch) -> PairGraphM sym arch Bool -handleKnownDesync priority ne blktPair = fmap (fromMaybe False) $ tryPG $ do +handleKnownDesync priority ne blkt = fmap (fromMaybe False) $ tryPG $ do let dp = GraphNode ne - blktO <- PPa.get PBi.OriginalRepr blktPair - blktP <- PPa.get PBi.PatchedRepr blktPair - knownDesyncsO <- getSyncData syncDesyncExits PBi.OriginalRepr dp - knownDesyncsP <- getSyncData syncDesyncExits PBi.PatchedRepr dp - case Set.member blktO knownDesyncsO && Set.member blktP knownDesyncsP of + desyncExitsO <- getSyncData syncDesyncExits PBi.OriginalRepr dp + desyncExitsP <- getSyncData syncDesyncExits PBi.PatchedRepr dp + case not (Set.null desyncExitsO) && not (Set.null desyncExitsP) of True -> do + addDesyncExits dp blkt queueSplitAnalysis (priority PriorityHandleDesync) ne return True False -> return False @@ -819,8 +823,7 @@ getCurrentDomainM :: PairGraphM sym arch (AbstractDomainSpec sym arch) getCurrentDomainM nd = do pg <- get - Just spec <- return $ getCurrentDomain pg nd - return spec + pgValid $ pgMaybe ("missing domain for: " ++ show nd) $ getCurrentDomain pg nd getEdgesFrom :: PairGraph sym arch -> @@ -1421,9 +1424,12 @@ isSyncExit :: isSyncExit sne blkt@(PB.BlockTarget{}) = do cuts <- getSingleNodeData syncCutAddresses sne excepts <- getSingleNodeData syncExceptions sne + syncs <- getSingleNodeData syncPoints sne let isExcept = Set.member (TupleF2 sne blkt) excepts - case (not isExcept) && - Set.member (PPa.WithBin (singleEntryBin sne) (PB.targetRawPC blkt)) cuts of + let isCutExit = Set.member (PPa.WithBin (singleEntryBin sne) (PB.targetRawPC blkt)) cuts + let exitSyncs = Set.fromList $ catMaybes $ map (\case SyncAtExits sne' _ -> Just sne'; _ -> Nothing) (Set.toList syncs) + let isAlreadySync = Set.member sne exitSyncs + case (not isExcept) && (isCutExit || isAlreadySync) of True -> return $ Just (mkSingleNodeEntry (singleToNodeEntry sne) (PB.targetCall blkt)) False -> return Nothing isSyncExit _ _ = return Nothing @@ -1488,6 +1494,31 @@ filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleN queueExitMerges priority (SyncAtExits sne (Set.fromList syncExits)) return blktPairs +-- | Mark the return point of a target as a sync point, if +-- it matches a cut address +addReturnPointSync :: + (NodePriorityK -> NodePriority) -> + NodeEntry arch -> + PPa.PatchPair (PB.BlockTarget arch) -> + PairGraphM sym arch () +addReturnPointSync priority ne blktPair = case asSingleNodeEntry ne of + Just (Some sne) -> do + let bin = singleEntryBin sne + blkt <- PPa.get bin blktPair + case PB.targetReturn blkt of + Just ret -> do + cuts <- getSingleNodeData syncCutAddresses sne + excepts <- getSingleNodeData syncExceptions sne + let isExcept = Set.member (TupleF2 sne blkt) excepts + case (not isExcept) && + Set.member (PPa.WithBin (singleEntryBin sne) (PB.concreteAddress ret)) cuts of + True -> do + let syncExit = mkSingleNodeEntry (singleToNodeEntry sne) ret + queueExitMerges priority (SyncAtExits sne (Set.singleton syncExit)) + False -> return () + Nothing -> return () + Nothing -> return () + queueSyncPoints :: (NodePriorityK -> NodePriority) -> diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index ec461a01..3e9a32ea 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -139,6 +139,7 @@ import qualified What4.JSON as W4S import qualified What4.Concrete as W4 import Data.Parameterized.PairF (PairF(..)) import qualified What4.Concrete as W4 +import Data.Parameterized (Pair(..)) -- Overall module notes/thoughts -- @@ -407,11 +408,11 @@ chooseDesyncPoint nd pg0 = do pblks <- PD.lookupBlocks blk divergeSingle <- toSingleGraphNode bin nd return $ (divergeSingle, Some blk, pblks) - (_, Some syncBin) <- pickCutPoint syncMsg + [Some (PPa.WithBin syncBin _)] <- pickCutPoints False syncMsg [divergeO, divergeP] let otherBin = PBi.flipRepr syncBin diverge <- PPa.getC otherBin divergePair - _ <- pickCutPoint syncMsg [diverge] + _ <- pickCutPoints False syncMsg [diverge] return pg0 where syncMsg = "Choose a desynchronization point:" @@ -423,23 +424,14 @@ chooseSyncPoint :: PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) chooseSyncPoint nd pg0 = do - divergePair@(PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do + (PPa.PatchPairC divergeO divergeP) <- PPa.forBinsC $ \bin -> do blk <- PPa.get bin (graphNodeBlocks nd) pblks <- PD.lookupBlocks blk divergeSingle <- toSingleGraphNode bin nd return $ (divergeSingle, Some blk, pblks) - (sync, Some syncBin) <- pickCutPoint syncMsg - [divergeO, divergeP] - let otherBin = PBi.flipRepr syncBin - - addr <- PB.concreteAddress <$> PPa.get syncBin (nodeBlocks sync) - withPG_ pg0 $ do - liftPG $ addSyncAddress nd syncBin addr - diverge <- PPa.getC otherBin divergePair - syncOther <- lift $ fst <$> pickCutPoint syncMsg [diverge] - addrOther <- PB.concreteAddress <$> PPa.get otherBin (nodeBlocks syncOther) - liftPG $ addSyncAddress nd otherBin addrOther - + cuts <- pickCutPoints True syncMsg [divergeO, divergeP] + execPG pg0 $ forM_ cuts $ \(Some (PPa.WithBin bin addr)) -> do + addSyncAddress nd bin addr where syncMsg = "Choose a synchronization point:" @@ -498,22 +490,37 @@ getIntermediateAddrs pb = -- | Introduce a cut point (chosen from a list of nodes). -- Code discovery will consider any CFAR that reaches this cut point to end in a Jump -- to the next CFAR (i.e. splits a CFAR in two at the given address) -pickCutPoint :: +pickCutPoints :: + Bool {- ^ true if this should keep asking for cut points -} -> String -> [(GraphNode arch, Some (PB.ConcreteBlock arch), PD.ParsedBlocks arch)] -> - EquivM sym arch (NodeEntry arch, Some PBi.WhichBinaryRepr) -pickCutPoint msg inputs = do - (sync, Some bin, (addr, Some blk)) <- choose @"node" msg $ \choice -> do - forM_ inputs $ \(divergeSingle, Some blk, PD.ParsedBlocks pblks) -> do - let bin = PB.blockBinRepr blk - forM_ pblks $ \pblk -> forM_ (getIntermediateAddrs pblk) $ \addr -> do - -- FIXME: block entry kind is unused at the moment? - let concBlk = PB.mkConcreteBlock blk PB.BlockEntryJump addr - let node = mkNodeEntry' divergeSingle (PPa.mkSingle bin concBlk) - choice "" (GraphNode node) $ do - return (node, Some bin, (addr, Some concBlk)) - _ <- addIntraBlockCut addr blk - return (sync, Some bin) + EquivM sym arch [Some (PPa.WithBin (PAd.ConcreteAddress arch))] +pickCutPoints pickMany msg inputs = go [] + where + hasBin bin picked = + any (\(Some (PPa.WithBin bin' _)) -> case testEquality bin bin' of Just Refl -> True; _ -> False) picked + go picked = do + mres <- choose @"()" msg $ \choice -> do + forM_ inputs $ \(_divergeSingle, Some blk, PD.ParsedBlocks pblks) -> do + let bin = PB.blockBinRepr blk + forM_ pblks $ \pblk -> forM_ (getIntermediateAddrs pblk) $ \addr -> do + -- FIXME: block entry kind is unused at the moment? + let concBlk = PB.mkConcreteBlock blk PB.BlockEntryJump addr + --let node = mkNodeEntry' divergeSingle (PPa.mkSingle bin concBlk) + choice (show addr ++ " " ++ "(" ++ show bin ++ ")") () $ do + return $ Just $ (Pair concBlk (PPa.WithBin bin addr)) + case pickMany && hasBin PBi.OriginalRepr picked && hasBin PBi.PatchedRepr picked of + True -> choice "Finish Choosing" () $ return Nothing + False -> return () + case mres of + Just (Pair blk (PPa.WithBin bin addr)) -> do + _ <- addIntraBlockCut addr blk + let x = Some (PPa.WithBin bin (PAd.segOffToAddr addr)) + case pickMany of + True -> go (x:picked) + False -> return (x:picked) + Nothing -> return picked + -- | Add an intra-block cut to *both* binaries after the given address. cutAfterAddress :: @@ -571,16 +578,38 @@ initSingleSidedDomain sne pg0 = withPG_ pg0 $ do let nd_single = GraphNode (singleToNodeEntry sne) dom_spec <- liftPG $ getCurrentDomainM nd PS.forSpec dom_spec $ \scope dom -> do + dom_single <- PAD.singletonDomain bin dom + {- case getCurrentDomain pg0 nd_single of Just{} -> return () Nothing -> do - dom_single <- PAD.singletonDomain bin dom + emitTrace @"message" "init single-sided domain" let dom_single_spec = PS.mkSimSpec scope dom_single liftPG $ modify $ \pg -> initDomain pg nd nd_single (priority PriorityHandleDesync) dom_single_spec + -} bundle <- lift $ noopBundle scope (graphNodeBlocks nd) - liftEqM_ $ \pg -> widenAlongEdge scope bundle nd dom pg nd_single + liftEqM_ $ \pg -> do + pr <- currentPriority + atPriority (raisePriority pr) (Just "Starting Split Analysis") $ + withGraphNode' scope nd bundle dom pg $ + widenAlongEdge scope bundle nd dom_single pg nd_single return (PS.WithScope ()) +withGraphNode' :: + PS.SimScope sym arch v -> + GraphNode arch -> + PS.SimBundle sym arch v -> + AbstractDomain sym arch v -> + PairGraph sym arch -> + EquivM sym arch (PairGraph sym arch) -> + EquivM sym arch (PairGraph sym arch) +withGraphNode' scope nd bundle dom pg f = case nd of + GraphNode ne -> withPredomain scope bundle dom $ withAbsDomain ne dom pg $ withValidInit scope (nodeBlocks ne) $ + withConditionsAssumed scope bundle dom nd pg $ f + ReturnNode nr -> withPredomain scope bundle dom $ withConditionsAssumed scope bundle dom (ReturnNode nr) pg $ + f + + handleProcessSplit :: SingleNodeEntry arch bin -> PairGraph sym arch -> @@ -684,17 +713,19 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do specO <- evalPG pg $ getCurrentDomainM ndO specP <- evalPG pg $ getCurrentDomainM ndP - + pg1 <- fmap (\x -> PS.viewSpecBody x PS.unWS) $ withFreshScope blkPair $ \scope -> fmap PS.WithScope $ withValidInit scope blkPairO $ withValidInit scope blkPairP $ do (_, domO) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) specO (_, domP) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) specP dom <- PAD.zipSingletonDomains sym domO domP bundle <- noopBundle scope (nodeBlocks syncNode) - withPredomain scope bundle dom $ withConditionsAssumed scope bundle domP ndP pg $ do - withTracing @"node" ndP $ do + withPredomain scope bundle dom $ + withConditionsAssumed scope bundle domO ndO pg $ + withConditionsAssumed scope bundle domP ndP pg $ do emitTraceLabel @"domain" PAD.Predomain (Some dom) - widenAlongEdge scope bundle ndP dom pg (GraphNode syncNode) + pg1 <- withTracing @"node" ndO $ widenAlongEdge scope bundle ndO dom pg (GraphNode syncNode) + withTracing @"node" ndP $ widenAlongEdge scope bundle ndP dom pg1 (GraphNode syncNode) return (syncNode, pg1) -- | Choose some work item (optionally interactively) @@ -718,15 +749,22 @@ withWorkItem gr0 f = do runPendingActions refineActions nd' (TupleF2 scope d) gr1 >>= \case Just gr2 -> return $ (Nothing, gr2) Nothing -> return $ (Just nd', gr1) - ProcessSplit sne -> handleProcessSplit sne gr1 - ProcessMerge sneO sneP -> handleProcessMerge sneO sneP gr1 + ProcessSplit sne -> do + emitTrace @"debug" $ "ProcessSplit: " ++ show sne + handleProcessSplit sne gr1 + ProcessMerge sneO sneP -> do + emitTrace @"debug" $ "ProcessMerge: " ++ show sneO ++ " vs. " ++ show sneP + handleProcessMerge sneO sneP gr1 case (mnext, getCurrentDomain gr2 nd) of (Just next, Just spec) | next == nd -> fmap Right $ f (priority, gr2, wi, spec) _ -> return $ Left (mnext, gr2) case res of - (Left ((Just next), gr2)) -> subTraceLabel @"node" (printPriorityKind priority) next $ do - spec <- evalPG gr2 $ getCurrentDomainM next - atPriority priority Nothing $ (Just <$> (f (priority, gr2, wi, spec))) + (Left ((Just next), gr2)) -> do + case getCurrentDomain gr2 next of + Just spec -> subTraceLabel @"node" (printPriorityKind priority) next $ + atPriority priority Nothing $ (Just <$> (f (priority, gr2, wi, spec))) + -- we are missing the expected domain, so we need to just try again + Nothing -> withWorkItem (queueWorkItem priority wi gr2) f Left (Nothing, gr2) -> withWorkItem gr2 f Right a -> return $ Just a @@ -2208,6 +2246,7 @@ triageBlockTarget :: EquivM sym arch (BranchState sym arch) triageBlockTarget scope bundle' paths currBlock st d blkts = withSym $ \sym -> do let gr = branchGraph st + priority <- thisPriority stubPair <- fnTrace "getFunctionStubPair" $ getFunctionStubPair blkts matches <- PD.matchesBlockTarget bundle' blkts res <- withPathCondition matches $ do @@ -2230,7 +2269,9 @@ triageBlockTarget scope bundle' paths currBlock st d blkts = withSym $ \sym -> d let isEquatedCallSite = any (PB.matchEquatedAddress pPair) (PMC.equatedFunctions ctx) if | isEquatedCallSite -> handleInlineCallee scope bundle currBlock d gr pPair rets - | hasStub stubPair -> handleStub scope bundle currBlock d gr pPair (Just rets) stubPair + | hasStub stubPair -> withPG_ gr $ do + liftEqM_ $ \gr_ -> handleStub scope bundle currBlock d gr_ pPair (Just rets) stubPair + liftPG $ addReturnPointSync priority currBlock blkts | otherwise -> handleOrdinaryFunCall scope bundle currBlock d gr pPair rets (Just ecase, PPa.PatchPairNothing) -> fmap (updateBranchGraph st blkts) $ do diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index f22ec509..3941dfa2 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -765,14 +765,13 @@ propagateCondition scope bundle from to gr0_ = fnTrace "propagateCondition" $ do Nothing -> do emitTrace @"debug" "No condition to propagate" return Nothing - _ | not (shouldPropagate (getPropagationKind gr to condK)) -> do - emitTrace @"debug" "Condition not propagated" - return Nothing Just{} -> do -- take the condition of the target edge and bind it to -- the output state of the bundle cond <- getEquivPostCondition scope bundle to condK gr {- + + let blks = graphNodeBlocks from skip <- case (blks, graphNodeBlocks to) of -- this is a synchronization edge, so we attempt to filter the equivalence condition @@ -791,23 +790,31 @@ propagateCondition scope bundle from to gr0_ = fnTrace "propagateCondition" $ do -- we need to update our own condition cond_pred <- PEC.toPred sym cond goalTimeout <- CMR.asks (PC.cfgGoalTimeout . envConfig) - not_cond <- liftIO $ W4.notPred sym cond_pred - isPredSat' goalTimeout not_cond >>= \case - -- equivalence condition for this path holds, we - -- don't need any changes + isPredSat' goalTimeout cond_pred >>= \case Just False -> do - emitTraceLabel @"expr" (ExprLabel $ "Proven " ++ conditionName condK) (Some cond_pred) + emitTrace @"message" "Condition is infeasible, dropping branch." + Just <$> pruneCurrentBranch scope (from,to) condK gr + _ | not (shouldPropagate (getPropagationKind gr to condK)) -> do + emitTrace @"debug" "Condition not propagated" return Nothing - -- we need more assumptions for this condition to hold - Just True -> do - priority <- thisPriority - emitTraceLabel @"expr" (ExprLabel $ "Propagated " ++ conditionName condK) (Some cond_pred) - let propK = getPropagationKind gr to condK - gr1 <- updateEquivCondition scope from condK (Just (nextPropagate propK)) cond gr - return $ Just $ queueAncestors (priority PriorityPropagation) from $ - queueNode (priority PriorityNodeRecheck) from $ - dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr1) - Nothing -> throwHere $ PEE.InconclusiveSAT + _ -> do + not_cond <- liftIO $ W4.notPred sym cond_pred + isPredSat' goalTimeout not_cond >>= \case + -- equivalence condition for this path holds, we + -- don't need any changes + Just False -> do + emitTraceLabel @"expr" (ExprLabel $ "Proven " ++ conditionName condK) (Some cond_pred) + return Nothing + -- we need more assumptions for this condition to hold + Just True -> do + priority <- thisPriority + emitTraceLabel @"expr" (ExprLabel $ "Propagated " ++ conditionName condK) (Some cond_pred) + let propK = getPropagationKind gr to condK + gr1 <- updateEquivCondition scope from condK (Just (nextPropagate propK)) cond gr + return $ Just $ queueAncestors (priority PriorityPropagation) from $ + queueNode (priority PriorityNodeRecheck) from $ + dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr1) + Nothing -> throwHere $ PEE.InconclusiveSAT -- | Given the results of symbolic execution, and an edge in the pair graph -- to consider, compute an updated abstract domain for the target node, From 367dfdfd6c6117915a70499640db65f7e77ed4e5 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 5 Jun 2024 11:20:49 -0700 Subject: [PATCH 17/26] update challenge 10 script --- tests/aarch32/scripted/challenge10.pate | 29 +++++++++++++++---------- 1 file changed, 18 insertions(+), 11 deletions(-) diff --git a/tests/aarch32/scripted/challenge10.pate b/tests/aarch32/scripted/challenge10.pate index 713dd22f..2c5e3bd9 100644 --- a/tests/aarch32/scripted/challenge10.pate +++ b/tests/aarch32/scripted/challenge10.pate @@ -24,17 +24,9 @@ segment1+0x4120 [ via: "transport_handler" (segment1+0x400c) ] Choose a synchronization point: > segment1+0x412a (patched) > segment1+0x412a (original) - -segment1+0x4120 (original) vs. segment1+0x3dd44 (patched) [ via: "transport_handler" (segment1+0x400c) ] - ... - Branch to: "transport_handler" (segment1+0x412a) (original) vs. Call to: "puts" (segment1+0x33ac) Returns to: "transport_handler" (segment1+0x41b8) (patched) - ... - ... - > Remove divergence in equivalence condition - Call to: "puts" (segment1+0x33ac) Returns to: "transport_handler" (segment1+0x41b8) (original) vs. Jump to: "transport_handler" (segment1+0x412a) (patched) - ... - ... - > Remove divergence in equivalence condition + > segment1+0x41b0 (original) + > segment1+0x41b0 (patched) + > Finish Choosing segment1+0x412a [ via: "transport_handler" (segment1+0x400c) ] Modify Proof Node @@ -45,6 +37,21 @@ segment1+0x412a [ via: "transport_handler" (segment1+0x400c) ] Include Location: > Include All Registers +segment1+0x412a (original) vs. segment1+0x41b0 (patched) + ... + ... + ... + ... + > Align control flow in equivalence condition + +segment1+0x41b0 (original) vs. segment1+0x412a (patched) + ... + ... + ... + ... + > Align control flow in equivalence condition + + Verification Finished Continue verification? > Finish and view final result \ No newline at end of file From 8aaf24bed168c20e444842fc236bed75de63a0ab Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 08:56:18 -0700 Subject: [PATCH 18/26] update tests --- tests/aarch32/desync-defer.pate | 2 ++ tests/aarch32/desync-simple.pate | 1 + tests/aarch32/desync-zerostep.pate | 1 + tests/aarch32/unequal/desync-defer.pate | 2 ++ tests/aarch32/unequal/desync-simple.pate | 1 + 5 files changed, 7 insertions(+) diff --git a/tests/aarch32/desync-defer.pate b/tests/aarch32/desync-defer.pate index 9bbb9948..9800df5f 100644 --- a/tests/aarch32/desync-defer.pate +++ b/tests/aarch32/desync-defer.pate @@ -24,6 +24,7 @@ Function Entry "f" (0x10158) Choose a synchronization point: > 0x10188 (original) > 0x10170 (patched) + > Finish Choosing 0x101e8 (original) vs. 0x101d8 (patched) ... @@ -49,6 +50,7 @@ Function Entry "f" (0x10158) Choose a synchronization point: > 0x101f4 (original) > 0x101ec (patched) + > Finish Choosing diff --git a/tests/aarch32/desync-simple.pate b/tests/aarch32/desync-simple.pate index 942617cb..74aa9a7e 100644 --- a/tests/aarch32/desync-simple.pate +++ b/tests/aarch32/desync-simple.pate @@ -12,6 +12,7 @@ Function Entry "f" Choose a synchronization point: > 0x8054 (original) > 0x8054 (patched) + > Finish Choosing Verification Finished Continue verification? diff --git a/tests/aarch32/desync-zerostep.pate b/tests/aarch32/desync-zerostep.pate index 1051f0c3..917ea996 100644 --- a/tests/aarch32/desync-zerostep.pate +++ b/tests/aarch32/desync-zerostep.pate @@ -24,6 +24,7 @@ Function Entry "f" Choose a synchronization point: > 0x1014c (original) > 0x1015c (patched) + > Finish Choosing // TODO: this is just to finish the analysis // so the test doesn't hang. We need to replace this diff --git a/tests/aarch32/unequal/desync-defer.pate b/tests/aarch32/unequal/desync-defer.pate index 873c7b55..54eae297 100644 --- a/tests/aarch32/unequal/desync-defer.pate +++ b/tests/aarch32/unequal/desync-defer.pate @@ -24,6 +24,7 @@ Function Entry "f" (0x10158) Choose a synchronization point: > 0x10188 (original) > 0x10170 (patched) + > Finish Choosing 0x10188 (original) vs. 0x10170 (patched) ... @@ -64,6 +65,7 @@ Function Entry "f" (0x10158) Choose a synchronization point: > 0x101f4 (original) > 0x101ec (patched) + > Finish Choosing diff --git a/tests/aarch32/unequal/desync-simple.pate b/tests/aarch32/unequal/desync-simple.pate index 223edb5d..72726209 100644 --- a/tests/aarch32/unequal/desync-simple.pate +++ b/tests/aarch32/unequal/desync-simple.pate @@ -12,6 +12,7 @@ Function Entry "f" Choose a synchronization point: > 0x8054 (original) > 0x8054 (patched) + > Finish Choosing 0x8054 [ via: "f" (0x8048) Handle observable difference: From 48186bc2e2cea25ef9d3fabc17612e5a8f8b4fb1 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 12:51:20 -0700 Subject: [PATCH 19/26] update desync-zerostep tests --- tests/aarch32/desync-zerostep.original.exe | Bin 128176 -> 128228 bytes tests/aarch32/desync-zerostep.patched.exe | Bin 128176 -> 128228 bytes tests/aarch32/desync-zerostep.pate | 32 +++++++++++---------- tests/src/desync-zerostep.original.c | 9 ++++-- tests/src/desync-zerostep.patched.c | 9 ++++-- 5 files changed, 29 insertions(+), 21 deletions(-) diff --git a/tests/aarch32/desync-zerostep.original.exe b/tests/aarch32/desync-zerostep.original.exe index fff50d8cfb18ca357ef276a006957d0434096b40..0dcb57bada8d1a522369a1cc31d2577c66419760 100755 GIT binary patch delta 654 zcmZ8fJxc>Y5PcIbCTf#dNI)U+6F*TQrD7q1;E9EWMHCb*6cIrXn}~`aDO613*{RrQ zrG;qa53sYe_2bZ>$dOC0Z!QVM%rX1+?VFjM-MyPk;5`#KiutC7o&f58s0lwH z#UUj=&yzobWO^ylml%kL>e|{C6DJSX(Url&+s5D>Mtd^G&B1FBr*;JR0?uBLdidNH zLHc{PEBG`{t;UY@o!SyRdqZs34x--v`2F=_ji<3!jpt^&t8%|8vh#E7$Wd4es8#S& zOIhcROl%dGRfuv~c_mTETZzwJ`<%ds298b%S3Ot4Ro6r2&G6#ki8CRlyz2t3c w$CYNk_fuF`u3U6De4r{82-9`L5M6ok0y%}56>M7TIcbhOa;p6nE&sg0A5>#&cmMzZ delta 580 zcmZ9JKS%;m9LIk@J-Y;ns|2G24>c%Kuq6vBh%DNoh?WS73JMyGpd5lDTnY@7qh6av zw7a z?4pXZ%9C|I9&tc`R^Hzjg2hm6lmmzs|JVT8@cPZBE$^QuK4|t!AV82fLHP)22j#=0 zt;Ae8_X8*pp+HwNFhKg(V1$?-NFZ&eb;_1sB<2_Jl5)d2TYlNbW5oPI4L=b!AoPF3 zZCk?*@h6)wuuoWp@H*Qyu*~L79LIB(Gcn-i&yl2uZQ7(!^%T>l9Gx)1-){EpKo$I7ka(A{mNZM6f@LMG8XONeHbD4hE9N zmqAEG5ZnY2U0h3@%qZQAJ}_A1k(XV+^AaJ=xt#mm?|%23^Ul3*zY)1=M2c4ErC%Bz ze!eMydKhZL0hBqFB^3D5tzfCNIA@!ujo)j#FaCZl3{4!Ye49OM#tt#{s$uLG>QPkO z1aJdXFR*@cT@*p--@%1^2bCWPZ7_9cDO(Y{hYlnu6nDB ztFBGA%?QrJYnKBe0pI9+hUUuvd2Dq8;xI76$Se=MAwK1SQDU523n_n193$sN1>7cf z$4`*!2N*y!$`F$DV*ma_yj|$MPjD$IiSjgJHeoqVv<2WH|UqoIPK5Mm;`I9}}2#Ef}XOf4D#{k!=cA TobN43CjM~wN%uO|eqP`nLKu0G delta 596 zcmZ9J&r1S96vyAwwQWH{Qz%GkGsB34jV?hE1P0Ni2%>{sA}`UUIz$ISNf3j=U*H@y zy41~Em!$px|9}WOXe}s)h-=c#-mDvlv&{SQdB5h(>{m@J)WoE0`fa7$?%5au@NEIU zkUoGonK+vC9cmziQpW+MSS>xSyzFmz>)A-4s2Jz{V5`T^eJ?s!i2P Choose desynchronization points ... Choose a desynchronization point: - > 0x1014c (original) - > 0x1014c (patched) + > 0x1015c (original) + > 0x1015c (patched) + + -0x1014c [ via: "f" +0x1015c [ via: "f" ... - Call to: "puts" (0x10108) Returns to: "f" + Call to: "puts" (0x10110) Returns to: "f" ... ... > Choose synchronization points ... Choose a synchronization point: - > 0x1014c (original) - > 0x1015c (patched) + > 0x1015c (original) + > 0x1016c (patched) > Finish Choosing -// TODO: this is just to finish the analysis -// so the test doesn't hang. We need to replace this -// once this case is handled properly. -0x1014c (original) vs. 0x10150 (patched) +// verifier can't automatically figure out that +// the pointer written by 'puts' is the same/unmodified +0x1015c (original) vs. 0x1016c (patched) ... - Call to: "puts" (0x10108) Returns to: "f" - ... - ... - > Ignore divergence + ... + ... + ... + > Assert difference is infeasible (prove immediately) + Verification Finished Continue verification? diff --git a/tests/src/desync-zerostep.original.c b/tests/src/desync-zerostep.original.c index abeaf20b..b54e2f07 100644 --- a/tests/src/desync-zerostep.original.c +++ b/tests/src/desync-zerostep.original.c @@ -1,13 +1,16 @@ #include "util.h" +static const char HELLO[] = "hello"; + void f(); void _start() { - f(); + f(HELLO); } // dummy implementation int clock() { return 0; } int puts(const char *str) { return 0; } + int NON_OBSERVE = -11; int OBSERVE __attribute__((section(".output"))) = -12; //int OBSERVE = -12; @@ -18,7 +21,7 @@ int g() { } #pragma noinline -void f() { +void f(char* msg) { NON_OBSERVE = 1; - puts("hello"); + puts(msg); } \ No newline at end of file diff --git a/tests/src/desync-zerostep.patched.c b/tests/src/desync-zerostep.patched.c index 6a8d69b8..eeebd30f 100644 --- a/tests/src/desync-zerostep.patched.c +++ b/tests/src/desync-zerostep.patched.c @@ -1,13 +1,16 @@ #include "util.h" +static const char HELLO[] = "hello"; + void f(); void _start() { - f(); + f(HELLO); } // dummy implementation int clock() { return 0; } int puts(const char *str) { return 0; } + int NON_OBSERVE = -11; int OBSERVE __attribute__((section(".output"))) = -12; //int OBSERVE = -12; @@ -18,12 +21,12 @@ int g() { } #pragma noinline -void f() { +void f(char* msg) { // desync NON_OBSERVE = g(); // sync NON_OBSERVE = 1; - puts("hello"); + puts(msg); } From 3bd4ac5ea113642b7c7b75d995ed7dba6d55aff5 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 12:52:05 -0700 Subject: [PATCH 20/26] ensure that merge work items aren't lost from the queue --- src/Pate/Verification/PairGraph.hs | 8 +++++--- tests/AArch32TestMain.hs | 2 +- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 387a5486..61d74fa9 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -928,10 +928,12 @@ queueWorkItem priority wi pg = case wi of neP = GraphNode (singleToNodeEntry spP) in case (getCurrentDomain pg neO, getCurrentDomain pg neP) of (Just{},Just{}) -> addItemToWorkList wi priority pg - (Just{}, Nothing) -> queueNode priority neP pg - (Nothing, Just{}) -> queueNode priority neO pg + (Just{}, Nothing) -> queueAncestors (raisePriority priority) neP (addItemToWorkList wi priority pg) + (Nothing, Just{}) -> queueAncestors (raisePriority priority) neO (addItemToWorkList wi priority pg) (Nothing, Nothing) -> - queueNode priority neP (queueNode priority neO pg) + queueAncestors (raisePriority priority) neP + $ queueAncestors (raisePriority priority) neO + $ addItemToWorkList wi priority pg ProcessSplit sne -> case getCurrentDomain pg (singleNodeDivergence sne) of Just{} -> addItemToWorkList wi priority pg Nothing -> queueNode priority (singleNodeDivergence sne) pg diff --git a/tests/AArch32TestMain.hs b/tests/AArch32TestMain.hs index 8add9790..6082cdb0 100644 --- a/tests/AArch32TestMain.hs +++ b/tests/AArch32TestMain.hs @@ -9,7 +9,7 @@ main = do { testArchName = "aarch32" , testArchLoader = AArch32.archLoader , testExpectEquivalenceFailure = - [ "stack-struct", "unequal/stack-struct", "max-signed", "desync-zerostep", "desync-orphan-return" + [ "stack-struct", "unequal/stack-struct", "max-signed","desync-orphan-return" -- missing interactive test support ] , testExpectSelfEquivalenceFailure = [] From 6ff9dd742291528fa60edec9e337754073fbd97b Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 12:56:18 -0700 Subject: [PATCH 21/26] only output "Finish Choosing" once when picking sync point --- src/Pate/Verification/StrongestPosts.hs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 3e9a32ea..16846578 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -509,9 +509,9 @@ pickCutPoints pickMany msg inputs = go [] --let node = mkNodeEntry' divergeSingle (PPa.mkSingle bin concBlk) choice (show addr ++ " " ++ "(" ++ show bin ++ ")") () $ do return $ Just $ (Pair concBlk (PPa.WithBin bin addr)) - case pickMany && hasBin PBi.OriginalRepr picked && hasBin PBi.PatchedRepr picked of - True -> choice "Finish Choosing" () $ return Nothing - False -> return () + case pickMany && hasBin PBi.OriginalRepr picked && hasBin PBi.PatchedRepr picked of + True -> choice "Finish Choosing" () $ return Nothing + False -> return () case mres of Just (Pair blk (PPa.WithBin bin addr)) -> do _ <- addIntraBlockCut addr blk From b7132d75e83effaff252d9b33e991cc7173c5cb7 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 16:50:10 -0700 Subject: [PATCH 22/26] handle orphaned returns by implicitly adding equivalence condition --- src/Pate/Equivalence/Error.hs | 4 +-- src/Pate/Verification/StrongestPosts.hs | 41 +++++++++++++++++++------ tests/aarch32/desync-orphan-return.pate | 5 ++- 3 files changed, 38 insertions(+), 12 deletions(-) diff --git a/src/Pate/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs index 06587b78..f82d89d0 100644 --- a/src/Pate/Equivalence/Error.hs +++ b/src/Pate/Equivalence/Error.hs @@ -166,7 +166,7 @@ data InnerEquivalenceError arch | UninterpretedInstruction | FailedToResolveAddress (MM.MemWord (MM.ArchAddrWidth arch)) | forall tp. FailedToGroundExpr (SomeExpr tp) - | OrphanedSingletonAnalysis (PB.FunPair arch) + | OrphanedSinglesidedAnalysis (PB.FunPair arch) | RequiresInvalidPointerOps | PairGraphError PairGraphErr | forall e. X.Exception e => UnhandledException e @@ -231,7 +231,7 @@ isRecoverable' e = case e of BlockHasNoExit{} -> True OrphanedFunctionReturns{} -> True CallReturnsToFunctionEntry{} -> True - OrphanedSingletonAnalysis{} -> True + OrphanedSinglesidedAnalysis{} -> True UnsatisfiableEquivalenceCondition{} -> True _ -> False diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 16846578..1c623655 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -369,9 +369,9 @@ handleDanglingReturns fnPairs pg = do [] -> return pg0 _ -> do let fn_single_ = PPa.mkSingle (PB.functionBinRepr fn_single) fn_single - err <- emitError' (PEE.OrphanedSingletonAnalysis fn_single_) + err <- emitError' (PEE.OrphanedSinglesidedAnalysis fn_single_) return $ recordMiscAnalysisError pg0 (ReturnNode ret) err - + foldM go pg single_rets @@ -1241,7 +1241,7 @@ processBundle scope wi node bundle d exitPairs gr0_ = withSym $ \sym -> do st <- subTree @"blocktarget" "Block Exits" $ accM initBranchState (zip [0 ..] filteredPairs) $ \st0 (idx,tgt) -> do pg1 <- lift $ queuePendingNodes (branchGraph st0) let st1 = st0 { branchGraph = pg1 } - case checkNodeRequeued st1 wi of + case checkNodeRequeued gr1 st1 wi of True -> return st1 False -> subTrace tgt $ followExit scope bundle paths node d st1 (idx,tgt) -- confirm that all handled exits cover the set of possible exits @@ -1394,9 +1394,8 @@ visitNode scope (workItemNode -> (ReturnNode fPair)) d gr0 = do Nothing -> withTracing @"message" "Toplevel Return" $ do withConditionsAssumed scope bundle d (ReturnNode fPair) gr0' $ do case isSingleReturn fPair of - Just{} -> void $ emitError' $ PEE.OrphanedSingletonAnalysis (nodeFuns fPair) - Nothing -> return () - return gr0' + Just{} -> handleOrphanedSingleSidedReturn scope fPair gr0' + Nothing -> return gr0' -- Here, we're using a bit of a trick to propagate abstract domain information to call sites. -- We are making up a "dummy" simulation bundle that basically just represents a no-op, and @@ -1429,6 +1428,26 @@ visitNode scope (workItemNode -> (ReturnNode fPair)) d gr0 = do liftEqM_ $ \pg -> widenAlongEdge scope bundle (ReturnNode fPair) d pg (GraphNode node) liftPG $ handleSingleSidedReturnTo priority node +-- | Used to handle the case where a single-sided analysis +-- has continued up to the top-level return. +-- In most cases, this represents a control flow path that +-- is only present in the patched program, and so we +-- simply add as an equivalence condition that this +-- single-sided return isn't taken. +-- We emit a warning as well, however, since this is also potentially +-- a result of some issue with the analysis (e.g. forgetting to +-- provide one of the synchronization points) +handleOrphanedSingleSidedReturn :: + PS.SimScope sym arch v -> + NodeReturn arch -> + PairGraph sym arch -> + EquivM sym arch (PairGraph sym arch) +handleOrphanedSingleSidedReturn scope nd pg = withSym $ \sym -> do + priority <- thisPriority + emitWarning $ PEE.OrphanedSinglesidedAnalysis (nodeFuns nd) + pg1 <- addToEquivCondition scope (ReturnNode nd) ConditionEquiv (W4.falsePred sym) pg + return $ queueAncestors (priority PriorityPropagation) (ReturnNode nd) pg1 + -- | Construct a "dummy" simulation bundle that basically just -- immediately returns the prestate as the poststate. -- This is used to compute widenings that propagate abstract domain @@ -2086,13 +2105,17 @@ updateBranchGraph :: BranchState sym arch -> PPa.PatchPair (PB.BlockTarget arch) updateBranchGraph st blkt pg = st {branchGraph = pg, branchHandled = blkt : branchHandled st } checkNodeRequeued :: + PairGraph sym arch -> BranchState sym arch -> WorkItem arch -> Bool -checkNodeRequeued st wi = fromMaybe False $ do - bc <- branchDesyncChoice st +checkNodeRequeued stPre stPost wi = fromMaybe False $ do + bc <- branchDesyncChoice stPost return $ choiceRequiresRequeue bc - <|> (getQueuedPriority wi (branchGraph st) >> return True) + <|> do + Nothing <- return $ getQueuedPriority wi stPre + _ <- getQueuedPriority wi (branchGraph stPost) + return True followExit :: PS.SimScope sym arch v -> diff --git a/tests/aarch32/desync-orphan-return.pate b/tests/aarch32/desync-orphan-return.pate index fd317210..d1ea0251 100644 --- a/tests/aarch32/desync-orphan-return.pate +++ b/tests/aarch32/desync-orphan-return.pate @@ -25,8 +25,11 @@ Function Entry "f" ... Choose a synchronization point: > 0x1014c (original) - > 0x10164 (patched) + > 0x10160 (patched) + > Finish Choosing + +/* // TODO: we should assume that the additional // return in the patched program isn't reachable, // however at the moment there is simply an error raised From 93bfc71f4f4853b3b251bcd5e2e42ac83c40ede4 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Fri, 7 Jun 2024 17:03:38 -0700 Subject: [PATCH 23/26] mark desync-orphan as expected conditional verification --- tests/AArch32TestMain.hs | 2 +- tests/TestBase.hs | 10 +++++----- tests/aarch32/desync-orphan-return.expect | 1 + tests/aarch32/desync-orphan-return.pate | 2 -- 4 files changed, 7 insertions(+), 8 deletions(-) create mode 100644 tests/aarch32/desync-orphan-return.expect diff --git a/tests/AArch32TestMain.hs b/tests/AArch32TestMain.hs index 6082cdb0..8737b707 100644 --- a/tests/AArch32TestMain.hs +++ b/tests/AArch32TestMain.hs @@ -9,7 +9,7 @@ main = do { testArchName = "aarch32" , testArchLoader = AArch32.archLoader , testExpectEquivalenceFailure = - [ "stack-struct", "unequal/stack-struct", "max-signed","desync-orphan-return" + [ "stack-struct", "unequal/stack-struct", "max-signed" -- missing interactive test support ] , testExpectSelfEquivalenceFailure = [] diff --git a/tests/TestBase.hs b/tests/TestBase.hs index 40b8c165..f8a16a66 100644 --- a/tests/TestBase.hs +++ b/tests/TestBase.hs @@ -67,7 +67,7 @@ runTests cfg = do [ T.testGroup "equivalence" $ map (mkTest cfg) equivTestFiles , T.testGroup "inequivalence" $ map (\fp -> T.testGroup fp $ [mkEquivTest cfg ShouldNotVerify fp]) inequivTestFiles , T.testGroup "conditional equivalence" $ map (\fp -> T.testGroup fp $ [mkEquivTest cfg ShouldConditionallyVerify fp]) condequivTestFiles - , T.testGroup "scripted" $ map (\fp -> T.testGroup fp $ [mkEquivTest cfg ShouldExpect fp]) scriptedFiles + , T.testGroup "scripted" $ map (\fp -> T.testGroup fp $ [mkEquivTest cfg ShouldConditionallyVerify fp]) scriptedFiles ] expectSelfEquivalenceFailure :: TestConfig -> FilePath -> Bool @@ -84,7 +84,6 @@ expectEquivalenceFailure cfg sv fp = ShouldVerify -> baseName' ShouldNotVerify -> "unequal/" ++ baseName' ShouldConditionallyVerify -> "conditional/" ++ baseName' - ShouldExpect -> "expect/" ++ baseName' mkTest :: TestConfig -> FilePath -> T.TestTree mkTest cfg fp = @@ -97,7 +96,7 @@ mkTest cfg fp = wrap :: T.TestTree -> T.TestTree wrap t = if (expectSelfEquivalenceFailure cfg fp) then T.expectFail t else t -data ShouldVerify = ShouldVerify | ShouldNotVerify | ShouldConditionallyVerify | ShouldExpect +data ShouldVerify = ShouldVerify | ShouldNotVerify | ShouldConditionallyVerify deriving Show mkEquivTest :: TestConfig -> ShouldVerify -> FilePath -> T.TestTree @@ -135,8 +134,9 @@ doTest mwb cfg _sv fp = do infoCfgExists <- doesFileExist (fp <.> "toml") argFileExists <- doesFileExist (fp <.> "args") scriptFileExists <- doesFileExist (fp <.> "pate") - sv <- case _sv of - ShouldExpect -> readFile (fp <.> "expect") >>= \case + expectFileExists <- doesFileExist (fp <.> "expect") + sv <- case expectFileExists of + True -> readFile (fp <.> "expect") >>= \case "Equivalent" -> return ShouldVerify "Inequivalent" -> return ShouldNotVerify "ConditionallyEquivalent" -> return ShouldConditionallyVerify diff --git a/tests/aarch32/desync-orphan-return.expect b/tests/aarch32/desync-orphan-return.expect new file mode 100644 index 00000000..e1eadd4d --- /dev/null +++ b/tests/aarch32/desync-orphan-return.expect @@ -0,0 +1 @@ +ConditionallyEquivalent \ No newline at end of file diff --git a/tests/aarch32/desync-orphan-return.pate b/tests/aarch32/desync-orphan-return.pate index d1ea0251..d91d3558 100644 --- a/tests/aarch32/desync-orphan-return.pate +++ b/tests/aarch32/desync-orphan-return.pate @@ -28,8 +28,6 @@ Function Entry "f" > 0x10160 (patched) > Finish Choosing - -/* // TODO: we should assume that the additional // return in the patched program isn't reachable, // however at the moment there is simply an error raised From 95229aecd76d848ad71b828899b51da4877f9b36 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Mon, 10 Jun 2024 09:44:54 -0700 Subject: [PATCH 24/26] add a 20 minute per-test timeout --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index f8c2b6bc..2d804d18 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -190,7 +190,7 @@ jobs: - name: Test if: runner.os == 'Linux' run: | - cabal test pkg:pate + cabal test pkg:pate --test-options="-t 1200s" - name: Docs run: cabal haddock pkg:pate From e13b7e4adcf1d8be9ff3e54d5a11f5210ed7ee26 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 11 Jun 2024 09:06:55 -0700 Subject: [PATCH 25/26] don't use .expect file for self-equivalence test --- tests/TestBase.hs | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/tests/TestBase.hs b/tests/TestBase.hs index f8a16a66..0b863df2 100644 --- a/tests/TestBase.hs +++ b/tests/TestBase.hs @@ -135,8 +135,8 @@ doTest mwb cfg _sv fp = do argFileExists <- doesFileExist (fp <.> "args") scriptFileExists <- doesFileExist (fp <.> "pate") expectFileExists <- doesFileExist (fp <.> "expect") - sv <- case expectFileExists of - True -> readFile (fp <.> "expect") >>= \case + sv <- case (expectFileExists, mwb) of + (True, Nothing) -> readFile (fp <.> "expect") >>= \case "Equivalent" -> return ShouldVerify "Inequivalent" -> return ShouldNotVerify "ConditionallyEquivalent" -> return ShouldConditionallyVerify @@ -236,9 +236,7 @@ doTest mwb cfg _sv fp = do ShouldVerify -> failTest "Failed to prove equivalence." ShouldNotVerify -> return () ShouldConditionallyVerify -> failTest "Failed to prove conditional equivalence." - _ -> failTest $ "Unhandled expected result: " ++ show sv PEq.ConditionallyEquivalent -> case sv of ShouldVerify -> failTest "Failed to prove equivalence." ShouldNotVerify -> failTest "Unexpectedly proved conditional equivalence." ShouldConditionallyVerify -> return () - _ -> failTest $ "Unhandled expected result: " ++ show sv From fbf06248f805eee9a16fc8cd0962448067ab2573 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 11 Jun 2024 09:46:07 -0700 Subject: [PATCH 26/26] proper handling for special case where stub returns exactly to a sync point --- src/Pate/Verification/PairGraph.hs | 62 +++++++++++++++++++----------- 1 file changed, 39 insertions(+), 23 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 61d74fa9..dfb76701 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -436,8 +436,9 @@ data SyncData arch = , _syncDesyncExits :: PPa.PatchPair (SetF (PB.BlockTarget arch)) } +-- sync exit point should *always* point to a cut address data SyncPoint arch bin = - SyncAtExits { syncPointNode :: SingleNodeEntry arch bin , _syncPointExits :: Set (SingleNodeEntry arch bin) } + SyncAtExit { syncPointNode :: SingleNodeEntry arch bin , _syncPointExit :: SingleNodeEntry arch bin } | SyncAtStart { syncPointNode :: SingleNodeEntry arch bin } deriving (Eq, Ord, Show) @@ -570,14 +571,14 @@ mkProcessMerge :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (WorkItem arch) -mkProcessMerge syncAtExits sne1 sne2 +mkProcessMerge syncAtExit sne1 sne2 | dp1 <- singleNodeDivergePoint sne1 , dp2 <- singleNodeDivergePoint sne2 , dp1 == dp2 = case singleEntryBin sne1 of - PBi.OriginalRepr -> case syncAtExits of + PBi.OriginalRepr -> case syncAtExit of True -> Just $ ProcessMergeAtExitsCtor sne1 sne2 False -> Just $ ProcessMergeAtEntryCtor sne1 sne2 - PBi.PatchedRepr -> case syncAtExits of + PBi.PatchedRepr -> case syncAtExit of True -> Just $ ProcessMergeAtExitsCtor sne2 sne1 False -> Just $ ProcessMergeAtEntryCtor sne2 sne1 mkProcessMerge _ _ _ = Nothing @@ -1417,23 +1418,42 @@ getPendingActions lens = do pg <- get return $ (pairGraphPendingActs pg) ^. lens +isCutAddressFor :: + SingleNodeEntry arch bin -> + PAd.ConcreteAddress arch -> + PairGraphM sym arch Bool +isCutAddressFor sne addr = do + cuts <- getSingleNodeData syncCutAddresses sne + return $ Set.member (PPa.WithBin (singleEntryBin sne) addr) cuts isSyncExit :: forall sym arch bin. SingleNodeEntry arch bin -> PB.BlockTarget arch bin -> - PairGraphM sym arch (Maybe (SingleNodeEntry arch bin)) + PairGraphM sym arch (Maybe (SyncPoint arch bin)) isSyncExit sne blkt@(PB.BlockTarget{}) = do - cuts <- getSingleNodeData syncCutAddresses sne excepts <- getSingleNodeData syncExceptions sne syncs <- getSingleNodeData syncPoints sne - let isExcept = Set.member (TupleF2 sne blkt) excepts - let isCutExit = Set.member (PPa.WithBin (singleEntryBin sne) (PB.targetRawPC blkt)) cuts - let exitSyncs = Set.fromList $ catMaybes $ map (\case SyncAtExits sne' _ -> Just sne'; _ -> Nothing) (Set.toList syncs) - let isAlreadySync = Set.member sne exitSyncs - case (not isExcept) && (isCutExit || isAlreadySync) of - True -> return $ Just (mkSingleNodeEntry (singleToNodeEntry sne) (PB.targetCall blkt)) - False -> return Nothing + let isExcept = Set.member (TupleF2 sne blkt) excepts + case isExcept of + True -> return Nothing + False -> isCutAddressFor sne (PB.targetRawPC blkt) >>= \case + True -> do + let sne_tgt = mkSingleNodeEntry (singleToNodeEntry sne) (PB.targetCall blkt) + return $ Just $ SyncAtExit sne sne_tgt + False -> case PB.targetReturn blkt of + Just ret -> do + let sne_tgt = mkSingleNodeEntry (singleToNodeEntry sne) ret + let sync = SyncAtExit sne sne_tgt + -- special case where this block target + -- has already been marked as a sync exit for this node, but + -- exiting to the return point of the target (rather than its call site) + -- (i.e. via 'addReturnPointSync' in order to handle a function stub) + -- In this case, we return that sync point. + case Set.member sync syncs of + True -> return $ Just sync + False -> return Nothing + Nothing -> return Nothing isSyncExit _ _ = return Nothing -- | True if the given node starts at exactly a sync point @@ -1489,11 +1509,7 @@ filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleN let bin = singleEntryBin sne blkts <- mapM (PPa.get bin) blktPairs syncExits <- catMaybes <$> mapM (isSyncExit sne) blkts - unless (null syncExits) $ do - -- if any of the exits from this node are sync exits, - -- then we need to queue up processing this node as - -- a merge against all known merge points - queueExitMerges priority (SyncAtExits sne (Set.fromList syncExits)) + forM_ syncExits $ \exit -> queueExitMerges priority exit return blktPairs -- | Mark the return point of a target as a sync point, if @@ -1516,7 +1532,7 @@ addReturnPointSync priority ne blktPair = case asSingleNodeEntry ne of Set.member (PPa.WithBin (singleEntryBin sne) (PB.concreteAddress ret)) cuts of True -> do let syncExit = mkSingleNodeEntry (singleToNodeEntry sne) ret - queueExitMerges priority (SyncAtExits sne (Set.singleton syncExit)) + queueExitMerges priority (SyncAtExit sne syncExit) False -> return () Nothing -> return () Nothing -> return () @@ -1528,11 +1544,11 @@ queueSyncPoints :: SyncPoint arch (PBi.OtherBinary bin) -> PairGraphM sym arch () queueSyncPoints priority sp1 sp2 = case (sp1, sp2) of - (SyncAtExits _ exits1, SyncAtStart sne2) -> forM_ exits1 $ \exit1 -> do - wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge True exit1 sne2 + (SyncAtExit _ exit1, SyncAtStart sne2) -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge False exit1 sne2 modify $ queueWorkItem (priority PriorityHandleMerge) wi - (SyncAtStart{}, SyncAtExits{}) | Refl <- PBi.otherInvolutive bin -> queueSyncPoints priority sp2 sp1 - (SyncAtExits{}, SyncAtExits{}) -> do + (SyncAtStart{}, SyncAtExit{}) | Refl <- PBi.otherInvolutive bin -> queueSyncPoints priority sp2 sp1 + (SyncAtExit{}, SyncAtExit{}) -> do wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge True (syncPointNode sp1) (syncPointNode sp2) modify $ queueWorkItem (priority PriorityHandleMerge) wi (SyncAtStart{}, SyncAtStart{}) -> do