Implement eval_unary_op

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 ()