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 VPDomain work #159

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

Make VPDomain work #159

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

Comments

@alexandernutz
Copy link
Member

Fix remaining bugs, fix support for procedure calls, and whatever is necessary to get VPDomain running and producing sensible results on practical programs.
@alexandernutz alexandernutz self-assigned this Apr 11, 2017
alexandernutz referenced this issue Apr 12, 2017
@alexandernutz
- remove some erroneous assertions
6a01cc9 
 - catch bottom-state special case through overwriting remove-/addVariable methods
 - cosmetics
@alexandernutz
Copy link
Member Author

alexandernutz commented Apr 18, 2017 •
edited
Loading

New plan for VpTfStates:

  • move handleTransFormula into VpTfState, from VPPostOperator (probably)
  • add fields "inVariables" and "outVariables", indicating the scopes before/after the transition (roughly corresponding to inVars/outVars of TransFormulas, but with the full scope, i.e., including variables that the Transformula skips)
  • add method "patchIn(state)" that copies the relations in a state into the tfStates, using its In-Variables
  • add method "patchOut(state)" that copies the relations in the state into the given state, using the Out-Variables; also havocs assignedVars

Expected advantages:

  • support for Calls/Returns should be easy afterwards
  • avoids problem of the current solution where relations might get lost unnecessarily (because in the current solution TfStates only track variables that occur in the TransFormula, and thus sometimes loses relations to variables that are not in that set -- even on internal/non-context-switch transitions)

EDIT: this plan is made obsolete by the new one in Ticket #178

alexandernutz added a commit that referenced this issue Apr 18, 2017
@alexandernutz
refactoring, related to #159:
1341b0e 
 - moved code that does setup of tfStateBuilders from VPTfStateBuilder into new class CreateVanillaTfStateBuilder
 - rewrote the two VPPostOperator.apply(..) methods
 - the tfState applies its own TransFormula now -- moved methods that apply the TransFormula to VPTfState (handleEquality and others, from VPPostOperator)
alexandernutz added a commit that referenced this issue Apr 19, 2017
@alexandernutz
see #159 added computation of VPDomain-flavour inVars and outVars for…
e31910d 
… VPTfStateBuilders
alexandernutz added a commit that referenced this issue Apr 19, 2017
@alexandernutz
VPTfStates are now (primarily) associated with an IAction, not a Tran…
8de7e9f 
…sFormula, see #159
alexandernutz added a commit that referenced this issue Apr 19, 2017
@alexandernutz
instead of a new "patchOut"-method use tfStateFactory.projectToOutVar…
6037c06 
…s(..) and VPState.patch(..), see #159
alexandernutz added a commit that referenced this issue Apr 19, 2017
@alexandernutz
towards the new handling of transitions, prepared new node creation f…
d980e6d 
…or tfStates, see #159
alexandernutz added a commit that referenced this issue Apr 20, 2017
@alexandernutz
preparing for new creation of EqGraphNodes for TfStates, see #159
f117f7b
alexandernutz added a commit that referenced this issue Apr 20, 2017
@alexandernutz
local EqNodes know their procedure now. related to #159
b31a51a
alexandernutz added a commit that referenced this issue Apr 20, 2017
@alexandernutz
finished slight rework of CreateVanillaTfStateBuilder.createEqGraphNo…
cf8be3e 
…des(..), #159
alexandernutz added a commit that referenced this issue Apr 20, 2017
@alexandernutz
reimplemented VPState.patch(), #159
ff58df6
alexandernutz added a commit that referenced this issue Apr 20, 2017
@alexandernutz
improvements to VPState.patch(), #159
a84f860
alexandernutz added a commit that referenced this issue Apr 21, 2017
@alexandernutz
VPState.removeVariables(..) now also havocs the removed variables, to…
256a8cf 
…wards #159

 --> before, this led to failing "isPostSound"-checks, because the HoareTripleChecker seems to take the primed versions in the of variables that neither state nor the TransFormula does know for the  postcondition..
alexandernutz added a commit that referenced this issue Apr 25, 2017
@alexandernutz
fix for VPState variable handling wrt removeVariables and getTerm: re…
b7c6e83 
…moveVariables does not havoc anymore (we might lose information we want to keep), getTerm does not report (dis)equalities that contain variables that the state does not "officially" (indicated by its getVariables) know, see #159
alexandernutz added a commit that referenced this issue Apr 25, 2017
@alexandernutz
fixed CreateVanillaTfStateBuilder.createEqGraphNodes, finally, hopefu…
4f576be 
…lly, #159
alexandernutz added a commit that referenced this issue Apr 26, 2017
@alexandernutz
- VPDomainPreanalysis recognizes tracked arrays more generously now (…
1fa9894 
…C To Boogie and BoogieProcedureInliner introduce some renamings) (still not recognized: the memory array in the bitvector case)

 - VPState debug output now optionally shows equivalence classes instead of equivalence edges
 - minor cleanup
towards #159
alexandernutz added a commit that referenced this issue Apr 26, 2017
@alexandernutz
in order to account for array equalities in some (rather common) case…
96d2c83 
…s, we need more EqNodes than we created before.

Before we only created EqNodes corresponded to a term in a TransFormula of the program, now we ensure that if arrays a and b are equated they have the same accessing nodes each.
This means we now have EqNodes that do not correspond to a term in the program.
#159
alexandernutz added a commit that referenced this issue Apr 26, 2017
@alexandernutz
slight refactoring to VPState/VPTfState: moved some code into supercl…
429c9bb 
…ass, added extra debugging output mode, #159
alexandernutz added a commit that referenced this issue May 9, 2017
@alexandernutz
towards #159
12fe501 
 - introduced code that adds certain nodes into tfStates that are needed for exploiting array equations/extensionality
 - added comments
 - renamed VPTransFormulaStateBuilderPreparer.java
alexandernutz added a commit that referenced this issue May 9, 2017
@alexandernutz
in/outVars that are not in the transFormula need nodes in the tfState…
06c71dc 
…, too (and may not be represented by "through"-nodes!), #159
alexandernutz added a commit that referenced this issue May 9, 2017
@alexandernutz
- improved CreateVanillaTfStateBuilder.createEqGraphNodes(..): nodes …
3444585 
…for array equalities are inserted with a different strategy now.

- bugfixes
towards #159
alexandernutz added a commit that referenced this issue May 10, 2017
@alexandernutz
bugfix: when creating a VPTfNodeIdentifier for a subterm with many ar…
df78c69 
…guments, the projection of the inVars/outVars only projected away the function symbol, but it needs to project away the symbols of the other arguments, too!

related to #159
alexandernutz added a commit that referenced this issue May 10, 2017
@alexandernutz
simple reimplementation of disjoin
49d9d79 
other minor changes
#159
alexandernutz added a commit that referenced this issue May 10, 2017
@alexandernutz
fixes concerning when to use "addDisEquality" without/with propagatio…
e6596b5 
…ns, #159
@alexandernutz alexandernutz mentioned this issue May 17, 2017
Closed
alexandernutz added a commit that referenced this issue Jun 20, 2017
@alexandernutz
EqGraphNode: initCcpar needs to be a set, #159
0cf7a9c
alexandernutz added a commit that referenced this issue Jun 20, 2017
@alexandernutz
moved UnionFind functionalities from EqConstraint to ArrayEquivalence…
8b045b4 
…Graph, #159
alexandernutz added a commit that referenced this issue Jun 26, 2017
@alexandernutz
when returning a set of EqStates, we now ensure that all have the sam…
2b68a82 
…e "getVariables()"-result, #159
alexandernutz added a commit that referenced this issue Jun 26, 2017
@alexandernutz
- rewrote read-over-write axiom propagations for nested and multidime…
06af728 
…nsional cases (only tested nested so far..)

 - the variables of an EqState are now exclusively determined from the 'outside', not from the constraint it holds (modified EqDisjunctiveConstraint.toEqStates(..))
#159
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
towards #159, fixes and small changes
d7cf0e2 
 - pass over right method for merge operator
 - don't crash on unknown relation symbols (just use empty constraint)
 - bugfix: EqFunctionNode.getArgs() returned a writable list --> consequence: bugs
 - added some assertions in EqPostOperator, CongruenceGraph.havoc
 - fixed variable handling in EqState.union and EqState.intersect, also switched to hashing via int ids (not sure about the consequences..)
 - EqStateFactory caches the TopState (with no variables) now
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
improved EqState.isSubsetOf and EqState.isEqualTo methods by checking…
4470021 
… some simple cases involving "bottom" and "top" (turns out they are quite important for performance..)

as a consequence added emptiness check for EqConstraint (i.e. when the constraint is "top")
#159
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
bugfix: EqBottomConstraint needs to overwrite getTerm() (isPostSound …
d3ffcdd 
…reported wrong results because it did not, and yielded "true"), #159

to be safe overwrote everything from EqConstraint
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
VPDomainPreanalysis: added option/method "trackAllElements" --> if it…
26622a4 
… is set to true (currently hardcoded in VPDomainPreanalysis.Settings), then everything that occurs in a (dis)equation is tracked, #159
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
minor fixes, #159
70913a0
alexandernutz added a commit that referenced this issue Jun 27, 2017
@alexandernutz
- reintroduced using EqNonAtomicBaseNode (for example for tracking ar…
ce708a6 
…ithmetic expressions "as a whole"), using CommuHashNormalForm

 - minor changes,
#159
alexandernutz added a commit that referenced this issue Jun 28, 2017
@alexandernutz
added support for Boolean variables, #159
8cb2b7d
alexandernutz added a commit that referenced this issue Jun 28, 2017
@alexandernutz
fix to dubious havoc bug, (was exposed in many (not all) runs of regr…
ab08788 
…ession/all/bug-nonrelationalpost-smtidentifier.bpl), #159

cosmetics
alexandernutz added a commit that referenced this issue Jun 28, 2017
@alexandernutz
bugfixes: true/false EqNodes are now treated as Literals (i.e. are as…
a6a1fd2 
…sumed to be distict), only literals of the same sort are marked distinct in the CongruenceGraph, #159
alexandernutz added a commit that referenced this issue Jun 28, 2017
@alexandernutz
improves EqState.isSubsetOf implementation (checking subset between c…
ac0a475 
…onstraint sets), #159
alexandernutz added a commit that referenced this issue Jun 30, 2017
@alexandernutz
added remove method to UnionFind, commented weird workaround that we …
d838c42 
…had instead, #159
alexandernutz added a commit that referenced this issue Jun 30, 2017
@alexandernutz
bugfix to EqConstraint.getAllEqualities/Disequalities, #159
ca60b11
alexandernutz added a commit that referenced this issue Jun 30, 2017
@alexandernutz
fixes concerning return in equality domain, #159
a581709
alexandernutz added a commit that referenced this issue Jul 1, 2017
@alexandernutz
purged old-style EqNodes, i.e., based on IProgramVarOrConst, not on T…
71f3ab8 
…erms, #159, consequence of the changes in #178
alexandernutz added a commit that referenced this issue Jul 6, 2017
@alexandernutz
EqConstraintFactory, implemented propagateDisequalitiesFlat, complete…
3db9f22 
…d switch to "flat" methods, #159
alexandernutz added a commit that referenced this issue Jul 26, 2017
@alexandernutz
equality domain: CongruenceGraph can now return equivalence classes (…
526de98 
…as sets), added debugging option using that, #159
alexandernutz added a commit that referenced this issue Sep 7, 2017
@alexandernutz
improved Term normalization, we attempt to convert all base terms to …
d456621 
…an AffineTerm, and if that does not work, into CommuHashNormalForm, #159
alexandernutz added a commit that referenced this issue Sep 7, 2017
@alexandernutz
bugfixes
7114ab8 
 - script locking
 - AffineTermTransformer does not return an AffineTerm if fed with a TermVariabel -- needed to catch that case
#159
alexandernutz added a commit that referenced this issue Sep 7, 2017
@alexandernutz
weakened assert, #159
550945a
alexandernutz added a commit that referenced this issue Sep 8, 2017
@alexandernutz
EqNonAtomicBaseNodes can depend on arrays/functions, too, #159
2cbdcdb
alexandernutz added a commit that referenced this issue Sep 9, 2017
@alexandernutz
added some assertions, comment, #159
c2d4c91
alexandernutz added a commit that referenced this issue Sep 9, 2017
@alexandernutz
minor refactoring, #159
7af4e2e
alexandernutz added a commit that referenced this issue Sep 9, 2017
@alexandernutz
fix to StoreChainSquisher, #159
fe0318a
alexandernutz added a commit that referenced this issue Sep 9, 2017
@alexandernutz
check if array sorts match before introducing a weak equivalence betw…
c72293d 
…een them, #159
alexandernutz added a commit that referenced this issue Sep 11, 2017
@alexandernutz
minor changes, #159
a8cb0db
@alexandernutz
Copy link
Member Author

I consider the VPDomain as "roughly working" now. For further problems I will try to make more specific issues than this one.

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