diff options
| author | Maxime Dénès | 2016-10-25 08:09:24 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-25 08:09:24 +0200 |
| commit | b63a5cfa919fc0ebe664bbfb3add0fce387b1491 (patch) | |
| tree | 69662aacaaa7129a6b50805f2653fd96d9e9e04d /kernel/vm.ml | |
| parent | 014e02e0a7d469d46bf5d8314efe039bea3c0dbe (diff) | |
| parent | 7ba4dee1dd9bf600256827b3517db338d7390566 (diff) | |
Merge remote-tracking branch 'github/pr/329' into v8.5
Was PR#329: Fix #5127 Memory corruption with the VM
Diffstat (limited to 'kernel/vm.ml')
| -rw-r--r-- | kernel/vm.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/kernel/vm.ml b/kernel/vm.ml index 7029876438..781a05884d 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -170,7 +170,7 @@ type whd = external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" +external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) @@ -206,7 +206,9 @@ let apply_varray vf varray = else begin push_ra stop; - push_vstack varray; + (* The fun code of [vf] will make sure we have enough stack, so we put 0 + here. *) + push_vstack varray 0; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -560,7 +562,9 @@ let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci let type_of_switch sw = - push_vstack sw.sw_stk; + (* The fun code of types will make sure we have enough stack, so we put 0 + here. *) + push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = @@ -580,9 +584,10 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then - (push_ra stop;push_vstack sw.sw_stk) + (push_ra stop;push_vstack sw.sw_stk sw.sw_annot.max_stack_size) else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + (push_vstack sw.sw_stk sw.sw_annot.max_stack_size; + push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 let branch_of_switch k sw = |