Switch IR to Patronus Expressions, Enhance Edge Contraction

[Nikil-Shyamsunder]

Switch to Patronus Expressions in Lowering/Edge Contraction:

• ProtoGraphs now hold a Patronus Context for expressions (type-aliased as ExprContext).
• At lowering, AST expressions are recursively lowered into the Patronus expression equivalents.
  • Sym expressions are turned into Patronus BVSymbol, and we track them with symbol_expr: FxHashMap<SymbolId, ExprRef>, allowing us to consistently lower the same SymbolId to the same ExprRef as well as handle Assign ops in the IR, which still refer to AST symbols
  • DontCare expressions are turned into BVSymbols with names prefixed by a DONTCARE_PREFIX (__dontcare__) @ekiwi maybe we could just store all the ExprRef that are DontCare in a set as an internal attribute of the ProtoGraph instead of doing this.
• Edge contraction now uses the Patronus simplifier to construct simplified and and or expressions.

Graph Interpreter:

• the graph interpreter is entirely rewritten. it operates logically quite similarly to before, but how it evaluates expressions and binds values is new since it does not share any code with the AST interpreter anymore
• first note that we are now dealing with ExprRefs in two contexts. IR ExprRefs, and Patronus transition system simulator ExprRefs. we will refer to ProtoExprRef and SimExprRef here for writing clarity, but they're not distinguished in the code
• first, bindings are built for BVSymbol ProtoExprRefs. A binding just maps a ProtoExprRef to one of 3 things:
  • a Sim(SimExprRef) binding , saying that this ProtoExprRef get's its concrete value from the simulator
  • a Arg(Value) binding - this is just the standard Arg also used in the AST interpreter
  • a DontCare binding - i.e. we have no binding for this at all.
  • we build this binding by going through all the expressions that are symbolic, and binding them to one of the 3 enum variants above depending on if they're ports, args, or DontCare values at the AST level.
• Next, we build our initial SymbolValueStore, which Patronus will use to evaluate ProtoExprRefs. This is simply done by looking up the Arg and Sim values from the arg_map passed in to the interpreter by the .tx parser, and from the Patronus simulator. DontCare are not left unbound, they are given random values.
• Each time we loop in the graph interpreter (i.e. interpret a node), we update the value store with the latest values. Since only simulator values can change, those are the only ones we bother doing.
• Expressions are evaluated via Patronus' evaluator, but other than that the logic is the same as the old graph interpreter.

Edge Contraction updates: <-- this part can be moved into a LaTeX doc at some point and fleshed out further

• introduce an InternalAssertFalse action. if the guard is true this asserts false. these just panic if hit in the graph interpreter
• there is now an invariant (which is true even from lowering), that there is exactly 0 or 1 of fork, done, port write in the action vector.
• there is also an invariant that all assignments look like [1] <input port> := ite(P, <expr>, <input port expr>) at lowering.
• every time we add a fork or done, we OR the guard into the existing action or make a new one if none exists
• every time we add a fork, we also maintain an InternalAssertFalse. Suppose the existing Fork is action guarded by P or Q, and the new Fork is action guarded by R. the existing InternalAssertFalse guarded by P and Q. So we update the action guard to P or Q or R and we update the InternalAssertFalse guard to (P or Q) and R. likewise if we added guard W, the guard would become `(P or Q or R) and W) etc.
• every time we add an assignment guarded by P, we look up an existing assignment. if it exists, it will create ite(P, new_assign, existing_assign). If it does not exist, we just append the action - this appended action must be an ITE anyways by invariant 2 above.
• note this means that all assignments have a true guard always because the actual conditionals are fully represented by ITEs. TODO: this also should mean I can get rid of the semantics that handle retaining old port values into the new cycle n the graph_interpreter.rs , but I want to leave this to a follow-up PR once we have tested and thought about it.
• the worklist now contains (Transition, set of NodeId) pairs. That set is the visited path of Nodes for this worklist item. if we revisit one of those nodes, we have a non-step cycle. If two transtions P and Q respectively send us back to a node we've already seen without a step, we just have an InternalAssertFalse for the guarded transitions. The current Transition we popped off the worklist has a guard that is literally the path condition, so we just have an InternalAssertFalse for (Transition.guard AND P) OR (Transition.guard AND Q).
• finally, we run normalize_assignments to ensure all ports have an assignment in each node. If a port didn't have an assignment, an assignment of the form DUT.a := DUT.a is generated (RHS is the old value).

graphviz.rs

• we're not using the Patronus serializer. This is because we need recursive access in order to format DontCare as X, and luckily we're using only a small part of the Patronus expression expressivity, so it's not too painful to write the formatter myself.

[ekiwi]