cli, concurrency, syntax: Pretty-print syntax errors

GaloisInc · Jan 22, 2025 · 0762355 · 0762355
1 parent 0f1b3b8
commit 0762355
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 8 deletions.
diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -27,6 +27,8 @@ import Data.Map (Map)
 import Data.Text (Text)
 import Data.String (IsString(..))
 import qualified Data.Text.IO as T
+import qualified Prettyprinter as PP
+import qualified Prettyprinter.Render.Text as PP
 import System.IO
 import System.Exit
 import Text.Megaparsec as MP
@@ -43,7 +45,6 @@ import Lang.Crucible.CFG.SSAConversion
 
 import Lang.Crucible.Syntax.Atoms
 import Lang.Crucible.Syntax.Concrete
-import Lang.Crucible.Syntax.ExprParse (printSyntaxError)
 import Lang.Crucible.Syntax.Prog (doParseCheck, assertNoExterns, assertNoForwardDecs)
 import Lang.Crucible.Syntax.SExpr
 
@@ -139,8 +140,8 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
             let hdls = [ (SomeHandle h, p) | (FnBinding h _,p) <- ovrs ]
             parseResult <- top ng ha hdls $ prog v
             case parseResult of
-              Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
-              Left err -> hPutStrLn outh $ show err
+              Left e ->
+                T.hPutStrLn outh (PP.renderStrict (PP.layoutPretty PP.defaultLayoutOptions (PP.pretty e)))
               Right (ParsedProgram{ parsedProgCFGs = cs
                                   , parsedProgExterns = externs
                                   , parsedProgForwardDecs = fds

diff --git a/crucible-concurrency/crucible-concurrency.cabal b/crucible-concurrency/crucible-concurrency.cabal
@@ -39,6 +39,7 @@ library
                      , megaparsec
                      , mtl
                      , parameterized-utils
+                     , prettyprinter
                      , simple-get-opt < 0.5
                      , text
                      , vector

diff --git a/crucible-concurrency/src/Cruces/CrucesMain.hs b/crucible-concurrency/src/Cruces/CrucesMain.hs
@@ -20,6 +20,7 @@ import Data.List (find)
 import qualified Data.Map as Map
 import Data.Text (pack)
 import Data.String (IsString(..))
+import qualified Prettyprinter as PP
 import System.Exit
 import Text.Megaparsec as MP
 
@@ -138,8 +139,7 @@ run (cruxOpts, opts) =
                      let ?parserHooks = defaultParserHooks
                      parseResult <- top nonceGen ha builtins $ prog v
                      case parseResult of
-                       Left (SyntaxParseError e) -> error $ show $ printSyntaxError e
-                       Left err -> error $ show err
+                       Left err -> error (show (PP.pretty err))
                        Right (ParsedProgram
                                { parsedProgGlobals = gs
                                , parsedProgExterns = externs

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Prog.hs
@@ -17,6 +17,7 @@ import qualified Data.Map as Map
 import Data.Map (Map)
 import Data.Text (Text)
 import qualified Data.Text.IO as T
+import qualified Prettyprinter as PP
 import System.IO
 import System.Exit
 import Text.Megaparsec as MP
@@ -31,7 +32,6 @@ import Lang.Crucible.CFG.SSAConversion
 
 import Lang.Crucible.Syntax.Concrete
 import Lang.Crucible.Syntax.SExpr
-import Lang.Crucible.Syntax.ExprParse (printSyntaxError)
 import Lang.Crucible.Syntax.Atoms
 
 import Lang.Crucible.Analysis.Postdom
@@ -72,8 +72,7 @@ doParseCheck fn theInput pprint outh =
                 \e -> T.hPutStrLn outh (printExpr e) >> hPutStrLn outh ""
             cs <- top ng ha [] $ prog v
             case cs of
-              Left (SyntaxParseError e) -> T.hPutStrLn outh $ printSyntaxError e
-              Left err -> hPutStrLn outh $ show err
+              Left err -> hPutStrLn outh (show (PP.pretty e))
               Right (ParsedProgram{ parsedProgCFGs = ok
                                   , parsedProgExterns = externs
                                   , parsedProgForwardDecs = fds