[sledge] Revise Sh_domain handling of function call and return

Summary:
Fix a bug where the actual return variable was not scoped correctly in
cases where its name clashed with a local or formal of the
callee. Also comment and simplify to attempt to make more
understandable.

Reviewed By: bennostein

Differential Revision: D17801944

fbshipit-source-id: 286739241

sledge/src/llair/term.ml

@@ -472,6 +472,9 @@ module Var = struct
           else (
             assert (not (Set.equal vs' vs)) ;
             Set.add vs' data ) )
+      |> check (fun vs' ->
+             assert (Set.disjoint (domain sub) vs') ;
+             assert (Set.is_subset (range sub) ~of_:vs') )
   end
 end
 

sledge/src/symbheap/sh.ml

@@ -276,7 +276,10 @@ let exists xs q =
   assert (
     Set.is_subset xs ~of_:q.us
     || fail "Sh.exists xs - q.us: %a" Var.Set.pp (Set.diff xs q.us) () ) ;
-  {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant
+  ( if Set.is_empty xs then q
+  else
+    {q with us= Set.diff q.us xs; xs= Set.union q.xs xs} |> check invariant
+  )
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 

sledge/src/symbheap/sh_domain.ml

@@ -106,6 +106,34 @@ let garbage_collect (q : t) ~wrt =
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]
 
+let and_eqs sub formals actuals q =
+  let and_eq q formal actual =
+    let actual' = Term.rename sub actual in
+    Sh.and_ (Term.eq (Term.var formal) actual') q
+  in
+  List.fold2_exn ~f:and_eq formals actuals ~init:q
+
+let localize_entry globals actuals formals freturn locals subst 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 = Reg.Set.vars (Set.add_option freturn locals) in
+  let function_summary_pre =
+    garbage_collect entry
+      ~wrt:(Set.union formals_set (Reg.Set.vars globals))
+  in
+  [%Trace.info "function summary pre %a" pp function_summary_pre] ;
+  let foot = Sh.exists formals_set function_summary_pre in
+  let xs, foot = Sh.bind_exists ~wrt:pre.Sh.us foot in
+  let frame =
+    Option.value_exn
+      (Solver.infer_frame pre xs foot)
+      ~message:"Solver couldn't infer frame of a garbage-collected pre"
+  in
+  let q'' =
+    Sh.extend_us freturn_locals (and_eqs subst formals actuals foot)
+  in
+  (q'', frame)
+
 type from_call = {areturn: Var.t option; subst: Var.Subst.t; frame: Sh.t}
 [@@deriving compare, equal, sexp]
 
@@ -123,52 +151,35 @@ let call ~summaries ~globals ~actuals ~areturn ~formals ~freturn ~locals q =
   let actuals = List.map ~f:Exp.term actuals in
   let areturn = Option.map ~f:Reg.var areturn in
   let formals = List.map ~f:Reg.var formals in
-  let locals = Reg.Set.vars (Set.add_option freturn locals) in
-  let q', freshen_locals =
-    Sh.freshen q ~wrt:(Set.add_list formals locals)
-  in
-  let and_eq q formal actual =
-    let actual' = Term.rename freshen_locals actual in
-    Sh.and_ (Term.eq (Term.var formal) actual') q
-  in
-  let and_eqs formals actuals q =
-    List.fold2_exn ~f:and_eq formals actuals ~init:q
-  in
-  let q'' = and_eqs formals actuals q' in
-  ( if not summaries then
-    let q'' = Sh.extend_us locals q'' in
-    (q'', {areturn; subst= freshen_locals; frame= Sh.emp})
+  let freturn_locals = Reg.Set.vars (Set.add_option freturn locals) in
+  let modifs = Var.Set.of_option areturn in
+  (* quantify modifs, their current value will be overwritten and so does
+     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 = Sh.freshen q ~wrt:(Set.add_list formals freturn_locals) in
+  assert (Set.disjoint modifs (Var.Subst.domain subst)) ;
+  (* pass arguments by conjoining equations between formals and actuals *)
+  let entry = and_eqs subst formals actuals q' in
+  (* note: locals and formals are in scope *)
+  assert (Set.is_subset (Set.add_list formals freturn_locals) ~of_:entry.us) ;
+  ( if not summaries then (entry, {areturn; subst; frame= Sh.emp})
   else
-    (* Add the formals here to do garbage collection and then get rid of
-       them *)
-    let formals_set = Var.Set.of_list formals in
-    let function_summary_pre =
-      garbage_collect q''
-        ~wrt:(Set.union formals_set (Reg.Set.vars globals))
+    let q'', frame =
+      localize_entry globals actuals formals freturn locals subst q' entry
     in
-    [%Trace.info "function summary pre %a" pp function_summary_pre] ;
-    let foot = Sh.exists formals_set function_summary_pre in
-    let pre = q' in
-    let xs, foot = Sh.bind_exists ~wrt:pre.us foot in
-    let frame =
-      Option.value_exn
-        (Solver.infer_frame pre xs foot)
-        ~message:"Solver couldn't infer frame of a garbage-collected pre"
-    in
-    let q'' = Sh.extend_us locals (and_eqs formals actuals foot) in
-    (q'', {areturn; subst= freshen_locals; frame}) )
+    (q'', {areturn; subst; frame}) )
   |>
-  [%Trace.retn fun {pf} (q', {subst; frame}) ->
-    pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
-      q']
+  [%Trace.retn fun {pf} (entry, {subst; frame}) ->
+    pf "@[<v>subst: %a@ frame: %a@ entry: %a@]" Var.Subst.pp subst pp frame
+      pp entry]
 
 (** Leave scope of locals: existentially quantify locals. *)
 let post locals _ q =
   [%Trace.call fun {pf} ->
     pf "@[<hv>locals: {@[%a@]}@ q: %a@]" Reg.Set.pp locals Sh.pp q]
   ;
-  let locals = Reg.Set.vars locals in
-  Sh.exists locals q
+  Sh.exists (Reg.Set.vars locals) q
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 
@@ -177,21 +188,33 @@ let post locals _ q =
     restore the shadowed variables. *)
 let retn formals freturn {areturn; subst; frame} q =
   [%Trace.call fun {pf} ->
-    pf "@[<v>formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]"
-      (List.pp ", " Reg.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
-      q pp frame]
+    pf "@[<v>formals: {@[%a@]}%a%a@ subst: %a@ q: %a@ frame: %a@]"
+      (List.pp ", " Reg.pp) formals
+      (Option.pp "@ freturn: %a" Reg.pp)
+      freturn
+      (Option.pp "@ areturn: %a" Var.pp)
+      areturn Var.Subst.pp (Var.Subst.invert subst) pp q pp frame]
   ;
   let formals = List.map ~f:Reg.var formals in
   let freturn = Option.map ~f:Reg.var freturn in
-  let q =
-    match (areturn, freturn) with
-    | Some areturn, Some freturn ->
-        Exec.move q (Vector.of_ (areturn, Term.var freturn))
-    | Some areturn, None -> Exec.kill q areturn
-    | _ -> q
+  let inv_subst = Var.Subst.invert subst in
+  let q, inv_subst =
+    match areturn with
+    | Some areturn -> (
+        (* reenter scope of areturn just before exiting scope of formals *)
+        let q = Sh.extend_us (Var.Set.of_ areturn) q in
+        (* pass return value *)
+        match freturn with
+        | Some freturn ->
+            (Exec.move q (Vector.of_ (areturn, Term.var freturn)), inv_subst)
+        | None -> (Exec.kill q areturn, inv_subst) )
+    | None -> (q, inv_subst)
   in
+  (* exit scope of formals *)
   let q = Sh.exists (Set.add_list formals (Var.Set.of_option freturn)) q in
-  let q = Sh.rename (Var.Subst.invert subst) q in
+  (* reinstate shadowed values of locals *)
+  let q = Sh.rename inv_subst q in
+  (* reconjoin frame *)
   Sh.star frame q
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]