Skip to content

Commit 97f8a9e

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents ab3468e + abf81e9 commit 97f8a9e

18 files changed

+4120
-541
lines changed

‎booster/library/Booster/Pattern/ApplyEquations.hs‎

Lines changed: 58 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@ module Booster.Pattern.ApplyEquations (
2626
evaluateConstraints,
2727
) where
2828

29+
import Control.Exception qualified as Exception (throw)
2930
import Control.Monad
3031
import Control.Monad.Extra (fromMaybeM, whenJust)
3132
import Control.Monad.IO.Class (MonadIO (..))
@@ -39,7 +40,7 @@ import Data.ByteString.Char8 qualified as BS
3940
import Data.Coerce (coerce)
4041
import Data.Data (Data, Proxy)
4142
import Data.Foldable (toList, traverse_)
42-
import Data.List (intersperse, partition)
43+
import Data.List (foldl1', intersperse, partition)
4344
import Data.List.NonEmpty qualified as NonEmpty
4445
import Data.Map (Map)
4546
import Data.Map qualified as Map
@@ -817,17 +818,45 @@ applyEquation term rule =
817818
-- could now be syntactically present in the path constraints, filter again
818819
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions
819820

820-
-- abort if any of the conditions is still unclear at that point
821+
mbSolver :: Maybe SMT.SMTContext <- (.smtSolver) <$> lift getConfig
822+
823+
-- check any conditions that are still unclear with the SMT solver
824+
-- (or abort if no solver is being used), abort if still unclear after
821825
unless (null stillUnclear) $
822-
throwE
823-
( \ctxt ->
824-
ctxt $
825-
logMessage $
826-
renderOneLineText $
827-
"Uncertain about a condition(s) in rule:"
828-
<+> hsep (intersperse "," $ map (pretty' @mods) unclearConditions)
829-
, IndeterminateCondition unclearConditions
830-
)
826+
let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool)
827+
checkWithSmt smt =
828+
SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case
829+
Left SMT.SMTSolverUnknown{} -> do
830+
pure Nothing
831+
Left other ->
832+
liftIO $ Exception.throw other
833+
Right result ->
834+
pure result
835+
in maybe (pure Nothing) (lift . checkWithSmt) mbSolver >>= \case
836+
Nothing -> do
837+
-- no solver or still unclear: abort
838+
throwE
839+
( \ctx ->
840+
ctx . logMessage $
841+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
842+
renderOneLineText
843+
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
844+
)
845+
, IndeterminateCondition stillUnclear
846+
)
847+
Just False -> do
848+
-- actually false given path condition: fail
849+
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
850+
throwE
851+
( \ctx ->
852+
ctx . logMessage $
853+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
854+
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
855+
, ConditionFalse failedP
856+
)
857+
Just True -> do
858+
-- can proceed
859+
pure ()
831860

832861
-- check ensured conditions, filter any
833862
-- true ones, prune if any is false
@@ -842,6 +871,24 @@ applyEquation term rule =
842871
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p)
843872
)
844873
ensured
874+
-- check all ensured conditions together with the path condition
875+
whenJust mbSolver $ \solver -> do
876+
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
877+
Right (Just False) -> do
878+
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
879+
throwE
880+
( \ctx ->
881+
ctx . logMessage $
882+
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
883+
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
884+
, EnsuresFalse falseEnsures
885+
)
886+
Right _other ->
887+
pure ()
888+
Left SMT.SMTSolverUnknown{} ->
889+
pure ()
890+
Left other ->
891+
liftIO $ Exception.throw other
845892
lift $ pushConstraints $ Set.fromList ensuredConditions
846893
pure $ substituteInTerm subst rule.rhs
847894
where

‎booster/test/rpc-integration/resources/simplify-smt.k‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
module SIMPLIFY-SMT-SYNTAX
2+
imports INT
3+
imports BOOL
4+
imports STRING
5+
6+
// testing SMT solver use during equation application
7+
8+
syntax Thing ::= unevaluated ( Int, Int ) [function, symbol("unevaluated")]
9+
| evaluated ( String ) [symbol("evaluated")]
10+
endmodule
11+
12+
module SIMPLIFY-SMT
13+
imports INT
14+
imports BOOL
15+
imports SIMPLIFY-SMT-SYNTAX
16+
17+
// contradicting requires clauses: unclear in isolation, false when checked together
18+
rule [bad-requires]:
19+
unevaluated(A, B) => evaluated("contradicting requires clause")
20+
requires A *Int B <=Int 0 andBool A <Int B andBool B <Int A // should never apply
21+
[priority(10), preserves-definedness]
22+
// unclear without SMT solver, aborting function evaluation)
23+
24+
// Should apply with the right path conditions about A and B.
25+
rule [good-requires]:
26+
unevaluated(A, B) => evaluated("A and B have the same sign and are not zero")
27+
requires 0 <Int A *Int B
28+
[priority(20), preserves-definedness]
29+
30+
// contradicting ensures clauses: unclear in isolation, false when checked together
31+
rule [bad-ensures]:
32+
unevaluated(A, B) => evaluated("contradicting ensures clause")
33+
ensures A <Int B andBool B <Int A // should terminate the evaluation
34+
[priority(30), preserves-definedness]
35+
// would be added to the path condition without SMT solver
36+
37+
endmodule

0 commit comments

Comments
 (0)