diff options
| author | Guillaume Melquiond | 2020-08-30 09:12:17 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2020-11-13 15:13:23 +0100 |
| commit | aebc10aab3581a0561f96de6b5db6d530a65e658 (patch) | |
| tree | fc77c92a0e39e4f77c4600ea4dc9e51f20a247b6 /kernel | |
| parent | fdd16113a042170022dce276e53e7a3308c0451c (diff) | |
Remove some unused opcodes from VM.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/byterun/coq_fix_code.c | 2 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 14 | ||||
| -rw-r--r-- | kernel/genOpcodeFiles.ml | 2 | ||||
| -rw-r--r-- | kernel/vmbytecodes.ml | 3 | ||||
| -rw-r--r-- | kernel/vmbytecodes.mli | 1 | ||||
| -rw-r--r-- | kernel/vmemitcodes.ml | 5 |
6 files changed, 1 insertions, 26 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index cd431dbf2e..1ffb323748 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -43,7 +43,7 @@ void init_arity () { arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]= arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]= arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= - arity[ISINT]=arity[AREINT2]=0; + 0; /* instruction with one operand */ arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]= arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]= diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 74eb4973d0..67e6bed0d9 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -1558,20 +1558,6 @@ value coq_interprete Next; } - Instruct (ISINT){ - print_instr("ISINT"); - accu = (Is_uint63(accu)) ? coq_true : coq_false; - Next; - } - - Instruct (AREINT2){ - print_instr("AREINT2"); - accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false; - sp++; - Next; - } - - Instruct (CHECKOPPFLOAT) { print_instr("CHECKOPPFLOAT"); CheckFloat1(); diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index b48084109b..c8c8f61d59 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -129,8 +129,6 @@ let opcodes = "CHECKCOMPAREINT63"; "CHECKHEAD0INT63"; "CHECKTAIL0INT63"; - "ISINT"; - "AREINT2"; "CHECKOPPFLOAT"; "CHECKABSFLOAT"; "CHECKEQFLOAT"; diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml index a1dea977cd..2cef6e3359 100644 --- a/kernel/vmbytecodes.ml +++ b/kernel/vmbytecodes.ml @@ -62,7 +62,6 @@ type instruction = | Kbranch of Label.t (* jump to label *) | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list @@ -152,8 +151,6 @@ let rec pp_instr i = str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++ pp_lbl lbl - | Kareint n -> str "areint " ++ int n - and pp_bytecodes c = match c with | [] -> str "" diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli index 33071b917b..138778eac4 100644 --- a/kernel/vmbytecodes.mli +++ b/kernel/vmbytecodes.mli @@ -61,7 +61,6 @@ type instruction = | Kbranch of Label.t (** jump to label, is it needed ? *) | Kprim of CPrimitives.t * pconstant | Kcamlprim of CPrimitives.t * Label.t - | Kareint of int and bytecodes = instruction list diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml index d0422dd324..ae2399c872 100644 --- a/kernel/vmemitcodes.ml +++ b/kernel/vmemitcodes.ml @@ -355,13 +355,8 @@ let emit_instr env = function out_label env lbl; slot_for_caml_prim env op - | Kareint 1 -> out env opISINT - | Kareint 2 -> out env opAREINT2; - | Kstop -> out env opSTOP - | Kareint _ -> assert false - (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) let rec emit env insns remaining = match insns with |