Add variable names to LP solver.

test/libsolutil/LP.cpp

@@ -23,8 +23,12 @@
 #include <libsolutil/StringUtils.h>
 #include <test/Common.h>
 
+#include <algorithm>
+
 #include <boost/test/unit_test.hpp>
 
+#include <range/v3/view/enumerate.hpp>
+
 using namespace std;
 using namespace solidity::smtutil;
 using namespace solidity::util;
@@ -41,6 +45,37 @@ public:
 		m_solvingState.variableNames.emplace_back("");
 	}
 
+	LinearExpression linearExpression(vector<int> _factors)
+	{
+		LinearExpression lexp;
+		lexp.resize(_factors.size());
+		for (auto&& [index, value]: _factors | ranges::views::enumerate)
+			lexp[index] = rational{value};
+		return lexp;
+	}
+
+	void addFuzzerInput(vector<vector<int>> _constraints)
+	{
+		size_t totalNumVariables = 0;
+		for (auto c: _constraints)
+		{
+			bool equality = static_cast<bool>(c[0]);
+			vector<int> factors(c.begin() + 1, c.end());
+			m_solvingState.constraints.push_back(
+				{
+					linearExpression(factors),
+					equality
+				}
+			);
+		    auto it = find_if(factors.rbegin(), factors.rend(), [](auto const& _i) { return _i != 0; });
+            size_t numVariablesInConstraint = factors.size() - 1 - static_cast<size_t>(distance(factors.rbegin(), it));
+			if (totalNumVariables < numVariablesInConstraint)
+				totalNumVariables = numVariablesInConstraint;
+		}
+		for (size_t i = 0; i < totalNumVariables; i++)
+			m_solvingState.variableNames.emplace_back("x" + to_string(i));
+	}
+
 	LinearExpression constant(rational _value)
 	{
 		return LinearExpression::factorForVariable(0, _value);
@@ -153,6 +188,23 @@ BOOST_AUTO_TEST_CASE(fuzzer)
 	sat();
 }
 
+BOOST_AUTO_TEST_CASE(fuzzer3)
+{
+	addFuzzerInput(
+		{
+			{1,-1,0,0,0,0,90,9},
+			{0,0,0,0,-76,0,0,74},
+			{0,0,0,0,0,31,0,0,0,0,-71},
+			{0,0,5,0,-85,60},
+			{1,0,0,-9,0,0,63,-31,-2,0,-78},
+			{0,0,50,-70,2,-76,94},
+			{1,1,0,-3,51},
+			{1,0,0,-33,0,0,0,60}
+		}
+	);
+	infeasible();
+}
+
 BOOST_AUTO_TEST_CASE(fuzzer2)
 {
 	/*

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp

@@ -48,6 +48,18 @@ void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint)
 	m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first});
 }
 
+void FuzzerSolverInterface::addLPVariable(string _varName)
+{
+	if (
+		find(
+			m_lpSolvingState.variableNames.begin(),
+			m_lpSolvingState.variableNames.end(),
+			_varName
+		) == m_lpSolvingState.variableNames.end()
+	)
+		m_lpSolvingState.variableNames.emplace_back(_varName);
+}
+
 void FuzzerSolverInterface::addZ3Constraint(pair<bool, vector<int>> _constraint)
 {
 	bool isEquality = _constraint.first;
@@ -57,6 +69,8 @@ void FuzzerSolverInterface::addZ3Constraint(pair<bool, vector<int>> _constraint)
 		if (index != 0 && value != 0)
 		{
 			string varName = "x" + to_string(index - 1);
+			// Add variable name to LP solving state to aid debugging
+			addLPVariable(varName);
 			expr var = m_z3Ctx.real_const(varName.c_str());
 			expr factor = m_z3Ctx.int_val(value);
 			reduce = reduce + var * factor;
@@ -105,9 +119,13 @@ string FuzzerSolverInterface::checkZ3Result()
 
 bool FuzzerSolverInterface::differentialCheck(vector<pair<bool, vector<int>>> _constraints)
 {
-	addLPConstraints(_constraints);
 	addZ3Constraints(_constraints);
 	string z3Result = checkZ3Result();
+	// There is no point in continuing if z3 (the quicker solver) returns
+	// unknown.
+	if (z3Result == "unknown")
+		return true;
+	addLPConstraints(_constraints);
 	string lpResult = checkLPResult();
 	bool checkFailed = ((z3Result == "infeasible") && (lpResult == "feasible")) ||
 		((z3Result == "feasible") && (lpResult == "infeasible"));

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h

@@ -75,6 +75,9 @@ private:
 	/// @returns Z3 result as string.
 	std::string z3Result(z3::check_result _result);
 
+	/// Adds variable name to LP solver solving state.
+	void addLPVariable(std::string _varName);
+
 	solidity::util::LPSolver m_lpSolver;
 	solidity::util::SolvingState m_lpSolvingState;
 	z3::context m_z3Ctx;