{crucible,crux}-llvm: Adapt to GaloisInc/llvm-pretty#118 (#1162)

This patch:

* Bumps the `llvm-pretty` and `llvm-pretty-bc-parser` submodules to recent
  commits that include the changes from
  GaloisInc/llvm-pretty#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

@@ -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,

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 ]))

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)

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.

crucible-llvm/src/Lang/Crucible/LLVM/PrettyPrint.hs

@@ -6,19 +6,38 @@
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <[email protected]>
 -- 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
   , ppPtrType
   , 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

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

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)
                        ]
 
 

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))

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
         ]
 

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.

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.