Uses faster but approximating functions for [join], [narrow] and [add]:
in resulting maps (m, i), the inverse map [i] may contain variables that do
not appear in [m]. Do not fail when this is the case.

Fixes performance issues: the initialization of large arrays or structures
can lead to a very large number of relations or intervals.

Also, do not infer intervals on volatile lvalues.

- Includes both direct and indirect dependencies of variables.
- Avoids using Base.SetLattice.project.
- Properly catches Not_found error when a variable is not in relation in the
  state.

Also fixes [get_var_bases] function on missing variables.
This function is called by [relate] according to the [Relations] map, which is
an over-approximation of the relations really inferred in the state — it can
contains variables that do not belong to the state, so [get_var_bases] should
not crash in that case.

(Outside of the Variable module, which still differentiates variables and
lvalues for now.)

Infers intervals about lvalues and not only variables.
Registers in deps variables and lvalues for which an interval is inferred.

The order between variables in an octagon state now depends on the id of
hashconsed lvalues, which is not deterministic — unless option -deterministic
is set.

Valentin Perrelle authored 2 years ago and David Bühler committed 1 year ago

- remove variables present only left or only right during joins