drop equivalence domains when updating conditions

this ensures that the domain is computed under the
strongest possible set of assumptions, as well
as ensuring that assertions are necessarily propagated

NB: this breaks challenge 10 and target 7, since
it fixes #447 but not #448 (i.e. desync points
are now properly re-queued for analysis during
propagation, but the generated assertions are incorrect)

src/Pate/Verification/StrongestPosts.hs

@@ -1578,10 +1578,8 @@ handleOrphanedSingleSidedReturn ::
   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
+  addToEquivCondition scope (ReturnNode nd) ConditionEquiv (W4.falsePred sym) pg
 
 -- | Construct a "dummy" simulation bundle that basically just
 --   immediately returns the prestate as the poststate.
@@ -1811,7 +1809,6 @@ doCheckObservables scope ne bundle preD pg = case PS.simOut bundle of
                       modify $ queueAncestors (priority p) nd
                       when ((condK, p) == (ConditionEquiv, PriorityPropagation)) $
                         modify $ setPropagationKind nd ConditionEquiv PropagateOnce
-                    modify $ dropPostDomains nd (priority PriorityDomainRefresh)
                     modify $ queueNode (raisePriority (priority PriorityNodeRecheck)) nd
                   return Nothing
               Nothing -> return $ (Just cex, pg)
@@ -2887,10 +2884,7 @@ handleDivergingPaths scope bundle currBlock st dom blkt = fnTrace "handleDivergi
               -- 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
+              addToEquivCondition scope (GraphNode currBlock) condK traces_eq pg
             _ -> return pg
           return $ st'{ branchGraph = pg2 }
 

src/Pate/Verification/Widening.hs

@@ -302,9 +302,12 @@ updateEquivCondition scope nd condK mpropK cond gr = withSym $ \sym -> do
     False -> return cond
   eqCond <- getScopedCondition scope gr nd condK
   eqCond' <- PEC.merge sym cond' eqCond
-  return $ setCondition nd condK propK (PS.mkSimSpec scope eqCond') gr
+  let gr1 = setCondition nd condK propK (PS.mkSimSpec scope eqCond') gr
+  priority <- thisPriority
+  return $ dropDomain nd (priority PriorityDomainRefresh) gr1
 
--- | Adds the given predicate to the equivalence condition for the given node
+-- | Adds the given predicate to the equivalence condition for the given node.
+--   Note that this drops the domain of the current node.
 addToEquivCondition ::
   PS.SimScope sym arch v ->
   GraphNode arch ->
@@ -313,11 +316,20 @@ addToEquivCondition ::
   PairGraph sym arch ->
   EquivM sym arch (PairGraph sym arch)    
 addToEquivCondition scope nd condK condPred gr = withSym $ \sym -> do
-  let eqCond = (PEC.universal sym) { PEC.eqCondExtraCond = PAs.NamedAsms $ PAs.fromPred condPred}
-  eqCond' <- getScopedCondition scope gr nd condK 
-  eqCond'' <- PEC.merge sym eqCond eqCond'
-  let propK = getPropagationKind gr nd condK
-  return $ setCondition nd condK propK (PS.mkSimSpec scope eqCond'') gr
+  case W4.asConstantPred condPred of
+    Just True ->
+      -- condition is trivial, do nothing 
+      return gr
+      -- note we don't handle 'Just False', since a 'False' condition is still valid (causes
+      -- the branch to be pruned)
+    _ -> do
+      let eqCond = (PEC.universal sym) { PEC.eqCondExtraCond = PAs.NamedAsms $ PAs.fromPred condPred}
+      eqCond' <- getScopedCondition scope gr nd condK 
+      eqCond'' <- PEC.merge sym eqCond eqCond'
+      let propK = getPropagationKind gr nd condK
+      let gr1 = setCondition nd condK propK (PS.mkSimSpec scope eqCond'') gr
+      priority <- thisPriority
+      return $ dropDomain nd (priority PriorityDomainRefresh) gr1
 
 pruneCurrentBranch ::
   PS.SimScope sym arch v ->
@@ -330,14 +342,11 @@ pruneCurrentBranch scope (from,to) condK gr0 = withSym $ \sym -> do
   let gr1 = gr0
   pathCond <- CMR.asks envPathCondition >>= PAs.toPred sym
   notPath <- liftIO $ W4.notPred sym pathCond
-  gr2 <- addToEquivCondition scope from condK notPath gr1
+  gr2 <- addToEquivCondition scope from condK notPath (markEdge from to gr1)
   let propK = getPropagationKind gr1 from condK
   case shouldPropagate propK of
-    True -> do
-      return $ queueAncestors (priority PriorityPropagation) from $ 
-        dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr2)
-    False -> return $ queueNode (priority PriorityNodeRecheck) from $
-      dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr2)
+    True -> return $ queueNode (priority PriorityPropagation) from gr2
+    False -> return $ queueNode (priority PriorityNodeRecheck) from gr2
 
 traceEqCond ::
   ConditionKind -> 
@@ -596,12 +605,11 @@ applyDomainRefinements scope (from,to) bundle preD postD gr0 = fnTrace "applyDom
           emitTrace @"debug" "Equivalence condition holds, no propagation needed"
           return gr1
         False -> do
-          gr2 <- updateEquivCondition scope from condK Nothing eqCond gr1
+          gr2 <- updateEquivCondition scope from condK Nothing eqCond (markEdge from to gr1)
           -- since its equivalence condition has been modified, we need to re-examine
           -- all outgoing edges from the predecessor node
           priority <- thisPriority
-          gr3 <- return $ queueAncestors (priority PriorityPropagation) from $ 
-            dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr2)
+          gr3 <- return $ queueAncestors (priority PriorityPropagation) from gr2
           next gr3
 
 
@@ -843,10 +851,9 @@ propagateCondition scope bundle from to gr0_ = fnTrace "propagateCondition" $ 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
+                  gr1 <- updateEquivCondition scope from condK (Just (nextPropagate propK)) cond (markEdge from to gr)
                   return $ Just $ queueAncestors (priority PriorityPropagation) from $ 
-                    queueNode (priority PriorityNodeRecheck) from $ 
-                    dropPostDomains from (priority PriorityDomainRefresh) (markEdge from to gr1)
+                    queueNode (priority PriorityNodeRecheck) from gr1
                 Nothing -> throwHere $ PEE.InconclusiveSAT
 
 -- | Given the results of symbolic execution, and an edge in the pair graph