load8 vs load_word?

[andres-erbsen]

If we can have multiplication in the AST and still get compiler proofs for rv32im (if the code does not use it), can we have load8 in the AST and still get compiler proof for 32-bit architectures (if the code does not use load8). This would make it easier for the C back-end to satisfy strict aliasing rule (mit-plv/fiat-crypto#821 (comment)).

[samuelgruetter]

Aaww, do you remember when we defined

bedrock2/bedrock2/src/bedrock2/Syntax.v

Line 11 in b28c1dc

Variant access_size := one | two | four | word.

how smart we felt that this automatically allows 8-byte load/store only on 64bit architectures? 😉

Is this not sufficient any more? As in, why couldn't you use access_size.word for load8?

If needed, you could probably change access_size to

  Variant access_size := one | two | four | word | eight.

but before doing that, I'd like to properly understand why it's needed.

[andres-erbsen]

In the idiomatic C translation of these constructs, storing using "store8" and then loading using "loadword" is a strict aliasing violation. And the code that would be calling bedrock2-printed-as-C sure uses uint64_t not uintptr_t.

[andres-erbsen]

Another thought: we could just play safe and stupid with strict aliasing and load larger words in 8-bit chunks in the C back-end... or perhaps have two back-ends, "sane C" and "standard C".

[samuelgruetter]

Could you write bitwidth-specific bedrock2-to-C pretty-printers that never output uintptr_t, but only uint32/64_t?

[andres-erbsen]

Yes, we could. Using the wrong one could lead to really awkward bugs.