Merge remote-tracking branch 'origin/master' into release

runtimeverification · Jul 30, 2024 · 03e1eb6 · 03e1eb6
2 parents c2260e7 + f66df15
commit 03e1eb6
Show file tree

Hide file tree

Showing 12 changed files with 222 additions and 214 deletions.
diff --git a/booster/library/Booster/Definition/Ceil.hs b/booster/library/Booster/Definition/Ceil.hs
@@ -18,6 +18,7 @@ import Booster.Log
 import Booster.Pattern.Bool
 import Booster.Pattern.Pretty
 import Booster.Pattern.Util (isConcrete, sortOfTerm)
+import Booster.SMT.Interface
 import Booster.Util (Flag (..))
 import Control.DeepSeq (NFData)
 import Control.Monad (foldM)
@@ -101,7 +102,8 @@ computeCeilRule ::
 computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
     | null computedAttributes.notPreservesDefinednessReasons = pure Nothing
     | otherwise = do
-        (res, _) <- runEquationT def mllvm Nothing mempty mempty $ do
+        ns <- noSolver
+        (res, _) <- runEquationT def mllvm ns mempty mempty $ do
             lhsCeils <- Set.fromList <$> computeCeil lhs
             requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
             let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList

diff --git a/booster/library/Booster/JsonRpc.hs b/booster/library/Booster/JsonRpc.hs
@@ -20,7 +20,6 @@ import Control.Applicative ((<|>))
 import Control.Concurrent (MVar, putMVar, readMVar, takeMVar)
 import Control.Exception qualified as Exception
 import Control.Monad
-import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class
 import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
 import Crypto.Hash (SHA256 (..), hashWith)
@@ -145,10 +144,10 @@ respond stateVar request =
                                     , ceilConditions = pat.ceilConditions
                                     }
 
-                        solver <- traverse (SMT.initSolver def) mSMTOptions
+                        solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
                         result <-
                             performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat
-                        whenJust solver SMT.finaliseSolver
+                        SMT.finaliseSolver solver
                         stop <- liftIO $ getTime Monotonic
                         let duration =
                                 if fromMaybe False req.logTiming
@@ -228,7 +227,7 @@ respond stateVar request =
                         | otherwise =
                             Nothing
 
-                solver <- traverse (SMT.initSolver def) mSMTOptions
+                solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
 
                 result <- case internalised of
                     Left patternErrors -> do
@@ -299,7 +298,7 @@ respond stateVar request =
                                             pure $ Right (addHeader $ Syntax.KJAnd predicateSort result)
                                         (Left something, _) ->
                                             pure . Left . RpcError.backendError $ RpcError.Aborted $ renderText $ pretty' @mods something
-                whenJust solver SMT.finaliseSolver
+                SMT.finaliseSolver solver
                 stop <- liftIO $ getTime Monotonic
 
                 let duration =
@@ -362,7 +361,7 @@ respond stateVar request =
                                         withContext CtxGetModel $
                                             withContext CtxSMT $
                                                 logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
-                                        pure $ Left SMT.Unknown
+                                        pure $ Left $ SMT.Unknown $ Just "No predicates or substitutions given"
                                     else do
                                         solver <- SMT.initSolver def smtOptions
                                         result <- SMT.getModelFor solver boolPs suppliedSubst
@@ -380,12 +379,7 @@ respond stateVar request =
                                         { satisfiable = RpcTypes.Unsat
                                         , substitution = Nothing
                                         }
-                                Left SMT.ReasonUnknown{} ->
-                                    RpcTypes.GetModelResult
-                                        { satisfiable = RpcTypes.Unknown
-                                        , substitution = Nothing
-                                        }
-                                Left SMT.Unknown ->
+                                Left SMT.Unknown{} ->
                                     RpcTypes.GetModelResult
                                         { satisfiable = RpcTypes.Unknown
                                         , substitution = Nothing
@@ -485,7 +479,7 @@ respond stateVar request =
                             MatchSuccess subst -> do
                                 let filteredConsequentPreds =
                                         Set.map (substituteInPredicate subst) substPatR.constraints `Set.difference` substPatL.constraints
-                                solver <- traverse (SMT.initSolver def) mSMTOptions
+                                solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
 
                                 if null filteredConsequentPreds
                                     then implies (sortOfPattern substPatL) req.antecedent.term req.consequent.term subst
@@ -555,7 +549,10 @@ handleSmtError = JsonRpcHandler $ \case
         let bool = externaliseSort Pattern.SortBool -- predicates are terms of sort Bool
             externalise = Syntax.KJAnd bool . map (externalisePredicate bool) . Set.toList
             allPreds = addHeader $ Syntax.KJAnd bool [externalise premises, externalise preds]
-        pure $ RpcError.backendError $ RpcError.SmtSolverError $ RpcError.ErrorWithTerm reason allPreds
+        pure $
+            RpcError.backendError $
+                RpcError.SmtSolverError $
+                    RpcError.ErrorWithTerm (fromMaybe "UNKNOWN" reason) allPreds
   where
     runtimeError prefix err = do
         let msg = "SMT " <> prefix <> ": " <> err

diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -144,7 +144,7 @@ instance Pretty (PrettyWithModifiers mods EquationFailure) where
 data EquationConfig = EquationConfig
     { definition :: KoreDefinition
     , llvmApi :: Maybe LLVM.API
-    , smtSolver :: Maybe SMT.SMTContext
+    , smtSolver :: SMT.SMTContext
     , maxRecursion :: Bound "Recursion"
     , maxIterations :: Bound "Iterations"
     , logger :: Logger LogMessage
@@ -281,7 +281,7 @@ runEquationT ::
     LoggerMIO io =>
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     Set Predicate ->
     EquationT io a ->
@@ -394,7 +394,7 @@ evaluateTerm ::
     Direction ->
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     Set Predicate ->
     Term ->
     io (Either EquationFailure Term, SimplifierCache)
@@ -417,7 +417,7 @@ evaluatePattern ::
     LoggerMIO io =>
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     Pattern ->
     io (Either EquationFailure Pattern, SimplifierCache)
@@ -462,7 +462,7 @@ evaluateConstraints ::
     LoggerMIO io =>
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     Set Predicate ->
     io (Either EquationFailure (Set Predicate), SimplifierCache)
@@ -828,7 +828,7 @@ applyEquation term rule =
                         -- could now be syntactically present in the path constraints, filter again
                         stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
 
-                        mbSolver :: Maybe SMT.SMTContext <- (.smtSolver) <$> lift getConfig
+                        solver :: SMT.SMTContext <- (.smtSolver) <$> lift getConfig
 
                         -- check any conditions that are still unclear with the SMT solver
                         -- (or abort if no solver is being used), abort if still unclear after
@@ -842,7 +842,7 @@ applyEquation term rule =
                                             liftIO $ Exception.throw other
                                         Right result ->
                                             pure result
-                             in maybe (pure Nothing) (lift . checkWithSmt) mbSolver >>= \case
+                             in lift (checkWithSmt solver) >>= \case
                                     Nothing -> do
                                         -- no solver or still unclear: abort
                                         throwE
@@ -882,23 +882,22 @@ applyEquation term rule =
                                     )
                                     ensured
                         -- check all ensured conditions together with the path condition
-                        whenJust mbSolver $ \solver -> do
-                            lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
-                                Right (Just False) -> do
-                                    let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
-                                    throwE
-                                        ( \ctx ->
-                                            ctx . logMessage $
-                                                WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
-                                                    renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
-                                        , EnsuresFalse falseEnsures
-                                        )
-                                Right _other ->
-                                    pure ()
-                                Left SMT.SMTSolverUnknown{} ->
-                                    pure ()
-                                Left other ->
-                                    liftIO $ Exception.throw other
+                        lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
+                            Right (Just False) -> do
+                                let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
+                                throwE
+                                    ( \ctx ->
+                                        ctx . logMessage $
+                                            WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
+                                                renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
+                                    , EnsuresFalse falseEnsures
+                                    )
+                            Right _other ->
+                                pure ()
+                            Left SMT.SMTSolverUnknown{} ->
+                                pure ()
+                            Left other ->
+                                liftIO $ Exception.throw other
                         lift $ pushConstraints $ Set.fromList ensuredConditions
                         pure $ substituteInTerm subst rule.rhs
   where
@@ -1004,19 +1003,19 @@ simplifyConstraint ::
     LoggerMIO io =>
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     Set Predicate ->
     Predicate ->
     io (Either EquationFailure Predicate, SimplifierCache)
-simplifyConstraint def mbApi mbSMT cache knownPredicates (Predicate p) = do
-    runEquationT def mbApi mbSMT cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
+simplifyConstraint def mbApi smt cache knownPredicates (Predicate p) = do
+    runEquationT def mbApi smt cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
 
 simplifyConstraints ::
     LoggerMIO io =>
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     [Predicate] ->
     io (Either EquationFailure [Predicate], SimplifierCache)

diff --git a/booster/library/Booster/Pattern/Rewrite.hs b/booster/library/Booster/Pattern/Rewrite.hs
@@ -79,7 +79,7 @@ newtype RewriteT io a = RewriteT
 data RewriteConfig = RewriteConfig
     { definition :: KoreDefinition
     , llvmApi :: Maybe LLVM.API
-    , smtSolver :: Maybe SMT.SMTContext
+    , smtSolver :: SMT.SMTContext
     , doTracing :: Flag "CollectRewriteTraces"
     , logger :: Logger LogMessage
     , prettyModifiers :: ModifiersRep
@@ -102,7 +102,7 @@ runRewriteT ::
     Flag "CollectRewriteTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     SimplifierCache ->
     RewriteT io a ->
     io (Either (RewriteFailed "Rewrite") (a, SimplifierCache))
@@ -355,7 +355,7 @@ applyRule pat@Pattern{ceilConditions} rule =
                     stillUnclear <- lift $ filterOutKnownConstraints prior unclearRequires
 
                     -- check unclear requires-clauses in the context of known constraints (prior)
-                    mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
+                    solver <- lift $ RewriteT $ (.smtSolver) <$> ask
 
                     let smtUnclear = do
                             withContext CtxConstraint . withContext CtxAbort . logMessage $
@@ -366,34 +366,23 @@ applyRule pat@Pattern{ceilConditions} rule =
                             failRewrite $
                                 RuleConditionUnclear rule . coerce . foldl1 AndTerm $
                                     map coerce stillUnclear
-                    case mbSolver of
-                        Just solver -> do
-                            checkAllRequires <-
-                                SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)
-
-                            case checkAllRequires of
-                                Left SMT.SMTSolverUnknown{} ->
-                                    smtUnclear -- abort rewrite if a solver result was Unknown
-                                Left other ->
-                                    liftIO $ Exception.throw other -- fail hard on other SMT errors
-                                Right (Just False) -> do
-                                    -- requires is actually false given the prior
-                                    withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
-                                    RewriteRuleAppT $ pure NotApplied
-                                Right (Just True) ->
-                                    pure () -- can proceed
-                                Right Nothing ->
-                                    smtUnclear -- no implication could be determined
-                        Nothing ->
-                            unless (null stillUnclear) $ do
-                                withContext CtxConstraint . withContext CtxAbort $
-                                    logMessage $
-                                        WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
-                                            renderOneLineText $
-                                                "Uncertain about a condition(s) in rule, no SMT solver:"
-                                                    <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
-                                failRewrite $
-                                    RuleConditionUnclear rule (head stillUnclear)
+
+                    checkAllRequires <-
+                        SMT.checkPredicates solver prior mempty (Set.fromList stillUnclear)
+
+                    case checkAllRequires of
+                        Left SMT.SMTSolverUnknown{} ->
+                            smtUnclear -- abort rewrite if a solver result was Unknown
+                        Left other ->
+                            liftIO $ Exception.throw other -- fail hard on other SMT errors
+                        Right (Just False) -> do
+                            -- requires is actually false given the prior
+                            withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
+                            RewriteRuleAppT $ pure NotApplied
+                        Right (Just True) ->
+                            pure () -- can proceed
+                        Right Nothing ->
+                            smtUnclear -- no implication could be determined
 
                     -- check ensures constraints (new) from rhs: stop and return `Trivial` if
                     -- any are false, remove all that are trivially true, return the rest
@@ -405,17 +394,16 @@ applyRule pat@Pattern{ceilConditions} rule =
                         catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures
 
                     -- check all new constraints together with the known side constraints
-                    whenJust mbSolver $ \solver ->
-                        (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
-                            Right (Just False) -> do
-                                withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
-                                RewriteRuleAppT $ pure Trivial
-                            Right _other ->
-                                pure ()
-                            Left SMT.SMTSolverUnknown{} ->
-                                pure ()
-                            Left other ->
-                                liftIO $ Exception.throw other
+                    (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
+                        Right (Just False) -> do
+                            withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
+                            RewriteRuleAppT $ pure Trivial
+                        Right _other ->
+                            pure ()
+                        Left SMT.SMTSolverUnknown{} ->
+                            pure ()
+                        Left other ->
+                            liftIO $ Exception.throw other
 
                     -- existential variables may be present in rule.rhs and rule.ensures,
                     -- need to strip prefixes and freshen their names with respect to variables already
@@ -714,7 +702,7 @@ performRewrite ::
     Flag "CollectRewriteTraces" ->
     KoreDefinition ->
     Maybe LLVM.API ->
-    Maybe SMT.SMTContext ->
+    SMT.SMTContext ->
     -- | maximum depth
     Maybe Natural ->
     -- | cut point rule labels
@@ -723,7 +711,7 @@ performRewrite ::
     [Text] ->
     Pattern ->
     io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
-performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalLabels pat = do
+performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels terminalLabels pat = do
     (rr, RewriteStepsState{counter, traces}) <-
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
@@ -748,7 +736,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
     simplifyP p = withContext CtxSimplify $ do
         st <- get
         let cache = st.simplifierCache
-        evaluatePattern def mLlvmLibrary mSolver cache p >>= \(res, newCache) -> do
+        evaluatePattern def mLlvmLibrary smtSolver cache p >>= \(res, newCache) -> do
             updateCache newCache
             case res of
                 Right newPattern -> do
@@ -815,7 +803,7 @@ performRewrite doTracing def mLlvmLibrary mSolver mbMaxDepth cutLabels terminalL
                     doTracing
                     def
                     mLlvmLibrary
-                    mSolver
+                    smtSolver
                     simplifierCache
                     (withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
                     >>= \case

diff --git a/booster/library/Booster/SMT/Base.hs b/booster/library/Booster/SMT/Base.hs
@@ -81,9 +81,8 @@ data Response
     = Success -- for command_
     | Sat
     | Unsat
-    | Unknown
+    | Unknown (Maybe Text)
     | Values [(SExpr, Value)]
-    | ReasonUnknown Text
     | Error BS.ByteString
     deriving stock (Eq, Ord, Show)