summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-07 15:04:11 +0100
committerSon Ho2022-01-07 15:04:11 +0100
commitc16ad7c78a149d3fd62976f4eb17d07a9c03b8c6 (patch)
treee7469ec9de1799bc843643643b81f180c63cd1c9
parent4e2dd5806fe41275bf8c037b9071175e51c88c62 (diff)
Factorize initialize_symbolic_context_for_fun and
eval_function_call_symbolic_from_inst_sig and make minor modifications
-rw-r--r--src/Interpreter.ml37
-rw-r--r--src/InterpreterStatements.ml87
-rw-r--r--src/Values.ml3
3 files changed, 69 insertions, 58 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index b938fe90..f38cb66e 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -69,42 +69,23 @@ module Test = struct
let input_svs =
List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
in
- (* Create the abstractions and insert them in the context *)
- let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
- ref V.AbstractionId.Map.empty
+ (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+ let empty_absl =
+ create_empty_abstractions_from_abs_region_groups
+ inst_sg.A.regions_hierarchy
in
- let create_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
- let ancestors_regions =
- List.fold_left
- (fun acc parent_id ->
- T.RegionId.Set.union acc
- (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
- regions rg.A.parents
- in
- abs_to_ancestors_regions :=
- V.AbstractionId.Map.add abs_id ancestors_regions
- !abs_to_ancestors_regions;
+ (* Add the avalues to the abstractions and insert them in the context *)
+ let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
(* Project over the values - we use *loan* projectors, as explained above *)
let avalues = List.map mk_aproj_loans_from_symbolic_value input_svs in
- (* Create the abstraction *)
- let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
+ (* Insert the avalues in the abstraction *)
+ let abs = { abs with avalues } in
(* Insert the abstraction in the context *)
let ctx = { ctx with env = Abs abs :: ctx.env } in
(* Return *)
ctx
in
- let ctx = List.fold_left create_abs ctx inst_sg.regions_hierarchy in
+ let ctx = List.fold_left insert_abs ctx empty_absl in
(* Split the variables between return var, inputs and remaining locals *)
let ret_var = List.hd fdef.locals in
let input_vars, local_vars =
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 03940bb7..917f1265 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -513,6 +513,54 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig)
(* Return *)
(ctx, inst_sig)
+(** Helper
+
+ Create abstractions (with no avalues, which have to be inserted afterwards)
+ from a list of abs region groups.
+ *)
+let create_empty_abstractions_from_abs_region_groups
+ (rgl : A.abs_region_group list) : V.abs list =
+ (* We use a reference to progressively create a map from abstraction ids
+ * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
+ * returns the union of:
+ * - the regions of the ancestors of abs_id
+ * - the regions of abs_id
+ *)
+ let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
+ ref V.AbstractionId.Map.empty
+ in
+ (* Auxiliary function to create one abstraction *)
+ let create_abs (rg : A.abs_region_group) : V.abs =
+ 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
+ let ancestors_regions =
+ List.fold_left
+ (fun acc parent_id ->
+ T.RegionId.Set.union acc
+ (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
+ T.RegionId.Set.empty rg.A.parents
+ in
+ let ancestors_regions_union_current_regions =
+ T.RegionId.Set.union ancestors_regions regions
+ in
+ abs_to_ancestors_regions :=
+ V.AbstractionId.Map.add abs_id ancestors_regions_union_current_regions
+ !abs_to_ancestors_regions;
+ (* Create the abstraction *)
+ { V.abs_id; parents; regions; ancestors_regions; avalues = [] }
+ in
+ (* Apply *)
+ List.map create_abs rgl
+
(** Evaluate a statement *)
let rec eval_statement (config : C.config) (ctx : C.eval_ctx) (st : A.statement)
: (C.eval_ctx * statement_eval_res) eval_result list =
@@ -817,49 +865,30 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
(fun ((arg, rty) : V.typed_value * T.rty) ->
arg.V.ty = Subst.erase_regions rty)
args_with_rtypes);
- (* Create the abstractions from the region groups and add them to the context *)
- let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref =
- ref V.AbstractionId.Map.empty
+ (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
+ let empty_absl =
+ create_empty_abstractions_from_abs_region_groups inst_sg.A.regions_hierarchy
in
- let create_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
- let ancestors_regions =
- List.fold_left
- (fun acc parent_id ->
- T.RegionId.Set.union acc
- (V.AbstractionId.Map.find parent_id !abs_to_ancestors_regions))
- regions rg.A.parents
- in
- abs_to_ancestors_regions :=
- V.AbstractionId.Map.add abs_id ancestors_regions !abs_to_ancestors_regions;
+ (* Add the avalues to the abstractions and insert them in the context *)
+ let insert_abs (ctx : C.eval_ctx) (abs : V.abs) : C.eval_ctx =
(* Project over the input values *)
let ctx, args_projs =
List.fold_left_map
(fun ctx (arg, arg_rty) ->
- apply_proj_borrows_on_input_value config ctx regions ancestors_regions
- arg arg_rty)
+ apply_proj_borrows_on_input_value config ctx abs.regions
+ abs.ancestors_regions arg arg_rty)
ctx args_with_rtypes
in
(* Group the input and output values *)
let avalues = List.append args_projs [ ret_av ] in
- (* Create the abstraction *)
- let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in
+ (* Add the avalues to the abstraction *)
+ let abs = { abs with avalues } in
(* Insert the abstraction in the context *)
let ctx = { ctx with env = Abs abs :: ctx.env } in
(* Return *)
ctx
in
- let ctx = List.fold_left create_abs ctx inst_sg.A.regions_hierarchy in
+ let ctx = List.fold_left insert_abs ctx empty_absl in
(* Move the return value to its destination *)
let ctx = assign_to_place config ctx ret_value dest in
(* Synthesis *)
diff --git a/src/Values.ml b/src/Values.ml
index 53851cea..bcb08dc8 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -564,7 +564,8 @@ type abs = {
parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *)
regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *)
ancestors_regions : (RegionId.set_t[@opaque]);
- (** Union of the regions owned by this abstraction and its ancestors *)
+ (** Union of the regions owned by this abstraction's ancestors (not
+ including the regions of this abstraction itself) *)
avalues : typed_avalue list; (** The values in this abstraction *)
}
[@@deriving