From 39278439ad26cb5eb22b496066c0f044c33ef28b Mon Sep 17 00:00:00 2001 From: "xavier.leroy" Date: Sat, 25 Jan 2020 18:59:33 -0600 Subject: Reduce the checking time for the "decidable_equality_from" tactic Just moved a frequent failure case ahead of a costly "simpl". --- lib/BoolEqual.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/lib/BoolEqual.v b/lib/BoolEqual.v index c9e7bad5..e8c1d831 100644 --- a/lib/BoolEqual.v +++ b/lib/BoolEqual.v @@ -106,8 +106,8 @@ Ltac bool_eq_refl_case := end. Ltac bool_eq_refl := - let H := fresh "Hrec" in let x := fresh "x" in - fix H 1; intros x; destruct x; simpl; bool_eq_refl_case. + let Hrec := fresh "Hrec" in let x := fresh "x" in + fix Hrec 1; intros x; destruct x; simpl; bool_eq_refl_case. Lemma false_not_true: forall (P: Prop), false = true -> P. @@ -124,7 +124,6 @@ Qed. Ltac bool_eq_sound_case := match goal with - | [ H: false = true |- _ ] => exact (false_not_true _ H) | [ H: _ && _ = true |- _ ] => apply andb_prop in H; destruct H; bool_eq_sound_case | [ H: proj_sumbool ?a = true |- _ ] => apply proj_sumbool_true in H; bool_eq_sound_case | [ |- ?C ?x1 ?x2 ?x3 ?x4 = ?C ?y1 ?y2 ?y3 ?y4 ] => apply f_equal4; auto @@ -137,7 +136,9 @@ Ltac bool_eq_sound_case := Ltac bool_eq_sound := let Hrec := fresh "Hrec" in let x := fresh "x" in let y := fresh "y" in - fix Hrec 1; intros x y; destruct x, y; simpl; intro; bool_eq_sound_case. + let H := fresh "EQ" in + fix Hrec 1; intros x y; destruct x, y; intro H; + try (apply (false_not_true _ H)); simpl in H; bool_eq_sound_case. Lemma dec_eq_from_bool_eq: forall (A: Type) (f: A -> A -> bool) -- cgit From 3e5fba812749b9240b655a99809e62231d1145aa Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 5 Feb 2020 18:31:20 +0100 Subject: Incorrect computation of extra stack size for vararg calls in RISC-V (#213) Currently, the extra size for the variable arguments is too small for the 64 bit RISC-V and the extra arguments are stored in the wrong stack slots. --- riscV/Asmexpand.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index 3e734747..1df63308 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -483,7 +483,7 @@ let expand_instruction instr = emit (Pmv (X30, X2)); if sg.sig_cc.cc_vararg then begin let n = arguments_size sg in - let extra_sz = if n >= 8 then 0 else align 16 ((8 - n) * wordsize) in + let extra_sz = if n >= 8 then 0 else align ((8 - n) * wordsize) 16 in let full_sz = Z.add sz (Z.of_uint extra_sz) in expand_addptrofs X2 X2 (Ptrofs.repr (Z.neg full_sz)); expand_storeind_ptr X30 X2 ofs; @@ -501,7 +501,7 @@ let expand_instruction instr = let extra_sz = if sg.sig_cc.cc_vararg then begin let n = arguments_size sg in - if n >= 8 then 0 else align 16 ((8 - n) * wordsize) + if n >= 8 then 0 else align ((8 - n) * wordsize) 16 end else 0 in expand_addptrofs X2 X2 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz))) -- cgit From b0fdbb0e88d6decd068709ea673dbe51fd6727b0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Feb 2020 18:33:13 +0100 Subject: Support Coq 8.11.0 (#212) Update configure. Ignore and clean up .vok and .vos files, which Coq 8.11.0 generates. --- .gitignore | 2 ++ Changelog | 4 ++++ Makefile | 2 +- configure | 2 +- 4 files changed, 8 insertions(+), 2 deletions(-) diff --git a/.gitignore b/.gitignore index 4b497387..da883cff 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1,7 @@ # Object files, in general *.vo +*.vok +*.vos *.glob *.o *.a diff --git a/Changelog b/Changelog index 935f77f2..08586da5 100644 --- a/Changelog +++ b/Changelog @@ -1,3 +1,7 @@ +Coq development: +- Compatibility with Coq version 8.11.0 (#316) + + Release 3.6, 2019-09-17 ======================= diff --git a/Makefile b/Makefile index 80eca80d..af069e3f 100644 --- a/Makefile +++ b/Makefile @@ -258,7 +258,7 @@ endif clean: - rm -f $(patsubst %, %/*.vo, $(DIRS)) + rm -f $(patsubst %, %/*.vo*, $(DIRS)) rm -f $(patsubst %, %/.*.aux, $(DIRS)) rm -rf doc/html doc/*.glob rm -f driver/Version.ml diff --git a/configure b/configure index b964c124..d91bfebf 100755 --- a/configure +++ b/configure @@ -530,7 +530,7 @@ missingtools=false echo "Testing Coq... " | tr -d '\n' coq_ver=$(${COQBIN}coqc -v 2>/dev/null | sed -n -e 's/The Coq Proof Assistant, version \([^ ]*\).*$/\1/p') case "$coq_ver" in - 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2) + 8.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2|8.11.0) echo "version $coq_ver -- good!";; ?*) echo "version $coq_ver -- UNSUPPORTED" -- cgit From 6950ac8fb096768cb3811ae7f89d0db080bf965a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 5 Feb 2020 18:36:08 +0100 Subject: Revised menhirLib autoconfiguration (#331) Since Menhir version 20200123, we need to link with menhirLib.cmxa instead of menhirLib.cmx. This commit chooses automatically the file to link with: menhirLib.cmxa if it exists in the menhirLib installation directory, menhirLib.cmx otherwise. To reliably find the installation directory, configure was changed to record the menhirLib directory in Makefile.config, variable MENHIR_DIR, instead of a pre-cooked command-line option MENHIR_INCLUDES. Makefile.extr was adapted accordingly. Fixes: #329 Closes: #330 --- Makefile.extr | 2 +- Makefile.menhir | 6 +++++- configure | 6 +++--- 3 files changed, 9 insertions(+), 5 deletions(-) diff --git a/Makefile.extr b/Makefile.extr index d375fd29..7b59ed24 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -55,7 +55,7 @@ extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60 cparser/pre_parser.cmx: WARNINGS += -w -41 cparser/pre_parser.cmo: WARNINGS += -w -41 -COMPFLAGS+=-g $(INCLUDES) $(MENHIR_INCLUDES) $(WARNINGS) +COMPFLAGS+=-g $(INCLUDES) -I "$(MENHIR_DIR)" $(WARNINGS) # Using .opt compilers if available diff --git a/Makefile.menhir b/Makefile.menhir index 98bfc750..7909b2f6 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -41,7 +41,11 @@ MENHIR_FLAGS = -v --no-stdlib -la 1 # Using Menhir in --table mode requires MenhirLib. ifeq ($(MENHIR_TABLE),true) - MENHIR_LIBS = menhirLib.cmx + ifeq ($(wildcard $(MENHIR_DIR)/menhirLib.cmxa),) + MENHIR_LIBS = menhirLib.cmx + else + MENHIR_LIBS = menhirLib.cmxa + endif else MENHIR_LIBS = endif diff --git a/configure b/configure index d91bfebf..a8efb551 100755 --- a/configure +++ b/configure @@ -582,8 +582,8 @@ case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" - menhir_include_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') - if test -z "$menhir_include_dir"; then + menhir_dir=$(menhir --suggest-menhirLib | tr -d '\r' | tr '\\' '/') + if test -z "$menhir_dir"; then echo "Error: cannot determine the location of the Menhir API library." echo "This can be due to an incorrect Menhir package." echo "Consider using the OPAM package for Menhir." @@ -677,7 +677,7 @@ MANDIR=$sharedir/man SHAREDIR=$sharedir COQDEVDIR=$coqdevdir OCAML_OPT_COMP=$ocaml_opt_comp -MENHIR_INCLUDES=-I "$menhir_include_dir" +MENHIR_DIR=$menhir_dir COMPFLAGS=-bin-annot EOF -- cgit From d5435a34169d92a96f1436128f3e90df7f4f9e9a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 6 Feb 2020 17:27:05 +0100 Subject: Compatibility with OCaml 4.10 (#214) debug/DwarfPrinter.mli: unused functor parameter trigger warning 69, replace by non-dependent functor type. Makefile.extr: turn warning 69 (unused functor parameter) off for extracted code configure: accept OCaml versions above 4.09 configure: update messages for unsupported versions of OCaml and Coq --- Makefile.extr | 4 ++-- configure | 8 ++++---- debug/DwarfPrinter.mli | 2 +- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Makefile.extr b/Makefile.extr index 7b59ed24..5948bfc6 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -50,8 +50,8 @@ INCLUDES=$(patsubst %,-I %, $(DIRS)) # Control of warnings: WARNINGS=-w +a-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 -extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60 -extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60 +extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67 +extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45-60-67 cparser/pre_parser.cmx: WARNINGS += -w -41 cparser/pre_parser.cmo: WARNINGS += -w -41 diff --git a/configure b/configure index a8efb551..6bd7ed0e 100755 --- a/configure +++ b/configure @@ -537,7 +537,7 @@ case "$coq_ver" in if $ignore_coq_version; then echo "Warning: this version of Coq is unsupported, proceed at your own risks." else - echo "Error: CompCert requires one of the following Coq versions: 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" + echo "Error: CompCert requires one of the following Coq versions: 8.11.0, 8.10.2, 8.10.1, 8.10.0, 8.9.1, 8.9.0, 8.8.2, 8.8.1, 8.8.0" missingtools=true fi;; "") @@ -553,15 +553,15 @@ case "$ocaml_ver" in echo "version $ocaml_ver -- UNSUPPORTED" echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; - 4.0*) + 4.*) echo "version $ocaml_ver -- good!";; ?.*) echo "version $ocaml_ver -- UNSUPPORTED" - echo "Error: CompCert requires OCaml version 4.02 or later." + echo "Error: CompCert requires OCaml version 4.05 or later." missingtools=true;; *) echo "NOT FOUND" - echo "Error: make sure OCaml version 4.02 or later is installed." + echo "Error: make sure OCaml version 4.05 or later is installed." missingtools=true;; esac diff --git a/debug/DwarfPrinter.mli b/debug/DwarfPrinter.mli index e1e10601..78dc05fb 100644 --- a/debug/DwarfPrinter.mli +++ b/debug/DwarfPrinter.mli @@ -12,7 +12,7 @@ open DwarfTypes -module DwarfPrinter: functor (Target: DWARF_TARGET) -> +module DwarfPrinter: DWARF_TARGET -> sig val print_debug: out_channel -> debug_entries -> unit end -- cgit From 6ca9f9bfc7119f1ca4f48de3b5a37cbaee07e4fd Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 6 Feb 2020 14:55:34 +0100 Subject: Added base address if needed. Ranges of locations are relative to some base address. Most times this is just the same as the compilation unit. However if the compilation unit contains functions in multiple sections we need to add a base address of the section that the locations are contained. --- debug/DwarfPrinter.ml | 45 +++++++++++++++++++++++++-------------------- debug/DwarfTypes.mli | 25 +++++++++++++++++-------- debug/Dwarfgen.ml | 16 +++++++++++----- 3 files changed, 53 insertions(+), 33 deletions(-) diff --git a/debug/DwarfPrinter.ml b/debug/DwarfPrinter.ml index 9a24041b..2cb8c7d9 100644 --- a/debug/DwarfPrinter.ml +++ b/debug/DwarfPrinter.ml @@ -602,8 +602,13 @@ module DwarfPrinter(Target: DWARF_TARGET): print_sleb128 oc "" 0; print_label oc debug_end (* End of the debug section *) - let print_location_entry oc c_low l = + let print_location_entry oc needs_base c_low l = print_label oc (loc_to_label l.loc_id); + (* If we have multiple ranges per compilation unit we need to specify a base address for the location *) + if needs_base then begin + fprintf oc " %s -1\n" address; + fprintf oc " %s %a\n" address label c_low; + end; List.iter (fun (b,e,loc) -> fprintf oc " %s %a-%a\n" address label b label c_low; fprintf oc " %s %a-%a\n" address label e label c_low; @@ -621,11 +626,11 @@ module DwarfPrinter(Target: DWARF_TARGET): fprintf oc " %s 0\n" address - let print_location_list oc (c_low,l) = - let f = match c_low with - | Some s -> print_location_entry oc s - | None -> print_location_entry_abs oc in - List.iter f l + let print_location_list oc needs_base l = + let f l = match l.loc_sec_begin with + | Some s -> print_location_entry oc needs_base s l + | None -> print_location_entry_abs oc l in + List.iter f l let list_opt l f = match l with @@ -635,15 +640,15 @@ module DwarfPrinter(Target: DWARF_TARGET): let print_diab_entries oc entries = let abbrev_start = new_label () in abbrev_start_addr := abbrev_start; - List.iter (fun e -> compute_abbrev e.entry) entries; + List.iter (fun e -> compute_abbrev e.diab_entry) entries; print_abbrev oc; List.iter (fun e -> let name = if e.section_name <> ".text" then Some e.section_name else None in section oc (Section_debug_info name); - print_debug_info oc e.start_label e.line_label e.entry) entries; - if List.exists (fun e -> match e.dlocs with _,[] -> false | _,_ -> true) entries then begin + print_debug_info oc e.start_label e.line_label e.diab_entry) entries; + if List.exists (fun e -> match e.diab_locs with [] -> false | _ -> true) entries then begin section oc Section_debug_loc; - List.iter (fun e -> print_location_list oc e.dlocs) entries + List.iter (fun e -> print_location_list oc false e.diab_locs) entries end let print_ranges oc r = @@ -665,8 +670,8 @@ module DwarfPrinter(Target: DWARF_TARGET): fprintf oc " %s 0\n" address; fprintf oc " %s 0\n" address) r - let print_gnu_entries oc cp (lpc,loc) s r = - compute_abbrev cp; + let print_gnu_entries oc entries = + compute_abbrev entries.gnu_entry; let line_start = new_label () and start = new_label () and abbrev_start = new_label () @@ -674,18 +679,18 @@ module DwarfPrinter(Target: DWARF_TARGET): debug_ranges_addr := range_label; abbrev_start_addr := abbrev_start; section oc (Section_debug_info None); - print_debug_info oc start line_start cp; + print_debug_info oc start line_start entries.gnu_entry; print_abbrev oc; - list_opt loc (fun () -> + list_opt entries.gnu_locs (fun () -> section oc Section_debug_loc; - print_location_list oc (lpc,loc)); - list_opt r (fun () -> - print_ranges oc r); + print_location_list oc entries.several_secs entries.gnu_locs); + list_opt entries.range_table (fun () -> + print_ranges oc entries.range_table); section oc (Section_debug_line None); print_label oc line_start; - list_opt s (fun () -> + list_opt entries.string_table (fun () -> section oc Section_debug_str; - let s = List.sort (fun (a,_) (b,_) -> compare a b) s in + let s = List.sort (fun (a,_) (b,_) -> compare a b) entries.string_table in List.iter (fun (id,s) -> print_label oc (loc_to_label id); fprintf oc " .asciz %S\n" s) s) @@ -698,6 +703,6 @@ module DwarfPrinter(Target: DWARF_TARGET): Hashtbl.clear loc_labels; match debug with | Diab entries -> print_diab_entries oc entries - | Gnu (cp,loc,s,r) -> print_gnu_entries oc cp loc s r + | Gnu entries -> print_gnu_entries oc entries end diff --git a/debug/DwarfTypes.mli b/debug/DwarfTypes.mli index 5a2bce3b..567c65cd 100644 --- a/debug/DwarfTypes.mli +++ b/debug/DwarfTypes.mli @@ -266,11 +266,13 @@ type dw_entry = (* The type for the location list. *) type location_entry = - { - loc: (address * address * location_value) list; - loc_id: reference; - } -type dw_locations = constant option * location_entry list + { + loc: (address * address * location_value) list; + loc_id: reference; + loc_sec_begin : address option; + } + +type dw_locations = location_entry list type range_entry = | AddressRange of (address * address) list @@ -285,13 +287,20 @@ type diab_entry = section_name: string; start_label: int; line_label: int; - entry: dw_entry; - dlocs: dw_locations; + diab_entry: dw_entry; + diab_locs: dw_locations; } type diab_entries = diab_entry list -type gnu_entries = dw_entry * dw_locations * dw_string * dw_ranges +type gnu_entries = + { + string_table: dw_string; + range_table: dw_ranges; + gnu_locs: dw_locations; + gnu_entry: dw_entry; + several_secs: bool; + } type debug_entries = | Diab of diab_entries diff --git a/debug/Dwarfgen.ml b/debug/Dwarfgen.ml index e1b71f13..6c1d0846 100644 --- a/debug/Dwarfgen.ml +++ b/debug/Dwarfgen.ml @@ -408,7 +408,7 @@ module Dwarfgenaux (Target: TARGET) = and lo = translate_label f_id lo in hi,lo,range_entry_loc i.var_loc) l in let id = next_id () in - Some (LocRef id),[{loc = l;loc_id = id;}] + Some (LocRef id),[{loc_sec_begin = !current_section_start; loc = l;loc_id = id;}] end with Not_found -> None,[] else @@ -574,8 +574,8 @@ let diab_gen_compilation_section sec_name s defs acc = section_name = s; start_label = debug_start; line_label = line_start; - entry = cp; - dlocs = Some low_pc,accu.locs; + diab_entry = cp; + diab_locs = accu.locs; }::acc let gen_diab_debug_info sec_name var_section : debug_entries = @@ -643,6 +643,12 @@ let gen_gnu_debug_info sec_name var_section : debug_entries = } in let cp = new_entry (next_id ()) (DW_TAG_compile_unit cp) in let cp = add_children cp (types@defs) in - let loc_pc = if StringSet.cardinal sec > 1 then None else low_pc in let string_table = Hashtbl.fold (fun s i acc -> (i,s)::acc) string_table [] in - Gnu (cp,(loc_pc,accu.locs),string_table,snd accu.ranges) + let cp = { + string_table = string_table; + range_table = snd accu.ranges; + gnu_locs = accu.locs; + gnu_entry = cp; + several_secs = StringSet.cardinal sec > 1} + in + Gnu cp -- cgit