From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/InterpreterLoops.ml | 55 ++++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 27 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index afbe0501..98aa0e14 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -9,12 +9,13 @@ open InterpreterUtils open InterpreterLoopsCore open InterpreterLoopsMatchCtxs open InterpreterLoopsFixedPoint +open Errors (** The local logger *) let log = Logging.loops_log (** Evaluate a loop in concrete mode *) -let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = +let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> (* We need a loop id for the [LoopReturn]. In practice it won't be used (it is useful only for the symbolic execution *) @@ -52,10 +53,10 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = * {!Unit} would account for the first iteration of the loop. * We prefer to write it this way for consistency and sanity, * though. *) - raise (Failure "Unreachable") + craise meta "Unreachable" | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We can't get there: this is only used in symbolic mode *) - raise (Failure "Unreachable") + craise meta "Unreachable" in (* Apply *) @@ -67,24 +68,24 @@ let eval_loop_symbolic (config : config) (meta : meta) fun cf ctx -> (* Debug *) log#ldebug - (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); + (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n")); (* Generate a fresh loop id *) let loop_id = fresh_loop_id () in (* Compute the fixed point at the loop entrance *) let fp_ctx, fixed_ids, rg_to_abs = - compute_loop_entry_fixed_point config loop_id eval_loop_body ctx + compute_loop_entry_fixed_point meta config loop_id eval_loop_body ctx in (* Debug *) log#ldebug (lazy - ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ctx - ^ "\n\nFixed point:\n" ^ eval_ctx_to_string fp_ctx)); + ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string meta ctx + ^ "\n\nFixed point:\n" ^ eval_ctx_to_string meta fp_ctx)); (* Compute the loop input parameters *) - let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values ctx fp_ctx in + let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values meta ctx fp_ctx in let fp_input_svalues = List.map (fun sv -> sv.sv_id) input_svalues in (* Synthesize the end of the function - we simply match the context at the @@ -115,16 +116,16 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Compute the id correspondance between the contexts *) let fp_bl_corresp = - compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx + compute_fixed_point_id_correspondance meta fixed_ids ctx fp_ctx in log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context with the \ original context:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx)); let end_expr : SymbolicAst.expression option = - match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues + match_ctx_with_target meta config loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx cf ctx in log#ldebug @@ -149,15 +150,15 @@ let eval_loop_symbolic (config : config) (meta : meta) cf res ctx | Continue i -> (* We don't support nested loops for now *) - assert (i = 0); + cassert (i = 0) meta "Nested loops are not supported yet"; log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context \ with the context at a continue:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string fp_ctx - ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx)); let cc = - match_ctx_with_target config loop_id false fp_bl_corresp + match_ctx_with_target meta config loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx in cc cf ctx @@ -165,16 +166,16 @@ let eval_loop_symbolic (config : config) (meta : meta) (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) - raise (Failure "Unreachable") + craise meta "Unreachable" in let loop_expr = eval_loop_body cf_loop fp_ctx in log#ldebug (lazy ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter ctx + ^ eval_ctx_to_string_no_filter meta ctx ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter fp_ctx + ^ eval_ctx_to_string_no_filter meta fp_ctx ^ "\n- fixed_sids: " ^ SymbolicValueId.Set.show fixed_ids.sids ^ "\n- fresh_sids: " @@ -199,7 +200,7 @@ let eval_loop_symbolic (config : config) (meta : meta) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> raise (Failure "Unreachable") + | _ -> craise meta "Unreachable" in let borrows, loans = List.partition is_borrow abs.avalues in @@ -208,10 +209,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ABorrow (AMutBorrow (bid, child_av)) -> - assert (is_aignored child_av.value); + cassert (is_aignored child_av.value) meta "TODO: error message"; Some (bid, child_av.ty) | ABorrow (ASharedBorrow _) -> None - | _ -> raise (Failure "Unreachable")) + | _ -> craise meta "Unreachable") borrows in let borrows = ref (BorrowId.Map.of_list borrows) in @@ -221,10 +222,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ALoan (AMutLoan (bid, child_av)) -> - assert (is_aignored child_av.value); + cassert (is_aignored child_av.value) meta "TODO: error message"; Some bid | ALoan (ASharedLoan _) -> None - | _ -> raise (Failure "Unreachable")) + | _ -> craise meta "Unreachable") loans in @@ -240,7 +241,7 @@ let eval_loop_symbolic (config : config) (meta : meta) ty) loan_ids in - assert (BorrowId.Map.is_empty !borrows); + cassert (BorrowId.Map.is_empty !borrows) meta "TODO: error message"; given_back_tys in @@ -259,7 +260,7 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> match config.mode with - | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx + | ConcreteMode -> eval_loop_concrete meta eval_loop_body cf ctx | SymbolicMode -> (* Simplify the context by ending the unnecessary borrows/loans and getting rid of the useless symbolic values (which are in anonymous variables) *) @@ -283,5 +284,5 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : introduce *fixed* abstractions, and again later to introduce *non-fixed* abstractions. *) - let cc = comp cc (prepare_ashared_loans None) in + let cc = comp cc (prepare_ashared_loans meta None) in comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx -- cgit v1.2.3 From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Mon, 25 Mar 2024 12:06:05 +0100 Subject: Inverted meta and config argument orders (from meta -> config to config -> meta) --- compiler/InterpreterLoops.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 98aa0e14..4d4b709e 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -75,7 +75,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Compute the fixed point at the loop entrance *) let fp_ctx, fixed_ids, rg_to_abs = - compute_loop_entry_fixed_point meta config loop_id eval_loop_body ctx + compute_loop_entry_fixed_point config meta loop_id eval_loop_body ctx in (* Debug *) @@ -125,7 +125,7 @@ let eval_loop_symbolic (config : config) (meta : meta) - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx)); let end_expr : SymbolicAst.expression option = - match_ctx_with_target meta config loop_id true fp_bl_corresp fp_input_svalues + match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx cf ctx in log#ldebug @@ -158,7 +158,7 @@ let eval_loop_symbolic (config : config) (meta : meta) - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx)); let cc = - match_ctx_with_target meta config loop_id false fp_bl_corresp + match_ctx_with_target config meta loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx in cc cf ctx -- cgit v1.2.3 From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 13:56:31 +0100 Subject: Should answer all comments, there are still some TODO: error message left --- compiler/InterpreterLoops.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 4d4b709e..d2f1b5fb 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -68,7 +68,7 @@ let eval_loop_symbolic (config : config) (meta : meta) fun cf ctx -> (* Debug *) log#ldebug - (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string meta ctx ^ "\n\n")); + (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n")); (* Generate a fresh loop id *) let loop_id = fresh_loop_id () in @@ -81,8 +81,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Debug *) log#ldebug (lazy - ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string meta ctx - ^ "\n\nFixed point:\n" ^ eval_ctx_to_string meta fp_ctx)); + ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n\nFixed point:\n" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx)); (* Compute the loop input parameters *) let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values meta ctx fp_ctx in @@ -122,8 +122,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context with the \ original context:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string meta ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let end_expr : SymbolicAst.expression option = match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues fixed_ids fp_ctx cf ctx @@ -155,8 +155,8 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context \ with the context at a continue:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string meta fp_ctx - ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string meta ctx)); + - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let cc = match_ctx_with_target config meta loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx @@ -173,9 +173,9 @@ let eval_loop_symbolic (config : config) (meta : meta) log#ldebug (lazy ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string_no_filter meta ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) ctx ^ "\n- fixed point:\n" - ^ eval_ctx_to_string_no_filter meta fp_ctx + ^ eval_ctx_to_string_no_filter ~meta:(Some meta) fp_ctx ^ "\n- fixed_sids: " ^ SymbolicValueId.Set.show fixed_ids.sids ^ "\n- fresh_sids: " @@ -209,7 +209,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ABorrow (AMutBorrow (bid, child_av)) -> - cassert (is_aignored child_av.value) meta "TODO: error message"; + sanity_check (is_aignored child_av.value) meta; Some (bid, child_av.ty) | ABorrow (ASharedBorrow _) -> None | _ -> craise meta "Unreachable") @@ -222,7 +222,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ALoan (AMutLoan (bid, child_av)) -> - cassert (is_aignored child_av.value) meta "TODO: error message"; + sanity_check (is_aignored child_av.value) meta; Some bid | ALoan (ASharedLoan _) -> None | _ -> craise meta "Unreachable") @@ -241,7 +241,7 @@ let eval_loop_symbolic (config : config) (meta : meta) ty) loan_ids in - cassert (BorrowId.Map.is_empty !borrows) meta "TODO: error message"; + sanity_check (BorrowId.Map.is_empty !borrows) meta; given_back_tys in -- cgit v1.2.3 From 53347ecc40b308b0b75a620453bfa8bd520a2c70 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 16:31:24 +0100 Subject: changes after git rebase main --- compiler/InterpreterLoops.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index d2f1b5fb..89015f71 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -102,7 +102,7 @@ let eval_loop_symbolic (config : config) (meta : meta) - src ctx (fixed-point ctx):\n" ^ eval_ctx_to_string fp_ctx ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ctx)); - prepare_match_ctx_with_target config loop_id fixed_ids fp_ctx cf ctx + prepare_match_ctx_with_target config meta loop_id fixed_ids fp_ctx cf ctx in (* Actually match *) @@ -264,7 +264,7 @@ let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) : | SymbolicMode -> (* Simplify the context by ending the unnecessary borrows/loans and getting rid of the useless symbolic values (which are in anonymous variables) *) - let cc = cleanup_fresh_values_and_abs config empty_ids_set in + let cc = cleanup_fresh_values_and_abs config meta empty_ids_set in (* We want to make sure the loop will *not* manipulate shared avalues containing themselves shared loans (i.e., nested shared loans in -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/InterpreterLoops.ml | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 89015f71..d369aef9 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -15,7 +15,8 @@ open Errors let log = Logging.loops_log (** Evaluate a loop in concrete mode *) -let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : st_cm_fun = +let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : + st_cm_fun = fun cf ctx -> (* We need a loop id for the [LoopReturn]. In practice it won't be used (it is useful only for the symbolic execution *) @@ -68,7 +69,10 @@ let eval_loop_symbolic (config : config) (meta : meta) fun cf ctx -> (* Debug *) log#ldebug - (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx ^ "\n\n")); + (lazy + ("eval_loop_symbolic:\nContext:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n\n")); (* Generate a fresh loop id *) let loop_id = fresh_loop_id () in @@ -81,11 +85,15 @@ let eval_loop_symbolic (config : config) (meta : meta) (* Debug *) log#ldebug (lazy - ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx - ^ "\n\nFixed point:\n" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx)); + ("eval_loop_symbolic:\nInitial context:\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx + ^ "\n\nFixed point:\n" + ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx)); (* Compute the loop input parameters *) - let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values meta ctx fp_ctx in + let fresh_sids, input_svalues = + compute_fp_ctx_symbolic_values meta ctx fp_ctx + in let fp_input_svalues = List.map (fun sv -> sv.sv_id) input_svalues in (* Synthesize the end of the function - we simply match the context at the @@ -122,11 +130,13 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context with the \ original context:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx - ^ "\n\n-tgt ctx (original context):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + - src ctx (fixed-point ctx)" + ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (original context):\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let end_expr : SymbolicAst.expression option = - match_ctx_with_target config meta loop_id true fp_bl_corresp fp_input_svalues - fixed_ids fp_ctx cf ctx + match_ctx_with_target config meta loop_id true fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx cf ctx in log#ldebug (lazy @@ -155,8 +165,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (lazy ("eval_loop_symbolic: about to match the fixed-point context \ with the context at a continue:\n\ - - src ctx (fixed-point ctx)" ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx - ^ "\n\n-tgt ctx (ctx at continue):\n" ^ eval_ctx_to_string ~meta:(Some meta) ctx)); + - src ctx (fixed-point ctx)" + ^ eval_ctx_to_string ~meta:(Some meta) fp_ctx + ^ "\n\n-tgt ctx (ctx at continue):\n" + ^ eval_ctx_to_string ~meta:(Some meta) ctx)); let cc = match_ctx_with_target config meta loop_id false fp_bl_corresp fp_input_svalues fixed_ids fp_ctx -- cgit v1.2.3 From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 13:21:08 +0100 Subject: added file and line arg to craise and cassert --- compiler/InterpreterLoops.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index d369aef9..17487401 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -54,10 +54,10 @@ let eval_loop_concrete (meta : Meta.meta) (eval_loop_body : st_cm_fun) : * {!Unit} would account for the first iteration of the loop. * We prefer to write it this way for consistency and sanity, * though. *) - craise meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> (* We can't get there: this is only used in symbolic mode *) - craise meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" in (* Apply *) @@ -160,7 +160,7 @@ let eval_loop_symbolic (config : config) (meta : meta) cf res ctx | Continue i -> (* We don't support nested loops for now *) - cassert (i = 0) meta "Nested loops are not supported yet"; + cassert __FILE__ __LINE__ (i = 0) meta "Nested loops are not supported yet"; log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context \ @@ -178,7 +178,7 @@ let eval_loop_symbolic (config : config) (meta : meta) (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}. For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now. *) - craise meta "Unreachable" + craise __FILE__ __LINE__ meta "Unreachable" in let loop_expr = eval_loop_body cf_loop fp_ctx in @@ -212,7 +212,7 @@ let eval_loop_symbolic (config : config) (meta : meta) match av.value with | ABorrow _ -> true | ALoan _ -> false - | _ -> craise meta "Unreachable" + | _ -> craise __FILE__ __LINE__ meta "Unreachable" in let borrows, loans = List.partition is_borrow abs.avalues in @@ -221,10 +221,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ABorrow (AMutBorrow (bid, child_av)) -> - sanity_check (is_aignored child_av.value) meta; + sanity_check __FILE__ __LINE__ (is_aignored child_av.value) meta; Some (bid, child_av.ty) | ABorrow (ASharedBorrow _) -> None - | _ -> craise meta "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable") borrows in let borrows = ref (BorrowId.Map.of_list borrows) in @@ -234,10 +234,10 @@ let eval_loop_symbolic (config : config) (meta : meta) (fun (av : typed_avalue) -> match av.value with | ALoan (AMutLoan (bid, child_av)) -> - sanity_check (is_aignored child_av.value) meta; + sanity_check __FILE__ __LINE__ (is_aignored child_av.value) meta; Some bid | ALoan (ASharedLoan _) -> None - | _ -> craise meta "Unreachable") + | _ -> craise __FILE__ __LINE__ meta "Unreachable") loans in @@ -253,7 +253,7 @@ let eval_loop_symbolic (config : config) (meta : meta) ty) loan_ids in - sanity_check (BorrowId.Map.is_empty !borrows) meta; + sanity_check __FILE__ __LINE__ (BorrowId.Map.is_empty !borrows) meta; given_back_tys in -- cgit v1.2.3 From 8f969634f3f192a9282a21a1ca2a1b6a676984ca Mon Sep 17 00:00:00 2001 From: Escherichia Date: Fri, 29 Mar 2024 14:07:36 +0100 Subject: formatting and changed save_error condition for failing from b to not b --- compiler/InterpreterLoops.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'compiler/InterpreterLoops.ml') diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 17487401..e4370367 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -160,7 +160,8 @@ let eval_loop_symbolic (config : config) (meta : meta) cf res ctx | Continue i -> (* We don't support nested loops for now *) - cassert __FILE__ __LINE__ (i = 0) meta "Nested loops are not supported yet"; + cassert __FILE__ __LINE__ (i = 0) meta + "Nested loops are not supported yet"; log#ldebug (lazy ("eval_loop_symbolic: about to match the fixed-point context \ -- cgit v1.2.3