The decoupled domain allows crab to use two different domains during
the two different phases of the analysis.  In the descending
(narrowing) phase it is possible to use an abstract domain which is
more precise than the domain used in the ascending (widening) phase.

The decoupled domains require two new abstract operations
is_asc_phase() and set_phase() in order to manage ascending and
descending phases. By default, start in *descending* (i.e., more
precise) phase. The interleaved fixpoint iterator has been also
modified to notify the underlying domains when there is change of
(ascending or descending) phase.

Implemented by Greta Dolcetti and Enea Zaffanella.

We minimize string allocation and copies.  Also, we add some macros
that allow each domain to turn on or off statistics collection which
adds a counter and a timer per operation. If stats collection is off
then no string allocation or string copy should take place.

For instance, the region domain enables stats by adding

#define REGION_DOMAIN_SCOPED_STATS(NAME) CRAB_DOMAIN_SCOPED_STATS(NAME, 1)

And the interval domain disables stats by adding

#define INTERVALS_DOMAIN_SCOPED_STATS(NAME) CRAB_DOMAIN_SCOPED_STATS(NAME, 0)

The macro CRAB_DOMAIN_SCOPED_STATS is defined in
crab/domains/abstract_domain_macros.def

In spite of all optimizations, the most efficient thing is to disable
stats collection. By default, only the fixpoint solver and the region
domain turn on stats. This is okay because stats gathering is a
feature intended only for developers. If needed then the developer can
turn on more stats timers and counters and recompile the code.

Giving a method to group region variables passed/returned between
caller and callee based on dsa intrinsics. The information is precomputed
before the analysis and stored into callsite_info class for further
abstract operations of calls.

…bject

In crab IR, region initialization / copy occurs before intrinsic calls.
The object info is required for each abstract object so that
we need to initialize that info for object not informed by
intrinsic calls.

The abstract domain is based on memory abstraction which models
memory architecture with cache. Each abstract object contains a
cache that precisely materializes memory load / store. The cache
only records the most recently used by load/store instructions.
The current cache size is one so that any loads / stores for
non mru object require to commit and update cache subdomain.

In the implementation, we also includes an alias analysis that abstracts
references alias properties. That is, we only know two references are
alias according to the DSA analysis. Such info are stored in an EUF domain.

We use UF domain to represent base addresses.
The caches in given two states refer the same MRU object if the base addresses of caches refer the same symbol in the uf domain.
The symbol is actually a term operator in crab. The comparison is based
on the value of operator but not the term.

Introduce a new redution operator (transfer function) that reduce equalities
between registers and fields in the cache. The reduction can be either adding
constraints for registers into base domain or adding constraints for fields
into corresponding cache domain.

The object domain can handle an intrinsic reduction named:
crab_intrinsic(do_reduction,@V_1:region,V_2:ref,V_3:bool);
where V_1 is a region and V_2 is a reference. The V_3 indicates
the direction for reduction. The value of V_3 is true(false) will
perform reduction from cache to base (from base to cache).

…object is top

…ormation

Since object domain can express relations between fields in more expressive
way, we also want to deal with pointer analysis such as is-dereferenceable.
The requirement for this check is using ghost variables to convey pointer
information: offset and size.

In object domain, now each typed variable such as region or reference
are now having at least one ghost variables with fixed naming.
This is also guarentee the efficiency for creating and manipulating
such variables.

Based on subdomains we have right now, we need to distinguish three
types of variables: variables in base domain, reference variables,
and fields variables used in odi map.

Once we have this classification, the operators can be performed based
on each subdomain: base domain, address domain, uf register domain,
and (summary domain, cache domain, uf field domain) in odi map.

This commit fixes the issue of join / meet when two states
contain singleton objects. Two states with singleton objects
where they might refer the same object (with same address),
or they are different. Therefore, join of two singleton objects
will become a non-singleton object if they are different.

If odi map is used, the object is not singleton. Therefore,
any join / meet over non-singleton objects require to commit caches
if necessary. If committed, we also need to reset caches as empty.

- change global object-id map (locate) function to local
- add efficient join / meet operations on odi map

A symbolic equality domain is an abstract domain which represents equalities
used in analyses for allocation-site abstraction or domain reduction.
In short, giving two program variables are known to hold equal values in concrete semantics
if the analyzer determines that the variables hold equal symbolic term.

A special seperate domain for odi map. Especially, it covers
different cases during domain operations such as join or meet.

…r eq domain

object.reduction_level=FULL_REDUCTION to perform reduction before
each transfer function;
object.reduction_level=REDUCTION_BEFORE_CHECK to perform
reduction only before assertion;
object.reduction_level=NO_REDUCTION for no reduction.

- `object_domain`: avoid deep copy during updating odi values;
support new statistics; refactor cache operations.
- `odi_map_domain`: perform cache flushing before join / meet
each odi value; refactor cache operations.
- `symbolic equality domain`: supports new join operation in
quadratic running time