aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c34
-rw-r--r--kernel/byterun/coq_memory.c4
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--kernel/nativecode.mli2
-rw-r--r--kernel/nativelambda.ml5
-rw-r--r--kernel/nativelibrary.ml17
-rw-r--r--kernel/nativelibrary.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/subtyping.ml14
-rw-r--r--kernel/vmlambda.ml4
-rw-r--r--kernel/vmvalues.ml2
-rw-r--r--kernel/vmvalues.mli1
12 files changed, 35 insertions, 54 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 704eb1ef98..27287205f4 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -230,6 +230,12 @@ if (sp - num_args < coq_stack_threshold) { \
*sp = swap_accu_sp_tmp__; \
}while(0)
+/* Turn a code pointer into a stack value usable as a return address, and conversely.
+ The least significant bit is set to 1 so that the GC does not mistake return
+ addresses for heap pointers. */
+#define StoreRA(p) ((value)(p) + 1)
+#define LoadRA(p) ((code_t)((value)(p) - 1))
+
#if OCAML_VERSION < 41000
/* For signal handling, we hijack some code from the caml runtime */
@@ -445,7 +451,7 @@ value coq_interprete
Instruct(PUSH_RETADDR) {
print_instr("PUSH_RETADDR");
sp -= 3;
- sp[0] = (value) (pc + *pc);
+ sp[0] = StoreRA(pc + *pc);
sp[1] = coq_env;
sp[2] = Val_long(coq_extra_args);
coq_extra_args = 0;
@@ -466,7 +472,7 @@ value coq_interprete
arg1 = sp[0];
sp -= 3;
sp[0] = arg1;
- sp[1] = (value)pc;
+ sp[1] = StoreRA(pc);
sp[2] = coq_env;
sp[3] = Val_long(coq_extra_args);
print_instr("call stack=");
@@ -489,7 +495,7 @@ value coq_interprete
sp -= 3;
sp[0] = arg1;
sp[1] = arg2;
- sp[2] = (value)pc;
+ sp[2] = StoreRA(pc);
sp[3] = coq_env;
sp[4] = Val_long(coq_extra_args);
pc = Code_val(accu);
@@ -511,7 +517,7 @@ value coq_interprete
sp[0] = arg1;
sp[1] = arg2;
sp[2] = arg3;
- sp[3] = (value)pc;
+ sp[3] = StoreRA(pc);
sp[4] = coq_env;
sp[5] = Val_long(coq_extra_args);
pc = Code_val(accu);
@@ -531,7 +537,7 @@ value coq_interprete
sp[1] = arg2;
sp[2] = arg3;
sp[3] = arg4;
- sp[4] = (value)pc;
+ sp[4] = StoreRA(pc);
sp[5] = coq_env;
sp[6] = Val_long(coq_extra_args);
pc = Code_val(accu);
@@ -647,7 +653,7 @@ value coq_interprete
coq_env = accu;
} else {
print_instr("extra args = 0");
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -682,7 +688,7 @@ value coq_interprete
for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
sp += num_args;
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -707,7 +713,7 @@ value coq_interprete
Field(accu, 2) = coq_env;
for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
sp += num_args;
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -745,7 +751,7 @@ value coq_interprete
Code_val(block) = accumulate;
Field(block, 1) = Val_int(2);
accu = block;
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -1031,7 +1037,7 @@ value coq_interprete
mlsize_t i, nargs;
sp -= 2;
// Push the current instruction as the return address
- sp[0] = (value)(pc - 1);
+ sp[0] = StoreRA(pc - 1);
sp[1] = coq_env;
coq_env = Field(accu, 0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
@@ -1142,7 +1148,7 @@ value coq_interprete
for (i = size; i < sz; ++i)
caml_initialize(&Field(accu, i), *sp++);
}
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -1160,7 +1166,7 @@ value coq_interprete
sp-=2;
pc++;
// Push the return address
- sp[0] = (value) (pc + *pc);
+ sp[0] = StoreRA(pc + *pc);
sp[1] = coq_env;
coq_env = Field(accu,0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
@@ -1263,7 +1269,7 @@ value coq_interprete
}
Code_val(accu) = accumulate;
Field(accu, 1) = Val_int(2);
- pc = (code_t)(sp[0]);
+ pc = LoadRA(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
sp += 3;
@@ -1916,7 +1922,7 @@ value coq_push_ra(value code) {
code_t tcode = Code_val(code);
print_instr("push_ra");
coq_sp -= 3;
- coq_sp[0] = (value) tcode;
+ coq_sp[0] = StoreRA(tcode);
coq_sp[1] = Val_unit;
coq_sp[2] = Val_long(0);
return Val_unit;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a55ff57c8d..f404cb2b1c 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -66,10 +66,6 @@ static void coq_scan_roots(scanning_action action)
/* 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_in_heap_or_young(*i)) continue;
-#endif
(*action) (*i, i);
};
/* Hook */
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d517d215ed..9ce388929c 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -2130,7 +2130,7 @@ let compile_deps env sigma prefix init t =
in
aux env 0 init t
-let compile_constant_field env _prefix con acc cb =
+let compile_constant_field env con acc cb =
let gl = compile_constant env empty_evars con cb in
gl@acc
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 90525a19b2..17312ec8ea 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val register_native_file : string -> unit
val is_loaded_native_file : string -> bool
-val compile_constant_field : env -> string -> Constant.t ->
+val compile_constant_field : env -> Constant.t ->
global list -> 'a constant_body -> global list
val compile_mind_field : ModPath.t -> Label.t ->
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f3b483467d..aa30a01134 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -381,10 +381,7 @@ let makeblock env ind tag nparams arity args =
Lmakeblock(prefix, ind, tag, args)
let makearray args def =
- try
- let p = Array.map get_value args in
- Lval (Nativevalues.parray_of_array p (get_value def))
- with Not_found -> Lparray (args, def)
+ Lparray (args, def)
(* Translation of constants *)
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 2e27fe071e..6dd7f315e0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -17,21 +17,21 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-let rec translate_mod prefix mp env mod_expr acc =
+let rec translate_mod mp env mod_expr acc =
match mod_expr with
| NoFunctor struc ->
let env' = add_structure mp struc empty_delta_resolver env in
- List.fold_left (translate_field prefix mp env') acc struc
+ List.fold_left (translate_field mp env') acc struc
| MoreFunctor _ -> acc
-and translate_field prefix mp env acc (l,x) =
+and translate_field mp env acc (l,x) =
match x with
| SFBconst cb ->
let con = Constant.make2 mp l in
(debug_native_compiler (fun () ->
let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
Pp.str msg));
- compile_constant_field env prefix con acc cb
+ compile_constant_field env con acc cb
| SFBmind mb ->
(debug_native_compiler (fun () ->
let id = mb.mind_packets.(0).mind_typename in
@@ -45,7 +45,7 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env md.mod_type acc
+ translate_mod mp env md.mod_type acc
| SFBmodtype mdtyp ->
let mp = mdtyp.mod_mp in
(debug_native_compiler (fun () ->
@@ -53,19 +53,18 @@ and translate_field prefix mp env acc (l,x) =
Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
in
Pp.str msg));
- translate_mod prefix mp env mdtyp.mod_type acc
+ translate_mod mp env mdtyp.mod_type acc
-let dump_library mp dp env mod_expr =
+let dump_library mp env mod_expr =
debug_native_compiler (fun () -> Pp.str "Compiling library...");
match mod_expr with
| NoFunctor struc ->
let env = add_structure mp struc empty_delta_resolver env in
- let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
clear_symbols ();
let mlcode =
- List.fold_left (translate_field prefix mp env) [] struc
+ List.fold_left (translate_field mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 8f58dfa8d3..1d0d56703d 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -15,5 +15,5 @@ open Nativecode
(** This file implements separate compilation for libraries in the native
compiler *)
-val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
+val dump_library : ModPath.t -> env -> module_signature ->
global list * Nativevalues.symbols
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a35f94e3ce..5f83e78eb0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir =
in
let ast, symbols =
if output_native_objects then
- Nativelibrary.dump_library mp dir senv.env str
+ Nativelibrary.dump_library mp senv.env str
else [], Nativevalues.empty_symbols
in
let lib = {
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1a4c786e43..627bf42570 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,6 +226,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
in
match info1 with
+ | IndType _ | IndConstr _ -> error DefinitionFieldExpected
| Constant cb1 ->
let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
let cb1 = Declareops.subst_const_body subst1 cb1 in
@@ -254,18 +255,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
let c1 = Mod_subst.force_constr lc1 in
let c2 = Mod_subst.force_constr lc2 in
check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
- | IndType ((_kn,_i),_mind1) ->
- CErrors.user_err Pp.(str @@
- "The kernel does not recognize yet that a parameter can be " ^
- "instantiated by an inductive type. Hint: you can rename the " ^
- "inductive type and give a definition to map the old name to the new " ^
- "name.")
- | IndConstr (((_kn,_i),_j),_mind1) ->
- CErrors.user_err Pp.(str @@
- "The kernel does not recognize yet that a parameter can be " ^
- "instantiated by a constructor. Hint: you can rename the " ^
- "constructor and give a definition to map the old name to the new " ^
- "name.")
+
let rec check_modules cst env msb1 msb2 subst1 subst2 =
let mty1 = module_type_of_module msb1 in
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index e353348ac7..ee32384ec9 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -494,10 +494,6 @@ let makeblock tag nparams arity args =
else Lmakeblock(tag, args)
let makearray args def =
- try
- let p = Array.map get_value args in
- Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def))
- with Not_found ->
let ar = Lmakeblock(0, args) in (* build the ocaml array *)
let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *)
Lmakeblock(0,[|kind|]) (* the reference *)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9944458d6b..938d1f28f7 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -459,8 +459,6 @@ let val_of_int i = (Obj.magic i : values)
let val_of_uint i = (Obj.magic i : structured_values)
-let val_of_parray p = (Obj.magic p : structured_values)
-
let atom_of_proj kn v =
let r = Obj.new_block proj_tag 2 in
Obj.set_field r 0 (Obj.repr kn);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d15595766a..534a85d773 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -148,7 +148,6 @@ val val_of_atom : atom -> values
val val_of_int : int -> structured_values
val val_of_block : tag -> structured_values array -> structured_values
val val_of_uint : Uint63.t -> structured_values
-val val_of_parray : structured_values Parray.t -> structured_values
external val_of_annot_switch : annot_switch -> values = "%identity"
external val_of_proj_name : Projection.Repr.t -> values = "%identity"
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 15:39:37 +0000