Bump submodules.

heapster-saw/src/Verifier/SAW/Heapster/LLVMGlobalConst.hs

@@ -30,6 +30,7 @@ import Data.Parameterized.Some
 import Lang.Crucible.Types
 import Lang.Crucible.LLVM.DataLayout
 import Lang.Crucible.LLVM.MemModel
+import Lang.Crucible.LLVM.PrettyPrint
 
 import Verifier.SAW.OpenTerm
 import Verifier.SAW.Term.Functor (ModuleName)
@@ -86,12 +87,12 @@ traceAndZeroM msg =
 -- | Helper function to pretty-print the value of a global
 ppLLVMValue :: L.Value -> String
 ppLLVMValue val =
-  L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppValue val)
+  ppLLVMLatest (show $ PPHPJ.nest 2 $ L.ppValue val)
 
 -- | Helper function to pretty-print an LLVM constant expression
 ppLLVMConstExpr :: L.ConstExpr -> String
 ppLLVMConstExpr ce =
-  L.withConfig (L.Config True True True) (show $ PPHPJ.nest 2 $ L.ppConstExpr ce)
+  ppLLVMLatest (show $ PPHPJ.nest 2 $ L.ppConstExpr ce)
 
 -- | Translate a typed LLVM 'L.Value' to a Heapster shape + an element of the
 -- translation of that shape to a SAW core type
@@ -182,7 +183,7 @@ translateLLVMType _ (L.PrimType (L.Integer n))
             (bvTypeOpenTerm n))
 translateLLVMType _ tp =
   traceAndZeroM ("translateLLVMType does not yet handle:\n"
-                 ++ show (L.ppType tp))
+                 ++ show (ppType tp))
 
 -- | Helper function for 'translateLLVMValue' applied to a constant expression
 translateLLVMConstExpr :: (1 <= w, KnownNat w) => NatRepr w -> L.ConstExpr ->
@@ -251,7 +252,7 @@ translateZeroInit w (L.PackedStruct tps) =
 
 translateZeroInit _ tp =
   traceAndZeroM ("translateZeroInit cannot handle type:\n"
-                 ++ show (L.ppType tp))
+                 ++ show (ppType tp))
 
 -- | Top-level call to 'translateLLVMValue', running the 'LLVMTransM' monad
 translateLLVMValueTop :: (1 <= w, KnownNat w) => DebugLevel -> EndianForm ->

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -124,7 +124,6 @@ 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.URI
 import qualified Control.Monad.Trans.Maybe as MaybeT
 
@@ -167,6 +166,7 @@ import qualified Lang.Crucible.LLVM.Bytes as Crucible
 import qualified Lang.Crucible.LLVM.Intrinsics as Crucible
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 import qualified Lang.Crucible.LLVM.MemType as Crucible
+import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible
 import           Lang.Crucible.LLVM.QQ( llvmOvr )
 import qualified Lang.Crucible.LLVM.Translation as Crucible
 
@@ -231,13 +231,13 @@ displayVerifExceptionOpts opts (DefNotFound (L.Symbol nm) nms) =
   [ "Could not find definition for function named `" ++ nm ++ "`."
   ] ++ if simVerbose opts < 3
        then [ "Run SAW with --sim-verbose=3 to see all function names" ]
-       else "Available function names:" : map (("  " ++) . show . L.ppSymbol) nms
+       else "Available function names:" : map (("  " ++) . show . Crucible.ppSymbol) nms
 displayVerifExceptionOpts opts (DeclNotFound (L.Symbol nm) nms) =
   unlines $
   [ "Could not find declaration for function named `" ++ nm ++ "`."
   ] ++ if simVerbose opts < 3
        then [ "Run SAW with --sim-verbose=3 to see all function names" ]
-       else "Available function names:" : map (("  " ++) . show . L.ppSymbol) nms
+       else "Available function names:" : map (("  " ++) . show . Crucible.ppSymbol) nms
 displayVerifExceptionOpts _ (SetupError e) =
   "Error during simulation setup: " ++ show (ppSetupError e)
 
@@ -1825,7 +1825,7 @@ handleTranslationWarning :: Options -> Crucible.LLVMTranslationWarning -> IO ()
 handleTranslationWarning opts (Crucible.LLVMTranslationWarning s p msg) =
   printOutLn opts Warn $ unwords
     [ "LLVM bitcode translation warning"
-    , show (L.ppSymbol s)
+    , show (Crucible.ppSymbol s)
     , show p
     , Text.unpack msg
     ]
@@ -2163,7 +2163,7 @@ llvm_fresh_var name lty =
      sc <- lift $ lift getSharedContext
      let dl = Crucible.llvmDataLayout (ccTypeCtx cctx)
      case cryptolTypeOfActual dl lty' of
-       Nothing -> throwCrucibleSetup loc $ "Unsupported type in llvm_fresh_var: " ++ show (L.ppType lty)
+       Nothing -> throwCrucibleSetup loc $ "Unsupported type in llvm_fresh_var: " ++ show (Crucible.ppType lty)
        Just cty -> Setup.freshVariable sc name cty
 
 llvm_fresh_cryptol_var ::
@@ -2261,7 +2261,7 @@ memTypeForLLVMType loc lty =
   case Crucible.liftMemType lty of
     Right m -> return m
     Left err -> throwCrucibleSetup loc $ unlines
-      [ "unsupported type: " ++ show (L.ppType lty)
+      [ "unsupported type: " ++ show (Crucible.ppType lty)
       , "Details:"
       , err
       ]
@@ -2277,7 +2277,7 @@ llvm_sizeof (Some lm) lty =
      case Crucible.liftMemType lty of
        Right mty -> pure (Crucible.bytesToInteger (Crucible.memTypeSize dl mty))
        Left err -> fail $ unlines
-         [ "llvm_sizeof: Unsupported type: " ++ show (L.ppType lty)
+         [ "llvm_sizeof: Unsupported type: " ++ show (Crucible.ppType lty)
          , "Details:"
          , err
          ]

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -121,7 +121,6 @@ import           Data.Functor.Compose (Compose(..))
 import qualified Data.Map as Map
 import qualified Prettyprinter as PPL
 import qualified Text.LLVM.AST as L
-import qualified Text.LLVM.PP as L
 
 import           Data.Parameterized.All (All(All))
 import           Data.Parameterized.Some (Some(Some))
@@ -132,6 +131,7 @@ import           What4.ProgramLoc (ProgramLoc)
 import qualified Lang.Crucible.Types as Crucible (SymbolRepr, knownSymbol)
 import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
   (IntrinsicMuxFn(IntrinsicMuxFn))
+import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM
 
 import           SAWScript.Crucible.Common
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
@@ -243,11 +243,11 @@ data SetupError
 ppSetupError :: SetupError -> PPL.Doc ann
 ppSetupError (InvalidReturnType t) =
   PPL.pretty "Can't lift return type" PPL.<+>
-  PPL.viaShow (L.ppType t) PPL.<+>
+  PPL.viaShow (Crucible.LLVM.ppType t) PPL.<+>
   PPL.pretty "to a Crucible type."
 ppSetupError (InvalidArgTypes ts) =
   PPL.pretty "Can't lift argument types " PPL.<+>
-  PPL.encloseSep PPL.lparen PPL.rparen PPL.comma (map (PPL.viaShow . L.ppType) ts) PPL.<+>
+  PPL.encloseSep PPL.lparen PPL.rparen PPL.comma (map (PPL.viaShow . Crucible.LLVM.ppType) ts) PPL.<+>
   PPL.pretty "to Crucible types."
 
 resolveArgs ::

src/SAWScript/Crucible/LLVM/Setup/Value.hs

@@ -83,6 +83,7 @@ module SAWScript.Crucible.LLVM.Setup.Value
 import           Control.Lens
 import           Data.Map ( Map )
 import qualified Data.Map as Map
+import           Data.Maybe
 import qualified Data.Text as Text
 import           Data.Type.Equality (TestEquality(..))
 import           Data.Void (Void)
@@ -100,6 +101,7 @@ import           What4.ProgramLoc (ProgramLoc)
 import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator)
 import qualified Lang.Crucible.Simulator.ExecutionTree as Crucible (SimContext)
 import qualified Lang.Crucible.Simulator.GlobalState as Crucible (SymGlobalState)
+import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM
 
 import           SAWScript.Crucible.Common
 import qualified SAWScript.Crucible.Common.Setup.Value as Setup
@@ -236,19 +238,19 @@ showLLVMModule :: LLVMModule arch -> String
 showLLVMModule (LLVMModule name m _) =
   unlines [ "Module: " ++ name
           , "Types:"
-          , showParts L.ppTypeDecl (L.modTypes m)
+          , showParts (Crucible.LLVM.ppLLVMLatest L.ppTypeDecl) (L.modTypes m)
           , "Globals:"
-          , showParts ppGlobal' (L.modGlobals m)
+          , showParts (Crucible.LLVM.ppLLVMLatest ppGlobal') (L.modGlobals m)
           , "External references:"
-          , showParts L.ppDeclare (L.modDeclares m)
+          , showParts Crucible.LLVM.ppDeclare (L.modDeclares m)
           , "Definitions:"
-          , showParts ppDefine' (L.modDefines m)
+          , showParts (Crucible.LLVM.ppLLVMLatest ppDefine') (L.modDefines m)
           ]
   where
     showParts pp xs = unlines $ map (show . PP.nest 2 . pp) xs
     ppGlobal' g =
       L.ppSymbol (L.globalSym g) PP.<+> PP.char '=' PP.<+>
-      L.ppGlobalAttrs (L.globalAttrs g) PP.<+>
+      L.ppGlobalAttrs (isJust $ L.globalValue g) (L.globalAttrs g) PP.<+>
       L.ppType (L.globalType g)
     ppDefine' d =
       L.ppMaybe L.ppLinkage (L.defLinkage d) PP.<+>

src/SAWScript/HeapsterBuiltins.hs

@@ -101,14 +101,14 @@ import Lang.Crucible.FunctionHandle
 import Lang.Crucible.CFG.Core
 import Lang.Crucible.LLVM.Extension
 import Lang.Crucible.LLVM.MemModel
+import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM
 import Lang.Crucible.LLVM.Translation
 -- import Lang.Crucible.LLVM.Translation.Types
 import Lang.Crucible.LLVM.TypeContext
 import Lang.Crucible.LLVM.DataLayout
 
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.Parser as L
-import qualified Text.LLVM.PP as L
 import qualified Text.PrettyPrint.HughesPJ as L (render)
 
 import SAWScript.TopLevel
@@ -973,7 +973,7 @@ heapster_find_symbol_commands _bic _opts henv str =
   return $
   concatMap (\tp ->
               "heapster_find_symbol_with_type env\n  \"" ++ str ++ "\"\n  " ++
-              print_as_saw_script_string (L.render $ L.ppType tp) ++ ";\n") $
+              print_as_saw_script_string (L.render $ Crucible.LLVM.ppType tp) ++ ";\n") $
   concatMap (\(Some lm) ->
               mapMaybe (\decl ->
                          if isInfixOf str (symString $ L.decName decl)

src/SAWScript/Value.hs

@@ -74,7 +74,6 @@ import qualified SAWScript.Crucible.JVM.MethodSpecIR ()
 import qualified SAWScript.Crucible.MIR.MethodSpecIR ()
 import qualified Lang.JVM.Codebase as JSS
 import qualified Text.LLVM.AST as LLVM (Type)
-import qualified Text.LLVM.PP as LLVM (ppType)
 import SAWScript.JavaExpr (JavaType(..))
 import SAWScript.JavaPretty (prettyClass)
 import SAWScript.MGU (instantiate)
@@ -118,6 +117,7 @@ import qualified Lang.Crucible.JVM as CJ
 
 import           Lang.Crucible.Utils.StateContT
 import           Lang.Crucible.LLVM.ArraySizeProfile
+import qualified Lang.Crucible.LLVM.PrettyPrint as Crucible.LLVM
 
 import           Mir.Generator
 import           Mir.Intrinsics (MIR)
@@ -373,7 +373,7 @@ showsPrecValue opts nenv p v =
     VLLVMSkeletonState _ -> showString "<<Skeleton state>>"
     VLLVMFunctionProfile _ -> showString "<<Array sizes for function>>"
     VJavaType {} -> showString "<<Java type>>"
-    VLLVMType t -> showString (show (LLVM.ppType t))
+    VLLVMType t -> showString (show (Crucible.LLVM.ppType t))
     VMIRType t -> showString (show (PP.pretty t))
     VCryptolModule m -> showString (showCryptolModule m)
     VLLVMModule (Some m) -> showString (CMSLLVM.showLLVMModule m)