Skip to content

Commit be64ead

Browse files
jbertholdgoodlyrottenapple
jberthold
and
goodlyrottenapple
authored
Booster: Avoid var. names from input substitution when creating new ones (#4007)
When rewriting with rules that have existentials on the RHS, booster needs to rename these existential variables to avoid collisions. However, the input is pre-processed to recognise predicates of the form `X ==K expr` and apply them (after checking/vetting) as a _substitution_ to the configuration and (other) path conditions. As a result, the variable names in the substitution are not present in the pattern any more when rewriting. The substitution is added back (as additional information) in the output, so subsequent simplification steps will apply it again, falsely, if variable names from the substitution are reused during rewriting. As a solution, we supply the "forbidden variable names" to the rewriter. Alternatively, we could stop including the applied substitution in the output, but this would create a disparity between `booster` and `kore-rpc`. Fixes #4006 --------- Co-authored-by: Samuel Balco <[email protected]>
1 parent f66df15 commit be64ead

File tree

7 files changed

+701
-11
lines changed

7 files changed

+701
-11
lines changed

‎booster/library/Booster/JsonRpc.hs

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ import Booster.Pattern.Rewrite (
5959
performRewrite,
6060
)
6161
import Booster.Pattern.Util (
62+
freeVariables,
6263
sortOfPattern,
6364
substituteInPredicate,
6465
substituteInTerm,
@@ -143,10 +144,16 @@ respond stateVar request =
143144
, constraints = Set.map (substituteInPredicate substitution) pat.constraints
144145
, ceilConditions = pat.ceilConditions
145146
}
147+
-- remember all variables used in the substitutions
148+
substVars =
149+
Set.unions
150+
[ Set.singleton v <> freeVariables e
151+
| (v, e) <- Map.assocs substitution
152+
]
146153

147154
solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
148155
result <-
149-
performRewrite doTracing def mLlvmLibrary solver mbDepth cutPoints terminals substPat
156+
performRewrite doTracing def mLlvmLibrary solver substVars mbDepth cutPoints terminals substPat
150157
SMT.finaliseSolver solver
151158
stop <- liftIO $ getTime Monotonic
152159
let duration =

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

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,7 @@ data RewriteConfig = RewriteConfig
8080
{ definition :: KoreDefinition
8181
, llvmApi :: Maybe LLVM.API
8282
, smtSolver :: SMT.SMTContext
83+
, varsToAvoid :: Set.Set Variable
8384
, doTracing :: Flag "CollectRewriteTraces"
8485
, logger :: Logger LogMessage
8586
, prettyModifiers :: ModifiersRep
@@ -103,15 +104,18 @@ runRewriteT ::
103104
KoreDefinition ->
104105
Maybe LLVM.API ->
105106
SMT.SMTContext ->
107+
Set.Set Variable ->
106108
SimplifierCache ->
107109
RewriteT io a ->
108110
io (Either (RewriteFailed "Rewrite") (a, SimplifierCache))
109-
runRewriteT doTracing definition llvmApi smtSolver cache m = do
111+
runRewriteT doTracing definition llvmApi smtSolver varsToAvoid cache m = do
110112
logger <- getLogger
111113
prettyModifiers <- getPrettyModifiers
112114
runExceptT
113115
. flip runStateT cache
114-
. flip runReaderT RewriteConfig{definition, llvmApi, smtSolver, doTracing, logger, prettyModifiers}
116+
. flip
117+
runReaderT
118+
RewriteConfig{definition, llvmApi, smtSolver, varsToAvoid, doTracing, logger, prettyModifiers}
115119
. unRewriteT
116120
$ m
117121

@@ -408,9 +412,10 @@ applyRule pat@Pattern{ceilConditions} rule =
408412
-- existential variables may be present in rule.rhs and rule.ensures,
409413
-- need to strip prefixes and freshen their names with respect to variables already
410414
-- present in the input pattern and in the unification substitution
411-
let varsFromInput = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
415+
varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
416+
let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
412417
varsFromSubst = Set.unions . map freeVariables . Map.elems $ subst
413-
forbiddenVars = varsFromInput <> varsFromSubst
418+
forbiddenVars = varsFromInput <> varsFromPattern <> varsFromSubst
414419
existentialSubst =
415420
Map.fromSet
416421
(\v -> Var $ freshenVar v{variableName = stripMarker v.variableName} forbiddenVars)
@@ -703,6 +708,8 @@ performRewrite ::
703708
KoreDefinition ->
704709
Maybe LLVM.API ->
705710
SMT.SMTContext ->
711+
-- | Variable names to avoid (for new existentials)
712+
Set.Set Variable ->
706713
-- | maximum depth
707714
Maybe Natural ->
708715
-- | cut point rule labels
@@ -711,7 +718,7 @@ performRewrite ::
711718
[Text] ->
712719
Pattern ->
713720
io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
714-
performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels terminalLabels pat = do
721+
performRewrite doTracing def mLlvmLibrary smtSolver varsToAvoid mbMaxDepth cutLabels terminalLabels pat = do
715722
(rr, RewriteStepsState{counter, traces}) <-
716723
flip runStateT rewriteStart $ doSteps False pat
717724
pure (counter, traces, rr)
@@ -804,6 +811,7 @@ performRewrite doTracing def mLlvmLibrary smtSolver mbMaxDepth cutLabels termina
804811
def
805812
mLlvmLibrary
806813
smtSolver
814+
varsToAvoid
807815
simplifierCache
808816
(withPatternContext pat' $ rewriteStep cutLabels terminalLabels pat')
809817
>>= \case

‎booster/test/rpc-integration/test-questionmark-vars/README.md

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -92,3 +92,31 @@ transition rules that unconditionally introduce a fresh variable in the configur
9292
<a-state> ?X2 </a-state>
9393
<b-state> ?X1 </b-state>
9494
```
95+
96+
5) _ques-and-substitution_
97+
98+
If a substitution `X ==K b` is supplied, it will be applied before rewriting.
99+
However, the variable `X` can still not be used because the substitution will also be returned in the result (for information).
100+
Therefore, the newly created variable cannot be `X0`.
101+
102+
_Input:_
103+
104+
```
105+
<k> #setAStateSymbolic </k>
106+
<a-state> ?X0 </a-state>
107+
<b-state> ?X </b-state>
108+
#And
109+
?X #Equals b #And ?X0 #Equals ?X1 #And ?X2 #Equals ?X3 // substitutions
110+
```
111+
112+
_Expected:_
113+
114+
```
115+
<k> .K </k>
116+
<a-state> ?X0 </a-state>
117+
<b-state> b </b-state>
118+
#And
119+
?X #Equals b #And ?X0 #Equals ?X1 #And ?X2 #Equals ?X3 // substitutions
120+
#And
121+
condition(?X4)
122+
```

‎booster/test/rpc-integration/test-questionmark-vars/response-one-ques-substitution.booster-dev

Lines changed: 225 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,225 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "stuck",
6+
"depth": 1,
7+
"state": {
8+
"term": {
9+
"format": "KORE",
10+
"version": 1,
11+
"term": {
12+
"tag": "App",
13+
"name": "Lbl'-LT-'generatedTop'-GT-'",
14+
"sorts": [],
15+
"args": [
16+
{
17+
"tag": "App",
18+
"name": "Lbl'-LT-'k'-GT-'",
19+
"sorts": [],
20+
"args": [
21+
{
22+
"tag": "App",
23+
"name": "dotk",
24+
"sorts": [],
25+
"args": []
26+
}
27+
]
28+
},
29+
{
30+
"tag": "App",
31+
"name": "Lbl'-LT-'a-state'-GT-'",
32+
"sorts": [],
33+
"args": [
34+
{
35+
"tag": "EVar",
36+
"name": "Var'Ques'X4",
37+
"sort": {
38+
"tag": "SortApp",
39+
"name": "SortState",
40+
"args": []
41+
}
42+
}
43+
]
44+
},
45+
{
46+
"tag": "App",
47+
"name": "Lbl'-LT-'b-state'-GT-'",
48+
"sorts": [],
49+
"args": [
50+
{
51+
"tag": "App",
52+
"name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
53+
"sorts": [],
54+
"args": []
55+
}
56+
]
57+
},
58+
{
59+
"tag": "App",
60+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
61+
"sorts": [],
62+
"args": [
63+
{
64+
"tag": "DV",
65+
"sort": {
66+
"tag": "SortApp",
67+
"name": "SortInt",
68+
"args": []
69+
},
70+
"value": "0"
71+
}
72+
]
73+
}
74+
]
75+
}
76+
},
77+
"substitution": {
78+
"format": "KORE",
79+
"version": 1,
80+
"term": {
81+
"tag": "And",
82+
"sort": {
83+
"tag": "SortApp",
84+
"name": "SortGeneratedTopCell",
85+
"args": []
86+
},
87+
"patterns": [
88+
{
89+
"tag": "Equals",
90+
"argSort": {
91+
"tag": "SortApp",
92+
"name": "SortState",
93+
"args": []
94+
},
95+
"sort": {
96+
"tag": "SortApp",
97+
"name": "SortGeneratedTopCell",
98+
"args": []
99+
},
100+
"first": {
101+
"tag": "EVar",
102+
"name": "Var'Ques'X",
103+
"sort": {
104+
"tag": "SortApp",
105+
"name": "SortState",
106+
"args": []
107+
}
108+
},
109+
"second": {
110+
"tag": "App",
111+
"name": "Lblb'Unds'QUESTIONMARK-VARS'Unds'State",
112+
"sorts": [],
113+
"args": []
114+
}
115+
},
116+
{
117+
"tag": "Equals",
118+
"argSort": {
119+
"tag": "SortApp",
120+
"name": "SortState",
121+
"args": []
122+
},
123+
"sort": {
124+
"tag": "SortApp",
125+
"name": "SortGeneratedTopCell",
126+
"args": []
127+
},
128+
"first": {
129+
"tag": "EVar",
130+
"name": "Var'Ques'X0",
131+
"sort": {
132+
"tag": "SortApp",
133+
"name": "SortState",
134+
"args": []
135+
}
136+
},
137+
"second": {
138+
"tag": "EVar",
139+
"name": "Var'Ques'X1",
140+
"sort": {
141+
"tag": "SortApp",
142+
"name": "SortState",
143+
"args": []
144+
}
145+
}
146+
},
147+
{
148+
"tag": "Equals",
149+
"argSort": {
150+
"tag": "SortApp",
151+
"name": "SortState",
152+
"args": []
153+
},
154+
"sort": {
155+
"tag": "SortApp",
156+
"name": "SortGeneratedTopCell",
157+
"args": []
158+
},
159+
"first": {
160+
"tag": "EVar",
161+
"name": "Var'Ques'X2",
162+
"sort": {
163+
"tag": "SortApp",
164+
"name": "SortState",
165+
"args": []
166+
}
167+
},
168+
"second": {
169+
"tag": "EVar",
170+
"name": "Var'Ques'X3",
171+
"sort": {
172+
"tag": "SortApp",
173+
"name": "SortState",
174+
"args": []
175+
}
176+
}
177+
}
178+
]
179+
}
180+
},
181+
"predicate": {
182+
"format": "KORE",
183+
"version": 1,
184+
"term": {
185+
"tag": "Equals",
186+
"argSort": {
187+
"tag": "SortApp",
188+
"name": "SortBool",
189+
"args": []
190+
},
191+
"sort": {
192+
"tag": "SortApp",
193+
"name": "SortGeneratedTopCell",
194+
"args": []
195+
},
196+
"first": {
197+
"tag": "DV",
198+
"sort": {
199+
"tag": "SortApp",
200+
"name": "SortBool",
201+
"args": []
202+
},
203+
"value": "true"
204+
},
205+
"second": {
206+
"tag": "App",
207+
"name": "Lblcondition'LParUndsRParUnds'QUESTIONMARK-VARS'Unds'Bool'Unds'State",
208+
"sorts": [],
209+
"args": [
210+
{
211+
"tag": "EVar",
212+
"name": "Var'Ques'X4",
213+
"sort": {
214+
"tag": "SortApp",
215+
"name": "SortState",
216+
"args": []
217+
}
218+
}
219+
]
220+
}
221+
}
222+
}
223+
}
224+
}
225+
}

0 commit comments

Comments
 (0)