[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

This revision was landed with ongoing or failed builds.
This revision was automatically updated to reflect the committed changes.
Closed by commit rGcd5783d3e82b: [analyzer][solver] Handle UnarySymExpr in 
SMTConv (authored by martong).

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/test/Analysis/unary-sym-expr-z3-refutation.c
  clang/test/Analysis/z3-crosscheck.c


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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@-1{{garbage}}
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,28 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+
+  QualType OperandTy;
+  llvm::SMTExprRef OperandExp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , 
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 different 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(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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:   

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 432019.
martong marked an inline comment as done.
martong added a comment.

- Compare the size of the types instead of the type pointers


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/test/Analysis/unary-sym-expr-z3-refutation.c
  clang/test/Analysis/z3-crosscheck.c


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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@-1{{garbage}}
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,28 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+
+  QualType OperandTy;
+  llvm::SMTExprRef OperandExp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , 
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 different 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(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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 

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong marked an inline comment as done.
martong added inline comments.



Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:463
+  // has a different type than the unary itself.
+  if (OperandTy != Sym->getType()) {
+if (hasComparison)

steakhal wrote:
> Could this fail spuriously due to a constness mismatch, since you compare 
> QualTypes instead of types?
> What happens if one of these refers to typedef? 
> Shouldn't we compare the canonical type pointers instead? Or this works out 
> just fine in practice. I might over-worry this :D
> 
> ALternatively, we could emit this cast only if the bitwidths are different. 
> (which caused the sort difference, thus the crash)
> Could this fail spuriously due to a constness mismatch, since you compare 
> QualTypes instead of types?
No, I don't think so. The underlying `fromCast` would simply return the same 
`SMTExprRef` if the bitwidths are the same.

> What happens if one of these refers to typedef? 
The same as in case of the qualifier mismatch.

> Shouldn't we compare the canonical type pointers instead? Or this works out 
> just fine in practice. I might over-worry this :D
> 
> ALternatively, we could emit this cast only if the bitwidths are different. 
> (which caused the sort difference, thus the crash)
Good point. The code would be more direct and efficient like that, I am going 
to update.




Comment at: clang/test/Analysis/unary-sym-expr-z3-refutation.c:28
+void k(long L) {
+  int g = L;
+  int h = g + 1;

steakhal wrote:
> So this is the implicit cast that we don't emit.
Yes.


Actually, without emitting SymbolCasts: `h` is evaluated as `$L + 1`. 
However, the expression's type is `int`.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.

I think it looks greatt
There are a couple questions you need to think about, but I don't insist about 
changing anything if the code works passed widescale testing.




Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:463
+  // has a different type than the unary itself.
+  if (OperandTy != Sym->getType()) {
+if (hasComparison)

Could this fail spuriously due to a constness mismatch, since you compare 
QualTypes instead of types?
What happens if one of these refers to typedef? 
Shouldn't we compare the canonical type pointers instead? Or this works out 
just fine in practice. I might over-worry this :D

ALternatively, we could emit this cast only if the bitwidths are different. 
(which caused the sort difference, thus the crash)



Comment at: clang/test/Analysis/unary-sym-expr-z3-refutation.c:28
+void k(long L) {
+  int g = L;
+  int h = g + 1;

So this is the implicit cast that we don't emit.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 431970.
martong added a comment.

- Fix Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must 
have the same sort!"' failed.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

Files:
  clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
  clang/test/Analysis/unary-sym-expr-z3-refutation.c
  clang/test/Analysis/z3-crosscheck.c


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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@-1{{garbage}}
+}
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,28 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+
+  QualType OperandTy;
+  llvm::SMTExprRef OperandExp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , 
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 different type than the unary itself.
+  if (OperandTy != Sym->getType()) {
+if (hasComparison)
+  *hasComparison = false;
+return getCastExpr(Solver, Ctx, UnaryExp, OperandTy, Sym->getType());
+  }
+  return UnaryExp;
+}
+
 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/test/Analysis/unary-sym-expr-z3-refutation.c
===
--- /dev/null
+++ 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:   

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

There are Z3 refutation related assertions on open-source projects once the 
patch stack is applied. Interestingly it happens in `fromBinOp`.

  clang-14: 
../../git/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:96:
 static const llvm::SMTExpr* 
clang::ento::SMTConv::fromBinOp(llvm::SMTSolverRef&, const llvm::SMTExpr* 
const&, clang::BinaryOperator::Opcode, const llvm::SMTExpr* const&, bool): 
Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have 
the same sort!"' failed.

This is the minimal reproducer:

  int b;
  long c();
  void d(int e, long *f) { *f = e; }
  void k() {
long a = c();
int g = a, h = g - 2, i = -h;
_Bool j;
d(i, );
j &= b == 0;
  }

I'd like to delay the commit of the patch stack until we can fix that, since Z3 
refutation is essential for most of our (internal) users.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong added a comment.

In D125547#3515259 , @steakhal wrote:

> Something is messed up with the diff. You refer to `fromUnOp()` but it's not 
> defined anywhere.

No. There is no mess up here, the diff is correct. `fromUnOp` had been 
implemented way before. I missed that when I created the initial patch. So, we 
just have to call that preexisting function in `getSymExpr`.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

Something is messed up with the diff. You refer to `fromUnOp()` but it's not 
defined anywhere.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong updated this revision to Diff 429633.
martong marked 2 inline comments as done.
martong added a comment.

- Use existing fromUnOp
- pass nullptr as FromTy


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

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


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,14 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), nullptr, hasComparison);
+  return fromUnOp(Solver, USE->getOpcode(), Exp);
+}
+
 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -446,6 +446,14 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), nullptr, hasComparison);
+  return fromUnOp(Solver, USE->getOpcode(), Exp);
+}
+
 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong marked 2 inline comments as done.
martong added inline comments.



Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:258
 
+  static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef ,
+   ASTContext ,

steakhal wrote:
> I would prefer the `fromUnOp` similarly to how `fromBinOp` is called.
Yeah, very good point, I just realized that `fromUnOp` is already implemented!



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:467-469
+  QualType FromTy;
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , hasComparison);

steakhal wrote:
> If you discard the `FromTy`, you could have passed a nullptr there.
Ok, Changed it.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Balázs Benics via Phabricator via cfe-commits]

steakhal accepted this revision.
steakhal added a comment.
This revision is now accepted and ready to land.

minor nits;
Thanks




Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:258
 
+  static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef ,
+   ASTContext ,

I would prefer the `fromUnOp` similarly to how `fromBinOp` is called.



Comment at: 
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:467-469
+  QualType FromTy;
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , hasComparison);

If you discard the `FromTy`, you could have passed a nullptr there.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D125547/new/

https://reviews.llvm.org/D125547

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D125547: [analyzer][solver] Handle UnarySymExpr in SMTConv

[Gabor Marton via Phabricator via cfe-commits]

martong created this revision.
martong added reviewers: steakhal, NoQ, mikhail.ramalho.
Herald added subscribers: manas, ASDenysPetrov, gamesh411, dkrupp, donat.nagy, 
Szelethus, a.sidorin, rnkovacs, szepet, baloghadamsoftware, xazax.hun.
Herald added a reviewer: Szelethus.
Herald added a project: All.
martong requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.

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


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D125547

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


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -255,6 +255,20 @@
 llvm_unreachable("Unimplemented opcode");
   }
 
+  static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef ,
+   ASTContext ,
+   const llvm::SMTExprRef ,
+   const UnaryOperator::Opcode Op) {
+switch (Op) {
+case UO_Minus:
+  return Solver->mkBVNeg(Exp);
+case UO_Not:
+  return Solver->mkBVNot(Exp);
+default:;
+}
+llvm_unreachable("Unimplemented opcode");
+  }
+
   /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
   /// and their bit widths.
   static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef ,
@@ -446,6 +460,17 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+
+  QualType FromTy;
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , hasComparison);
+
+  return fromUnary(Solver, Ctx, Exp, USE->getOpcode());
+}
+
 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);


Index: clang/test/Analysis/z3-crosscheck.c
===
--- clang/test/Analysis/z3-crosscheck.c
+++ clang/test/Analysis/z3-crosscheck.c
@@ -14,6 +14,20 @@
   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) {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -255,6 +255,20 @@
 llvm_unreachable("Unimplemented opcode");
   }
 
+  static inline llvm::SMTExprRef fromUnary(llvm::SMTSolverRef ,
+   ASTContext ,
+   const llvm::SMTExprRef ,
+   const UnaryOperator::Opcode Op) {
+switch (Op) {
+case UO_Minus:
+  return Solver->mkBVNeg(Exp);
+case UO_Not:
+  return Solver->mkBVNot(Exp);
+default:;
+}
+llvm_unreachable("Unimplemented opcode");
+  }
+
   /// Construct an SMTSolverRef from a QualType FromTy to a QualType ToTy,
   /// and their bit widths.
   static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef ,
@@ -446,6 +460,17 @@
   return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
 }
 
+if (const UnarySymExpr *USE = dyn_cast(Sym)) {
+  if (RetTy)
+*RetTy = Sym->getType();
+
+  QualType FromTy;
+  llvm::SMTExprRef Exp =
+  getSymExpr(Solver, Ctx, USE->getOperand(), , hasComparison);
+
+  return fromUnary(Solver, Ctx, Exp, USE->getOpcode());
+}
+
 if (const BinarySymExpr *BSE = dyn_cast(Sym)) {
   llvm::SMTExprRef Exp =
   getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
___
cfe-commits mailing