[SMTChecker] Supporting conditional operator

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.

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.

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;

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;

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;

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

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

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

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.

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

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.

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.

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.

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

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.

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.

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

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

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.