Name clash with `free`

[nikswamy]

$ cat Free.fst Free.fsti
module Free

let free (x:bool) = not x

let test (x:bool) = free x

module Free
val test : bool -> bool

$ cat Free.c
/*
  This file was generated by KaRaMeL <https://github.com/FStarLang/karamel>
  KaRaMeL invocation: /home/nswamy/everest/karamel/krml prims.krml FStar_Pervasives_Native.krml FStar_Pervasives.krml Free.krml
  F* version: 46cbaf03
  KaRaMeL version: 70084646
 */

#include "Free.h"



static bool free(bool x)
{
  return !x;
}

bool Free_test(bool x)
{
  return free(x);
}

produces

✘ [CC,./Free.c] (use -verbose to see the output)
./Free.c:12:13: error: conflicting types for ‘free’
   12 | static bool free(bool x)
      |             ^~~~
In file included from /home/nswamy/everest/karamel/include/krml/internal/target.h:7,
                 from /home/nswamy/everest/karamel/include/krmllib.h:19,
                 from ./Free.h:11,
                 from ./Free.c:8:
/usr/include/stdlib.h:565:13: note: previous declaration of ‘free’ was here
  565 | extern void free (void *__ptr) __THROW;
      |             ^~~~
cc1: error: unrecognized command line option ‘-Wno-unknown-warning-option’ [-Werror]
cc1: all warnings being treated as errors

Warning 3: run_or_warn: the following command failed:
gcc-9 -I /home/nswamy/everest/karamel/krmllib/dist/minimal -I /home/nswamy/everest/karamel/krmllib -I /home/nswamy/everest/karamel/include -I . -Wall -Werror -Wno-unused-variable -Wno-unknown-warning-option -Wno-unused-but-set-variable -Wno-unused-function -g -fwrapv -D_BSD_SOURCE -D_DEFAULT_SOURCE -Wno-parentheses -std=c11 -c ./Free.c -o ./Free.o
Warning 3 is fatal, exiting.
make: *** [Makefile:7: all] Error 255

[nikswamy]

cc @tahina-pro @arvinda

[msprotz]

copy-pasting what I wrote on Teams: there's not much I can do since there's potentially an unbounded amount of external definitions in system headers, whatever is defined in headers you pass to -add-include, etc.

note that you would have the same problem if you defined free in your own C file without prefixing it suitably (and note that C compilers don't give you a warning saying "your free function collides with a name from the standard library")

krml has a mechanism for dealing with these name collisions, which is to prefix everything; if you use -no-prefix, there you must handle name collisions yourself

the one thing I can do is add a note to the -no-prefix option saying that you might run into this problem if you elect to use -no-prefix

[nikswamy]

I didn't use -no-prefix in this case. Is it on by default or something?

[tahina-pro]

From what I understood, krml strips (or skips) such prefixes from static functions (here, free does not appear in the interface of module Free)

[msprotz]

Ugh! I thought you had used no-prefix but I was wrong about that. Sorry.

Tahina: you are correct, this is the prefix that gets kicked from static functions for readability. This was a big readability improvement for HACL* and a long-standing request from many of our downstream consumers. This is also in line with standard C practices: no need to prefix a static inline function which does not generate an external symbol.

I'm not sure what can be done in a principled way... I see two not-so-great fixes:

• make this behavior optional (at the expense of verbosity)
• try to add a list of "common" names and avoid colliding with them, although it'll always be brittle because I can't maintain an up-to-date list of what's exported by system headers... it's also tricky because some of the libc functions are treated as compiler builtins and I think I've seen some C compiler allow shadowing something like "sin" or "cos" (or maybe something else).

The other fix is of course to do nothing, although that's a sub-par user experience.

[nikswamy]

I would be happy if there was a way to make this behavior optional.

[arvinda]

Another option might be to support a "--with-prefix=(val)" option, which overrides the default and adds a user-provided namespace/prefix to every function static or otherwise.