[pulse] more config options to model dynamic memory management

Summary:
Add an option for realloc and fiddle with the other options' help for
consistency.

Moved the memory leak test to memory_leak.c and added more.

Moved the place where we take the options into account closer to their
corresponding models to defend a bit against modifying one without
modifying the other.

Reviewed By: da319

Differential Revision: D28543340

fbshipit-source-id: 75894d06d

infer/man/man1/infer-analyze.txt

@@ -287,10 +287,22 @@ OPTIONS
            Regex of methods that should be modelled as allocs in Pulse
 
        --pulse-model-free-pattern string
-           Regex of methods that should be modelled as free in Pulse
+           Regex of methods that should be modelled as wrappers to free(3) in
+           Pulse. The pointer to be freed should be the first argument of the
+           function. This should only be needed if the code of the wrapper is
+           not visible to infer or if Pulse somehow doesn't understand it
+           (e.g. the call is dispatched to global function pointers).
 
        --pulse-model-malloc-pattern string
-           Regex of methods that should be modelled as mallocs in Pulse
+           Regex of methods that should be modelled as wrappers to malloc(3)
+           in Pulse. The size to allocate should be the first argument of the
+           function. See --pulse-model-free-pattern for more information.
+
+       --pulse-model-realloc-pattern string
+           Regex of methods that should be modelled as wrappers to realloc(3)
+           in Pulse. The pointer to be reallocated should be the first
+           argument of the function and the new size the second argument. See
+           --pulse-model-free-pattern for more information.
 
        --pulse-model-release-pattern string
            Regex of methods that should be modelled as release in Pulse

infer/man/man1/infer-full.txt

@@ -1007,13 +1007,25 @@ OPTIONS
     See also infer-analyze(1).
 
        --pulse-model-free-pattern string
-           Regex of methods that should be modelled as free in Pulse       
+           Regex of methods that should be modelled as wrappers to free(3) in
+           Pulse. The pointer to be freed should be the first argument of the
+           function. This should only be needed if the code of the wrapper is
+           not visible to infer or if Pulse somehow doesn't understand it
+           (e.g. the call is dispatched to global function pointers).       
     See also infer-analyze(1).
 
        --pulse-model-malloc-pattern string
-           Regex of methods that should be modelled as mallocs in Pulse       
+           Regex of methods that should be modelled as wrappers to malloc(3)
+           in Pulse. The size to allocate should be the first argument of the
+           function. See --pulse-model-free-pattern for more information.       
     See also infer-analyze(1).
 
+       --pulse-model-realloc-pattern string
+           Regex of methods that should be modelled as wrappers to realloc(3)
+           in Pulse. The pointer to be reallocated should be the first
+           argument of the function and the new size the second argument. See
+           --pulse-model-free-pattern for more information.           See also infer-analyze(1).
+
        --pulse-model-release-pattern string
            Regex of methods that should be modelled as release in Pulse       
     See also infer-analyze(1).
@@ -1952,6 +1964,9 @@ INTERNAL OPTIONS
        --pulse-model-malloc-pattern-reset
            Cancel the effect of --pulse-model-malloc-pattern.
 
+       --pulse-model-realloc-pattern-reset
+           Cancel the effect of --pulse-model-realloc-pattern.
+
        --pulse-model-release-pattern-reset
            Cancel the effect of --pulse-model-release-pattern.
 

infer/man/man1/infer.txt

@@ -1007,13 +1007,25 @@ OPTIONS
     See also infer-analyze(1).
 
        --pulse-model-free-pattern string
-           Regex of methods that should be modelled as free in Pulse       
+           Regex of methods that should be modelled as wrappers to free(3) in
+           Pulse. The pointer to be freed should be the first argument of the
+           function. This should only be needed if the code of the wrapper is
+           not visible to infer or if Pulse somehow doesn't understand it
+           (e.g. the call is dispatched to global function pointers).       
     See also infer-analyze(1).
 
        --pulse-model-malloc-pattern string
-           Regex of methods that should be modelled as mallocs in Pulse       
+           Regex of methods that should be modelled as wrappers to malloc(3)
+           in Pulse. The size to allocate should be the first argument of the
+           function. See --pulse-model-free-pattern for more information.       
     See also infer-analyze(1).
 
+       --pulse-model-realloc-pattern string
+           Regex of methods that should be modelled as wrappers to realloc(3)
+           in Pulse. The pointer to be reallocated should be the first
+           argument of the function and the new size the second argument. See
+           --pulse-model-free-pattern for more information.           See also infer-analyze(1).
+
        --pulse-model-release-pattern string
            Regex of methods that should be modelled as release in Pulse       
     See also infer-analyze(1).

infer/src/base/Config.ml

@@ -2012,22 +2012,35 @@ and pulse_model_abort =
     "Methods that should be modelled as abort in Pulse"
 
 
-and pulse_model_malloc_pattern =
-  CLOpt.mk_string_opt ~long:"pulse-model-malloc-pattern"
+and pulse_model_alloc_pattern =
+  CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
-    "Regex of methods that should be modelled as mallocs in Pulse"
+    "Regex of methods that should be modelled as allocs in Pulse"
 
 
 and pulse_model_free_pattern =
   CLOpt.mk_string_opt ~long:"pulse-model-free-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
-    "Regex of methods that should be modelled as free in Pulse"
+    "Regex of methods that should be modelled as wrappers to $(i,free)(3) in Pulse. The pointer to \
+     be freed should be the first argument of the function. This should only be needed if the code \
+     of the wrapper is not visible to infer or if Pulse somehow doesn't understand it (e.g. the \
+     call is dispatched to global function pointers)."
 
 
-and pulse_model_alloc_pattern =
-  CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern"
+and pulse_model_malloc_pattern =
+  CLOpt.mk_string_opt ~long:"pulse-model-malloc-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
-    "Regex of methods that should be modelled as allocs in Pulse"
+    "Regex of methods that should be modelled as wrappers to $(i,malloc)(3) in Pulse. The size to \
+     allocate should be the first argument of the function. See $(b,--pulse-model-free-pattern) \
+     for more information."
+
+
+and pulse_model_realloc_pattern =
+  CLOpt.mk_string_opt ~long:"pulse-model-realloc-pattern"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Regex of methods that should be modelled as wrappers to $(i,realloc)(3) in Pulse. The pointer \
+     to be reallocated should be the first argument of the function and the new size the second \
+     argument. See $(b,--pulse-model-free-pattern) for more information."
 
 
 and pulse_model_release_pattern =
@@ -3287,11 +3300,13 @@ and pulse_max_disjuncts = !pulse_max_disjuncts
 
 and pulse_model_abort = RevList.to_list !pulse_model_abort
 
+and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern
+
 and pulse_model_free_pattern = Option.map ~f:Str.regexp !pulse_model_free_pattern
 
 and pulse_model_malloc_pattern = Option.map ~f:Str.regexp !pulse_model_malloc_pattern
 
-and pulse_model_alloc_pattern = Option.map ~f:Str.regexp !pulse_model_alloc_pattern
+and pulse_model_realloc_pattern = Option.map ~f:Str.regexp !pulse_model_realloc_pattern
 
 and pulse_model_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern
 

infer/src/base/Config.mli

@@ -502,6 +502,8 @@ val pulse_model_free_pattern : Str.regexp option
 
 val pulse_model_malloc_pattern : Str.regexp option
 
+val pulse_model_realloc_pattern : Str.regexp option
+
 val pulse_model_release_pattern : Str.regexp option
 
 val pulse_model_return_first_arg : Str.regexp option

infer/src/pulse/PulseModels.ml

@@ -1412,8 +1412,12 @@ module ProcNameDispatcher = struct
     make_dispatcher
       ( transfer_ownership_matchers @ abort_matchers
       @ [ +BuiltinDecl.(match_builtin free) <>$ capt_arg_payload $--> C.free
+        ; +match_regexp_opt Config.pulse_model_free_pattern <>$ capt_arg_payload $+...$--> C.free
         ; +BuiltinDecl.(match_builtin malloc) <>$ capt_exp $--> C.malloc
+        ; +match_regexp_opt Config.pulse_model_malloc_pattern <>$ capt_exp $+...$--> C.malloc
         ; -"realloc" <>$ capt_arg_payload $+ capt_exp $--> C.realloc
+        ; +match_regexp_opt Config.pulse_model_realloc_pattern
+          <>$ capt_arg_payload $+ capt_exp $+...$--> C.realloc
         ; +BuiltinDecl.(match_builtin __delete) <>$ capt_arg_payload $--> Cplusplus.delete
         ; +BuiltinDecl.(match_builtin __new)
           <>$ capt_exp
@@ -1814,8 +1818,6 @@ module ProcNameDispatcher = struct
           <>$ capt_arg_payload
           $+...$--> Misc.id_first_arg
                       ~desc:"modelled as returning the first argument due to configuration option"
-        ; +match_regexp_opt Config.pulse_model_malloc_pattern <>$ capt_exp $+...$--> C.malloc
-        ; +match_regexp_opt Config.pulse_model_free_pattern <>$ capt_arg_payload $--> C.free
         ; +match_regexp_opt Config.pulse_model_skip_pattern
           &::.*++> Misc.skip "modelled as skip due to configuration option" ] )
 end

infer/tests/codetoanalyze/c/pulse/.inferconfig

@@ -0,0 +1,5 @@
+{
+  "pulse-model-free-pattern": "^my_free$",
+  "pulse-model-malloc-pattern": "\\(my\\|a\\)_malloc",
+  "pulse-model-realloc-pattern": "my_realloc"
+}

infer/tests/codetoanalyze/c/pulse/Makefile

@@ -7,10 +7,12 @@ TESTS_DIR = ../../..
 
 CLANG_OPTIONS = -c
 INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
-  --pulse-report-latent-issues --pulse-model-malloc-pattern a_malloc
+  --pulse-report-latent-issues
 
 INFERPRINT_OPTIONS = --issues-tests
 
 SOURCES = $(wildcard *.c)
 
 include $(TESTS_DIR)/clang.make
+
+infer-out$(TEST_SUFFIX)/report.json: .inferconfig

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

@@ -25,6 +25,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DE
 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/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
+codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_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]
 codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
@@ -35,7 +37,6 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, 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, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
-codetoanalyze/c/pulse/nullptr.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `l` of access_use_after_free_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `l` of access_use_after_free_bad,invalid access occurs here]
 codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]

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

@@ -25,6 +25,8 @@ codetoanalyze/c/pulse/memory_leak.c, malloc_ptr_no_check_leak_bad, 2, NULLPTR_DE
 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/memory_leak.c, test_config_options_no_free_bad, 2, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `my_realloc` here,memory becomes unreachable here]
+codetoanalyze/c/pulse/memory_leak.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_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]
 codetoanalyze/c/pulse/nullptr.c, bug_with_allocation_bad, 1, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `malloc` here,memory becomes unreachable here]
@@ -35,7 +37,6 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 codetoanalyze/c/pulse/nullptr.c, null_alias_bad, 3, 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, null_alias_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/nullptr.c, nullptr_deref_young_bad, 5, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
-codetoanalyze/c/pulse/nullptr.c, user_malloc_leak_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by `a_malloc` here,memory becomes unreachable here]
 codetoanalyze/c/pulse/traces.c, access_null_deref_bad, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [is the null pointer,assigned,invalid access occurs here]
 codetoanalyze/c/pulse/traces.c, access_use_after_free_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,invalid access occurs here]
 codetoanalyze/c/pulse/traces.c, call_makes_null_deref_manifest_bad, 4, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `something_about_strings_latent`,null pointer dereference part of the trace starts here,in call to `malloc` (modelled),is the null pointer,assigned,invalid access occurs here]

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

@@ -121,3 +121,27 @@ void realloc_no_check_bad() {
   *q = 42;
   free(q);
 }
+
+void* my_malloc(size_t size);
+void* a_malloc(size_t size);
+void my_free(void* p);
+void* my_realloc(void* p, size_t size);
+
+void user_malloc_leak_bad() { int* x = (int*)a_malloc(sizeof(int)); }
+
+void test_config_options_1_ok() {
+  int* p = (int*)malloc(sizeof(int));
+  int* q = my_realloc(p, sizeof(int));
+  my_free(q);
+}
+
+void test_config_options_2_ok() {
+  int* p = (int*)my_malloc(sizeof(int));
+  int* q = realloc(p, sizeof(int));
+  my_free(q);
+}
+
+void test_config_options_no_free_bad() {
+  int* p = (int*)my_malloc(sizeof(int));
+  int* q = my_realloc(p, sizeof(int));
+}

infer/tests/codetoanalyze/c/pulse/nullptr.c

@@ -89,8 +89,6 @@ void wrap_malloc(int** x) {
   }
 }
 
-void user_malloc_leak_bad() { int* x = (int*)a_malloc(sizeof(int)); }
-
 void call_no_return_good() {
   int* x = NULL;
   wrap_malloc(&x);