Dm/desync

src/Pate/CLI.hs

@@ -93,6 +93,7 @@ mkRunConfig archLoader opts mtt = let
         , PC.cfgTargetEquivRegs = targetEquivRegs opts
         , PC.cfgRescopingFailureMode = rerrMode opts
         , PC.cfgScriptPath = scriptPath opts
+        , PC.cfgTraceTree = fromMaybe noTraceTree mtt
         }
     cfg = PL.RunConfig
         { PL.archLoader = archLoader
@@ -105,15 +106,7 @@ mkRunConfig archLoader opts mtt = let
         , PL.useDwarfHints = not $ noDwarfHints opts
         , PL.elfLoaderConfig = PLE.defaultElfLoaderConfig { PLE.ignoreSegments = ignoreSegments opts }
         }
-
-  in case PC.cfgScriptPath (PL.verificationCfg cfg) of
-        Just fp -> PSc.readScript fp >>= \case
-          Left err -> return $ Left (show err)
-          Right scr -> do
-            let tt = fromMaybe noTraceTree mtt
-            tt' <- PSc.attachToTraceTree scr tt
-            return $ Right $ PL.setTraceTree tt' cfg
-        Nothing -> return $ Right $ PL.setTraceTree (fromMaybe noTraceTree mtt) cfg
+  in PL.parseAndAttachScript cfg
 
 data CLIOptions = CLIOptions
   { originalBinary :: FilePath

src/Pate/Loader.hs

@@ -13,8 +13,8 @@ module Pate.Loader
   , runSelfEquivConfig
   , runEquivConfig
   , RunConfig(..)
-  , setTraceTree
   , Logger(..)
+  , parseAndAttachScript
   )
 where
 
@@ -58,6 +58,19 @@ data RunConfig =
     , elfLoaderConfig :: ElfLoaderConfig
     }
 
+parseAndAttachScript ::
+  RunConfig ->
+  IO (Either String RunConfig)
+parseAndAttachScript cfg = case PC.cfgScriptPath (verificationCfg cfg) of
+    Just fp -> PS.readScript fp >>= \case
+      Left err -> return $ Left (show err)
+      Right scr -> do
+        let tt = PC.cfgTraceTree $ verificationCfg cfg
+        tt' <- PS.attachToTraceTree scr tt
+        return $ Right $ setTraceTree tt' cfg
+    Nothing -> return $ Right cfg
+
+
 setTraceTree :: SomeTraceTree PA.ValidRepr -> RunConfig -> RunConfig
 setTraceTree traceTree rcfg = rcfg { verificationCfg = (verificationCfg rcfg){ PC.cfgTraceTree = traceTree }}
 

src/Pate/Script.hs

@@ -138,8 +138,8 @@ matchAnyAct = NodeFinalAction $ \_ -> return True
 
 parseIdentQuery :: Parser NodeIdentQuery
 parseIdentQuery =
-  (do
-    i <- int
+  P.try (do
+    i <-  int
     _ <- ":"
     s <- P.many (P.notFollowedBy (P.newline) >> L.charLiteral)
     case s of

src/Pate/TraceTree.hs

@@ -134,6 +134,7 @@ import           Control.Monad (void, unless, forM) -- GHC 9.6
 import           Control.Applicative
 
 import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.String as PP
 
 import qualified Data.Aeson as JSON
 import qualified Compat.Aeson as JSON
@@ -377,13 +378,14 @@ resolveQuery (NodeQuery (q_outer:qs_outer) fin_outer) t_outer =
       -- we need to reverse it here so the indices match up
       fmap catMaybes $ forM (zip [0..] (reverse nodes')) $ \(i,(SomeTraceNode (nm :: SymbolRepr nm) lbl v, t)) -> do
         Just pp <- return $ getNodePrinter @k @nm [Simplified]
+        let as_string = PP.renderString $ PP.layoutPretty (PP.defaultLayoutOptions { PP.layoutPageWidth = PP.Unbounded }) (pp lbl v)
         let matched = case q of
               QueryInt i' -> i == i'
-              QueryString s -> isPrefixOf s (show (pp lbl v))
-              QueryStringInt i' s -> i == i' && isPrefixOf s (show (pp lbl v))
+              QueryString s -> isPrefixOf s as_string
+              QueryStringInt i' s -> i == i' && isPrefixOf s as_string
               QueryAny -> True
         case matched of
-          True -> return $ Just $ (QueryStringInt i (show (pp lbl v)), SomeTraceNode nm lbl v,t)
+          True -> return $ Just $ (QueryStringInt i as_string, SomeTraceNode nm lbl v,t)
           False -> return Nothing
 
 data InteractionMode =

src/Pate/Verification/PairGraph.hs

@@ -110,7 +110,7 @@ module Pate.Verification.PairGraph
 
 import           Prettyprinter
 
-import           Control.Monad (foldM)
+import           Control.Monad (foldM, guard)
 import           Control.Monad.IO.Class
 import qualified Control.Lens as L
 import           Control.Lens ( (&), (.~), (^.), (%~) )
@@ -147,7 +147,7 @@ import qualified Pate.Verification.Domain as PVD
 import qualified Pate.SimState as PS
 
 
-import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, NodeReturn, pattern GraphNodeEntry, pattern GraphNodeReturn, rootEntry, nodeBlocks, rootReturn, nodeFuns, graphNodeBlocks, getDivergePoint )
+import           Pate.Verification.PairGraph.Node ( GraphNode(..), NodeEntry, NodeReturn, pattern GraphNodeEntry, pattern GraphNodeReturn, rootEntry, nodeBlocks, rootReturn, nodeFuns, graphNodeBlocks, getDivergePoint, divergePoint, mkNodeEntry, mkNodeReturn, nodeContext )
 import           Pate.Verification.StrongestPosts.CounterExample ( TotalityCounterexample(..), ObservableCounterexample(..) )
 
 import qualified Pate.Verification.AbstractDomain as PAD
@@ -972,17 +972,23 @@ combineNodes node1 node2 = do
   (nodeO, nodeP) <- case PPa.get PBi.OriginalRepr (graphNodeBlocks node1) of
     Just{} -> return (node1, node2)
     Nothing -> return (node2, node1)
+  -- it only makes sense to combine nodes that share a divergence point,
+  -- where that divergence point will be used as the calling context for the
+  -- merged point
+  GraphNode divergeO <- divergePoint $ nodeContext nodeO
+  GraphNode divergeP <- divergePoint $ nodeContext nodeP
+  guard $ divergeO == divergeP
   case (nodeO, nodeP) of
     (GraphNode nodeO', GraphNode nodeP') -> do
       blocksO <- PPa.get PBi.OriginalRepr (nodeBlocks nodeO')
       blocksP <- PPa.get PBi.PatchedRepr (nodeBlocks nodeP')
       -- FIXME: retain calling context?
-      return $ GraphNode $ rootEntry (PPa.PatchPair blocksO blocksP)
+      return $ GraphNode $ mkNodeEntry divergeO (PPa.PatchPair blocksO blocksP)
     (ReturnNode nodeO', ReturnNode nodeP') -> do
       fnsO <- PPa.get PBi.OriginalRepr (nodeFuns nodeO')
       fnsP <- PPa.get PBi.PatchedRepr (nodeFuns nodeP')
       -- FIXME: retain calling context?
-      return $ ReturnNode $ rootReturn (PPa.PatchPair fnsO fnsP)
+      return $ ReturnNode $ mkNodeReturn divergeO (PPa.PatchPair fnsO fnsP)
     _ -> Nothing
 
 singleNodeRepr :: GraphNode arch -> Maybe (Some (PBi.WhichBinaryRepr))

src/Pate/Verification/PairGraph/Node.hs

@@ -22,6 +22,8 @@ module Pate.Verification.PairGraph.Node (
   , CallingContext
   , pattern GraphNodeEntry
   , pattern GraphNodeReturn
+  , nodeContext
+  , divergePoint
   , graphNodeBlocks
   , mkNodeEntry
   , mkNodeEntry'
@@ -87,6 +89,9 @@ graphNodeBlocks :: GraphNode arch -> PB.BlockPair arch
 graphNodeBlocks (GraphNode ne) = nodeBlocks ne
 graphNodeBlocks (ReturnNode ret) = TF.fmapF PB.functionEntryToConcreteBlock (nodeFuns ret)
 
+nodeContext :: GraphNode arch -> CallingContext arch
+nodeContext (GraphNode nd) = graphNodeContext nd
+nodeContext (ReturnNode ret) = returnNodeContext ret
 
 pattern GraphNodeEntry :: PB.BlockPair arch -> GraphNode arch
 pattern GraphNodeEntry blks <- (GraphNode (NodeEntry _ blks))

tests/AArch32TestMain.hs

@@ -9,9 +9,8 @@ main = do
         { testArchName = "aarch32"
         , testArchLoader = AArch32.archLoader
         , testExpectEquivalenceFailure =
-            [ "stack-struct", "unequal/stack-struct", "max-signed",
+            [ "stack-struct", "unequal/stack-struct", "max-signed"
               -- missing interactive test support
-              "desync-defer", "desync-simple"
             ]
         , testExpectSelfEquivalenceFailure = []
         -- TODO: we should define a section name here and read its address

tests/TestBase.hs

@@ -131,9 +131,9 @@ doTest ::
 doTest mwb cfg sv fp = do
   infoCfgExists <- doesFileExist (fp <.> "toml")
   argFileExists <- doesFileExist (fp <.> "args")
+  scriptFileExists <- doesFileExist (fp <.> "pate")
 
   (logsRef :: IOR.IORef [String]) <- IOR.newIORef []
-
   let
     addLogMsg :: String -> IO ()
     addLogMsg msg = IOR.atomicModifyIORef' logsRef $ \logs -> (msg : logs, ())
@@ -158,9 +158,14 @@ doTest mwb cfg sv fp = do
           let (msg, _exit) = OA.renderFailure failure progn
           failTest ("Input: \n" ++ (show optsList) ++ "\n" ++ msg)
         _ -> failTest "unexpected parser result"
-    False -> let
-      infoPath = if infoCfgExists then Just $ fp <.> "toml" else Nothing
-      in return $ ("./", PL.RunConfig
+    False -> do
+      let infoPath = if infoCfgExists then Just $ fp <.> "toml" else Nothing
+      -- only include the script for the equivalence proof, for self-equivalence we
+      -- assume no script
+      -- NB: this is not necessarily true if code discovery requires input, but we don't have
+      -- any tests that require this at the moment
+      let scriptPath = if scriptFileExists && not (isJust mwb) then Just (fp <.> "pate") else Nothing
+      mrcfg <- PL.parseAndAttachScript $ PL.RunConfig
         { PL.patchInfoPath = infoPath
         , PL.patchData = defaultPatchData cfg
         , PL.origPaths = PLE.simplePaths (fp <.> "original" <.> "exe")
@@ -173,6 +178,7 @@ doTest mwb cfg sv fp = do
               , PC.cfgIgnoreUnnamedFunctions = False
               , PC.cfgIgnoreDivergedControlFlow = False
               , PC.cfgStackScopeAssume = False
+              , PC.cfgScriptPath = scriptPath
               }
         , PL.logger = \(PA.SomeValidArch{}) -> do
             let
@@ -196,7 +202,11 @@ doTest mwb cfg sv fp = do
         , PL.archLoader = testArchLoader cfg
         , PL.useDwarfHints = False
         , PL.elfLoaderConfig = PLE.defaultElfLoaderConfig
-        })
+        }
+      case mrcfg of
+        Left err -> failTest err
+        Right rcfg -> return ("./", rcfg)
+
   result <- withCurrentDirectory dir $ case mwb of
     Just wb -> PL.runSelfEquivConfig rcfg wb
     Nothing -> PL.runEquivConfig rcfg

tests/aarch32/desync-defer.pate

@@ -0,0 +1,43 @@
+Choose Entry Point
+    > Function Entry "_start"
+
+Function Entry "f" (0x10158)
+    ...
+    Call to: "malloc" (0x10104) Returns to: "f" (0x10178) (original) vs. Call to: "write" (0x100d8) Returns to: "f" (0x101a8) (patched)
+        ...
+        ...
+        > Choose desynchronization points
+
+        ...
+        Choose a desynchronization point:
+            > 0x1016c (original)
+            > 0x1016c (patched)
+            // 0x1070 - should be this, but the splitting for desync points is incorrect
+
+0x10170 [ via: "f" (0x10158) <- "_start" (0x10218) (original) vs. "_start" (0x10214) (patched) ]
+    ...
+    Call to: "malloc"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > 0x10188 (original)
+            > 0x10178 (patched)
+
+0x101e8 (original) vs. 0x101d8 (patched)
+    ...
+    Return (original) vs. Call to: "g"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > Return "f" (0x10158)
+            // applies to both original and patched
+
+Verification Finished
+Continue verification?
+    > Finish and view final result

tests/aarch32/desync-simple.pate

@@ -0,0 +1,18 @@
+Choose Entry Point
+    > Function Entry "_start"
+
+Function Entry "f"
+    ...
+    Call to: "clock"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > 0x8058 (original)
+            > 0x8054 (patched)
+
+Verification Finished
+Continue verification?
+    > Finish and view final result

tests/aarch32/unequal/desync-defer.pate

@@ -0,0 +1,43 @@
+Choose Entry Point
+    > Function Entry "_start"
+
+Function Entry "f" (0x10158)
+    ...
+    Call to: "malloc" (0x10104) Returns to: "f" (0x10178) (original) vs. Call to: "write" (0x100d8) Returns to: "f" (0x101a8) (patched)
+        ...
+        ...
+        > Choose desynchronization points
+
+        ...
+        Choose a desynchronization point:
+            > 0x1016c (original)
+            > 0x1016c (patched)
+            // 0x1070 - should be this, but the splitting for desync points is incorrect
+
+0x10170 [ via: "f" (0x10158) <- "_start" (0x10218) (original) vs. "_start" (0x10214) (patched) ]
+    ...
+    Call to: "malloc"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > 0x10188 (original)
+            > 0x10178 (patched)
+
+0x101e8 (original) vs. 0x101d8 (patched)
+    ...
+    Return (original) vs. Call to: "g"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > Return "f" (0x10158)
+            // applies to both original and patched
+
+Verification Finished
+Continue verification?
+    > Finish and view final result

tests/aarch32/unequal/desync-simple.pate

@@ -0,0 +1,18 @@
+Choose Entry Point
+    > Function Entry "_start"
+
+Function Entry "f"
+    ...
+    Call to: "clock"
+        ...
+        ...
+        > Choose synchronization points
+
+        ...
+        Choose a synchronization point:
+            > 0x8058 (original)
+            > 0x8054 (patched)
+
+Verification Finished
+Continue verification?
+    > Finish and view final result

tests/template.mk

@@ -39,6 +39,11 @@ malloc-%.exe: ./build/malloc-%.s ./build/link.ld
 	diff ./dumps/$(basename $@).original.dump ./dumps/$(basename $@).patched.dump || true
 	diff ./dumps/$(basename $@).original.dump ./dumps/$(basename $@).patched-bad.dump || true
 
+%.test_run: %.original.exe %.patched.exe
+	../../pate.sh -o $(basename $@).original.exe -p $(basename $@).patched.exe \
+		`( (test -f $(basename $@).toml && echo "-b $(basename $@).toml") || echo "")` \
+		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")`
+
 .PRECIOUS: ./build/%.s ./build/%.i %.exe malloc-%.exe ./unequal/%.original.exe ./unequal/%.patched.exe
 
 clean: