Switch from ansi-wl-pprint to the prettyprinter package.

The following submodules have been updated to use prettyprinter:
- what4
- saw-core

The following packages have been converted:
- crucible
- crucible-jvm
- crucible-llvm
- crucible-saw
- crucible-server
- crucible-syntax
- crux
- crux-llvm
- crux-mir

crucible-jvm/crucible-jvm.cabal

@@ -19,7 +19,6 @@ executable crucible-jvm
  base >= 4 && < 5,
  bv-sized >= 1.0.0,
  aig,
- ansi-wl-pprint,
  array,
  containers,
  crucible,
@@ -53,7 +52,6 @@ library
  build-depends:
  base >= 4 && < 5,
  aig,
- ansi-wl-pprint,
  array,
  bv-sized >= 1.0.0,
  containers,

crucible-llvm/crucible-llvm.cabal

@@ -13,7 +13,6 @@ Synopsis: Support for translating and executing LLVM code in Crucible
 library
  build-depends:
  base >= 4.7 && < 4.15,
- ansi-wl-pprint,
  attoparsec,
  bv-sized >= 1.0.0,
  bytestring,
@@ -32,6 +31,7 @@ library
  llvm-pretty >= 0.8 && < 0.12,
  mtl,
  parameterized-utils >= 1.0.4 && < 2.2,
+ prettyprinter >= 1.7.0,
  text,
  template-haskell,
  transformers,

crucible-llvm/src/Lang/Crucible/LLVM/Errors.hs

@@ -46,7 +46,7 @@ import Data.Text (Text)
 
 import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter
 
 import What4.Interface
 import What4.Expr (GroundValue)
@@ -135,17 +135,17 @@ predicate = lens _predicate (\s v -> s { _predicate = v})
 extra :: Simple Lens (LLVMSafetyAssertion sym) (Maybe Text)
 extra = lens _extra (\s v -> s { _extra = v})
 
-explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc
+explainBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
 explainBB = \case
  BBUndefinedBehavior ub -> UB.explain ub
  BBMemoryError me -> ME.explain me
 
-detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc
+detailBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
 detailBB = \case
  BBUndefinedBehavior ub -> UB.ppDetails ub
  BBMemoryError me -> ME.details me
 
-ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc
+ppBB :: IsExpr (SymExpr sym) => BadBehavior sym -> Doc ann
 ppBB = \case
  BBUndefinedBehavior ub -> UB.ppDetails ub
  BBMemoryError me -> ME.ppMemoryError me

crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs

@@ -34,10 +34,9 @@ module Lang.Crucible.LLVM.Errors.MemoryError
 import Prelude hiding (pred)
 
 import Data.Text (Text)
-import qualified Data.Text as Text
 import qualified Text.LLVM.PP as L
 import qualified Text.LLVM.AST as L
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter
 
 import What4.Interface
 import What4.Expr (GroundValue)
@@ -78,95 +77,98 @@ data MemoryErrorReason sym w =
  | NoSatisfyingWrite StorageType (LLVMPtr sym w)
  | UnwritableRegion
  | UnreadableRegion
- | BadFunctionPointer Doc
+ | BadFunctionPointer (Doc ())
  | OverlappingRegions
 
 type MemErrContext sym w = MemoryOp sym w
 
-ppGSym :: Maybe String -> [Doc]
+ppGSym :: Maybe String -> [Doc ann]
 ppGSym Nothing = []
-ppGSym (Just nm) = [ text "Global symbol", text (show nm) ]
+ppGSym (Just nm) = [ "Global symbol", pretty (show nm) ]
 
-ppMemoryOp :: IsExpr (SymExpr sym) => MemoryOp sym w -> Doc
+ppMemoryOp :: IsExpr (SymExpr sym) => MemoryOp sym w -> Doc ann
 ppMemoryOp (MemLoadOp tp gsym ptr mem) =
  vsep [ "Performing overall load at type:" <+> ppType tp
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemStoreOp tp gsym ptr mem) =
  vsep [ "Performing store at type:" <+> ppType tp
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemStoreBytesOp gsym ptr Nothing mem) =
  vsep [ "Performing byte array store for entire address space"
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemStoreBytesOp gsym ptr (Just len) mem) =
  vsep [ "Performing byte array store of length:" <+> printSymExpr len
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) =
  vsep [ "Performing a memory copy of" <+> printSymExpr len <+> "bytes"
- , indent 2 (hsep ([ text "Destination:" ] ++ ppGSym gsym_dest ++ [ ppPtr dest ]))
- , indent 2 (hsep ([ text "Source: " ] ++ ppGSym gsym_src ++ [ ppPtr src ]))
- , text "In memory state:"
+ , indent 2 (hsep ([ "Destination:" ] ++ ppGSym gsym_dest ++ [ ppPtr dest ]))
+ , indent 2 (hsep ([ "Source: " ] ++ ppGSym gsym_src ++ [ ppPtr src ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemLoadHandleOp sig gsym ptr mem) =
- vsep [ "Attempting to load callable function with type:" <+> text (show (L.ppType sig))
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ vsep [ "Attempting to load callable function with type:" <+> pretty (show (L.ppType sig))
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
 ppMemoryOp (MemInvalidateOp msg gsym ptr len mem) =
  vsep [ "Performing explicit memory invalidation of" <+> printSymExpr len <+> "bytes"
- , text (Text.unpack msg)
- , indent 2 (hsep ([ text "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
- , text "In memory state:"
+ , pretty msg
+ , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ]))
+ , "In memory state:"
  , indent 2 (ppMem mem)
  ]
 
-explain :: IsExpr (SymExpr sym) => MemoryError sym -> Doc
+explain :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
 explain (MemoryError _mop rsn) = ppMemoryErrorReason rsn
 
-details :: IsExpr (SymExpr sym) => MemoryError sym -> Doc
+details :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
 details (MemoryError mop _rsn) = ppMemoryOp mop
 
-ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc
-ppMemoryError (MemoryError mop rsn) = ppMemoryErrorReason rsn <$$> ppMemoryOp mop
+ppMemoryError :: IsExpr (SymExpr sym) => MemoryError sym -> Doc ann
+ppMemoryError (MemoryError mop rsn) = vcat [ppMemoryErrorReason rsn, ppMemoryOp mop]
 
-ppMemoryErrorReason :: IsExpr (SymExpr sym) => MemoryErrorReason sym w -> Doc
+ppMemoryErrorReason :: IsExpr (SymExpr sym) => MemoryErrorReason sym w -> Doc ann
 ppMemoryErrorReason =
  \case
  TypeMismatch ty1 ty2 ->
- "Type mismatch: "
- <$$> indent 2 (vcat [ text (show ty1)
- , text (show ty2)
- ])
+ vcat
+ [ "Type mismatch: "
+ , indent 2 (vcat [ pretty (show ty1)
+ , pretty (show ty2)
+ ])
+ ]
  UnexpectedArgumentType txt vals ->
- vcat [ "Unexpected argument type:"
- , text (Text.unpack txt)
- ]
- <$$> indent 2 (vcat (map (text . show) vals))
+ vcat
+ [ "Unexpected argument type:"
+ , pretty txt
+ , indent 2 (vcat (map (pretty . show) vals))
+ ]
  ApplyViewFail vw ->
- "Failure when applying value view" <+> text (show vw)
+ "Failure when applying value view" <+> pretty (show vw)
  Invalid ty ->
- "Load from invalid memory at type " <+> text (show ty)
+ "Load from invalid memory at type " <+> pretty (show ty)
  Invalidated msg ->
- "Load from explicitly invalidated memory:" <+> text (Text.unpack msg)
+ "Load from explicitly invalidated memory:" <+> pretty msg
  NoSatisfyingWrite tp ptr ->
  vcat
  [ "No previous write to this location was found"
@@ -180,7 +182,7 @@ ppMemoryErrorReason =
  BadFunctionPointer msg ->
  vcat
  [ "The given pointer could not be resolved to a callable function"
- , msg
+ , unAnnotate msg
  ]
  OverlappingRegions ->
  "Memory regions required to be disjoint"

crucible-llvm/src/Lang/Crucible/LLVM/Errors/Poison.hs

@@ -41,10 +41,9 @@ module Lang.Crucible.LLVM.Errors.Poison
  ) where
 
 import Data.Kind (Type)
-import Data.Text (unpack)
 import Data.Maybe (isJust)
 import Data.Typeable (Typeable)
-import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import Prettyprinter
 
 import qualified Data.Parameterized.TraversableF as TF
 import Data.Parameterized.TraversableF (FunctorF(..), FoldableF(..), TraversableF(..))
@@ -154,8 +153,8 @@ standard =
  GEPOutOfBounds _ -> LLVMRef LLVM8
 
 -- | Which section(s) of the document state that this is poison?
-cite :: Poison e -> Doc
-cite = text .
+cite :: Poison e -> Doc ann
+cite =
  \case
  AddNoUnsignedWrap _ _ -> "‘add’ Instruction (Semantics)"
  AddNoSignedWrap _ _ -> "‘add’ Instruction (Semantics)"
@@ -176,7 +175,7 @@ cite = text .
  InsertElementIndex _ -> "‘insertelement’ Instruction (Semantics)"
  GEPOutOfBounds _ -> "‘getelementptr’ Instruction (Semantics)"
 
-explain :: Poison e -> Doc
+explain :: Poison e -> Doc ann
 explain =
  \case
  AddNoUnsignedWrap _ _ ->
@@ -226,8 +225,8 @@ explain =
  , "treats all GEP instructions as if they had the `inbounds` flag set."
  ]
 
-details :: forall sym.
- W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> [Doc]
+details :: forall sym ann.
+ W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> [Doc ann]
 details =
  \case
  AddNoUnsignedWrap v1 v2 -> args [v1, v2]
@@ -250,29 +249,29 @@ details =
  GEPOutOfBounds v -> args [v]
 
  where
- args :: forall w. [RegValue' sym (BVType w)] -> [Doc]
- args [] = [ text "No arguments" ]
- args [RV v] = [ text "Argument:" <+> W4I.printSymExpr v ]
- args vs = [ hsep (text "Arguments:" : map (W4I.printSymExpr . unRV) vs) ]
+ args :: forall w. [RegValue' sym (BVType w)] -> [Doc ann]
+ args [] = [ "No arguments" ]
+ args [RV v] = [ "Argument:" <+> W4I.printSymExpr v ]
+ args vs = [ hsep ("Arguments:" : map (W4I.printSymExpr . unRV) vs) ]
 
 
 -- | Pretty print an error message relating to LLVM poison values,
 -- when given a printer to produce a detailed message.
-pp :: (Poison e -> [Doc]) -> Poison e -> Doc
+pp :: (Poison e -> [Doc ann]) -> Poison e -> Doc ann
 pp extra poison = vcat $
  [ "Poison value encountered: "
  , explain poison
  , vcat (extra poison)
  , cat [ "Reference: "
- , text (unpack (ppStd (standard poison)))
+ , pretty (ppStd (standard poison))
  , cite poison
  ]
  ] ++ case stdURL (standard poison) of
- Just url -> ["Document URL:" <+> text (unpack url)]
+ Just url -> ["Document URL:" <+> pretty url]
  Nothing -> []
 
 -- | Pretty print an error message relating to LLVM poison values
-ppReg ::W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> Doc
+ppReg ::W4I.IsExpr (W4I.SymExpr sym) => Poison (RegValue' sym) -> Doc ann
 ppReg = pp details
 
 -- | Concretize a poison error message.