From ccfde2fc639de574579db03d075e0c3eb9639921 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Feb 2025 11:08:43 -0500 Subject: [PATCH 1/2] Add smtFloatMode option to VerifierOptions. Refs #79. This allows users to switch between `FloatUninterpreted` (the default setting, where all floating-point operations are treated as uninterpreted functions) and `FloatIEEE` (where floating-point values are treated as IEEE-754 floats). While `FloatIEEE` is unable to handle floating-point operations that are not native to SMT-LIB (`sin`, `cos`, `tan`, etc.), it can handle more specifications in which a C compiler optimizes the floating-point expressions found in the generated C code. An example of where this is crucible can be found in the newly added `FPNegation` example, which was inspired by Ogma. --- copilot-verifier/copilot-verifier.cabal | 3 + .../examples/Copilot/Verifier/Examples.hs | 2 + .../Examples/ShouldPass/FPNegation.hs | 62 ++++++ copilot-verifier/src/Copilot/Verifier.hs | 183 ++++++++++-------- .../src/Copilot/Verifier/FloatMode.hs | 56 ++++++ 5 files changed, 230 insertions(+), 76 deletions(-) create mode 100644 copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs create mode 100644 copilot-verifier/src/Copilot/Verifier/FloatMode.hs diff --git a/copilot-verifier/copilot-verifier.cabal b/copilot-verifier/copilot-verifier.cabal index 9fcc64c..20ce5ca 100644 --- a/copilot-verifier/copilot-verifier.cabal +++ b/copilot-verifier/copilot-verifier.cabal @@ -70,6 +70,7 @@ library hs-source-dirs: src exposed-modules: Copilot.Verifier + Copilot.Verifier.FloatMode Copilot.Verifier.Log Copilot.Verifier.Solver @@ -81,6 +82,7 @@ library copilot-verifier-examples case-insensitive, copilot >= 4.2 && < 4.3, copilot-language >= 4.2 && < 4.3, + copilot-libraries >= 4.2 && < 4.3, copilot-prettyprinter >= 4.2 && < 4.3, copilot-verifier exposed-modules: @@ -104,6 +106,7 @@ library copilot-verifier-examples 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/copilot-verifier/examples/Copilot/Verifier/Examples.hs b/copilot-verifier/examples/Copilot/Verifier/Examples.hs index 04f84a6..7e593a7 100644 --- a/copilot-verifier/examples/Copilot/Verifier/Examples.hs +++ b/copilot-verifier/examples/Copilot/Verifier/Examples.hs @@ -28,6 +28,7 @@ import qualified Copilot.Verifier.Examples.ShouldPass.Arith a 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 @@ shouldPassExamples verb = Map.fromList , 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/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs b/copilot-verifier/examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs new file mode 100644 index 0000000..5078d07 --- /dev/null +++ b/copilot-verifier/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/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs index 676eef0..097f86c 100644 --- a/copilot-verifier/src/Copilot/Verifier.hs +++ b/copilot-verifier/src/Copilot/Verifier.hs @@ -3,6 +3,7 @@ {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ImplicitParams #-} @@ -49,6 +50,7 @@ import qualified Copilot.Core.Type as CT 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 @@ -73,10 +75,10 @@ import Lang.Crucible.Backend , 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 @@ -151,7 +153,7 @@ import What4.Interface , getAnnotation, natAdd, natEq, natIte, natLit ) import What4.Expr.Builder - ( FloatModeRepr(..), ExprBuilder, BoolExpr, startCaching + ( Flags, ExprBuilder, BoolExpr, startCaching , newExprBuilder ) import What4.FunctionName (functionName) @@ -204,6 +206,20 @@ data VerifierOptions = VerifierOptions -- 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': @@ -216,12 +232,16 @@ data VerifierOptions = VerifierOptions -- * 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 @@ -335,86 +355,97 @@ verifyBitcode :: 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 :: ExprBuilder t st fs) <- - 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 - - -- 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 } - - -- 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 - - -- 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 $ - - 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 - - -- 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 [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 [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 + 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. + 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 } + + -- 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 + + -- 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 $ + + 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 + + -- 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 [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 [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 + -- If @logSmtInteractions@ is enabled, enable offline solver output in the -- supplied 'CruxOptions' with the supplied file template. Otherwise, return -- the supplied 'CruxOptions' unaltered. diff --git a/copilot-verifier/src/Copilot/Verifier/FloatMode.hs b/copilot-verifier/src/Copilot/Verifier/FloatMode.hs new file mode 100644 index 0000000..7d2f627 --- /dev/null +++ b/copilot-verifier/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 From de7b2267cf5bfcadfaab3079f3301b83e090cad0 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 3 Feb 2025 11:41:03 -0500 Subject: [PATCH 2/2] Document changes in the CHANGELOG. Refs #79. --- copilot-verifier/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG index bc6b2bc..ab61d59 100644 --- a/copilot-verifier/CHANGELOG +++ b/copilot-verifier/CHANGELOG @@ -1,5 +1,6 @@ -2025-01-31 +2025-02-03 * Add `smtSolver` option to `VerifierOptions`. (#78) + * Add `smtFloatMode` option to `VerifierOptions`. (#79) 2025-01-20 * Version bump (4.2). (#76)