Merge pull request #178 from GaloisInc/prettyprinter

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

base/macaw-base.cabal

@@ -29,7 +29,6 @@ description:
 library
   build-depends:
     base >= 4,
-    ansi-wl-pprint,
     binary,
     binary-symbols >= 0.1.3,
     bytestring,
@@ -40,6 +39,7 @@ library
     lens >= 4.7,
     mtl,
     parameterized-utils >= 2.1.0 && < 2.2,
+    prettyprinter >= 1.7.0,
     template-haskell,
     text,
     vector,

base/src/Data/Macaw/AbsDomain/AbsState.hs

@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -78,7 +79,7 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 import           GHC.Stack
 import           Numeric (showHex)
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 
 import           Data.Macaw.AbsDomain.CallParams
 import qualified Data.Macaw.AbsDomain.StridedInterval as SI
@@ -256,31 +257,31 @@ instance EqF (AbsValue w) where
 instance MemWidth w => Show (AbsValue w tp) where
   show = show . pretty
 
-ppSet :: [Doc] -> Doc
+ppSet :: [Doc ann] -> Doc ann
 ppSet = encloseSep lbrace rbrace comma
 
 instance MemWidth w => Pretty (AbsValue w tp) where
-  pretty (BoolConst b) = text (show b)
-  pretty (FinSet s) = text "finset" <+> ppIntegerSet s
-  pretty (CodePointers s b) = text "code" <+> ppSet (s0 ++ sd)
-    where s0 = if b then [text "0"] else []
+  pretty (BoolConst b) = viaShow b
+  pretty (FinSet s) = "finset" <+> ppIntegerSet s
+  pretty (CodePointers s b) = "code" <+> ppSet (s0 ++ sd)
+    where s0 = if b then ["0"] else []
           sd = f <$> Set.toList s
-          f segAddr = text (show segAddr)
+          f segAddr = viaShow segAddr
 
   pretty (StridedInterval s) =
-    text "strided" <> parens (pretty s)
+    "strided" <> parens (pretty s)
   pretty (SubValue n av) =
-    text "sub" <> parens (integer (intValue n) <> comma <+> pretty av)
+    "sub" <> parens (pretty (intValue n) <> comma <+> pretty av)
   pretty (StackOffsetAbsVal a v')
-    | v' >= 0   = text $ "rsp_" ++ show a ++ " + " ++ showHex v' ""
-    | otherwise = text $ "rsp_" ++ show a ++ " - " ++ showHex (negate (toInteger v')) ""
-  pretty (SomeStackOffset a) = text $ "rsp_" ++ show a ++ " + ?"
-  pretty TopV = text "top"
-  pretty ReturnAddr = text "return_addr"
+    | v' >= 0   = pretty $ "rsp_" ++ show a ++ " + " ++ showHex v' ""
+    | otherwise = pretty $ "rsp_" ++ show a ++ " - " ++ showHex (negate (toInteger v')) ""
+  pretty (SomeStackOffset a) = pretty $ "rsp_" ++ show a ++ " + ?"
+  pretty TopV = "top"
+  pretty ReturnAddr = "return_addr"
 
-ppIntegerSet :: (Integral w, Show w) => Set w -> Doc
+ppIntegerSet :: (Integral w, Show w) => Set w -> Doc ann
 ppIntegerSet s = ppSet (ppv <$> Set.toList s)
-  where ppv v' | v' >= 0 = text (showHex v' "")
+  where ppv v' | v' >= 0 = pretty (showHex v' "")
                | otherwise = error "ppIntegerSet given negative value"
 
 -- | Returns a set of concrete integers that this value may be.
@@ -366,7 +367,7 @@ joinAbsValue x y
     | Set.null s = r
     | otherwise = debug DAbsInt ("dropping " ++ show dropped ++ "\n" ++ show x ++ "\n" ++ show y ++ "\n") r
   where (r,s) = runState (joinAbsValue' x y) Set.empty
-        dropped = ppSet (text . show <$> Set.toList s)
+        dropped = ppSet (viaShow <$> Set.toList s)
 
 addWords :: Set (MemSegmentOff w) -> State (Set (MemSegmentOff w)) ()
 addWords s = modify $ Set.union s
@@ -855,14 +856,14 @@ bitop doOp _w (asConcreteSingleton -> Just v) (asFinSet "bitop" -> IsFin s)
   = FinSet (Set.map (doOp v) s)
 bitop _ _ _ _ = TopV
 
-ppAbsValue :: MemWidth w => AbsValue w tp -> Maybe Doc
+ppAbsValue :: MemWidth w => AbsValue w tp -> Maybe (Doc ann)
 ppAbsValue TopV = Nothing
 ppAbsValue v = Just (pretty v)
 
 -- | Print a list of Docs vertically separated.
 instance (MemWidth w, ShowF r) => PrettyRegValue r (AbsValue w) where
   ppValueEq _ TopV = Nothing
-  ppValueEq r v = Just (text (showF r) <+> text "=" <+> pretty v)
+  ppValueEq r v = Just (pretty (showF r) <+> "=" <+> pretty v)
 
 
 absTrue :: AbsValue w BoolType
@@ -1030,9 +1031,9 @@ showSignedHex :: Integer -> ShowS
 showSignedHex x | x < 0 = showString "-0x" . showHex (negate x)
                 | otherwise = showString "0x" . showHex x
 
-ppAbsStack :: MemWidth w => AbsBlockStack w -> Doc
+ppAbsStack :: MemWidth w => AbsBlockStack w -> Doc ann
 ppAbsStack m = vcat (pp <$> Map.toDescList m)
-  where pp (o,StackEntry _ v) = text (showSignedHex (toInteger o) " :=") <+> pretty v
+  where pp (o,StackEntry _ v) = pretty (showSignedHex (toInteger o) " :=") <+> pretty v
 
 ------------------------------------------------------------------------
 -- AbsBlockState
@@ -1108,13 +1109,18 @@ instance ( ShowF r
          , MemWidth (RegAddrWidth r)
          ) => Pretty (AbsBlockState r) where
   pretty s =
-      text "registers:" <$$>
-      indent 2 (pretty (s^.absRegState)) <$$>
-      stack_d
+    vcat
+    [ "registers:"
+    , indent 2 (pretty (s^.absRegState))
+    , stack_d
+    ]
     where stack = startAbsStack s
-          stack_d | Map.null stack = empty
-                  | otherwise = text "stack:" <$$>
-                                indent 2 (ppAbsStack stack)
+          stack_d | Map.null stack = emptyDoc
+                  | otherwise =
+                      vcat
+                      [ "stack:"
+                      , indent 2 (ppAbsStack stack)
+                      ]
 
 instance (ShowF r, MemWidth (RegAddrWidth r)) => Show (AbsBlockState r) where
   show = show . pretty
@@ -1171,13 +1177,18 @@ curAbsStack = lens _curAbsStack (\s v -> s { _curAbsStack = v })
 instance (ShowF r, MemWidth (RegAddrWidth r))
       => Pretty (AbsProcessorState r ids) where
   pretty s =
-      text "registers:" <$$>
-      indent 2 (pretty (s^.absInitialRegs)) <$$>
-      stack_d
+    vcat
+    [ "registers:"
+    , indent 2 (pretty (s^.absInitialRegs))
+    , stack_d
+    ]
     where stack = s^.curAbsStack
-          stack_d | Map.null stack = empty
-                  | otherwise = text "stack:" <$$>
-                                indent 2 (ppAbsStack stack)
+          stack_d | Map.null stack = emptyDoc
+                  | otherwise =
+                    vcat
+                    [ "stack:"
+                    , indent 2 (ppAbsStack stack)
+                    ]
 
 instance (ShowF r, MemWidth (RegAddrWidth r))
       => Show (AbsProcessorState r ids) where

base/src/Data/Macaw/AbsDomain/JumpBounds.hs

@@ -11,6 +11,7 @@ known equivalent values.
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -45,7 +46,7 @@ import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Pair
 import           Numeric.Natural
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 
 import           Data.Macaw.AbsDomain.CallParams
 import           Data.Macaw.AbsDomain.StackAnalysis
@@ -119,7 +120,7 @@ data InitJumpBounds arch
                     }
 
 -- | Pretty print jump bounds.
-ppInitJumpBounds :: forall arch . ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc]
+ppInitJumpBounds :: forall arch ann . ShowF (ArchReg arch) => InitJumpBounds arch -> [Doc ann]
 ppInitJumpBounds cns
   =  ppBlockStartStackConstraints (initBndsMap cns)
   <> ppLocMap ppSubRange (initRngPredMap cns)
@@ -420,8 +421,8 @@ data SubRange tp where
 instance Pretty (SubRange tp) where
   pretty (SubRange p) = pretty p
 
-ppSubRange :: Doc -> SubRange tp -> Doc
-ppSubRange d (SubRange r) = d <+> text "in" <+> pretty r
+ppSubRange :: Doc ann -> SubRange tp -> Doc ann
+ppSubRange d (SubRange r) = d <+> "in" <+> pretty r
 
 -- | Take the union of two subranges, and return `Nothing` if this is
 -- a maximum range bound.
@@ -467,10 +468,10 @@ instance ShowF (ArchReg arch) => Pretty (BranchConstraints arch ids) where
   pretty x =
     let cl = MapF.toList (newClassRepConstraints x)
         al = MapF.toList (newUninterpAssignConstraints x)
-        ppLoc :: Pair (BoundLoc (ArchReg arch)) SubRange -> Doc
-        ppLoc (Pair l r) = prettyF l <+> text ":=" <+> pretty r
-        ppAssign :: Pair (AssignId ids) SubRange -> Doc
-        ppAssign (Pair l r) = ppAssignId l <+> text ":=" <+> pretty r
+        ppLoc :: Pair (BoundLoc (ArchReg arch)) SubRange -> Doc ann
+        ppLoc (Pair l r) = prettyF l <+> ":=" <+> pretty r
+        ppAssign :: Pair (AssignId ids) SubRange -> Doc ann
+        ppAssign (Pair l r) = ppAssignId l <+> ":=" <+> pretty r
      in vcat (fmap ppLoc cl ++ fmap ppAssign al)
 
 instance ShowF (ArchReg arch) => Show (BranchConstraints arch ids) where

base/src/Data/Macaw/AbsDomain/StackAnalysis.hs

@@ -39,6 +39,7 @@ proof rules:
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -118,7 +119,7 @@ import           Data.Parameterized.TraversableFC
 import           Data.Proxy
 import           Data.STRef
 import           GHC.Natural
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
+import           Prettyprinter
 import           Text.Printf
 
 import           Data.Macaw.AbsDomain.CallParams
@@ -132,14 +133,14 @@ import           Data.Macaw.Utils.Changed
 addrTypeRepr :: MemWidth w => TypeRepr (BVType w)
 addrTypeRepr = BVTypeRepr memWidthNatRepr
 
-ppAddend :: MemInt w -> Doc
+ppAddend :: MemInt w -> Doc ann
 ppAddend o | memIntValue o < 0 =
-               text "-" <+> pretty (negate (toInteger (memIntValue o)))
-           | otherwise = text "+" <+> pretty o
+               "-" <+> pretty (negate (toInteger (memIntValue o)))
+           | otherwise = "+" <+> pretty o
 
-ppStackOff :: MemInt w -> MemRepr tp -> Doc
+ppStackOff :: MemInt w -> MemRepr tp -> Doc ann
 ppStackOff o repr =
-  text "*(stack_frame" <+> ppAddend o <> text ", " <> pretty repr <> text ")"
+  "*(stack_frame" <+> ppAddend o <> ", " <> pretty repr <> ")"
 
 ------------------------------------------------------------------------
 -- JoinClassPair
@@ -211,7 +212,7 @@ instance OrdF r => OrdF (BoundLoc r) where
       EQ -> compareF xr yr
 
 instance ShowF r => Pretty (BoundLoc r tp) where
-  pretty (RegLoc r) = text (showF r)
+  pretty (RegLoc r) = pretty (showF r)
   pretty (StackOffLoc i tp) = ppStackOff i tp
 
 instance ShowF r => PrettyF (BoundLoc r) where
@@ -434,7 +435,7 @@ locMapTraverseWithKey_ f m0 = do
    *> memMapTraverseWithKey_ stackFn (locMapStack m0)
 
 -- | Pretty print a location map.
-ppLocMap :: ShowF r => (forall tp . Doc -> p tp -> Doc) -> LocMap r p -> [Doc]
+ppLocMap :: ShowF r => (forall tp . Doc ann -> p tp -> Doc ann) -> LocMap r p -> [Doc ann]
 ppLocMap f m =
   let ppPair (Pair l v) = f (pretty l) v
    in ppPair <$> locMapToList m
@@ -500,11 +501,11 @@ data StackEqConstraint r tp where
          -> StackEqConstraint r (BVType w)
 
 
-ppStackEqConstraint :: ShowF r => Doc -> StackEqConstraint r tp -> Doc
+ppStackEqConstraint :: ShowF r => Doc ann -> StackEqConstraint r tp -> Doc ann
 ppStackEqConstraint d (IsStackOff i) =
-  d <+> text "= stack_frame" <+> ppAddend i
-ppStackEqConstraint d (EqualLoc   l) = d <> text " = " <> pretty l
-ppStackEqConstraint d (IsUExt l w) = d <> text " = (uext " <> pretty l <+> text (show w) <> text ")"
+  d <+> "= stack_frame" <+> ppAddend i
+ppStackEqConstraint d (EqualLoc   l) = d <> " = " <> pretty l
+ppStackEqConstraint d (IsUExt l w) = d <> " = (uext " <> pretty l <+> viaShow w <> ")"
 
 ------------------------------------------------------------------------
 -- BlockStartStackConstraints
@@ -521,7 +522,7 @@ newtype BlockStartStackConstraints arch =
 -- | Pretty print the lines in stack constraints.
 ppBlockStartStackConstraints :: ShowF (ArchReg arch)
                              => BlockStartStackConstraints arch
-                             -> [Doc]
+                             -> [Doc ann]
 ppBlockStartStackConstraints = ppLocMap ppStackEqConstraint . unBSSC
 
 fnEntryBlockStartStackConstraints :: RegisterInfo (ArchReg arch)
@@ -875,13 +876,13 @@ instance ShowF (ArchReg arch) => Pretty (StackExpr arch id tp) where
   pretty e =
     case e of
       ClassRepExpr l -> pretty l
-      UninterpAssignExpr n _ -> parens (text "uninterp" <+> ppAssignId n)
+      UninterpAssignExpr n _ -> parens ("uninterp" <+> ppAssignId n)
       StackOffsetExpr o
-        | memIntValue o > 0 -> parens (text "+ stack_off" <+> pretty o)
-        | memIntValue o < 0 -> parens (text "- stack_off" <+> pretty (negate (toInteger (memIntValue o))))
-        | otherwise -> text "stack_off"
+        | memIntValue o > 0 -> parens ("+ stack_off" <+> pretty o)
+        | memIntValue o < 0 -> parens ("- stack_off" <+> pretty (negate (toInteger (memIntValue o))))
+        | otherwise -> "stack_off"
       CExpr v -> pretty v
-      UExtExpr l w -> parens (text "uext " <> pretty l <+> text (show w))
+      UExtExpr l w -> parens ("uext " <> pretty l <+> viaShow w)
       AppExpr n _ -> ppAssignId n
 
 instance ShowF (ArchReg arch) => PrettyF (StackExpr arch id) where
@@ -918,21 +919,21 @@ data BlockIntraStackConstraints arch ids
 
 instance ShowF (ArchReg arch) => Pretty (BlockIntraStackConstraints arch ids) where
   pretty cns =
-    let ppStk :: MemInt (ArchAddrWidth arch) -> MemRepr tp -> StackExpr arch ids tp -> Doc
-        ppStk o r v = text (show o) <> text ", " <> pretty r <> text " := " <> pretty v
-        sm :: Doc
-        sm = memMapFoldrWithKey (\o r v d -> ppStk o r v <$$> d) empty (stackExprMap cns)
-        ppAssign :: AssignId ids tp -> StackExpr arch ids tp -> Doc -> Doc
+    let ppStk :: MemInt (ArchAddrWidth arch) -> MemRepr tp -> StackExpr arch ids tp -> Doc ann
+        ppStk o r v = viaShow o <> ", " <> pretty r <> " := " <> pretty v
+        sm :: Doc ann
+        sm = memMapFoldrWithKey (\o r v d -> vcat [ppStk o r v, d]) emptyDoc (stackExprMap cns)
+        ppAssign :: AssignId ids tp -> StackExpr arch ids tp -> Doc ann -> Doc ann
         ppAssign a (AppExpr u app) d =
           case testEquality a u of
-            Nothing -> ppAssignId a <> text " := " <> ppAssignId u <$$> d
-            Just Refl -> ppAssignId a <> text " := " <> ppApp pretty app <$$> d
-        ppAssign a e d = ppAssignId a <> text " := " <> pretty e <$$> d
-        am :: Doc
-        am = MapF.foldrWithKey ppAssign empty (assignExprMap cns)
-     in vcat [ text "stackExprMap:"
+            Nothing -> vcat [ppAssignId a <> " := " <> ppAssignId u, d]
+            Just Refl -> vcat [ppAssignId a <> " := " <> ppApp pretty app, d]
+        ppAssign a e d = vcat [ppAssignId a <> " := " <> pretty e, d]
+        am :: Doc ann
+        am = MapF.foldrWithKey ppAssign emptyDoc (assignExprMap cns)
+     in vcat [ "stackExprMap:"
              , indent 2 sm
-             , text "assignExprMap:"
+             , "assignExprMap:"
              , indent 2 am
              ]
 

base/src/Data/Macaw/AbsDomain/StridedInterval.hs

@@ -6,6 +6,7 @@ A strided interval domain x + [a .. b] * c
 -}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternGuards #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
@@ -33,8 +34,8 @@ import           Control.Exception (assert)
 import qualified Data.Foldable as Fold
 import           Data.Parameterized.NatRepr
 import           GHC.TypeLits (Nat)
+import           Prettyprinter
 import           Test.QuickCheck
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), empty)
 
 -- import           Data.Macaw.DebugLogging
 
@@ -488,12 +489,12 @@ toList :: StridedInterval w -> [Integer]
 toList si@StridedInterval{} = map (\v -> base si + stride si * v) [0 .. range si]
 
 instance Pretty (StridedInterval w) where
-  pretty si | isEmpty si = text "[]"
-  pretty si | Just s <- isSingleton si = brackets (integer s)
-  pretty si@StridedInterval{} = brackets (integer (base si) <> comma
-                                          <+> integer (base si + stride si)
-                                          <+> text ".."
-                                          <+> integer (base si + range si * stride si))
+  pretty si | isEmpty si = "[]"
+  pretty si | Just s <- isSingleton si = brackets (pretty s)
+  pretty si@StridedInterval{} = brackets (pretty (base si) <> comma
+                                          <+> pretty (base si + stride si)
+                                          <+> ".."
+                                          <+> pretty (base si + range si * stride si))
 
 instance Arbitrary (StridedInterval 64) where
   arbitrary = frequency [ (1, return (empty knownNat))