From e2d7bba73f52285475da813433c703d7df7ae44a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 27 Apr 2023 16:33:57 +0100 Subject: Update to Coq 8.17 and CompCert 3.12 --- driver/VericertDriver.ml | 10 ++--- dune | 2 +- flake.lock | 6 +-- flake.nix | 6 +-- lib/CompCert | 2 +- src/extraction/Extraction.v | 7 +-- src/hls/DeadBlocksproof.v | 2 +- src/hls/HTLgenproof.v | 2 +- src/hls/HashTree.v | 4 +- src/hls/PipelineOp.v | 2 +- src/hls/Sat.v | 104 -------------------------------------------- 11 files changed, 22 insertions(+), 125 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 index 4f46759..ab617cf 160000 --- a/lib/CompCert +++ b/lib/CompCert @@ -1 +1 @@ -Subproject commit 4f467596f8674f5f4fbf84a793cb8fcfc35a44a2 +Subproject commit ab617cf8e6e60e8de3eb8de220f71dd05c18209f 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 ##quite## 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). -- cgit