Clarification on termination measure

[Frédéric Bour]

Hi,

In the code beloew, the recursive call in the make_vector lemma is rejected by the termination checker.
However the characters extracted by the call to uchars_split are still in the heap. That should satisfy the heap size decrease criterion if I understood the documentation well.
I also tried to open the uchars explicitly, such that there is directly a u_character(buffer, _) among the chunks, to no effect.

Am I missing something about the termination measure?

Regards,
Fred

predicate record_vector(unsigned char *buffer, int record_size, int count) =
  count == 0
  ?
    true
  :
    uchars(buffer, record_size, _) &*&
    record_vector(buffer + record_size, record_size, count - 1)
;

lemma void make_vector(unsigned char *buffer, int record_size, int count)
  requires uchars(buffer, record_size * count, _) &*& record_size > 0 &*& count >= 0;
  ensures record_vector(buffer, record_size, count);
{
  if (count == 0)
  {
    close record_vector(buffer, record_size, 0);
  }
  else
  {
    uchars_split(buffer, record_size);
    make_vector(buffer + record_size, record_size, count - 1);
    close record_vector(buffer, record_size, count);
  }
}

[Bart Jacobs]

Hi,

No, the "heap size decreases" criterion is very specific (and incomplete): it is satisfied only if, at the recursive call, after consuming its precondition, a (non-fractional) *struct field chunk* is still in the heap. A u_character chunk is not currently recognized by this criterion (even though that would make perfect sense).

For make_vector, you can use induction on 'count'. This currently requires the following hack:

//@ #include "nat.gh"

/*@

predicate record_vector(unsigned char *buffer, int record_size, int count) =
  count == 0
  ?
    true
  :
    uchars(buffer, record_size, _) &*&
    record_vector(buffer + record_size, record_size, count - 1)
;

lemma void make_vector_(unsigned char *buffer, int record_size, nat count)
  requires uchars(buffer, record_size * int_of_nat(count), _) &*& record_size > 0;
  ensures record_vector(buffer, record_size, int_of_nat(count));
{
  switch (count) {
    case zero:
      close record_vector(buffer, record_size, 0);
    case succ(count0):
      uchars_split(buffer, record_size);
      make_vector_(buffer + record_size, record_size, count0);
      close record_vector(buffer, record_size, int_of_nat(count));

  }
}

lemma void make_vector(unsigned char *buffer, int record_size, int count)
  requires uchars(buffer, record_size * count, _) &*& record_size > 0 &*& count >= 0;
  ensures record_vector(buffer, record_size, count);
{

  make_vector_(buffer, record_size, nat_of_int(count));
}

@*/

Regards,
Bart

--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To post to this group, send email to veri...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/636e26bc-f283-4047-a3fb-d37a69e847f1%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Frédéric Bour]

Thanks for your answer.

Has a hack to check what I was doing, I assumed these two lemmas:

struct uchar_s { unsigned char a; };
/*@
lemma void field_of_uchar(unsigned char *a);
  requires u_character(a, ?c);
  ensures struct_uchar_s_padding(?uchar_a)
      &*& a == &uchar_a->a
      &*& uchar_a->a |-> c;

lemma void uchar_of_field(unsigned char *a);
  requires struct_uchar_s_padding(?uchar_a)
      &*& a == &uchar_a->a
      &*& uchar_a->a |-> ?c;
  ensures u_character(a, c);
@*/

Which confirmed that turning a u_character into a field chunk satisfied the criterion.

Building on that, I made a small fork of verifast which adds a `predicate_nonempty` declaration and changed prelude to mark character, u_character, ..., pointer as nonempty.
Non empty predicates are added to the Verify_expr.nonempty_pred_symbs map.

My fork is really just a toy, I am not checking validity of non-emptiness assertions.
However if you think it is a way worth pursuing, I can look at inferring non-emptiness for user-defined predicates by checking that all paths have a non-empty chunk. Otherwise, induction on nats is fine for me :).

Naive thoughts: the logic seems powerful enough to make precise statements about the memory (for instance, consider contiguous bytes as the primitive heap resource, on which a type can be put). Non-emptiness would be an axiom only on a byte predicate and inferred for everything that is derived.
Yet the scheme that derives predicates from C definitions seems to have a quite coarse-grained memory model.

Sorry if what I say is non-sensical, I am just discovering the project and haven't had time to digest all the available resources. That's all very exciting, thanks for this project.

[Bart Jacobs]

On 24/01/18 04:45, Frédéric Bour wrote:

Building on that, I made a small fork of verifast which adds a `predicate_nonempty` declaration and changed prelude to mark character, u_character, ..., pointer as nonempty.
Non empty predicates are added to the Verify_expr.nonempty_pred_symbs map.

Nice!!

My fork is really just a toy, I am not checking validity of non-emptiness assertions.
However if you think it is a way worth pursuing, I can look at inferring non-emptiness for user-defined predicates by checking that all paths have a non-empty chunk.

I have to say that I never use the "heap size decreases" criterion. It is probably always possible to use one of the other criteria, and indeed, this has been the case in my experience. Also, note that even the extended criterion has limitations:
- some predicates (e.g. chars) are only conditionally nonempty.
- sometimes, only a fraction of a nonempty chunk is available, typically with an unspecified coefficient. It would not be sound to have arbitrary fractions of nonempty chunks satisfy the criterion.

Probably the best way to make record_vector go through more smoothly, is to add direct support for induction on int.

Having said that, I would definitely accept a pull request that adds support for a nonemptiness keyword on predicate declarations. Note that, as a first iteration, your nonemptiness analysis could simply reject all predicate bodies; the keyword would still be useful for axiomatized predicates.

Otherwise, induction on nats is fine for me :).

Naive thoughts: the logic seems powerful enough to make precise statements about the memory (for instance, consider contiguous bytes as the primitive heap resource, on which a type can be put). Non-emptiness would be an axiom only on a byte predicate and inferred for everything that is derived.

Yes, this could be done, I guess.

Yet the scheme that derives predicates from C definitions seems to have a quite coarse-grained memory model.

Note that field chunks can be opened into generic chunks (integer, character, pointer, ...) (I call these "pointee predicates" in the code.)

Sorry if what I say is non-sensical, I am just discovering the project and haven't had time to digest all the available resources. That's all very exciting, thanks for this project.

Thanks for your interest and it's great to see you diving into the codebase!

To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/9ceb25b6-b8b7-41d3-be35-f3f75742438f%40googlegroups.com.