aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal')
-rw-r--r--libsolidity/formal/Why3Translator.cpp43
-rw-r--r--libsolidity/formal/Why3Translator.h17
2 files changed, 34 insertions, 26 deletions
diff --git a/libsolidity/formal/Why3Translator.cpp b/libsolidity/formal/Why3Translator.cpp
index 356a336c..c2022837 100644
--- a/libsolidity/formal/Why3Translator.cpp
+++ b/libsolidity/formal/Why3Translator.cpp
@@ -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,13 @@ 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();
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h
index 21dafa3c..34c6c34f 100644
--- a/libsolidity/formal/Why3Translator.h
+++ b/libsolidity/formal/Why3Translator.h
@@ -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;
};