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

7 files changed, 74 insertions, 124 deletions

diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
index ab155e9c..55922e9e 100644
--- a/aarch64/Asmexpand.ml
+++ b/aarch64/Asmexpand.ml
@@ -408,13 +408,28 @@ let expand_instruction instr =
   | _ ->
      emit instr
 
-let int_reg_to_dwarf r = 0              (* TODO *)
-
-let float_reg_to_dwarf r = 0            (* TODO *)
+let int_reg_to_dwarf = function
+  | X0 -> 0 | X1 -> 1 | X2 -> 2 | X3 -> 3 | X4 -> 4
+  | X5 -> 5 | X6 -> 6 | X7 -> 7 | X8 -> 8 | X9 -> 9
+  | X10 -> 10 | X11 -> 11 | X12 -> 12 | X13 -> 13 | X14 -> 14
+  | X15 -> 15 | X16 -> 16 | X17 -> 17 | X18 -> 18 | X19 -> 19
+  | X20 -> 20 | X21 -> 21 | X22 -> 22 | X23 -> 23 | X24 -> 24
+  | X25 -> 25 | X26 -> 26 | X27 -> 27 | X28 -> 28 | X29 -> 29
+  | X30 -> 30
+
+let float_reg_to_dwarf = function
+  | D0 -> 64 | D1 -> 65 | D2 -> 66 | D3 -> 67 | D4 -> 68
+  | D5 -> 69 | D6 -> 70 | D7 -> 71 | D8 -> 72 | D9 -> 73
+  | D10 -> 74 | D11 -> 75 | D12 -> 76 | D13 -> 77 | D14 -> 78
+  | D15 -> 79 | D16 -> 80 | D17 -> 81 | D18 -> 82 | D19 -> 83
+  | D20 -> 84 | D21 -> 85 | D22 -> 86 | D23 -> 87 | D24 -> 88
+  | D25 -> 89 | D26 -> 90 | D27 -> 91 | D28 -> 92 | D29 -> 93
+  | D30 -> 94 | D31 -> 95
 
 let preg_to_dwarf = function
    | IR r -> int_reg_to_dwarf r
    | FR r -> float_reg_to_dwarf r
+   | SP -> 31
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index c7332329..0c72c7cc 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -20,6 +20,11 @@ Local Open Scope string_scope.
 Local Open Scope list_scope.
 Local Open Scope error_monad_scope.
 
+(** Alignment check for symbols *)
+
+Parameter symbol_is_aligned : ident -> Z -> bool.
+(** [symbol_is_aligned id sz] checks whether the symbol [id] is [sz] aligned *)
+
 (** Extracting integer or float registers. *)
 
 Definition ireg_of (r: mreg) : res ireg :=
@@ -942,7 +947,7 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg)
                            (insn (ADimm X16 Int64.zero) :: k))
   | Aglobal id ofs, nil =>
       assertion (negb (Archi.pic_code tt));
-      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero
+      if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz
       then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k)
       else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k))
   | Ainstack ofs, nil =>
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 245eeb62..b622a0bb 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -1592,7 +1592,7 @@ Proof.
   simpl; rewrite Int64.add_zero; auto.
   intros. apply C; eauto with asmgen.
 - (* Aglobal *)
-  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero); inv TR.
+  destruct (Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz); inv TR.
 + econstructor; econstructor; split.
   apply exec_straight_opt_intro. apply exec_straight_one. simpl; eauto. auto.
   split. simpl. Simpl. rewrite symbol_high_low. simpl in EV. congruence.
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index a447d12f..e82056e2 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -21,3 +21,4 @@ Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
 (* Asm *)
 Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false".
 Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false".
+Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned".
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index dc25b516..24e3cacf 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -61,6 +61,11 @@ let atom_alignof a =
   with Not_found ->
     None
 
+let atom_is_aligned a sz =
+  match atom_alignof a with
+  | None -> false
+  | Some align -> align mod (Z.to_int sz) = 0
+
 let atom_sections a =
   try
     (Hashtbl.find decl_atom a).a_sections
diff --git a/configure b/configure
index 142222c4..b8555973 100755
--- a/configure
+++ b/configure
@@ -568,7 +568,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.8.0|8.8.1|8.8.2|8.9.0|8.9.1|8.10.0|8.10.1|8.10.2)
         echo "version $coq_ver -- good!";;
   ?*)
         echo "version $coq_ver -- UNSUPPORTED"
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 012e4b66..7957375c 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -104,30 +104,46 @@ type warning_type =
   | Reduced_alignment
   | Non_linear_cond_expr
 
+(* List of all warnings with default status.
+   "true" means the warning is active by default.
+   "false" means the warning is off by default. *)
+let all_warnings =
+  [ (Unnamed, true);
+    (Unknown_attribute, true);
+    (Zero_length_array, false);
+    (Celeven_extension, false);
+    (Gnu_empty_struct, true);
+    (Missing_declarations, true);
+    (Constant_conversion, true);
+    (Int_conversion, true);
+    (Varargs, true);
+    (Implicit_function_declaration, true);
+    (Pointer_type_mismatch, true);
+    (Compare_distinct_pointer_types, true);
+    (Implicit_int, true);
+    (Main_return_type, true);
+    (Invalid_noreturn, true);
+    (Return_type, true);
+    (Literal_range, true);
+    (Unknown_pragmas, false);
+    (CompCert_conformance, false);
+    (Inline_asm_sdump, true);
+    (Unused_variable, false);
+    (Unused_parameter, false);
+    (Wrong_ais_parameter, true);
+    (Unused_ais_parameter, true);
+    (Ignored_attributes, true);
+    (Extern_after_definition, true);
+    (Static_in_inline, true);
+    (Flexible_array_extensions, false);
+    (Tentative_incomplete_static, false);
+    (Reduced_alignment, false);
+    (Non_linear_cond_expr, false);
+  ]
+
 (* List of active warnings *)
-let active_warnings: warning_type list ref = ref [
-  Unnamed;
-  Unknown_attribute;
-  Gnu_empty_struct;
-  Missing_declarations;
-  Constant_conversion;
-  Int_conversion;
-  Varargs;
-  Implicit_function_declaration;
-  Pointer_type_mismatch;
-  Compare_distinct_pointer_types;
-  Implicit_int;
-  Main_return_type;
-  Invalid_noreturn;
-  Return_type;
-  Literal_range;
-  Inline_asm_sdump;
-  Wrong_ais_parameter;
-  Unused_ais_parameter;
-  Ignored_attributes;
-  Extern_after_definition;
-  Static_in_inline;
-]
+let active_warnings: warning_type list ref =
+  ref (List.map fst (List.filter snd all_warnings))
 
 (* List of errors treated as warning *)
 let error_warnings: warning_type list ref = ref []
@@ -188,76 +204,14 @@ let warning_not_as_error w () =
 
 (* Activate all warnings *)
 let wall () =
-  active_warnings:=[
-    Unnamed;
-    Unknown_attribute;
-    Zero_length_array;
-    Celeven_extension;
-    Gnu_empty_struct;
-    Missing_declarations;
-    Constant_conversion;
-    Int_conversion;
-    Varargs;
-    Implicit_function_declaration;
-    Pointer_type_mismatch;
-    Compare_distinct_pointer_types;
-    Implicit_int;
-    Main_return_type;
-    Invalid_noreturn;
-    Return_type;
-    Literal_range;
-    Unknown_pragmas;
-    CompCert_conformance;
-    Inline_asm_sdump;
-    Unused_variable;
-    Unused_parameter;
-    Wrong_ais_parameter;
-    Ignored_attributes;
-    Extern_after_definition;
-    Static_in_inline;
-    Flexible_array_extensions;
-    Tentative_incomplete_static;
-    Reduced_alignment;
-    Non_linear_cond_expr;
-  ]
+  active_warnings:= List.map fst all_warnings
 
 let wnothing () =
   active_warnings :=[]
 
 (* Make all warnings an error *)
 let werror () =
-  error_warnings:=[
-    Unnamed;
-    Unknown_attribute;
-    Zero_length_array;
-    Celeven_extension;
-    Gnu_empty_struct;
-    Missing_declarations;
-    Constant_conversion;
-    Int_conversion;
-    Varargs;
-    Implicit_function_declaration;
-    Pointer_type_mismatch;
-    Compare_distinct_pointer_types;
-    Implicit_int;
-    Main_return_type;
-    Invalid_noreturn;
-    Return_type;
-    Literal_range;
-    Unknown_pragmas;
-    CompCert_conformance;
-    Inline_asm_sdump;
-    Unused_variable;
-    Wrong_ais_parameter;
-    Unused_ais_parameter;
-    Ignored_attributes;
-    Extern_after_definition;
-    Static_in_inline;
-    Flexible_array_extensions;
-    Tentative_incomplete_static;
-    Reduced_alignment;
-    Non_linear_cond_expr;
-  ]
+  error_warnings:= List.map fst all_warnings
 
 (* Generate the warning key for the message *)
 let key_of_warning w =
@@ -411,37 +365,7 @@ let error_option w =
    Exact ("-Wno-error="^key), Unit ( warning_not_as_error w)]
 
 let warning_options =
-  error_option Unnamed @
-  error_option Unknown_attribute @
-  error_option Zero_length_array @
-  error_option Celeven_extension @
-  error_option Gnu_empty_struct @
-  error_option Missing_declarations @
-  error_option Constant_conversion @
-  error_option Int_conversion @
-  error_option Varargs @
-  error_option Implicit_function_declaration @
-  error_option Pointer_type_mismatch @
-  error_option Compare_distinct_pointer_types @
-  error_option Implicit_int @
-  error_option Main_return_type @
-  error_option Invalid_noreturn @
-  error_option Return_type @
-  error_option Literal_range @
-  error_option Unknown_pragmas @
-  error_option CompCert_conformance @
-  error_option Inline_asm_sdump @
-  error_option Unused_variable @
-  error_option Unused_parameter @
-  error_option Wrong_ais_parameter @
-  error_option Unused_ais_parameter @
-  error_option Ignored_attributes @
-  error_option Extern_after_definition @
-  error_option Static_in_inline @
-  error_option Flexible_array_extensions @
-  error_option Tentative_incomplete_static @
-  error_option Reduced_alignment @
-  error_option Non_linear_cond_expr @
+  List.concat (List.map (fun (w, active) -> error_option w) all_warnings) @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;