How to represent 2D array in Verifiable C

Question

I have a 2D array unsigned int a[10][10], and would like to represent it in the SEP clause.

I get the first part as data_at sh2 (tarray (tarray tuint 10) 10) but am confused about the second part. For a 1D array, we represent as (map Vint (map Int.repr contents_a1)) a_1 where a_1 : val and contents_a1 : list Z.

In this case I have taken two lists (contents_a11 :Z, contents_a22 : Z), but am however having problems to structure them up int the second clause of SEP with map Vint..

Answer 1

I'll give here an example in which the "contents" is an array of int instead of an array of Z. You can adapt as necessary with an extra "map Int.repr" in the right places.

Consider this C program:

unsigned sumarray(unsigned a[][3], int n) {
  int i,j; unsigned s;
  s=0;
  for (i=0; i<n; i++)
    for (j=0; j<3; j++)
      s+=a[i][j];
  return s;
}

You could prove it correct with the following specification and proof:

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

Definition sum_int : list int -> int := fold_right Int.add Int.zero.

Lemma sum_int_app:
  forall a b, sum_int (a++b) =  Int.add (sum_int a) (sum_int b).
Proof.
  intros. induction a; simpl. rewrite Int.add_zero_l. auto.
rewrite IHa. rewrite Int.add_assoc. auto.
Qed.

Definition sumarray_spec : ident * funspec :=
 DECLARE _sumarray
  WITH a: val, sh : share, contents : list (list int), size: Z
  PRE [ tptr (tarray tuint 3), tint ]
          PROP  (readable_share sh; 0 <= size <= Int.max_signed)
          PARAMS (a; Vint (Int.repr size))
          GLOBALS ()
          SEP   (data_at sh (tarray (tarray tuint 3) size) (map (map Vint) contents) a)
  POST [ tuint ]
        PROP () LOCAL(temp ret_temp  (Vint (sum_int (concat contents))))
           SEP (data_at sh (tarray (tarray tuint 3) size) (map (map Vint) contents) a).

Definition Gprog : funspecs := [].

Lemma body_sumarray: semax_body Vprog Gprog f_sumarray sumarray_spec.
Proof.
start_function.
forward.  (* s = 0; *)
forward_for_simple_bound size
  (EX i:Z, PROP() 
     LOCAL (temp _s (Vint (sum_int (concat (sublist 0 i contents))));
            temp _a a;
            temp _n (Vint (Int.repr size)))
     SEP (data_at sh (tarray (tarray tuint 3) size) (map (map Vint) contents) a)).
-
entailer!.
- 
  assert_PROP (Zlength (Znth i contents) = 3). {
    entailer!. 
    rewrite Forall_forall in H2.
    specialize (H2 (map Vint (Znth i contents))).
    spec H2.
    apply in_map_iff.
    exists (Znth i contents). split; auto.
    apply Znth_In. list_solve.
    simplify_value_fits in H2. destruct H2. list_solve.
  }
  forward_for_simple_bound 3
  (EX j:Z,
     PROP() 
     LOCAL (temp _s (Vint (Int.add (sum_int (concat (sublist 0 i contents)))
                                (sum_int (sublist 0 j (Znth i contents)))));
            temp _a a;
            temp _i (Vint (Int.repr i));
            temp _n (Vint (Int.repr size)))
     SEP (data_at sh (tarray (tarray tuint 3) size) (map (map Vint) contents) a)).
 + entailer!.
 + rename i0 into j.
   forward.
   entailer!. hnf. rewrite !Znth_map by list_solve. auto.
   forward.
   entailer!. rewrite !Znth_map by list_solve.
   simpl. f_equal.
   set (t := sum_int (concat _)). clearbody t.
   rewrite (sublist_split 0 j (j+1)) by list_solve.
   rewrite sum_int_app.
   set (u := sublist 0 j _). clearbody u.
   rewrite sublist_one by list_solve. simpl.
   rewrite <- (Int.add_commut Int.zero),  Int.add_zero_l.
   rewrite Int.add_assoc. auto.
 + entailer!.
   f_equal.
   rewrite (sublist_split 0 i (i+1)) by list_solve.
   rewrite concat_app, sum_int_app.
   set (u := sum_int (concat _)).
   rewrite sublist_one by list_solve. simpl.
   rewrite <- app_nil_end.
   rewrite sublist_same by list_solve. auto.
-
forward.
entailer!.
autorewrite with sublist; auto. 
Qed.