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<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 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<BinarySymExpr>(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: -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<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 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<BinarySymExpr>(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
