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

Stack overflow #964

Closed
AllanBlanchard opened this issue Nov 22, 2023 · 2 comments · Fixed by #990
Closed

Stack overflow #964

AllanBlanchard opened this issue Nov 22, 2023 · 2 comments · Fixed by #990
Assignees
@bclement-ocp
Labels
bug

Comments

@AllanBlanchard
Copy link

The following file produces a stack overflow. Note that I don't know if it is provable or not, this is a reduced example.
bug.txt
@bclement-ocp bclement-ocp self-assigned this Nov 22, 2023
@bclement-ocp
Copy link
Collaborator

Thanks for the report. I can confirm the issue on both the development branch and Alt-Ergo 2.5.2. It looks like we are trying to substitute a term with another term that contains it, which is not going to work. I will investigate.

@bclement-ocp
Copy link
Collaborator

Great: this is a case where there are two separate AC symbols, and it turns out that we don't do things properly. We were just talking with @Gbury the other day and noticed that what Alt-Ergo implements is not actually what is described in the paper that's suppose to describe it, and that we should investigate this as it could be problematic… so this proves that, I guess.

The issue is as follows:

  • The bug.txt introduces an AC symbol gcd to compute the greatest common divisor.
  • Alt-Ergo treats the built-in multiplication as an AC symbol (but this should work with any other AC symbol)
  • At some point we try to solve: div(gcd(i1, 0), gcd(abs(i), i2))'*'i1 = gcd((-div(gcd(i1, 0), gcd(abs(i), i2))'*'i1),(0)) which is a term of the form a * b = gcd(-(a * b), c)
  • Because as symbols, * is an operator and gcd is a name, Ac.compare decides that the equation is properly oriented
  • Then we look while trying to apply the substitution a * b → gcd(-(a * b), c) to gcd(-(a * b), c).

Minimal reproducer:

logic ac u : int, int -> int
logic ac v : int, int -> int

goal g : v(0, 1) = u(-v(0, 1), 2)

(Side note: v(0, 1) = u(v(0, 1), 2) actually works because Alt-Ergo performs a variant of the abstraction procedure described in the paper for nested AC symbols in Ac.abstract2)

bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 24, 2023
@bclement-ocp
fix(AC): Also abstract non-AC arguments of AC symbols
b75802e 
Alt-Ergo uses an abstraction mechanism for the arguments of AC symbols
to ensure termination of the induced rewrite ordering without resorting
to a recursive path ordering.

This is described in section 6 of [this paper][1], except that the
implementation doesn't do exactly what is described there -- in
particular, it only abstracts nested AC symbols, which is an issue when
an argument is not an AC symbol but a semantic value that contains
another AC symbol.

This patch changes the `abstract2` function in `ac.ml`, where this
abstraction mechanism is implemented, to also introduce abstracted
constants for non-constant terms.

Fixes OCamlPro#964

[1]: https://arxiv.org/abs/1207.3262
@bclement-ocp bclement-ocp mentioned this issue Nov 24, 2023
Closed
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 28, 2023
@bclement-ocp
fix(AC): Also abstract non-AC arguments of AC symbols
b52ac0f 
Alt-Ergo uses an abstraction mechanism for the arguments of AC symbols
to ensure termination of the induced rewrite ordering without resorting
to a recursive path ordering.

This is described in section 6 of [this paper][1], except that the
implementation doesn't do exactly what is described there -- in
particular, it only abstracts nested AC symbols, which is an issue when
an argument is not an AC symbol but a semantic value that contains
another AC symbol.

This patch changes the `abstract2` function in `ac.ml`, where this
abstraction mechanism is implemented, to also introduce abstracted
constants for non-constant terms.

Fixes OCamlPro#964

[1]: https://arxiv.org/abs/1207.3262
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 29, 2023
@bclement-ocp
fix(AC): Abstract AC arguments that contain other AC symbols
8ab2d72 
This patch implements a variation of the abstraction mechanism described
in the AC(X) paper. This should hopefully ensure that we can't create
substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when
the AC symbols are identical, the AC theory uses a multiset ordering on
its argument, which prevent substitution cycles. But when the AC symbols
are different, only the symbols are compared, not the arguments, and so
we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of OCamlPro#974 that
should be closer in spirit to the implementation of the paper and
without the associated regressions.

Fixes OCamlPro#964
@bclement-ocp bclement-ocp mentioned this issue Nov 29, 2023
Merged
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Nov 29, 2023
@bclement-ocp
fix(AC): Abstract AC arguments that contain other AC symbols
7922507 
This patch implements a variation of the abstraction mechanism described
in the AC(X) paper. This should hopefully ensure that we can't create
substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when
the AC symbols are identical, the AC theory uses a multiset ordering on
its argument, which prevent substitution cycles. But when the AC symbols
are different, only the symbols are compared, not the arguments, and so
we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of OCamlPro#974 that
should be closer in spirit to the implementation of the paper and
without the associated regressions.

Fixes OCamlPro#964
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Feb 7, 2024
@bclement-ocp
fix(AC): Abstract AC arguments that contain other AC symbols
cf6748b 
This patch implements a variation of the abstraction mechanism described
in the AC(X) paper. This should hopefully ensure that we can't create
substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when
the AC symbols are identical, the AC theory uses a multiset ordering on
its argument, which prevent substitution cycles. But when the AC symbols
are different, only the symbols are compared, not the arguments, and so
we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of OCamlPro#974 that
should be closer in spirit to the implementation of the paper and
without the associated regressions.

Fixes OCamlPro#964
bclement-ocp added a commit to bclement-ocp/alt-ergo that referenced this issue Mar 14, 2024
@bclement-ocp
fix(AC): Abstract AC arguments that contain other AC symbols
7d9cec2 
This patch implements a variation of the abstraction mechanism described
in the AC(X) paper. This should hopefully ensure that we can't create
substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when
the AC symbols are identical, the AC theory uses a multiset ordering on
its argument, which prevent substitution cycles. But when the AC symbols
are different, only the symbols are compared, not the arguments, and so
we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of OCamlPro#974 that
should be closer in spirit to the implementation of the paper and
without the associated regressions.

Fixes OCamlPro#964
bclement-ocp added a commit that referenced this issue Mar 14, 2024
@bclement-ocp
fix(AC): Abstract AC arguments that contain other AC symbols (#990)
40a54f8 
This patch implements a variation of the abstraction mechanism described
in the AC(X) paper. This should hopefully ensure that we can't create
substitution cycles due to improper term ordering.

Note that the issue is related to comparing distinct AC symbols: when
the AC symbols are identical, the AC theory uses a multiset ordering on
its argument, which prevent substitution cycles. But when the AC symbols
are different, only the symbols are compared, not the arguments, and so
we must rely on the abstraction mechanism to prevent cycles.

This is a do-over of #974 that
should be closer in spirit to the implementation of the paper and
without the associated regressions.

Fixes #964
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@bclement-ocp bclement-ocp

Labels
bug
Projects
None yet
Milestone
No milestone
2 participants
@AllanBlanchard @bclement-ocp