[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<long> + 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