From 0b743c472efca616f462b2423d3c667f96023965 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Mon, 16 Jul 2018 13:32:22 +0000 Subject: [PATCH] [analyzer] Fix the Z3 backend always generating unsigned APSInt Summary: In `toAPSInt`, the Z3 backend was not checking the variable `Int`'s type and was always generating unsigned `APSInt`s. This was found by accident when I removed: ``` llvm::APSInt ConvertedLHS, ConvertedRHS; QualType LTy, RTy; std::tie(ConvertedLHS, LTy) = fixAPSInt(*LHS); std::tie(ConvertedRHS, RTy) = fixAPSInt(*RHS); - doIntTypePromotion( - ConvertedLHS, LTy, ConvertedRHS, RTy); return BVF.evalAPSInt(BSE->getOpcode(), ConvertedLHS, ConvertedRHS); ``` And the `BasicValueFactory` started to complain about different `signedness`. Reviewers: george.karpenkov, NoQ, ddcc Reviewed By: ddcc Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49305 git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337169 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 9e975676cc..721e17759f 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -681,12 +681,14 @@ public: Z3_get_numeral_uint64(Z3Context::ZC, AST, reinterpret_cast<__uint64 *>(&Value[0])); if (Sort.getBitvectorSortSize() <= 64) { - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), true); + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value[0]), + Int.isUnsigned()); } else if (Sort.getBitvectorSortSize() == 128) { Z3Expr ASTHigh = Z3Expr(Z3_mk_extract(Z3Context::ZC, 127, 64, AST)); Z3_get_numeral_uint64(Z3Context::ZC, AST, reinterpret_cast<__uint64 *>(&Value[1])); - Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), true); + Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), Value), + Int.isUnsigned()); } else { assert(false && "Bitwidth not supported!"); return false; @@ -702,7 +704,7 @@ public: llvm::APInt(Int.getBitWidth(), Z3_get_bool_value(Z3Context::ZC, AST) == Z3_L_TRUE ? 1 : 0), - true); + Int.isUnsigned()); return true; } } -- 2.40.0