Support "if in" and "in" blocks

[mcoblenz]

This lets users conveniently check the state of the current contract after a possible transition and offers appropriate lexical scoping regarding the current state.

[mcoblenz]

From email:

There are two concerns that we are trying to address here:

// Example 1 if (x is in S) { x.changeState(); // Now a typestate specification held by the owner of the object referenced by x might be violated! }

// Example 2 if (x is in S) { // I will call this block the “state-check-block” below foo(); // foo() might have changed the state of the object referenced by x (via the owner)! // Now we can’t safely assume the object is still in state S. }

1. Once a state check has been performed on x, if we allow changing the state via x, then that might violate a state specification of an owner.
2. If the state of the object referenced by x is changed (by the owner) after the state has been tested, then the state specification is invalid.

(have I captured all the cases?)

So, what is the most precise way of preventing unsoundness? Address both #1 and #2:

1. Dynamically track not just whether an object is owned, but the specific set of states that the owner allows the object to be in. Then, while in the state-check-block: Option A: raise an exception if the object attempts to transition out of the set of allowed states (conservative). Option B: raise an exception if the owner attempts to dereference the state-specified reference when it is in an incorrect state (most precise, but the exception is raised after the bug has arguably occurred. This is harder to debug but we could enable variant A in debug mode. Note that the dynamic checks are more expensive than in A, but still not so bad because they only have to occur until the state-check block exits.)

2. Every use of x inside the state-check-block after the first statement will be guarded by a dynamic state check (making sure it is in state S), which will throw an exception if it fails.

Now, regarding exceptions, we can take three different perspectives:

1. Add general-purpose support for exceptions; throw a specific exception that users can catch if they want.
2. Assume that these exceptions will only be raised in cases of bugs and that therefore terminating the program is acceptable.
3. Modify the syntax to provide a place to put error handlers without exposing a general-purpose exception mechanism. e.g.

if (x is in S) { // ... } on state error { // handle the error… }

One nice thing about this approach is that it can be applied gradually. We could default to the static approach or the dynamic approach, and allow users to switch between them on a per-block basis or on a whole-program basis (via a compiler flag). Then we could evaluate in case studies in what cases the conservative approach would indicate a bug when the code is actually safe.

[bloemy7]

Solved.