From dcf8866ec52adfe2ae471a9cc3054825f13adc93 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 15 Jun 2020 15:42:03 -0700 Subject: [PATCH] [sledge] Change: Store inverted Domain_sh.from_call.subst, and clarify Summary: `Domain_sh.from_call.subst` is a substitution that replaces shadowed variables with fresh ones, which is constructed by `Domain_sh.call` and used by `Domain_sh.retn`, after inverting it. This patch changes the stored substitution to the inverted one, and renames it to `unshadow` for clarity. After this change, the stored substitutions have the property that they map variables to program variables. This is desirable since it avoids the question about the uninverted substitution of whether the variables in the range of the uninverted substitution are "fresh". Reviewed By: jvillard Differential Revision: D21974020 fbshipit-source-id: d469c89f9 --- sledge/src/domain_sh.ml | 42 ++++++++++++++++++++--------------------- 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml index 86070e330..0f1182c1e 100644 --- a/sledge/src/domain_sh.ml +++ b/sledge/src/domain_sh.ml @@ -124,7 +124,7 @@ let and_eqs sub formals actuals q = in List.fold2_exn ~f:and_eq formals actuals ~init:q -let localize_entry globals actuals formals freturn locals subst pre entry = +let localize_entry globals actuals formals freturn locals shadow pre entry = (* Add the formals here to do garbage collection and then get rid of them *) let formals_set = Var.Set.of_list formals in let freturn_locals = @@ -143,11 +143,11 @@ let localize_entry globals actuals formals freturn locals subst pre entry = fail "Solver couldn't infer frame of a garbage-collected pre" () in let q'' = - Sh.extend_us freturn_locals (and_eqs subst formals actuals foot) + Sh.extend_us freturn_locals (and_eqs shadow formals actuals foot) in (q'', frame) -type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t} +type from_call = {areturn: Var.t option; unshadow: Var.Subst.t; frame: Sh.t} [@@deriving compare, equal, sexp] (** Express formula in terms of formals instead of actuals, and enter scope @@ -175,12 +175,13 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = not need to be saved in the freshening renaming *) let q = Sh.exists modifs q in (* save current values of shadowed formals and locals with a renaming *) - let q', subst = + let q', shadow = Sh.freshen q ~wrt:(Var.Set.add_list formals freturn_locals) in - assert (Var.Set.disjoint modifs (Var.Subst.domain subst)) ; + let unshadow = Var.Subst.invert shadow in + assert (Var.Set.disjoint modifs (Var.Subst.domain shadow)) ; (* pass arguments by conjoining equations between formals and actuals *) - let entry = and_eqs subst formals actuals q' in + let entry = and_eqs shadow formals actuals q' in (* note: locals and formals are in scope *) assert ( Var.Set.is_subset @@ -188,16 +189,16 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q = ~of_:entry.us ) ; (* simplify *) let entry = simplify entry in - ( if not summaries then (entry, {areturn; subst; frame= Sh.emp}) + ( if not summaries then (entry, {areturn; unshadow; frame= Sh.emp}) else let q'', frame = - localize_entry globals actuals formals freturn locals subst q' entry + localize_entry globals actuals formals freturn locals shadow q' entry in - (q'', {areturn; subst; frame}) ) + (q'', {areturn; unshadow; frame}) ) |> - [%Trace.retn fun {pf} (entry, {subst; frame}) -> - pf "@[subst: %a@ frame: %a@ entry: %a@]" Var.Subst.pp subst pp frame - pp entry] + [%Trace.retn fun {pf} (entry, {unshadow; frame}) -> + pf "@[unshadow: %a@ frame: %a@ entry: %a@]" Var.Subst.pp unshadow pp + frame pp entry] (** Leave scope of locals: existentially quantify locals. *) let post locals _ q = @@ -211,20 +212,19 @@ let post locals _ q = (** Express in terms of actuals instead of formals: existentially quantify formals, and apply inverse of fresh variables for formals renaming to restore the shadowed variables. *) -let retn formals freturn {areturn; subst; frame} q = +let retn formals freturn {areturn; unshadow; frame} q = [%Trace.call fun {pf} -> - pf "@[formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]" + pf "@[formals: {@[%a@]}%a%a@ shadows: %a@ q: %a@ frame: %a@]" (List.pp ", " Llair.Reg.pp) formals (Option.pp "@ freturn: %a" Llair.Reg.pp) freturn (Option.pp "@ areturn: %a" Var.pp) - areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame] + areturn Var.Subst.pp unshadow pp q pp frame] ; let formals = List.map ~f:Var.of_reg formals in let freturn = Option.map ~f:Var.of_reg freturn in - let inv_subst = Var.Subst.invert subst in - let q, inv_subst = + let q, shadows = match areturn with | Some areturn -> ( (* reenter scope of areturn just before exiting scope of formals *) @@ -232,16 +232,16 @@ let retn formals freturn {areturn; subst; frame} q = (* pass return value *) match freturn with | Some freturn -> - (Exec.move q (IArray.of_ (areturn, Term.var freturn)), inv_subst) - | None -> (Exec.kill q areturn, inv_subst) ) - | None -> (q, inv_subst) + (Exec.move q (IArray.of_ (areturn, Term.var freturn)), unshadow) + | None -> (Exec.kill q areturn, unshadow) ) + | None -> (q, unshadow) in (* exit scope of formals *) let q = Sh.exists (Var.Set.add_list formals (Var.Set.of_option freturn)) q in (* reinstate shadowed values of locals *) - let q = Sh.rename inv_subst q in + let q = Sh.rename shadows q in (* reconjoin frame *) Sh.star frame q (* simplify *)