Skip to content

Commit 2038fb5

Browse files
rv-auditorrv-auditor
committed
Merge remote-tracking branch 'origin/master' into release
2 parents 14bb544 + 6862e0b commit 2038fb5

File tree

12 files changed

+559
-26
lines changed

12 files changed

+559
-26
lines changed

‎booster/library/Booster/Definition/Ceil.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ computeCeilRule ::
101101
computeCeilRule mllvm def r@RewriteRule.RewriteRule{lhs, requires, rhs, attributes, computedAttributes}
102102
| null computedAttributes.notPreservesDefinednessReasons = pure Nothing
103103
| otherwise = do
104-
(res, _) <- runEquationT def mllvm Nothing mempty $ do
104+
(res, _) <- runEquationT def mllvm Nothing mempty mempty $ do
105105
lhsCeils <- Set.fromList <$> computeCeil lhs
106106
requiresCeils <- Set.fromList <$> concatMapM (computeCeil . coerce) (Set.toList requires)
107107
let subtractLHSAndRequiresCeils = (Set.\\ (lhsCeils `Set.union` requiresCeils)) . Set.fromList

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

Lines changed: 17 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -182,13 +182,13 @@ data EquationMetadata = EquationMetadata
182182
}
183183
deriving stock (Eq, Show)
184184

185-
startState :: SimplifierCache -> EquationState
186-
startState cache =
185+
startState :: SimplifierCache -> Set Predicate -> EquationState
186+
startState cache known =
187187
EquationState
188188
{ termStack = mempty
189189
, recursionStack = []
190190
, changed = False
191-
, predicates = mempty
191+
, predicates = known
192192
, cache
193193
}
194194

@@ -282,14 +282,15 @@ runEquationT ::
282282
Maybe LLVM.API ->
283283
Maybe SMT.SMTContext ->
284284
SimplifierCache ->
285+
Set Predicate ->
285286
EquationT io a ->
286287
io (Either EquationFailure a, SimplifierCache)
287-
runEquationT definition llvmApi smtSolver sCache (EquationT m) = do
288+
runEquationT definition llvmApi smtSolver sCache known (EquationT m) = do
288289
globalEquationOptions <- liftIO GlobalState.readGlobalEquationOptions
289290
logger <- getLogger
290291
prettyModifiers <- getPrettyModifiers
291292
(res, endState) <-
292-
flip runStateT (startState sCache) $
293+
flip runStateT (startState sCache known) $
293294
runExceptT $
294295
runReaderT
295296
m
@@ -394,10 +395,11 @@ evaluateTerm ::
394395
KoreDefinition ->
395396
Maybe LLVM.API ->
396397
Maybe SMT.SMTContext ->
398+
Set Predicate ->
397399
Term ->
398400
io (Either EquationFailure Term, SimplifierCache)
399-
evaluateTerm direction def llvmApi smtSolver =
400-
runEquationT def llvmApi smtSolver mempty
401+
evaluateTerm direction def llvmApi smtSolver knownPredicates =
402+
runEquationT def llvmApi smtSolver mempty knownPredicates
401403
. evaluateTerm' direction
402404

403405
-- version for internal nested evaluation
@@ -419,16 +421,15 @@ evaluatePattern ::
419421
SimplifierCache ->
420422
Pattern ->
421423
io (Either EquationFailure Pattern, SimplifierCache)
422-
evaluatePattern def mLlvmLibrary smtSolver cache =
423-
runEquationT def mLlvmLibrary smtSolver cache . evaluatePattern'
424+
evaluatePattern def mLlvmLibrary smtSolver cache pat =
425+
runEquationT def mLlvmLibrary smtSolver cache pat.constraints . evaluatePattern' $ pat
424426

425427
-- version for internal nested evaluation
426428
evaluatePattern' ::
427429
LoggerMIO io =>
428430
Pattern ->
429431
EquationT io Pattern
430-
evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
431-
pushConstraints constraints
432+
evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
432433
newTerm <- withTermContext term $ evaluateTerm' BottomUp term
433434
-- after evaluating the term, evaluate all (existing and
434435
-- newly-acquired) constraints, once
@@ -455,7 +456,7 @@ evaluateConstraints ::
455456
Set Predicate ->
456457
io (Either EquationFailure (Set Predicate), SimplifierCache)
457458
evaluateConstraints def mLlvmLibrary smtSolver cache =
458-
runEquationT def mLlvmLibrary smtSolver cache . evaluateConstraints'
459+
runEquationT def mLlvmLibrary smtSolver cache mempty . evaluateConstraints'
459460

460461
evaluateConstraints' ::
461462
LoggerMIO io =>
@@ -948,10 +949,11 @@ simplifyConstraint ::
948949
Maybe LLVM.API ->
949950
Maybe SMT.SMTContext ->
950951
SimplifierCache ->
952+
Set Predicate ->
951953
Predicate ->
952954
io (Either EquationFailure Predicate, SimplifierCache)
953-
simplifyConstraint def mbApi mbSMT cache (Predicate p) = do
954-
runEquationT def mbApi mbSMT cache $ (coerce <$>) . simplifyConstraint' True $ p
955+
simplifyConstraint def mbApi mbSMT cache knownPredicates (Predicate p) = do
956+
runEquationT def mbApi mbSMT cache knownPredicates $ (coerce <$>) . simplifyConstraint' True $ p
955957

956958
simplifyConstraints ::
957959
LoggerMIO io =>
@@ -962,7 +964,7 @@ simplifyConstraints ::
962964
[Predicate] ->
963965
io (Either EquationFailure [Predicate], SimplifierCache)
964966
simplifyConstraints def mbApi mbSMT cache ps =
965-
runEquationT def mbApi mbSMT cache $
967+
runEquationT def mbApi mbSMT cache mempty $
966968
concatMap splitAndBools
967969
<$> mapM ((coerce <$>) . simplifyConstraint' True . coerce) ps
968970

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

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -353,7 +353,7 @@ applyRule pat@Pattern{ceilConditions} rule =
353353
<+> (hsep . punctuate comma . map (pretty' @mods) $ knownTrue)
354354

355355
unclearRequires <-
356-
catMaybes <$> mapM (checkConstraint id notAppliedIfBottom) toCheck
356+
catMaybes <$> mapM (checkConstraint id notAppliedIfBottom prior) toCheck
357357

358358
-- check unclear requires-clauses in the context of known constraints (prior)
359359
mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
@@ -403,7 +403,7 @@ applyRule pat@Pattern{ceilConditions} rule =
403403
Set.toList rule.ensures
404404
trivialIfBottom = RewriteRuleAppT $ pure Trivial
405405
newConstraints <-
406-
catMaybes <$> mapM (checkConstraint id trivialIfBottom) ruleEnsures
406+
catMaybes <$> mapM (checkConstraint id trivialIfBottom prior) ruleEnsures
407407

408408
-- check all new constraints together with the known side constraints
409409
whenJust mbSolver $ \solver ->
@@ -450,17 +450,17 @@ applyRule pat@Pattern{ceilConditions} rule =
450450
checkConstraint ::
451451
(Predicate -> a) ->
452452
RewriteRuleAppT (RewriteT io) (Maybe a) ->
453+
Set.Set Predicate ->
453454
Predicate ->
454455
RewriteRuleAppT (RewriteT io) (Maybe a)
455-
checkConstraint onUnclear onBottom p = do
456+
checkConstraint onUnclear onBottom knownPredicates p = do
456457
RewriteConfig{definition, llvmApi, smtSolver} <- lift $ RewriteT ask
457458
oldCache <- lift . RewriteT . lift $ get
458459
(simplified, cache) <-
459460
withContext CtxConstraint $
460-
simplifyConstraint definition llvmApi smtSolver oldCache p
461+
simplifyConstraint definition llvmApi smtSolver oldCache knownPredicates p
461462
-- update cache
462463
lift . RewriteT . lift . modify $ const cache
463-
-- TODO should we keep the traces? Or only on success?
464464
case simplified of
465465
Right (Predicate FalseBool) -> onBottom
466466
Right (Predicate TrueBool) -> pure Nothing

‎booster/test/rpc-integration/resources/use-path-condition-in-equations.k‎

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
module USE-PATH-CONDITION-IN-EQUATIONS
2+
imports INT
3+
imports BOOL
4+
5+
syntax State ::= test1Init()
6+
| test1State1()
7+
| test1State2()
8+
9+
| test2Init()
10+
| test2State1()
11+
| test2State2()
12+
13+
syntax Int ::= test1F ( Int ) [function, total, no-evaluators]
14+
| test2F ( Int ) [function, total, no-evaluators]
15+
16+
configuration <k> $PGM:State ~> .K </k>
17+
<int> 0:Int </int>
18+
19+
////////////////////////////////////////////////////////////////////////////////
20+
// Here the simplification's side condition is syntactically present //
21+
// in the path condition and is not checked. //
22+
// Result: Stuck at depth 2 in state test1State2() //
23+
// after applying rules test1-init,test1-1-2 //
24+
////////////////////////////////////////////////////////////////////////////////
25+
rule [test1-init]: <k> test1Init() => test1State1() ... </k>
26+
<int> _ => ?X </int>
27+
ensures ?X ==Int 42
28+
29+
rule [test1-1-2]: <k> test1State1() => test1State2() ... </k>
30+
<int> X </int>
31+
requires test1F(X) >Int 0
32+
33+
rule [test1F-simplify]: test1F(X:Int) => X requires X ==Int 42 [simplification]
34+
35+
////////////////////////////////////////////////////////////////////////////////
36+
// Here the simplification's side condition is implied by the path condition, //
37+
// but we need an SMT solver to establish that. //
38+
// Result: Aborted at depth 1 due to indeterminate condition of rule test2-1-2 //
39+
////////////////////////////////////////////////////////////////////////////////
40+
rule [test2-init]: <k> test2Init() => test2State1() ... </k>
41+
<int> _ => ?X </int>
42+
ensures ?X ==Int 42
43+
44+
rule [test2-1-2]: <k> test2State1() => test2State2() ... </k>
45+
<int> X </int>
46+
requires test2F(X) >Int 0
47+
48+
rule [test2F-simplify]: test2F(X:Int) => X requires X >Int 0 [simplification]
49+
50+
// to produce input state:
51+
// krun --output kore --depth 1 -cPGM='test1Init()' | kore-parser test-kompiled/definition.kore --module TEST --pattern /dev/stdin --print-pattern-json > state-test1Init.json
52+
// then edit state-test1Init.json to substitute test1State1() for test1Init()
53+
54+
endmodule

‎booster/test/rpc-integration/resources/use-path-condition-in-equations.kompile‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
echo "kompiling use-path-condition-in-equations.k"
2+
kompile --backend haskell use-path-condition-in-equations.k
3+
cp use-path-condition-in-equations-kompiled/definition.kore use-path-condition-in-equations.kore
4+
rm -r use-path-condition-in-equations-kompiled

‎booster/test/rpc-integration/test-use-path-condition-in-equations/README.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Test the use of the known path condition when applying simplifications
2+
3+
See `../resourses/use-path-condition-in-equations.k`.

‎booster/test/rpc-integration/test-use-path-condition-in-equations/response-test1.json‎

Lines changed: 148 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,148 @@
1+
{
2+
"jsonrpc": "2.0",
3+
"id": 1,
4+
"result": {
5+
"reason": "stuck",
6+
"depth": 2,
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": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "inj",
29+
"sorts": [
30+
{
31+
"tag": "SortApp",
32+
"name": "SortState",
33+
"args": []
34+
},
35+
{
36+
"tag": "SortApp",
37+
"name": "SortKItem",
38+
"args": []
39+
}
40+
],
41+
"args": [
42+
{
43+
"tag": "App",
44+
"name": "Lbltest1State2'LParRParUnds'USE-PATH-CONDITION-IN-EQUATIONS'Unds'State",
45+
"sorts": [],
46+
"args": []
47+
}
48+
]
49+
},
50+
{
51+
"tag": "App",
52+
"name": "dotk",
53+
"sorts": [],
54+
"args": []
55+
}
56+
]
57+
}
58+
]
59+
},
60+
{
61+
"tag": "App",
62+
"name": "Lbl'-LT-'int'-GT-'",
63+
"sorts": [],
64+
"args": [
65+
{
66+
"tag": "EVar",
67+
"name": "Var'Ques'X",
68+
"sort": {
69+
"tag": "SortApp",
70+
"name": "SortInt",
71+
"args": []
72+
}
73+
}
74+
]
75+
},
76+
{
77+
"tag": "App",
78+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
79+
"sorts": [],
80+
"args": [
81+
{
82+
"tag": "DV",
83+
"sort": {
84+
"tag": "SortApp",
85+
"name": "SortInt",
86+
"args": []
87+
},
88+
"value": "0"
89+
}
90+
]
91+
}
92+
]
93+
}
94+
},
95+
"predicate": {
96+
"format": "KORE",
97+
"version": 1,
98+
"term": {
99+
"tag": "Equals",
100+
"argSort": {
101+
"tag": "SortApp",
102+
"name": "SortBool",
103+
"args": []
104+
},
105+
"sort": {
106+
"tag": "SortApp",
107+
"name": "SortGeneratedTopCell",
108+
"args": []
109+
},
110+
"first": {
111+
"tag": "DV",
112+
"sort": {
113+
"tag": "SortApp",
114+
"name": "SortBool",
115+
"args": []
116+
},
117+
"value": "true"
118+
},
119+
"second": {
120+
"tag": "App",
121+
"name": "Lbl'UndsEqlsEqls'Int'Unds'",
122+
"sorts": [],
123+
"args": [
124+
{
125+
"tag": "EVar",
126+
"name": "Var'Ques'X",
127+
"sort": {
128+
"tag": "SortApp",
129+
"name": "SortInt",
130+
"args": []
131+
}
132+
},
133+
{
134+
"tag": "DV",
135+
"sort": {
136+
"tag": "SortApp",
137+
"name": "SortInt",
138+
"args": []
139+
},
140+
"value": "42"
141+
}
142+
]
143+
}
144+
}
145+
}
146+
}
147+
}
148+
}

0 commit comments

Comments
 (0)