Hi David,
this is usually output from our bitfield generator tool in
https://github.com/seL4/seL4/blob/master/tools/bitfield_gen.py
This tool implements packed bitfields with shifting/or/etc, because at the time
we wrote this we didn’t trust gcc on ARM to produce correct, predictable, and
optimal code for that. The tool also generates accessor functions, specs and
proofs for these pieces of C code that we use in the rest of the proof.
The wrapping inside the struct is to force the compiler to see the array as
distinct type, as you say. Apart from the compiler, this also allows us to
track these types in the proof as separate entities and get a few free theorems
from our machinery for C types.
The array in this case is the degenerate form of a 1-word bitfield. All this
disappears in the optimisation phase of gcc, so the binary code is the same as
accessing the word directly. Since we usually don’t write this code by hand and
even the theorems for it are generated, it’s not much of a burden. Easier to
keep the generator simple and let the compiler do the optimisations it already
understands.
Cheers,
Gerwin
ps: no need to stop ;-)
> On 29.01.2015, at 02:20, David Greve <david.gr...@rockwellcollins.com> wrote:
>
>
> One more and then I'll stop .. I promise.
>
> There appear to be numerous instances of the following design pattern:
>
> struct message_info {
> uint32_t words[1];
> };
>
> Where the above structure is then allocated locally, initialized and
> returned by a procedure.
>
> Seems like a lot of work to return a uint32_t.
>
> I originally assumed that all/much of this code was generated automatically
> from Haskell .. so I figured it was some odd corner case in the translator.
> Subsequent discussions, however, have suggested that this assumption is false
> and that the code was actually written by hand.
>
> I could understand using structures to present a unique, statically
> checkable procedure type signature .. but I can't rationalize the use of the
> single element array.
>
> So .. is there a reason for this curious design pattern?
>
> Thanks,
> Dave
> _______________________________________________
> Devel mailing list
> Devel@sel4.systems
> https://sel4.systems/lists/listinfo/devel
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
Devel mailing list
Devel@sel4.systems
https://sel4.systems/lists/listinfo/devel
