walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: Use smt solver Z3

This commit is contained in:
Daniel Marjamäki 2019-10-02 17:59:04 +02:00
parent 4ba00d0694
commit 7ab22c7176
5 changed files with 185 additions and 242 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Makefile
View File

@ -5,6 +5,14 @@ ifndef HAVE_RULES
HAVE_RULES=no
endif
ifndef USE_Z3
USE_Z3=no
endif
ifeq ($(USE_Z3),yes)
CPPFLAGS += -DUSE_Z3
LIBS += -lz3
endif
# use match compiler
ifeq ($(SRCDIR),build)
$(warning Usage of SRCDIR to activate match compiler is deprecated. Use MATCHCOMPILER=yes instead.)

253
lib/exprengine.cpp
View File

@ -22,9 +22,13 @@
#include "symboldatabase.h"
#include "tokenize.h"
#include <cstdlib>
#include <limits>
#include <memory>
#include <iostream>
#ifdef USE_Z3
#include <z3++.h>
#endif
std::string ExprEngine::str(int128_t value)
{
@ -259,7 +263,7 @@ static ExprEngine::ValuePtr simplifyValue(ExprEngine::ValuePtr origValue)
if (!b->op1 || !b->op2)
return origValue;
auto intRange1 = std::dynamic_pointer_cast<ExprEngine::IntRange>(b->op1);
auto intRange2 = std::dynamic_pointer_cast<ExprEngine::IntRange>(b->op1);
auto intRange2 = std::dynamic_pointer_cast<ExprEngine::IntRange>(b->op2);
if (intRange1 && intRange2 && intRange1->minValue == intRange1->maxValue && intRange2->minValue == intRange2->maxValue) {
const std::string &binop = b->binop;
int128_t v;
@ -499,181 +503,100 @@ std::string ExprEngine::PointerValue::getRange() const
return r;
}
std::string ExprEngine::BinOpResult::getRange() const
{
IntOrFloatValue minValue, maxValue;
getRange(&minValue, &maxValue);
const std::string s1 = minValue.isFloat()
? std::to_string(minValue.floatValue)
: str(minValue.intValue);
const std::string s2 = maxValue.isFloat()
? std::to_string(maxValue.floatValue)
: str(maxValue.intValue);
if (s1 == s2)
return s1;
return s1 + ":" + s2;
}
void ExprEngine::BinOpResult::getRange(ExprEngine::BinOpResult::IntOrFloatValue *minValue, ExprEngine::BinOpResult::IntOrFloatValue *maxValue) const
{
std::map<ValuePtr, int> valueBit;
// Assign a bit number for each leaf
int bit = 0;
for (ValuePtr v : mLeafs) {
if (auto intRange = std::dynamic_pointer_cast<IntRange>(v)) {
if (intRange->minValue == intRange->maxValue) {
valueBit[v] = 30;
continue;
}
}
valueBit[v] = bit++;
}
if (bit > 24)
throw std::runtime_error("Internal error: bits");
for (int test = 0; test < (1 << bit); ++test) {
auto result = evaluate(test, valueBit);
if (test == 0)
*minValue = *maxValue = result;
else if (result.isFloat()) {
if (result.floatValue < minValue->floatValue)
*minValue = result;
else if (result.floatValue > maxValue->floatValue)
*maxValue = result;
} else {
if (result.intValue < minValue->intValue)
*minValue = result;
else if (result.intValue > maxValue->intValue)
*maxValue = result;
}
}
}
std::string ExprEngine::IntegerTruncation::getSymbolicExpression() const
{
return sign + std::to_string(bits) + "(" + inputValue->getSymbolicExpression() + ")";
}
#ifdef USE_Z3
struct ExprData {
typedef std::map<ExprEngine::ValuePtr, z3::expr> ValueExpr;
typedef std::vector<z3::expr> AssertionList;
z3::context c;
ValueExpr valueExpr;
AssertionList assertionList;
void addAssertions(z3::solver &solver) const {
for (auto assertExpr : assertionList)
solver.add(assertExpr);
}
};
static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData);
static z3::expr getExpr(const ExprEngine::BinOpResult *b, ExprData &exprData)
{
auto op1 = getExpr(b->op1, exprData);
auto op2 = getExpr(b->op2, exprData);
if (b->binop == "+")
return op1 + op2;
if (b->binop == "-")
return op1 - op2;
if (b->binop == "*")
return op1 * op2;
if (b->binop == "/")
return op1 / op2;
if (b->binop == "%")
return op1 % op2;
if (b->binop == "==")
return op1 == op2;
throw std::runtime_error("Internal error: Unhandled operator");
}
static z3::expr getExpr(ExprEngine::ValuePtr v, ExprData &exprData)
{
if (auto intRange = std::dynamic_pointer_cast<ExprEngine::IntRange>(v)) {
if (intRange->name[0] != '$')
return exprData.c.int_val(int64_t(intRange->minValue));
auto it = exprData.valueExpr.find(v);
if (it != exprData.valueExpr.end())
return it->second;
auto e = exprData.c.int_const(("v" + std::to_string(exprData.valueExpr.size())).c_str());
exprData.valueExpr.emplace(v, e);
if (intRange->maxValue <= INT_MAX)
exprData.assertionList.push_back(e <= int(intRange->maxValue));
if (intRange->minValue >= INT_MIN)
exprData.assertionList.push_back(e >= int(intRange->minValue));
return e;
}
if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(v)) {
return getExpr(b.get(), exprData);
}
throw std::runtime_error("Internal error: Unhandled value type");
}
#endif
bool ExprEngine::BinOpResult::isIntValueInRange(int value) const
{
IntOrFloatValue minValue, maxValue;
getRange(&minValue, &maxValue);
return value >= minValue.intValue && value <= maxValue.intValue;
#ifdef USE_Z3
ExprData exprData;
z3::solver s(exprData.c);
s.add(::getExpr(this, exprData) == value);
return s.check() == z3::sat;
#else
(void)value;
return false;
#endif
}
#define BINARY_OP(OP) \
if (binop == #OP) { \
struct ExprEngine::BinOpResult::IntOrFloatValue result(lhs); \
if (lhs.isFloat()) \
{ result.type = lhs.type; result.floatValue = lhs.floatValue OP (rhs.isFloat() ? rhs.floatValue : rhs.intValue); } \
else if (rhs.isFloat()) \
{ result.type = rhs.type; result.floatValue = lhs.intValue OP rhs.floatValue; } \
else { result.type = lhs.type; result.intValue = lhs.intValue OP rhs.intValue; } \
return result; \
}
#define BINARY_RELATIONAL_COMPARISON(OP) \
if (binop == #OP) { \
struct ExprEngine::BinOpResult::IntOrFloatValue result(lhs); \
if (lhs.isFloat()) \
{ result.setIntValue(lhs.floatValue OP (rhs.isFloat() ? rhs.floatValue : rhs.intValue)); } \
else if (rhs.isFloat()) \
{ result.setIntValue(lhs.intValue OP rhs.floatValue); } \
else { result.setIntValue(lhs.intValue OP rhs.intValue); } \
return result; \
}
#define BINARY_EQ_COMPARISON(OP) \
if (binop == #OP && !lhs.isFloat() && !rhs.isFloat()) { \
struct ExprEngine::BinOpResult::IntOrFloatValue result; \
result.setIntValue(lhs.intValue OP rhs.intValue); \
return result; \
}
#define BINARY_INT_OP(OP) \
if (binop == #OP) { \
struct ExprEngine::BinOpResult::IntOrFloatValue result; \
result.setIntValue(lhs.intValue OP rhs.intValue); \
return result; \
}
#define BINARY_OP_DIV(OP) \
if (binop == #OP) { \
struct ExprEngine::BinOpResult::IntOrFloatValue result(lhs); \
if (lhs.isFloat()) \
{ result.type = lhs.type; result.floatValue = lhs.floatValue OP (rhs.isFloat() ? rhs.floatValue : rhs.intValue); } \
else if (rhs.isFloat()) \
{ result.type = rhs.type; result.floatValue = lhs.intValue OP rhs.floatValue; } \
else if (rhs.intValue != 0) { result.type = lhs.type; result.intValue = lhs.intValue OP rhs.intValue; } \
return result; \
}
ExprEngine::BinOpResult::IntOrFloatValue ExprEngine::BinOpResult::evaluate(int test, const std::map<ExprEngine::ValuePtr, int> &valueBit) const
std::string ExprEngine::BinOpResult::getExpr() const
{
const ExprEngine::BinOpResult::IntOrFloatValue lhs = evaluateOperand(test, valueBit, op1);
const ExprEngine::BinOpResult::IntOrFloatValue rhs = evaluateOperand(test, valueBit, op2);
BINARY_OP(+)
BINARY_OP(-)
BINARY_OP(*)
BINARY_OP_DIV(/)
BINARY_INT_OP(&)
BINARY_INT_OP(|)
BINARY_INT_OP(^)
BINARY_INT_OP(<<)
BINARY_INT_OP(>>)
BINARY_EQ_COMPARISON(==)
BINARY_EQ_COMPARISON(!=)
BINARY_RELATIONAL_COMPARISON(>=)
BINARY_RELATIONAL_COMPARISON(>)
BINARY_RELATIONAL_COMPARISON(<=)
BINARY_RELATIONAL_COMPARISON(<)
if (binop == "%" && rhs.intValue != 0) {
struct ExprEngine::BinOpResult::IntOrFloatValue result;
result.setIntValue(lhs.intValue % rhs.intValue);
return result;
}
throw std::runtime_error("Internal error: Unhandled operator;" + binop);
#ifdef USE_Z3
ExprData exprData;
z3::solver s(exprData.c);
s.add(::getExpr(this, exprData));
exprData.addAssertions(s);
std::ostringstream os;
os << s;
return os.str();
#else
return "";
#endif
}
ExprEngine::BinOpResult::IntOrFloatValue ExprEngine::BinOpResult::evaluateOperand(int test, const std::map<ExprEngine::ValuePtr, int> &valueBit, ExprEngine::ValuePtr value) const
{
if (!value)
throw std::runtime_error("Internal error: null value");
auto binOpResult = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(value);
if (binOpResult)
return binOpResult->evaluate(test, valueBit);
auto it = valueBit.find(value);
if (it == valueBit.end())
throw std::runtime_error("Internal error: valueBit not set properly");
bool valueType = test & (1 << it->second);
if (auto intRange = std::dynamic_pointer_cast<IntRange>(value)) {
ExprEngine::BinOpResult::IntOrFloatValue result;
result.setIntValue(valueType ? intRange->minValue : intRange->maxValue);
return result;
}
if (auto floatRange = std::dynamic_pointer_cast<FloatRange>(value)) {
ExprEngine::BinOpResult::IntOrFloatValue result;
result.setFloatValue(valueType ? floatRange->minValue : floatRange->maxValue);
return result;
}
if (auto integerTruncation = std::dynamic_pointer_cast<IntegerTruncation>(value)) {
ExprEngine::BinOpResult::IntOrFloatValue result(evaluateOperand(test, valueBit, integerTruncation->inputValue));
if (result.isFloat())
result.setIntValue(truncateInt(result.floatValue, integerTruncation->bits, integerTruncation->sign));
else
result.setIntValue(truncateInt(result.intValue, integerTruncation->bits, integerTruncation->sign));
return result;
}
throw std::runtime_error("Internal error: Unhandled value:" + std::to_string((int)value->type));
}
// Todo: This is taken from ValueFlow and modified.. we should reuse it
static int getIntBitsFromValueType(const ValueType *vt, const cppcheck::Platform &platform)
@ -1271,6 +1194,7 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer,
errorLogger->reportErr(errmsg);
};
#ifdef VERIFY_INTEGEROVERFLOW
std::function<void(const Token *, const ExprEngine::Value &)> integerOverflow = [&](const Token *tok, const ExprEngine::Value &value) {
if (!tok->isArithmeticalOp() || !tok->valueType() || !tok->valueType()->isIntegral() || tok->valueType()->pointer > 0)
return;
@ -1306,6 +1230,7 @@ void ExprEngine::runChecks(ErrorLogger *errorLogger, const Tokenizer *tokenizer,
ErrorLogger::ErrorMessage errmsg(callstack, &tokenizer->list, Severity::SeverityType::error, "verificationIntegerOverflow", "Integer overflow, " + tok->valueType()->str() + " result." + note, false);
errorLogger->reportErr(errmsg);
};
#endif
std::vector<ExprEngine::Callback> callbacks;
callbacks.push_back(divByZero);

40
lib/exprengine.h
View File

@ -230,42 +230,10 @@ namespace ExprEngine {
, binop(binop)
, op1(op1)
, op2(op2) {
auto b1 = std::dynamic_pointer_cast<BinOpResult>(op1);
if (b1)
mLeafs = b1->mLeafs;
else
mLeafs.insert(op1);
auto b2 = std::dynamic_pointer_cast<BinOpResult>(op2);
if (b2)
mLeafs.insert(b2->mLeafs.begin(), b2->mLeafs.end());
else
mLeafs.insert(op2);
}
std::string getRange() const override;
struct IntOrFloatValue {
void setIntValue(int128_t v) {
type = INT;
intValue = v;
floatValue = 0;
}
void setFloatValue(long double v) {
type = FLOAT;
intValue = 0;
floatValue = v;
}
enum {INT,FLOAT} type;
bool isFloat() const {
return type == FLOAT;
}
int128_t intValue;
long double floatValue;
};
void getRange(IntOrFloatValue *minValue, IntOrFloatValue *maxValue) const;
bool isIntValueInRange(int value) const override;
bool isIntValueInRange(int value) const;
std::string getExpr() const;
std::string binop;
ValuePtr op1;
@ -276,10 +244,6 @@ namespace ExprEngine {
std::string name2 = op2 ? op2->name : std::string("null");
return "(" + name1 + ")" + binop + "(" + name2 + ")";
}
IntOrFloatValue evaluate(int test, const std::map<ValuePtr, int> &valueBit) const;
IntOrFloatValue evaluateOperand(int test, const std::map<ValuePtr, int> &valueBit, ValuePtr value) const;
std::set<ValuePtr> mLeafs;
};
class IntegerTruncation : public Value {

119
test/testexprengine.cpp
View File

@ -32,10 +32,7 @@ public:
private:
void run() OVERRIDE {
TEST_CASE(argPointer);
TEST_CASE(argSmartPointer);
TEST_CASE(argStruct);
#ifdef USE_Z3
TEST_CASE(expr1);
TEST_CASE(expr2);
TEST_CASE(expr3);
@ -66,14 +63,39 @@ private:
TEST_CASE(functionCall2);
TEST_CASE(functionCall3);
TEST_CASE(pointer1);
TEST_CASE(pointer2);
TEST_CASE(int1);
TEST_CASE(pointer1);
TEST_CASE(pointerAlias1);
TEST_CASE(pointerAlias2);
TEST_CASE(pointerAlias3);
TEST_CASE(pointerAlias4);
TEST_CASE(pointerNull1);
TEST_CASE(structMember);
#endif
}
std::string expr(const char code[], const std::string &binop) {
Settings settings;
settings.platform(cppcheck::Platform::Unix64);
Tokenizer tokenizer(&settings, this);
std::istringstream istr(code);
tokenizer.tokenize(istr, "test.cpp");
std::string ret;
std::function<void(const Token *, const ExprEngine::Value &)> f = [&](const Token *tok, const ExprEngine::Value &value) {
if (tok->str() != binop)
return;
auto b = dynamic_cast<const ExprEngine::BinOpResult *>(&value);
if (!b)
return;
ret = b->getExpr();
};
std::vector<ExprEngine::Callback> callbacks;
callbacks.push_back(f);
std::ostringstream dummy;
ExprEngine::executeAllFunctions(&tokenizer, &settings, callbacks, dummy);
return ret;
}
std::string getRange(const char code[], const std::string &str, int linenr = 0) {
@ -112,45 +134,28 @@ private:
return ret.str();
}
void argPointer() {
ASSERT_EQUALS("->$1,null,->?", getRange("void f(unsigned char *p) { a = *p; }", "p"));
}
void argSmartPointer() {
ASSERT_EQUALS("->{x=$2},null", getRange("struct S { int x; }; void f(std::shared_ptr<S> ptr) { x = ptr; }", "ptr"));
}
void argStruct() {
ASSERT_EQUALS("0:510",
getRange("struct S {\n"
" unsigned char a;\n"
" unsigned char b;\n"
"};\n"
"void f(struct S s) { return s.a + s.b; }", "s.a+s.b"));
}
void expr1() {
ASSERT_EQUALS("-32768:32767", getRange("void f(short x) { a = x; }", "x"));
}
void expr2() {
ASSERT_EQUALS("-65536:65534", getRange("void f(short x) { a = x + x; }", "x+x"));
ASSERT_EQUALS("($1)+($1)", getRange("void f(short x) { a = x + x; }", "x+x"));
}
void expr3() {
ASSERT_EQUALS("-65536:65534", getRange("int f(short x) { int a = x + x; return a; }", "return a"));
ASSERT_EQUALS("($1)+($1)", getRange("int f(short x) { int a = x + x; return a; }", "return a"));
}
void expr4() {
ASSERT_EQUALS("0", getRange("int f(short x) { int a = x - x; return a; }", "return a"));
ASSERT_EQUALS("($1)-($1)", getRange("int f(short x) { int a = x - x; return a; }", "return a"));
}
void expr5() {
ASSERT_EQUALS("-65536:65534", getRange("void f(short a, short b, short c, short d) { if (a+b<c+d) {} }", "a+b"));
ASSERT_EQUALS("($1)+($2)", getRange("void f(short a, short b, short c, short d) { if (a+b<c+d) {} }", "a+b"));
}
void exprAssign1() {
ASSERT_EQUALS("1:256", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1"));
}
void exprAssign2() {
@ -158,11 +163,11 @@ private:
}
void if1() {
ASSERT_EQUALS("7:32768", getRange("inf f(short x) { if (x > 5) a = x + 1; }", "x+1"));
ASSERT_EQUALS("($2)+(1)", getRange("inf f(short x) { if (x > 5) a = x + 1; }", "x+1"));
}
void if2() {
ASSERT_EQUALS("7:32768,-32767:6", getRange("inf f(short x) { if (x > 5) {} a = x + 1; }", "x+1"));
ASSERT_EQUALS("($2)+(1),($3)+(1)", getRange("inf f(short x) { if (x > 5) {} a = x + 1; }", "x+1"));
}
void if3() {
@ -178,20 +183,27 @@ private:
}
void ifelse1() {
ASSERT_EQUALS("-32767:6", getRange("inf f(short x) { if (x > 5) ; else a = x + 1; }", "x+1"));
ASSERT_EQUALS("($3)+(1)", getRange("inf f(short x) { if (x > 5) ; else a = x + 1; }", "x+1"));
}
void array1() {
ASSERT_EQUALS("5", getRange("inf f() { int arr[10]; arr[4] = 5; return arr[4]; }", "arr[4]"));
ASSERT_EQUALS("(assert (= 5 0))\n",
expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "=="));
}
void array2() {
ASSERT_EQUALS("0:255", getRange("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4]; }", "arr[4]"));
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (= v0 365))\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n",
expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "=="));
}
void array3() {
ASSERT_EQUALS("?,43", getRange("int f(unsigned char x) { int arr[10]; arr[4] = 43; int vx = arr[x]; }", "arr[x]"));
const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }";
ASSERT_EQUALS("?,43", getRange(code, "arr[x]"));
// TODO: ASSERT_EQUALS("", expr(code, "=="));
}
void array4() {
@ -215,14 +227,16 @@ private:
ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]"));
}
void floatValue1() {
ASSERT_EQUALS(std::to_string(std::numeric_limits<float>::min()) + ":" + std::to_string(std::numeric_limits<float>::max()), getRange("float f; void func() { f=f; }", "f=f"));
}
void floatValue2() {
ASSERT_EQUALS("14.500000", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0"));
ASSERT_EQUALS("(29.0)/(2.0)", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0"));
}
void functionCall1() {
ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x"));
}
@ -242,12 +256,20 @@ private:
ASSERT_EQUALS("-2147483648:2147483647", getRange("int fgets(int, const char *, void *); void f() { int x = -1; fgets(stdin, \"%d\", &x); x=x; }", "x=x"));
}
void pointer1() {
ASSERT_EQUALS("?", getRange("int f() { int *x; x = x; }", "x=x"));
void int1() {
ASSERT_EQUALS("(declare-fun v0 () Int)\n"
"(assert (= (+ 2 v0) 3))\n"
"(assert (<= v0 2147483647))\n"
"(assert (>= v0 (- 2147483648)))\n",
expr("void f(int x) { return 2+x==3; }", "=="));
}
void pointer2() {
ASSERT_EQUALS("?", getRange("int f() { sometype *x; x = x; }", "x=x"));
void pointer1() {
const char code[] = "void f(unsigned char *p) { a = *p; }";
ASSERT_EQUALS("->$1,null,->?", getRange(code, "p"));
// TODO expr
}
void pointerAlias1() {
@ -272,8 +294,25 @@ private:
}
void pointerNull1() {
ASSERT_EQUALS("0", getRange("void f(void *p) { p = NULL; p += 1; }", "p+=1"));
ASSERT_EQUALS("1", getRange("void f(void *p) { p = NULL; p += 1; }", "p+=1"));
}
void structMember() {
ASSERT_EQUALS("(declare-fun v1 () Int)\n"
"(declare-fun v0 () Int)\n"
"(assert (= (+ v0 v1) 0))\n"
"(assert (<= v0 255))\n"
"(assert (>= v0 0))\n"
"(assert (<= v1 255))\n"
"(assert (>= v1 0))\n",
expr("struct S {\n"
" unsigned char a;\n"
" unsigned char b;\n"
"};\n"
"void f(struct S s) { return s.a + s.b == 0; }", "=="));
}
};
REGISTER_TEST(TestExprEngine)

7
tools/dmake.cpp
View File

@ -217,6 +217,13 @@ int main(int argc, char **argv)
fout << "# To compile with rules, use 'make HAVE_RULES=yes'\n";
makeConditionalVariable(fout, "HAVE_RULES", "no");
// Z3 is an optional dependency now..
makeConditionalVariable(fout, "USE_Z3", "no");
fout << "ifeq ($(USE_Z3),yes)\n"
<< " CPPFLAGS += -DUSE_Z3\n"
<< " LIBS += -lz3\n"
<< "endif\n";
// use match compiler..
fout << "# use match compiler\n";
fout << "ifeq ($(SRCDIR),build)\n"