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

Misc. Enhancements to VPDomain #239

Closed
alexandernutz opened this issue Oct 5, 2017 · 1 comment
Closed

Misc. Enhancements to VPDomain #239

alexandernutz opened this issue Oct 5, 2017 · 1 comment
Assignees
@alexandernutz
Labels
abstract interpretation enhancement

Comments

@alexandernutz
Copy link
Member

The VPDomain is not perfect yet, things to be done as they come up:

  • improvements to precision
  • general bugfixes
@alexandernutz alexandernutz self-assigned this Oct 5, 2017
alexandernutz added a commit that referenced this issue Oct 5, 2017
@alexandernutz
#239, fix precision loss in WeakEquivalenceGraph.join (did not take i…
a109e0a 
…nto account strong equivalences)
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239 , hashCode and equals for EqNode (based on mTerm field)
cf347a5
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, equip eqnodes now can return a version of themselver where a su…
e5362ec 
…bnode has been replaced, before they could only replace direct children (currently unused)
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, added method CongruenceClosure.removeSimpleElementWithReplaceme…
27ff8e1 
…ntPreference -- should fix an unnecessary (and unintentional) precision loss in WeakEquivalenceEdgeLabel.projectElement
danieldietsch added a commit that referenced this issue Oct 6, 2017
@danieldietsch
see #239 -- add minimal example for assertion error in VpDomain
6302c88
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, hashCodes for all! (more precise: EqConstraint and related clas…
1d1e397 
…ses)
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, minor, related to EqConstraint.hashCode
0228e8a
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, CongruenceClosure.projectToElements now also keeps constraints …
af5109a 
…that refer to elements that are equivalent to an element in the parameter set (perhaps make removeSimpleElementWithReplacementPreference obsolete)
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, further precision fix to WeakEquivalenceGraph.join
4053290
alexandernutz added a commit that referenced this issue Oct 6, 2017
@alexandernutz
#239, after last commits, WeakEquivalenceEdgeLabel.projectElement may…
d57f190 
… introduce new nodes to weq labels --> added code that also adds them to the corresponding ground partial arrangement; dealt with implications for sanity checks (architecturally a bit "interesting" changes.. will look for improvements..)
danieldietsch added a commit that referenced this issue Oct 9, 2017
@danieldietsch
see #239 -- another minimal example for assertion error in vpdomain
29ba405
danieldietsch added a commit that referenced this issue Oct 9, 2017
@danieldietsch
see #239 -- example for StackOverflowError
2f81361
alexandernutz added a commit that referenced this issue Oct 9, 2017
@alexandernutz
#239, cleanup, remove some functionality that is not needed
1bb1c24
alexandernutz added a commit that referenced this issue Oct 9, 2017
@alexandernutz
#239, getting rid of ACTION dependency, as far as possible, intermedi…
9f68eef 
…ate commit
alexandernutz added a commit that referenced this issue Oct 9, 2017
@alexandernutz
#239, got rid of unnecessary parametrizations of classes with "ACTION"
22c0a46
alexandernutz added a commit that referenced this issue Oct 9, 2017
@alexandernutz
#239, the subpackages of vpdomain seemed overkill since the recent re…
4302c28 
…factoring, removed them
alexandernutz added a commit that referenced this issue Oct 10, 2017
@alexandernutz
#239, implemented VPDomain.createBottomState
041768f
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, reworking CongruenceClosure.removeSimpleElement, intermediate c…
031c484 
…ommit (no crashes on regressions, but still imprecision)
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, reworking CongruenceClosure.removeSimpleElement, towards gettin…
b7e1d42 
…g all the precision we had back
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, reworking how nodes are added during remove/project, fwcc case …
d7fd49c 
…implemented roweq case missing
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, intermediate commit
503a82a
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, introduce ICongruenceClosureElement.replace method (currently u…
dcd8c2e 
…nused)
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, rework CongruenceClosure.projectToElements (projected away too …
5cf3081 
…much before)
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, continued reworking remove, rework sanityChecks, rework Congrue…
7a59268 
…nceClosure.projectToElements
alexandernutz added a commit that referenced this issue Oct 11, 2017
@alexandernutz
#239, bugfixes, refine sanity checks
988d623
danieldietsch added a commit that referenced this issue Oct 12, 2017
@danieldietsch
see #239,#155, close #232, #155 -- add support for domains that use h…
ac23cbe 
…ierachical pre (i.e., VpDomain) to AbsIntHoareTripleChecker, remove FutureRcfgVariableProvider (not needed anymore after BoogieVar refactoring)
alexandernutz added a commit that referenced this issue Oct 25, 2017
@alexandernutz
#239, some more benchmark data
5a85b0f
alexandernutz added a commit that referenced this issue Oct 25, 2017
@alexandernutz
#239, refactorings, improved CongruenceClosure.removeSimpleElement, t…
96fce2e 
…owards using (Weq)CcManager instead of directly calling methods on CongruenceClosure
alexandernutz added a commit that referenced this issue Oct 30, 2017
@alexandernutz
#239, more code cleanup: moved mNodeToDependents up to CongruenceClos…
e11cc70 
…ure, more steps towards (Weq)CcManager
alexandernutz added a commit that referenced this issue Oct 30, 2017
@alexandernutz
#239, even more cleanup
8c0f0da
alexandernutz added a commit that referenced this issue Oct 30, 2017
@alexandernutz
#239, cleanup, steps towards flattening WeqEdges before meetWithWeqGpa
7620177
alexandernutz added a commit that referenced this issue Oct 31, 2017
@alexandernutz
#239, added capability to flatten all weq edges before doing "meetWit…
71ba6e5 
…hWeqGpa", fixed some corner cases, refactoring: move WeakEquivalenceEdgeLabel into its own file
alexandernutz added a commit that referenced this issue Nov 3, 2017
@alexandernutz
#239, bugfixes
ac5159f
alexandernutz added a commit that referenced this issue Nov 3, 2017
@alexandernutz
#239, bugfix + regression test
55085e0
alexandernutz added a commit that referenced this issue Nov 6, 2017
@alexandernutz
#239, add test case
659a8fc
alexandernutz added a commit that referenced this issue Nov 6, 2017
@alexandernutz
#239, minor improvements
041b9c3
alexandernutz added a commit that referenced this issue Nov 29, 2017
@alexandernutz
#239 refactoring: WeqCongruenceClosure no more inherits from Congruen…
4ae24a0 
…ceClosure
alexandernutz added a commit that referenced this issue Nov 30, 2017
@alexandernutz
#239, more refactoring
b662df7
alexandernutz added a commit that referenced this issue Dec 1, 2017
@alexandernutz
#239, added logging and debug mode flags in some places
726a2ab
alexandernutz added a commit that referenced this issue Dec 1, 2017
@alexandernutz
#239, towards doing all (Weq)CongruenceClosure operations through Weq…
2d4d0d0 
…CcManager/CcManager
alexandernutz added a commit that referenced this issue Dec 1, 2017
@alexandernutz
#239, pass WeakEquivalenceEdgeLabels around instead of their contents
781945f
alexandernutz added a commit that referenced this issue Dec 2, 2017
@alexandernutz
#239, making more use of WeqCcManager and CcManager, add smt-solver c…
b81df92 
…hecks for operations
alexandernutz added a commit that referenced this issue Dec 4, 2017
@alexandernutz
#239, more refactorings surrounding WeqCcManager, EqConstraintFactory
c1662f9
alexandernutz added a commit that referenced this issue Dec 5, 2017
@alexandernutz
#239, more steps towards useing WeqCcManager, CcManager
66cc184
alexandernutz added a commit that referenced this issue Dec 5, 2017
@alexandernutz
fix compile errors due to last #239 commit
e7c4d7c
alexandernutz added a commit that referenced this issue Dec 6, 2017
@alexandernutz
#239, *CcManager cont'd
5145e6c
alexandernutz added a commit that referenced this issue Dec 6, 2017
@alexandernutz
#239, refactoring: give CongruenceClosure its own subpackage
a13b60d
alexandernutz added a commit that referenced this issue Dec 6, 2017
@alexandernutz
#239, add some settings flags
a0a0a70
alexandernutz added a commit that referenced this issue Dec 6, 2017
@alexandernutz
#239, bugfix to WeakEquivalenceEdgeLabel.flatten, occured during mana…
71153c7 
…ger-refactoring
alexandernutz added a commit that referenced this issue Dec 6, 2017
@alexandernutz
#239, even more refactoring
a8deeb4
alexandernutz added a commit that referenced this issue Dec 7, 2017
@alexandernutz
#239, misc enhancements
937ca88
alexandernutz added a commit that referenced this issue Dec 8, 2017
@alexandernutz
#239, bug-chasing: added some assertions, comments
690e28c
alexandernutz added a commit that referenced this issue Dec 8, 2017
@alexandernutz
#239
cc66d94 
 - still working on *CcManager and freezing mechanics
 - fix a bug that was introduced when inheritance between WeqCongruenceClosure and CongruenceClosure was removed: WeqCongruenceClosure.addElement needs to call WeqCongruenceClosure.registerNewElement!
 - more assertions
 - pull out some constants into WeqSettings/CcSettings
@alexandernutz
Copy link
Member Author

Closing this as I don't seem to use it anymore. Using #285 mostly. Plan is to open more specific tickets when they come up.

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

@alexandernutz alexandernutz

Labels
abstract interpretation enhancement
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@danieldietsch @alexandernutz