[vm] Protect accu and coq_env

Protect accu and coq_env against GC calls in the VM when calling
primitive integer functions on 32 bits architecture.

4 files changed, 236 insertions, 134 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d2c88bffcc..2293ae9dfd 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -193,6 +193,12 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
 #define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
 
+#define Swap_accu_sp do{                        \
+    value swap_accu_sp_tmp__ = accu;            \
+    accu = *sp;                                 \
+    *sp = swap_accu_sp_tmp__;                   \
+  }while(0)
+
 /* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat caml_signals_are_pending;
@@ -1213,7 +1219,7 @@ value coq_interprete
         /* Adds the integer in the accumulator with 
            the one ontop of the stack (which is poped)*/
         print_instr("ADDINT63");
-        accu = uint63_add(accu, *sp++);
+        Uint63_add(accu, *sp++);
         Next;
       }
 
@@ -1221,10 +1227,12 @@ value coq_interprete
         print_instr("CHECKADDCINT63");
         CheckInt2();
 	/* returns the sum with a carry */
-        value s;
-        s = uint63_add(accu, *sp++);
-        AllocCarry(uint63_lt(s,accu));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_add(accu, *sp);
+        Uint63_lt(c, accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1232,10 +1240,12 @@ value coq_interprete
         print_instr("ADDCARRYCINT63");
         CheckInt2();
 	/* returns the sum plus one with a carry */
-        value s;
-        s = uint63_addcarry(accu, *sp++);
-        AllocCarry(uint63_leq(s, accu));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_addcarry(accu, *sp);
+        Uint63_leq(c, accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1246,7 +1256,7 @@ value coq_interprete
       Instruct (SUBINT63) {
         print_instr("SUBINT63");
 	/* returns the subtraction */
-        accu = uint63_sub(accu, *sp++);
+        Uint63_sub(accu, *sp++);
         Next;
       }
 
@@ -1254,12 +1264,12 @@ value coq_interprete
         print_instr("SUBCINT63");
         CheckInt2();
 	/* returns the subtraction with a carry */
-        value b;
-        value s;
-        b = *sp++;
-        s = uint63_sub(accu,b);
-        AllocCarry(uint63_lt(accu,b));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_lt(c, accu, *sp);
+        Uint63_sub(accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1267,12 +1277,12 @@ value coq_interprete
         print_instr("SUBCARRYCINT63");
         CheckInt2();
 	/* returns the subtraction minus one with a carry */
-        value b;
-        value s;
-        b = *sp++;
-        s = uint63_subcarry(accu,b);
-        AllocCarry(uint63_leq(accu,b));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_leq(c,accu,*sp);
+        Uint63_subcarry(accu,*sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1280,7 +1290,7 @@ value coq_interprete
         print_instr("MULINT63");
         CheckInt2();
 	/* returns the multiplication */
-        accu = uint63_mul(accu,*sp++);
+        Uint63_mul(accu,*sp++);
 	Next;
       }
 
@@ -1294,9 +1304,11 @@ value coq_interprete
         AllocPair(); */
         /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
         /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
-        value x = accu;
+        Uint63_mulc(accu, *sp, sp);
+        *--sp = accu;
         AllocPair();
-        Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+        Field(accu, 1) = *sp++;
+        Field(accu, 0) = *sp++;
         Next;
       }
 
@@ -1306,13 +1318,13 @@ value coq_interprete
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          accu = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
 	}
 	else {
-          accu = uint63_div(accu, divisor);
+          Uint63_div(accu, *sp++);
         }
 	Next;
       }
@@ -1320,13 +1332,13 @@ value coq_interprete
       Instruct(CHECKMODINT63) {
         print_instr("CHEKMODINT63");
         CheckInt2();
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          accu = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
 	}
         else {
-          accu = uint63_mod(accu,divisor);
+          Uint63_mod(accu,*sp++);
 	}
 	Next;
       }
@@ -1337,19 +1349,24 @@ value coq_interprete
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-          Field(accu, 0) = divisor;
-          Field(accu, 1) = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          AllocPair();
+          Field(accu, 0) = *sp;
+          Field(accu, 1) = *sp++;
         }
         else {
-          value modulus;
-          modulus = accu;
-          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-          Field(accu, 0) = uint63_div(modulus,divisor);
-          Field(accu, 1) = uint63_mod(modulus,divisor);
+          *--sp = accu;
+          Uint63_div(sp[0],sp[1]);
+          Swap_accu_sp;
+          Uint63_mod(accu,sp[1]);
+          sp[1] = sp[0];
+          Swap_accu_sp;
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[0];
+          sp += 2;
         }
 	Next;
       }
@@ -1376,59 +1393,57 @@ value coq_interprete
           Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
           Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
         } */
-        value bigint; /* TODO: fix */
-        bigint = *sp++; /* TODO: take accu into account */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          Alloc_small(accu, 2, 1);
-          Field(accu, 0) = divisor;
-          Field(accu, 1) = divisor;
+        int b;
+        Uint63_eq0(b, sp[1]);
+        if (b) {
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[1];
 	}
         else {
-          value quo, mod;
-          mod = uint63_div21(accu, bigint, divisor, &quo);
-          Alloc_small(accu, 2, 1);
-          Field(accu, 0) = quo;
-          Field(accu, 1) = mod;
+          Uint63_div21(accu, sp[0], sp[1], sp);
+          sp[1] = sp[0];
+          Swap_accu_sp;
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[0];
 	}
+        sp += 2;
         Next;
       }
 
       Instruct(CHECKLXORINT63) {
         print_instr("CHECKLXORINT63");
         CheckInt2();
-        accu = uint63_lxor(accu,*sp++);
+        Uint63_lxor(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLORINT63) {
         print_instr("CHECKLORINT63");
         CheckInt2();
-        accu = uint63_lor(accu,*sp++);
+        Uint63_lor(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLANDINT63) {
         print_instr("CHECKLANDINT63");
         CheckInt2();
-        accu = uint63_land(accu,*sp++);
+        Uint63_land(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLSLINT63) {
         print_instr("CHECKLSLINT63");
         CheckInt2();
-        value p = *sp++;
-        accu = uint63_lsl(accu,p);
+        Uint63_lsl(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLSRINT63) {
         print_instr("CHECKLSRINT63");
         CheckInt2();
-        value p = *sp++;
-        accu = uint63_lsr(accu,p);
+        Uint63_lsr(accu,*sp++);
         Next;
       }
 
@@ -1436,7 +1451,7 @@ value coq_interprete
         print_instr("CHECKLSLINT63CONST1");
         if (Is_uint63(accu)) {
           pc++;
-          accu = uint63_lsl1(accu);
+          Uint63_lsl1(accu);
           Next;
         } else {
           *--sp = uint63_one();
@@ -1450,7 +1465,7 @@ value coq_interprete
         print_instr("CHECKLSRINT63CONST1");
         if (Is_uint63(accu)) {
           pc++;
-          accu = uint63_lsr1(accu);
+          Uint63_lsr1(accu);
           Next;
         } else {
           *--sp = uint63_one();
@@ -1463,18 +1478,17 @@ value coq_interprete
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
-        value x;
-        value y;
-        x = *sp++;
-        y = *sp++;
-        accu = uint63_addmuldiv(accu,x,y);
+        Uint63_addmuldiv(accu,sp[0],sp[1]);
+        sp += 2;
         Next;
       }
 
       Instruct (CHECKEQINT63) {
         print_instr("CHECKEQINT63");
         CheckInt2();
-        accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+        int b;
+        Uint63_eq(b, accu, *sp++);
+        accu = b ? coq_true : coq_false;
         Next;
       }
 
@@ -1484,7 +1498,9 @@ value coq_interprete
      }
      Instruct (LTINT63) {
        print_instr("LTINT63");
-       accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+       int b;
+       Uint63_lt(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
        Next;
      }
 
@@ -1494,7 +1510,9 @@ value coq_interprete
      }
      Instruct (LEINT63) {
        print_instr("LEINT63");
-       accu = uint63_leq(accu,*sp++) ? coq_true : coq_false;
+       int b;
+       Uint63_leq(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
        Next;
      }
 
@@ -1503,25 +1521,30 @@ value coq_interprete
         /* assumes Inductive _ : _ := Eq | Lt | Gt */
         print_instr("CHECKCOMPAREINT63");
         CheckInt2();
-        if (uint63_eq(accu,*sp)) {
+        int b;
+        Uint63_eq(b, accu, *sp);
+        if (b) {
           accu = coq_Eq;
           sp++;
         }
-        else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
+        else {
+          Uint63_lt(b, accu, *sp++);
+          accu = b ? coq_Lt : coq_Gt;
+        }
         Next;
       }
 
       Instruct (CHECKHEAD0INT63) {
         print_instr("CHECKHEAD0INT63");
         CheckInt1();
-        accu = uint63_head0(accu);
+        Uint63_head0(accu);
         Next;
       }
 
       Instruct (CHECKTAIL0INT63) {
         print_instr("CHECKTAIL0INT63");
         CheckInt1();
-        accu = uint63_tail0(accu);
+        Uint63_tail0(accu);
         Next;
       }
 
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 9375b15de2..1ea461c5e5 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -19,7 +19,7 @@
 
 
 #define Coq_stack_size (4096 * sizeof(value))
-#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value))  /* see kernel/cbytegen.ml */
 #define Coq_max_stack_size (256 * 1024)
 
 #define TRANSP 0
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 5499f124a2..d982f67566 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -15,83 +15,142 @@ value uint63_##name() { \
   }
 
 # define DECLARE_UNOP(name) \
-value uint63_##name(value x) { \
+value uint63_##name##_ml(value x) { \
   static value* cb = 0; \
   CAMLparam1(x); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback(*cb, x)); \
   }
 
-# define DECLARE_PREDICATE(name) \
-value uint63_##name(value x) { \
-  static value* cb = 0; \
-  CAMLparam1(x); \
-  if (!cb) cb = caml_named_value("uint63 " #name); \
-  CAMLreturn(Int_val(caml_callback(*cb, x))); \
-  }
+# define CALL_UNOP_NOASSIGN(name, x) \
+  value uint63_return_value__; \
+  value uint63_arg_x__ = (x); \
+  Setup_for_gc; \
+  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \
+  Restore_after_gc
+
+# define CALL_UNOP(name, x) do{ \
+    CALL_UNOP_NOASSIGN(name, x); \
+    accu = uint63_return_value__; \
+  }while(0)
+
+# define CALL_PREDICATE(r, name, x) do{ \
+    CALL_UNOP_NOASSIGN(name, x); \
+    (r) = Int_val(uint63_return_value__); \
+  }while(0)
 
 # define DECLARE_BINOP(name) \
-value uint63_##name(value x, value y) { \
+value uint63_##name##_ml(value x, value y) { \
   static value* cb = 0; \
   CAMLparam2(x, y); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback2(*cb, x, y)); \
   }
 
-# define DECLARE_RELATION(name) \
-value uint63_##name(value x, value y) { \
-  static value* cb = 0; \
-  CAMLparam2(x, y); \
-  if (!cb) cb = caml_named_value("uint63 " #name); \
-  CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
-  }
+# define CALL_BINOP_NOASSIGN(name, x, y) \
+  value uint63_return_value__; \
+  value uint63_arg_x__ = (x); \
+  value uint63_arg_y__ = (y); \
+  Setup_for_gc; \
+  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \
+  Restore_after_gc
+
+# define CALL_BINOP(name, x, y) do{ \
+    CALL_BINOP_NOASSIGN(name, x, y);  \
+    accu = uint63_return_value__; \
+  }while(0)
+
+# define CALL_RELATION(r, name, x, y) do{ \
+    CALL_BINOP_NOASSIGN(name, x, y); \
+    (r) = Int_val(uint63_return_value__); \
+  }while(0)
 
 # define DECLARE_TEROP(name) \
-value uint63_##name(value x, value y, value z) { \
+value uint63_##name##_ml(value x, value y, value z) { \
   static value* cb = 0; \
   CAMLparam3(x, y, z); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback3(*cb, x, y, z)); \
   }
 
+# define CALL_TEROP(name, x, y, z) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    value uint63_arg_z__ = (z); \
+    Setup_for_gc; \
+    uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+    Restore_after_gc; \
+    accu = uint63_return_value__; \
+  }while(0)
 
 DECLARE_NULLOP(one)
 DECLARE_BINOP(add)
+#define Uint63_add(x, y) CALL_BINOP(add, x, y)
 DECLARE_BINOP(addcarry)
+#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y)
 DECLARE_TEROP(addmuldiv)
+#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
 DECLARE_BINOP(div)
-DECLARE_TEROP(div21_ml)
-DECLARE_RELATION(eq)
-DECLARE_PREDICATE(eq0)
+#define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(eq)
+#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
+DECLARE_UNOP(eq0)
+#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
 DECLARE_UNOP(head0)
+#define Uint63_head0(x) CALL_UNOP(head0, x)
 DECLARE_BINOP(land)
-DECLARE_RELATION(leq)
+#define Uint63_land(x, y) CALL_BINOP(land, x, y)
+DECLARE_BINOP(leq)
+#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
 DECLARE_BINOP(lor)
+#define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
+#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
 DECLARE_UNOP(lsl1)
+#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
 DECLARE_BINOP(lsr)
+#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
 DECLARE_UNOP(lsr1)
-DECLARE_RELATION(lt)
+#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
+DECLARE_BINOP(lt)
+#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
 DECLARE_BINOP(lxor)
+#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
 DECLARE_BINOP(mod)
+#define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
 DECLARE_BINOP(mul)
-DECLARE_BINOP(mulc_ml)
+#define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
 DECLARE_BINOP(sub)
+#define Uint63_sub(x, y) CALL_BINOP(sub, x, y)
 DECLARE_BINOP(subcarry)
+#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y)
 DECLARE_UNOP(tail0)
+#define Uint63_tail0(x) CALL_UNOP(tail0, x)
+
+DECLARE_TEROP(div21_ml)
+# define Uint63_div21(x, y, z, q) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    value uint63_arg_z__ = (z); \
+    Setup_for_gc; \
+    uint63_return_value__ = \
+      uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+    Restore_after_gc; \
+    *q = Field(uint63_return_value__, 0); \
+    accu = Field(uint63_return_value__, 1); \
+  }while(0)
 
-value uint63_div21(value x, value y, value z, value* q) {
-  CAMLparam3(x, y, z);
-  CAMLlocal1(qr);
-  qr = uint63_div21_ml(x, y, z);
-  *q = Field(qr, 0);
-  CAMLreturn(Field(qr, 1));
-}
-
-value uint63_mulc(value x, value y, value* h) {
-  CAMLparam2(x, y);
-  CAMLlocal1(hl);
-  hl = uint63_mulc_ml(x, y);
-  *h = Field(hl, 0);
-  CAMLreturn(Field(hl, 1));
-}
+DECLARE_BINOP(mulc_ml)
+# define Uint63_mulc(x, y, h) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    Setup_for_gc; \
+    uint63_return_value__ = \
+      uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \
+    Restore_after_gc; \
+    *(h) = Field(uint63_return_value__, 0); \
+    accu = Field(uint63_return_value__, 1); \
+  }while(0)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 92f4dc79bc..d431dc1e5c 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -9,28 +9,43 @@
 #define uint63_one() ((value) 3) /* 2*1 + 1 */
 
 #define uint63_eq(x,y) ((x) == (y))
-#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
+#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
 #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
 #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
 
-#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
-#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
-#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
-#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
-#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
-#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
-#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define Uint63_subcarry(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
 
-#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
-#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
-#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
+#define Uint63_land(x,y) (accu = (value)((uint64_t)(x) & (uint64_t)(y)))
 
 /* TODO: is + or | better? OCAML uses + */
 /* TODO: is - or ^ better? */
-#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
-#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+#define Uint63_lsl(x,y) do{ \
+  value uint63_lsl_y__ = (y); \
+  if (uint63_lsl_y__ < (uint64_t) 127) \
+    accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
+  else \
+    accu = uint63_zero; \
+  }while(0)
+#define Uint63_lsr(x,y) do{ \
+  value uint63_lsl_y__ = (y); \
+  if (uint63_lsl_y__ < (uint64_t) 127) \
+    accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
+  else \
+    accu = uint63_zero; \
+  }while(0)
+#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1))
+#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1))
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
 /* (modulo 2^63) for p <= 63 */
@@ -40,6 +55,7 @@ value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
   r |= ((uint64_t)y >> (63-shiftby)) | 1;
   return r;
 }
+#define Uint63_addmuldiv(p, x, y) (accu = uint63_addmuldiv(p, x, y))
 
 value uint63_head0(uint64_t x) {
   int r = 0;
@@ -51,6 +67,7 @@ value uint63_head0(uint64_t x) {
   if (!(x & 0x8000000000000000)) { x <<=1;   r += 1; }
   return Val_int(r);
 }
+#define Uint63_head0(x) (accu = uint63_head0(x))
 
 value uint63_tail0(value x) {
   int r = 0;
@@ -63,6 +80,7 @@ value uint63_tail0(value x) {
   if (!(x & 0x00000001)) { x >>=1;   r += 1; }
   return Val_int(r);
 }
+#define Uint63_tail0(x) (accu = uint63_tail0(x))
 
 value uint63_mulc(value x, value y, value* h) {
   x = (uint64_t)x >> 1;
@@ -86,6 +104,7 @@ value uint63_mulc(value x, value y, value* h) {
   *h = Val_int(hr);
   return Val_int(lr);
 }
+#define Uint63_mulc(x, y, h) (accu = uint63_mulc(x, y, h))
 
 #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
 #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
@@ -123,3 +142,4 @@ value uint63_div21(value xh, value xl, value y, value* q) {
   *q = Val_int(quotient);
   return Val_int(reml);
 }
+#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))