Differentially fuzz against z3.

test/tools/ossfuzz/CMakeLists.txt

@@ -28,7 +28,7 @@ if (OSSFUZZ)
         LPSolverFuzzer.cpp
         LPSolverCustomMutatorInterface.cpp
     )
-    target_link_libraries(lpsolver_ossfuzz PRIVATE solutil lpsolvergen)
+    target_link_libraries(lpsolver_ossfuzz PRIVATE solutil lpsolvergen z3)
     set_target_properties(lpsolver_ossfuzz PROPERTIES LINK_FLAGS ${LIB_FUZZING_ENGINE})
 
     add_executable(solc_ossfuzz

test/tools/ossfuzz/LPSolverFuzzer.cpp

@@ -113,21 +113,12 @@ extern "C" int LLVMFuzzerTestOneInput(uint8_t const* _data, size_t _size)
 		auto constraints = parseConstraints(input);
 		if (constraints.has_value())
 		{
-			// TODO: Z3 on constraints provided by fuzzer interface and comparing its outcome
-			// with LP solver.
-			FuzzerSolverInterface solverWithoutModels(/*supportModels=*/false);
 			FuzzerSolverInterface solverWithModels(/*supportModels=*/true);
-
+			if (!solverWithModels.differentialCheck(constraints.value()))
-			solverWithoutModels.addConstraints(constraints.value());
-			string resultWithoutModels = solverWithoutModels.checkResult();
-			solverWithModels.addConstraints(constraints.value());
-			string resultWithModels = solverWithModels.checkResult();
-
-			if (resultWithoutModels != resultWithModels)
 			{
-				cout << resultWithoutModels << endl;
+				cout << solverWithModels.m_lpResult << endl;
-				cout << resultWithModels << endl;
+				cout << solverWithModels.m_z3Result << endl;
-				solAssert(false, "LP result without models did not match with result with models.");
+				solAssert(false, "LP result did not match with z3 result.");
 			}
 		}
 	}

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.cpp

@@ -17,14 +17,21 @@
 
 #include <range/v3/view/enumerate.hpp>
 
+#include <set>
+
 using namespace solidity::test::fuzzer::lpsolver;
 using namespace solidity::util;
 using namespace std;
+using namespace z3;
 
 FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels):
-	m_solver(_supportModels)
+	m_lpSolver(_supportModels),
+	m_z3Solver(m_z3Ctx)
 {
-	m_solvingState.variableNames.emplace_back("");
+	m_lpSolvingState.variableNames.emplace_back("");
+	params z3Params(m_z3Ctx);
+	z3Params.set(":timeout", static_cast<unsigned>(10)); // in milliseconds
+	m_z3Solver.set(z3Params);
 }
 
 LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
@@ -36,26 +43,75 @@ LinearExpression FuzzerSolverInterface::linearExpression(vector<int> _factors)
 	return lexp;
 }
 
-void FuzzerSolverInterface::addConstraint(pair<bool, vector<int>> _constraint)
+void FuzzerSolverInterface::addLPConstraint(pair<bool, vector<int>> _constraint)
 {
-	m_solvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first});
+	m_lpSolvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first});
 }
 
-void FuzzerSolverInterface::addConstraints(vector<pair<bool, vector<int>>> _constraints)
+void FuzzerSolverInterface::addZ3Constraint(pair<bool, vector<int>> _constraint)
+{
+	bool isEquality = _constraint.first;
+	expr reduce = m_z3Ctx.real_val(0);
+	for (auto&& [index, value]: _constraint.second | ranges::views::enumerate)
+	{
+		if (index != 0 && value != 0)
+		{
+			string varName = "x" + to_string(index - 1);
+			expr var = m_z3Ctx.real_const(varName.c_str());
+			expr factor = m_z3Ctx.int_val(value);
+			reduce = reduce + var * factor;
+			m_z3Solver.add(var >= 0);
+		}
+	}
+	if (isEquality)
+		m_z3Solver.add(reduce == _constraint.second[0]);
+	else
+		m_z3Solver.add(reduce <= _constraint.second[0]);
+}
+
+void FuzzerSolverInterface::addLPConstraints(vector<pair<bool, vector<int>>> _constraints)
 {
 	for (auto c: _constraints)
-		addConstraint(c);
+		addLPConstraint(c);
 }
 
-solution FuzzerSolverInterface::check()
+void FuzzerSolverInterface::addZ3Constraints(vector<pair<bool, vector<int>>> _constraints)
 {
-	return m_solver.check(m_solvingState);
+	for (auto c: _constraints)
+		addZ3Constraint(c);
 }
 
-string FuzzerSolverInterface::checkResult()
+solution FuzzerSolverInterface::checkLP()
 {
-	auto r = check();
+	return m_lpSolver.check(m_lpSolvingState);
-	return lpResult(r.first);
+}
+
+check_result FuzzerSolverInterface::checkZ3()
+{
+	return m_z3Solver.check();
+}
+
+string FuzzerSolverInterface::checkLPResult()
+{
+	m_lpResult = lpResult(checkLP().first);
+	return m_lpResult;
+}
+
+string FuzzerSolverInterface::checkZ3Result()
+{
+	m_z3Result = z3Result(checkZ3());
+	return m_z3Result;
+}
+
+bool FuzzerSolverInterface::differentialCheck(vector<pair<bool, vector<int>>> _constraints)
+{
+	addLPConstraints(_constraints);
+	addZ3Constraints(_constraints);
+	string z3Result = checkZ3Result();
+	string lpResult = checkLPResult();
+	bool checkFailed = ((z3Result == "infeasible") && (lpResult == "feasible")) ||
+		((z3Result == "feasible") && (lpResult == "infeasible"));
+	return !checkFailed;
 }
 
 string FuzzerSolverInterface::lpResult(LPResult _result)
@@ -72,3 +128,18 @@ string FuzzerSolverInterface::lpResult(LPResult _result)
 		return "infeasible";
 	}
 }
+
+string FuzzerSolverInterface::z3Result(check_result _result)
+{
+	switch (_result)
+	{
+	case check_result::unsat:
+		return "infeasible";
+	case check_result::sat:
+		return "feasible";
+	case check_result::unknown:
+		return "unknown";
+	default:
+		solAssert(false, "Invalid Z3 result");
+	}
+}

test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h

@@ -21,6 +21,8 @@
 #include <libsolutil/LP.h>
 #include <libsolutil/LinearExpression.h>
 
+#include <z3++.h>
+
 #include <string>
 
 namespace solidity::test::fuzzer::lpsolver
@@ -37,25 +39,48 @@ public:
 	FuzzerSolverInterface(bool _supportModels);
 
 	/// Adds @param _constraint to LP solver.
-	void addConstraint(std::pair<bool, std::vector<int>> _constraint);
+	void addLPConstraint(std::pair<bool, std::vector<int>> _constraint);
+
+	/// Adds @param _constraint to Z3 solver.
+	void addZ3Constraint(std::pair<bool, std::vector<int>> _constraint);
 
 	/// Adds @param _constraints to LP solver.
-	void addConstraints(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+	void addLPConstraints(std::vector<std::pair<bool, std::vector<int>>> _constraints);
+
+	/// Adds @param _constraints to Z3 solver.
+	void addZ3Constraints(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();
+	solution checkLP();
+
+	/// Queries Z3 solver and @returns solution.
+	z3::check_result checkZ3();
 
 	/// Queries LP solver and @returns sat result as string.
-	std::string checkResult();
+	std::string checkLPResult();
 
+	/// Queries Z3 solver and @returns sat result as string.
+	std::string checkZ3Result();
+
+	/// @returns true if both the LP and the Z3 solver return an identical result on
+	/// @param _constraints, false otherwise.
+	bool differentialCheck(std::vector<std::pair<bool, std::vector<int>>> _constraints);
 private:
 	/// @returns LP result as string.
 	std::string lpResult(solidity::util::LPResult _result);
 
-	solidity::util::LPSolver m_solver;
+	/// @returns Z3 result as string.
-	solidity::util::SolvingState m_solvingState;
+	std::string z3Result(z3::check_result _result);
+
+	solidity::util::LPSolver m_lpSolver;
+	solidity::util::SolvingState m_lpSolvingState;
+	z3::context m_z3Ctx;
+	z3::solver m_z3Solver;
+public:
+	std::string m_lpResult;
+	std::string m_z3Result;
 };
 }