From f1ae175d18f373fe0fe89b6f9399d86ec3db3e05 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 24 Nov 2020 18:21:25 -0800
Subject: [PATCH] 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
---
 deps/crucible                               |  2 +-
 deps/elf-edit                               |  2 +-
 deps/macaw                                  |  2 +-
 deps/what4                                  |  2 +-
 src/SAWScript/Crucible/Common.hs            | 25 ++++++++++++---------
 src/SAWScript/Crucible/JVM/Builtins.hs      |  5 ++---
 src/SAWScript/Crucible/LLVM/Builtins.hs     | 11 +++++----
 src/SAWScript/Crucible/LLVM/MethodSpecIR.hs |  4 ----
 src/SAWScript/Crucible/LLVM/Override.hs     |  7 ++----
 9 files changed, 27 insertions(+), 33 deletions(-)

diff --git a/deps/crucible b/deps/crucible
index d869268e12..c1da81f05e 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit d869268e125c771e3e3c2c71fcadc51c9d50f825
+Subproject commit c1da81f05e7a8ac80787e2f161ba341a312a6302
diff --git a/deps/elf-edit b/deps/elf-edit
index a24700f0bb..fe018fbf6c 160000
--- a/deps/elf-edit
+++ b/deps/elf-edit
@@ -1 +1 @@
-Subproject commit a24700f0bb5dd936e06c4c5240afb2b65801b231
+Subproject commit fe018fbf6c2df56fc3f565d2732780c064228f1b
diff --git a/deps/macaw b/deps/macaw
index 2a56e404bd..7761a6f6e1 160000
--- a/deps/macaw
+++ b/deps/macaw
@@ -1 +1 @@
-Subproject commit 2a56e404bdaad4f6488bcf5c820d7754db6d4264
+Subproject commit 7761a6f6e1348e6479b2ad272ad47e59fb5a8fd7
diff --git a/deps/what4 b/deps/what4
index 419ed1d899..3461006b51 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit 419ed1d89984b10cee8d80c5213098d653c6914c
+Subproject commit 3461006b5156904d82dedd32175849a6aa00059f
diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
index 6f4f6b7c5a..bd50dd4145 100644
--- a/src/SAWScript/Crucible/Common.hs
+++ b/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 =>
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index b132c8d7b0..1c246942cd 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/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
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index d919327a95..5c6bc42d88 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/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
 
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
index eb624e05fc..52abc4f27b 100644
--- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
+++ b/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
 
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index adb81b7495..007f197527 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/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'