From d2bbd834841ba3c8b2b482a02489bd4fac19f0fb Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Thu, 4 Apr 2019 11:07:14 +0200
Subject: [vm] x86_64 registers

Backport
https://github.com/ocaml/ocaml/commit/bc333918980b97a2c81031ec33e72a417f854376
from OCaml VM
---
 kernel/byterun/coq_interp.c | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 2293ae9dfd..e838519fe4 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -159,6 +159,11 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define ACCU_REG asm("38")
 #define JUMPTBL_BASE_REG asm("39")
 #endif
+#ifdef __x86_64__
+#define PC_REG asm("%r15")
+#define SP_REG asm("%r14")
+#define ACCU_REG asm("%r13")
+#endif
 #endif
 
 #define CheckInt1() do{                            \
-- 
cgit v1.2.3


From d1905fbcde5905de640657a820e531929e23dd8a Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:35:10 +0200
Subject: [vm] Arm 64 registers

Backport
https://github.com/ocaml/ocaml/commit/055d5c0379e42b4f561cb1fc5159659d8e9a7b6f
from OCaml VM
---
 kernel/byterun/coq_interp.c | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index e838519fe4..1925ef5932 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -164,6 +164,12 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("%r14")
 #define ACCU_REG asm("%r13")
 #endif
+#ifdef __aarch64__
+#define PC_REG asm("%x19")
+#define SP_REG asm("%x20")
+#define ACCU_REG asm("%x21")
+#define JUMPTBL_BASE_REG asm("%x22")
+#endif
 #endif
 
 #define CheckInt1() do{                            \
-- 
cgit v1.2.3


From 46896e9442e74cb78ad7396054cee76564f78ec3 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:37:03 +0200
Subject: [vm] ARM registers

Backport
https://github.com/ocaml/ocaml/commit/eb1922c6ab88e832e39ba3972fab619081061928
from OCaml VM
---
 kernel/byterun/coq_interp.c | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 1925ef5932..9742768c5d 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -148,8 +148,9 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("a4")
 #define ACCU_REG asm("d7")
 #endif
-#if defined(__arm__) && !defined(__thumb2__)
-#define PC_REG asm("r9")
+/* OCaml PR#4953: these specific registers not available in Thumb mode */
+#if defined(__arm__) && !defined(__thumb__)
+#define PC_REG asm("r6")
 #define SP_REG asm("r8")
 #define ACCU_REG asm("r7")
 #endif
-- 
cgit v1.2.3


From df6328178a92d7a51e2a08acbec5013d080e73aa Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:44:08 +0200
Subject: [vm] PPC64 registers

Backport
https://github.com/ocaml/ocaml/commit/c6ce97fe26e149d43ee2cf71ca821a4592ce1785
from OCaml VM
---
 kernel/byterun/coq_interp.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 9742768c5d..a8fd2fbe47 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -133,7 +133,7 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define SP_REG asm("%edi")
 #define ACCU_REG
 #endif
-#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#if defined(__ppc__) || defined(__ppc64__)
 #define PC_REG asm("26")
 #define SP_REG asm("27")
 #define ACCU_REG asm("28")
-- 
cgit v1.2.3


From e9fec7c112a7792d67949ef5abe3de8a8832beda Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Fri, 5 Apr 2019 12:49:53 +0200
Subject: [vm] Backport from OCaml

Backport
https://github.com/ocaml/ocaml/commit/71b94fa3e8d73c40e298409fa5fd6501383d38a6
and
https://github.com/ocaml/ocaml/commit/d3e86fdfcc8f40a99380303f16f9b782233e047e
from OCaml VM
---
 kernel/byterun/coq_interp.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a8fd2fbe47..da152599ce 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -104,7 +104,8 @@ if (sp - num_args < coq_stack_threshold) {                                     \
    several architectures.
 */
 
-#if defined(__GNUC__) && !defined(DEBUG)
+#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \
+    && !defined(__llvm__)
 #ifdef __mips__
 #define PC_REG asm("$16")
 #define SP_REG asm("$17")
-- 
cgit v1.2.3