Add Bitwuzla support

.github/ci.sh

@@ -99,7 +99,12 @@ install_solvers() {
   chmod +x $BIN/*
   export PATH=$BIN:$PATH
   echo "$BIN" >> "$GITHUB_PATH"
-  is_exe "$BIN" z3 && is_exe "$BIN" cvc4 && is_exe "$BIN" yices
+  is_exe   "$BIN" z3 && \
+    is_exe "$BIN" cvc4 && \
+    is_exe "$BIN" cvc5 && \
+    is_exe "$BIN" boolector && \
+    is_exe "$BIN" bitwuzla && \
+    is_exe "$BIN" yices
 }
 
 install_system_deps() {

crucible/CHANGELOG.md

@@ -1,3 +1,7 @@
+# next -- TBA
+
+* Add support for Bitwuzla as an online SMT solver backend.
+
 # 0.7.1 -- 2024-08-30
 
 * Add support for GHC 9.8

crucible/src/Lang/Crucible/Backend/Online.hs

@@ -52,6 +52,9 @@ module Lang.Crucible.Backend.Online
     -- ** Z3
   , Z3OnlineBackend
   , withZ3OnlineBackend
+    -- ** Bitwuzla
+  , BitwuzlaOnlineBackend
+  , withBitwuzlaOnlineBackend
     -- ** Boolector
   , BoolectorOnlineBackend
   , withBoolectorOnlineBackend
@@ -92,6 +95,7 @@ import           What4.Protocol.Online
 import           What4.Protocol.SMTWriter as SMT
 import           What4.Protocol.SMTLib2 as SMT2
 import           What4.SatResult
+import qualified What4.Solver.Bitwuzla as Bitwuzla
 import qualified What4.Solver.Boolector as Boolector
 import qualified What4.Solver.CVC4 as CVC4
 import qualified What4.Solver.CVC5 as CVC5
@@ -272,6 +276,28 @@ withZ3OnlineBackend sym unsatFeat extraFeatures action =
     do liftIO $ tryExtendConfig Z3.z3Options (getConfiguration sym)
        action bak
 
+type BitwuzlaOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Bitwuzla.Bitwuzla) scope st fs
+
+-- | Do something with a Bitwuzla online backend.
+--   The backend is only valid in the continuation.
+--
+--   The Bitwuzla configuration options will be automatically
+--   installed into the backend configuration object.
+--
+--   > withBitwuzlaOnineBackend FloatRealRepr ng f'
+withBitwuzlaOnlineBackend ::
+  (MonadIO m, MonadMask m) =>
+  B.ExprBuilder scope st fs ->
+  UnsatFeatures ->
+  ProblemFeatures ->
+  (BitwuzlaOnlineBackend scope st fs -> m a) ->
+  m a
+withBitwuzlaOnlineBackend sym unsatFeat extraFeatures action =
+  let feat = (SMT2.defaultFeatures Bitwuzla.Bitwuzla .|. unsatFeaturesToProblemFeatures unsatFeat .|. extraFeatures) in
+  withOnlineBackend sym feat $ \bak -> do
+    liftIO $ tryExtendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym)
+    action bak
+
 type BoolectorOnlineBackend scope st fs = OnlineBackend (SMT2.Writer Boolector.Boolector) scope st fs
 
 -- | Do something with a Boolector online backend.

crux-llvm/CHANGELOG.md

@@ -1,3 +1,7 @@
+# next -- TBA
+
+* Add support for the Bitwuzla SMT solver in the test suite.
+
 # 0.9 -- 2024-08-30
 
 * Add support for GHC 9.8

crux-llvm/README.md

@@ -299,8 +299,8 @@ In addition, the following flags can optionally be provided:
   time-based bound.
 
 * `--solver=NAME`, `-s NAME`: Use the given SMT solver to discharge
-  proof obligations. Valid values for `NAME` are `cvc4`, `cvc5`, `yices`, and
-  `z3`.
+  proof obligations. Valid values for `NAME` are `bitwuzla`, `boolector`,
+  `cvc4`, `cvc5`, `yices`, and `z3`.
 
 * `--timeout=N`, `-t N`: Set the timeout for the first phase of analysis
   (symbolic execution) which happens before sending the main goals to an

crux-llvm/test/Test.hs

@@ -198,6 +198,16 @@ getBoolectorVersion =
       getVer (Left full) = full
   in mkVC "boolector" . getVer <$> readProcessVersion "boolector"
 
+getBitwuzlaVersion :: IO VersionCheck
+getBitwuzlaVersion =
+  let getVer (Right inp) =
+        -- example inp: "3.2.1"
+        case words inp of
+          verNum:_ -> verNum
+          [] -> "?"
+      getVer (Left full) = full
+  in mkVC "bitwuzla" . getVer <$> readProcessVersion "bitwuzla"
+
 readProcessVersion :: String -> IO (Either String String)
 readProcessVersion forTool =
   catches (Right <$> readProcess forTool [ "--version" ] "")
@@ -373,6 +383,7 @@ mkTest sweet _ expct =
       "cvc4" -> getCVC4Version
       "cvc5" -> getCVC5Version
       "boolector" -> getBoolectorVersion
+      "bitwuzla" -> getBitwuzlaVersion
       _ -> return $ VC solver $ Left "unknown-solver-for-version"
 
     -- Some tests take longer, so only run one of them in fast-test mode

crux/CHANGELOG.md

@@ -1,3 +1,7 @@
+# next -- TBA
+
+* Add support for the Bitwuzla SMT solver.
+
 # 0.7.1 -- 2024-08-30
 
 * Add support for GHC 9.8

crux/src/Crux.hs

@@ -76,6 +76,7 @@ import           What4.FunctionName (FunctionName)
 import           What4.Interface (IsExprBuilder, getConfiguration)
 import           What4.Protocol.Online (OnlineSolver)
 import qualified What4.Solver as WS
+import           What4.Solver.Bitwuzla (bitwuzlaTimeout)
 import           What4.Solver.CVC4 (cvc4Timeout)
 import           What4.Solver.CVC5 (cvc5Timeout)
 import           What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout)
@@ -364,6 +365,7 @@ withSelectedOnlineBackend cruxOpts nonceGen selectedSolver maybeExplicitFloatMod
         CCS.CVC5 -> withOnlineBackendFM WE.FloatRealRepr
         CCS.STP -> withOnlineBackendFM WE.FloatRealRepr
         CCS.Z3 -> withOnlineBackendFM WE.FloatIEEERepr
+        CCS.Bitwuzla -> withOnlineBackendFM WE.FloatIEEERepr
     fm -> fail ("Unknown floating point mode: " ++ fm ++ "; expected one of [real|ieee|uninterpreted|default]")
 
   where
@@ -415,6 +417,11 @@ withSelectedOnlineBackend' cruxOpts selectedSolver sym k =
          Just s -> symCfg sym z3Timeout (floor (s * 1000))
          Nothing -> return ()
        k bak
+     CCS.Bitwuzla -> withBitwuzlaOnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do
+       case goalTimeout cruxOpts of
+         Just s -> symCfg sym bitwuzlaTimeout (floor (s * 1000))
+         Nothing -> return ()
+       k bak
      CCS.STP -> do
        -- We don't have a timeout option for STP
        case goalTimeout cruxOpts of
@@ -556,6 +563,7 @@ withSolverAdapter solverOff k =
     CCS.SolverOnline CCS.STP -> k WS.stpAdapter
     CCS.SolverOnline CCS.Yices -> k WS.yicesAdapter
     CCS.SolverOnline CCS.Z3 -> k WS.z3Adapter
+    CCS.SolverOnline CCS.Bitwuzla -> k WS.bitwuzlaAdapter
 
 withSolverAdapters :: [CCS.SolverOffline] -> ([WS.SolverAdapter st] -> a) -> a
 withSolverAdapters solverOffs k =

crux/src/Crux/Config/Solver.hs

@@ -23,7 +23,7 @@ import qualified What4.InterpretedFloatingPoint as WIF
 
 import qualified Crux.Config.Common as CCC
 
-data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP
+data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla
   deriving (Eq, Ord, Show)
 data SolverOffline = SolverOnline SolverOnline | Boolector | DReal
   deriving (Eq, Ord, Show)
@@ -43,6 +43,7 @@ instance HasDefaultFloatRepr SolverOnline where
       STP -> k WEB.FloatRealRepr
       Yices -> k WEB.FloatRealRepr
       Z3 -> k WEB.FloatIEEERepr
+      Bitwuzla -> k WEB.FloatIEEERepr
 
 instance HasDefaultFloatRepr SolverOffline where
   withDefaultFloatRepr st s k =
@@ -124,11 +125,12 @@ asAnyOfflineSolver s = case s of
       "cvc4" -> pure (SolverOnline CVC4)
       "cvc5" -> pure (SolverOnline CVC5)
       "stp" -> pure (SolverOnline STP)
-      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, or stp)" s)
+      "bitwuzla" -> pure (SolverOnline Bitwuzla)
+      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, or bitwuzla)" s)
 
 asManyOfflineSolvers :: String -> Validated [SolverOffline]
 asManyOfflineSolvers s
-  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp"
+  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla"
   | length solvers > 1 = traverse asAnyOfflineSolver solvers
   | otherwise          = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s)
   where
@@ -143,7 +145,8 @@ asOnlineSolver s =
     "cvc5" -> pure CVC5
     "z3" -> pure Z3
     "stp" -> pure STP
-    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, or stp)" s)
+    "bitwuzla" -> pure Bitwuzla
+    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, stp, or bitwuzla)" s)
 
 -- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for
 -- symbolic execution.  This can fail if an invalid solver configuration is