summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/InterpreterExpansion.ml57
-rw-r--r--src/InterpreterExpressions.ml21
-rw-r--r--src/InterpreterPaths.ml3
-rw-r--r--src/InterpreterStatements.ml27
-rw-r--r--src/PrintPure.ml4
-rw-r--r--src/SymbolicAst.ml35
-rw-r--r--src/SynthesizeSymbolic.ml61
7 files changed, 150 insertions, 58 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 2dd36535..77bf0bd8 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -12,6 +12,7 @@ module L = Logging
open TypesUtils
module Inv = Invariants
module S = SynthesizeSymbolic
+module SA = SymbolicAst
open Cps
open ValuesUtils
open InterpreterUtils
@@ -264,7 +265,8 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
see
let expand_symbolic_value_shared_borrow (config : C.config)
- (original_sv : V.symbolic_value) (ref_ty : T.rty) : cm_fun =
+ (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+ (ref_ty : T.rty) : cm_fun =
fun cf ctx ->
(* First, replace the projectors on borrows.
* The important point is that the symbolic value to expand may appear
@@ -374,12 +376,14 @@ let expand_symbolic_value_shared_borrow (config : C.config)
(* Call the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv see expr
+ S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place see
+ expr
(** TODO: simplify and merge with the other expansion function *)
let expand_symbolic_value_borrow (config : C.config)
- (original_sv : V.symbolic_value) (region : T.RegionId.id T.region)
- (ref_ty : T.rty) (rkind : T.ref_kind) : cm_fun =
+ (original_sv : V.symbolic_value) (original_sv_place : SA.place option)
+ (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind) :
+ cm_fun =
fun cf ctx ->
(* Check that we are allowed to expand the reference *)
assert (not (region_in_set region ctx.ended_regions));
@@ -407,9 +411,11 @@ let expand_symbolic_value_borrow (config : C.config)
(* Apply the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv see expr
+ S.synthesize_symbolic_expansion_no_branching original_sv original_sv_place
+ see expr
| T.Shared ->
- expand_symbolic_value_shared_borrow config original_sv ref_ty cf ctx
+ expand_symbolic_value_shared_borrow config original_sv original_sv_place
+ ref_ty cf ctx
(** A small helper.
@@ -420,7 +426,7 @@ let expand_symbolic_value_borrow (config : C.config)
[see_cf_l]: list of pairs (optional symbolic expansion, continuation)
*)
let apply_branching_symbolic_expansions_non_borrow (config : C.config)
- (sv : V.symbolic_value)
+ (sv : V.symbolic_value) (sv_place : SA.place option)
(see_cf_l : (V.symbolic_expansion option * m_fun) list) : m_fun =
fun ctx ->
assert (see_cf_l <> []);
@@ -450,7 +456,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
in
(* Synthesize and return *)
let seel = List.map fst see_cf_l in
- S.synthesize_symbolic_expansion sv seel subterms
+ S.synthesize_symbolic_expansion sv sv_place seel subterms
(** Expand a symbolic value which is not an enumeration with several variants
(i.e., in a situation where it doesn't lead to branching).
@@ -461,7 +467,7 @@ let apply_branching_symbolic_expansions_non_borrow (config : C.config)
TODO: rename [sp] to [sv]
*)
let expand_symbolic_value (config : C.config) (allow_branching : bool)
- (sp : V.symbolic_value) : cm_fun =
+ (sp : V.symbolic_value) (sp_place : SA.place option) : cm_fun =
fun cf ctx ->
(* Debug *)
log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sp));
@@ -470,6 +476,7 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Compute the expanded value - note that when doing so, we may introduce
* fresh symbolic values in the context (which thus gets updated) *)
let original_sv = sp in
+ let original_sv_place = sp_place in
let rty = original_sv.V.sv_ty in
let cc : cm_fun =
fun cf ctx ->
@@ -485,8 +492,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
assert (List.length seel <= 1 || allow_branching);
(* Apply *)
let seel = List.map (fun see -> (Some see, cf)) seel in
- apply_branching_symbolic_expansions_non_borrow config original_sv seel
- ctx
+ apply_branching_symbolic_expansions_non_borrow config original_sv
+ original_sv_place seel ctx
(* Tuples *)
| T.Adt (T.Tuple, [], tys) ->
(* Generate the field values *)
@@ -498,7 +505,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Call the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv see expr
+ S.synthesize_symbolic_expansion_no_branching original_sv
+ original_sv_place see expr
(* Boxes *)
| T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
@@ -509,11 +517,12 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
(* Call the continuation *)
let expr = cf ctx in
(* Update the synthesized program *)
- S.synthesize_symbolic_expansion_no_branching original_sv see expr
+ S.synthesize_symbolic_expansion_no_branching original_sv
+ original_sv_place see expr
(* Borrows *)
| T.Ref (region, ref_ty, rkind) ->
- expand_symbolic_value_borrow config original_sv region ref_ty rkind cf
- ctx
+ expand_symbolic_value_borrow config original_sv original_sv_place region
+ ref_ty rkind cf ctx
(* Booleans *)
| T.Bool ->
assert allow_branching;
@@ -523,8 +532,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
let seel = [ see_true; see_false ] in
let seel = List.map (fun see -> (Some see, cf)) seel in
(* Apply the symbolic expansion (this also outputs the updated symbolic AST) *)
- apply_branching_symbolic_expansions_non_borrow config original_sv seel
- ctx
+ apply_branching_symbolic_expansions_non_borrow config original_sv
+ original_sv_place seel ctx
| _ -> failwith ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty)
in
(* Debug *)
@@ -569,8 +578,8 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
switch. The continuation is thus for the execution *after* the switch.
*)
let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
- (int_type : T.integer_type) (tgts : (V.scalar_value * m_fun) list)
- (otherwise : m_fun) : m_fun =
+ (sv_place : SA.place option) (int_type : T.integer_type)
+ (tgts : (V.scalar_value * m_fun) list) (otherwise : m_fun) : m_fun =
(* Sanity check *)
assert (sv.V.sv_ty = T.Integer int_type);
(* For all the branches of the switch, we expand the symbolic value
@@ -587,13 +596,13 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
in
let tgts = List.append tgts [ (None, otherwise) ] in
(* Then expand and evaluate - this generates the proper symbolic AST *)
- apply_branching_symbolic_expansions_non_borrow config sv tgts
+ apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts
(** See [expand_symbolic_value] *)
let expand_symbolic_value_no_branching (config : C.config)
- (sp : V.symbolic_value) : cm_fun =
+ (sv : V.symbolic_value) (sv_place : SA.place option) : cm_fun =
let allow_branching = false in
- expand_symbolic_value config allow_branching sp
+ expand_symbolic_value config allow_branching sv sv_place
(** Expand all the symbolic values which contain borrows.
Allows us to restrict ourselves to a simpler model for the projectors over
@@ -649,10 +658,10 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
("Attempted to greedily expand a recursive definition (option \
[greedy_expand_symbolics_with_borrows] of [config]): "
^ Print.name_to_string def.name)
- else expand_symbolic_value_no_branching config sv
+ else expand_symbolic_value_no_branching config sv None
| T.Adt ((Tuple | Assumed Box), _, _) | T.Ref (_, _, _) ->
(* Ok *)
- expand_symbolic_value_no_branching config sv
+ expand_symbolic_value_no_branching config sv None
| T.Array _ -> raise Errors.Unimplemented
| T.Slice _ -> failwith "Can't expand symbolic slices"
| T.TypeVar _ | Bool | Char | Never | Integer _ | Str ->
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 84f51c94..356bae2d 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -39,7 +39,9 @@ let expand_primitively_copyable_at_place (config : C.config)
with
| None -> cf ctx
| Some sv ->
- let cc = expand_symbolic_value_no_branching config sv in
+ let cc =
+ expand_symbolic_value_no_branching config sv (Some (S.mk_place p ctx))
+ in
comp cc expand cf ctx
in
(* Apply *)
@@ -290,7 +292,9 @@ let eval_unary_op_symbolic (config : C.config) (unop : E.unop) (op : E.operand)
(* Call the continuation *)
let expr = cf (Ok (mk_typed_value_from_symbolic_value res_sv)) ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_unary_op unop v res_sv expr
+ S.synthesize_unary_op unop v
+ (S.mk_opt_place_from_op op ctx)
+ res_sv None expr
in
(* Compose and apply *)
comp eval_op apply cf ctx
@@ -427,7 +431,9 @@ let eval_binary_op_symbolic (config : C.config) (binop : E.binop)
let v = mk_typed_value_from_symbolic_value res_sv in
let expr = cf (Ok v) ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_binary_op binop v1 v2 res_sv expr
+ let p1 = S.mk_opt_place_from_op op1 ctx in
+ let p2 = S.mk_opt_place_from_op op2 ctx in
+ S.synthesize_binary_op binop v1 p1 v2 p2 res_sv None expr
in
(* Compose and apply *)
comp eval_ops compute cf ctx
@@ -488,7 +494,10 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
| Symbolic sv ->
(* Expand the symbolic value - may lead to branching *)
let allow_branching = true in
- let cc = expand_symbolic_value config allow_branching sv in
+ let cc =
+ expand_symbolic_value config allow_branching sv
+ (Some (S.mk_place p ctx))
+ in
(* This time the value is concrete: reevaluate *)
comp cc (eval_rvalue_discriminant_concrete config p) cf ctx
| _ -> failwith "Invalid input for `discriminant`"
@@ -584,7 +593,7 @@ let eval_rvalue_aggregate (config : C.config)
(* Call the continuation *)
let expr = cf aggregated ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_aggregated_value aggregated expr
+ S.synthesize_aggregated_value aggregated None expr
| E.AggregatedAdt (def_id, opt_variant_id, regions, types) ->
(* Sanity checks *)
let type_def = C.ctx_lookup_type_def ctx def_id in
@@ -605,7 +614,7 @@ let eval_rvalue_aggregate (config : C.config)
(* Call the continuation *)
let expr = cf aggregated ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_aggregated_value aggregated expr
+ S.synthesize_aggregated_value aggregated None expr
in
(* Compose and apply *)
comp eval_ops compute cf
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 300e50c5..8b103eb8 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -11,6 +11,7 @@ open InterpreterUtils
open InterpreterBorrowsCore
open InterpreterBorrows
open InterpreterExpansion
+module Synth = SynthesizeSymbolic
(** The local logger *)
let log = L.paths_log
@@ -473,6 +474,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
| FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
expand_symbolic_value_no_branching config sp
+ (Some (Synth.mk_place p ctx))
| FailBottom (_, _, _) ->
(* We can't expand [Bottom] values while reading them *)
failwith "Found [Bottom] while reading a place"
@@ -502,6 +504,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
| FailSymbolic (_pe, sp) ->
(* Expand the symbolic value *)
expand_symbolic_value_no_branching config sp
+ (Some (Synth.mk_place p ctx))
| FailBottom (remaining_pes, pe, ty) ->
(* Expand the [Bottom] value *)
fun cf ctx ->
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index b0d4e5e0..16c66094 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -155,7 +155,10 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
(* Expand the symbolic value, then call the evaluation function for the
* non-symbolic case *)
let allow_branching = true in
- let expand = expand_symbolic_value config allow_branching sv in
+ let expand =
+ expand_symbolic_value config allow_branching sv
+ (S.mk_opt_place_from_op assertion.cond ctx)
+ in
comp expand (eval_assertion_concrete config assertion) cf ctx
| _ -> failwith ("Expected a boolean, got: " ^ typed_value_to_string ctx v)
in
@@ -804,6 +807,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
(** Evaluate a switch *)
and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
st_cm_fun =
+ fun cf ctx ->
(* We evaluate the operand in two steps:
* first we prepare it, then we check if its value is concrete or
* symbolic. If it is concrete, we can then evaluate the operand
@@ -816,6 +820,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
let cf_prepare_op cf : m_fun = eval_operand_prepare config op cf in
(* Match on the targets *)
let cf_match (cf : st_m_fun) (op_v : V.typed_value) : m_fun =
+ fun ctx ->
match tgts with
| A.If (st1, st2) -> (
match op_v.value with
@@ -830,17 +835,19 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
else eval_statement config st2 cf
in
(* Compose the continuations *)
- comp cf_eval_op cf_branch cf
+ comp cf_eval_op cf_branch cf ctx
| V.Symbolic sv ->
(* Expand the symbolic value *)
let allows_branching = true in
let cf_expand cf =
- expand_symbolic_value config allows_branching sv cf
+ expand_symbolic_value config allows_branching sv
+ (S.mk_opt_place_from_op op ctx)
+ cf
in
(* Retry *)
let cf_eval_if cf = eval_switch config op tgts cf in
(* Compose *)
- comp cf_expand cf_eval_if cf
+ comp cf_expand cf_eval_if cf ctx
| _ -> failwith "Inconsistent state")
| A.SwitchInt (int_ty, stgts, otherwise) -> (
match op_v.value with
@@ -858,7 +865,7 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
| Some (_, tgt) -> eval_statement config tgt cf
in
(* Compose *)
- comp cf_eval_op cf_eval_branch cf
+ comp cf_eval_op cf_eval_branch cf ctx
| V.Symbolic sv ->
(* Expand the symbolic value - note that contrary to the boolean
* case, we can't expand then retry, because when switching over
@@ -871,11 +878,13 @@ and eval_switch (config : C.config) (op : E.operand) (tgts : A.switch_targets) :
stgts
in
let otherwise = eval_statement config otherwise cf in
- expand_symbolic_int config sv int_ty stgts otherwise
+ expand_symbolic_int config sv
+ (S.mk_opt_place_from_op op ctx)
+ int_ty stgts otherwise ctx
| _ -> failwith "Inconsistent state")
in
(* Compose the continuations *)
- comp cf_prepare_op cf_match
+ comp cf_prepare_op cf_match cf ctx
(** Evaluate a function call (auxiliary helper for [eval_statement]) *)
and eval_function_call (config : C.config) (call : A.call) : st_cm_fun =
@@ -992,6 +1001,8 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
let ret_av regions =
mk_aproj_loans_value_from_symbolic_value regions ret_spc
in
+ let args_places = List.map (fun p -> S.mk_opt_place_from_op p ctx) args in
+ let dest_place = Some (S.mk_place dest ctx) in
(* Evaluate the input operands *)
let cc = eval_operands config args in
@@ -1047,7 +1058,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(* Synthesize the symbolic AST *)
let abs_ids = List.map (fun rg -> rg.T.id) inst_sg.regions_hierarchy in
S.synthesize_regular_function_call fid call_id abs_ids type_params args
- ret_spc expr
+ args_places ret_spc dest_place expr
in
let cc = comp cc cf_call in
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 3d41e67d..b631f940 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -183,7 +183,7 @@ let type_def_to_string (fmt : type_formatter) (def : type_def) : string =
"enum " ^ name ^ params ^ " =\n" ^ variants
let var_to_string (fmt : type_formatter) (v : var) : string =
- "(" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")"
+ "(@" ^ VarId.to_string v.id ^ " : " ^ ty_to_string fmt v.ty ^ ")"
let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string =
match v with
@@ -218,7 +218,7 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
"(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name))
let place_to_string (fmt : ast_formatter) (p : place) : string =
- let var = fmt.var_id_to_string p.var in
+ let var = "@" ^ fmt.var_id_to_string p.var in
projection_to_string fmt var p.projection
let rec typed_rvalue_to_string (fmt : ast_formatter) (v : typed_rvalue) : string
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index f0873aa3..a3aedeab 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -9,6 +9,25 @@ module V = Values
module E = Expressions
module A = CfimAst
+type place = {
+ bv : Contexts.binder;
+ (** It is important that we store the binder, and not just the variable id,
+ because the most important information in a place is the name of the
+ variable!
+ *)
+ projection : E.projection;
+ (** We store the projection because we can, but it is actually not that useful *)
+}
+(** In this module, [place] is meta information.
+
+ Whenever we need to introduce new symbolic variables, for instance because
+ of symbolic expansions, we try to store a "place", which gives information
+ about the origin of the values (this place information comes from assignment
+ information, etc.).
+ We later use this place information to generate meaningful name, to prettify
+ the generated code.
+ *)
+
type call_id =
| Fun of A.fun_id * V.FunCallId.id
(** A "regular" function (i.e., a function which is not a primitive operation) *)
@@ -21,7 +40,9 @@ type call = {
abstractions : V.AbstractionId.id list;
type_params : T.ety list;
args : V.typed_value list;
+ args_places : place option list; (** Meta information *)
dest : V.symbolic_value;
+ dest_place : place option; (** Meta information *)
}
(** **Rk.:** here, [expression] is not at all equivalent to the expressions
@@ -37,7 +58,15 @@ type expression =
| Panic
| FunCall of call * expression
| EndAbstraction of V.abs * expression
- | Expansion of V.symbolic_value * expansion
+ | Expansion of place option * V.symbolic_value * expansion
+ (** Expansion of a symbolic value.
+
+ The place is "meta": it gives the path to the symbolic value (if available)
+ which got expanded (this path is available when the symbolic expansion
+ comes from a path evaluation, during an assignment for instance).
+ We use it to compute meaningful names for the variables we introduce,
+ to prettify the generated code.
+ *)
| Meta of meta * expression (** Meta information *)
and expansion =
@@ -63,4 +92,6 @@ and expansion =
generate a pretty output.
*)
-and meta = Aggregate of V.typed_value (** We generated an aggregate value *)
+and meta =
+ | Aggregate of place option * V.typed_value
+ (** We generated an aggregate value *)
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index 6aec95bd..7050c14b 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -5,7 +5,20 @@ module E = Expressions
module A = CfimAst
open SymbolicAst
-let synthesize_symbolic_expansion (sv : V.symbolic_value)
+let mk_place (p : E.place) (ctx : Contexts.eval_ctx) : place =
+ let bv = Contexts.ctx_lookup_binder ctx p.var_id in
+ { bv; projection = p.projection }
+
+let mk_opt_place (p : E.place option) (ctx : Contexts.eval_ctx) : place option =
+ match p with None -> None | Some p -> Some (mk_place p ctx)
+
+let mk_opt_place_from_op (op : E.operand) (ctx : Contexts.eval_ctx) :
+ place option =
+ match op with
+ | E.Copy p | E.Move p -> Some (mk_place p ctx)
+ | E.Constant _ -> None
+
+let synthesize_symbolic_expansion (sv : V.symbolic_value) (place : place option)
(seel : V.symbolic_expansion option list) (exprl : expression list option) :
expression option =
match exprl with
@@ -71,46 +84,62 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
| T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
failwith "Ill-formed symbolic expansion"
in
- Some (Expansion (sv, expansion))
+ Some (Expansion (place, sv, expansion))
let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
- (see : V.symbolic_expansion) (expr : expression option) : expression option
- =
+ (place : place option) (see : V.symbolic_expansion)
+ (expr : expression option) : expression option =
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
- synthesize_symbolic_expansion sv [ Some see ] exprl
+ synthesize_symbolic_expansion sv place [ Some see ] exprl
let synthesize_function_call (call_id : call_id)
(abstractions : V.AbstractionId.id list) (type_params : T.ety list)
- (args : V.typed_value list) (dest : V.symbolic_value)
+ (args : V.typed_value list) (args_places : place option list)
+ (dest : V.symbolic_value) (dest_place : place option)
(expr : expression option) : expression option =
match expr with
| None -> None
| Some expr ->
- let call = { call_id; abstractions; type_params; args; dest } in
+ let call =
+ {
+ call_id;
+ abstractions;
+ type_params;
+ args;
+ dest;
+ args_places;
+ dest_place;
+ }
+ in
Some (FunCall (call, expr))
let synthesize_regular_function_call (fun_id : A.fun_id)
(call_id : V.FunCallId.id) (abstractions : V.AbstractionId.id list)
(type_params : T.ety list) (args : V.typed_value list)
- (dest : V.symbolic_value) (expr : expression option) : expression option =
+ (args_places : place option list) (dest : V.symbolic_value)
+ (dest_place : place option) (expr : expression option) : expression option =
synthesize_function_call
(Fun (fun_id, call_id))
- abstractions type_params args dest expr
+ abstractions type_params args args_places dest dest_place expr
let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
- (dest : V.symbolic_value) (expr : expression option) : expression option =
- synthesize_function_call (Unop unop) [] [] [ arg ] dest expr
+ (arg_place : place option) (dest : V.symbolic_value)
+ (dest_place : place option) (expr : expression option) : expression option =
+ synthesize_function_call (Unop unop) [] [] [ arg ] [ arg_place ] dest
+ dest_place expr
let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
- (arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
- : expression option =
- synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr
+ (arg0_place : place option) (arg1 : V.typed_value)
+ (arg1_place : place option) (dest : V.symbolic_value)
+ (dest_place : place option) (expr : expression option) : expression option =
+ synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ]
+ [ arg0_place; arg1_place ] dest dest_place expr
-let synthesize_aggregated_value (aggr_v : V.typed_value)
+let synthesize_aggregated_value (aggr_v : V.typed_value) (place : place option)
(expr : expression option) : expression option =
match expr with
| None -> None
- | Some expr -> Some (Meta (Aggregate aggr_v, expr))
+ | Some expr -> Some (Meta (Aggregate (place, aggr_v), expr))
let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
expression option =