summaryrefslogtreecommitdiff
path: root/src/Interpreter.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/Interpreter.ml')
-rw-r--r--src/Interpreter.ml214
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