Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

12 files changed, 84 insertions, 54 deletions

diff --git a/.gitignore b/.gitignore
index eb11c837..e886bc10 100644
--- a/.gitignore
+++ b/.gitignore
@@ -5,6 +5,8 @@
 **.out
 **.tok
 *.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 d2c81266..e248aaf5 100644
--- a/Makefile
+++ b/Makefile
@@ -265,7 +265,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/Makefile.extr b/Makefile.extr
index 51e9be59..f2d06def 100644
--- a/Makefile.extr
+++ b/Makefile.extr
@@ -50,13 +50,12 @@ INCLUDES=$(patsubst %,-I %, $(DIRS))
 # Control of warnings:
 
 WARNINGS=-w +a-4-9-27-42 -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
 
-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 716e5e81..9d5bfcf9 100755
--- a/configure
+++ b/configure
@@ -568,14 +568,14 @@ 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"
         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;;
   "")
@@ -591,15 +591,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
 
@@ -620,8 +620,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."
@@ -715,7 +715,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
 
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/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
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
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)
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)))