[clang] cd5783d - [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via cfe-commits]

Author: Gabor Marton
Date: 2022-05-26T14:14:10+02:00
New Revision: cd5783d3e82b98bfa140853fee95170852fd3c74

URL: https://github.com/llvm/llvm-project/commit/cd5783d3e82b98bfa140853fee95170852fd3c74
DIFF: https://github.com/llvm/llvm-project/commit/cd5783d3e82b98bfa140853fee95170852fd3c74.diff

LOG: [analyzer][solver] Handle UnarySymExpr in SMTConv

Dependent patch adds UnarySymExpr, now I'd like to handle that for SMT
conversions like refutation.

Differential Revision: https://reviews.llvm.org/D125547

Added: 
    clang/test/Analysis/unary-sym-expr-z3-refutation.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
    clang/test/Analysis/z3-crosscheck.c

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index 2d0f169260a4..bc38a54533be 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,28 @@ class SMTConv {
       return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
     }
 
+    if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+      if (RetTy)
+        *RetTy = Sym->getType();
+
+      QualType OperandTy;
+      llvm::SMTExprRef OperandExp =
+          getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
+      llvm::SMTExprRef UnaryExp =
+          fromUnOp(Solver, USE->getOpcode(), OperandExp);
+
+      // Currently, without the `support-symbolic-integer-casts=true` option,
+      // we do not emit `SymbolCast`s for implicit casts.
+      // One such implicit cast is missing if the operand of the unary operator
+      // has a 
diff erent type than the unary itself.
+      if (Ctx.getTypeSize(OperandTy) != Ctx.getTypeSize(Sym->getType())) {
+        if (hasComparison)
+          *hasComparison = false;
+        return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
+      }
+      return UnaryExp;
+    }
+
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       llvm::SMTExprRef Exp =
           getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);

diff  --git a/clang/test/Analysis/unary-sym-expr-z3-refutation.c b/clang/test/Analysis/unary-sym-expr-z3-refutation.c
new file mode 100644
index 000000000000..33585236232a
--- /dev/null
+++ b/clang/test/Analysis/unary-sym-expr-z3-refutation.c
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=true \
+// RUN:   -verify
+
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=true \
+// RUN:   -analyzer-config support-symbolic-integer-casts=true \
+// RUN:   -verify
+
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=true \
+// RUN:   -analyzer-config crosscheck-with-z3=true \
+// RUN:   -verify
+
+// RUN: %clang_analyze_cc1 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config eagerly-assume=true \
+// RUN:   -analyzer-config crosscheck-with-z3=true \
+// RUN:   -analyzer-config support-symbolic-integer-casts=true \
+// RUN:   -verify
+
+// REQUIRES: z3
+
+void k(long L) {
+  int g = L;
+  int h = g + 1;
+  int j;
+  j += -h < 0; // should not crash
+  // expected-warning at -1{{garbage}}
+}

diff  --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
index 67d410434fbb..7711597eb9ec 100644
--- a/clang/test/Analysis/z3-crosscheck.c
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@ int foo(int x)
   return 0;
 }
 
+int unary(int x, long l)
+{
+  int *z = 0;
+  int y = l;
+  if ((x & 1) && ((x & 1) ^ 1))
+    if (-y)
+#ifdef NO_CROSSCHECK
+        return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+        return *z; // no-warning
+#endif
+  return 0;
+}
+
 void g(int d);
 
 void f(int *a, int *b) {