Function postconditions are not checked soundly

[viper-admin]

Created by @alexanderjsummers on 2019-02-19 14:16
Last updated on 2019-05-06 12:43

The following example should not verify, but does

function test() : Int 
   ensures false
{
  42
}

[viper-admin]

@mschwerhoff commented on 2019-02-26 20:24

The cause of the unsoundness seems to be that the postcondition axiom, which is generated before checking the postcondition (since the function may be recursive), is instantiated by Z3 too eagerly. The postcondition axiom is shown in the following SMT-LIB snippet:

(assert (forall ( (x Int)) (!
    false
    :pattern ((test%limited x))
    )))
(check-sat) ;; UNSAT

The check-sat yields UNSAT although the trigger term isn't available.

A logically equivalent but slightly convoluted postcondition axiom doesn't seem to be eagerly instantiated any more:

(assert (forall ((x Int)) (!
    (and
      (< 0 (test%limited x))
      (< (test%limited x) 0))
    :pattern ((test%limited x))
    )))
(check-sat) ;; UNKNOWN

An idea of working around this would be to emit the postcondition axiom only after the function body and the postcondition have been verified, and to "manually" assume postconditions for function applications until then. This would require a case split in Silicon's code for symbolically evaluating function applications.

[viper-admin]

@alexanderjsummers commented on 2019-02-27 17:09

Thanks, Malte - that makes sense. In Carbon, the postcondition axiom is omitted, but it is conditional on either the function level being appropriate or a special additional term being available; this is assumed while processing the function postcondition, for each call of the function occurring there (note that this means postconditions will also trivially go through in Carbon if one mentions an identical call to the function in the postcondition, rather than using result, but that's essentially a termination failure).

Here is the relevant Boogie code for the axiom (the additional term has the slightly surprisingly name test#trigger(EmptyFrame)):

// Postcondition axioms
axiom (forall Heap: HeapType, Mask: MaskType ::
  { state(Heap, Mask), test'(Heap) }
  state(Heap, Mask) && (AssumeFunctionsAbove < 0 || test#trigger(EmptyFrame)) ==> false
);

[viper-admin]

@mschwerhoff commented on 2019-05-06 12:43

See also #376

[viper-admin]

@mschwerhoff on 2019-05-06 12:43:

• changed component from (none) to Functions

[marcoeilers]

Finally fixed.