summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-15 22:06:58 +0100
committerSon Ho2023-11-15 22:06:58 +0100
commit15f13494becbb3cf4afe8fee51b5cef50f807b52 (patch)
tree18fa1099bb8ab94a81fc41e8de6ca54965c7755b
parent21e3b719f2338f4d4a65c91edc0eb83d0b22393e (diff)
Do more cleanup
-rw-r--r--compiler/InterpreterLoops.ml67
-rw-r--r--compiler/InterpreterLoops.mli5
2 files changed, 34 insertions, 38 deletions
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 30b9316d..f88fc977 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -1,12 +1,7 @@
-module T = Types
-module PV = PrimitiveValues
-module V = Values
-module E = Expressions
-module C = Contexts
-module Subst = Substitute
-module A = LlbcAst
+open Types
+open Values
+open Contexts
open ValuesUtils
-module Inv = Invariants
module S = SynthesizeSymbolic
open Cps
open InterpreterUtils
@@ -22,7 +17,7 @@ let eval_loop_concrete (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 *)
- let loop_id = C.fresh_loop_id () in
+ let loop_id = fresh_loop_id () in
(* Continuation for after we evaluate the loop body: depending the result
of doing one loop iteration:
- redoes a loop iteration
@@ -65,7 +60,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
eval_loop_body reeval_loop_body ctx
(** Evaluate a loop in symbolic mode *)
-let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
+let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) :
st_cm_fun =
fun cf ctx ->
(* Debug *)
@@ -73,7 +68,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
(lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ctx ^ "\n\n"));
(* Generate a fresh loop id *)
- let loop_id = C.fresh_loop_id () in
+ let loop_id = fresh_loop_id () in
(* Compute the fixed point at the loop entrance *)
let fp_ctx, fixed_ids, rg_to_abs =
@@ -88,7 +83,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
(* Compute the loop input parameters *)
let fresh_sids, input_svalues = compute_fp_ctx_symbolic_values ctx fp_ctx in
- let fp_input_svalues = List.map (fun sv -> sv.V.sv_id) input_svalues 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
loop entry with the fixed point: in the synthesized code, the function
@@ -139,9 +134,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
^ "\n- fixed point:\n"
^ eval_ctx_to_string_no_filter fp_ctx
^ "\n- fixed_sids: "
- ^ V.SymbolicValueId.Set.show fixed_ids.sids
+ ^ SymbolicValueId.Set.show fixed_ids.sids
^ "\n- fresh_sids: "
- ^ V.SymbolicValueId.Set.show fresh_sids
+ ^ SymbolicValueId.Set.show fresh_sids
^ "\n- input_svalues: "
^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues
^ "\n\n"));
@@ -154,9 +149,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
is important in {!SymbolicToPure}, where we expect the given back
values to have a specific order.
*)
- let compute_abs_given_back_tys (abs : V.abs) : T.RegionId.Set.t * T.rty list =
- let is_borrow (av : V.typed_avalue) : bool =
- match av.V.value with
+ let compute_abs_given_back_tys (abs : abs) : RegionId.Set.t * rty list =
+ let is_borrow (av : typed_avalue) : bool =
+ match av.value with
| ABorrow _ -> true
| ALoan _ -> false
| _ -> raise (Failure "Unreachable")
@@ -165,25 +160,25 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
let borrows =
List.filter_map
- (fun av ->
- match av.V.value with
- | V.ABorrow (V.AMutBorrow (bid, child_av)) ->
- assert (is_aignored child_av.V.value);
- Some (bid, child_av.V.ty)
- | V.ABorrow (V.ASharedBorrow _) -> None
+ (fun (av : typed_avalue) ->
+ match av.value with
+ | ABorrow (AMutBorrow (bid, child_av)) ->
+ assert (is_aignored child_av.value);
+ Some (bid, child_av.ty)
+ | ABorrow (ASharedBorrow _) -> None
| _ -> raise (Failure "Unreachable"))
borrows
in
- let borrows = ref (V.BorrowId.Map.of_list borrows) in
+ let borrows = ref (BorrowId.Map.of_list borrows) in
let loan_ids =
List.filter_map
- (fun av ->
- match av.V.value with
- | V.ALoan (V.AMutLoan (bid, child_av)) ->
- assert (is_aignored child_av.V.value);
+ (fun (av : typed_avalue) ->
+ match av.value with
+ | ALoan (AMutLoan (bid, child_av)) ->
+ assert (is_aignored child_av.value);
Some bid
- | V.ALoan (V.ASharedLoan _) -> None
+ | ALoan (ASharedLoan _) -> None
| _ -> raise (Failure "Unreachable"))
loans
in
@@ -193,28 +188,28 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
List.map
(fun lid ->
let bid =
- V.BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
+ BorrowId.InjSubst.find lid fp_bl_corresp.loan_to_borrow_id_map
in
- let ty = V.BorrowId.Map.find bid !borrows in
- borrows := V.BorrowId.Map.remove bid !borrows;
+ let ty = BorrowId.Map.find bid !borrows in
+ borrows := BorrowId.Map.remove bid !borrows;
ty)
loan_ids
in
- assert (V.BorrowId.Map.is_empty !borrows);
+ assert (BorrowId.Map.is_empty !borrows);
(abs.regions, given_back_tys)
in
let rg_to_given_back =
- T.RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
+ RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs
in
(* Put together *)
S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
loop_expr
-let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
fun cf ctx ->
- match config.C.mode with
+ match config.mode with
| ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
| SymbolicMode ->
(* We want to make sure the loop will *not* manipulate shared avalues
diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli
index 7395739b..320e4bcb 100644
--- a/compiler/InterpreterLoops.mli
+++ b/compiler/InterpreterLoops.mli
@@ -56,7 +56,8 @@
From here, we deduce that [abs@fp { MB l0, ML l1}] is the loop abstraction.
*)
-module C = Contexts
+open Contexts
+open Cps
(** Evaluate a loop *)
-val eval_loop : C.config -> Cps.st_cm_fun -> Cps.st_cm_fun
+val eval_loop : config -> st_cm_fun -> st_cm_fun