Update to Coq 8.17 and CompCert 3.12

11 files changed, 21 insertions, 124 deletions

diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml
index 85a4372..d45587c 100644
--- a/driver/VericertDriver.ml
+++ b/driver/VericertDriver.ml
@@ -49,7 +49,7 @@ let nolink () =
 
 let object_filename sourcename suff =
   if nolink () then
-    output_filename ~final: !option_c sourcename suff ".o"
+    output_filename ~final: !option_c sourcename ~suffix:suff
   else
     tmp_file ".o"
 
@@ -58,7 +58,7 @@ let object_filename sourcename suff =
 let compile_c_file sourcename ifile ofile =
   (* Prepare to dump Clight, RTL, etc, if requested *)
   let set_dest dst opt ext =
-    dst := if !opt then Some (output_filename sourcename ".c" ext)
+    dst := if !opt then Some (output_filename sourcename ~suffix:ext)
       else None in
   set_dest Vericert.Cprint.destination option_dparse ".parsed.c";
   set_dest Vericert.PrintCsyntax.destination option_dcmedium ".compcert.c";
@@ -118,12 +118,12 @@ let compile_i_file sourcename preproname =
         ""
   end else if !option_hls then begin
     compile_c_file sourcename preproname
-      (output_filename ~final:true sourcename ".c" ".v");
+      (output_filename ~final:true sourcename ~suffix:".v");
     ""
   end else begin
     let asmname =
       if !option_dasm
-      then output_filename sourcename ".c" ".s"
+      then output_filename sourcename ~suffix:".s"
       else tmp_file ".s" in
     compile_c_file sourcename preproname asmname;
     let objname = object_filename sourcename ".c" in
@@ -140,7 +140,7 @@ let process_c_file sourcename =
     ""
   end else begin
     let preproname = if !option_dprepro then
-      output_filename sourcename ".c" ".i"
+      output_filename sourcename ~suffix:".i"
     else
       tmp_file ".i" in
     preprocess sourcename preproname;
diff --git a/dune b/dune
index 9bd70aa..3ad2811 100644
--- a/dune
+++ b/dune
@@ -1,4 +1,4 @@
-(dirs :standard \ "./lib/CompCert/x86_32" "./lib/CompCert/powerpc" "./lib/CompCert/riscV"
+(dirs :standard \ "./lib/CompCert/x86_32" "./lib/CompCert/cfrontend" "./lib/CompCert/powerpc" "./lib/CompCert/riscV"
       "./lib/CompCert/arm" "./lib/CompCert/aarch64" "./lib/CompCert/extraction"
       "./lib/CompCert/x86" "./lib/CompCert/x86_64")
 
diff --git a/flake.lock b/flake.lock
index 63ef7a4..a82f06d 100644
--- a/flake.lock
+++ b/flake.lock
@@ -2,11 +2,11 @@
   "nodes": {
     "nixpkgs": {
       "locked": {
-        "lastModified": 1656083042,
-        "narHash": "sha256-G6m/OAIcmoEWeS+DbU70aNv21QB3kZCtJuUo+33s5VY=",
+        "lastModified": 1682591986,
+        "narHash": "sha256-BU5dJ9MmZYsGr1Dnf8p5VV8cSbMKuNiqw4A14/V8pjo=",
         "owner": "nixos",
         "repo": "nixpkgs",
-        "rev": "dc0380bb215ce001fcfccf4609d902115f87ddf9",
+        "rev": "1c8257a313a5eb4d5f86edc2d325a23ff8085b94",
         "type": "github"
       },
       "original": {
diff --git a/flake.nix b/flake.nix
index e01bcd8..06f2cf9 100644
--- a/flake.nix
+++ b/flake.nix
@@ -6,13 +6,13 @@
   outputs = { self, nixpkgs }:
     let vericertDevPackages = pkgs:
           let
-            ncoq = pkgs.coq_8_14;
-            ncoqPackages = pkgs.coqPackages_8_14;
+            ncoq = pkgs.coq_8_17;
+            ncoqPackages = pkgs.coqPackages_8_17;
           in
             pkgs.mkShell {
               buildInputs = with pkgs;
                 [ ncoq ncoq.ocaml ncoqPackages.serapi dune_3 gcc python3 ]
-                ++ (with ncoq.ocamlPackages; [ findlib menhir menhirLib ocamlgraph ocp-indent utop ])
+                ++ (with ncoq.ocamlPackages; [ findlib menhir menhirLib ocamlgraph ocp-indent utop merlin ])
                 ++ (with python3Packages; [ alectryon sphinx_rtd_theme ]);
             };
     in {
diff --git a/lib/CompCert b/lib/CompCert
-Subproject 4f467596f8674f5f4fbf84a793cb8fcfc35a44a
+Subproject ab617cf8e6e60e8de3eb8de220f71dd05c18209
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index aba2fe7..6357531 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -178,7 +178,6 @@ Extraction Blacklist List String Int.
 Extract Inlined Constant Defs.F2R => "fun _ -> assert false".
 Extract Inlined Constant Binary.FF2R => "fun _ -> assert false".
 Extract Inlined Constant Binary.B2R => "fun _ -> assert false".
-Extract Inlined Constant Binary.round_mode => "fun _ -> assert false".
 Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
 
 (*Extract Constant Pipeline.pipeline => "pipelining.pipeline".*)
@@ -187,7 +186,7 @@ Extract Constant GiblePargen.schedule => "Schedule.schedule_fn".
 
 (* Loop normalization *)
 Extract Constant IfConversion.build_bourdoncle => "BourdoncleAux.build_bourdoncle".
-Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".
+(*Extract Constant IfConversion.get_if_conv_t => "(fun _ -> [Maps.PTree.empty; Maps.PTree.empty; Maps.PTree.empty])".*)
 
 (* Needed in Coq 8.4 to avoid problems with Function definitions. *)
 Set Extraction AccessOpaque.
@@ -204,7 +203,8 @@ Separate Extraction
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-   Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
+   Ctypes.merge_attributes Ctypes.remove_attributes 
+   Ctypes.build_composite_env Ctypes.layout_struct
    Initializers.transl_init Initializers.constval
    Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection
    Ctyping.typecheck_program
@@ -216,6 +216,7 @@ Separate Extraction
    Conventions1.int_caller_save_regs Conventions1.float_caller_save_regs
    Conventions1.int_callee_save_regs Conventions1.float_callee_save_regs
    Conventions1.dummy_int_reg Conventions1.dummy_float_reg
+   Conventions1.allocatable_registers
    RTL.instr_defs RTL.instr_uses
    Machregs.mregs_for_operation Machregs.mregs_for_builtin
    Machregs.two_address_op Machregs.is_stack_reg
diff --git a/src/hls/DeadBlocksproof.v b/src/hls/DeadBlocksproof.v
index 7f1da9c..107e206 100644
--- a/src/hls/DeadBlocksproof.v
+++ b/src/hls/DeadBlocksproof.v
@@ -544,7 +544,7 @@ Proof.
   elim H.
 
   intros.
-  elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes.
+  eelim not_seen_sons_prop6 with (1:=TT) (i:=i); auto with datatypes.
   rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes.
   rewrite PTree.gempty in H0; congruence.
 
diff --git a/src/hls/HTLgenproof.v b/src/hls/HTLgenproof.v
index 1089356..4fc00bc 100644
--- a/src/hls/HTLgenproof.v
+++ b/src/hls/HTLgenproof.v
@@ -140,7 +140,7 @@ Definition match_prog (p: RTL.program) (tp: HTL.program) :=
   Linking.match_program (fun cu f tf => transl_fundef f = Errors.OK tf) eq p tp /\
   main_is_internal p = true.
 
-Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
+#[global] Instance TransfHTLLink (tr_fun: RTL.program -> Errors.res HTL.program):
   TransfLink (fun (p1: RTL.program) (p2: HTL.program) => match_prog p1 p2).
 Proof.
   red. intros. exfalso. destruct (link_linkorder _ _ _ H) as [LO1 LO2].
diff --git a/src/hls/HashTree.v b/src/hls/HashTree.v
index 7387401..a088a54 100644
--- a/src/hls/HashTree.v
+++ b/src/hls/HashTree.v
@@ -498,14 +498,14 @@ Module HashTree(H: Hashable).
     forall x, match_one x x.
   Proof. unfold match_one; auto. Qed.
   
-  Instance match_one_Reflexive : Reflexive match_one.
+  #[global] Instance match_one_Reflexive : Reflexive match_one.
   Proof. unfold Reflexive. auto using match_one_refl. Qed.
   
   Lemma match_one_trans :
     forall x y z, match_one x y -> match_one y z -> match_one x z.
   Proof. unfold match_one; auto. Qed.
   
-  Instance match_one_Transitive : Transitive match_one.
+  #[global] Instance match_one_Transitive : Transitive match_one.
   Proof. unfold Transitive. eauto using match_one_trans. Qed.
 
   Lemma hash_value_gt :
diff --git a/src/hls/PipelineOp.v b/src/hls/PipelineOp.v
index 90ccea0..76634a6 100644
--- a/src/hls/PipelineOp.v
+++ b/src/hls/PipelineOp.v
@@ -34,7 +34,7 @@ Require Import vericert.hls.FunctionalUnits.
 Require Import vericert.common.Monad.
 
 Module OptionExtra := MonadExtra(Option).
-Import OptionExtra.MonadNotation.
+(*Import OptionExtra.MonadNotation.*)
 
 Local Open Scope positive.
 
diff --git a/src/hls/Sat.v b/src/hls/Sat.v
index 3924ce7..b5970da 100644
--- a/src/hls/Sat.v
+++ b/src/hls/Sat.v
@@ -372,110 +372,6 @@ Fixpoint interp_alist (al : alist) : asgn :=
   | l :: al' => upd (interp_alist al') l
   end.
 
-(** Here's the final definition!
-
-  This implementation isn't #<i>#quite#</i># what you would expect, since it
-  takes an extra parameter expressing a search tree depth.  Writing the function
-  without that parameter would be trickier when it came to proving termination.
-  In practice, you can just seed the bound with one plus the number of variables
-  in the input, but the function's return type still indicates a possibility for
-  a "time-out" by returning [None].
- *)
-Definition boundedSat: forall (bound : nat) (fm : formula),
-    option ({al : alist | satFormula fm (interp_alist al)}
-            + {forall a, ~satFormula fm a}).
-  refine (fix boundedSat (bound : nat) (fm : formula) {struct bound}
-          : option ({al : alist | satFormula fm (interp_alist al)}
-                    + {forall a, ~satFormula fm a}) :=
-            match bound with
-            | O => None
-            | S bound' =>
-              if isNil fm
-              then Some (inleft _ (exist _ nil _))
-              else match unitPropagate fm with
-                   | Some (inleft (existT _ fm' (exist _ l _))) =>
-                     match boundedSat bound' fm' with
-                     | None => None
-                     | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
-                     | Some (inright _) => Some (inright _ _)
-                     end
-                   | Some (inright _) => Some (inright _ _)
-                   | None =>
-                     let l := chooseSplit fm in
-                     match setFormula fm l with
-                     | inleft (exist _ fm' _) =>
-                       match boundedSat bound' fm' with
-                       | None => None
-                       | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (l :: al) _))
-                       | Some (inright _) =>
-                         match setFormula fm (negate l) with
-                         | inleft (exist _ fm' _) =>
-                           match boundedSat bound' fm' with
-                           | None => None
-                           | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
-                           | Some (inright _) => Some (inright _ _)
-                           end
-                         | inright _ => Some (inright _ _)
-                         end
-                       end
-                     | inright _ =>
-                       match setFormula fm (negate l) with
-                       | inleft (exist _ fm' _) =>
-                         match boundedSat bound' fm' with
-                         | None => None
-                         | Some (inleft (exist _ al _)) => Some (inleft _ (exist _ (negate l :: al) _))
-                         | Some (inright _) => Some (inright _ _)
-                         end
-                       | inright _ => Some (inright _ _)
-                       end
-                     end
-                   end
-            end); simpl; intros; subst; intuition; try generalize dependent (interp_alist al).
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  assert (satFormula fm (upd a0 l)); firstorder.
-  assert (satFormula fm (upd a0 l)); firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  firstorder.
-  destruct (satLit_dec l a);
-    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-  destruct (satLit_dec l a);
-    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-  destruct (satLit_dec l a);
-    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-  destruct (satLit_dec l a);
-    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-  destruct (satLit_dec l a); intuition eauto;
-    assert (satFormula fm (upd a l)); firstorder.
-  destruct (satLit_dec l a); intuition eauto;
-    assert (satFormula fm (upd a l)); firstorder.
-  firstorder.
-  firstorder.
-  destruct (satLit_dec l a); intuition eauto;
-    assert (satFormula fm (upd a (negate l))); firstorder.
-  destruct (satLit_dec l a); intuition eauto;
-    assert (satFormula fm (upd a (negate l))); firstorder.
-  destruct (satLit_dec l a);
-    [assert (satFormula fm (upd a l)) | assert (satFormula fm (upd a (negate l)))]; firstorder.
-Defined.
-
-Definition boundedSatSimple (bound : nat) (fm : formula) :=
-  match boundedSat bound fm with
-  | None => None
-  | Some (inleft (exist _ a _)) => Some (Some a)
-  | Some (inright _) => Some None
-  end.
-
 (*Eval compute in boundedSatSimple 100 nil.
 Eval compute in boundedSatSimple 100 (((true, 1%nat) :: nil) :: ((false, 1%nat) :: nil) :: nil).
 Eval compute in boundedSatSimple 100 (((true, 0) :: nil) :: nil).