Releases: ptal/turbo
Releases · ptal/turbo
Release v1.2.0
This refactoring is quite large with order reversal and changes in the abstract domain functions:
- Add the lattice type
B(Boolean lattice where true <= false) which is now the type ofhas_changedinstead ofBInc.Bis not an abstract domain, just a lattice, which is what we want for has_changed (it does not represent logical information). - Remove
has_changedfrom the argument list oftellanddtell. Instead we returntrueorfalseif it changed or not. It avoids having two versions of tell/dtell if we are interested in has_changed or not. - For abstract universe (primitive_upset, interval, Cartesian product, ...): Rename
tellanddtelltojoinandmeet, actually tell is essentially an "in-place join operator". - For abstract domain (vstore, ..): Rename
telltodeduce, because tell is essentially an idempotent refine operator (it models a constraint, but we only need to apply refine once for it to be taken into account, basically, there is no need of fixpoint, but it is still the same idea thandeduce). - Rename
refinetodeduceto follow the abstract satisfaction framework. - For abstract domain (vstore,...): Rename
tell(AVar x, Dom dom)toembed, this version of tell was implementing a specific version of what is called the accessibility semantics in abstract interpretation. Essentially, from a term (e.g.,xorx + y) and a domain, modify the abstract domain such that the result of the term is in the domain. We have a restricted version with variable only invstore::embed. - Rename
funintoprojectwith a new signatureCUDA constexpr void project(Sig fun, const local_type& x, const local_type& y)(Sig not a template, non-static version, *this is updated with the result). - Add to
deinterpretan allocator instead of always relying on the one of Env. - Reverse the lattice order.
- Rename primitive_upset to arith_bound.
- Remove BInc / BDec which were ill-defined. Use b.hpp (B) if a Boolean lattice is required.
OR-parallelism
v0.4 V0.4, working or-parallelism.
v0.3
Turbo, improved propagation stop condition
v0.2 Turbo version 0.2!
Turbo slow but functionnal version
v0.1 Turbo v0.1, fully functional.