[sledge] Fix scope on return in case actual return clashes with formals

Summary:
It can happen that the actual return variable, which is the name of
the variable in the caller's scope that receives the returned value,
clashes with the formals of the callee. The scope of the return
formula was wrong in this case, as the actual return was outscoped via
existential quantification with the rest of the formals after the
return values was passed.

Reviewed By: jvillard

Differential Revision: D25196727

fbshipit-source-id: 94cf25418

sledge/src/domain_sh.ml

@@ -215,8 +215,13 @@ let retn formals freturn {areturn; unshadow; frame} q =
         | None -> Exec.kill q areturn )
     | None -> q
   in
-  (* exit scope of formals *)
+  (* exit scope of formals, except for areturn, which move/kill handled *)
-  let q = Sh.exists (Var.Set.union formals (Var.Set.of_option freturn)) q in
+  let outscoped =
+    Var.Set.diff
+      (Var.Set.union formals (Var.Set.of_option freturn))
+      (Var.Set.of_option areturn)
+  in
+  let q = Sh.exists outscoped q in
   (* reinstate shadowed values of locals *)
   let q = Sh.rename unshadow q in
   (* reconjoin frame *)