summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-05 19:52:07 +0100
committerSon Ho2022-01-05 19:52:07 +0100
commitde4a2300b734e9ea9c29a160a968110507d7747f (patch)
tree121cd2633d91bc522bdf8dc0385730d00ec4a914
parent6b9653a3f1a361c72eb841a5a9c04a374b99c8e5 (diff)
Make progress on eval_non_local_function_call_symbolic
-rw-r--r--src/Interpreter.ml138
-rw-r--r--src/InterpreterUtils.ml8
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