completes bvops

lib/constructors/bitVector.ml

@@ -124,6 +124,26 @@ let mk_shr_s (e1 : expr) (e2 : expr) (t : num_type) : expr =
   in
   Binop (op, e1, e2)
 
+let mk_rotl (e1 : expr) (e2 : expr) (t : num_type) : expr =
+  let op =
+    match t with
+    | `I32Type -> I32 I32.Rotl
+    | `I64Type -> I64 I64.Rotl
+    | _ ->
+        raise (Error ("mk_rotl: invalid type '" ^ string_of_num_type t ^ "'"))
+  in
+  Binop (op, e1, e2)
+
+let mk_rotr (e1 : expr) (e2 : expr) (t : num_type) : expr =
+  let op =
+    match t with
+    | `I32Type -> I32 I32.Rotr
+    | `I64Type -> I64 I64.Rotr
+    | _ ->
+        raise (Error ("mk_rotr: invalid type '" ^ string_of_num_type t ^ "'"))
+  in
+  Binop (op, e1, e2)
+
 let mk_and (e1 : expr) (e2 : expr) (t : num_type) : expr =
   let op =
     match t with

lib/constructors/bitVector.mli

@@ -42,6 +42,12 @@ val mk_shr_u : expr -> expr -> num_type -> expr
 val mk_shr_s : expr -> expr -> num_type -> expr
 (** [mk_shr_u i1 i2] create an expression representing unsigned [i1 >> i2]. *)
 
+val mk_rotl : expr -> expr -> num_type -> expr
+(** [mk_rotl i1 i2] create an expression representing [rotl i1 i2]. *)
+
+val mk_rotr : expr -> expr -> num_type -> expr
+(** [mk_rotr i1 i2] create an expression representing [rotr i1 i2]. *)
+
 val mk_and : expr -> expr -> num_type -> expr
 (** [mk_and i1 i2] create an expression representing unsigned [i1 & i2]. *)
 

lib/exec/eval_numeric.ml

@@ -65,6 +65,7 @@ module I32Op = struct
       | Shl -> shl
       | ShrU -> shr_s
       | ShrS -> shr_u
+      | Rotl | Rotr -> assert false
     in
     fun v1 v2 -> to_value (f (of_value 1 v1) (of_value 2 v2))
 
@@ -139,6 +140,7 @@ module I64Op = struct
       | Shl -> shl
       | ShrU -> shr_s
       | ShrS -> shr_u
+      | Rotl | Rotr -> assert false
     in
     fun v1 v2 -> to_value (f (of_value 1 v1) (of_value 2 v2))
 

lib/mappings/z3_mappings.ml

@@ -272,6 +272,7 @@ module I32Z3Op = struct
       | ShrU -> BitVector.mk_lshr ctx
       | RemS -> BitVector.mk_srem ctx
       | RemU -> BitVector.mk_urem ctx
+      | Rotl | Rotr -> failwith "z3_mappings: rotl|rotr not implemented!"
     in
     op' e1 e2
 
@@ -295,12 +296,13 @@ module I32Z3Op = struct
   let encode_cvtop (op : cvtop) (e : Expr.expr) : Expr.expr =
     let op' =
       match op with
+      | WrapI64 -> BitVector.mk_extract ctx 31 0
       | TruncSF32 -> fun f -> FloatingPoint.mk_to_sbv ctx rtz f 32
       | TruncUF32 -> fun f -> FloatingPoint.mk_to_ubv ctx rtz f 32
       | TruncSF64 -> fun f -> FloatingPoint.mk_to_sbv ctx rtz f 32
       | TruncUF64 -> fun f -> FloatingPoint.mk_to_ubv ctx rtz f 32
       | ReinterpretFloat -> FloatingPoint.mk_to_ieee_bv ctx
-      | WrapI64 | ExtendSI32 | ExtendUI32 -> assert false
+      | ExtendSI32 | ExtendUI32 -> assert false
     in
     op' e
 
@@ -340,6 +342,7 @@ module I64Z3Op = struct
       | ShrU -> BitVector.mk_lshr ctx
       | RemS -> BitVector.mk_srem ctx
       | RemU -> BitVector.mk_urem ctx
+      | Rotl | Rotr -> failwith "z3_mappings: rotl|rotr not implemented!"
     in
     op' e1 e2
 

lib/operators/bvOp.ml

@@ -12,6 +12,8 @@ type binop =
   | ShrS
   | Or
   | Xor
+  | Rotl
+  | Rotr
 [@@deriving compare, sexp_of, hash]
 
 type unop = Not | Clz (*  Falta:  Ctz | Popcnt *)
@@ -64,6 +66,8 @@ let string_of_binop (op : binop) : string =
   | ShrU -> "shr_u"
   | RemS -> "rem_s"
   | RemU -> "rem_u"
+  | Rotl -> "rotl"
+  | Rotr -> "rotr"
 
 let string_of_relop (op : relop) : string =
   match op with