Update saw-script and submodules to use prettyprinter package.

This commit includes the following submodule PRs:
- GaloisInc/what4#77
- GaloisInc/crucible#586
- GaloisInc/macaw#178
- GaloisInc/elf-edit#20

src/SAWScript/Crucible/Common.hs

@@ -27,30 +27,33 @@ import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
 import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
-import qualified Text.PrettyPrint.ANSI.Leijen as PP hiding ((<$>), (<>))
+import qualified Prettyprinter as PP
 
 -- | The symbolic backend we use for SAW verification
 type Sym = SAWCoreBackend Nonce.GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal)
 
-ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc)
+ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann)
                 -> AbortedResult Sym ext
-                -> PP.Doc
+                -> PP.Doc ann
 ppAbortedResult _ (AbortedExec InfeasibleBranch _) =
-  PP.text "Infeasible branch"
+  PP.pretty "Infeasible branch"
 ppAbortedResult ppGP (AbortedExec abt gp) = do
-  ppAbortExecReason abt PP.<$$> ppGP gp
+  PP.vcat
+    [ ppAbortExecReason abt
+    , ppGP gp
+    ]
 ppAbortedResult ppGP (AbortedBranch loc _predicate trueBranch falseBranch) =
   PP.vcat
-    [ PP.text "Both branches aborted after a symbolic branch."
-    , PP.text "Location of control-flow branching:"
-    , PP.indent 2 (PP.text (show (W4.plSourceLoc loc)))
-    , PP.text "Message from the true branch:"
+    [ PP.pretty "Both branches aborted after a symbolic branch."
+    , PP.pretty "Location of control-flow branching:"
+    , PP.indent 2 (PP.pretty (W4.plSourceLoc loc))
+    , PP.pretty "Message from the true branch:"
     , PP.indent 2 (ppAbortedResult ppGP trueBranch)
-    , PP.text "Message from the false branch:"
+    , PP.pretty "Message from the false branch:"
     , PP.indent 2 (ppAbortedResult ppGP falseBranch)
     ]
 ppAbortedResult _ (AbortedExit ec) =
-  PP.text "Branch exited:" PP.<+> PP.text (show ec)
+  PP.pretty "Branch exited:" PP.<+> PP.viaShow ec
 
 setupProfiling ::
   IsSymInterface sym =>

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -56,10 +56,9 @@ import qualified Data.Set as Set
 import qualified Data.Sequence as Seq
 import qualified Data.Vector as V
 import           Data.Void (absurd)
+import           Prettyprinter
 import           System.IO
 
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
-
 -- jvm-verifier
 -- TODO: transition to Lang.JVM.Codebase from crucible-jvm
 import qualified Verifier.Java.Codebase as CB
@@ -130,7 +129,7 @@ type SetupCondition = MS.SetupCondition CJ.JVM
 -- TODO: something useful with the global pair?
 ppAbortedResult :: JVMCrucibleContext
                 -> Crucible.AbortedResult Sym a
-                -> Doc
+                -> Doc ann
 ppAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
 
 -- FIXME: We need a better way to identify a set of class names to

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -102,11 +102,10 @@ import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import qualified Data.Text as Text
 import qualified Data.Vector as V
+import           Prettyprinter
 import           System.IO
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L (ppType, ppSymbol)
-import           Text.PrettyPrint.ANSI.Leijen hiding ((<$>), (<>))
-import qualified Text.PrettyPrint.ANSI.Leijen as PP
 import           Text.URI
 import qualified Control.Monad.Trans.Maybe as MaybeT
 
@@ -917,17 +916,17 @@ doAlloc cc i (LLVMAllocSpec mut _memTy alignment sz loc fresh)
 
 ppAbortedResult :: LLVMCrucibleContext arch
                 -> Crucible.AbortedResult Sym a
-                -> Doc
+                -> Doc ann
 ppAbortedResult cc = Common.ppAbortedResult (ppGlobalPair cc)
 
 ppGlobalPair :: LLVMCrucibleContext arch
              -> Crucible.GlobalPair Sym a
-             -> Doc
+             -> Doc ann
 ppGlobalPair cc gp =
   let mvar = Crucible.llvmMemVar (ccLLVMContext cc)
       globals = gp ^. Crucible.gpGlobals in
   case Crucible.lookupGlobal mvar globals of
-    Nothing -> text "LLVM Memory global variable not initialized"
+    Nothing -> "LLVM Memory global variable not initialized"
     Just mem -> Crucible.ppMem (Crucible.memImplHeap mem)
 
 
@@ -1263,7 +1262,7 @@ setupLLVMCrucibleContext bic opts pathSat lm action =
                  [ W4.opt
                      enableSMTArrayMemoryModel
                      (W4.ConcreteBool smt_array_memory_model_enabled)
-                     (PP.text "Enable SMT array memory model")
+                     ("Enable SMT array memory model" :: Text.Text)
                  ]
                  cfg
 

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -158,10 +158,6 @@ type instance MS.HasGhostState (CL.LLVM _) = 'True
 type instance MS.TypeName (CL.LLVM arch) = CL.Ident
 type instance MS.ExtType (CL.LLVM arch) = CL.MemType
 
--- TODO: remove when crucible switches to prettyprinter
-instance PPL.Pretty CL.MemType where
-  pretty = PPL.viaShow . CL.ppMemType
-
 --------------------------------------------------------------------------------
 -- *** LLVMMethodId
 

src/SAWScript/Crucible/LLVM/Override.hs

@@ -71,7 +71,6 @@ import           Data.Text (Text, pack)
 import qualified Data.Vector as V
 import           GHC.Generics (Generic)
 import           Numeric.Natural
-import qualified Text.PrettyPrint.ANSI.Leijen as PPWL
 import qualified Prettyprinter as PP
 
 import qualified Text.LLVM.AST as L
@@ -186,8 +185,7 @@ mkStructuralMismatch _opts cc _sc spec llvmval setupval memTy =
       nameEnv = MS.csTypeNames spec
       maybeTy = typeOfSetupValue cc tyEnv nameEnv setupval
   in pure $ StructuralMismatch
-              -- TODO: remove 'viaShow' when crucible switches to prettyprinter
-              (PP.viaShow (PPWL.pretty llvmval))
+              (PP.pretty llvmval)
               (MS.ppSetupValue setupval)
               maybeTy
               memTy
@@ -209,8 +207,7 @@ ppPointsToAsLLVMVal opts cc sc spec (LLVMPointsTo loc cond ptr val) = do
                  , "Pointee:" PP.<+> pretty2
                  , maybe PP.emptyDoc (\tt -> "Condition:" PP.<+> MS.ppTypedTerm tt) cond
                  , "Assertion made at:" PP.<+>
-                   -- TODO: replace 'viaShow' with 'pretty' when what4 switches to prettyprinter
-                   PP.viaShow (W4.plSourceLoc loc)
+                   PP.pretty (W4.plSourceLoc loc)
                  ]
 
 -- | Create an error stating that the 'LLVMVal' was not equal to the 'SetupValue'