Skip to content

Commit

Permalink
Add example traces for any assumptions/assertions/eq. conditions
Browse files Browse the repository at this point in the history
Additionally adds a summary to the final result (only serialized to JSON for now).
  • Loading branch information
danmatichuk authored Mar 1, 2024
2 parents 8ba50ba + 197cbdc commit c10939d
Show file tree
Hide file tree
Showing 6 changed files with 184 additions and 44 deletions.
2 changes: 2 additions & 0 deletions src/Pate/SimState.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
8 changes: 8 additions & 0 deletions src/Pate/Verification/PairGraph/Node.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@

{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE FlexibleInstances #-}

module Pate.Verification.PairGraph.Node (
GraphNode(..)
Expand Down Expand Up @@ -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
Expand All @@ -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 }
Expand Down
12 changes: 12 additions & 0 deletions src/Pate/Verification/Simplify.hs
Original file line number Diff line number Diff line change
Expand Up @@ -17,6 +17,7 @@ module Pate.Verification.Simplify (
, applySimplifier
, runSimplifier
, getSimplifier
, deepPredicateSimplifier
) where

import Control.Monad (foldM)
Expand Down Expand Up @@ -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)
Expand Down
177 changes: 145 additions & 32 deletions src/Pate/Verification/StrongestPosts.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
--
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 ()
Expand All @@ -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
Expand Down
17 changes: 13 additions & 4 deletions src/Pate/Verification/StrongestPosts/CounterExample.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
]

Expand Down
12 changes: 4 additions & 8 deletions src/Pate/Verification/Widening.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit c10939d

Please sign in to comment.