Skip to content

Refuse to apply sort predicates to unevaluated terms #4133

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jberthold wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Refuse to apply sort predicates to unevaluated terms #4133

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
3efa529
Refuse to apply sort predicates to unevaluated terms
jberthold Dec 5, 2025
749cc19
redundant dolars :)
jberthold Dec 5, 2025
6691af7
adjust expectation for simplify-log test
jberthold Dec 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 33 additions & 0 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -844,6 +844,27 @@ applyEquations theory handler term = do
)
err

{- | A sort predicate equation is characterised by the following:
* Its lhs is a function application (of a symbol starting with 'Lblis', not checked)
* function argument is a singleton K sequence
* containing an injection of a Variable into the 'KItem' sort
* rhs is a boolean
* requires and ensures are both empty (i.e., plain "true" DVs)
* the rule has no location information
-}
isSortPredicate :: RewriteRule tag -> Bool
isSortPredicate rule
| SymbolApplication _funSym [] [arg] <- rule.lhs
, KSeq sort (Var v) <- arg -- implicitly: Injection sort KItem (Var v)
, v.variableSort == sort
, (rule.rhs == TrueBool || rule.rhs == FalseBool)
, [Predicate TrueBool] <- rule.requires -- , null rule.requires
, [Predicate TrueBool] <- rule.ensures -- , null rule.ensures
, UNKNOWN <- sourceRef rule.attributes =
True
| otherwise =
False

applyEquation ::
forall io tag.
LoggerMIO io =>
Expand All @@ -852,6 +873,18 @@ applyEquation ::
EquationT
io
(Either ((EquationT io () -> EquationT io ()) -> EquationT io (), ApplyEquationFailure) Term)
applyEquation (FunctionApplication _sym [] [Term term _]) rule
| isSortPredicate rule
, not term.isEvaluated =
-- sort predicates only match on a sort injection, unevaluated
-- function applications may create false negatives
getPrettyModifiers >>= \case
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
pure $
Left
( \ctxt -> ctxt $ logWarn "Refusing to apply sort predicate rule to an unevaluated term"
, IndeterminateMatch
)
applyEquation term rule =
runExceptT $
getPrettyModifiers >>= \case
Expand Down
30 changes: 30 additions & 0 deletions booster/test/rpc-integration/resources/sort-predicates.k
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
module TEST
imports BOOL
imports INT

// sorts involved
syntax Evaluation ::= Value | Stuff
syntax Value ::= Integer ( Int ) [symbol(Integer)]
syntax Stuff ::= Stuff() [symbol(Stuff)]
syntax Wrap ::= Wrap ( Int ) [symbol(Wrap)]

// lookup function, two-stage
// upper level, dispatching
syntax Evaluation ::= lookup ( Wrap ) [function, total, symbol(lookup), no-evaluators]
// The no-evaluators here leads to the HS backend evaluating it ^^^^^^^^^^^^^
rule [dispatch]: lookup(Wrap(N)) => lookup0(N) requires N %Int 1 ==Int 0

syntax Evaluation ::= lookup0 ( Int ) [function, total, symbol(lookup0)]
// ----------------------------------------------------
rule [notfound]: lookup0(_N) => Stuff() [owise]
rule [target]: lookup0(42) => Integer(42)

// test harness
syntax KItem ::= Run ( Int ) [symbol(Run)]
| Done ( Value ) [symbol(Done)]
| Fail ( Int ) [symbol(Fail)]

rule [run-done]: Run(I) => Done(Integer(I)) requires isValue( lookup(Wrap(I)) )
rule [run-fail]: Run(I) => Fail(I) [owise]

endmodule
3,060 changes: 3,060 additions & 0 deletions booster/test/rpc-integration/resources/sort-predicates.kore
View file
Open in desktop

Large diffs are not rendered by default.

100 changes: 84 additions & 16 deletions booster/test/rpc-integration/test-log-simplify-json/simplify-log.txt.golden
View file
Open in desktop

Large diffs are not rendered by default.

73 changes: 73 additions & 0 deletions booster/test/rpc-integration/test-sort-predicates/response-run-41.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"reason": "stuck",
"depth": 1,
"state": {
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "LblFail",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "41"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
}
}
}
80 changes: 80 additions & 0 deletions booster/test/rpc-integration/test-sort-predicates/response-run-42.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,80 @@
{
"jsonrpc": "2.0",
"id": 1,
"result": {
"reason": "stuck",
"depth": 1,
"state": {
"term": {
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "LblDone",
"sorts": [],
"args": [
{
"tag": "App",
"name": "LblInteger",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "42"
}
]
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
}
}
}
63 changes: 63 additions & 0 deletions booster/test/rpc-integration/test-sort-predicates/state-run-41.execute
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
{
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "LblRun",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "41"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
63 changes: 63 additions & 0 deletions booster/test/rpc-integration/test-sort-predicates/state-run-42.execute
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
{
"format": "KORE",
"version": 1,
"term": {
"tag": "App",
"name": "Lbl'-LT-'generatedTop'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "Lbl'-LT-'k'-GT-'",
"sorts": [],
"args": [
{
"tag": "App",
"name": "kseq",
"sorts": [],
"args": [
{
"tag": "App",
"name": "LblRun",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "42"
}
]
},
{
"tag": "App",
"name": "dotk",
"sorts": [],
"args": []
}
]
}
]
},
{
"tag": "App",
"name": "Lbl'-LT-'generatedCounter'-GT-'",
"sorts": [],
"args": [
{
"tag": "DV",
"sort": {
"tag": "SortApp",
"name": "SortInt",
"args": []
},
"value": "0"
}
]
}
]
}
}
2 changes: 1 addition & 1 deletion scripts/booster-integration-tests.sh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ for dir in $(ls -d test-*); do
name=${dir##test-}
echo "Running $name..."
case "$name" in
"a-to-f" | "diamond")
"a-to-f" | "diamond" | "sort-predicates")
SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
SERVER=$KORE_RPC_DEV ./runDirectoryTest.sh test-$name $@
SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name $@
Expand Down
Loading