pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[inferbo] No need to canonicalize paths in on-demand

Browse Source 
Summary:
Thanks to the newly added `StarField`, path length is better controlled before ondemand is used.
Hence there is no need to (unsoundly) canonicalize paths then anymore.

Reviewed By: ezgicicek

Differential Revision: D15409716

fbshipit-source-id: 9ea7b4717
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 66f6f54035
commit 64dea4dc0f
4 changed files with 30 additions and 45 deletions
Show Stats Download Patch File Download Diff File

1
infer/src/bufferoverrun/bufferOverrunDomain.ml
Unescape View File

@ -536,7 +536,6 @@ module Val = struct
l ->
let do_on_demand path typ =
let may_last_field = may_last_field path in
let path = OndemandEnv.canonical_path typ_of_param_path path in
of_path tenv ~may_last_field integer_type_widths entry_location typ path
in
match Loc.is_literal_string l with

40
infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml
Unescape View File

@ -81,43 +81,3 @@ let mk pdesc =
in
let entry_location = Procdesc.Node.get_loc (Procdesc.get_start_node pdesc) in
{tenv; typ_of_param_path; may_last_field; entry_location; integer_type_widths}
let canonical_path typ_of_param_path path =
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 _ | SPath.StarField _ ->
(None, KnownFields.empty)
| SPath.Deref (deref_kind, ptr) ->
let ptr_opt, known_fields = helper ptr in
(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 =
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)
| None ->
let field_path =
Option.value_map struct_path_opt ~default:path ~f:(fun struct_path ->
SPath.field struct_path fn )
in
(None, KnownFields.add key field_path known_fields) )
in
Option.value (helper path |> fst) ~default:path

30
infer/tests/codetoanalyze/c/bufferoverrun/get_field.c
Unescape View File

@ -41,10 +41,9 @@ struct List {
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 call_get_v_Good() {
int a[10];
struct List* l = (struct List*)malloc(sizeof(struct List));
struct List* next = (struct List*)malloc(sizeof(struct List));
@ -55,7 +54,7 @@ int call_get_v_Good_FP() {
a[get_v(l)] = 0;
}
int call_get_v_Bad_FN() {
int call_get_v_Bad() {
int a[10];
struct List* l = (struct List*)malloc(sizeof(struct List));
struct List* next = (struct List*)malloc(sizeof(struct List));
@ -65,3 +64,28 @@ int call_get_v_Bad_FN() {
next->v = 0;
a[get_v(l)] = 0;
}
// [l->next->prev->next->prev->v] is abstracted in [l->next->prev.*.v].
int get_v2(struct List* l) { return l->next->prev->next->prev->v; }
int call_get_v2_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_v2(l)] = 0;
}
int call_get_v2_Bad() {
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_v2(l)] = 0;
}

4
infer/tests/codetoanalyze/c/bufferoverrun/issues.exp
Unescape View File

@ -123,7 +123,9 @@ 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/get_field.c, call_get_v2_Bad, 8, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_v2_Good_FP, 8, BUFFER_OVERRUN_L5, no_bucket, ERROR, [<Offset trace>,Call,Assignment,<Length trace>,Array declaration,Array access: Offset: [-oo, +oo] Size: 10]
codetoanalyze/c/bufferoverrun/get_field.c, call_get_v_Bad, 8, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Call,Parameter `l->next->prev->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]

Write Preview
Loading…
Cancel
Save