diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterLoopsCore.ml | 1 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 16 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 7 |
3 files changed, 24 insertions, 0 deletions
diff --git a/compiler/InterpreterLoopsCore.ml b/compiler/InterpreterLoopsCore.ml index e663eb42..0bd57756 100644 --- a/compiler/InterpreterLoopsCore.ml +++ b/compiler/InterpreterLoopsCore.ml @@ -12,6 +12,7 @@ type updt_env_kind = | AbsInRight of AbstractionId.id | LoanInRight of BorrowId.id | LoansInRight of BorrowId.Set.t +[@@deriving show] (** Utility exception *) exception ValueMatchFailure of updt_env_kind diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index 4dabe974..c9bad3ef 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -352,6 +352,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) let cf_exit_loop_body (res : statement_eval_res) : m_fun = fun ctx -> + log#ldebug (lazy "compute_loop_entry_fixed_point: cf_exit_loop_body"); match res with | Return | Panic | Break _ -> None | Unit -> @@ -377,6 +378,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) context (the context at the loop entry, after we called {!prepare_ashared_loans}, if this is the first iteration) *) let join_ctxs (ctx1 : eval_ctx) : eval_ctx = + log#ldebug (lazy "compute_loop_entry_fixed_point: join_ctxs"); (* If this is the first iteration, end the borrows/loans/abs which appear in ctx1 and not in the other contexts, then compute the set of fixed ids. This means those borrows/loans have to end @@ -400,6 +402,15 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) ctx in (* End the borrows/abs in [ctx1] *) + log#ldebug + (lazy + ("compute_loop_entry_fixed_point: join_ctxs: ending \ + borrows/abstractions before entering the loop:\n\ + - ending borrow ids: " + ^ BorrowId.Set.to_string None blids + ^ "\n- ending abstraction ids: " + ^ AbstractionId.Set.to_string None aids + ^ "\n\n")); let ctx1 = end_borrows_abs blids aids ctx1 in (* We can also do the same in the contexts [ctxs]: if there are several contexts, maybe one of them ended some borrows and some @@ -420,6 +431,8 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) ctxs := []; ctx2 in + log#ldebug (lazy "compute_loop_entry_fixed_point: after join_ctxs"); + (* Compute the set of fixed ids - for the symbolic ids, we compute the intersection of ids between the original environment and the list of new environments *) @@ -440,6 +453,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) existentially quantified borrows/abstractions/symbolic values. *) let equiv_ctxs (ctx1 : eval_ctx) (ctx2 : eval_ctx) : bool = + log#ldebug (lazy "compute_fixed_point: equiv_ctx:"); let fixed_ids = compute_fixed_ids [ ctx1; ctx2 ] in let check_equivalent = true in let lookup_shared_value _ = raise (Failure "Unreachable") in @@ -531,6 +545,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) in let cf_loop : st_m_fun = fun res ctx -> + log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop"); match res with | Continue _ | Panic -> (* We don't want to generate anything *) @@ -544,6 +559,7 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) *) raise (Failure "Unreachable") | Return -> + log#ldebug (lazy "compute_loop_entry_fixed_point: cf_loop: Return"); (* Should we consume the return value and pop the frame? * If we check in [Interpreter] that the loop abstraction we end is * indeed the correct one, I think it is sound to under-approximate here diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index 97c8bcd6..0cf8b88a 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -933,6 +933,11 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun = (* Evaluate *) let cf_eval_st cf : m_fun = fun ctx -> + log#ldebug + (lazy + ("\neval_statement: cf_eval_st: statement:\n" + ^ statement_to_string_with_tab ctx st + ^ "\n\n")); match st.content with | Assign (p, rvalue) -> ( (* We handle global assignments separately *) @@ -1520,8 +1525,10 @@ and eval_assumed_function_call_symbolic (config : config) (fid : assumed_fun_id) (** Evaluate a statement seen as a function body *) and eval_function_body (config : config) (body : statement) : st_cm_fun = fun cf ctx -> + log#ldebug (lazy "eval_function_body:"); let cc = eval_statement config body in let cf_finish cf res = + log#ldebug (lazy "eval_function_body: cf_finish"); (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we * delegate the check to the caller. *) (* Expand the symbolic values if necessary - we need to do that before |