From 4ca8a3210264effa9056b32266c4dc93fde13676 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 6 Mar 2019 20:22:59 -0800 Subject: [PATCH] [inferbo] Do not add Unknown location to alias Summary: Unknown locations in the alias domain resulted in unexpected unreachable code. Reviewed By: mbouaziz Differential Revision: D14339412 fbshipit-source-id: a5dca6489 --- infer/src/bufferoverrun/absLoc.ml | 11 +++++++++ .../src/bufferoverrun/bufferOverrunDomain.ml | 8 ++++++- .../codetoanalyze/c/bufferoverrun/issues.exp | 3 +++ .../c/bufferoverrun/prune_alias.c | 23 +++++++++++++++++++ 4 files changed, 44 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 2f51391c6..684fde390 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -63,6 +63,8 @@ module Allocsite = struct let is_literal_string = function LiteralString s -> Some s | _ -> None + let is_unknown = function Unknown -> true | Symbol _ | Known _ | LiteralString _ -> false + let to_string x = F.asprintf "%a" pp x let make : @@ -129,6 +131,15 @@ module Loc = struct let unknown = Allocsite Allocsite.unknown + let rec is_unknown = function + | Var _ -> + false + | Allocsite a -> + Allocsite.is_unknown a + | Field (x, _) -> + is_unknown x + + let rec pp_paren ~paren fmt = let module SP = Symb.SymbolPath in function diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index d2175cc4f..fbee9c9a4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -697,6 +697,10 @@ module AliasTarget = struct let widen ~prev ~next ~num_iters:_ = join prev next + + let is_unknown = function + | Simple l | SimplePlusA (l, _) | Empty l | Fgets l | Nullity l -> + Loc.is_unknown l end (* Relations between values of logical variables(registers) and program variables @@ -728,7 +732,9 @@ module AliasMap = struct F.pp_print_list ~pp_sep pp1 fmt (bindings x) - let load : Ident.t -> AliasTarget.t -> t -> t = add + let load : Ident.t -> AliasTarget.t -> t -> t = + fun id a x -> if not (AliasTarget.is_unknown a) then add id a x else x + let store : Loc.t -> t -> t = fun l m -> filter (fun _ y -> not (AliasTarget.use l y)) m diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index f7622a0bf..3fb18e1e4 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -263,6 +263,9 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 7, CONDITION_AL codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Bad, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 10] +codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: unknown1,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_200_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_fromHex2_sym_Good_FP, 3, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Call,Assignment,Assignment,,Array declaration,Array access: Offset: [-28, 16] Size: 17] codetoanalyze/c/bufferoverrun/prune_constant.c, call_greater_than_Good_FP, 3, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [,Assignment,Binary operation: (0 - 1):unsigned32] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index cb2b3635c..e598f0ff6 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -342,3 +342,26 @@ void call_not_prune_multiple4_Bad_FN() { int m[2] = {0, 10}; not_prune_multiple4(m); } + +int* unknown1(); +int* unknown2(); + +void unknown_alias_Good() { + int* x = unknown1(); + int* y = unknown2(); + + if (*x < *y) { + int a[10]; // Here should be reachable. + a[5] = 0; + } +} + +void unknown_alias_Bad() { + int* x = unknown1(); + int* y = unknown2(); + + if (*x < *y) { + int a[10]; // Here should be reachable. + a[10] = 0; + } +}