diff --git a/Changelog.md b/Changelog.md index 043bb9e9a..f5698bf3b 100644 --- a/Changelog.md +++ b/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. diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 0071efd99..7bd0be655 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/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 rightArguments; diff --git a/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol b/test/libsolidity/smtCheckerTests/complex/slither/data_dependency.sol new file mode 100644 index 000000000..89c38a4cd --- /dev/null +++ b/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.