How to Specify and Prove a Function Reading Header from a Payload Pointer

[laforetbarroso]

Hello,

I'm trying to write a specification and prove a simple function in VST, but I’m not sure whether my spec is correct or how to approach the proof. I'd really appreciate any guidance!

The C code

typedef uint64_t uintnat;
typedef int64_t intnat;
typedef intnat value;
typedef uintnat header_t;
typedef volatile uintnat atomic_uintnat;

/* Cast value to atomic_uintnat* and subtract 1 */
#define Hp_atomic_val(val) ((atomic_uintnat *)((uintptr_t)(val)) - 1)

header_t Hd_val(value v) {
    volatile header_t* p = Hp_atomic_val(v);
    return *p;
}

int main(void) {
    /* Allocate memory as uintnat*, since atomic_uintnat is just volatile uintnat */
    uintnat* block = (uintnat*)malloc(2 * sizeof(uintnat));
    
    if (block == NULL) {
        return 1;
    }

    block[0] = 123456; /* Header */
    block[1] = 42;      /* Payload */

    /* Cast the address of the second cell to value */
    value v = (value)(uintptr_t)(block + 1);

    printf("%llu\n", Hd_val(v));

    free(block);
    return 0;
}

My VST specification:

Definition uintnat := tulong.
Definition atomic_uintnat := tulong. (* no volatile in memory spec *)
Definition header_t := tulong.

Definition Hd_val_spec : ident * funspec :=
  DECLARE _Hd_val
    WITH v: val, p: val, hdr: Z, payload: Z
    PRE [ tptr atomic_uintnat ]
      PROP ( isptr v; v = offset_val 8 p )
      PARAMS (v)
      SEP (
        field_at Tsh (tarray tulong 2) [ArraySubsc 0] (Vlong (Int64.repr hdr)) p;
        field_at Tsh (tarray tulong 2) [ArraySubsc 1] (Vlong (Int64.repr payload)) p
      )
    POST [ header_t ]
      PROP ()
      RETURN ((Vlong (Int64.repr hdr)))
      SEP ( 
        field_at Tsh (tarray tulong 2) [ArraySubsc 0] (Vlong (Int64.repr hdr)) p;
        field_at Tsh (tarray tulong 2) [ArraySubsc 1] (Vlong (Int64.repr payload)) p
       ).

What I’m struggling with

I’m trying to prove Hd_val using this spec, but I’m running into difficulties. More precisely, forward can't load *_p.

semax ⊤ Delta
  (PROP ( )
   LOCAL (temp _p
      (force_val (sem_binary_operation' Osub (tptr tulong) tint v
                 (Vint (Int.repr 1)))); temp _v v)
   SEP (field_at Tsh (tarray tulong 2) (SUB 0) (Vlong (Int64.repr hdr)) p;
           field_at Tsh (tarray tulong 2) (SUB 1) (Vlong (Int64.repr payload)) p))
(_t'1 = *_p;
MORE_COMMANDS) POSTCONDITION

I suspect the issue is in the way I’m specifying the memory layout. Is my spec correct, or am I missing something subtle in how memory is described or how pointer arithmetic should be modelled in VST?

Thanks in advance for any suggestions or pointers to the right solution!

[mansky1]

You have isptr v here, right? It might help to destruct v so that the sem_binary_operation' can simplify. That (and maybe some math) should be enough to simply the value of _p to p, which is what you'll need to run the next line. After that, you may run into some trouble due to VST's limited support for volatile -- but let's see! If that does turn out to be a problem, you could consider using our custom atomic library instead (https://github.com/PrincetonUniversity/VST/blob/master/atomics/SC_atomics.h).

By the way, this kind of question is better sent to the vst-user mailing list than posted as an issue.