diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Interpreter.ml | 25 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.ml | 22 | ||||
| -rw-r--r-- | compiler/InterpreterLoopsFixedPoint.mli | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 4 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 3 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 39 | ||||
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 2 |
8 files changed, 70 insertions, 31 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index 22d176c9..0634eed7 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -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) *) @@ -354,7 +356,7 @@ 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 let pred (abs : abs) = match abs.kind with @@ -383,14 +385,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 = @@ -427,7 +439,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) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index 5f217983..55836e48 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -191,7 +191,7 @@ let eval_loop_symbolic (config : config) (meta : meta) is important in {!SymbolicToPure}, where we expect the given back values to have a specific order. *) - let compute_abs_given_back_tys (abs : abs) : RegionId.Set.t * rty list = + let compute_abs_given_back_tys (abs : abs) : rty list = let is_borrow (av : typed_avalue) : bool = match av.value with | ABorrow _ -> true @@ -239,7 +239,7 @@ let eval_loop_symbolic (config : config) (meta : meta) in assert (BorrowId.Map.is_empty !borrows); - (abs.regions, given_back_tys) + given_back_tys in let rg_to_given_back = RegionGroupId.Map.map compute_abs_given_back_tys rg_to_abs diff --git a/compiler/InterpreterLoopsFixedPoint.ml b/compiler/InterpreterLoopsFixedPoint.ml index c9bad3ef..39a17c25 100644 --- a/compiler/InterpreterLoopsFixedPoint.ml +++ b/compiler/InterpreterLoopsFixedPoint.ml @@ -620,12 +620,24 @@ let compute_loop_entry_fixed_point (config : config) (loop_id : LoopId.id) (* Retrieve the first id of the group *) match ids with | [] -> - (* We shouldn't get there: we actually introduce reborrows with - {!prepare_ashared_loans} and in the [match_mut_borrows] function - of {!MakeJoinMatcher} to introduce some fresh abstractions for - this purpose. + (* We *can* get there, if the loop doesn't touch the borrowed + values. + For instance: + {[ + pub fn iter_slice(a: &mut [u8]) { + let len = a.len(); + let mut i = 0; + while i < len { + i += 1; + } + } + ]} *) - raise (Failure "Unexpected") + log#ldebug + (lazy + ("No loop region to end for the region group " + ^ RegionGroupId.to_string rg_id)); + () | id0 :: ids -> let id0 = ref id0 in (* Add the proper region group into the abstraction *) diff --git a/compiler/InterpreterLoopsFixedPoint.mli b/compiler/InterpreterLoopsFixedPoint.mli index 65a76359..c0e5dca5 100644 --- a/compiler/InterpreterLoopsFixedPoint.mli +++ b/compiler/InterpreterLoopsFixedPoint.mli @@ -56,6 +56,8 @@ val prepare_ashared_loans : loop_id option -> Cps.cm_fun - the map from region group id to the corresponding abstraction appearing in the fixed point (this is useful to compute the return type of the loop backward functions for instance). + Note that this is a partial map: the loop doesn't necessarily introduce + an abstraction for each input region of the function. Rem.: the list of symbolic values should be computable by simply exploring the fixed point environment and listing all the symbolic values we find. diff --git a/compiler/Print.ml b/compiler/Print.ml index 8658a7d5..0c69bd05 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -16,6 +16,10 @@ module Expressions = Charon.PrintExpressions let list_to_string (to_string : 'a -> string) (ls : 'a list) : string = "[" ^ String.concat "; " (List.map to_string ls) ^ "]" +let pair_to_string (to_string0 : 'a -> string) (to_string1 : 'b -> string) + ((x, y) : 'a * 'b) : string = + "(" ^ to_string0 x ^ ", " ^ to_string1 y ^ ")" + let bool_to_string (b : bool) : string = if b then "true" else "false" (** Pretty-printing for values *) diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 8e8cdec3..e1f0ad38 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -215,8 +215,7 @@ and loop = { input_svalues : symbolic_value list; (** The input symbolic values *) fresh_svalues : symbolic_value_id_set; (** The symbolic values introduced by the loop fixed-point *) - rg_to_given_back_tys : - ((RegionId.Set.t * ty list) RegionGroupId.Map.t[@opaque]); + rg_to_given_back_tys : (ty list RegionGroupId.Map.t[@opaque]); (** The map from region group ids to the types of the values given back by the corresponding loop abstractions. *) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 2db5f66c..51a5da15 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -2944,12 +2944,9 @@ and translate_forward_end (ectx : C.eval_ctx) (* We are translating the forward function - nothing to do *) (ctx, fwd_e, fun e -> e) | Some bid -> - (* There are two cases here: - - if we split the fwd/backward functions, we simply need to update - the state. - - if we don't split, we also need to wrap the expression in a - lambda, which introduces the additional inputs of the backward - function + (* We need to update the state, and wrap the expression in a + lambda, which introduces the additional inputs of the backward + function. *) let ctx = (* Introduce variables for the inputs and the state variable @@ -3266,10 +3263,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl ^ "\n- rg_to_abs\n:" ^ T.RegionGroupId.Map.show - (fun (rids, tys) -> - "(" ^ T.RegionId.Set.show rids ^ ", " - ^ Print.list_to_string (ty_to_string ctx) tys - ^ ")") + (Print.list_to_string (ty_to_string ctx)) loop.rg_to_given_back_tys ^ "\n")); let ctx, _ = fresh_vars_for_symbolic_values svl ctx in @@ -3297,7 +3291,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let ctx = ref ctx in let rg_to_given_back_tys = RegionGroupId.Map.map - (fun (_, tys) -> + (fun tys -> (* The types shouldn't contain borrows - we can translate them as forward types *) List.map (fun ty -> @@ -3313,11 +3307,24 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let back_effect_infos, output_ty = (* The loop backward functions consume the same additional inputs as the parent function, but have custom outputs *) - let back_sgs = RegionGroupId.Map.bindings ctx.sg.back_sg in - let given_back_tys = RegionGroupId.Map.values rg_to_given_back_tys in + log#ldebug + (lazy + (let back_sgs = RegionGroupId.Map.bindings ctx.sg.back_sg in + "translate_loop:" ^ "\n- back_sgs: " + ^ (Print.list_to_string + (Print.pair_to_string RegionGroupId.to_string show_back_sg_info)) + back_sgs + ^ "\n- given_back_tys: " + ^ (RegionGroupId.Map.to_string None + (Print.list_to_string (pure_ty_to_string ctx))) + rg_to_given_back_tys + ^ "\n")); let back_info_tys = List.map - (fun (((id, back_sg), given_back) : (_ * back_sg_info) * ty list) -> + (fun ((rg_id, given_back) : RegionGroupId.id * ty list) -> + (* Lookup the effect information about the parent function region group + associated to this loop region abstraction *) + let back_sg = RegionGroupId.Map.find rg_id ctx.sg.back_sg in (* Remark: the effect info of the backward function for the loop is almost the same as for the backward function of the parent function. Quite importantly, the fact that the function is stateful and/or can fail @@ -3342,8 +3349,8 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = let ty = mk_arrows inputs output in Some ty in - ((id, effect_info), ty)) - (List.combine back_sgs given_back_tys) + ((rg_id, effect_info), ty)) + (RegionGroupId.Map.bindings rg_to_given_back_tys) in let back_info = List.map fst back_info_tys in let back_info = RegionGroupId.Map.of_list back_info in diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml index 865185a8..20bc107e 100644 --- a/compiler/SynthesizeSymbolic.ml +++ b/compiler/SynthesizeSymbolic.ml @@ -171,7 +171,7 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx) let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list) (fresh_svalues : SymbolicValueId.Set.t) - (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t) + (rg_to_given_back_tys : ty list RegionGroupId.Map.t) (end_expr : expression option) (loop_expr : expression option) (meta : Meta.meta) : expression option = match (end_expr, loop_expr) with |