Cppcheck
Macros | Functions | Variables
exprengine.cpp File Reference
#include "exprengine.h"
#include "astutils.h"
#include "bughuntingchecks.h"
#include "errorlogger.h"
#include "library.h"
#include "mathlib.h"
#include "platform.h"
#include "settings.h"
#include "symboldatabase.h"
#include "token.h"
#include "tokenize.h"
#include "tokenlist.h"
#include <cctype>
#include <climits>
#include <cstdint>
#include <ctime>
#include <exception>
#include <iostream>
#include <limits>
#include <list>
#include <memory>
#include <set>
#include <tuple>

Go to the source code of this file.

Macros

#define CONTRACT   1
 

Functions

static std::string str (ExprEngine::ValuePtr val)
 
static size_t extfind (const std::string &str, const std::string &what, size_t pos)
 
static ExprEngine::ValuePtr getValueRangeFromValueType (const std::string &name, const ValueType *vt, const cppcheck::Platform &platform)
 
static ExprEngine::ValuePtr simplifyValue (ExprEngine::ValuePtr origValue)
 
static ExprEngine::ValuePtr translateUninitValueToRange (ExprEngine::ValuePtr value, const ::ValueType *valueType, Data &data)
 
static int128_t truncateInt (int128_t value, int bits, char sign)
 
static bool isEqual (ExprEngine::ValuePtr v1, ExprEngine::ValuePtr v2)
 
static bool isNonOverlapping (ExprEngine::ValuePtr v1, ExprEngine::ValuePtr v2)
 
static int getIntBitsFromValueType (const ValueType *vt, const cppcheck::Platform &platform)
 
static ExprEngine::ValuePtr getValueRangeFromValueType (const ValueType *valueType, Data &data)
 
static void call (const std::vector< ExprEngine::Callback > &callbacks, const Token *tok, ExprEngine::ValuePtr value, Data *dataBase)
 
static ExprEngine::ValuePtr executeExpression (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeExpression1 (const Token *tok, Data &data)
 
static std::string execute (const Token *start, const Token *end, Data &data)
 
static ExprEngine::ValuePtr calculateArrayIndex (const Token *tok, Data &data, const ExprEngine::ArrayValue &arrayValue)
 
static ExprEngine::ValuePtr executeReturn (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr truncateValue (ExprEngine::ValuePtr val, const ValueType *valueType, Data &data)
 
static void assignExprValue (const Token *expr, ExprEngine::ValuePtr value, Data &data)
 
static ExprEngine::ValuePtr executeAssign (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeIncDec (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeFunctionCall (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeArrayIndex (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeCast (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeDot (const Token *tok, Data &data)
 
static void streamReadSetValue (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeStreamRead (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeBinaryOp (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeAddressOf (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeDeref (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeNot (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeVariable (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeKnownMacro (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeNumber (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr executeStringLiteral (const Token *tok, Data &data)
 
static ExprEngine::ValuePtr createVariableValue (const Variable &var, Data &data)
 
static std::tuple< bool, bool > checkConditionBranches (const ExprEngine::ValuePtr &condValue, const Data &data)
 
static ExprEngine::ValuePtr createStructVal (const Token *tok, const Scope *structScope, bool uninitData, Data &data)
 
static void dumpRecursive (ExprEngine::ValuePtr val)
 

Variables

const uint32_t MAX_BUFFER_SIZE = ~0U >> 1
 This is the ExprEngine component in Cppcheck. More...
 

Macro Definition Documentation

◆ CONTRACT

#define CONTRACT   1

Definition at line 166 of file exprengine.cpp.

Function Documentation

◆ assignExprValue()

static void assignExprValue ( const Token *  expr,
ExprEngine::ValuePtr  value,
Data &  data 
)
static

Definition at line 1865 of file exprengine.cpp.

References ExprEngine::AddressOfValue, ExprEngine::ArrayValue, Token::astOperand1(), Token::astOperand2(), ExprEngine::BinOpResult::binop, ExprEngine::BinOpResult, calculateArrayIndex(), call(), executeExpression(), Token::isUnaryOp(), Token::Match(), Token::next(), ExprEngine::BinOpResult::op1, ExprEngine::BinOpResult::op2, Token::scope(), Token::simpleMatch(), ExprEngine::str(), Token::str(), ExprEngine::StringLiteralValue, ExprEngine::StructValue, ExprEngine::Value::type, Token::variable(), and Token::varId().

Referenced by executeAssign(), executeFunctionCall(), executeIncDec(), and streamReadSetValue().

◆ calculateArrayIndex()

static ExprEngine::ValuePtr calculateArrayIndex ( const Token *  tok,
Data &  data,
const ExprEngine::ArrayValue &  arrayValue 
)
static

Definition at line 1782 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), executeExpression(), Token::simpleMatch(), simplifyValue(), and ExprEngine::ArrayValue::size.

Referenced by assignExprValue(), and executeArrayIndex().

◆ call()

static void call ( const std::vector< ExprEngine::Callback > &  callbacks,
const Token *  tok,
ExprEngine::ValuePtr  value,
Data *  dataBase 
)
static

Definition at line 1765 of file exprengine.cpp.

Referenced by assignExprValue(), execute(), executeAddressOf(), executeArrayIndex(), executeAssign(), executeBinaryOp(), executeCast(), executeDeref(), executeDot(), ExprEngine::executeFunction(), executeFunctionCall(), executeIncDec(), executeKnownMacro(), executeNot(), executeNumber(), executeReturn(), executeVariable(), loadReflection(), Summaries::loadReturn(), streamReadSetValue(), and writeReflection().

◆ checkConditionBranches()

static std::tuple<bool, bool> checkConditionBranches ( const ExprEngine::ValuePtr &  condValue,
const Data &  data 
)
static

Definition at line 2516 of file exprengine.cpp.

References ExprEngine::BinOpResult::isEqual(), and ExprEngine::BinOpResult::isTrue().

Referenced by execute().

◆ createStructVal()

static ExprEngine::ValuePtr createStructVal ( const Token *  tok,
const Scope *  structScope,
bool  uninitData,
Data &  data 
)
static

Definition at line 2916 of file exprengine.cpp.

References createVariableValue(), Variable::isInit(), ValueType::isIntegral(), Variable::isPointer(), Variable::name(), ValueType::type, Variable::valueType(), and Scope::varlist.

Referenced by createVariableValue().

◆ createVariableValue()

static ExprEngine::ValuePtr createVariableValue ( const Variable &  var,
Data &  data 
)
static

Definition at line 2942 of file exprengine.cpp.

References Type::classScope, ValueType::constness, createStructVal(), Scope::definedType, Type::False, getValueRangeFromValueType(), Variable::isArgument(), Variable::isArray(), Variable::isConst(), ValueType::isFloat(), ValueType::isIntegral(), Variable::isLocal(), Variable::isPointer(), Variable::isStatic(), MAX_BUFFER_SIZE, Variable::nameToken(), Type::needInitialization, ValueType::pointer, ValueType::smartPointerType, ValueType::type, ValueType::typeScope, Variable::valueType(), and Token::valueType().

Referenced by createStructVal(), execute(), and ExprEngine::executeFunction().

◆ dumpRecursive()

static void dumpRecursive ( ExprEngine::ValuePtr  val)
static

Definition at line 3103 of file exprengine.cpp.

References ExprEngine::AddressOfValue, ExprEngine::ArrayValue, ExprEngine::BailoutValue, ExprEngine::BinOpResult::binop, ExprEngine::BinOpResult, ExprEngine::ConditionalValue, ExprEngine::FloatRange, ExprEngine::FunctionCallArgumentValues, ExprEngine::IntegerTruncation, ExprEngine::IntRange, ExprEngine::BinOpResult::op1, ExprEngine::BinOpResult::op2, ExprEngine::StringLiteralValue, ExprEngine::StructValue, and ExprEngine::UninitValue.

Referenced by ExprEngine::dump().

◆ execute()

static std::string execute ( const Token *  start,
const Token *  end,
Data &  data 
)
static

Definition at line 2536 of file exprengine.cpp.

References ExprEngine::ArrayValue, Token::astOperand1(), Token::astOperand2(), Token::astParent(), Scope::bodyEnd, call(), checkConditionBranches(), createVariableValue(), Scope::eElse, Scope::eIf, executeExpression(), extractForLoopValues(), getValueRangeFromValueType(), Token::isUnaryOp(), Token::link(), Token::linkAt(), Token::Match(), MAX_BUFFER_SIZE, Variable::name(), Scope::nestedIn, Token::next(), nonneg, op1_and_op2, precedes(), Token::previous(), Token::scope(), Token::simpleMatch(), Token::str(), Token::tokAt(), MathLib::toString(), Scope::type, ValueType::typeScope, ExprEngine::UninitValue, Variable::valueType(), Token::valueType(), Token::variable(), Token::varId(), Scope::varlist, and visitAstNodes().

Referenced by ConditionHandler::afterCondition(), ValueFlowAnalyzer::evaluateInt(), ExprEngine::executeFunction(), executeFunctionCall(), valueFlowForLoop2(), and valueFlowFunctionReturn().

◆ executeAddressOf()

static ExprEngine::ValuePtr executeAddressOf ( const Token *  tok,
Data &  data 
)
static

Definition at line 2363 of file exprengine.cpp.

References Token::astOperand1(), and call().

Referenced by executeExpression1().

◆ executeArrayIndex()

static ExprEngine::ValuePtr executeArrayIndex ( const Token *  tok,
Data &  data 
)
static

Definition at line 2187 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), calculateArrayIndex(), call(), Token::eLambda, executeExpression(), Token::simpleMatch(), and Token::tokType().

Referenced by executeExpression1().

◆ executeAssign()

static ExprEngine::ValuePtr executeAssign ( const Token *  tok,
Data &  data 
)
static

Definition at line 1936 of file exprengine.cpp.

References assignExprValue(), Token::astOperand1(), Token::astOperand2(), call(), executeExpression(), getValueRangeFromValueType(), ValueType::pointer, simplifyValue(), Token::str(), truncateValue(), and Token::valueType().

Referenced by executeExpression1().

◆ executeBinaryOp()

static ExprEngine::ValuePtr executeBinaryOp ( const Token *  tok,
Data &  data 
)
static

Definition at line 2315 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), call(), executeExpression(), simplifyValue(), and Token::str().

Referenced by executeExpression1().

◆ executeCast()

static ExprEngine::ValuePtr executeCast ( const Token *  tok,
Data &  data 
)
static

Definition at line 2212 of file exprengine.cpp.

References ExprEngine::ArrayValue, Token::astOperand1(), Token::astOperand2(), call(), executeExpression(), getValueRangeFromValueType(), MAX_BUFFER_SIZE, ValueType::pointer, ValueType::type, and Token::valueType().

Referenced by executeExpression1().

◆ executeDeref()

static ExprEngine::ValuePtr executeDeref ( const Token *  tok,
Data &  data 
)
static

Definition at line 2370 of file exprengine.cpp.

References Token::astOperand1(), call(), executeExpression(), getValueRangeFromValueType(), and Token::valueType().

Referenced by executeExpression1().

◆ executeDot()

static ExprEngine::ValuePtr executeDot ( const Token *  tok,
Data &  data 
)
static

Definition at line 2248 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), call(), executeExpression(), getValueRangeFromValueType(), Token::originalName(), and Token::valueType().

Referenced by executeExpression1().

◆ executeExpression()

static ExprEngine::ValuePtr executeExpression ( const Token *  tok,
Data &  data 
)
static

Definition at line 2509 of file exprengine.cpp.

References executeExpression1(), translateUninitValueToRange(), and Token::valueType().

Referenced by assignExprValue(), calculateArrayIndex(), execute(), executeArrayIndex(), executeAssign(), executeBinaryOp(), executeCast(), executeDeref(), executeDot(), executeFunctionCall(), executeIncDec(), executeNot(), and executeReturn().

◆ executeExpression1()

static ExprEngine::ValuePtr executeExpression1 ( const Token *  tok,
Data &  data 
)
static

Definition at line 2447 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), Token::astParent(), executeAddressOf(), executeArrayIndex(), executeAssign(), executeBinaryOp(), executeCast(), executeDeref(), executeDot(), executeFunctionCall(), executeIncDec(), executeKnownMacro(), executeNot(), executeNumber(), executeReturn(), executeStreamRead(), executeStringLiteral(), executeVariable(), Token::getKnownIntValue(), Token::hasKnownIntValue(), Token::isAssignmentOp(), Token::isBinaryOp(), Token::isCast(), Token::isName(), Token::isNumber(), Token::isUnaryOp(), Token::Match(), Token::str(), Settings::terminated(), Token::tokType(), and Token::varId().

Referenced by executeExpression(), ExprEngine::executeFunction(), and executeFunctionCall().

◆ executeFunctionCall()

static ExprEngine::ValuePtr executeFunctionCall ( const Token *  tok,
Data &  data 
)
static

Definition at line 2065 of file exprengine.cpp.

References assignExprValue(), Token::astOperand1(), bailout, ExprEngine::BailoutValue, Scope::bodyEnd, Scope::bodyStart, call(), Variable::declarationId(), execute(), executeExpression(), executeExpression1(), getArguments(), Token::getKnownIntValue(), getValueRangeFromValueType(), Token::hasKnownIntValue(), Scope::isExecutable(), ValueType::isIntegral(), Variable::isReference(), MAX_BUFFER_SIZE, Scope::nestedIn, ValueType::pointer, Token::previous(), Token::scope(), Token::simpleMatch(), translateUninitValueToRange(), Scope::type, Variable::valueType(), and Token::valueType().

Referenced by executeExpression1().

◆ executeIncDec()

static ExprEngine::ValuePtr executeIncDec ( const Token *  tok,
Data &  data 
)
static

Definition at line 1975 of file exprengine.cpp.

References assignExprValue(), Token::astOperand1(), call(), executeExpression(), precedes(), simplifyValue(), and Token::str().

Referenced by executeExpression1().

◆ executeKnownMacro()

static ExprEngine::ValuePtr executeKnownMacro ( const Token *  tok,
Data &  data 
)
static

Definition at line 2419 of file exprengine.cpp.

References call(), and Token::getKnownIntValue().

Referenced by executeExpression1().

◆ executeNot()

static ExprEngine::ValuePtr executeNot ( const Token *  tok,
Data &  data 
)
static

Definition at line 2401 of file exprengine.cpp.

References Token::astOperand1(), call(), executeExpression(), and simplifyValue().

Referenced by executeExpression1().

◆ executeNumber()

static ExprEngine::ValuePtr executeNumber ( const Token *  tok,
Data &  data 
)
static

Definition at line 2427 of file exprengine.cpp.

References call(), ValueType::isFloat(), Token::str(), MathLib::toDoubleNumber(), MathLib::toLongNumber(), and Token::valueType().

Referenced by executeExpression1().

◆ executeReturn()

static ExprEngine::ValuePtr executeReturn ( const Token *  tok,
Data &  data 
)
static

Definition at line 1823 of file exprengine.cpp.

References Token::astOperand1(), call(), and executeExpression().

Referenced by executeExpression1().

◆ executeStreamRead()

static ExprEngine::ValuePtr executeStreamRead ( const Token *  tok,
Data &  data 
)
static

Definition at line 2304 of file exprengine.cpp.

References Token::astOperand1(), Token::astOperand2(), Token::simpleMatch(), and streamReadSetValue().

Referenced by executeExpression1().

◆ executeStringLiteral()

static ExprEngine::ValuePtr executeStringLiteral ( const Token *  tok,
Data &  data 
)
static

Definition at line 2441 of file exprengine.cpp.

References Token::str().

Referenced by executeExpression1().

◆ executeVariable()

static ExprEngine::ValuePtr executeVariable ( const Token *  tok,
Data &  data 
)
static

Definition at line 2412 of file exprengine.cpp.

References call(), Token::valueType(), and Token::varId().

Referenced by executeExpression1().

◆ extfind()

static size_t extfind ( const std::string &  str,
const std::string &  what,
size_t  pos 
)
static

Definition at line 222 of file exprengine.cpp.

References indent(), and str().

◆ getIntBitsFromValueType()

static int getIntBitsFromValueType ( const ValueType *  vt,
const cppcheck::Platform &  platform 
)
static

Definition at line 1695 of file exprengine.cpp.

References cppcheck::Platform::char_bit, cppcheck::Platform::int_bit, cppcheck::Platform::long_bit, cppcheck::Platform::long_long_bit, cppcheck::Platform::short_bit, and ValueType::type.

Referenced by getValueRangeFromValueType(), and truncateValue().

◆ getValueRangeFromValueType() [1/2]

static ExprEngine::ValuePtr getValueRangeFromValueType ( const std::string &  name,
const ValueType *  vt,
const cppcheck::Platform &  platform 
)
static

Definition at line 1718 of file exprengine.cpp.

References getIntBitsFromValueType(), ValueType::isFloat(), ValueType::isIntegral(), ValueType::pointer, and ValueType::sign.

Referenced by ExprEngine::ArrayValue::ArrayValue(), createVariableValue(), execute(), executeAssign(), executeCast(), executeDeref(), executeDot(), executeFunctionCall(), getValueRangeFromValueType(), streamReadSetValue(), translateUninitValueToRange(), and truncateValue().

◆ getValueRangeFromValueType() [2/2]

static ExprEngine::ValuePtr getValueRangeFromValueType ( const ValueType *  valueType,
Data &  data 
)
static

Definition at line 1740 of file exprengine.cpp.

References ValueType::container, ValueType::containerTypeToken, getValueRangeFromValueType(), ExprEngine::ArrayValue::MAXSIZE, ValueType::parseDecl(), ValueType::pointer, and Library::Container::stdStringLike.

◆ isEqual()

static bool isEqual ( ExprEngine::ValuePtr  v1,
ExprEngine::ValuePtr  v2 
)
static

Definition at line 974 of file exprengine.cpp.

Referenced by ExprEngine::ArrayValue::read().

◆ isNonOverlapping()

static bool isNonOverlapping ( ExprEngine::ValuePtr  v1,
ExprEngine::ValuePtr  v2 
)
static

Definition at line 981 of file exprengine.cpp.

Referenced by ExprEngine::ArrayValue::read().

◆ simplifyValue()

static ExprEngine::ValuePtr simplifyValue ( ExprEngine::ValuePtr  origValue)
static

Definition at line 833 of file exprengine.cpp.

References ExprEngine::str().

Referenced by calculateArrayIndex(), executeAssign(), executeBinaryOp(), executeIncDec(), and executeNot().

◆ str()

static std::string str ( ExprEngine::ValuePtr  val)
static

Definition at line 177 of file exprengine.cpp.

References ExprEngine::AddressOfValue, ExprEngine::ArrayValue, ExprEngine::BailoutValue, ExprEngine::BinOpResult, ExprEngine::ConditionalValue, ExprEngine::FloatRange, ExprEngine::FunctionCallArgumentValues, ExprEngine::IntegerTruncation, ExprEngine::IntRange, ExprEngine::StringLiteralValue, ExprEngine::StructValue, and ExprEngine::UninitValue.

Referenced by Settings::addEnabled(), TimerResults::addResults(), TokenList::addtoken(), clangimport::AstNode::addtoken(), clangimport::AstNode::addTypeTokens(), bufferOverflow(), CppCheckExecutor::bughuntingReport(), ThreadResult::bughuntingReport(), CppCheck::bughuntingReport(), ErrorLogger::callStackToString(), checkAssignment(), CheckOther::checkFuncArgNamesDifferent(), TokenList::createTokens(), MathLib::encodeMultiChar(), endsWith(), CppCheck::executeRules(), TemplateSimplifier::expandTemplate(), extfind(), floatHexToDoubleNumber(), getCharLiteral(), Library::getInvalidArgValues(), getMode(), clangimport::AstNode::getSpelling(), getStringCharLiteral(), getStringLiteral(), TemplateSimplifier::getTemplateInstantiations(), CheckStl::if_findError(), ImportProject::importCompileCommands(), MathLib::isBin(), isCharLiteral(), MathLib::isDec(), MathLib::isDecimalFloat(), MathLib::isFloat(), MathLib::isFloatHex(), MathLib::isInt(), MathLib::isIntHex(), MathLib::isNegative(), MathLib::isNullValue(), MathLib::isOct(), MathLib::isPositive(), isPrefixStringCharLiteral(), isStringCharLiteral(), isStringLiteral(), MathLib::isValidIntegerSuffix(), Library::load(), Library::loadFunction(), ResultsView::log(), myStod(), CheckString::overlappingStrcmp(), parsedecl(), CmdLineParser::parseFromArgs(), readUntil(), Standards::setC(), Standards::setCPP(), TemplateSimplifier::simplifyNumericCalculations(), TemplateSimplifier::simplifyTemplateAliases(), Tokenizer::simplifyUsing(), split(), stringFromTokenRange(), ErrorMessage::FileLocation::stringify(), CheckString::stringLiteralWrite(), MathLib::toDoubleNumber(), MathLib::toLongNumber(), ErrorItem::toString(), MathLib::toULongNumber(), ErrorLogger::toxml(), Tokenizer::unsupportedTypedef(), ProjectFile::writeStringList(), and Check::wrongData().

◆ streamReadSetValue()

static void streamReadSetValue ( const Token *  tok,
Data &  data 
)
static

Definition at line 2290 of file exprengine.cpp.

References assignExprValue(), call(), getValueRangeFromValueType(), ValueType::pointer, Token::valueType(), and Token::varId().

Referenced by executeStreamRead().

◆ translateUninitValueToRange()

static ExprEngine::ValuePtr translateUninitValueToRange ( ExprEngine::ValuePtr  value,
const ::ValueType *  valueType,
Data &  data 
)
static

Definition at line 862 of file exprengine.cpp.

References getValueRangeFromValueType(), and ExprEngine::UninitValue.

Referenced by executeExpression(), and executeFunctionCall().

◆ truncateInt()

static int128_t truncateInt ( int128_t  value,
int  bits,
char  sign 
)
static

Definition at line 881 of file exprengine.cpp.

Referenced by truncateValue().

◆ truncateValue()

static ExprEngine::ValuePtr truncateValue ( ExprEngine::ValuePtr  val,
const ValueType *  valueType,
Data &  data 
)
static

Definition at line 1830 of file exprengine.cpp.

References getIntBitsFromValueType(), getValueRangeFromValueType(), ValueType::isIntegral(), ValueType::pointer, ValueType::sign, ExprEngine::str(), and truncateInt().

Referenced by executeAssign().

Variable Documentation

◆ MAX_BUFFER_SIZE

const uint32_t MAX_BUFFER_SIZE = ~0U >> 1

This is the ExprEngine component in Cppcheck.

Its job is to convert the C/C++ code into expressions that the Z3 prover understands. We can then ask Z3 prover for instance if variable "x" can be 123 and the Z3 prover can tell us that.

Overview

The ExprEngine performs a "abstract execution" of each function.

  • ExprEngine performs "forward" analysis only. It starts at the top of the functions.
  • There is a abstract program state Data::memory.
  • The constraints are stored in the vector Data::constraints.

Abstract program state

The map Data::memory contains the abstract values of all variables that are used in the current function scope.

Use --debug-bug-hunting --verbose to dump out Data::memory. Example output: 2:5: { x=$1 y=$2} Explanation: At line 2, column 5: The memory has two variables. Variable x has the value $1. Variable y has the value $2.

Different value names:

  • Typical abstract value has name that starts with "$". The number is just a incremented value.
  • If a variable has a known value then the concrete value is written. Example: { x=1 }.
  • For an uninitialized value the output says "?". For example: { a=? }
  • For buffers the output is something like { buf=($3,size=10,[:]=?,[$1]=$2) } The first item "$3" is the name of the buffer value. The second item says that the size of this buffer is 10. After that comes [index]=value items that show what values buffer items have: [:]=? means that all items are uninitialized. [$1]=$2 means that the buffer item at index "$1" has value "$2".

Abstract execution

The function: static std::string execute(const Token *start, const Token *end, Data &data)

Perform abstract execution of the code from start to end. The data is modified during the abstract execution.

Each astTop token is executed. From that, operands are executed recursively in the "execute.." functions. The result of an operand is a abstract value.

Branches

Imagine: code1 if (x > 0) code2 else code3 code4

When "if" is reached.. the current data is branched into thenData and elseData. For "thenData" a constraint is added: x>0 For "elseData" a constraint is added: !(x>0)

Then analysis of thenData and elseData will continue separately, by recursive execution. The "code4" block will be analysed both with thenData and elseData.

Z3

The ExprEngine will not execute Z3 unless a check wants it to.

The abstract values and all their constraints is added to a Z3 solver object and after that Z3 can tell us if some condition can be true.

Z3 is a SMT solver: https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

In SMT:

  • all variables are "constant". A variable can not be changed or assigned.
  • There is no "execution". The solver considers all equations simultaneously.

Simple example (TestExpr::expr6): 

void f(unsigned char x)
{
     unsigned char y = 8 - x;\n"
     y > 1000;
}

If a check wants to know if "y > 1000" can be true, ExprEngine will generate this Z3 input: 

(declare-fun $1 () Int)
(assert (and (>= $1 0) (<= $1 255)))
(assert (> (- 8 $1) 1000))

A symbol "$1" is created. assert that "$1" is a value 0-255. assert that "8-$1" is greater than 1000.

Z3 can now determine if these assertions are possible or not. In this case these assertions are not possible, there is no value for $1 between 0-255 that means that "8-$1" is greater than 1000.

Definition at line 165 of file exprengine.cpp.

Referenced by createVariableValue(), execute(), executeCast(), and executeFunctionCall().

Generated on Sun Apr 10 2022 11:53:32 for Cppcheck by doxygen 1.9.1