summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Interpreter.ml59
-rw-r--r--src/Synthesis.ml3
-rw-r--r--src/Values.ml3
3 files changed, 50 insertions, 15 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index ed5c52d3..2192c491 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -442,6 +442,11 @@ let symbolic_expansion_non_borrow_to_value (sv : V.symbolic_value)
in
{ V.value; V.ty }
+let apply_proj_borrows_in_context (check_symbolic_no_ended : bool)
+ (ctx : C.eval_ctx) (regions : T.RegionId.set_t) (v : V.typed_value)
+ (ty : T.rty) : C.eval_ctx * V.typed_avalue =
+ raise Unimplemented
+
(** Convert a symbolic expansion to a value.
If the expansion is a mutable reference expansion, it converts it to a borrow.
@@ -4201,23 +4206,55 @@ and eval_local_function_call_symbolic (config : C.config) (ctx : C.eval_ctx)
let inst_sg = Subst.substitute_signature asubst rsubst tsubst sg in
(* Generate a fresh symbolic value for the result *)
let res_sv_ty = inst_sg.A.output in
- let ctx, res_sv =
+ let ctx, res_spc =
mk_fresh_symbolic_proj_comp T.RegionId.Set.empty res_sv_ty ctx
in
- (* Generate the abstractions from the region groups *)
- let generate_abs (ctx : C.eval_ctx) (rg : A.abs_region_group) :
- C.eval_ctx * V.abs =
- raise Unimplemented
+ let res_value = mk_typed_value_from_proj_comp res_spc in
+ let res_av = V.ASymbolic (V.AProjLoans res_spc.V.svalue) in
+ let res_av : V.typed_avalue =
+ { V.value = res_av; V.ty = res_spc.V.svalue.V.sv_ty }
in
- let ctx, abs =
- List.fold_left_map generate_abs ctx inst_sg.A.regions_hierarchy
+ (* Evaluate the input operands *)
+ let ctx, args = eval_operands config ctx args in
+ assert (List.length args = def.A.arg_count);
+ let args_with_rtypes = List.combine args rtype_params in
+ (* 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
+ let parents =
+ List.fold_left
+ (fun s pid -> V.AbstractionId.Set.add pid s)
+ V.AbstractionId.Set.empty rg.A.parents
+ in
+ let regions =
+ List.fold_left
+ (fun s rid -> T.RegionId.Set.add rid s)
+ T.RegionId.Set.empty rg.A.regions
+ in
+ (* Project over the input values *)
+ let check_symbolic_no_ended = true in
+ let ctx, args_projs =
+ List.fold_left_map
+ (fun ctx (arg, arg_rty) ->
+ apply_proj_borrows_in_context check_symbolic_no_ended ctx regions arg
+ arg_rty)
+ ctx args_with_rtypes
+ in
+ (* Group the input and output values *)
+ let avalues = List.append args_projs [ res_av ] in
+ (* Create the abstraction *)
+ let abs = { V.abs_id; parents; regions; avalues } in
+ (* Insert the abstraction in the context *)
+ let ctx = { ctx with env = Abs abs :: ctx.env } in
+ (* Return *)
+ ctx
in
- (* Add the abstractions to the context *)
- let abs = List.rev (List.map (fun abs -> C.Abs abs) abs) in
- let ctx = { ctx with C.env = List.append abs ctx.C.env } in
+ let ctx = List.fold_left gen_abs ctx inst_sg.A.regions_hierarchy in
+ (* Move the return value to its destination *)
+ let ctx = assign_to_place config ctx res_value dest in
(* Synthesis *)
S.synthesize_local_function_call fid region_params type_params args dest
- res_sv.V.svalue;
+ res_spc.V.svalue;
(* Return *)
ctx
diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index f317a5f9..60c387d2 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -70,5 +70,6 @@ let synthesize_non_local_function_call (fid : A.assumed_fun_id)
let synthesize_local_function_call (fid : A.FunDefId.id)
(region_params : T.erased_region list) (type_params : T.ety list)
- (args : E.operand list) (dest : E.place) (res : V.symbolic_value) : unit =
+ (args : V.typed_value list) (dest : E.place) (res : V.symbolic_value) : unit
+ =
()
diff --git a/src/Values.ml b/src/Values.ml
index 001c0347..ae9eb127 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -542,9 +542,6 @@ and typed_avalue = { value : avalue; ty : rty }
type abs = {
abs_id : (AbstractionId.id[@opaque]);
parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *)
- acc_regions : (RegionId.set_t[@opaque]);
- (** Union of the regions owned by the (transitive) parent abstractions and
- by the current abstraction. TODO: why do we need those? *)
regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *)
avalues : typed_avalue list; (** The values in this abstraction *)
}