From 6f7f60903ed4a91363df5c7f06ce28fee1bf7599 Mon Sep 17 00:00:00 2001
From: chriseth <chris@ethereum.org>
Date: Thu, 3 Mar 2022 20:36:29 +0100
Subject: [PATCH] Hacky for loop implementation.

---
 libyul/optimiser/ReasoningBasedSimplifier.cpp | 51 +++++++++++++++++++
 libyul/optimiser/ReasoningBasedSimplifier.h   |  1 +
 2 files changed, 52 insertions(+)

diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp
index 6519b9723..c14212e16 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.cpp
+++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp
@@ -110,6 +110,57 @@ void ReasoningBasedSimplifier::operator()(If& _if)
 	m_solver->pop();
 }
 
+void ReasoningBasedSimplifier::operator()(ForLoop& _for)
+{
+	// TODO handle break / continue
+
+	if (!SideEffectsCollector{m_dialect, *_for.condition}.movable())
+		return;
+
+	cout << "Checking if condition  can be false" << endl;
+	smtutil::Expression condition = encodeExpression(*_for.condition);
+	m_solver->push();
+	m_solver->addAssertion(condition == constantValue(0));
+	cout << "  running check" << endl;
+	CheckResult result = m_solver->check({}).first;
+	m_solver->pop();
+	if (result == CheckResult::UNSATISFIABLE)
+	{
+		cout << " unsat => cannot be false!" << endl;
+		Literal trueCondition = m_dialect.trueLiteral();
+		trueCondition.debugData = debugDataOf(*_for.condition);
+		_for.condition = make_unique<yul::Expression>(move(trueCondition));
+	}
+	else
+	{
+		cout << "Checking if condition  can be true" << endl;
+		m_solver->push();
+		m_solver->addAssertion(condition != constantValue(0));
+		cout << "  running check" << endl;
+		CheckResult result2 = m_solver->check({}).first;
+		m_solver->pop();
+		if (result2 == CheckResult::UNSATISFIABLE)
+		{
+			cout << " unsat => cannot be true!" << endl;
+			Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
+			falseCondition.debugData = debugDataOf(*_for.condition);
+			_for.condition = make_unique<yul::Expression>(move(falseCondition));
+			_for.body = yul::Block{};
+			// Nothing left to be done.
+			return;
+		}
+	}
+
+	m_solver->push();
+	cout << "Setting condition true inside body" << endl;
+	m_solver->addAssertion(condition != constantValue(0));
+
+	ASTModifier::operator()(_for.body);
+	ASTModifier::operator()(_for.post);
+
+	m_solver->pop();
+}
+
 ReasoningBasedSimplifier::ReasoningBasedSimplifier(
 	Dialect const& _dialect,
 	set<YulString> const& _ssaVariables
diff --git a/libyul/optimiser/ReasoningBasedSimplifier.h b/libyul/optimiser/ReasoningBasedSimplifier.h
index c08488dbd..7c8a05256 100644
--- a/libyul/optimiser/ReasoningBasedSimplifier.h
+++ b/libyul/optimiser/ReasoningBasedSimplifier.h
@@ -57,6 +57,7 @@ public:
 	using ASTModifier::operator();
 	void operator()(VariableDeclaration& _varDecl) override;
 	void operator()(If& _if) override;
+	void operator()(ForLoop& _for) override;
 
 private:
 	explicit ReasoningBasedSimplifier(