store_tac_with_hint insufficiently general for array of struct

[andrew-appel]

[in any recent version of VST such as 2.9, 2.10, master branch]
Consider this program,

void f (struct foo {int x,y;} *p, unsigned i, unsigned n) {
  p[i].x = 0;
}

with this precondition just before the forward command:

H : 0 <= i < n
H0 : field_compatible (tarray t_foo n) [] p
______________________________________(1/1)
semax Delta
  (PROP ( )
   LOCAL (temp _p p; temp _i (Vint (Int.repr i));
   temp _n (Vint (Int.repr n)))
   SEP (data_at_ Ews (tarray t_foo (n - i))
          (field_address (tarray t_foo n) (SUB i) p)))
  ((_p + _i -> _x) = (0);) POSTCONDITION

Then forward_store will give an error message about doing an assert_PROP,
so let's do that and prove, above the line as directed,

H1 : offset_val 0
          (force_val (sem_add_ptr_int (Tstruct _foo noattr) Unsigned p
                                (Vint (Int.repr i))))
   = field_address  (tarray t_foo n) (SUB i) p

Now, forward gives the following error message:

Tactic failure: unexpected failure in load/store_tac_with_hint.
The expression (_p + _i -> _x)%expr has type (Tint I32 Signed noattr)
but is expected to have type (Tstruct _foo noattr) (level 996).

This is wrong; it's a bug in store_tac_with_hint, that comes from insufficient generality in the underlying lemma, semax_PTree_field_store_with_hint.

Below is the complete VST proof script to reproduce this bug.

Require Import VST.floyd.proofauto.
Require Import test_store_array_field.

#[export] Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Definition t_foo := Tstruct _foo noattr.

Definition f_spec :=
DECLARE _f
 WITH p: val, i: Z, n:Z
 PRE [ tptr (Tstruct _foo noattr), tuint, tuint ]
   PROP(0 <= i < n; field_compatible (tarray t_foo n) nil p)
   PARAMS (p; Vint (Int.repr i); Vint (Int.repr n))
   SEP (data_at_ Ews (tarray t_foo (n-i)) 
            (field_address (tarray t_foo n) (SUB i) p))
 POST [ tvoid ]
   PROP() RETURN()
   SEP (data_at_ Ews (tarray t_foo (n-i)) 
            (field_address (tarray t_foo n) (SUB i) p)).

Definition Gprog : funspecs := nil.

Lemma body_f: semax_body Vprog Gprog f_f f_spec.
Proof.
start_function.
assert_PROP (
  offset_val 0
   (force_val
      (sem_add_ptr_int (Tstruct _foo noattr) Unsigned p
         (Vint (Int.repr i)))) 
  = field_address (tarray t_foo n) (SUB i) p). {
 entailer!.
 rewrite field_address_offset by auto with field_compatible.
 simpl; f_equal; lia.
}
forward.