diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,21 @@ +# 0.13 -- 2026-09-10 + +* Add support for GHC 9.12 (at 9.12.2) and bump from 9.10.1 to 9.10.3. +* Support LLVM 22. +* **BREAKING**: `explainFailure` now takes a `FloatModeRepr` argument. + +# 0.12 -- 2026-01-29 + +# 0.11 -- 2025-11-09 + +* Sync the version number with `crux-mir-0.11` as part of the overall Crux 0.10 + release. + +# 0.10 -- 2025-03-24 + +* Sync the version number with `crux-mir-0.10` as part of the overall Crux 0.10 + release. + # 0.9.1 -- 2025-03-21 * Add support for the Bitwuzla SMT solver in the test suite. diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,12 +1,16 @@ -# Overview +# Crux-LLVM +Crux logo + +## Overview + The `crux-llvm` tool (and corresponding C library) are intended for verifying C programs containing inline specifications (in the form of function calls to create non-deterministic values and assert properties). For more information about Crux itself, refer to the [official website](https://crux.galois.com). -# Licensing and bundled tools +## Licensing and bundled tools `crux-llvm` is licensed under the 3-Clause BSD license. For more details, refer to the `LICENSE` file. Some binary distributions of `crux-llvm` come bundled @@ -21,7 +25,7 @@ `crux-llvm` does not link against any of these tools directly. As a result, `crux-llvm` adheres to the GPLv3 licensing terms in Yices. -# Prerequisites +## Prerequisites Before running `crux-llvm`, you'll need to install the following software: @@ -46,11 +50,11 @@ and `cabal` version 3.10. We recommend Yices 2.6.x, and Z3 4.8.x. Technically, only one of Yices or Z3 is required, and CVC4 is also supported. However, in practice, having both tends to be -convenient. Finally, LLVM versions from 3.6 through 16 are likely to +convenient. Finally, LLVM versions from 3.6 through 22 are likely to work well, and any failures with versions in that range should be [reported as bugs](https://github.com/GaloisInc/crucible/issues). -# Building +## Building The `crux-llvm` tool can be built by doing the following: @@ -72,7 +76,7 @@ You can also use the `--installdir` flag to install binaries in a different location. -# Invocation +## Invocation In the `crux-llvm` directory (either in the repository or the root of the directory extracted from a distribution tarball), to analyze @@ -157,7 +161,7 @@ `main`, these arguments will _not_ be passed automatically to the counterexample executables. -# API +## API The [`crucible.h` header file](c-src/includes/crucible.h) contains declarations of several functions that can be used to describe the @@ -191,7 +195,7 @@ that the conditions used in assertions are directly available and not obscured by a conditional wrapper around an error function. -# Standard C and C++ Libraries +## Standard C and C++ Libraries The code supplied to `crux-llvm` should be largely self-contained, without calls to external code. However, some standard library functions @@ -253,7 +257,7 @@ most C++ code that doesn't use third-party libraries (or that includes those libraries linked into a single bitcode file) should work. -# Command-line Flags +## Command-line Flags The most important and only required argument to `crux-llvm` is the source file or list of source files to analyze. In the case that @@ -408,7 +412,7 @@ * `--debug`: Start the Crucible debugger. -# Environment Variables +## Environment Variables The following environment variables are supported: @@ -423,7 +427,7 @@ * `LLVM_LINK`: Specify the name of the `llvm-link` command used to combine multiple LLVM bitcode files. -# Configuration Files +## Configuration Files In addition to command-line flags and environment variables, `crux-llvm` can be configured with a key-value input file. The file consists of a @@ -450,7 +454,7 @@ `llvm-link`, instructs `crux-llvm` not to create counter-example demonstration executables, and provides a list of input files. -# Symbolic I/O [Experimental] +## Symbolic I/O [Experimental] Note that Symbolic I/O is currently experimental. We expect that the API (both internal and command line) will change. @@ -534,7 +538,7 @@ sequential file descriptors. In contrast, the real program would allocate the same file descriptor to both (as only one branch would be taken). -# Test suite +## Test suite The `crux-llvm` test suite is implemented in `test/Test.hs`, and the accompanying test case data can be found under `test-data`. Each test case @@ -574,7 +578,7 @@ read anything past `SKIP_TEST`, so the rest of the file can be used to document why the test is skipped on that particular configuration. -# Acknowledgements +## Acknowledgements Crux is partly based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. N66001-18-C-4011. diff --git a/crux-llvm.cabal b/crux-llvm.cabal --- a/crux-llvm.cabal +++ b/crux-llvm.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: crux-llvm -Version: 0.9.1 +Version: 0.13 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com, langston@galois.com Copyright: (c) Galois, Inc 2014-2022 @@ -55,7 +55,7 @@ -Wincomplete-uni-patterns ghc-prof-options: -O2 default-language: Haskell2010 - build-depends: base >= 4.8 && < 4.20 + build-depends: base >= 4.8 && < 4.22 , bytestring , containers , crucible @@ -64,11 +64,105 @@ , crux , directory , filepath - , lens + , microlens , process , text , what4 +common warns + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 9.6 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=deriving-typeable + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=gadt-mono-local-binds + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=orphans + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=type-defaults + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unused-do-bind + -Werror=unused-imports + -Werror=unused-record-wildcards + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=deprecated-type-abstractions + -Werror=incomplete-record-selectors + + if impl(ghc < 9.12) + ghc-options: + -Werror=compat-unqualified-imports + common testdefs build-depends: tasty >= 0.10 , tasty-hunit >= 0.10 @@ -95,9 +189,11 @@ aeson, bv-sized, config-schema >= 1.2.2.0, + crucible-debug, logict, llvm-pretty, - llvm-pretty-bc-parser, + llvm-pretty-bc-parser >= 0.5, + microlens-mtl, mtl, parameterized-utils, prettyprinter >= 1.7.0 @@ -131,6 +227,7 @@ aeson, crux-llvm, lumberjack, + microlens-th, websockets >= 0.12 main-is: Main.hs @@ -174,6 +271,7 @@ test-suite crux-llvm-test import: bldflags, testdefs + import: warns type: exitcode-stdio-1.0 hs-source-dirs: test diff --git a/for-ide/Main.hs b/for-ide/Main.hs --- a/for-ide/Main.hs +++ b/for-ide/Main.hs @@ -4,7 +4,6 @@ module Main (main) where -import Control.Lens (makeLenses, set, view) import Crux (OutputConfig) import qualified Crux import Crux.Config.Common (OutputOptions) @@ -16,6 +15,9 @@ ) import qualified Data.Aeson as JSON import Data.Text as Text (Text, unpack) +import Lens.Micro (set) +import Lens.Micro.Extras (view) +import Lens.Micro.TH (makeLenses) import qualified Lumberjack as LJ import qualified Network.WebSockets as WS import Paths_crux_llvm (version) diff --git a/src/Crux/LLVM/Compile.hs b/src/Crux/LLVM/Compile.hs --- a/src/Crux/LLVM/Compile.hs +++ b/src/Crux/LLVM/Compile.hs @@ -35,7 +35,7 @@ import Crux import qualified Crux.Config.Common as CC -import Crux.Model ( toDouble, showBVLiteral, showFloatLiteral +import Crux.Model ( toDouble, showBVLiteralSigned, showFloatLiteral , showDoubleLiteral ) import Crux.Types @@ -325,7 +325,7 @@ ppValsC ty (Vals xs) = let (cty, cnm, ppRawVal) = case ty of BaseBVRepr n -> - ("int" ++ show n ++ "_t", "int" ++ show n ++ "_t", showBVLiteral n) + ("int" ++ show n ++ "_t", "int" ++ show n ++ "_t", showBVLiteralSigned n) BaseFloatRepr (FloatingPointPrecisionRepr eb sb) | Just Refl <- testEquality eb (knownNat @8) , Just Refl <- testEquality sb (knownNat @24) diff --git a/src/Crux/LLVM/Config.hs b/src/Crux/LLVM/Config.hs --- a/src/Crux/LLVM/Config.hs +++ b/src/Crux/LLVM/Config.hs @@ -9,6 +9,7 @@ import Control.Exception ( Exception, displayException, throwIO ) import Control.Monad ( guard ) import Control.Monad.State ( liftIO, MonadIO ) +import Data.List (intercalate) import qualified Data.Text as Text import System.Directory ( doesDirectoryExist ) import System.Environment ( getExecutablePath ) @@ -46,7 +47,7 @@ ppCError err = case err of NoFiles -> "crux-llvm requires at least one input file." EnvError msg -> msg - BadFun fnName isMain -> unlines $ + BadFun fnName isMain -> ofLines $ [ "The '" ++ fnName ++ "' function should have no arguments"] ++ [ "Enable `supply-main-arguments` to relax this restriction" | isMain @@ -54,14 +55,16 @@ MissingFun x -> "Cannot find code for " ++ show x LLVMParseError e -> LLVM.formatError e ClangError n sout serr -> - unlines $ [ "`clang` compilation failed." + ofLines $ [ "`clang` compilation failed." , "*** Exit code: " ++ show n , "*** Standard out:" ] ++ [ " " ++ l | l <- lines sout ] ++ [ "*** Standard error:" ] ++ [ " " ++ l | l <- lines serr ] - + where + -- Contrast with `Prelude.unlines`, which appends a trailing newline + ofLines = intercalate "\n" throwCError :: MonadIO m => CError -> m b throwCError e = liftIO (throwIO e) diff --git a/src/Crux/LLVM/Simulate.hs b/src/Crux/LLVM/Simulate.hs --- a/src/Crux/LLVM/Simulate.hs +++ b/src/Crux/LLVM/Simulate.hs @@ -1,31 +1,38 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeSynonymInstances #-} module Crux.LLVM.Simulate where import Control.Monad (unless) -import Data.String (fromString) -import qualified Data.Map.Strict as Map +import Control.Monad.IO.Class (liftIO) import Data.IORef import qualified Data.List as List +import qualified Data.Map.Strict as Map import Data.Maybe ( fromMaybe ) import qualified Data.Parameterized.Map as MapF import Data.Sequence (Seq) +import Data.String (fromString) import qualified Data.Traversable as T -import Control.Lens ((&), (%~), (%=), (^.), use, view) -import Control.Monad.IO.Class (liftIO) import Data.Text as Text (Text, pack) +import Data.Void (Void) import GHC.Exts ( proxy# ) +import qualified Lens.Micro as Lens +import Lens.Micro ((&), (%~), (^.)) +import Lens.Micro.Extras (view) +import Lens.Micro.Mtl ((%=), use) import System.IO (stdout) @@ -58,6 +65,8 @@ import Lang.Crucible.Simulator.GlobalState ( insertGlobal, lookupGlobal ) import Lang.Crucible.Simulator.Profiling ( Metric(Metric) ) +-- crucible-debug +import qualified Lang.Crucible.Debug as Debug -- crucible-llvm import Lang.Crucible.LLVM(llvmExtensionImpl, llvmGlobals, registerLazyModule ) @@ -100,6 +109,14 @@ import qualified Crux.LLVM.Log as Log import Crux.LLVM.Overrides +-- | Crux LLVM personality +newtype CruxLLVM sym + = CruxLLVM { getCruxLLVM :: Debug.Context Void sym LLVM UnitType } + +instance Debug.HasContext (CruxLLVM sym) Void sym LLVM UnitType where + context = Lens.lens getCruxLLVM (const CruxLLVM) + {-# INLINE context #-} + -- | Create a simulator context for the given architecture. setupSimCtxt :: (IsSymBackend sym bak, HasLLVMAnn sym) => @@ -107,16 +124,27 @@ bak -> MemOptions -> GlobalVar Mem -> - SimCtxt Crux sym LLVM -setupSimCtxt halloc bak mo memVar = - initSimContext bak - (MapF.union llvmIntrinsicTypes llvmSymIOIntrinsicTypes) - halloc - stdout - (fnBindingsFromList []) - (llvmExtensionImpl mo) - CruxPersonality - & profilingMetrics %~ Map.union (memMetrics memVar) + IO (SimCtxt CruxLLVM sym LLVM) +setupSimCtxt halloc bak mo memVar = do + -- TODO(#1576): Use LLVM debugger extensions (crucible-llvm-debug) + let cExts = Debug.voidExts + inps <- Debug.defaultDebuggerInputs cExts + dbgCtx <- + Debug.initCtx + cExts + (Debug.IntrinsicPrinters MapF.empty) + inps + Debug.defaultDebuggerOutputs + UnitRepr + pure $ + initSimContext bak + (MapF.union llvmIntrinsicTypes llvmSymIOIntrinsicTypes) + halloc + stdout + (fnBindingsFromList []) + (llvmExtensionImpl mo) + (CruxLLVM dbgCtx) + & profilingMetrics %~ Map.union (memMetrics memVar) -- | Parse an LLVM bit-code file. parseLLVM :: @@ -140,7 +168,7 @@ LLVM.Module -> ModuleTranslation arch -> Maybe (LLVMFileSystem ptrW) -> - OverM Crux sym LLVM () + OverM CruxLLVM sym LLVM () registerFunctions llvmOpts llvm_module mtrans fs0 = do let llvm_ctx = mtrans ^. transContext let ?lc = llvm_ctx ^. llvmTypeCtx @@ -165,9 +193,9 @@ -- | Path to the LLVM module FilePath -> LLVMOptions -> - Crux.SimulatorCallbacks msgs Crux.Types.CruxSimulationResult + Crux.SimulatorCallbacks msgs st Crux.Types.CruxSimulationResult simulateLLVMFile llvm_file llvmOpts = - Crux.SimulatorCallbacks $ + Crux.SimulatorCallbacks $ \fm -> do bbMapRef <- newIORef (Map.empty :: LLVMAnnMap sym) let ?recordLLVMAnnotation = \callStack an bb -> @@ -179,7 +207,7 @@ do halloc <- newHandleAllocator setupFileSim halloc llvm_file llvmOpts bak maybeOnline , Crux.onErrorHook = - \bak -> return (explainFailure (backendGetSym bak) bbMapRef) + \bak -> return (explainFailure (backendGetSym bak) fm bbMapRef) , Crux.resultHook = \_sym result -> return result } @@ -199,8 +227,8 @@ do let sym = backendGetSym bak memVar <- mkMemVar "crux:llvm_memory" halloc - let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar) - { printHandle = view outputHandle ?outputConfig } + simctx_ <- setupSimCtxt halloc bak (memOpts llvmOpts) memVar + let simctx = simctx_ { printHandle = view outputHandle ?outputConfig } prepped <- prepLLVMModule llvmOpts halloc bak llvm_file memVar @@ -306,7 +334,7 @@ , Just Refl <- testEquality w (knownNat @32) -> checkMainWithArguments anyCfg - _ -> throwCError (BadFun nm isMain) -- TODO(lb): Suggest uc-crux-llvm? + _ -> throwCError (BadFun nm isMain) Nothing -> throwCError (MissingFun nm) where @@ -398,13 +426,14 @@ detailLimit = 10 explainFailure :: IsSymInterface sym - => sym ~ WEB.ExprBuilder t st fs + => sym ~ WEB.ExprBuilder t st (WEB.Flags fm) => sym + -> WEB.FloatModeRepr fm -> IORef (LLVMAnnMap sym) -> Crux.Explainer sym t ann -explainFailure sym bbMapRef evalFn gl = +explainFailure sym fm bbMapRef evalFn gl = do bb <- readIORef bbMapRef - ex <- explainCex sym bb evalFn >>= \f -> f (gl ^. labeledPred) + ex <- explainCex sym fm bb evalFn >>= \f -> f (gl ^. labeledPred) let details = case ex of NoExplanation -> mempty diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -3,10 +3,9 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} -module Main where +module Main (main) where import Control.Exception ( SomeException, catches, try, Handler(..), IOException ) -import Control.Lens ( (^?), _Right ) import Control.Monad ( unless, when ) import Data.Bifunctor ( first ) import qualified Data.ByteString.Lazy as BSIO @@ -15,8 +14,10 @@ import Data.List.Extra ( isInfixOf ) import Data.Maybe ( catMaybes, fromMaybe ) import qualified Data.Text as T +import qualified Data.Version as Version import Data.Versions ( Versioning, versioning, prettyV, major ) import qualified GHC.IO.Exception as GE +import Lens.Micro ((^?), _Right) import Numeric.Natural import System.Environment ( withArgs, lookupEnv ) import System.Exit ( ExitCode(..) ) @@ -52,6 +53,9 @@ , "pre-clang14" , "pre-clang15" , "pre-clang16" + , "pre-clang18" + , "pre-clang19" + , "pre-clang20" ]) ] , TS.associatedNames = [ ("config", "config") @@ -408,13 +412,18 @@ Info.arch /= "x86_64" && TS.rootBaseName sweet == "T972-fail" + -- T816 has different output on GHC 9.10.1, see #1377. + let skipGhc910T816 = + Info.compilerVersion == Version.makeVersion [9, 10] && + TS.rootBaseName sweet == "T816" + -- If a .good file begins with SKIP_TEST, skip that test entirely. For test -- cases that require a minimum Clang version, this technique is used to -- prevent running the test on older Clang versions. skipTest <- ("SKIP_TEST" `BSIO.isPrefixOf`) <$> BSIO.readFile (TS.expectedFile expct) - if or [ skipTest, skipX86_64Tests, testLevel == "0" && longTests ] + if or [ skipTest, skipX86_64Tests, skipGhc910T816, testLevel == "0" && longTests ] then do when (testLevel == "0" && longTests) $ putStrLn "*** Longer running test skipped; set CI_TEST_LEVEL=1 env var to enable"