Verification of return and declaration statements

Hello,

are these rules for return and declarations compatible with the reference?

  • pc return e; Q = pc return; Q = true
  • vc return e; Q = vc return; Q = {}
  • pc t x; Q = Q
  • vc t x Q = {}

where e is an expression, t is a type and x is an identifier.

The reasoning is that when we have declarations the only thing related to correctness is that they are well typed, which is already covered by the semantic analysis. Hence during verification they should have no impact on either kind of condition (vc or pc).

Furthermore I read the statement:

… assignments shall only be used in ExpressionStatements and must be the outermost expression.

from page 10 of the specfication, as: declarations may not assign at all. So this:

void f() {
    int x = 0;
}

should throw an exception, while this:

void f() {
    int x;
    x = 0;
}

should not. For verification purposes we only consider the body of the function, i.e. we would apply pc and vc to {int x; x = 0;} and thus get (using the block rule and my definitions above):

pc {int x; x = 0;} true = pc {x = 0;} true (= true)
vc {int x; x = 0;} true = vc {x = 0;} true (= {})

It is already late, so I don’t have time to investigate this further, but my definitions make sense at least when the declarations are at the very front:

pc {t_1 e_1, ... ,  t_n e_n, s_1, ..., s_m} Q = pc {s_1, ... , s_m} Q
vc {t_1 e_1, ... ,  t_n e_n, s_1, ..., s_m} Q = vc {s_1, ... , s_m} Q

I assume one can use induction to produce a more general block rule which allows splitting blocks arbitrarily, thus proving that declarations at arbitrary positions “vanish”. (I checked on {s, t x, s'} and it has the same pc and vc as {s, s'})

With regards to return I am not so sure, since it should nullify everything that comes after it, and hence make it “easier” to fulfill the verification conditions. Thus pc assigning true to it seems reasonable. This has the effect that:

pc {s, return;} Q = pc s true;
vc {s, return;} Q = vc s true

which means that in order to guarantee correctness we need to at least terminate (i.e. be in state true at the end).

Declarations with assignments are syntactic sugar and should be handled like the desugared version, i.e. as if there was a not assigning declaration and an assignmemt behind it.

Otherwise, your rules are correct. In particular, declarations do nothing and the return statement is always safe and thus have true as the (weakest) precondition, since the code behind them is dead.

In the project specification, §6.2.1 Restrictions on TinyC for testing preconditions, it is mentioned that

… assignments shall only be used in ExpressionStatements and must be the outermost expression.

Ensure that these restrictions are fulfilled while building the formulas and throw any exception, if that is not the case.

I thought hence that, the verifier must throw an exception whenever a variable is initialized within its declaration statement, i.e. if init != null.

An initializer is not an AssignExpression.

So int i = 5 is fine, but int i = (i = 5) is not because the latter actually contains an assign expression.

1 Like