From 62cfd554c78809458121045dbb836eb5e9412d4d Mon Sep 17 00:00:00 2001
From: Jia Chen <grievejia@fb.com>
Date: Wed, 21 Jun 2017 10:13:18 -0700
Subject: [PATCH] Teach the Prover additional aliasing rules about local
 variables

Reviewed By: cristianoc

Differential Revision: D5285926

fbshipit-source-id: bc57500
---
 infer/src/backend/prover.ml                        |  6 ++++++
 infer/tests/codetoanalyze/c/biabduction/example.c  | 14 ++++++++++++++
 infer/tests/codetoanalyze/c/biabduction/issues.exp |  1 +
 3 files changed, 21 insertions(+)

diff --git a/infer/src/backend/prover.ml b/infer/src/backend/prover.ml
index 3c9edc98e..3e2e23bcf 100644
--- a/infer/src/backend/prover.ml
+++ b/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 =
diff --git a/infer/tests/codetoanalyze/c/biabduction/example.c b/infer/tests/codetoanalyze/c/biabduction/example.c
index b77c3953f..fa5b80ddb 100644
--- a/infer/tests/codetoanalyze/c/biabduction/example.c
+++ b/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;
diff --git a/infer/tests/codetoanalyze/c/biabduction/issues.exp b/infer/tests/codetoanalyze/c/biabduction/issues.exp
index 2dd25ef22..d7c0e65aa 100644
--- a/infer/tests/codetoanalyze/c/biabduction/issues.exp
+++ b/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]