WP: false labels

[guancio]

The original tool weakest precondition had the signature WP(l,ls,Q), where l is the initial label, ls are the labels of the exit points, and Q is the postcondition. This generates the weakest preconditon P that guarantees the program reaches an exit point and that Q is establishes as soon a label in ls is reached.

This approach forces us to establish the same postconditions for all exit points, which can be undesirable. For example

l1: cjmp c; l2; l3

If this fragment implements the guard of a while loop, l2 is the entry point of the loop body, and l3 is the first label outside the loop, we would like to verify {I and c} l1 -> {l2} {I and c} and {I and not c} l1 -> {l3} {I and not c}. This is not possible using the the original procedure for weakest precondition.

• If we use a single analysis with ls={l2,l3} then Q must be the same for both exit points
• if we use WP(l1,{l2},I and c), then the algorithm cannot compute the WP of l1 since it does not know the postcondition of on of the target addresses (i.e. l3).
• if we could use WP(l1,{l2,l3},I and c and (pc \neq l3). However, BIR does not allow postconditions to reason about the program counter.

[guancio]

For the tutorial we used a simple approach. We take an additional list of labels, for which we use false as precondition. This approach is sound because {false}l->ls{Q} always holds. If we want different precondition per exit-point we can now compute

• P1=WP(l1, {l2}, {l3}, I and c), which uses the initial triple {false}l3->{l2}{I and c} and generates the contract {P1}l1->{l2}{I and c}, and
• P2=WP(l1, {l3}, {l2}, I and not c), which uses the initial triple {false}l2->{l3}{I and not c} and generates the contract {P2}l1->{l3}{I and not c}

A benefit of this approach is that it can also be used to speed up analysis of dead code, since it simply propagates false along paths that we do not want to analyse.

[guancio]

We could generalize this approach, by allowing the WP procedure to take a list of initial contracts: WP(l, ls, thms, Q), where each theorem in thms is a contract {P}l1->ls{Q}.

[guancio]

An alternative approach is to change the definition of the triple, allowing to specify different postcondition for different exit points. E.g {P}l1[l2->Q, l3->Q', etc]. This approach could make sense for the general Hoare triple, but it does not simplifiy the work for the wp algorithm. In fact, except very few exceptions this approach will force us to repeat the work for each postcondition. In this case it is easier to just generate several contracts, with the other approach.

[totorigolo]

In fact, except very few exceptions this approach will force us to repeat the work for each postcondition.

Can you elaborate on this point? I don't see why this wouldn't work or would complicate the WP propagation procedure.

For {P} l1 -> {l2, l3, etc} [l2 |-> Q, l3 |-> Q', etc] I also see advantages when producing HT for functions having early returns for error handling (for example), where you don't want to impose too strong postconditions in those exit points.

[didriklundberg]

A benefit of this approach is that it can also be used to speed up analysis of dead code, since it simply propagates false along paths that we do not want to analyse.

Yes, it could do this, however the current version doesn't actually do this. Right now everything after (in order of concrete execution) the False-triple block is generated as usual, then just thrown away by the analysis. If we want to continue with this approach we mustn't forget to implement the time-saving tricks that are made possible by introducing the False-triple.