Creating a C Buffer From the ARM to the VideoCore on RPi3

I am looking into the the hello world of bare metal on RPi3, which is turning on the ACT LED.

There many good resources:

1. Some in assembly for Pi 1
2. David Welch's excellent baremetal tutorial for Pi 1 and 2
3. and his blinker01 example for Pi 1 and 2

The Pi3 unfortunately has moved the LED's off GPIO. You instead have to send a message to the VideoCore (GPU) in its mailbox to turn on the LED.

The documentation states the buffer content of that message as follows:

u32: buffer size in bytes (including the header values, the end tag and padding)

u32: buffer request/response code

 Request codes:
    0x00000000: process request
    All other values reserved 
 Response codes:
    0x80000000: request successful
    0x80000001: error parsing request
    All other values reserved 

u8...: sequence of concatenated tags

u32: 0x0 (end tag)

u8...: padding

I was able to get this assembly example successfully running on the Pi 3. The ACT LED turns on and stays on.

But my point in doing this is to learn bare metal C. I am new to C but I understand enough to explain what the following function does:

/**
*** This is my own summary ** so likely incorrect
* 
* Assigns the address of the Mailbox which is 0x3f00b880 to the mailbox variable
* 
* Then waits until Mailbox 0 which the GPU uses as interrupt to the ARM;
* basically saying I am ready for your message.
* 
* The function then puts the address of the message buffer
* plus the channel to be used; in this case channel 4 for ACT LED
*/
unsigned int MailboxWrite ( unsigned int fbinfo_addr, unsigned int channel )
{
    unsigned int mailbox;

    mailbox=0x3f00b880;
    while(1)
    {
        if((GET32(mailbox+0x18)&0x80000000)==0) break;
    }
    PUT32(mailbox+0x20,fbinfo_addr+channel);
    return(0);
}

The problem I am having (and maybe it's because it's late at night and I have been at this for several hours) is I am not sure how to construct the buffer.

My thinking is to make an int array that looks like:

# ?? buffer size in bytes
# 0 is the request code
# 0x00038041 Tag ID (SET_GPIO_STATE)
# 8 value buffer size
# 0 Request/response size
# 130 ACT_LED pin number
# 1 Turn it on
# 0 End tag
[??,0,0x00038041,8,0,130,1,0]

How should I calculate the buffer size? Is it the size of the array?

So would I add just a 0 as the first element, then run sizeof and update the array?

int[] buffer = [0,0,0x00038041,8,0,130,1,0];
buffer[0] = sizeof(buffer)

Maybe it's bad form to answer my own question but I hope it helps someone.

Thanks to the comment from @old_timer I search the bare metal forum and found this solution:

void set_PI3LED(bool on) {
    uint32_t __attribute__((aligned(16))) mailbox_message[8];
    mailbox_message[0] = sizeof(mailbox_message);
    mailbox_message[1] = 0;
    mailbox_message[2] = 0x38041;
    mailbox_message[3] = 8;
    mailbox_message[4] = 8;
    mailbox_message[5] = 130;
    mailbox_message[6] = (uint32_t)on;
    mailbox_message[7] = 0;
    mailbox_write(MB_CHANNEL_TAGS, mailbox_ARM_to_VC(&mailbox_message[0]));
    mailbox_read(MB_CHANNEL_TAGS);
}

It's nice to know I wasn't too far off and it's good to know I now have the exact syntax I need.