Static Fork Analysis

[Nikil-Shyamsunder]

Do not merge until #271
The analysis:

• this is a very similar analysis to the assignment analysis, but different enough (and way simpler) that I ended up writing new data structures and a separate file for the analysis. Putting it in the existing assignment analysis would be more confusing probably. Luckily, it ended up being relatively simple to implement (like 150 LOC)
• Every node has an in_fact and an out_fact, which are of type ForkFact
• a ForkFact is a no_fork_guard: ExprRef and a fork_guard: ExprRef. no_fork_guard means "if this is true, there is some path ending at this node where no fork is triggered". fork_guard means "if this is true, there is some path ending at this node where a fork is triggered."
• The merge function is just OR-ing the no_fork_guard for all in neighbors, and same for the fork_guards. The catch is that we know which edges must've been taken, so we can do a similar trick as in the assignment analysis and say "if the predecessor forks under p and only transitions to this node under p, it definitely forked: simplify to true". We then simplify/canonicalize the expressions.
• If there is a fork guarded by p in this node, the transfer function is just OR-ing with p on the fork_guard and OR-ing with !p on the not_fork_guard.
• Once again, I don't really have a good reason why this will converge because it'd dependent on the simplifier, but in our cases this works great
• Then we do the traditional worklist thing

Using the analysis:
Once we have the in_fact and out_fact for each node at the fixpoint, we can make the following inferences for some node n:

• if the in_fact fork_guard to n is DefinitelyUnsat (the expression simplifies to false), we definitely didn't fork before this
• if the in_fact not_fork_guard to n is DefinitelyUnsat and the fork_guard to n is AlwaysSat (the expression simplifies to true), we definitely did fork before this
• otherwise, we MaybeForked

Assertions:

• For every node that has a fork, we assert that the in_fact fork_guard to this node is DefinitelyNotForked. i.e. if we hit a fork, we haven't forked prior. This is maybe too strong an assertion, but for now everything satisfies this.
• For the done Node, we want to prove we either DefinitelyNotForked or DefinitelyForked. If we MaybeForked we need internal state, so we panic for now. If we DefinitelyNotForked, then we graft the next protocol onto the done node. If we DefinitelyForked, we do not.

Testing:
All the tests pass without tripping those assertions. Also I wrote very targeted unit tests that test different important cases for the analysis.

While it's not in the rust suite because it needs extra flags and some modifications, for a sanity check I also was able to test that the following protocol, run with --skip-static-step-fork-checks panics after the analysis because fork node node6 can be reached after a prior fork

prot add_double_fork<DUT: Adder>(a: u32, b: u32, s: u32) {
  DUT.a := a;
  DUT.b := b;
  fork();
  step();
  fork();
  DUT.a := X;
  DUT.b := X;

  assert_eq(s, DUT.s);
  step();
}

Other Minor stuff:

• Changed DefinitelySat to AlwaysSat because I think that is more descriptive. AlwaysSat is just if the expression tautologically simplifies to true.
• propogate_assigns.rs and reaching_defs.rs have some small changes which are just generalizing helpers so I can use them in the fork analysis as well