Add gasleft constraint and use full member access name

libsolidity/formal/SMTChecker.cpp

@@ -399,16 +399,21 @@ void SMTChecker::visitRequire(FunctionCall const& _funCall)
 
 void SMTChecker::visitGasLeft(FunctionCall const& _funCall)
 {
-	string gasLeft = "gasleft";
+	string gasLeft = "gasleft()";
 	// We increase the variable index since gasleft changes
 	// inside a tx.
 	defineSpecialVariable(gasLeft, _funCall, true);
-	m_specialVariables.at(gasLeft)->setUnknownValue();
+	auto const& symbolicVar = m_specialVariables.at(gasLeft);
+	unsigned index = symbolicVar->index();
+	// We set the current value to unknown anyway to add type constraints.
+	symbolicVar->setUnknownValue();
+	if (index > 0)
+		m_interface->addAssertion(symbolicVar->currentValue() <= symbolicVar->valueAtIndex(index - 1));
 }
 
 void SMTChecker::visitBlockHash(FunctionCall const& _funCall)
 {
-	string blockHash = "blockhash";
+	string blockHash = "blockhash()";
 	// TODO Define blockhash as an uninterpreted function
 	defineSpecialVariable(blockHash, _funCall);
 }
@@ -480,11 +485,12 @@ void SMTChecker::endVisit(Identifier const& _identifier)
 	}
 	else if (FunctionType const* fun = dynamic_cast<FunctionType const*>(_identifier.annotation().type.get()))
 	{
-		if (fun->kind() == FunctionType::Kind::Assert ||
+		if (
+			fun->kind() == FunctionType::Kind::Assert ||
 			fun->kind() == FunctionType::Kind::Require ||
 			fun->kind() == FunctionType::Kind::GasLeft ||
 			fun->kind() == FunctionType::Kind::BlockHash
-			)
+		)
 			return;
 		createExpr(_identifier);
 	}
@@ -541,7 +547,16 @@ bool SMTChecker::visit(MemberAccess const& _memberAccess)
 	solAssert(exprType, "");
 	if (exprType->category() == Type::Category::Magic)
 	{
-		defineSpecialVariable(_memberAccess.memberName(), _memberAccess);
+		auto identifier = dynamic_cast<Identifier const*>(&_memberAccess.expression());
+		string accessedName;
+		if (identifier)
+			accessedName = identifier->name();
+		else
+			m_errorReporter.warning(
+				_memberAccess.location(),
+				"Assertion checker does not yet support this expression."
+			);
+		defineSpecialVariable(accessedName + "." + _memberAccess.memberName(), _memberAccess);
 		return false;
 	}
 	else

libsolidity/formal/SSAVariable.cpp

@@ -28,6 +28,6 @@ SSAVariable::SSAVariable()
 void SSAVariable::resetIndex()
 {
 	m_currentIndex = 0;
-	m_nextFreeIndex.reset (new int);
+	m_nextFreeIndex.reset (new unsigned);
 	*m_nextFreeIndex = 1;
 }

libsolidity/formal/SSAVariable.h

@@ -34,19 +34,19 @@ public:
 	void resetIndex();
 
 	/// This function returns the current index of this SSA variable.
-	int index() const { return m_currentIndex; }
+	unsigned index() const { return m_currentIndex; }
-	int& index() { return m_currentIndex; }
+	unsigned& index() { return m_currentIndex; }
 
-	int operator++()
+	unsigned operator++()
 	{
 		return m_currentIndex = (*m_nextFreeIndex)++;
 	}
 
 private:
-	int m_currentIndex;
+	unsigned m_currentIndex;
 	/// The next free index is a shared pointer because we want
 	/// the copy and the copied to share it.
-	std::shared_ptr<int> m_nextFreeIndex;
+	std::shared_ptr<unsigned> m_nextFreeIndex;
 };
 
 }

libsolidity/formal/SymbolicVariable.cpp

@@ -35,7 +35,7 @@ SymbolicVariable::SymbolicVariable(
 {
 }
 
-string SymbolicVariable::uniqueSymbol(int _index) const
+string SymbolicVariable::uniqueSymbol(unsigned _index) const
 {
 	return m_uniqueName + "_" + to_string(_index);
 }

libsolidity/formal/SymbolicVariable.h

@@ -59,8 +59,8 @@ public:
 		return currentValue();
 	}
 
-	int index() const { return m_ssa->index(); }
+	unsigned index() const { return m_ssa->index(); }
-	int& index() { return m_ssa->index(); }
+	unsigned& index() { return m_ssa->index(); }
 
 	/// Sets the var to the default value of its type.
 	/// Inherited types must implement.
@@ -70,7 +70,7 @@ public:
 	virtual void setUnknownValue() {}
 
 protected:
-	std::string uniqueSymbol(int _index) const;
+	std::string uniqueSymbol(unsigned _index) const;
 
 	TypePointer m_type = nullptr;
 	std::string m_uniqueName;

test/libsolidity/smtCheckerTests/special/difficulty.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint difficulty) public view {
+		assert(block.difficulty == difficulty);
+	}
+}
+// ----
+// Warning: (91-129): Assertion violation happens here

test/libsolidity/smtCheckerTests/special/gasleft.sol

@@ -4,7 +4,11 @@ contract C
 {
 	function f() public view {
 		assert(gasleft() > 0);
+		uint g = gasleft();
+		assert(g < gasleft());
+		assert(g >= gasleft());
 	}
 }
 // ----
 // Warning: (76-97): Assertion violation happens here
+// Warning: (123-144): Assertion violation happens here