[sledge] [summaries] Fix variable naming bugs

Summary:
This fixes two bugs:
* All local variables would get existentially quantified out, that means
  the the local variables of the caller couldn't be restored properly
* Frame was added back on after the formals were killed. Which meant
  that if frame talked about formals (in pure for example), those
  formals would remain to be free variables.

Reviewed By: ngorogiannis

Differential Revision: D16091157

fbshipit-source-id: dfe12ed82

sledge/src/symbheap/state_domain.ml

@@ -114,40 +114,29 @@ let call ~summaries actuals formals locals globals q =
   let and_eqs formals actuals q =
     List.fold2_exn ~f:and_eq formals actuals ~init:q
   in
-  let q'', subst =
+  let q'' = and_eqs formals actuals q' in
-    (Sh.extend_us locals (and_eqs formals actuals q'), freshen_locals)
-  in
   ( if not summaries then
+    let q'', subst = (Sh.extend_us locals q'', freshen_locals) in
     (q'', {subst; frame= Sh.emp; actuals_to_formals= []})
   else
     let formals_set = Var.Set.of_list formals in
-    let non_function_specific_vars =
+    (* Add the formals here to do garbage collection and then get rid of
-      Set.diff (Sh.fv q'') (Set.union formals_set globals)
+       them *)
-    in
-    let function_summary_pre = Sh.exists non_function_specific_vars q'' in
     let function_summary_pre =
-      garbage_collect function_summary_pre ~wrt:function_summary_pre.us
+      garbage_collect q'' ~wrt:(Set.union formals_set globals)
     in
     [%Trace.info "function summary pre %a" pp function_summary_pre] ;
-    let and_eq q formal actual =
+    let foot = Sh.exists formals_set function_summary_pre in
-      Sh.and_ (Exp.eq (Exp.var formal) actual) q
+    let pre = q' in
-    in
-    (* Replace formals with actuals in the function summary *)
-    let foot =
-      Sh.exists formals_set
-        (List.fold2_exn ~f:and_eq formals actuals ~init:function_summary_pre)
-    in
-    (* Replace formals with actuals in the callsite precondition *)
-    let pre =
-      Sh.exists formals_set
-        (List.fold2_exn ~f:and_eq formals actuals ~init:q'')
-    in
     let xs, foot = Sh.bind_exists ~wrt:pre.us foot in
     let frame =
       Option.value ~default:Sh.emp (Solver.infer_frame pre xs foot)
     in
-    ( function_summary_pre
+    let q'', subst =
-    , {subst; frame; actuals_to_formals= List.zip_exn actuals formals} ) )
+      (Sh.extend_us locals (and_eqs formals actuals foot), freshen_locals)
+    in
+    (q'', {subst; frame; actuals_to_formals= List.zip_exn actuals formals})
+  )
   |>
   [%Trace.retn fun {pf} (q', {subst; frame}) ->
     pf "@[<v>subst: %a@ frame: %a@ q': %a@]" Var.Subst.pp subst pp frame pp
@@ -165,21 +154,15 @@ 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 {subst; frame; actuals_to_formals} q =
+let retn formals {subst; frame} q =
   [%Trace.call fun {pf} ->
     pf "@[<v>formals: {@[%a@]}@ subst: %a@ q: %a@ frame: %a@]"
       (List.pp ", " Var.pp) formals Var.Subst.pp (Var.Subst.invert subst) pp
       q pp frame]
   ;
-  let and_eq q (actual, formal) =
+  let q = Sh.exists (Var.Set.of_list formals) q in
-    Sh.and_ (Exp.eq (Exp.var formal) actual) q
+  let q = Sh.rename (Var.Subst.invert subst) q in
-  in
+  Sh.star frame q
-  let q = List.fold ~f:and_eq actuals_to_formals ~init:q in
-  let func_post =
-    Sh.rename (Var.Subst.invert subst)
-      (Sh.exists (Var.Set.of_list formals) q)
-  in
-  Sh.star frame func_post
   |>
   [%Trace.retn fun {pf} -> pf "%a" pp]