Duplicate definitions in generated C

[rmn30]

When attempting to compile the current version of this PR: https://github.com/riscv/sail-riscv/pull/197 I get an error when compiling the C file generated by Sail:

make csim
gcc -g  -I /mnt/rust/.opam/4.14.0/share/sail/lib -I c_emulator   -I c_emulator/SoftFloat-3e/source/include -fcommon -O3 -flto generated_definitions/c/riscv_model_RV64.c c_emulator/riscv_prelude.c c_emulator/riscv_platform_impl.c c_emulator/riscv_platform.c c_emulator/riscv_softfloat.c c_emulator/riscv_sim.c /mnt/rust/.opam/4.14.0/share/sail/lib/*.c -lgmp -lz c_emulator/SoftFloat-3e/build/Linux-RISCV-GCC/softfloat.a -o c_emulator/riscv_sim_RV64
generated_definitions/c/riscv_model_RV64.c:64842:6: error: redefinition of ‘zinternal_errorzIUMemoryOpResultzIozKzK’
 void zinternal_errorzIUMemoryOpResultzIozKzK(struct zMemoryOpResultzIozK *zcbz355, sail_string zfile, sail_int zline, sail_string zs)
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
generated_definitions/c/riscv_model_RV64.c:64623:6: note: previous definition of ‘zinternal_errorzIUMemoryOpResultzIozKzK’ was here
 void zinternal_errorzIUMemoryOpResultzIozKzK(struct zMemoryOpResultzIozK *zcbz350, sail_string zfile, sail_int zline, sail_string zs)
      ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
generated_definitions/c/riscv_model_RV64.c:64885:15: error: redefinition of ‘zinternal_errorzIERetiredz5zK’
 enum zRetired zinternal_errorzIERetiredz5zK(sail_string zfile, sail_int zline, sail_string zs)
               ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
generated_definitions/c/riscv_model_RV64.c:64710:15: note: previous definition of ‘zinternal_errorzIERetiredz5zK’ was here
 enum zRetired zinternal_errorzIERetiredz5zK(sail_string zfile, sail_int zline, sail_string zs)

I've not been able to reproduce in a smaller example yet. I suspect it is something to do with the interesting type of internal_error:

val internal_error : forall ('a : Type). (string, int, string) -> 'a effect {escape}
function internal_error(file, line, s) = {
    assert (false, file ^ ":" ^ string_of_int(line) ^ ": " ^ s);
    throw Error_internal_error()
}

[rmn30]

Also the function I introduced that calls internal_error:

/*!
 * Raise an internal error reporting that width w is invalid for access kind, k,
 * and current xlen. The file name and line number should be passed in as the
 * first two arguments using the __FILE__ and __LINE__ built-in macros.
 * This is mainly used to supress Sail warnings about incomplete matches and
 * should be unreachable. See https://github.com/riscv/sail-riscv/issues/194
 * and https://github.com/riscv/sail-riscv/pull/197 .
 */
val report_invalid_width : forall ('a : Type). (string, int, word_width, string) -> 'a effect {escape}
function report_invalid_width(f , l, w, k) -> 'a = {
  internal_error(f, l, "Invalid width, " ^ size_mnemonic(w) ^ ", for " ^ k ^
    " with xlen=" ^ string_of_int(sizeof(xlen)));
}

[Alasdair]

I guess it probably has something to do with the return type. Do you mean to use throw right after an assert(false) though? The throw will never actually occur.

[Alasdair]

default Order dec

$include <prelude.sail>

infixr 5 ^^

overload operator ^^ = {concat_str}

union exception = {
    Error_internal_error : unit
}

val internal_error : forall ('a : Type). (string, int, string) -> 'a

function internal_error(file, line, s) = {
    assert (false, file ^^ ":" ^^ dec_str(line) ^^ ": " ^^ s);
    throw Error_internal_error()
}

val internal_error_caller : forall ('a : Type). (string, int, string) -> 'a

function internal_error_caller(f , l, k) -> 'a = {
    internal_error(f, l, k);
}

val main : unit -> unit

function main() = {
    internal_error_caller(__FILE__, __LINE__, "message 1");
    internal_error(__FILE__, __LINE__, "message 2");
}

Should be a fairly minimal example

[Alasdair]

What it's doing is it does one round of monomorphisation, specialising internal_error and internal_error_caller, then it does a second round because the call to internal_error within internal_error_caller can now be monomorphised within the body of the specialised internal_error_caller producing the duplicate definition.

[Alasdair]

Should be fixed by https://github.com/rems-project/sail/commit/21314bc82b2877eaadb87d5c1987ca1e3bfed227

[rmn30]

Thanks! Re. the throw at the end of internal_error I think it is required to get it to type check as otherwise Sail is not aware that it never returns? Perhaps it should be rewritten to just throw Internal_Error(string).

[rmn30]

I can confirm it now compiles!

[Alasdair]

If this is needed for the RISC-V spec would it make sense to do a 0.15.1 point release?

[rmn30]

It is blocking the merge of the above PR so yes please. There are also some fixes to SMT I'd like to have in a release :-)

[arichardson]

If this is needed for the RISC-V spec would it make sense to do a 0.15.1 point release?

FYI https://github.com/rems-project/sail/commit/444132c18fff5a3cde45c8a8642f1ed8e923fbdb causes lots of warnings in the RISC-V model. I'm not sure how to fix those so it would be good to check that they are indeed valid warnings before releasing the fix.

[Alasdair]

I made that warning one that only prints at most once so it prints less often. I think most of the issues in the RISC-V spec are valid warnings though. I fixed an issue with spurious warnings for mappings, but the definitions in https://github.com/riscv/sail-riscv/blob/master/model/prelude_mapping.sail are in the wrong order to do what I think is intended so the warnings for those are valid.

[Alasdair]

I will see about making a pull request to fix that file