Properly scope dynamic loop permissions

[conradz]

TLDR: This is a major change, involving a refactoring/rewriting of much of the Weaver (the part that inserts the runtime checks) and the baseline checker.

This PR is ostensibly to implement proper scoping of permissions around/in while loops at runtime (many other changes got wrapped in, see list at end). Previously, the same set of permissions was used throughout the entire method, regardless of permission boundaries introduced by equirecursively-precise loop invariants.

For example, if we have a method

Node* prepend(int value, Node* tl)
  //@requires true;
  //@ensures \result != NULL && acc(\result->value) && acc(\result->next);

and we use it in a loop like

Node* list = NULL;
int i = 0;
while (i < 10)
//@loop_invariant list == NULL ? true : acc(list->value) && acc(list->next);
{
  list = prepend(i, list);
}

after executing the while loop, we should only have gained the permissions specified by the loop invariant. That is, we would only have access to the value and next fields of the head element, and we would not have access to any of the following fields.

So, if we have

void print_list(Node* list)
  //@requires ?;
{
  if (list != NULL)
  {
    printint(list->value);
    print_list(list->tail);
  }
}

calling print_list(list) after the while loop above should result in an error, since it does not have access to the Nodes that are referenced from the root list.

Prior to this change, the same set of permissions was used throughout, so the set of permissions included the permissions gained from every prepend call, and thus it would have access to all the nodes.

This change aligns the static reasoning with the dynamic checks, and makes it possible to catch errors that stem from insufficient (precise) loop invariants earlier.

Some other changes implemented along the way:

1. (The other large change): Added a whole-program analysis (except #use-imported methods) that analyzes which methods actually check the set of dynamic permissions, and which modify the permission set. We now track permissions only when there is a runtime check that may use those permissions, in contrast to the previous behavior where it tracked permissions anywhere that was imprecise. Methods that only modify (but do not assert) permissions can be passed a NULL set of permissions, in which case they skip tracking of permissions.
2. Rewrote most of the Weaver code (Collector, Checker, etc.) a. Factored out SeparationChecks (adds the checks necessary to ensure heap locations referenced in a single formula do not overlap) b. Factored out InstanceCounter (inserts the necessary code for tracking _id of objects, now separated entirely from runtime/OwnedFields code, reused entirely between weaver and baseline) c. Factored out EquirecursivePrecision (calculates equirecursive precision of specs, used in weaver and baseline) d. Added CheckScopes to calculate proper scoping of permissions/checks e. Added Dependencies for analysis of which methods require/modify permissions (see item 1)
3. Rewrote BaselineChecker entirely. It can now omit both/either of framing and spec checks (for example, allowing only the permission passing to be done, without any assertions)
4. Refactored a lot of the runtime, simplifying it and renaming all methods to be runtime_*. [Hopefully] more performant by allowing reuse of FieldArray instances and removing unused entries only when more space is needed.
5. Added a test that compiles and runs all the verifier and quant-study examples using the baseline checker.
6. Fixed a weird bug that duplicated fold/unfold statements when they occurred immediately before a for loop.