summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--rust-tests/src/main.rs9
-rw-r--r--src/CfimOfJson.ml24
-rw-r--r--src/Interpreter.ml78
-rw-r--r--src/Print.ml14
-rw-r--r--src/Scalars.ml52
-rw-r--r--src/Values.ml14
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 =
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 01:04:26 +0000