Use atomistic lattice to link up events

Instead of recording the address of the memory that is being affected by
an indirect write, we associate each variable, through which the memory
is accessed, with an element in an atomistic lattice. Each lattice element
is of type Tag. Two events, e and e', can be linked up if the meet of their
respective tags is not bottom, i.e. tag(e) /\ tag(e') must be strictly
greater than the least lattice element.

Example:

  1. static char xs[3];  : initialize k_1 constant array
  2. char v;             : initialize k_2
  3.
  4. xs[i] = 'A';        : k_4 == store(k_3, i, 'A')
  5. xs[j] = 'B';        : k_6 == store(k_5, j, 'B')
  6. v = xs[j];          : k_8 == select(k_7, j)
  7. assert('B' != v);   : Assert 'B' != k_9

The left-hand column is a concurrent program where "xs" is a shared array,
whereas the other variables are thread-local. On the right-hand column,
each program statement is shown as an equality using McCarthy's theory of
arrays. Notice that each read and write event is associated with a fresh
SMT solver constant.

In addition, we associate both variable declaration at line 1 and 2 with
two unique atoms in the atomistic lattice (cf. Tag class).

The dereference read instruction at line 6 consists of a read event (k_7)
and a literal index read instruction (j). Note k_7 could refer to either
the indirect write event k_4 or k_6. However, the FR axiom should rule
out that k_7 == k_4 because of the intermittent indirect write at line 5.
Since k_4's and k_6's tags are the same, their meet is not bottom. Thus,
FR orders them such that the equality k_7 == k_4 is unsatisfiable.

Changes:

* Remove all array offset calculations
* Add Tag class
* Remove MemoryAddr class
Fix Block doc