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