From 5c825f263698433ed4e8db8ccd0c14394520535a Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 11 Aug 2012 13:33:26 +0000
Subject: 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
---
 kernel/byterun/coq_fix_code.c |  3 ++-
 kernel/byterun/coq_instruct.h |  1 +
 kernel/byterun/coq_interp.c   | 22 ++++++++++++++++++++++
 3 files changed, 25 insertions(+), 1 deletion(-)

(limited to 'kernel/byterun')

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   */
 
-- 
cgit v1.2.3