Use *WithWarnings functions from llvm-pretty-bc-parser

This bumps the `llvm-pretty-bc-parser` submodule to bring in the changes from GaloisInc/llvm-pretty-bc-parser#282. It also updates the code to use the `*WithWarnings` variants of bitcode parsing functions.
GaloisInc · Feb 20, 2025 · f6e262f · f6e262f
1 parent 50d1550
commit f6e262f
Show file tree

Hide file tree

Showing 6 changed files with 34 additions and 7 deletions.
diff --git a/crucible-llvm/test/Tests.hs b/crucible-llvm/test/Tests.hs
@@ -43,6 +43,7 @@ import qualified System.Directory as Dir
 import           System.Environment ( lookupEnv )
 import           System.Exit ( ExitCode(..) )
 import           System.FilePath ( (-<.>), splitExtension, splitFileName )
+import qualified System.IO as IO
 import qualified System.Process as Proc
 
 -- Modules being tested
@@ -112,11 +113,13 @@ assemble (LLVMAssembler llvm_as) !inputFile !outputFile =
 -- Mostly copied from crucible-c.
 parseLLVM :: FilePath -> IO (Either String Module)
 parseLLVM !file =
-  parseBitCodeFromFile file >>=
+  parseBitCodeFromFileWithWarnings file >>=
     \case
       Left err -> pure $ Left $ "Couldn't parse LLVM bitcode from file"
                                 ++ file ++ "\n" ++ show err
-      Right m  -> pure $ Right m
+      Right (m, warnings) -> do
+        IO.hPrint IO.stderr $ ppParseWarnings warnings
+        pure $ Right m
 
 llvmTestIngredients :: [TR.Ingredient]
 llvmTestIngredients = includingOptions [ TO.Option (Proxy @(SomeSym LLVMAssembler))

diff --git a/crux-llvm/CHANGELOG.md b/crux-llvm/CHANGELOG.md
@@ -2,6 +2,10 @@
 
 * Add support for the Bitwuzla SMT solver in the test suite.
 * Add `--debug` option for starting the Crucible debugger.
+* Emit a warning when parsing an LLVM bitcode metadata record that `crux-llvm`
+  does not support. (Previously, `crux-llvm` would throw a fatal error if this
+  occurred, so this change makes `crux-llvm` more permissive with respect to
+  unsupported LLVM versions.)
 
 # 0.9 -- 2024-08-30
 

diff --git a/crux-llvm/src/Crux/LLVM/Log.hs b/crux-llvm/src/Crux/LLVM/Log.hs
@@ -25,6 +25,7 @@ data CruxLLVMLogMessage
   | FailedToBuildCounterexampleExecutable
   | SimulatingFunction Text
   | UsingPointerWidthForFile Integer Text
+  | ParseWarning Text -- The pretty-printed warnings
   | TranslationWarning Text Text Text -- Function name, position, msg
   deriving ( Generic, ToJSON )
 
@@ -65,6 +66,8 @@ cruxLLVMLogMessageToSayWhat (UsingPointerWidthForFile width file) =
           file
         ]
     )
+cruxLLVMLogMessageToSayWhat (ParseWarning msg) =
+  SayWhat Warn cruxLogTag msg
 cruxLLVMLogMessageToSayWhat (TranslationWarning nm p msg) =
   SayWhat Warn cruxLogTag
     ( Text.unwords

diff --git a/crux-llvm/src/Crux/LLVM/Simulate.hs b/crux-llvm/src/Crux/LLVM/Simulate.hs
@@ -19,6 +19,7 @@ import Data.IORef
 import qualified Data.List as List
 import Data.Maybe ( fromMaybe )
 import qualified Data.Parameterized.Map as MapF
+import Data.Sequence (Seq)
 import qualified Data.Traversable as T
 import Control.Lens ((&), (%~), (%=), (^.), use, view)
 import Control.Monad.IO.Class (liftIO)
@@ -30,7 +31,8 @@ import System.IO (stdout)
 import Data.Parameterized.Some (Some(..))
 import Data.Parameterized.Context (pattern Empty, pattern (:>))
 
-import Data.LLVM.BitCode (parseBitCodeFromFile)
+import Data.LLVM.BitCode (ParseWarning(..), parseBitCodeFromFileWithWarnings,
+                          ppParseWarnings)
 import qualified Text.LLVM as LLVM
 import Prettyprinter
 
@@ -116,12 +118,18 @@ setupSimCtxt halloc bak mo memVar =
     & profilingMetrics %~ Map.union (memMetrics memVar)
 
 -- | Parse an LLVM bit-code file.
-parseLLVM :: FilePath -> IO LLVM.Module
+parseLLVM ::
+  Crux.Logs msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  FilePath ->
+  IO LLVM.Module
 parseLLVM file =
-  do ok <- parseBitCodeFromFile file
+  do ok <- parseBitCodeFromFileWithWarnings file
      case ok of
        Left err -> throwCError (LLVMParseError err)
-       Right m  -> return m
+       Right (m, warnings) -> do
+         sayParseWarnings warnings
+         return m
 
 registerFunctions ::
   Crux.Logs msgs =>
@@ -256,6 +264,13 @@ prepLLVMModule llvmOpts halloc bak bcFile memVar = do
                  =<< initializeAllMemory bak llvmCtxt llvmMod
     return $ PreppedLLVM llvmMod (Some trans) memVar mem
 
+sayParseWarnings ::
+  Log.SupportsCruxLLVMLogMessage msgs =>
+  Crux.Logs msgs =>
+  Seq ParseWarning -> IO ()
+sayParseWarnings =
+  Log.sayCruxLLVM . Log.ParseWarning . Text.pack . show . ppParseWarnings
+
 sayTranslationWarning ::
   Log.SupportsCruxLLVMLogMessage msgs =>
   Crux.Logs msgs =>

diff --git a/dependencies/llvm-pretty-bc-parser b/dependencies/llvm-pretty-bc-parser
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs
@@ -288,6 +288,8 @@ data SomeModuleContext'
   = forall m arch. SomeModuleContext' (ModuleContext m arch)
 
 translateFile ::
+  Crux.Logs msgs =>
+  Log.SupportsCruxLLVMLogMessage msgs =>
   LLVMOptions ->
   Crucible.HandleAllocator ->
   GlobalVar Mem ->
+19 −0		CHANGELOG.md
+16 −9		disasm-test/Main.hs
+32 −0		disasm-test/known_bugs/llvm_dbg_declare_inline
+23 −0		disasm-test/tests/localstatic.c
+146 −0		disasm-test/tests/localstatic.ll
+3 −3		flake.lock
+7 −5		llvm-disasm/LLVMDis.hs
+1 −1		llvm-pretty
+2 −2		llvm-pretty-bc-parser.cabal
+111 −8		src/Data/LLVM/BitCode.hs
+23 −44		src/Data/LLVM/BitCode/IR/Function.hs
+5 −5		src/Data/LLVM/BitCode/IR/Globals.hs
+29 −32		src/Data/LLVM/BitCode/IR/Metadata.hs
+22 −20		src/Data/LLVM/BitCode/IR/Module.hs
+5 −3		src/Data/LLVM/BitCode/IR/Values.hs
+224 −52		src/Data/LLVM/BitCode/Parse.hs