Make progress on inserting more calls for synthesis

1 files changed, 112 insertions, 102 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index e27aaaa8..d7004371 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -3176,6 +3176,114 @@ let eval_binary_op (config : C.config) (ctx : C.eval_ctx) (binop : E.binop)
   | C.ConcreteMode -> eval_binary_op_concrete config ctx binop op1 op2
   | C.SymbolicMode -> eval_binary_op_symbolic config ctx binop op1 op2
 
+let eval_rvalue_discriminant (config : C.config) (ctx : C.eval_ctx)
+    (p : E.place) : (C.eval_ctx * V.typed_value) eval_result =
+  S.synthesize_eval_rvalue_discriminant p;
+  (* Note that discriminant values have type `isize` *)
+  (* Access the value *)
+  let access = Read in
+  let ctx, v = prepare_rplace config access p ctx in
+  match v.V.value with
+  | Adt av -> (
+      match av.variant_id with
+      | None ->
+          failwith "Invalid input for `discriminant`: structure instead of enum"
+      | Some variant_id -> (
+          let id = Z.of_int (T.VariantId.to_int variant_id) in
+          match mk_scalar Isize id with
+          | Error _ ->
+              failwith "Disciminant id out of range"
+              (* Should really never happen *)
+          | Ok sv ->
+              Ok
+                (ctx, { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize })
+          ))
+  | Symbolic _ -> raise Unimplemented
+  | _ -> failwith "Invalid input for `discriminant`"
+
+let eval_rvalue_ref (config : C.config) (ctx : C.eval_ctx) (p : E.place)
+    (bkind : E.borrow_kind) : (C.eval_ctx * V.typed_value) eval_result =
+  S.synthesize_eval_rvalue_ref p bkind;
+  match bkind with
+  | E.Shared | E.TwoPhaseMut ->
+      (* Access the value *)
+      let access = if bkind = E.Shared then Read else Write in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Compute the rvalue - simply a shared borrow with a fresh id *)
+      let ctx, bid = C.fresh_borrow_id ctx in
+      (* Note that the reference is *mutable* if we do a two-phase borrow *)
+      let rv_ty =
+        T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
+      in
+      let bc =
+        if bkind = E.Shared then V.SharedBorrow bid
+        else V.InactivatedMutBorrow bid
+      in
+      let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
+      (* Compute the value with which to replace the value at place p *)
+      let nv =
+        match v.V.value with
+        | V.Loan (V.SharedLoan (bids, sv)) ->
+            (* Shared loan: insert the new borrow id *)
+            let bids1 = V.BorrowId.Set.add bid bids in
+            { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
+        | _ ->
+            (* Not a shared loan: add a wrapper *)
+            let v' = V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v)) in
+            { v with V.value = v' }
+      in
+      (* Update the value in the context *)
+      let ctx = write_place_unwrap config access p nv ctx in
+      (* Return *)
+      Ok (ctx, rv)
+  | E.Mut ->
+      (* Access the value *)
+      let access = Write in
+      let ctx, v = prepare_rplace config access p ctx in
+      (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
+      let ctx, bid = C.fresh_borrow_id ctx in
+      let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
+      let rv : V.typed_value =
+        { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
+      in
+      (* Compute the value with which to replace the value at place p *)
+      let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
+      (* Update the value in the context *)
+      let ctx = write_place_unwrap config access p nv ctx in
+      (* Return *)
+      Ok (ctx, rv)
+
+let eval_rvalue_aggregate (config : C.config) (ctx : C.eval_ctx)
+    (aggregate_kind : E.aggregate_kind) (ops : E.operand list) :
+    (C.eval_ctx * V.typed_value) eval_result =
+  S.synthesize_eval_rvalue_aggregate aggregate_kind ops;
+  (* Evaluate the operands *)
+  let ctx, values = eval_operands config ctx ops in
+  (* Match on the aggregate kind *)
+  match aggregate_kind with
+  | E.AggregatedTuple ->
+      let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
+      let v = V.Adt { variant_id = None; field_values = values } in
+      let ty = T.Adt (T.Tuple, [], tys) in
+      Ok (ctx, { V.value = v; ty })
+  | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
+      (* Sanity checks *)
+      let type_def = C.ctx_lookup_type_def ctx def_id in
+      assert (List.length type_def.region_params = List.length regions);
+      let expected_field_types =
+        Subst.ctx_adt_get_instantiated_field_etypes ctx def_id opt_variant_id
+          types
+      in
+      assert (
+        expected_field_types
+        = List.map (fun (v : V.typed_value) -> v.V.ty) values);
+      (* Construct the value *)
+      let av : V.adt_value =
+        { V.variant_id = opt_variant_id; V.field_values = values }
+      in
+      let aty = T.Adt (T.AdtId def_id, regions, types) in
+      Ok (ctx, { V.value = Adt av; ty = aty })
+
 (** Evaluate an rvalue in a given context: return the updated context and
     the computed value
 *)
@@ -3183,110 +3291,12 @@ let eval_rvalue (config : C.config) (ctx : C.eval_ctx) (rvalue : E.rvalue) :
     (C.eval_ctx * V.typed_value) eval_result =
   match rvalue with
   | E.Use op -> Ok (eval_operand config ctx op)
-  | E.Ref (p, bkind) -> (
-      match bkind with
-      | E.Shared | E.TwoPhaseMut ->
-          (* Access the value *)
-          let access = if bkind = E.Shared then Read else Write in
-          let ctx, v = prepare_rplace config access p ctx in
-          (* Compute the rvalue - simply a shared borrow with a fresh id *)
-          let ctx, bid = C.fresh_borrow_id ctx in
-          (* Note that the reference is *mutable* if we do a two-phase borrow *)
-          let rv_ty =
-            T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut)
-          in
-          let bc =
-            if bkind = E.Shared then V.SharedBorrow bid
-            else V.InactivatedMutBorrow bid
-          in
-          let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in
-          (* Compute the value with which to replace the value at place p *)
-          let nv =
-            match v.V.value with
-            | V.Loan (V.SharedLoan (bids, sv)) ->
-                (* Shared loan: insert the new borrow id *)
-                let bids1 = V.BorrowId.Set.add bid bids in
-                { v with V.value = V.Loan (V.SharedLoan (bids1, sv)) }
-            | _ ->
-                (* Not a shared loan: add a wrapper *)
-                let v' =
-                  V.Loan (V.SharedLoan (V.BorrowId.Set.singleton bid, v))
-                in
-                { v with V.value = v' }
-          in
-          (* Update the value in the context *)
-          let ctx = write_place_unwrap config access p nv ctx in
-          (* Return *)
-          Ok (ctx, rv)
-      | E.Mut ->
-          (* Access the value *)
-          let access = Write in
-          let ctx, v = prepare_rplace config access p ctx in
-          (* Compute the rvalue - wrap the value in a mutable borrow with a fresh id *)
-          let ctx, bid = C.fresh_borrow_id ctx in
-          let rv_ty = T.Ref (T.Erased, v.ty, Mut) in
-          let rv : V.typed_value =
-            { V.value = V.Borrow (V.MutBorrow (bid, v)); ty = rv_ty }
-          in
-          (* Compute the value with which to replace the value at place p *)
-          let nv = { v with V.value = V.Loan (V.MutLoan bid) } in
-          (* Update the value in the context *)
-          let ctx = write_place_unwrap config access p nv ctx in
-          (* Return *)
-          Ok (ctx, rv))
+  | E.Ref (p, bkind) -> eval_rvalue_ref config ctx p bkind
   | E.UnaryOp (unop, op) -> eval_unary_op config ctx unop op
   | E.BinaryOp (binop, op1, op2) -> eval_binary_op config ctx binop op1 op2
-  | E.Discriminant p -> (
-      (* Note that discriminant values have type `isize` *)
-      (* Access the value *)
-      let access = Read in
-      let ctx, v = prepare_rplace config access p ctx in
-      match v.V.value with
-      | Adt av -> (
-          match av.variant_id with
-          | None ->
-              failwith
-                "Invalid input for `discriminant`: structure instead of enum"
-          | Some variant_id -> (
-              let id = Z.of_int (T.VariantId.to_int variant_id) in
-              match mk_scalar Isize id with
-              | Error _ ->
-                  failwith "Disciminant id out of range"
-                  (* Should really never happen *)
-              | Ok sv ->
-                  Ok
-                    ( ctx,
-                      { V.value = V.Concrete (V.Scalar sv); ty = Integer Isize }
-                    )))
-      | Symbolic _ -> raise Unimplemented
-      | _ -> failwith "Invalid input for `discriminant`")
-  | E.Aggregate (aggregate_kind, ops) -> (
-      (* Evaluate the operands *)
-      let ctx, values = eval_operands config ctx ops in
-      (* Match on the aggregate kind *)
-      match aggregate_kind with
-      | E.AggregatedTuple ->
-          let tys = List.map (fun (v : V.typed_value) -> v.V.ty) values in
-          let v = V.Adt { variant_id = None; field_values = values } in
-          let ty = T.Adt (T.Tuple, [], tys) in
-          Ok (ctx, { V.value = v; ty })
-      | E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
-          (* Sanity checks *)
-          let type_def = C.ctx_lookup_type_def ctx def_id in
-          assert (List.length type_def.region_params = List.length regions);
-          let expected_field_types =
-            Subst.ctx_adt_get_instantiated_field_etypes ctx def_id
-              opt_variant_id types
-          in
-          assert (
-            expected_field_types
-            = List.map (fun (v : V.typed_value) -> v.V.ty) values);
-          (* Construct the value *)
-          let av : V.adt_value =
-            { V.variant_id = opt_variant_id; V.field_values = values }
-          in
-          let aty = T.Adt (T.AdtId def_id, regions, types) in
-          Ok (ctx, { V.value = Adt av; ty = aty }))
+  | E.Discriminant p -> eval_rvalue_discriminant config ctx p
+  | E.Aggregate (aggregate_kind, ops) ->
+      eval_rvalue_aggregate config ctx aggregate_kind ops
 
 (** Result of evaluating a statement *)
 type statement_eval_res = Unit | Break of int | Continue of int | Return