diff options
| author | Alex Beregszaszi <alex@rtfs.hu> | 2017-10-04 21:23:27 +0800 |
|---|---|---|
| committer | Alex Beregszaszi <alex@rtfs.hu> | 2017-10-05 19:29:20 +0800 |
| commit | 18ae0c3d784cb587d50bdfc1f33e200fd97f2676 (patch) | |
| tree | 9a99925d003f200cdd8b18509c04a8cc004ae143 /libsolidity/formal | |
| parent | 6ba0c2bba85ba099b10c58d1c7d10d91e1364471 (diff) | |
| download | dexon-solidity-18ae0c3d784cb587d50bdfc1f33e200fd97f2676.tar.gz dexon-solidity-18ae0c3d784cb587d50bdfc1f33e200fd97f2676.tar.zst dexon-solidity-18ae0c3d784cb587d50bdfc1f33e200fd97f2676.zip | |
SMT enforce variable types
Diffstat (limited to 'libsolidity/formal')
| -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; }; } |