From 78eb85bcf4599e9659d191e6434ef2fbaba6d8e2 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 2 Dec 2020 13:46:06 -0800
Subject: [PATCH] [sledge] Fix scope when entering scope of a local shadowed by
 a callee

Summary:
It was possible for the scope of a local to be incorrectly restored
when entering it for the first time in a caller after is was shadowed
by a callee. This could happen because scope management in the
analysis relies on renaming variables to adjust the vocabulary of
symbolic states. This was usually done, but optimizations of renaming
with a substitution whose domain is disjoint from the vocabulary of a
formula inadvertantly violated this vocabulary-adjustment
assumption. (Yes, this is too easy to get wrong.)

Reviewed By: jvillard

Differential Revision: D25146162

fbshipit-source-id: 30f2d657f
---
 sledge/src/domain_sh.ml    |  2 +-
 sledge/src/fol/var0.ml     | 16 ++++++++--------
 sledge/src/fol/var_intf.ml |  6 +++++-
 sledge/src/sh.ml           | 11 ++++-------
 4 files changed, 18 insertions(+), 17 deletions(-)

diff --git a/sledge/src/domain_sh.ml b/sledge/src/domain_sh.ml
index 2081bed0c..85e214ac9 100644
--- a/sledge/src/domain_sh.ml
+++ b/sledge/src/domain_sh.ml
@@ -200,7 +200,7 @@ let post locals _ q =
     restore the shadowed variables. *)
 let retn formals freturn {areturn; unshadow; frame} q =
   [%Trace.call fun {pf} ->
-    pf "@[<v>formals: {@[%a@]}%a%a@ shadows: %a@ q: %a@ frame: %a@]"
+    pf "@[<v>formals: {@[%a@]}%a%a@ unshadow: %a@ q: %a@ frame: %a@]"
       (List.pp ", " Llair.Reg.pp)
       formals
       (Option.pp "@ freturn: %a" Llair.Reg.pp)
diff --git a/sledge/src/fol/var0.ml b/sledge/src/fol/var0.ml
index 714c640c6..5e8240c0a 100644
--- a/sledge/src/fol/var0.ml
+++ b/sledge/src/fol/var0.ml
@@ -100,21 +100,21 @@ module Make (T : REPR) = struct
           Map.add_exn ~key:data ~data:key sub' )
       |> check invariant
 
-    let restrict sub vs =
-      Map.fold sub {sub; dom= Set.empty; rng= Set.empty}
+    let restrict_dom sub0 vs =
+      Map.fold sub0 {sub= sub0; dom= Set.empty; rng= Set.empty}
         ~f:(fun ~key ~data z ->
-          if Set.mem key vs then
-            {z with dom= Set.add key z.dom; rng= Set.add data z.rng}
+          let rng = Set.add data z.rng in
+          if Set.mem key vs then {z with dom= Set.add key z.dom; rng}
           else (
             assert (
               (* all substs are injective, so the current mapping is the
                  only one that can cause [data] to be in [rng] *)
-              (not (Set.mem data (range (Map.remove key sub))))
-              || violates invariant sub ) ;
-            {z with sub= Map.remove key z.sub} ) )
+              (not (Set.mem data (range (Map.remove key sub0))))
+              || violates invariant sub0 ) ;
+            {z with sub= Map.remove key z.sub; rng} ) )
       |> check (fun {sub; dom; rng} ->
              assert (Set.equal dom (domain sub)) ;
-             assert (Set.equal rng (range sub)) )
+             assert (Set.equal rng (range sub0)) )
 
     let apply sub v = Map.find v sub |> Option.value ~default:v
   end
diff --git a/sledge/src/fol/var_intf.ml b/sledge/src/fol/var_intf.ml
index 92d2d0801..f363467f0 100644
--- a/sledge/src/fol/var_intf.ml
+++ b/sledge/src/fol/var_intf.ml
@@ -60,7 +60,11 @@ module type VAR = sig
     val empty : t
     val freshen : Set.t -> wrt:Set.t -> x * Set.t
     val invert : t -> t
-    val restrict : t -> Set.t -> x
+
+    val restrict_dom : t -> Set.t -> x
+    (** restrict the domain of a substitution to a set, and yield the range
+        of the unrestricted substitution *)
+
     val is_empty : t -> bool
     val domain : t -> Set.t
     val range : t -> Set.t
diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml
index 2c27dca18..a1624dbb7 100644
--- a/sledge/src/sh.ml
+++ b/sledge/src/sh.ml
@@ -353,12 +353,9 @@ and rename_ Var.Subst.{sub; dom; rng} q =
     pf "@[%a@]@ %a" Var.Subst.pp sub pp q ;
     assert (Var.Set.subset dom ~of_:q.us)]
   ;
+  let q = extend_us rng q in
   ( if Var.Subst.is_empty sub then q
-  else
-    let us = Var.Set.union (Var.Set.diff q.us dom) rng in
-    assert (not (Var.Set.equal us q.us)) ;
-    let q' = apply_subst sub (freshen_xs q ~wrt:(Var.Set.union dom us)) in
-    {q' with us} )
+  else {(apply_subst sub q) with us= Var.Set.diff q.us dom} )
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -368,7 +365,7 @@ and rename_ Var.Subst.{sub; dom; rng} q =
 and rename sub q =
   [%Trace.call fun {pf} -> pf "@[%a@]@ %a" Var.Subst.pp sub pp q]
   ;
-  rename_ (Var.Subst.restrict sub q.us) q
+  rename_ (Var.Subst.restrict_dom sub q.us) q
   |>
   [%Trace.retn fun {pf} q' ->
     pf "%a" pp q' ;
@@ -395,7 +392,7 @@ and freshen_xs q ~wrt =
     assert (Var.Set.disjoint q'.xs (Var.Set.inter q.xs wrt)) ;
     invariant q']
 
-let extend_us us q =
+and extend_us us q =
   let us = Var.Set.union us q.us in
   (if us == q.us then q else {(freshen_xs q ~wrt:us) with us})
   |> check invariant