From 3f97a1012af4afc3d4f88f2f2c81b88014ebd337 Mon Sep 17 00:00:00 2001
From: Djordje Mijovic <djordje.mijovic@gmail.com>
Date: Tue, 18 Aug 2020 19:25:36 +0200
Subject: [PATCH] [SMTChecker] Supporting conditional operator

---
 Changelog.md                                  |  1 +
 libsolidity/formal/BMC.cpp                    | 18 +++++++++++++
 libsolidity/formal/BMC.h                      |  1 +
 libsolidity/formal/SMTEncoder.cpp             | 21 +++++++++++++++
 libsolidity/formal/SMTEncoder.h               |  1 +
 .../operators/conditional_assignment_1.sol    | 10 +++++++
 .../operators/conditional_assignment_2.sol    | 11 ++++++++
 .../operators/conditional_assignment_3.sol    | 13 +++++++++
 .../operators/conditional_assignment_4.sol    | 25 +++++++++++++++++
 .../operators/conditional_assignment_5.sol    | 27 +++++++++++++++++++
 .../operators/conditional_assignment_6.sol    | 26 ++++++++++++++++++
 .../conditional_assignment_always_false.sol   | 11 ++++++++
 .../conditional_assignment_always_true.sol    | 12 +++++++++
 .../conditional_assignment_function_1.sol     | 13 +++++++++
 .../conditional_assignment_function_2.sol     | 19 +++++++++++++
 ...ditional_assignment_nested_always_true.sol | 11 ++++++++
 .../conditional_assignment_nested_unsafe.sol  | 10 +++++++
 .../conditional_assignment_statevar_1.sol     | 13 +++++++++
 .../types/mapping_as_local_var_1.sol          |  1 -
 19 files changed, 243 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_4.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_false.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_always_true.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol
 create mode 100644 test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol

diff --git a/Changelog.md b/Changelog.md
index 59ce52435..e90c0b6da 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
  * Standard JSON Interface: Do not run EVM bytecode code generation, if only Yul IR or EWasm output is requested.
  * Yul: Report error when using non-string literals for ``datasize()``, ``dataoffset()``, ``linkersymbol()``, ``loadimmutable()``, ``setimmutable()``.
  * Yul Optimizer: LoopInvariantCodeMotion can move reading operations outside for-loops as long as the affected area is not modified inside the loop.
+ * SMTChecker: Support conditional operator.
 
 Bugfixes:
  * Optimizer: Keep side-effects of ``x`` in ``byte(a, shr(b, x))`` even if the constants ``a`` and ``b`` would make the expression zero unconditionally. This optimizer rule is very hard if not impossible to trigger in a way that it can result in invalid code, though.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 74f814e00..568b2f326 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -198,6 +198,24 @@ bool BMC::visit(IfStatement const& _node)
 	return false;
 }
 
+bool BMC::visit(Conditional const& _op)
+{
+	m_context.pushSolver();
+	_op.condition().accept(*this);
+
+	if (isRootFunction())
+		addVerificationTarget(
+			VerificationTarget::Type::ConstantCondition,
+			expr(_op.condition()),
+			&_op.condition()
+		);
+	m_context.popSolver();
+
+	SMTEncoder::visit(_op);
+
+	return false;
+}
+
 // Here we consider the execution of two branches:
 // Branch 1 assumes the loop condition to be true and executes the loop once,
 // after resetting touched variables.
diff --git a/libsolidity/formal/BMC.h b/libsolidity/formal/BMC.h
index 324595bba..bd86d7360 100644
--- a/libsolidity/formal/BMC.h
+++ b/libsolidity/formal/BMC.h
@@ -84,6 +84,7 @@ private:
 	bool visit(FunctionDefinition const& _node) override;
 	void endVisit(FunctionDefinition const& _node) override;
 	bool visit(IfStatement const& _node) override;
+	bool visit(Conditional const& _node) override;
 	bool visit(WhileStatement const& _node) override;
 	bool visit(ForStatement const& _node) override;
 	void endVisit(UnaryOperation const& _node) override;
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index f9ae5794e..730b42bf2 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -579,6 +579,27 @@ void SMTEncoder::endVisit(BinaryOperation const& _op)
 		);
 }
 
+bool SMTEncoder::visit(Conditional const& _op)
+{
+	_op.condition().accept(*this);
+
+	auto indicesEndTrue = visitBranch(&_op.trueExpression(), expr(_op.condition()));
+	auto touchedVars = touchedVariables(_op.trueExpression());
+
+	auto indicesEndFalse = visitBranch(&_op.falseExpression(), !expr(_op.condition()));
+	touchedVars += touchedVariables(_op.falseExpression());
+
+	mergeVariables(touchedVars, expr(_op.condition()), indicesEndTrue, indicesEndFalse);
+
+	defineExpr(_op, smtutil::Expression::ite(
+		expr(_op.condition()),
+		expr(_op.trueExpression()),
+		expr(_op.falseExpression())
+	));
+
+	return false;
+}
+
 void SMTEncoder::endVisit(FunctionCall const& _funCall)
 {
 	auto functionCallKind = *_funCall.annotation().kind;
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index ec097a2c9..4eb5ce965 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -83,6 +83,7 @@ protected:
 	void endVisit(UnaryOperation const& _node) override;
 	bool visit(BinaryOperation const& _node) override;
 	void endVisit(BinaryOperation const& _node) override;
+	bool visit(Conditional const& _node) override;
 	void endVisit(FunctionCall const& _node) override;
 	bool visit(ModifierInvocation const& _node) override;
 	void endVisit(Identifier const& _node) override;
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol
new file mode 100644
index 000000000..f01fb6029
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_1.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		uint a = b ? 2 : 3;
+		assert(a > 2);
+	}
+}
+// ----
+// Warning 6328: (104-117): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol
new file mode 100644
index 000000000..99ee3c2a0
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_2.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint b) public pure {
+		require(b < 3);
+		uint c = (b > 0) ? b++ : ++b;
+		assert(c == 0);
+	}
+}
+// ----
+// Warning 6328: (132-146): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol
new file mode 100644
index 000000000..12c580e24
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_3.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint a, uint b) public pure {
+		require(a < 10);
+		require(b <= a);
+
+		uint c = (b > 4) ? a++ : b++;
+		assert(c > a);
+	}
+}
+// ----
+// Warning 6328: (161-174): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_4.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_4.sol
new file mode 100644
index 000000000..87b48e982
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_4.sol
@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+    function d() public virtual ;
+}
+
+contract C {
+    bool a;
+    uint x;
+    D d;
+    function g() public returns (uint) {
+        x = 2;
+        return x;
+    }
+    function f(bool b) public {
+        x = 1;
+        uint y = b ? g() : 3;
+        assert(x == 2 || x == 1);
+    }
+    function h() public {
+        x = 3;
+    }
+}
+// ----
+// Warning 2072: (273-279): Unused local variable.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
new file mode 100644
index 000000000..675ae3eb5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_5.sol
@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+    function d() public virtual ;
+}
+
+contract C {
+    bool a;
+    uint x;
+    D d;
+    function g() public returns (uint) {
+        x = 2;
+        d.d();
+        return x;
+    }
+    function f(bool b) public {
+        x = 1;
+        uint y = b ? g() : 3;
+        assert(x == 2 || x == 1);
+    }
+    function h() public {
+        x = 3;
+    }
+}
+// ----
+// Warning 2072: (288-294): Unused local variable.
+// Warning 6328: (318-342): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
new file mode 100644
index 000000000..d1fe62aac
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_6.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+    function d() public virtual ;
+}
+
+contract C {
+    bool a;
+    uint x;
+    D d;
+    function g() public returns (uint) {
+        x = 2;
+        d.d();
+        return x;
+    }
+    function f(bool b) public {
+        x = 1;
+        uint y = b ? g() : 3;
+        assert(x == 2 || x == 1);
+    }
+    function h() internal {
+        x = 3;
+    }
+}
+// ----
+// Warning 2072: (288-294): Unused local variable.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_false.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_false.sol
new file mode 100644
index 000000000..7958e0237
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_false.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(uint b) public pure returns (uint d) {
+		require(b < 10);
+		uint c = b < 5 ? 5 : 1;
+		d = c > 5 ? 3 : 2;
+	}
+}
+// ----
+// Warning 6838: (148-153): Condition is always false.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol
new file mode 100644
index 000000000..705ca9c2b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_always_true.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool b) public pure {
+		require(b);
+		uint c = b ? 5 : 1;
+		assert(c < 5);
+	}
+}
+// ----
+// Warning 6328: (118-131): Assertion violation happens here
+// Warning 6838: (105-106): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol
new file mode 100644
index 000000000..890db61ca
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint a) internal pure returns (bool b) {
+        b = a > 5;
+    }
+    function g(uint a) public pure {
+        uint c = f(a) ? 3 : 4;
+        assert(c > 5);
+    }
+}
+// ----
+// Warning 6328: (203-216): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_2.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_2.sol
new file mode 100644
index 000000000..a934a273c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_function_2.sol
@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(uint a) internal pure returns (uint b) {
+        require(a < 1000);
+        return a * a;
+    }
+    function g(uint a) internal pure returns (uint b) {
+        require(a < 1000);
+        return a + 100;
+    }
+    function h(uint a) public pure {
+        uint c = a < 5 ? g(a) : f(a);
+        assert(c >= 25);
+        assert(c < 20);
+    }
+}
+// ----
+// Warning 6328: (378-392): Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_always_true.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_always_true.sol
new file mode 100644
index 000000000..cd85df0c4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_always_true.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(bool b1, bool b2) public pure {
+        require(b1 || b2);
+        uint c = b1 ? 3 : (b2 ? 2 : 1);
+        assert(c > 1);
+    }
+}
+// ----
+// Warning 6838: (147-149): Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol
new file mode 100644
index 000000000..0dabdf0f6
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_nested_unsafe.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+    function f(bool b1, bool b2) public pure {
+        uint c = b1 ? 3 : (b2 ? 2 : 1);
+        assert(c > 1);
+    }
+}
+// ----
+// Warning 6328: (141-154): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol
new file mode 100644
index 000000000..07cf3fef4
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+    uint a;
+    bool b;
+
+    function f() public returns(uint c) {
+        c = b ? a + 1 : a--;
+        assert(c > a);
+    }
+}
+// ----
+// Warning 2661: (129-134): Overflow (resulting value larger than 2**256 - 1) happens here
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol b/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
index ec8c795a5..e99eea071 100644
--- a/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
+++ b/test/libsolidity/smtCheckerTests/types/mapping_as_local_var_1.sol
@@ -18,4 +18,3 @@ contract c {
 // ----
 // Warning 6328: (288-324): Assertion violation happens here
 // Warning 6328: (336-372): Assertion violation happens here
-// Warning 6031: (166-178): Internal error: Expression undefined for SMT solver.