diff --git a/src/Pate/SimState.hs b/src/Pate/SimState.hs index e578c4ad..0a972ffe 100644 --- a/src/Pate/SimState.hs +++ b/src/Pate/SimState.hs @@ -245,6 +245,8 @@ data SimScope sym arch v = instance Scoped (SimScope sym arch) where unsafeCoerceScope scope = coerce scope +instance Scoped (Const x) where + unsafeCoerceScope scope = coerce scope scopeBoundVars :: SimScope sym arch v -> PPa.PatchPair (SimBoundVars sym arch v) scopeBoundVars scope = PPa.PatchPair (scopeBoundVarsO scope) (scopeBoundVarsP scope) diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index 089de9f3..28d3991e 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/src/Pate/Verification/PairGraph/Node.hs @@ -14,6 +14,7 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE FlexibleInstances #-} module Pate.Verification.PairGraph.Node ( GraphNode(..) @@ -59,6 +60,7 @@ import Pate.TraceTree import qualified Pate.Binary as PB import qualified Prettyprinter as PP import Data.Parameterized (Some(..), Pair (..)) +import qualified What4.JSON as W4S -- | Nodes in the program graph consist either of a pair of -- program points (GraphNode), or a synthetic node representing @@ -80,6 +82,12 @@ instance PA.ValidArch arch => JSON.ToJSON (GraphNode arch) where GraphNode nd -> JSON.object [ ("graph_node_type", "entry"), "entry_body" JSON..= nd] ReturnNode nd -> JSON.object [ ("graph_node_type", "return"), "return_body" JSON..= nd] +instance PA.ValidArch arch => W4S.W4Serializable sym (GraphNode arch) where + w4Serialize r = return $ JSON.toJSON r + +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 } diff --git a/src/Pate/Verification/Simplify.hs b/src/Pate/Verification/Simplify.hs index 313a209f..2ca21fcd 100644 --- a/src/Pate/Verification/Simplify.hs +++ b/src/Pate/Verification/Simplify.hs @@ -17,6 +17,7 @@ module Pate.Verification.Simplify ( , applySimplifier , runSimplifier , getSimplifier + , deepPredicateSimplifier ) where import Control.Monad (foldM) @@ -218,6 +219,17 @@ applySimplifier simplifier v = withSym $ \sym -> do True -> withTracing @"debug_tree" "Simplifier" $ PEM.mapExpr sym (runSimplifier simplifier) v False -> withNoTracing $ PEM.mapExpr sym (runSimplifier simplifier) v +deepPredicateSimplifier :: forall sym arch. EquivM sym arch (Simplifier sym arch) +deepPredicateSimplifier = withSym $ \sym -> do + Simplifier f <- getSimplifier + return $ Simplifier $ \e0 -> do + e1 <- liftIO $ WEH.stripAnnotations sym e0 + e2 <- f e1 + e4 <- case W4.exprType e0 of + W4.BaseBoolRepr -> simplifyPred_deep e2 + _ -> return e2 + applyCurrentAsms e4 + getSimplifier :: forall sym arch. EquivM sym arch (Simplifier sym arch) getSimplifier = withSym $ \sym -> do heuristicTimeout <- CMR.asks (PC.cfgHeuristicTimeout . envConfig) diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index d2689f5d..f5f21e55 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -133,6 +133,7 @@ import qualified Pate.Solver as PSo import qualified Pate.EventTrace as ET import Control.Exception (throw) import qualified What4.ExprHelpers as WEH +import qualified What4.JSON as W4S -- Overall module notes/thoughts -- @@ -659,7 +660,7 @@ updateCombinedSyncPoint divergeNode pg_top = withPG_ pg_top $ do 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 syncO pg $ + 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 @@ -770,7 +771,7 @@ mergeDualNodes in1 in2 spec1 spec2 syncNode gr0 = fnTrace "mergeDualNodes" $ wit (_, 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 in2 gr2 $ do + withPredomain scope bundle dom $ withConditionsAssumed scope bundle dom2 in2 gr2 $ do withTracing @"node" in2 $ do emitTraceLabel @"domain" PAD.Predomain (Some dom) widenAlongEdge scope bundle in2 dom gr2 syncNode @@ -849,23 +850,101 @@ pairGraphComputeFixpoint entries gr_init = do showFinalResult :: PairGraph sym arch -> EquivM sym arch () showFinalResult pg = withTracing @"final_result" () $ withSym $ \sym -> do + + subTree @"node" "Observable Counter-examples" $ do forM_ (Map.toList (pairGraphObservableReports pg)) $ \(nd,report) -> subTrace (GraphNode nd) $ emitTrace @"observable_result" (CE.ObservableCheckCounterexample report) - subTree @"node" "Assumed Equivalence Conditions" $ do - forM_ (getAllNodes pg) $ \nd -> do + eq_conds <- fmap catMaybes $ subTree @"node" "Assumed Equivalence Conditions" $ do + + forM (getAllNodes pg) $ \nd -> do case getCondition pg nd ConditionEquiv of - Just eqCondSpec -> subTrace nd $ do - _ <- withFreshScope (graphNodeBlocks nd) $ \scope -> do - (_, eqCond) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) eqCondSpec - eqCondPred <- PEE.someExpr sym <$> PEC.toPred sym eqCond - emitTraceLabel @"eqcond" (eqCondPred) (Some eqCond) - return eqCond - return () - Nothing -> return () + Just cond_spec -> subTrace nd $ do + s <- withFreshScope (graphNodeBlocks nd) $ \scope -> do + (_,cond) <- IO.liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) cond_spec + (tr, _) <- withGraphNode scope nd pg $ \bundle d -> do + simplifier <- PSi.deepPredicateSimplifier + cond_simplified <- PSi.applySimplifier simplifier cond + eqCond_pred <- PEC.toPred sym cond_simplified + (mtraceT, mtraceF) <- getTracesForPred scope bundle d eqCond_pred + case (mtraceT, mtraceF) of + (Just traceT, Just traceF) -> + return $ (Just (FinalEquivCond eqCond_pred traceT traceF), pg) + _ -> return (Nothing, pg) + return $ (Const (fmap (nd,) tr)) + return $ PS.viewSpec s (\_ -> getConst) + Nothing -> return Nothing result <- pairGraphComputeVerdict pg emitTrace @"equivalence_result" result + let eq_conds_map = Map.fromList eq_conds + let toplevel_result = FinalResult result (pairGraphObservableReports pg) eq_conds_map + emitTrace @"toplevel_result" toplevel_result + +data FinalResult sym arch = FinalResult + { + _finEqStatus :: PE.EquivalenceStatus + , _finObservableCE :: Map.Map (NodeEntry arch) (CE.ObservableCounterexample sym arch) + , _finEqConds :: Map.Map (GraphNode arch) (FinalEquivCond sym arch) + } + +data FinalEquivCond sym arch = FinalEquivCond + { + _finEqCondPred :: W4.Pred sym + , _finEqCondTraceTrue :: CE.TraceEvents sym arch + , _finEqCondTraceFalse :: CE.TraceEvents sym arch + } + + +instance W4S.W4Serializable sym (PE.EquivalenceStatus) where + w4Serialize st = W4S.w4SerializeString st + +instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalResult sym arch) where + w4Serialize (FinalResult st obs conds) = do + W4S.object [ "eq_status" W4S..= st, "observable_counterexamples" W4S..= obs, "eq_conditions" W4S..= conds ] + +instance (PA.ValidArch arch, PSo.ValidSym sym) => W4S.W4Serializable sym (FinalEquivCond sym arch) where + w4Serialize (FinalEquivCond p trT trF) = do + W4S.object [ "predicate" W4S..== p, "trace_true" W4S..= trT, "trace_false" W4S..= trF ] + + +instance (PSo.ValidSym sym, PA.ValidArch arch) => IsTraceNode '(sym,arch) "toplevel_result" where + type TraceNodeType '(sym,arch) "toplevel_result" = FinalResult sym arch + prettyNode () _ = "Toplevel Result" + nodeTags = mkTags @'(sym, arch) @"toplevel_result" [Simplified, Summary] + jsonNode sym () v = W4S.w4ToJSON sym v + +-- | Run a 'PairGraph' computation in the assumption context of +-- a given 'GraphNode' +-- This is a subset of the steps taken in 'visitNode' which +-- sets up the context before performing code discovery and +-- domain widening. +withGraphNode :: + PS.SimScope sym arch v -> + GraphNode arch -> + PairGraph sym arch -> + (PS.SimBundle sym arch v -> + AbstractDomain sym arch v -> + EquivM_ sym arch (a, PairGraph sym arch)) -> + EquivM sym arch (a, PairGraph sym arch) +withGraphNode scope nd pg f = withSym $ \sym -> do + case getCurrentDomain pg nd of + Nothing | GraphNode ne <- nd -> throwHere $ PEE.MissingDomainForBlock (nodeBlocks ne) + Nothing | ReturnNode nr <- nd -> throwHere $ PEE.MissingDomainForFun (nodeFuns nr) + Just dom_spec -> do + (_, d) <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) dom_spec + case nd of + GraphNode ne -> withAbsDomain ne d pg $ withValidInit scope (nodeBlocks ne) $ + withSimBundle pg (PS.scopeVars scope) ne $ \bundle -> + withPredomain scope bundle d $ + {- withConditionsAssumed scope bundle d nd pg $ -} + f bundle d + ReturnNode nr -> do + bundle <- noopBundle scope (graphNodeBlocks (ReturnNode nr)) + withPredomain scope bundle d $ + {- withConditionsAssumed scope bundle d (ReturnNode nr) pg $ -} + f bundle d + -- | For an orphan return, we treat it the same as an undefined PLT stub, -- since we effectively have no way to characterize the function behavior. @@ -1088,40 +1167,74 @@ updateAbsBlockState node d = do withSatConditionAssumed :: PS.SimScope sym arch v -> + PS.SimBundle sym arch v -> + AbstractDomain sym arch v -> GraphNode arch -> ConditionKind -> PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch) -> - EquivM sym arch (PairGraph sym arch) -withSatConditionAssumed scope nd condK gr0 f = withSym $ \sym -> do + EquivM sym arch (PairGraph sym arch) +withSatConditionAssumed scope bundle dom nd condK gr0 f = withSym $ \sym -> do priority <- thisPriority eqCond <- getScopedCondition scope gr0 nd condK eqCond_pred <- PEC.toPred sym eqCond - (withSatAssumption (PAS.fromPred eqCond_pred) (traceEqCond condK eqCond >> f)) >>= \case - Just result -> return result - -- for propagated assumptions and assertions, we mark this branch as infeasible - Nothing | shouldPropagate (getPropagationKind gr0 nd condK) -> do - gr1 <- return $ addDomainRefinement nd (PruneBranch condK) gr0 - emitTrace @"message" ("Branch dropped as " ++ conditionPrefix condK) - return $ queueAncestors (priority PriorityPropagation) nd gr1 - -- for non-propagated assumptions we don't attempt to prune this branch, - -- we just do nothing - Nothing -> do - emitTrace @"message" ("Branch is " ++ conditionAction condK ++ " infeasible") - return gr0 - + case W4.asConstantPred eqCond_pred of + Just True -> f + _ -> do + let msg = conditionPrefix condK + (mtraceT, mtraceF) <- withTracing @"message" msg $ getTracesForPred scope bundle dom eqCond_pred + case (mtraceT, mtraceF) of + -- condition is not necessarily true or false + (Just{}, Just{}) -> do + withAssumption eqCond_pred f + -- condition is necessarily true, so we don't need to do anything + (Just{}, Nothing) -> f + -- condition is not satisfiable + (Nothing, _) -> case shouldPropagate (getPropagationKind gr0 nd condK) of + True -> do + gr1 <- return $ addDomainRefinement nd (PruneBranch condK) gr0 + emitTrace @"message" ("Branch dropped as " ++ conditionPrefix condK) + return $ queueAncestors (priority PriorityPropagation) nd gr1 + -- for non-propagated assumptions we don't attempt to prune this branch, + -- we just do nothing + False -> do + emitTrace @"message" ("Branch is " ++ conditionAction condK ++ " infeasible") + return gr0 +getTracesForPred :: + PS.SimScope sym arch v -> + PS.SimBundle sym arch v -> + AbstractDomain sym arch v -> + W4.Pred sym -> + EquivM sym arch (Maybe (CE.TraceEvents sym arch), Maybe (CE.TraceEvents sym arch)) +getTracesForPred scope bundle dom p = withSym $ \sym -> do + not_p <- liftIO $ W4.notPred sym p + withTracing @"expr" (Some p) $ do + mtraceT <- withTracing @"message" "With condition assumed" $ + withSatAssumption (PAS.fromPred p) $ do + traceT <- getSomeGroundTrace scope bundle dom Nothing + emitTrace @"trace_events" traceT + return traceT + mtraceF <- withTracing @"message" "With negation assumed" $ + withSatAssumption (PAS.fromPred not_p) $ do + traceF <- getSomeGroundTrace scope bundle dom Nothing + emitTrace @"trace_events" traceF + return traceF + return (mtraceT, mtraceF) + withConditionsAssumed :: PS.SimScope sym arch v -> + PS.SimBundle sym arch v -> + AbstractDomain sym arch v -> GraphNode arch -> PairGraph sym arch -> EquivM_ sym arch (PairGraph sym arch) -> EquivM sym arch (PairGraph sym arch) -withConditionsAssumed scope node gr0 f = do +withConditionsAssumed scope bundle d node gr0 f = do foldr go f [minBound..maxBound] where go condK g = - withSatConditionAssumed scope node condK gr0 g + withSatConditionAssumed scope bundle d node condK gr0 g accM :: (Monad m, Foldable t) => b -> t a -> (b -> a -> m b) -> m b accM b ta f = foldM f b ta @@ -1267,7 +1380,7 @@ visitNode scope (GraphNode node@(nodeBlocks -> bPair)) d gr0 = Just gr3 -> do priority <- thisPriority return $ queueNode (priority PriorityHandleActions) (GraphNode node) gr3 - Nothing -> withConditionsAssumed scope (GraphNode node) gr0 $ do + 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 @@ -1302,7 +1415,7 @@ visitNode scope (ReturnNode fPair) d gr0 = do priority <- thisPriority return $ queueNode (priority PriorityHandleActions) (ReturnNode fPair) gr1 Nothing -> withTracing @"message" "Toplevel Return" $ do - withConditionsAssumed scope (ReturnNode fPair) gr0' $ do + withConditionsAssumed scope bundle d (ReturnNode fPair) gr0' $ do case isSingleReturn fPair of Just{} -> void $ emitError' $ PEE.OrphanedSingletonAnalysis (nodeFuns fPair) Nothing -> return () @@ -1325,7 +1438,7 @@ visitNode scope (ReturnNode fPair) d gr0 = do Just gr1 -> do priority <- thisPriority return $ queueNode (priority PriorityHandleActions) (ReturnNode fPair) gr1 - Nothing -> withConditionsAssumed scope (ReturnNode fPair) gr0 $ do + Nothing -> withConditionsAssumed scope bundle d (ReturnNode fPair) gr0 $ do traceBundle bundle "Processing return edge" -- observable events may occur in return nodes specifically -- when they are a synchronization point, since the abstract diff --git a/src/Pate/Verification/StrongestPosts/CounterExample.hs b/src/Pate/Verification/StrongestPosts/CounterExample.hs index b0633494..be074c74 100644 --- a/src/Pate/Verification/StrongestPosts/CounterExample.hs +++ b/src/Pate/Verification/StrongestPosts/CounterExample.hs @@ -129,6 +129,18 @@ data ObservableCheckResult sym arch (ObservableCounterexample sym arch) | ObservableCheckError String +obsResultSummary :: ObservableCheckResult sym arch -> String +obsResultSummary res = case res of + ObservableCheckEq -> "Observably Equivalent" + ObservableCheckCounterexample{} -> "Observable Inequivalence Detected" + ObservableCheckError{} -> "Error during observability check" + +instance (PA.ValidArch arch, PSo.ValidSym sym) => W4Serializable sym (ObservableCounterexample sym arch) where + w4Serialize r = w4SerializeString (show (ppObservableCounterexample r)) + +instance W4Serializable sym (ObservableCheckResult sym arch) where + w4Serialize r = w4SerializeString (show (obsResultSummary r)) + instance (PA.ValidArch arch, PSo.ValidSym sym) => IsTraceNode '(sym,arch) "observable_result" where type TraceNodeType '(sym,arch) "observable_result" = ObservableCheckResult sym arch prettyNode () = \case @@ -139,10 +151,7 @@ instance (PA.ValidArch arch, PSo.ValidSym sym) => IsTraceNode '(sym,arch) "obser , PP.pretty msg ] nodeTags = - [ (tag, \() res -> case res of - ObservableCheckEq -> "Observably Equivalent" - ObservableCheckCounterexample{} -> "Observable Inequivalence Detected" - ObservableCheckError{} -> "Error during observability check") + [ (tag, \() res -> PP.viaShow $ obsResultSummary res) | tag <- [Simplified, Summary] ] diff --git a/src/Pate/Verification/Widening.hs b/src/Pate/Verification/Widening.hs index 34932d46..b6b4980a 100644 --- a/src/Pate/Verification/Widening.hs +++ b/src/Pate/Verification/Widening.hs @@ -441,16 +441,12 @@ addRefinementChoice nd gr0 = withTracing @"message" "Modify Proof Node" $ do emitTrace @"message" (conditionName condK ++ " Discharged") return Nothing False -> do - simplifier <- PSi.getSimplifier + simplifier <- PSi.deepPredicateSimplifier curAsm <- currentAsm emitTrace @"assumption" curAsm - eqCond_pred1 <- liftIO $ WEH.stripAnnotations sym eqCond_pred - eqCond_pred2 <- PSi.applySimplifier simplifier eqCond_pred1 - eqCond_pred3 <- PSi.simplifyPred_deep eqCond_pred2 - eqCond_pred4 <- applyCurrentAsms eqCond_pred3 - - emitTraceLabel @"expr" (ExprLabel $ "Simplified " ++ conditionName condK) (Some eqCond_pred4) - return $ Just eqCond_pred4 + eqCond_pred_simp <- PSi.applySimplifier simplifier eqCond_pred + emitTraceLabel @"expr" (ExprLabel $ "Simplified " ++ conditionName condK) (Some eqCond_pred_simp) + return $ Just eqCond_pred_simp case meqCond_pred' of Nothing -> return $ dropCondition nd condK gr0_ Just eqCond_pred' -> do