diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Contexts.ml | 19 | ||||
| -rw-r--r-- | src/InterpreterBorrows.ml | 15 | ||||
| -rw-r--r-- | src/InterpreterExpansion.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterPaths.ml | 4 | ||||
| -rw-r--r-- | src/InterpreterStatements.ml | 17 | ||||
| -rw-r--r-- | src/InterpreterUtils.ml | 2 | ||||
| -rw-r--r-- | src/Invariants.ml | 7 | ||||
| -rw-r--r-- | src/Print.ml | 4 | ||||
| -rw-r--r-- | src/main.ml | 3 |
9 files changed, 71 insertions, 4 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 7f0c822e..97584639 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -162,12 +162,30 @@ type config = { we need to expand an enumeration with strictly more than one variant) or if we need to expand a recursive type (because this leads to looping). *) + allow_bottom_below_borrow : bool; + (** Experimental. + + We sometimes want to temporarily break the invariant that there is no + bottom value below a borrow. If this value is true, we don't check + the invariant, and the rule becomes: we can't end a borrow *if* it contains + a bottom value. The consequence is that it becomes ok to temporarily + have bottom below a borrow, if we put something else inside before ending + the borrow. + + For instance, when evaluating an assignment, we move the value which + will be overwritten then do some administrative tasks with the borrows, + then move the rvalue to its destination. We currently want to be able + to check the invariants every time we end a borrow/an abstraction, + meaning at intermediate steps of the assignment where the invariants + might actually be broken. + *) } [@@deriving show] type partial_config = { check_invariants : bool; greedy_expand_symbolics_with_borrows : bool; + allow_bottom_below_borrow : bool; } (** See [config] *) @@ -178,6 +196,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) : check_invariants = config.check_invariants; greedy_expand_symbolics_with_borrows = config.greedy_expand_symbolics_with_borrows; + allow_bottom_below_borrow = config.allow_bottom_below_borrow; } type type_context = { diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index f430c15d..d200276f 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -1127,6 +1127,9 @@ and end_abstraction_loans (config : C.config) (chain : borrow_or_abs_ids) and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) (abs_id : V.AbstractionId.id) : cm_fun = fun cf ctx -> + log#ldebug + (lazy + ("end_abstraction_borrows: abs_id: " ^ V.AbstractionId.to_string abs_id)); (* Note that the abstraction mustn't contain any loans *) (* We end the borrows, starting with the *inner* ones. This is important when considering nested borrows which have the same lifetime. @@ -1193,6 +1196,10 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) with (* There are concrete (i.e., not symbolic) borrows: end them, then reexplore *) | FoundABorrowContent bc -> + log#ldebug + (lazy + ("end_abstraction_borrows: found aborrow content: " + ^ aborrow_content_to_string ctx bc)); let ctx = match bc with | V.AMutBorrow (_, bid, av) -> @@ -1242,6 +1249,10 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) end_abstraction_borrows config chain abs_id cf ctx (* There are symbolic borrows: end them, then reexplore *) | FoundAProjBorrows (sv, proj_ty) -> + log#ldebug + (lazy + ("end_abstraction_borrows: found aproj borrows: " + ^ aproj_to_string ctx (V.AProjBorrows (sv, proj_ty)))); (* Generate a fresh symbolic value *) let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in (* Replace the proj_borrows - there should be exactly one *) @@ -1255,6 +1266,10 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids) end_abstraction_borrows config chain abs_id cf ctx (* There are concrete (i.e., not symbolic) borrows in shared values: end them, then reexplore *) | FoundBorrowContent bc -> + log#ldebug + (lazy + ("end_abstraction_borrows: found borrow content: " + ^ borrow_content_to_string ctx bc)); let ctx = match bc with | V.SharedBorrow (_, bid) -> ( diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml index 4ccd2ec8..a379fe96 100644 --- a/src/InterpreterExpansion.ml +++ b/src/InterpreterExpansion.ml @@ -637,6 +637,10 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun = cf ctx with FoundSymbolicValue sv -> (* Expand and recheck the environment *) + log#ldebug + (lazy + ("greedy_expand_symbolics_with_borrows: about to expand: " + ^ symbolic_value_to_string ctx sv)); let cc : cm_fun = match sv.V.sv_ty with | T.Adt (AdtId def_id, _, _) -> diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml index 4a7d8dc8..281e7634 100644 --- a/src/InterpreterPaths.ml +++ b/src/InterpreterPaths.ml @@ -783,6 +783,10 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config) let prepare_lplace (config : C.config) (end_borrows : bool) (p : E.place) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> + log#ldebug + (lazy + ("prepare_lplace:" ^ "\n- p: " ^ place_to_string ctx p + ^ "\n- Initial context:\n" ^ eval_ctx_to_string ctx)); (* Access the place *) let access = Write in let cc = update_ctx_along_write_place config access p in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index d36c653e..56d5a260 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -85,6 +85,12 @@ let push_vars (vars : (A.var * V.typed_value) list) : cm_fun = let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : cm_fun = fun cf ctx -> + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Initial context:\n" + ^ eval_ctx_to_string ctx)); (* Push the rvalue to a dummy variable, for bookkeeping *) let cc = push_dummy_var rv in (* Prepare the destination *) @@ -104,6 +110,13 @@ let assign_to_place (config : C.config) (rv : V.typed_value) (p : E.place) : assert (not (bottom_in_value ctx.ended_regions rv)); (* Update the destination *) let ctx = write_place_unwrap config Write p rv ctx in + (* Debug *) + log#ldebug + (lazy + ("assign_to_place:" ^ "\n- rv: " + ^ typed_value_to_string ctx rv + ^ "\n- p: " ^ place_to_string ctx p ^ "\n- Final context:\n" + ^ eval_ctx_to_string ctx)); (* Continue *) cf ctx in @@ -759,6 +772,10 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = let cf_eval_rvalue = eval_rvalue config rvalue in (* Assign *) let cf_assign cf (res : (V.typed_value, eval_error) result) ctx = + log#ldebug + (lazy + ("about to assign to place: " ^ place_to_string ctx p + ^ "\n- Context:\n" ^ eval_ctx_to_string ctx)); match res with | Error EPanic -> cf Panic ctx | Ok rv -> ( diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index 0445c6b6..68547d86 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -27,6 +27,8 @@ let aborrow_content_to_string = PA.aborrow_content_to_string let aloan_content_to_string = PA.aloan_content_to_string +let aproj_to_string = PA.aproj_to_string + let typed_value_to_string = PA.typed_value_to_string let typed_avalue_to_string = PA.typed_avalue_to_string diff --git a/src/Invariants.ml b/src/Invariants.ml index fff5b897..0e4b1e23 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -298,14 +298,15 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = - borrows/loans can't contain ⊥ or inactivated mut borrows - shared loans can't contain mutable loans *) -let check_borrowed_values_invariant (ctx : C.eval_ctx) : unit = +let check_borrowed_values_invariant (config : C.config) (ctx : C.eval_ctx) : + unit = let visitor = object inherit [_] C.iter_eval_ctx as super method! visit_Bottom info = (* No ⊥ inside borrowed values *) - assert (not info.outer_borrow) + assert (config.C.allow_bottom_below_borrow || not info.outer_borrow) method! visit_ABottom _info = (* ⊥ inside an abstraction is not the same as in a regular value *) @@ -784,7 +785,7 @@ let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit = if config.C.check_invariants then ( log#ldebug (lazy "Checking invariants"); check_loans_borrows_relation_invariant ctx; - check_borrowed_values_invariant ctx; + check_borrowed_values_invariant config ctx; check_typing_invariant ctx; check_symbolic_values config ctx) else log#ldebug (lazy "Not checking invariants (check is not activated)") diff --git a/src/Print.ml b/src/Print.ml index db0b325a..d19e03e5 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1138,6 +1138,10 @@ module EvalCtxCfimAst = struct let fmt = PC.eval_ctx_to_ctx_formatter ctx in PV.aloan_content_to_string fmt lc + let aproj_to_string (ctx : C.eval_ctx) (p : V.aproj) : string = + let fmt = PC.eval_ctx_to_ctx_formatter ctx in + PV.aproj_to_string fmt p + let symbolic_value_to_string (ctx : C.eval_ctx) (sv : V.symbolic_value) : string = let fmt = PC.eval_ctx_to_ctx_formatter ctx in diff --git a/src/main.ml b/src/main.ml index d42a4f02..ca05ba78 100644 --- a/src/main.ml +++ b/src/main.ml @@ -98,7 +98,7 @@ let () = expressions_log#set_level EL.Debug; expansion_log#set_level EL.Debug; borrows_log#set_level EL.Debug; - invariants_log#set_level EL.Debug; + invariants_log#set_level EL.Warning; symbolic_to_pure_log#set_level EL.Debug; pure_micro_passes_log#set_level EL.Debug; pure_to_extract_log#set_level EL.Debug; @@ -121,6 +121,7 @@ let () = { C.check_invariants = true; greedy_expand_symbolics_with_borrows = true; + allow_bottom_below_borrow = true; } in |