Add ROL and ROR operators (#290)

Extend lexing and parsing with `<<r` and `>>r`.
Extend latex and EasyCrypt printing.
Define operators in `eclib/JWord.ec`.
Implement lowering for x86 and ARM-M4.
Add rotation operators to CHANGELOG

CHANGELOG.md

@@ -17,6 +17,10 @@
   `VPAVG`
   ([PR #285](https://github.com/jasmin-lang/jasmin/pull/285)).
 
+- Add bit rotation operators for expressions: `<<r` and `>>r`
+  ([PR #290](https://github.com/jasmin-lang/jasmin/pull/290)).
+  These get extracted to `|<<|` and `|>>|` in EasyCrypt.
+
 ## Other changes
 
 - Explicit if-then-else in flag combinations is no longer supported

compiler/examples/arm_m4/intrinsic_ror.jazz

@@ -5,7 +5,8 @@ fn add(reg u32 arg0, reg u32 arg1) -> reg u32 {
 
     // Immediates.
     x = #ROR(x, 1);
-    x = #ROR(x, 3);
+    x = #ROR(x, 4);
+    x = #ROR(x, 31);
 
     // Set flags.
     reg bool n, z, c, v;

compiler/examples/arm_m4/ror.jazz

@@ -0,0 +1,36 @@
+export
+fn ror(reg u32 arg0, reg u32 arg1) -> reg u32 {
+    reg u32 x;
+    x = arg0 >>r arg1;
+
+    // Immediates.
+    x = x >>r 1;
+    x = x >>r 4;
+    x = x >>r 31;
+
+    // Set flags.
+    reg bool n, z, c, v;
+    n, z, c, v, _ = #MOVS(x);
+
+    // Conditions.
+    x = x >>r arg0 if z;            // EQ
+    x = x >>r arg0 if !z;           // NE
+    x = x >>r arg0 if c;            // CS
+    x = x >>r arg0 if !c;           // CC
+    x = x >>r arg0 if n;            // MI
+    x = x >>r arg0 if !n;           // PL
+    x = x >>r arg0 if v;            // VS
+    x = x >>r arg0 if !v;           // VC
+    x = x >>r arg0 if c && !z;      // HI
+    x = x >>r arg0 if !c || z;      // LS
+    x = x >>r arg0 if n == v;       // GE
+    x = x >>r arg0 if n != v;       // LT
+    x = x >>r arg0 if !z && n == v; // GT
+    x = x >>r arg0 if z || n != v;  // LE
+
+    x = x >>r 1 if !!!!z;
+
+    reg u32 res;
+    res = x;
+    return res;
+}

compiler/src/latex_printer.ml

@@ -55,6 +55,8 @@ let pp_op2 fmt =
   | `BXOr s -> f s "\\textasciicircum{}"
   | `ShR s -> f s ">{}>"
   | `ShL s -> f s "<{}<"
+  | `ROR s -> f s ">{}>r"
+  | `ROL s -> f s "<{}<r"
   | `Eq s -> f s "=="
   | `Neq s -> f s "!="
   | `Lt s -> f s "<"
@@ -94,7 +96,7 @@ let prio_of_op2 =
   | `BAnd _ -> Pbwand
   | `BOr _ -> Pbwor
   | `BXOr _ -> Pbwxor
-  | `ShR _ | `ShL _ -> Pshift
+  | `ShR _  | `ShL _ | `ROR _ | `ROL _ -> Pshift
   | `Eq _ | `Neq _ -> Pcmpeq
   | `Lt _ | `Le _ | `Gt _ | `Ge _
     -> Pcmp

compiler/src/lexer.mll

@@ -152,6 +152,8 @@ rule main = parse
   | "?"     { QUESTIONMARK  }
   | ":"     { COLON  }
 
+  | ">>r"                   { ROR              }
+  | "<<r"                   { ROL              }
   | "<<"                    { LTLT            }
   | "<=" (signletter as s)? { LE   (mk_sign s) }
   | "<"  (signletter as s)? { LT   (mk_sign s) }

compiler/src/parser.mly

@@ -65,6 +65,8 @@
 %token REG
 %token REQUIRE
 %token RETURN
+%token ROR
+%token ROL
 %token SEMICOLON
 %token <Syntax.swsize>SWSIZE
 %token <Syntax.svsize> SVSIZE
@@ -88,7 +90,7 @@
 %left PIPE
 %left HAT
 %left AMP
-%left LTLT GTGT
+%left LTLT GTGT ROR ROL
 %left PLUS MINUS
 %left STAR SLASH PERCENT
 %nonassoc BANG 
@@ -211,6 +213,8 @@ cast:
 | HAT         c=castop { `BXOr c}
 | LTLT        c=castop { `ShL  c} 
 | s=loc(GTGT) c=castop { `ShR (setsign c s)}
+| ROR         c=castop { `ROR  c}
+| ROL         c=castop { `ROL  c}
 | EQEQ        c=castop { `Eq   c}
 | BANGEQ      c=castop { `Neq  c}
 | s=loc(LT)   c=castop { `Lt  (setsign c s)}
@@ -294,6 +298,8 @@ peqop:
 | STAR  c=castop EQ  { `Mul  c }
 | s=loc(GTGT)  c=castop EQ  { `ShR  (setsign c s) }
 | LTLT  c=castop EQ  { `ShL  c }
+| ROR   c=castop EQ  { `ROR  c }
+| ROL   c=castop EQ  { `ROL  c }
 | AMP   c=castop EQ  { `BAnd c }
 | HAT   c=castop EQ  { `BXOr c }
 | PIPE  c=castop EQ  { `BOr  c }

compiler/src/pretyping.ml

@@ -857,7 +857,20 @@ let shr_info =
     opi_wcmp = true, cmp_8_256;
     opi_vcmp = Some cmp_8_64;
   }
-
+
+let rot_info exn op =
+  let mk opk =
+    match opk with
+    | OpKE Cmp_int -> raise exn
+    | OpKE (Cmp_w (_, ws)) -> op ws
+    | OpKV _ -> raise exn
+  in
+  {
+    opi_op = mk;
+    opi_wcmp = true, cmp_8_64;
+    opi_vcmp = None;
+  }
+
 let shl_info = 
   let mk = function
     | OpKE (Cmp_int)      -> E.Olsl E.Op_int
@@ -903,6 +916,8 @@ let op2_of_pop2 exn ty (op : S.peop2) =
   | `BXOr c -> op2_of_ty exn op c (max_ty ty P.u256 |> oget ~exn) lxor_info
   | `ShR  c -> op2_of_ty exn op c ty shr_info
   | `ShL  c -> op2_of_ty exn op c ty shl_info
+  | `ROR  c -> op2_of_ty exn op c ty (rot_info exn (fun x -> E.Oror x))
+  | `ROL  c -> op2_of_ty exn op c ty (rot_info exn (fun x -> E.Orol x))
 
   | `Eq   c -> op2_of_ty exn op c ty eq_info 
   | `Neq  c -> op2_of_ty exn op c ty neq_info
@@ -931,6 +946,8 @@ let peop2_of_eqop (eqop : S.peqop) =
   | `Sub  s -> Some (`Sub s)
   | `Mul  s -> Some (`Mul s)
   | `ShR  s -> Some (`ShR s)
+  | `ROR  s -> Some (`ROR s)
+  | `ROL  s -> Some (`ROL s)
   | `ShL  s -> Some (`ShL s)
   | `BAnd s -> Some (`BAnd s)
   | `BXOr s -> Some (`BXOr s)
@@ -979,7 +996,7 @@ let tt_op2 (loc1, (e1, ety1)) (loc2, (e2, ety2))
     let ty = 
       match pop with
       | `And   | `Or    -> P.tbool 
-      | `ShR _ | `ShL _ -> ety1 
+      | `ShR _ | `ShL _ | `ROR _ | `ROL _ -> ety1
       | `Add _ | `Sub _ | `Mul _ | `Div _ | `Mod _
         | `BAnd _ | `BOr _ | `BXOr _
         | `Eq _ | `Neq _ | `Lt _ | `Le _ | `Gt _ | `Ge _ ->

compiler/src/printer.ml

@@ -83,6 +83,8 @@ let string_of_op2 = function
   | E.Olsr _ -> ">>"
   | E.Olsl _ -> "<<"
   | E.Oasr _ -> ">>s"
+  | E.Oror _ -> ">>r"
+  | E.Orol _ -> "<<r"
 
   | E.Oeq  k -> "==" ^ string_of_op_kind k
   | E.Oneq k -> "!=" ^ string_of_op_kind k

compiler/src/safety/safetyAbsExpr.ml

@@ -78,12 +78,19 @@ let op1_to_abs_unop op1 = match op1 with
   | E.Oword_of_int _ | E.Oint_of_word _ | E.Ozeroext _ -> assert false
   | _ -> None
 
+type shift_kind =
+  | Unsigned_left
+  | Unsigned_right
+  | Signed_right
+  | Rotation_right
+  | Rotation_left
+
 type word_op =
   | Wand                        (* supported only for padding with 2^n - 1 *)
   | Wor                         (* currently not-supported *)
   | Wxor                        (* currently not-supported *)
 
-  | Wshift of [`Unsigned_left | `Unsigned_right | `Signed_right ]
+  | Wshift of shift_kind
   (* Remarks: 
      - signed left is a synonymous for unsigned left.
      - currently, shift-right is not supported. *)
@@ -106,9 +113,11 @@ let op2_to_abs_binop op2 = match op2 with
   | E.Odiv (Cmp_w (Signed, _)) -> AB_Unknown
   | E.Odiv _ -> AB_Arith Texpr1.Div
 
-  | E.Olsr _ -> AB_Wop (Wshift `Unsigned_right)
-  | E.Olsl _ -> AB_Wop (Wshift `Unsigned_left)
-  | E.Oasr _ -> AB_Wop (Wshift `Signed_right)
+  | E.Olsr _ -> AB_Wop (Wshift Unsigned_right)
+  | E.Olsl _ -> AB_Wop (Wshift Unsigned_left)
+  | E.Oasr _ -> AB_Wop (Wshift Signed_right)
+  | E.Oror _ -> AB_Wop (Wshift Rotation_right)
+  | E.Orol _ -> AB_Wop (Wshift Rotation_left)
 
   | E.Obeq | E.Oand | E.Oor                   (* boolean connectives *)
   | E.Oeq _ | E.Oneq _ | E.Olt _ | E.Ole _ | E.Ogt _ | E.Oge _ -> AB_Unknown
@@ -526,7 +535,9 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
             else wrap_lin_expr Unsigned ws_out lin
           else lin
 
-        | AB_Wop (Wshift `Signed_right)
+        | AB_Wop (Wshift Signed_right)
+        | AB_Wop (Wshift Rotation_left)
+        | AB_Wop (Wshift Rotation_right)
         | AB_Arith Texpr1.Div
         | AB_Arith Texpr1.Pow
         | AB_Unknown ->
@@ -537,8 +548,8 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
             match aeval_cst_w_i abs e2 with
             | Some i when i <= int_of_ws ws_e ->
               let absop = match stype with
-                | `Unsigned_right -> Texpr1.Div
-                | `Unsigned_left -> Texpr1.Mul
+                | Unsigned_right -> Texpr1.Div
+                | Unsigned_left -> Texpr1.Mul
                 | _ -> assert false in
               let lin = Mtexpr.(binop absop
                                   (linearize_wexpr abs e1)
@@ -668,6 +679,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
     match op2 with
     | E.Obeq | E.Oand | E.Oor | E.Oadd _ | E.Omul _ | E.Osub _
     | E.Odiv _ | E.Omod _ | E.Oland _ | E.Olor _
+    | E.Oror _ | E.Orol _
     | E.Olxor _ | E.Olsr _ | E.Olsl _ | E.Oasr _ -> assert false
 
     | E.Oeq k -> (Tcons1.EQ, to_cmp_kind k)
@@ -719,6 +731,7 @@ module AbsExpr (AbsDom : AbsNumBoolType) = struct
     | Papp2 (op2, e1, e2) -> begin match op2 with
         | E.Oadd _ | E.Omul _ | E.Osub _
         | E.Odiv _ | E.Omod _ | E.Oland _ | E.Olor _
+        | E.Oror _ | E.Orol _
         | E.Olxor _ | E.Olsr _ | E.Olsl _ | E.Oasr _ -> assert false
 
         | Ovadd (_, _) | Ovsub (_, _) | Ovmul (_, _)

compiler/src/safety/safetyInterpreter.ml

@@ -234,6 +234,7 @@ let safe_op2 e2 = function
   | E.Obeq | E.Oand | E.Oor | E.Oadd _ | E.Omul _ | E.Osub _
   | E.Oland _ | E.Olor _ | E.Olxor _
   | E.Olsr _ | E.Olsl _ | E.Oasr _
+  | E.Oror _ | E.Orol _
   | E.Oeq _ | E.Oneq _ | E.Olt _ | E.Ole _ | E.Ogt _ | E.Oge _ -> []
 
   | E.Odiv E.Cmp_int -> []

compiler/src/syntax.ml

@@ -89,6 +89,8 @@ type peop2 = [
   | `BOr  of castop
   | `BXOr of castop
   | `ShR  of castop
+  | `ROR  of castop
+  | `ROL  of castop
   | `ShL  of castop
 
   | `Eq   of castop
@@ -137,6 +139,8 @@ let string_of_peop2 : peop2 -> string =
   | `BXOr s -> f s "^"
   | `ShR s -> f s ">>"
   | `ShL s -> f s "<<"
+  | `ROR s -> f s ">>r"
+  | `ROL s -> f s "<<r"
   | `Eq s -> f s "=="
   | `Neq s -> f s "!="
   | `Lt s -> f s "<"
@@ -194,6 +198,8 @@ type peqop = [
   | `Sub  of castop
   | `Mul  of castop
   | `ShR  of castop
+  | `ROR  of castop
+  | `ROL  of castop
   | `ShL  of castop
   | `BAnd of castop
   | `BXOr of castop

compiler/src/toEC.ml

@@ -463,6 +463,8 @@ let pp_op2 fmt = function
   | E.Olsr  _ -> Format.fprintf fmt "`>>`"
   | E.Olsl  _ -> Format.fprintf fmt "`<<`"
   | E.Oasr  _ -> Format.fprintf fmt "`|>>`"
+  | E.Orol _ -> Format.fprintf fmt "`|<<|`"
+  | E.Oror _ -> Format.fprintf fmt "`|>>|`"
 
   | E.Oeq   _ -> Format.fprintf fmt "="
   | E.Oneq  _ -> Format.fprintf fmt "<>"
@@ -951,6 +953,7 @@ module Leak = struct
     | E.Oadd _  | E.Omul _  | E.Osub _ 
     | E.Oland _ | E.Olor _  | E.Olxor _ 
     | E.Olsr _  | E.Olsl _  | E.Oasr _
+    | E.Orol _ | E.Oror _
     | E.Oeq _   | E.Oneq _  | E.Olt _  | E.Ole _ | E.Ogt _ | E.Oge _ 
     | E.Ovadd _ | E.Ovsub _ | E.Ovmul _
     | E.Ovlsr _ | E.Ovlsl _ | E.Ovasr _ -> safe

compiler/tests/success/test_rotations.jazz

@@ -1,15 +1,31 @@
+/* Register rotations. */
+
 export
 fn f(reg u64 x) -> reg u64 {
-reg u64 a, b, c;
-reg u8 d;
-reg bool cf, of;
-
-a = x;
-d = 4;
-_, _, a = #ROL(a, d);
-of, cf, b = #ROL(a, 2);
-cf, b += x + cf;
-_, _, c = #ROR(b, d);
-_, _, c = #ROR(c, 3);
-return c;
+    reg u64 a, b, c;
+    reg u8 d;
+    reg bool cf, of;
+
+    a = x;
+    d = 4;
+
+    // Left rotations (flags are discarded).
+    a = a <<r d;
+    a = a <<r 2;
+
+    // Intrinsic syntax.
+    _, _, a = #ROL(a, d);
+    of, cf, b = #ROL(a, 2);
+
+    cf, b += x + cf;
+
+    // Right rotations (flags are discarded).
+    c = b >>r d;
+    c = b >>r 3;
+
+    // Intrinsic syntax.
+    _, _, c = #ROR(b, d);
+    _, _, c = #ROR(c, 3);
+
+    return c;
 }