add modified packet example and build scripts

arch/Pate/AArch32.hs

@@ -269,7 +269,7 @@ stubOverrides =
     case PB.fnSymBase fs of
       -- FIXME: multiple variants of this constructor
       "basic_string" -> Just $ PA.mkDefaultStubOverride "basic_string" r0
-      "print" -> Just $ PA.mkObservableOverride "print" r0 r1
+      "print" -> Just $ PA.mkObservableOverride "print" r0 [r0]
       _ -> lookup (PB.fnSymBase fs) override_list
   where
     override_list =
@@ -282,8 +282,8 @@ stubOverrides =
       , ("write", PA.mkWriteOverride "write" r0 r1 r2 r0)
       -- FIXME: fixup arguments for fwrite (len = size * nmemb)
       , ("fwrite", PA.mkWriteOverride "fwrite" r3 r0 r1 r0)
-      , ("printf", PA.mkObservableOverride "printf" r0 r1)
-      , ("puts", PA.mkObservableOverride "puts" r0 r0)
+      , ("printf", PA.mkObservableOverride "printf" r0 [r0,r1])
+      , ("puts", PA.mkObservableOverride "puts" r0 [r0])
       -- fixme: double check this
       , ("ceilf", PA.mkDefaultStubOverrideArg "ceilf" [Some v0] r0)
       -- FIXME: check abi for args

arch/Pate/PPC.hs

@@ -328,7 +328,8 @@ stubOverrides = PA.ArchStubOverrides (PA.mkDefaultStubOverride "__pate_stub" r3
       , ("write", PA.mkWriteOverride "write" r3 r4 r5 r3)
       -- FIXME: fixup arguments for fwrite
       , ("fwrite", PA.mkWriteOverride "fwrite" r3 r4 r5 r3)
-      , ("printf", PA.mkObservableOverride "printf" r3 r4)
+
+      , ("printf", PA.mkObservableOverride "printf" r3 [r3, r4])
 
       -- FIXME: added for relaySAT challenge problem
       , ("CFE_SB_AllocateMessageBuffer", PA.mkMallocOverride' (Just (PA.MemIndPointer (PA.MemPointer 0x00013044) 0x7c)) r3 r3)

pate.cabal

@@ -175,6 +175,7 @@ library
                        What4.SymSequence,
                        What4.Simplify,
                        What4.Simplify.Bitvector,
+                       What4.Simplify.Array,
                        Data.Parameterized.SetF,
                        Data.Parameterized.SetCtx,
                        Data.Parameterized.PairF,

pate_binja/pate.py

@@ -614,6 +614,9 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
             if not lastTopLevelResult:
                 out.write(f'No equivalence conditions found\n')
             else:
+                eqStatus = lastTopLevelResult.get('content', {}).get('eq_status')
+                out.write(f'Equivalence status: {eqStatus}\n')
+                out.write('\n')
                 eqconds = lastTopLevelResult.get('content', {}).get('eq_conditions', {}).get('map')
                 if eqconds:
                     # Found eq conditions
@@ -643,8 +646,8 @@ def processFinalResult(self, traceConstraints: Optional[list[tuple[TraceVar, str
                         # out.write('\nTrace False\n')
                         # pprint_node_event_trace(trace_false, 'False Trace', out=out)
 
-                else:
-                    # Hack to handle case where constraints were unsatisfiable
+                elif cfarNode:
+                    # Handle case where trace constraints were unsatisfiable
                     ect = cfarNode.equivalenceConditionTrace
                     ect.trace_true = False
                     ect.trace_false = False

src/Pate/Arch.hs

@@ -127,6 +127,7 @@ import qualified Data.Parameterized.TraversableF as TF
 import Data.Maybe
 import Pate.Memory
 import qualified Pate.ExprMappable as PEM
+import Control.Monad (forM)
 
 -- | The type of architecture-specific dedicated registers
 --
@@ -457,23 +458,29 @@ mkObservableOverride ::
   16 <= MC.ArchAddrWidth arch =>
   MS.SymArchConstraints arch =>
   T.Text {- ^ name of call -} ->
-  MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ r0 -} ->
-  MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ r1 -} ->
+  MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch)) {- ^ return -} ->
+  [MC.ArchReg arch (MT.BVType (MC.ArchAddrWidth arch))] {- ^ args -} ->
   StubOverride arch
-mkObservableOverride nm r0_reg r1_reg = StubOverride $ \sym _archInfo _wsolver -> do
+mkObservableOverride nm return_reg arg_regs = StubOverride $ \sym _archInfo _wsolver -> do
   let w_mem = MC.memWidthNatRepr @(MC.ArchAddrWidth arch)
-  let bv_repr = W4.BaseBVRepr w_mem
   -- FIXME: this is wrong, since this value needs to read from memory
-  bv_fn <- W4U.mkUninterpretedSymFn sym ("written_" ++ show nm) (Ctx.empty Ctx.:> bv_repr) (W4.BaseBVRepr w_mem)
+
   return $ StateTransformer $ \st -> do
-    let (CLM.LLVMPointer _ r1_val) = PSR.macawRegValue $ (PS.simRegs st) ^. MC.boundValue r1_reg
+    args <- forM arg_regs $ \r -> do
+      let (CLM.LLVMPointer _reg r_val) = PSR.macawRegValue $ (PS.simRegs st) ^. MC.boundValue r
+      return $ r_val
+
+    Some argsCtx <- return $ Ctx.fromList (map Some args)
+    let reprsCtx = TFC.fmapFC W4.exprType argsCtx
+    bv_fn <- W4U.mkUninterpretedSymFn sym ("written_" ++ show nm) reprsCtx (W4.BaseBVRepr w_mem)
+
     let mem = PS.simMem st
-    mem' <- PMT.addExternalCallEvent sym nm (Ctx.empty Ctx.:> r1_val) mem
+    mem' <- PMT.addExternalCallEvent sym nm argsCtx mem
     let st' = st { PS.simMem = mem' }
     zero_nat <- W4.natLit sym 0
-    fresh_bv <- W4.applySymFn sym bv_fn (Ctx.empty Ctx.:> r1_val) 
+    fresh_bv <- W4.applySymFn sym bv_fn argsCtx
     let ptr = PSR.ptrToEntry (CLM.LLVMPointer zero_nat fresh_bv)
-    return (st' { PS.simRegs = ((PS.simRegs st') & (MC.boundValue r0_reg) .~ ptr ) })
+    return (st' { PS.simRegs = ((PS.simRegs st') & (MC.boundValue return_reg) .~ ptr ) })
 
 mkEventOverride ::
   forall arch ptrW.

src/Pate/Equivalence/Condition.hs

@@ -111,14 +111,16 @@ weaken ::
   W4.Pred sym ->
   EquivalenceCondition sym arch v ->
   m (EquivalenceCondition sym arch v)  
-weaken sym p cond = do
-  mem <- WPM.weaken sym p (eqCondMem cond)
-  regs <- weakenRegCond sym p (eqCondRegs cond)
-  let (PAS.NamedAsms mr) = (eqCondMaxRegion cond)
-  mrCond <- PAS.NamedAsms <$> PAS.weaken sym p mr
-  let (PAS.NamedAsms pc) = (eqCondExtraCond cond)
-  pcond <- PAS.NamedAsms <$> PAS.weaken sym p pc
-  return $ EquivalenceCondition mem regs mrCond pcond
+weaken sym p cond = case W4.asConstantPred p of
+  Just True -> return cond
+  _ -> do
+    mem <- WPM.weaken sym p (eqCondMem cond)
+    regs <- weakenRegCond sym p (eqCondRegs cond)
+    let (PAS.NamedAsms mr) = (eqCondMaxRegion cond)
+    mrCond <- PAS.NamedAsms <$> PAS.weaken sym p mr
+    let (PAS.NamedAsms pc) = (eqCondExtraCond cond)
+    pcond <- PAS.NamedAsms <$> PAS.weaken sym p pc
+    return $ EquivalenceCondition mem regs mrCond pcond
 
 -- | Preconditions for graph nodes. These represent additional conditions
 --   that must be true for the equivalence domain of the node to be considered

src/Pate/Monad/PairGraph.hs

@@ -22,6 +22,7 @@ module Pate.Monad.PairGraph
   , catchPG
   , liftEqM
   , liftEqM_
+  , evalEqM
   , initializePairGraph
   , initialDomain
   , initialDomainSpec
@@ -147,6 +148,12 @@ liftEqM_ ::
   StateT (PairGraph sym arch) (EquivM_ sym arch) ()
 liftEqM_ f = liftEqM $ \pg -> ((),) <$> (f pg)
 
+evalEqM :: 
+  HasCallStack =>
+  (PairGraph sym arch -> EquivM_ sym arch a) -> 
+  StateT (PairGraph sym arch) (EquivM_ sym arch) a
+evalEqM f = liftEqM $ \pg -> f pg >>= \a -> return (a, pg)
+
 liftPartEqM_ :: 
   (PairGraph sym arch -> EquivM_ sym arch (Maybe (PairGraph sym arch))) -> 
   StateT (PairGraph sym arch) (EquivM_ sym arch) Bool

src/Pate/Verification/PairGraph.hs

@@ -423,7 +423,7 @@ data ConditionKind =
   | ConditionEquiv
   -- ^ a separate category for equivalence conditions, which should be shown
   --   to the user once the analysis is complete
-  deriving (Eq,Ord, Enum, Bounded)
+  deriving (Eq,Ord, Enum, Bounded, Show)
 
 data PropagateKind =
     PropagateFull

src/Pate/Verification/Simplify.hs

@@ -44,6 +44,8 @@ import qualified Pate.Equivalence.Error as PEE
 import           Pate.Monad
 import qualified What4.ExprHelpers as WEH
 import           What4.ExprHelpers (Simplifier, SimpStrategy)
+import           What4.Simplify.Array
+import           What4.Simplify.Bitvector (memWritePrettySimplify)
 import           Pate.TraceTree
 import qualified Data.Set as Set
 import Pate.AssumptionSet
@@ -240,14 +242,17 @@ unfoldDefsStrategy = WEH.joinStrategy $ withValid $ return $ WEH.SimpStrategy $
 --   Interleaved with the deep predicate simplifier in order to
 --   drop any redundant terms that are introduced.
 prettySimplifier :: forall sym arch. SimpStrategy sym (EquivM_ sym arch)
-prettySimplifier = deepPredicateSimplifier <> base <> unfoldDefsStrategy <> deepPredicateSimplifier <> unfoldDefsStrategy <> base
+prettySimplifier = deepPredicateSimplifier <> base <> unfoldDefsStrategy <> deepPredicateSimplifier <> unfoldDefsStrategy <> base <> (WEH.joinStrategy $ withValid $ return $ memWritePrettySimplify)
   where
     mem :: SimpStrategy sym (EquivM_ sym arch)
     mem = WEH.joinStrategy $ withValid $ return WEH.memReadPrettySimplify
 
     base :: SimpStrategy sym (EquivM_ sym arch)
     base = WEH.joinStrategy $ withValid $ 
-      return $ WEH.bvPrettySimplify <> WEH.memReadPrettySimplify <> WEH.collapseBVOps
+      return $ WEH.bvPrettySimplify 
+      <> WEH.memReadPrettySimplify 
+      <> WEH.collapseBVOps 
+      <> multiArraySimplify
 
 -- TODO: the "core" simplification strategy that stitches together the main strategies
 -- from 'What4.ExprHelpers'. These are implemented in "old" style (i.e. as expression

src/Pate/Verification/StrongestPosts.hs

@@ -612,12 +612,13 @@ initSingleSidedDomain sne pg0 = withRepr bin $ withRepr (PBi.flipRepr bin) $ wit
     mbindsThis <- lift $ lookupFnBindings scope (GraphNode sne) pg0
     mbindsOther <- lift $ lookupFnBindings scope sne_other pg0
 
-    let rewrite_assert exprBinds pg = fnTrace "rewrite_assert" $ case getCondition pg nd ConditionAsserted of
+    let rewrite_cond condK exprBinds pg = fnTrace "rewrite_cond" $ case getCondition pg nd condK of
           Just condSpec -> do
             cond <- liftIO $ PS.bindSpec sym (PS.scopeVarsPair scope) condSpec
             cond' <- PSi.applySimpStrategy (PSi.rewriteStrategy exprBinds) cond
             let condSpec' = PS.mkSimSpec scope cond'
-            let pg' = setCondition nd ConditionAsserted PropagateFull condSpec' pg
+            let propK = getPropagationKind pg nd condK
+            let pg' = setCondition nd condK propK condSpec' pg
             -- we need to schedule the ancestors here to ensure that the resulting
             -- assertion is propagated (if needed), since 'propagateOne' doesn't do this step
             return $ queueAncestors (lowerPriority pr) nd pg'
@@ -626,9 +627,10 @@ initSingleSidedDomain sne pg0 = withRepr bin $ withRepr (PBi.flipRepr bin) $ wit
 
     let do_widen binds pg = fnTrace "do_widen" $ do
           atPriority (raisePriority pr) (Just "Starting Split Analysis") $  do
-            pg2 <- propagateOne scope bundle nd nd_single ConditionAsserted pg >>= \case
+            pg2 <- propagateOne scope bundle [ConditionAssumed, ConditionEquiv] nd nd_single ConditionAsserted pg >>= \case
               (ConditionNotPropagated, pg1) -> return pg1
-              (_, pg1) -> rewrite_assert binds pg1
+              (ConditionPropagated preconds, pg1) -> foldM (\pg_ condK -> rewrite_cond condK binds pg_) pg1 (ConditionAsserted:preconds) 
+              (ConditionInfeasible, pg1) -> rewrite_cond ConditionAsserted binds pg1
 
             withAssumptionSet (PAS.fromExprBindings binds) $ withGraphNode' scope nd bundle dom pg2 $ do
               widenAlongEdge scope bundle nd dom_single pg2 nd_single
@@ -821,8 +823,9 @@ mergeSingletons sneO sneP pg = fnTrace "mergeSingletons" $ withSym $ \sym -> do
               let sne_other = Qu.quantEach snePair (PBi.flipRepr bin) 
               let nd = GraphNode $ singleToNodeEntry sne
               let scope = singleBundleScope sbundle
-              liftEqM $ \pg_ -> propagateOne scope  (singleBundle sbundle) nd syncNode ConditionAsserted pg_ >>= \case
-                (ConditionNotPropagated, pg_') -> 
+
+              liftEqM $ \pg_ -> propagateOne scope  (singleBundle sbundle) [ConditionAssumed, ConditionEquiv] nd syncNode ConditionAsserted pg_ >>= \case
+                (ConditionNotPropagated, _) -> 
                   -- bindings already assumed above
                   return (W4.truePred sym, pg_)
                 (_, pg_') -> do
@@ -1525,7 +1528,7 @@ withConditionsAssumed ::
   EquivM_ sym arch (PairGraph sym arch) ->
   EquivM sym arch (PairGraph sym arch)
 withConditionsAssumed scope bundle d node gr0 f = do
-  foldr go f' [minBound..maxBound]
+  foldr go f' [ConditionEquiv, ConditionAssumed, ConditionAsserted]
   where 
     f' = withSym $ \sym -> case asSingleNode node of
       Just (Some (Qu.AsSingle snode)) ->