Implement eval_unary_op_symbolic

3 files changed, 23 insertions, 4 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 192dfe25..44bd1b9e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3098,14 +3098,26 @@ let eval_unary_op_concrete (config : C.config) (ctx : C.eval_ctx)
       match mk_scalar sv.int_ty i with
       | Error _ -> Error Panic
       | Ok sv -> Ok (ctx, { v with V.value = V.Concrete (V.Scalar sv) }))
-  | (E.Not | E.Neg), Symbolic _ -> raise Unimplemented (* TODO *)
   | _ -> failwith "Invalid value for unop"
 
 let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
     (unop : E.unop) (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result
     =
-  S.synthesize_unary_op unop op;
-  raise Unimplemented
+  (* Evaluate the operand *)
+  let ctx, v = eval_operand config ctx op in
+  (* Generate a fresh symbolic value to store the result *)
+  let ctx, res_sv_id = C.fresh_symbolic_value_id ctx in
+  let res_sv_ty =
+    match (unop, v.V.ty) with
+    | E.Not, T.Bool -> T.Bool
+    | E.Neg, T.Integer int_ty -> T.Integer int_ty
+    | _ -> failwith "Invalid parameters for unop"
+  in
+  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  (* Synthesize *)
+  S.synthesize_unary_op unop v res_sv;
+  (* Return *)
+  Ok (ctx, mk_typed_value_from_symbolic_value res_sv)
 
 let eval_unary_op (config : C.config) (ctx : C.eval_ctx) (unop : E.unop)
     (op : E.operand) : (C.eval_ctx * V.typed_value) eval_result =
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 4633664f..20d4c3af 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -79,6 +79,11 @@ let mk_typed_value_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_value =
   let value = V.Symbolic sv in
   { V.value; ty }
 
+let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
+    V.typed_value =
+  let spc = { V.svalue; rset_ended = T.RegionId.Set.empty } in
+  mk_typed_value_from_proj_comp spc
+
 let mk_aproj_loans_from_proj_comp (sv : V.symbolic_proj_comp) : V.typed_avalue =
   let ty = sv.V.svalue.V.sv_ty in
   let proj = V.AProjLoans sv.V.svalue in
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 1519d0f0..aef001be 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -31,7 +31,9 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
     (see : symbolic_expansion) : unit =
   ()
 
-let synthesize_unary_op (unop : E.unop) (op : E.operand) : unit = ()
+let synthesize_unary_op (unop : E.unop) (op : V.typed_value)
+    (dest : V.symbolic_value) : unit =
+  ()
 
 let synthesize_binary_op (binop : E.binop) (op1 : E.operand) (op2 : E.operand) :
     unit =