summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-24 14:20:26 +0100
committerSon Ho2021-11-24 14:20:26 +0100
commited18b966b671fdd1da60b6582a4bdd92813d5e5a (patch)
tree8ffd45debe3564abd9068f8765888ef3a0331bc9
parent094d59f4a17feab59d379a1fc3df490ad6595085 (diff)
Implement eval_unary_op
-rw-r--r--rust-tests/src/main.rs6
-rw-r--r--src/Contexts.ml2
-rw-r--r--src/Interpreter.ml84
-rw-r--r--src/Scalars.ml19
4 files changed, 69 insertions, 42 deletions
diff --git a/rust-tests/src/main.rs b/rust-tests/src/main.rs
index e85acf8c..b7478c0e 100644
--- a/rust-tests/src/main.rs
+++ b/rust-tests/src/main.rs
@@ -66,4 +66,10 @@ fn main() {
println!("| {} i -> i", s);
}
println!("\n");
+
+ // Generate the mk_scalar body
+ for s in &ints_upper {
+ println!("| Types.{} -> Ok ({} i)", s, s);
+ }
+ println!("\n");
}
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 1f7d28a4..afa68272 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -8,8 +8,6 @@ type env_value = Var of VarId.id * typed_value | Abs of abs
type env = env_value list
-type 'a eval_result = Stuck | Panic | Res of 'a
-
type interpreter_mode = ConcreteMode | SymbolicMode
type config = { mode : interpreter_mode; check_invariants : bool }
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index d1c2889f..0eee9bc5 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -10,6 +10,10 @@ open Contexts
(* TODO: Change state-passing style to : st -> ... -> (st, v) *)
(* TODO: check that the value types are correct when evaluating *)
+type eval_error = Panic
+
+type 'a eval_result = ('a, eval_error) result
+
type exploration_kind = {
enter_shared_loans : bool;
enter_mut_borrows : bool;
@@ -1466,57 +1470,59 @@ let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety)
| _, Unit | _, ConstantAdt _ | _, ConstantValue _ ->
failwith "Improperly typed constant value"
+(** Small utility *)
+let prepare_rplace (config : config) (access : access_kind) (p : place)
+ (ctx : eval_ctx) : eval_ctx * typed_value =
+ let env1 = update_env_along_read_place config access p ctx.env in
+ let env2 = collect_borrows_at_place config access p env1 in
+ let v = read_place_unwrap config access p env2 in
+ let ctx2 = { ctx with env = env2 } in
+ (ctx2, v)
+
let eval_operand (config : config) (ctx : eval_ctx) (op : operand) :
eval_ctx * typed_value =
match op with
| Expressions.Constant (ty, cv) ->
let v = constant_value_to_typed_value ctx ty cv in
(ctx, v)
- | Expressions.Copy p -> (
+ | Expressions.Copy p ->
(* Access the value *)
let access = Read in
- let env1 = update_env_along_read_place config access p ctx.env in
- let env2 = collect_borrows_at_place config access p env1 in
- match read_place config access p env2 with
- | Error _ -> failwith "Unreachable"
- | Ok v ->
- (* Copy the value *)
- assert (not (bottom_in_value v));
- let ctx2 = { ctx with env = env2 } in
- copy_value config ctx2 v)
+ let ctx2, v = prepare_rplace config access p ctx in
+ (* Copy the value *)
+ assert (not (bottom_in_value v));
+ copy_value config ctx2 v
| Expressions.Move p -> (
(* Access the value *)
let access = Move in
- let env1 = update_env_along_read_place config access p ctx.env in
- let env2 = collect_borrows_at_place config access p env1 in
- match read_place config access p env2 with
+ let ctx2, v = prepare_rplace config access p ctx in
+ (* Move the value *)
+ assert (not (bottom_in_value v));
+ let bottom = { value = Bottom; ty = v.ty } in
+ match write_place config access p bottom ctx2.env with
| Error _ -> failwith "Unreachable"
- | Ok v -> (
- (* Move the value *)
- assert (not (bottom_in_value v));
- let bottom = { value = Bottom; ty = v.ty } in
- match write_place config access p bottom env2 with
- | Error _ -> failwith "Unreachable"
- | Ok env3 ->
- let ctx3 = { ctx with env = env3 } in
- (ctx3, v)))
+ | Ok env3 ->
+ let ctx3 = { ctx2 with env = env3 } in
+ (ctx3, v))
-(** Small utility *)
-let prepare_rplace (config : config) (access : access_kind) (p : place)
- (ctx : eval_ctx) : eval_ctx =
- let env1 = update_env_along_read_place config access p ctx.env in
- let env2 = collect_borrows_at_place config access p env1 in
- { ctx with env = env2 }
-
-(*let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop) (op : operand) :
- eval_ctx * typed_value =
+let eval_unary_op (config : config) (ctx : eval_ctx) (unop : unop)
+ (op : operand) : (eval_ctx * typed_value) eval_result =
(* Evaluate the operand *)
let access = Read in
- let env1 = update_env_along_read_place config access p ctx.env in
- let env2 = collect_borrows_at_place config access p env1 in
- (* *)
- match unop with
- |*)
+ let ctx1, v = eval_operand config ctx op in
+ (* Apply the unop *)
+ match (unop, v.value) with
+ | 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
+ | 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_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
eval_ctx * typed_value =
@@ -1527,8 +1533,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
| Expressions.Shared | Expressions.TwoPhaseMut ->
(* Access the value *)
let access = if bkind = Expressions.Shared then Read else Write in
- let ctx2 = prepare_rplace config access p ctx in
- let v = read_place_unwrap config access p ctx2.env in
+ let ctx2, v = prepare_rplace config access p ctx in
(* Compute the rvalue - simply a shared borrow with a fresh id *)
let ctx3, bid = fresh_borrow_id ctx2 in
let rv_ty = Types.Ref (Erased, v.ty, Shared) in
@@ -1556,8 +1561,7 @@ let eval_rvalue (config : config) (ctx : eval_ctx) (rvalue : rvalue) :
| Expressions.Mut ->
(* Access the value *)
let access = Write in
- let ctx2 = prepare_rplace config access p ctx in
- let v = read_place_unwrap config access p ctx2.env in
+ let ctx2, v = prepare_rplace config access p ctx in
(* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
let ctx3, bid = fresh_borrow_id ctx2 in
let rv_ty = Types.Ref (Erased, v.ty, Mut) in
diff --git a/src/Scalars.ml b/src/Scalars.ml
index 29c2779f..178929c6 100644
--- a/src/Scalars.ml
+++ b/src/Scalars.ml
@@ -108,3 +108,22 @@ 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
+
+(** 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 ()