aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c11
-rw-r--r--kernel/byterun/coq_float64.c (renamed from kernel/byterun/coq_float64.h)52
-rw-r--r--kernel/byterun/coq_interp.c201
-rw-r--r--kernel/byterun/coq_memory.c3
-rw-r--r--kernel/byterun/coq_values.h3
-rw-r--r--kernel/byterun/dune2
6 files changed, 154 insertions, 118 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 9118410549..1ba6a8c8fe 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -43,9 +43,7 @@ void init_arity () {
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
- arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
- arity[LTFLOAT]=arity[LEFLOAT]=
- arity[ISINT]=arity[AREINT2]=0;
+ 0;
/* instruction with one operand */
arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -75,9 +73,10 @@ void init_arity () {
arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[ISARRAY_CAML_CALL1]=arity[ISINT_CAML_CALL2]=
- arity[ISARRAY_INT_CAML_CALL2]=arity[ISARRAY_INT_CAML_CALL3]=
- arity[PROJ]=2;
+ arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]=
+ arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]=
+ arity[PROJ]=
+ 2;
/* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.c
index 84a3edf1c7..bea47dd47e 100644
--- a/kernel/byterun/coq_float64.h
+++ b/kernel/byterun/coq_float64.c
@@ -8,19 +8,40 @@
/* * (see LICENSE file for the text of the license) */
/************************************************************************/
-#ifndef _COQ_FLOAT64_
-#define _COQ_FLOAT64_
-
#include <math.h>
+#include <stdint.h>
-#define DECLARE_FREL(name, e) \
- int coq_##name(double x, double y) { \
- return e; \
- } \
- \
- value coq_##name##_byte(value x, value y) { \
- return coq_##name(Double_val(x), Double_val(y)); \
- }
+#define CAML_INTERNALS
+#include <caml/alloc.h>
+
+#include "coq_values.h"
+
+union double_bits {
+ double d;
+ uint64_t u;
+};
+
+static double next_up(double x) {
+ union double_bits bits;
+ if (!(x < INFINITY)) return x; // x is +oo or NaN
+ bits.d = x;
+ int64_t i = bits.u;
+ if (i >= 0) ++bits.u; // x >= +0.0, go away from zero
+ else if (bits.u + bits.u == 0) bits.u = 1; // x is -0.0, should almost never happen
+ else --bits.u; // x < 0.0, go toward zero
+ return bits.d;
+}
+
+static double next_down(double x) {
+ union double_bits bits;
+ if (!(x > -INFINITY)) return x; // x is -oo or NaN
+ bits.d = x;
+ int64_t i = bits.u;
+ if (i == 0) bits.u = INT64_MIN + 1; // x is +0.0
+ else if (i < 0) ++bits.u; // x <= -0.0, go away from zero
+ else --bits.u; // x > 0.0, go toward zero
+ return bits.d;
+}
#define DECLARE_FBINOP(name, e) \
double coq_##name(double x, double y) { \
@@ -40,19 +61,14 @@
return caml_copy_double(coq_##name(Double_val(x))); \
}
-DECLARE_FREL(feq, x == y)
-DECLARE_FREL(flt, x < y)
-DECLARE_FREL(fle, x <= y)
DECLARE_FBINOP(fmul, x * y)
DECLARE_FBINOP(fadd, x + y)
DECLARE_FBINOP(fsub, x - y)
DECLARE_FBINOP(fdiv, x / y)
DECLARE_FUNOP(fsqrt, sqrt(x))
-DECLARE_FUNOP(next_up, nextafter(x, INFINITY))
-DECLARE_FUNOP(next_down, nextafter(x, -INFINITY))
+DECLARE_FUNOP(next_up, next_up(x))
+DECLARE_FUNOP(next_down, next_down(x))
value coq_is_double(value x) {
return Val_long(Is_double(x));
}
-
-#endif /* _COQ_FLOAT64_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 1b6da7dd6f..6255250218 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -28,7 +28,6 @@
#include "coq_fix_code.h"
#include "coq_memory.h"
#include "coq_values.h"
-#include "coq_float64.h"
#if OCAML_VERSION < 41000
extern void caml_minor_collection(void);
@@ -113,7 +112,7 @@ if (sp - num_args < coq_stack_threshold) { \
#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
#define Setup_for_caml_call { *--sp = coq_env; coq_sp = sp; }
-#define Restore_after_caml_call { sp = coq_sp; coq_env = *sp++; }
+#define Restore_after_caml_call coq_env = *sp++;
/* Register optimization.
Some compilers underestimate the use of the local variables representing
@@ -193,7 +192,9 @@ if (sp - num_args < coq_stack_threshold) { \
#endif
#endif
-#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate)
+/* We should also check "Code_val(v) == accumulate" to be sure,
+ but Is_accu is only used in places where closures cannot occur. */
+#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag)
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
@@ -237,6 +238,9 @@ extern intnat volatile caml_pending_signals[];
extern void caml_process_pending_signals(void);
#endif
+extern double coq_next_up(double);
+extern double coq_next_down(double);
+
/* The interpreter itself */
value coq_interprete
@@ -712,8 +716,8 @@ value coq_interprete
coq_extra_args = Long_val(sp[2]);
sp += 3;
} else {
- /* The recursif argument is an accumulator */
- mlsize_t num_args, i;
+ /* The recursive argument is an accumulator */
+ mlsize_t num_args, sz, i;
value block;
/* Construction of fixpoint applied to its [rec_pos-1] first arguments */
Alloc_small(accu, rec_pos + 3, Closure_tag);
@@ -728,11 +732,22 @@ value coq_interprete
accu = block;
/* Construction of the accumulator */
num_args = coq_extra_args - rec_pos;
- Alloc_small(block, 3 + num_args, Closure_tag);
+ sz = 3 + num_args;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(block, sz, Closure_tag);
+ Field(block, 2) = accu;
+ for (i = 3; i < sz; ++i)
+ Field(block, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ block = caml_alloc_shr(sz, Closure_tag);
+ caml_initialize(&Field(block, 2), accu);
+ for (i = 3; i < sz; ++i)
+ caml_initialize(&Field(block, i), *sp++);
+ }
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
- Field(block, 2) = accu;
- for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++;
accu = block;
pc = (code_t)(sp[0]);
coq_env = sp[1];
@@ -1126,13 +1141,25 @@ value coq_interprete
/* Special operations for reduction of open term */
Instruct(ACCUMULATE) {
- mlsize_t i, size;
+ mlsize_t i, size, sz;
print_instr("ACCUMULATE");
size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Closure_tag);
- for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
- for(i = size; i <= coq_extra_args + size; i++)
- Field(accu, i) = *sp++;
+ sz = size + coq_extra_args + 1;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(accu, sz, Closure_tag);
+ for (i = 0; i < size; ++i)
+ Field(accu, i) = Field(coq_env, i);
+ for (i = size; i < sz; ++i)
+ Field(accu, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ accu = caml_alloc_shr(sz, Closure_tag);
+ for (i = 0; i < size; ++i)
+ caml_initialize(&Field(accu, i), Field(coq_env, i));
+ for (i = size; i < sz; ++i)
+ caml_initialize(&Field(accu, i), *sp++);
+ }
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -1236,13 +1263,24 @@ value coq_interprete
Instruct(MAKEACCU) {
- int i;
+ mlsize_t i, sz;
print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 4, Closure_tag);
+ sz = coq_extra_args + 4;
+ if (sz <= Max_young_wosize) {
+ Alloc_small(accu, sz, Closure_tag);
+ Field(accu, 2) = Field(coq_atom_tbl, *pc);
+ for (i = 3; i < sz; ++i)
+ Field(accu, i) = *sp++;
+ } else {
+ // too large for Alloc_small, so use caml_alloc_shr instead
+ // it never triggers a GC, so no need for Setup_for_gc
+ accu = caml_alloc_shr(sz, Closure_tag);
+ caml_initialize(&Field(accu, 2), Field(coq_atom_tbl, *pc));
+ for (i = 3; i < sz; ++i)
+ caml_initialize(&Field(accu, i), *sp++);
+ }
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
- Field(accu, 2) = Field(coq_atom_tbl, *pc);
- for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -1271,11 +1309,8 @@ value coq_interprete
Instruct(CHECKADDINT63){
print_instr("CHECKADDINT63");
CheckInt2();
- }
- Instruct(ADDINT63) {
/* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
- print_instr("ADDINT63");
Uint63_add(accu, *sp++);
Next;
}
@@ -1309,9 +1344,6 @@ value coq_interprete
Instruct (CHECKSUBINT63) {
print_instr("CHECKSUBINT63");
CheckInt2();
- }
- Instruct (SUBINT63) {
- print_instr("SUBINT63");
/* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
@@ -1517,9 +1549,6 @@ value coq_interprete
Instruct (CHECKLTINT63) {
print_instr("CHECKLTINT63");
CheckInt2();
- }
- Instruct (LTINT63) {
- print_instr("LTINT63");
int b;
Uint63_lt(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1529,9 +1558,6 @@ value coq_interprete
Instruct (CHECKLEINT63) {
print_instr("CHECKLEINT63");
CheckInt2();
- }
- Instruct (LEINT63) {
- print_instr("LEINT63");
int b;
Uint63_leq(b,accu,*sp++);
accu = b ? coq_true : coq_false;
@@ -1570,20 +1596,6 @@ value coq_interprete
Next;
}
- Instruct (ISINT){
- print_instr("ISINT");
- accu = (Is_uint63(accu)) ? coq_true : coq_false;
- Next;
- }
-
- Instruct (AREINT2){
- print_instr("AREINT2");
- accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
- sp++;
- Next;
- }
-
-
Instruct (CHECKOPPFLOAT) {
print_instr("CHECKOPPFLOAT");
CheckFloat1();
@@ -1601,27 +1613,21 @@ value coq_interprete
Instruct (CHECKEQFLOAT) {
print_instr("CHECKEQFLOAT");
CheckFloat2();
- accu = coq_feq(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) == Double_val(*sp++) ? coq_true : coq_false;
Next;
}
Instruct (CHECKLTFLOAT) {
print_instr("CHECKLTFLOAT");
CheckFloat2();
- }
- Instruct (LTFLOAT) {
- print_instr("LTFLOAT");
- accu = coq_flt(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) < Double_val(*sp++) ? coq_true : coq_false;
Next;
}
Instruct (CHECKLEFLOAT) {
print_instr("CHECKLEFLOAT");
CheckFloat2();
- }
- Instruct (LEFLOAT) {
- print_instr("LEFLOAT");
- accu = coq_fle(Double_val(accu), Double_val(*sp++)) ? coq_true : coq_false;
+ accu = Double_val(accu) <= Double_val(*sp++) ? coq_true : coq_false;
Next;
}
@@ -1674,35 +1680,35 @@ value coq_interprete
Instruct (CHECKADDFLOAT) {
print_instr("CHECKADDFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fadd(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) + Double_val(*sp++));
Next;
}
Instruct (CHECKSUBFLOAT) {
print_instr("CHECKSUBFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fsub(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) - Double_val(*sp++));
Next;
}
Instruct (CHECKMULFLOAT) {
print_instr("CHECKMULFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fmul(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) * Double_val(*sp++));
Next;
}
Instruct (CHECKDIVFLOAT) {
print_instr("CHECKDIVFLOAT");
CheckFloat2();
- Coq_copy_double(coq_fdiv(Double_val(accu), Double_val(*sp++)));
+ Coq_copy_double(Double_val(accu) / Double_val(*sp++));
Next;
}
Instruct (CHECKSQRTFLOAT) {
print_instr("CHECKSQRTFLOAT");
CheckFloat1();
- Coq_copy_double(coq_fsqrt(Double_val(accu)));
+ Coq_copy_double(sqrt(Double_val(accu)));
Next;
}
@@ -1784,11 +1790,25 @@ value coq_interprete
Next;
}
+ Instruct (CHECKNEXTUPFLOATINPLACE) {
+ print_instr("CHECKNEXTUPFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_up(Double_val(accu)));
+ Next;
+ }
- Instruct(ISINT_CAML_CALL2) {
+ Instruct (CHECKNEXTDOWNFLOATINPLACE) {
+ print_instr("CHECKNEXTDOWNFLOATINPLACE");
+ CheckFloat1();
+ Store_double_val(accu, coq_next_down(Double_val(accu)));
+ Next;
+ }
+
+ Instruct(CHECKCAMLCALL2_1) {
+ // arity-2 callback, the last argument can be an accumulator
value arg;
- print_instr("ISINT_CAML_CALL2");
- if (Is_uint63(accu)) {
+ print_instr("CHECKCAMLCALL2_1");
+ if (!Is_accu(accu)) {
pc++;
print_int(*pc);
arg = sp[0];
@@ -1801,47 +1821,50 @@ value coq_interprete
Next;
}
- Instruct(ISARRAY_CAML_CALL1) {
- print_instr("ISARRAY_CAML_CALL1");
- if (Is_coq_array(accu)) {
- pc++;
- Setup_for_caml_call;
- print_int(*pc);
- accu = caml_callback(Field(coq_global_data, *pc),accu);
- Restore_after_caml_call;
- pc++;
- }
- else pc += *pc;
- Next;
+ Instruct(CHECKCAMLCALL1) {
+ // arity-1 callback, no argument can be an accumulator
+ print_instr("CHECKCAMLCALL1");
+ if (!Is_accu(accu)) {
+ pc++;
+ Setup_for_caml_call;
+ print_int(*pc);
+ accu = caml_callback(Field(coq_global_data, *pc), accu);
+ Restore_after_caml_call;
+ pc++;
+ }
+ else pc += *pc;
+ Next;
}
- Instruct(ISARRAY_INT_CAML_CALL2) {
+ Instruct(CHECKCAMLCALL2) {
+ // arity-2 callback, no argument can be an accumulator
value arg;
- print_instr("ISARRAY_INT_CAML_CALL2");
- if (Is_coq_array(accu) && Is_uint63(sp[0])) {
- pc++;
- arg = sp[0];
- Setup_for_caml_call;
- print_int(*pc);
- accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
- Restore_after_caml_call;
- sp += 1;
- pc++;
- } else pc += *pc;
- Next;
+ print_instr("CHECKCAMLCALL2");
+ if (!Is_accu(accu) && !Is_accu(sp[0])) {
+ pc++;
+ arg = sp[0];
+ Setup_for_caml_call;
+ print_int(*pc);
+ accu = caml_callback2(Field(coq_global_data, *pc), accu, arg);
+ Restore_after_caml_call;
+ sp += 1;
+ pc++;
+ } else pc += *pc;
+ Next;
}
- Instruct(ISARRAY_INT_CAML_CALL3) {
+ Instruct(CHECKCAMLCALL3_1) {
+ // arity-3 callback, the last argument can be an accumulator
value arg1;
value arg2;
- print_instr("ISARRAY_INT_CAML_CALL3");
- if (Is_coq_array(accu) && Is_uint63(sp[0])) {
+ print_instr("CHECKCAMLCALL3_1");
+ if (!Is_accu(accu) && !Is_accu(sp[0])) {
pc++;
arg1 = sp[0];
arg2 = sp[1];
Setup_for_caml_call;
print_int(*pc);
- accu = caml_callback3(Field(coq_global_data, *pc),accu, arg1, arg2);
+ accu = caml_callback3(Field(coq_global_data, *pc), accu, arg1, arg2);
Restore_after_caml_call;
sp += 2;
pc++;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index ae5251c252..fe076f8f04 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -65,9 +65,10 @@ static void coq_scan_roots(scanning_action action)
register value * i;
/* Scan the stack */
for (i = coq_sp; i < coq_stack_high; i++) {
+ if (!Is_block(*i)) continue;
#ifdef NO_NAKED_POINTERS
/* The VM stack may contain C-allocated bytecode */
- if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue;
+ if (!Is_in_heap_or_young(*i)) continue;
#endif
(*action) (*i, i);
};
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index f07018711b..0cdef34050 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -30,9 +30,6 @@
#define Is_double(v) (Tag_val(v) == Double_tag)
#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
-/* coq array */
-#define Is_coq_array(v) (Is_block(v) && (Wosize_val(v) == 1))
-
/* coq values for primitive operations */
#define coq_tag_C1 2
#define coq_tag_C0 1
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 2998178be2..d3e2a2fa7f 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -4,7 +4,7 @@
(public_name coq.vm)
(foreign_stubs
(language c)
- (names coq_fix_code coq_memory coq_values coq_interp)
+ (names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
(flags (:include %{project_root}/config/dune.c_flags))))
(rule
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 09:20:11 +0000