diff options
| -rw-r--r-- | src/Interpreter.ml | 138 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 8 |
2 files changed, 92 insertions, 54 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 770c1c71..50b53a67 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -3778,32 +3778,66 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list) | _ -> failwith "Inconsistent state" (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_new_symbolic (config : C.config) - (region_params : T.erased_region list) (type_params : T.ety list) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - raise Unimplemented +let eval_box_new_inst_sig (config : C.config) + (region_params : T.erased_region list) (type_params : T.ety list) : + A.inst_fun_sig = + (* The signature is: + `T -> Box<T>` + where T is the type pram + *) + match (region_params, type_params) with + | [], [ ty_param ] -> + let input = ety_no_regions_to_rty ty_param in + let output = mk_box_ty ty_param in + let output = ety_no_regions_to_rty output in + { A.regions_hierarchy = []; inputs = [ input ]; output } + | _ -> failwith "Inconsistent state" (** Auxiliary function which factorizes code to evaluate `std::Deref::deref` and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *) -let eval_box_deref_mut_or_shared_symbolic (config : C.config) +let eval_box_deref_mut_or_shared_inst_sig (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = - raise Unimplemented + (is_mut : bool) (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig = + (* The signature is: + `&'a (mut) Box<T> -> &'a (mut) T` + where T is the type param + *) + let ctx, rid = C.fresh_region_id ctx in + let r = T.Var rid in + let ctx, abs_id = C.fresh_abstraction_id ctx in + match (region_params, type_params) with + | [], [ ty_param ] -> + let ty_param = ety_no_regions_to_rty ty_param in + let ref_kind = if is_mut then T.Mut else T.Shared in + + let input = mk_box_ty ty_param in + let input = mk_ref_ty r input ref_kind in + + let output = mk_ref_ty r ty_param ref_kind in + + let regions = { A.id = abs_id; regions = [ rid ]; parents = [] } in + + let inst_sg = + { A.regions_hierarchy = [ regions ]; inputs = [ input ]; output } + in + + (ctx, inst_sg) + | _ -> failwith "Inconsistent state" (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref_symbolic (config : C.config) +let eval_box_deref_inst_sig (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig = let is_mut = false in - eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut + eval_box_deref_mut_or_shared_inst_sig config region_params type_params is_mut ctx (** Auxiliary function - see [eval_non_local_function_call] *) -let eval_box_deref_mut_symbolic (config : C.config) +let eval_box_deref_mut_inst_sig (config : C.config) (region_params : T.erased_region list) (type_params : T.ety list) - (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value = + (ctx : C.eval_ctx) : C.eval_ctx * A.inst_fun_sig = let is_mut = true in - eval_box_deref_mut_or_shared_symbolic config region_params type_params is_mut + eval_box_deref_mut_or_shared_inst_sig config region_params type_params is_mut ctx (** Evaluate a non-local function call in concrete mode *) @@ -3877,46 +3911,38 @@ let eval_non_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx) (fid : A.assumed_fun_id) (region_params : T.erased_region list) (type_params : T.ety list) (args : E.operand list) (dest : E.place) : C.eval_ctx = - raise Unimplemented - -(* (* Synthesis *) - S.synthesize_function_call (A.Assumed fid) region_params type_params args dest; - - (* Sanity check: make sure the type parameters don't contain regions - - * this is a current limitation of our synthesis *) - assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params); - - (* There are two cases (and this is extremely annoying): - - the function is not box_free - - the function is box_free - See [eval_box_free] - *) - match fid with - | A.BoxFree -> - (* Degenerate case: box_free *) - eval_box_free config region_params type_params args dest ctx - | _ -> - (* "Normal" case: not box_free *) - (* Evaluate the operands *) - let ctx, args_vl = eval_operands config ctx args in - - (* Evaluate the function call *) - let ctx, ret_value = - match fid with - | A.BoxNew -> eval_box_new_symbolic config region_params type_params ctx - | A.BoxDeref -> - eval_box_deref_symbolic config region_params type_params ctx - | A.BoxDerefMut -> - eval_box_deref_mut_symbolic config region_params type_params ctx - | A.BoxFree -> failwith "Unreachable" - (* should have been treated above *) - in - - (* Move the return value to its destination *) - let ctx = assign_to_place config ctx ret_value dest in - - (* Return *) - ctx*) + (* Sanity check: make sure the type parameters don't contain regions - + * this is a current limitation of our synthesis *) + assert (List.for_all (fun ty -> not (ty_has_regions ty)) type_params); + + (* There are two cases (and this is extremely annoying): + - the function is not box_free + - the function is box_free + See [eval_box_free] + *) + match fid with + | A.BoxFree -> + (* Degenerate case: box_free - note that this is not really a function + * call *) + eval_box_free config region_params type_params args dest ctx + | _ -> + (* "Normal" case: not box_free *) + (* In symbolic mode, the behaviour of a function call is completely defined + * by the signature of the function: we thus simply generate correctly + * instantiated signatures, and delegate the work to an auxiliary function *) + let ctx, inst_sig = + match fid with + | A.BoxNew -> + (ctx, eval_box_new_inst_sig config region_params type_params) + | A.BoxDeref -> + eval_box_deref_inst_sig config region_params type_params ctx + | A.BoxDerefMut -> + eval_box_deref_mut_inst_sig config region_params type_params ctx + | A.BoxFree -> failwith "Unreachable" + (* should have been treated above *) + in + + raise Unimplemented (** Evaluate a non-local (i.e, assumed) function call such as `Box::deref` (auxiliary helper for [eval_statement]) *) @@ -4290,6 +4316,12 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config) (* Evaluate the input operands *) let ctx, args = eval_operands config ctx args in let args_with_rtypes = List.combine args inst_sg.A.inputs in + (* Check the type of the input arguments *) + assert ( + List.for_all + (fun ((arg, rty) : V.typed_value * T.rty) -> + arg.V.ty = Subst.erase_regions rty) + args_with_rtypes); (* Generate the abstractions from the region groups and add them to the context *) let gen_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) : C.eval_ctx = let abs_id = rg.A.id in diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 66ca8998..edc8594c 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -52,9 +52,15 @@ let ty_get_ref (ty : T.ety) : T.erased_region * T.ety * T.ref_kind = | T.Ref (r, ty, ref_kind) -> (r, ty, ref_kind) | _ -> failwith "Not a ref type" +let mk_ref_ty (r : 'r) (ty : 'r T.ty) (ref_kind : T.ref_kind) : 'r T.ty = + T.Ref (r, ty, ref_kind) + +(** Make a box type *) +let mk_box_ty (ty : 'r T.ty) : 'r T.ty = T.Adt (T.Assumed T.Box, [], [ ty ]) + (** Box a value *) let mk_box_value (v : V.typed_value) : V.typed_value = - let box_ty = T.Adt (T.Assumed T.Box, [], [ v.V.ty ]) in + let box_ty = mk_box_ty v.V.ty in let box_v = V.Adt { variant_id = None; field_values = [ v ] } in mk_typed_value box_ty box_v |