Generating C const qualifiers

Pre-requisites: http://en.cppreference.com/w/c/language/const.

In C, the const qualifier turns an lvalue into a non-modifiable lvalue. The const qualifier recursively applies to aggregates (i.e. structs and unions), but does not apply to pointed-to objects (i.e. int * const p and const int *p are not the same).

There are three ways we can derive const from the F* semantics.

1) Non-mutable values

F* does not have mutable values; that is, let x = 1 can always be converted to const int x = 1. Similarly, let f (x: Buffer.buffer int) can always be converted to void f(int *const x). Note the placement of the const qualifier: it means that x itself will not be mutated (via, say, x = malloc(...)), but says nothing about whether we're going to modify the contents of the pointed-to buffer. Note: this is equivalent to void f(int x[const]).

We could use the same reasoning to mark inner fields of structs as const, too. We never mutate struct fields directly because F* doesn't support it (yet). Dafny-generated code relies on this, though.

Important note: in C array declarations, the const qualifier is implicit. This means that let x = Buffer.create 2 0 is translated as int x[2] = { 0 } and x is implicitly const. If you try x = malloc(...), this is a compiler error. const int x[2] = { 0 } has a different meaning and means that the pointed-to elements are const, i.e. you cannot modify elements anymore via x[0] = 1.

Digression: mutable values may appear because

• let mutable (currently unused)
• internal KreMLin transformations (expression-to-statement)

2) modifies-clauses on function parameters

Consider:

let f (x: Buffer.buffer int):
  Stack unit
    (requires (fun _ -> True))
    (ensures (fun h0 _ h1 -> modifies_none h0 h1))

The modifies clause tell us that no buffer will be modified through that function call. In particular, this means that we can translate f as:

void f (const int *x) {
  ...
}

That is, the buffer is taken to be "immutable" (in the F* sense of the term), i.e. elements cannot be modified through the x pointer (in the C sense).

Unclear what the performance gains are.

Note: if we carry over modifies clauses, then carrying over disjoint clauses would also allow using restrict, another C type qualifier like const.

3) Immutable buffers

If we had immutable buffers, then we could derive const-ness like above directly from the type. For instance, a p: ibuffer int would always be const int *p no matter what. This would allow marking constants at top-level as const, i.e. turning:

let x = Buffer.icreateL [ 1; 2 ]

into

const int x[] = { 1, 2 }

Conversely, 1) would only allow writing:

int *const x = { 1, 2 }

(this is not what we want)

and 2) doesn't help (we have no modifies clauses at the level of an F* module).