diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_interp.c | 34 | ||||
| -rw-r--r-- | kernel/byterun/coq_memory.c | 4 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 14 |
3 files changed, 22 insertions, 30 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/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 |