[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

@@ -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 "@[<v>subst: %a@ frame: %a@ entry: %a@]" Var.Subst.pp subst pp frame
-      pp entry]
+  [%Trace.retn fun {pf} (entry, {unshadow; frame}) ->
+    pf "@[<v>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 "@[<v>formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]"
+    pf "@[<v>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 *)