Use of inferred specification in entailment

[EmilyOng]

Issue

This program fails to prove the entailment for main.

let call_ret f =
  f 100

let main ()
(*@ ens res=100 @*)
= let id i = i in
  id 2;
  call_ret id

The above program gives the following specification.

ex v21 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); v22(2, v21); ex v19; call_ret(v22, v19); ens res=v19

It fails to prove the entailment because, in the entailment process for main:

(a) id (v22) is unfolded as v22(i,v15) == ens v15=i, giving the specification:

ex v21 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); ens v21=2; ex v19; call_ret(v22, v19); ens res=v19

(b) call_ret is unfolded as call_ret(f,res) == ex v0; f(100, v0); ens res=v0, giving the specification:

ex v19 v22; ens v22=(fun i v15 (*@ ens v15=i @*) -> i); ex v49; v22(100, v49); ens v19=v49; ens res=v19

Here, call_ret has to be unfolded because the inferred specification (in the first step) is not used. But, the unfolding introduces an additional appearance id (v22), and we are required to unfold id (v22) again (I think the only heuristic available for use here is to unfold).

Note (from discussion)

A workaround requires one to provide an explicit specification ex v0; f(100, v0); ens res=v0 to call_ret. This works because we can use the inferred specification directly and avoid an additional unfold of id (v22). Another workaround is to increase the unfolding bound to 2 to accommodate the additional unfolding of id (v22).

Questions

We can use the rec_flag (from parsing) to allow unfolding of non-recursive predicates during the entailment as discussed, or to directly use the inferred specification when analyzing the method.

[dariusf]

I think the way to fix this is to always unfold non-recursive predicates during entailment. Something like this should work:

• Add a field to pred_def to say if the predicate is recursive
• When we create a pred_def, traverse its disj_spec body (using a visitor like this to visit_HigherOrder) to check if the predicate name occurs in any function stages. We can deal with mutual recursion later.
• When we remember which predicates we've unfolded, don't count non-recursive predicates