add --quickstart option to begin analysis immediately

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

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)"
          )

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
                      }

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

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

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"

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 "<<At top level>>"
+    [] -> case print_msg of
+      True -> PO.printMsgLn "<<At top level>>"
+      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