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.greve@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.