diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 900984e0b..a28eefcd7 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -942,9 +942,9 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path | Sil.Call (ret_ids, Sil.Const (Sil.Cfun fn), args, loc, call_flags) when function_is_builtin fn -> let sym_exe_builtin = Builtin.get_sym_exe_builtin fn in sym_exe_builtin cfg pdesc instr tenv _prop path ret_ids args fn loc - | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_param, loc, call_flags) -> + | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) -> (** Generic fun call with known name *) - let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_param in + let (prop_r, _n_actual_params) = normalize_params pdesc _prop actual_params in let fn, n_actual_params = handle_special_cases_call tenv cfg callee_pname _n_actual_params in let resolved_pname = if call_flags.Sil.cf_virtual then @@ -954,7 +954,7 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path match Cfg.Procdesc.find_from_name cfg resolved_pname with | None -> None | Some pd -> Some (Cfg.Procdesc.get_ret_type pd) in - let skip_call () = + let skip_call prop path = let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in Reporting.log_info pname exn; L.d_strln @@ -967,17 +967,21 @@ let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path summary.Specs.stats.Specs.call_stats callee_pname loc (Specs.CallStats.CR_skip) !Config.footprint); call_unknown_or_scan - false cfg pdesc tenv prop_r path + false cfg pdesc tenv prop path ret_ids ret_typ_opt n_actual_params resolved_pname loc in - begin + let sentinel_result = + if !Sil.curr_language = Sil.C_CPP then + sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop_r path actual_params callee_pname loc + else [(prop_r, path)] in + let do_call (prop, path) = match Specs.get_summary resolved_pname with - | None -> skip_call () + | None -> skip_call prop path | Some summary when call_should_be_skipped resolved_pname summary -> - skip_call () + skip_call prop path | Some summary -> sym_exec_call - cfg pdesc tenv prop_r path ret_ids n_actual_params summary loc - end + cfg pdesc tenv prop path ret_ids n_actual_params summary loc in + list_flatten (list_map do_call sentinel_result) | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *) let (prop_r, n_actual_params) = normalize_params pdesc _prop actual_params in if call_flags.Sil.cf_is_objc_block then @@ -1222,21 +1226,21 @@ and call_unknown_or_scan is_scan cfg pdesc tenv pre path let path_pos = State.get_path_pos () in [(Prop.mark_vars_as_undefined pre''' exps_to_mark callee_pname loc path_pos, path)] -and sym_exe_check_variadic_sentinel cfg pdesc tenv prop path actual_params fails_on_nil (sentinel, null_pos) pname loc = - let proc_attributes = Cfg.Procdesc.get_attributes pdesc in - let args = if proc_attributes.Sil.is_objc_instance_method then - (* we are calling an objc method so the first actual is the instance *) - list_tl actual_params - else - actual_params in - let nargs = list_length args in +and sym_exe_check_variadic_sentinel ?(fails_on_nil=false) cfg pdesc tenv prop path n_formals actual_params (sentinel, null_pos) callee_pname loc = + (* from clang's lib/Sema/SemaExpr.cpp: *) + (* "nullPos" is the number of formal parameters at the end which *) + (* effectively count as part of the variadic arguments. This is *) + (* useful if you would prefer to not have *any* formal parameters, *) + (* but the language forces you to have at least one. *) + let first_var_arg_pos = if null_pos > n_formals then 0 else n_formals - null_pos in + let nargs = list_length actual_params in (* sentinels start counting from the last argument to the function *) - let n = nargs - sentinel - 1 in - let build_argsi (acc, i) a = - if i = n then (acc, i +1) - else ((a, i):: acc, i +1) in + let sentinel_pos = nargs - sentinel - 1 in + let mk_non_terminal_argsi (acc, i) a = + if i < first_var_arg_pos || i >= sentinel_pos then (acc, i+1) + else ((a,i)::acc, i+1) in (* list_fold_left reverses the arguments *) - let non_terminal_actuals_i = fst (list_fold_left build_argsi ([], 0) args) in + let non_terminal_argsi = fst (list_fold_left mk_non_terminal_argsi ([], 0) actual_params) in let check_allocated result ((lexp, typ), i) = (* simulate a Letderef for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in @@ -1245,7 +1249,7 @@ and sym_exe_check_variadic_sentinel cfg pdesc tenv prop path actual_params fails sym_exec_generated false cfg tenv pdesc [letderef] result with e when exn_not_timeout e -> if not fails_on_nil then - let deref_str = Localise.deref_str_nil_argument_in_variadic_method pname nargs i in + let deref_str = Localise.deref_str_nil_argument_in_variadic_method callee_pname nargs i in let err_desc = Errdesc.explain_dereference ~use_buckets: true ~is_premature_nil: true deref_str prop loc in @@ -1255,7 +1259,19 @@ and sym_exe_check_variadic_sentinel cfg pdesc tenv prop path actual_params fails raise e in (* list_fold_left reverses the arguments back so that we report an *) (* error on the first premature nil argument *) - list_fold_left check_allocated [(prop, path)] non_terminal_actuals_i + list_fold_left check_allocated [(prop, path)] non_terminal_argsi + + +and sym_exe_check_variadic_sentinel_if_present cfg pdesc tenv prop path actual_params callee_pname loc = + match Cfg.Procdesc.find_from_name cfg callee_pname with + | None -> [(prop, path)] + | Some callee_pdesc -> + let proc_attributes = Cfg.Procdesc.get_attributes callee_pdesc in + match Sil.get_sentinel_func_attribute_value proc_attributes.Sil.func_attributes with + | None -> [(prop,path)] + | Some sentinel_arg -> + let formals = Cfg.Procdesc.get_formals callee_pdesc in + sym_exe_check_variadic_sentinel cfg pdesc tenv prop path (list_length formals) actual_params sentinel_arg callee_pname loc (** Perform symbolic execution for a function call *) and sym_exec_call cfg pdesc tenv pre path ret_ids actual_pars summary loc = @@ -2295,11 +2311,13 @@ module ModelBuiltins = struct execute_objc_alloc_no_fail cfg pdesc tenv symb_state ret_ids nsarray_typ loc let execute_NSArray_arrayWithObjects_count cfg pdesc instr tenv prop path ret_ids args callee_pname loc = - let res' = sym_exe_check_variadic_sentinel cfg pdesc tenv prop path args true (0,1) callee_pname loc in + let n_formals = 1 in + let res' = sym_exe_check_variadic_sentinel ~fails_on_nil:true cfg pdesc tenv prop path n_formals args (0,1) callee_pname loc in execute_objc_NSArray_alloc_no_fail cfg pdesc tenv res' ret_ids loc let execute_NSArray_arrayWithObjects cfg pdesc instr tenv prop path ret_ids args callee_pname loc = - let res' = sym_exe_check_variadic_sentinel cfg pdesc tenv prop path args false (0,1) callee_pname loc in + let n_formals = 1 in + let res' = sym_exe_check_variadic_sentinel cfg pdesc tenv prop path n_formals args (0,1) callee_pname loc in execute_objc_NSArray_alloc_no_fail cfg pdesc tenv res' ret_ids loc let _ = diff --git a/infer/tests/codetoanalyze/c/errors/Makefile b/infer/tests/codetoanalyze/c/errors/Makefile index 5b93dd82d..70a71dc57 100644 --- a/infer/tests/codetoanalyze/c/errors/Makefile +++ b/infer/tests/codetoanalyze/c/errors/Makefile @@ -2,6 +2,7 @@ all: make -C arithmetic make -C assertions + make -C attributes make -C initialization make -C local_vars make -C null_dereference @@ -12,6 +13,7 @@ all: clean: make -C arithmetic clean make -C assertions clean + make -C attributes clean make -C initialization clean make -C local_vars clean make -C null_dereference clean diff --git a/infer/tests/codetoanalyze/c/errors/attributes/Makefile b/infer/tests/codetoanalyze/c/errors/attributes/Makefile new file mode 100644 index 000000000..ec67ebe4f --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/attributes/Makefile @@ -0,0 +1,12 @@ + +SOURCES = $(shell ls *.c) +OBJECTS = $(SOURCES:.c=.o) + +all: clean $(OBJECTS) + echo $(OBJECTS) + +.c.o: + ${CC} -c $< + +clean: + rm -rf $(OBJECTS) diff --git a/infer/tests/codetoanalyze/c/errors/attributes/sentinel.c b/infer/tests/codetoanalyze/c/errors/attributes/sentinel.c new file mode 100644 index 000000000..1a6476e78 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/attributes/sentinel.c @@ -0,0 +1,16 @@ +#include + +extern int add_all_ints(int x, int y, int z, ...) __attribute__((sentinel)); + +void valid_call(int *a, int *b, int *c) { + // fine + int x = add_all_ints(0, 0, 0, a, b, c, NULL); +} + +void truncated_call(void) { + int a = 0, b = 1, c = 2, d = 3; + int *p = NULL; + + // warning: p is NULL so only first argument sent to add_all_ints + int x = add_all_ints(0, 0, 0, &a, p, &b, &c, &d, NULL); +} diff --git a/infer/tests/codetoanalyze/objc/errors/npe/nil_in_array_literal.m b/infer/tests/codetoanalyze/objc/errors/npe/nil_in_array_literal.m index b1c8e8bb6..39f5d9676 100644 --- a/infer/tests/codetoanalyze/objc/errors/npe/nil_in_array_literal.m +++ b/infer/tests/codetoanalyze/objc/errors/npe/nil_in_array_literal.m @@ -22,18 +22,39 @@ NSArray *foofoo = @[foo]; } --(void) nilInArrayLiteral { +-(void) nilInArrayLiteral0 { + NSString *str = nil; + + // nil argument in array literal crashes + NSArray *foo = @[str]; +} + +-(void) nilInArrayLiteral1 { + NSString *str = nil; + + // nil argument in array literal crashes + NSArray *foo = @[str, @"bbb"]; +} + +-(void) nilInArrayLiteral2 { NSString *str = nil; // nil argument in array literal crashes NSArray *foo = @[@"aaa", str, @"bbb"]; } +-(void) nilInArrayLiteral3 { + NSString *str = nil; + + // nil argument in array literal crashes + NSArray *foo = @[@"aaa", @"bbb", str]; +} + @end int main() { A *a = [A alloc]; [a noProblem]; - [a nilInArrayLiteral]; + [a nilInArrayLiteral0]; return 0; } diff --git a/infer/tests/endtoend/c/SentinelTest.java b/infer/tests/endtoend/c/SentinelTest.java new file mode 100644 index 000000000..afdc5ad38 --- /dev/null +++ b/infer/tests/endtoend/c/SentinelTest.java @@ -0,0 +1,48 @@ +/* + * Copyright (c) 2013- Facebook. + * All rights reserved. + */ + +package endtoend.c; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; + +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; + +public class SentinelTest { + + public static final String SOURCE_FILE = + "attributes/sentinel.c"; + + public static final String PREMATURE_NIL_TERMINATION_ARGUMENT = + "PREMATURE_NIL_TERMINATION_ARGUMENT"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults( + SentinelTest.class, + SOURCE_FILE); + } + + @Test + public void whenInferRunsOnThenPNTAisFound() + throws InterruptedException, IOException, InferException { + String[] expectedPNTAProcedures = {"truncated_call"}; + + assertThat( + "Only PNTA should be found", inferResults, + containsExactly( + PREMATURE_NIL_TERMINATION_ARGUMENT, + SOURCE_FILE, + expectedPNTAProcedures)); + } +} diff --git a/infer/tests/endtoend/objc/NPEArrayLiteralTest.java b/infer/tests/endtoend/objc/NPEArrayLiteralTest.java index c270545c3..46c90d50b 100644 --- a/infer/tests/endtoend/objc/NPEArrayLiteralTest.java +++ b/infer/tests/endtoend/objc/NPEArrayLiteralTest.java @@ -59,7 +59,12 @@ public class NPEArrayLiteralTest { PREMATURE_NIL_FILE, "no_problem")); - String[] expectedNPEProcedures = {"nilInArrayLiteral"}; + String[] expectedNPEProcedures = { + "nilInArrayLiteral0", + "nilInArrayLiteral1", + "nilInArrayLiteral2", + "nilInArrayLiteral3" + }; assertThat( "Only NPE should be found", inferResults, containsExactly(