From 4739fe7e9dc001b93e00febf5579d3fa0cfee73f Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 10 Jan 2024 10:09:05 -0500 Subject: [PATCH] {crucible,crux}-llvm: Adapt to elliottt/llvm-pretty#118 This patch: * Bumps the `llvm-pretty` and `llvm-pretty-bc-parser` submodules to recent commits that include the changes from https://github.com/elliottt/llvm-pretty/pull/118. * Introduces a `ppLLVMLatest` combinator to `Lang.Crucible.LLVM.PrettyPrint` that prints a `Fmt` value (from `Text.LLVM.PP`) using the latest version of LLVM that `llvm-pretty` supports. * Uses `ppLLVMLatest` in the appropriate places to fix compilation errors. Fixes #1145. --- crucible-llvm/crucible-llvm.cabal | 1 + .../Lang/Crucible/LLVM/Errors/MemoryError.hs | 4 +- .../src/Lang/Crucible/LLVM/Globals.hs | 7 +-- .../src/Lang/Crucible/LLVM/MemType.hs | 8 +-- .../src/Lang/Crucible/LLVM/PrettyPrint.hs | 55 +++++++++++++++++++ .../src/Lang/Crucible/LLVM/Translation.hs | 4 +- .../Crucible/LLVM/Translation/Constant.hs | 5 +- .../Crucible/LLVM/Translation/Instruction.hs | 4 +- .../Lang/Crucible/LLVM/Translation/Types.hs | 4 +- .../src/Lang/Crucible/LLVM/TypeContext.hs | 6 +- crux-llvm/src/Crux/LLVM/Simulate.hs | 4 +- dependencies/llvm-pretty | 2 +- dependencies/llvm-pretty-bc-parser | 2 +- 13 files changed, 80 insertions(+), 26 deletions(-) diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal index 219a79dbe..8a6af2ef2 100644 --- a/crucible-llvm/crucible-llvm.cabal +++ b/crucible-llvm/crucible-llvm.cabal @@ -42,6 +42,7 @@ library llvm-pretty >= 0.8 && < 0.12, mtl, parameterized-utils >= 2.1.5 && < 2.2, + pretty, prettyprinter >= 1.7.0, text, template-haskell, diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs index 35a821620..6972935ab 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Errors/MemoryError.hs @@ -36,7 +36,6 @@ module Lang.Crucible.LLVM.Errors.MemoryError import Prelude hiding (pred) import Data.Text (Text) -import qualified Text.LLVM.PP as L import qualified Text.LLVM.AST as L import Type.Reflection (SomeTypeRep(SomeTypeRep)) import Prettyprinter @@ -48,6 +47,7 @@ import Lang.Crucible.LLVM.MemModel.Pointer (LLVMPtr, concBV) import Lang.Crucible.LLVM.MemModel.Common import Lang.Crucible.LLVM.MemModel.Type import Lang.Crucible.LLVM.MemModel.MemLog +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP data MemoryOp sym w = MemLoadOp StorageType (Maybe String) (LLVMPtr sym w) (Mem sym) @@ -159,7 +159,7 @@ ppMemoryOp (MemCopyOp (gsym_dest, dest) (gsym_src, src) len mem) = ppMemoryOp (MemLoadHandleOp sig gsym ptr mem) = vsep [ case sig of Just s -> - hsep ["Attempting to load callable function with type:", viaShow (L.ppType s)] + hsep ["Attempting to load callable function with type:", viaShow (LPP.ppType s)] Nothing -> hsep ["Attempting to load callable function:"] , indent 2 (hsep ([ "Via pointer:" ] ++ ppGSym gsym ++ [ ppPtr ptr ])) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs index 9aba1b27c..897c80459 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Globals.hs @@ -57,7 +57,6 @@ import Data.Maybe (fromMaybe) import qualified Data.Parameterized.Context as Ctx import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as LPP import qualified Data.BitVector.Sized as BV import Data.Parameterized.NatRepr as NatRepr @@ -67,6 +66,7 @@ import Lang.Crucible.LLVM.DataLayout import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.MemModel import qualified Lang.Crucible.LLVM.MemModel.Generic as G +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.Translation.Constant import Lang.Crucible.LLVM.Translation.Monad import Lang.Crucible.LLVM.Translation.Types @@ -129,12 +129,9 @@ makeGlobalMap ctx m = foldl' addAliases globalMap (Map.toList (llvmGlobalAliases (globalToConst' g) (\err -> Left $ "Encountered error while processing global " - ++ showSymbol (L.globalSym g) + ++ show (LPP.ppSymbol (L.globalSym g)) ++ ": " ++ err) - where showSymbol sym = - show $ let ?config = LPP.Config False False False - in LPP.ppSymbol $ sym globalToConst' :: forall m. (MonadError String m) => L.Global -> m (MemType, Maybe LLVMConst) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs index a5d2c48b7..f885c94e5 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemType.hs @@ -57,12 +57,12 @@ import Data.Vector (Vector) import qualified Data.Vector as V import Numeric.Natural import qualified Text.LLVM as L -import qualified Text.LLVM.PP as L import Prettyprinter import Lang.Crucible.LLVM.Bytes import Lang.Crucible.LLVM.DataLayout -import Lang.Crucible.LLVM.PrettyPrint +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP +import Lang.Crucible.LLVM.PrettyPrint hiding (ppIdent, ppType) import Lang.Crucible.Panic ( panic ) -- | Performs a binary search on a range of ints. @@ -81,7 +81,7 @@ binarySearch f = go where i = l + (h - l) `div` 2 ppIdent :: L.Ident -> Doc ann -ppIdent = viaShow . L.ppIdent +ppIdent = viaShow . LPP.ppIdent -- TODO: update if llvm-pretty switches to prettyprinter -- | LLVM types supported by symbolic simulator. @@ -110,7 +110,7 @@ ppSymType (Alias i) = ppIdent i ppSymType (FunType d) = ppFunDecl d ppSymType VoidType = pretty "void" ppSymType OpaqueType = pretty "opaque" -ppSymType (UnsupportedType tp) = viaShow (L.ppType tp) +ppSymType (UnsupportedType tp) = viaShow (LPP.ppType tp) -- TODO: update if llvm-pretty switches to prettyprinter -- | LLVM types supported by simulator with a defined size and alignment. diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/PrettyPrint.hs b/crucible-llvm/src/Lang/Crucible/LLVM/PrettyPrint.hs index 5389f6031..06d23b303 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/PrettyPrint.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/PrettyPrint.hs @@ -6,8 +6,15 @@ -- License : BSD3 -- Maintainer : Rob Dockins -- Stability : provisional +-- +-- This module defines several functions whose names clash with functions +-- offered elsewhere in @llvm-pretty@ (e.g., "Text.LLVM.PP") and in +-- @crucible-llvm@ (e.g., "Lang.Crucible.LLVM.MemModel.MemLog"). For this +-- reason, it is recommended to import this module qualified. ------------------------------------------------------------------------ +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE RankNTypes #-} module Lang.Crucible.LLVM.PrettyPrint ( commaSepList , ppIntType @@ -15,10 +22,22 @@ module Lang.Crucible.LLVM.PrettyPrint , ppArrayType , ppVectorType , ppIntVector + + -- * @llvm-pretty@ printing with the latest LLVM version + , ppLLVMLatest + , ppDeclare + , ppIdent + , ppSymbol + , ppType + , ppValue ) where import Numeric.Natural import Prettyprinter +import qualified Text.PrettyPrint.HughesPJ as HPJ + +import qualified Text.LLVM.AST as L +import qualified Text.LLVM.PP as L -- | Print list of documents separated by commas and spaces. commaSepList :: [Doc ann] -> Doc ann @@ -40,3 +59,39 @@ ppVectorType n e = angles (pretty (toInteger n) <+> pretty 'x' <+> e) ppIntVector :: Integral a => Natural -> a -> Doc ann ppIntVector n w = ppVectorType n (ppIntType w) + +-- | Pretty-print an LLVM-related AST in accordance with the latest LLVM version +-- that @llvm-pretty@ currently supports (i.e., the value of 'L.llvmVlatest'.) +-- +-- Note that we are mainly using the @llvm-pretty@ printer in @crucible-llvm@ +-- for the sake of defining 'Show' instances and creating error messages, not +-- for creating machine-readable LLVM code. As a result, it doesn't particularly +-- matter which LLVM version we use, as any version-specific differences in +-- pretty-printer output won't be that impactful. +ppLLVMLatest :: ((?config :: L.Config) => a) -> a +ppLLVMLatest = L.withConfig (L.Config { L.cfgVer = L.llvmVlatest }) + +-- | Invoke 'L.ppDeclare' in accordance with the latest LLVM version that +-- @llvm-pretty@ supports. +ppDeclare :: L.Declare -> HPJ.Doc +ppDeclare = ppLLVMLatest L.ppDeclare + +-- | Invoke 'L.ppIdent' in accordance with the latest LLVM version that +-- @llvm-pretty@ supports. +ppIdent :: L.Ident -> HPJ.Doc +ppIdent = ppLLVMLatest L.ppIdent + +-- | Invoke 'L.ppSymbol' in accordance with the latest LLVM version that +-- @llvm-pretty@ supports. +ppSymbol :: L.Symbol -> HPJ.Doc +ppSymbol = ppLLVMLatest L.ppSymbol + +-- | Invoke 'L.ppType' in accordance with the latest LLVM version that +-- @llvm-pretty@ supports. +ppType :: L.Type -> HPJ.Doc +ppType = ppLLVMLatest L.ppType + +-- | Invoke 'L.ppValue' in accordance with the latest LLVM version that +-- @llvm-pretty@ supports. +ppValue :: L.Value -> HPJ.Doc +ppValue = ppLLVMLatest L.ppValue diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs index 66361649d..e438e23e7 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation.hs @@ -105,7 +105,6 @@ import qualified Data.Text as Text import Prettyprinter (pretty) import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L import Data.Parameterized.NatRepr as NatRepr import Data.Parameterized.Some @@ -123,6 +122,7 @@ import Lang.Crucible.LLVM.Extension import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.Globals import Lang.Crucible.LLVM.MemModel +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.Translation.Aliases import Lang.Crucible.LLVM.Translation.Constant import Lang.Crucible.LLVM.Translation.Expr @@ -406,7 +406,7 @@ checkEntryPointUseSet nm bi args malformedLLVMModule ("Invalid SSA form for function: " <> pretty nm) ([ "The following LLVM virtual registers have at least one use site that" , "is not dominated by the corresponding definition:" ] ++ - [ " " <> pretty (show (L.ppIdent i)) | i <- Set.toList unsatisfiedUses ]) + [ " " <> pretty (show (LPP.ppIdent i)) | i <- Set.toList unsatisfiedUses ]) where argSet = Set.fromList (map L.typedValue args) useSet = block_use_set bi diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs index 745ef59f4..ce720cada 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Constant.hs @@ -79,6 +79,7 @@ import Lang.Crucible.LLVM.Bytes import Lang.Crucible.LLVM.DataLayout( intLayout, EndianForm(..) ) import Lang.Crucible.LLVM.MemModel.Pointer import Lang.Crucible.LLVM.MemType +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.Translation.Types import Lang.Crucible.LLVM.TypeContext @@ -346,7 +347,7 @@ instance Show LLVMConst where (IntConst w x) -> ["IntConst", show w, show x] (FloatConst f) -> ["FloatConst", show f] (DoubleConst d) -> ["DoubleConst", show d] - ld@(LongDoubleConst _)-> ["LongDoubleConst", show $ L.ppLLVM ld] + ld@(LongDoubleConst _)-> ["LongDoubleConst", show ld] (ArrayConst mem a) -> ["ArrayConst", show mem, show a] (VectorConst mem v) -> ["VectorConst", show mem, show v] (StructConst si a) -> ["StructConst", show si, show a] @@ -468,7 +469,7 @@ transConstant' _ (L.ValConstExpr cexpr) = transConstantExpr cexpr transConstant' tp val = throwError $ unlines [ "Cannot compute constant value for expression: " , "Type: " ++ (show $ ppMemType tp) - , "Value: " ++ (show $ L.ppLLVM val) + , "Value: " ++ (show $ LPP.ppValue val) ] diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs index e88585319..4595a244a 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs @@ -63,7 +63,6 @@ import Prettyprinter (pretty) import GHC.Exts ( Proxy#, proxy# ) import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L import qualified Data.BitVector.Sized as BV import qualified Data.Parameterized.Context as Ctx @@ -82,6 +81,7 @@ import qualified Lang.Crucible.LLVM.Errors.UndefinedBehavior as UB import Lang.Crucible.LLVM.Extension import Lang.Crucible.LLVM.MemModel import Lang.Crucible.LLVM.MemType +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.Translation.Constant import Lang.Crucible.LLVM.Translation.Expr import Lang.Crucible.LLVM.Translation.Monad @@ -1985,7 +1985,7 @@ dbgArgs defSet args = pure (Right (v, lv, di)) else do let msg = unwords (["dbg intrinsic def/use violation for:"] ++ - map (show . L.ppIdent) (Set.toList unusableIdents)) + map (show . LPP.ppIdent) (Set.toList unusableIdents)) pure (Left msg) _ -> pure (Left ("dbg: argument 3 expected DIExpression, got: " ++ show diArg)) _ -> pure (Left ("dbg: argument 2 expected local variable metadata, got: " ++ show lvArg)) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs index a310757a0..13517a0dc 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/Translation/Types.hs @@ -54,7 +54,6 @@ import Data.Foldable import Data.String import qualified Text.LLVM.AST as L -import qualified Text.LLVM.PP as L import Prettyprinter import qualified Data.Parameterized.Context as Ctx @@ -67,6 +66,7 @@ import Lang.Crucible.Types import Lang.Crucible.LLVM.MemModel.Pointer import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.MalformedLLVMModule +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP import Lang.Crucible.LLVM.TypeContext as TyCtx @@ -178,7 +178,7 @@ llvmDeclToFunHandleRepr' decl k = Left msg -> malformedLLVMModule ( "Invalid declaration for:" <+> fromString (show (L.decName decl)) ) - [ fromString (show (L.ppDeclare decl)) + [ fromString (show (LPP.ppDeclare decl)) , fromString msg ] diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs b/crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs index 6678caf85..7ef79cd77 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/TypeContext.hs @@ -49,12 +49,12 @@ import qualified Data.Set as Set import qualified Data.Vector as V import qualified Text.LLVM as L import qualified Text.LLVM.DebugUtils as L -import qualified Text.LLVM.PP as L import Prettyprinter import Data.IntMap (IntMap) import Lang.Crucible.LLVM.MemType import Lang.Crucible.LLVM.DataLayout +import qualified Lang.Crucible.LLVM.PrettyPrint as LPP data IdentStatus = Resolved SymType @@ -83,8 +83,8 @@ runTC pdl initMap m = over _1 tcsErrors . view swapped $ runState m tcs0 tcsErrors :: TCState -> [Doc ann] tcsErrors tcs = (ppUnsupported <$> Set.toList (tcsUnsupported tcs)) ++ (ppUnresolvable <$> Set.toList (tcsUnresolvable tcs)) - where ppUnsupported tp = pretty "Unsupported type:" <+> viaShow (L.ppType tp) - ppUnresolvable i = pretty "Could not resolve identifier:" <+> viaShow (L.ppIdent i) + where ppUnsupported tp = pretty "Unsupported type:" <+> viaShow (LPP.ppType tp) + ppUnresolvable i = pretty "Could not resolve identifier:" <+> viaShow (LPP.ppIdent i) -- TODO: update if llvm-pretty switches to prettyprinter -- | Type lifter contains types that could not be parsed. diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs index 9c8774cac..d836ae067 100644 --- a/crux-llvm/src/Crux/LLVM/Simulate.hs +++ b/crux-llvm/src/Crux/LLVM/Simulate.hs @@ -33,7 +33,6 @@ import Data.Parameterized.Context (pattern Empty, pattern (:>)) import Data.LLVM.BitCode (parseBitCodeFromFile) import qualified Text.LLVM as LLVM -import qualified Text.LLVM.PP as LLVM import Prettyprinter -- what4 @@ -72,6 +71,7 @@ import Lang.Crucible.LLVM.MemModel ) import Lang.Crucible.LLVM.MemModel.CallStack (ppCallStack) import Lang.Crucible.LLVM.MemType (MemType(..), SymType(..), i8, memTypeAlign, memTypeSize) +import Lang.Crucible.LLVM.PrettyPrint (ppSymbol) import Lang.Crucible.LLVM.Translation ( translateModule, ModuleTranslation, globalInitMap , transContext, getTranslatedCFG, llvmPtrWidth, llvmTypeCtx @@ -264,7 +264,7 @@ sayTranslationWarning :: sayTranslationWarning = Log.sayCruxLLVM . f where f (LLVMTranslationWarning s p msg) = - Log.TranslationWarning (Text.pack (show (LLVM.ppSymbol s))) (Text.pack (show p)) msg + Log.TranslationWarning (Text.pack (show (ppSymbol s))) (Text.pack (show p)) msg checkFun :: forall arch msgs personality sym. diff --git a/dependencies/llvm-pretty b/dependencies/llvm-pretty index 94e384842..8124fc026 160000 --- a/dependencies/llvm-pretty +++ b/dependencies/llvm-pretty @@ -1 +1 @@ -Subproject commit 94e384842b214ba72446d1694446fb5261ab6ce2 +Subproject commit 8124fc0265b6ca5fde5812c789f40b2ea54af678 diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser index ac9fff49e..39b4a5ff2 160000 --- a/dependencies/llvm-pretty-bc-parser +++ b/dependencies/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit ac9fff49ef1670e58be9ce90075eaa02726f8662 +Subproject commit 39b4a5ff26ad88f7db250185cc5b471fac50141d