Merge pull request #6702 from ethereum/smt_fix_asgn_unsupported_type

[SMTChecker] Fix unsupported type assignment

Changelog.md

@@ -14,6 +14,7 @@ Bugfixes:
  * SMTChecker: Fix bad cast in base constructor modifier.
  * SMTChecker: Fix internal error when visiting state variable inherited from base class.
  * SMTChecker: Fix internal error in fixed point operations.
+ * SMTChecker: Fix internal error in assignment to unsupported type.
 
 
 

libsolidity/formal/SMTChecker.cpp

@@ -377,10 +377,15 @@ void SMTChecker::endVisit(Assignment const& _assignment)
 			"Assertion checker does not yet implement this assignment operator."
 		);
 	else if (!isSupportedType(_assignment.annotation().type->category()))
+	{
 		m_errorReporter.warning(
 			_assignment.location(),
 			"Assertion checker does not yet implement type " + _assignment.annotation().type->toString()
 		);
+		// Give it a new index anyway to keep the SSA scheme sound.
+		if (auto varDecl = identifierToVariable(_assignment.leftHandSide()))
+			newValue(*varDecl);
+	}
 	else
 	{
 		vector<smt::Expression> rightArguments;

test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol

@@ -0,0 +1,136 @@
+pragma experimental SMTChecker;
+contract Simple{
+
+    address destination;
+    address source;
+
+    function set(address source_taint) public{
+        destination = source_taint;
+    }
+
+    function set2() public{
+        destination = source;
+    }
+}
+
+contract Reference{
+
+    struct St{
+        uint val;
+    }
+
+    St destination;
+    St source;
+    St destination_indirect_1;
+    St destination_indirect_2;
+
+    function set(uint source_taint) public{
+        destination.val = source_taint;
+    }
+
+    function set2() public{
+        destination.val = source.val;
+    }
+
+    function set3(uint source_taint) public{
+        St storage ref = destination_indirect_1;
+        if(true){
+            ref = destination_indirect_2;
+        }
+        ref.val = source_taint;
+    }
+}
+
+contract SolidityVar{
+
+    address addr_1;
+    address addr_2;
+
+    constructor() public{
+        addr_1 = msg.sender;
+    }
+
+}
+
+contract Intermediate{
+
+    uint destination;
+    uint source_intermediate;
+    uint source;
+
+    function f() public{
+        destination = source_intermediate;
+    }
+    function f2() public{
+        source_intermediate = source;
+    }
+
+}
+
+
+contract Base{
+
+    uint destination;
+    uint source_intermediate;
+    uint source;
+
+    function f() public{
+        destination = source_intermediate;
+    }
+}
+contract Derived is Base{
+
+    function f2() public{
+        source_intermediate = source;
+    }
+
+
+}
+
+
+contract PropagateThroughArguments {
+    uint var_tainted;
+    uint var_not_tainted;
+    uint var_dependant;
+
+    function f(uint user_input) public {
+        f2(user_input, 4);
+        var_dependant = var_tainted;
+    }
+
+    function f2(uint x, uint y) internal {
+        var_tainted = x;
+        var_not_tainted = y;
+    }
+}
+
+contract PropagateThroughReturnValue {
+  uint var_dependant;
+  uint var_state;
+
+  function foo() public {
+    var_dependant = bar();
+  }
+
+  function bar() internal returns (uint) {
+    return (var_state);
+  }
+}
+// ----
+// Warning: (1886-1954): Function state mutability can be restricted to view
+// Warning: (318-332): Assertion checker does not yet support the type of this variable.
+// Warning: (338-347): Assertion checker does not yet support the type of this variable.
+// Warning: (353-378): Assertion checker does not yet support the type of this variable.
+// Warning: (384-409): Assertion checker does not yet support the type of this variable.
+// Warning: (464-479): Assertion checker does not yet support this expression.
+// Warning: (464-494): Assertion checker does not yet implement such assignments.
+// Warning: (539-554): Assertion checker does not yet support this expression.
+// Warning: (557-567): Assertion checker does not yet support this expression.
+// Warning: (539-567): Assertion checker does not yet implement such assignments.
+// Warning: (629-643): Assertion checker does not yet support the type of this variable.
+// Warning: (646-668): Internal error: Expression undefined for SMT solver.
+// Warning: (646-668): Assertion checker does not yet implement this type.
+// Warning: (700-728): Assertion checker does not yet implement type struct Reference.St storage pointer
+// Warning: (748-755): Assertion checker does not yet support this expression.
+// Warning: (748-770): Assertion checker does not yet implement such assignments.
+// Warning: (849-905): Assertion checker does not yet support constructors.