cerc-io/solidity
16
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

Merge pull request #239 from chriseth/why3Fix

Browse Source 
Again some why3 fixes with regards to separators in blocks.
This commit is contained in:
chriseth 2015-11-26 11:52:57 +01:00
commit b49b268600
2 changed files with 35 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
libsolidity/formal/Why3Translator.cpp
View File

@ -21,6 +21,7 @@
*/
#include <libsolidity/formal/Why3Translator.h>
#include <boost/algorithm/string/predicate.hpp>
using namespace std;
using namespace dev;
@ -30,8 +31,7 @@ bool Why3Translator::process(SourceUnit const& _source)
{
try
{
m_indentation = 0;
if (!m_result.empty())
if (m_lines.size() != 1 || !m_lines.back().contents.empty())
fatalError(_source, "Multiple source units not yet supported");
appendPreface();
_source.accept(*this);
@ -43,6 +43,14 @@ bool Why3Translator::process(SourceUnit const& _source)
return !m_errorOccured;
}
string Why3Translator::translation() const
{
string result;
for (auto const& line: m_lines)
result += string(line.indentation, '\t') + line.contents + "\n";
return result;
}
void Why3Translator::error(ASTNode const& _node, string const& _description)
{
auto err = make_shared<Error>(Error::Type::Why3TranslatorError);
@ -61,7 +69,7 @@ void Why3Translator::fatalError(ASTNode const& _node, string const& _description
void Why3Translator::appendPreface()
{
m_result += R"(
m_lines.push_back(Line{R"(
module UInt256
use import mach.int.Unsigned
type uint256
@ -70,7 +78,7 @@ module UInt256
type t = uint256,
constant max = max_uint256
end
)";
)", 0});
}
string Why3Translator::toFormalType(Type const& _type) const
@ -100,28 +108,20 @@ void Why3Translator::addLine(string const& _line)
void Why3Translator::add(string const& _str)
{
if (m_currentLine.empty())
m_indentationAtLineStart = m_indentation;
m_currentLine += _str;
m_lines.back().contents += _str;
}
void Why3Translator::newLine()
{
if (!m_currentLine.empty())
{
for (size_t i = 0; i < m_indentationAtLineStart; ++i)
m_result.push_back('\t');
m_result += m_currentLine;
m_result.push_back('\n');
m_currentLine.clear();
}
if (!m_lines.back().contents.empty())
m_lines.push_back({"", m_lines.back().indentation});
}
void Why3Translator::unindent()
{
newLine();
solAssert(m_indentation > 0, "");
m_indentation--;
solAssert(m_lines.back().indentation > 0, "");
m_lines.back().indentation--;
}
bool Why3Translator::visit(ContractDefinition const& _contract)
@ -289,8 +289,14 @@ bool Why3Translator::visit(Block const& _node)
for (size_t i = 0; i < _node.statements().size(); ++i)
{
_node.statements()[i]->accept(*this);
if (!m_currentLine.empty() && i != _node.statements().size() - 1)
add(";");
if (i != _node.statements().size() - 1)
{
auto it = m_lines.end() - 1;
while (it != m_lines.begin() && it->contents.empty())
--it;
if (!boost::algorithm::ends_with(it->contents, "begin"))
it->contents += ";";
}
newLine();
}
unindent();

17
libsolidity/formal/Why3Translator.h
View File

@ -43,13 +43,13 @@ class SourceUnit;
class Why3Translator: private ASTConstVisitor
{
public:
Why3Translator(ErrorList& _errors): m_errors(_errors) {}
Why3Translator(ErrorList& _errors): m_lines{{std::string(), 0}}, m_errors(_errors) {}
/// Appends formalisation of the given source unit to the output.
/// @returns false on error.
bool process(SourceUnit const& _source);
std::string translation() const { return m_result; }
std::string translation() const;
private:
/// Returns an error.
@ -64,11 +64,12 @@ private:
/// if the type is not supported.
std::string toFormalType(Type const& _type) const;
void indent() { newLine(); m_indentation++; }
void indent() { newLine(); m_lines.back().indentation++; }
void unindent();
void addLine(std::string const& _line);
void add(std::string const& _str);
void newLine();
void appendSemicolon();
virtual bool visit(SourceUnit const&) override { return true; }
virtual bool visit(ContractDefinition const& _contract) override;
@ -111,9 +112,6 @@ private:
/// Transforms substring like `#varName` and `#stateVarName` to code that evaluates to their value.
std::string transformVariableReferences(std::string const& _annotation);
size_t m_indentationAtLineStart = 0;
size_t m_indentation = 0;
std::string m_currentLine;
/// True if we have already seen a contract. For now, only a single contract
/// is supported.
bool m_seenContract = false;
@ -122,7 +120,12 @@ private:
std::vector<ASTPointer<VariableDeclaration>> const* m_stateVariables = nullptr;
std::map<std::string, VariableDeclaration const*> m_localVariables;
std::string m_result;
struct Line
{
std::string contents;
unsigned indentation;
};
std::vector<Line> m_lines;
ErrorList& m_errors;
};