Search code examples
ccoqformal-verificationverifiable-c

VST forward_call fail on non-standard calling convention

I'm using VST 2.5 and Coq 8.11.0

Got an error while doing forward_call on function with non-standard calling convention. Minimal code example:

struct t {
  int t_1;
  int t_2;
};

struct t test_aux() {
  struct t ret;
  ret.t_1 = 1;
  ret.t_2 = 2;
  return ret;
}

void test_f() {
  test_aux();
}

VST specs:

Require Import VST.floyd.proofauto. 
Require Import example.

Definition Vprog : varspecs. mk_varspecs prog. Defined. Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Open Scope Z.

Definition aux_spec : ident * funspec :=   DECLARE _test_aux
    WITH res : val
    PRE [tptr (Tstruct _t noattr)]
      PROP ()
      PARAMS (res)
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) res)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP (data_at Tsh (Tstruct _t noattr) 
                   (Vint (Int.repr 1), Vint (Int.repr 2)) res).

Definition test_spec : ident * funspec :=   DECLARE _test_f
    WITH temp : val
    PRE []
      PROP ()
      PARAMS ()
      GLOBALS ()
      SEP (data_at_ Tsh (Tstruct _t noattr) temp)
    POST [tvoid]
      PROP ()
      LOCAL ()
      SEP ().

Definition Gprog := ltac:(with_library prog [aux_spec; test_spec]).

Theorem test : semax_body Vprog Gprog f_test_f test_spec. Proof.   start_function.   Fail forward_call (nullval). Admitted.

Error:

Unable to unify  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid cc_default" with  "Tfunction (Tcons (tptr (Tstruct _t noattr)) Tnil)
    tvoid
    {|
    cc_vararg := false;
    cc_unproto := false;
    cc_structret := true |}".

I don't know if this is a bug or intended behavior, so I have a few questions here:

1) Is this a bug?

2) If not, what workarounds exists to prove such cases?

UPDATE:

We ran into this problem after using the following workaround around the struct-copying restriction: we define a struct_normalize : statement -> statement function in Coq that replaces struct assignments with field-by-field assignments. Hence we are working under the assumption that there is no struct copy-ing in the function we are calling. That is, we can verify the test_aux from the example above. So the questions are:

  1. Does forward_call fail only because cc_structret := true in the test_aux AST?

  2. Given that we normalize the functions and remove stucture-copying from the bodies of the functions, is it safe to change structret value accordingly and proceed with the proof?

Solution

  • Unfortunately, VST does not support struct-copying, struct-passing, or struct-returning. See also this question. So you can't verify this program without changing it.