From f5936689a45f98f5fe40bf6132ee08e4b527f61d Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 1 Feb 2021 11:57:52 -0800 Subject: [PATCH] [pulse] case split in model of free(3) Summary: Having different behaviours inter-procedurally and intra-procedurally sounds like a bad design in retrospect. The model of free() should not depend on whether we currently know the value is not null as that means some specs are missing from the summary. Reviewed By: skcho Differential Revision: D26019712 fbshipit-source-id: 1ac4316a5 --- infer/src/pulse/PulseModels.ml | 16 ++++++++-------- .../codetoanalyze/c/pulse/interprocedural.c | 4 ++-- infer/tests/codetoanalyze/c/pulse/issues.exp | 2 ++ infer/tests/codetoanalyze/cpp/pulse/issues.exp | 1 + .../codetoanalyze/cpp/pulse/use_after_free.cpp | 6 ++++++ 5 files changed, 19 insertions(+), 10 deletions(-) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 747840027..3059338d7 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -116,15 +116,12 @@ module Misc = struct let free_or_delete operation deleted_access : model = fun _ ~callee_procname:_ location ~ret:_ astate -> - (* NOTE: we could introduce a case-split explicitly on =0 vs ≠0 but instead only act on what we - currently know about the value. This is purely to avoid contributing to path explosion. *) - (* freeing 0 is a no-op *) - if PulseArithmetic.is_known_zero astate (fst deleted_access) then ok_continue astate - else + (* NOTE: freeing 0 is a no-op so we introduce a case split *) + let invalidation = + match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete + in + let astates_alloc = let astate = PulseArithmetic.and_positive (fst deleted_access) astate in - let invalidation = - match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete - in if Config.pulse_isl then match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with | Error _ as err -> @@ -134,6 +131,9 @@ module Misc = struct else let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in astate + in + let astate_zero = PulseArithmetic.and_eq_int (fst deleted_access) IntLit.zero astate in + Ok (ContinueProgram astate_zero) :: astates_alloc end module C = struct diff --git a/infer/tests/codetoanalyze/c/pulse/interprocedural.c b/infer/tests/codetoanalyze/c/pulse/interprocedural.c index d51a3501a..a1f6ab68e 100644 --- a/infer/tests/codetoanalyze/c/pulse/interprocedural.c +++ b/infer/tests/codetoanalyze/c/pulse/interprocedural.c @@ -13,10 +13,10 @@ void if_freed_invalid_latent(int x, int* y) { } } -void FN_call_if_freed_invalid_latent(int x) { +void call_if_freed_invalid_latent(int x) { if (x > 0) { if_freed_invalid_latent(x, NULL); } } -void FN_call_if_freed_invalid2_bad() { FN_call_if_freed_invalid_latent(7); } +void call_if_freed_invalid2_bad() { call_if_freed_invalid_latent(7); } diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index f8bfe2f5a..f27909aef 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -1,5 +1,7 @@ codetoanalyze/c/pulse/frontend.c, assign_implicit_cast_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/c/pulse/frontend.c, assign_paren_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid2_bad, 0, NULLPTR_DEREFERENCE, no_bucket, ERROR, [calling context starts here,in call to `call_if_freed_invalid_latent`,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] +codetoanalyze/c/pulse/interprocedural.c, call_if_freed_invalid_latent, 2, NULLPTR_DEREFERENCE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,when calling `if_freed_invalid_latent` here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index e952a1d72..3ae733fb2 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -116,6 +116,7 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_afte codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor::use_after_scope4_bad, 6, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `c` declared here,is the address of a stack variable `c` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `c` declared here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_global_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,global variable `global_pointer` accessed here,when calling `free_global_pointer_ok` here,global variable `global_pointer` accessed here,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, double_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of double_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of double_free_simple_bad,invalid access occurs here] +codetoanalyze/cpp/pulse/use_after_free.cpp, free_null_then_deref_bad, 3, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of use_after_free_simple_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of use_after_free_simple_bad,invalid access occurs here] codetoanalyze/cpp/pulse/use_after_scope.cpp, access_out_of_scope_stack_ref_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [invalidation part of the trace starts here,variable `p` declared here,when calling `invalidate_local_ok` here,variable `t` declared here,is the address of a stack variable `t` whose lifetime has ended,use-after-lifetime part of the trace starts here,variable `p` declared here,passed as argument to `invalidate_local_ok`,variable `t` declared here,assigned,return from call to `invalidate_local_ok`,invalid access occurs here] codetoanalyze/cpp/pulse/values.cpp, error_under_true_conditionals_bad, 5, USE_AFTER_FREE, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `x` of error_under_true_conditionals_bad,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp index 7ff1679d3..9188c56c3 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/use_after_free.cpp @@ -24,3 +24,9 @@ void double_free_global_bad() { free_global_pointer_ok(); free_global_pointer_ok(); } + +void free_null_then_deref_bad() { + int* x = NULL; + free(x); + *x = 1; +}