cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

SMT enforce variable types

Browse Source
This commit is contained in:
Alex Beregszaszi 2017-10-04 14:23:27 +01:00
parent 6ba0c2bba8
commit 18ae0c3d78
2 changed files with 16 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
libsolidity/formal/SMTLib2Interface.cpp
View File

@ -64,6 +64,8 @@ void SMTLib2Interface::pop()
Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain) Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
{ {
solAssert(!m_variables.count(_name), "");
m_variables[_name] = SMTVariableType::Function;
write( write(
"(declare-fun |" + "(declare-fun |" +
_name + _name +
@ -78,12 +80,16 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
Expression SMTLib2Interface::newInteger(string _name) Expression SMTLib2Interface::newInteger(string _name)
{ {
solAssert(!m_variables.count(_name), "");
m_variables[_name] = SMTVariableType::Integer;
write("(declare-const |" + _name + "| Int)"); write("(declare-const |" + _name + "| Int)");
return SolverInterface::newInteger(move(_name)); return SolverInterface::newInteger(move(_name));
} }
Expression SMTLib2Interface::newBool(string _name) Expression SMTLib2Interface::newBool(string _name)
{ {
solAssert(!m_variables.count(_name), "");
m_variables[_name] = SMTVariableType::Bool;
write("(declare-const |" + _name + "| Bool)"); write("(declare-const |" + _name + "| Bool)");
return SolverInterface::newBool(std::move(_name)); return SolverInterface::newBool(std::move(_name));
} }
@ -145,7 +151,8 @@ string SMTLib2Interface::checkSatAndGetValuesCommand(vector<Expression> const& _
for (size_t i = 0; i < _expressionsToEvaluate.size(); i++) for (size_t i = 0; i < _expressionsToEvaluate.size(); i++)
{ {
auto const& e = _expressionsToEvaluate.at(i); auto const& e = _expressionsToEvaluate.at(i);
// TODO they don't have to be ints... solAssert(m_variables.count(e.name), "");
solAssert(m_variables[e.name] == SMTVariableType::Integer, "");
command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n"; command += "(declare-const |EVALEXPR_" + to_string(i) + "| Int)\n";
command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n"; command += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
} }

8
libsolidity/formal/SMTLib2Interface.h
View File

@ -68,6 +68,14 @@ private:
ReadCallback::Callback m_queryCallback; ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput; std::vector<std::string> m_accumulatedOutput;
enum class SMTVariableType {
Function,
Integer,
Bool
};
std::map<std::string,SMTVariableType> m_variables;
}; };
} }