diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,8 @@ +2025-03-10 + * Version bump (4.3). (#82) + * Add `smtSolver` option to `VerifierOptions`. (#78) + * Add `smtFloatMode` option to `VerifierOptions`. (#79) + 2025-01-20 * Version bump (4.2). (#76) * Reject specs that use multiple triggers with the same name. (#74) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -38,6 +38,13 @@ * Ensure that you have the `z3` SMT solver in your `PATH`. `z3` binaries are available at https://github.com/Z3Prover/z3/releases. + Alternatively, the verifier can be configured to use one of the following + SMT solvers instead: + + * `cvc4`: https://cvc4.github.io/downloads.html + * `cvc5`: https://github.com/cvc5/cvc5/releases/ + * `yices`: https://yices.csl.sri.com + Then, clone the repo and run: ``` diff --git a/copilot-verifier.cabal b/copilot-verifier.cabal --- a/copilot-verifier.cabal +++ b/copilot-verifier.cabal @@ -1,6 +1,6 @@ Cabal-version: 2.2 Name: copilot-verifier -Version: 4.2 +Version: 4.3 Author: Galois Inc. Maintainer: rscott@galois.com Copyright: (c) Galois, Inc 2021-2024 @@ -45,9 +45,9 @@ bv-sized >= 1.0.0 && < 1.1, bytestring, containers >= 0.5.9.0, - copilot-c99 >= 4.2 && < 4.3, - copilot-core >= 4.2 && < 4.3, - copilot-theorem >= 4.2 && < 4.3, + copilot-c99 >= 4.3 && < 4.4, + copilot-core >= 4.3 && < 4.4, + copilot-theorem >= 4.3 && < 4.4, crucible >= 0.7.1 && < 0.8, crucible-llvm >= 0.7 && < 0.8, crux >= 0.7.1 && < 0.8, @@ -70,7 +70,9 @@ hs-source-dirs: src exposed-modules: Copilot.Verifier + Copilot.Verifier.FloatMode Copilot.Verifier.Log + Copilot.Verifier.Solver library copilot-verifier-examples import: bldflags @@ -78,9 +80,10 @@ hs-source-dirs: examples build-depends: case-insensitive, - copilot >= 4.2 && < 4.3, - copilot-language >= 4.2 && < 4.3, - copilot-prettyprinter >= 4.2 && < 4.3, + copilot >= 4.3 && < 4.4, + copilot-language >= 4.3 && < 4.4, + copilot-libraries >= 4.3 && < 4.4, + copilot-prettyprinter >= 4.3 && < 4.4, copilot-verifier exposed-modules: Copilot.Verifier.Examples @@ -103,6 +106,7 @@ Copilot.Verifier.Examples.ShouldPass.Clock Copilot.Verifier.Examples.ShouldPass.Counter Copilot.Verifier.Examples.ShouldPass.Engine + Copilot.Verifier.Examples.ShouldPass.FPNegation Copilot.Verifier.Examples.ShouldPass.FPOps Copilot.Verifier.Examples.ShouldPass.Heater Copilot.Verifier.Examples.ShouldPass.IntOps diff --git a/examples/Copilot/Verifier/Examples.hs b/examples/Copilot/Verifier/Examples.hs --- a/examples/Copilot/Verifier/Examples.hs +++ b/examples/Copilot/Verifier/Examples.hs @@ -28,6 +28,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Clock as Clock import qualified Copilot.Verifier.Examples.ShouldPass.Counter as Counter import qualified Copilot.Verifier.Examples.ShouldPass.Engine as Engine +import qualified Copilot.Verifier.Examples.ShouldPass.FPNegation as FPNegation import qualified Copilot.Verifier.Examples.ShouldPass.FPOps as FPOps import qualified Copilot.Verifier.Examples.ShouldPass.Heater as Heater import qualified Copilot.Verifier.Examples.ShouldPass.IntOps as IntOps @@ -70,6 +71,7 @@ , example "Clock" (Clock.verifySpec verb) , example "Counter" (Counter.verifySpec verb) , example "Engine" (Engine.verifySpec verb) + , example "FPNegation" (FPNegation.verifySpec verb) , example "FPOps" (FPOps.verifySpec verb) , example "Heater" (Heater.verifySpec verb) , example "IntOps" (IntOps.verifySpec verb) diff --git a/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs b/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs new file mode 100644 --- /dev/null +++ b/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs @@ -0,0 +1,62 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +-- | This will not succeed when 'smtFloatMode' is 'FloatUninterpreted', as Clang +-- will turn @input /= 30.0@ below into a more complicated expression that also +-- checks if @30.0@ is NaN or not. This is logically equivalent to the original +-- specification, but an SMT solver cannot conclude this when all of the +-- floating-point operations involved are treated as uninterpreted functions. +-- +-- To make this work, we set 'smtFloatMode' to 'FloatIEEE' instead. This works +-- because all of the floating-point operations in the specification below are +-- native to SMT-LIB. +module Copilot.Verifier.Examples.ShouldPass.FPNegation where + +import Copilot.Compile.C99 (mkDefaultCSettings) +import Copilot.Verifier ( Verbosity, VerifierOptions(..) + , defaultVerifierOptions, verifyWithOptions ) +import Copilot.Verifier.FloatMode (FloatMode(..)) +import qualified Copilot.Library.PTLTL as PTLTL +import Language.Copilot + +input :: Stream Float +input = extern "input" Nothing + +-- | MyProperty +-- @ +-- Input is never 30.0 +-- @ +propMyProperty :: Stream Bool +propMyProperty = PTLTL.alwaysBeen (input /= 30.0) + +-- | Clock that increases in one-unit steps. +clock :: Stream Int64 +clock = [0] ++ (clock + 1) + +-- | First Time Point +ftp :: Stream Bool +ftp = [True] ++ false + +pre :: Stream Bool -> Stream Bool +pre = ([False] ++) + +tpre :: Stream Bool -> Stream Bool +tpre = ([True] ++) + +notPreviousNot :: Stream Bool -> Stream Bool +notPreviousNot = not . PTLTL.previous . not + +-- | Complete specification. Calls C handler functions when properties are +-- violated. +spec :: Spec +spec = do + trigger "handlerMyProperty" (not propMyProperty) [] + +verifySpec :: Verbosity -> IO () +verifySpec verb = do + spec' <- reify spec + verifyWithOptions + (defaultVerifierOptions + { verbosity = verb + , smtFloatMode = FloatIEEE + }) + mkDefaultCSettings [] "fpNegation" spec' diff --git a/src/Copilot/Verifier.hs b/src/Copilot/Verifier.hs --- a/src/Copilot/Verifier.hs +++ b/src/Copilot/Verifier.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-} @@ -49,7 +50,9 @@ import qualified Copilot.Theorem.What4 as CW4 +import qualified Copilot.Verifier.FloatMode as FloatMode import qualified Copilot.Verifier.Log as Log +import qualified Copilot.Verifier.Solver as Solver import Data.Parameterized.Ctx (EmptyCtx) import Data.Parameterized.Context (pattern Empty) @@ -72,10 +75,10 @@ , labeledPred, labeledPredMsg -- , ProofObligations, proofGoal, goalsToList, labeledPredMsg ) -import Lang.Crucible.Backend.Simple (newSimpleBackend) +import Lang.Crucible.Backend.Simple (SimpleBackend, newSimpleBackend) import Lang.Crucible.CFG.Core (AnyCFG(..), cfgArgTypes, cfgReturnType) import Lang.Crucible.CFG.Common ( freshGlobalVar ) -import Lang.Crucible.FunctionHandle (newHandleAllocator) +import Lang.Crucible.FunctionHandle (HandleAllocator, newHandleAllocator) import Lang.Crucible.Simulator ( SimContext(..), ctxSymInterface, ExecResult(..), ExecState(..) , defaultAbortHandler, runOverrideSim, partialValue, gpValue @@ -150,7 +153,7 @@ , getAnnotation, natAdd, natEq, natIte, natLit ) import What4.Expr.Builder - ( FloatModeRepr(..), ExprBuilder, BoolExpr, startCaching + ( Flags, ExprBuilder, BoolExpr, startCaching , newExprBuilder ) import What4.FunctionName (functionName) @@ -160,7 +163,6 @@ ) import What4.ProgramLoc (ProgramLoc, mkProgramLoc, plFunction, Position(..)) import What4.Solver.Adapter (SolverAdapter(..)) -import What4.Solver.Z3 (z3Adapter) import What4.Symbol (safeSymbol) -- | @'verify' csettings props prefix spec@ verifies the Copilot specification @@ -202,6 +204,22 @@ -- * @@ is the name of the SMT solver used to discharge the proof -- goal. Currently, this will always be @z3@, although we might make this -- configurable in the future. + , smtSolver :: Solver.Solver + -- ^ Which SMT solver to use when solving proof goals. + , smtFloatMode :: FloatMode.FloatMode + -- ^ How the verifier should interpret floating-point operations when + -- translating them to SMT. + -- + -- By default, the verifier will treat all floating-point operations as + -- uninterpreted functions ('FloatMode.FloatUninterpreted'). This allows the + -- verifier to perform some limited reasoning about floating-point + -- operations that SMT solvers do not have built-in operations for (@sin@, + -- @cos@, @tan@, etc.), but at the expense of not being able to verify C + -- code in which the compiler optimizes floating-point expressions. One can + -- also opt into an alternative mode where floating-point values are treated + -- as IEEE-754 floats ('FloatMode.FloatIEEE'), but this comes with the + -- drawback that the verifier will not be able to perform /any/ reasoning + -- about @sin@, @cos@, @tan@, etc. } deriving stock Show -- | The default 'VerifierOptions': @@ -212,11 +230,18 @@ -- * Do not assume any side conditions related to partial operations. -- -- * Do not log any SMT solver interactions. +-- +-- * Use the Z3 SMT solver. +-- +-- * Treat all floating-point operations as uninterpreted functions when +-- translating to SMT. defaultVerifierOptions :: VerifierOptions defaultVerifierOptions = VerifierOptions { verbosity = Default , assumePartialSideConds = False , logSmtInteractions = False + , smtSolver = Solver.Z3 + , smtFloatMode = FloatMode.FloatUninterpreted } -- | Like 'defaultVerifierOptions', except that the verifier will assume side @@ -330,84 +355,97 @@ FilePath {- ^ Path to the bitcode file to verify -} -> IO () verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile = + FloatMode.withFloatMode (smtFloatMode opts) $ \fm -> do -- Set up the expression builder and symbolic backend halloc <- newHandleAllocator - sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator + sym <- newExprBuilder fm CopilotVerifierData globalNonceGenerator bak <- newSimpleBackend sym -- turn on hash-consing startCaching sym - -- capture LLVM side-condition information for use in error reporting - clRefs <- newCopilotLogRefs - let ?recordLLVMAnnotation = recordLLVMAnnotation clRefs + FloatMode.withInterpretedFloatExprBuilder sym fm $ + verifyWithSymBackend bak halloc + where + verifyWithSymBackend :: + forall t st fm. + IsInterpretedFloatExprBuilder (ExprBuilder t st (Flags fm)) => + SimpleBackend t st (Flags fm) -> + HandleAllocator -> + IO () + verifyWithSymBackend bak halloc = do + let sym = backendGetSym bak + -- capture LLVM side-condition information for use in error reporting + clRefs <- newCopilotLogRefs + let ?recordLLVMAnnotation = recordLLVMAnnotation clRefs - -- Set up the solver to use for verification. Right now we hard-code this to Z3. - let adapters = [z3Adapter] -- TODO? configurable - extendConfig (solver_adapter_config_options z3Adapter) (getConfiguration sym) + -- Set up the solver to use for verification. + let adapter :: SolverAdapter st + adapter = Solver.solverAdapter (smtSolver opts) + extendConfig (solver_adapter_config_options adapter) (getConfiguration sym) - -- Set up the Crucible/LLVM simulation context - memVar <- mkMemVar "llvm_memory" halloc - let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar) - { printHandle = view Log.outputHandle ?outputConfig } + -- Set up the Crucible/LLVM simulation context + memVar <- mkMemVar "llvm_memory" halloc + let simctx = (setupSimCtxt halloc bak (memOpts llvmOpts) memVar) + { printHandle = view Log.outputHandle ?outputConfig } - -- Load and translate the input LLVM module - llvmMod <- parseLLVM bcFile - Some trans <- - let ?transOpts = transOpts llvmOpts - in translateModule halloc memVar llvmMod + -- Load and translate the input LLVM module + llvmMod <- parseLLVM bcFile + Some trans <- + let ?transOpts = transOpts llvmOpts + in translateModule halloc memVar llvmMod - Log.sayCopilot Log.TranslatedToCrucible + Log.sayCopilot Log.TranslatedToCrucible - -- Grab some metadata from the bitcode file and options; - -- make the available via implicit arguments to the places - -- that expect them. - let llvmCtxt = trans ^. transContext - let ?lc = llvmCtxt ^. llvmTypeCtx - let ?memOpts = memOpts llvmOpts - let ?intrinsicsOpts = intrinsicsOpts llvmOpts + -- Grab some metadata from the bitcode file and options; + -- make the available via implicit arguments to the places + -- that expect them. + let llvmCtxt = trans ^. transContext + let ?lc = llvmCtxt ^. llvmTypeCtx + let ?memOpts = memOpts llvmOpts + let ?intrinsicsOpts = intrinsicsOpts llvmOpts - llvmPtrWidth llvmCtxt $ \ptrW -> - withPtrWidth ptrW $ + llvmPtrWidth llvmCtxt $ \ptrW -> + withPtrWidth ptrW $ - do -- Compute the LLVM memory state with global variables allocated - -- but not initialized - emptyMem <- initializeAllMemory bak llvmCtxt llvmMod + do -- Compute the LLVM memory state with global variables allocated + -- but not initialized + emptyMem <- initializeAllMemory bak llvmCtxt llvmMod - -- Compute the LLVM memory state with global variables initialized - -- to their initial values. - initialMem <- populateAllGlobals bak (trans ^. globalInitMap) emptyMem + -- Compute the LLVM memory state with global variables initialized + -- to their initial values. + initialMem <- populateAllGlobals bak (trans ^. globalInitMap) emptyMem - -- Use the Copilot spec directly to compute the symbolic states - -- necessary to carry out the states of the bisimulation proof. - Log.sayCopilot Log.GeneratingProofState - proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec + -- Use the Copilot spec directly to compute the symbolic states + -- necessary to carry out the states of the bisimulation proof. + Log.sayCopilot Log.GeneratingProofState + proofStateBundle <- CW4.computeBisimulationProofBundle sym properties spec - -- First check that the initial state of the program matches the starting - -- segment of the associated Copilot streams. - let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts - initGoals <- - verifyInitialState cruxOptsInit adapters clRefs simctx initialMem - (CW4.initialStreamState proofStateBundle) + -- First check that the initial state of the program matches the starting + -- segment of the associated Copilot streams. + let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts + initGoals <- + verifyInitialState cruxOptsInit [adapter] clRefs simctx initialMem + (CW4.initialStreamState proofStateBundle) - -- Now, the real meat. Carry out the bisimulation step of the proof. - let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts - bisimGoals <- - verifyStepBisimulation opts cruxOptsTrans adapters csettings - clRefs simctx llvmMod trans memVar initialMem proofStateBundle + -- Now, the real meat. Carry out the bisimulation step of the proof. + let cruxOptsTrans = setCruxOfflineSolverOutput "transition-step" cruxOpts + bisimGoals <- + verifyStepBisimulation opts cruxOptsTrans [adapter] csettings + clRefs simctx llvmMod trans memVar initialMem proofStateBundle - Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals bisimGoals - -- We only want to inform users about Noisy if the verbosity level is - -- sufficiently low. Crux's logging framework isn't particularly - -- suited to doing this, as it assumes that all log messages enabled - -- for low verbosity levels should also be enabled for higher - -- verbosity levels. That is a reasonable assumption most of the time, - -- but not here. - -- - -- To compensate, we hack around the issue by manually checking the - -- verbosity level before logging the message. - when (verbosity opts < Noisy) $ - Log.sayCopilot Log.NoisyVerbositySuggestion - where + Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals bisimGoals + -- We only want to inform users about Noisy if the verbosity level is + -- sufficiently low. Crux's logging framework isn't particularly + -- suited to doing this, as it assumes that all log messages enabled + -- for low verbosity levels should also be enabled for higher + -- verbosity levels. That is a reasonable assumption most of the time, + -- but not here. + -- + -- To compensate, we hack around the issue by manually checking the + -- verbosity level before logging the message. + when (verbosity opts < Noisy) $ + Log.sayCopilot Log.NoisyVerbositySuggestion + -- If @logSmtInteractions@ is enabled, enable offline solver output in the -- supplied 'CruxOptions' with the supplied file template. Otherwise, return -- the supplied 'CruxOptions' unaltered. @@ -976,7 +1014,7 @@ loop (CW4.XFloat x) (FloatRepr SingleFloatRepr) = return x loop (CW4.XDouble x) (FloatRepr DoubleFloatRepr) = return x - loop CW4.XEmptyArray (VectorRepr _tpr) = + loop (CW4.XEmptyArray _ctp) (VectorRepr _tpr) = pure V.empty loop (CW4.XArray xs) (VectorRepr tpr) = V.generateM (PVec.lengthInt xs) (\i -> loop (PVec.elemAtUnsafe i xs) tpr) @@ -1037,7 +1075,7 @@ loop Float (CW4.XFloat x) (FloatRepr SingleFloatRepr) v = iFloatEq @_ @SingleFloat sym x v loop Double (CW4.XDouble x) (FloatRepr DoubleFloatRepr) v = iFloatEq @_ @DoubleFloat sym x v - loop (Array _ctp) CW4.XEmptyArray (VectorRepr _tpr) vs = + loop (Array _ctp) (CW4.XEmptyArray _ctp2) (VectorRepr _tpr) vs = pure $ backendPred sym $ V.null vs loop (Array ctp) (CW4.XArray xs) (VectorRepr tpr) vs | PVec.lengthInt xs == V.length vs diff --git a/src/Copilot/Verifier/FloatMode.hs b/src/Copilot/Verifier/FloatMode.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Verifier/FloatMode.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} + +module Copilot.Verifier.FloatMode + ( FloatMode(..) + , withFloatMode + , withInterpretedFloatExprBuilder + ) where + +import qualified What4.Expr.Builder as W4 +import qualified What4.InterpretedFloatingPoint as W4 + +-- | How the verifier should interpret floating-point operations. +data FloatMode + = -- | Floating-point values are treated as bitvectors of the appropriate + -- width, and all operations on them are translated as uninterpreted + -- functions. This is the verifier's default interpretation, and it is what + -- allows the verifier to perform any reasoning at all over floating-point + -- operations that are not native to SMT-LIB (@sin@, @cos@, @tan@, etc.). + FloatUninterpreted + + | -- | Floating-point values are treated as bit-precise IEEE-754 floats. This + -- interpretation can perform deeper reasoning about floating-point + -- operations that are native to SMT-LIB, but at the expense of causing the + -- verifier to throw an error if it encounters operations that are not + -- native to SMT-LIB (@sin@, @cos@, @tan@, etc.). Use at your own risk. + FloatIEEE + deriving Show + +-- | Convert a 'FloatMode' into a What4 'W4.FloatModeRepr' and pass it to a +-- continuation. +withFloatMode :: + FloatMode -> + (forall fm. W4.FloatModeRepr fm -> r) -> + r +withFloatMode fm k = + case fm of + FloatUninterpreted -> + k W4.FloatUninterpretedRepr + FloatIEEE -> + k W4.FloatIEEERepr + +-- | Match on a 'W4.FloatModeRepr', compute evidence that it gives rise to an +-- instance of 'W4.IsInterpretedFloatExprBuilder', and pass the evidence to a +-- continutation. +withInterpretedFloatExprBuilder :: + W4.ExprBuilder t st (W4.Flags fm) -> + W4.FloatModeRepr fm -> + (W4.IsInterpretedFloatExprBuilder (W4.ExprBuilder t st (W4.Flags fm)) => r) -> + r +withInterpretedFloatExprBuilder _sym fm k = + case fm of + W4.FloatUninterpretedRepr -> k + W4.FloatIEEERepr -> k + W4.FloatRealRepr -> k diff --git a/src/Copilot/Verifier/Log.hs b/src/Copilot/Verifier/Log.hs --- a/src/Copilot/Verifier/Log.hs +++ b/src/Copilot/Verifier/Log.hs @@ -799,7 +799,7 @@ CW4.XWord64 w -> WI.printSymExpr w CW4.XFloat f -> WI.printSymExpr f CW4.XDouble d -> WI.printSymExpr d - CW4.XEmptyArray -> "[]" + CW4.XEmptyArray {} -> "[]" CW4.XArray a -> ppBracesWith ppCopilotValue (PV.toList a) CW4.XStruct s -> ppBracketsWith ppCopilotValue s diff --git a/src/Copilot/Verifier/Solver.hs b/src/Copilot/Verifier/Solver.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Verifier/Solver.hs @@ -0,0 +1,25 @@ +module Copilot.Verifier.Solver + ( Solver(..) + , solverAdapter + ) where + +import qualified What4.Solver.Adapter as W4 +import qualified What4.Solver.CVC4 as W4.CVC4 +import qualified What4.Solver.CVC5 as W4.CVC5 +import qualified What4.Solver.Yices as W4.Yices +import qualified What4.Solver.Z3 as W4.Z3 + +-- | General-purpose SMT solvers that @copilot-verifier@ supports. +data Solver + = CVC4 + | CVC5 + | Yices + | Z3 + deriving Show + +-- | Return the @what4@ 'W4.SolverAdapter' corresponding to a given 'Solver'. +solverAdapter :: Solver -> W4.SolverAdapter st +solverAdapter CVC4 = W4.CVC4.cvc4Adapter +solverAdapter CVC5 = W4.CVC5.cvc5Adapter +solverAdapter Yices = W4.Yices.yicesAdapter +solverAdapter Z3 = W4.Z3.z3Adapter