diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Interpreter.ml | 97 | ||||
| -rw-r--r-- | compiler/InterpreterBorrows.ml | 15 | ||||
| -rw-r--r-- | compiler/InterpreterExpressions.ml | 34 | ||||
| -rw-r--r-- | compiler/InterpreterLoops.ml | 586 | ||||
| -rw-r--r-- | compiler/InterpreterStatements.ml | 4 | ||||
| -rw-r--r-- | compiler/InterpreterUtils.ml | 23 | ||||
| -rw-r--r-- | compiler/Invariants.ml | 2 | ||||
| -rw-r--r-- | compiler/Print.ml | 1 | ||||
| -rw-r--r-- | compiler/PrintPure.ml | 2 | ||||
| -rw-r--r-- | compiler/SymbolicAst.ml | 16 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 57 | ||||
| -rw-r--r-- | compiler/Values.ml | 7 |
12 files changed, 594 insertions, 250 deletions
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml index f47c6226..ea61e2b2 100644 --- a/compiler/Interpreter.ml +++ b/compiler/Interpreter.ml @@ -138,7 +138,9 @@ let evaluate_function_symbolic_synthesize_backward_from_return log#ldebug (lazy ("evaluate_function_symbolic_synthesize_backward_from_return:" - ^ "\n- back_id: " + ^ "\n- fname: " + ^ Print.fun_name_to_string fdef.name + ^ "\n- back_id: " ^ T.RegionGroupId.to_string back_id ^ "\n- loop_id: " ^ Print.option_to_string V.LoopId.to_string loop_id @@ -213,6 +215,62 @@ let evaluate_function_symbolic_synthesize_backward_from_return else ctx in + (* We now need to end the proper *input* abstractions - pay attention + * to the fact that we end the *input* abstractions, not the *return* + * abstractions (of course, the corresponding return abstractions will + * automatically be ended, because they consumed values coming from the + * input abstractions...) *) + (* End the parent abstractions and the current abstraction - note that we + * end them in an order which follows the regions hierarchy: it should lead + * to generated code which has a better consistency between the parent + * and children backward functions. + * + * Note that we don't end the same abstraction if we are *inside* a loop (i.e., + * we are evaluating an [EndContinue]) or not. + *) + let current_abs_id, end_fun_synth_input = + let fun_abs_id = + (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id + in + if not inside_loop then (fun_abs_id, true) + else + let pred (abs : V.abs) = + match abs.kind with + | V.Loop (_, rg_id', kind) -> + let rg_id' = Option.get rg_id' in + let is_ret = + match kind with V.LoopSynthInput -> true | V.LoopCall -> false + in + rg_id' = back_id && is_ret + | _ -> false + in + (* There is not necessarily an input synthesis abstraction specifically + for the loop. + If there is none, the input synthesis abstraction is actually the + function input synthesis abstraction. + + Example: + ======== + {[ + fn clear(v: &mut Vec<u32>) { + let mut i = 0; + while i < v.len() { + v[i] = 0; + i += 1; + } + } + ]} + *) + match C.ctx_find_abs ctx pred with + | Some abs -> (abs.abs_id, false) + | None -> (fun_abs_id, true) + in + log#ldebug + (lazy + ("evaluate_function_symbolic_synthesize_backward_from_return: ending \ + input abstraction: " + ^ V.AbstractionId.to_string current_abs_id)); + (* Set the proper abstractions as endable *) let ctx = let visit_loop_abs = @@ -237,7 +295,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return assert (loop_id = Some loop_id'); { abs with can_end = true } | V.SynthInput rg_id' -> - if rg_id' = back_id && not inside_loop then + if rg_id' = back_id && end_fun_synth_input then { abs with can_end = true } else abs | _ -> @@ -248,41 +306,6 @@ let evaluate_function_symbolic_synthesize_backward_from_return visit_loop_abs#visit_eval_ctx () ctx in - (* We now need to end the proper *input* abstractions - pay attention - * to the fact that we end the *input* abstractions, not the *return* - * abstractions (of course, the corresponding return abstractions will - * automatically be ended, because they consumed values coming from the - * input abstractions...) *) - (* End the parent abstractions and the current abstraction - note that we - * end them in an order which follows the regions hierarchy: it should lead - * to generated code which has a better consistency between the parent - * and children backward functions. - * - * Note that we don't end the same abstraction if we are *inside* a loop (i.e., - * we are evaluating an [EndContinue]) or not. - *) - let current_abs_id = - if not inside_loop then - (T.RegionGroupId.nth inst_sg.regions_hierarchy back_id).id - else - let pred (abs : V.abs) = - match abs.kind with - | V.Loop (_, rg_id', kind) -> - let rg_id' = Option.get rg_id' in - let is_ret = - match kind with V.LoopSynthInput -> true | V.LoopCall -> false - in - rg_id' = back_id && is_ret - | _ -> false - in - let abs = Option.get (C.ctx_find_abs ctx pred) in - abs.abs_id - in - log#ldebug - (lazy - ("evaluate_function_symbolic_synthesize_backward_from_return: ending \ - input abstraction: " - ^ V.AbstractionId.to_string current_abs_id)); let target_abs_ids = List.append parent_input_abs_ids [ current_abs_id ] in let cf_end_target_abs cf = List.fold_left diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml index b2a46b1e..38c6df3d 100644 --- a/compiler/InterpreterBorrows.ml +++ b/compiler/InterpreterBorrows.ml @@ -753,6 +753,9 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind) | V.SynthRet _ -> V.SynthRetGivenBack | V.SynthInput _ -> V.SynthInputGivenBack | V.Loop _ -> V.LoopGivenBack + | V.Identity -> + (* Identity abstractions give back nothing *) + raise (Failure "Unreachable") in mk_fresh_symbolic_value sv_kind av.V.ty @@ -1453,18 +1456,6 @@ let end_borrows config : V.BorrowId.Set.t -> cm_fun = let end_abstraction config = end_abstraction_aux config [] let end_abstractions config = end_abstractions_aux config [] -(** Auxiliary function - call a function which requires a continuation, - and return the let context given to the continuation *) -let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx = - let nctx = ref None in - let cf ctx = - assert (!nctx = None); - nctx := Some ctx; - None - in - let _ = f cf ctx in - Option.get !nctx - let end_borrow_no_synth config id ctx = get_cf_ctx_no_synth (end_borrow config id) ctx diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml index 43580312..82d8586a 100644 --- a/compiler/InterpreterExpressions.ml +++ b/compiler/InterpreterExpressions.ml @@ -548,9 +548,22 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) (cf : V.typed_value -> m_fun) : m_fun = fun ctx -> match bkind with - | E.Shared | E.TwoPhaseMut -> + | E.Shared | E.TwoPhaseMut | E.Shallow -> + (* **REMARK**: we treat shallow borrows like shared borrows. In theory, + this is incomplete. But in practice, this should allow to handle + many cases: in effect, we are simply forbidding match guards from + performing too many modifications in the environment, which is + probably not a too bad thing to do. + *) + (* Access the value *) - let access = if bkind = E.Shared then Read else Write in + let access = + match bkind with + | E.Shared | E.Shallow -> Read + | E.TwoPhaseMut -> Write + | _ -> raise (Failure "Unreachable") + in + let expand_prim_copy = false in let prepare = access_rplace_reorganize_and_read config expand_prim_copy access p @@ -578,12 +591,21 @@ let eval_rvalue_ref (config : C.config) (p : E.place) (bkind : E.borrow_kind) let ctx = write_place access p nv ctx in (* Compute the rvalue - simply a shared borrow with a the fresh id. * Note that the reference is *mutable* if we do a two-phase borrow *) - let rv_ty = - T.Ref (T.Erased, v.ty, if bkind = E.Shared then Shared else Mut) + let ref_kind = + match bkind with + | E.Shared | E.Shallow -> T.Shared + | E.TwoPhaseMut -> T.Mut + | _ -> raise (Failure "Unreachable") in + let rv_ty = T.Ref (T.Erased, v.ty, ref_kind) in let bc = - if bkind = E.Shared then V.SharedBorrow bid - else V.ReservedMutBorrow bid + match bkind with + | E.Shared | E.Shallow -> + (* See the remark at the beginning of the match branch: we + handle shallow borrows like shared borrows *) + V.SharedBorrow bid + | E.TwoPhaseMut -> V.ReservedMutBorrow bid + | _ -> raise (Failure "Unreachable") in let rv : V.typed_value = { V.value = V.Borrow bc; ty = rv_ty } in (* Continue *) diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml index d5d6fa7e..76085b55 100644 --- a/compiler/InterpreterLoops.ml +++ b/compiler/InterpreterLoops.ml @@ -89,7 +89,7 @@ type updt_env_kind = exception ValueMatchFailure of updt_env_kind (** Utility exception *) -exception Distinct +exception Distinct of string type ctx_or_update = (C.eval_ctx, updt_env_kind) result @@ -1781,90 +1781,102 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct module MkGetSetM (Id : Identifiers.Id) = struct module Inj = Id.InjSubst - let get (m : Inj.t ref) (k : Id.id) : Id.id = - match Inj.find_opt k !m with None -> k | Some k -> k - - let add (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = - if Inj.mem k0 !m then raise Distinct - else if Inj.Set.mem k1 (Inj.elements !m) then raise Distinct - else ( - m := Inj.add k0 k1 !m; - k1) - - let match_e (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id = - let k0 = get m k0 in - if k0 = k1 then k1 else add m k0 k1 - - let match_el (m : Inj.t ref) (kl0 : Id.id list) (kl1 : Id.id list) : - Id.id list = - List.map (fun (k0, k1) -> match_e m k0 k1) (List.combine kl0 kl1) + let add (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) = + (* Check if k0 is already registered as a key *) + match Inj.find_opt k0 !m with + | None -> + (* Not registered: check if k1 is in the set of values, + otherwise add the binding *) + if Inj.Set.mem k1 (Inj.elements !m) then + raise + (Distinct + (msg ^ "adding [k0=" ^ Id.to_string k0 ^ " -> k1=" + ^ Id.to_string k1 ^ " ]: k1 already in the set of elements")) + else ( + m := Inj.add k0 k1 !m; + k1) + | Some k1' -> + (* It is: check that the bindings are consistent *) + if k1 <> k1' then raise (Distinct (msg ^ "already a binding for k0")) + else k1 + + let match_e (msg : string) (m : Inj.t ref) (k0 : Id.id) (k1 : Id.id) : Id.id + = + (* TODO: merge the add and merge functions *) + add msg m k0 k1 + + let match_el (msg : string) (m : Inj.t ref) (kl0 : Id.id list) + (kl1 : Id.id list) : Id.id list = + List.map (fun (k0, k1) -> match_e msg m k0 k1) (List.combine kl0 kl1) (** Figuring out mappings between sets of ids is hard in all generality... We use the fact that the fresh ids should have been generated the same way (i.e., in the same order) and match the ids two by two in increasing order. *) - let match_es (m : Inj.t ref) (ks0 : Id.Set.t) (ks1 : Id.Set.t) : Id.Set.t = - Id.Set.of_list (match_el m (Id.Set.elements ks0) (Id.Set.elements ks1)) + let match_es (msg : string) (m : Inj.t ref) (ks0 : Id.Set.t) + (ks1 : Id.Set.t) : Id.Set.t = + Id.Set.of_list + (match_el msg m (Id.Set.elements ks0) (Id.Set.elements ks1)) end module GetSetRid = MkGetSetM (T.RegionId) - let match_rid = GetSetRid.match_e S.rid_map + let match_rid = GetSetRid.match_e "match_rid: " S.rid_map (* let match_ridl = GetSetRid.match_el S.rid_map *) - let match_rids = GetSetRid.match_es S.rid_map + let match_rids = GetSetRid.match_es "match_rids: " S.rid_map module GetSetBid = MkGetSetM (V.BorrowId) - let get_blid = GetSetBid.get S.blid_map - let match_blid = GetSetBid.match_e S.blid_map - let match_blidl = GetSetBid.match_el S.blid_map - let match_blids = GetSetBid.match_es S.blid_map - - let get_borrow_id = - if S.check_equiv then get_blid else GetSetBid.get S.borrow_id_map + let match_blid msg = GetSetBid.match_e msg S.blid_map + let match_blidl msg = GetSetBid.match_el msg S.blid_map + let match_blids msg = GetSetBid.match_es msg S.blid_map let match_borrow_id = - if S.check_equiv then match_blid else GetSetBid.match_e S.borrow_id_map + if S.check_equiv then match_blid "match_borrow_id: " + else GetSetBid.match_e "match_borrow_id: " S.borrow_id_map let match_borrow_idl = - if S.check_equiv then match_blidl else GetSetBid.match_el S.borrow_id_map + if S.check_equiv then match_blidl "match_borrow_idl: " + else GetSetBid.match_el "match_borrow_idl: " S.borrow_id_map let match_borrow_ids = - if S.check_equiv then match_blids else GetSetBid.match_es S.borrow_id_map - - let get_loan_id = - if S.check_equiv then get_blid else GetSetBid.get S.loan_id_map + if S.check_equiv then match_blids "match_borrow_ids: " + else GetSetBid.match_es "match_borrow_ids: " S.borrow_id_map let match_loan_id = - if S.check_equiv then match_blid else GetSetBid.match_e S.loan_id_map + if S.check_equiv then match_blid "match_loan_id: " + else GetSetBid.match_e "match_loan_id: " S.loan_id_map let match_loan_idl = - if S.check_equiv then match_blidl else GetSetBid.match_el S.loan_id_map + if S.check_equiv then match_blidl "match_loan_idl: " + else GetSetBid.match_el "match_loan_idl: " S.loan_id_map let match_loan_ids = - if S.check_equiv then match_blids else GetSetBid.match_es S.loan_id_map + if S.check_equiv then match_blids "match_loan_ids: " + else GetSetBid.match_es "match_loan_ids: " S.loan_id_map module GetSetSid = MkGetSetM (V.SymbolicValueId) module GetSetAid = MkGetSetM (V.AbstractionId) - let match_aid = GetSetAid.match_e S.aid_map - let match_aidl = GetSetAid.match_el S.aid_map - let match_aids = GetSetAid.match_es S.aid_map + let match_aid = GetSetAid.match_e "match_aid: " S.aid_map + let match_aidl = GetSetAid.match_el "match_aidl: " S.aid_map + let match_aids = GetSetAid.match_es "match_aids: " S.aid_map (** *) - let match_etys ty0 ty1 = if ty0 <> ty1 then raise Distinct else ty0 + let match_etys ty0 ty1 = + if ty0 <> ty1 then raise (Distinct "match_etys") else ty0 let match_rtys ty0 ty1 = - let match_distinct_types _ _ = raise Distinct in + let match_distinct_types _ _ = raise (Distinct "match_rtys") in let match_regions r0 r1 = match (r0, r1) with | T.Static, T.Static -> r1 | Var rid0, Var rid1 -> let rid = match_rid rid0 rid1 in Var rid - | _ -> raise Distinct + | _ -> raise (Distinct "match_rtys") in match_types match_distinct_types match_regions ty0 ty1 @@ -1874,11 +1886,16 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct let match_distinct_adts (_ty : T.ety) (_adt0 : V.adt_value) (_adt1 : V.adt_value) : V.typed_value = - raise Distinct + raise (Distinct "match_distinct_adts") let match_shared_borrows (match_typed_values : V.typed_value -> V.typed_value -> V.typed_value) (_ty : T.ety) (bid0 : V.borrow_id) (bid1 : V.borrow_id) : V.borrow_id = + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_shared_borrows: " ^ "bid0: " + ^ V.BorrowId.to_string bid0 ^ ", bid1: " ^ V.BorrowId.to_string bid1)); + let bid = match_borrow_id bid0 bid1 in (* If we don't check for equivalence (i.e., we apply a fixed-point), we lookup the shared values and match them. @@ -1888,6 +1905,14 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct else let v0 = S.lookup_shared_value_in_ctx0 bid0 in let v1 = S.lookup_shared_value_in_ctx1 bid1 in + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_shared_borrows: looked up values:" + ^ "sv0: " + ^ typed_value_to_string S.ctx v0 + ^ ", sv1: " + ^ typed_value_to_string S.ctx v1)); + let _ = match_typed_values v0 v1 in () in @@ -1914,14 +1939,24 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct let id0 = sv0.sv_id in let id1 = sv1.sv_id in + log#ldebug + (lazy + ("MakeCheckEquivMatcher: match_symbolic_values: " ^ "sv0: " + ^ V.SymbolicValueId.to_string id0 + ^ ", sv1: " + ^ V.SymbolicValueId.to_string id1)); + (* If we don't check for equivalence, we also update the map from sids to values *) if S.check_equiv then (* Create the joined symbolic value *) - let sv_id = GetSetSid.match_e S.sid_map id0 id1 in + let sv_id = + GetSetSid.match_e "match_symbolic_values: ids: " S.sid_map id0 id1 + in let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in let sv_kind = - if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind else raise Distinct + if sv0.V.sv_kind = sv1.V.sv_kind then sv0.V.sv_kind + else raise (Distinct "match_symbolic_values: sv_kind") in let sv = { V.sv_id; sv_ty; sv_kind } in sv @@ -1942,7 +1977,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct let match_symbolic_with_other (left : bool) (sv : V.symbolic_value) (v : V.typed_value) : V.typed_value = - if S.check_equiv then raise Distinct + if S.check_equiv then raise (Distinct "match_symbolic_with_other") else ( assert left; let id = sv.sv_id in @@ -1963,9 +1998,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct a continue, where the fixed point contains some bottom values. *) if left && not (value_has_loans_or_borrows S.ctx v.V.value) then mk_bottom v.V.ty - else raise Distinct + else raise (Distinct "match_bottom_with_other") - let match_distinct_aadts _ _ _ _ _ = raise Distinct + let match_distinct_aadts _ _ _ _ _ = raise (Distinct "match_distinct_adts") let match_ashared_borrows _ty0 bid0 _ty1 bid1 ty = let bid = match_borrow_id bid0 bid1 in @@ -2001,7 +2036,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct ^ typed_avalue_to_string S.ctx v0 ^ "\n- v1: " ^ typed_avalue_to_string S.ctx v1)); - raise Distinct + raise (Distinct "match_avalues") end (** See {!match_ctxs} *) @@ -2154,7 +2189,8 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) in let _ = CEM.match_aid abs_id0 abs_id1 in - if kind0 <> kind1 || can_end0 <> can_end1 then raise Distinct; + if kind0 <> kind1 || can_end0 <> can_end1 then + raise (Distinct "match_abstractions: kind or can_end"); let _ = CEM.match_aids parents0 parents1 in let _ = CEM.match_aidl original_parents0 original_parents1 in let _ = CEM.match_rids regions0 regions1 in @@ -2192,21 +2228,19 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) match (env0, env1) with | ( C.Var (C.DummyBinder b0, v0) :: env0', C.Var (C.DummyBinder b1, v1) :: env1' ) -> - (* Two cases: the dummy value is an old value, in which case the bindings - must be the same and their values equal (and the borrows/loans/symbolic - values they reference must be fixed) *) + (* Sanity check: if the dummy value is an old value, the bindings must + be the same and their values equal (and the borrows/loans/symbolic *) if C.DummyVarId.Set.mem b0 fixed_ids.dids then ( (* Fixed values: the values must be equal *) assert (b0 = b1); assert (v0 = v1); (* The ids present in the left value must be fixed *) let ids, _ = compute_typed_value_ids v0 in - assert ((not S.check_equiv) || ids_are_fixed ids); - (* Continue *) - match_envs env0' env1') - else - let _ = M.match_typed_values ctx v0 v1 in - match_envs env0' env1' + assert ((not S.check_equiv) || ids_are_fixed ids)); + (* We still match the values - allows to compute mappings (which + are the identity actually) *) + let _ = M.match_typed_values ctx v0 v1 in + match_envs env0' env1' | C.Var (C.VarBinder b0, v0) :: env0', C.Var (C.VarBinder b1, v1) :: env1' -> assert (b0 = b1); @@ -2238,7 +2272,7 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) () | _ -> (* The elements don't match *) - raise Distinct + raise (Distinct "match_ctxs: match_envs: env elements don't match") in (* Match the environments. @@ -2267,7 +2301,9 @@ let match_ctxs (check_equiv : bool) (fixed_ids : ids_sets) } in Some maps - with Distinct -> None + with Distinct msg -> + log#ldebug (lazy ("match_ctxs: distinct: " ^ msg)); + None (** Compute whether two contexts are equivalent modulo an identifier substitution. @@ -2350,17 +2386,6 @@ let loop_join_origin_with_continue_ctxs (config : C.config) ("loop_join_origin_with_continue_ctxs:join_one: initial ctx:\n" ^ eval_ctx_to_string ctx)); - (* (* Push the abstractions introduced by {!prepare_shared_loans} as - far as we can to preserve the structure of the context. *) - let ctx = - push_fresh_shared_loans_abs fresh_shared_loans_abs_ids original_ctx_length - ctx - in - log#ldebug - (lazy - ("loop_join_origin_with_continue_ctxs:join_one: after push fresh \ - shared loan abs:\n" ^ eval_ctx_to_string ctx)); *) - (* Destructure the abstractions introduced in the new context *) let ctx = destructure_new_abs loop_id fixed_ids.aids ctx in log#ldebug @@ -2435,9 +2460,40 @@ let loop_join_origin_with_continue_ctxs (config : C.config) We do this because it makes it easier to compute joins and fixed points. We return the new context and the set of fresh abs ids. + + **REMARK**: + As a side note, only reborrow the loan ids whose corresponding borrows appear in + values (i.e., not in abstractions). + + For instance, if we have: + {[ + abs'0 { + SL {l0} s0 + SL {l1} s1 + } + abs'1 { SB l0 } + x -> SB l1 + ]} + + we only introduce a fresh abstraction for [l1]. + *) +let prepare_ashared_loans (loop_id : V.LoopId.id option) : cm_fun = + fun cf ctx0 -> + let ctx = ctx0 in + (* Compute the set of borrows which appear in the abstractions, so that + we can filter the borrows that we reborrow. *) -let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : - C.eval_ctx * V.AbstractionId.Set.t = + let absl = + List.filter_map + (function C.Var _ | C.Frame -> None | C.Abs abs -> Some abs) + ctx.env + in + let absl_ids, absl_id_maps = compute_absl_ids absl in + let abs_borrow_ids = absl_ids.borrow_ids in + + (* Map from the fresh sids to the original symbolic values *) + let sid_subst = ref [] in + (* Return the same value but where: - the shared loans have been removed - the symbolic values have been replaced with fresh symbolic values @@ -2453,7 +2509,11 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : (fun r -> if T.RegionId.Set.mem r rids then nrid else r) (fun x -> x) (fun x -> x) - (fun _ -> C.fresh_symbolic_value_id ()) + (fun id -> + let nid = C.fresh_symbolic_value_id () in + let sv = V.SymbolicValueId.Map.find id absl_id_maps.sids_to_values in + sid_subst := (nid, sv) :: !sid_subst; + nid) (fun x -> x) v in @@ -2522,7 +2582,11 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : (* Create the abstraction *) let avalues = [ borrow_value; loan_value ] in - let kind = V.Loop (loop_id, None, V.LoopSynthInput) in + let kind = + match loop_id with + | Some loop_id -> V.Loop (loop_id, None, V.LoopSynthInput) + | None -> V.Identity + in let can_end = true in let fresh_abs = { @@ -2546,26 +2610,30 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : when necessary. *) let collect_shared_values_in_abs (abs : V.abs) : unit = + let collect_shared_value lids (sv : V.typed_value) = + (* Sanity check: we don't support nested borrows for now *) + assert (not (value_has_borrows ctx sv.V.value)); + + (* Filter the loan ids whose corresponding borrows appear in abstractions + (see the documentation of the function) *) + let lids = V.BorrowId.Set.diff lids abs_borrow_ids in + + (* Generate fresh borrows and values *) + V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids + in + let visit_avalue = object inherit [_] V.iter_typed_avalue as super method! visit_SharedLoan env lids sv = - (* Sanity check: we don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.V.value)); - - (* Generate fresh borrows and values *) - V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids; + collect_shared_value lids sv; (* Continue the exploration *) super#visit_SharedLoan env lids sv method! visit_ASharedLoan env lids sv _ = - (* Sanity check: we don't support nested borrows for now *) - assert (not (value_has_borrows ctx sv.V.value)); - - (* Generate fresh borrows and values *) - V.BorrowId.Set.iter (push_abs_for_shared_value abs sv) lids; + collect_shared_value lids sv; (* Continue the exploration *) super#visit_SharedLoan env lids sv @@ -2635,14 +2703,30 @@ let prepare_ashared_loans (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : in (* Add the abstractions *) - let fresh_abs_ids = - V.AbstractionId.Set.of_list (List.map (fun abs -> abs.V.abs_id) !fresh_absl) - in let fresh_absl = List.map (fun abs -> C.Abs abs) !fresh_absl in let env = List.append fresh_absl env in - - (* Return *) - ({ ctx with C.env }, fresh_abs_ids) + let ctx = { ctx with env } in + + let _, new_ctx_ids_map = compute_context_ids ctx in + + (* Synthesize *) + match cf ctx with + | None -> None + | Some e -> + (* Add the let-bindings which introduce the fresh symbolic values *) + Some + (List.fold_left + (fun e (sid, v) -> + let v = mk_typed_value_from_symbolic_value v in + let sv = + V.SymbolicValueId.Map.find sid new_ctx_ids_map.sids_to_values + in + SymbolicAst.IntroSymbolic (ctx, None, sv, v, e)) + e !sid_subst) + +let prepare_ashared_loans_no_synth (loop_id : V.LoopId.id) (ctx : C.eval_ctx) : + C.eval_ctx = + get_cf_ctx_no_synth (prepare_ashared_loans (Some loop_id)) ctx (** Compute a fixed-point for the context at the entry of the loop. We also return the sets of fixed ids, and the list of symbolic values @@ -2669,7 +2753,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) For more details, see the comments for {!prepare_ashared_loans} *) - let ctx, _ = prepare_ashared_loans loop_id ctx0 in + let ctx = prepare_ashared_loans_no_synth loop_id ctx0 in (* Debug *) log#ldebug @@ -2935,9 +3019,23 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id) (* Retrieve the first id of the group *) match ids with | [] -> - (* This would be rather unexpected... let's fail for now to see - in which situations this happens *) - raise (Failure "Unexpected") + (* This happens for instance in the following case (there + is no "magic wand" linking the values before and after + the loop, in particular because we return nothing): + + Example: + ======== + {[ + fn clear(v: &mut Vec<u32>) { + let mut i = 0; + while i < v.len() { + v[i] = 0; + i += 1; + } + } + ]} + *) + () | id0 :: ids -> let id0 = ref id0 in (* Add the proper region group into the abstraction *) @@ -3072,6 +3170,7 @@ type borrow_loan_corresp = { borrow_to_loan_id_map : V.BorrowId.InjSubst.t; loan_to_borrow_id_map : V.BorrowId.InjSubst.t; } +[@@deriving show] let ids_sets_empty_borrows_loans (ids : ids_sets) : ids_sets = let { aids; blids = _; borrow_ids = _; loan_ids = _; dids; rids; sids } = @@ -3442,10 +3541,14 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets) **Parameters**: [is_loop_entry]: [true] if first entry into the loop, [false] if re-entry (i.e., continue). + [fp_input_svalues]: the list of symbolic values appearing in the fixed + point and which must be instantiated during the match (this is the list + of input parameters of the loop). *) let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) (is_loop_entry : bool) (fp_bl_maps : borrow_loan_corresp) - (fixed_ids : ids_sets) (src_ctx : C.eval_ctx) : st_cm_fun = + (fp_input_svalues : V.SymbolicValueId.id list) (fixed_ids : ids_sets) + (src_ctx : C.eval_ctx) : st_cm_fun = fun cf tgt_ctx -> (* Debug *) log#ldebug @@ -3543,10 +3646,14 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) we substitute the loans and introduce fresh ids for the borrows, symbolic values, etc. About the *identity abstractions*, see the comments for [compute_fixed_point_id_correspondance]. + + TODO: this whole thing is very technical and error-prone. + We should rely on a more primitive and safer function + [add_identity_abs] to add the identity abstractions one by one. *) let cf_introduce_loop_fp_abs : m_fun = fun tgt_ctx -> - (* Match the tgt and target contexts *) + (* Match the source and target contexts *) let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in let filt_src_env, new_absl, new_dummyl = ctx_split_fixed_new fixed_ids src_ctx @@ -3555,8 +3662,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) let filt_tgt_ctx = { tgt_ctx with env = filt_tgt_env } in let filt_src_ctx = { src_ctx with env = filt_src_env } in - let check_equiv = false in let src_to_tgt_maps = + let check_equiv = false in let fixed_ids = ids_sets_empty_borrows_loans fixed_ids in let open InterpreterBorrowsCore in let lookup_shared_loan lid ctx : V.typed_value = @@ -3567,6 +3674,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) in let lookup_in_src id = lookup_shared_loan id src_ctx in let lookup_in_tgt id = lookup_shared_loan id tgt_ctx in + (* Match *) Option.get (match_ctxs check_equiv fixed_ids lookup_in_src lookup_in_tgt filt_src_ctx filt_tgt_ctx) @@ -3581,12 +3689,17 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) (* Debug *) log#ldebug (lazy - ("match_ctx_with_target:cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: " + ("match_ctx_with_target: cf_introduce_loop_fp_abs:" ^ "\n\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx ^ "\n\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n\n- filt_tgt_ctx: " - ^ eval_ctx_to_string filt_tgt_ctx + ^ eval_ctx_to_string_no_filter filt_tgt_ctx ^ "\n\n- filt_src_ctx: " - ^ eval_ctx_to_string filt_src_ctx + ^ eval_ctx_to_string_no_filter filt_src_ctx + ^ "\n\n- new_absl:\n" + ^ eval_ctx_to_string + { src_ctx with C.env = List.map (fun abs -> C.Abs abs) new_absl } + ^ "\n\n- fixed_ids:\n" ^ show_ids_sets fixed_ids ^ "\n\n- fp_bl_maps:\n" + ^ show_borrow_loan_corresp fp_bl_maps ^ "\n\n- src_to_tgt_maps: " ^ show_ids_maps src_to_tgt_maps)); @@ -3618,8 +3731,8 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) } ]} - Through matching, we detected that in [env_fp], [l1] will be matched - to [l5]. We introduced a fresh borrow [l6] for [l1], and remember + Through matching, we detect that in [env_fp], [l1] is matched + to [l5]. We introduce a fresh borrow [l6] for [l1], and remember in the map [src_fresh_borrows_map] that: [{ l1 -> l6}]. We get: @@ -3638,6 +3751,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) abs@2 { MB l5, ML l6 } ]} *) + (* First, compute the set of borrows which appear in the fresh abstractions + of the fixed-point: we want to introduce fresh ids only for those. *) + let new_absl_ids, _ = compute_absl_ids new_absl in let src_fresh_borrows_map = ref V.BorrowId.Map.empty in let visit_tgt = object @@ -3646,8 +3762,13 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) method! visit_borrow_id _ id = (* Map the borrow, if it needs to be mapped *) if + (* We map the borrows for which we computed a mapping *) V.BorrowId.InjSubst.Set.mem id (V.BorrowId.InjSubst.elements src_to_tgt_maps.borrow_id_map) + (* And which have corresponding loans in the fresh fixed-point abstractions *) + && V.BorrowId.Set.mem + (V.BorrowId.Map.find id tgt_to_src_borrow_map) + new_absl_ids.loan_ids then ( let src_id = V.BorrowId.Map.find id tgt_to_src_borrow_map in let nid = C.fresh_borrow_id () in @@ -3659,6 +3780,13 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) in let tgt_ctx = visit_tgt#visit_eval_ctx () tgt_ctx in + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + src_fresh_borrows_map:\n" + ^ V.BorrowId.Map.show V.BorrowId.to_string !src_fresh_borrows_map + ^ "\n")); + (* Rem.: we don't update the symbolic values. It is not necessary because there shouldn't be any symbolic value containing borrows. @@ -3695,21 +3823,54 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) inherit [_] C.map_eval_ctx as super method! visit_borrow_id _ bid = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_borrow_id: " ^ V.BorrowId.to_string bid ^ "\n")); + (* Lookup the id of the loan corresponding to this borrow *) let src_lid = V.BorrowId.InjSubst.find bid fp_bl_maps.borrow_to_loan_id_map in + + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + src_lid: " + ^ V.BorrowId.to_string src_lid + ^ "\n")); + (* Lookup the tgt borrow id to which this borrow was mapped *) let tgt_bid = V.BorrowId.InjSubst.find src_lid src_to_tgt_maps.borrow_id_map in + + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: looked up \ + tgt_bid: " + ^ V.BorrowId.to_string tgt_bid + ^ "\n")); + tgt_bid method! visit_loan_id _ id = + log#ldebug + (lazy + ("match_ctx_with_target: cf_introduce_loop_fp_abs: \ + visit_loan_id: " ^ V.BorrowId.to_string id ^ "\n")); (* Map the borrow - rem.: we mapped the borrows *in the values*, meaning we know how to map the *corresponding loans in the abstractions* *) - V.BorrowId.Map.find id !src_fresh_borrows_map + match V.BorrowId.Map.find_opt id !src_fresh_borrows_map with + | None -> + (* No mapping: this means that the borrow was mapped when + we matched values (it doesn't come from a fresh abstraction) + and because of this, it should actually be mapped to itself *) + assert ( + V.BorrowId.InjSubst.find id src_to_tgt_maps.borrow_id_map = id); + id + | Some id -> id method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id () method! visit_abstraction_id _ _ = C.fresh_abstraction_id () @@ -3752,7 +3913,15 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id) let cc = InterpreterBorrows.end_borrows config new_borrows in (* Compute the loop input values *) - let input_values = src_to_tgt_maps.sid_to_value_map in + let input_values = + V.SymbolicValueId.Map.of_list + (List.map + (fun sid -> + ( sid, + V.SymbolicValueId.Map.find sid src_to_tgt_maps.sid_to_value_map + )) + fp_input_svalues) + in (* Continue *) cc @@ -3812,6 +3981,95 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun = (* Apply *) eval_loop_body reeval_loop_body ctx +(** Compute the set of "quantified" symbolic value ids in a fixed-point context. + + We compute: + - the set of symbolic value ids that are freshly introduced + - the list of input symbolic values + *) +let compute_fp_ctx_symbolic_values (ctx : C.eval_ctx) (fp_ctx : C.eval_ctx) : + V.SymbolicValueId.Set.t * V.symbolic_value list = + let old_ids, _ = compute_context_ids ctx in + let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in + let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in + + (* Compute the set of symbolic values which appear in shared values inside + *fixed* abstractions: because we introduce fresh abstractions and reborrows + with {!prepare_ashared_loans}, those values are never accessed directly + inside the loop iterations: we can ignore them (and should, because + otherwise it leads to a very ugly translation with duplicated, unused + values) *) + let shared_sids_in_fixed_abs = + let fixed_absl = + List.filter + (fun (ee : C.env_elem) -> + match ee with + | C.Var _ | C.Frame -> false + | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids) + ctx.env + in + + (* Rem.: as we greedily expand the symbolic values containing borrows, and + in particular the (mutable/shared) borrows, we could simply list the + symbolic values appearing in the abstractions: those are necessarily + shared values. We prefer to be more general, in prevision of later + changes. + *) + let sids = ref V.SymbolicValueId.Set.empty in + let visitor = + object (self : 'self) + inherit [_] C.iter_env + + method! visit_ASharedLoan inside_shared _ sv child_av = + self#visit_typed_value true sv; + self#visit_typed_avalue inside_shared child_av + + method! visit_symbolic_value_id inside_shared sid = + if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids + end + in + visitor#visit_env false fixed_absl; + !sids + in + + (* Remove the shared symbolic values present in the fixed abstractions - + see comments for [shared_sids_in_fixed_abs]. *) + let sids_to_values = fp_ids_maps.sids_to_values in + + log#ldebug + (lazy + ("compute_fp_ctx_symbolic_values:" ^ "\n- shared_sids_in_fixed_abs:" + ^ V.SymbolicValueId.Set.show shared_sids_in_fixed_abs + ^ "\n- all_sids_to_values: " + ^ V.SymbolicValueId.Map.show (symbolic_value_to_string ctx) sids_to_values + ^ "\n")); + + let sids_to_values = + V.SymbolicValueId.Map.filter + (fun sid _ -> + not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs)) + sids_to_values + in + + (* The value ids should be listed in increasing order *) + let input_svalues = + List.map snd (V.SymbolicValueId.Map.bindings sids_to_values) + in + + log#ldebug + (lazy + ("compute_fp_ctx_symbolic_values:" ^ "\n- src context:\n" + ^ eval_ctx_to_string_no_filter ctx + ^ "\n- fixed point:\n" + ^ eval_ctx_to_string_no_filter fp_ctx + ^ "\n- fresh_sids: " + ^ V.SymbolicValueId.Set.show fresh_sids + ^ "\n- input_svalues: " + ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues + ^ "\n\n")); + + (fresh_sids, input_svalues) + (** Evaluate a loop in symbolic mode *) let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = @@ -3820,14 +4078,9 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : log#ldebug (lazy ("eval_loop_symbolic:\nContext:\n" ^ eval_ctx_to_string ctx ^ "\n\n")); - (* Compute a fresh loop id *) + (* Generate a fresh loop id *) let loop_id = C.fresh_loop_id () in - log#ldebug - (lazy - ("eval_loop_symbolic:\nContext after shared borrows preparation:\n" - ^ eval_ctx_to_string ctx ^ "\n\n")); - (* Compute the fixed point at the loop entrance *) let fp_ctx, fixed_ids = compute_loop_entry_fixed_point config loop_id eval_loop_body ctx @@ -3839,6 +4092,10 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : ("eval_loop_symbolic:\nInitial context:\n" ^ eval_ctx_to_string ctx ^ "\n\nFixed point:\n" ^ eval_ctx_to_string fp_ctx)); + (* 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 + (* 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 will end with a call to the loop translation @@ -3847,8 +4104,8 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx in let end_expr = - match_ctx_with_target config loop_id true fp_bl_corresp fixed_ids fp_ctx cf - ctx + match_ctx_with_target config loop_id true fp_bl_corresp fp_input_svalues + fixed_ids fp_ctx cf ctx in (* Synthesize the loop body by evaluating it, with the continuation for @@ -3869,8 +4126,8 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : (* We don't support nested loops for now *) assert (i = 0); let cc = - match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids - fp_ctx + match_ctx_with_target config loop_id false fp_bl_corresp + fp_input_svalues fixed_ids fp_ctx in cc cf ctx | Unit | LoopReturn _ | EndEnterLoop _ | EndContinue _ -> @@ -3881,75 +4138,18 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) : in let loop_expr = eval_loop_body cf_loop fp_ctx in - (* Compute the list of fresh symbolic values *) - let fresh_sids, input_svalues = - let old_ids, _ = compute_context_ids ctx in - let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in - let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in - - (* Compute the set of symbolic values which appear in shared values inside - *fixed* abstractions: because we introduce fresh abstractions and reborrows - with {!prepare_ashared_loans}, those values are never accessed directly - inside the loop iterations: we can ignore them (and should, because - otherwise it leads to a very ugly translation with duplicated, unused - values) *) - let shared_sids_in_fixed_abs = - let fixed_absl = - List.filter - (fun (ee : C.env_elem) -> - match ee with - | C.Var _ | C.Frame -> false - | Abs abs -> V.AbstractionId.Set.mem abs.abs_id old_ids.aids) - ctx.env - in - - (* Rem.: as we greedily expand the symbolic values containing borrows, and - in particular the (mutable/shared) borrows, we could simply list the - symbolic values appearing in the abstractions: those are necessarily - shared values. We prefer to be more general, in prevision of later - changes. - *) - let sids = ref V.SymbolicValueId.Set.empty in - let visitor = - object (self : 'self) - inherit [_] C.iter_env - - method! visit_ASharedLoan inside_shared _ sv child_av = - self#visit_typed_value true sv; - self#visit_typed_avalue inside_shared child_av - - method! visit_symbolic_value_id inside_shared sid = - if inside_shared then sids := V.SymbolicValueId.Set.add sid !sids - end - in - visitor#visit_env false fixed_absl; - !sids - in - - (* Remove the shared symbolic values present in the fixed abstractions - - see comments for [shared_sids_in_fixed_abs]. *) - let sids_to_values = fp_ids_maps.sids_to_values in - let sids_to_values = - V.SymbolicValueId.Map.filter - (fun sid _ -> - not (V.SymbolicValueId.Set.mem sid shared_sids_in_fixed_abs)) - sids_to_values - in - (* The value ids should be listed in increasing order *) - let input_svalues = - List.map snd (V.SymbolicValueId.Map.bindings sids_to_values) - in - (fresh_sids, input_svalues) - in - log#ldebug (lazy ("eval_loop_symbolic: result:" ^ "\n- src context:\n" - ^ eval_ctx_to_string ctx ^ "\n- fixed point:\n" ^ eval_ctx_to_string fp_ctx - ^ "\n- fixed_sids: " + ^ eval_ctx_to_string_no_filter ctx + ^ "\n- fixed point:\n" + ^ eval_ctx_to_string_no_filter fp_ctx + ^ "\n- fixed_sids: " ^ V.SymbolicValueId.Set.show fixed_ids.sids - ^ "\n- input_svalues: " + ^ "\n- fresh_sids: " ^ V.SymbolicValueId.Set.show fresh_sids + ^ "\n- input_svalues: " + ^ Print.list_to_string (symbolic_value_to_string ctx) input_svalues ^ "\n\n")); (* Put together *) @@ -3960,4 +4160,24 @@ let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun = fun cf ctx -> match config.C.mode with | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx - | SymbolicMode -> eval_loop_symbolic config eval_loop_body cf ctx + | SymbolicMode -> + (* We want to make sure the loop will *not* manipulate shared avalues + containing themselves shared loans (i.e., nested shared loans in + the abstractions), because it complexifies the matches between values + (when joining environments, or checking that two environments are + equivalent). + + We thus call {!prepare_ashared_loans} once *before* diving into + the loop, to make sure the shared values are deconstructed. + + Note that we will call this function again inside {!eval_loop_symbolic}, + to introduce fresh, non-fixed abstractions containing the shared values + which can be manipulated (and thus borrowed, expanded, etc.) so + that the fixed abstractions are never modified. + + This is important to understand: we call this function once here to + introduce *fixed* abstractions, and again later to introduce + *non-fixed* abstractions. + *) + let cc = prepare_ashared_loans None in + comp cc (eval_loop_symbolic config eval_loop_body) cf ctx diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml index fe508f6b..f5b1111e 100644 --- a/compiler/InterpreterStatements.ml +++ b/compiler/InterpreterStatements.ml @@ -811,12 +811,12 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun = let expr = assign_to_place config rv p (cf Unit) ctx in (* Update the synthesized AST - here we store meta-information. * We do it only in specific cases (it is not always useful, and - * also it can lead to issues - for instance, if we borrow an + * also it can lead to issues - for instance, if we borrow a * reserved borrow, we later can't translate it to pure values...) *) match rvalue with | E.Global _ -> raise (Failure "Unreachable") | E.Use _ - | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut)) + | E.Ref (_, (E.Shared | E.Mut | E.TwoPhaseMut | E.Shallow)) | E.UnaryOp _ | E.BinaryOp _ | E.Discriminant _ | E.Aggregate _ -> let rp = rvalue_get_place rvalue in diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml index 670435a5..d60ddfe6 100644 --- a/compiler/InterpreterUtils.ml +++ b/compiler/InterpreterUtils.ml @@ -8,9 +8,22 @@ module L = Logging open Utils open TypesUtils module PA = Print.EvalCtxLlbcAst +open Cps (** Some utilities *) +(** Auxiliary function - call a function which requires a continuation, + and return the let context given to the continuation *) +let get_cf_ctx_no_synth (f : cm_fun) (ctx : C.eval_ctx) : C.eval_ctx = + let nctx = ref None in + let cf ctx = + assert (!nctx = None); + nctx := Some ctx; + None + in + let _ = f cf ctx in + Option.get !nctx + let eval_ctx_to_string_no_filter = Print.Contexts.eval_ctx_to_string_no_filter let eval_ctx_to_string = Print.Contexts.eval_ctx_to_string let ety_to_string = PA.ety_to_string @@ -368,12 +381,16 @@ let compute_absl_ids (xl : V.abs list) : ids_sets * ids_to_values = let compute_abs_ids (x : V.abs) : ids_sets * ids_to_values = compute_absl_ids [ x ] -(** Compute the sets of ids found in an environment element. *) -let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values = +(** Compute the sets of ids found in an environment. *) +let compute_env_ids (x : C.env) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in - compute#visit_env_elem () x; + compute#visit_env () x; (get_ids (), get_ids_to_values ()) +(** Compute the sets of ids found in an environment element. *) +let compute_env_elem_ids (x : C.env_elem) : ids_sets * ids_to_values = + compute_env_ids [ x ] + (** Compute the sets of ids found in a list of contexts. *) let compute_contexts_ids (ctxl : C.eval_ctx list) : ids_sets * ids_to_values = let compute, get_ids, get_ids_to_values = compute_ids () in diff --git a/compiler/Invariants.ml b/compiler/Invariants.ml index c69e6441..981c2c46 100644 --- a/compiler/Invariants.ml +++ b/compiler/Invariants.ml @@ -784,7 +784,7 @@ let check_symbolic_values (ctx : C.eval_ctx) : unit = let check_invariants (ctx : C.eval_ctx) : unit = if !Config.check_invariants then ( - log#ldebug (lazy "Checking invariants"); + log#ldebug (lazy ("Checking invariants:\n" ^ eval_ctx_to_string ctx)); check_loans_borrows_relation_invariant ctx; check_borrowed_values_invariant ctx; check_typing_invariant ctx; diff --git a/compiler/Print.ml b/compiler/Print.ml index d040680f..cf227172 100644 --- a/compiler/Print.ml +++ b/compiler/Print.ml @@ -315,6 +315,7 @@ module Values = struct ^ ", loop abs kind: " ^ loop_abs_kind_to_string abs_kind ^ ")" + | Identity -> "Identity" let abs_to_string (fmt : value_formatter) (verbose : bool) (indent : string) (indent_incr : string) (abs : V.abs) : string = diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index 33082dc3..de68adc3 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -426,7 +426,7 @@ let fun_suffix (lp_id : LoopId.id option) (rg_id : T.RegionGroupId.id option) : let lp_suff = match lp_id with | None -> "" - | Some lp_id -> "^loop^" ^ LoopId.to_string lp_id + | Some lp_id -> "^loop" ^ LoopId.to_string lp_id in let rg_suff = diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml index 4ecb194b..7f682c9c 100644 --- a/compiler/SymbolicAst.ml +++ b/compiler/SymbolicAst.ml @@ -160,6 +160,22 @@ type expression = We use it to compute meaningful names for the variables we introduce, to prettify the generated code. *) + | IntroSymbolic of + Contexts.eval_ctx + * mplace option + * V.symbolic_value + * V.typed_value + * expression + (** We introduce a new symbolic value, equal to some other value. + + This is used for instance when reorganizing the environment to compute + fixed points: we duplicate some shared symbolic values to destructure + the shared values, in order to make the environment a bit more general + (while losing precision of course). + + The context is the evaluation context from before introducing the new + value. It has the same purpose as for the {!Return} case. + *) | ForwardEnd of Contexts.eval_ctx * V.typed_value symbolic_value_id_map option diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 174fc4d1..b2b5e010 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1278,6 +1278,8 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression = | EvalGlobal (gid, sv, e) -> translate_global_eval gid sv e ctx | Assertion (ectx, v, e) -> translate_assertion ectx v e ctx | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx + | IntroSymbolic (ectx, p, sv, v, e) -> + translate_intro_symbolic ectx p sv v e ctx | Meta (meta, e) -> translate_meta meta e ctx | ForwardEnd (ectx, loop_input_values, e, back_e) -> translate_forward_end ectx loop_input_values e back_e ctx @@ -1521,6 +1523,7 @@ and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs) | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id | V.Loop (loop_id, rg_id, abs_kind) -> translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind + | V.Identity -> translate_end_abstraction_identity ectx abs e ctx and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression @@ -1707,6 +1710,20 @@ and translate_end_abstraction_fun_call (ectx : C.eval_ctx) (abs : V.abs) next_e) else mk_let effect_info.can_fail output call next_e +and translate_end_abstraction_identity (ectx : C.eval_ctx) (abs : V.abs) + (e : S.expression) (ctx : bs_ctx) : texpression = + (* We simply check that the abstraction only contains shared borrows/loans, + and translate the next expression *) + + (* We can do this simply by checking that it consumes and gives back nothing *) + let inputs = abs_to_consumed ctx ectx abs in + let ctx, outputs = abs_to_given_back None abs ctx in + assert (inputs = []); + assert (outputs = []); + + (* Translate the next expression *) + translate_expression e ctx + and translate_end_abstraction_synth_ret (ectx : C.eval_ctx) (abs : V.abs) (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression = @@ -2087,6 +2104,25 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) List.for_all (fun (br : match_branch) -> br.branch.ty = ty) branches); { e; ty } +and translate_intro_symbolic (ectx : C.eval_ctx) (p : S.mplace option) + (sv : V.symbolic_value) (v : V.typed_value) (e : S.expression) + (ctx : bs_ctx) : texpression = + let mplace = translate_opt_mplace p in + + (* Introduce a fresh variable for the symbolic value *) + let ctx, var = fresh_var_for_symbolic_value sv ctx in + + (* Translate the value *) + let v = typed_value_to_texpression ctx ectx v in + + (* Translate the next expression *) + let next_e = translate_expression e ctx in + + (* Make the let-binding *) + let monadic = false in + let var = mk_typed_pattern_from_var var mplace in + mk_let monadic var v next_e + and translate_forward_end (ectx : C.eval_ctx) (loop_input_values : V.typed_value S.symbolic_value_id_map option) (e : S.expression) (back_e : S.expression S.region_group_id_map) @@ -2129,12 +2165,19 @@ and translate_forward_end (ectx : C.eval_ctx) ^ "\n- loop_info.input_svl:\n" ^ Print.list_to_string (symbolic_value_to_string ctx) - loop_info.input_svl)); + loop_info.input_svl + ^ "\n")); (* Translate the input values *) let loop_input_values = List.map - (fun sv -> V.SymbolicValueId.Map.find sv.V.sv_id loop_input_values) + (fun sv -> + log#ldebug + (lazy + ("translate_forward_end: looking up input_svl: " + ^ V.SymbolicValueId.to_string sv.V.sv_id + ^ "\n")); + V.SymbolicValueId.Map.find sv.V.sv_id loop_input_values) loop_info.input_svl in let args = @@ -2218,8 +2261,12 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression = in log#ldebug (lazy - ("translate_loop:" ^ "\n- filtered svl: " - ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl)); + ("translate_loop:" ^ "\n- input_svalues: " + ^ (Print.list_to_string (symbolic_value_to_string ctx)) + loop.input_svalues + ^ "\n- filtered svl: " + ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl + ^ "\n")); let ctx, _ = fresh_vars_for_symbolic_values svl ctx in ctx in @@ -2384,7 +2431,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl = ^ Print.fun_name_to_string def.A.name ^ " (" ^ Print.option_to_string T.RegionGroupId.to_string bid - ^ ")")); + ^ ")\n")); (* Translate the declaration *) let def_id = def.A.def_id in diff --git a/compiler/Values.ml b/compiler/Values.ml index 7d5ecc01..d4eff58a 100644 --- a/compiler/Values.ml +++ b/compiler/Values.ml @@ -939,6 +939,13 @@ type abs_kind = After we computed a fixed point, we give a unique region group identifier for each loop abstraction. *) + | Identity + (** An identity abstraction, which only consumes and provides shared + borrows/loans. + + We introduce them to abstract the context a bit, for instance + to compute fixed-points. + *) [@@deriving show, ord] (** Ancestor for {!abs} iter visitor *) |