Merge pull request #551 from AbsInt/PIC

Support PIC and PIE for AArch64, RISC-V and x86-64

Author: xavierleroy

.github/workflows/build.yml

@@ -66,3 +66,5 @@ jobs:
         run: tools/runner.sh test1
       - name: Test alternate configuration
         run: tools/runner.sh test2
+      - name: Test alternate configuration 2
+        run: tools/runner.sh test3

Makefile

@@ -330,7 +330,8 @@ compcert.ini: Makefile.config
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
          echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
-	 echo "response_file_style=$(RESPONSEFILE)";) \
+	 echo "response_file_style=$(RESPONSEFILE)"; \
+	 echo "pic_supported=$(PIC_SUPPORTED)") \
         > compcert.ini
 
 compcert.config: Makefile.config

aarch64/extractionMachdep.v

@@ -30,7 +30,7 @@ Extract Constant Archi.abi =>
 Extract Constant SelectOp.symbol_is_relocatable =>
   "match Configuration.system with
     | ""macos"" -> C2C.atom_is_external
-    | _ -> (fun _ -> false)".
+    | _ -> C2C.atom_needs_GOT_access".
 
 (* Asm *)
 

cfrontend/C2C.ml

@@ -52,7 +52,10 @@ let atom_is_static a =
   with Not_found ->
     false
 
-(* Is it possible for symbol [a] to be defined in a DLL? *)
+(* Is it possible for symbol [a] to be defined in a DLL?
+   Yes, unless [a] is defined in the current compilation unit, or is static.
+   (This criterion is appropriate for macOS and for Cygwin; for ELF,
+    see [atom_needs_GOT_access] below.)  *)
 let atom_is_external a =
   match Hashtbl.find decl_atom a with
   | { a_defined = true } -> false
@@ -61,6 +64,20 @@ let atom_is_external a =
   | _ -> true
   | exception Not_found -> true
 
+(* In ELF PIC code, all non-static symbols must be accessed through
+   the GOT, even if they are defined in the current compilation unit.
+   (This is to allow symbol interposition by the dynamic loader.)
+   In ELF PIE code, there is no interposition, so locally-defined
+   symbols do not need GOT access.
+   In non-PIC, non-PIE mode, the GOT is unused. *)
+let atom_needs_GOT_access a =
+  if !Clflags.option_fpic then
+    not (atom_is_static a)
+  else if !Clflags.option_fpie then
+    atom_is_external a
+  else
+    false
+
 let atom_alignof a =
   try
     (Hashtbl.find decl_atom a).a_alignment

configure

@@ -234,6 +234,7 @@ cprepro_options="-E"
 archiver="${toolprefix}ar rcs"
 libmath="-lm"
 responsefile="gnu"
+pic_supported=false
 
 #
 # ARM Target Configuration
@@ -352,17 +353,21 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         casm_options="-m64 -c"
         clinker="${toolprefix}cc"
         clinker_options="-m64"
+        clinker_needs_no_pie=false
         cprepro="${toolprefix}cc"
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="bsd"
+        pic_supported=true
         ;;
     linux)
         abi="standard"
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
+        clinker_needs_no_pie=false
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="linux"
+        pic_supported=true
         ;;
     macos|macosx)
         abi="macos"
@@ -373,6 +378,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cprepro_options="-arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
+        pic_supported=true
         ;;
     cygwin)
         abi="standard"
@@ -403,8 +409,10 @@ if test "$arch" = "riscV"; then
   cc_options="$model_options"
   casm_options="$model_options -c"
   clinker_options="$model_options"
+  clinker_needs_no_pie=false
   cprepro_options="$model_options -U__GNUC__ -E"
   system="linux"
+  pic_supported=true
 fi
 
 #
@@ -415,7 +423,9 @@ if test "$arch" = "aarch64"; then
     linux)
         abi="standard"
         cprepro_options="-U__GNUC__ -E"
-        system="linux";;
+        system="linux"
+        pic_supported=true
+        ;;
     macos|macosx)
         abi="apple"
         casm="${toolprefix}cc"
@@ -427,6 +437,7 @@ if test "$arch" = "aarch64"; then
         cprepro_options="-arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
+        pic_supported=true
         ;;
     *)
         echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
@@ -697,6 +708,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers
 INSTALL_COQDEV=$install_coqdev
 LIBMATH=$libmath
 MODEL=$model
+PIC_SUPPORTED=$pic_supported
 SYSTEM=$system
 RESPONSEFILE=$responsefile
 LIBRARY_FLOCQ=$library_Flocq
@@ -760,6 +772,10 @@ ENDIANNESS=
 # SYSTEM=cygwin
 SYSTEM=
 
+# Are we able to produce position-independent code (with the `-fpic` option)?
+#PIC_SUPPORTED=true
+PIC_SUPPORTED=false
+
 # C compiler (for testing only)
 CC=cc
 
@@ -858,6 +874,7 @@ CompCert configuration:
     Hardware model................ $model
     Application binary interface.. $abi
     Endianness.................... $endianness
+    PIC generation supported...... $pic_supported
     OS and development env........ $system
     C compiler.................... $cc $cc_options
     C preprocessor................ $cprepro $cprepro_options

driver/Clflags.ml

@@ -22,6 +22,8 @@ let option_funprototyped = ref true
 let option_fpacked_structs = ref false
 let option_funstructured_switch = ref false
 let option_ffpu = ref true
+let option_fpic = ref false
+let option_fpie = ref Configuration.pic_supported
 let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
 let option_fconstprop = ref true

driver/Configuration.ml

@@ -142,6 +142,7 @@ let stdlib_path =
   else
     ""
 let asm_supports_cfi = get_bool_config "asm_supports_cfi"
+let pic_supported = get_bool_config "pic_supported"
 
 type response_file_style =
   | Gnu         (* responsefiles in gnu compatible syntax *)

driver/Configuration.mli

@@ -59,3 +59,6 @@ val gnu_toolchain: bool
 
 val elf_target: bool
   (** Is the target binary format ELF? *)
+
+val pic_supported: bool
+  (** Are we able to generate PIC and PIE code? *)

driver/Driver.ml

@@ -200,6 +200,8 @@ Processing options:
                  single caller [on]
   -fif-conversion Perform if-conversion (generation of conditional moves) [on]
 Code generation options: (use -fno-<opt> to turn off -f<opt>)
+  -fpic / -fPIC  Generate position-independent code [off]
+  -fpie / -fPIE  Generate position-independent executables [on if supported]
   -ffpu          Use FP registers for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
@@ -266,6 +268,16 @@ let cmdline_actions =
     if n <= 0 || ((n land (n - 1)) <> 0) then
       error no_loc "requested alignment %d is not a power of 2" n
     in
+  let set_pic_mode () =
+    if Configuration.pic_supported
+    then option_fpic := true
+    else warning no_loc Unnamed
+         "option -fpic not supported on this platform, ignored" in
+  let set_pie_mode () =
+    if Configuration.pic_supported
+    then option_fpie := true
+    else warning no_loc Unnamed
+         "option -fpie not supported on this platform, ignored" in
   [
 (* Getting help *)
   Exact "-help", Unit print_usage_and_exit;
@@ -301,7 +313,15 @@ let cmdline_actions =
   Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); 
   Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n);
   Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n);
-  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
+  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);
+  Exact "-fpic", Unit set_pic_mode;
+  Exact "-fPIC", Unit set_pic_mode;
+  Exact "-fno-pic", Unset option_fpic;
+  Exact "-fno-PIC", Unset option_fpic;
+  Exact "-fpie", Unit set_pie_mode;
+  Exact "-fPIE", Unit set_pie_mode;
+  Exact "-fno-pie", Unset option_fpie;
+  Exact "-fno-PIE", Unset option_fpie ] @
       f_opt "common" option_fcommon @
 (* Target processor options *)
   (if Configuration.arch = "arm" then

driver/Linker.ml

@@ -39,6 +39,9 @@ let gnu_linker_help =
                  linking
   -nostdlib      Do not use the standard system startup files or
                  libraries when linking
+  -no-pie        Do not produce a position-independent executable
+  -pie           Produce a position-independent executable
+  -shared        Produce a shared library instead of an executable
 |}
 
 let linker_help =
@@ -71,7 +74,10 @@ let linker_actions =
   ] @
   (if Configuration.gnu_toolchain then
     [ Exact "-nodefaultlibs", Self push_linker_arg;
-      Exact "-nostdlib", Self push_linker_arg;]
+      Exact "-nostdlib", Self push_linker_arg;
+      Exact "-pie", Self push_linker_arg;
+      Exact "-no-pie", Self push_linker_arg;
+      Exact "-shared", Self push_linker_arg]
   else []) @
   [ Exact "-s", Self push_linker_arg;
     Exact "-static", Self push_linker_arg;