diff options
| -rw-r--r-- | src/CfimAst.ml | 19 | ||||
| -rw-r--r-- | src/CfimOfJson.ml | 17 | ||||
| -rw-r--r-- | tests/trace_reference.txt | 2 |
3 files changed, 37 insertions, 1 deletions
diff --git a/src/CfimAst.ml b/src/CfimAst.ml index 250cd223..28f23758 100644 --- a/src/CfimAst.ml +++ b/src/CfimAst.ml @@ -5,6 +5,8 @@ open Expressions module FunDefId = IdGen () +module RegionGroupId = IdGen () + type var = { index : VarId.id; (** Unique variable identifier *) name : string option; @@ -24,9 +26,26 @@ type fun_id = Local of FunDefId.id | Assumed of assumed_fun_id type assertion = { cond : operand; expected : bool } [@@deriving show] +type region_group = { + id : RegionGroupId.id; + regions : RegionVarId.id list; + parents : RegionGroupId.id list; +} +[@@deriving show] +(** A group of regions. + + Results from a lifetime analysis: we group the regions with the same + lifetime together, and compute the hierarchy between the regions. + This is necessary to introduce the proper abstraction with the + proper constraints, when evaluating a function call in symbolic mode. +*) + +type region_groups = region_group list [@@deriving show] + type fun_sig = { region_params : region_var list; num_early_bound_regions : int; + regions_hierarchy : region_groups; type_params : type_var list; inputs : sty list; output : sty; diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml index 3494f004..4f39d7ff 100644 --- a/src/CfimOfJson.ml +++ b/src/CfimOfJson.ml @@ -436,6 +436,20 @@ let assertion_of_json (js : json) : (A.assertion, string) result = Ok { A.cond; expected } | _ -> Error "") +let region_group_of_json (js : json) : (A.region_group, string) result = + combine_error_msgs js "region_group_of_json" + (match js with + | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] -> + let* id = A.RegionGroupId.id_of_json id in + let* regions = list_of_json T.RegionVarId.id_of_json regions in + let* parents = list_of_json A.RegionGroupId.id_of_json parents in + Ok { A.id; regions; parents } + | _ -> Error "") + +let region_groups_of_json (js : json) : (A.region_groups, string) result = + combine_error_msgs js "region_group_of_json" + (list_of_json region_group_of_json js) + let fun_sig_of_json (js : json) : (A.fun_sig, string) result = combine_error_msgs js "fun_sig_of_json" (match js with @@ -443,12 +457,14 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result = [ ("region_params", region_params); ("num_early_bound_regions", num_early_bound_regions); + ("regions_hierarchy", regions_hierarchy); ("type_params", type_params); ("inputs", inputs); ("output", output); ] -> let* region_params = list_of_json region_var_of_json region_params in let* num_early_bound_regions = int_of_json num_early_bound_regions in + let* regions_hierarchy = region_groups_of_json regions_hierarchy in let* type_params = list_of_json type_var_of_json type_params in let* inputs = list_of_json sty_of_json inputs in let* output = sty_of_json output in @@ -456,6 +472,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result = { A.region_params; num_early_bound_regions; + regions_hierarchy; type_params; inputs; output; diff --git a/tests/trace_reference.txt b/tests/trace_reference.txt index 52edcc93..f32f5de8 100644 --- a/tests/trace_reference.txt +++ b/tests/trace_reference.txt @@ -724,7 +724,7 @@ fn test_loop4(max : u32) -> u32 { var@18 : (u32, bool); var@19 : (u32, bool); - i := 0: u32 + i := 1: u32 j := 0: u32 s := 0: u32 loop { |