[pulse] added user-defined models for malloc/free

Reviewed By: jvillard

Differential Revision: D28549360

fbshipit-source-id: c5e6466cf

infer/man/man1/infer-analyze.txt

@@ -286,6 +286,12 @@ OPTIONS
        --pulse-model-alloc-pattern string
            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
+
+       --pulse-model-malloc-pattern string
+           Regex of methods that should be modelled as mallocs in Pulse
+
        --pulse-model-release-pattern string
            Regex of methods that should be modelled as release in Pulse
 

infer/man/man1/infer-full.txt

@@ -1005,6 +1005,14 @@ OPTIONS
            Regex of methods that should be modelled as allocs in Pulse       
     See also infer-analyze(1).
 
+       --pulse-model-free-pattern string
+           Regex of methods that should be modelled as free in Pulse       
+    See also infer-analyze(1).
+
+       --pulse-model-malloc-pattern string
+           Regex of methods that should be modelled as mallocs in Pulse       
+    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).
@@ -1937,6 +1945,12 @@ INTERNAL OPTIONS
        --pulse-model-alloc-pattern-reset
            Cancel the effect of --pulse-model-alloc-pattern.
 
+       --pulse-model-free-pattern-reset
+           Cancel the effect of --pulse-model-free-pattern.
+
+       --pulse-model-malloc-pattern-reset
+           Cancel the effect of --pulse-model-malloc-pattern.
+
        --pulse-model-release-pattern-reset
            Cancel the effect of --pulse-model-release-pattern.
 

infer/man/man1/infer.txt

@@ -1005,6 +1005,14 @@ OPTIONS
            Regex of methods that should be modelled as allocs in Pulse       
     See also infer-analyze(1).
 
+       --pulse-model-free-pattern string
+           Regex of methods that should be modelled as free in Pulse       
+    See also infer-analyze(1).
+
+       --pulse-model-malloc-pattern string
+           Regex of methods that should be modelled as mallocs in Pulse       
+    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,6 +2012,18 @@ 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"
+    ~in_help:InferCommand.[(Analyze, manual_generic)]
+    "Regex of methods that should be modelled as mallocs 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"
+
+
 and pulse_model_alloc_pattern =
   CLOpt.mk_string_opt ~long:"pulse-model-alloc-pattern"
     ~in_help:InferCommand.[(Analyze, manual_generic)]
@@ -3268,6 +3280,10 @@ and pulse_max_disjuncts = !pulse_max_disjuncts
 
 and pulse_model_abort = RevList.to_list !pulse_model_abort
 
+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_release_pattern = Option.map ~f:Str.regexp !pulse_model_release_pattern

infer/src/base/Config.mli

@@ -498,6 +498,10 @@ val pulse_model_abort : string list
 
 val pulse_model_alloc_pattern : Str.regexp option
 
+val pulse_model_free_pattern : Str.regexp option
+
+val pulse_model_malloc_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

@@ -1799,6 +1799,8 @@ 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/Makefile

@@ -7,7 +7,7 @@ TESTS_DIR = ../../..
 
 CLANG_OPTIONS = -c
 INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
-  --pulse-report-latent-issues
+  --pulse-report-latent-issues --pulse-model-malloc-pattern a_malloc
 
 INFERPRINT_OPTIONS = --issues-tests
 

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

@@ -31,6 +31,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 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, null_alias_bad, 4, 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, 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

@@ -30,6 +30,7 @@ codetoanalyze/c/pulse/nullptr.c, malloc_then_call_create_null_path_then_deref_un
 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, null_alias_bad, 4, 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, 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/nullptr.c

@@ -89,6 +89,8 @@ 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);