diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-02-19 09:31:03 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2021-02-23 11:33:14 +0100 |
| commit | 014883f2f4cfc4fd64fe9aa5f561a971e2ed1345 (patch) | |
| tree | 7738077335321874d76379435d596236f192d04c | |
| parent | ed89275cb820bb7ab283c51e461d852d1c8bec63 (diff) | |
| download | compcert-014883f2f4cfc4fd64fe9aa5f561a971e2ed1345.tar.gz compcert-014883f2f4cfc4fd64fe9aa5f561a971e2ed1345.zip | |
Fix regression on PowerPC / Diab
On PowerPC/Diab, common declarations must not be used for small data sections.
Add a `~common` option to `PrintAsmaux.variable_section` to control
the use of common declarations. The default is whatever is specified
on the command line using the `-fcommon` and `-fno-common` options.
Use `~common:false` for `Section_small_data` on PowerPC / Diab.
Note that on PowerPC/Linux, GCC uses common declarations for uninitialized
variables in small data section, so we keep doing this in CompCert as well.
| -rw-r--r-- | backend/PrintAsmaux.ml | 9 | ||||
| -rw-r--r-- | powerpc/TargetPrinter.ml | 6 |
2 files changed, 11 insertions, 4 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 7a692d20..e39ba8aa 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -312,12 +312,17 @@ let print_version_and_options oc comment = containing relocations. If not provided, [sec] is used. - [bss] is the name of the section to use if uninitialized and common declarations are not used. If not provided, [sec] is used. + - [common] says whether common declarations can be used for uninitialized + variables. It defaults to the status of the [-fcommon] / [-fno-common] + command-line option. Passing [~common:false] is needed when + common declarations cannot be used at all, for example in the context of + small data areas. *) -let variable_section ~sec ?bss ?reloc i = +let variable_section ~sec ?bss ?reloc ?(common = !Clflags.option_fcommon) i = match i with | Uninit -> - if !Clflags.option_fcommon + if common then "COMM" else begin match bss with Some s -> s | None -> sec end | Init -> sec diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index e32348a3..52d30e33 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -212,8 +212,10 @@ module Diab_System : SYSTEM = let name_of_section = function | Section_text -> ".text" - | Section_data i -> variable_section ~sec:".data" ~bss:".bss" i - | Section_small_data i -> variable_section ~sec:".sdata" ~bss:".sbss" i + | Section_data i -> + variable_section ~sec:".data" ~bss:".bss" i + | Section_small_data i -> + variable_section ~sec:".sdata" ~bss:".sbss" ~common:false i | Section_const _ -> ".text" | Section_small_const _ -> ".sdata2" | Section_string -> ".text" |