[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 &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);


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D125547.429230.patch
Type: text/x-patch
Size: 2167 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20220513/004178f7/attachment.bin>