From 4132a6678c058187fcc64cc97e674db3245e85b8 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 27 Feb 2024 12:04:08 -0800 Subject: [PATCH 1/5] Pate.EventTrace: add general-purpose sequence comparisons These are to be used to compare instruction traces of original vs. patched CFARs. Also refactor 'zipSeq' to use caching --- src/Pate/EventTrace.hs | 187 ++++++++++++++++++++++++++++++++++------- 1 file changed, 157 insertions(+), 30 deletions(-) diff --git a/src/Pate/EventTrace.hs b/src/Pate/EventTrace.hs index a4bf2f53..336239d9 100644 --- a/src/Pate/EventTrace.hs +++ b/src/Pate/EventTrace.hs @@ -49,6 +49,8 @@ module Pate.EventTrace , takeMatchingPrefix2 , reverseSeq , collapsePartialSeq +, compareSymSeq +, concatSymSequence ) where import Prettyprinter @@ -81,9 +83,12 @@ import qualified Pate.ExprMappable as PEM import qualified Pate.SimulatorRegisters as PSr import qualified Data.Parameterized.TraversableFC as TFC import qualified Pate.Pointer as Ptr -import Control.Monad (forM) +import Control.Monad (forM, foldM) import Data.Maybe (catMaybes) import What4.Partial (PartExpr, pattern Unassigned, pattern PE) +import qualified Data.IORef as IO +import qualified Data.Map as Map +import Data.Parameterized.Nonce -- Needed since SymBV is a type alias newtype SymBV' sym w = SymBV' { unSymBV :: SymBV sym w } @@ -565,60 +570,122 @@ muxSeqM3 sym p f_s1 f_s2 = case asConstantPred p of c <- muxSymSequence' sym p c1 c2 return $ (a,b,c) --- | Zip two sequences pointwise. If one is longer than the other, return --- the suffix of elements. --- Notably this is not an 'Either' result (i.e. returning only the suffix of the longer sequence), --- as both suffixes may be nontrivial and symbolic. --- TODO: not obvious how to handle caching here -zipSeq :: + +-- TODO: This is a duplicate of Pate.Verification.StrongestPosts.SeqPairCache +-- Replacing 'equivalentSequences' in that module with 'compareSymSeq' will also +-- let us remove the duplicates there +data SeqPairCache a b c = SeqPairCache (IO.IORef (Map.Map (Maybe (Nonce GlobalNonceGenerator a), Maybe (Nonce GlobalNonceGenerator b)) c)) + +newSeqPairCache :: IO (SeqPairCache a b c) +newSeqPairCache = SeqPairCache <$> IO.newIORef Map.empty + +-- TODO: clagged from SymSequence module, should probably be exported, either +-- directly or with some abstraction for the nonces +symSequenceNonce :: SymSequence sym a -> Maybe (Nonce GlobalNonceGenerator a) +symSequenceNonce SymSequenceNil = Nothing +symSequenceNonce (SymSequenceCons n _ _ ) = Just n +symSequenceNonce (SymSequenceAppend n _ _) = Just n +symSequenceNonce (SymSequenceMerge n _ _ _) = Just n + +-- TODO: duplicated in Pate.Verification.StrongestPosts, see above +evalWithPairCache :: IO.MonadIO m => + SeqPairCache a b c -> + SymSequence sym a -> + SymSequence sym b -> + m c -> + m c +evalWithPairCache (SeqPairCache ref) seq1 seq2 f = do + m <- IO.liftIO (IO.readIORef ref) + let k = (symSequenceNonce seq1, symSequenceNonce seq2) + case Map.lookup k m of + Just v -> return v + Nothing -> do + v <- f + IO.liftIO (IO.modifyIORef ref (Map.insert k v)) + return v + +zipSeq' :: forall sym a b. - IsExprBuilder sym => + IsSymExprBuilder sym => sym -> + SeqPairCache a b (SymSequence sym (a,b), SymSequence sym a, SymSequence sym b) -> SymSequence sym a -> SymSequence sym b -> IO (SymSequence sym (a,b), SymSequence sym a, SymSequence sym b) -zipSeq sym as_outer bs_outer = go SymSequenceNil as_outer bs_outer +zipSeq' sym cache as_outer bs_outer = go as_outer bs_outer where handle_append :: forall x y. - (SymSequence sym (a,b) -> SymSequence sym x -> SymSequence sym y -> IO (SymSequence sym (a,b), SymSequence sym x, SymSequence sym y)) -> - SymSequence sym (a,b) -> + (SymSequence sym x -> SymSequence sym y -> IO (SymSequence sym (a,b), SymSequence sym x, SymSequence sym y)) -> SymSequence sym x -> SymSequence sym y -> Maybe (IO (SymSequence sym (a,b), SymSequence sym x, SymSequence sym y)) - handle_append rec acc xs@(SymSequenceAppend _ xs_1 xs_2) ys = Just $ do - (acc', xs_suf', ys_suf) <- rec acc xs_1 ys + handle_append rec xs@(SymSequenceAppend _ xs_1 xs_2) ys = Just $ do + (acc, xs_suf', ys_suf) <- rec xs_1 ys p <- isNilSymSequence sym xs_suf' - muxSeqM3 sym p + (acc', xs_fin, ys_fin) <- muxSeqM3 sym p -- if xs_suf' is nil then it means we consumed all of the first -- and thus we can continue zipping elements - (rec acc' xs_2 ys_suf) $ do + (do + (acc', xs_fin, ys_fin) <- rec xs_2 ys_suf + return (acc', xs_fin, ys_fin) + ) $ do -- otherwise, we append the tail to the found suffix and return -- as a small optimization, if the suffix is the same as the input -- then we don't need to create a new sequence for appended suffix xs_suf'' <- if xs_suf' == xs_1 then return xs else appendSymSequence sym xs_suf' xs_2 - return $ (acc', xs_suf'', ys_suf) + return $ (SymSequenceNil, xs_suf'', ys_suf) + acc'' <- appendSymSequence sym acc acc' + return (acc'', xs_fin, ys_fin) - handle_append _ _ _ _ = Nothing - go' :: SymSequence sym (a,b) -> SymSequence sym b -> SymSequence sym a -> IO (SymSequence sym (a,b), SymSequence sym b, SymSequence sym a) - go' acc s_b s_a = go acc s_a s_b >>= \(acc', s_a', s_b') -> return (acc', s_b', s_a') + handle_append _ _ _ = Nothing + go' :: SymSequence sym b -> SymSequence sym a -> IO (SymSequence sym (a,b), SymSequence sym b, SymSequence sym a) + go' s_b s_a = go s_a s_b >>= \(acc, s_a', s_b') -> return (acc, s_b', s_a') - go :: SymSequence sym (a,b) -> SymSequence sym a -> SymSequence sym b -> IO (SymSequence sym (a,b), SymSequence sym a, SymSequence sym b) - go acc s_a s_b = case (s_a, s_b) of + go :: SymSequence sym a -> SymSequence sym b -> IO (SymSequence sym (a,b), SymSequence sym a, SymSequence sym b) + go s_a s_b = evalWithPairCache cache s_a s_b $ case (s_a, s_b) of -- if either sequence is nil that we can't extend the matching prefix any more -- and so we return - (_, SymSequenceNil) -> return $ (acc, s_a, s_b) - (SymSequenceNil, _) -> return $ (acc, s_a, s_b) + (_, SymSequenceNil) -> return $ (SymSequenceNil, s_a, s_b) + (SymSequenceNil, _) -> return $ (SymSequenceNil, s_a, s_b) (SymSequenceCons _ a s_a', SymSequenceCons _ b s_b') -> do + + (acc, suf_a, suf_b) <- go s_a' s_b' acc' <- IO.liftIO $ appendSingle sym acc (a,b) - go acc' s_a' s_b' - _ | Just g <- handle_append go acc s_a s_b -> g - _ | Just g <- handle_append go' acc s_b s_a -> g >>= \(acc', s_b', s_a') -> return (acc', s_a', s_b') - (SymSequenceMerge _ p a_T a_F, _) -> muxSeqM3 sym p (go acc a_T s_b) (go acc a_F s_b) - (_, SymSequenceMerge _ p b_T b_F) -> muxSeqM3 sym p (go acc s_a b_T) (go acc s_a b_F) + return (acc', suf_a, suf_b) + _ | Just g <- handle_append go s_a s_b -> g + _ | Just g <- handle_append go' s_b s_a -> g >>= \(acc', s_b', s_a') -> return (acc', s_a', s_b') + (SymSequenceMerge _ p_a a_T a_F, SymSequenceMerge _ p_b b_T b_F) + | Just Refl <- testEquality p_a p_b -> muxSeqM3 sym p_a (go a_T b_T) (go a_F b_F) + (SymSequenceMerge _ p_a a_T a_F, SymSequenceMerge _ p_b b_T b_F) -> do + p_a_p_b <- andPred sym p_a p_b + not_p_a <- notPred sym p_a + not_p_b <- notPred sym p_b + not_p_a_not_p_b <- andPred sym not_p_a not_p_b + + muxSeqM3 sym p_a_p_b (go a_T b_T) $ + muxSeqM3 sym not_p_a_not_p_b (go a_F b_F) $ + muxSeqM3 sym p_a (go a_T b_F) (go a_F b_T) + + (SymSequenceMerge _ p a_T a_F, _) -> muxSeqM3 sym p (go a_T s_b) (go a_F s_b) + (_, SymSequenceMerge _ p b_T b_F) -> muxSeqM3 sym p (go s_a b_T) (go s_a b_F) (SymSequenceAppend{}, _) -> error "zipSeq: handle_append unexpectedly failed" (_, SymSequenceAppend{}) -> error "zipSeq: handle_append unexpectedly failed" + +-- | Zip two sequences pointwise. If one is longer than the other, return +-- the suffix of elements. +-- Notably this is not an 'Either' result (i.e. returning only the suffix of the longer sequence), +-- as both suffixes may be nontrivial and symbolic. +zipSeq :: + forall sym a b. + IsSymExprBuilder sym => + sym -> + SymSequence sym a -> + SymSequence sym b -> + IO (SymSequence sym (a,b), SymSequence sym a, SymSequence sym b) +zipSeq sym as bs = newSeqPairCache >>= \cache -> zipSeq' sym cache as bs + unzipSeq :: forall sym a b. IsExprBuilder sym => @@ -696,7 +763,7 @@ collapsePartialSeq sym s_outer = mapConcatSeq sym (partToSeq sym) s_outer -- TODO: caching? takeMatchingPrefix2 :: forall sym m a b c. - IsExprBuilder sym => + IsSymExprBuilder sym => IO.MonadIO m => sym -> (a -> b -> m (PartExpr (Pred sym) c)) -> @@ -731,4 +798,64 @@ reverseSeq sym s_outer = evalWithFreshCache go s_outer go rec (SymSequenceMerge _ p sT sF) = do sT_rev <- rec sT sF_rev <- rec sF - muxSymSequence sym p sT_rev sF_rev \ No newline at end of file + muxSymSequence sym p sT_rev sF_rev + +-- | Concatenate the elements of a 'SymSequence' together +-- using the provided combine and mux operations and +-- empty value. +concatSymSequence :: + forall sym m c. + IsExprBuilder sym => + IO.MonadIO m => + sym -> + (Pred sym -> c -> c -> m c) {-^ mux for 'c' -} -> + (c -> c -> m c) {-^ combining 'c' values -} -> + c {-^ empty c -} -> + SymSequence sym c -> + m c +concatSymSequence _sym f g c_init s_outer = getConst <$> evalWithFreshCache go s_outer + where + go :: (SymSequence sym c -> m ((Const c) c)) -> SymSequence sym c -> m ((Const c) c) + go rec s = fmap Const $ case s of + SymSequenceNil -> return $ c_init + SymSequenceCons _ c1 sa -> do + Const c2 <- rec sa + g c1 c2 + SymSequenceAppend _ sa1 sa2 -> do + Const c1 <- rec sa1 + Const c2 <- rec sa2 + g c1 c2 + SymSequenceMerge _ p' saT saF -> do + Const cT <- rec saT + Const cF <- rec saF + f p' cT cF + +-- | Pointwise comparison of two sequences. When they are (semantically) not +-- the same length, the resulting predicate is False. Otherwise it is +-- the result of 'f' on each pair of values. +-- TODO: Pate.Verification.StrongestPosts.equivalentSequences should be +-- replaced with this. They are semantically equivalent, however +-- 'zipSeq' creates more concise terms in cases where the predicates +-- for sequence merges aren't exactly equivalent between the two sequences. + +compareSymSeq :: + forall sym a b m. + IsSymExprBuilder sym => + IO.MonadIO m => + sym -> + SymSequence sym a -> + SymSequence sym b -> + (a -> b -> m (Pred sym)) -> + m (Pred sym) +compareSymSeq sym sa sb f = do + (matching_pfx, suf_a, suf_b) <- IO.liftIO $ zipSeq sym sa sb + f_seq <- traverseSymSequence sym (\(a,b) -> f a b) matching_pfx + nil_a <- IO.liftIO $ isNilSymSequence sym suf_a + nil_b <- IO.liftIO $ isNilSymSequence sym suf_b + + matching_head <- concatSymSequence sym + (\p a b -> IO.liftIO $ baseTypeIte sym p a b) + (\a b -> IO.liftIO $ andPred sym a b) + (truePred sym) + f_seq + IO.liftIO $ andPred sym matching_head nil_a >>= andPred sym nil_b From 01592a15cadc5f393f00c45c3e5361a60c1462c4 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Tue, 27 Feb 2024 12:28:20 -0800 Subject: [PATCH 2/5] Add control flow alignment as strategy for handling diverging control flow This adds an additional set of actions for adding an assumption/assertion/equivalence condition stating that both the original and patched CFARs execute the exact same instructions in the same order. This is intended to handle the common case where the analysis has proceeded past the location of the patch and is now discovering control flow divergences that are a result of the equivalence domain being weakened from exact equality. These divergences are either spurious and can be resolved by asserting control flow alignment, or are actual differences introduced by the patch and can be resolved by adding control flow alignment as an equivalence condition at this point. --- src/Pate/Verification/PairGraph.hs | 3 +- src/Pate/Verification/StrongestPosts.hs | 50 ++++++++++++++++++++++--- src/Pate/Verification/Widening.hs | 2 + 3 files changed, 49 insertions(+), 6 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index db8ca953..b5cfe3fd 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -424,7 +424,7 @@ conditionAction :: ConditionKind -> String conditionAction = \case ConditionAsserted{} -> "Assert" ConditionAssumed{} -> "Assume" - ConditionEquiv{} -> "Assume (Equivalence Condition)" + ConditionEquiv{} -> "Assume as equivalence condition" data DomainRefinementKind = @@ -436,6 +436,7 @@ data DomainRefinementKind = data DomainRefinement sym arch = LocationRefinement ConditionKind DomainRefinementKind (PL.SomeLocation sym arch -> Bool) | PruneBranch ConditionKind + | AlignControlFlowRefinment ConditionKind addDomainRefinement :: GraphNode arch -> diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index aea46042..674d4a8a 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -130,6 +130,8 @@ import qualified Data.Macaw.BinaryLoader as MBL import What4.Partial (justPartExpr) import qualified Data.Aeson as JSON import qualified Pate.Solver as PSo +import qualified Pate.EventTrace as ET +import Control.Exception (throw) -- Overall module notes/thoughts -- @@ -2482,17 +2484,52 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi -- doesn't need synchronization Just pg1 <- return $ addToWorkList divergeNode (priority PriorityDeferred) pg return $ st'{ branchGraph = pg1 } - -data DesyncChoice = AdmitNonTotal | IsInfeasible ConditionKind | ChooseDesyncPoint | ChooseSyncPoint | DeferDecision + 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 here. + -- It can be simplified later outside of this context, once it has been + -- added to the assumptions for the node + traces_eq <- ET.compareSymSeq sym traceO traceP $ \evO evP -> + return $ W4.backendPred sym (ET.instrDisassembled evO == ET.instrDisassembled evP) + 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 } + +bundleToInstrTraces :: + PS.SimBundle sym arch v -> + EquivM sym arch (PPa.PatchPairC (ET.InstructionTrace sym arch)) +bundleToInstrTraces bundle = withSym $ \sym -> PPa.forBinsC $ \bin -> do + out_ <- PPa.get bin (simOut bundle) + let evt = MT.memFullSeq (PS.simOutMem out_) + IO.liftIO $ ET.asInstructionTrace sym evt + +data DesyncChoice = + AdmitNonTotal + | IsInfeasible ConditionKind + | ChooseDesyncPoint + | ChooseSyncPoint + | DeferDecision + | AlignControlFlow ConditionKind deriving (Eq,Ord) allDesyncChoice :: [DesyncChoice] allDesyncChoice = [AdmitNonTotal - , IsInfeasible ConditionAsserted, IsInfeasible ConditionAssumed, IsInfeasible ConditionEquiv - , ChooseDesyncPoint + ] ++ map IsInfeasible [minBound..maxBound] + ++ + [ ChooseDesyncPoint , ChooseSyncPoint - , DeferDecision] + , DeferDecision + ] ++ map AlignControlFlow [minBound..maxBound] instance Bounded DesyncChoice where minBound = head allDesyncChoice @@ -2511,6 +2548,9 @@ instance Show DesyncChoice where IsInfeasible ConditionAssumed -> "Assume divergence is infeasible" IsInfeasible ConditionEquiv -> "Remove divergence in equivalence condition" DeferDecision -> "Defer decision" + AlignControlFlow ConditionEquiv -> "Align control flow in equivalence condition" + AlignControlFlow condK -> conditionAction condK ++ " control flow alignment" + choiceRequiresRequeue :: DesyncChoice -> Bool choiceRequiresRequeue = \case diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 5a1efe95..34932d46 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -31,6 +31,7 @@ module Pate.Verification.Widening , InteractiveBundle(..) , getSomeGroundTrace , getTraceFromModel + , addToEquivCondition ) where import GHC.Stack @@ -87,6 +88,7 @@ import qualified Pate.Verification.Simplify as PSi import Pate.Monad import qualified Pate.Memory.MemTrace as MT +import qualified Pate.EventTrace as ET import qualified Pate.PatchPair as PPa import qualified Pate.SimState as PS From a1225edbbadee340e6227f7be8c83c92d34229f5 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 28 Feb 2024 09:28:50 -0800 Subject: [PATCH 3/5] Add "--ignore-warnings" command line flag Note that this just prevents warnings from being shown in the TraceTree or emitted in the log. Warnings that affect verification (e.g. non-total block exits) will still affect the final result. --- src/Pate/CLI.hs | 8 +++++++- src/Pate/Config.hs | 2 ++ src/Pate/Equivalence/Error.hs | 11 +++++++++++ src/Pate/Monad.hs | 18 +++++++++++------- src/Pate/Verification/PairGraph.hs | 11 +++++------ 5 files changed, 36 insertions(+), 14 deletions(-) diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs index 484279bd..7d1b67fe 100644 --- a/src/Pate/CLI.hs +++ b/src/Pate/CLI.hs @@ -95,6 +95,7 @@ mkRunConfig archLoader opts mtt = let , PC.cfgScriptPath = scriptPath opts , PC.cfgTraceTree = fromMaybe noTraceTree mtt , PC.cfgStackScopeAssume = not $ noAssumeStackScope opts + , PC.cfgIgnoreWarnings = ignoreWarnings opts } cfg = PL.RunConfig { PL.archLoader = archLoader @@ -144,6 +145,7 @@ data CLIOptions = CLIOptions , readOnlySegments :: [Int] , scriptPath :: Maybe FilePath , noAssumeStackScope :: Bool + , ignoreWarnings :: [String] } deriving (Eq, Ord, Show) printAtVerbosity @@ -456,4 +458,8 @@ cliOptions = OA.info (OA.helper <*> parser) <*> OA.switch ( OA.long "no-assume-stack-scope" <> OA.help "Don't add additional assumptions about stack frame scoping" - ) \ No newline at end of file + ) + <*> OA.many (OA.strOption + ( OA.long "ignore-warnings" + <> OA.help "Don't raise any of the given warning types" + )) \ No newline at end of file diff --git a/src/Pate/Config.hs b/src/Pate/Config.hs index 882ffd98..50bb4e3a 100644 --- a/src/Pate/Config.hs +++ b/src/Pate/Config.hs @@ -281,6 +281,7 @@ data VerificationConfig validRepr = -- ^ true if out-of-scope stack slots should always be considered equal once -- returning from a function (i.e. differences in these slots are implicitly ignored) , cfgScriptPath :: Maybe FilePath + , cfgIgnoreWarnings :: [String] } @@ -305,4 +306,5 @@ defaultVerificationCfg = , cfgRescopingFailureMode = ThrowOnEqRescopeFailure , cfgStackScopeAssume = True , cfgScriptPath = Nothing + , cfgIgnoreWarnings = [] } diff --git a/src/Pate/Equivalence/Error.hs b/src/Pate/Equivalence/Error.hs index 4140e0d1..6f2fd72e 100644 --- a/src/Pate/Equivalence/Error.hs +++ b/src/Pate/Equivalence/Error.hs @@ -29,6 +29,7 @@ module Pate.Equivalence.Error ( , loaderError , someExpr , PairGraphErr(..) + , errShortName ) where import qualified Control.Exception as X @@ -76,6 +77,11 @@ data InnerSymEquivalenceError sym arch = forall tp pre post. RescopingFailure (PAS.AssumptionSet sym) (PS.ScopedExpr sym pre tp) (PS.ScopedExpr sym post tp) | AssumedFalse (PAS.AssumptionSet sym) (PAS.AssumptionSet sym) +symErrShortName :: InnerSymEquivalenceError sym arch -> String +symErrShortName = \case + RescopingFailure{} -> "RescopingFailure" + AssumedFalse{} -> "AssumedFalse" + deriving instance W4.IsExprBuilder sym => Show (InnerSymEquivalenceError sym arch) pattern InnerSymEquivalenceError :: (sym ~ sym', arch ~ arch', W4.IsExprBuilder sym', PAr.ValidArch arch') => () => InnerSymEquivalenceError sym arch -> InnerEquivalenceError arch' @@ -164,6 +170,11 @@ data InnerEquivalenceError arch | RequiresInvalidPointerOps | PairGraphError PairGraphErr +errShortName :: MS.SymArchConstraints arch => InnerEquivalenceError arch -> String +errShortName = \case + InnerSymEquivalenceError_ se -> symErrShortName se + e -> head $ words (show e) + data PairGraphErr = PairGraphErr String deriving Show diff --git a/src/Pate/Monad.hs b/src/Pate/Monad.hs index 52a9edc7..d264397e 100644 --- a/src/Pate/Monad.hs +++ b/src/Pate/Monad.hs @@ -292,13 +292,17 @@ emitWarning :: PEE.InnerEquivalenceError arch -> EquivM sym arch () emitWarning innererr = do - err <- CMR.asks envWhichBinary >>= \case - Just (Some wb) -> return $ PEE.equivalenceErrorFor wb innererr - Nothing -> return $ PEE.equivalenceError innererr - case PEE.isTracedWhenWarning err of - True -> emitTraceWarning err - False -> return () - emitEvent (\_ -> PE.Warning err) + cfg <- CMR.asks envConfig + case elem (PEE.errShortName innererr) (PC.cfgIgnoreWarnings cfg) of + True -> return () + False -> do + err <- CMR.asks envWhichBinary >>= \case + Just (Some wb) -> return $ PEE.equivalenceErrorFor wb innererr + Nothing -> return $ PEE.equivalenceError innererr + case PEE.isTracedWhenWarning err of + True -> emitTraceWarning err + False -> return () + emitEvent (\_ -> PE.Warning err) -- | Emit an event declaring that an error has been raised, but only throw -- the error if it is not recoverable (according to 'PEE.isRecoverable') diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index b5cfe3fd..12a9b14b 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/src/Pate/Verification/PairGraph.hs @@ -752,19 +752,18 @@ considerObservableEvent gr bPair action = -- | If a program desync has not already be found -- for this block pair, run the given action to check if there -- currently is one. -considerDesyncEvent :: Monad m => - IsTreeBuilder '(sym, arch) PEE.EquivalenceError m => +considerDesyncEvent :: PA.ValidArch arch => PairGraph sym arch -> NodeEntry arch -> - (m (Maybe (TotalityCounterexample (MM.ArchAddrWidth arch)), PairGraph sym arch)) -> - m (PairGraph sym arch) + (EquivM_ sym arch (Maybe (TotalityCounterexample (MM.ArchAddrWidth arch)), PairGraph sym arch)) -> + EquivM sym arch (PairGraph sym arch) considerDesyncEvent gr bPair action = case Map.lookup bPair (pairGraphDesyncReports gr) of -- we have already found observable event differences at this location, so skip the check Just cex -> do withTracing @"totalityce" cex $ - emitTraceWarning $ PEE.equivalenceError $ PEE.NonTotalBlockExits (nodeBlocks bPair) + emitWarning $ PEE.NonTotalBlockExits (nodeBlocks bPair) return gr Nothing -> do (mcex, gr') <- action @@ -772,7 +771,7 @@ considerDesyncEvent gr bPair action = Nothing -> return gr' Just cex -> do withTracing @"totalityce" cex $ - emitTraceWarning $ PEE.equivalenceError $ PEE.NonTotalBlockExits (nodeBlocks bPair) + emitWarning $ PEE.NonTotalBlockExits (nodeBlocks bPair) return gr'{ pairGraphDesyncReports = Map.insert bPair cex (pairGraphDesyncReports gr) } -- | Record an error that occured during analysis that doesn't fall into one of the From e90280491cb9821ee839493a4671bee57be30eaa Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 28 Feb 2024 09:32:05 -0800 Subject: [PATCH 4/5] Add 'iteToImp' for converting if-then-else into implications in predicates This makes the resulting predicates from control flow alignment slightly more readable after simplification --- src/Pate/Verification/StrongestPosts.hs | 9 +++-- src/What4/ExprHelpers.hs | 48 +++++++++++++++++++++++++ 2 files changed, 55 insertions(+), 2 deletions(-) diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 674d4a8a..d2689f5d 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -132,6 +132,7 @@ import qualified Data.Aeson as JSON import qualified Pate.Solver as PSo import qualified Pate.EventTrace as ET import Control.Exception (throw) +import qualified What4.ExprHelpers as WEH -- Overall module notes/thoughts -- @@ -2492,11 +2493,15 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi -- 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 here. + -- 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 <- ET.compareSymSeq sym traceO traceP $ \evO evP -> + traces_eq_ <- ET.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 diff --git a/src/What4/ExprHelpers.hs b/src/What4/ExprHelpers.hs index b9fe3ac8..28430f73 100644 --- a/src/What4/ExprHelpers.hs +++ b/src/What4/ExprHelpers.hs @@ -77,6 +77,7 @@ module What4.ExprHelpers ( , stripAnnotations , assertPositiveNat , printAtoms + , iteToImp ) where import GHC.TypeNats @@ -1488,6 +1489,53 @@ simplifyApp sym cache simp_check simp_app outer = do _ -> else_ e go outer +-- (if x then y else z) ==> (x -> y) AND (NOT(x) -> z) +-- Truth table: +--- x | y | z | expr | simp +--- T | T | T | T | T +-- T | T | F | T | T +-- T | F | T | F | F +-- T | F | F | F | F +-- F | T | T | T | T +-- F | T | F | F | F +-- F | F | T | T | T +-- F | F | F | F | F +iteToImp' :: + forall sym. + W4.IsExprBuilder sym => + sym -> + W4.Pred sym {-^ if -} -> + W4.Pred sym {-^ then -} -> + W4.Pred sym {-^ else -} -> + IO (W4.Pred sym) +iteToImp' sym i t e = do + i_imp_t <- W4.impliesPred sym i t + not_i <- W4.notPred sym i + not_i_imp_e <- W4.impliesPred sym not_i e + W4.andPred sym i_imp_t not_i_imp_e + +-- | Rewrite subterms with: (if x then y else z) ==> (x -> y) AND (NOT(x) -> z) +iteToImp :: + forall sym t solver fs tp. + sym ~ (W4B.ExprBuilder t solver fs) => + sym -> + W4.SymExpr sym tp -> + IO (W4.SymExpr sym tp) +iteToImp sym e_outer = do + cache <- W4B.newIdxCache + let + go :: forall tp'. W4.SymExpr sym tp' -> IO (W4.SymExpr sym tp') + go = simplifyApp sym cache noSimpCheck goApp + + goApp :: forall tp'. W4B.App (W4B.Expr t) tp' -> IO (Maybe (W4.SymExpr sym tp')) + goApp = \case + W4B.BaseIte W4.BaseBoolRepr _ p t e -> do + p' <- go p + t' <- go t + e' <- go e + Just <$> iteToImp' sym p' t' e' + _ -> return Nothing + go e_outer -- | Simplify the given predicate by deciding which atoms are logically necessary -- according to the given provability function. From f4f7fa236868c9ec1c78088ff1ab99f37b61617a Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Wed, 28 Feb 2024 09:34:11 -0800 Subject: [PATCH 5/5] Add script file for target 3 Does not yet add target 3 to the test suite --- demos/nov-2023/Makefile | 5 ++++- demos/nov-2023/target3.pate | 40 +++++++++++++++++++++++++++++++++++++ 2 files changed, 44 insertions(+), 1 deletion(-) create mode 100644 demos/nov-2023/target3.pate diff --git a/demos/nov-2023/Makefile b/demos/nov-2023/Makefile index 9ddde3ad..60041a5f 100644 --- a/demos/nov-2023/Makefile +++ b/demos/nov-2023/Makefile @@ -148,7 +148,10 @@ target3: target3.original.so target3.patched.so -s _ZN3ros22TransportPublisherLink15onMessageLengthERKN5boost10shared_ptrINS_10ConnectionEEERKNS1_12shared_arrayIhEEjb \ -s _ZN3ros22TransportPublisherLink16onHeaderReceivedERKN5boost10shared_ptrINS_10ConnectionEEERKNS_6HeaderE \ -s _ZN3ros22TransportPublisherLinkD2Ev \ - --save-macaw-cfgs target1_CFGs + --save-macaw-cfgs target1_CFGs \ + --ignore-warnings NonTotalBlockExits \ + --ignore-warnings RequiresInvalidPointerOps \ + --script target3.pate target3.diff: target3.original.so target3.patched.so arm-none-eabi-objdump -M force-thumb-mode -d target3.original.so > target3.original.dump diff --git a/demos/nov-2023/target3.pate b/demos/nov-2023/target3.pate new file mode 100644 index 00000000..14696b88 --- /dev/null +++ b/demos/nov-2023/target3.pate @@ -0,0 +1,40 @@ +Choose Entry Point + > Function Entry "onMessageLength" + +Function Entry "onMessageLength" + ... + Call to: "function4" (segment1+0x71980) Returns to: "onMessageLength" (segment1+0x1200b8) (original) vs. Jump to: "onMessageLength" (segment1+0x11ffc0) + ... + ... + > Choose desynchronization points + + Choose a desynchronization point: + > segment1+0x11ffc0 (original) + > segment1+0x11ffc0 (patched) + + +segment1+0x11ffc0 [ via: "onMessageLength" (segment1+0x11febc) ] + Block Exits + ... + ... + Control flow desynchronization found + > Align control flow in equivalence condition + + +segment1+0x11ebe4 + Block Exits + ... + ... + Control flow desynchronization found + > Align control flow in equivalence condition + +segment1+0x11ec7c + Block Exits + ... + ... + Control flow desynchronization found + > Align control flow in equivalence condition + +Verification Finished +Continue verification? + > Finish and view final result \ No newline at end of file