diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 22 |
1 files changed, 19 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index cc580021..9a2b9bbf 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -78,6 +78,9 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_interface->reset(); m_pathConditions.clear(); m_expressions.clear(); + m_specialVariables.clear(); + m_uninterpretedFunctions.clear(); + m_uninterpretedTerms.clear(); resetStateVariables(); initializeLocalVariables(_function); } @@ -412,9 +415,12 @@ void SMTChecker::visitGasLeft(FunctionCall const& _funCall) void SMTChecker::visitBlockHash(FunctionCall const& _funCall) { - string blockHash = "blockhash()"; - // TODO Define blockhash as an uninterpreted function - defineSpecialVariable(blockHash, _funCall); + string blockHash = "blockhash"; + defineUninterpretedFunction(blockHash, {smt::Sort::Int}, smt::Sort::Int); + auto const& arguments = _funCall.arguments(); + solAssert(arguments.size() == 1, ""); + defineExpr(_funCall, m_uninterpretedFunctions.at(blockHash)({expr(*arguments[0])})); + m_uninterpretedTerms.push_back(&_funCall); } void SMTChecker::inlineFunctionCall(FunctionCall const& _funCall) @@ -587,6 +593,11 @@ void SMTChecker::defineSpecialVariable(string const& _name, Expression const& _e defineExpr(_expr, m_specialVariables.at(_name)->currentValue()); } +void SMTChecker::defineUninterpretedFunction(string const& _name, vector<smt::Sort> const& _domain, smt::Sort _codomain) +{ + if (!m_uninterpretedFunctions.count(_name)) + m_uninterpretedFunctions.emplace(_name, m_interface->newFunction(_name, _domain, _codomain)); +} void SMTChecker::arithmeticOperation(BinaryOperation const& _op) { @@ -770,6 +781,11 @@ void SMTChecker::checkCondition( expressionsToEvaluate.emplace_back(var.second->currentValue()); expressionNames.push_back(var.first); } + for (auto const& uf: m_uninterpretedTerms) + { + expressionsToEvaluate.emplace_back(expr(*uf)); + expressionNames.push_back(m_scanner->sourceAt(uf->location())); + } } smt::CheckResult result; vector<string> values; |