Skip to content

Commit aa5984e

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 0f13799 + be64ead commit aa5984e

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)