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

VPDomain Optimization: handle disequalites between constants symbolically #162

Closed
alexandernutz opened this issue Apr 18, 2017 · 2 comments
Closed

VPDomain Optimization: handle disequalites between constants symbolically #162

alexandernutz opened this issue Apr 18, 2017 · 2 comments
Assignees
@alexandernutz
Labels
abstract interpretation

Comments

@alexandernutz
Copy link
Member

Right now the disequalities between nodes in the congruence closure that represent a constant are stored explicitly.
This may or may not be relevant to practical runtime in the future. The overhead grows quadratically in the number of constants in the program.
Can we handle these disequalities symbolically?
@alexandernutz alexandernutz self-assigned this Apr 18, 2017
alexandernutz added a commit that referenced this issue Sep 6, 2017
@alexandernutz
added basic literal management (in particular the abstract states hav…
cab12c0 
…e to know that their literals are pairwise unequal), #216, related to #162
@alexandernutz
Copy link
Member Author

This ticket is somewhat outdated.
Currently we have the solution to only introduce literals that are referred to by the current state, but for them we introduce all disequalities when adding them to a constraint.
I don't see a better solution at the moment.

@alexandernutz alexandernutz reopened this Sep 28, 2017
@alexandernutz
Copy link
Member Author

reopening because there is a new plan:

  • literal disequalites are not added explicitly anymore
  • getEqualityStatus, gets extra check for if elem1 and elem2's representative are different literals
  • literal treatment is moved up to CongruenceClosure (necessary anyway, becaus we need it on the weak equivalence edge labels)
  • CongruenceClosure has to make sure that if an equivalence class contains a literal, then that is chosen as the representative

alexandernutz added a commit that referenced this issue Sep 28, 2017
@alexandernutz
- towards better literal treatment in CongruenceClosure, #162
20cd2b5 
 - towards containing the explosion of WeakEquivalenceEdgeLabels ..
alexandernutz added a commit that referenced this issue Sep 28, 2017
@alexandernutz
- fixed bugs that were introduced during working on #162 (reportEqual…
740abf6 
…ityRec had some special cases where it referred to mElementTVER without checking for isLiteral)

 - fixed/completed reduction/minimization of WeakEquivalenceEdgeLabels, should solve (at least some) termination/runtime issues
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@alexandernutz alexandernutz

Labels
abstract interpretation
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@alexandernutz