From 05db1377f1b987050e58643b9bf001f62a77e303 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 5 Jan 2022 08:43:24 +0100 Subject: Introduce the type_context definition --- src/Print.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index 2fd7e336..90f3946b 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -492,17 +492,19 @@ module Contexts = struct v.name in let type_def_id_to_string def_id = - let def = T.TypeDefId.nth ctx.type_context def_id in + let def = T.TypeDefId.nth ctx.type_context.type_defs def_id in PT.name_to_string def.name in let adt_variant_to_string = - type_ctx_to_adt_variant_to_string_fun ctx.type_context + type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs in let var_id_to_string vid = let bv = C.ctx_lookup_binder ctx vid in binder_to_string bv in - let adt_field_names = type_ctx_to_adt_field_names_fun ctx.C.type_context in + let adt_field_names = + type_ctx_to_adt_field_names_fun ctx.type_context.type_defs + in { rvar_to_string; r_to_string; @@ -604,7 +606,7 @@ module CfimAst = struct let eval_ctx_to_ast_formatter (ctx : C.eval_ctx) : ast_formatter = let ctx_fmt = PC.eval_ctx_to_ctx_formatter ctx in let adt_field_to_string = - type_ctx_to_adt_field_to_string_fun ctx.type_context + type_ctx_to_adt_field_to_string_fun ctx.type_context.type_defs in let fun_def_id_to_string def_id = let def = A.FunDefId.nth ctx.fun_context def_id in -- cgit v1.2.3 From f2fb0dc39cfa9aef2b16963d3f8a270ec45bae5e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 14:43:35 +0100 Subject: Make good progress on implementing utilities to test symbolic execution --- src/Print.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index 90f3946b..de1952e1 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -843,7 +843,7 @@ module CfimAst = struct (* Arguments *) let inputs = List.tl def.locals in - let inputs, _aux_locals = Utilities.list_split_at inputs def.arg_count in + let inputs, _aux_locals = Utils.list_split_at inputs def.arg_count in let args = List.combine inputs sg.inputs in let args = List.map -- cgit v1.2.3 From ef7141aab368f682a3846a56624f3c1b90dc445c Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 15:37:55 +0100 Subject: Fix some printing issues --- src/Print.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index de1952e1..f265cacb 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -739,7 +739,7 @@ module CfimAst = struct indent ^ "set_discriminant(" ^ place_to_string fmt p ^ ", " ^ T.VariantId.to_string variant_id ^ ")" - | A.Drop p -> "drop(" ^ place_to_string fmt p ^ ")" + | A.Drop p -> indent ^ "drop(" ^ place_to_string fmt p ^ ")" | A.Assert a -> let cond = operand_to_string fmt a.A.cond in if a.A.expected then indent ^ "assert(" ^ cond ^ ")" @@ -777,7 +777,7 @@ module CfimAst = struct | A.Nop -> indent ^ "nop" | A.Sequence (st1, st2) -> statement_to_string fmt indent indent_incr st1 - ^ "\n" + ^ ";\n" ^ statement_to_string fmt indent indent_incr st2 | A.Switch (op, tgts) -> ( let op = operand_to_string fmt op in -- cgit v1.2.3 From 12752a3e62a53c56753cb58f044cd6d277f19734 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 15:48:38 +0100 Subject: Make minor improvements to printing --- src/Print.ml | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index f265cacb..e751d0a3 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -419,18 +419,20 @@ module Values = struct ^ abstract_shared_borrows_to_string fmt sb ^ ")" - let abs_to_string (fmt : value_formatter) (abs : V.abs) : string = + let abs_to_string (fmt : value_formatter) (indent : string) + (indent_incr : string) (abs : V.abs) : string = + let indent2 = indent ^ indent_incr in let avs = - List.map (fun av -> " " ^ typed_avalue_to_string fmt av) abs.avalues + List.map (fun av -> indent2 ^ typed_avalue_to_string fmt av) abs.avalues in let avs = String.concat ",\n" avs in - "abs@" + indent ^ "abs@" ^ V.AbstractionId.to_string abs.abs_id ^ "{parents=" ^ V.AbstractionId.set_to_string abs.parents ^ "}" ^ "{regions=" ^ T.RegionId.set_to_string abs.regions - ^ "}" ^ " {\n" ^ avs ^ "\n}" + ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" end module PV = Values (* local module *) @@ -442,17 +444,20 @@ module Contexts = struct | None -> PV.var_id_to_string bv.index | Some name -> name - let env_elem_to_string (fmt : PV.value_formatter) (ev : C.env_elem) : string = + let env_elem_to_string (fmt : PV.value_formatter) (indent : string) + (indent_incr : string) (ev : C.env_elem) : string = match ev with | Var (var, tv) -> - binder_to_string var ^ " -> " ^ PV.typed_value_to_string fmt tv ^ " ;" - | Abs abs -> PV.abs_to_string fmt abs + indent ^ binder_to_string var ^ " -> " + ^ PV.typed_value_to_string fmt tv + ^ " ;" + | Abs abs -> PV.abs_to_string fmt indent indent_incr abs | Frame -> failwith "Can't print a Frame element" let env_to_string (fmt : PV.value_formatter) (env : C.env) : string = "{\n" ^ String.concat "\n" - (List.map (fun ev -> " " ^ env_elem_to_string fmt ev) env) + (List.map (fun ev -> env_elem_to_string fmt " " " " ev) env) ^ "\n}" type ctx_formatter = PV.value_formatter -- cgit v1.2.3 From 407474a35b7dd80116c8d358873d25e1a9b49048 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 16:18:40 +0100 Subject: Fix some bugs --- src/Print.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index e751d0a3..0b436f1a 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -981,6 +981,10 @@ module EvalCtxCfimAst = struct let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.typed_value_to_string fmt v + let typed_avalue_to_string (ctx : C.eval_ctx) (v : V.typed_avalue) : string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.typed_avalue_to_string fmt v + let place_to_string (ctx : C.eval_ctx) (op : E.place) : string = let fmt = PA.eval_ctx_to_ast_formatter ctx in PA.place_to_string fmt op -- cgit v1.2.3 From 7137e0733650e0ce37eff4ff805c95543f2c1161 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 6 Jan 2022 17:44:17 +0100 Subject: Remove the symbolic_proj_comp def and make the set of ended regions a field in the eval_ctx struct --- src/Print.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'src/Print.ml') diff --git a/src/Print.ml b/src/Print.ml index 0b436f1a..f714e847 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -214,11 +214,6 @@ module Values = struct (sv : V.symbolic_value) : string = symbolic_value_id_to_string sv.sv_id ^ " : " ^ PT.rty_to_string fmt sv.sv_ty - let symbolic_proj_comp_to_string (fmt : PT.rtype_formatter) - (sp : V.symbolic_proj_comp) : string = - let regions = T.RegionId.set_to_string sp.rset_ended in - "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")" - let symbolic_value_proj_to_string (fmt : value_formatter) (sv : V.symbolic_value) (rty : T.rty) : string = symbolic_value_id_to_string sv.sv_id @@ -275,8 +270,7 @@ module Values = struct | Bottom -> "⊥ : " ^ PT.ty_to_string ty_fmt v.ty | Borrow bc -> borrow_content_to_string fmt bc | Loan lc -> loan_content_to_string fmt lc - | Symbolic s -> - symbolic_proj_comp_to_string (value_to_rtype_formatter fmt) s + | Symbolic s -> symbolic_value_to_string (value_to_rtype_formatter fmt) s and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) : string = @@ -539,6 +533,7 @@ module Contexts = struct let eval_ctx_to_string (ctx : C.eval_ctx) : string = let fmt = eval_ctx_to_ctx_formatter ctx in + let ended_regions = T.RegionId.set_to_string ctx.ended_regions in let frames = split_env_according_to_frames ctx.env in let num_frames = List.length frames in let frames = @@ -547,7 +542,8 @@ module Contexts = struct "\n# Frame " ^ string_of_int i ^ ":\n" ^ env_to_string fmt f ^ "\n") frames in - "# " ^ string_of_int num_frames ^ " frame(s)\n" ^ String.concat "" frames + "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames + ^ " frame(s)\n" ^ String.concat "" frames end module PC = Contexts (* local module *) -- cgit v1.2.3