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 diff --git a/src/Data/Parameterized/PairF.hs b/src/Data/Parameterized/PairF.hs index 3450274f..f5d03ab1 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,22 @@ 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 + +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 665b8533..950a1a26 100644 --- a/src/Data/Parameterized/SetF.hs +++ b/src/Data/Parameterized/SetF.hs @@ -43,10 +43,14 @@ module Data.Parameterized.SetF , union , unions , null + , toSet + , fromSet + , 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 @@ -55,6 +59,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 @@ -91,13 +96,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 => @@ -130,6 +135,25 @@ 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 + +-- | 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) + ppSetF :: (f tp -> PP.Doc a) -> SetF f tp -> 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 diff --git a/src/Pate/Binary.hs b/src/Pate/Binary.hs index 943f1e82..1f03307c 100644 --- a/src/Pate/Binary.hs +++ b/src/Pate/Binary.hs @@ -29,8 +29,11 @@ module Pate.Binary , Patched , WhichBinaryRepr(..) , OtherBinary + , binCases , flipRepr - , short) + , short + , otherInvolutive + ) where import Data.Parameterized.WithRepr @@ -50,16 +53,27 @@ 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 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/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs index f27a7a8a..f82d89d0 100644 --- a/src/Pate/Equivalence/Error.hs +++ b/src/Pate/Equivalence/Error.hs @@ -166,10 +166,11 @@ 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 + | IncompatibleSingletonNodes (PB.ConcreteBlock arch PBi.Original) (PB.ConcreteBlock arch PBi.Patched) | SolverError X.SomeException errShortName :: MS.SymArchConstraints arch => InnerEquivalenceError arch -> String @@ -230,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/Monad/Environment.hs b/src/Pate/Monad/Environment.hs index cbf92d5c..022f7d39 100644 --- a/src/Pate/Monad/Environment.hs +++ b/src/Pate/Monad/Environment.hs @@ -134,6 +134,7 @@ data NodePriorityK = | PriorityDeferredPropagation | PriorityDomainRefresh | PriorityHandleReturn + | PriorityHandleMerge | PriorityMiscCleanup | PriorityDeferred deriving (Eq, Ord) @@ -153,6 +154,7 @@ 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" diff --git a/src/Pate/Monad/PairGraph.hs b/src/Pate/Monad/PairGraph.hs index 5a2897b2..36e1c556 100644 --- a/src/Pate/Monad/PairGraph.hs +++ b/src/Pate/Monad/PairGraph.hs @@ -6,10 +6,17 @@ {-# 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 ( withPG + , evalPG , withPG_ , liftPG , catchPG @@ -23,6 +30,9 @@ module Pate.Monad.PairGraph , considerDesyncEvent , addLazyAction , queuePendingNodes + , runPG + , execPG + , liftPartEqM_ ) where import Control.Monad.State.Strict @@ -52,44 +62,93 @@ 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) +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 => PairGraph sym arch -> StateT (PairGraph sym arch) (EquivM_ sym arch) a -> EquivM sym arch (a, PairGraph sym arch) 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 -> 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 - 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 -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 = 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 => (PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch)) -> 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 :: + 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/PatchPair.hs b/src/Pate/PatchPair.hs index 0d2ef51e..41a8b102 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 @@ -71,6 +72,7 @@ module Pate.PatchPair ( , zip , jsonPatchPair , w4SerializePair + , WithBin(..) ) where import Prelude hiding (zip) @@ -125,6 +127,43 @@ 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 + +-- 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) @@ -136,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" @@ -223,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) @@ -332,6 +361,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/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 diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 87a1a4ac..dfb76701 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(..) @@ -26,6 +27,7 @@ module Pate.Verification.PairGraph , PairGraph , PairGraphM , runPairGraphM + , runPairGraphMLog , execPairGraphM , evalPairGraphM , maybeUpdate @@ -34,10 +36,8 @@ module Pate.Verification.PairGraph , hasWorkLeft , pairGraphWorklist , pairGraphObservableReports - , popWorkItem , updateDomain , updateDomain' - , dropWorkItem , addReturnVector , getReturnVectors , getEdgesFrom @@ -68,19 +68,25 @@ module Pate.Verification.PairGraph , dropReturns , dropPostDomains , markEdge - , getSyncPoints , getBackEdgesFrom - , addSyncNode - , getCombinedSyncPoints , combineNodes , NodePriority(..) , addToWorkList + , WorkItem(ProcessNode, ProcessSplit) + , pattern ProcessMerge + , workItemNode , getQueuedPriority , queueAncestors , queueNode + , queueWorkItem , emptyWorkList + , SyncData , SyncPoint(..) - , updateSyncPoint + , getSyncData + , modifySyncData + , syncPoints + , syncCutAddresses + , syncExceptions , singleNodeRepr , edgeActions , nodeActions @@ -107,23 +113,32 @@ module Pate.Verification.PairGraph , propagateOnce , getPropagationKind , propagateAction - , getSyncAddress - , setSyncAddress - , checkForNodeSync - , checkForReturnSync + , addSyncAddress + -- , filterSyncExits , pairGraphComputeVerdict -- FIXME: remove this and have modules import this directly , module Data.Parameterized.PairF + , handleSingleSidedReturnTo + , filterSyncExits + , isDivergeNode + , mkProcessMerge + , dropWorkItem + , addDesyncExits + , queueSplitAnalysis + , handleKnownDesync + , addReturnPointSync ) 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 (..)) 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 ( (&), (.~), (^.), (%~) ) @@ -132,7 +147,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 @@ -159,7 +174,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 @@ -173,6 +188,11 @@ 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 +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 @@ -233,7 +253,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 @@ -287,20 +307,313 @@ 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]) } +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) + -- | Handle merging two single-sided analyses (both nodes must share a diverge point) + | ProcessMergeAtExitsCtor + (SingleNodeEntry arch PBi.Original) + (SingleNodeEntry arch PBi.Patched) + | 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 +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)) + +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 = + 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 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 + _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 + , _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))) + -- Exits from the corresponding desync node that start the single-sided analysis + , _syncDesyncExits :: PPa.PatchPair (SetF (PB.BlockTarget arch)) + } + +-- sync exit point should *always* point to a cut address +data SyncPoint arch bin = + SyncAtExit { syncPointNode :: SingleNodeEntry arch bin , _syncPointExit :: SingleNodeEntry arch bin } + | SyncAtStart { syncPointNode :: SingleNodeEntry arch bin } + deriving (Eq, Ord, Show) + +syncPointBin :: SyncPoint arch bin -> PBi.WhichBinaryRepr bin +syncPointBin sp = singleEntryBin $ syncPointNode sp + +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) -newtype PairGraphM sym arch a = PairGraphT { unpgT :: ExceptT PEE.PairGraphErr (State (PairGraph sym arch)) a } +instance Semigroup (SyncData arch) where + (SyncData a1 b1 c1 d1) <> (SyncData a2 b2 c2 d2) = (SyncData (a1 <> a2) (b1 <> b2) (c1 <> c2) (d1 <> d2)) + + +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) + (PPa.mkPair PBi.OriginalRepr SetF.empty SetF.empty) + +$(L.makeLenses ''SyncData) +$(L.makeLenses ''ActionQueue) + +type ActionQueueLens sym arch k v = L.Lens' (ActionQueue sym arch) (Map k [PendingAction sym arch v]) + +getSyncData :: + forall sym arch x bin. + HasCallStack => + (OrdF x, Ord (x bin)) => + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + PairGraphM sym arch (Set (x bin)) +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 + +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' (SyncData arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch -> + (Set (x bin) -> Set (x bin)) -> + PairGraphM sym arch () +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 { pairGraphSyncData = Map.insert dp sp' (pairGraphSyncData pg)} + +addToSyncData :: + forall sym arch x bin. + (OrdF x, Ord (x bin)) => + HasCallStack => + L.Lens' (SyncData arch) (PPa.PatchPair (SetF x)) -> + PBi.WhichBinaryRepr bin -> + GraphNode arch {- ^ The divergent node -} -> + x bin -> + PairGraphM sym arch () +addToSyncData lens bin nd x = modifySyncData 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 = 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) + +-- | 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 blkt = fmap (fromMaybe False) $ tryPG $ do + let dp = GraphNode ne + 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 + +-- | 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 :: + Bool -> + SingleNodeEntry arch bin -> + SingleNodeEntry arch (PBi.OtherBinary bin) -> + Maybe (WorkItem arch) +mkProcessMerge syncAtExit sne1 sne2 + | dp1 <- singleNodeDivergePoint sne1 + , dp2 <- singleNodeDivergePoint sne2 + , dp1 == dp2 = case singleEntryBin sne1 of + PBi.OriginalRepr -> case syncAtExit of + True -> Just $ ProcessMergeAtExitsCtor sne1 sne2 + False -> Just $ ProcessMergeAtEntryCtor sne1 sne2 + PBi.PatchedRepr -> case syncAtExit of + True -> Just $ ProcessMergeAtExitsCtor sne2 sne1 + 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 = 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 @@ -314,25 +627,42 @@ 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] -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') +pgValid :: (PA.ValidArch arch => PairGraphM sym arch a) -> PairGraphM sym arch a +pgValid f = do + PairGraphEnv <- PairGraphM ask + f -execPairGraphM :: PairGraph sym arch -> PairGraphM sym arch a -> Either PEE.PairGraphErr (PairGraph sym arch) +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 :: 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 :: 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 lookupPairGraph :: forall sym arch b. + HasCallStack => (PairGraph sym arch -> Map (GraphNode arch) b) -> GraphNode arch -> PairGraphM sym arch b @@ -340,24 +670,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 @@ -411,18 +723,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 -> @@ -443,33 +743,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.PatchPairC (Set (GraphNode arch)) - , syncCutAddresses :: PPa.PatchPairC (PAd.ConcreteAddress arch) - } - ppProgramDomains :: forall sym arch a. ( PA.ValidArch arch @@ -505,7 +778,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 } @@ -551,8 +824,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 -> @@ -615,9 +887,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'' @@ -642,6 +914,40 @@ 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__) +-- | 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. +-- 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 + ProcessMerge spO spP -> + let + 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) -> queueAncestors (raisePriority priority) neP (addItemToWorkList wi priority pg) + (Nothing, Just{}) -> queueAncestors (raisePriority priority) neO (addItemToWorkList wi priority pg) + (Nothing, Nothing) -> + 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 + +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 queueNode' :: NodePriority -> GraphNode arch -> (Set (GraphNode arch), PairGraph sym arch) -> (Set (GraphNode arch), PairGraph sym arch) @@ -776,25 +1082,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 @@ -802,21 +1096,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 (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 -- work list is empty, return Nothing, indicating that we are done. chooseWorkItem :: PA.ValidArch arch => PairGraph sym arch -> - Maybe (NodePriority, PairGraph sym arch, GraphNode 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 (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) + 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 <- 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 + -- 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. @@ -857,7 +1179,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,121 +1235,38 @@ 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 pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg -getSyncPoints :: - forall sym arch bin. - PBi.WhichBinaryRepr bin -> - GraphNode arch -> - PairGraphM sym arch (Set (GraphNode arch)) -getSyncPoints bin nd = do - (SyncPoint syncPair _) <- lookupPairGraph @sym pairGraphSyncPoints nd - PPa.getC bin syncPair - -getSyncAddress :: - forall sym arch bin. - 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 - -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. - GraphNode arch -> - PairGraphM sym arch ([((GraphNode arch, GraphNode arch), 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 - 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? -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 - GraphNode divergeO <- divergePoint $ nodeContext nodeO - GraphNode 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') - -- FIXME: retain calling context? - return $ GraphNode $ mkNodeEntry divergeO (PPa.PatchPair 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) - _ -> Nothing + return $ GraphNode $ mkMergedNodeEntry divergeO (singleNodeBlock nodeO) (singleNodeBlock nodeP) singleNodeRepr :: GraphNode arch -> Maybe (Some (PBi.WhichBinaryRepr)) singleNodeRepr nd = case graphNodeBlocks nd of PPa.PatchPairSingle bin _ -> return $ Some bin PPa.PatchPair{} -> Nothing -addSyncNode :: - forall sym arch. - GraphNode arch {- ^ The divergent node -} -> - GraphNode arch {- ^ the sync node -} -> - PairGraphM sym arch () -addSyncNode ndDiv ndSync = do - Pair bin _ <- PPa.asSingleton (graphNodeBlocks ndSync) - let ndSync' = PPa.PatchPairSingle bin (Const 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')) - 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 :: - 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 (Const Set.empty) (Const Set.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 -- an existing abstract domain for it. Otherwise return Nothing. @@ -1037,12 +1276,30 @@ 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 $ 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) } + +-- | 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 'WorkItem' getQueuedPriority :: - GraphNode arch -> PairGraph sym arch -> Maybe NodePriority -getQueuedPriority nd pg = RevMap.lookup 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 } @@ -1057,7 +1314,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 :: @@ -1119,12 +1376,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 -> @@ -1167,47 +1418,171 @@ 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))] -> +isCutAddressFor :: + SingleNodeEntry arch bin -> + PAd.ConcreteAddress 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) - 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 - -- 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 -> - NodeEntry arch -> +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 (SyncPoint arch bin)) +isSyncExit sne blkt@(PB.BlockTarget{}) = do + excepts <- getSingleNodeData syncExceptions sne + syncs <- getSingleNodeData syncPoints sne + 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 +isZeroStepSync :: + forall sym arch bin. + SingleNodeEntry arch bin -> 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 +isZeroStepSync sne = do + cuts <- getSingleNodeData syncCutAddresses sne + let addr = PB.concreteAddress $ singleNodeBlock sne + 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 +-- 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) -> + WorkItem arch -> + [PPa.PatchPair (PB.BlockTarget arch)] -> + PairGraphM sym arch [PPa.PatchPair (PB.BlockTarget arch)] +filterSyncExits _ (ProcessNode (ReturnNode{})) _ = fail "Unexpected ReturnNode work item" +filterSyncExits _ (ProcessMergeAtExits 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 +-- 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 + isZeroStepSync sne >>= \case + True -> do + queueExitMerges priority (SyncAtStart sne) + return [] + False -> do + let bin = singleEntryBin sne + desyncExits <- getSingleNodeData syncDesyncExits sne + let isDesyncExitPair blktPair = do + blkt <- PPa.get bin blktPair + return $ Set.member blkt desyncExits + x <- filterM isDesyncExitPair blktPairs + return x +filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of + Nothing -> return blktPairs + Just (Some sne) -> do + let bin = singleEntryBin sne + blkts <- mapM (PPa.get bin) blktPairs + syncExits <- catMaybes <$> mapM (isSyncExit sne) blkts + forM_ syncExits $ \exit -> queueExitMerges priority exit + 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 (SyncAtExit sne syncExit) + False -> return () + Nothing -> return () + Nothing -> return () + + +queueSyncPoints :: + (NodePriorityK -> NodePriority) -> + SyncPoint arch bin -> + SyncPoint arch (PBi.OtherBinary bin) -> + PairGraphM sym arch () +queueSyncPoints priority sp1 sp2 = case (sp1, sp2) of + (SyncAtExit _ exit1, SyncAtStart sne2) -> do + wi <- pgMaybe "unexpected node merge failure" $ mkProcessMerge False exit1 sne2 + modify $ queueWorkItem (priority PriorityHandleMerge) wi + (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 + 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. +-- This will be handled specially +handleSingleSidedReturnTo :: + (NodePriorityK -> NodePriority) -> + NodeEntry arch -> + PairGraphM sym arch () +handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of + Just (Some sne) -> do + 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) + 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 28d3991e..2b1156af 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 #-} @@ -24,10 +25,12 @@ module Pate.Verification.PairGraph.Node ( , pattern GraphNodeEntry , pattern GraphNodeReturn , nodeContext + , graphNodeContext , divergePoint , graphNodeBlocks , mkNodeEntry , mkNodeEntry' + , mkSingleNodeEntry , addContext , mkNodeReturn , rootEntry @@ -46,6 +49,17 @@ module Pate.Verification.PairGraph.Node ( , splitGraphNode , getDivergePoint , eqUptoDivergePoint + , mkMergedNodeEntry + , mkMergedNodeReturn + , SingleNodeEntry + , singleEntryBin + , singleNodeDivergePoint + , asSingleNodeEntry + , singleToNodeEntry + , singleNodeBlock + , combineSingleEntries + , singleNodeDivergence + , toSingleNodeEntry ) where import Prettyprinter ( Pretty(..), sep, (<+>), Doc ) @@ -61,6 +75,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 @@ -88,28 +105,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 #-} @@ -150,15 +187,44 @@ 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 +294,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 +374,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 @@ -316,3 +387,98 @@ 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) + } + +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 + +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) + +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 + case divergePoint cctx of + 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 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)) = + NodeEntry cctx (PPa.PatchPairSingle bin v) + +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"] + +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) + +-- | 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 a6f5df72..1c623655 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 @@ -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 import Pate.Verification.Widening import qualified Pate.Verification.AbstractDomain as PAD import Data.Monoid (All(..), Any (..)) @@ -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 -- @@ -366,31 +367,13 @@ 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_) + err <- emitError' (PEE.OrphanedSinglesidedAnalysis fn_single_) return $ recordMiscAnalysisError pg0 (ReturnNode ret) err - - foldM go pg single_rets + foldM go pg single_rets -handleSyncPoint :: - GraphNode 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 - addSyncNode divergeNode nd - return divergeNode - liftEqM_ $ updateCombinedSyncPoint divergeNode addressOfNode :: GraphNode arch -> @@ -425,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:" @@ -441,25 +424,27 @@ 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 $ setSyncAddress 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 + 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:" +{- +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 :: @@ -505,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 :: @@ -543,157 +543,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 nd) syncsO_ - syncsP <- fmap catMaybes $ mapM (\nd -> catchPG $ fmap (nd,) $ getCurrentDomainM 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) 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 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 - - -- 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" syncO - emitTrace @"node" syncP - 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,61 +564,210 @@ addImmediateEqDomRefinementChoice nd preD gr0 = do choice ("No refinements") () $ return gr1 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 -} -> - GraphNode arch {- ^ combined sync node -} -> +-- | 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 :: + SingleNodeEntry arch bin -> + PairGraph sym arch -> + EquivM sym arch (PairGraph sym arch) +initSingleSidedDomain sne pg0 = withPG_ pg0 $ do + priority <- lift $ thisPriority + 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 + dom_single <- PAD.singletonDomain bin dom + {- + case getCurrentDomain pg0 nd_single of + Just{} -> return () + Nothing -> do + 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 -> 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) -mergeDualNodes in1 in2 spec1 spec2 syncNode gr0 = fnTrace "mergeDualNodes" $ withSym $ \sym -> do - let gr2 = gr0 - - 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 +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 -> + 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 + 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 + 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 + 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 + dom_spec <- liftPG $ getCurrentDomainM (GraphNode syncNode) + return $ Just (GraphNode syncNode, dom_spec) + _ -> do + liftPG $ modify $ queueNode (priority PriorityDomainRefresh) divergeNode + 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 domO ndO pg $ + withConditionsAssumed scope bundle domP ndP pg $ do emitTraceLabel @"domain" PAD.Predomain (Some dom) - widenAlongEdge scope bundle in2 dom gr2 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) 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 - 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) + 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 -> 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 gr2 -> withWorkItem gr2 f + (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 -{- - 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 @@ -782,7 +780,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) @@ -796,7 +795,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 @@ -1219,13 +1218,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 @@ -1235,19 +1238,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 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 - 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 @@ -1344,11 +1350,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 @@ -1363,21 +1369,10 @@ visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 = priority <- thisPriority 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 (GraphNode 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 + 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 -- all of the known call sites of this function. let rets = getReturnVectors gr0 fPair @@ -1399,9 +1394,8 @@ visitNode scope (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 @@ -1409,6 +1403,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 @@ -1418,7 +1413,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" @@ -1432,10 +1426,28 @@ 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 (GraphNode node) - False -> return () - + 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 @@ -2093,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 -> - NodeEntry arch -> + WorkItem arch -> Bool -checkNodeRequeued st node = fromMaybe False $ do - bc <- branchDesyncChoice st +checkNodeRequeued stPre stPost wi = fromMaybe False $ do + bc <- branchDesyncChoice stPost return $ choiceRequiresRequeue bc - <|> (getQueuedPriority (GraphNode node) (branchGraph st) >> return True) + <|> do + Nothing <- return $ getQueuedPriority wi stPre + _ <- getQueuedPriority wi (branchGraph stPost) + return True followExit :: PS.SimScope sym arch v -> @@ -2253,6 +2269,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 @@ -2275,7 +2292,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 @@ -2590,6 +2609,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. @@ -2603,8 +2625,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 @@ -2625,6 +2647,7 @@ handleSplitAnalysis scope node dom pg = do emitTraceLabel @"address" "Synchronization Address" syncP return $ Just pg' Left{} -> return Nothing +-} handleDivergingPaths :: HasCallStack => @@ -2641,72 +2664,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 - -- 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 - 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 @@ -2767,6 +2797,7 @@ instance Show DesyncChoice where choiceRequiresRequeue :: DesyncChoice -> Bool choiceRequiresRequeue = \case AdmitNonTotal -> False + ChooseSyncPoint -> False _ -> True handleStub :: diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index d55d3998..3941dfa2 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) @@ -811,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 @@ -837,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, @@ -1676,7 +1637,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 :: diff --git a/tests/AArch32TestMain.hs b/tests/AArch32TestMain.hs index 8add9790..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-zerostep", "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..0b863df2 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, 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 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-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 fd317210..d91d3558 100644 --- a/tests/aarch32/desync-orphan-return.pate +++ b/tests/aarch32/desync-orphan-return.pate @@ -25,7 +25,8 @@ 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, 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.original.exe b/tests/aarch32/desync-zerostep.original.exe index fff50d8c..0dcb57ba 100755 Binary files a/tests/aarch32/desync-zerostep.original.exe and b/tests/aarch32/desync-zerostep.original.exe differ diff --git a/tests/aarch32/desync-zerostep.patched.exe b/tests/aarch32/desync-zerostep.patched.exe index 7604018b..b910d3d2 100755 Binary files a/tests/aarch32/desync-zerostep.patched.exe and b/tests/aarch32/desync-zerostep.patched.exe differ diff --git a/tests/aarch32/desync-zerostep.pate b/tests/aarch32/desync-zerostep.pate index 1051f0c3..29718ec0 100644 --- a/tests/aarch32/desync-zerostep.pate +++ b/tests/aarch32/desync-zerostep.pate @@ -3,37 +3,40 @@ Choose Entry Point Function Entry "f" ... - Call to: "puts" (0x10108) Returns to: "f" + Call to: "puts" (0x10110) Returns to: "f" ... ... > 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/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 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: 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); }