From 524ae3a7e2237fe34b1464c921828b5875112d0c Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 23 Aug 2018 06:07:30 -0700 Subject: [PATCH] [inferbo] Return unknown value on non-const function calls Summary: It returns unknown values on non-const function calls like on unknown function calls. Reviewed By: mbouaziz Differential Revision: D9478862 fbshipit-source-id: 4b795ec55 --- .../src/bufferoverrun/bufferOverrunChecker.ml | 8 ++++---- infer/src/bufferoverrun/bufferOverrunDomain.ml | 10 ++++++++-- infer/src/bufferoverrun/bufferOverrunTrace.ml | 13 ++++++++++--- .../c/bufferoverrun/function_call.c | 18 ++++++++++++++++++ .../codetoanalyze/c/bufferoverrun/issues.exp | 2 ++ 5 files changed, 42 insertions(+), 9 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunChecker.ml b/infer/src/bufferoverrun/bufferOverrunChecker.ml index 039eaca53..69df868f6 100644 --- a/infer/src/bufferoverrun/bufferOverrunChecker.ml +++ b/infer/src/bufferoverrun/bufferOverrunChecker.ml @@ -197,12 +197,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct "/!\\ Unknown call to %a at %a@\n" Typ.Procname.pp callee_pname Location.pp location ; Dom.Mem.add_unknown_from id ~callee_pname ~location mem ) - | Call (_, fun_exp, _, location, _) -> + | Call ((id, _), fun_exp, _, location, _) -> let () = L.(debug BufferOverrun Verbose) "/!\\ Call to non-const function %a at %a" Exp.pp fun_exp Location.pp location in - mem + Dom.Mem.add_unknown_from_funcptr id ~location mem | Remove_temps (temps, _) -> Dom.Mem.remove_temps temps mem | Abstract _ | Nullify _ -> @@ -571,8 +571,8 @@ module Report = struct else let desc = Format.asprintf "Parameter: %a" Loc.pp loc in (Errlog.make_trace_element depth location desc [] :: trace, depth) - | Trace.UnknownFrom (pname, location) -> - let desc = Format.asprintf "Unknown value from: %a" Typ.Procname.pp pname in + | Trace.UnknownFrom (pname_opt, location) -> + let desc = Format.asprintf "Unknown value from: %a" Trace.pp_pname_opt pname_opt in (Errlog.make_trace_element depth location desc [] :: trace, depth) in List.fold_right ~f ~init:([], 0) trace.trace |> fst |> List.rev diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index be65aaf6a..6ed9c1964 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -741,7 +741,8 @@ module MemReach = struct let add_heap : Loc.t -> Val.t -> t -> t = fun k v m -> {m with heap= Heap.add k v m.heap} - let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = + let add_unknown_from + : Ident.t -> callee_pname:Typ.Procname.t option -> location:Location.t -> t -> t = fun id ~callee_pname ~location m -> let val_unknown = Val.unknown_from ~callee_pname ~location in add_stack (Loc.of_id id) val_unknown m |> add_heap Loc.unknown val_unknown @@ -938,7 +939,12 @@ module Mem = struct let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> f_lift (MemReach.add_heap k v) let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = - fun id ~callee_pname ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname ~location) + fun id ~callee_pname ~location -> + f_lift (MemReach.add_unknown_from id ~callee_pname:(Some callee_pname) ~location) + + + let add_unknown_from_funcptr : Ident.t -> location:Location.t -> t -> t = + fun id ~location -> f_lift (MemReach.add_unknown_from id ~callee_pname:None ~location) let strong_update_heap : PowLoc.t -> Val.t -> t -> t = diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index d9c260396..d49e1c451 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -18,7 +18,7 @@ module BoTrace = struct | Call of Location.t | Return of Location.t | SymAssign of Loc.t * Location.t - | UnknownFrom of Typ.Procname.t * Location.t + | UnknownFrom of Typ.Procname.t option * Location.t [@@deriving compare] type t = {length: int; trace: elem list} [@@deriving compare] @@ -31,6 +31,13 @@ module BoTrace = struct let append x y = {length= x.length + y.length; trace= x.trace @ y.trace} + let pp_pname_opt fmt = function + | None -> + F.fprintf fmt "non-const function" + | Some pname -> + Typ.Procname.pp fmt pname + + let pp_elem : F.formatter -> elem -> unit = fun fmt elem -> match elem with @@ -48,8 +55,8 @@ module BoTrace = struct F.fprintf fmt "Return (%a)" Location.pp_file_pos location | SymAssign (loc, location) -> F.fprintf fmt "SymAssign (%a, %a)" Loc.pp loc Location.pp_file_pos location - | UnknownFrom (pname, location) -> - F.fprintf fmt "UnknownFrom (%a, %a)" Typ.Procname.pp pname Location.pp_file_pos location + | UnknownFrom (pname_opt, location) -> + F.fprintf fmt "UnknownFrom (%a, %a)" pp_pname_opt pname_opt Location.pp_file_pos location let pp : F.formatter -> t -> unit = diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c index fa54f7daf..288a3cac9 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/function_call.c @@ -72,3 +72,21 @@ void call_by_struct_ptr_bad() { struct_ptr_set_to_zero(sp); arr[sp->field - 1] = 123; } + +int ret_zero() { return 0; } + +void call_function_ptr_good_FP() { + int (*func_ptr)(void) = &ret_zero; + int arr[10]; + if ((*func_ptr)() != 0) { + arr[10] = 1; + } +} + +void call_function_ptr_bad() { + int (*func_ptr)(void) = &ret_zero; + int arr[10]; + if ((*func_ptr)() == 0) { + arr[10] = 1; + } +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 0e1460335..03ebf178a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -22,6 +22,8 @@ codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bu codetoanalyze/c/bufferoverrun/function_call.c, call_by_arr_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_by_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, call_by_struct_ptr_bad, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Assignment,ArrayAccess: Offset: -1 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_bad, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/function_call.c, call_function_ptr_good_FP, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,ArrayAccess: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Call,Parameter: arr,Assignment,ArrayAccess: Offset: 100 Size: 10 by call to `arr_access` ] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [] codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_bad_FN, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, []