Adding a test in symbolic execution when a dangling uninitialized pointer is dereferenced

Summary:
The symbolic execution was not stopping in case an unitialized dangling pointer was
passed to a function and then dereferenced inside the callee.
What would happen is that a wrong footprint would be added to the unititialized pointer
at the end of the function call in the caller proposition.

This checks that if we do:

frame * new_footprint

checks that we do not add heap predicates to the frame into uninitialized local variables.
If we can identify the variable then we raise a danglind pointer dereference. If instead
we cannot give a good explanation we give an internal error.
The latter case should be temporary. We should find a general way to raise dangling pointer
deref instead of the internal error.

I also fixed the model of getc that was the way I found the problem.

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 ());

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

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

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

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
 

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);

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
 

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)

infer/tests/codetoanalyze/c/errors/dangling_deref/dpd.c

@@ -0,0 +1,43 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+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;
+}

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"));
+    }
+    
+    
+    
+}

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());