Merge pull request #80 from Copilot-Language/T78-configure-smt-solver

Add `smtSolver` option to `VerifierOptions`. Refs #78.

Author: RyanGlScott

README.md

@@ -38,6 +38,13 @@ prerequisites:
 * 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:
 
 ```

copilot-verifier/CHANGELOG

@@ -1,3 +1,6 @@
+2025-01-31
+        * Add `smtSolver` option to `VerifierOptions`. (#78)
+
 2025-01-20
         * Version bump (4.2). (#76)
         * Reject specs that use multiple triggers with the same name. (#74)

copilot-verifier/copilot-verifier.cabal

@@ -71,6 +71,7 @@ library
   exposed-modules:
     Copilot.Verifier
     Copilot.Verifier.Log
+    Copilot.Verifier.Solver
 
 library copilot-verifier-examples
   import: bldflags

copilot-verifier/src/Copilot/Verifier.hs

@@ -50,6 +50,7 @@ import qualified Copilot.Core.Type as CT
 import qualified Copilot.Theorem.What4 as CW4
 
 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)
@@ -160,7 +161,6 @@ import What4.InterpretedFloatingPoint
   )
 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 +202,8 @@ data VerifierOptions = VerifierOptions
     -- * @<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.
   } deriving stock Show
 
 -- | The default 'VerifierOptions':
@@ -212,11 +214,14 @@ data VerifierOptions = VerifierOptions
 -- * Do not assume any side conditions related to partial operations.
 --
 -- * Do not log any SMT solver interactions.
+--
+-- * Use the Z3 SMT solver.
 defaultVerifierOptions :: VerifierOptions
 defaultVerifierOptions = VerifierOptions
   { verbosity = Default
   , assumePartialSideConds = False
   , logSmtInteractions = False
+  , smtSolver = Solver.Z3
   }
 
 -- | Like 'defaultVerifierOptions', except that the verifier will assume side
@@ -332,7 +337,8 @@ verifyBitcode ::
 verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile =
   do -- Set up the expression builder and symbolic backend
      halloc <- newHandleAllocator
-     sym <- newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator
+     (sym :: ExprBuilder t st fs) <-
+       newExprBuilder FloatUninterpretedRepr CopilotVerifierData globalNonceGenerator
      bak <- newSimpleBackend sym
      -- turn on hash-consing
      startCaching sym
@@ -341,9 +347,10 @@ verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile =
      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
@@ -386,13 +393,13 @@ verifyBitcode opts csettings properties spec cruxOpts llvmOpts cFile bcFile =
           -- segment of the associated Copilot streams.
           let cruxOptsInit = setCruxOfflineSolverOutput "initial-step" cruxOpts
           initGoals <-
-            verifyInitialState cruxOptsInit adapters clRefs simctx initialMem
+            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
+            verifyStepBisimulation opts cruxOptsTrans [adapter] csettings
               clRefs simctx llvmMod trans memVar initialMem proofStateBundle
 
           Log.sayCopilot $ Log.SuccessfulProofSummary cFile initGoals bisimGoals

copilot-verifier/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