Skip to content

Commit b88b8b6

Browse files
jbertholdjberthold
authored
Refuse to apply sort predicates to unevaluated terms (#4133)
Sort predicates in K (`isMySort : KItem -> Bool`) only match on the sort injection of the argument into `KItem`. Paraphrased: ``` rule isMySort(inj{MySort,KItem}(VAR)) => true rule isMySort( VAR ) => false [owise] ``` Therefore, the result is wrong in the presence of a function that may return a super-sort of the target sort. ``` syntax SuperSort ::= MySort | SomethingElse syntax SuperSort ::= f ( Int ) [function, total] ``` leads to a wrong matching result for a term `isMySort(f(0))`, which in kore would be `LblisMySort(kseq{}(inj{SortSuperSort{},SortKItem{}}(Lblf{}(\dv{SortInt}("0"))),dotk{}()))`. The matching routine would report a failed match due to the sorts being different in the sort injections. However, the sort injection would change as soon as f(0) gets evaluated (to an `A:MySort`). See added test for an example K program going wrong without the fix. The PR changes the evaluation routine to return an indeterminate match in case it detects a sort predicate applied to a function call. The iterative evaluation will (bottom-up) evaluate the function call in the next round and is ultimately able to evaluate the predicate. Fixes #4132
1 parent 978a558 commit b88b8b6

File tree

11 files changed

+3493
-23
lines changed

11 files changed

+3493
-23
lines changed

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

Lines changed: 33 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -844,6 +844,27 @@ applyEquations theory handler term = do
844844
)
845845
err
846846

847+
{- | A sort predicate equation is characterised by the following:
848+
* Its lhs is a function application (of a symbol starting with 'Lblis', not checked)
849+
* function argument is a singleton K sequence
850+
* containing an injection of a Variable into the 'KItem' sort
851+
* rhs is a boolean
852+
* requires and ensures are both empty (i.e., plain "true" DVs)
853+
* the rule has no location information
854+
-}
855+
isSortPredicate :: RewriteRule tag -> Bool
856+
isSortPredicate rule
857+
| SymbolApplication _funSym [] [arg] <- rule.lhs
858+
, KSeq sort (Var v) <- arg -- implicitly: Injection sort KItem (Var v)
859+
, v.variableSort == sort
860+
, (rule.rhs == TrueBool || rule.rhs == FalseBool)
861+
, [Predicate TrueBool] <- rule.requires -- , null rule.requires
862+
, [Predicate TrueBool] <- rule.ensures -- , null rule.ensures
863+
, UNKNOWN <- sourceRef rule.attributes =
864+
True
865+
| otherwise =
866+
False
867+
847868
applyEquation ::
848869
forall io tag.
849870
LoggerMIO io =>
@@ -852,6 +873,18 @@ applyEquation ::
852873
EquationT
853874
io
854875
(Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term)
876+
applyEquation (FunctionApplication _sym [] [Term term _]) rule
877+
| isSortPredicate rule
878+
, not term.isEvaluated =
879+
-- sort predicates only match on a sort injection, unevaluated
880+
-- function applications may create false negatives
881+
getPrettyModifiers >>= \case
882+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
883+
pure $
884+
Left
885+
( \ctxt -> ctxt $ logWarn "Refusing to apply sort predicate rule to an unevaluated term"
886+
, IndeterminateMatch
887+
)
855888
applyEquation term rule =
856889
runExceptT $
857890
getPrettyModifiers >>= \case

‎booster/test/rpc-integration/resources/sort-predicates.k‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module TEST
2+
imports BOOL
3+
imports INT
4+
5+
// sorts involved
6+
syntax Evaluation ::= Value | Stuff
7+
syntax Value ::= Integer ( Int ) [symbol(Integer)]
8+
syntax Stuff ::= Stuff() [symbol(Stuff)]
9+
syntax Wrap ::= Wrap ( Int ) [symbol(Wrap)]
10+
11+
// lookup function, two-stage
12+
// upper level, dispatching
13+
syntax Evaluation ::= lookup ( Wrap ) [function, total, symbol(lookup), no-evaluators]
14+
// The no-evaluators here leads to the HS backend evaluating it ^^^^^^^^^^^^^
15+
rule [dispatch]: lookup(Wrap(N)) => lookup0(N) requires N %Int 1 ==Int 0
16+
17+
syntax Evaluation ::= lookup0 ( Int ) [function, total, symbol(lookup0)]
18+
// ----------------------------------------------------
19+
rule [notfound]: lookup0(_N) => Stuff() [owise]
20+
rule [target]: lookup0(42) => Integer(42)
21+
22+
// test harness
23+
syntax KItem ::= Run ( Int ) [symbol(Run)]
24+
| Done ( Value ) [symbol(Done)]
25+
| Fail ( Int ) [symbol(Fail)]
26+
27+
rule [run-done]: Run(I) => Done(Integer(I)) requires isValue( lookup(Wrap(I)) )
28+
rule [run-fail]: Run(I) => Fail(I) [owise]
29+
30+
endmodule

‎booster/test/rpc-integration/resources/sort-predicates.kore‎

Lines changed: 3060 additions & 0 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden‎

Lines changed: 84 additions & 16 deletions
Large diffs are not rendered by default.

‎booster/test/rpc-integration/test-sort-predicates/response-run-41.json‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,73 @@
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": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "LblFail",
29+
"sorts": [],
30+
"args": [
31+
{
32+
"tag": "DV",
33+
"sort": {
34+
"tag": "SortApp",
35+
"name": "SortInt",
36+
"args": []
37+
},
38+
"value": "41"
39+
}
40+
]
41+
},
42+
{
43+
"tag": "App",
44+
"name": "dotk",
45+
"sorts": [],
46+
"args": []
47+
}
48+
]
49+
}
50+
]
51+
},
52+
{
53+
"tag": "App",
54+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
55+
"sorts": [],
56+
"args": [
57+
{
58+
"tag": "DV",
59+
"sort": {
60+
"tag": "SortApp",
61+
"name": "SortInt",
62+
"args": []
63+
},
64+
"value": "0"
65+
}
66+
]
67+
}
68+
]
69+
}
70+
}
71+
}
72+
}
73+
}

‎booster/test/rpc-integration/test-sort-predicates/response-run-42.json‎

Lines changed: 80 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
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": "kseq",
24+
"sorts": [],
25+
"args": [
26+
{
27+
"tag": "App",
28+
"name": "LblDone",
29+
"sorts": [],
30+
"args": [
31+
{
32+
"tag": "App",
33+
"name": "LblInteger",
34+
"sorts": [],
35+
"args": [
36+
{
37+
"tag": "DV",
38+
"sort": {
39+
"tag": "SortApp",
40+
"name": "SortInt",
41+
"args": []
42+
},
43+
"value": "42"
44+
}
45+
]
46+
}
47+
]
48+
},
49+
{
50+
"tag": "App",
51+
"name": "dotk",
52+
"sorts": [],
53+
"args": []
54+
}
55+
]
56+
}
57+
]
58+
},
59+
{
60+
"tag": "App",
61+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
62+
"sorts": [],
63+
"args": [
64+
{
65+
"tag": "DV",
66+
"sort": {
67+
"tag": "SortApp",
68+
"name": "SortInt",
69+
"args": []
70+
},
71+
"value": "0"
72+
}
73+
]
74+
}
75+
]
76+
}
77+
}
78+
}
79+
}
80+
}

‎booster/test/rpc-integration/test-sort-predicates/state-run-41.execute‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
{
2+
"format": "KORE",
3+
"version": 1,
4+
"term": {
5+
"tag": "App",
6+
"name": "Lbl'-LT-'generatedTop'-GT-'",
7+
"sorts": [],
8+
"args": [
9+
{
10+
"tag": "App",
11+
"name": "Lbl'-LT-'k'-GT-'",
12+
"sorts": [],
13+
"args": [
14+
{
15+
"tag": "App",
16+
"name": "kseq",
17+
"sorts": [],
18+
"args": [
19+
{
20+
"tag": "App",
21+
"name": "LblRun",
22+
"sorts": [],
23+
"args": [
24+
{
25+
"tag": "DV",
26+
"sort": {
27+
"tag": "SortApp",
28+
"name": "SortInt",
29+
"args": []
30+
},
31+
"value": "41"
32+
}
33+
]
34+
},
35+
{
36+
"tag": "App",
37+
"name": "dotk",
38+
"sorts": [],
39+
"args": []
40+
}
41+
]
42+
}
43+
]
44+
},
45+
{
46+
"tag": "App",
47+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
48+
"sorts": [],
49+
"args": [
50+
{
51+
"tag": "DV",
52+
"sort": {
53+
"tag": "SortApp",
54+
"name": "SortInt",
55+
"args": []
56+
},
57+
"value": "0"
58+
}
59+
]
60+
}
61+
]
62+
}
63+
}

‎booster/test/rpc-integration/test-sort-predicates/state-run-42.execute‎

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
{
2+
"format": "KORE",
3+
"version": 1,
4+
"term": {
5+
"tag": "App",
6+
"name": "Lbl'-LT-'generatedTop'-GT-'",
7+
"sorts": [],
8+
"args": [
9+
{
10+
"tag": "App",
11+
"name": "Lbl'-LT-'k'-GT-'",
12+
"sorts": [],
13+
"args": [
14+
{
15+
"tag": "App",
16+
"name": "kseq",
17+
"sorts": [],
18+
"args": [
19+
{
20+
"tag": "App",
21+
"name": "LblRun",
22+
"sorts": [],
23+
"args": [
24+
{
25+
"tag": "DV",
26+
"sort": {
27+
"tag": "SortApp",
28+
"name": "SortInt",
29+
"args": []
30+
},
31+
"value": "42"
32+
}
33+
]
34+
},
35+
{
36+
"tag": "App",
37+
"name": "dotk",
38+
"sorts": [],
39+
"args": []
40+
}
41+
]
42+
}
43+
]
44+
},
45+
{
46+
"tag": "App",
47+
"name": "Lbl'-LT-'generatedCounter'-GT-'",
48+
"sorts": [],
49+
"args": [
50+
{
51+
"tag": "DV",
52+
"sort": {
53+
"tag": "SortApp",
54+
"name": "SortInt",
55+
"args": []
56+
},
57+
"value": "0"
58+
}
59+
]
60+
}
61+
]
62+
}
63+
}

‎scripts/booster-integration-tests.sh‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ for dir in $(ls -d test-*); do
2828
name=${dir##test-}
2929
echo "Running $name..."
3030
case "$name" in
31-
"a-to-f" | "diamond")
31+
"a-to-f" | "diamond" | "sort-predicates")
3232
SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
3333
SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
3434
SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@

0 commit comments

Comments
 (0)