[pulse] model realloc(3)

Summary:
Let's model all the dynamic memory management functions as they all work
together and are important for a lot of C projects.

Reviewed By: ezgicicek

Differential Revision: D28543008

fbshipit-source-id: f130e1ab6

infer/src/pulse/PulseModels.ml

@@ -227,6 +227,21 @@ module C = struct
   let malloc_not_null size_exp = malloc_not_null_common ~size_exp_opt:(Some size_exp)
 
   let malloc_not_null_no_param = malloc_not_null_common ~size_exp_opt:None
+
+  let realloc pointer size : model =
+   fun data astate ->
+    free pointer data astate
+    |> List.concat_map ~f:(fun result ->
+           let<*> exec_state = result in
+           match (exec_state : ExecutionDomain.t) with
+           | ContinueProgram astate ->
+               malloc size data astate
+           | ExitProgram _
+           | AbortProgram _
+           | LatentAbortProgram _
+           | LatentInvalidAccess _
+           | ISLLatentMemoryError _ ->
+               [Ok exec_state] )
 end
 
 module ObjCCoreFoundation = struct
@@ -1398,6 +1413,7 @@ module ProcNameDispatcher = struct
       ( transfer_ownership_matchers @ abort_matchers
       @ [ +BuiltinDecl.(match_builtin free) <>$ capt_arg_payload $--> C.free
         ; +BuiltinDecl.(match_builtin malloc) <>$ capt_exp $--> C.malloc
+        ; -"realloc" <>$ capt_arg_payload $+ capt_exp $--> C.realloc
         ; +BuiltinDecl.(match_builtin __delete) <>$ capt_arg_payload $--> Cplusplus.delete
         ; +BuiltinDecl.(match_builtin __new)
           <>$ capt_exp

infer/tests/codetoanalyze/c/pulse/issues.exp

@@ -22,6 +22,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_out_parameter_local_mutation_bad, 3,
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc_via_ptr`,is the null pointer,returned,return from call to `malloc_via_ptr`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]

infer/tests/codetoanalyze/c/pulse/issues.exp-isl

@@ -22,6 +22,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_out_parameter_local_mutation_bad, 3,
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `malloc_via_ptr` here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc_via_ptr`,is the null pointer,returned,return from call to `malloc_via_ptr`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_check_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,in call to `realloc_wrapper`,in call to `realloc` (modelled),is the null pointer,returned,return from call to `realloc_wrapper`,assigned,invalid access occurs here]
+codetoanalyze/c/pulse/memory_leak.c, realloc_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `realloc_wrapper` here,allocated by `realloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/memory_leak.c, report_leak_in_correct_line_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_abduction_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, bug_after_malloc_result_test_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]

infer/tests/codetoanalyze/c/pulse/memory_leak.c

@@ -101,3 +101,23 @@ void report_leak_in_correct_line_bad(int* x) {
   }
   free(x);
 }
+
+void* realloc_wrapper(void* p, size_t size) { return realloc(p, size); }
+
+void realloc_free_ok() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+  free(q);
+}
+
+void realloc_no_free_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+}
+
+void realloc_no_check_bad() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = realloc_wrapper(p, sizeof(int));
+  *q = 42;
+  free(q);
+}