summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-01-27 11:19:50 +0100
committerSon Ho2022-01-27 11:21:05 +0100
commit98677400fc27087ab4443094fb94a95412515422 (patch)
tree0c6354c1a4b69b2a30d9b4e7909d90a0ddcb48ee /src
parent2c9f43840c7c2721d8fab9981ecac9cc0e6fafd5 (diff)
Add some printing facilities to SymbolicToPure
Diffstat (limited to 'src')
-rw-r--r--src/Print.ml50
-rw-r--r--src/SymbolicToPure.ml19
-rw-r--r--src/Translate.ml5
3 files changed, 70 insertions, 4 deletions
diff --git a/src/Print.ml b/src/Print.ml
index e1834ca6..69feeb6c 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -583,6 +583,11 @@ module PC = Contexts (* local module *)
(** Pretty-printing for contexts (generic functions) *)
module CfimAst = struct
+ let var_to_string (var : A.var) : string =
+ match var.name with
+ | None -> V.VarId.to_string var.index
+ | Some name -> name
+
type ast_formatter = {
rvar_to_string : T.RegionVarId.id -> string;
r_to_string : T.RegionId.id -> string;
@@ -608,6 +613,9 @@ module CfimAst = struct
PV.adt_field_names = fmt.adt_field_names;
}
+ let ast_to_value_formatter (fmt : ast_formatter) : PV.value_formatter =
+ ast_to_ctx_formatter fmt
+
let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
{
PT.r_to_string = PT.erased_region_to_string;
@@ -658,6 +666,48 @@ module CfimAst = struct
fun_def_id_to_string;
}
+ let fun_def_to_ast_formatter (type_defs : T.type_def T.TypeDefId.Map.t)
+ (fun_defs : A.fun_def A.FunDefId.Map.t) (fdef : A.fun_def) : ast_formatter
+ =
+ let rvar_to_string r =
+ let rvar = T.RegionVarId.nth fdef.signature.region_params r in
+ PT.region_var_to_string rvar
+ in
+ let r_to_string r = PT.region_id_to_string r in
+
+ let type_var_id_to_string vid =
+ let var = T.TypeVarId.nth fdef.signature.type_params vid in
+ PT.type_var_to_string var
+ in
+ let type_def_id_to_string def_id =
+ let def = T.TypeDefId.Map.find def_id type_defs in
+ name_to_string def.name
+ in
+ let adt_variant_to_string =
+ PC.type_ctx_to_adt_variant_to_string_fun type_defs
+ in
+ let var_id_to_string vid =
+ let var = V.VarId.nth fdef.locals vid in
+ var_to_string var
+ in
+ let adt_field_names = PC.type_ctx_to_adt_field_names_fun type_defs in
+ let adt_field_to_string = type_ctx_to_adt_field_to_string_fun type_defs in
+ let fun_def_id_to_string def_id =
+ let def = A.FunDefId.Map.find def_id fun_defs in
+ name_to_string def.name
+ in
+ {
+ rvar_to_string;
+ r_to_string;
+ type_var_id_to_string;
+ type_def_id_to_string;
+ adt_variant_to_string;
+ var_id_to_string;
+ adt_field_names;
+ adt_field_to_string;
+ fun_def_id_to_string;
+ }
+
let rec projection_to_string (fmt : ast_formatter) (inside : string)
(p : E.projection) : string =
match p with
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 884c7c8f..1985bfd3 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -190,6 +190,7 @@ type call_info = {
type bs_ctx = {
type_context : type_context;
fun_context : fun_context;
+ fun_def : A.fun_def;
bid : T.RegionGroupId.id option; (** TODO: rename *)
sv_to_var : var V.SymbolicValueId.Map.t;
(** Whenever we encounter a new symbolic value (introduced because of
@@ -210,6 +211,19 @@ type bs_ctx = {
}
(** Body synthesis context *)
+(* TODO: move *)
+let bs_ctx_to_value_formatter (ctx : bs_ctx) : Print.CfimAst.ast_formatter =
+ Print.CfimAst.fun_def_to_ast_formatter ctx.type_context.cfim_type_defs
+ ctx.fun_context.cfim_fun_defs ctx.fun_def
+
+(* TODO: move *)
+let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string =
+ let fmt = bs_ctx_to_value_formatter ctx in
+ let fmt = Print.CfimAst.ast_to_value_formatter fmt in
+ let indent = "" in
+ let indent_incr = " " in
+ Print.Values.abs_to_string fmt indent indent_incr abs
+
let get_instantiated_fun_sig (fun_id : A.fun_id)
(back_id : T.RegionGroupId.id option) (tys : ty list) (ctx : bs_ctx) :
inst_fun_sig =
@@ -692,6 +706,7 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
See [typed_avalue_to_consumed].
*)
let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
+ log#ldebug (lazy ("abs_to_consumed:\n" ^ abs_to_string ctx abs));
List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
(** Explore an abstraction value and convert it to a given back value
@@ -1162,8 +1177,8 @@ 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 (def : A.fun_def) (ctx : bs_ctx) (body : S.expression) :
- fun_def =
+let translate_fun_def (ctx : bs_ctx) (body : S.expression) : fun_def =
+ let def = ctx.fun_def in
let bid = ctx.bid in
log#ldebug
(lazy
diff --git a/src/Translate.ml b/src/Translate.ml
index ec580258..ce9f085c 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -90,6 +90,7 @@ let translate_function_to_pure (config : C.partial_config)
var_counter;
type_context;
fun_context;
+ fun_def = fdef;
forward_inputs = [];
(* Empty for now *)
backward_inputs = T.RegionGroupId.Map.empty;
@@ -116,7 +117,7 @@ let translate_function_to_pure (config : C.partial_config)
(* Translate the forward function *)
let pure_forward =
- SymbolicToPure.translate_fun_def fdef
+ SymbolicToPure.translate_fun_def
(add_forward_inputs (fst symbolic_forward) ctx)
(snd symbolic_forward)
in
@@ -155,7 +156,7 @@ let translate_function_to_pure (config : C.partial_config)
in
(* Translate *)
- SymbolicToPure.translate_fun_def fdef ctx symbolic
+ SymbolicToPure.translate_fun_def ctx symbolic
in
let pure_backwards =
List.map translate_backward fdef.signature.regions_hierarchy