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 &Solver,
+ ASTContext &Ctx,
+ const llvm::SMTExprRef &Exp,
+ 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 &Solver,
@@ -446,6 +460,17 @@
return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
}
+ if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ QualType FromTy;
+ llvm::SMTExprRef Exp =
+ getSymExpr(Solver, Ctx, USE->getOperand(), &FromTy, hasComparison);
+
+ return fromUnary(Solver, Ctx, Exp, USE->getOpcode());
+ }
+
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/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 &Solver,
+ ASTContext &Ctx,
+ const llvm::SMTExprRef &Exp,
+ 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 &Solver,
@@ -446,6 +460,17 @@
return getCastExpr(Solver, Ctx, Exp, FromTy, Sym->getType());
}
+ if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
+ if (RetTy)
+ *RetTy = Sym->getType();
+
+ QualType FromTy;
+ llvm::SMTExprRef Exp =
+ getSymExpr(Solver, Ctx, USE->getOperand(), &FromTy, hasComparison);
+
+ return fromUnary(Solver, Ctx, Exp, USE->getOpcode());
+ }
+
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
