To second what Gerwin said, AutoCorres is possibly not getting this right. I would expect that it would be possible to prove that "subfield_C_update f x = foo_struct_C (f (subfield_C x))", which would simplify your goal a bit. However, the presence of sub-addressing constants *after* the AutoCorres abstraction suggests that not everything has been converted properly. (The constants I'm thinking of are the Ptr -> [''subfield''] syntax.) I don't have any simple ideas how to investigate further. As Gerwin already implied, there are two memory representations here. The C parser uses a low-level memory representation (thanks to Harvey Tuch) which handles arbitrarily nested structures. AutoCorres then makes some simplifying assumptions and transformations. I think that AutoCorres is intended to handle nested structure, but not use of references to nested structures. That's the intention, I haven't tested it. Cheers, Thomas. On 25/10/17 15:06, Gerwin.Klein@data61.csiro.au wrote:

Hi Dan,

there are two things in this example AutoCorres probably has trouble with.

The first part is that "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield” is true only for packed structs (structs that have no padding in them), because padding allows the compiler to make incompatible choices for the padded memory content.

The consequence of that is that in our memory model, the two updates are not equal — their effect viewed under the struct type is equal, but their effect viewed under a byte heap for instance would not be equal.

I’m not quite sure (would have to look at the encoding details) wether this really applies here, but it might: at least on ARM, there is an alignment condition on the struct size, and it’s possible that the foo_struct is actually 4 bytes large, i.e. contains 2 bytes for the unit16_t and 2 bytes of padding.

The second problem is that AutoCorres’ memory abstraction does not support nested structs, which is what you seem to have in the example. The more detailed (but complex) memory model before abstraction does support nested structs, and, for packed structs, your property should hold. If memory serves correctly, the generic version of that property should be proved in https://github.com/seL4/l4v/blob/master/tools/c-parser/PackedTypes.thy#L860

Cheers, Gerwin

...

On 25.10.2017, at 03:56, Dan DaCosta wrote:

seL4 Developers:

Consider the following c structure declarations:

struct foo_struct{ uint16_t subfield; };

struct bar_struct{ struct foo foo; };

I am wondering if anyone has any suggestions on how I might go about proving something like this:

s[Ptr &(bar→[''foo_C'']) := subfield_C_update (λ_. b) (heap_MissionCommand_struct_C s (Ptr &(bar→[''foo_C''])))] = s[Ptr &(bar→[''missioncommand_C''])→subfield := b]

where s of type lifted_globals, bar is of type foo_struct_C, and b is of type word16.

I *think* it should be provable, i.e., "updating all of the foo field with a copy of what was there originally modulo some change to subfield is equivalent to making that change directly to the subfield."

I apologize in for taking this "into the weeds" but some of the definitions being used are buried in the AutoCorres translation and I am unsure how to make my question more abstract.

Thanks in Advance! Dan DaCosta _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel

---

Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel