From 8917bf6aca4465873e7e7642719c70789d97590c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 12:39:58 +0100 Subject: Add an optional borrow identifier to AIgnoredMutBorrow, introduce the AEndedIgnoredMutBorrow variant and fix a couple of bugs --- src/Interpreter.ml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 2789517e..9ac8149b 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -67,6 +67,9 @@ module Test = struct 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 + 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 = @@ -79,10 +82,20 @@ module Test = struct (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; (* 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; avalues } in + let abs = { V.abs_id; parents; regions; ancestors_regions; avalues } in (* Insert the abstraction in the context *) let ctx = { ctx with env = Abs abs :: ctx.env } in (* Return *) -- cgit v1.2.3 From 2ee5357216cc5a620dbe6d091b0081d419951a4e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 13:55:16 +0100 Subject: Make more modifications to logging --- src/Interpreter.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'src/Interpreter.ml') diff --git a/src/Interpreter.ml b/src/Interpreter.ml index 9ac8149b..b938fe90 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -21,6 +21,9 @@ open InterpreterStatements (* TODO: remove the config parameters when they are useless *) +(** The local logger *) +let log = L.interpreter_log + module Test = struct let initialize_context (type_context : C.type_context) (fun_defs : A.fun_def list) (type_vars : T.type_var list) : C.eval_ctx = @@ -126,7 +129,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_unit_function: " ^ Print.Types.name_to_string fdef.A.name)); (* Sanity check - *) @@ -177,7 +180,7 @@ module Test = struct let fdef = A.FunDefId.nth fun_defs fid in (* Debug *) - L.log#ldebug + log#ldebug (lazy ("test_function_symbolic: " ^ Print.Types.name_to_string fdef.A.name)); -- cgit v1.2.3 From c16ad7c78a149d3fd62976f4eb17d07a9c03b8c6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 7 Jan 2022 15:04:11 +0100 Subject: Factorize initialize_symbolic_context_for_fun and eval_function_call_symbolic_from_inst_sig and make minor modifications --- src/Interpreter.ml | 37 +++++++++---------------------------- 1 file changed, 9 insertions(+), 28 deletions(-) (limited to 'src/Interpreter.ml') 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 = -- cgit v1.2.3