summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/InterpreterStatements.ml6
-rw-r--r--src/Pure.ml8
-rw-r--r--src/SymbolicAst.ml1
-rw-r--r--src/SymbolicToPure.ml192
-rw-r--r--src/SynthesizeSymbolic.ml19
-rw-r--r--src/Values.ml8
6 files changed, 182 insertions, 52 deletions
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index ef2c069d..59d2c4da 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -673,6 +673,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
V.abs =
let abs_id = rg.T.id in
let back_id = Some back_id in
+ let original_parents = rg.parents in
let parents =
List.fold_left
(fun s pid -> V.AbstractionId.Set.add pid s)
@@ -703,6 +704,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
back_id;
kind;
parents;
+ original_parents;
regions;
ancestors_regions;
avalues = [];
@@ -1060,7 +1062,9 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
let expr = cf ctx in
(* Synthesize the symbolic AST *)
- S.synthesize_regular_function_call fid call_id type_params args ret_spc expr
+ 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
in
let cc = comp cc cf_call in
diff --git a/src/Pure.ml b/src/Pure.ml
index a0c8d70c..869729a1 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -95,6 +95,7 @@ type projection = projection_elem list
type place = { var : VarId.id; projection : projection }
+(* TODO: this doesn't make sense: value can contain variables... *)
type operand = Value of typed_value | Place of place
(* type assertion = { cond : operand; expected : bool } *)
@@ -112,9 +113,12 @@ type call = { func : fun_id; type_params : ty list; args : operand list }
type left_value = unit
(** TODO: assignment left value *)
+type lvalue = typed_value
+(* TODO: define that *)
+
type let_bindings =
- | Call of var_or_dummy list * call
- (** The called function and the tuple of returned values *)
+ | Call of lvalue list * call
+ (** The called function and the tuple of returned values. *)
| Assignment of var * operand
(** Variable assignment: the introduced variable and the place we read *)
| Deconstruct of
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index 45cdc4b2..9dc20468 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -18,6 +18,7 @@ type call_id =
type call = {
call_id : call_id;
+ abstractions : V.AbstractionId.id list;
type_params : T.ety list;
args : V.typed_value list;
dest : V.symbolic_value;
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 11d7a657..97d9baf1 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -99,10 +99,14 @@ let translate_type_name (def : T.type_def) : Id.name = def.T.name
type type_context = {
types_infos : TA.type_infos;
+ cfim_type_defs : T.type_def TypeDefId.Map.t;
type_defs : type_def TypeDefId.Map.t;
}
-type fun_context = { fun_defs : fun_def FunDefId.Map.t }
+type fun_context = {
+ cfim_fun_defs : A.fun_def FunDefId.Map.t;
+ fun_defs : fun_def FunDefId.Map.t;
+}
(* TODO: do we really need that actually? *)
type synth_ctx = {
@@ -113,15 +117,57 @@ type synth_ctx = {
declarations : M.declaration_group list;
}
+type call_info = {
+ forward : S.call;
+ backwards : V.abs T.RegionGroupId.Map.t;
+ (** TODO: not sure we need this anymore *)
+}
+(** Whenever we translate a function call or an ended abstraction, we
+ store the related information (this is useful when translating ended
+ children abstractions)
+ *)
+
type bs_ctx = {
type_context : type_context;
+ fun_context : fun_context;
fun_def : A.fun_def;
bid : T.RegionGroupId.id option;
+ calls : call_info V.FunCallId.Map.t;
+ abstractions : V.abs V.AbstractionId.Map.t;
}
(** Body synthesis context *)
-let bs_ctx_lookup_type_def (id : TypeDefId.id) (ctx : bs_ctx) : type_def =
- TypeDefId.Map.find id ctx.type_context.type_defs
+(*let bs_ctx_lookup_type_def (id : TypeDefId.id) (ctx : bs_ctx) : type_def =
+ TypeDefId.Map.find id ctx.type_context.type_defs*)
+let bs_ctx_lookup_cfim_type_def (id : TypeDefId.id) (ctx : bs_ctx) : T.type_def
+ =
+ TypeDefId.Map.find id ctx.type_context.cfim_type_defs
+
+let bs_ctx_lookup_cfim_fun_def (id : FunDefId.id) (ctx : bs_ctx) : A.fun_def =
+ FunDefId.Map.find id ctx.fun_context.cfim_fun_defs
+
+let bs_ctx_register_forward_call (call_id : V.FunCallId.id) (forward : S.call)
+ (ctx : bs_ctx) : bs_ctx =
+ let calls = ctx.calls in
+ assert (not (V.FunCallId.Map.mem call_id calls));
+ let info = { forward; backwards = T.RegionGroupId.Map.empty } in
+ let calls = V.FunCallId.Map.add call_id info calls in
+ { ctx with calls }
+
+let bs_ctx_register_backward_call (abs : V.abs) (ctx : bs_ctx) : bs_ctx =
+ (* Insert the abstraction in the call informations *)
+ let back_id = Option.get abs.back_id in
+ let info = V.FunCallId.Map.find abs.call_id ctx.calls in
+ assert (not (T.RegionGroupId.Map.mem back_id info.backwards));
+ let backwards = T.RegionGroupId.Map.add back_id abs info.backwards in
+ let info = { info with backwards } in
+ let calls = V.FunCallId.Map.add abs.call_id info ctx.calls in
+ (* Insert the abstraction in the abstractions map *)
+ let abstractions = ctx.abstractions in
+ assert (not (V.AbstractionId.Map.mem abs.abs_id abstractions));
+ let abstractions = V.AbstractionId.Map.add abs.abs_id abs abstractions in
+ (* Update the context *)
+ { ctx with calls; abstractions }
let rec translate_sty (ty : T.sty) : ty =
let translate = translate_sty in
@@ -256,6 +302,8 @@ let rec translate_back_ty (ctx : bs_ctx) (keep_region : 'r -> bool)
(** Small utility: list the transitive parents of a region var group.
We don't do that in an efficient manner, but it doesn't matter.
+
+ TODO: remove?
*)
let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) :
T.RegionGroupId.Set.t =
@@ -273,7 +321,10 @@ let rec list_parent_region_groups (def : A.fun_def) (gid : T.RegionGroupId.id) :
in
parents
-(** Small utility: same as [list_parent_region_groups], but returns an ordered list *)
+(** Small utility: same as [list_parent_region_groups], but returns an ordered list.
+
+ TODO: remove?
+ *)
let list_ordered_parent_region_groups (def : A.fun_def)
(gid : T.RegionGroupId.id) : T.RegionGroupId.id list =
let pset = list_parent_region_groups def gid in
@@ -285,6 +336,30 @@ let list_ordered_parent_region_groups (def : A.fun_def)
let parents = List.map (fun (rg : T.region_var_group) -> rg.id) parents in
parents
+let list_ancestor_abstractions_ids (ctx : bs_ctx) (abs : V.abs) :
+ V.AbstractionId.id list =
+ (* We could do something more "elegant" without references, but it is
+ * so much simpler to use references... *)
+ let abs_set = ref V.AbstractionId.Set.empty in
+ let rec gather (abs_id : V.AbstractionId.id) : unit =
+ if V.AbstractionId.Set.mem abs_id !abs_set then ()
+ else (
+ abs_set := V.AbstractionId.Set.add abs_id !abs_set;
+ let abs = V.AbstractionId.Map.find abs_id ctx.abstractions in
+ List.iter gather abs.original_parents)
+ in
+ gather abs.abs_id;
+ let ids = !abs_set in
+ (* List the ancestors, in the proper order *)
+ let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+ List.filter
+ (fun id -> V.AbstractionId.Set.mem id ids)
+ call_info.forward.abstractions
+
+let list_ancestor_abstractions (ctx : bs_ctx) (abs : V.abs) : V.abs list =
+ let abs_ids = list_ancestor_abstractions_ids ctx abs in
+ List.map (fun id -> V.AbstractionId.Map.find id ctx.abstractions) abs_ids
+
let translate_fun_sig (ctx : bs_ctx) (def : A.fun_def)
(bid : T.RegionGroupId.id option) : fun_sig =
let sg = def.signature in
@@ -390,31 +465,38 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
(* TODO: move *)
-let type_def_is_enum (def : type_def) : bool =
- match def.kind with Struct _ -> false | Enum _ -> true
+let type_def_is_enum (def : T.type_def) : bool =
+ match def.kind with T.Struct _ -> false | Enum _ -> true
let typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
typed_value option =
raise Unimplemented
-let typed_avalue_to_given_back (ctx : bs_ctx) (av : V.typed_avalue) :
- typed_value option =
- raise Unimplemented
-
let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_value list =
List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
-let abs_to_given_back (ctx : bs_ctx) (abs : V.abs) : typed_value list =
- List.filter_map (typed_avalue_to_given_back ctx) abs.avalues
+let typed_avalue_to_given_back (av : V.typed_avalue) (ctx : bs_ctx) :
+ bs_ctx * lvalue option =
+ raise Unimplemented
+
+let abs_to_given_back (abs : V.abs) (ctx : bs_ctx) : bs_ctx * lvalue list =
+ let ctx, values =
+ List.fold_left_map
+ (fun ctx av -> typed_avalue_to_given_back av ctx)
+ ctx abs.avalues
+ in
+ let values = List.filter_map (fun x -> x) values in
+ (ctx, values)
(** Return the ordered list of the (transitive) parents of a given abstraction.
Is used for instance when collecting the input values given to all the
parent functions, in order to properly instantiate an
*)
-let get_abs_ordered_parents (ctx : bs_ctx) (call_id : S.call_id)
- (gid : T.RegionGroupId.id) : S.call * V.abs list =
- raise Unimplemented
+let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) : S.call * V.abs list =
+ let call_info = V.FunCallId.Map.find abs.call_id ctx.calls in
+ let abs_ancestors = list_ancestor_abstractions ctx abs in
+ (call_info.forward, abs_ancestors)
let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
match e with
@@ -422,46 +504,71 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : expression =
let v = translate_typed_value ctx v in
Return (Value v)
| Panic -> Panic
- | FunCall (call, e) ->
- (* Translate the function call *)
- let type_params = List.map (translate_fwd_ty ctx) call.type_params in
- let args = List.map (translate_typed_value ctx) call.args in
- let args = List.map (fun v -> Value v) args in
- let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
- let func =
- match call.call_id with
- | S.Fun (A.Local fid, _) -> Local (fid, None)
- | S.Fun (A.Assumed fid, _) -> Assumed fid
- | S.Unop unop -> Unop unop
- | S.Binop binop -> Binop binop
- in
- let call = { func; type_params; args } in
- (* Translate the next expression *)
- let e = translate_expression e ctx in
- (* Put together *)
- Let (Call ([ Var dest ], call), e)
- | EndAbstraction (abs, e) -> translate_end_abstraction abs e
+ | FunCall (call, e) -> translate_function_call call e ctx
+ | EndAbstraction (abs, e) -> translate_end_abstraction abs e ctx
| Expansion (sv, exp) -> translate_expansion sv exp ctx
| Meta (_, e) ->
(* We ignore the meta information *)
translate_expression e ctx
-and translate_end_abstraction (abs : V.abs) (e : S.expression) : expression =
+and translate_function_call (call : S.call) (e : S.expression) (ctx : bs_ctx) :
+ expression =
+ (* Translate the function call *)
+ let type_params = List.map (translate_fwd_ty ctx) call.type_params in
+ let args = List.map (translate_typed_value ctx) call.args in
+ let args = List.map (fun v -> Value v) args in
+ let ctx, dest = fresh_var_for_symbolic_value call.dest ctx in
+ (* Retrieve the function id, and register the function call in the context
+ * if necessary *)
+ let ctx, func =
+ match call.call_id with
+ | S.Fun (fid, call_id) ->
+ let ctx = bs_ctx_register_forward_call call_id call ctx in
+ let func =
+ match fid with
+ | A.Local fid -> Local (fid, None)
+ | A.Assumed fid -> Assumed fid
+ in
+ (ctx, func)
+ | S.Unop unop -> (ctx, Unop unop)
+ | S.Binop binop -> (ctx, Binop binop)
+ in
+ let call = { func; type_params; args } in
+ (* Translate the next expression *)
+ let e = translate_expression e ctx in
+ (* Put together *)
+ Let (Call ([ Var dest ], call), e)
+
+and translate_end_abstraction (abs : V.abs) (e : S.expression) (ctx : bs_ctx) :
+ expression =
match abs.kind with
| V.SynthInput ->
(* There are no nested borrows for now: we shouldn't get there *)
raise Unimplemented
| V.FunCall ->
(* Retrive the orignal call and the parent abstractions *)
+ let forward, backwards = get_abs_ancestors ctx abs in
(* Retrieve the values consumed when we called the forward function and
* ended the parent backward functions: those give us part of the input
* values *)
+ let fwd_inputs = List.map (translate_typed_value ctx) forward.args in
+ let back_ancestors_inputs =
+ List.concat (List.map abs_to_consumed backwards)
+ in
(* Retrieve the values consumed upon ending the loans inside this
* abstraction: those give us the remaining input values *)
+ let back_inputs = abs_to_consumed abs in
+ let inputs =
+ List.concat [ fwd_inputs; back_ancestors_inputs; back_inputs ]
+ in
(* Retrieve the values given back by this function: those are the output
* values *)
+ let ctx, outputs = abs_to_given_back abs ctx in
+ (* Translate the next expression *)
+ let e = translate_expression e ctx in
(* Put everything together *)
- raise Unimplemented
+ let call = { func; type_params; args = inputs } in
+ Let (Call (outputs, call), e)
| V.SynthRet ->
(* *)
raise Unimplemented
@@ -499,7 +606,7 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
match type_id with
| T.AdtId adt_id ->
(* Detect if this is an enumeration or not *)
- let tdef = bs_ctx_lookup_type_def adt_id ctx in
+ let tdef = bs_ctx_lookup_cfim_type_def adt_id ctx in
let is_enum = type_def_is_enum tdef in
if is_enum then
(* This is an enumeration: introduce an [ExpandEnum] let-binding *)
@@ -568,9 +675,14 @@ and translate_expansion (sv : V.symbolic_value) (exp : S.expansion)
let otherwise = translate_expression otherwise ctx in
Switch (scrutinee, SwitchInt (int_ty, branches, otherwise))
-let translate_fun_def (type_context : type_context) (def : A.fun_def)
- (bid : T.RegionGroupId.id option) (body : S.expression) : fun_def =
- let bs_ctx = { type_context; fun_def = def; bid } in
+let translate_fun_def (type_context : type_context) (fun_context : fun_context)
+ (def : A.fun_def) (bid : T.RegionGroupId.id option) (body : S.expression) :
+ fun_def =
+ let calls = V.FunCallId.Map.empty in
+ let abstractions = V.AbstractionId.Map.empty in
+ let bs_ctx =
+ { type_context; fun_context; fun_def = def; bid; calls; abstractions }
+ in
(* Translate the function *)
let def_id = def.A.def_id in
let name = translate_fun_name def bid in
diff --git a/src/SynthesizeSymbolic.ml b/src/SynthesizeSymbolic.ml
index c0d4489c..d578a13e 100644
--- a/src/SynthesizeSymbolic.ml
+++ b/src/SynthesizeSymbolic.ml
@@ -81,29 +81,32 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
synthesize_symbolic_expansion sv [ Some see ] exprl
-let synthesize_function_call (call_id : call_id) (type_params : T.ety list)
+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)
(expr : expression option) : expression option =
match expr with
| None -> None
| Some expr ->
- let call = { call_id; type_params; args; dest } in
+ let call = { call_id; abstractions; type_params; args; dest } in
Some (FunCall (call, expr))
let synthesize_regular_function_call (fun_id : A.fun_id)
- (call_id : V.FunCallId.id) (type_params : T.ety list)
- (args : V.typed_value list) (dest : V.symbolic_value)
- (expr : expression option) : expression option =
- synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr
+ (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 =
+ synthesize_function_call
+ (Fun (fun_id, call_id))
+ abstractions type_params args dest 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
+ synthesize_function_call (Unop unop) [] [] [ arg ] dest 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
+ synthesize_function_call (Binop binop) [] [] [ arg0; arg1 ] dest expr
let synthesize_aggregated_value (aggr_v : V.typed_value)
(expr : expression option) : expression option =
diff --git a/src/Values.ml b/src/Values.ml
index cc458bca..6378269f 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -737,12 +737,18 @@ type abs = {
symbolic AST, generated by the symbolic execution.
*)
back_id : (RegionGroupId.id option[@opaque]);
- (** The id of the backward function to which this abstraction is linked.
+ (** The id of the backward function to which this abstraction is linked,
+ if there is one. Note that it may not be the case, when introducing
+ abstractions to handle the input values for the function we are
+ synthesizing for instance. TODO: actually should never be None.
+
This is not used by the symbolic execution: it is a utility for
the symbolic AST, generated by the symbolic execution.
*)
kind : (abs_kind[@opaque]);
parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *)
+ original_parents : (AbstractionId.id list[@opaque]);
+ (** The original list of parents, ordered. This is used for synthesis. *)
regions : (RegionId.Set.t[@opaque]); (** Regions owned by this abstraction *)
ancestors_regions : (RegionId.Set.t[@opaque]);
(** Union of the regions owned by this abstraction's ancestors (not
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 00:47:23 +0000