Skip to content

Commit cefb70b

Browse files
jbertholdjberthold
authored
4100 booster abort rewrite on subject vars (#4101)
Fixes #4100 During rewriting, booster was reporting the rule match as "failed" when trying to match a non-variable in the rule to a variable in the subject (introduced by a refactoring mid 2024). This produces unsound results because the subject variable could be constrained to have a value that would match the rule term, enabling the application of this rule. The result in `booster` should therefore be `aborted` as long as we don't allow for introducing constraints like this to the rule application. The new code adds the subject variable to a set of "indeterminate" match pairs. Code has been kept separate so we can later extend the branching mechanism by the collected constraints on subject variables.
1 parent 5fb452a commit cefb70b

File tree

4 files changed

+36
-32
lines changed

4 files changed

+36
-32
lines changed

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

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,13 +9,11 @@ import Control.Monad.Extra (void)
99
import Control.Monad.Trans.Except (runExcept)
1010
import Data.Coerce (coerce)
1111
import Data.Data (Proxy)
12-
import Data.List.NonEmpty qualified as NonEmpty
1312
import Data.Map qualified as Map
1413
import Data.Set qualified as Set
1514
import Data.Text (Text, pack)
1615
import Data.Text qualified as Text
1716
import Network.JSONRPC (ErrorObj)
18-
import Prettyprinter (comma, hsep, punctuate, (<+>))
1917

2018
import Booster.Definition.Base (KoreDefinition)
2119
import Booster.LLVM qualified
@@ -123,22 +121,18 @@ runImplies def mLlvmLibrary mSMTOptions antecedent consequent =
123121
(sortOfPattern patL)
124122
(externaliseExistTerm existsL patL.term)
125123
(externaliseExistTerm existsR patR.term)
126-
MatchIndeterminate remainder ->
124+
MatchIndeterminate _remainder ->
127125
ApplyEquations.evaluatePattern def mLlvmLibrary solver mempty patL >>= \case
128126
(Right simplifedSubstPatL, _) ->
129127
if patL == simplifedSubstPatL
130-
then -- we are being conservative here for now and returning an error.
131-
-- since we have already simplified the LHS, we may want to eventually return implise, but the condition
132-
-- will contain the remainder as an equality contraint, predicating the implication on that equality being true.
128+
then -- we are being conservative here for now and returning "not-implied".
129+
-- We could return implies, but the condition will contain the remainder
130+
-- as an equality contraint, predicating the implication on that equality being true.
133131

134-
pure . Left . RpcError.backendError . RpcError.ImplicationCheckError . RpcError.ErrorOnly . pack $
135-
"match remainder: "
136-
<> renderDefault
137-
( hsep $
138-
punctuate comma $
139-
map (\(t1, t2) -> pretty' @mods t1 <+> "==" <+> pretty' @mods t2) $
140-
NonEmpty.toList remainder
141-
)
132+
doesNotImply
133+
(sortOfPattern patL)
134+
(externaliseExistTerm existsL patL.term)
135+
(externaliseExistTerm existsR patR.term)
142136
else checkImpliesMatchTerms existsL simplifedSubstPatL existsR patR
143137
(Left err, _) ->
144138
pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ err)

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

Lines changed: 16 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,6 @@ data FailReason
7979
SubsortingError SortError
8080
| -- | The two terms have differing argument lengths
8181
ArgLengthsDiffer Term Term
82-
| -- | Not a matching substitution
83-
SubjectVariableMatch Term Variable
8482
deriving stock (Eq, Show)
8583

8684
instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) where
@@ -115,8 +113,6 @@ instance FromModifiersT mods => Pretty (PrettyWithModifiers mods FailReason) whe
115113
pretty $ show err
116114
ArgLengthsDiffer t1 t2 ->
117115
hsep ["Argument length differ", pretty' @mods t1, pretty' @mods t2]
118-
SubjectVariableMatch t v ->
119-
hsep ["Cannot match variable in subject:", pretty' @mods v, pretty' @mods t]
120116

121117
{- | Attempts to find a simple unifying substitution for the given
122118
terms.
@@ -216,9 +212,11 @@ match1 _ t1@DomainValue{} t2@KSet{}
216212
match1 _ t1@DomainValue{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
217213
match1 _ t1@DomainValue{} t2@FunctionApplication{} = addIndeterminate t1 t2
218214
-- match with var on the RHS must be indeterminate when evaluating functions. see: https://github.com/runtimeverification/hs-backend-booster/issues/231
219-
match1 Rewrite t1@DomainValue{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
220-
match1 Implies t1@DomainValue{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
221215
match1 Eval t1@DomainValue{} t2@Var{} = addIndeterminate t1 t2
216+
-- match with var on RHS may lead to branching during rewriting, see https://github.com/runtimeverification/haskell-backend/issues/4100
217+
-- Related cases are currently marked with a special function so they can be identified and changed together later (extending branching functionality)
218+
match1 Rewrite t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2
219+
match1 Implies t1@DomainValue{} (Var v2) = subjectVariableMatch t1 v2
222220
match1 Eval t1@Injection{} t2@AndTerm{} = addIndeterminate t1 t2
223221
match1 _ t1@Injection{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
224222
match1 _ t1@Injection{} t2@DomainValue{} = failWith $ DifferentSymbols t1 t2
@@ -228,6 +226,7 @@ match1 _ t1@Injection{} t2@KList{}
228226
match1 _ t1@Injection{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
229227
match1 _ t1@Injection{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
230228
match1 _ t1@Injection{} t2@FunctionApplication{} = addIndeterminate t1 t2
229+
match1 Rewrite t1@Injection{} (Var v2) = subjectVariableMatch t1 v2
231230
match1 _ t1@Injection{} t2@Var{} = addIndeterminate t1 t2
232231
match1 Eval t1@KMap{} t2@AndTerm{} = addIndeterminate t1 t2
233232
match1 _ t1@KMap{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -239,7 +238,7 @@ match1 _ t1@KMap{} t2@KList{}
239238
match1 _ t1@KMap{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
240239
match1 _ t1@KMap{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
241240
match1 _ t1@KMap{} t2@FunctionApplication{} = addIndeterminate t1 t2
242-
match1 Rewrite t1@KMap{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
241+
match1 Rewrite t1@KMap{} (Var v2) = subjectVariableMatch t1 v2
243242
match1 _ t1@KMap{} t2@Var{} = addIndeterminate t1 t2
244243
match1 Eval t1@KList{} t2@AndTerm{} = addIndeterminate t1 t2
245244
match1 _ t1@KList{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -252,7 +251,7 @@ match1 _ t1@(KList def1 heads1 rest1) t2@(KList def2 heads2
252251
match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
253252
match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
254253
match1 _ t1@KList{} t2@FunctionApplication{} = addIndeterminate t1 t2
255-
match1 Rewrite t1@KList{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
254+
match1 Rewrite t1@KList{} (Var t2) = subjectVariableMatch t1 t2
256255
match1 _ t1@KList{} t2@Var{} = addIndeterminate t1 t2
257256
match1 Eval t1@KSet{} t2@AndTerm{} = addIndeterminate t1 t2
258257
match1 _ t1@KSet{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -264,7 +263,7 @@ match1 _ t1@KSet{} t2@KList{}
264263
match1 _ t1@(KSet def1 patElements patRest) t2@(KSet def2 subjElements subjRest) = if def1 == def2 then matchSets def1 patElements patRest subjElements subjRest else failWith $ DifferentSorts t1 t2
265264
match1 _ t1@KSet{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2
266265
match1 _ t1@KSet{} t2@FunctionApplication{} = addIndeterminate t1 t2
267-
match1 Rewrite t1@KSet{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
266+
match1 Rewrite t1@KSet{} (Var t2) = subjectVariableMatch t1 t2
268267
match1 _ t1@KSet{} t2@Var{} = addIndeterminate t1 t2
269268
match1 Eval t1@ConsApplication{} t2@AndTerm{} = addIndeterminate t1 t2
270269
match1 _ t1@ConsApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -276,7 +275,7 @@ match1 _ t1@ConsApplication{} t2@KSet{}
276275
match1 matchTy (ConsApplication symbol1 sorts1 args1) (ConsApplication symbol2 sorts2 args2) = matchSymbolAplications matchTy symbol1 sorts1 args1 symbol2 sorts2 args2
277276
match1 Eval (ConsApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2
278277
match1 _ t1@ConsApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2
279-
match1 Rewrite t1@ConsApplication{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
278+
match1 Rewrite t1@ConsApplication{} (Var t2) = subjectVariableMatch t1 t2
280279
match1 _ t1@ConsApplication{} t2@Var{} = addIndeterminate t1 t2
281280
match1 Eval t1@FunctionApplication{} t2@AndTerm{} = addIndeterminate t1 t2
282281
match1 _ t1@FunctionApplication{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -294,7 +293,7 @@ match1 Eval (FunctionApplication symbol1 sorts1 args1) (ConsApplication symbo
294293
match1 _ t1@FunctionApplication{} t2@ConsApplication{} = addIndeterminate t1 t2
295294
match1 Eval (FunctionApplication symbol1 sorts1 args1) (FunctionApplication symbol2 sorts2 args2) = matchSymbolAplications Eval symbol1 sorts1 args1 symbol2 sorts2 args2
296295
match1 _ t1@FunctionApplication{} t2@FunctionApplication{} = addIndeterminate t1 t2
297-
match1 Rewrite t1@FunctionApplication{} (Var t2) = failWith $ SubjectVariableMatch t1 t2
296+
match1 Rewrite t1@FunctionApplication{} (Var t2) = subjectVariableMatch t1 t2
298297
match1 _ t1@FunctionApplication{} t2@Var{} = addIndeterminate t1 t2
299298
match1 Eval t1@Var{} t2@AndTerm{} = addIndeterminate t1 t2
300299
match1 _ t1@Var{} (AndTerm t2a t2b) = enqueueRegularProblem t1 t2a >> enqueueRegularProblem t1 t2b
@@ -448,6 +447,12 @@ matchVar
448447
else Injection termSort variableSort term2
449448
else failWith $ DifferentSorts (Var var) term2
450449

450+
-- Subject variable matches are currently marked as indeterminate.
451+
-- The code may be extended to collect these as separate conditional
452+
-- results (for branching).
453+
subjectVariableMatch :: Term -> Variable -> StateT MatchState (Except MatchResult) ()
454+
subjectVariableMatch t v = addIndeterminate t (Var v)
455+
451456
{- | pair up the argument lists and return the pairs in the first argument. If the lists
452457
are of equal length, return Nothing in second, else return the remaining
453458
terms in the longer list, tagged with their origin).

‎booster/unit-tests/Test/Booster/Pattern/Rewrite.hs

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ test_rewriteStep =
4141
"Rewriting"
4242
[ errorCases
4343
, rewriteSuccess
44-
, unifyNotMatch
44+
, subjectVariables
4545
, definednessUnclear
4646
, rewriteStuck
4747
, rulePriority
@@ -176,7 +176,7 @@ testConf = do
176176
----------------------------------------
177177
errorCases
178178
, rewriteSuccess
179-
, unifyNotMatch
179+
, subjectVariables
180180
, definednessUnclear
181181
, rewriteStuck
182182
, rulePriority ::
@@ -207,10 +207,15 @@ rewriteSuccess =
207207
`rewritesTo` ( "con1-f1"
208208
, [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}( \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
209209
)
210-
unifyNotMatch =
211-
testCase "Stuck case when subject has variables" $
212-
getsStuck
213-
[trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
210+
subjectVariables =
211+
testCase "Aborts case when subject has variables" $ do
212+
let t =
213+
[trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( X:SomeSort{}, \dv{SomeSort{}}("thing") ) ), ConfigVar:SortK{}) ) |]
214+
t
215+
`failsWith` RuleApplicationUnclear
216+
rule3
217+
t
218+
(NE.singleton ([trm| \dv{SomeSort{}}("otherThing")|], [trm| X:SomeSort{} |]))
214219
definednessUnclear =
215220
testCase "con4 rewrite to f2 might become undefined" $ do
216221
let pcon4 =

‎scripts/performance-tests-kontrol.sh

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ master_shell() {
104104
}
105105

106106
# kompile Kontrol's K dependencies
107-
feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.foundry --jobs 4"
107+
feature_shell "poetry install && poetry run kdist --verbose build evm-semantics.plugin evm-semantics.haskell kontrol.* --jobs 4"
108108

109109
# kompile the test contracts, to be reused in feature_shell and master_shell. Copy the result from pytest's temp directory
110110
PYTEST_TEMP_DIR=$TEMPD/pytest-temp-dir

0 commit comments

Comments
 (0)