Skip to content

Commit

Permalink
Do more cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
@sonmarcho
sonmarcho committed Nov 15, 2023
1 parent 21e3b71 commit 15f1349
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 38 deletions.
67 changes: 31 additions & 36 deletions compiler/InterpreterLoops.ml
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand Down Expand Up @@ -65,15 +60,15 @@ 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 *)
log#ldebug
(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 =
Expand All @@ -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
Expand Down Expand Up @@ -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"));
Expand All @@ -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")
Expand All @@ -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
Expand All @@ -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
Expand Down
5 changes: 3 additions & 2 deletions compiler/InterpreterLoops.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit 15f1349

Please sign in to comment.