aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-10-20 22:55:09 +0800
committerGitHub <noreply@github.com>2017-10-20 22:55:09 +0800
commit7d0e46bf59cd966f943ef9839e8e26d857150192 (patch)
tree824de8024ac992cb084f72252a4a894f31107f5a
parentbdd2858bfd6bb5b880797a5984e212c4b63d9e04 (diff)
parent18ae0c3d784cb587d50bdfc1f33e200fd97f2676 (diff)
downloaddexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar.gz
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar.bz2
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar.lz
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar.xz
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.tar.zst
dexon-solidity-7d0e46bf59cd966f943ef9839e8e26d857150192.zip
Merge pull request #3030 from ethereum/smt-variable-types
SMT enforce variable types
-rw-r--r--libsolidity/formal/SMTLib2Interface.cpp9
-rw-r--r--libsolidity/formal/SMTLib2Interface.h8
2 files changed, 16 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index cbd766fb..c627057a 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -64,6 +64,8 @@ void SMTLib2Interface::pop()
Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
{
+ solAssert(!m_variables.count(_name), "");
+ m_variables[_name] = SMTVariableType::Function;
write(
"(declare-fun |" +
_name +
@@ -78,12 +80,16 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
Expression SMTLib2Interface::newInteger(string _name)
{
+ solAssert(!m_variables.count(_name), "");
+ m_variables[_name] = SMTVariableType::Integer;
write("(declare-const |" + _name + "| Int)");
return SolverInterface::newInteger(move(_name));
}
Expression SMTLib2Interface::newBool(string _name)
{
+ solAssert(!m_variables.count(_name), "");
+ m_variables[_name] = SMTVariableType::Bool;
write("(declare-const |" + _name + "| Bool)");
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++)
{
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 += "(assert (= |EVALEXPR_" + to_string(i) + "| " + toSExpr(e) + "))\n";
}
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 63188acd..e827449f 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -68,6 +68,14 @@ private:
ReadCallback::Callback m_queryCallback;
std::vector<std::string> m_accumulatedOutput;
+
+ enum class SMTVariableType {
+ Function,
+ Integer,
+ Bool
+ };
+
+ std::map<std::string,SMTVariableType> m_variables;
};
}