Skip to content

Releases: ptal/turbo

Release v1.2.0

10 Sep 11:33

Choose a tag to compare

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 of has_changed instead of BInc. B is not an abstract domain, just a lattice, which is what we want for has_changed (it does not represent logical information).
  • Remove has_changed from the argument list of tell and dtell. Instead we return true or false if 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 tell and dtell to join and meet, actually tell is essentially an "in-place join operator".
  • For abstract domain (vstore, ..): Rename tell to deduce, 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 than deduce).
  • Rename refine to deduce to follow the abstract satisfaction framework.
  • For abstract domain (vstore,...): Rename tell(AVar x, Dom dom) to embed, 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., x or x + 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 in vstore::embed.
  • Rename fun into project with a new signature CUDA 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 deinterpret an 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

10 Feb 15:00

Choose a tag to compare

OR-parallelism Pre-release
Pre-release
v0.4

V0.4, working or-parallelism.

v0.3

09 Feb 07:11

Choose a tag to compare

v0.3 Pre-release
Pre-release
Simplify stop criterion propagation loop.

Turbo, improved propagation stop condition

06 Feb 18:53

Choose a tag to compare

v0.2

Turbo version 0.2!

Turbo slow but functionnal version

06 Feb 14:51

Choose a tag to compare

Pre-release
v0.1

Turbo v0.1, fully functional.