Skip to content

Commit

Permalink
Merge pull request #85 from AeneasVerif/son/fix_loops3
Browse files Browse the repository at this point in the history 
Fix some issues with the loops
  • Loading branch information
@sonmarcho
sonmarcho authored Mar 9, 2024
2 parents 169d011 + 46f2f1c commit 1417147
Show file tree
Hide file tree
Showing 28 changed files with 1,185 additions and 350 deletions.
30 changes: 27 additions & 3 deletions backends/lean/Base/Diverge/Elab.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -510,9 +510,19 @@ def mkDeclareUnaryBodies (grLvlParams : List Name) (kk_var : Expr)
let i ← mkFinVal grSize id
-- Check that there are no type parameters
if type_info.num_params ≠ 0 then throwError "mkUnaryBodies: a recursive call was not eliminated"
-- Introduce the call to the continuation
let param_args ← mkSigmasVal type_info.params_ty []
mkAppM' kk_var #[i, param_args]
-- We might be in a degenerate case, if the function takes no arguments
-- at all (i.e., the function is a constant).
-- For instance:
-- ```
-- divergent def infinite_loop : Result Unit := infinite_loop
-- ``
if type_info.total_num_args == 0 then do
trace[Diverge.def.genBody.visit] "Degenerate case: total_num_args=0"
mkAppM' kk_var #[i, UnitValue, UnitValue]
else do
-- Introduce the call to the continuation
let param_args ← mkSigmasVal type_info.params_ty []
mkAppM' kk_var #[i, param_args]
else pure e
| _ => pure e
trace[Diverge.def.genBody.visit] "done with expression (depth: {i}): {e}"
Expand Down Expand Up @@ -1571,6 +1581,20 @@ namespace Tests

#check test1.unfold

-- Testing a degenerate case
divergent def infinite_loop : Result Unit :=
do
let _ ← infinite_loop
Result.ret ()

#check infinite_loop.unfold

-- Testing a degenerate case
divergent def infinite_loop1 : Result Unit :=
infinite_loop1

#check infinite_loop1.unfold

/- Tests with higher-order functions -/
section HigherOrder
open Ex8
Expand Down
10 changes: 7 additions & 3 deletions compiler/Contexts.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -467,8 +467,8 @@ let env_find_abs (env : env) (pred : abs -> bool) : abs option =
in
lookup env

let env_lookup_abs (env : env) (abs_id : AbstractionId.id) : abs =
Option.get (env_find_abs env (fun abs -> abs.abs_id = abs_id))
let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
env_find_abs env (fun abs -> abs.abs_id = abs_id)

(** Remove an abstraction from the context, as well as all the references to
this abstraction (for instance, remove the abs id from all the parent sets
Expand Down Expand Up @@ -524,8 +524,12 @@ let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
in
update env

let ctx_lookup_abs_opt (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs option
=
env_lookup_abs_opt ctx.env abs_id

let ctx_lookup_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) : abs =
env_lookup_abs ctx.env abs_id
Option.get (ctx_lookup_abs_opt ctx abs_id)

let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
env_find_abs ctx.env p
Expand Down
26 changes: 21 additions & 5 deletions compiler/Interpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,8 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let parent_input_abs_ids =
List.filter_map (fun x -> x) parent_input_abs_ids
in
(* TODO: need to be careful for loops *)
assert (parent_input_abs_ids = []);

(* Insert the return value in the return abstractions (by applying
* borrow projections) *)
Expand Down Expand Up @@ -354,8 +356,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
let fun_abs_id =
(RegionGroupId.nth inst_sg.regions_hierarchy back_id).id
in
if not inside_loop then (fun_abs_id, true)
if not inside_loop then (Some fun_abs_id, true)
else
(* We are inside a loop *)
let pred (abs : abs) =
match abs.kind with
| Loop (_, rg_id', kind) ->
Expand Down Expand Up @@ -383,14 +386,24 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
}
]}
*)
let abs = Option.get (ctx_find_abs ctx pred) in
(abs.abs_id, false)
match ctx_find_abs ctx pred with
| None ->
(* The loop gives back nothing for this region group.
Ex.:
{[
pub fn ignore_input_mut_borrow(_a: &mut u32) {
loop {}
}
]}
*)
(None, false)
| Some abs -> (Some abs.abs_id, false)
in
log#ldebug
(lazy
("evaluate_function_symbolic_synthesize_backward_from_return: ending \
input abstraction: "
^ AbstractionId.to_string current_abs_id));
^ Print.option_to_string AbstractionId.to_string current_abs_id));

(* Set the proper abstractions as endable *)
let ctx =
Expand Down Expand Up @@ -427,7 +440,10 @@ let evaluate_function_symbolic_synthesize_backward_from_return (config : config)
visit_loop_abs#visit_eval_ctx () ctx
in

let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in
let current_abs_id =
match current_abs_id with None -> [] | Some id -> [ id ]
in
let target_abs_ids = List.append parent_input_abs_ids current_abs_id in
let cf_end_target_abs cf =
List.fold_left
(fun cf id -> end_abstraction config id cf)
Expand Down
134 changes: 73 additions & 61 deletions compiler/InterpreterBorrows.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -963,74 +963,86 @@ and end_abstraction_aux (config : config) (chain : borrow_or_abs_ids)
^ AbstractionId.to_string abs_id
^ "\n- original context:\n" ^ eval_ctx_to_string ctx0));

(* Lookup the abstraction *)
let abs = ctx_lookup_abs ctx abs_id in

(* Check that we can end the abstraction *)
if abs.can_end then ()
else
raise
(Failure
("Can't end abstraction "
^ AbstractionId.to_string abs.abs_id
^ " as it is set as non-endable"));

(* End the parent abstractions first *)
let cc = end_abstractions_aux config chain abs.parents in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- context after parent abstractions ended:\n"
^ eval_ctx_to_string ctx)))
in
(* Lookup the abstraction - note that if we end a list of abstractions,
ending one abstraction may lead to the current abstraction having
preemptively been ended, so the abstraction might not be in the context
anymore. *)
match ctx_lookup_abs_opt ctx abs_id with
| None ->
log#ldebug
(lazy
("abs not found (already ended): "
^ AbstractionId.to_string abs_id
^ "\n"));
cf ctx
| Some abs ->
(* Check that we can end the abstraction *)
if abs.can_end then ()
else
raise
(Failure
("Can't end abstraction "
^ AbstractionId.to_string abs.abs_id
^ " as it is set as non-endable"));

(* End the parent abstractions first *)
let cc = end_abstractions_aux config chain abs.parents in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- context after parent abstractions ended:\n"
^ eval_ctx_to_string ctx)))
in

(* End the loans inside the abstraction *)
let cc = comp cc (end_abstraction_loans config chain abs_id) in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
in
(* End the loans inside the abstraction *)
let cc = comp cc (end_abstraction_loans config chain abs_id) in
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- context after loans ended:\n" ^ eval_ctx_to_string ctx)))
in

(* End the abstraction itself by redistributing the borrows it contains *)
let cc = comp cc (end_abstraction_borrows config chain abs_id) in
(* End the abstraction itself by redistributing the borrows it contains *)
let cc = comp cc (end_abstraction_borrows config chain abs_id) in

(* End the regions owned by the abstraction - note that we don't need to
* relookup the abstraction: the set of regions in an abstraction never
* changes... *)
let cc =
comp_update cc (fun ctx ->
let ended_regions = RegionId.Set.union ctx.ended_regions abs.regions in
{ ctx with ended_regions })
in
(* End the regions owned by the abstraction - note that we don't need to
* relookup the abstraction: the set of regions in an abstraction never
* changes... *)
let cc =
comp_update cc (fun ctx ->
let ended_regions =
RegionId.Set.union ctx.ended_regions abs.regions
in
{ ctx with ended_regions })
in

(* Remove all the references to the id of the current abstraction, and remove
* the abstraction itself.
* **Rk.**: this is where we synthesize the updated symbolic AST *)
let cc = comp cc (end_abstraction_remove_from_context config abs_id) in
(* Remove all the references to the id of the current abstraction, and remove
* the abstraction itself.
* **Rk.**: this is where we synthesize the updated symbolic AST *)
let cc = comp cc (end_abstraction_remove_from_context config abs_id) in

(* Debugging *)
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
in
(* Debugging *)
let cc =
comp_unit cc (fun ctx ->
log#ldebug
(lazy
("end_abstraction_aux: "
^ AbstractionId.to_string abs_id
^ "\n- original context:\n" ^ eval_ctx_to_string ctx0
^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx)))
in

(* Sanity check: ending an abstraction must preserve the invariants *)
let cc = comp cc Invariants.cf_check_invariants in
(* Sanity check: ending an abstraction must preserve the invariants *)
let cc = comp cc Invariants.cf_check_invariants in

(* Apply the continuation *)
cc cf ctx
(* Apply the continuation *)
cc cf ctx

and end_abstractions_aux (config : config) (chain : borrow_or_abs_ids)
(abs_ids : AbstractionId.Set.t) : cm_fun =
Expand Down
Loading

0 comments on commit 1417147

Please sign in to comment.