[sledge] Add formal parameters to functions for return values

Summary:
This diff adds a formal parameter to each non-void-returning function
to name the return value, and similarly a formal parameter for the
thrown exception value. These are interpreted as call-by-reference
parameters, so that they can be constrained in formulas to e.g. be
equal to the return value, and are still in scope when the function
returns, and so can be passed to the return block. Prior to
summarizing functions, this means that these formals need to be
tracked on the analyzer's control stack.

This will be needed to express function specs/summaries in terms of
formals, and fixes a bug where in some cases return values were not
tracked correctly.

Reviewed By: kren1

Differential Revision: D15738026

fbshipit-source-id: fff2d107c

sledge/src/control.ml

@@ -19,7 +19,7 @@ module Stack : sig
   val push_jump : Var.Set.t -> t -> t
 
   val push_call :
-       Var.Set.t
+       Llair.block
     -> retreating:bool
     -> bound:int
     -> return:Llair.jump
@@ -31,14 +31,14 @@ module Stack : sig
   val pop_return :
        t
     -> init:'a
-    -> f:(Var.Set.t -> Domain.from_call -> 'a -> 'b)
-    -> (t * 'b * Llair.jump) option
+    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Llair.jump * 'a * t) option
 
   val pop_throw :
        t
     -> init:'a
-    -> f:(Var.Set.t -> Domain.from_call -> 'a -> 'a)
-    -> (t * 'a * Llair.jump) option
+    -> f:(Var.t option -> Var.Set.t -> Domain.from_call -> 'a -> 'a)
+    -> (Llair.jump * 'a * t) option
 end = struct
   type t =
     | Locals of Var.Set.t * t
@@ -46,6 +46,8 @@ end = struct
         { retreating: bool
               (** return from a call not known to be nonrecursive *)
         ; dst: Llair.Jump.t
+        ; freturn: Var.t option
+        ; fthrow: Var.t
         ; from_call: Domain.from_call
         ; stk: t }
     | Throw of Llair.Jump.t * t
@@ -110,14 +112,16 @@ end = struct
     (if Set.is_empty lcls then stk else Locals (lcls, stk))
     |> check invariant
 
-  let push_return ~retreating dst from_call stk =
-    Return {retreating; dst; from_call; stk} |> check invariant
+  let push_return ~retreating dst freturn fthrow from_call stk =
+    Return {retreating; dst; freturn; fthrow; from_call; stk}
+    |> check invariant
 
   let push_throw jmp stk =
     (match jmp with None -> stk | Some jmp -> Throw (jmp, stk))
     |> check invariant
 
-  let push_call locals ~retreating ~bound ~return from_call ?throw stk =
+  let push_call {Llair.locals; parent= {freturn; fthrow}} ~retreating ~bound
+      ~return from_call ?throw stk =
     [%Trace.call fun {pf} -> pf "%a" print_abbrev stk]
     ;
     let rec count_f_in_stack acc f = function
@@ -132,7 +136,8 @@ end = struct
     else
       Some
         (push_jump locals
-           (push_throw throw (push_return ~retreating return from_call stk)))
+           (push_throw throw
+              (push_return ~retreating return freturn fthrow from_call stk)))
     )
     |>
     [%Trace.retn fun {pf} _ ->
@@ -142,8 +147,13 @@ end = struct
     let rec pop_return_ scope = function
       | Locals (locals, stk) -> pop_return_ (Set.union locals scope) stk
       | Throw (_, stk) -> pop_return_ scope stk
-      | Return {dst; from_call; stk} ->
-          Some (stk, f scope from_call init, dst)
+      | Return {dst; freturn; from_call; stk} ->
+          let dst =
+            match freturn with
+            | Some freturn -> {dst with args= Exp.var freturn :: dst.args}
+            | None -> dst
+          in
+          Some (dst, f freturn scope from_call init, stk)
       | Empty -> None
     in
     pop_return_ Var.Set.empty stk
@@ -152,10 +162,11 @@ end = struct
     let rec pop_throw_ scope state = function
       | Locals (locals, stk) ->
           pop_throw_ (Set.union locals scope) state stk
-      | Return {from_call; stk} ->
-          pop_throw_ Var.Set.empty (f scope from_call state) stk
-      | Throw (jmp, Return {from_call; stk}) ->
-          Some (stk, f scope from_call state, jmp)
+      | Return {freturn; from_call; stk} ->
+          pop_throw_ Var.Set.empty (f freturn scope from_call state) stk
+      | Throw (dst, Return {fthrow; from_call; stk}) ->
+          let dst = {dst with args= Exp.var fthrow :: dst.args} in
+          Some (dst, f (Some fthrow) scope from_call state, stk)
       | Empty -> None
       | Throw _ as stk -> violates invariant stk
     in
@@ -269,30 +280,29 @@ let exec_goto stk state block ({dst; retreating} : Llair.jump) =
   Work.add ~prev:block ~retreating stk state dst
 
 let exec_jump stk state block ({dst; args} as jmp : Llair.jump) =
-  let state, _ = Domain.call state args dst.params dst.locals in
+  let state, _ = Domain.call args dst.params dst.locals state in
   exec_goto stk state block jmp
 
 let exec_call ~opts stk state block ({dst; args; retreating} : Llair.jump)
     return throw =
-  let state, from_call = Domain.call state args dst.params dst.locals in
+  let state, from_call = Domain.call args dst.params dst.locals state in
   match
-    Stack.push_call ~bound:opts.bound dst.locals ~retreating ~return
-      from_call ?throw stk
+    Stack.push_call ~bound:opts.bound dst ~retreating ~return from_call
+      ?throw stk
   with
   | Some stk -> Work.add stk ~prev:block ~retreating state dst
   | None -> Work.skip
 
-let exec_return stk state block exp =
-  match Stack.pop_return stk ~init:state ~f:Domain.retn with
-  | Some (stk, state, ({args} as jmp)) ->
-      exec_jump stk state block {jmp with args= Option.cons exp args}
+let exec_pop pop stk state block exp =
+  match pop stk ~init:state ~f:(Domain.retn exp) with
+  | Some (jmp, state, stk) -> exec_jump stk state block jmp
   | None -> Work.skip
 
+let exec_return stk state block exp =
+  exec_pop Stack.pop_return stk state block exp
+
 let exec_throw stk state block exc =
-  match Stack.pop_throw stk ~init:state ~f:Domain.retn with
-  | Some (stk, state, ({args} as jmp)) ->
-      exec_jump stk state block {jmp with args= exc :: args}
-  | None -> Work.skip
+  exec_pop Stack.pop_throw stk state block (Some exc)
 
 let exec_skip_func :
     Stack.t -> Domain.t -> Llair.block -> Llair.jump -> Work.x =
@@ -405,7 +415,7 @@ let harness : Llair.t -> (int -> Work.t) option =
   | Some {entry= {params= []} as block} ->
       Some
         (Work.init
-           (fst (Domain.call (Domain.init pgm.globals) [] [] block.locals))
+           (fst (Domain.call [] [] block.locals (Domain.init pgm.globals)))
            block)
   | _ -> None
 

sledge/src/import/import.ml

@@ -262,6 +262,7 @@ module Set = struct
   let equal_m__t (module Elt : Compare_m) = equal
   let pp pp_elt fs x = List.pp ",@ " pp_elt fs (to_list x)
   let disjoint x y = is_empty (inter x y)
+  let add_list ys x = List.fold ~f:add ~init:x ys
   let diff_inter_diff x y = (diff x y, inter x y, diff y x)
   let inter_diff x y = (inter x y, diff y x)
   let of_vector cmp x = of_array cmp (Vector.to_array x)

sledge/src/import/import.mli

@@ -212,6 +212,7 @@ module Set : sig
 
   val pp : 'e pp -> ('e, 'c) t pp
   val disjoint : ('e, 'c) t -> ('e, 'c) t -> bool
+  val add_list : 'e list -> ('e, 'c) t -> ('e, 'c) t
 
   val diff_inter_diff :
     ('e, 'c) t -> ('e, 'c) t -> ('e, 'c) t * ('e, 'c) t * ('e, 'c) t

sledge/src/llair/llair.ml

@@ -56,7 +56,12 @@ and cfg = block vector
 (* [entry] is not part of [cfg] since it is special in several ways: its
    params are the func params, its locals are all the locals in it plus the
    cfg, and it cannot be jumped to, only called. *)
-and func = {name: Global.t; entry: block; cfg: cfg}
+and func =
+  { name: Global.t
+  ; entry: block
+  ; cfg: cfg
+  ; freturn: Var.t option
+  ; fthrow: Var.t }
 
 let sexp_cons (hd : Sexp.t) (tl : Sexp.t) =
   match tl with
@@ -201,10 +206,13 @@ let rec dummy_block =
   ; sort_index= 0 }
 
 and dummy_func =
+  let dummy_var = Var.program "dummy" in
   let dummy_ptr_typ = Typ.pointer ~elt:(Typ.opaque ~name:"dummy") in
-  { name= Global.mk (Var.program "dummy") dummy_ptr_typ Loc.none
+  { name= Global.mk dummy_var dummy_ptr_typ Loc.none
   ; entry= dummy_block
-  ; cfg= Vector.empty }
+  ; cfg= Vector.empty
+  ; freturn= None
+  ; fthrow= dummy_var }
 
 (** Instructions *)
 
@@ -416,13 +424,25 @@ module Func = struct
 
   let find functions name = Map.find functions name
 
-  let mk ~name ~entry ~cfg =
+  let mk ~(name : Global.t) ~entry ~cfg =
     let locals =
       Vector.fold ~init:entry.locals cfg ~f:(fun locals block ->
           Set.union locals block.locals )
     in
+    let freturn, locals =
+      match name.typ with
+      | Pointer {elt= Function {return= Some _}} ->
+          let freturn, locals =
+            Var.fresh "freturn" ~wrt:(Set.add_list entry.params locals)
+          in
+          (Some freturn, locals)
+      | _ -> (None, locals)
+    in
+    let fthrow, locals =
+      Var.fresh "fthrow" ~wrt:(Set.add_list entry.params locals)
+    in
     let entry = {entry with locals} in
-    let func = {name; entry; cfg} in
+    let func = {name; entry; cfg; freturn; fthrow} in
     let resolve_parent_and_jumps block =
       block.parent <- func ;
       let lookup cfg lbl : block =

sledge/src/llair/llair.mli

@@ -107,7 +107,12 @@ and cfg
 
 (** A function is a control-flow graph with distinguished entry block, whose
     parameters are the function parameters. *)
-and func = private {name: Global.t; entry: block; cfg: cfg}
+and func = private
+  { name: Global.t
+  ; entry: block
+  ; cfg: cfg
+  ; freturn: Var.t option
+  ; fthrow: Var.t }
 
 type functions
 

sledge/src/symbheap/domain.ml

@@ -29,7 +29,7 @@ type from_call = Var.Subst.t [@@deriving compare, equal, sexp]
 (** Express formula in terms of formals instead of actuals, and enter scope
     of locals: rename formals to fresh vars in formula and actuals, add
     equations between each formal and actual, and quantify the fresh vars. *)
-let call q actuals formals locals =
+let call actuals formals locals q =
   [%Trace.call fun {pf} ->
     pf
       "@[<hv>actuals: (@[%a@])@ formals: (@[%a@])@ locals: {@[%a@]}@ q: %a@]"
@@ -52,14 +52,25 @@ let call q actuals formals locals =
 (** Leave scope of locals and express in terms of actuals instead of
     formals: existentially quantify locals and formals, and apply inverse of
     fresh variables for formals renaming to restore the shadowed variables. *)
-let retn locals freshen_locals q =
+let retn actual formal locals freshen_locals q =
   [%Trace.call fun {pf} ->
-    pf "@[<hv>locals: {@[%a@]}@ subst: %a@ q: %a@]" Var.Set.pp locals
-      Var.Subst.pp
+    pf "@[<hv>%a%alocals: {@[%a@]}@ subst: %a@ q: %a@]"
+      (Option.pp "%a to " Exp.pp)
+      actual (Option.pp "%a@ " Var.pp) formal Var.Set.pp locals Var.Subst.pp
       (Var.Subst.invert freshen_locals)
       Sh.pp q]
   ;
-  Sh.rename (Var.Subst.invert freshen_locals) (Sh.exists locals q)
+  let q' =
+    match (actual, formal) with
+    | Some actl, Some frml -> Sh.and_ (Exp.eq (Exp.var frml) actl) q
+    | None, None -> q
+    | _ ->
+        fail "mismatched actual and formal return: %a to %a"
+          (Option.pp "%a" Exp.pp) actual (Option.pp "%a" Var.pp) formal ()
+  in
+  Sh.rename
+    (Var.Subst.invert freshen_locals)
+    (Sh.exists (Option.fold ~f:Set.remove ~init:locals formal) q')
   |>
   [%Trace.retn fun {pf} -> pf "%a" Sh.pp]
 

sledge/src/symbheap/domain.mli

@@ -20,8 +20,8 @@ val exec_intrinsic :
 
 type from_call [@@deriving compare, equal, sexp]
 
-val call : t -> Exp.t list -> Var.t list -> Var.Set.t -> t * from_call
-val retn : Var.Set.t -> from_call -> t -> t
+val call : Exp.t list -> Var.t list -> Var.Set.t -> t -> t * from_call
+val retn : Exp.t option -> Var.t option -> Var.Set.t -> from_call -> t -> t
 
 val resolve_callee :
   (Var.t -> Llair.func list) -> Exp.t -> t -> Llair.func list

sledge/src/symbheap/exec.ml

@@ -571,7 +571,7 @@ let strlen_spec us reg ptr =
 (* execute a command with given spec from pre *)
 let exec_spec pre {xs; foot; post} =
   [%Trace.call fun {pf} ->
-    pf "@[%a@]@ @[<2>%a@\n@[<hv>{%a  }@;<1 -1>--@ {%a  }@]@]" Sh.pp pre
+    pf "@[%a@]@ @[<2>%a@,@[<hv>{%a  }@;<1 -1>--@ {%a  }@]@]" Sh.pp pre
       (Sh.pp_us ~pre:"@<2>∀ ")
       xs Sh.pp foot Sh.pp post ;
     assert (

sledge/test/exec/wrap_malloc.c

@@ -0,0 +1,14 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdlib.h>
+
+char* c() { return malloc(12); }
+int main() {
+  char* s = c();
+  return s ? *s : 1;
+}

sledge/test/report.expected

@@ -3,6 +3,7 @@ frontend/cond_alloca.bc:	RESULT: Internal error: no applicable harness
 exec/globals.bc:	RESULT: Success
 exec/global_vars.bc:	RESULT: Success
 exec/recursion.bc:	RESULT: Success
+exec/wrap_malloc.bc:	RESULT: Success
 frontend/destructor_bases.bc:	RESULT: Success
 frontend/exceptions.bc:	RESULT: Success
 frontend/rethrow.bc:	RESULT: Success