aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_interp.c79
-rw-r--r--kernel/byterun/coq_memory.c16
-rw-r--r--kernel/byterun/coq_values.c1
-rw-r--r--kernel/byterun/coq_values.h10
-rw-r--r--kernel/byterun/int64_emul.h270
-rw-r--r--kernel/byterun/int64_native.h48
6 files changed, 47 insertions, 377 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 399fa843f1..bf383a33ac 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -22,18 +22,10 @@
#include "coq_memory.h"
#include "coq_values.h"
-/*spiwack : imports support functions for 64-bit integers */
-#include <caml/config.h>
-#ifdef ARCH_INT64_TYPE
-#include "int64_native.h"
-#else
-#include "int64_emul.h"
-#endif
-
/* spiwack: I append here a few macros for value/number manipulation */
#define uint32_of_value(val) (((uint32_t)val >> 1))
#define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1))
-#define UI64_of_uint32(lo) ((uint64_t)(I64_literal(0,(uint32_t)(lo))))
+#define UI64_of_uint32(lo) ((uint64_t)(lo))
#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
/* /spiwack */
@@ -341,6 +333,7 @@ value coq_interprete
/* Fallthrough */
Instruct(ENVACC){
print_instr("ENVACC");
+ print_int(*pc);
accu = Field(coq_env, *pc++);
Next;
}
@@ -371,6 +364,10 @@ value coq_interprete
sp[1] = (value)pc;
sp[2] = coq_env;
sp[3] = Val_long(coq_extra_args);
+ print_instr("call stack=");
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ print_lint(sp[3]);
pc = Code_val(accu);
coq_env = accu;
coq_extra_args = 0;
@@ -458,6 +455,7 @@ value coq_interprete
sp[0] = arg1;
sp[1] = arg2;
pc = Code_val(accu);
+ print_lint(accu);
coq_env = accu;
coq_extra_args += 1;
goto check_stacks;
@@ -481,11 +479,18 @@ value coq_interprete
print_instr("RETURN");
print_int(*pc);
sp += *pc++;
+ print_instr("stack=");
+ print_lint(sp[0]);
+ print_lint(sp[1]);
+ print_lint(sp[2]);
if (coq_extra_args > 0) {
+ print_instr("extra args > 0");
+ print_lint(coq_extra_args);
coq_extra_args--;
pc = Code_val(accu);
coq_env = accu;
} else {
+ print_instr("extra args = 0");
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -585,7 +590,10 @@ value coq_interprete
Alloc_small(accu, 1 + nvars, Closure_tag);
Code_val(accu) = pc + *pc;
pc++;
- for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
sp += nvars;
Next;
}
@@ -720,6 +728,7 @@ value coq_interprete
/* Fallthrough */
Instruct(GETGLOBAL){
print_instr("GETGLOBAL");
+ print_int(*pc);
accu = Field(coq_global_data, *pc);
pc++;
Next;
@@ -732,7 +741,7 @@ value coq_interprete
tag_t tag = *pc++;
mlsize_t i;
value block;
- print_instr("MAKEBLOCK");
+ print_instr("MAKEBLOCK, tag=");
Alloc_small(block, wosize, tag);
Field(block, 0) = accu;
for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -743,7 +752,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK1");
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
Alloc_small(block, 1, tag);
Field(block, 0) = accu;
accu = block;
@@ -753,7 +763,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK2");
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
Alloc_small(block, 2, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -764,7 +775,8 @@ value coq_interprete
Instruct(MAKEBLOCK3) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK3");
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
Alloc_small(block, 3, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -776,7 +788,8 @@ value coq_interprete
Instruct(MAKEBLOCK4) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK4");
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
Alloc_small(block, 4, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -844,7 +857,6 @@ value coq_interprete
}
Instruct(SETFIELD1){
- int i, j, size, size_aux;
print_instr("SETFIELD1");
caml_modify(&Field(accu, 1),*sp);
sp++;
@@ -884,19 +896,17 @@ value coq_interprete
Instruct(PROJ){
print_instr("PROJ");
if (Is_accu (accu)) {
+ value block;
/* Skip over the index of projected field */
pc++;
- /* Save the argument on the stack */
- *--sp = accu;
/* Create atom */
- Alloc_small(accu, 2, ATOM_PROJ_TAG);
- Field(accu, 0) = Field(coq_global_data, *pc);
- Field(accu, 1) = sp[0];
- sp[0] = accu;
+ Alloc_small(block, 2, ATOM_PROJ_TAG);
+ Field(block, 0) = Field(coq_global_data, *pc);
+ Field(block, 1) = accu;
/* Create accumulator */
Alloc_small(accu, 2, Accu_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
+ Field(accu, 1) = block;
} else {
accu = Field(accu, *pc++);
}
@@ -943,6 +953,7 @@ value coq_interprete
/* Fallthrough */
Instruct(CONSTINT) {
print_instr("CONSTINT");
+ print_int(*pc);
accu = Val_int(*pc);
pc++;
Next;
@@ -1110,7 +1121,6 @@ value coq_interprete
/* returns the sum plus one with a carry */
uint32_t s;
s = (uint32_t)accu + (uint32_t)*sp++ + 1;
- value block;
if( (uint32_t)s <= (uint32_t)accu ) {
/* carry */
Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1183,8 +1193,8 @@ value coq_interprete
print_instr("MULCINT31");
uint64_t p;
/*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
- p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
- if ( I64_is_zero(p) ) {
+ p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1);
+ if (p == 0) {
accu = (value)1;
}
else {
@@ -1193,8 +1203,8 @@ value coq_interprete
of the non-constant constructor is then 1 */
Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
/*unsigned shift*/
- Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; /*higher part*/
- Field(accu, 1) = (value)(I64_to_int32(p)|1); /*lower part*/
+ Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/
+ Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/
}
Next;
}
@@ -1206,19 +1216,20 @@ value coq_interprete
int62 by the int31 */
uint64_t bigint;
bigint = UI64_of_value(accu);
- bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+ bigint = (bigint << 31) | UI64_of_value(*sp++);
uint64_t divisor;
divisor = UI64_of_value(*sp++);
Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
- if (I64_is_zero (divisor)) {
+ if (divisor == 0) {
Field(accu, 0) = 1; /* 2*0+1 */
Field(accu, 1) = 1; /* 2*0+1 */
}
else {
uint64_t quo, mod;
- I64_udivmod(bigint, divisor, &quo, &mod);
- Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
- Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+ quo = bigint / divisor;
+ mod = bigint % divisor;
+ Field(accu, 0) = value_of_uint32((uint32_t)(quo));
+ Field(accu, 1) = value_of_uint32((uint32_t)(mod));
}
Next;
}
@@ -1271,7 +1282,7 @@ value coq_interprete
Instruct (COMPAREINT31) {
/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
- /* assumes Inudctive _ : _ := Eq | Lt | Gt */
+ /* assumes Inductive _ : _ := Eq | Lt | Gt */
print_instr("COMPAREINT31");
if ((uint32_t)accu == (uint32_t)*sp) {
accu = 1; /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829ab0..c9bcdc32ff 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
value coq_global_data;
-int coq_all_transp;
value coq_atom_tbl;
int drawinstr;
@@ -104,7 +103,6 @@ static int coq_vm_initialized = 0;
value init_coq_vm(value unit) /* ML */
{
- int i;
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
@@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
init_coq_global_data(Coq_global_data_Size);
init_coq_atom_tbl(40);
/* Initialing the interpreter */
- coq_all_transp = 0;
init_coq_interpreter();
/* Some predefined pointer code */
@@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
{
asize_t size;
value * new_low, * new_high, * new_sp;
- value * p;
size = coq_stack_high - coq_stack_low;
do {
size *= 2;
@@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size) /* ML */
return Val_unit;
}
-
-value coq_set_transp_value(value transp)
-{
- coq_all_transp = (transp == Val_true);
- return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
- return Val_bool(coq_all_transp);
-}
-
value coq_set_drawinstr(value unit)
{
drawinstr = 1;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b27c..528babebfc 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
value coq_kind_of_closure(value v) {
opcode_t * c;
- int res;
int is_app = 0;
c = Code_val(v);
if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1590a2141d..bb0f0eb5e4 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,23 +17,17 @@
#define Default_tag 0
#define Accu_tag 0
-
-
#define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
#define ATOM_PROJ_TAG 3
#define ATOM_FIX_TAG 4
#define ATOM_SWITCH_TAG 5
#define ATOM_COFIX_TAG 6
#define ATOM_COFIXEVALUATED_TAG 7
-
-
/* Les blocs accumulate */
#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#endif /* _COQ_VALUES_ */
-
-
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
deleted file mode 100644
index 86bee72edb..0000000000
--- a/kernel/byterun/int64_emul.h
+++ /dev/null
@@ -1,270 +0,0 @@
-/***********************************************************************/
-/* */
-/* Objective Caml */
-/* */
-/* Xavier Leroy, projet Cristal, INRIA Rocquencourt */
-/* */
-/* Copyright 2002 Institut National de Recherche en Informatique et */
-/* en Automatique. All rights reserved. This file is distributed */
-/* under the terms of the GNU Library General Public License, with */
-/* the special exception on linking described in file ../LICENSE. */
-/* */
-/***********************************************************************/
-
-/* Software emulation of 64-bit integer arithmetic, for C compilers
- that do not support it. */
-
-#ifndef CAML_INT64_EMUL_H
-#define CAML_INT64_EMUL_H
-
-#include <math.h>
-
-#ifdef ARCH_BIG_ENDIAN
-#define I64_literal(hi,lo) { hi, lo }
-#else
-#define I64_literal(hi,lo) { lo, hi }
-#endif
-
-/* Unsigned comparison */
-static int I64_ucompare(uint64 x, uint64 y)
-{
- if (x.h > y.h) return 1;
- if (x.h < y.h) return -1;
- if (x.l > y.l) return 1;
- if (x.l < y.l) return -1;
- return 0;
-}
-
-#define I64_ult(x, y) (I64_ucompare(x, y) < 0)
-
-/* Signed comparison */
-static int I64_compare(int64 x, int64 y)
-{
- if ((int32)x.h > (int32)y.h) return 1;
- if ((int32)x.h < (int32)y.h) return -1;
- if (x.l > y.l) return 1;
- if (x.l < y.l) return -1;
- return 0;
-}
-
-/* Negation */
-static int64 I64_neg(int64 x)
-{
- int64 res;
- res.l = -x.l;
- res.h = ~x.h;
- if (res.l == 0) res.h++;
- return res;
-}
-
-/* Addition */
-static int64 I64_add(int64 x, int64 y)
-{
- int64 res;
- res.l = x.l + y.l;
- res.h = x.h + y.h;
- if (res.l < x.l) res.h++;
- return res;
-}
-
-/* Subtraction */
-static int64 I64_sub(int64 x, int64 y)
-{
- int64 res;
- res.l = x.l - y.l;
- res.h = x.h - y.h;
- if (x.l < y.l) res.h--;
- return res;
-}
-
-/* Multiplication */
-static int64 I64_mul(int64 x, int64 y)
-{
- int64 res;
- uint32 prod00 = (x.l & 0xFFFF) * (y.l & 0xFFFF);
- uint32 prod10 = (x.l >> 16) * (y.l & 0xFFFF);
- uint32 prod01 = (x.l & 0xFFFF) * (y.l >> 16);
- uint32 prod11 = (x.l >> 16) * (y.l >> 16);
- res.l = prod00;
- res.h = prod11 + (prod01 >> 16) + (prod10 >> 16);
- prod01 = prod01 << 16; res.l += prod01; if (res.l < prod01) res.h++;
- prod10 = prod10 << 16; res.l += prod10; if (res.l < prod10) res.h++;
- res.h += x.l * y.h + x.h * y.l;
- return res;
-}
-
-#define I64_is_zero(x) (((x).l | (x).h) == 0)
-
-#define I64_is_negative(x) ((int32) (x).h < 0)
-
-/* Bitwise operations */
-static int64 I64_and(int64 x, int64 y)
-{
- int64 res;
- res.l = x.l & y.l;
- res.h = x.h & y.h;
- return res;
-}
-
-static int64 I64_or(int64 x, int64 y)
-{
- int64 res;
- res.l = x.l | y.l;
- res.h = x.h | y.h;
- return res;
-}
-
-static int64 I64_xor(int64 x, int64 y)
-{
- int64 res;
- res.l = x.l ^ y.l;
- res.h = x.h ^ y.h;
- return res;
-}
-
-/* Shifts */
-static int64 I64_lsl(int64 x, int s)
-{
- int64 res;
- s = s & 63;
- if (s == 0) return x;
- if (s < 32) {
- res.l = x.l << s;
- res.h = (x.h << s) | (x.l >> (32 - s));
- } else {
- res.l = 0;
- res.h = x.l << (s - 32);
- }
- return res;
-}
-
-static int64 I64_lsr(int64 x, int s)
-{
- int64 res;
- s = s & 63;
- if (s == 0) return x;
- if (s < 32) {
- res.l = (x.l >> s) | (x.h << (32 - s));
- res.h = x.h >> s;
- } else {
- res.l = x.h >> (s - 32);
- res.h = 0;
- }
- return res;
-}
-
-static int64 I64_asr(int64 x, int s)
-{
- int64 res;
- s = s & 63;
- if (s == 0) return x;
- if (s < 32) {
- res.l = (x.l >> s) | (x.h << (32 - s));
- res.h = (int32) x.h >> s;
- } else {
- res.l = (int32) x.h >> (s - 32);
- res.h = (int32) x.h >> 31;
- }
- return res;
-}
-
-/* Division and modulus */
-
-#define I64_SHL1(x) x.h = (x.h << 1) | (x.l >> 31); x.l <<= 1
-#define I64_SHR1(x) x.l = (x.l >> 1) | (x.h << 31); x.h >>= 1
-
-static void I64_udivmod(uint64 modulus, uint64 divisor,
- uint64 * quo, uint64 * mod)
-{
- int64 quotient, mask;
- int cmp;
-
- quotient.h = 0; quotient.l = 0;
- mask.h = 0; mask.l = 1;
- while ((int32) divisor.h >= 0) {
- cmp = I64_ucompare(divisor, modulus);
- I64_SHL1(divisor);
- I64_SHL1(mask);
- if (cmp >= 0) break;
- }
- while (mask.l | mask.h) {
- if (I64_ucompare(modulus, divisor) >= 0) {
- quotient.h |= mask.h; quotient.l |= mask.l;
- modulus = I64_sub(modulus, divisor);
- }
- I64_SHR1(mask);
- I64_SHR1(divisor);
- }
- *quo = quotient;
- *mod = modulus;
-}
-
-static int64 I64_div(int64 x, int64 y)
-{
- int64 q, r;
- int32 sign;
-
- sign = x.h ^ y.h;
- if ((int32) x.h < 0) x = I64_neg(x);
- if ((int32) y.h < 0) y = I64_neg(y);
- I64_udivmod(x, y, &q, &r);
- if (sign < 0) q = I64_neg(q);
- return q;
-}
-
-static int64 I64_mod(int64 x, int64 y)
-{
- int64 q, r;
- int32 sign;
-
- sign = x.h;
- if ((int32) x.h < 0) x = I64_neg(x);
- if ((int32) y.h < 0) y = I64_neg(y);
- I64_udivmod(x, y, &q, &r);
- if (sign < 0) r = I64_neg(r);
- return r;
-}
-
-/* Coercions */
-
-static int64 I64_of_int32(int32 x)
-{
- int64 res;
- res.l = x;
- res.h = x >> 31;
- return res;
-}
-
-#define I64_to_int32(x) ((int32) (x).l)
-
-/* Note: we assume sizeof(intnat) = 4 here, which is true otherwise
- autoconfiguration would have selected native 64-bit integers */
-#define I64_of_intnat I64_of_int32
-#define I64_to_intnat I64_to_int32
-
-static double I64_to_double(int64 x)
-{
- double res;
- int32 sign = x.h;
- if (sign < 0) x = I64_neg(x);
- res = ldexp((double) x.h, 32) + x.l;
- if (sign < 0) res = -res;
- return res;
-}
-
-static int64 I64_of_double(double f)
-{
- int64 res;
- double frac, integ;
- int neg;
-
- neg = (f < 0);
- f = fabs(f);
- frac = modf(ldexp(f, -32), &integ);
- res.h = (uint32) integ;
- res.l = (uint32) ldexp(frac, 32);
- if (neg) res = I64_neg(res);
- return res;
-}
-
-#endif /* CAML_INT64_EMUL_H */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
deleted file mode 100644
index 657d0a07e0..0000000000
--- a/kernel/byterun/int64_native.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/***********************************************************************/
-/* */
-/* Objective Caml */
-/* */
-/* Xavier Leroy, projet Cristal, INRIA Rocquencourt */
-/* */
-/* Copyright 2002 Institut National de Recherche en Informatique et */
-/* en Automatique. All rights reserved. This file is distributed */
-/* under the terms of the GNU Library General Public License, with */
-/* the special exception on linking described in file ../LICENSE. */
-/* */
-/***********************************************************************/
-
-/* Wrapper macros around native 64-bit integer arithmetic,
- so that it has the same interface as the software emulation
- provided in int64_emul.h */
-
-#ifndef CAML_INT64_NATIVE_H
-#define CAML_INT64_NATIVE_H
-
-#define I64_literal(hi,lo) ((int64_t)(hi) << 32 | (lo))
-#define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
-#define I64_ult(x,y) ((uint64_t)(x) < (uint64_t)(y))
-#define I64_neg(x) (-(x))
-#define I64_add(x,y) ((x) + (y))
-#define I64_sub(x,y) ((x) - (y))
-#define I64_mul(x,y) ((x) * (y))
-#define I64_is_zero(x) ((x) == 0)
-#define I64_is_negative(x) ((x) < 0)
-#define I64_div(x,y) ((x) / (y))
-#define I64_mod(x,y) ((x) % (y))
-#define I64_udivmod(x,y,quo,rem) \
- (*(rem) = (uint64_t)(x) % (uint64_t)(y), \
- *(quo) = (uint64_t)(x) / (uint64_t)(y))
-#define I64_and(x,y) ((x) & (y))
-#define I64_or(x,y) ((x) | (y))
-#define I64_xor(x,y) ((x) ^ (y))
-#define I64_lsl(x,y) ((x) << (y))
-#define I64_asr(x,y) ((x) >> (y))
-#define I64_lsr(x,y) ((uint64_t)(x) >> (y))
-#define I64_to_intnat(x) ((intnat) (x))
-#define I64_of_intnat(x) ((intnat) (x))
-#define I64_to_int32(x) ((int32_t) (x))
-#define I64_of_int32(x) ((int64_t) (x))
-#define I64_to_double(x) ((double)(x))
-#define I64_of_double(x) ((int64_t)(x))
-
-#endif /* CAML_INT64_NATIVE_H */
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-03 19:10:41 +0000