Teach the Prover additional aliasing rules about local variables

Reviewed By: cristianoc

Differential Revision: D5285926

fbshipit-source-id: bc57500

infer/src/backend/prover.ml

@@ -632,6 +632,12 @@ let check_disequal tenv prop e1 e2 =
     | Exp.BinOp (Binop.Mult, Exp.Sizeof _, e21), Exp.Const (Const.Cint n)
     | Exp.BinOp (Binop.Mult, e21, Exp.Sizeof _), Exp.Const (Const.Cint n) ->
         IntLit.iszero n && not (Exp.is_zero e21)
+    | Exp.Lvar pv0, Exp.Lvar pv1 ->
+        (* Addresses of any two local vars must be different *)
+        not (Pvar.equal pv0 pv1)
+    | Exp.Lvar _, Exp.Var id | Exp.Var id, Exp.Lvar _ ->
+        (* Address of any local var must be different from the value of any footprint var *)
+        Ident.is_footprint id
     | _, _ -> false in
   let ineq = lazy (Inequalities.from_prop tenv prop) in
   let check_pi_implies_disequal e1 e2 =

infer/tests/codetoanalyze/c/biabduction/example.c

@@ -12,6 +12,20 @@ void foo() {
   *p = 42;
 }
 
+void local_addr_noalis_ok(int* p) {
+  int* q = 0;
+  int x = 1;
+  if (&x == p)
+    *q = 42;
+}
+
+void local_addr_noalias_bad(int* p) {
+  int* q = 0;
+  int x = 1;
+  if (&x != p)
+    *q = 42;
+}
+
 int bar() {
   /* The division by zero should be found but filtered out by default */
   return 1 / 0;

infer/tests/codetoanalyze/c/biabduction/issues.exp

@@ -1 +1,2 @@
 codetoanalyze/c/biabduction/example.c, foo, 2, NULL_DEREFERENCE, [start of procedure foo()]
+codetoanalyze/c/biabduction/example.c, local_addr_noalias_bad, 4, NULL_DEREFERENCE, [start of procedure local_addr_noalias_bad(),Condition is true]