1 /* 2 * Cppcheck - A tool for static C/C++ code analysis 3 * Copyright (C) 2007-2021 Cppcheck team. 4 * 5 * This program is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * This program is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with this program. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 #include "config.h" 20 #include "exprengine.h" 21 #include "library.h" 22 #include "platform.h" 23 #include "settings.h" 24 #include "token.h" 25 #include "tokenize.h" 26 #include "testsuite.h" 27 28 #include <string> 29 30 class TestExprEngine : public TestFixture { 31 public: TestExprEngine()32 TestExprEngine() : TestFixture("TestExprEngine") {} 33 34 private: run()35 void run() OVERRIDE { 36 #ifdef USE_Z3 37 TEST_CASE(annotation1); 38 TEST_CASE(annotation2); 39 40 TEST_CASE(expr1); 41 TEST_CASE(expr2); 42 TEST_CASE(expr3); 43 TEST_CASE(expr4); 44 TEST_CASE(expr5); 45 TEST_CASE(expr6); 46 TEST_CASE(expr7); 47 TEST_CASE(expr8); 48 TEST_CASE(expr9); 49 TEST_CASE(exprAssign1); 50 TEST_CASE(exprAssign2); // Truncation 51 TEST_CASE(exprNot); 52 53 TEST_CASE(getValueConst1); 54 55 TEST_CASE(inc1); 56 TEST_CASE(inc2); 57 58 TEST_CASE(if1); 59 TEST_CASE(if2); 60 TEST_CASE(if3); 61 TEST_CASE(if4); 62 TEST_CASE(if5); 63 TEST_CASE(ifAlwaysTrue1); 64 TEST_CASE(ifAlwaysTrue2); 65 TEST_CASE(ifAlwaysTrue3); 66 TEST_CASE(ifAlwaysFalse1); 67 TEST_CASE(ifAlwaysFalse2); 68 TEST_CASE(ifelse1); 69 TEST_CASE(ifif); 70 TEST_CASE(ifreturn); 71 TEST_CASE(ifIntRangeAlwaysFalse); 72 TEST_CASE(ifIntRangeAlwaysTrue); 73 74 TEST_CASE(istream); 75 76 TEST_CASE(switch1); 77 TEST_CASE(switch2); 78 79 TEST_CASE(for1); 80 TEST_CASE(forAlwaysFalse1); 81 82 TEST_CASE(while1); 83 TEST_CASE(while2); 84 TEST_CASE(while3); 85 TEST_CASE(while4); 86 TEST_CASE(while5); 87 88 TEST_CASE(array1); 89 TEST_CASE(array2); 90 TEST_CASE(array3); 91 TEST_CASE(array4); 92 TEST_CASE(array5); 93 TEST_CASE(array6); 94 TEST_CASE(array7); 95 TEST_CASE(arrayInit1); 96 TEST_CASE(arrayInit2); 97 TEST_CASE(arrayInit3); 98 TEST_CASE(arrayUninit); 99 TEST_CASE(arrayInLoop); 100 101 TEST_CASE(floatValue1); 102 TEST_CASE(floatValue2); 103 TEST_CASE(floatValue3); 104 TEST_CASE(floatValue4); 105 TEST_CASE(floatValue5); 106 107 TEST_CASE(functionCall1); 108 TEST_CASE(functionCall2); 109 TEST_CASE(functionCall3); 110 TEST_CASE(functionCall4); 111 TEST_CASE(functionCall5); 112 113 TEST_CASE(functionCallContract1); 114 TEST_CASE(functionCallContract2); 115 116 TEST_CASE(int1); 117 118 TEST_CASE(pointer1); 119 TEST_CASE(pointer2); 120 TEST_CASE(pointer3); 121 TEST_CASE(pointerAlias1); 122 TEST_CASE(pointerAlias2); 123 TEST_CASE(pointerAlias3); 124 TEST_CASE(pointerAlias4); 125 TEST_CASE(pointerNull1); 126 127 TEST_CASE(structMember1); 128 TEST_CASE(structMember2); 129 TEST_CASE(structMember3); 130 131 TEST_CASE(pointerToStructInLoop); 132 133 TEST_CASE(ternaryOperator1); 134 #endif 135 } 136 replace(std::string & str,const std::string & from,const std::string & to)137 static void replace(std::string& str, const std::string& from, const std::string& to) { 138 size_t pos = 0; 139 while ((pos = str.find(from, pos)) != std::string::npos) 140 str.replace(pos, from.length(), to); 141 } 142 cleanupExpr(std::string rawexpr)143 static std::string cleanupExpr(std::string rawexpr) { 144 std::string ret; 145 std::istringstream istr(rawexpr); 146 std::string line; 147 while (std::getline(istr, line)) { 148 if (line.empty()) 149 continue; 150 line = line.substr(line.find_first_not_of(" ")); 151 if (line.compare(0,13,"(declare-fun ") == 0) 152 continue; 153 if (line == "(solver") 154 continue; 155 if (line.compare(0,9,"(assert (") == 0) { 156 line.erase(0,8); 157 line.erase(line.size()-1); 158 } 159 replace(line, "(fp.gt ", "(> "); 160 replace(line, "(fp.lt ", "(< "); 161 replace(line, "(_ +zero 11 53)", "0.0"); 162 replace(line, "(fp #b0 #b10000000010 #x899999999999a)", "12.3"); 163 replace(line, "(/ 123.0 10.0)", "12.3"); 164 int par = 0; 165 for (char pos : line) { 166 if (pos == '(') 167 par++; 168 else if (pos == ')') 169 --par; 170 } 171 if (par < 0) 172 line.erase(line.size() - 1); 173 ret += line + "\n"; 174 } 175 return ret; 176 } 177 expr(const char code[],const std::string & binop)178 std::string expr(const char code[], const std::string &binop) { 179 Settings settings; 180 settings.platform(cppcheck::Platform::Unix64); 181 Tokenizer tokenizer(&settings, this); 182 std::istringstream istr(code); 183 tokenizer.tokenize(istr, "test.cpp"); 184 std::string ret; 185 ExprEngine::Callback f = [&](const Token *tok, const ExprEngine::Value &value, ExprEngine::DataBase *dataBase) { 186 if (tok->str() != binop) 187 return; 188 const auto *b = dynamic_cast<const ExprEngine::BinOpResult *>(&value); 189 if (!b) 190 return; 191 ret += TestExprEngine::cleanupExpr(b->getExpr(dataBase)); 192 }; 193 std::vector<ExprEngine::Callback> callbacks; 194 callbacks.push_back(f); 195 std::ostringstream trace; 196 ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); 197 return ret; 198 } 199 functionCallContractExpr(const char code[],const Settings & s)200 std::string functionCallContractExpr(const char code[], const Settings &s) { 201 Settings settings; 202 settings.bugHunting = true; 203 settings.debugBugHunting = true; 204 settings.functionContracts = s.functionContracts; 205 settings.platform(cppcheck::Platform::Unix64); 206 Tokenizer tokenizer(&settings, this); 207 std::istringstream istr(code); 208 tokenizer.tokenize(istr, "test.cpp"); 209 std::vector<ExprEngine::Callback> callbacks; 210 std::ostringstream trace; 211 ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); 212 std::string ret = trace.str(); 213 std::string::size_type pos1 = ret.find("checkContract:{"); 214 std::string::size_type pos2 = ret.find("}", pos1); 215 if (pos2 == std::string::npos) 216 return "Error:" + ret; 217 return TestExprEngine::cleanupExpr(ret.substr(pos1, pos2+1-pos1)); 218 } 219 getRange(const char code[],const std::string & str,int linenr=0)220 std::string getRange(const char code[], const std::string &str, int linenr = 0) { 221 Settings settings; 222 settings.platform(cppcheck::Platform::Unix64); 223 settings.library.smartPointers["std::shared_ptr"]; 224 Tokenizer tokenizer(&settings, this); 225 std::istringstream istr(code); 226 tokenizer.tokenize(istr, "test.cpp"); 227 std::string ret; 228 ExprEngine::Callback f = [&](const Token *tok, const ExprEngine::Value &value, ExprEngine::DataBase *dataBase) { 229 (void)dataBase; 230 if ((linenr == 0 || linenr == tok->linenr()) && tok->expressionString() == str) { 231 if (!ret.empty()) 232 ret += ","; 233 ret += value.getRange(); 234 } 235 }; 236 std::vector<ExprEngine::Callback> callbacks; 237 callbacks.push_back(f); 238 std::ostringstream trace; 239 ExprEngine::executeAllFunctions(this, &tokenizer, &settings, callbacks, trace); 240 return ret; 241 } 242 trackExecution(const char code[],Settings * settings=nullptr)243 std::string trackExecution(const char code[], Settings *settings = nullptr) { 244 Settings s; 245 if (!settings) 246 settings = &s; 247 settings->bugHunting = true; 248 settings->debugBugHunting = true; 249 settings->platform(cppcheck::Platform::Unix64); 250 settings->library.smartPointers["std::shared_ptr"]; 251 Tokenizer tokenizer(settings, this); 252 std::istringstream istr(code); 253 tokenizer.tokenize(istr, "test.cpp"); 254 std::vector<ExprEngine::Callback> callbacks; 255 std::ostringstream ret; 256 ExprEngine::executeAllFunctions(this, &tokenizer, settings, callbacks, ret); 257 return ret.str(); 258 } 259 annotation1()260 void annotation1() { 261 const char code[] = "void f(__cppcheck_low__(100) short x) {\n" 262 " return x < 10;\n" 263 "}"; 264 265 const char expected[] = "(>= $1 100)\n" // <- annotation 266 "(and (>= $1 (- 32768)) (<= $1 32767))\n" 267 "(< $1 10)\n" 268 "z3::unsat\n"; 269 270 ASSERT_EQUALS(expected, expr(code, "<")); 271 } 272 annotation2()273 void annotation2() { 274 const char code[] = "__cppcheck_low__(100) short x;\n" 275 " void f() {\n" 276 " return x < 10;\n" 277 "}"; 278 279 const char expected[] = "(>= $1 100)\n" // <- annotation 280 "(and (>= $1 (- 32768)) (<= $1 32767))\n" 281 "(< $1 10)\n" 282 "z3::unsat\n"; 283 284 ASSERT_EQUALS(expected, expr(code, "<")); 285 } 286 expr1()287 void expr1() { 288 ASSERT_EQUALS("-32768:32767", getRange("void f(short x) { a = x; }", "x")); 289 } 290 expr2()291 void expr2() { 292 ASSERT_EQUALS("($1)+($1)", getRange("void f(short x) { a = x + x; }", "x+x")); 293 } 294 expr3()295 void expr3() { 296 ASSERT_EQUALS("($1)+($1)", getRange("int f(short x) { int a = x + x; return a; }", "return a")); 297 } 298 expr4()299 void expr4() { 300 ASSERT_EQUALS("($1)-($1)", getRange("int f(short x) { int a = x - x; return a; }", "return a")); 301 } 302 expr5()303 void expr5() { 304 ASSERT_EQUALS("($1)+($2)", getRange("void f(short a, short b, short c, short d) { if (a+b<c+d) {} }", "a+b")); 305 } 306 expr6()307 void expr6() { 308 const char code[] = "void f(unsigned char x) {\n" 309 " unsigned char result = 8 - x;\n" 310 " result > 1000;" 311 "}"; 312 313 ASSERT_EQUALS("(8)-($1)", getRange(code, "8-x")); 314 315 ASSERT_EQUALS("(and (>= $1 0) (<= $1 255))\n" 316 "(> (- 8 $1) 1000)\n" 317 "z3::unsat\n", 318 expr(code, ">")); 319 } 320 expr7()321 void expr7() { 322 const char code[] = "void f(bool a, bool b, int c) {\n" 323 " if (a||b) {}\n" 324 " c > 1000;" 325 "}"; 326 327 ASSERT_EQUALS("(or (distinct $1 0) (distinct $2 0))\n" 328 "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" 329 "(and (>= $1 0) (<= $1 1))\n" 330 "(and (>= $2 0) (<= $2 1))\n" 331 "(> $3 1000)\n" 332 "z3::sat\n" 333 "(= (ite (or (distinct $1 0) (distinct $2 0)) 1 0) 0)\n" 334 "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" 335 "(and (>= $1 0) (<= $1 1))\n" 336 "(and (>= $2 0) (<= $2 1))\n" 337 "(> $3 1000)\n" 338 "z3::sat\n", 339 expr(code, ">")); 340 } 341 expr8()342 void expr8() { 343 const char code[] = "void foo(int x, int y) {\n" 344 " if (x % 32) {}\n" 345 " y==3;\n" 346 "}"; 347 // Do not crash 348 expr(code, "=="); 349 } 350 expr9()351 void expr9() { 352 Settings settings; 353 LOAD_LIB_2(settings.library, "std.cfg"); 354 355 ASSERT_EQUALS("1:26: $4=ArrayValue([$3],[:]=$2)\n" 356 "1:26: $3=IntRange(0:2147483647)\n" 357 "1:26: $2=IntRange(-128:127)\n" 358 "1:27: 0:memory:{s=($4,[$3],[:]=$2)}\n", 359 trackExecution("void foo() { std::string s; }", &settings)); 360 361 362 ASSERT_EQUALS("1:52: $4=ArrayValue([$3],[:]=$2)\n" 363 "1:52: $3=IntRange(0:2147483647)\n" 364 "1:52: $2=IntRange(-128:127)\n" 365 "1:66: 0:memory:{s=($4,[$3],[:]=$2)}\n", 366 trackExecution("std::string getName(int); void foo() { std::string s = getName(1); }", &settings)); 367 } 368 exprAssign1()369 void exprAssign1() { 370 ASSERT_EQUALS("($1)+(1)", getRange("void f(unsigned char a) { a += 1; }", "a+=1")); 371 } 372 exprAssign2()373 void exprAssign2() { 374 ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x")); 375 } 376 exprNot()377 void exprNot() { 378 ASSERT_EQUALS("($1)==(0)", getRange("void f(unsigned char a) { return !a; }", "!a")); 379 } 380 getValueConst1()381 void getValueConst1() { // Data::getValue 382 ASSERT_EQUALS("512", getRange("const int x=512; void func() { x=x }", "x=x")); 383 } 384 385 inc1()386 void inc1() { 387 ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 388 "(= (+ $1 1) $1)\n" 389 "z3::unsat\n", 390 expr("void f(int x) { int y = x++; x == y; }", "==")); 391 392 ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 393 "(= (+ $1 1) (+ $1 1))\n" 394 "z3::sat\n", 395 expr("void f(int x) { int y = ++x; x == y; }", "==")); 396 } 397 inc2()398 void inc2() { 399 ASSERT_EQUALS("(= 2 2)\n" 400 "z3::sat\n", 401 expr("void f() { unsigned char a[2]; a[0] = 1; a[0]++; a[0] == a[0]; }", "==")); 402 } 403 if1()404 void if1() { 405 ASSERT_EQUALS("(< $1 $2)\n" 406 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 407 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 408 "(= $1 $2)\n" 409 "z3::unsat\n", 410 expr("void f(int x, int y) { if (x < y) return x == y; }", "==")); 411 } 412 if2()413 void if2() { 414 const char code[] = "void foo(int x) {\n" 415 " if (x > 0 && x == 20) {}\n" 416 "}"; 417 // In expression "x + x < 20", "x" is greater than 0 418 const char expected[] = "(> $1 0)\n" 419 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 420 "(= $1 20)\n" 421 "z3::sat\n"; 422 ASSERT_EQUALS(expected, expr(code, "==")); 423 } 424 if3()425 void if3() { 426 const char code[] = "void foo(int x) {\n" 427 " if (x > 0 || x == 20) {}\n" 428 "}"; 429 // In expression "x + x < 20", "x" is greater than 0 430 const char expected[] = "(<= $1 0)\n" 431 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 432 "(= $1 20)\n" 433 "z3::unsat\n"; // "x == 20" is unsat 434 ASSERT_EQUALS(expected, expr(code, "==")); 435 } 436 if4()437 void if4() { 438 const char code[] = "void foo(unsigned int x, unsigned int y) {\n" 439 " unsigned int z = y;" 440 " if (x < z) { return z == 0; }\n" 441 "}"; 442 const char expected[] = "(< $1 $2)\n" 443 "(>= $2 0)\n" 444 "(>= $1 0)\n" 445 "(= $2 0)\n" 446 "z3::unsat\n"; 447 ASSERT_EQUALS(expected, expr(code, "==")); 448 } 449 if5()450 void if5() { 451 ASSERT_EQUALS("(> |$2:0| 12)\n" 452 "(and (>= |$2:0| (- 2147483648)) (<= |$2:0| 2147483647))\n" 453 "(= |$2:0| 5)\n" 454 "z3::unsat\n", 455 expr("void foo(const int *x) { if (f1() && *x > 12) dostuff(*x == 5); }", "==")); 456 } 457 ifAlwaysTrue1()458 void ifAlwaysTrue1() { 459 const char code[] = "int foo() {\n" 460 " int a = 42;\n" 461 " if (1) {\n" 462 " a = 0;\n" 463 " }\n" 464 " return a == 0;\n" 465 "}"; 466 const char expected[] = "(= 0 0)\n" 467 "z3::sat\n"; 468 ASSERT_EQUALS(expected, expr(code, "==")); 469 } 470 ifAlwaysTrue2()471 void ifAlwaysTrue2() { 472 const char code[] = "int foo() {\n" 473 " int a = 42;\n" 474 " if (12.3) {\n" 475 " a = 0;\n" 476 " }\n" 477 " return a == 0;\n" 478 "}"; 479 const char expected[] = "(= 0 0)\n" 480 "z3::sat\n"; 481 ASSERT_EQUALS(expected, expr(code, "==")); 482 } 483 ifAlwaysTrue3()484 void ifAlwaysTrue3() { 485 const char code[] = "int foo() {\n" 486 " int a = 42;\n" 487 " if (\"test\") {\n" 488 " a = 0;\n" 489 " }\n" 490 " return a == 0;\n" 491 "}"; 492 // String literals are always true. z3 will not be involved. 493 ASSERT_EQUALS("(= 0 0)\n" 494 "z3::sat\n", 495 expr(code, "==")); 496 } 497 ifAlwaysFalse1()498 void ifAlwaysFalse1() { 499 const char code[] = "int foo() {\n" 500 " int a = 42;\n" 501 " if (0) {\n" 502 " a = 0;\n" 503 " }\n" 504 " return a == 0;\n" 505 "}"; 506 const char expected[] = "(= 42 0)\n" 507 "z3::unsat\n"; 508 ASSERT_EQUALS(expected, expr(code, "==")); 509 } 510 ifAlwaysFalse2()511 void ifAlwaysFalse2() { 512 const char code[] = "int foo() {\n" 513 " int a = 42;\n" 514 " if (0.0) {\n" 515 " a = 0;\n" 516 " }\n" 517 " return a == 0;\n" 518 "}"; 519 const char expected[] = "(= 42 0)\n" 520 "z3::unsat\n"; 521 ASSERT_EQUALS(expected, expr(code, "==")); 522 } 523 ifelse1()524 void ifelse1() { 525 ASSERT_EQUALS("(<= $1 5)\n" 526 "(and (>= $1 (- 32768)) (<= $1 32767))\n" 527 "(= (+ $1 2) 40)\n" 528 "z3::unsat\n", 529 expr("void f(short x) { if (x > 5) ; else if (x+2==40); }", "==")); 530 } 531 532 ifif()533 void ifif() { 534 const char code[] = "void foo(unsigned char x) {\n" 535 " if (x > 5) {}\n" 536 " if (x > 5) {}\n" 537 " return x == 13;\n" 538 "}"; 539 540 ASSERT_EQUALS("(> $1 5)\n" 541 "(and (>= $1 0) (<= $1 255))\n" 542 "(= $1 13)\n" 543 "z3::sat\n" 544 "(<= $1 5)\n" 545 "(and (>= $1 0) (<= $1 255))\n" 546 "(= $1 13)\n" 547 "z3::unsat\n", 548 expr(code, "==")); 549 } 550 551 ifreturn()552 void ifreturn() { // Early return 553 const char code[] = "void foo(unsigned char x) {\n" 554 " if (x > 5) { return; }\n" 555 " return x == 13;\n" 556 "}"; 557 558 ASSERT_EQUALS("(<= $1 5)\n" 559 "(and (>= $1 0) (<= $1 255))\n" 560 "(= $1 13)\n" 561 "z3::unsat\n", 562 expr(code, "==")); 563 } 564 ifIntRangeAlwaysFalse()565 void ifIntRangeAlwaysFalse() { 566 const char code[] = "void foo(unsigned char x) {\n" 567 " if (x > 0)\n" 568 " return;\n" 569 " if (x) {\n" // <-- condition should be "always false". 570 " x++;\n" 571 " }\n" 572 " return x == 0;\n" // <- sat 573 "}"; 574 ASSERT_EQUALS("(<= $1 0)\n" 575 "(and (>= $1 0) (<= $1 255))\n" 576 "(= $1 0)\n" 577 "z3::sat\n", 578 expr(code, "==")); 579 } 580 ifIntRangeAlwaysTrue()581 void ifIntRangeAlwaysTrue() { 582 const char code[] = "void foo(unsigned char x) {\n" 583 " if (x < 1)\n" 584 " return;\n" 585 " if (x) {\n" // <-- condition should be "always true". 586 " x++;\n" 587 " }\n" 588 " return x == 0;\n" // <- unsat 589 "}"; 590 ASSERT_EQUALS("(>= $1 1)\n" 591 "(and (>= $1 0) (<= $1 255))\n" 592 "(= (+ $1 1) 0)\n" 593 "z3::unsat\n", 594 expr(code, "==")); 595 } 596 istream()597 void istream() { 598 const char code[] = "void foo(const std::string& in) {\n" 599 " std::istringstream istr(in);\n" 600 " unsigned short x=5;\n" 601 " istr >> x;\n" 602 " x==3;\n" 603 "}"; 604 605 ASSERT_EQUALS("(and (>= $1 0) (<= $1 65535))\n" 606 "(= $1 3)\n" 607 "z3::sat\n", 608 expr(code, "==")); 609 } 610 switch1()611 void switch1() { 612 const char code[] = "void f(int x) {\n" 613 " switch (x) {\n" 614 " case 1: x==3; break;\n" 615 " case 2: x>0; break;\n" 616 " };\n" 617 " x<=4;\n" 618 "}"; 619 ASSERT_EQUALS("(= $1 1)\n" 620 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 621 "(= $1 3)\n" 622 "z3::unsat\n", 623 expr(code, "==")); 624 } 625 switch2()626 void switch2() { 627 const char code[] = "void foo(char type, int mcc) {\n" 628 " switch (type) {\n" 629 " case '1':\n" 630 " case '3':\n" 631 " break;\n" 632 " default:\n" 633 " return false;\n" 634 " }\n" 635 " p[0] = mcc == 0;\n" 636 "}"; 637 ASSERT_EQUALS("(= $1 49)\n" 638 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 639 "(and (>= $1 (- 128)) (<= $1 127))\n" 640 "(= $2 0)\n" 641 "z3::sat\n" 642 "(= $1 51)\n" 643 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 644 "(and (>= $1 (- 128)) (<= $1 127))\n" 645 "(= $2 0)\n" 646 "z3::sat\n", 647 expr(code, "==")); 648 } 649 650 for1()651 void for1() { 652 const char code[] = "void f() {\n" 653 " int x[10];\n" 654 " for (int i = 0; i < 10; i++) x[i] = 0;\n" 655 " x[4] == 67;\n" 656 "}"; 657 ASSERT_EQUALS("(= 0 67)\n" 658 "z3::unsat\n", 659 expr(code, "==")); 660 } 661 forAlwaysFalse1()662 void forAlwaysFalse1() { 663 const char code[] = "int f() {\n" 664 " int a = 19;\n" 665 " for (int i = 0; i < 0; i++)\n" 666 " a += 8;\n" 667 " for (int i = 0; i < 1; i++)\n" 668 " a += 23;\n" 669 " for (int i = 100; i >= 1; i--)\n" 670 " a += 23;\n" 671 " return a == 42;\n" 672 "}"; 673 const char expected[] = "(and (>= $4 (- 2147483648)) (<= $4 2147483647))\n" 674 "(= (+ $4 23) 42)\n" 675 "z3::sat\n"; 676 ASSERT_EQUALS(expected, expr(code, "==")); 677 } 678 while1()679 void while1() { 680 const char code[] = "void f(int y) {\n" 681 " int x = 0;\n" 682 " while (x < y)\n" 683 " x = x + 34;\n" 684 " x == 340;\n" 685 "}"; 686 const char expected[] = "(< 0 $1)\n" 687 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 688 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 689 "(= (+ $2 34) 340)\n" 690 "z3::sat\n" 691 "(= 0 340)\n" 692 "z3::unsat\n"; 693 ASSERT_EQUALS(expected, expr(code, "==")); 694 } 695 while2()696 void while2() { 697 const char code[] = "void f(int y) {\n" 698 " int x = 0;\n" 699 " while (x < y)\n" 700 " x++;\n" 701 " x == 1;\n" 702 "}"; 703 const char expected[] = "(< 0 $1)\n" 704 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 705 "(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 706 "(= (+ $2 1) 1)\n" 707 "z3::sat\n" 708 "(= 0 1)\n" 709 "z3::unsat\n"; 710 ASSERT_EQUALS(expected, expr(code, "==")); 711 } 712 while3()713 void while3() { 714 const char code[] = "struct AB {int a; int b;};\n" 715 "void f() {\n" 716 " struct AB ab;\n" 717 " while (1)\n" 718 " ab.a = 3;\n" 719 " ab.a == 0;\n" 720 "}"; 721 ASSERT_EQUALS("(= 3 0)\n" 722 "z3::unsat\n", 723 expr(code, "==")); 724 } 725 while4()726 void while4() { 727 const char code[] = "void f(const char *host, int *len) {\n" 728 " while (*host)\n" 729 " *len = 0;\n" 730 " *len == 0;\n" 731 "}"; 732 const char expected[] = "(distinct |$2:0| 0)\n" 733 "(and (>= |$2:0| (- 128)) (<= |$2:0| 127))\n" 734 "(= 0 0)\n" 735 "z3::sat\n" 736 "(and (>= $8 (- 2147483648)) (<= $8 2147483647))\n" 737 "(= $8 0)\n" 738 "z3::sat\n"; 739 ASSERT_EQUALS(expected, expr(code, "==")); 740 } 741 while5()742 void while5() { 743 const char code[] = "void f() {\n" 744 " int x;\n" 745 " while (cond)\n" 746 " x += 4;\n" 747 "}"; 748 ASSERT(getRange(code, "x", 4).find("?") != std::string::npos); 749 } 750 751 array1()752 void array1() { 753 ASSERT_EQUALS("(= 5 0)\nz3::unsat\n", 754 expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "==")); 755 } 756 array2()757 void array2() { 758 ASSERT_EQUALS("(and (>= |$4:4| 0) (<= |$4:4| 255))\n" 759 "(= |$4:4| 365)\n" 760 "z3::unsat\n", 761 expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "==")); 762 } 763 array3()764 void array3() { 765 const char code[] = "void f(unsigned char x) { int arr[10]; arr[4] = 43; return arr[x] == 12; }"; 766 ASSERT_EQUALS("?,43", getRange(code, "arr[x]")); 767 ASSERT_EQUALS("(and (>= $1 0) (<= $1 255))\n" 768 "(= (ite (= $1 4) 43 0) 12)\n" 769 "z3::unsat\n", 770 expr(code, "==")); 771 } 772 array4()773 void array4() { 774 const char code[] = "int buf[10];\n" 775 "void f() { int x = buf[0]; }"; 776 ASSERT_EQUALS("2:16: $2:0=IntRange(-2147483648:2147483647)\n" 777 "2:20: $1=ArrayValue([10],[:]=$2)\n" 778 "2:20: $2=IntRange(-2147483648:2147483647)\n" 779 "2:26: 0:memory:{buf=($1,[10],[:]=$2) x=$2:0}\n", 780 trackExecution(code)); 781 } 782 array5()783 void array5() { 784 const char code[] = "int f(int x) {\n" 785 " int buf[3][4][5];\n" 786 " buf[x][1][2] = 10;\n" 787 " return buf[0][1][2];\n" 788 "}"; 789 ASSERT_EQUALS("1:14: $1=IntRange(-2147483648:2147483647)\n" 790 "1:14: 0:memory:{x=$1}\n" 791 "2:7: $2=ArrayValue([3][4][5],[:]=?)\n" 792 "2:19: 0:memory:{x=$1 buf=($2,[3][4][5],[:]=?)}\n" 793 "3:20: 0:memory:{x=$1 buf=($2,[3][4][5],[:]=?,[((20)*($1))+(7)]=10)}\n", 794 trackExecution(code)); 795 } 796 array6()797 void array6() { 798 const char code[] = "void foo(int *x) {\n" 799 " *x = 2;\n" 800 " if (*x == 21) {}" 801 "}"; 802 ASSERT_EQUALS("(= 2 21)\n" 803 "z3::unsat\n", 804 expr(code, "==")); 805 } 806 array7()807 void array7() { 808 const char code[] = "void foo(unsigned char *x) {\n" 809 " *x = 2;\n" 810 " *x = 1;\n" 811 "}"; 812 ASSERT_EQUALS("1:28: $2=ArrayValue([$1],[:]=?,null)\n" 813 "1:28: $1=IntRange(1:ffffffffffffffff)\n" 814 "1:28: 0:memory:{x=($2,[$1],[:]=?)}\n" 815 "2:9: 0:memory:{x=($2,[$1],[:]=?,[0]=2)}\n" 816 "3:9: 0:memory:{x=($2,[$1],[:]=?,[0]=1)}\n", 817 trackExecution(code)); 818 } 819 arrayInit1()820 void arrayInit1() { 821 ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]")); 822 } 823 arrayInit2()824 void arrayInit2() { 825 ASSERT_EQUALS("66", getRange("void f() { char str[] = \"hello\"; str[0] = \'B\'; }", "str[0]=\'B\'")); 826 } 827 arrayInit3()828 void arrayInit3() { 829 ASSERT_EQUALS("-32768:32767", getRange("void f() { short buf[5] = {2, 1, 0, 3, 4}; ret = buf[2]; }", "buf[2]")); 830 } 831 arrayUninit()832 void arrayUninit() { 833 ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]")); 834 } 835 arrayInLoop()836 void arrayInLoop() { 837 const char code[] = "void f() {\n" 838 " int arr[3][3];\n" 839 " for (int i = 0; i < 3; i++) arr[i][0] = arr[1][2];\n" 840 " return arr[0][0];" 841 "}"; 842 ASSERT_EQUALS("?", getRange(code, "arr[1][2]")); 843 } 844 845 floatValue1()846 void floatValue1() { 847 ASSERT_EQUALS("-inf:inf", getRange("float f; void func() { f=f; }", "f=f")); 848 } 849 floatValue2()850 void floatValue2() { 851 ASSERT_EQUALS("(29.0)/(2.0)", getRange("void func() { float f = 29.0; f = f / 2.0; }", "f/2.0")); 852 } 853 floatValue3()854 void floatValue3() { 855 const char code[] = "void foo(float f) { return f > 12.3; }"; 856 const char expected[] = "(> $1 12.3)\n" 857 "z3::sat\n"; 858 ASSERT_EQUALS(expected, expr(code, ">")); 859 } 860 floatValue4()861 void floatValue4() { 862 const char code[] = "void foo(float f) { return f > 12.3f; }"; 863 const char expected[] = "(> $1 12.3)\n" 864 "z3::sat\n"; 865 ASSERT_EQUALS(expected, expr(code, ">")); 866 } 867 floatValue5()868 void floatValue5() { // float < int 869 const char code[] = "void foo(float f) { if (f < 1){} }"; 870 const char expected[] = "(< $1 (to_real 1))\n" 871 "z3::sat\n"; 872 ASSERT_EQUALS(expected, expr(code, "<")); 873 } 874 functionCall1()875 void functionCall1() { 876 ASSERT_EQUALS("-2147483648:2147483647", getRange("int atoi(const char *p); void f() { int x = atoi(a); x = x; }", "x=x")); 877 } 878 functionCall2()879 void functionCall2() { 880 const char code[] = "namespace NS {\n" 881 " short getValue();\n" 882 "}" 883 "void f() {\n" 884 " short value = NS::getValue();\n" 885 " value = value;\n" 886 "}"; 887 ASSERT_EQUALS("-32768:32767", getRange(code, "value=value")); 888 } 889 functionCall3()890 void functionCall3() { 891 ASSERT_EQUALS("-2147483648:2147483647", getRange("int fgets(int, const char *, void *); void f() { int x = -1; fgets(stdin, \"%d\", &x); x=x; }", "x=x")); 892 } 893 functionCall4()894 void functionCall4() { 895 ASSERT_EQUALS("1:2147483647", getRange("void f() { sizeof(data); }", "sizeof(data)")); 896 } 897 functionCall5()898 void functionCall5() { // unknown result from function, pointer type.. 899 ASSERT_EQUALS("1:36: $3=ArrayValue([$2],[:]=bailout,null)\n" 900 "1:36: $2=IntRange(1:2147483647)\n" 901 "1:36: bailout=BailoutValue(bailout)\n" 902 "1:46: 0:memory:{p=($3,[$2],[:]=bailout)}\n", 903 trackExecution("char *foo(int); void bar() { char *p = foo(1); }")); 904 } 905 functionCallContract1()906 void functionCallContract1() { 907 const char code[] = "void foo(int x);\n" 908 "void bar(unsigned short x) { foo(x); }"; 909 910 Settings s; 911 s.functionContracts["foo(x)"] = "x < 1000"; 912 913 ASSERT_EQUALS("checkContract:{\n" 914 "(ite (< $2 1000) false true)\n" 915 "(= $2 $1)\n" 916 "(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" 917 "(and (>= $1 0) (<= $1 65535))\n" 918 "}\n", 919 functionCallContractExpr(code, s)); 920 } 921 functionCallContract2()922 void functionCallContract2() { 923 const char code[] = "void foo(float x);\n" 924 "void bar(float x) { foo(x); }"; 925 926 Settings s; 927 s.functionContracts["foo(x)"] = "x < 12.3"; 928 929 ASSERT_EQUALS("checkContract:{\n" 930 "(ite (< $2 12.3) false true)\n" 931 "}\n", 932 functionCallContractExpr(code, s)); 933 } 934 935 int1()936 void int1() { 937 ASSERT_EQUALS("(and (>= $1 (- 2147483648)) (<= $1 2147483647))\n" 938 "(= (+ 2 $1) 3)\n" 939 "z3::sat\n", 940 expr("void f(int x) { return 2+x==3; }", "==")); 941 } 942 943 pointer1()944 void pointer1() { 945 const char code[] = "void f(unsigned char *p) { return *p == 7; }"; 946 ASSERT_EQUALS("[$1],[:]=?,null", getRange(code, "p")); 947 ASSERT_EQUALS("(and (>= $3 0) (<= $3 255))\n" 948 "(= $3 7)\n" 949 "z3::sat\n", 950 expr(code, "==")); 951 } 952 pointer2()953 void pointer2() { 954 const char code[] = "void f(unsigned char *p) { return p[2] == 7; }"; 955 ASSERT_EQUALS("(and (>= $3 0) (<= $3 255))\n" 956 "(= $3 7)\n" 957 "z3::sat\n", 958 expr(code, "==")); 959 } 960 pointer3()961 void pointer3() { 962 const char code[] = "void f(void *p) {\n" 963 " double *data = (double *)p;\n" 964 " return *data;" 965 "}"; 966 ASSERT_EQUALS("[$1],[:]=?,null", getRange(code, "p")); 967 ASSERT_EQUALS("[$4],[:]=?,null", getRange(code, "data")); 968 } 969 pointerAlias1()970 void pointerAlias1() { 971 ASSERT_EQUALS("3", getRange("int f() { int x; int *p = &x; x = 3; return *p; }", "return*p")); 972 } 973 pointerAlias2()974 void pointerAlias2() { 975 ASSERT_EQUALS("1", getRange("int f() { int x; int *p = &x; *p = 1; return *p; }", "return*p")); 976 } 977 pointerAlias3()978 void pointerAlias3() { 979 ASSERT_EQUALS("7", getRange("int f() {\n" 980 " int x = 18;\n" 981 " int *p = &x;\n" 982 " *p = 7;\n" 983 " return x;\n" 984 "}", "x", 5)); 985 } 986 pointerAlias4()987 void pointerAlias4() { 988 ASSERT_EQUALS("71", getRange("int f() { int x[10]; int *p = x+3; *p = 71; return x[3]; }", "x[3]")); 989 } 990 pointerNull1()991 void pointerNull1() { 992 ASSERT_EQUALS("1", getRange("void f(void *p) { p = NULL; p += 1; }", "p+=1")); 993 } 994 995 structMember1()996 void structMember1() { 997 ASSERT_EQUALS("(and (>= $2 0) (<= $2 255))\n" 998 "(and (>= $3 0) (<= $3 255))\n" 999 "(= (+ $2 $3) 0)\n" 1000 "z3::sat\n", 1001 expr("struct S {\n" 1002 " unsigned char a;\n" 1003 " unsigned char b;\n" 1004 "};\n" 1005 "void f(struct S s) { return s.a + s.b == 0; }", "==")); 1006 } 1007 structMember2()1008 void structMember2() { 1009 const char code[] = "struct S { int x; };\n" 1010 "void foo(struct S *s) { return s->x == 123; }"; 1011 1012 const char expected[] = "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" 1013 "(= $3 123)\n" 1014 "z3::sat\n"; 1015 1016 ASSERT_EQUALS(expected, expr(code, "==")); 1017 } 1018 structMember3()1019 void structMember3() { 1020 const char code[] = "struct S { int x; };\n" 1021 "void foo(struct S *s) {\n" 1022 " s->x = iter->second.data;\n" // assign some unknown value 1023 " return s->x == 1;\n" 1024 "}"; 1025 1026 const char expected[] = "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" 1027 "(= $3 1)\n" 1028 "z3::sat\n"; 1029 1030 ASSERT_EQUALS(expected, expr(code, "==")); 1031 } 1032 pointerToStructInLoop()1033 void pointerToStructInLoop() { 1034 const char code[] = "struct S { int x; };\n" 1035 "void foo(struct S *s) {\n" 1036 " while (1)\n" 1037 " s->x = 42; \n" 1038 "}"; 1039 1040 const char expected[] = "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n" 1041 "(= $3 42)\n" 1042 "z3::sat\n"; 1043 1044 TODO_ASSERT_EQUALS(expected, "", expr(code, "==")); 1045 } 1046 1047 ternaryOperator1()1048 void ternaryOperator1() { 1049 const char code[] = "void foo(signed char x) {\n" 1050 " x = (x > 0) ? (0==x) : 0;\n" 1051 "}"; 1052 1053 const char expected[] = "(> $1 0)\n" 1054 "(and (>= $1 (- 128)) (<= $1 127))\n" 1055 "(= 0 $1)\n" 1056 "z3::unsat\n"; 1057 1058 ASSERT_EQUALS(expected, expr(code, "==")); 1059 } 1060 }; 1061 1062 REGISTER_TEST(TestExprEngine) 1063