Basic support to free constants

libsolidity/formal/BMC.cpp

@@ -61,8 +61,6 @@ BMC::BMC(
 
 void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<VerificationTargetType>> _solvedTargets)
 {
-	/// This is currently used to abort analysis of SourceUnits
-	/// containing file level functions or constants.
 	if (SMTEncoder::analyze(_source))
 	{
 		m_solvedTargets = move(_solvedTargets);
@@ -70,6 +68,7 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 		m_context.clear();
 		m_context.setAssertionAccumulation(true);
 		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+		createFreeConstants(sourceDependencies(_source));
 
 		_source.accept(*this);
 	}

libsolidity/formal/CHC.cpp

@@ -76,17 +76,13 @@ CHC::CHC(
 
 void CHC::analyze(SourceUnit const& _source)
 {
-	/// This is currently used to abort analysis of SourceUnits
-	/// containing file level functions or constants.
 	if (SMTEncoder::analyze(_source))
 	{
 		resetSourceAnalysis();
 
-		set<SourceUnit const*, ASTNode::CompareByID> sources;
+		auto sources = sourceDependencies(_source);
-		sources.insert(&_source);
-		for (auto const& source: _source.referencedSourceUnits(true))
-			sources.insert(source);
 		collectFreeFunctions(sources);
+		createFreeConstants(sources);
 		for (auto const* source: sources)
 			defineInterfacesAndSummaries(*source);
 		for (auto const* source: sources)
@@ -1422,7 +1418,8 @@ void CHC::verificationTargetEncountered(
 	if (!m_settings.targets.has(_type))
 		return;
 
-	solAssert(m_currentContract || m_currentFunction, "");
+	if (!(m_currentContract || m_currentFunction))
+		return;
 
 	bool scopeIsFunction = m_currentFunction && !m_currentFunction->isConstructor();
 	auto errorId = newErrorId();

libsolidity/formal/SMTEncoder.cpp

@@ -51,27 +51,6 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 
 bool SMTEncoder::analyze(SourceUnit const& _source)
 {
-	set<SourceUnit const*, smt::EncodingContext::IdCompare> sources;
-	sources.insert(&_source);
-	for (auto const& source: _source.referencedSourceUnits(true))
-		sources.insert(source);
-
-	bool analysis = true;
-	for (auto source: sources)
-		for (auto node: source->nodes())
-			if (auto var = dynamic_pointer_cast<VariableDeclaration>(node))
-			{
-				m_errorReporter.warning(
-					8195_error,
-					var->location(),
-					"Model checker analysis was not possible because file level constants are not supported."
-				);
-				analysis = false;
-			}
-
-	if (!analysis)
-		return false;
-
 	state().prepareForSourceUnit(_source);
 
 	return true;
@@ -437,14 +416,9 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
 		auto values = applyMap(_tuple.components(), [this](auto const& component) -> optional<smtutil::Expression> {
 			if (component)
 			{
-				if (auto varDecl = identifierToVariable(*component))
+				if (!m_context.knownExpression(*component))
-					return currentValue(*varDecl);
-				else
-				{
-					if (!m_context.knownExpression(*component))
 						createExpr(*component);
-					return expr(*component);
+				return expr(*component);
-				}
 			}
 			return {};
 		});
@@ -1395,6 +1369,9 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
+
+		if (varDecl && varDecl->isConstant())
+			m_context.addAssertion(currentValue(*varDecl) == expr(*id));
 	}
 	else
 	{
@@ -2599,6 +2576,7 @@ VariableDeclaration const* SMTEncoder::identifierToVariable(Expression const& _e
 				solAssert(m_context.knownVariable(*varDecl), "");
 				return varDecl;
 			}
+
 	return nullptr;
 }
 
@@ -2913,6 +2891,15 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 	return ABIFunctions(_node).abiCalls;
 }
 
+set<SourceUnit const*, ASTNode::CompareByID> SMTEncoder::sourceDependencies(SourceUnit const& _source)
+{
+	set<SourceUnit const*, ASTNode::CompareByID> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+	return sources;
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
 	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
@@ -2978,6 +2965,14 @@ void SMTEncoder::collectFreeFunctions(set<SourceUnit const*, ASTNode::CompareByI
 			}
 }
 
+void SMTEncoder::createFreeConstants(set<SourceUnit const*, ASTNode::CompareByID> const& _sources)
+{
+	for (auto source: _sources)
+		for (auto node: source->nodes())
+			if (auto var = dynamic_cast<VariableDeclaration const*>(node.get()))
+				createVariable(*var);
+}
+
 smt::SymbolicState& SMTEncoder::state()
 {
 	return m_context.state();

libsolidity/formal/SMTEncoder.h

@@ -112,6 +112,10 @@ public:
 
 	static std::set<FunctionCall const*> collectABICalls(ASTNode const* _node);
 
+	/// @returns all the sources that @param _source depends on,
+	/// including itself.
+	static std::set<SourceUnit const*, ASTNode::CompareByID> sourceDependencies(SourceUnit const& _source);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined
@@ -373,6 +377,8 @@ protected:
 	/// and internal library functions in m_freeFunctions.
 	void collectFreeFunctions(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
 	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& allFreeFunctions() const { return m_freeFunctions; }
+	/// Create symbolic variables for the free constants in all @param _sources.
+	void createFreeConstants(std::set<SourceUnit const*, ASTNode::CompareByID> const& _sources);
 
 	/// @returns a note to be added to warnings.
 	std::string extraComment();

test/libsolidity/smtCheckerTests/file_level/free_constant_1.sol

@@ -7,5 +7,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.
+// Warning 4984: (125-130): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\n\nx = 115792089237316195423570985008687907853269984665640564039457584007913129639894\n = 0\n\nTransaction trace:\nC.constructor()\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129639894)
-// Warning 8195: (0-20): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_constant_2.sol

@@ -10,10 +10,4 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 2018: (188-278): Function state mutability can be restricted to pure
+// Warning 2018: (220-310): Function state mutability can be restricted to pure
-// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (0-23): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (79-133): Model checker analysis was not possible because file level constants are not supported.
-// Warning 8195: (135-172): Model checker analysis was not possible because file level constants are not supported.

test/libsolidity/smtCheckerTests/file_level/free_function_and_constant_1.sol

@@ -12,5 +12,6 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.
+// Warning 4984: (222-234): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    ::fun(_x, []) -- internal call
-// Warning 8195: (32-52): Model checker analysis was not possible because file level constants are not supported.
+// Warning 4984: (222-238): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 115792089237316195423570985008687907853269984665640564039457584007913129632175\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(115792089237316195423570985008687907853269984665640564039457584007913129632175, input)\n    ::fun(_x, []) -- internal call
+// Warning 6368: (347-352): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 14, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call