diff options
| author | Son Ho | 2023-12-05 17:34:13 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 17:34:13 +0100 |
| commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
| tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /compiler/InterpreterLoopsFixedPoint.mli | |
| parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
| parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) | |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'compiler/InterpreterLoopsFixedPoint.mli')
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 26 |
1 files changed, 9 insertions, 17 deletions
diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index cb03bc9e..65a76359 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -1,13 +1,5 @@ -module T = Types -module PV = PrimitiveValues -module V = Values -module E = Expressions -module C = Contexts -module Subst = Substitute -module A = LlbcAst -module L = Logging -module Inv = Invariants -module S = SynthesizeSymbolic +open Values +open Contexts open InterpreterUtils open InterpreterLoopsCore @@ -56,7 +48,7 @@ open InterpreterLoopsCore we only introduce a fresh abstraction for [l1]. *) -val prepare_ashared_loans : V.loop_id option -> Cps.cm_fun +val prepare_ashared_loans : loop_id option -> Cps.cm_fun (** Compute a fixed-point for the context at the entry of the loop. We also return: @@ -71,11 +63,11 @@ val prepare_ashared_loans : V.loop_id option -> Cps.cm_fun the values which are read or modified (some symbolic values may be ignored). *) val compute_loop_entry_fixed_point : - C.config -> - V.loop_id -> + config -> + loop_id -> Cps.st_cm_fun -> - C.eval_ctx -> - C.eval_ctx * ids_sets * V.abs SymbolicAst.region_group_id_map + eval_ctx -> + eval_ctx * ids_sets * abs SymbolicAst.region_group_id_map (** For the abstractions in the fixed point, compute the correspondance between the borrows ids and the loans ids, if we want to introduce equivalent @@ -154,7 +146,7 @@ val compute_loop_entry_fixed_point : through the loan [l1] is actually the value which has to be given back to [l0]. *) val compute_fixed_point_id_correspondance : - ids_sets -> C.eval_ctx -> C.eval_ctx -> borrow_loan_corresp + ids_sets -> eval_ctx -> eval_ctx -> borrow_loan_corresp (** Compute the set of "quantified" symbolic value ids in a fixed-point context. @@ -163,4 +155,4 @@ val compute_fixed_point_id_correspondance : - the list of input symbolic values *) val compute_fp_ctx_symbolic_values : - C.eval_ctx -> C.eval_ctx -> V.symbolic_value_id_set * V.symbolic_value list + eval_ctx -> eval_ctx -> symbolic_value_id_set * symbolic_value list |