Add options -fpic and -shared

`-fpic` is not implemented yet and just ignored (with an "unsupported" warning).
`-shared` is passed to the GNU linker.

Author: xavierleroy

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

configure

@@ -234,6 +234,7 @@ cprepro_options="-E"
 archiver="${toolprefix}ar rcs"
 libmath="-lm"
 responsefile="gnu"
+pic_supported=false
 
 #
 # ARM Target Configuration
@@ -426,8 +427,7 @@ if test "$arch" = "aarch64"; then
         cprepro="${toolprefix}cc"
         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"
-        ;;
+        system="macos";;
     *)
         echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
         echo "$usage" 1>&2
@@ -697,6 +697,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 +761,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 +863,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,7 @@ 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_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 code? *)

driver/Driver.ml

@@ -200,6 +200,7 @@ 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]
   -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 +267,11 @@ 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
   [
 (* Getting help *)
   Exact "-help", Unit print_usage_and_exit;
@@ -301,7 +307,11 @@ 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 ] @
       f_opt "common" option_fcommon @
 (* Target processor options *)
   (if Configuration.arch = "arm" then

driver/Linker.ml

@@ -35,7 +35,8 @@ let linker exe_name files =
 
 
 let gnu_linker_help =
-{|  -nodefaultlibs Do not use the standard system libraries when
+{|  -shared        Produce a shared library instead of an executable
+  -nodefaultlibs Do not use the standard system libraries when
                  linking
   -nostdlib      Do not use the standard system startup files or
                  libraries when linking
@@ -71,7 +72,8 @@ 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 "-shared", Self push_linker_arg]
   else []) @
   [ Exact "-s", Self push_linker_arg;
     Exact "-static", Self push_linker_arg;