Update to Coq 8.14

[mattam82]

This is a WIP PR to update CertiCoq to the latest MetaCoq (with the change of case representation) and Coq 8.14.
I managed to adapt most of the pipeline including the L6 prototype generation.
-I have tested check_roundtrip works in Prototype.v and tried my best to fix gen_case_tree but some bug must have been introduced still. @joom or @john-ml could you have a look?-

Also, I don't know how to resolve the problem with the dependency on flocq+compcert, maybe VST wizards can tell me as we are apparently using the same trick there.
I updated the submodules so you can get the same working environment as myself if you want to test it.

In general, things are simplified for CertiCoq: we no longer need the case branches expansion and stripping we used to do, so we have one phase less (L3->L3_eta disappears, and L3_eta->L4 is simpler).

[mattam82]

I guess @andrew-appel knows best how to update the compcert/ directory for compatibility with 8.14.0, that's the only missing bit now.

[andrew-appel]

We should move to CompCert 3.9, which builds in Coq 8.14, instead of CompCert 3.5, which is (apparently) what's in certicoq/compcert right now. It looks like there's a certicoq branch called compcert-3.7. Perhaps this is a good start. Between CompCert 3.7 and CompCert 3.9, in the subset of the CompCert files that we have here, there is only a very small change (a boolean attribute field has become an option, easy to adapt to).

We should also consider accessing the flocq library directly through opam, instead of copying flocq into a subdirectory of compcert. This feature of CompCert is called "external flocq", and was not available in CompCert 3.5.

I do not suggest moving to CompCert 3.10 at this time, because it will require a bit more work to achieve compatibility with CompCert 3.10's new representation of structure fields.

[mattam82]

Ok, I've updated the compcert files to 3.9 and tried to keep the same subset as before. I installed coq-flocq-3.4.2 from opam and removed the flocq/ directory as well. I could adapt the compiler .v files relatively easily and the printClight / printAST functionality as well. The plugin compiles now and in benchmarks/tests.v runs to completion but I couldn't test the generated code. I had to make one change in the extracted code I'm unsure about, while cutting a new dependency on C2C.atomic_is_static: in compcert-3.9's printCsyntax.ml we have:

let print_globvardecl p  id v =
  let name = extern_atom id in
  let name = if v.gvar_readonly then "const "^name else name in
  let linkage = if C2C.atom_is_static id then "static" else "extern" in
  fprintf p "%s %s;@ @ " linkage (name_cdecl name v.gvar_info)

I modifed it to have linkage = "extern" in all cases, but I'm not sure that's the right choice. In general, printClight and printCsyntax seemed to be modified in a non-trivial way for certicoq, so that should be reviewed carefully.

[andrew-appel]

I think linkage="extern" in all cases is fine for now.

[mattam82]

The CI is all green now, but that doesn't mean that certicoq works, I don't know if it would be preferable to merge now (so we can all move to 8.14) or wait until someone can check that it behaves properly.

[intoverflow]

I pulled the branch last night and setup a new opam switch. Confirmed that everything builds; will deep dive into the tests (+ uvrooster) tonight or tomorrow

Copy/paste setup commands for anyone else following along:

opam switch create coq-8.14 ocaml-system
eval $(opam env)
opam repo --switch=coq-8.14 add coq-released https://coq.inria.fr/opam/released
opam update --switch=coq-8.14
opam install --switch=coq-8.14 coq.8.14.0 coq-flocq.3.4.2

git clone [email protected]:mattam82/certicoq.git
cd certicoq
git checkout -b master-coq-8.14
git pull origin master-coq-8.14
git submodule update --init --recursive

pushd submodules/Equations
opam install --switch=coq-8.14 ./coq-equations.opam
popd

pushd submodules/coq-ext-lib
opam install --switch=coq-8.14 ./coq-ext-lib.opam
popd

pushd submodules/metacoq
opam install --switch=coq-8.14 ./*.opam
popd

opam exec --switch=coq-8.14 -- make -j 4
opam exec --switch=coq-8.14 -- make plugin

[intoverflow]

I tested the benchmarks directory. I had to update benchmarks/Makefile (diff below; note the -I argument) to help Coq find the CertiCoq plugin.

The build fails for demo1.c but I suspect the fix will be easy. The error can be replicated by applying the Makefile diff and running make -C benchmarks all. I've included a sample of the build errors & the relevant code down below.

Makefile diff

tcarstens@pop-os:~/formal_methods/8.14/certicoq/benchmarks$ git diff Makefile
diff --git a/benchmarks/Makefile b/benchmarks/Makefile
index 094cacef..a5b314cf 100644
--- a/benchmarks/Makefile
+++ b/benchmarks/Makefile
@@ -1,4 +1,4 @@
-COQOPTS = -R ../theories/compcert compcert -R ./ CertiCoq.Benchmarks -R lib CertiCoq.Benchmarks.lib
+COQOPTS = -R ../theories/compcert compcert -I ../plugin/ -R ../plugin/ CertiCoq.Plugin -R ./ CertiCoq.Benchmarks -R lib CertiCoq.Benchmarks.lib
 CCOMPILER=gcc
 
 # Names of the benchmarks
tcarstens@pop-os:~/formal_methods/8.14/certicoq/benchmarks$

Build error messages

This is a representative sample of the build errors for demo1.c:

CertiCoq.Benchmarks.tests.demo1.c:48:3: error: ‘$alloc’ undeclared (first use in this function); did you mean ‘alloc’?
   48 |   $alloc = (*$tinfo).alloc;
      |   ^~~~~~
      |   alloc
CertiCoq.Benchmarks.tests.demo1.c:48:3: note: each undeclared identifier is reported only once for each function it appears in
CertiCoq.Benchmarks.tests.demo1.c:49:3: error: ‘$limit’ undeclared (first use in this function); did you mean ‘limit’?
   49 |   $limit = (*$tinfo).limit;
      |   ^~~~~~
      |   limit
CertiCoq.Benchmarks.tests.demo1.c:50:3: error: ‘$args’ undeclared (first use in this function); did you mean ‘args’?
   50 |   $args = (*$tinfo).args;
      |   ^~~~~
      |   args
CertiCoq.Benchmarks.tests.demo1.c:54:8: error: ‘l_112’ undeclared (first use in this function); did you mean ‘$l_112’?
   54 |   if ((l_112 & 1) == 0) {
      |        ^~~~~
      |        $l_112

The glue code is also impacted:

glue.CertiCoq.Benchmarks.tests.demo1.c:274:7: error: ‘$args’ undeclared (first use in this function); did you mean ‘args’?
  274 |       $args = get_Coq_Init_Datatypes_S_args(v);
      |       ^~~~~
      |       args
glue.CertiCoq.Benchmarks.tests.demo1.c:274:45: error: ‘v’ undeclared (first use in this function); did you mean ‘$v’?
  274 |       $args = get_Coq_Init_Datatypes_S_args(v);
      |                                             ^
      |                                             $v

Here is the glue code from the error above. Note the names of the variables:

void print_Coq_Init_Datatypes_nat(unsigned long long $v)
{
  unsigned int tag;
  void *args;
  $tag = get_Coq_Init_Datatypes_nat_tag($v);
  switch (tag) {
    case 0:
      printf(*(names_of_Coq_Init_Datatypes_nat + tag));
      break;
    case 1:
      $args = get_Coq_Init_Datatypes_S_args(v);
      printf(lparen_lit);
      printf(*(names_of_Coq_Init_Datatypes_nat + tag));
      printf(space_lit);
      print_Coq_Init_Datatypes_nat(*((unsigned long long *) args + 0));
      printf(rparen_lit);
      break;

  }
}

[joom]

@intoverflow I'm getting PHP flashbacks :) Jokes aside, this can be fixed by either

1. Redefining temp_name in PrintClight.ml so that it doesn't prepend $ to names.
2. Changing all uses of Sset to Sassign in theories/Glue.

[intoverflow]

@joomy I think there's more going on here. I just tried both of the proposes fixes but neither works.

Would you mind taking a look?

Are we mixing Evar and Etempvar? Is it OK to mix them?

For example, consider this function in glue.v:

certicoq/theories/Glue/glue.v

Line 526 in 6cda38e

Definition generate_printer

Here we declare v:

certicoq/theories/Glue/glue.v

Line 544 in 6cda38e

_v <- gensym "v" ;;

Here we use it as an Evar:

certicoq/theories/Glue/glue.v

Line 709 in 6cda38e

(Evar _v val :: nil) ;;;

Here we use it as an Etempvar:

certicoq/theories/Glue/glue.v

Line 727 in 6cda38e

((Etempvar _v val) :: nil) ;;;

The problem is not unique to the printing functions

Here is some C code from the benchmarks (CertiCoq.Benchmarks.tests.demo1.c). Note that sometimes l1_113 has $, but not always:

void app_uncurried_102(struct thread_info *$tinfo, unsigned long long $m_111, unsigned long long $l_112)
{
  unsigned long long l1_113;
  unsigned long long a_114;
  unsigned long long y_115;
  unsigned long long y_116;
  struct stack_frame frame;
  unsigned long long root[2];
  unsigned long long *alloc;
  unsigned long long *limit;
  unsigned long long *args;
  _Bool arg;
  $alloc = (*$tinfo).alloc;
  $limit = (*$tinfo).limit;
  $args = (*$tinfo).args;
  frame.next = root;
  frame.root = root;
  frame.prev = (*$tinfo).fp;
  if ((l_112 & 1) == 0) {
    switch (*((unsigned long long *) $l_112 + 18446744073709551615LLU)
              & 255LLU) {
      default:
        $l1_113 = *((unsigned long long *) $l_112 + 0LLU);

[intoverflow]

@mattam82 Thank you again for putting this together. I have diagnosed and fixed the issues in the code generator (see branch https://github.com/CertiCoq/certicoq/tree/coq-8.14/main). With those fixes now in place, I can confirm that your PR works as intended.

In the interest of moving fast, I will merge your PR then follow-up with a separate PR for the fixes.