Advice on how to add struct support

[Alastair Reid]

Hello,

I am working with a codebase that makes very heavy use of code like this

    struct W { T t; };

to create a new type "struct W" that is different from type T but isomorphic to T.

There are lots of functions that take a "struct W" as an argument or return a "struct W" as a result.

And, as far as I can tell, VeriFast does not support this.

I would like to add support for this to VeriFast but I would appreciate some suggestions about how to go about it.  (I am comfortable reading/writing OCaml and compiler-like codebases and I have been reading a lot of VeriFast papers and separation logic papers - but I don't know my way around the codebase and there is a risk that I do something fundamentally unsound.)

Here are my thoughts so far.

## Design

1) Generality.

    At the moment, I think it may be sufficient to only support structs with one field.

    But I don't think it should be any harder to support structs with multiple fields so I will.

2) I want to support passing structs in and out of functions like this

    struct W inc_W(struct W w)

    //@ requires is_good_W(&w);

    //@ ensures  is_good_W(&result);

    {

        w.t = foo_T(w.t);

        return w;

    }

3) I don't plan to change predicates to let me pass structs to them.

     I am fine with writing predicates that take pointers to structs - like this

        predicate is_good_W(struct W* w) = ... w->t ...;

     So, unless I have to, I don't plan to change that.

4) Not critical but very nice to have is extended support for struct initialization.

     The original codebase contained lots of code like this

        struct vcpu_locked locked = {

                .vcpu = vcpu,

        };

      This caused parsing errors and had to be rewritten like this.

          struct vcpu_locked locked;

          locked.vcpu = vcpu;

      I think that this is just a parser limitation so, if I can do it without extending the AST,

      I'd like to support this too.

## Implementation

Here is what I have pieced together so far.  This is all very speculative because I am new to the codebase and only partway through implementation.

1) For each struct declaration, I need to define a predicate.

     (I am currently using the struct name as the name of the predicate family)

    I think that I can create this at the same time as (and with similar code to) malloc_block predicates - seems straightforward.

2) Change try_pointee_pred_symb to return the new predicate for StructTypes

[I have done the two steps above, and I am working on the remaining steps]

3) There are two places in verifast1.ml that report the error "Taking the address of this expression is not supported."

    I think I need to modify both of them to accept StructType arguments.

    But I think that they are both well-formedness checks so once I change them to accept StructTypes, I will start hitting errors in the core of VeriFast.

4) When passing structs to functions and returning them, I will need to produce/consume the corresponding struct predicates.

     If I am lucky, I will be able to figure out what to change based on stack backtraces.

I'd really appreciate any suggestions/corrections to the above plan.

And, of course, I am happy to contribute my changes.

--

Alastair Reid