Generic abstract domains and strategy solvers #141

viktormalik · 2020-03-31T07:42:30Z

This PR implements several generic domains and corresponding strategy solvers:

A generic simple strategy solver that is now a base of all simple abstract domains (tpolyhedra, heap, equalities, predabs, linrank, lexlinrank). The domain defines a standard form of template (composed of template rows) and methods that are common for many domains.
A generic product domain. The domain can contain any number of arbitrary domains and infers invariants in these domains side-by-side.
A generic domain with symbolic paths that can take an arbitrary inner domain and infer multiple invariants in the inner domains for different symbolic paths.

For more implementation details, see individual commit messages.

The existing domains, especially the heap domain, are simplified. Also, the inter-procedural heap analysis is removed since it does not work and is quite confusing in the code.

The CLI interface of 2LS has been altered w.r.t. the above changes. Every simple domain has its own CLI option and if multiple of them are specified, a product domain is used.

src/domains/Makefile

peterschrammel · 2020-04-01T19:17:31Z

src/domains/domain.h

+    /// Each abstract value needs to implement clone with covariant return type.
+    /// This is needed to properly clone abstract value when only a pointer to
+    /// valuet is available.
+    virtual valuet *clone()=0;


🚫 Why is the return value a pointer? Who is cleaning up the instances?

This is because returning covariant types cannot be implemented with unique_ptr. I added a comment that the caller is responsible for taking ownership of the cloned object (ideally by enclosing it into a unique_ptr).

peterschrammel · 2020-04-01T19:19:15Z

src/domains/heap_tpolyhedra_sympath_domain.h


 class heap_tpolyhedra_sympath_domaint:public domaint
 {
 public:
-  heap_tpolyhedra_domaint heap_tpolyhedra_domain;
+  product_domaint *heap_tpolyhedra_domain;


🚫 Use unique_ptr wherever possible.

I refactored all the work with abstract domains, values, and strategy solvers to use unique_ptr only. It is implemented as a separate commit.

peterschrammel · 2020-04-01T19:21:02Z

src/domains/strategy_solver_heap_tpolyhedra_sympath.cpp

@@ -9,7 +9,7 @@ Author: Viktor Malik
 /// \file
 /// Strategy solver for heap-tpolyhedra domain using symbolic paths

-// #define DEBUG
+#define DEBUG


spurious change

The file gets completely rewritten in one of the following commits, should I fix this particular commit anyway?

src/2ls/version.h

peterschrammel · 2020-04-01T19:27:17Z

That's a massive clean up that simplifies the code a lot! Thanks for this great piece of work!

Remove a lot of legacy code that is not used anymore. The code is related to 2 unused features: - distinguishing of stack and heap template rows - heap rows proved to be useless - interprocedural heap analysis Removal of the code improves clarity and eases understanding of the domain.

The analysis is not used since it does not work. Therefore, ssa_heap_analysis can be removed. ssa_heap_analysis was a static analysis used to determine dynamic objects that may have been created/altered by a function call and based on the results of this analysis, appropriate abstractions were created.

viktormalik · 2020-06-10T10:02:24Z

@peterschrammel Since we started to use unique_ptr, it would make sense to compile with C++14 to have std::make_unique available (to simplify the code). What do you think?

Add function for printing the value assigned to an expression and to all its sub-expressions by the SMT solver. This can be used for debugging the invariant inferrence.

The generic domain contains features and methods that are common for all (or at least for a number of) simple abstract domains. These are in particular: - template is a vector of template rows - template row contains a row expression (defined per-domain) and guards - abstract value is defined per-domain - each abstract value needs to implement a method returning an expression corresponding to the current value of a template row - generic simple domain contains a vector of expressions whose values need to be retrieved from the SMT model and a vector to store these values (this replaces the get_required_smt_values and got_values methods that the domain had to implement) - getting pre- and post- constraints has a generic implementation: - pre-constraint is a conjunction of row pre-constraints - row pre-constraint has form: pre_guard => row_value_expr - post-constraint is a disjunction of row post-constraints - row post constraint has a form: aux_expr && not(post_guard => row_value_expr) - projection of abstract value on a set of variables has a generic implementation: projection is a conjunction of pre-constraints of all template rows such that all variables that the template row describes are in the set of variables to project onto - methods for printing variable specs, template, and abstract value have generic implementations strategy_solvert is renamed to strategy_solver_simplet to reflect the fact that it works with the generic simple domain. Domains may re-implement the default behaviour. All existing simple domains are refactored to be based on the generic domain, using as much of the generic implementation as possible. There are some important implementation details and changes to mention: - template row (or var spec) kind, pre_guard, post_guard, and aux_expr are merged into a new struct guardst - guardts, var_spect, and related typedefs were moved out of domaint to be separate classes (or structs) - many simple domain methods were moved into template row expression or into abstract value where it makes sense (better encapsulation)

The domain can contain multiple arbitrary abstract domains that are used side-by-side. The invariant for each domain is computed individually in parallel with invariants for other domains. Moreover, candidate invariant (abstract value computed so far) from one domain is used as a context to strengthen invariant inference in all other domains. Heap-tpolyhedra domain is completely replaced by the new product domain. There is an important addition to the general abstract value interface - each abstract value needs to implement a clone method with covariant return type. This is especially needed for the product domain so that it can be properly cloned (clone is used by domain with symbolic paths).

Add new abstract domain for inference of different invariants in different program symbolic paths. The invariants can be inferred in an arbitrary domain. However, the inner domain must support working with symbolic paths, which in particular means: - implement restriction of template to symbolic paths - strategy solver of the inner domain must set the symbolic path that it found during solving - in case the domain infers multiple invariants (e.g. the product domain), its solver must make sure that all invariants in a single solver iteration are inferred for the same symbolic path heap_tpolyhedra_sympath_domain is replaced by the new generic domain.

The 2LS interface now allows to specify multiple simple domains to use. These include --heap, --equalities, and all value domains. If mutliple domains are specified, a product domain is created and invariants are inferred in all domains in parallel. Since the domains are created in template_generator_base while the strategy solvers and abstract values are created in ssa_analyzer, it is required that the order of simple domains/solvers/values within the product domain/solver/value is always the same. CLI options of all tests are ported to the new interface.

Instead of using raw pointers and managing memory manually, start using unique_ptr. If an object contains a unique_ptr to another object as a member, it is the owner. In particular: - template generator owns the abstract domain - ssa analyzer owns the abstract value - ssa analyzer owns the strategy solver (as a local variable in operator()) - product domain owns the inner domains, likewise for the product value and for the product strategy solver - sympath domain owns the inner domain, likewise for the sympath solver - sympath value owns all the inner values for individual symbolic paths, it also owns the inner value template Generic abstract value has an abstract method "clone" that returns a covariant type. Since this cannot be implemented using unique_ptr, it returns a raw pointer. The caller is therefore responsible for taking ownership of the cloned object.

peterschrammel · 2020-07-24T10:51:13Z

Thanks. I'll have a look asap.

Instead of allocating strategy solvers and abstract values in ssa_analyzer based on CLI options, make domains responsible for allocating adequate solvers. Each abstract domain must implement methods new_value and new_strategy_solver that return a unique_ptr to a new abstract value and new strategy solver for the domain, respectively. These methods are then called from ssa_analyzer, which simplifies the code a lot. This change required some unification of interfaces of strategy solver constructors.

peterschrammel reviewed Apr 1, 2020

View reviewed changes

peterschrammel assigned viktormalik Apr 18, 2020

viktormalik added 2 commits June 9, 2020 16:44

viktormalik force-pushed the generic-solvers branch from 78b101a to 0361525 Compare June 10, 2020 09:51

viktormalik force-pushed the generic-solvers branch from 0361525 to 0e2a2ed Compare June 10, 2020 10:45

viktormalik added 7 commits July 3, 2020 12:01

Printing SMT model in strategy solver

7062dfb

Add function for printing the value assigned to an expression and to all its sub-expressions by the SMT solver. This can be used for debugging the invariant inferrence.

Remove unused include from summary_checker_kindt

65a8c9b

viktormalik force-pushed the generic-solvers branch from 0e2a2ed to 3845dbf Compare July 3, 2020 10:01

viktormalik force-pushed the generic-solvers branch 3 times, most recently from 87d2ef5 to 69d2d58 Compare July 24, 2020 09:53

viktormalik added 2 commits July 27, 2020 09:30

Version 0.9.0

90c3c63

viktormalik force-pushed the generic-solvers branch from 69d2d58 to 90c3c63 Compare July 27, 2020 07:30

peterschrammel approved these changes Jul 27, 2020

View reviewed changes

peterschrammel merged commit b856541 into diffblue:master Jul 27, 2020

viktormalik deleted the generic-solvers branch December 8, 2020 14:53

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Generic abstract domains and strategy solvers #141

Generic abstract domains and strategy solvers #141

Uh oh!

viktormalik commented Mar 31, 2020

Uh oh!

Uh oh!

peterschrammel Apr 1, 2020

Uh oh!

viktormalik Jun 10, 2020

Uh oh!

peterschrammel Apr 1, 2020

Uh oh!

viktormalik Jun 10, 2020

Uh oh!

peterschrammel Apr 1, 2020

Uh oh!

viktormalik Jun 10, 2020

Uh oh!

Uh oh!

peterschrammel commented Apr 1, 2020

Uh oh!

viktormalik commented Jun 10, 2020

Uh oh!

peterschrammel commented Jul 24, 2020

Uh oh!

Uh oh!

Generic abstract domains and strategy solvers #141

Generic abstract domains and strategy solvers #141

Uh oh!

Conversation

viktormalik commented Mar 31, 2020

Uh oh!

Uh oh!

peterschrammel Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

viktormalik Jun 10, 2020

Choose a reason for hiding this comment

Uh oh!

peterschrammel Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

viktormalik Jun 10, 2020

Choose a reason for hiding this comment

Uh oh!

peterschrammel Apr 1, 2020

Choose a reason for hiding this comment

Uh oh!

viktormalik Jun 10, 2020

Choose a reason for hiding this comment

Uh oh!

Uh oh!

peterschrammel commented Apr 1, 2020

Uh oh!

viktormalik commented Jun 10, 2020

Uh oh!

peterschrammel commented Jul 24, 2020

Uh oh!

Uh oh!