[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

@@ -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

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
 

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, [<Length trace>,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, [<Length trace>,Array declaration,Array access: Offset: 10 Size: 10]
+codetoanalyze/c/bufferoverrun/prune_alias.c, unknown_alias_Good, 4, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,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, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,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, [<Offset trace>,Call,Assignment,Assignment,<Length trace>,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, [<LHS trace>,Assignment,Binary operation: (0 - 1):unsigned32]

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;
+  }
+}