search

formalsec / waspc

OWI's C frontend now in https://github.com/OCamlPro/owi/pull/100
Apache License 2.0
0 stars 2 forks source link

Alignment guarantees of malloc #4

Open krtab opened 8 months ago

krtab commented 8 months ago

https://github.com/formalsec/waspc/blob/c7cd3f91dcee40cec532dc0cad21a96da9c1c988/share/lib/src/stdlib.c#L26-L32

We currently make no guarantee on the returned pointer alignment. Malloc's pointer alignment seems not to be completely clearly defined, and even less clearly implemented, but it is reasonable for a C programmer on x64 to expect malloc(8) to return an 8-aligned pointer.

krtab commented 8 months ago

@filipeom : Eric volunteers to fix it and I'll mentor him if it is fine with you.

filipeom commented 8 months ago

Malloc's pointer alignment seems not to be completely clearly defined, and even less clearly implemented

Yes you are correct, we do not implement nor have any mechanism to guarantee pointer alignment.

Eric volunteers to fix it and I'll mentor him if it is fine with you.

Of course! Thank you so much! :smiley:

filipeom commented 8 months ago

I don't know if you saw, but this c frontend is moving to owi directly: https://github.com/OCamlPro/owi/pull/100. We might have to patch this there as well

epatrizio commented 8 months ago

Thanks @filipeom @krtab ! It helps me to understand the interface between Owi symbolic and C language https://github.com/OCamlPro/owi/pull/104