From 484e67815af9f9679e6e8d8cc1abb28323957c74 Mon Sep 17 00:00:00 2001 From: Martin Blicha Date: Mon, 18 Jan 2021 10:37:09 +0100 Subject: [PATCH] [SMTChecker] Basic support for inline assembly using over-approximating analysis --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 55 ++++++++++++++++++- libsolidity/formal/SMTEncoder.h | 2 + .../inline_assembly/assembly_1.sol | 24 ++++++++ .../inline_assembly/assembly_2.sol | 16 ++++++ .../inline_assembly/assembly_3.sol | 16 ++++++ .../inline_assembly/assembly_4.sol | 16 ++++++ .../inline_assembly/assembly_5.sol | 26 +++++++++ .../inline_assembly/assembly_6.sol | 25 +++++++++ ...y_local_storage_access_inside_function.sol | 24 ++++++++ .../assembly_local_storage_pointer.sol | 25 +++++++++ .../inline_assembly/assembly_memory_write.sol | 28 ++++++++++ .../smtCheckerTests/inline_assembly/empty.sol | 4 +- .../inline_assembly/local_var.sol | 4 +- 14 files changed, 261 insertions(+), 5 deletions(-) create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_1.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol create mode 100644 test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol diff --git a/Changelog.md b/Changelog.md index 9b4826386..49ef544d8 100644 --- a/Changelog.md +++ b/Changelog.md @@ -24,6 +24,7 @@ Bugfixes: * Code Generator: Fix length check when decoding malformed error data in catch clause. * Control Flow Graph: Fix missing error caused by read from/write to uninitialized variables. * SMTChecker: Fix false negatives in overriding modifiers and functions. + * SMTChecker: Fix false negatives in the presence of inline assembly. * SMTChecker: Fix false negatives when analyzing external function calls. * SMTChecker: Fix internal error on ``block.chainid``. * SMTChecker: Fix internal error on pushing string literal to ``bytes`` array. diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 27c60f910..a931c6c17 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -24,6 +24,9 @@ #include +#include +#include + #include #include @@ -304,10 +307,46 @@ void SMTEncoder::endVisit(Block const& _block) bool SMTEncoder::visit(InlineAssembly const& _inlineAsm) { + /// This is very similar to `yul::Assignments`, except I need to collect `Identifier`s and not just names as `YulString`s. + struct AssignedExternalsCollector: public yul::ASTWalker + { + AssignedExternalsCollector(InlineAssembly const& _inlineAsm): externalReferences(_inlineAsm.annotation().externalReferences) + { + this->operator()(_inlineAsm.operations()); + } + + map const& externalReferences; + set assignedVars; + + using yul::ASTWalker::operator(); + void operator()(yul::Assignment const& _assignment) + { + auto const& vars = _assignment.variableNames; + for (auto const& identifier: vars) + if (auto externalInfo = valueOrNullptr(externalReferences, &identifier)) + if (auto varDecl = dynamic_cast(externalInfo->declaration)) + assignedVars.insert(varDecl); + } + }; + + yul::SideEffectsCollector sideEffectsCollector(_inlineAsm.dialect(), _inlineAsm.operations()); + if (sideEffectsCollector.invalidatesMemory()) + resetMemoryVariables(); + if (sideEffectsCollector.invalidatesStorage()) + resetStorageVariables(); + + auto assignedVars = AssignedExternalsCollector(_inlineAsm).assignedVars; + for (auto const* var: assignedVars) + { + solAssert(var, ""); + solAssert(var->isLocalVariable(), "Non-local variable assigned in inlined assembly"); + m_context.resetVariable(*var); + } + m_errorReporter.warning( 7737_error, _inlineAsm.location(), - "Assertion checker does not support inline assembly." + "Inline assembly may cause SMTChecker to produce spurious warnings (false positives)." ); return false; } @@ -2256,6 +2295,20 @@ void SMTEncoder::resetStateVariables() m_context.resetVariables([&](VariableDeclaration const& _variable) { return _variable.isStateVariable(); }); } +void SMTEncoder::resetMemoryVariables() +{ + m_context.resetVariables([&](VariableDeclaration const& _variable) { + return _variable.referenceLocation() == VariableDeclaration::Location::Memory; + }); +} + +void SMTEncoder::resetStorageVariables() +{ + m_context.resetVariables([&](VariableDeclaration const& _variable) { + return _variable.referenceLocation() == VariableDeclaration::Location::Storage || _variable.isStateVariable(); + }); +} + void SMTEncoder::resetReferences(VariableDeclaration const& _varDecl) { m_context.resetVariables([&](VariableDeclaration const& _var) { diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h index 93675637b..728c38663 100644 --- a/libsolidity/formal/SMTEncoder.h +++ b/libsolidity/formal/SMTEncoder.h @@ -260,6 +260,8 @@ protected: void initializeLocalVariables(FunctionDefinition const& _function); void initializeFunctionCallParameters(CallableDeclaration const& _function, std::vector const& _callArgs); void resetStateVariables(); + void resetStorageVariables(); + void resetMemoryVariables(); /// Resets all references/pointers that have the same type or have /// a subexpression of the same type as _varDecl. void resetReferences(VariableDeclaration const& _varDecl); diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_1.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_1.sol new file mode 100644 index 000000000..f8473ff40 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_1.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C { + function f() internal pure returns (bool) { + bool b; + assembly { b := 1 } // This assignment is overapproximated at the moment, we don't know value of b after the assembly block + return b; + } + function g() public pure { + assert(f()); // False positive currently + assert(!f()); // should fail, now because of overapproximation in the analysis + require(f()); // BMC constant value not detected at the moment + require(!f()); // BMC constant value not ddetected at the moment + } +} +// ---- +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (272-283): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call +// Warning 6328: (315-327): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n C.f() -- internal call\n C.f() -- internal call +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (103-122): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol new file mode 100644 index 000000000..60c4a7e0c --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_2.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure returns (bool) { + bool b; + int x = 42; + assembly { b := 1 } + assert(x == 42); // should hold + assert(b); // should hold, but fails due to overapproximation + return b; + } +} +// ---- +// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (171-180): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol new file mode 100644 index 000000000..37a616b67 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_3.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure returns (bool) { + bool b; + bool c = true; + assembly { b := c } + assert(c); // should hold, c is not assigned in the assembly + assert(b); // should hold, but fails currently because of overapproximation + return b; + } +} +// ---- +// Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (236-245): CHC: Assertion violation happens here.\nCounterexample:\n\n = false\n\nTransaction trace:\nC.constructor()\nC.f() +// Warning 7737: (139-158): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol new file mode 100644 index 000000000..81bc9c27e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_4.sol @@ -0,0 +1,16 @@ +pragma experimental SMTChecker; + +contract C { + function f() public pure returns (bool) { + bool b; + int x = 42; + assembly { b := 1 } + b = true; + assert(x == 42); // should hold + assert(b); // should hold + return b; + } +} +// ---- +// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (115-134): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol new file mode 100644 index 000000000..e3fec75db --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_5.sol @@ -0,0 +1,26 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + } + + S s; + + function f() public { + s.x = 42; + S memory sm = s; + assert(sm.x == 42); // should hold + uint256 i = 7; + assembly { + mstore(sm, i) + } + sm.x = 10; + assert(sm.x == 10); // should hold + assert(s.x == 42); // should hold, storage not changed by the assembly + assert(i == 7); // should hold, not changed by the assembly + } +} +// ---- +// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol new file mode 100644 index 000000000..9222f6e22 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_6.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + } + + S s; + + function f() public { + s.x = 42; + S storage sm = s; + assert(sm.x == 42); // should hold + uint256 i = 7; + assembly { + sstore(sm.slot, i) + } + sm.x = 10; + assert(sm.x == 10); // should hold + assert(i == 7); // should hold, not changed by the assembly + } +} +// ---- +// Warning 7737: (190-226): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (190-226): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol new file mode 100644 index 000000000..69a1b2a3a --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_access_inside_function.sol @@ -0,0 +1,24 @@ +pragma experimental SMTChecker; + +contract C { + uint256 public z; + + function f() public { + z = 42; + uint i = 32; + assembly { + function f() { + sstore(z.slot, 7) + } + f() + } + assert(z == 42); // should fail + assert(z == 7); // should hold, but the analysis cannot know this yet + assert(i == 32); // should hold, not changed by the assembly + } +} +// ---- +// Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (185-200): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() +// Warning 6328: (219-233): CHC: Assertion violation happens here.\nCounterexample:\nz = 0\n\nTransaction trace:\nC.constructor()\nState: z = 0\nC.f() +// Warning 7737: (116-182): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol new file mode 100644 index 000000000..dc340c451 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_local_storage_pointer.sol @@ -0,0 +1,25 @@ +pragma experimental SMTChecker; + +contract C { + uint256[] public a; + + function f() public { + require(a.length == 0); + uint256[] storage x = a; + assert(x.length == 0); // should hold + uint256 i = 7; + assembly { + sstore(x.slot, 7) + } + assert(x.length == 0); // should fail + assert(x.length == 7); // should hold, but the analysis cannot know this yet + assert(i == 7); // should hold, not changed by the assembly + } +} +// ==== +// SMTIgnoreCex: yes +// ---- +// Warning 7737: (203-238): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (241-262): CHC: Assertion violation happens here. +// Warning 6328: (281-302): CHC: Assertion violation happens here. +// Warning 7737: (203-238): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol new file mode 100644 index 000000000..8467b5084 --- /dev/null +++ b/test/libsolidity/smtCheckerTests/inline_assembly/assembly_memory_write.sol @@ -0,0 +1,28 @@ +pragma experimental SMTChecker; + +contract C { + struct S { + uint x; + } + + S s; + + function f() public { + s.x = 42; + S memory sm = s; + assert(sm.x == 42); // should hold + uint256 i = 7; + assembly { + mstore(sm, i) + } + assert(sm.x == 42); // should fail + assert(sm.x == 7); // should hold, but the analysis cannot know this yet + assert(s.x == 42); // should hold, storage not changed by the assembly + assert(i == 7); // should hold, not changed by the assembly + } +} +// ---- +// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 6328: (223-241): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f() +// Warning 6328: (260-277): CHC: Assertion violation happens here.\nCounterexample:\ns = {x: 42}\n\nTransaction trace:\nC.constructor()\nState: s = {x: 0}\nC.f() +// Warning 7737: (189-220): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol index 0996e82ba..0377e326c 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/empty.sol @@ -8,5 +8,5 @@ contract C } } // ---- -// Warning 7737: (76-90): Assertion checker does not support inline assembly. -// Warning 7737: (76-90): Assertion checker does not support inline assembly. +// Warning 7737: (76-90): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (76-90): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). diff --git a/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol index a1e3cfff3..297031d4a 100644 --- a/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol +++ b/test/libsolidity/smtCheckerTests/inline_assembly/local_var.sol @@ -10,5 +10,5 @@ contract C } } // ---- -// Warning 7737: (97-121): Assertion checker does not support inline assembly. -// Warning 7737: (97-121): Assertion checker does not support inline assembly. +// Warning 7737: (97-121): Inline assembly may cause SMTChecker to produce spurious warnings (false positives). +// Warning 7737: (97-121): Inline assembly may cause SMTChecker to produce spurious warnings (false positives).