diff options
| -rw-r--r-- | rust-tests/src/main.rs | 6 | ||||
| -rw-r--r-- | src/Contexts.ml | 2 | ||||
| -rw-r--r-- | src/Interpreter.ml | 84 | ||||
| -rw-r--r-- | src/Scalars.ml | 19 |
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 () |