From a73ec6a82f1da9f5cfa9ea1033a73ac78a9b0580 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 28 May 2020 12:17:53 +0200 Subject: [PATCH 1/2] [SMTChecker] Fix ICE in inlining function calls while short circuiting --- Changelog.md | 1 + libsolidity/formal/SMTEncoder.cpp | 1 - libsolidity/formal/VariableUsage.cpp | 3 ++- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/Changelog.md b/Changelog.md index 9006ac777..992436ea3 100644 --- a/Changelog.md +++ b/Changelog.md @@ -25,6 +25,7 @@ Bugfixes: * Scanner: Fix bug when two empty NatSpec comments lead to scanning past EOL. * Code Generator: Trigger proper unimplemented errors on certain array copy operations. * SMTChecker: Fix internal error when applying arithmetic operators to fixed point variables. + * SMTChecker: Fix internal error when short circuiting Boolean expressions with function calls in state variable initialization. ### 0.6.8 (2020-05-14) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index fd1acb66f..be9bea10f 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -1791,7 +1791,6 @@ Expression const* SMTEncoder::leftmostBase(IndexAccess const& _indexAccess) set SMTEncoder::touchedVariables(ASTNode const& _node) { - solAssert(!m_callStack.empty(), ""); vector callStack; for (auto const& call: m_callStack) callStack.push_back(call.first); diff --git a/libsolidity/formal/VariableUsage.cpp b/libsolidity/formal/VariableUsage.cpp index 1871c0908..acfd34909 100644 --- a/libsolidity/formal/VariableUsage.cpp +++ b/libsolidity/formal/VariableUsage.cpp @@ -33,7 +33,8 @@ set VariableUsage::touchedVariables(ASTNode const& _ m_touchedVariables.clear(); m_callStack.clear(); m_callStack += _outerCallstack; - m_lastCall = m_callStack.back(); + if (!m_callStack.empty()) + m_lastCall = m_callStack.back(); _node.accept(*this); return m_touchedVariables; } From ec766958eace1acdb36abfce888f7d539b49c72c Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 28 May 2020 12:40:08 +0200 Subject: [PATCH 2/2] Add test --- .../functions/internal_call_state_var_init.sol | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init.sol diff --git a/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init.sol b/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init.sol new file mode 100644 index 000000000..8f6276e0e --- /dev/null +++ b/test/libsolidity/smtCheckerTests/functions/internal_call_state_var_init.sol @@ -0,0 +1,5 @@ +pragma experimental SMTChecker; +contract c { + bool b = (f() == 0) && (f() == 0); + function f() internal returns (uint) {} +}