Page MenuHomePhabricator

[analyzer][solver] Handle UnarySymExpr in SMTConv
ClosedPublic

Authored by martong on May 13 2022, 7:07 AM.

Details

Summary

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

Diff Detail

Event Timeline

martong created this revision.May 13 2022, 7:07 AM
Herald added a project: Restricted Project. · View Herald Transcript
martong requested review of this revision.May 13 2022, 7:07 AM
Herald added a project: Restricted Project. · View Herald TranscriptMay 13 2022, 7:07 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
steakhal accepted this revision.May 13 2022, 7:22 AM

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.

This revision is now accepted and ready to land.May 13 2022, 7:22 AM
martong marked 2 inline comments as done.May 16 2022, 12:50 AM
martong added inline comments.
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 updated this revision to Diff 429633.May 16 2022, 12:51 AM
martong marked 2 inline comments as done.
  • Use existing fromUnOp
  • pass nullptr as FromTy

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

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.

steakhal accepted this revision.May 16 2022, 3:42 AM

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 updated this revision to Diff 431970.May 25 2022, 6:53 AM
  • Fix Assertion `*Solver->getSort(LHS) == *Solver->getSort(RHS) && "AST's must have the same sort!"' failed.
steakhal accepted this revision.May 25 2022, 7:46 AM

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 marked an inline comment as done.May 25 2022, 9:14 AM
martong added inline comments.
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 updated this revision to Diff 432019.May 25 2022, 9:17 AM
martong marked an inline comment as done.
  • Compare the size of the types instead of the type pointers
steakhal accepted this revision.May 25 2022, 9:54 AM
This revision was landed with ongoing or failed builds.May 26 2022, 5:17 AM
This revision was automatically updated to reflect the committed changes.