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/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index d2689f5d..f50e63ca 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -659,7 +659,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 +770,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 @@ -856,17 +856,48 @@ showFinalResult pg = withTracing @"final_result" () $ withSym $ \sym -> do subTree @"node" "Assumed Equivalence Conditions" $ do forM_ (getAllNodes pg) $ \nd -> do case getCondition pg nd ConditionEquiv of - Just eqCondSpec -> subTrace nd $ do + Just{} -> 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 + -- 'withConditionsAssumed' emits the expected tracing info here + _ <- withGraphNode scope nd pg $ \_ _ -> return pg + return $ (Const ()) return () Nothing -> return () result <- pairGraphComputeVerdict pg emitTrace @"equivalence_result" result +-- | 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 (PairGraph sym arch)) -> + EquivM sym arch (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. -- In this case we model the function behavior as having peformed the @@ -1088,40 +1119,60 @@ 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 - + not_eqCond_pred <- liftIO $ W4.notPred sym eqCond_pred + mtraceT <- withSatAssumption (PAS.fromPred eqCond_pred) $ + getSomeGroundTrace scope bundle dom Nothing + mtraceF <- withSatAssumption (PAS.fromPred not_eqCond_pred) $ + getSomeGroundTrace scope bundle dom Nothing + case (mtraceT, mtraceF) of + -- condition is not necessarily true or false + (Just traceT, Just traceF) -> do + let msg = conditionPrefix condK + withTracing @"message" msg $ do + emitTraceLabel @"eqcond" (PEE.someExpr sym eqCond_pred) (Some eqCond) + withTracing @"message" "With condition assumed" $ + emitTrace @"trace_events" traceT + withTracing @"message" "With negation assumed" $ + emitTrace @"trace_events" traceF + 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 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 +1318,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 +1353,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 +1376,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