[inferbo] Weaken canonical path in on-demand value generation

Summary:
It weakens canonical path in order to avoid an explosion of locations when a struct type has pointers to struct.

For example:
```
struct Tree {
  struct Tree *root;
  struct Tree *left;
  struct Tree *right;
};
```

It was able to generate lots of abstract locations before this diff:
```
t->root
t->left
t->right
t->root->left
t->root->right
t->left->root
t->left->right
t->right->root
t->right->left
t->root->left->right
t->root->right->left
t->left->root->right
t->left->right->root
t->right->root->left
t->right->left->root
```

By this diff, pointer fields that have the same type are (unsoundly) canonicalized to the same one. For example,

```
t->root
t->root->left
t->root->right
t->root->left->right
t->root->right->left
```
are canonicalized to `t->root`. This is definitely unsound but I believe it is better than the location explosion by which analyses do not terminate in a reasonable time or giving a fixed limit of depth to the field access.

Reviewed By: mbouaziz

Differential Revision: D13503808

fbshipit-source-id: 867018712
master
Sungkeun Cho 6 years ago committed by Facebook Github Bot
parent 1f2b0d4152
commit fc26f79b92

@ -75,9 +75,13 @@ let mk pdesc =
let canonical_path typ_of_param_path path =
let module KnownFields = Caml.Map.Make (struct
type t = Typ.t option * Typ.Fieldname.t [@@deriving compare]
end) in
let module K = struct
type t =
| Default of {struct_typ: Typ.t option; fn: Typ.Fieldname.t}
| FldTypKnownPtr of {fld_typ: Typ.t}
[@@deriving compare]
end in
let module KnownFields = Caml.Map.Make (K) in
let rec helper path =
match path with
| SPath.Pvar _ | SPath.Callsite _ ->
@ -87,7 +91,16 @@ let canonical_path typ_of_param_path path =
(Option.map ptr_opt ~f:(fun ptr -> SPath.deref ~deref_kind ptr), known_fields)
| SPath.Field (fn, struct_path) -> (
let struct_path_opt, known_fields = helper struct_path in
let key = (typ_of_param_path (Option.value ~default:struct_path struct_path_opt), fn) in
let key =
match typ_of_param_path path with
| Some fld_typ when Typ.is_pointer fld_typ ->
K.FldTypKnownPtr {fld_typ}
| _ ->
let struct_typ =
typ_of_param_path (Option.value ~default:struct_path struct_path_opt)
in
K.Default {struct_typ; fn}
in
match KnownFields.find_opt key known_fields with
| Some _ as canonicalized ->
(canonicalized, known_fields)

@ -34,3 +34,34 @@ void call_get_field_Bad() {
t x = {10};
a[get_field_wrapper(&x)] = 0;
}
struct List {
struct List* next;
struct List* prev;
int v;
};
// [l->next->prev->v] is unsoundly canonicalized to [l->next->v].
int get_v(struct List* l) { return l->next->prev->v; }
int call_get_v_Good_FP() {
int a[10];
struct List* l = (struct List*)malloc(sizeof(struct List));
struct List* next = (struct List*)malloc(sizeof(struct List));
l->next = next;
next->prev = l;
l->v = 0;
next->v = 10;
a[get_v(l)] = 0;
}
int call_get_v_Bad_FN() {
int a[10];
struct List* l = (struct List*)malloc(sizeof(struct List));
struct List* next = (struct List*)malloc(sizeof(struct List));
l->next = next;
next->prev = l;
l->v = 10;
next->v = 0;
a[get_v(l)] = 0;
}

@ -100,6 +100,7 @@ codetoanalyze/c/bufferoverrun/function_call.c, function_call, 4, BUFFER_OVERRUN_
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_field_cond_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 5]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_v_Good_FP, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `l->next->v`,Assignment,<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_const_enum_Good_FP, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]

Loading…
Cancel
Save