From 54d47c05616ff89f9d06937aee30bcd3665d041a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 May 2025 10:00:21 +0200
Subject: [PATCH 1/6] Add options `-fpic` and `-shared`

`-fpic` is not implemented yet and just ignored (with an "unsupported" warning).
`-shared` is passed to the GNU linker.
---
 Makefile                 |  3 ++-
 configure                | 10 ++++++++--
 driver/Clflags.ml        |  1 +
 driver/Configuration.ml  |  1 +
 driver/Configuration.mli |  3 +++
 driver/Driver.ml         | 12 +++++++++++-
 driver/Linker.ml         |  6 ++++--
 test                     |  2 +-
 8 files changed, 31 insertions(+), 7 deletions(-)

diff --git a/Makefile b/Makefile
index 690d02851c..6af062c513 100644
--- a/Makefile
+++ b/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
diff --git a/configure b/configure
index bd2c9b2cf5..d8654784d4 100755
--- a/configure
+++ b/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
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 995be34d73..cc941d08fb 100644
--- a/driver/Clflags.ml
+++ b/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
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 4b0c116ef2..986cff93f1 100644
--- a/driver/Configuration.ml
+++ b/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 *)
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index a71da72d66..926920c763 100644
--- a/driver/Configuration.mli
+++ b/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? *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 4266e57e04..daf2881f12 100644
--- a/driver/Driver.ml
+++ b/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
diff --git a/driver/Linker.ml b/driver/Linker.ml
index d6e1d38430..16cf3bf718 100644
--- a/driver/Linker.ml
+++ b/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;
diff --git a/test b/test
index 72ca254ccd..02b559f624 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 72ca254ccd357849215b596610807bfc3ec2d807
+Subproject commit 02b559f624ff271053998b892ec6de8cf4e7a36e

From 50df9b1c76e2c54f5c9a0a0f2ba0eefd7cfbafc8 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 May 2025 10:56:31 +0200
Subject: [PATCH 2/6] Add `C2C.atom_needs_GOT_access`

This is used on ELF platforms to determine which symbols are relocatable.
---
 cfrontend/C2C.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 4f7363b01c..cdd4995493 100644
--- a/cfrontend/C2C.ml
+++ b/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,18 @@ let atom_is_external a =
   | _ -> true
   | exception Not_found -> true
 
+(* In ELF PIC code, the rules are different: 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.)  *)
+let atom_needs_GOT_access a =
+  !Clflags.option_fpic &&
+  begin match Hashtbl.find decl_atom a with
+  | { a_storage = C.Storage_static } -> false
+  | _ -> true
+  | exception Not_found -> true
+  end
+
 let atom_alignof a =
   try
     (Hashtbl.find decl_atom a).a_alignment

From 41553afef90b189a28333401aed9f70e8dd1a58a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 May 2025 10:57:42 +0200
Subject: [PATCH 3/6] x86 support for `-fpic`

---
 .github/workflows/build.yml |  2 ++
 configure                   |  3 +++
 test                        |  2 +-
 tools/runner.sh             |  8 +++++++-
 x86/ConstpropOp.vp          |  2 +-
 x86/ConstpropOpproof.v      |  2 +-
 x86/SelectOp.vp             |  9 ++++-----
 x86/SelectOpproof.v         |  2 +-
 x86/TargetPrinter.ml        | 14 ++++++++++++--
 x86/extractionMachdep.v     |  6 +++---
 10 files changed, 35 insertions(+), 15 deletions(-)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index eb06a7c5c4..4ef34fe69a 100644
--- a/.github/workflows/build.yml
+++ b/.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
diff --git a/configure b/configure
index d8654784d4..a8a8e8bc89 100755
--- a/configure
+++ b/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"
diff --git a/test b/test
index 02b559f624..29085c328b 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 02b559f624ff271053998b892ec6de8cf4e7a36e
+Subproject commit 29085c328bd6c36ead1cf4319f6486a23f799656
diff --git a/tools/runner.sh b/tools/runner.sh
index 995fc57061..4b5529b6b3 100755
--- a/tools/runner.sh
+++ b/tools/runner.sh
@@ -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
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index ada7ca6be5..15c16cf04a 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -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))
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 5624953646..0858d78a3c 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -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.
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index eb9b203a2a..ca4f149376 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -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)
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 1b68b39f0b..b730666514 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -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.
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3db1af98d0..ab85b69b43 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -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) ->
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index d1a29c729c..72dc0c1050 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -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".

From e99d3df6403ad04d447a8006f76269275ae0ca19 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 May 2025 11:04:37 +0200
Subject: [PATCH 4/6] aarch64 support for `-fpic`

---
 aarch64/extractionMachdep.v | 2 +-
 configure                   | 8 ++++++--
 tools/runner.sh             | 6 ++++--
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index 78eb363fba..143e77e3a1 100644
--- a/aarch64/extractionMachdep.v
+++ b/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 *)
 
diff --git a/configure b/configure
index a8a8e8bc89..721cce3520 100755
--- a/configure
+++ b/configure
@@ -419,7 +419,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"
@@ -430,7 +432,9 @@ 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"
+        pic_supported=true
+        ;;
     *)
         echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
         echo "$usage" 1>&2
diff --git a/tools/runner.sh b/tools/runner.sh
index 4b5529b6b3..40fec763e9 100755
--- a/tools/runner.sh
+++ b/tools/runner.sh
@@ -181,12 +181,14 @@ case "$target,$os" in
   aarch64,linux)
     case "$1" in
       1) Run_test "$simu_aarch64" "";;
-      2) Run_test "$simu_aarch64" "-Os";;
+      2) Run_test "$simu_aarch64" "-fpic";;
+      3) Run_test "$simu_aarch64" "-Os";;
     esac;;
   aarch64,macos)
     case "$1" in
       1) Run_test "" "";;
-      2) Run_test "" "-Os";;
+      2) Run_test "" "-fpic";;
+      3) Run_test "" "-Os";;
     esac;;
   arm,linux)
     case "$1" in

From 36b59742607f70aab739bebd83daf21928eba5e7 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 26 May 2025 11:29:38 +0200
Subject: [PATCH 5/6] RISC-V support for `-fpic`

---
 configure                 |  1 +
 riscV/Archi.v             |  4 ----
 riscV/Asmgen.v            |  3 ++-
 riscV/Asmgenproof.v       |  2 +-
 riscV/Asmgenproof1.v      |  2 +-
 riscV/ConstpropOp.vp      |  3 ++-
 riscV/ConstpropOpproof.v  |  2 +-
 riscV/SelectOp.vp         | 10 +++++++++-
 riscV/SelectOpproof.v     |  2 +-
 riscV/TargetPrinter.ml    | 16 ++++++++++++----
 riscV/extractionMachdep.v |  8 ++++++--
 tools/runner.sh           |  3 ++-
 12 files changed, 38 insertions(+), 18 deletions(-)

diff --git a/configure b/configure
index 721cce3520..e244f30cc4 100755
--- a/configure
+++ b/configure
@@ -409,6 +409,7 @@ if test "$arch" = "riscV"; then
   clinker_options="$model_options"
   cprepro_options="$model_options -U__GNUC__ -E"
   system="linux"
+  pic_supported=true
 fi
 
 #
diff --git a/riscV/Archi.v b/riscV/Archi.v
index ce93572870..52802f9c94 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -71,7 +71,3 @@ Global Opaque ptr64 big_endian splitlong
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN
               float_conversion_default_nan.
-
-(** Whether to generate position-independent code or not *)
-
-Parameter pic_code: unit -> bool.
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4e867b678c..be00925d91 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -21,6 +21,7 @@ Require Archi.
 Require Import Coqlib Errors.
 Require Import AST Integers Floats Memdata.
 Require Import Op Locations Mach Asm.
+Require SelectOp.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
@@ -419,7 +420,7 @@ Definition transl_op
           else Ploadsi rd f :: k)
   | Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
-      OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
+      OK (if SelectOp.symbol_is_relocatable s && negb (Ptrofs.eq ofs Ptrofs.zero)
           then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k
           else Ploadsymbol rd s ofs :: k)
   | Oaddrstack n, nil =>
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index c6784ee144..ed841616b1 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -278,7 +278,7 @@ Opaque Int.eq.
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
 - destruct (Float.eq_dec n Float.zero); TailNoLabel.
 - destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+- destruct (SelectOp.symbol_is_relocatable id && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
 + TailNoLabel. 
 - apply opimm32_label; intros; exact I.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 0f9f2adc29..6e3b260e3d 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -989,7 +989,7 @@ Opaque Int.eq.
   apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl. 
 - (* addrsymbol *)
-  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+  destruct (SelectOp.symbol_is_relocatable id && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
   exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
   intros (rs2 & A & B & C).
diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp
index 75f8a2bb8a..ce49245d1d 100644
--- a/riscV/ConstpropOp.vp
+++ b/riscV/ConstpropOp.vp
@@ -18,6 +18,7 @@ Require Import Coqlib Compopts.
 Require Import AST Integers Floats.
 Require Import Op Registers.
 Require Import ValueDomain.
+Require SelectOp.
 
 (** * Converting known values to constants *)
 
@@ -298,7 +299,7 @@ Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
   | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil =>
-      if Archi.pic_code tt
+      if SelectOp.symbol_is_relocatable symb
       then (addr, args)
       else (Aglobal symb (Ptrofs.add n1 n), nil)
   | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index 85a19a0a7e..d5355f3896 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -734,7 +734,7 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- destruct (Archi.pic_code tt).
+- destruct (SelectOp.symbol_is_relocatable symb).
 + exists (Val.offset_ptr e#r1 n); auto.
 + simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
   inv H0; simpl; auto.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 00476b0d1b..dfa5fce090 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -450,10 +450,18 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
  
 (** ** Recognition of addressing modes for load and store operations *)
 
+(** Some symbols are relocatable (e.g. global symbols in PIC mode)
+    and cannot be used with [Aglobal] addressing mode. *)
+
+Parameter symbol_is_relocatable: ident -> bool.
+
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
-  | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)
+  | Eop (Oaddrsymbol id ofs) Enil =>
+      if symbol_is_relocatable id
+      then (Aindexed Ptrofs.zero, e:::Enil)
+      else (Aglobal id ofs, Enil)
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index f5998f28c5..391f4ebcb4 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -893,7 +893,7 @@ Theorem eval_addressing:
 Proof.
   intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
   - exists (@nil val);  split. eauto with evalexpr. simpl. auto.
-  - destruct (Archi.pic_code tt).
+  - destruct (symbol_is_relocatable id).
   + exists (Vptr b ofs0 :: nil); split.
     constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence.
   + exists (@nil val); split. constructor. simpl; auto.
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 1144ae26e8..b6eb313ef9 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -111,7 +111,7 @@ module Target : TARGET =
 (* Generate code to load the address of id + ofs in register r *)
 
     let loadsymbol oc r id ofs =
-      if Archi.pic_code () then begin
+      if SelectOp.symbol_is_relocatable id then begin
         assert (ofs = Integers.Ptrofs.zero);
         fprintf oc "	la	%a, %s\n" ireg r (extern_atom id)
       end else begin
@@ -144,6 +144,13 @@ module Target : TARGET =
         assert (!latest_auipc = Some(id, ofs));
         fprintf oc "%%pcrel_lo(1b)"
 
+(* Emit the target of a call, with a `@plt` suffix in PIC mode. *)
+
+    let symbol_plt oc s =
+      if !Clflags.option_fpic
+      then fprintf oc "%a@plt" symbol s
+      else symbol oc s
+
 (* Printing of instructions *)
     let print_instruction oc = function
       | Pmv(rd, rs) ->
@@ -277,11 +284,11 @@ module Target : TARGET =
       | Pj_l(l) ->
          fprintf oc "	j	%a\n" print_label l
       | Pj_s(s, sg) ->
-         fprintf oc "	jump	%a, x31\n" symbol s
+         fprintf oc "	tail	%a\n" symbol_plt s
       | Pj_r(r, sg) ->
          fprintf oc "	jr	%a\n" ireg r
       | Pjal_s(s, sg) ->
-         fprintf oc "	call	%a\n" symbol s
+         fprintf oc "	call	%a\n" symbol_plt s
       | Pjal_r(r, sg) ->
          fprintf oc "	jalr	%a\n" ireg r
 
@@ -596,7 +603,8 @@ module Target : TARGET =
     let address = if Archi.ptr64 then ".quad" else ".long"
 
     let print_prologue oc =
-      fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic");
+      fprintf oc "	.option %s\n"
+        (if !Clflags.option_fpic then "pic" else "nopic");
       if !Clflags.option_g then begin
         section oc Section_text;
       end
diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v
index 890735bad4..84de6a0388 100644
--- a/riscV/extractionMachdep.v
+++ b/riscV/extractionMachdep.v
@@ -16,13 +16,17 @@
 
 (* Additional extraction directives specific to the RISC-V port *)
 
-Require Archi Asm.
+Require Archi Asm SelectOp.
 
 (* Archi *)
 
 Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ".
-Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
+
+(* SelectOp *)
+
+Extract Constant SelectOp.symbol_is_relocatable => "C2C.atom_needs_GOT_access".
 
 (* Asm *)
+
 Extract Constant Asm.low_half => "fun _ _ _ -> assert false".
 Extract Constant Asm.high_half => "fun _ _ _ -> assert false".
diff --git a/tools/runner.sh b/tools/runner.sh
index 40fec763e9..929b5ef25b 100755
--- a/tools/runner.sh
+++ b/tools/runner.sh
@@ -205,7 +205,8 @@ case "$target,$os" in
   riscv,linux)
     case "$1" in
       1) Run_test "$simu_rv64" "";;
-      2) Run_test "$simu_rv64" "-Os";;
+      2) Run_test "$simu_rv64" "-fpic";;
+      3) Run_test "$simu_rv64" "-Os";;
     esac;;
   x86_32,*)
     case "$1" in

From f1335cf832efc081aa97c5992174114bf25c365b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Wed, 28 May 2025 14:31:05 +0200
Subject: [PATCH 6/6] Generate Position-Independent Executables (PIE) if
 possible

The same ELF target platforms that support PIC also use PIE by default.
PIE code generation is a small variation on PIC code generation.
Controllable via `-fpie` / `-fno-pie` (for code generation)
and `-pie` / `-no-pie` (for linking).
---
 cfrontend/C2C.ml         | 22 ++++++++++++----------
 configure                |  3 +++
 driver/Clflags.ml        |  1 +
 driver/Configuration.mli |  2 +-
 driver/Driver.ml         | 12 +++++++++++-
 driver/Linker.ml         |  8 ++++++--
 riscV/TargetPrinter.ml   |  6 ++++--
 tools/runner.sh          |  6 +++---
 x86/TargetPrinter.ml     |  2 +-
 9 files changed, 42 insertions(+), 20 deletions(-)

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index cdd4995493..0b20db5548 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -64,17 +64,19 @@ let atom_is_external a =
   | _ -> true
   | exception Not_found -> true
 
-(* In ELF PIC code, the rules are different: 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 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 =
-  !Clflags.option_fpic &&
-  begin match Hashtbl.find decl_atom a with
-  | { a_storage = C.Storage_static } -> false
-  | _ -> true
-  | exception Not_found -> true
-  end
+  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
diff --git a/configure b/configure
index e244f30cc4..631b1af174 100755
--- a/configure
+++ b/configure
@@ -353,6 +353,7 @@ 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"
@@ -363,6 +364,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         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
@@ -407,6 +409,7 @@ 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
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index cc941d08fb..391e1ca1ac 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -23,6 +23,7 @@ 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
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index 926920c763..39f183524d 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -61,4 +61,4 @@ val elf_target: bool
   (** Is the target binary format ELF? *)
 
 val pic_supported: bool
-  (** Are we able to generate PIC code? *)
+  (** Are we able to generate PIC and PIE code? *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index daf2881f12..0052d32886 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -201,6 +201,7 @@ Processing options:
   -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
@@ -272,6 +273,11 @@ let cmdline_actions =
     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;
@@ -311,7 +317,11 @@ let cmdline_actions =
   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 "-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
diff --git a/driver/Linker.ml b/driver/Linker.ml
index 16cf3bf718..06b88b73b6 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -35,11 +35,13 @@ let linker exe_name files =
 
 
 let gnu_linker_help =
-{|  -shared        Produce a shared library instead of an executable
-  -nodefaultlibs Do not use the standard system libraries when
+{|  -nodefaultlibs Do not use the standard system libraries when
                  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 =
@@ -73,6 +75,8 @@ let linker_actions =
   (if Configuration.gnu_toolchain then
     [ Exact "-nodefaultlibs", 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;
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index b6eb313ef9..fb948b325c 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -147,7 +147,7 @@ module Target : TARGET =
 (* Emit the target of a call, with a `@plt` suffix in PIC mode. *)
 
     let symbol_plt oc s =
-      if !Clflags.option_fpic
+      if SelectOp.symbol_is_relocatable s
       then fprintf oc "%a@plt" symbol s
       else symbol oc s
 
@@ -604,7 +604,9 @@ module Target : TARGET =
 
     let print_prologue oc =
       fprintf oc "	.option %s\n"
-        (if !Clflags.option_fpic then "pic" else "nopic");
+        (if !Clflags.option_fpic || !Clflags.option_fpie
+         then "pic"
+         else "nopic");
       if !Clflags.option_g then begin
         section oc Section_text;
       end
diff --git a/tools/runner.sh b/tools/runner.sh
index 929b5ef25b..f914c07d82 100755
--- a/tools/runner.sh
+++ b/tools/runner.sh
@@ -182,7 +182,7 @@ case "$target,$os" in
     case "$1" in
       1) Run_test "$simu_aarch64" "";;
       2) Run_test "$simu_aarch64" "-fpic";;
-      3) Run_test "$simu_aarch64" "-Os";;
+      3) Run_test "$simu_aarch64" "-Os -fno-pie -no-pie";;
     esac;;
   aarch64,macos)
     case "$1" in
@@ -206,7 +206,7 @@ case "$target,$os" in
     case "$1" in
       1) Run_test "$simu_rv64" "";;
       2) Run_test "$simu_rv64" "-fpic";;
-      3) Run_test "$simu_rv64" "-Os";;
+      3) Run_test "$simu_rv64" "-Os -fno-pie -no-pie";;
     esac;;
   x86_32,*)
     case "$1" in
@@ -217,7 +217,7 @@ case "$target,$os" in
     case "$1" in
       1) Run_test "" "";;
       2) Run_test "" "-fpic";;
-      3) Run_test "" "-Os";;
+      3) Run_test "" "-Os -fno-pie -no-pie";;
     esac;;
   *)
     Fatal "Unknown configuration \"$target\" - \"$os\""
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index ab85b69b43..610be0f5a1 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -140,7 +140,7 @@ module ELF_System : SYSTEM =
 
     let symbol_function oc symb =
       symbol_paren oc symb;
-      if !Clflags.option_fpic then fprintf oc "@PLT"
+      if SelectOp.symbol_is_relocatable symb then fprintf oc "@PLT"
 
     let label = elf_label