diff options
| -rw-r--r-- | src/Interpreter.ml | 214 |
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 |