search

draperlaboratory / VIBES

Verified, Incremental, Binary Editing with Synthesis
MIT License
51 stars 1 forks source link

Fixes semantics of higher variables #202

Closed bmourad01 closed 2 years ago

bmourad01 commented 2 years ago

The previous way of handling higher variables was broken, specifically in terms of what is meant by the at-entry and at-exit fields.

This PR introduces the new semantics for higher vars:

  1. constant stays the same, but we fix a bug where a higher var that is meant to represent a constant value appears on the LHS of an assignment.
  2. memory is a new type of higher var value, indicating that all occurrences of a variable must be substituted with a memory location.
  3. at-entry and at-exit may now only refer to registers. If a higher var v is specified as having a register r for at-entry, then the assignment v := r is inserted at the entry block. Likewise, if it has register r' for at-exit, then in all exit blocks the assignment r' := v is inserted.

This may result in more verbose code being generated if the register allocator returns a suboptimal solution, but at least for all of the (now fixed) system tests, it's able to give solutions that enable the peephole optimizer to reduce the size of the patch.

bmourad01 commented 2 years ago

Can we express this example now?

We couldn't actually express this example before, either, since the at-exit semantics was broken. Might be possible in the future, but will require some thought.