diff options
| author | chriseth <chris@ethereum.org> | 2017-10-20 22:55:09 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-20 22:55:09 +0800 |
| commit | 7d0e46bf59cd966f943ef9839e8e26d857150192 (patch) | |
| tree | 824de8024ac992cb084f72252a4a894f31107f5a | |
| parent | bdd2858bfd6bb5b880797a5984e212c4b63d9e04 (diff) | |
| parent | 18ae0c3d784cb587d50bdfc1f33e200fd97f2676 (diff) | |
| download | dexon-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.cpp | 9 | ||||
| -rw-r--r-- | libsolidity/formal/SMTLib2Interface.h | 8 |
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; }; } |