From f6e262f96b73eb208c30285b71a2fa8d938325fe Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Thu, 20 Feb 2025 09:57:38 -0500 Subject: [PATCH] Use *WithWarnings functions from llvm-pretty-bc-parser This bumps the `llvm-pretty-bc-parser` submodule to bring in the changes from https://github.com/GaloisInc/llvm-pretty-bc-parser/pull/282. It also updates the code to use the `*WithWarnings` variants of bitcode parsing functions. --- crucible-llvm/test/Tests.hs | 7 +++++-- crux-llvm/CHANGELOG.md | 4 ++++ crux-llvm/src/Crux/LLVM/Log.hs | 3 +++ crux-llvm/src/Crux/LLVM/Simulate.hs | 23 +++++++++++++++++++---- dependencies/llvm-pretty-bc-parser | 2 +- uc-crux-llvm/src/UCCrux/LLVM/Main.hs | 2 ++ 6 files changed, 34 insertions(+), 7 deletions(-) diff --git a/crucible-llvm/test/Tests.hs b/crucible-llvm/test/Tests.hs index b9c7fdbc6..83dfabde5 100644 --- 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 index 3c7900200..aa3182841 100644 --- 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 index cab89a333..04bf7d157 100644 --- 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 index 4bdfa00e9..6e1fc0954 100644 --- 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 index 0f789a1fb..fefa21658 160000 --- a/dependencies/llvm-pretty-bc-parser +++ b/dependencies/llvm-pretty-bc-parser @@ -1 +1 @@ -Subproject commit 0f789a1fb5150363e573dbe602e0dcd8bbf9f23c +Subproject commit fefa216587d7c6a37ea63dcdfcddb8fde657fbe3 diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/uc-crux-llvm/src/UCCrux/LLVM/Main.hs index 23d6055e1..824a80d9f 100644 --- 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 ->