Implement eval_binary_op

6 files changed, 97 insertions, 94 deletions

diff --git a/rust-tests/src/main.rs b/rust-tests/src/main.rs
index b7478c0e..3e0e7a43 100644
--- a/rust-tests/src/main.rs
+++ b/rust-tests/src/main.rs
@@ -1,5 +1,9 @@
 /// The following code generates the limits for the scalar types
 
+fn test_modulo(x: i32, y: i32) {
+    println!("{} % {} = {}", x, y, x % y);
+}
+
 fn main() {
     let ints_lower = [
         "isize", "i8", "i16", "i32", "i64", "i128", "usize", "u8", "u16", "u32", "u64", "u128",
@@ -72,4 +76,9 @@ fn main() {
         println!("| Types.{} -> Ok ({} i)", s, s);
     }
     println!("\n");
+
+    // Modulo tests
+    test_modulo(1, 2);
+    test_modulo(-1, 2);
+    test_modulo(-1, -2);
 }
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 39aa88f6..681bc009 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -203,40 +203,40 @@ let scalar_value_of_json (js : json) : (scalar_value, string) result =
       (match js with
       | `Assoc [ ("Isize", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (Isize bi)
+          Ok { value = bi; int_ty = Isize }
       | `Assoc [ ("I8", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (I8 bi)
+          Ok { value = bi; int_ty = I8 }
       | `Assoc [ ("I16", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (I16 bi)
+          Ok { value = bi; int_ty = I16 }
       | `Assoc [ ("I32", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (I32 bi)
+          Ok { value = bi; int_ty = I32 }
       | `Assoc [ ("I64", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (I64 bi)
+          Ok { value = bi; int_ty = I64 }
       | `Assoc [ ("I128", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (I128 bi)
+          Ok { value = bi; int_ty = I128 }
       | `Assoc [ ("Usize", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (Usize bi)
+          Ok { value = bi; int_ty = Usize }
       | `Assoc [ ("U8", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (U8 bi)
+          Ok { value = bi; int_ty = U8 }
       | `Assoc [ ("U16", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (U16 bi)
+          Ok { value = bi; int_ty = U16 }
       | `Assoc [ ("U32", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (U32 bi)
+          Ok { value = bi; int_ty = U32 }
       | `Assoc [ ("U64", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (U64 bi)
+          Ok { value = bi; int_ty = U64 }
       | `Assoc [ ("U128", bi) ] ->
           let* bi = big_int_of_json bi in
-          Ok (U128 bi)
+          Ok { value = bi; int_ty = U128 }
       | _ -> Error "")
   in
   match res with
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d63f48d5..ebb4f2ee 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -1462,7 +1462,7 @@ let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety)
   | Types.Str, ConstantValue (String v) -> { value = Concrete (String v); ty }
   | Types.Integer int_ty, ConstantValue (Scalar v) ->
       (* Check the type and the ranges *)
-      assert (int_ty == scalar_value_get_integer_type v);
+      assert (int_ty == v.int_ty);
       assert (check_scalar_value_in_range v);
       { value = Concrete (Scalar v); ty }
   (* Remaining cases (invalid) - listing as much as we can on purpose
@@ -1515,15 +1515,81 @@ let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop)
   | Not, Concrete (Bool b) ->
       Ok (ctx1, { v with value = Concrete (Bool (not b)) })
   | Neg, Concrete (Scalar sv) -> (
-      let int_ty = scalar_value_get_integer_type sv in
-      let i = scalar_value_get_value sv in
-      let i = Z.neg i in
-      match mk_scalar int_ty i with
+      let i = Z.neg sv.value in
+      match mk_scalar sv.int_ty i with
       | Error _ -> Error Panic
       | Ok sv -> Ok (ctx1, { v with value = Concrete (Scalar sv) }))
   | (Not | Neg), Symbolic _ -> raise Unimplemented (* TODO *)
   | _ -> failwith "Invalid value for unop"
 
+let eval_binary_op (config : config) (ctx : eval_ctx) (binop : binop)
+    (op1 : operand) (op2 : operand) : (eval_ctx * typed_value) eval_result =
+  (* Evaluate the operands *)
+  let access = Read in
+  let ctx1, v1 = eval_operand config ctx op1 in
+  let ctx2, v2 = eval_operand config ctx1 op2 in
+  (* Binary operations only apply on integer values, but when we check for
+   * equality *)
+  if binop = Eq || binop = Ne then (
+    (* Equality/inequality check is primitive only on primitive types *)
+    assert (v1.ty = v2.ty);
+    let b = v1 = v2 in
+    Ok (ctx2, { value = Concrete (Bool b); ty = Types.Bool }))
+  else
+    match (v1.value, v2.value) with
+    | Concrete (Scalar sv1), Concrete (Scalar sv2) -> (
+        let res =
+          (* There are binops which require the two operands to have the same
+             type, and binops for which it is not the case.
+             There are also binops which return booleans, and binops which
+             return integers.
+          *)
+          match binop with
+          | Lt | Le | Ge | Gt ->
+              (* The two operands must have the same type and the result is a boolean *)
+              assert (sv1.int_ty = sv2.int_ty);
+              let b =
+                match binop with
+                | Lt -> Z.lt sv1.value sv1.value
+                | Le -> Z.leq sv1.value sv1.value
+                | Ge -> Z.geq sv1.value sv1.value
+                | Gt -> Z.gt sv1.value sv1.value
+                | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr | Shl
+                | Shr | Ne | Eq ->
+                    failwith "Unreachable"
+              in
+              Ok { value = Concrete (Bool b); ty = Types.Bool }
+          | Div | Rem | Add | Sub | Mul | BitXor | BitAnd | BitOr -> (
+              (* The two operands must have the same type and the result is an integer *)
+              assert (sv1.int_ty = sv2.int_ty);
+              let res =
+                match binop with
+                | Div ->
+                    if sv2.value = Z.zero then Error ()
+                    else mk_scalar sv1.int_ty (Z.div sv1.value sv2.value)
+                | Rem ->
+                    (* See [https://github.com/ocaml/Zarith/blob/master/z.mli] *)
+                    if sv2.value = Z.zero then Error ()
+                    else mk_scalar sv1.int_ty (Z.rem sv1.value sv2.value)
+                | Add -> mk_scalar sv1.int_ty (Z.add sv1.value sv2.value)
+                | Sub -> mk_scalar sv1.int_ty (Z.sub sv1.value sv2.value)
+                | Mul -> mk_scalar sv1.int_ty (Z.mul sv1.value sv2.value)
+                | BitXor -> raise Unimplemented
+                | BitAnd -> raise Unimplemented
+                | BitOr -> raise Unimplemented
+                | Lt | Le | Ge | Gt | Shl | Shr | Ne | Eq ->
+                    failwith "Unreachable"
+              in
+              match res with
+              | Error err -> Error err
+              | Ok sv ->
+                  Ok { value = Concrete (Scalar sv); ty = Integer sv1.int_ty })
+          | Shl | Shr -> raise Unimplemented
+          | Ne | Eq -> failwith "Unreachable"
+        in
+        match res with Error _ -> Error Panic | Ok v -> Ok (ctx2, v))
+    | _ -> failwith "Invalid inputs for binop"
+
 let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
     (eval_ctx * typed_value) eval_result =
   match rvalue with
@@ -1573,7 +1639,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
           (* Return *)
           Ok ({ ctx3 with env = env4 }, rv))
   | UnaryOp (unop, op) -> eval_unary_op config ctx unop op
-  | BinaryOp (binop, op1, op2) -> raise Unimplemented
+  | BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
   | Discriminant p -> raise Unimplemented
   | Aggregate (aggregate_kind, ops) -> raise Unimplemented
 
diff --git a/src/Print.ml b/src/Print.ml
index 4b46914f..156c9fe1 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -180,19 +180,7 @@ module Values = struct
   let big_int_to_string (bi : big_int) : string = Z.to_string bi
 
   let scalar_value_to_string (sv : scalar_value) : string =
-    match sv with
-    | Isize bi -> big_int_to_string bi ^ ": isize"
-    | I8 bi -> big_int_to_string bi ^ ": i8"
-    | I16 bi -> big_int_to_string bi ^ ": i16"
-    | I32 bi -> big_int_to_string bi ^ ": i32"
-    | I64 bi -> big_int_to_string bi ^ ": i64"
-    | I128 bi -> big_int_to_string bi ^ ": i128"
-    | Usize bi -> big_int_to_string bi ^ ": usize"
-    | U8 bi -> big_int_to_string bi ^ ": u8"
-    | U16 bi -> big_int_to_string bi ^ ": u16"
-    | U32 bi -> big_int_to_string bi ^ ": u32"
-    | U64 bi -> big_int_to_string bi ^ ": u64"
-    | U128 bi -> big_int_to_string bi ^ ": u128"
+    big_int_to_string sv.value ^ ": " ^ integer_type_to_string sv.int_ty
 
   let constant_value_to_string (cv : constant_value) : string =
     match cv with
diff --git a/src/Scalars.ml b/src/Scalars.ml
index 178929c6..3324c24b 100644
--- a/src/Scalars.ml
+++ b/src/Scalars.ml
@@ -55,38 +55,6 @@ let usize_min = u32_min
 
 let usize_max = u32_max
 
-(** Return the integer value in a scalar value *)
-let scalar_value_get_value (v : scalar_value) : big_int =
-  match v with
-  | Isize i -> i
-  | I8 i -> i
-  | I16 i -> i
-  | I32 i -> i
-  | I64 i -> i
-  | I128 i -> i
-  | Usize i -> i
-  | U8 i -> i
-  | U16 i -> i
-  | U32 i -> i
-  | U64 i -> i
-  | U128 i -> i
-
-(** Retrieve the [integer_type] of a scalar value *)
-let scalar_value_get_integer_type (sv : scalar_value) : integer_type =
-  match sv with
-  | Isize _ -> Types.Isize
-  | I8 _ -> Types.I8
-  | I16 _ -> Types.I16
-  | I32 _ -> Types.I32
-  | I64 _ -> Types.I64
-  | I128 _ -> Types.I128
-  | Usize _ -> Types.Usize
-  | U8 _ -> Types.U8
-  | U16 _ -> Types.U16
-  | U32 _ -> Types.U32
-  | U64 _ -> Types.U64
-  | U128 _ -> Types.U128
-
 (** Check that an integer value is in range *)
 let check_int_in_range (int_ty : integer_type) (i : big_int) : bool =
   match int_ty with
@@ -105,25 +73,9 @@ let check_int_in_range (int_ty : integer_type) (i : big_int) : bool =
 
 (** Check that a scalar value is correct (the integer value it contains is in range) *)
 let check_scalar_value_in_range (v : scalar_value) : bool =
-  let i = scalar_value_get_value v in
-  let int_ty = scalar_value_get_integer_type v in
-  check_int_in_range int_ty i
+  check_int_in_range v.int_ty v.value
 
 (** Make a scalar value, while checking the value is in range *)
 let mk_scalar (int_ty : integer_type) (i : big_int) :
     (scalar_value, unit) result =
-  if check_int_in_range int_ty i then
-    match int_ty with
-    | Types.Isize -> Ok (Isize i)
-    | Types.I8 -> Ok (I8 i)
-    | Types.I16 -> Ok (I16 i)
-    | Types.I32 -> Ok (I32 i)
-    | Types.I64 -> Ok (I64 i)
-    | Types.I128 -> Ok (I128 i)
-    | Types.Usize -> Ok (Usize i)
-    | Types.U8 -> Ok (U8 i)
-    | Types.U16 -> Ok (U16 i)
-    | Types.U32 -> Ok (U32 i)
-    | Types.U64 -> Ok (U64 i)
-    | Types.U128 -> Ok (U128 i)
-  else Error ()
+  if check_int_in_range int_ty i then Ok { value = i; int_ty } else Error ()
diff --git a/src/Values.ml b/src/Values.ml
index 90267ce1..5c31feef 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -31,24 +31,12 @@ let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
 
 let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
 
+type scalar_value = { value : big_int; int_ty : integer_type }
 (** A scalar value
 
     Note that we use unbounded integers everywhere.
     We then harcode the boundaries for the different types.
  *)
-type scalar_value =
-  | Isize of big_int
-  | I8 of big_int
-  | I16 of big_int
-  | I32 of big_int
-  | I64 of big_int
-  | I128 of big_int
-  | Usize of big_int
-  | U8 of big_int
-  | U16 of big_int
-  | U32 of big_int
-  | U64 of big_int
-  | U128 of big_int
 
 (** A constant value *)
 type constant_value =