diff --git a/infer/src/checkers/impurity.ml b/infer/src/checkers/impurity.ml index 12d4d0e12..65cd89def 100644 --- a/infer/src/checkers/impurity.ml +++ b/infer/src/checkers/impurity.ml @@ -99,8 +99,15 @@ let extract_impurity pdesc pre_post : ImpurityDomain.t = |> List.fold_left ~init:ImpurityDomain.ModifiedVarSet.empty ~f:(fun acc (name, typ) -> let var = Var.of_pvar (Pvar.mk name pname) in match BaseStack.find_opt var post_stack with - | Some (addr, _) when Typ.is_pointer typ -> - add_to_modified var addr acc + | Some (addr, _) when Typ.is_pointer typ -> ( + match BaseMemory.find_opt addr pre_heap with + | Some (edges_pre, _) -> + BaseMemory.Edges.fold + (fun _ (addr, _) acc -> add_to_modified var addr acc) + edges_pre acc + | None -> + debug "The address is not materialized in pre-heap." ; + acc ) | _ -> acc ) in diff --git a/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp b/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp index 4d9bd2485..a99dbe7a7 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp +++ b/infer/tests/codetoanalyze/cpp/impurity/invalid_test.cpp @@ -5,7 +5,6 @@ * LICENSE file in the root directory of this source tree. */ #include - int* global_pointer; void free_global_pointer_impure() { free(global_pointer); } @@ -30,7 +29,30 @@ void local_deleted_pure() { delete s; } -Simple* reassign_impure(Simple* s) { +Simple* reassign_pure(Simple* s) { s = new Simple{2}; return s; } + +Simple* reassign_impure(Simple* s) { + *s = *(new Simple{2}); + return s; +} + +void swap_impure(Simple* s1, Simple* s2) { + Simple temp = *s2; + *s2 = *s1; + *s1 = temp; +} + +void swap_pure(Simple* s1, Simple* s2) { + Simple* temp = s2; + s2 = s1; + s1 = temp; +} + +void swap_address_impure(Simple& lhs, Simple& rhs) { + Simple temp = rhs; + rhs = lhs; + lhs = temp; +} diff --git a/infer/tests/codetoanalyze/cpp/impurity/issues.exp b/infer/tests/codetoanalyze/cpp/impurity/issues.exp index 9a5df05bc..2da6795e6 100644 --- a/infer/tests/codetoanalyze/cpp/impurity/issues.exp +++ b/infer/tests/codetoanalyze/cpp/impurity/issues.exp @@ -11,12 +11,15 @@ codetoanalyze/cpp/impurity/global_test.cpp, local_static_var_impure, 0, IMPURE_F codetoanalyze/cpp/impurity/global_test.cpp, modify_global_array_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_array_impure,global variable `a` accessed here,global variable `a` modified here] codetoanalyze/cpp/impurity/global_test.cpp, modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(), 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_inside_lamda_impure::lambda_global_test.cpp:33:14::operator(),global variable `x` accessed here,global variable `x` modified here] codetoanalyze/cpp/impurity/global_test.cpp, modify_global_primitive_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_global_primitive_impure,global variable `x` accessed here,global variable `x` modified here] +codetoanalyze/cpp/impurity/invalid_test.cpp, Simple::operator=, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Simple::operator=,parameter `this` of Simple::operator=,parameter `this` modified here] codetoanalyze/cpp/impurity/invalid_test.cpp, delete_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function delete_param_impure,parameter `s` of delete_param_impure,parameter `s` was invalidated by `delete` here] codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function double_free_global_impure] codetoanalyze/cpp/impurity/invalid_test.cpp, double_free_global_impure, 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_impure` 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_impure` here,global variable `global_pointer` accessed here,invalid access occurs here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_global_pointer_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_global_pointer_impure,global variable `global_pointer` accessed here,global variable `global_pointer` was invalidated by call to `free()` here] codetoanalyze/cpp/impurity/invalid_test.cpp, free_param_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function free_param_impure,parameter `x` of free_param_impure,parameter `x` was invalidated by call to `free()` here] -codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter `s` of reassign_impure,parameter `s` modified here] +codetoanalyze/cpp/impurity/invalid_test.cpp, reassign_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function reassign_impure,parameter `s` of reassign_impure,when calling `Simple::operator=` here,parameter `this` of Simple::operator=,parameter `s` modified here] +codetoanalyze/cpp/impurity/invalid_test.cpp, swap_address_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function swap_address_impure,parameter `rhs` of swap_address_impure,when calling `Simple::operator=` here,parameter `this` of Simple::operator=,parameter `rhs` modified here,parameter `lhs` of swap_address_impure,when calling `Simple::operator=` here,parameter `this` of Simple::operator=,parameter `lhs` modified here] +codetoanalyze/cpp/impurity/invalid_test.cpp, swap_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function swap_impure,parameter `s2` of swap_impure,when calling `Simple::operator=` here,parameter `this` of Simple::operator=,parameter `s2` modified here,parameter `s1` of swap_impure,when calling `Simple::operator=` here,parameter `this` of Simple::operator=,parameter `s1` modified here] codetoanalyze/cpp/impurity/param_test.cpp, create_cycle_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function create_cycle_impure,parameter `x` of create_cycle_impure,parameter `x` modified here] codetoanalyze/cpp/impurity/param_test.cpp, invalidate_local_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function invalidate_local_impure,parameter `pp` of invalidate_local_impure,parameter `pp` modified here] codetoanalyze/cpp/impurity/param_test.cpp, modify_mut_ref_impure, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function modify_mut_ref_impure,parameter `x` of modify_mut_ref_impure,parameter `x` modified here] diff --git a/infer/tests/codetoanalyze/java/impurity/Localities.java b/infer/tests/codetoanalyze/java/impurity/Localities.java index 67ebc5221..7aeaba8e8 100644 --- a/infer/tests/codetoanalyze/java/impurity/Localities.java +++ b/infer/tests/codetoanalyze/java/impurity/Localities.java @@ -135,11 +135,10 @@ class Localities { return tmp.bar; } - // This behavior seems to be different than C++ // @pure, @loc:{} - boolean copy_ref_pure_FP(int[] a, int b) { + boolean copy_ref_pure(int[] a, int b) { int[] local = a; // copy reference - a = new int[1]; // can't detect that a becomes fresh + a = new int[1]; // a becomes fresh a[0] = local[0]; // not modification return true; } @@ -153,4 +152,10 @@ class Localities { b = a[0]; // not modification return true; } + + void swap_pure(Object s1, Object s2) { + Object temp = s2; + s2 = s1; + s1 = temp; + } } diff --git a/infer/tests/codetoanalyze/java/impurity/issues.exp b/infer/tests/codetoanalyze/java/impurity/issues.exp index 1591496de..7a807414e 100644 --- a/infer/tests/codetoanalyze/java/impurity/issues.exp +++ b/infer/tests/codetoanalyze/java/impurity/issues.exp @@ -5,8 +5,7 @@ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.global_mod_via_argument_ codetoanalyze/java/impurity/GlobalTest.java, GlobalTest.incr(GlobalTest$Foo,int):void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` of void GlobalTest.incr(GlobalTest$Foo,int),parameter `foo` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Counter.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Counter.inc_impure(),parameter `this` of void Localities$Counter.inc_impure(),parameter `this` modified here] codetoanalyze/java/impurity/Localities.java, Localities$Foo.inc_impure():void, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function void Localities$Foo.inc_impure(),parameter `this` of void Localities$Foo.inc_impure(),parameter `this` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),parameter `a` modified here] -codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_pure_FP(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` of boolean Localities.copy_ref_pure_FP(int[],int),parameter `a` modified here] +codetoanalyze/java/impurity/Localities.java, Localities.copy_ref_impure(int[],int):boolean, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function boolean Localities.copy_ref_impure(int[],int),parameter `a` of boolean Localities.copy_ref_impure(int[],int),assigned,parameter `a` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_array_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo[], 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo[] Localities.get_array_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_f_impure(Localities$Foo[],int,Localities$Foo):Localities$Foo, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),parameter `array` of Localities$Foo Localities.get_f_impure(Localities$Foo[],int,Localities$Foo),assigned,parameter `array` modified here] codetoanalyze/java/impurity/Localities.java, Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo):Localities$Bar, 0, IMPURE_FUNCTION, no_bucket, ERROR, [Impure function Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here,parameter `array` of Localities$Bar Localities.get_foo_via_tmp_impure(Localities$Foo[],int,Localities$Foo,Localities$Foo),assigned,parameter `array` modified here]