search

diffblue / 2ls

Static Analyzer and Verifier
http://www.cprover.org/2LS
Other
43 stars 22 forks source link

Generic abstract domains and strategy solvers #141

Closed viktormalik closed 3 years ago

viktormalik commented 4 years ago

This PR implements several generic domains and corresponding strategy solvers:

  1. 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.
  2. A generic product domain. The domain can contain any number of arbitrary domains and infers invariants in these domains side-by-side.
  3. 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.

peterschrammel commented 4 years ago

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

viktormalik commented 4 years ago

@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?

peterschrammel commented 3 years ago

Thanks. I'll have a look asap.