Generate `const` qualifiers

[franziskuskiefer]

It would be nice if Eurydice would generate const qualifiers in C. We have this information in Rust and it would be nice to have it translated into the corresponding C qualifiers.

[msprotz]

I took a first stab at this a while back https://github.com/AeneasVerif/eurydice/tree/protz/preserve_const but don't remember why I didn't go all the way. Let me check.

[msprotz]

So I refreshed the branch and I think the reason why I didn't push on it further is that the gains seemed modest, especially given that slices compile to Eurydice_slice which has a char* as the pointer, so it's not like slices reflect mutability.

This might change with #259 which will make slice a proper type that undergoes monomorphization like any other type.

You can check the files in out/ -- main...protz/preserve_const (some files still have conflict markers and not all tests pass...).

There's also things like this: main...protz/preserve_const#diff-e0f5989854e1ab4d2ff060b0facec16b8fa28b0f110d0e72f78b3b861013fd1fL22 which no one really writes in C, but that Rust keeps track of (nested const qualifier).

Thoughts?

[msprotz]

Sub-issues:

• the EAddrOf node needs a flag (like TBuf) to indicate const vs non-const -- this breaks the global_ref test
  • need to refactor to use something that's not a boolean
• code quality is now impacted due to const/non-const variants
• subtle interactions with monomorphization, again

[ssyram]

I think getting const would make everything more complicated... I'm pretty satisfied with the current code quality as it is brief. Maybe a potential way would be to add additional flag to enable this?

[franziskuskiefer]

Thanks for digging this up @msprotz !

Thoughts?

I think the main issue I see with not having const qualifiers is that using Eurydice generated APIs forces the caller to remove consts from their arguments. Which i) doesn't look great, and ii) shifts the responsibility of keeping track of const/non-const to the caller.

So I think even just having this for the top level functions would help the generated code. I'm not sure if tracking const within the generated code is as important. The question is probably if we think that it would allow the compiler to catch bad generated code.

[msprotz]

I'm not sure if tracking const within the generated code is as important.

If the top-level APIs have const then either the rest of the code uses const, or there has to be cast from const T* to T* which in my opinion looks worse (and makes the generated code look bad).

Let's look at a few examples to see what adding const qualifiers would get us.

Slice borrows (currently). Right now, both fn foo(x: &[T]) and fn foo(x: &mut [T]) produce void foo(Eurydice_slice x) -- you don't get a const qualifier here in C because it's the same Eurydice_slice type for all slices

Slice borrows (with upcoming changes). With #259 on the horizon, this will change, and now fn foo(x: &[T]) will produce typedef struct { const T *ptr; size_t len } Eurydice_slice_00 followed by void foo(Eurydice_slice_00 x); similarly, fn foo(x: &mut [T]) will produce typedef struct { T *ptr; size_t len } Eurydice_slice_01 followed by void foo(Eurydice_slice_01 x) -- note that tracking the const qualifier now generates an additional slice type definition (not necessarily a bad thing -- just pointing it out).

Non-slice borrows. This is where you will get most of the benefits of const -- fn foo (x: &T) (with T != [U]) will produce void foo(const T* x) and fn foo (x: &mut T) will produce void foo (T *x).

Arrays (with upcoming changes). Arrays have a special treatment right now, but soon they will compile to structs containing a data field, and as such will follow the compilation scheme of non-slice borrows.

My feeling was that the APIs from libcrux were all taking slices, so I just want to be transparent that you may not get terribly good improvements in code quality. But on the other hand, if the libcrux APIs take a lot of &Ts where T is not of the form [U], then yes there will be improvements.

@franziskuskiefer what do you think?

@ssyram I don't think the impact is huge -- look at my PR, the changes are not so bad, and I managed to factor out the code of all the builtins. If you are running some sort of analysis on the generated C code, having const is great for you: it gives you more information that may even improve the quality of the analysis. What are you specifically concerned about?

[ssyram]

OK, we had a discussion on this case and agreed that const at the top level would indeed be helpful, though in the cost of seeing a whole bunch of const everywhere (given that Rust is by default const). I think we may have a try to see the effect.

[franziskuskiefer]

If the top-level APIs have const then either the rest of the code uses const, or there has to be cast from const T* to T* which in my opinion looks worse (and makes the generated code look bad).

Yeah, having only the top level API const just means that it would hide the const cast. But I agree that this doesn't look great.

My feeling was that the APIs from libcrux were all taking slices, so I just want to be transparent that you may not get terribly good improvements in code quality. But on the other hand, if the libcrux APIs take a lot of &Ts where T is not of the form [U], then yes there will be improvements.

The APIs that are problematic are the ones where we need to take const bytes for keys and other inputs from the consumer. Most input is const, except for the output, and hence requires a const_cast by the caller right now. That's for [T; N], &[T] and &[T; N] right now.

OK, we had a discussion on this case and agreed that const at the top level would indeed be helpful
I think we may have a try to see the effect.

Great, I agree, seeing what the impact is would be good.

[protz]

I revisited this now that the array PR and metadata PRs have landed. What this means is that:

• whereas previously e.g. &mut[u32] and &[u32] would both generate a typedef struct { uint32_t *ptr; size_t meta; } Eurydice_dst_ref_XX, now there will be BOTH typedef struct { uint32_t *ptr; size_t meta; } Eurydice_dst_ref_XX and typedef struct { const uint32_t *ptr; size_t meta; } Eurydice_dst_ref_XY
• arrays being passed by value, now a function that takes or return an array, instead of taking e.g. uint32_t *arg, or taking uint32_t *dst, now takes or returns an Eurydice_arr_XZ with typedef struct { uint32_t data[4]; } Eurydice_arr_XZ -- no more const or non-const pointer here
• pointers to arrays come in const and non-const flavors, e.g. fn f(x: &[u32; 4]) becomes void f(const Eurydice_arr_XZ *x) and fn f(x: &mut [u32; 4]) becomes void f(Eurydice_arr_XZ *x)
• every single built-in that is currently in abstract syntax in lib/Builtin.ml needs to come in two variants, both const and non-const (see e.g. array_to_slice, and others)

This is going to increase the verbosity, at the expense of generating safer code, which advertises correctly whether or not it mutates through a pointer.

I think some of the verbosity can be recovered with peephole optimizations.

This is on my plate for this week.

[protz]

There is a preview on #324 -- in out/test-array, there are already a few interesting changes. The rest of the work is mostly about missing const annotations.