Support models.

test/tools/ossfuzz/LPSolverFuzzer.cpp

@@ -16,6 +16,8 @@
 */
 // SPDX-License-Identifier: GPL-3.0
 
+#include <test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h>
+
 #include <cstddef>
 #include <iostream>
 #include <sstream>
@@ -23,11 +25,40 @@
 #include <string>
 #include <vector>
 
+using namespace solidity::test::fuzzer::lpsolver;
 using namespace std;
 
 // Prototype as we can't use the FuzzerInterface.h header.
 extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size);
 
+namespace
+{
+#ifdef DEBUG
+void printConstraints(vector<pair<bool, vector<int>>> _constraints)
+{
+	for (auto& i: _constraints)
+	{
+		cout << (i.first ? "=" : "<=");
+		for (auto& j: i.second)
+			cout << "," << j;
+		cout << endl;
+	}
+}
+#endif
+
+bool validConstraints(vector<pair<bool, vector<int>>> _constraints)
+{
+	// Zero input constraints is an invalid input
+	if (_constraints.size() < 1)
+		return false;
+	// Incomplete constraints are invalid
+	for (auto c: _constraints)
+		if (c.second.empty())
+			return false;
+	return true;
+}
+}
+
 extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
 {
 	// Parse CSV input
@@ -54,16 +85,26 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
 		constraints.emplace_back(constraint);
 	}
 
-	// Debug
+	if (!validConstraints(constraints))
-	for (auto& i: constraints)
+		return 0;
+	else
 	{
-		cout << (i.first ? "=" : "<=");
+		// TODO: Z3 on constraints provided by fuzzer interface and comparing its outcome
-		for (auto& j: i.second)
+		// with LP solver.
-			cout << "," << j;
+		FuzzerSolverInterface solverWithoutModels(/*supportModels=*/false);
-		cout << endl;
+		FuzzerSolverInterface solverWithModels(/*supportModels=*/true);
-	}
 
-	// TODO: Invoke LP solver and Z3 on constraints provided by fuzzer interface,
+		solverWithoutModels.addConstraints(constraints);
-	// comparing their outcomes.
+		string resultWithoutModels = solverWithoutModels.checkResult();
+		solverWithModels.addConstraints(constraints);
+		string resultWithModels = solverWithModels.checkResult();
+
+		if (resultWithoutModels != resultWithModels)
+		{
+			cout << resultWithoutModels << endl;
+			cout << resultWithModels << endl;
+			solAssert(false, "LP result without models did not match with result with models.");
+		}
 		return 0;
 	}
+}

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp

@@ -19,7 +19,8 @@ using namespace solidity::test::fuzzer::lpsolver;
 using namespace solidity::util;
 using namespace std;
 
-FuzzerSolverInterface::FuzzerSolverInterface()
+FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels):
+	m_solver(_supportModels)
 {
 	m_solvingState.variableNames.emplace_back("");
 }
@@ -53,11 +54,74 @@ void FuzzerSolverInterface::addEQConstraint(LinearExpression _lhs)
 	m_solvingState.constraints.push_back({move(_lhs), true});
 }
 
+LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
+{
+	bool first = true;
+	unsigned count = 0;
+	LinearExpression lexp;
+	for (auto f: _factors)
+	{
+		if (first)
+		{
+			first = false;
+			lexp += constant(f);
+		}
+		else
+			lexp += variable(f, "x" + to_string(count++));
+	}
+	return lexp;
+}
+
+void FuzzerSolverInterface::addEQConstraint(vector<int> _factors)
+{
+	addEQConstraint(linearExpression(_factors));
+}
+
+void FuzzerSolverInterface::addLEConstraint(vector<int> _factors)
+{
+	addLEConstraint(linearExpression(_factors));
+}
+
+void FuzzerSolverInterface::addConstraint(pair<bool, vector<int>> _constraint)
+{
+	if (_constraint.first)
+		addEQConstraint(_constraint.second);
+	else
+		addLEConstraint(_constraint.second);
+}
+
+void FuzzerSolverInterface::addConstraints(vector<pair<bool, vector<int>>> _constraints)
+{
+	for (auto c: _constraints)
+		addConstraint(c);
+}
+
 solution FuzzerSolverInterface::check()
 {
 	return m_solver.check(m_solvingState);
 }
 
+string FuzzerSolverInterface::checkResult()
+{
+	auto r = check();
+	return lpResult(r.first);
+}
+
+string FuzzerSolverInterface::lpResult(LPResult _result)
+{
+	switch (_result)
+	{
+	case LPResult::Unknown:
+		return "unknown";
+	case LPResult::Unbounded:
+		return "unbounded";
+	case LPResult::Feasible:
+		return "feasible";
+	case LPResult::Infeasible:
+		return "infeasible";
+	}
+}
+
 size_t FuzzerSolverInterface::variableIndex(string const& _name)
 {
 	if (m_solvingState.variableNames.empty())

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h

@@ -34,7 +34,7 @@ using solution = std::pair<
 class FuzzerSolverInterface
 {
 public:
-	FuzzerSolverInterface();
+	FuzzerSolverInterface(bool _supportModels);
 
 	/// @returns constant rational.
 	solidity::util::LinearExpression constant(solidity::util::rational _rationalConstant);
@@ -57,13 +57,34 @@ public:
 	/// Adds equal-to-zero constraint to solver.
 	void addEQConstraint(solidity::util::LinearExpression _lhs);
 
+	/// Adds less-than-equal constraint from vector of factors.
+	void addLEConstraint(std::vector<int> _factors);
+
+	/// Adds equal-to constraint from vector of factors.
+	void addEQConstraint(std::vector<int> _factors);
+
+	/// Adds @param _constraint to LP solver.
+	void addConstraint(std::pair<bool, std::vector<int>> _constraint);
+
+	/// Adds @param _constraints to LP solver.
+	void addConstraints(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+
+	/// @returns linear expression created from @param _factors.
+	solidity::util::LinearExpression linearExpression(std::vector<int> _factors);
+
 	/// Queries LP solver and @returns solution.
 	solution check();
 
+	/// Queries LP solver and @returns sat result as string.
+	std::string checkResult();
+
 private:
 	/// Adds variable if necessary to LP solver state and @returns index of variable.
 	size_t variableIndex(std::string const& _name);
 
+	/// @returns LP result as string.
+	std::string lpResult(solidity::util::LPResult _result);
+
 	solidity::util::LPSolver m_solver;
 	solidity::util::SolvingState m_solvingState;
 };