Skip to content

Commit

Permalink
Merge pull request #931 from GaloisInc/prettyprinter
Browse files Browse the repository at this point in the history
Switch from `ansi-wl-pprint` to the `prettyprinter` package.
  • Loading branch information
brianhuffman authored Dec 4, 2020
2 parents 14bab8f + 5c423ea commit 404e227
Show file tree
Hide file tree
Showing 17 changed files with 154 additions and 159 deletions.
2 changes: 0 additions & 2 deletions cabal.GHC-8.6.5.config
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 0 additions & 2 deletions cabal.GHC-8.8.3.config
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 0 additions & 2 deletions cabal.GHC-8.8.4.config
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion deps/crucible
Submodule crucible updated 122 files
2 changes: 1 addition & 1 deletion deps/macaw
Submodule macaw updated 47 files
+1 −1 base/macaw-base.cabal
+44 −33 base/src/Data/Macaw/AbsDomain/AbsState.hs
+9 −8 base/src/Data/Macaw/AbsDomain/JumpBounds.hs
+31 −30 base/src/Data/Macaw/AbsDomain/StackAnalysis.hs
+8 −7 base/src/Data/Macaw/AbsDomain/StridedInterval.hs
+23 −21 base/src/Data/Macaw/Analysis/RegisterUse.hs
+9 −9 base/src/Data/Macaw/CFG/App.hs
+6 −5 base/src/Data/Macaw/CFG/AssignRhs.hs
+13 −9 base/src/Data/Macaw/CFG/Block.hs
+59 −60 base/src/Data/Macaw/CFG/Core.hs
+8 −5 base/src/Data/Macaw/DebugLogging.hs
+1 −1 base/src/Data/Macaw/Discovery.hs
+51 −38 base/src/Data/Macaw/Discovery/State.hs
+43 −41 base/src/Data/Macaw/Dwarf.hs
+11 −10 base/src/Data/Macaw/Memory.hs
+8 −7 base/src/Data/Macaw/Types.hs
+6 −6 base/src/Data/Macaw/Utils/Pretty.hs
+2 −2 cabal.project.dist.ghc-8.10.2.freeze
+2 −2 cabal.project.dist.ghc-8.6.5.freeze
+2 −3 cabal.project.dist.ghc-8.8.4.freeze
+1 −1 deps/asl-translator
+1 −1 deps/crucible
+1 −1 deps/elf-edit
+1 −1 deps/macaw-loader
+1 −1 deps/what4
+2 −2 macaw-aarch32/macaw-aarch32.cabal
+2 −2 macaw-aarch32/src/Data/Macaw/ARM/ARMReg.hs
+11 −10 macaw-aarch32/src/Data/Macaw/ARM/Arch.hs
+3 −3 macaw-aarch32/src/Data/Macaw/ARM/BinaryFormat/ELF.hs
+2 −2 macaw-aarch32/tests/ARMTests.hs
+1 −1 macaw-ppc/macaw-ppc.cabal
+40 −39 macaw-ppc/src/Data/Macaw/PPC/Arch.hs
+1 −1 macaw-ppc/src/Data/Macaw/PPC/Eval.hs
+2 −2 macaw-ppc/src/Data/Macaw/PPC/PPCReg.hs
+0 −1 macaw-semmc/macaw-semmc.cabal
+0 −2 refinement/macaw-refinement.cabal
+2 −3 refinement/src/Data/Macaw/Refinement/Path.hs
+1 −1 symbolic/macaw-symbolic.cabal
+14 −14 symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+1 −1 x86/macaw-x86.cabal
+2 −2 x86/src/Data/Macaw/X86.hs
+16 −15 x86/src/Data/Macaw/X86/ArchTypes.hs
+2 −2 x86/src/Data/Macaw/X86/Generator.hs
+7 −6 x86/src/Data/Macaw/X86/Monad.hs
+2 −2 x86/src/Data/Macaw/X86/X86Reg.hs
+1 −1 x86_symbolic/macaw-x86-symbolic.cabal
+1 −1 x86_symbolic/src/Data/Macaw/X86/Crucible.hs
1 change: 0 additions & 1 deletion saw-script.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,6 @@ library
build-depends:
base >= 4
, aig
, ansi-wl-pprint
, array
, binary
, bimap
Expand Down
170 changes: 87 additions & 83 deletions src/SAWScript/AST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ Stability : provisional
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor,DeriveFoldable,DeriveTraversable #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
Expand Down Expand Up @@ -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 {{{

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand All @@ -346,71 +350,71 @@ 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
(_,[]) -> pretty par tc
(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 "<Block>"
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 -> "<Block>"
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

-- }}}
Expand Down
2 changes: 1 addition & 1 deletion src/SAWScript/AutoMatch.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
25 changes: 14 additions & 11 deletions src/SAWScript/Crucible/Common.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =>
Expand Down
Loading

0 comments on commit 404e227

Please sign in to comment.