[refinement] update run-refinement for summary and verbose modes.

refinement/macaw-refinement.cabal

@@ -99,11 +99,13 @@ executable run-refinement
                , macaw-x86-symbolic
                , optparse-applicative
                , parameterized-utils
+               , prettyprinter
                , semmc-ppc
                , text
 
 test-suite test-refinements
   type: exitcode-stdio-1.0
+  buildable: True
   default-language: Haskell2010
   GHC-options: -Wall -Werror -Wcompat
   hs-source-dirs: tests

refinement/tools/run-refinement.hs

@@ -16,26 +16,35 @@ import qualified Data.ElfEdit as E
 import           Data.Foldable
 import qualified Data.Macaw.Architecture.Info as AI
 import           Data.Macaw.BinaryLoader as MBL
-import           Data.Macaw.X86.Symbolic ()
 import           Data.Macaw.BinaryLoader.X86 ()
 import           Data.Macaw.CFG ( ArchAddrWidth )
 import qualified Data.Macaw.Discovery as MD
 import qualified Data.Macaw.Memory.ElfLoader as ML
+import           Data.Macaw.PPC
 import qualified Data.Macaw.Refinement as MR
 import           Data.Macaw.Symbolic ( SymArchConstraints )
-import           GHC.TypeLits
 import qualified Data.Macaw.X86 as MX86
+import           Data.Macaw.X86.Symbolic ()
 import qualified Data.Map as M
+import           Data.Maybe
+import           Data.Monoid
 import           Data.Parameterized.Some
 import           Data.Semigroup
+import           Data.Semigroup ()
 import qualified Data.Text.IO as TIO
+import           Data.Text.Prettyprint.Doc
+import           GHC.TypeLits
 import qualified Options.Applicative as O
-import qualified SemMC.Architecture.PPC64 as PPC64
 import qualified SemMC.Architecture.PPC32 as PPC32
+import qualified SemMC.Architecture.PPC64 as PPC64
 import           System.Exit
 
+import           Prelude
+
 data Options = Options { inputFile :: FilePath
                        , unrefined :: Bool
+                       , summaryOnly :: Bool
+                       , verbose :: Bool
                        }
 
 optionsParser :: O.Parser Options
@@ -44,8 +53,20 @@ optionsParser = Options
                                     <> O.help "The binary ELF file to perform discovery on"
                                   )
                 <*> O.switch ( O.long "unrefined"
+                             <> O.short 'u'
                              <> O.help "No refinement of discovery results"
                              )
+                <*> O.switch ( O.long "summary"
+                             <> O.short 's'
+                             <> O.help "Only show summary of discovery/refinement.\n\
+                                       \Without this flag a full list of all discovered\n\
+                                       \functions and blocks is output."
+                             )
+                <*> O.switch ( O.long "verbose"
+                             <> O.short 'v'
+                             <> O.help "Show verbose information about each discovered\n\
+                                       \function and block."
+                                       )
 
 main :: IO ()
 main = O.execParser optParser >>= doRefinement
@@ -95,17 +116,102 @@ withBinaryDiscoveredInfo :: ( X.MonadThrow m
                          -> m a
 withBinaryDiscoveredInfo opts f arch_info bin = do
   entries <- toList <$> entryPoints bin
-  liftIO $ do putStr "Entrypoints: "
+  when (verbose opts) $
-              putStrLn $ show $ fmap show entries
+    liftIO $ do putStr "Entrypoints: "
-              -- putStrLn $ show (fmap (show . MM.segoffSegment) entries)
+                putStrLn $ show $ fmap show entries
-              -- putStrLn $ show (fmap (show . MM.segoffOffset) entries)
+                -- putStrLn $ show (fmap (show . MM.segoffSegment) entries)
+                -- putStrLn $ show (fmap (show . MM.segoffOffset) entries)
   di <- liftIO $ if unrefined opts
            then return $ MD.cfgFromAddrs arch_info (memoryImage bin) M.empty entries []
            else AI.withArchConstraints arch_info $
                 MR.cfgFromAddrs bin arch_info (memoryImage bin) M.empty entries []
   f di
 
-showDiscoveryInfo _opts di =
+showDiscoveryInfo opts di = do
+  unless (summaryOnly opts) $
+    if verbose opts then showDetails di else showOverview di
+  showSummary di
+
+data Summary = Summary { functionCnt :: Int
+                       , functionsWithErrors :: Int
+                       , blockCnt :: Int
+                       , blockTranslateErrors :: Int
+                       , blockUnknownTargetErrors :: Int -- ClassifyFailure
+                       , maxBlocksPerFunction :: Int
+                       }
+
+instance Semigroup Summary where
+  a <> b =
+    Summary { functionCnt = functionCnt a + functionCnt b
+            , functionsWithErrors = functionsWithErrors a + functionsWithErrors b
+            , blockCnt = blockCnt a + blockCnt b
+            , blockTranslateErrors = blockTranslateErrors a + blockTranslateErrors b
+            , blockUnknownTargetErrors = blockUnknownTargetErrors a + blockUnknownTargetErrors b
+            , maxBlocksPerFunction = max (maxBlocksPerFunction a) (maxBlocksPerFunction b)
+            }
+
+instance Monoid Summary where
+  mempty = Summary 0 0 0 0 0 0
+
+instance Pretty Summary where
+  pretty s = vcat $ catMaybes
+    [ Just $ pretty ":: Function count =" <+> pretty (show $ functionCnt s)
+    , if functionsWithErrors s > 0
+      then Just $ pretty "::    with errors =" <+> pretty (show $ functionsWithErrors s)
+      else Nothing
+    , Just $ pretty ":: Total block count =" <+> pretty (show $ blockCnt s)
+    , Just $ pretty ":: Max blocks/function =" <+> pretty (show $ maxBlocksPerFunction s)
+    , if blockTranslateErrors s > 0
+      then Just (pretty "::  blocks with Translate errors (disassembly) =" <+>
+                 pretty (show $ blockTranslateErrors s))
+      else Nothing
+    , if blockUnknownTargetErrors s > 0
+      then Just (pretty "::  blocks with Classification/Unknown Target errors (discovery) =" <+>
+                 pretty (show $ blockUnknownTargetErrors s))
+      else Nothing
+    ]
+
+showSummary di =
+  let summarizeBlock (_blkAddr, pblk) s =
+        let s' = case MD.stmtsTerm (MD.blockStatementList pblk) of
+                   MD.ParsedTranslateError _ ->
+                     s { blockTranslateErrors = blockTranslateErrors s + 1 }
+                   MD.ClassifyFailure {} ->
+                     s { blockUnknownTargetErrors = blockUnknownTargetErrors s + 1 }
+                   _ -> s
+        in s'
+      summarizeFunction (_funAddr, (Some dfi)) s =
+        let funcSummary = mempty { functionCnt = 1
+                                 , blockCnt = numBlks
+                                 , maxBlocksPerFunction = numBlks
+                                 }
+            blks = (dfi ^. MD.parsedBlocks . to M.toList)
+            numBlks = length blks
+            blksSummary = foldr summarizeBlock funcSummary blks
+            funcErrs = foldr (\a v -> a blksSummary + v) 0 [ blockTranslateErrors, blockUnknownTargetErrors ]
+        in (mappend s blksSummary)
+           { functionsWithErrors = functionsWithErrors s + funcErrs
+           }
+      summarize = vcat [ pretty ":: ==== SUMMARY ===="
+                       , pretty $ foldr summarizeFunction mempty (di ^. MD.funInfo .to M.toList)
+                       ]
+  in putStrLn $ show $ summarize
+
+showOverview di =
+  let getIssue (blkAddr, pblk) =
+        let issue = case MD.stmtsTerm (MD.blockStatementList pblk) of
+              MD.ParsedTranslateError r -> pretty "Translation failure:" <+> pretty (show r)
+              MD.ClassifyFailure _ -> pretty "Classify failure"
+              _ -> emptyDoc
+        in hsep [ pretty "Block @", pretty $ show blkAddr, issue ]
+      funcSummary (funAddr, (Some dfi)) =
+        let blkSummary = map getIssue (dfi ^. MD.parsedBlocks . to M.toList)
+        in vcat [ pretty "Function @" <+> pretty (show funAddr)
+                , indent 2 $ vcat blkSummary
+                ]
+  in putStrLn $ show $ vcat $ map funcSummary (di ^. MD.funInfo .to M.toList)
+
+showDetails di =
   forM_ (M.toList (di ^. MD.funInfo)) $ \(funAddr, Some dfi) -> do
     putStrLn $ "===== BEGIN FUNCTION " ++ show funAddr ++ " ====="
     forM_ (M.toList (dfi ^. MD.parsedBlocks)) $ \(blockAddr, pb) -> do