From d3d77e482cbd10d5228a47f077ebe8e4c60a3d90 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 21 Oct 2020 22:04:34 +0100
Subject: [PATCH] Fix ICE on conditions with tuples of rationals

---
 Changelog.md                                  |  1 +
 libsolidity/formal/SMTEncoder.cpp             |  4 ++--
 libsolidity/formal/SymbolicVariables.cpp      | 22 +++++++++++++++++--
 libsolidity/formal/SymbolicVariables.h        |  6 +++--
 .../operators/tuple_rationals_conditional.sol | 11 ++++++++++
 5 files changed, 38 insertions(+), 6 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol

diff --git a/Changelog.md b/Changelog.md
index 9c5ea16ea..f602e41d6 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
  * SMTChecker: Fix internal error on conversion from string literal to byte.
+ * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index efd712644..7efb78205 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -574,8 +574,8 @@ bool SMTEncoder::visit(Conditional const& _op)
 
 	defineExpr(_op, smtutil::Expression::ite(
 		expr(_op.condition()),
-		expr(_op.trueExpression()),
-		expr(_op.falseExpression())
+		expr(_op.trueExpression(), _op.annotation().type),
+		expr(_op.falseExpression(), _op.annotation().type)
 	));
 
 	return false;
diff --git a/libsolidity/formal/SymbolicVariables.cpp b/libsolidity/formal/SymbolicVariables.cpp
index cff0efdac..2d6eaa748 100644
--- a/libsolidity/formal/SymbolicVariables.cpp
+++ b/libsolidity/formal/SymbolicVariables.cpp
@@ -245,7 +245,25 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	solAssert(m_sort->kind == Kind::Tuple, "");
 }
 
-vector<SortPointer> const& SymbolicTupleVariable::components()
+smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	if (!_targetType || sort() == smtSort(*_targetType))
+		return SymbolicVariable::currentValue();
+
+	auto thisTuple = dynamic_pointer_cast<TupleSort>(sort());
+	auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
+	solAssert(thisTuple && otherTuple, "");
+	solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
+	vector<smtutil::Expression> args;
+	for (size_t i = 0; i < thisTuple->components.size(); ++i)
+		args.emplace_back(component(i, type(), _targetType));
+	return smtutil::Expression::tuple_constructor(
+		smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
+		args
+	);
+}
+
+vector<SortPointer> const& SymbolicTupleVariable::components() const
 {
 	auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
 	solAssert(tupleSort, "");
@@ -256,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component(
 	size_t _index,
 	TypePointer _fromType,
 	TypePointer _toType
-)
+) const
 {
 	optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
 	if (conversion)
diff --git a/libsolidity/formal/SymbolicVariables.h b/libsolidity/formal/SymbolicVariables.h
index 843043c9d..d81f770a5 100644
--- a/libsolidity/formal/SymbolicVariables.h
+++ b/libsolidity/formal/SymbolicVariables.h
@@ -225,12 +225,14 @@ public:
 		EncodingContext& _context
 	);
 
-	std::vector<smtutil::SortPointer> const& components();
+	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+
+	std::vector<smtutil::SortPointer> const& components() const;
 	smtutil::Expression component(
 		size_t _index,
 		TypePointer _fromType = nullptr,
 		TypePointer _toType = nullptr
-	);
+	) const;
 };
 
 /**
diff --git a/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol b/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol
new file mode 100644
index 000000000..cdcff3f4f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool x) public pure {
+		(uint a, uint b) = x ? (10000000001, 2) : (3, 4);
+		assert(a != 0);
+		assert(b != 0);
+		assert(a % 2 == 1);
+		assert(b % 2 == 0);
+	}
+}