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/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 diff --git a/src/Pate/TraceTree.hs b/src/Pate/TraceTree.hs index bbbd4c65..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 @@ -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 = 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)) 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 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 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/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-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 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 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: