Skip to content

Commit

Permalink
3956 branching on complete conditions in Booster (#4058)
Browse files Browse the repository at this point in the history 
Part of #3956
Partially subsumes
#3960

This PR makes the rewrite rule application algorithm of Booster more
powerful by allowing branching on *complete conditions*.

The rewriting algorithm is modified:
- when checking the `requires` clause of a rule, we compute the
remainder condition `RULE_REM` of that attempted, which is the
semantically-checked subset of the required conjuncts `P` which
*unclear* after checking its entailment form the pattern's constrains
`PC`, meaning that (PC /\ P, PC /\ not P) is (SAT, SAT) or any of the
two queries were UNKNOWN
- if that remainder is not empty, we return it's *negation* together
with the result
- when we are finished attempting a *priority group* of rules, we
collect the negated remainder conditions `not RULE_REM_i` and conjunct
them. This the groups remainder condition `GROUP_REM == not RULE_REM_1
/\ not RULE_REM_2 /\ ... /\ not RULE_REM_n`
- At that point, we need to check `GROUP_REM` for satisfiablity.
- **If the `GROUP_REM` condition is UNSAT, it means that this group of
rules is *complete***, meaning that no other rule can possibly apply,
and we do not need to even attempt applying rules of lower priority.
This behaviour is the **primary contribution of this PR**.
- Otherwise, if it is SAT or solver said UNKNOWN, it means that this
group of rules is not complete, i.e. it does not cover the whole space
of logical possibility, and we need to construct a remainder
configuration, and continue attempting to apply other rules to it. If no
rules remain, it means that we are stuck and the semantics is
incomplete. This PR does not implement the process of descending into
the remainder branch. **Booster with this PR will abort on a SAT
remainder**.

This behaviour is active by default in `booster-dev` and can be enabled
in `kore-rpc-booster` with the flag `--fallback-on Aborted,Stuck` (the
default is `Aborted,Stuck,Branching`). Note that with the default
reasons, the behaviour of `kore-rpc-booster` is functionally the same,
but operationally slightly different: In `Proxy.hs`, Booster may not
return `Branching`, and the fallback logic will confirm that Kore
returns `Branching` as well, flagging any differences in the `[proxy]`
logs (see
[Proxy.hs#L391](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/tools/booster/Proxy.hs#L391)).

TODO: we need a better flag to enabled branching in Booster, as giving a
`--fallback-on Aborted,Stuck` is really non-intuitive.

Note:
a naive algorithm to compute the remainder conditions would be: after
applying a group of rules, take their substituted requires clauses,
disjunct and negate. However, this yields a non-minimal predicate that
was not simplified and syntactically filtered, potentially making it
harder for the SMT solver to solve. The algorithm described above and
implemented in this PR re-uses the indeterminate results obtained while
applying individual rules and simplifying/checking their individual
requires clauses. This logic has been originally proposed by Sam in
#3960.

See
[remainder-predicates.k](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/resources/remainder-predicates.k)
and
[test-remainder-predicates](https://github.com/runtimeverification/haskell-backend/blob/3956-booster-rewrite-rule-remainders/booster/test/rpc-integration/test-remainder-predicates)
for a series of integrations tests that cover the behaviour of
`booster-dev` and `kore-rpc-booster`.
  • Loading branch information
@geo2a
geo2a authored Oct 29, 2024
1 parent b2ef73c commit 328cd2c
Show file tree
Hide file tree
Showing 51 changed files with 123,761 additions and 214 deletions.
82 changes: 53 additions & 29 deletions booster/library/Booster/JsonRpc.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ import Control.Monad
import Control.Monad.IO.Class
import Control.Monad.Trans.Except (catchE, except, runExcept, runExceptT, throwE, withExceptT)
import Crypto.Hash (SHA256 (..), hashWith)
import Data.Bifunctor (second)
import Data.Bifunctor (first, second)
import Data.Foldable
import Data.List (singleton)
import Data.Map.Strict (Map)
Expand All @@ -38,7 +38,7 @@ import GHC.Records
import Numeric.Natural

import Booster.CLOptions (RewriteOptions (..))
import Booster.Definition.Attributes.Base (UniqueId, getUniqueId, uniqueId)
import Booster.Definition.Attributes.Base (getUniqueId, uniqueId)
import Booster.Definition.Base (KoreDefinition (..))
import Booster.Definition.Base qualified as Definition (RewriteRule (..))
import Booster.LLVM as LLVM (API)
Expand All @@ -49,6 +49,7 @@ import Booster.Pattern.Base qualified as Pattern
import Booster.Pattern.Implies (runImplies)
import Booster.Pattern.Pretty
import Booster.Pattern.Rewrite (
AppliedRuleMetadata (..),
RewriteConfig (..),
RewriteFailed (..),
RewriteResult (..),
Expand All @@ -57,7 +58,9 @@ import Booster.Pattern.Rewrite (
)
import Booster.Pattern.Substitution qualified as Substitution
import Booster.Pattern.Util (
externaliseRuleMarker,
freeVariables,
modifyVarName,
sortOfPattern,
sortOfTerm,
)
Expand Down Expand Up @@ -479,11 +482,13 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.Branching
, depth
, logs
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates =
Just $
map (\(_, muid, p') -> toExecState p' unsupported (Just muid)) $
toList nexts
Just
$ map
( \(rewritten, ruleMetadata) -> toExecState rewritten (Just ruleMetadata) unsupported
)
$ toList nexts
, rule = Nothing
, unknownPredicate = Nothing
}
Expand All @@ -494,7 +499,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.Stuck
, depth
, logs
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -506,7 +511,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.Vacuous
, depth
, logs
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -518,8 +523,8 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.CutPointRule
, depth
, logs
, state = toExecState p unsupported Nothing
, nextStates = Just [toExecState next unsupported Nothing]
, state = toExecState p Nothing unsupported
, nextStates = Just [toExecState next Nothing unsupported]
, rule = Just lbl
, unknownPredicate = Nothing
}
Expand All @@ -530,7 +535,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.TerminalRule
, depth
, logs
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates = Nothing
, rule = Just lbl
, unknownPredicate = Nothing
Expand All @@ -542,7 +547,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
{ reason = RpcTypes.DepthBound
, depth
, logs
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -559,7 +564,7 @@ execResponse req (d, traces, rr) unsupported = case rr of
(logSuccessfulRewrites, logFailedRewrites)
(RewriteStepFailed failure)
in logs <|> abortRewriteLog
, state = toExecState p unsupported Nothing
, state = toExecState p Nothing unsupported
, nextStates = Nothing
, rule = Nothing
, unknownPredicate = Nothing
Expand All @@ -582,23 +587,37 @@ execResponse req (d, traces, rr) unsupported = case rr of
xs@(_ : _) -> Just xs

toExecState ::
Pattern -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
toExecState pat unsupported muid =
Pattern ->
Maybe AppliedRuleMetadata ->
[Syntax.KorePattern] ->
RpcTypes.ExecuteState
{ term = addHeader t
, predicate = addHeader <$> addUnsupported p
, substitution = addHeader <$> s
, ruleSubstitution = Nothing
, rulePredicate = Nothing
, ruleId = getUniqueId <$> muid
}
where
(t, p, s) = externalisePattern pat
termSort = externaliseSort $ sortOfPattern pat
allUnsupported = Syntax.KJAnd termSort unsupported
addUnsupported
| null unsupported = id
| otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))
toExecState
pat
mRuleMetadata
unsupported =
RpcTypes.ExecuteState
{ term = addHeader t
, predicate = addHeader <$> addUnsupported p
, substitution = addHeader <$> s
, ruleSubstitution = addHeader <$> mruleSubstExt
, rulePredicate = addHeader <$> mrulePredExt
, ruleId = getUniqueId . ruleUniqueId <$> mRuleMetadata
}
where
mrulePredExt = externalisePredicate termSort . rulePredicate <$> mRuleMetadata
mruleSubstExt =
Syntax.KJAnd termSort
. map
(uncurry (externaliseSubstitution termSort) . first (modifyVarName externaliseRuleMarker))
. Map.toList
. ruleSubstitution
<$> mRuleMetadata
(t, p, s) = externalisePattern pat
termSort = externaliseSort $ sortOfPattern pat
allUnsupported = Syntax.KJAnd termSort unsupported
addUnsupported
| null unsupported = id
| otherwise = maybe (Just allUnsupported) (Just . Syntax.KJAnd termSort . (: unsupported))

mkLogRewriteTrace ::
(Bool, Bool) ->
Expand Down Expand Up @@ -639,6 +658,11 @@ mkLogRewriteTrace
{ reason = "Uncertain about a condition in rule"
, _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes r)
}
RewriteRemainderPredicate rs _ _ ->
Failure
{ reason = "Uncertain about the remainder after applying a rule"
, _ruleId = Just $ getUniqueId (uniqueId $ Definition.attributes (head rs))
}
DefinednessUnclear r _ undefReasons ->
Failure
{ reason = "Uncertain about definedness of rule because of: " <> pack (show undefReasons)
Expand Down
11 changes: 11 additions & 0 deletions booster/library/Booster/Pattern/Bool.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@ License : BSD-3-Clause
module Booster.Pattern.Bool (
foldAndBool,
isBottom,
isFalse,
negateBool,
splitBoolPredicates,
splitAndBools,
collapseAndBools,
-- patterns
pattern TrueBool,
pattern FalseBool,
Expand Down Expand Up @@ -188,6 +190,11 @@ foldAndBool (x : xs) = AndBool x $ foldAndBool xs
isBottom :: Pattern -> Bool
isBottom = (Predicate FalseBool `elem`) . constraints

isFalse :: Predicate -> Bool
isFalse = \case
(Predicate FalseBool) -> True
_ -> False

{- | We want to break apart predicates of type `Y1 andBool ... Yn` apart, in case some of the `Y`s are abstract
which prevents the original expression from being fed to the LLVM simplifyBool function
-}
Expand All @@ -205,3 +212,7 @@ splitAndBools :: Predicate -> [Predicate]
splitAndBools p@(Predicate t)
| AndBool l r <- t = concatMap (splitAndBools . Predicate) [l, r]
| otherwise = [p]

-- | Inverse of splitAndBools
collapseAndBools :: [Predicate] -> Predicate
collapseAndBools = Predicate . foldAndBool . map (\(Predicate p) -> p)
Loading

0 comments on commit 328cd2c

Please sign in to comment.