[analyzer][solver] Handle UnarySymExpr in SMTConv

[martong]

Summary

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

[steakhal]

minor nits;
Thanks

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

258

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

453–455

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

[martong]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

258

Yeah, very good point, I just realized that fromUnOp is already implemented!

453–455

Ok, Changed it.

[martong]

• Use existing fromUnOp
• pass nullptr as FromTy

[steakhal]

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

[martong]

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.

[martong]

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, &b);
  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.

[martong]

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

[steakhal]

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.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

463

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)

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

29

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

[martong]

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

463

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.

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

29

Yes.

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

[martong]

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

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

case BO_LOr:
       return fromBinOp(Solver, LHS, Op, RHS, /*isSigned=*/false);
 
     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,
                                           const llvm::SMTExprRef &Exp,
                                           QualType ToTy, uint64_t ToBitWidth,
                                           QualType FromTy,
                                           uint64_t FromBitWidth) {
     if ((FromTy->isIntegralOrEnumerationType() &&
          ToTy->isIntegralOrEnumerationType()) ||
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
       // Casting an expression with a comparison invalidates it. Note that this
       // must occur after the recursive call above.
       // e.g. (signed char) (x > 0)
       if (hasComparison)
         *hasComparison = false;
       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 (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);
       // Set the hasComparison parameter, in post-order traversal order.
       if (hasComparison)
         *hasComparison = BinaryOperator::isComparisonOp(BSE->getOpcode());
       return Exp;
     }

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

+// 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}}
+}

clang/test/Analysis/z3-crosscheck.c

 // RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
 // RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
 // REQUIRES: z3
 
 int foo(int x) 
 {
   int *z = 0;
   if ((x & 1) && ((x & 1) ^ 1))
 #ifdef NO_CROSSCHECK
       return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
 #else
       return *z; // no-warning
 #endif
   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) {
   int c = 5;
   if ((a - b) == 0)
     c = 0;
   if (a != b)
     g(3 / c); // no-warning