[pulse] Loosen fieldname comparison in state

Summary:
When C and C++ code handle a common struct typed value, the struct
type is handled as a `CStruct` in the C code, but as a `CppClass` in
the C++ code.  On the other hand, `Fieldname.t` contains a string of
field and **the struct type**.  As a result, even if a same field is
accessed in C and C++ code, the accessed fieldnames are different.

```
void callee_in_c(struct s* x) {
  x->a = 3;
}

void caller_in_cpp() {
  struct s x;
  x.a = 5;
  callee_in_c(&x);
  // HERE
}
```

For example, in the above code, `caller_in_cpp` sets the field `a` as
5, then calls `callee_in_c`, which sets the field `a` as 3.  However,
at `HERE`, the value of `x` in Pulse is `{a -> 5, a -> 3}`, because the two
fieldnames are addressed as different ones.

To avoid the issue, this diff loosens the fieldname comparison in
Pulse.

Reviewed By: jvillard

Differential Revision: D26000812

fbshipit-source-id: 77142ebda
master
Sungkeun Cho 4 years ago committed by Facebook GitHub Bot
parent caa8bd0e39
commit eeb34231fa

@ -8,7 +8,12 @@
open! IStd open! IStd
module F = Format module F = Format
type t = {class_name: Typ.Name.t; field_name: string} [@@deriving compare, equal, yojson_of] type 'typ_name t_ = {class_name: 'typ_name; field_name: string}
[@@deriving compare, equal, yojson_of]
type t = Typ.Name.t t_ [@@deriving compare, equal, yojson_of]
let loose_compare = compare_t_ Typ.Name.loose_compare
let make class_name field_name = {class_name; field_name} let make class_name field_name = {class_name; field_name}

@ -11,6 +11,9 @@ module F = Format
(** Names for fields of class/struct/union *) (** Names for fields of class/struct/union *)
type t [@@deriving compare, equal, yojson_of] type t [@@deriving compare, equal, yojson_of]
val loose_compare : t -> t -> int
(** Similar to compare, but addresses [CStruct x] and [CppClass x] as equal. *)
val make : Typ.Name.t -> string -> t val make : Typ.Name.t -> string -> t
(** create a field of the given class and fieldname *) (** create a field of the given class and fieldname *)

@ -355,6 +355,20 @@ let desc_to_string desc =
module Name = struct module Name = struct
type t = name [@@deriving compare, equal, yojson_of] type t = name [@@deriving compare, equal, yojson_of]
(* NOTE: When a same struct type is used in C/C++/ObjC/ObjC++, their struct types may different,
eg [CStruct] in, C but [CppClass] in C++. On the other hand, since [Fieldname.t] includes the
class names, even for the same field, its field name used in C and C++ can be different.
However, in analyses, we may want to *not* distinguish fieldnames of the same struct type. For
that, we can use these loosened compare functions instead. *)
let loose_compare x y =
match (x, y) with
| (CStruct name1 | CppClass (name1, NoTemplate)), (CStruct name2 | CppClass (name2, NoTemplate))
->
QualifiedCppName.compare name1 name2
| _ ->
compare x y
let hash = Hashtbl.hash let hash = Hashtbl.hash
let qual_name = function let qual_name = function

@ -152,6 +152,9 @@ module Name : sig
(** Named types. *) (** Named types. *)
type t = name [@@deriving compare, yojson_of] type t = name [@@deriving compare, yojson_of]
val loose_compare : t -> t -> int
(** Similar to compare, but addresses [CStruct x] and [CppClass x] as equal. *)
val equal : t -> t -> bool val equal : t -> t -> bool
(** Equality for typenames *) (** Equality for typenames *)

@ -16,13 +16,17 @@ let yojson_of_typ_ = [%yojson_of: _]
let compare_typ_ _ _ = 0 let compare_typ_ _ _ = 0
module Access = struct module Access = struct
type 'array_index t = type ('fieldname, 'array_index) t_ =
| FieldAccess of Fieldname.t | FieldAccess of 'fieldname
| ArrayAccess of typ_ * 'array_index | ArrayAccess of typ_ * 'array_index
| TakeAddress | TakeAddress
| Dereference | Dereference
[@@deriving compare, yojson_of] [@@deriving compare, yojson_of]
type 'array_index t = (Fieldname.t, 'array_index) t_ [@@deriving compare, yojson_of]
let loose_compare compare_array_index = compare_t_ Fieldname.loose_compare compare_array_index
let pp pp_array_index fmt = function let pp pp_array_index fmt = function
| FieldAccess field_name -> | FieldAccess field_name ->
Fieldname.pp fmt field_name Fieldname.pp fmt field_name

@ -9,13 +9,18 @@ open! IStd
module F = Format module F = Format
module Access : sig module Access : sig
type 'array_index t = type ('fieldname, 'array_index) t_ =
| FieldAccess of Fieldname.t | FieldAccess of 'fieldname
| ArrayAccess of Typ.t * 'array_index | ArrayAccess of Typ.t * 'array_index
| TakeAddress | TakeAddress
| Dereference | Dereference
[@@deriving compare, yojson_of] [@@deriving compare, yojson_of]
type 'array_index t = (Fieldname.t, 'array_index) t_ [@@deriving compare, yojson_of]
val loose_compare :
('array_index -> 'array_index -> int) -> 'array_index t -> 'array_index t -> int
val pp : (Format.formatter -> 'array_index -> unit) -> Format.formatter -> 'array_index t -> unit val pp : (Format.formatter -> 'array_index -> unit) -> Format.formatter -> 'array_index t -> unit
val is_field_or_array_access : 'a t -> bool val is_field_or_array_access : 'a t -> bool

@ -12,7 +12,9 @@ open PulseBasicInterface
(* {3 Heap domain } *) (* {3 Heap domain } *)
module Access = struct module Access = struct
type t = AbstractValue.t HilExp.Access.t [@@deriving compare, yojson_of] type t = AbstractValue.t HilExp.Access.t [@@deriving yojson_of]
let compare = HilExp.Access.loose_compare AbstractValue.compare
let equal = [%compare.equal: t] let equal = [%compare.equal: t]

@ -0,0 +1,24 @@
# Copyright (c) Facebook, Inc. and its affiliates.
#
# This source code is licensed under the MIT license found in the
# LICENSE file in the root directory of this source tree.
SOURCES = $(SOURCES_C) $(SOURCES_CPP)
ROOT_DIR = $(TESTS_DIR)/../..
CLEAN_EXTRA += duplicates.txt
OBJECTS = $(foreach source,$(filter %.c %.cpp %.m %.mm,$(SOURCES)),$(basename $(source)).o)
include $(TESTS_DIR)/infer.make
include $(TESTS_DIR)/clang-base.make
infer-out$(TEST_SUFFIX)/report.json: $(CLANG_DEPS) $(SOURCES) $(HEADERS) $(TESTS_DIR)/.inferconfig $(MAKEFILE_LIST)
$(QUIET)$(call silent_on_success,Testing infer/clang in $(TEST_REL_DIR),\
echo $(SOURCES) && \
$(INFER_BIN) capture --results-dir $(@D) --dump-duplicate-symbols \
$(INFER_OPTIONS) -- clang $(CLANG_OPTIONS_C) $(SOURCES_C) && \
$(INFER_BIN) capture --continue --results-dir $(@D) --dump-duplicate-symbols \
$(INFER_OPTIONS) -- clang $(CLANG_OPTIONS_CPP) $(SOURCES_CPP) && \
$(INFER_BIN) analyze --results-dir $(@D) --dump-duplicate-symbols $(INFER_OPTIONS))

@ -0,0 +1,19 @@
# Copyright (c) Facebook, Inc. and its affiliates.
#
# This source code is licensed under the MIT license found in the
# LICENSE file in the root directory of this source tree.
TESTS_DIR = ../../..
CLANG_OPTIONS_C = -c
CLANG_OPTIONS_CPP = -x c++ -std=c++17 -nostdinc++ -isystem$(CLANG_INCLUDES)/c++/v1/ -c
INFER_OPTIONS = --pulse-only --debug-exceptions --project-root $(TESTS_DIR) \
--pulse-report-latent-issues
INFERPRINT_OPTIONS = --issues-tests
SOURCES_C = $(wildcard *.c)
SOURCES_CPP = $(wildcard *.cpp)
include $(TESTS_DIR)/clang-c-cpp.make

@ -0,0 +1,10 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include "callee_in_c.h"
void set_field_three(struct s* x) { x->a = 3; }

@ -0,0 +1,20 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
struct s {
int a;
};
#ifdef __cplusplus
extern "C" {
#endif
void set_field_three(struct s* x);
#ifdef __cplusplus
}
#endif

@ -0,0 +1,19 @@
/*
* Copyright (c) Facebook, Inc. and its affiliates.
*
* This source code is licensed under the MIT license found in the
* LICENSE file in the root directory of this source tree.
*/
#include <stdlib.h>
#include "callee_in_c.h"
void call_set_field_three_Ok(int* p) {
struct s x;
x.a = 5;
set_field_three(&x);
if (x.a == 5) {
free(p);
*p = 3;
}
}
Loading…
Cancel
Save