Array range in precondition

Question

I am currently trying to learn how to use VST. I am using VST 1.5. I have this little C program (backref.c):

char* rbr (char* out, int length, int dist) {
  while (length-- > 0) { out[0] = out[-dist]; out++; }
  return out;
}

My Coq code (with a trivial pre- and postconditions) is

Require Import floyd.proofauto.
Require Import backref.

Local Open Scope logic.
Local Open Scope Z.

Definition rbr_spec :=
  DECLARE _rbr
    WITH sh : share, contents : Z -> int
      PRE [ _out OF (tptr tuchar), _length OF tint, _dist OF tint ]
        PROP ()
        LOCAL ()
        SEP ()
      POST [tptr tuchar] local(fun _ => True).

As a precondition, I would like to say that out[-dist] to out[-1] are readable, and out[0] to out[length-1] are writable. PLCC page 210 tells about a condition array_at_range, but it does not seem to be available in VST 1.5. How can I do this?

Answer 1

You can use array_at. But because the two different parts of your array have different ownership shares, you'll have to describe them as two different array segments.

Something like:

p: val  (* base address of array *)
v1: list val  (* contents of array segment 1 *)
v2: list val  (* contents of array segment 2 *)
sh: share (* readable *)
sh': share (* writable *)

SEP (`(array_at sh tint nil (-dist) (-1) v1 p);
     `(array_at sh' tint nil 0 (length-1) v2 p))

But it's more complicated than that, because this leaves out the description of the part below (-dist) and above (length-1).

Perhaps you don't need the full generality of different ownership shares for the parts of your array; can you think of why the client of your function would need this? In that case, it will be easier to have just one array segment, whose "value" is the concatenation of several lists. This is illustrated in the example progs/verif_revarray.v; pay particular attention to reverse_Inv in that file.