x86 support for -fpic

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

configure

@@ -356,6 +356,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cprepro="${toolprefix}cc"
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="bsd"
+        pic_supported=true
         ;;
     linux)
         abi="standard"
@@ -364,6 +365,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         clinker_options="-m64"
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="linux"
+        pic_supported=true
         ;;
     macos|macosx)
         abi="macos"
@@ -374,6 +376,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"

test

@@ -205,11 +205,17 @@ case "$target,$os" in
       1) Run_test "$simu_rv64" "";;
       2) Run_test "$simu_rv64" "-Os";;
     esac;;
-  x86_32,*|x86_64,*)
+  x86_32,*)
     case "$1" in
       1) Run_test "" "";;
       2) Run_test "" "-Os";;
     esac;;
+  x86_64,*)
+    case "$1" in
+      1) Run_test "" "";;
+      2) Run_test "" "-fpic";;
+      3) Run_test "" "-Os";;
+    esac;;
   *)
     Fatal "Unknown configuration \"$target\" - \"$os\""
 esac

tools/runner.sh

@@ -30,7 +30,7 @@ Definition const_for_result (a: aval) : option operation :=
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
   | Ptr(Gl id ofs) =>
-      if SelectOp.symbol_is_external id then
+      if SelectOp.symbol_is_relocatable id then
         if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None
       else
         Some (Olea_ptr (Aglobal id ofs))

x86/ConstpropOp.vp

@@ -109,7 +109,7 @@ Proof.
 - (* pointer *)
   destruct p; try discriminate; SimplVM.
   + (* global *)
-    destruct (SelectOp.symbol_is_external id).
+    destruct (SelectOp.symbol_is_relocatable id).
   * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ.
     exists (Genv.symbol_address ge id Ptrofs.zero); auto.
   * inv H2. exists (Genv.symbol_address ge id ofs); split.

x86/ConstpropOpproof.v

@@ -48,16 +48,15 @@ Local Open Scope cminorsel_scope.
 
 (** External oracle to determine whether a symbol should be addressed
   through [Oindirectsymbol] or can be addressed via [Oleal Aglobal].
-  This is to accommodate MacOS X's limitations on references to data
-  symbols imported from shared libraries.  It can also help with PIC
-  code under ELF. *)
+  Indirect access is needed for data symbols imported from shared libraries
+  in macOS and Cygwin, and for PIC code in ELF. *)
 
-Parameter symbol_is_external: ident -> bool.
+Parameter symbol_is_relocatable: ident -> bool.
 
 Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a.
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
-  if symbol_is_external id then
+  if symbol_is_relocatable id then
     if Ptrofs.eq ofs Ptrofs.zero
     then Eop (Oindirectsymbol id) Enil
     else Eop (Olea_ptr (Aindexed (Ptrofs.unsigned ofs))) (Eop (Oindirectsymbol id) Enil ::: Enil)

x86/SelectOp.vp

@@ -117,7 +117,7 @@ Theorem eval_addrsymbol:
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
   intros. unfold addrsymbol. exists (Genv.symbol_address ge id ofs); split; auto.
-  destruct (symbol_is_external id).
+  destruct (symbol_is_relocatable id).
   predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
   subst. EvalOp.
   EvalOp. econstructor. EvalOp. simpl; eauto. econstructor.

x86/SelectOpproof.v

@@ -107,6 +107,7 @@ module type SYSTEM =
       val raw_symbol: out_channel -> string -> unit
       val symbol: out_channel -> P.t -> unit
       val symbol_paren: out_channel -> P.t -> unit
+      val symbol_function: out_channel -> P.t -> unit
       val label: out_channel -> int -> unit
       val name_of_section: section_name -> string
       val stack_alignment: int
@@ -137,6 +138,10 @@ module ELF_System : SYSTEM =
       then fprintf oc "(%s)" s
       else fprintf oc "%s" s
 
+    let symbol_function oc symb =
+      symbol_paren oc symb;
+      if !Clflags.option_fpic then fprintf oc "@PLT"
+
     let label = elf_label
 
     let name_of_section = function
@@ -206,6 +211,9 @@ module MacOS_System : SYSTEM =
     let symbol_paren = symbol
         (* the leading '_' protects the leading '$' *)
 
+    let symbol_function = symbol
+        (* no need for @PLT even in PIC mode *)
+
     let label oc lbl =
       fprintf oc "L%d" lbl
 
@@ -278,6 +286,8 @@ module Cygwin_System : SYSTEM =
       then fprintf oc "(%a)" raw_symbol s
       else raw_symbol oc s
 
+    let symbol_function = symbol_paren
+
     let label oc lbl =
        fprintf oc "L%d" lbl
 
@@ -723,7 +733,7 @@ module Target(System: SYSTEM):TARGET =
       | Pjmp_l(l) ->
           fprintf oc "	jmp	%a\n" label (transl_label l)
       | Pjmp_s(f, sg) ->
-          fprintf oc "	jmp	%a\n" symbol_paren f
+          fprintf oc "	jmp	%a\n" symbol_function f
       | Pjmp_r(r, sg) ->
           fprintf oc "	jmp	*%a\n" ireg r
       | Pjcc(c, l) ->
@@ -749,7 +759,7 @@ module Target(System: SYSTEM):TARGET =
             fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r
           end
       | Pcall_s(f, sg) ->
-          fprintf oc "	call	%a\n" symbol_paren f;
+          fprintf oc "	call	%a\n" symbol_function f;
           if (not Archi.ptr64) && sg.sig_cc.cc_structret then
             fprintf oc "	pushl	%%eax\n"
       | Pcall_r(r, sg) ->

x86/TargetPrinter.ml

@@ -27,8 +27,8 @@ Extract Constant Archi.win64 =>
 
 (* SelectOp *)
 
-Extract Constant SelectOp.symbol_is_external =>
+Extract Constant SelectOp.symbol_is_relocatable =>
   "match Configuration.system with
     | ""macos"" -> C2C.atom_is_external
-    | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_external
-    | _ -> (fun _ -> false)".
+    | ""cygwin"" -> if Archi.ptr64 then C2C.atom_is_external else (fun _ -> false)
+    | _ -> C2C.atom_needs_GOT_access".