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

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/src/Lang/Crucible/LLVM/Errors/MemoryError.hs

@@ -48,6 +48,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           Lang.Crucible.LLVM.PrettyPrint
 
 data MemoryOp sym w
   = MemLoadOp  StorageType (Maybe String) (LLVMPtr sym w) (Mem sym)
@@ -159,7 +160,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 (ppLLVMLatest L.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

@@ -67,6 +67,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           Lang.Crucible.LLVM.PrettyPrint
 import           Lang.Crucible.LLVM.Translation.Constant
 import           Lang.Crucible.LLVM.Translation.Monad
 import           Lang.Crucible.LLVM.Translation.Types
@@ -133,8 +134,7 @@ makeGlobalMap ctx m = foldl' addAliases globalMap (Map.toList (llvmGlobalAliases
            ++ ": "
            ++ err)
      where showSymbol sym =
-             show $ let ?config = LPP.Config False False False
-                    in LPP.ppSymbol $ sym
+             show $ ppLLVMLatest $ LPP.ppSymbol $ sym
 
    globalToConst' :: forall m. (MonadError String m)
                   => L.Global -> m (MemType, Maybe LLVMConst)

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

@@ -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 . ppLLVMLatest L.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 (ppLLVMLatest L.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

@@ -8,18 +8,23 @@
 -- Stability        : provisional
 ------------------------------------------------------------------------
 
+{-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE RankNTypes #-}
 module Lang.Crucible.LLVM.PrettyPrint
   ( commaSepList
   , ppIntType
   , ppPtrType
   , ppArrayType
   , ppVectorType
   , ppIntVector
+  , ppLLVMLatest
   ) where
 
 import Numeric.Natural
 import Prettyprinter
 
+import qualified Text.LLVM.PP as LLVM
+
 -- | Print list of documents separated by commas and spaces.
 commaSepList :: [Doc ann] -> Doc ann
 commaSepList l = hcat (punctuate (comma <> pretty ' ') l)
@@ -40,3 +45,14 @@ 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 '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 :: LLVM.Config) => a) -> a
+ppLLVMLatest = LLVM.withConfig (LLVM.Config { LLVM.cfgVer = LLVM.llvmVlatest })

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

@@ -123,6 +123,7 @@ import           Lang.Crucible.LLVM.Extension
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.Globals
 import           Lang.Crucible.LLVM.MemModel
+import           Lang.Crucible.LLVM.PrettyPrint
 import           Lang.Crucible.LLVM.Translation.Aliases
 import           Lang.Crucible.LLVM.Translation.Constant
 import           Lang.Crucible.LLVM.Translation.Expr
@@ -406,7 +407,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 (ppLLVMLatest L.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           Lang.Crucible.LLVM.PrettyPrint
 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 $ ppLLVMLatest L.ppValue val)
                        ]
 
 

crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs

@@ -82,6 +82,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           Lang.Crucible.LLVM.PrettyPrint
 import           Lang.Crucible.LLVM.Translation.Constant
 import           Lang.Crucible.LLVM.Translation.Expr
 import           Lang.Crucible.LLVM.Translation.Monad
@@ -1985,7 +1986,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 . ppLLVMLatest L.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

@@ -67,6 +67,7 @@ import           Lang.Crucible.Types
 import           Lang.Crucible.LLVM.MemModel.Pointer
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.MalformedLLVMModule
+import           Lang.Crucible.LLVM.PrettyPrint
 import           Lang.Crucible.LLVM.TypeContext as TyCtx
 
 
@@ -178,7 +179,7 @@ llvmDeclToFunHandleRepr' decl k =
     Left msg ->
       malformedLLVMModule
         ( "Invalid declaration for:" <+> fromString (show (L.decName decl)) )
-        [ fromString (show (L.ppDeclare decl))
+        [ fromString (show (ppLLVMLatest L.ppDeclare decl))
         , fromString msg
         ]
 

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

@@ -55,6 +55,7 @@ import           Data.IntMap (IntMap)
 
 import           Lang.Crucible.LLVM.MemType
 import           Lang.Crucible.LLVM.DataLayout
+import           Lang.Crucible.LLVM.PrettyPrint
 
 data IdentStatus
   = Resolved SymType
@@ -83,8 +84,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 (ppLLVMLatest L.ppType tp)
+        ppUnresolvable i = pretty "Could not resolve identifier:" <+> viaShow (ppLLVMLatest L.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

@@ -72,6 +72,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 (ppLLVMLatest)
 import Lang.Crucible.LLVM.Translation
         ( translateModule, ModuleTranslation, globalInitMap
         , transContext, getTranslatedCFG, llvmPtrWidth, llvmTypeCtx
@@ -264,7 +265,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 (ppLLVMLatest LLVM.ppSymbol s))) (Text.pack (show p)) msg
 
 checkFun ::
   forall arch msgs personality sym.