Skip to content
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

Jump to bottom

Make the "simplify" endpoint in Booster evaluate inconsisten predicates and patterns to #Bottom #4012

Open
geo2a opened this issue Aug 1, 2024 · 0 comments · May be fixed by #4020
Open

Make the "simplify" endpoint in Booster evaluate inconsisten predicates and patterns to #Bottom #4012

geo2a opened this issue Aug 1, 2024 · 0 comments · May be fixed by #4020
Assignees
@geo2a

Comments

@geo2a
Copy link
Collaborator

geo2a commented Aug 1, 2024

The "simplify" endpoint in Booster, is different from what Kore does. When asked to simplify the state state-vacuous-but-rewritten.execute:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _=/=Int_(N:SortInt{}, "0")
    _==Int_(N:SortInt{}, "0")

which is a pattern with contradictory constraints, booster-dev returns the pattern almost unchanged:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _==Int_(N:SortInt{}, "0")
    notBool_(_==Int_(N:SortInt{}, "0"))

while kore-rpc-booster will return #Bottom (via Kore):

[request 1][proxy][timing] Performed SimplifyM in 0.45s (0.41s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628734/diff_file1.txt	2024-08-01 08:37:36.610508904 +0200
--- /tmp/extra-dir-51565986628734/diff_file2.txt	2024-08-01 08:37:36.610508904 +0200
***************
*** 1,9 ****
- Term:
-     <generatedTop>(
-         <k>(kseq("b", dotk())),
-         <int>(N:SortInt{}),
-         <generatedCounter>("0")
-     )
  Conditions:
!     _==Int_(N:SortInt{}, "0")
!     notBool_(_==Int_(N:SortInt{}, "0"))
\ No newline at end of file
--- 1,4 ----
  Conditions:
! Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

that means that ApplyEquations.evaluatePattern --- the function behind the "simplify" endpoint in Booster, is unable to detect a contradiction in constraints. And this is indeed the case, since it evaluates every constraint assuming all the others, but never calls Z3 on them together as we do when rewriting.

Same happens if we isolate the constraints and ask the servers to simplify that:

request 1][proxy][timing] Performed SimplifyM in 0.49s (0.47s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628735/diff_file1.txt	2024-08-01 08:40:47.352321295 +0200
--- /tmp/extra-dir-51565986628735/diff_file2.txt	2024-08-01 08:40:47.352321295 +0200
***************
*** 1,5 ****
  Conditions:
-     _==Int_(N:SortInt{}, "0")
-     notBool_(_==Int_(N:SortInt{}, "0"))
  Ceil conditions:
! Substitutions:
\ No newline at end of file
--- 1,4 ----
  Conditions:
  Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

and indeed, the "simplify" endpoint, when it receives predicates only, simplifies them in isolation and never checks their combined consistency.

I understand that this behaviour of the "simplify" endpoint in Booster is intentional, since, for most of its lifetime, Booster did not have an SMT solver and thus we've geared to towards simplifying constraints in isolation. It's time to change that.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@geo2a geo2a

Labels
None yet
Projects
None yet
Milestone
No milestone
1 participant
@geo2a