summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/InterpreterBorrowsCore.ml2
-rw-r--r--src/Invariants.ml2
-rw-r--r--src/Print.ml4
-rw-r--r--src/PrintSymbolicAst.ml60
-rw-r--r--src/SymbolicAstUtils.ml84
-rw-r--r--src/Values.ml16
-rw-r--r--src/main.ml2
7 files changed, 165 insertions, 5 deletions
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.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 01:45:16 +0000