fast bitwise operations (lor,land,lxor) on int31 and BigN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 47 insertions, 4 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 5d3026605..9a59a773f 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -46,7 +46,8 @@ void init_arity () {
     arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
     arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
     arity[HEAD0INT31]=arity[TAIL0INT31]=
-    arity[COMPINT31]=arity[DECOMPINT31]=0;
+    arity[COMPINT31]=arity[DECOMPINT31]=
+    arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=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_instruct.h b/kernel/byterun/coq_instruct.h
index e224a1080..d1136b2dc 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -49,6 +49,7 @@ enum instructions {
   HEAD0INT31, TAIL0INT31,
   ISCONST, ARECONST,
   COMPINT31, DECOMPINT31,
+  ORINT31, ANDINT31, XORINT31,
 /* /spiwack  */
   STOP
 };
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index aab08d890..216919ae3 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1373,7 +1373,29 @@ value coq_interprete
         Next;
       }
 
+      Instruct (ORINT31) {
+	/* returns the bitwise or */
+	print_instr("ORINT31");
+        accu =
+	  value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++)));
+	Next;
+      }
 
+      Instruct (ANDINT31) {
+	/* returns the bitwise and */
+	print_instr("ANDINT31");
+        accu =
+	  value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++)));
+	Next;
+      }
+
+      Instruct (XORINT31) {
+	/* returns the bitwise xor */
+	print_instr("XORINT31");
+        accu =
+	  value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++)));
+	Next;
+      }
 
       /*  /spiwack   */
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index c0119aa26..994242a8a 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -114,6 +114,9 @@ type instruction =
   | Kareconst of int*Label.t            (* conditional jump *)
   | Kcompint31                          (* dynamic compilation of int31 *)
   | Kdecompint31                        (* dynamic decompilation of int31 *)
+  | Klorint31                            (* bitwise operations: or and xor *)
+  | Klandint31
+  | Klxorint31
 (* /spiwack *)
 
 and bytecodes = instruction list
@@ -220,6 +223,9 @@ let rec instruction ppf = function
   | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
   | Kcompint31 -> fprintf ppf "\tcompint31"
   | Kdecompint31 -> fprintf ppf "\tdecompint"
+  | Klorint31 -> fprintf ppf "\tlorint31"
+  | Klandint31 -> fprintf ppf "\tlandint31"
+  | Klxorint31 -> fprintf ppf "\tlxorint31"
 
 (* /spiwack *)
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index dc2220c14..0a631987e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -107,9 +107,10 @@ type instruction =
   | Kisconst of Label.t                 (** conditional jump *)
   | Kareconst of int*Label.t            (** conditional jump *)
   | Kcompint31                          (** dynamic compilation of int31 *)
-  | Kdecompint31                        (** dynamix decompilation of int31 
-   /spiwack *)
-
+  | Kdecompint31                        (** dynamix decompilation of int31 *)
+  | Klorint31                           (** bitwise operations: or and xor *)
+  | Klandint31
+  | Klxorint31
 
 and bytecodes = instruction list
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 00f1f7fbd..680a5f9f2 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -258,6 +258,9 @@ let emit_instr = function
   | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
   | Kcompint31 -> out opCOMPINT31
   | Kdecompint31 -> out opDECOMPINT31
+  | Klorint31 -> out opORINT31
+  | Klandint31 -> out opANDINT31
+  | Klxorint31 -> out opXORINT31
   (*/spiwack *)
   | Kstop ->
       out opSTOP
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 50c7b11ae..2c723a834 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -521,6 +521,9 @@ fun env field value ->
     | KInt31 (_, Int31Compare) -> add_int31_binop_from_const Cbytecodes.Kcompareint31
     | KInt31 (_, Int31Head0) -> add_int31_unop_from_const Cbytecodes.Khead0int31
     | KInt31 (_, Int31Tail0) -> add_int31_unop_from_const Cbytecodes.Ktail0int31
+    | KInt31 (_, Int31Lor) -> add_int31_binop_from_const Cbytecodes.Klorint31
+    | KInt31 (_, Int31Land) -> add_int31_binop_from_const Cbytecodes.Klandint31
+    | KInt31 (_, Int31Lxor) -> add_int31_binop_from_const Cbytecodes.Klxorint31
     | _ -> env.retroknowledge
   in
   Retroknowledge.add_field retroknowledge_with_reactive_info field value
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 6f52edcd0..58bae94d6 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -65,6 +65,9 @@ type int31_field =
   | Int31Compare
   | Int31Head0
   | Int31Tail0
+  | Int31Lor
+  | Int31Land
+  | Int31Lxor
 
 type field =
  (* | KEq
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 88bdf706a..6b76e616a 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -52,6 +52,9 @@ type int31_field =
   | Int31Compare
   | Int31Head0
   | Int31Tail0
+  | Int31Lor
+  | Int31Land
+  | Int31Lxor
 
 type field =