aboutsummaryrefslogtreecommitdiff
path: root/kernel/byterun
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/byterun')
-rw-r--r--kernel/byterun/coq_fix_code.c65
-rw-r--r--kernel/byterun/coq_fix_code.h1
-rw-r--r--kernel/byterun/coq_interp.c80
-rw-r--r--kernel/byterun/coq_memory.c3
-rw-r--r--kernel/byterun/coq_uint63_emul.h15
-rw-r--r--kernel/byterun/coq_uint63_native.h22
-rw-r--r--kernel/byterun/dune6
7 files changed, 122 insertions, 70 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 4bc6848ba7..20890a28dc 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -21,68 +21,12 @@
#include <caml/alloc.h>
#include <caml/memory.h>
#include "coq_instruct.h"
+#include "coq_arity.h"
#include "coq_fix_code.h"
#ifdef THREADED_CODE
char ** coq_instr_table;
char * coq_instr_base;
-int arity[STOP+1];
-
-void init_arity () {
- /* instruction with zero operand */
- arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
- arity[ACC6]=arity[ACC7]=
- arity[PUSH]=arity[PUSHACC1]=
- arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
- arity[PUSHACC6]=arity[PUSHACC7]=
- arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=
- arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=
- arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]=
- arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]=
- arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]=
- arity[GETFIELD0]=arity[GETFIELD1]=
- arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
- arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
- arity[ACCUMULATE]=arity[STOP]=
- 0;
- /* instruction with one operand */
- arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
- arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
- arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]=
- arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
- arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
- arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
- arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
- arity[BRANCH]=arity[ENSURESTACKCAPACITY]=
- arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]=
- arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]=
- arity[CHECKMULINT63]=arity[CHECKMULCINT63]=
- arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]=
- arity[CHECKDIV21INT63]=
- arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
- arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
- arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
- arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=
- arity[CHECKEQFLOAT]=arity[CHECKLTFLOAT]=arity[CHECKLEFLOAT]=
- arity[CHECKOPPFLOAT]=arity[CHECKABSFLOAT]=arity[CHECKCOMPAREFLOAT]=
- arity[CHECKCLASSIFYFLOAT]=
- arity[CHECKADDFLOAT]=arity[CHECKSUBFLOAT]=arity[CHECKMULFLOAT]=
- arity[CHECKDIVFLOAT]=arity[CHECKSQRTFLOAT]=
- arity[CHECKFLOATOFINT63]=arity[CHECKFLOATNORMFRMANTISSA]=
- arity[CHECKFRSHIFTEXP]=arity[CHECKLDSHIFTEXP]=
- arity[CHECKNEXTUPFLOAT]=arity[CHECKNEXTDOWNFLOAT]=1;
- /* instruction with two operands */
- arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[CHECKCAMLCALL1]=arity[CHECKCAMLCALL2_1]=
- arity[CHECKCAMLCALL2]=arity[CHECKCAMLCALL3_1]=
- arity[PROJ]=
- 2;
- /* instruction with four operands */
- arity[MAKESWITCHBLOCK]=4;
- /* instruction with arbitrary operands */
- arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
-}
-
#endif /* THREADED_CODE */
@@ -164,9 +108,7 @@ value coq_tcode_of_code (value code) {
opcode_t instr;
COPY32(&instr,p);
p++;
- if (instr < 0 || instr > STOP){
- instr = STOP;
- };
+ if (instr < 0 || instr > STOP) abort();
*q++ = VALINSTR(instr);
if (instr == SWITCH) {
uint32_t i, sizes, const_size, block_size;
@@ -183,8 +125,9 @@ value coq_tcode_of_code (value code) {
q++;
for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
} else {
- uint32_t i, ar;
+ int i, ar;
ar = arity[instr];
+ if (ar < 0) abort();
for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
}
}
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 5a233e6178..916d9753a4 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -18,7 +18,6 @@ void * coq_stat_alloc (asize_t sz);
#ifdef THREADED_CODE
extern char ** coq_instr_table;
extern char * coq_instr_base;
-void init_arity();
#define VALINSTR(instr) ((opcode_t)(coq_instr_table[instr] - coq_instr_base))
#else
#define VALINSTR(instr) instr
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a9ea6d9f46..704eb1ef98 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -547,7 +547,7 @@ value coq_interprete
CHECK_STACK(0);
/* We also check for signals */
#if OCAML_VERSION >= 41000
- {
+ if (caml_something_to_do) {
value res = caml_process_pending_actions_exn();
if (Is_exception_result(res)) {
/* If there is an asynchronous exception, we reset the vm */
@@ -1426,6 +1426,41 @@ value coq_interprete
Next;
}
+ Instruct(CHECKDIVSINT63) {
+ print_instr("CHEKDIVSINT63");
+ CheckInt2();
+ int b;
+ Uint63_eq0(b, *sp);
+ if (b) {
+ accu = *sp++;
+ }
+ else {
+ Uint63_eqm1(b, *sp);
+ if (b) {
+ Uint63_neg(accu);
+ sp++;
+ }
+ else {
+ Uint63_divs(accu, *sp++);
+ }
+ }
+ Next;
+ }
+
+ Instruct(CHECKMODSINT63) {
+ print_instr("CHEKMODSINT63");
+ CheckInt2();
+ int b;
+ Uint63_eq0(b, *sp);
+ if (b) {
+ accu = *sp++;
+ }
+ else {
+ Uint63_mods(accu,*sp++);
+ }
+ Next;
+ }
+
Instruct (CHECKDIV21INT63) {
print_instr("DIV21INT63");
CheckInt3();
@@ -1473,6 +1508,13 @@ value coq_interprete
Next;
}
+ Instruct(CHECKASRINT63) {
+ print_instr("CHECKASRINT63");
+ CheckInt2();
+ Uint63_asr(accu,*sp++);
+ Next;
+ }
+
Instruct (CHECKADDMULDIVINT63) {
print_instr("CHECKADDMULDIVINT63");
CheckInt3();
@@ -1508,6 +1550,24 @@ value coq_interprete
Next;
}
+ Instruct (CHECKLTSINT63) {
+ print_instr("CHECKLTSINT63");
+ CheckInt2();
+ int b;
+ Uint63_lts(b,accu,*sp++);
+ accu = b ? coq_true : coq_false;
+ Next;
+ }
+
+ Instruct (CHECKLESINT63) {
+ print_instr("CHECKLESINT63");
+ CheckInt2();
+ int b;
+ Uint63_les(b,accu,*sp++);
+ accu = b ? coq_true : coq_false;
+ Next;
+ }
+
Instruct (CHECKCOMPAREINT63) {
/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
/* assumes Inductive _ : _ := Eq | Lt | Gt */
@@ -1526,6 +1586,24 @@ value coq_interprete
Next;
}
+ Instruct (CHECKCOMPARESINT63) {
+ /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
+ /* assumes Inductive _ : _ := Eq | Lt | Gt */
+ print_instr("CHECKCOMPARESINT63");
+ CheckInt2();
+ int b;
+ Uint63_eq(b, accu, *sp);
+ if (b) {
+ accu = coq_Eq;
+ sp++;
+ }
+ else {
+ Uint63_lts(b, accu, *sp++);
+ accu = b ? coq_Lt : coq_Gt;
+ }
+ Next;
+ }
+
Instruct (CHECKHEAD0INT63) {
print_instr("CHECKHEAD0INT63");
CheckInt1();
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index fe076f8f04..a55ff57c8d 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -100,9 +100,6 @@ value init_coq_vm(value unit) /* ML */
fprintf(stderr,"already open \n");fflush(stderr);}
else {
drawinstr=0;
-#ifdef THREADED_CODE
- init_arity();
-#endif /* THREADED_CODE */
/* Allocate the table of global and the stack */
init_coq_stack();
/* Initialing the interpreter */
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index dd9b9e55be..693716ee90 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \
accu = uint63_return_value__; \
}while(0)
+DECLARE_NULLOP(zero)
DECLARE_NULLOP(one)
+DECLARE_UNOP(neg)
+#define Uint63_neg(x) CALL_UNOP(neg, x)
DECLARE_BINOP(add)
#define Uint63_add(x, y) CALL_BINOP(add, x, y)
DECLARE_BINOP(addcarry)
@@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv)
#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
DECLARE_BINOP(div)
#define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(divs)
+#define Uint63_divs(x, y) CALL_BINOP(divs, x, y)
DECLARE_BINOP(eq)
#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
DECLARE_UNOP(eq0)
#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
+DECLARE_UNOP(eqm1)
+#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x)
DECLARE_UNOP(head0)
#define Uint63_head0(x) CALL_UNOP(head0, x)
DECLARE_BINOP(land)
#define Uint63_land(x, y) CALL_BINOP(land, x, y)
DECLARE_BINOP(leq)
#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
+DECLARE_BINOP(les)
+#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y)
DECLARE_BINOP(lor)
#define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
DECLARE_BINOP(lsl)
#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
DECLARE_BINOP(lsr)
#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
+DECLARE_BINOP(asr)
+#define Uint63_asr(x, y) CALL_BINOP(asr, x, y)
DECLARE_BINOP(lt)
#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
+DECLARE_BINOP(lts)
+#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y)
DECLARE_BINOP(lxor)
#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
DECLARE_BINOP(mod)
#define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
+DECLARE_BINOP(mods)
+#define Uint63_mods(x, y) CALL_BINOP(mods, x, y)
DECLARE_BINOP(mul)
#define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
DECLARE_BINOP(sub)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 731ae8f46e..da9ae7f147 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -12,21 +12,28 @@
#define uint_of_value(val) (((uint64_t)(val)) >> 1)
#define uint63_of_value(val) ((uint64_t)(val) >> 1)
+#define int63_of_value(val) ((int64_t)(val) >> 1)
/* 2^63 * y + x as a value */
//#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64)))
-#define uint63_zero ((value) 1) /* 2*0 + 1 */
+#define uint63_zero() ((value) 1) /* 2*0 + 1 */
#define uint63_one() ((value) 3) /* 2*1 + 1 */
#define uint63_eq(x,y) ((x) == (y))
#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
+#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1)))
#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
+#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y))
+#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y))
+#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y))
+#define Uint63_les(r,x,y) ((r) = uint63_les(x,y))
+#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x))
#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
@@ -34,6 +41,8 @@
#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y)))
+#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y)))
#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
@@ -46,14 +55,21 @@
if (uint63_lsl_y__ < (uint64_t) 127) \
accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
else \
- accu = uint63_zero; \
+ accu = uint63_zero(); \
}while(0)
#define Uint63_lsr(x,y) do{ \
value uint63_lsl_y__ = (y); \
if (uint63_lsl_y__ < (uint64_t) 127) \
accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
else \
- accu = uint63_zero; \
+ accu = uint63_zero(); \
+ }while(0)
+#define Uint63_asr(x,y) do{ \
+ value uint63_asr_y__ = (y); \
+ if (uint63_asr_y__ < (uint64_t) 127) \
+ accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \
+ else \
+ accu = uint63_zero(); \
}while(0)
/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index d3e2a2fa7f..b14ad5c558 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,7 +1,7 @@
(library
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
- (public_name coq.vm)
+ (public_name coq-core.vm)
(foreign_stubs
(language c)
(names coq_fix_code coq_float64 coq_memory coq_values coq_interp)
@@ -14,3 +14,7 @@
(rule
(targets coq_jumptbl.h)
(action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe jump))))
+
+(rule
+ (targets coq_arity.h)
+ (action (with-stdout-to %{targets} (run ../genOpcodeFiles.exe arity))))
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:07:06 +0000