Microcode internal changes: havocs, new framing, and push through

septract / starling-tool

An automatic verifier for concurrent algorithms.

MIT License

7 stars 4 forks source link

Microcode internal changes: havocs, new framing, and push through #119

Closed MattWindsor91 closed 7 years ago

MattWindsor91 commented 7 years ago

This PRQ does three big things:

1) Amends the definition of Assign in Microcode to allow assignment to nothing. This represents a havoc and implements #104. 2) Rewrites the command framer to work on Microcode instead of BoolExpr, implementing #112. 3) Adds Microcode to CommandSemantics, freeing it up for use in backends directly instead of relying on the low-level Boolean semantics or high-level PrimCommand representation.

Most changes are internal for now.

MattWindsor91 commented 7 years ago

Going to push this one through as well since we have a massive backlog.