VST Verification of Global Array of Doubles

Question

I am currently attempting to use VST to verify the correctness of a project which involves a global array of doubles. However, when attempting to access the array I have that the head of the array is given as a data_at statement while the rest of the array is given as a sepcon list of mapsto statements and there does not appear to be any way to prove field_compatible for elements beyond the head of the array.

Trying to access elements beyond offset_val 0 seems to inevitably involve proving a size_compatible statement. This is where I run into a problem. Since the alignment of tdouble is set to 4 and the size is set to 8, there seems to be a possibility that the head of the array is at Ptrofs.modulus - 12 making size_compatible false for the next element in the array. Am I going about this the wrong way?

I made a toy example with the same problem that I've mentioned above.

double dbls[] = {0.0, 1.1};
int main() {
  double sum;
  sum = dbls[0] + dbls[1];
  return 0;
}

Answer 1

I will frame my answer in the form of a Coq development:

Require Import VST.floyd.proofauto.
Require Import VST.progs.foo.
#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE  [] main_pre prog tt gv
  POST [ tint ] main_post prog gv.

Definition Gprog : funspecs :=   [ ].

Lemma body_main: semax_body Vprog Gprog f_main main_spec.
Proof.
start_function.
(* Remark 1:  it seems to be a bug in VST 2.11.1 (and earlier versions)
  that the array is not packaged up into 
   (data_at Ews (tarray Tdouble 2) ...)
  the way it ought to be.  This seems to work better for integer
 arrays, et cetera.*)

(* Remark 2:  you are right to be concerned about alignment, but
  VST addresses that issue correctly.  Any extern global variable
 in a C program, such as your [dbls] array, is aligned at the
 biggest possible alignment requirement.  VST expresses this
  with the "headptr" predicate, and for any identifier id,
  (gv id) is a headptr.  So therefore, *)
assert_PROP (headptr (gv _dbls)) by entailer!.
(* and you can see above the line, H: headptr (gv _dbls). *)
Print headptr.
(* This shows that (gv _dbls) must be at offset zero within
 some block, which guarantees alignment at any type. 
  One useful consequence is proved by the lemma
  headptr_field_compatible: *)
Check headptr_field_compatible.
(* And now, let's apply that lemma: *)
pose proof headptr_field_compatible (tarray tdouble 2) nil _
        H (eq_refl _) Logic.I ltac:(simpl; rep_lia).
(* So we see that as long as the pesky 'align_compatible_rec' is proved,
  the pointer (gv _dbls) should be 'field_compatible' with the array
 type that you want.  And it's straightforward though tedious to prove
 the 'align_compatible_rec' premise, as follows: *)
spec H0.
apply align_compatible_rec_Tarray; intros.
Search align_compatible_rec.
eapply align_compatible_rec_by_value; [ reflexivity | ].
apply Z.divide_add_r.
apply Z.divide_0_r.
apply Z.divide_mul_l.
apply Z.mod_divide; compute; intros; congruence.
(* Normally, VST users shouldn't have to do this 'by hand'.
  We should fix the bug (failure to nicely package the precondition).
  But in the interim, perhaps this gives what you need for a workaround.*)