diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index 0c4c387f3..7f7b0052c 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -929,6 +929,9 @@ let explain_dereference_as_caller_expression let position = find_formal_param_number pv_name in if !verbose then L.d_strln ("parameter number: " ^ string_of_int position); explain_nth_function_parameter use_buckets deref_str actual_pre position pvar_off + else + if Prop.has_dangling_uninit_attribute spec_pre exp then + Localise.desc_uninitialized_dangling_pointer_deref deref_str (pvar_to_string pv) loc else Localise.no_desc | None -> if !verbose then (L.d_str "explain_dereference_as_caller_expression "; Sil.d_exp exp; L.d_str ": cannot explain None "; L.d_ln ()); diff --git a/infer/src/backend/localise.ml b/infer/src/backend/localise.ml index 7e5b4cab7..19b12ad80 100644 --- a/infer/src/backend/localise.ml +++ b/infer/src/backend/localise.ml @@ -702,3 +702,18 @@ let desc_tainted_value_reaching_sensitive_function expr_str loc = expr_str (at_line tags loc) in [description], None, !tags + +let desc_uninitialized_dangling_pointer_deref deref expr_str loc = + let tags = Tags.create () in + Tags.add tags Tags.value expr_str; + let prefix = match deref.value_pre with + | Some s -> s + | _ -> "" in + let description = + Format.sprintf + "%s %s %s %s" + prefix + expr_str + deref.problem_str + (at_line tags loc) in + [description], None, !tags diff --git a/infer/src/backend/localise.mli b/infer/src/backend/localise.mli index b4296b2da..44b997acc 100644 --- a/infer/src/backend/localise.mli +++ b/infer/src/backend/localise.mli @@ -219,3 +219,5 @@ val desc_inherently_dangerous_function : Procname.t -> error_desc val desc_unary_minus_applied_to_unsigned_expression : string option -> string -> Sil.location -> error_desc val desc_tainted_value_reaching_sensitive_function : string -> Sil.location -> error_desc + +val desc_uninitialized_dangling_pointer_deref : deref_str -> string -> Sil.location -> error_desc \ No newline at end of file diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index d03d169b0..131f5b4e1 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1773,6 +1773,10 @@ let get_objc_null_attribute prop exp = let get_div0_attribute prop exp = get_attribute prop exp Sil.ACdiv0 +let has_dangling_uninit_attribute prop exp = + let la = get_exp_attributes prop exp in + list_exists (fun a -> Sil.attribute_equal a (Sil.Adangling (Sil.DAuninit))) la + (** Get all the attributes of the prop *) let get_all_attributes prop = let res = ref [] in diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index cd36c2ac0..77e0c0e75 100644 --- a/infer/src/backend/prop.mli +++ b/infer/src/backend/prop.mli @@ -289,6 +289,8 @@ val get_objc_null_attribute : 'a t -> exp -> attribute option (** Get all the attributes of the prop *) val get_all_attributes : 'a t -> (exp * attribute) list +val has_dangling_uninit_attribute : 'a t -> exp -> bool + (** Replace an attribute associated to the expression *) val add_or_replace_exp_attribute : (Sil.attribute -> Sil.attribute -> unit) -> normal t -> exp -> attribute -> normal t diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 1be555d4b..c2fd7d5b3 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -30,6 +30,7 @@ type deref_error = | Deref_minusone (** dereference -1 *) | Deref_null of Sil.path_pos (** dereference null *) | Deref_undef of Procname.t * Sil.location * Sil.path_pos (** dereference a value coming from the given undefined function *) + | Deref_undef_exp (** dereference an undefined expression *) type invalid_res = | Dereference_error of deref_error * Localise.error_desc * Paths.Path.t option (** dereference error and description *) @@ -256,6 +257,11 @@ let check_dereferences callee_pname actual_pre sub spec_pre formal_params = match deref_no_null_check_pos with | Some pos -> Some (Deref_null pos, desc true (Localise.deref_str_null (Some callee_pname))) | None -> assert false + else + (* Check if the dereferenced expr has the dangling uninitialized attribute. *) + (* In that case it raise a dangling pointer dereferece *) + if Prop.has_dangling_uninit_attribute spec_pre e then + Some (Deref_undef_exp, desc false (Localise.deref_str_dangling (Some Sil.DAuninit)) ) else if Sil.exp_equal e_sub Sil.exp_minus_one then Some (Deref_minusone, desc true (Localise.deref_str_dangling None)) else match Prop.get_resource_undef_attribute actual_pre e_sub with | Some (Sil.Aundef (s, loc, pos)) -> @@ -809,6 +815,13 @@ let get_check_exn check callee_pname loc ml_location = match check with | Prover.Class_cast_check (texp1, texp2, exp) -> class_cast_exn (Some callee_pname) texp1 texp2 exp ml_location +let check_uninitialize_dangling_deref callee_pname actual_pre sub formal_params props = + list_iter (fun (p, _ ) -> + match check_dereferences callee_pname actual_pre sub p formal_params with + | Some (Deref_undef_exp, desc) -> + raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x)) + | _ -> ()) props + (** Perform symbolic execution for a single spec *) let exe_spec tenv cfg ret_ids (n, nspecs) caller_pdesc callee_pname loc prop path_pre @@ -867,6 +880,8 @@ let exe_spec caller_pdesc callee_pname loc with | None -> Invalid_res Cannot_combine | Some results -> + (* After combining we check that we have not added a points-to of initialized variables.*) + check_uninitialize_dangling_deref callee_pname actual_pre split.sub formal_params results; let inconsistent_results, consistent_results = list_partition (fun (p, _) -> Prover.check_inconsistency p) results in let incons_pre_missing = inconsistent_actualpre_missing actual_pre (Some split) in @@ -989,6 +1004,10 @@ let exe_call_postprocess tenv ret_ids trace_call callee_pname loc initial_prop r trace_call Specs.CallStats.CR_not_met; extend_path path_opt None; raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAminusone, desc, try assert false with Assert_failure x -> x)) + | Dereference_error (Deref_undef_exp, desc, path_opt) -> + trace_call Specs.CallStats.CR_not_met; + extend_path path_opt None; + raise (Exceptions.Dangling_pointer_dereference (Some Sil.DAuninit, desc, try assert false with Assert_failure x -> x)) | Dereference_error (Deref_null pos, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met; extend_path path_opt (Some pos); diff --git a/infer/tests/codetoanalyze/c/errors/Makefile b/infer/tests/codetoanalyze/c/errors/Makefile index 70a71dc57..dcb6924bb 100644 --- a/infer/tests/codetoanalyze/c/errors/Makefile +++ b/infer/tests/codetoanalyze/c/errors/Makefile @@ -9,6 +9,7 @@ all: make -C resource_leaks make -C memory_leaks make -C lists + make -C dangling_deref clean: make -C arithmetic clean @@ -20,4 +21,5 @@ clean: make -C resource_leaks clean make -C memory_leaks make -C lists + make -C dangling_deref diff --git a/infer/tests/codetoanalyze/c/errors/dangling_deref/Makefile b/infer/tests/codetoanalyze/c/errors/dangling_deref/Makefile new file mode 100644 index 000000000..ec67ebe4f --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/dangling_deref/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/dangling_deref/dpd.c b/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c new file mode 100644 index 000000000..bba2069ea --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c @@ -0,0 +1,43 @@ +#include +#include + +int *set42(int* x) { + + *x=42; + return x; +} + +void nodpd () { + + int w,z; + + z=set42(&w); + +} + +void nodpd1 () { + + int *y = malloc(sizeof(int)); + int *z; + z=set42(y); + free(y); + +} + + + +void dpd () { + + int *y; + int *z; + z=set42(y); +} + + +void intraprocdpd () { + + int *y; + int *z; + *y=42; + z=y; +} diff --git a/infer/tests/endtoend/c/DanglingDereferenceTest.java b/infer/tests/endtoend/c/DanglingDereferenceTest.java new file mode 100644 index 000000000..88a422a5a --- /dev/null +++ b/infer/tests/endtoend/c/DanglingDereferenceTest.java @@ -0,0 +1,62 @@ +/* + * Copyright (c) 2013- Facebook. + * All rights reserved. + */ + +package endtoend.c; + +import static org.hamcrest.MatcherAssert.assertThat; +import static utils.matchers.ResultContainsExactly.containsExactly; +import static utils.matchers.ResultContainsLineNumbers.containsLines; +import static utils.matchers.ResultContainsErrorInMethod.contains; +import org.junit.BeforeClass; +import org.junit.Test; + +import java.io.IOException; + +import utils.InferException; +import utils.InferResults; +import utils.InferRunner; + +public class DanglingDereferenceTest { + + public static final String SOURCE_FILE = + "dangling_deref/dpd.c"; + + public static final String DANGLING_POINTER_DEREFERENCE = "DANGLING_POINTER_DEREFERENCE"; + + private static InferResults inferResults; + + @BeforeClass + public static void runInfer() throws InterruptedException, IOException { + inferResults = InferResults.loadCInferResults( + DanglingDereferenceTest.class, + SOURCE_FILE); + } + + + @Test + public void DanglingDereferenceTest1() throws InterruptedException, IOException, InferException { + assertThat( + "Results should contain dangling pointer dereference error", + inferResults, + contains( + DANGLING_POINTER_DEREFERENCE, + SOURCE_FILE, + "dpd")); + } + + @Test + public void DanglingDereferenceTest2() throws InterruptedException, IOException, InferException { + assertThat( + "Results should contain dangling pointer dereference error", + inferResults, + contains( + DANGLING_POINTER_DEREFERENCE, + SOURCE_FILE, + "intraprocdpd")); + } + + + +} \ No newline at end of file diff --git a/infer/tests/utils/InferResults.java b/infer/tests/utils/InferResults.java index 23877ed94..af1e93011 100644 --- a/infer/tests/utils/InferResults.java +++ b/infer/tests/utils/InferResults.java @@ -60,6 +60,7 @@ public class InferResults { errorType.equals("RETURN_VALUE_IGNORED") || errorType.equals("IMMUTABLE_CAST") || errorType.equals("PARAMETER_NOT_NULL_CHECKED") || + errorType.equals("DANGLING_POINTER_DEREFERENCE") || errorType.equals("IVAR_NOT_NULL_CHECKED") || errorType.startsWith("ERADICATE")) { Integer errorLine = Integer.parseInt(items[5].trim());