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 <[email protected]> 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 > [email protected] > https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
