diff options
| -rw-r--r-- | kernel/byterun/coq_interp.c | 14 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 2 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 15 |
3 files changed, 31 insertions, 0 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 0f7713a6bb..3c3f45f7e6 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1753,6 +1753,20 @@ value coq_interprete Next; } + Instruct (CHECKNEXTUPFLOATINPLACE) { + print_instr("CHECKNEXTUPFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, nextafter(Double_val(accu), INFINITY)); + Next; + } + + Instruct (CHECKNEXTDOWNFLOATINPLACE) { + print_instr("CHECKNEXTDOWNFLOATINPLACE"); + CheckFloat1(); + Store_double_val(accu, nextafter(Double_val(accu), -INFINITY)); + Next; + } + Instruct(CHECKCAMLCALL2_1) { // arity-2 callback, the last argument can be an accumulator value arg; diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 63abb50cc2..dc2cd349ce 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -147,6 +147,8 @@ let opcodes = "CHECKLDSHIFTEXP"; "CHECKNEXTUPFLOAT"; "CHECKNEXTDOWNFLOAT"; + "CHECKNEXTUPFLOATINPLACE"; + "CHECKNEXTDOWNFLOATINPLACE"; "CHECKCAMLCALL2_1"; "CHECKCAMLCALL1"; "CHECKCAMLCALL2"; diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index 592bdf775f..c1d8fcb855 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -257,6 +257,15 @@ let check_prim_op = function | Arraydefault | Arraycopy | Arraylength -> opCHECKCAMLCALL1 +let inplace_prim_op = function + | Float64next_up | Float64next_down -> true + | _ -> false + +let check_prim_op_inplace = function + | Float64next_up -> opCHECKNEXTUPFLOATINPLACE + | Float64next_down -> opCHECKNEXTDOWNFLOATINPLACE + | _ -> assert false + let emit_instr env = function | Klabel lbl -> define_label env lbl | Kacc n -> @@ -392,6 +401,12 @@ let rec emit env insns remaining = match insns with out env opRETURN; out_int env n; emit env c remaining | Ksequence c1 :: c -> emit env c1 (c :: remaining) + | Kprim (op1, (q1, _)) :: Kprim (op2, (q2, _)) :: c when inplace_prim_op op2 -> + out env (check_prim_op op1); + slot_for_getglobal env q1; + out env (check_prim_op_inplace op2); + slot_for_getglobal env q2; + emit env c remaining (* Default case *) | instr :: c -> emit_instr env instr; emit env c remaining |