copilot-verifier 4.2 → 4.3

raw patch · 9 files changed

+273/−74 lines, 9 filesdep +copilot-librariesdep ~copilotdep ~copilot-c99dep ~copilot-corePVP ok

version bump matches the API change (PVP)

Dependencies added: copilot-libraries

Dependency ranges changed: copilot, copilot-c99, copilot-core, copilot-language, copilot-prettyprinter, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +5/−0
• README.md +7/−0
• copilot-verifier.cabal +11/−7
• examples/Copilot/Verifier/Examples.hs +2/−0
• examples/Copilot/Verifier/Examples/ShouldPass/FPNegation.hs +62/−0
• src/Copilot/Verifier.hs +104/−66
• src/Copilot/Verifier/FloatMode.hs +56/−0
• src/Copilot/Verifier/Log.hs +1/−1
• src/Copilot/Verifier/Solver.hs +25/−0

@@ -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)

@@ -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:  ```

@@ -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

@@ -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)

@@ -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'

@@ -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 @@     -- * @<solver>@ 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

@@ -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

@@ -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 

@@ -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