From 536abedcbcd96922700a97de85ce2a91d807c955 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 24 Jan 2022 07:38:30 +0100 Subject: Start working on printing for symbolic AST --- src/InterpreterBorrowsCore.ml | 2 +- src/Invariants.ml | 2 +- src/Print.ml | 4 +-- src/PrintSymbolicAst.ml | 60 +++++++++++++++++++++++++++++++ src/SymbolicAstUtils.ml | 84 +++++++++++++++++++++++++++++++++++++++++++ src/Values.ml | 16 ++++++++- src/main.ml | 2 ++ 7 files changed, 165 insertions(+), 5 deletions(-) create mode 100644 src/PrintSymbolicAst.ml create mode 100644 src/SymbolicAstUtils.ml diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 1bcff935..57e47df0 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -1094,7 +1094,7 @@ let update_aproj_loans_to_ended (abs_id : V.AbstractionId.id) (* Lookup the projector of loans *) let given_back = lookup_aproj_loans abs_id sv ctx in (* Create the new value for the projector *) - let nproj = V.AEndedProjLoans given_back in + let nproj = V.AEndedProjLoans (sv, given_back) in (* Insert it *) let ctx = update_aproj_loans abs_id sv nproj ctx in (* Return *) diff --git a/src/Invariants.ml b/src/Invariants.ml index b16e71d0..6ebd3375 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -602,7 +602,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = * otherwise they should have been reduced to `_` *) let abs = Option.get info in assert (ty_has_regions_in_set abs.regions sv.V.sv_ty) - | V.AEndedProjLoans given_back_ls -> + | V.AEndedProjLoans (_msv, given_back_ls) -> List.iter (fun (_, proj) -> match proj with diff --git a/src/Print.ml b/src/Print.ml index 024d835d..cefa3ea5 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -322,7 +322,7 @@ module Values = struct ^ given_back ^ "]" | AProjBorrows (sv, rty) -> "(" ^ symbolic_value_proj_to_string fmt sv rty ^ ")" - | AEndedProjLoans given_back -> + | AEndedProjLoans (_, given_back) -> if given_back = [] then "_" else let given_back = List.map snd given_back in @@ -997,7 +997,7 @@ module Module = struct String.concat "\n\n" all_defs end -(** Pretty-printing for ASTs (functions based on an evaluation context) *) +(** Pretty-printing for CFIM ASTs (functions based on an evaluation context) *) module EvalCtxCfimAst = struct let ety_to_string (ctx : C.eval_ctx) (t : T.ety) : string = let fmt = PC.eval_ctx_to_ctx_formatter ctx in diff --git a/src/PrintSymbolicAst.ml b/src/PrintSymbolicAst.ml new file mode 100644 index 00000000..ec07a270 --- /dev/null +++ b/src/PrintSymbolicAst.ml @@ -0,0 +1,60 @@ +(** Printing utilities for symbolic AST. + + We don't put this in [Print] because: + - [Print] is getting quite big + - if we do so we have a dependency cycle... + *) + +open Errors +open Identifiers +module T = Types +module TU = TypesUtils +module V = Values +module E = Expressions +module A = CfimAst +module C = Contexts +module M = Modules +open SymbolicAst +open SymbolicAstUtils +module P = Print +module PT = Print.Types + +type formatting_ctx = { + type_context : C.type_context; + fun_context : A.fun_def A.FunDefId.Map.t; + type_vars : T.type_var list; +} + +type formatter = P.Values.value_formatter + +let formatting_ctx_to_formatter (ctx : formatting_ctx) : formatter = + (* We shouldn't use [rvar_to_string] *) + let rvar_to_string _ = failwith "Unexpected use of rvar_to_string" in + let r_to_string r = PT.region_id_to_string r in + + let type_var_id_to_string vid = + let v = T.TypeVarId.nth ctx.type_vars vid in + v.name + in + let type_def_id_to_string def_id = + let def = T.TypeDefId.Map.find def_id ctx.type_context.type_defs in + P.name_to_string def.name + in + let adt_variant_to_string = + P.Contexts.type_ctx_to_adt_variant_to_string_fun ctx.type_context.type_defs + in + (* We shouldn't use [var_id_to_string] *) + let var_id_to_string _ = failwith "Unexpected use of var_id_to_string" in + + let adt_field_names = + P.Contexts.type_ctx_to_adt_field_names_fun ctx.type_context.type_defs + 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; + } diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml new file mode 100644 index 00000000..7b93b019 --- /dev/null +++ b/src/SymbolicAstUtils.ml @@ -0,0 +1,84 @@ +open Errors +module T = Types +module V = Values +module E = Expressions +module A = CfimAst +open SymbolicAst +open ValuesUtils +open InterpreterUtils + +type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's + +type ended_loan = (V.mvalue, V.mvalue list) ended + +type ended_borrow = (V.mvalue, V.mvalue) ended + +type ended_loan_or_borrow = + | EndedLoan of ended_loan + | EndedBorrow of ended_borrow + +(** Return the list of the meta-values given to the top owned ended mutable + loans/borrows of an abstraction + + We expect an abstraction where all the loans/borrows have ended. + *) +let get_top_owned_ended_loans_borrows (abs : V.abs) : ended_loan_or_borrow list + = + (* The accumulator *) + let acc = ref [] in + let add x = acc := x :: !acc in + let add_loan x = add (EndedLoan x) in + let add_borrow x = add (EndedBorrow x) in + let add_sloan x = add_loan (EndedSymbolic x) in + let add_cloan x = add_loan (EndedConcrete x) in + let add_sborrow x = add_borrow (EndedSymbolic x) in + let add_cborrow x = add_borrow (EndedConcrete x) in + + (* The visitor *) + let obj = + object + inherit [_] V.iter_abs as super + + method! visit_aproj env aproj = + match aproj with + | AEndedProjLoans (msv, []) -> + (* The symbolic value was left unchanged *) + add_sloan [ mk_typed_value_from_symbolic_value msv ] + | AEndedProjLoans (_, mvl) -> add_sloan (List.map fst mvl) + | AEndedProjBorrows mv -> add_sborrow mv + | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) -> + failwith "Unreachable" + + method! visit_aloan_content env lc = + match lc with + | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable" + | AEndedMutLoan { child = _; given_back = _; given_back_meta } -> + (* Add the meta-value and stop the exploration *) + add_cloan given_back_meta + | AEndedSharedLoan (_, _) -> raise Unimplemented + | AEndedIgnoredMutLoan _ -> + (* Dive in *) + super#visit_aloan_content env lc + | AIgnoredSharedLoan _ -> + (* Ignore *) + () + + method! visit_aborrow_content env bc = + match bc with + | AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + failwith "Unreachable" + | AEndedMutBorrow (mv, _) -> + (* Add the meta-value and stop the exploration *) + add_cborrow mv + | AEndedIgnoredMutBorrow _ -> + (* Dive in *) + super#visit_aborrow_content env bc + | AProjSharedBorrow _ -> + (* Ignore *) + () + end + in + (* Apply *) + obj#visit_abs () abs; + (* Return the accumulated values *) + List.rev !acc diff --git a/src/Values.ml b/src/Values.ml index 1812cd18..bccb5134 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -199,6 +199,12 @@ type mvalue = typed_value [@@deriving show] as part of the environment during a symbolic execution. *) +type msymbolic_value = symbolic_value [@@deriving show] +(** "Meta"-symbolic value. + + See the explanations for [mvalue] + *) + (** When giving shared borrows to functions (i.e., inserting shared borrows inside abstractions) we need to reborrow the shared values. When doing so, we lookup the shared values and apply some special projections to the shared value @@ -229,6 +235,9 @@ class ['self] iter_aproj_base = method visit_rty : 'env -> rty -> unit = fun _ _ -> () method visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> () + + method visit_msymbolic_value : 'env -> msymbolic_value -> unit = + fun _ _ -> () end (** Ancestor for [aproj] map visitor *) @@ -239,6 +248,9 @@ class ['self] map_aproj_base = method visit_rty : 'env -> rty -> rty = fun _ ty -> ty method visit_mvalue : 'env -> mvalue -> mvalue = fun _ v -> v + + method visit_msymbolic_value : 'env -> msymbolic_value -> msymbolic_value = + fun _ m -> m end type aproj = @@ -284,10 +296,12 @@ type aproj = can't get updated/expanded: this means that we don't need to save any meta-value here. *) - | AEndedProjLoans of (mvalue * aproj) list + | AEndedProjLoans of msymbolic_value * (mvalue * aproj) list (** An ended projector of loans over a symbolic value. See the explanations for [AProjLoans] + + Note that we keep the original symbolic value as a meta-value. *) | AEndedProjBorrows of mvalue (** The only purpose of [AEndedProjBorrows] is to store, for synthesis diff --git a/src/main.ml b/src/main.ml index 062a1bd0..3772e7ac 100644 --- a/src/main.ml +++ b/src/main.ml @@ -7,6 +7,8 @@ module I = Interpreter module EL = Easy_logging.Logging module TA = TypesAnalysis module P = Pure +open SymbolicAstUtils +open PrintSymbolicAst (* This is necessary to have a backtrace when raising exceptions - for some * reason, the -g option doesn't work. -- cgit v1.2.3