diff --git a/pate_binja/pate.py b/pate_binja/pate.py index bec7e13d..331d8824 100644 --- a/pate_binja/pate.py +++ b/pate_binja/pate.py @@ -108,7 +108,7 @@ def _run_live(self): # We use a helper script to run logic in the user's shell environment. script = os.path.join(os.path.dirname(os.path.abspath(__file__)), "run-pate.sh") # Need -l to make sure user's env is fully setup (e.g. access to docker and ghc tools). - allArgs = ['/bin/bash', '-l', script, '-o', original, '-p', patched, '--json-toplevel', '--add-trace-constraints'] + args + allArgs = ['/bin/bash', '-l', script, '-o', original, '-p', patched, '--json-toplevel', '--add-trace-constraints', '--quickstart'] + args print('Pate command line: ' + ' '.join(allArgs)) with open(os.path.join(cwd, "lastrun.replay"), "w", encoding='utf-8') as trace: with Popen(allArgs, @@ -550,7 +550,7 @@ def command_loop(self): if self.config_callback: self.config_callback(self.config) rec = self.next_json() - self.command('goto_prompt') + self.command('init_json') while self.command_step(): pass # Enter trace constraint processing mode diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs index f54dd6de..b8239244 100644 --- a/src/Pate/CLI.hs +++ b/src/Pate/CLI.hs @@ -88,6 +88,7 @@ mkRunConfig archLoader opts rcfg mtt = let , PC.cfgIgnoreWarnings = ignoreWarnings opts , PC.cfgAlwaysClassifyReturn = alwaysClassifyReturn opts , PC.cfgTraceConstraints = traceConstraints opts + , PC.cfgQuickStart = quickStart opts } cfg = PL.RunConfig { PL.archLoader = archLoader @@ -142,6 +143,7 @@ data CLIOptions = CLIOptions , alwaysClassifyReturn :: Bool , preferTextInput :: Bool , traceConstraints :: Bool + , quickStart :: Bool } deriving (Eq, Ord, Show) printAtVerbosity @@ -448,4 +450,8 @@ cliOptions = OA.info (OA.helper <*> parser) <*> OA.switch ( OA.long "add-trace-constraints" <> OA.help "Prompt to add additional constraints when generating traces." + ) + <*> OA.switch + ( OA.long "quickstart" + <> OA.help "Start analysis immediately from the given entrypoint (provided from -s)" ) \ No newline at end of file diff --git a/src/Pate/Config.hs b/src/Pate/Config.hs index d07adda3..dbc2ccc4 100644 --- a/src/Pate/Config.hs +++ b/src/Pate/Config.hs @@ -292,6 +292,9 @@ data VerificationConfig validRepr = -- a menu selection , cfgTraceConstraints :: Bool -- ^ flag to determine if the user should be prompted to add constraints to traces + , cfgQuickStart :: Bool + -- ^ flag to indicate that the analysis should start from the provided entrypoint + -- (has no effect if no entrypoint is given) } @@ -320,4 +323,5 @@ defaultVerificationCfg = , cfgAlwaysClassifyReturn = False , cfgPreferTextInput = False , cfgTraceConstraints = False + , cfgQuickStart = False } diff --git a/src/Pate/Verification.hs b/src/Pate/Verification.hs index e02fad27..5423a46f 100644 --- a/src/Pate/Verification.hs +++ b/src/Pate/Verification.hs @@ -262,7 +262,9 @@ doVerifyPairs validArch logAction elf elf' vcfg pd gen sym = do return $ ctx { PMC.parsedFunctionMap = pfm1 }) context' entryPoints -- ordered by preference for chooseEntryPoint - let pPairs' = entryPoints' ++ (unpackedPairs upData) ++ [topEntryPoint] + let pPairs' = case PC.cfgQuickStart vcfg of + True | [singleEntry] <- entryPoints' -> [singleEntry] + _ -> entryPoints' ++ (unpackedPairs upData) ++ [topEntryPoint] let solver = PC.cfgSolver vcfg let saveInteraction = PC.cfgSolverInteractionFile vcfg let diff --git a/src/Pate/Verification/StrongestPosts.hs b/src/Pate/Verification/StrongestPosts.hs index 56ef795d..64ae3f2e 100644 --- a/src/Pate/Verification/StrongestPosts.hs +++ b/src/Pate/Verification/StrongestPosts.hs @@ -218,31 +218,35 @@ asRootEntry (ReturnNode{}) = Nothing -- FIXME: clagged from initializePairGraph chooseEntryPoint :: + forall sym arch. [PB.FunPair arch] -> PairGraph sym arch -> EquivM sym arch (PairGraph sym arch) -chooseEntryPoint entries pg0 = choose @"node" "Choose Entry Point" $ \choice -> do - +chooseEntryPoint entries pg0 = do let knownRoots = Set.fromList (mapMaybe asRootEntry (getAllNodes pg0)) let roots = Set.fromList (mapMaybe (\n -> case n of GraphNode ne -> Just (functionEntryOf ne); _ -> Nothing) (getAllNodes pg0)) let entries' = Set.fromList (map asEntry $ filter (\e -> not (Set.member e knownRoots)) entries) - -- avoid introducing new top-level entries for functions we've already analyzed - -- this is a bit clunky and could be done better - forM_ (Set.union roots entries') $ \nodeEntry -> do - let node = GraphNode nodeEntry - choice "" node $ do - priority <- thisPriority - let pg1 = emptyWorkList $ dropDomain node (priority PriorityDeferred) pg0 - idom <- initialDomainSpec node - rootDom <- PS.forSpec idom $ \_ idom' -> do - vals' <- PPa.forBins $ \bin -> do - vals <- PPa.get bin (PAD.absDomVals idom') - -- FIXME: compute this from the global and stack regions - return $ vals { PAD.absMaxRegion = PAD.AbsIntConstant 3 } - return $ idom' { PAD.absDomVals = vals' } - let pg2 = freshDomain pg1 node (priority PriorityUserRequest) rootDom - let pg3 = emptyReturnVector (dropReturns (returnOfEntry nodeEntry) pg2) (returnOfEntry nodeEntry) - return pg3 + let mkChoice (nodeEntry :: NodeEntry arch) = do + let node = GraphNode nodeEntry + priority <- thisPriority + let pg1 = emptyWorkList $ dropDomain node (priority PriorityDeferred) pg0 + idom <- initialDomainSpec node + rootDom <- PS.forSpec idom $ \_ idom' -> do + vals' <- PPa.forBins $ \bin -> do + vals <- PPa.get bin (PAD.absDomVals idom') + -- FIXME: compute this from the global and stack regions + return $ vals { PAD.absMaxRegion = PAD.AbsIntConstant 3 } + return $ idom' { PAD.absDomVals = vals' } + let pg2 = freshDomain pg1 node (priority PriorityUserRequest) rootDom + let pg3 = emptyReturnVector (dropReturns (returnOfEntry nodeEntry) pg2) (returnOfEntry nodeEntry) + return pg3 + asks (PCfg.cfgQuickStart . envConfig) >>= \case + True | [entry] <- Set.toList entries' -> mkChoice entry + -- avoid introducing new top-level entries for functions we've already analyzed + -- this is a bit clunky and could be done better + _ -> choose @"node" "Choose Entry Point" $ \choice -> do + forM_ (Set.union roots entries') $ \nodeEntry -> + choice "" (GraphNode nodeEntry) $ mkChoice nodeEntry -- | Returns a 'Just' result if we should restart verification after performing -- some interactive modifications diff --git a/tests/integration/packet/packet.exp b/tests/integration/packet/packet.exp index 15ee87e2..bb47822b 100755 --- a/tests/integration/packet/packet.exp +++ b/tests/integration/packet/packet.exp @@ -18,7 +18,7 @@ # Also note this example is mentioned in the README.rst and used in the User Manual. # Major changes here likely warrant an update of the corresponding User Manual content. -spawn ./pate.sh --original tests/integration/packet/packet.original.exe --patched tests/integration/packet/packet.patched.exe -s parse_packet --add-trace-constraints +spawn ./pate.sh --quickstart --original tests/integration/packet/packet.original.exe --patched tests/integration/packet/packet.patched.exe -s parse_packet --add-trace-constraints set timeout 480 @@ -27,19 +27,10 @@ expect_before { eof { send_user "\n\nFAILURE: eof\n"; exit 2 } } -expect "Choose Entry Point" -expect "1: Function Entry \"parse_packet\" (segment1+0x590)" -expect "?>" -send "1\r" -send "top\r" -send "wait\r" - expect "Handle observable difference:" expect "4: Avoid difference with equivalence condition" expect "?>" send "4\r" -send "top\r" -send "wait\r" expect "Continue verification?" expect "0: Finish and view final result" diff --git a/tools/pate-repl/Repl.hs b/tools/pate-repl/Repl.hs index 40d21742..d4d8dfbf 100644 --- a/tools/pate-repl/Repl.hs +++ b/tools/pate-repl/Repl.hs @@ -265,8 +265,14 @@ run rawOpts = do -- input (i.e. the initial prompt to select the symbol to start the analysis from) -- or has somehow finished executing tree_ready <- MVar.newEmptyMVar - topTraceTree' <- forkTraceTreeHook (\tr -> - (runWhenFinishedOrBlocked tr (MVar.putMVar tree_ready ()))) topTraceTree_ + let doQuickStart = + CLI.quickStart opts && length (CLI.startSymbols opts) == 1 + topTraceTree' <- case doQuickStart of + True -> do + -- for quickstart we consider the tree immediately ready + forkTraceTreeHook (\_ -> MVar.putMVar tree_ready ()) topTraceTree_ + False -> forkTraceTreeHook (\tr -> + (runWhenFinishedOrBlocked tr (MVar.putMVar tree_ready ()))) topTraceTree_ cfgE <- CLI.mkRunConfig PAL.archLoader opts PSc.noRunConfig (Just topTraceTree') case cfgE of @@ -323,8 +329,12 @@ run rawOpts = do -- The 'tree_ready' lock ensures that we only get to this point -- once the prompt is actually ready, so we don't need to -- add any explicit delays here. - startup - + case doQuickStart of + True -> case CLI.jsonToplevel opts of + True -> PO.printMsgLn "Pate started" + False -> wait + False -> startup + OA.Failure failure -> do progn <- getProgName let (msg, exit) = OA.renderFailure failure progn @@ -570,15 +580,21 @@ top :: IO () top = execReplM $ (top' >> ls') top' :: ReplM sym arch () -top' = do +top' = top'' True + +top'' :: Bool -> ReplM sym arch () +top'' print_msg = do prevNodes <- gets replPrev case prevNodes of - [] -> PO.printMsgLn "<>" + [] -> case print_msg of + True -> PO.printMsgLn "<>" + False -> return () _ -> do Some init <- return $ last prevNodes loadTraceNode init modify $ \st -> st { replPrev = [] } + status' :: Maybe Int -> IO () status' mlimit = do tr <- IO.readIORef ref @@ -664,17 +680,18 @@ asChoiceTree (node@(TraceNode _ v _)) = case testEquality (knownSymbol @nm) (kno Just Refl -> return $ Just v Nothing -> return Nothing -goto_status'' :: (NodeStatus -> Bool) -> [Some (TraceNode sym arch)] -> ReplM sym arch () +goto_status'' :: (NodeStatus -> Bool) -> [Some (TraceNode sym arch)] -> ReplM sym arch Bool goto_status'' f (Some node@(TraceNode _ _ subtree) : xs) = do st <- IO.liftIO $ getTreeStatus subtree case f st of True -> do - - goto_node' node >> (goto_status' f) + goto_node' node + goto_status' f + return True False -> goto_status'' f xs -goto_status'' f [] = return () +goto_status'' f [] = return False -goto_status' :: (NodeStatus -> Bool) -> ReplM sym arch () +goto_status' :: (NodeStatus -> Bool) -> ReplM sym arch Bool goto_status' f = do updateNextNodes nextNodes <- gets replNext @@ -692,6 +709,18 @@ goto_err = execReplM (goto_status' isErrStatus >> ls') goto_prompt :: IO () goto_prompt = execReplM (goto_status' isBlockedStatus >> ls') +-- | Sent by the front-end after receiving the first message +init_json :: IO () +init_json = do + did_goto <- runReplM $ do + top'' False + goto_status' isBlockedStatus >>= \case + True -> ls' >> return True + False -> return False + case did_goto of + Just True -> return () + _ -> wait + next :: IO () next = execReplM $ do nextNodes <- gets replNext