Merge pull request #281 from GaloisInc/vr/use-doc-for-discovery-error…

…-messages

use Doc for discovery error messages

reopt/Main_reopt.hs

@@ -57,7 +57,6 @@ import Paths_reopt (version)
 import Prettyprinter qualified as PP
 import Prettyprinter.Render.Text qualified as PP
 import Reopt
-import Reopt.CFG.FnRep.X86 ()
 import Reopt.ELFArchInfo (getElfArchInfo)
 import Reopt.EncodeInvariants (
   encodeInvariantFailedMsg,
@@ -728,8 +727,9 @@ showConstraints args elfPath = do
   mr <- runReoptM printLogEvent $ do
     hdrAnn <- resolveHeader (headerPath args) (clangPath args)
 
-    let funPrefix :: BSC.ByteString
-        funPrefix = unnamedFunPrefix args
+    let
+      funPrefix :: BSC.ByteString
+      funPrefix = unnamedFunPrefix args
 
     (os, initState) <- reoptX86Init (loadOptions args) rOpts origElf
     let symAddrMap = initDiscSymAddrMap initState
@@ -836,8 +836,9 @@ performReopt args elfPath = do
   mr <- runReoptM logger2 $ do
     hdrAnn <- resolveHeader (headerPath args) (clangPath args)
 
-    let funPrefix :: BSC.ByteString
-        funPrefix = unnamedFunPrefix args
+    let
+      funPrefix :: BSC.ByteString
+      funPrefix = unnamedFunPrefix args
 
     (os, initState) <- reoptX86Init (loadOptions args) rOpts origElf
     let symAddrMap = initDiscSymAddrMap initState
@@ -890,12 +891,13 @@ performReopt args elfPath = do
             (traceConstraintOrigins args)
 
     -- FIXME: move
-    let prettyDefs =
-          [ PP.pretty n PP.<+> "=" PP.<+> PP.pretty ty
-          | (n, ty) <- mcNamedTypes moduleConstraints
-          ]
-        prettyWarnings =
-          ["# Warning: " <> PP.viaShow w | w <- mcWarnings moduleConstraints]
+    let
+      prettyDefs =
+        [ PP.pretty n PP.<+> "=" PP.<+> PP.pretty ty
+        | (n, ty) <- mcNamedTypes moduleConstraints
+        ]
+      prettyWarnings =
+        ["# Warning: " <> PP.viaShow w | w <- mcWarnings moduleConstraints]
 
     case typedFnsExportPath args of
       Nothing -> pure ()
@@ -933,16 +935,17 @@ performReopt args elfPath = do
                 Right _ -> do
                   funStepFinished AnnotationGeneration fid ()
 
-            let vcgAnn :: Ann.ModuleAnnotations
-                vcgAnn =
-                  Ann.ModuleAnnotations
-                    { Ann.llvmFilePath = llvmPath
-                    , Ann.binFilePath = elfPath
-                    , Ann.pageSize = 4096
-                    , Ann.stackGuardPageCount = 1
-                    , Ann.functions = rights (snd <$> ann)
-                    , Ann.extFunctions = ext
-                    }
+            let
+              vcgAnn :: Ann.ModuleAnnotations
+              vcgAnn =
+                Ann.ModuleAnnotations
+                  { Ann.llvmFilePath = llvmPath
+                  , Ann.binFilePath = elfPath
+                  , Ann.pageSize = 4096
+                  , Ann.stackGuardPageCount = 1
+                  , Ann.functions = rights (snd <$> ann)
+                  , Ann.extFunctions = ext
+                  }
             reoptWriteByteString AnnotationsFileType annPath (Aeson.encode vcgAnn)
             funStepAllFinished AnnotationGeneration ()
 

src/Reopt.hs

@@ -152,6 +152,7 @@ import Data.Macaw.Analysis.RegisterUse (
   ppRegisterUseErrorReason,
  )
 import Data.Macaw.CFG (
+  ArchConstraints,
   ArchFn,
   ArchReg,
   ArchSegmentOff,
@@ -218,7 +219,6 @@ import Data.Parameterized.Some (Some (..))
 import Data.Parameterized.TraversableF (FoldableF)
 import Data.Set qualified as Set
 import Data.String (IsString (..))
-import Data.Text qualified as T
 import Data.Vector qualified as V
 import Data.Word (Word16, Word32, Word64)
 import Flexdis86 qualified as F
@@ -596,7 +596,10 @@ reoptRunInit m =
           Left e -> pure (Left (Events.ReoptInitError e))
           Right v -> c v
 
-checkBlockError :: Macaw.ParsedBlock arch ids -> Maybe Events.DiscoveryError
+checkBlockError ::
+  ArchConstraints arch =>
+  Macaw.ParsedBlock arch ids ->
+  Maybe Events.DiscoveryError
 checkBlockError b = do
   let a = memWordValue $ addrOffset $ segoffAddr $ Macaw.pblockAddr b
   case Macaw.pblockTermStmt b of
@@ -616,7 +619,7 @@ checkBlockError b = do
           , Events.discErrorBlockAddr = a
           , Events.discErrorBlockSize = Macaw.blockSize b
           , Events.discErrorBlockInsnIndex = length (Macaw.pblockStmts b)
-          , Events.discErrorMessage = msg
+          , Events.discErrorMessage = PP.pretty msg
           }
     Macaw.ClassifyFailure _ reasons ->
       Just $!
@@ -626,13 +629,22 @@ checkBlockError b = do
           , Events.discErrorBlockSize = Macaw.blockSize b
           , Events.discErrorBlockInsnIndex = length (Macaw.pblockStmts b)
           , Events.discErrorMessage =
-              "Unclassified control flow transfer.\n"
-                <> T.intercalate "\n" (map (T.pack . ("→ " <>)) reasons)
+              PP.vcat
+                [ "Unclassified control flow transfer"
+                , PP.indent 2 $
+                    PP.vcat
+                      [ "Block statements:"
+                      , PP.indent 2 $ PP.vcat $ map PP.viaShow (Macaw.pblockStmts b)
+                      , "Classifier failures:"
+                      , PP.indent 2 $ PP.vcat $ map PP.viaShow reasons
+                      ]
+                ]
           }
     _ -> Nothing
 
 -- | Prepend discovery event to list of reopt log evnts.
 logDiscEventAsReoptEvents ::
+  ArchConstraints arch =>
   MemWidth (Macaw.ArchAddrWidth arch) =>
   (Events.ReoptLogEvent arch -> IO ()) ->
   Macaw.AddrSymMap (Macaw.ArchAddrWidth arch) ->
@@ -671,6 +683,7 @@ logDiscEventAsReoptEvents logger symMap evt = do
       logger $ Events.ReoptFunStepLog Events.Discovery (mkFunId fa) msg
 
 reoptRunDiscovery ::
+  ArchConstraints arch =>
   MemWidth (Macaw.ArchAddrWidth arch) =>
   Macaw.AddrSymMap (Macaw.ArchAddrWidth arch) ->
   IncCompM (Macaw.DiscoveryEvent arch) a a ->
@@ -1758,6 +1771,7 @@ headerTypeMap hdrAnn dynDepsTypeMap symAddrMap noretMap = do
 
 doDiscovery ::
   forall arch r.
+  ArchConstraints arch =>
   -- | Header with hints for assisting typing.
   AnnDeclarations ->
   Elf.ElfHeaderInfo (Macaw.ArchAddrWidth arch) ->

src/Reopt/ELFArchInfo.hs

@@ -22,8 +22,8 @@ import Data.Vector qualified as V
 import Data.ByteString qualified as BS
 
 import Data.Macaw.Architecture.Info (ArchitectureInfo (..))
+import Data.Macaw.CFG qualified as Macaw
 import Data.Macaw.Utils.IncComp ( incCompLog, IncCompM)
-import Data.Macaw.Discovery qualified as Macaw
 import Reopt.PLTParser as Reopt (
   PLTInfo (..),
   extractPLTEntries,
@@ -46,6 +46,7 @@ type ProcessPLTEntries w =
 
 data SomeArchitectureInfo w where
   SomeArch ::
+    Macaw.ArchConstraints arch =>
     !(ArchitectureInfo arch) ->
     !(ProcessPLTEntries (Macaw.ArchAddrWidth arch)) ->
     SomeArchitectureInfo (Macaw.ArchAddrWidth arch)

src/Reopt/Events.hs

@@ -69,21 +69,10 @@ import Data.Map.Strict qualified as Map
 import Data.Maybe (fromMaybe)
 import Data.Parameterized.Some (Some (..))
 import Data.Text (Text)
-import Data.Text qualified as Text
 import Data.Void (Void)
 import Data.Word (Word64)
 import Numeric (showHex)
-import Prettyprinter (
-  Doc,
-  defaultLayoutOptions,
-  hang,
-  hsep,
-  indent,
-  layoutPretty,
-  pretty,
-  viaShow,
-  vsep,
- )
+import Prettyprinter qualified as PP
 import Prettyprinter.Render.String (renderString)
 import Reopt.ExternalTools qualified as Ext
 import Reopt.FunUseMap (mkFunUseMap, totalFunUseSize)
@@ -160,7 +149,7 @@ data DiscoveryError = DiscoveryError
   , discErrorBlockSize :: !Int
   , discErrorBlockInsnIndex :: !Int
   -- ^ Instruction index.
-  , discErrorMessage :: !Text
+  , discErrorMessage :: !(PP.Doc ())
   }
 
 -------------------------------------------------------------------------------
@@ -391,7 +380,7 @@ printLogEvent event = do
         case s of
           Discovery ->
             unlines $
-              [ printf "  Block 0x%x: %s" (discErrorBlockAddr de) (Text.unpack (discErrorMessage de))
+              [ printf "  Block 0x%x: %s" (discErrorBlockAddr de) (show (discErrorMessage de))
               | de <- e
               ]
                 ++ ["  Incomplete."]
@@ -514,28 +503,28 @@ incStepError stepTag failureTag = Map.alter logFail stepTag
   logFail (Just m) = Just $ Map.alter incErr failureTag m -- otherwise just increment the particular failure
 
 -- | Render the registered failures in an indented list-style Doc.
-renderAllFailures' :: forall a. (Num a, Show a) => StepErrorMap a -> Doc ()
-renderAllFailures' = vsep . map renderStepFailures . Map.toList
+renderAllFailures' :: forall a. (Num a, Show a) => StepErrorMap a -> PP.Doc ()
+renderAllFailures' = PP.vsep . map renderStepFailures . Map.toList
  where
-  renderStepFailures :: (ReoptStepTag, Map ReoptErrorTag a) -> Doc ()
+  renderStepFailures :: (ReoptStepTag, Map ReoptErrorTag a) -> PP.Doc ()
   renderStepFailures (tag, failures) =
     let hdr =
-          hsep
-            [ viaShow $ stepCount failures
-            , pretty "failures during"
-            , pretty (ppReoptStepTag tag) <> pretty " step:"
+          PP.hsep
+            [ PP.viaShow $ stepCount failures
+            , PP.pretty "failures during"
+            , PP.pretty (ppReoptStepTag tag) <> PP.pretty " step:"
             ]
-     in hang 2 $ vsep $ hdr : map renderFailure (Map.toList failures)
-  renderFailure :: (ReoptErrorTag, a) -> Doc ()
-  renderFailure (tag, cnt) = hsep [pretty $ show cnt, pretty $ ppReoptErrorTag tag]
+     in PP.hang 2 $ PP.vsep $ hdr : map renderFailure (Map.toList failures)
+  renderFailure :: (ReoptErrorTag, a) -> PP.Doc ()
+  renderFailure (tag, cnt) = PP.hsep [PP.pretty $ show cnt, PP.pretty $ ppReoptErrorTag tag]
   stepCount :: Map ReoptErrorTag a -> a
   stepCount = foldl' (+) 0 . Map.elems
 
 renderAllFailures :: (Num a, Show a) => StepErrorMap a -> String
 renderAllFailures failures =
   renderString $
-    layoutPretty defaultLayoutOptions $
-      indent 2 $
+    PP.layoutPretty PP.defaultLayoutOptions $
+      PP.indent 2 $
         renderAllFailures' failures
 
 -----------------------------------------------------------------------

src/Reopt/Events/Export.hs

@@ -10,6 +10,8 @@ import Data.ByteString.Lazy qualified as BSL
 import Data.Text (Text)
 import Data.Word (Word64)
 import GHC.Generics (Generic)
+import Prettyprinter qualified as PP
+import Prettyprinter.Render.Text qualified as PP
 import Reopt.Events (
   DiscoveryError (
     discErrorBlockAddr,
@@ -75,7 +77,10 @@ exportEvent h evt =
             let insn = discErrorBlockInsnIndex e
             let sz = discErrorBlockSize e
             let msg = discErrorMessage e
-            emitEvent h $ CFGError f b sz insn msg
+            emitEvent h $
+              CFGError f b sz insn $
+                PP.renderStrict $
+                  PP.layoutPretty PP.defaultLayoutOptions msg
         InvariantInference -> do
           pure ()
         AnnotationGeneration -> do