Object domain #60
Closed
Object domain #60
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The decoupled domain allows crab to use two different domains during the two different phases of the analysis. In the descending (narrowing) phase it is possible to use an abstract domain which is more precise than the domain used in the ascending (widening) phase. The decoupled domains require two new abstract operations is_asc_phase() and set_phase() in order to manage ascending and descending phases. By default, start in *descending* (i.e., more precise) phase. The interleaved fixpoint iterator has been also modified to notify the underlying domains when there is change of (ascending or descending) phase. Implemented by Greta Dolcetti and Enea Zaffanella.
We minimize string allocation and copies. Also, we add some macros that allow each domain to turn on or off statistics collection which adds a counter and a timer per operation. If stats collection is off then no string allocation or string copy should take place. For instance, the region domain enables stats by adding And the interval domain disables stats by adding The macro CRAB_DOMAIN_SCOPED_STATS is defined in crab/domains/abstract_domain_macros.def In spite of all optimizations, the most efficient thing is to disable stats collection. By default, only the fixpoint solver and the region domain turn on stats. This is okay because stats gathering is a feature intended only for developers. If needed then the developer can turn on more stats timers and counters and recompile the code.
The master branch is ok. This was introduced in commit 8c0e07f.
We were using const T&& instead of T&& in copy and assignment operators. As part of the commit, I also try to use default as much as possible. Thanks to Enea Zaffanella to point out the problem with move operators
This macro always used this but it needs to use other in assignment constructors. The reason is that we can have T o1; T o2 = std::move(o1); o1 = o2; <-- o1 was moved, so CRAB_DOMAIN_SCOPED_STATS should not access to o1.domain_name() Thanks to Enea Zaffanella to find the problem and explain to me the issue
This fix is related to commit f04d015
A symbolic equality domain is an abstract domain which represents equalities used in analyses for allocation-site abstraction or domain reduction. In short, giving two program variables are known to hold equal values in concrete semantics if the analyzer determines that the variables hold equal symbolic term.
A collection of key and object value pairs for inferring properties based on DSA analysis. Basically, the domain keep three subdomains named as cache, summary and equality of fields. The summary domain keeps properties for all memory objects shared the same DSA node. The cache domain, however, only keep the Most Recently Used memory object by memory load / store instruction. The way to determine which memory object uses cache domain is depended on object domain. Meanwhile, an equality of fields abstract domain keeps equalities between register (or scalars) and fields.
A new abstract domain followed by a new memory abstraction based on DSA analysis to infer relational properties between fields. The domain is split into several subdomains in order to reduce the complexity of the anlysis. In terms of precision, the object domain maintain equalities property between memory load and store to refine the relational properties between fields. There also involves domain reduction for precision refinement. Overall, This is a new abstract domain for the refinement of DSA analysis to infer properties of memory objects.
Closed
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
A new abstract domain for the refinement of DSA. It keeps relational properties between the fields of memory objects shared in the same DSA node.