diff options
Diffstat (limited to 'kernel/byterun')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 62 | ||||
| -rw-r--r-- | kernel/byterun/coq_uint63_emul.h | 8 |
2 files changed, 52 insertions, 18 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 8990743de2..6255250218 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -716,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); @@ -732,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]; @@ -1130,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]); @@ -1240,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]); diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index d92bbe87eb..13568957c2 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -20,7 +20,7 @@ # define DECLARE_NULLOP(name) \ value uint63_##name() { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam0(); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(*cb); \ @@ -28,7 +28,7 @@ value uint63_##name() { \ # define DECLARE_UNOP(name) \ value uint63_##name##_ml(value x) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam1(x); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback(*cb, x)); \ @@ -53,7 +53,7 @@ value uint63_##name##_ml(value x) { \ # define DECLARE_BINOP(name) \ value uint63_##name##_ml(value x, value y) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam2(x, y); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback2(*cb, x, y)); \ @@ -79,7 +79,7 @@ value uint63_##name##_ml(value x, value y) { \ # define DECLARE_TEROP(name) \ value uint63_##name##_ml(value x, value y, value z) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam3(x, y, z); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback3(*cb, x, y, z)); \ |