From f1ae175d18f373fe0fe89b6f9399d86ec3db3e05 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 24 Nov 2020 18:21:25 -0800 Subject: [PATCH 1/4] 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' From 6ecfdccdd47304f34ed2e66b3c3df39be2e9c245 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 3 Dec 2020 15:11:26 -0800 Subject: [PATCH 2/4] Convert the rest of saw-script from `ansi-wl-pprint` to `prettyprinter`. --- cabal.GHC-8.6.5.config | 2 - cabal.GHC-8.8.3.config | 2 - cabal.GHC-8.8.4.config | 2 - saw-script.cabal | 1 - src/SAWScript/AST.hs | 170 ++++++++++++++++++----------------- src/SAWScript/AutoMatch.hs | 2 +- src/SAWScript/Interpreter.hs | 2 +- src/SAWScript/JavaPretty.hs | 70 ++++++++------- 8 files changed, 127 insertions(+), 124 deletions(-) diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config index 09a0bbd5ac..5e839b7cb9 100644 --- a/cabal.GHC-8.6.5.config +++ b/cabal.GHC-8.6.5.config @@ -22,8 +22,6 @@ constraints: any.Cabal ==2.4.0.1, alex +small_base, any.ansi-terminal ==0.10.3, ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, any.array ==0.5.3.0, any.assoc ==1.0.1, any.async ==2.2.2, diff --git a/cabal.GHC-8.8.3.config b/cabal.GHC-8.8.3.config index ad36345755..823b869b81 100644 --- a/cabal.GHC-8.8.3.config +++ b/cabal.GHC-8.8.3.config @@ -22,8 +22,6 @@ constraints: any.Cabal ==3.0.1.0, alex +small_base, any.ansi-terminal ==0.10.3, ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, any.array ==0.5.4.0, any.assoc ==1.0.1, any.async ==2.2.2, diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index cf5afdb1e0..49b2c70951 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -22,8 +22,6 @@ constraints: any.Cabal ==3.0.1.0, alex +small_base, any.ansi-terminal ==0.10.3, ansi-terminal -example, - any.ansi-wl-pprint ==0.6.9, - ansi-wl-pprint -example, any.array ==0.5.4.0, any.assoc ==1.0.1, any.async ==2.2.2, diff --git a/saw-script.cabal b/saw-script.cabal index 04fe8e8fc1..f1107455e3 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -28,7 +28,6 @@ library build-depends: base >= 4 , aig - , ansi-wl-pprint , array , binary , bimap diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index b32f78c447..a6e462c8ac 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -7,6 +7,7 @@ Stability : provisional -} {-# LANGUAGE CPP #-} {-# LANGUAGE DeriveFunctor,DeriveFoldable,DeriveTraversable #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE LambdaCase #-} @@ -47,11 +48,11 @@ import Data.List (intercalate) import Data.Foldable (Foldable) import Data.Traversable (Traversable) #endif -import qualified Text.PrettyPrint.ANSI.Leijen as PP -import Text.PrettyPrint.ANSI.Leijen (Pretty) +import qualified Prettyprinter as PP +import Prettyprinter (Pretty) import qualified Cryptol.Parser.AST as P (ImportSpec(..), ModName) -import qualified Cryptol.Utils.Ident as P (unpackIdent, modNameChunks) +import qualified Cryptol.Utils.Ident as P (identText, modNameChunks) -- Names {{{ @@ -218,53 +219,56 @@ data Schema = Forall [Name] Type -- Pretty Printing {{{ -prettyWholeModule :: [Stmt] -> PP.Doc -prettyWholeModule = (PP.<> PP.linebreak) . vcatWithSemi . map PP.pretty +prettyWholeModule :: [Stmt] -> PP.Doc ann +prettyWholeModule = (PP.<> PP.line') . vcatWithSemi . map PP.pretty -vcatWithSemi :: [PP.Doc] -> PP.Doc +vcatWithSemi :: [PP.Doc ann] -> PP.Doc ann vcatWithSemi = PP.vcat . map (PP.<> PP.semi) instance Pretty Expr where pretty expr0 = case expr0 of - Bool b -> PP.text $ show b - String s -> PP.dquotes (PP.text s) - Int i -> PP.integer i - Code ls -> PP.braces . PP.braces $ PP.text (getVal ls) - CType (Located string _ _) -> PP.braces . PP.text $ "|" ++ string ++ "|" + Bool b -> PP.viaShow b + String s -> PP.dquotes (PP.pretty s) + Int i -> PP.pretty i + Code ls -> PP.braces . PP.braces $ PP.pretty (getVal ls) + CType (Located string _ _) -> PP.braces . PP.pretty $ "|" ++ string ++ "|" Array xs -> PP.list (map PP.pretty xs) Block stmts -> - PP.text "do" PP.<+> PP.lbrace PP.<> PP.linebreak PP.<> + "do" PP.<+> PP.lbrace PP.<> PP.line' PP.<> (PP.indent 3 $ (PP.align . vcatWithSemi . map PP.pretty $ stmts)) PP.<> - PP.linebreak PP.<> PP.rbrace + PP.line' PP.<> PP.rbrace Tuple exprs -> PP.tupled (map PP.pretty exprs) Record mapping -> PP.braces . (PP.space PP.<>) . (PP.<> PP.space) . PP.align . PP.sep . PP.punctuate PP.comma $ - map (\(name, value) -> PP.text name PP.<+> PP.text "=" PP.<+> PP.pretty value) + map (\(name, value) -> PP.pretty name PP.<+> "=" PP.<+> PP.pretty value) (Map.assocs mapping) Index _ _ -> error "No concrete syntax for AST node 'Index'" - Lookup expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.text name - TLookup expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.integer int + Lookup expr name -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty name + TLookup expr int -> PP.pretty expr PP.<> PP.dot PP.<> PP.pretty int Var (Located name _ _) -> - PP.text name + PP.pretty name Function pat expr -> - PP.text "\\" PP.<+> PP.pretty pat PP.<+> PP.text "-> " PP.<+> PP.pretty expr + "\\" PP.<+> PP.pretty pat PP.<+> "-> " PP.<+> PP.pretty expr -- FIXME, use precedence to minimize parentheses Application f a -> PP.parens (PP.pretty f PP.<+> PP.pretty a) Let (NonRecursive decl) expr -> - PP.text "let" PP.<+> - prettyDef decl PP. - PP.text "in" PP.<+> PP.pretty expr + PP.fillSep + [ "let" PP.<+> prettyDef decl + , "in" PP.<+> PP.pretty expr + ] Let (Recursive decls) expr -> - PP.text "let" PP.<+> - PP.cat (PP.punctuate - (PP.empty PP. PP.text "and" PP.<> PP.space) - (map prettyDef decls)) PP. - PP.text "in" PP.<+> PP.pretty expr + PP.fillSep + [ "let" PP.<+> + PP.cat (PP.punctuate + (PP.fillSep [PP.emptyDoc, "and" PP.<> PP.space]) + (map prettyDef decls)) + , "in" PP.<+> PP.pretty expr + ] TSig expr typ -> PP.parens $ PP.pretty expr PP.<+> PP.colon PP.<+> pretty 0 typ IfThenElse e1 e2 e3 -> - PP.text "if" PP.<+> PP.pretty e1 PP.<+> - PP.text "then" PP.<+> PP.pretty e2 PP.<+> - PP.text "else" PP.<+> PP.pretty e3 + "if" PP.<+> PP.pretty e1 PP.<+> + "then" PP.<+> PP.pretty e2 PP.<+> + "else" PP.<+> PP.pretty e3 LExpr _ e -> PP.pretty e instance PrettyPrint Expr where @@ -285,57 +289,57 @@ instance Pretty Stmt where StmtBind _ (PWild _leftType) _rightType expr -> PP.pretty expr StmtBind _ pat _rightType expr -> - PP.pretty pat PP.<+> PP.text "<-" PP.<+> PP.align (PP.pretty expr) + PP.pretty pat PP.<+> "<-" PP.<+> PP.align (PP.pretty expr) StmtLet _ (NonRecursive decl) -> - PP.text "let" PP.<+> prettyDef decl + "let" PP.<+> prettyDef decl StmtLet _ (Recursive decls) -> - PP.text "rec" PP.<+> + "rec" PP.<+> PP.cat (PP.punctuate - (PP.empty PP. PP.text "and" PP.<> PP.space) + (PP.fillSep [PP.emptyDoc, "and" PP.<> PP.space]) (map prettyDef decls)) StmtCode _ (Located code _ _) -> - PP.text "let" PP.<+> - (PP.braces . PP.braces $ PP.text code) + "let" PP.<+> + (PP.braces . PP.braces $ PP.pretty code) StmtImport _ Import{iModule,iAs,iSpec} -> - PP.text "import" PP.<+> + "import" PP.<+> (case iModule of Left filepath -> - PP.dquotes . PP.text $ filepath + PP.dquotes . PP.pretty $ filepath Right modName -> ppModName modName) PP.<> (case iAs of Just modName -> - PP.space PP.<> PP.text "as" PP.<+> ppModName modName - Nothing -> PP.empty) PP.<> + PP.space PP.<> "as" PP.<+> ppModName modName + Nothing -> PP.emptyDoc) PP.<> (case iSpec of Just (P.Hiding names) -> - PP.space PP.<> PP.text "hiding" PP.<+> PP.tupled (map ppIdent names) + PP.space PP.<> "hiding" PP.<+> PP.tupled (map ppIdent names) Just (P.Only names) -> PP.space PP.<> PP.tupled (map ppIdent names) - Nothing -> PP.empty) + Nothing -> PP.emptyDoc) StmtTypedef _ (Located name _ _) ty -> - PP.text "typedef" PP.<+> PP.text name PP.<+> pretty 0 ty - --expr -> PP.cyan . PP.text $ show expr + "typedef" PP.<+> PP.pretty name PP.<+> pretty 0 ty + --expr -> PP.cyan . PP.viaShow expr where - ppModName mn = PP.text (intercalate "." (P.modNameChunks mn)) - ppIdent i = PP.text (P.unpackIdent i) + ppModName mn = PP.pretty (intercalate "." (P.modNameChunks mn)) + ppIdent i = PP.pretty (P.identText i) --ppName n = ppIdent (P.nameIdent n) -prettyDef :: Decl -> PP.Doc +prettyDef :: Decl -> PP.Doc ann prettyDef (Decl _ pat _ def) = PP.pretty pat PP.<+> let (args, body) = dissectLambda def in (if not (null args) then PP.hsep (map PP.pretty args) PP.<> PP.space - else PP.empty) PP.<> - PP.text "=" PP.<+> PP.pretty body + else PP.emptyDoc) PP.<> + "=" PP.<+> PP.pretty body -prettyMaybeTypedArg :: (Name,Maybe Type) -> PP.Doc +prettyMaybeTypedArg :: (Name, Maybe Type) -> PP.Doc ann prettyMaybeTypedArg (name,Nothing) = - PP.text name + PP.pretty name prettyMaybeTypedArg (name,Just typ) = - PP.parens $ PP.text name PP.<+> PP.colon PP.<+> pretty 0 typ + PP.parens $ PP.pretty name PP.<+> PP.colon PP.<+> pretty 0 typ dissectLambda :: Expr -> ([Pattern], Expr) dissectLambda = \case @@ -346,12 +350,12 @@ pShow :: PrettyPrint a => a -> String pShow = show . pretty 0 class PrettyPrint p where - pretty :: Int -> p -> PP.Doc + pretty :: Int -> p -> PP.Doc ann instance PrettyPrint Schema where pretty _ (Forall ns t) = case ns of [] -> pretty 0 t - _ -> PP.braces (commaSepAll $ map PP.text ns) PP.<+> pretty 0 t + _ -> PP.braces (commaSepAll $ map PP.pretty ns) PP.<+> pretty 0 t instance PrettyPrint Type where pretty par t@(TyCon tc ts) = case (tc,ts) of @@ -359,58 +363,58 @@ instance PrettyPrint Type where (TupleCon _,_) -> PP.parens $ commaSepAll $ map (pretty 0) ts (ArrayCon,[typ]) -> PP.brackets (pretty 0 typ) (FunCon,[f,v]) -> (if par > 0 then PP.parens else id) $ - pretty 1 f PP.<+> PP.text "->" PP.<+> pretty 0 v + pretty 1 f PP.<+> "->" PP.<+> pretty 0 v (BlockCon,[cxt,typ]) -> (if par > 1 then PP.parens else id) $ pretty 1 cxt PP.<+> pretty 2 typ _ -> error $ "malformed TyCon: " ++ show t pretty _par (TyRecord fs) = PP.braces $ commaSepAll - $ map (\(n,t) -> PP.text n `prettyTypeSig` pretty 0 t) + $ map (\(n,t) -> PP.pretty n `prettyTypeSig` pretty 0 t) $ Map.toList fs - pretty _par (TyUnifyVar i) = PP.text "t." PP.<> PP.integer i - pretty _par (TySkolemVar n i) = PP.text n PP.<> PP.integer i - pretty _par (TyVar n) = PP.text n + pretty _par (TyUnifyVar i) = "t." PP.<> PP.pretty i + pretty _par (TySkolemVar n i) = PP.pretty n PP.<> PP.pretty i + pretty _par (TyVar n) = PP.pretty n pretty par (LType _ t) = pretty par t instance PrettyPrint TyCon where pretty par tc = case tc of - TupleCon n -> PP.parens $ replicateDoc (n - 1) $ PP.char ',' - ArrayCon -> PP.parens $ PP.brackets $ PP.empty - FunCon -> PP.parens $ PP.text "->" - StringCon -> PP.text "String" - TermCon -> PP.text "Term" - TypeCon -> PP.text "Type" - BoolCon -> PP.text "Bool" - IntCon -> PP.text "Int" - AIGCon -> PP.text "AIG" - CFGCon -> PP.text "CFG" - BlockCon -> PP.text "" + TupleCon n -> PP.parens $ replicateDoc (n - 1) $ PP.pretty ',' + ArrayCon -> PP.parens $ PP.brackets $ PP.emptyDoc + FunCon -> PP.parens $ "->" + StringCon -> "String" + TermCon -> "Term" + TypeCon -> "Type" + BoolCon -> "Bool" + IntCon -> "Int" + AIGCon -> "AIG" + CFGCon -> "CFG" + BlockCon -> "" ContextCon cxt -> pretty par cxt instance PrettyPrint Context where pretty _ c = case c of - CryptolSetup -> PP.text "CryptolSetup" - JavaSetup -> PP.text "JavaSetup" - LLVMSetup -> PP.text "LLVMSetup" - ProofScript -> PP.text "ProofScript" - TopLevel -> PP.text "TopLevel" - CrucibleSetup-> PP.text "CrucibleSetup" - -replicateDoc :: Integer -> PP.Doc -> PP.Doc + CryptolSetup -> "CryptolSetup" + JavaSetup -> "JavaSetup" + LLVMSetup -> "LLVMSetup" + ProofScript -> "ProofScript" + TopLevel -> "TopLevel" + CrucibleSetup-> "CrucibleSetup" + +replicateDoc :: Integer -> PP.Doc ann -> PP.Doc ann replicateDoc n d - | n < 1 = PP.empty + | n < 1 = PP.emptyDoc | True = d PP.<> replicateDoc (n-1) d -prettyTypeSig :: PP.Doc -> PP.Doc -> PP.Doc -prettyTypeSig n t = n PP.<+> PP.char ':' PP.<+> t +prettyTypeSig :: PP.Doc ann -> PP.Doc ann -> PP.Doc ann +prettyTypeSig n t = n PP.<+> PP.pretty ':' PP.<+> t -commaSep :: PP.Doc -> PP.Doc -> PP.Doc +commaSep :: PP.Doc ann -> PP.Doc ann -> PP.Doc ann commaSep = ((PP.<+>) . (PP.<> PP.comma)) -commaSepAll :: [PP.Doc] -> PP.Doc +commaSepAll :: [PP.Doc ann] -> PP.Doc ann commaSepAll ds = case ds of - [] -> PP.empty + [] -> PP.emptyDoc _ -> foldl1 commaSep ds -- }}} diff --git a/src/SAWScript/AutoMatch.hs b/src/SAWScript/AutoMatch.hs index 2dd84be006..1e813224e6 100644 --- a/src/SAWScript/AutoMatch.hs +++ b/src/SAWScript/AutoMatch.hs @@ -59,7 +59,7 @@ import SAWScript.LLVMBuiltins --import SAWScript.JavaBuiltins import Language.JVM.Common (dotsToSlashes, mkClassName) -import Text.PrettyPrint.ANSI.Leijen (putDoc, hPutDoc) +import Prettyprinter.Render.Text (putDoc, hPutDoc) import System.IO diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 5a6b562693..48e08ab03b 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -94,7 +94,7 @@ import qualified Cryptol.Backend.Monad as V (runEval) import qualified Cryptol.Eval.Value as V (defaultPPOpts, ppValue) import qualified Cryptol.Eval.Concrete as V (Concrete(..)) -import qualified Text.PrettyPrint.ANSI.Leijen as PP +import qualified Prettyprinter.Render.Text as PP (putDoc) import SAWScript.AutoMatch diff --git a/src/SAWScript/JavaPretty.hs b/src/SAWScript/JavaPretty.hs index 884b018955..beb2a2c91e 100644 --- a/src/SAWScript/JavaPretty.hs +++ b/src/SAWScript/JavaPretty.hs @@ -6,69 +6,75 @@ Maintainer : atomb Stability : provisional -} +{-# LANGUAGE OverloadedStrings #-} + module SAWScript.JavaPretty where import Data.Maybe (fromMaybe) -import Text.PrettyPrint.ANSI.Leijen hiding ((<$>)) +import Prettyprinter import Language.JVM.Common import Verifier.Java.Codebase -prettyClass :: Class -> Doc +prettyClass :: Class -> Doc ann prettyClass cls = vcat $ - [ empty - , text "Class name:" <+> text (unClassName (className cls)) <+> + [ emptyDoc + , "Class name:" <+> prettyClassName (className cls) <+> parens (commas attrs) - , text "Superclass:" <+> text (fromMaybe "none" (fmap unClassName (superClass cls))) - , empty + , "Superclass:" <+> maybe "none" prettyClassName (superClass cls) + , emptyDoc ] ++ (if null (classInterfaces cls) then [] - else [ text "Interfaces:" - , indent 2 (vcat (map (text . unClassName) (classInterfaces cls))) - , empty + else [ "Interfaces:" + , indent 2 (vcat (map prettyClassName (classInterfaces cls))) + , emptyDoc ]) ++ - [ text "Fields:" + [ "Fields:" , indent 2 (vcat (map prettyField (classFields cls))) - , empty - , text "Methods:" + , emptyDoc + , "Methods:" , indent 2 (vcat (map prettyMethod (classMethods cls))) - , empty + , emptyDoc ] where attrs = concat - [ if classIsPublic cls then [text "public"] else [] - , if classIsFinal cls then [text "final"] else [] - , if classHasSuperAttribute cls then [text "super"] else [] - , if classIsInterface cls then [text "interface"] else [] - , if classIsAbstract cls then [text "abstract"] else [] + [ if classIsPublic cls then ["public"] else [] + , if classIsFinal cls then ["final"] else [] + , if classHasSuperAttribute cls then ["super"] else [] + , if classIsInterface cls then ["interface"] else [] + , if classIsAbstract cls then ["abstract"] else [] ] -prettyField :: Field -> Doc +-- FIXME: avoid unpacking via String +prettyClassName :: ClassName -> Doc ann +prettyClassName cname = pretty (unClassName cname) + +prettyField :: Field -> Doc ann prettyField f = hsep $ - [ text (show (fieldVisibility f)) ] ++ + [ viaShow (fieldVisibility f) ] ++ attrs ++ - [ text (show (ppType (fieldType f))) -- TODO: Ick. Different PPs. - , text (fieldName f) + [ viaShow (ppType (fieldType f)) -- TODO: Ick. Different PPs. + , pretty (fieldName f) ] where attrs = concat - [ if fieldIsStatic f then [text "static"] else [] - , if fieldIsFinal f then [text "final"] else [] - , if fieldIsVolatile f then [text "volatile"] else [] - , if fieldIsTransient f then [text "transient"] else [] + [ if fieldIsStatic f then ["static"] else [] + , if fieldIsFinal f then ["final"] else [] + , if fieldIsVolatile f then ["volatile"] else [] + , if fieldIsTransient f then ["transient"] else [] ] -prettyMethod :: Method -> Doc +prettyMethod :: Method -> Doc ann prettyMethod m = hsep $ - (if methodIsStatic m then [text "static"] else []) ++ - [ maybe (text "void") prettyType ret - , text name + (if methodIsStatic m then ["static"] else []) ++ + [ maybe "void" prettyType ret + , pretty name , (parens . commas . map prettyType) params ] where (MethodKey name params ret) = methodKey m - prettyType = text . show . ppType -- TODO: Ick. + prettyType = viaShow . ppType -- TODO: Ick. -commas :: [Doc] -> Doc +commas :: [Doc ann] -> Doc ann commas = sep . punctuate comma From 141008e41a076f9629583e663f58a9792427e622 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 3 Dec 2020 16:00:44 -0800 Subject: [PATCH 3/4] Fix compiler warning. --- src/SAWScript/JavaPretty.hs | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/SAWScript/JavaPretty.hs b/src/SAWScript/JavaPretty.hs index beb2a2c91e..9d9108bd99 100644 --- a/src/SAWScript/JavaPretty.hs +++ b/src/SAWScript/JavaPretty.hs @@ -10,8 +10,6 @@ Stability : provisional module SAWScript.JavaPretty where -import Data.Maybe (fromMaybe) - import Prettyprinter import Language.JVM.Common From 5c423eab9c5c3522a05f5c9edb366777f2a87b52 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 3 Dec 2020 16:35:44 -0800 Subject: [PATCH 4/4] Remove redundant space character from saw-script AST prettyprinter. --- src/SAWScript/AST.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index a6e462c8ac..603c7a8ad6 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -248,7 +248,7 @@ instance Pretty Expr where Var (Located name _ _) -> PP.pretty name Function pat expr -> - "\\" PP.<+> PP.pretty pat PP.<+> "-> " PP.<+> PP.pretty expr + "\\" PP.<+> PP.pretty pat PP.<+> "->" PP.<+> PP.pretty expr -- FIXME, use precedence to minimize parentheses Application f a -> PP.parens (PP.pretty f PP.<+> PP.pretty a) Let (NonRecursive decl) expr ->