Skip to content

Commit 9e830fa

Browse files
geo2ageo2a
committed
Include rule predicate into branching response
Regenerate a test output
1 parent 09a73ad commit 9e830fa

File tree

4 files changed

+124
-25
lines changed

4 files changed

+124
-25
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 32 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ import Booster.Definition.Base qualified as Definition (RewriteRule (..))
4444
import Booster.LLVM as LLVM (API)
4545
import Booster.Log
4646
import Booster.Pattern.ApplyEquations qualified as ApplyEquations
47-
import Booster.Pattern.Base (Pattern (..), Sort (SortApp), Term, Variable)
47+
import Booster.Pattern.Base (Pattern (..), Predicate, Sort (SortApp), Term, Variable)
4848
import Booster.Pattern.Base qualified as Pattern
4949
import Booster.Pattern.Implies (runImplies)
5050
import Booster.Pattern.Pretty
@@ -483,11 +483,14 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
483483
{ reason = RpcTypes.Branching
484484
, depth
485485
, logs
486-
, state = toExecState p originalSubstitution unsupported Nothing
486+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
487487
, nextStates =
488-
Just $
489-
map (\(_, muid, p') -> toExecState p' originalSubstitution unsupported (Just muid)) $
490-
toList nexts
488+
-- FIXME return _ruleSubst in the response, removing '#'s from the variable names to make pyk happy
489+
Just
490+
$ map
491+
( \(_, muid, p', mrulePred, _ruleSubst) -> toExecState p' originalSubstitution unsupported (Just muid) mrulePred Nothing
492+
)
493+
$ toList nexts
491494
, rule = Nothing
492495
, unknownPredicate = Nothing
493496
}
@@ -498,7 +501,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
498501
{ reason = RpcTypes.Stuck
499502
, depth
500503
, logs
501-
, state = toExecState p originalSubstitution unsupported Nothing
504+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
502505
, nextStates = Nothing
503506
, rule = Nothing
504507
, unknownPredicate = Nothing
@@ -510,7 +513,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
510513
{ reason = RpcTypes.Vacuous
511514
, depth
512515
, logs
513-
, state = toExecState p originalSubstitution unsupported Nothing
516+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
514517
, nextStates = Nothing
515518
, rule = Nothing
516519
, unknownPredicate = Nothing
@@ -522,8 +525,8 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
522525
{ reason = RpcTypes.CutPointRule
523526
, depth
524527
, logs
525-
, state = toExecState p originalSubstitution unsupported Nothing
526-
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing]
528+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
529+
, nextStates = Just [toExecState next originalSubstitution unsupported Nothing Nothing Nothing]
527530
, rule = Just lbl
528531
, unknownPredicate = Nothing
529532
}
@@ -534,7 +537,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
534537
{ reason = RpcTypes.TerminalRule
535538
, depth
536539
, logs
537-
, state = toExecState p originalSubstitution unsupported Nothing
540+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
538541
, nextStates = Nothing
539542
, rule = Just lbl
540543
, unknownPredicate = Nothing
@@ -546,7 +549,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
546549
{ reason = RpcTypes.DepthBound
547550
, depth
548551
, logs
549-
, state = toExecState p originalSubstitution unsupported Nothing
552+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
550553
, nextStates = Nothing
551554
, rule = Nothing
552555
, unknownPredicate = Nothing
@@ -563,7 +566,7 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
563566
(logSuccessfulRewrites, logFailedRewrites)
564567
(RewriteStepFailed failure)
565568
in logs <|> abortRewriteLog
566-
, state = toExecState p originalSubstitution unsupported Nothing
569+
, state = toExecState p originalSubstitution unsupported Nothing Nothing Nothing
567570
, nextStates = Nothing
568571
, rule = Nothing
569572
, unknownPredicate = Nothing
@@ -586,19 +589,32 @@ execResponse req (d, traces, rr) originalSubstitution unsupported = case rr of
586589
xs@(_ : _) -> Just xs
587590

588591
toExecState ::
589-
Pattern -> Map Variable Term -> [Syntax.KorePattern] -> Maybe UniqueId -> RpcTypes.ExecuteState
590-
toExecState pat sub unsupported muid =
592+
Pattern ->
593+
Map Variable Term ->
594+
[Syntax.KorePattern] ->
595+
Maybe UniqueId ->
596+
Maybe Predicate ->
597+
Maybe (Map Variable Term) ->
598+
RpcTypes.ExecuteState
599+
toExecState pat sub unsupported muid mrulePredicate mruleSubst =
591600
RpcTypes.ExecuteState
592601
{ term = addHeader t
593602
, predicate = addHeader <$> addUnsupported p
594603
, substitution = addHeader <$> s
595-
, ruleSubstitution = Nothing
596-
, rulePredicate = Nothing
604+
, ruleSubstitution = addHeader <$> mruleSubstExt
605+
, rulePredicate = addHeader <$> mrulePredExt
597606
, ruleId = getUniqueId <$> muid
598607
}
599608
where
609+
mrulePredExt = externalisePredicate termSort <$> mrulePredicate
610+
mruleSubstExt =
611+
Syntax.KJAnd predicateSort
612+
. map (uncurry $ externaliseSubstitution predicateSort)
613+
. Map.toList
614+
<$> mruleSubst
600615
(t, p, s) = externalisePattern pat sub
601616
termSort = externaliseSort $ sortOfPattern pat
617+
predicateSort = externaliseSort Pattern.SortBool
602618
allUnsupported = Syntax.KJAnd termSort unsupported
603619
addUnsupported
604620
| null unsupported = id

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

Lines changed: 18 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -225,7 +225,7 @@ rewriteStep cutLabels terminalLabels pat = do
225225
pure $
226226
RewriteBranch pat $
227227
NE.fromList $
228-
map (\(r, p, _subst) -> (ruleLabelOrLocT r, uniqueId r, p)) xs
228+
map (\(r, p, subst) -> (ruleLabelOrLocT r, uniqueId r, p, mkRulePredicate r subst, subst)) xs
229229
| otherwise -> do
230230
-- otherwise, we need to check the remainder predicate with the SMT solver
231231
-- and construct an additional remainder branch if needed
@@ -237,7 +237,7 @@ rewriteStep cutLabels terminalLabels pat = do
237237
pure $
238238
RewriteBranch pat $
239239
NE.fromList $
240-
map (\(r, p, _subst) -> (ruleLabelOrLocT r, uniqueId r, p)) xs
240+
map (\(r, p, subst) -> (ruleLabelOrLocT r, uniqueId r, p, mkRulePredicate r subst, subst)) xs
241241
satRes@(SMT.IsSat{}) -> do
242242
-- the remainder condition is satisfiable.
243243
-- Have to construct the remainder branch and consider it
@@ -694,7 +694,7 @@ ruleLabelOrLoc rule =
694694
-- | Different rewrite results (returned from RPC execute endpoint)
695695
data RewriteResult pat
696696
= -- | branch point
697-
RewriteBranch pat (NonEmpty (Text, UniqueId, pat))
697+
RewriteBranch pat (NonEmpty (Text, UniqueId, pat, Maybe Predicate, Substitution))
698698
| -- | no rules could be applied, config is stuck
699699
RewriteStuck pat
700700
| -- | cut point rule, return current (lhs) and single next state
@@ -922,14 +922,14 @@ performRewrite rewriteConfig pat = do
922922
simplifyP p >>= \case
923923
Nothing -> pure $ RewriteTrivial orig
924924
Just p' -> do
925-
let simplifyP3rd (a, b, c) =
926-
fmap (a,b,) <$> simplifyP c
925+
let simplifyP3rd (a, b, c, e, f) =
926+
fmap (a,b,,e,f) <$> simplifyP c
927927
nexts' <- catMaybes <$> mapM simplifyP3rd (toList nexts)
928928
pure $ case nexts' of
929929
-- The `[]` case should be `Stuck` not `Trivial`, because `RewriteTrivial p'`
930930
-- means the pattern `p'` is bottom, but we know that is not the case here.
931931
[] -> RewriteStuck p'
932-
[(lbl, uId, n)] -> RewriteFinished (Just lbl) (Just uId) n
932+
[(lbl, uId, n, _rp, _rs)] -> RewriteFinished (Just lbl) (Just uId) n
933933
ns -> RewriteBranch p' $ NE.fromList ns
934934
r@RewriteStuck{} -> pure r
935935
r@RewriteTrivial{} -> pure r
@@ -999,7 +999,7 @@ performRewrite rewriteConfig pat = do
999999
incrementCounter
10001000
doSteps False single
10011001
RewriteBranch pat'' branches -> withPatternContext pat' $ do
1002-
emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _) -> (lbl, uid)) branches
1002+
emitRewriteTrace $ RewriteBranchingStep pat'' $ fmap (\(lbl, uid, _, _, _) -> (lbl, uid)) branches
10031003
pure simplified
10041004
_other -> withPatternContext pat' $ error "simplifyResult: Unexpected return value"
10051005
Right (cutPoint@(RewriteCutPoint lbl _ _ _), _) -> withPatternContext pat' $ do
@@ -1092,3 +1092,14 @@ rewriteStart =
10921092
, traces = mempty
10931093
, simplifierCache = mempty
10941094
}
1095+
1096+
{- | Instantiate a rewrite rule's requires clause with a substitution.
1097+
Returns Nothing is the resulting @Predicate@ is trivially @True@.
1098+
-}
1099+
mkRulePredicate :: RewriteRule a -> Substitution -> Maybe Predicate
1100+
mkRulePredicate rule subst =
1101+
case concatMap
1102+
(splitBoolPredicates . coerce . substituteInTerm subst . coerce)
1103+
rule.requires of
1104+
[] -> Nothing
1105+
xs -> Just $ collapseAndBools xs

‎booster/test/rpc-integration/test-a-to-f/response-branching.booster-dev

Lines changed: 72 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -156,7 +156,42 @@
156156
]
157157
}
158158
},
159-
"rule-id": "aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8"
159+
"rule-id": "aba8479fef763c749fa1a1837f2591f85d8541ca8837c738cf586de790c6f8b8",
160+
"rule-predicate": {
161+
"format": "KORE",
162+
"version": 1,
163+
"term": {
164+
"tag": "Equals",
165+
"argSort": {
166+
"tag": "SortApp",
167+
"name": "SortBool",
168+
"args": []
169+
},
170+
"sort": {
171+
"tag": "SortApp",
172+
"name": "SortGeneratedTopCell",
173+
"args": []
174+
},
175+
"first": {
176+
"tag": "DV",
177+
"sort": {
178+
"tag": "SortApp",
179+
"name": "SortBool",
180+
"args": []
181+
},
182+
"value": "true"
183+
},
184+
"second": {
185+
"tag": "DV",
186+
"sort": {
187+
"tag": "SortApp",
188+
"name": "SortBool",
189+
"args": []
190+
},
191+
"value": "true"
192+
}
193+
}
194+
}
160195
},
161196
{
162197
"term": {
@@ -233,7 +268,42 @@
233268
]
234269
}
235270
},
236-
"rule-id": "3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e"
271+
"rule-id": "3cfae148c63f879628626da1753b07d517f6ac9b414543f7dd8f7b3e8e19329e",
272+
"rule-predicate": {
273+
"format": "KORE",
274+
"version": 1,
275+
"term": {
276+
"tag": "Equals",
277+
"argSort": {
278+
"tag": "SortApp",
279+
"name": "SortBool",
280+
"args": []
281+
},
282+
"sort": {
283+
"tag": "SortApp",
284+
"name": "SortGeneratedTopCell",
285+
"args": []
286+
},
287+
"first": {
288+
"tag": "DV",
289+
"sort": {
290+
"tag": "SortApp",
291+
"name": "SortBool",
292+
"args": []
293+
},
294+
"value": "true"
295+
},
296+
"second": {
297+
"tag": "DV",
298+
"sort": {
299+
"tag": "SortApp",
300+
"name": "SortBool",
301+
"args": []
302+
},
303+
"value": "true"
304+
}
305+
}
306+
}
237307
}
238308
]
239309
}

‎booster/tools/booster/Proxy.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -527,6 +527,8 @@ respondEither cfg@ProxyConfig{boosterState} booster kore req = case req of
527527
sub
528528
unsup
529529
Nothing
530+
Nothing
531+
Nothing
530532
)
531533
{ ruleId = s.ruleId
532534
, ruleSubstitution = s.ruleSubstitution

0 commit comments

Comments
 (0)