From 12bab4b16bec1235fc6982755a8cbf65475ae993 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 10 Jun 2019 07:18:26 -0700 Subject: [PATCH] [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 | 66 +++++++++++++++++++--------------- sledge/src/import/import.ml | 1 + sledge/src/import/import.mli | 1 + sledge/src/llair/llair.ml | 30 +++++++++++++--- sledge/src/llair/llair.mli | 7 +++- sledge/src/symbheap/domain.ml | 21 ++++++++--- sledge/src/symbheap/domain.mli | 4 +-- sledge/src/symbheap/exec.ml | 2 +- sledge/test/exec/wrap_malloc.c | 14 ++++++++ sledge/test/report.expected | 1 + 10 files changed, 105 insertions(+), 42 deletions(-) create mode 100644 sledge/test/exec/wrap_malloc.c diff --git a/sledge/src/control.ml b/sledge/src/control.ml index a708fbc01..8112f7b62 100644 --- a/sledge/src/control.ml +++ b/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 diff --git a/sledge/src/import/import.ml b/sledge/src/import/import.ml index ee57eb87a..61f6f2f63 100644 --- a/sledge/src/import/import.ml +++ b/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) diff --git a/sledge/src/import/import.mli b/sledge/src/import/import.mli index 05efd2b75..de9ecf007 100644 --- a/sledge/src/import/import.mli +++ b/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 diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index 00edb1d44..1690a485e 100644 --- a/sledge/src/llair/llair.ml +++ b/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 = diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index 9be5956b2..161ce284d 100644 --- a/sledge/src/llair/llair.mli +++ b/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 diff --git a/sledge/src/symbheap/domain.ml b/sledge/src/symbheap/domain.ml index c0ab083ca..997ca26a3 100644 --- a/sledge/src/symbheap/domain.ml +++ b/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 "@[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 "@[locals: {@[%a@]}@ subst: %a@ q: %a@]" Var.Set.pp locals - Var.Subst.pp + pf "@[%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] diff --git a/sledge/src/symbheap/domain.mli b/sledge/src/symbheap/domain.mli index dab5e3182..01ae1c942 100644 --- a/sledge/src/symbheap/domain.mli +++ b/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 diff --git a/sledge/src/symbheap/exec.ml b/sledge/src/symbheap/exec.ml index 01806ecfb..7b2482789 100644 --- a/sledge/src/symbheap/exec.ml +++ b/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@[{%a }@;<1 -1>--@ {%a }@]@]" Sh.pp pre + pf "@[%a@]@ @[<2>%a@,@[{%a }@;<1 -1>--@ {%a }@]@]" Sh.pp pre (Sh.pp_us ~pre:"@<2>∀ ") xs Sh.pp foot Sh.pp post ; assert ( diff --git a/sledge/test/exec/wrap_malloc.c b/sledge/test/exec/wrap_malloc.c new file mode 100644 index 000000000..d07829b24 --- /dev/null +++ b/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 + +char* c() { return malloc(12); } +int main() { + char* s = c(); + return s ? *s : 1; +} diff --git a/sledge/test/report.expected b/sledge/test/report.expected index 90902b711..8d848d5b6 100644 --- a/sledge/test/report.expected +++ b/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