Update saw-core and adapt to GaloisInc/saw-core#106 "prettyprinter".

Some code within saw-script is also now using `prettyprinter`
instead of `ansi-wl-pprint`.

saw-script.cabal

@@ -65,6 +65,7 @@ library
     , parameterized-utils
     , parsec
     , pretty
+    , prettyprinter
     , pretty-show
     , process
     , rme

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -32,10 +32,10 @@ import           Control.Monad.Trans.Maybe
 import           Control.Monad.Trans (lift)
 import           Control.Lens
 import           Data.Kind (Type)
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 -- what4
-import           What4.ProgramLoc (ProgramLoc(plSourceLoc))
+import           What4.ProgramLoc (ProgramLoc(plSourceLoc), Position)
 
 import qualified Lang.Crucible.Types as Crucible
   (IntrinsicType, EmptyCtx)
@@ -123,35 +123,35 @@ deriving instance (SetupValueHas Show ext) => Show (SetupValue ext)
 --   are implementation details and won't be familiar to users.
 --   Consider using 'resolveSetupValue' and printing an 'LLVMVal'
 --   with @PP.pretty@ instead.
-ppSetupValue :: SetupValue ext -> PP.Doc
+ppSetupValue :: SetupValue ext -> PP.Doc ann
 ppSetupValue setupval = case setupval of
   SetupTerm tm   -> ppTypedTerm tm
-  SetupVar i     -> PP.text ("@" ++ show i)
-  SetupNull _    -> PP.text "NULL"
+  SetupVar i     -> PP.pretty ("@" ++ show i)
+  SetupNull _    -> PP.pretty "NULL"
   SetupStruct _ packed vs
     | packed     -> PP.angles (PP.braces (commaList (map ppSetupValue vs)))
     | otherwise  -> PP.braces (commaList (map ppSetupValue vs))
   SetupArray _ vs  -> PP.brackets (commaList (map ppSetupValue vs))
-  SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.text ("." ++ show i)
-  SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.text ("." ++ f)
-  SetupGlobal _ nm -> PP.text ("global(" ++ nm ++ ")")
-  SetupGlobalInitializer _ nm -> PP.text ("global_initializer(" ++ nm ++ ")")
+  SetupElem _ v i  -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ show i)
+  SetupField _ v f -> PP.parens (ppSetupValue v) PP.<> PP.pretty ("." ++ f)
+  SetupGlobal _ nm -> PP.pretty ("global(" ++ nm ++ ")")
+  SetupGlobalInitializer _ nm -> PP.pretty ("global_initializer(" ++ nm ++ ")")
   where
-    commaList :: [PP.Doc] -> PP.Doc
-    commaList []     = PP.empty
+    commaList :: [PP.Doc ann] -> PP.Doc ann
+    commaList []     = PP.emptyDoc
     commaList (x:xs) = x PP.<> PP.hcat (map (\y -> PP.comma PP.<+> y) xs)
 
-ppTypedTerm :: TypedTerm -> PP.Doc
+ppTypedTerm :: TypedTerm -> PP.Doc ann
 ppTypedTerm (TypedTerm tp tm) =
-  ppTerm defaultPPOpts tm
-  PP.<+> PP.text ":" PP.<+>
-  PP.text (show (Cryptol.ppPrec 0 tp))
+  PP.unAnnotate (ppTerm defaultPPOpts tm)
+  PP.<+> PP.pretty ":" PP.<+>
+  PP.viaShow (Cryptol.ppPrec 0 tp)
 
-ppTypedExtCns :: TypedExtCns -> PP.Doc
+ppTypedExtCns :: TypedExtCns -> PP.Doc ann
 ppTypedExtCns (TypedExtCns tp ec) =
-  ppName (ecName ec)
-  PP.<+> PP.text ":" PP.<+>
-  PP.text (show (Cryptol.ppPrec 0 tp))
+  PP.unAnnotate (ppName (ecName ec))
+  PP.<+> PP.pretty ":" PP.<+>
+  PP.viaShow (Cryptol.ppPrec 0 tp)
 
 setupToTypedTerm ::
   Options {-^ Printing options -} ->
@@ -375,20 +375,26 @@ data CrucibleMethodSpecIR ext =
 
 makeLenses ''CrucibleMethodSpecIR
 
+-- TODO: remove when what4 switches to prettyprinter
+prettyPosition :: Position -> PP.Doc ann
+prettyPosition = PP.viaShow
+
 ppMethodSpec ::
   ( PP.Pretty (MethodId ext)
   , PP.Pretty (ExtType ext)
   ) =>
   CrucibleMethodSpecIR ext ->
-  PP.Doc
+  PP.Doc ann
 ppMethodSpec methodSpec =
-  PP.text "Name: " <> PP.pretty (methodSpec ^. csMethod)
-  PP.<$$> PP.text "Location: " <> PP.pretty (plSourceLoc (methodSpec ^. csLoc))
-  PP.<$$> PP.text "Argument types: "
-  PP.<$$> bullets '-' (map PP.pretty (methodSpec ^. csArgs))
-  PP.<$$> PP.text "Return type: " <> case methodSpec ^. csRet of
-                                       Nothing  -> PP.text "<void>"
+  PP.vcat
+  [ PP.pretty "Name: " <> PP.pretty (methodSpec ^. csMethod)
+  , PP.pretty "Location: " <> prettyPosition (plSourceLoc (methodSpec ^. csLoc))
+  , PP.pretty "Argument types: "
+  , bullets '-' (map PP.pretty (methodSpec ^. csArgs))
+  , PP.pretty "Return type: " <> case methodSpec ^. csRet of
+                                       Nothing  -> PP.pretty "<void>"
                                        Just ret -> PP.pretty ret
+  ]
 
 csAllocations :: CrucibleMethodSpecIR ext -> Map AllocIndex (AllocSpec ext)
 csAllocations

src/SAWScript/Crucible/Common/Override.hs

@@ -64,8 +64,9 @@ import           Data.Kind (Type)
 import           Data.Map (Map)
 import           Data.Set (Set)
 import           Data.Typeable (Typeable)
+import           Data.Void
 import           GHC.Generics (Generic, Generic1)
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
+import qualified Prettyprinter as PP
 
 import qualified Data.Parameterized.Context as Ctx
 import           Data.Parameterized.Some (Some)
@@ -155,9 +156,9 @@ data OverrideFailureReason ext
     -- ^ type mismatch in return specification
   | NonlinearPatternNotSupported
   | BadEqualityComparison -- ^ Comparison on an undef value
-  | BadPointerLoad (Either (MS.PointsTo ext) PP.Doc) PP.Doc
+  | BadPointerLoad (Either (MS.PointsTo ext) (PP.Doc Void)) (PP.Doc Void)
     -- ^ @loadRaw@ failed due to type error
-  | StructuralMismatch PP.Doc PP.Doc (Maybe (ExtType ext)) (ExtType ext)
+  | StructuralMismatch (PP.Doc Void) (PP.Doc Void) (Maybe (ExtType ext)) (ExtType ext)
     -- ^
     -- * pretty-printed simulated value
     -- * pretty-printed specified value
@@ -177,44 +178,56 @@ instance ( PP.Pretty (ExtType ext)
 ppOverrideFailureReason ::
   ( PP.Pretty (ExtType ext)
   , PP.Pretty (MS.PointsTo ext)
-  ) => OverrideFailureReason ext -> PP.Doc
+  ) => OverrideFailureReason ext -> PP.Doc ann
 ppOverrideFailureReason rsn = case rsn of
   AmbiguousPointsTos pts ->
-    PP.text "LHS of points-to assertion(s) not reachable via points-tos from inputs/outputs:" PP.<$$>
-    (PP.indent 2 $ PP.vcat (map PP.pretty pts))
+    PP.vcat
+    [ PP.pretty "LHS of points-to assertion(s) not reachable via points-tos from inputs/outputs:"
+    , PP.indent 2 $ PP.vcat (map PP.pretty pts)
+    ]
   AmbiguousVars vs ->
-    PP.text "Fresh variable(s) not reachable via points-tos from function inputs/outputs:" PP.<$$>
-    (PP.indent 2 $ PP.vcat (map MS.ppTypedExtCns vs))
+    PP.vcat
+    [ PP.pretty "Fresh variable(s) not reachable via points-tos from function inputs/outputs:"
+    , PP.indent 2 $ PP.vcat (map MS.ppTypedExtCns vs)
+    ]
   BadTermMatch x y ->
-    PP.text "terms do not match" PP.<$$>
-    (PP.indent 2 (ppTerm defaultPPOpts x)) PP.<$$>
-    (PP.indent 2 (ppTerm defaultPPOpts y))
+    PP.vcat
+    [ PP.pretty "terms do not match"
+    , PP.indent 2 (PP.unAnnotate (ppTerm defaultPPOpts x))
+    , PP.indent 2 (PP.unAnnotate (ppTerm defaultPPOpts y))
+    ]
   BadPointerCast ->
-    PP.text "bad pointer cast"
-  BadReturnSpecification ty -> PP.vcat $ map PP.text $
-    [ "Spec had no return value, but the function returns a value of type:"
-    , show ty
+    PP.pretty "bad pointer cast"
+  BadReturnSpecification ty ->
+    PP.vcat
+    [ PP.pretty "Spec had no return value, but the function returns a value of type:"
+    , PP.viaShow ty
     ]
   NonlinearPatternNotSupported ->
-    PP.text "nonlinear pattern not supported"
+    PP.pretty "nonlinear pattern not supported"
   BadEqualityComparison ->
-    PP.text "value containing `undef` compared for equality"
+    PP.pretty "value containing `undef` compared for equality"
   BadPointerLoad pointsTo msg ->
-    PP.text "error when loading through pointer that" PP.<+>
-    PP.text "appeared in the override's points-to precondition(s):" PP.<$$>
-    PP.text "Precondition:" PP.<$$>
-      PP.indent 2 (either PP.pretty id pointsTo) PP.<$$>
-    PP.text "Failure reason: " PP.<$$> PP.indent 2 msg -- this can be long
+    PP.vcat
+    [ PP.pretty "error when loading through pointer that" PP.<+>
+      PP.pretty "appeared in the override's points-to precondition(s):"
+    , PP.pretty "Precondition:"
+    , PP.indent 2 (either PP.pretty PP.unAnnotate pointsTo)
+    , PP.pretty "Failure reason: "
+    , PP.indent 2 (PP.unAnnotate msg) -- this can be long
+    ]
   StructuralMismatch simVal setupVal setupValTy ty ->
-    PP.text "could not match specified value with actual value:" PP.<$$>
-    PP.vcat (map (PP.indent 2) $
-              [ PP.text "actual (simulator) value:" PP.<+> simVal
-              , PP.text "specified value:         " PP.<+> setupVal
-              , PP.text "type of actual value:   " PP.<+> PP.pretty ty
+    PP.vcat
+    [ PP.pretty "could not match specified value with actual value:"
+    , PP.vcat (map (PP.indent 2) $
+              [ PP.pretty "actual (simulator) value:" PP.<+> PP.unAnnotate simVal
+              , PP.pretty "specified value:         " PP.<+> PP.unAnnotate setupVal
+              , PP.pretty "type of actual value:   " PP.<+> PP.pretty ty
               ] ++ let msg ty_ =
-                         [PP.text "type of specified value:"
+                         [PP.pretty "type of specified value:"
                           PP.<+> PP.pretty ty_]
                    in maybe [] msg setupValTy)
+    ]
 
 --------------------------------------------------------------------------------
 -- ** OverrideFailure
@@ -223,10 +236,12 @@ data OverrideFailure ext = OF W4.ProgramLoc (OverrideFailureReason ext)
 
 ppOverrideFailure :: ( PP.Pretty (ExtType ext)
                      , PP.Pretty (MS.PointsTo ext)
-                     ) => OverrideFailure ext -> PP.Doc
+                     ) => OverrideFailure ext -> PP.Doc ann
 ppOverrideFailure (OF loc rsn) =
-  PP.text "at" PP.<+> PP.pretty (W4.plSourceLoc loc) PP.<$$>
-  ppOverrideFailureReason rsn
+  PP.vcat
+  [ PP.pretty "at" PP.<+> PP.viaShow (W4.plSourceLoc loc) -- TODO: fix when what4 switches to prettyprinter
+  , ppOverrideFailureReason rsn
+  ]
 
 instance ( PP.Pretty (ExtType ext)
          , PP.Pretty (MS.PointsTo ext)

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -28,7 +28,7 @@ Stability   : provisional
 module SAWScript.Crucible.JVM.MethodSpecIR where
 
 import           Control.Lens
-import qualified Text.PrettyPrint.ANSI.Leijen as PPL hiding ((<$>), (<>))
+import qualified Prettyprinter as PPL
 
 -- what4
 import           What4.ProgramLoc (ProgramLoc)
@@ -71,6 +71,10 @@ type instance MS.TypeName CJ.JVM = JIdent
 
 type instance MS.ExtType CJ.JVM = J.Type
 
+-- TODO: remove when jvm-parser switches to prettyprinter
+instance PPL.Pretty J.Type where
+  pretty = PPL.viaShow
+
 --------------------------------------------------------------------------------
 -- *** JVMMethodId
 
@@ -92,9 +96,10 @@ csMethodKey = MS.csMethod . jvmMethodKey
 csMethodName :: Getter (MS.CrucibleMethodSpecIR CJ.JVM) String
 csMethodName = MS.csMethod . jvmMethodName
 
+-- TODO: avoid intermediate 'String' values
 instance PPL.Pretty JVMMethodId where
   pretty (JVMMethodId methKey className) =
-    PPL.text (concat [J.unClassName className ,".", J.methodKeyName methKey])
+    PPL.pretty (concat [J.unClassName className ,".", J.methodKeyName methKey])
 
 type instance MS.MethodId CJ.JVM = JVMMethodId
 
@@ -126,20 +131,20 @@ data JVMPointsTo
   | JVMPointsToElem ProgramLoc (MS.SetupValue CJ.JVM) Int (MS.SetupValue CJ.JVM)
   | JVMPointsToArray ProgramLoc (MS.SetupValue CJ.JVM) TypedTerm
 
-ppPointsTo :: JVMPointsTo -> PPL.Doc
+ppPointsTo :: JVMPointsTo -> PPL.Doc ann
 ppPointsTo =
   \case
     JVMPointsToField _loc ptr fid val ->
-      MS.ppSetupValue ptr <> PPL.text "." <> PPL.text (J.fieldIdName fid)
-      PPL.<+> PPL.text "points to"
+      MS.ppSetupValue ptr <> PPL.pretty "." <> PPL.pretty (J.fieldIdName fid)
+      PPL.<+> PPL.pretty "points to"
       PPL.<+> MS.ppSetupValue val
     JVMPointsToElem _loc ptr idx val ->
-      MS.ppSetupValue ptr <> PPL.text "[" <> PPL.text (show idx) <> PPL.text "]"
-      PPL.<+> PPL.text "points to"
+      MS.ppSetupValue ptr <> PPL.pretty "[" <> PPL.pretty idx <> PPL.pretty "]"
+      PPL.<+> PPL.pretty "points to"
       PPL.<+> MS.ppSetupValue val
     JVMPointsToArray _loc ptr val ->
       MS.ppSetupValue ptr
-      PPL.<+> PPL.text "points to"
+      PPL.<+> PPL.pretty "points to"
       PPL.<+> MS.ppTypedTerm val
 
 instance PPL.Pretty JVMPointsTo where

src/SAWScript/Crucible/JVM/Override.hs

@@ -62,7 +62,7 @@ import qualified Data.Map as Map
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Void (absurd)
-import qualified Text.PrettyPrint.ANSI.Leijen as PPL
+import qualified Prettyprinter as PP
 
 -- cryptol
 import qualified Cryptol.TypeCheck.AST as Cryptol
@@ -123,10 +123,10 @@ type SetupCondition = MS.SetupCondition CJ.JVM
 type instance Pointer CJ.JVM = JVMRefVal
 
 -- TODO: Improve?
-ppJVMVal :: JVMVal -> PPL.Doc
-ppJVMVal = PPL.text . show
+ppJVMVal :: JVMVal -> PP.Doc ann
+ppJVMVal = PP.viaShow
 
-instance PPL.Pretty JVMVal where
+instance PP.Pretty JVMVal where
   pretty = ppJVMVal
 
 
@@ -206,8 +206,10 @@ methodSpecHandler opts sc cc top_loc css h = do
   branches <- case partitionEithers prestates of
                 (e, []) ->
                   fail $ show $
-                    PPL.text "All overrides failed during structural matching:" PPL.<$$>
-                    PPL.vcat (map (\x -> PPL.text "*" PPL.<> PPL.indent 2 (ppOverrideFailure x)) e)
+                  PP.vcat
+                  [ "All overrides failed during structural matching:"
+                  , PP.vcat (map (\x -> "*" <> PP.indent 2 (ppOverrideFailure x)) e)
+                  ]
                 (_, ss) -> liftIO $
                   forM ss $ \(cs,st) ->
                     do precond <- W4.andAllOf sym (folded.labeledPred) (st^.osAsserts)