diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 709fb501f..39b89492a 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -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 diff --git a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml index b8e85a22b..5ef1e3d2a 100644 --- a/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml +++ b/infer/src/bufferoverrun/bufferOverrunOndemandEnv.ml @@ -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 diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c index cc02683a9..b04c004b4 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/get_field.c @@ -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; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 7834427fa..c4fc872ad 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -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, [,Assignment,Call,Parameter `x->field`,Call,Parameter `x->field`,Assignment,Assignment,,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, [,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, [,Assignment,Call,Parameter `l->next->v`,Assignment,,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, [,Call,Assignment,,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, [,Call,Assignment,,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, [,Assignment,Call,Parameter `l->next->prev->v`,Assignment,,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, [,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, [,Array declaration,Array access: Offset: 10 Size: 10] codetoanalyze/c/bufferoverrun/global.c, compare_global_variable_bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10]