From c35db93ab07c5f8fbdf9bf312950f9aa94212851 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:15:44 -0800 Subject: [PATCH 1/9] Pate.TraceTree.resolveQuery: drop pretty-printer layout when matching output This resolves an issue where matches would fail against nodes with output that was too long, causing the pretty-printer to insert newlines and thus no longer matching the string in the script. --- src/Pate/TraceTree.hs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index bbbd4c65..1e750d78 100644 --- a/src/Pate/TraceTree.hs +++ b/src/Pate/TraceTree.hs @@ -377,13 +377,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 = From ea2c6a124eed82d608622a7fe6507fb1d1f9d892 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:18:47 -0800 Subject: [PATCH 2/9] Pate.Loader: move toplevel script parsing step to Pate.Loader --- src/Pate/CLI.hs | 11 ++--------- src/Pate/Loader.hs | 15 ++++++++++++++- src/Pate/TraceTree.hs | 1 + 3 files changed, 17 insertions(+), 10 deletions(-) diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs index 47bd079d..485b5125 100644 --- a/src/Pate/CLI.hs +++ b/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 diff --git a/src/Pate/Loader.hs b/src/Pate/Loader.hs index 6a0f887a..afdd81da 100644 --- a/src/Pate/Loader.hs +++ b/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 }} diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index 1e750d78..6a0f0598 100644 --- a/src/Pate/TraceTree.hs +++ b/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 From ee1e11af1f1779e3a3bb109caf30b5d72ea57e3b Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:20:18 -0800 Subject: [PATCH 3/9] Pate.Script: allow for matching strings that start with integers Wraps the int-prefixed parser in "try" (i.e. trying to match 'N:') so that it can backtrack when the ':' token is not found and fallthrough to parsing it as just a string. Needed to allow string queries that start with hex values --- src/Pate/Script.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Pate/Script.hs b/src/Pate/Script.hs index 28f1e925..9639b46f 100644 --- a/src/Pate/Script.hs +++ b/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 From 96bd7f4639c9a84b151e2b73ee8ef3d6be18312c Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:24:21 -0800 Subject: [PATCH 4/9] PairGraph.Node: support sync points at any call depth When the graph node for a synchronization point is created, it now inherits the calling context of the desync point, rather than dropping it. --- src/Pate/Verification/PairGraph.hs | 14 ++++++++++---- src/Pate/Verification/PairGraph/Node.hs | 5 +++++ 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/src/Pate/Verification/PairGraph.hs b/src/Pate/Verification/PairGraph.hs index 96e6c12f..e6db935b 100644 --- a/src/Pate/Verification/PairGraph.hs +++ b/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)) diff --git a/src/Pate/Verification/PairGraph/Node.hs b/src/Pate/Verification/PairGraph/Node.hs index df7d4d1f..b69b2726 100644 --- a/src/Pate/Verification/PairGraph/Node.hs +++ b/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)) From 8662bb82cc5461b7a7a367a75ca906babb7a3d29 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:35:54 -0800 Subject: [PATCH 5/9] TestBase: use ".pate" script files when present for any given test Script files are not used for self-equivalence tests --- tests/TestBase.hs | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/tests/TestBase.hs b/tests/TestBase.hs index 390ecd38..41cdd3f2 100644 --- a/tests/TestBase.hs +++ b/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 From deec0173b81e29aca6c5c4bba68341de2b432c3a Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 13:38:51 -0800 Subject: [PATCH 6/9] add script for desync-defer test --- tests/aarch32/desync-defer.pate | 43 +++++++++++++++++++++++++ tests/aarch32/unequal/desync-defer.pate | 43 +++++++++++++++++++++++++ 2 files changed, 86 insertions(+) create mode 100644 tests/aarch32/desync-defer.pate create mode 100644 tests/aarch32/unequal/desync-defer.pate diff --git a/tests/aarch32/desync-defer.pate b/tests/aarch32/desync-defer.pate new file mode 100644 index 00000000..f9be70a1 --- /dev/null +++ b/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 diff --git a/tests/aarch32/unequal/desync-defer.pate b/tests/aarch32/unequal/desync-defer.pate new file mode 100644 index 00000000..f9be70a1 --- /dev/null +++ b/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 From 5ed8b7f3917ec6bc3b933c36931e52ef584e21ac Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 14:04:05 -0800 Subject: [PATCH 7/9] add scripts for desync-simple tests --- tests/aarch32/desync-simple.pate | 18 ++++++++++++++++++ tests/aarch32/unequal/desync-simple.pate | 18 ++++++++++++++++++ 2 files changed, 36 insertions(+) create mode 100644 tests/aarch32/desync-simple.pate create mode 100644 tests/aarch32/unequal/desync-simple.pate diff --git a/tests/aarch32/desync-simple.pate b/tests/aarch32/desync-simple.pate new file mode 100644 index 00000000..e80d7d20 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/aarch32/unequal/desync-simple.pate b/tests/aarch32/unequal/desync-simple.pate new file mode 100644 index 00000000..e80d7d20 --- /dev/null +++ b/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 \ No newline at end of file From 36dd42cd17fd1e884d39908e2ae6eb601247f469 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 14:05:34 -0800 Subject: [PATCH 8/9] mark desync-defer and desync-simple tests as expected success --- tests/AArch32TestMain.hs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/AArch32TestMain.hs b/tests/AArch32TestMain.hs index 6d6398b0..8737b707 100644 --- a/tests/AArch32TestMain.hs +++ b/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 From af42ee2cb23a5237061432e0ed366c4eb0a14659 Mon Sep 17 00:00:00 2001 From: Daniel Matichuk Date: Thu, 8 Feb 2024 14:07:33 -0800 Subject: [PATCH 9/9] add 'test_run' makefile target for running tests interactively --- tests/template.mk | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/tests/template.mk b/tests/template.mk index 96227fd8..35f9da9f 100644 --- a/tests/template.mk +++ b/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: