mirror of
https://github.com/ethereum/solidity
synced 2023-10-03 13:03:40 +00:00
Refactor FuzzerSolverInterface.
Co-authored-by: chriseth <chris@ethereum.org>
This commit is contained in:
parent
30550429eb
commit
aeaf9addc0
@ -15,6 +15,8 @@
|
||||
|
||||
#include <test/tools/ossfuzz/lpsolver/FuzzerSolverInterface.h>
|
||||
|
||||
#include <range/v3/view/enumerate.hpp>
|
||||
|
||||
using namespace solidity::test::fuzzer::lpsolver;
|
||||
using namespace solidity::util;
|
||||
using namespace std;
|
||||
@ -25,69 +27,22 @@ FuzzerSolverInterface::FuzzerSolverInterface(bool _supportModels):
|
||||
m_solvingState.variableNames.emplace_back("");
|
||||
}
|
||||
|
||||
LinearExpression FuzzerSolverInterface::constant(rational _value)
|
||||
{
|
||||
return LinearExpression::factorForVariable(0, _value);
|
||||
}
|
||||
|
||||
LinearExpression FuzzerSolverInterface::variable(
|
||||
rational _factor,
|
||||
string const& _variable
|
||||
)
|
||||
{
|
||||
return LinearExpression::factorForVariable(variableIndex(_variable), _factor);
|
||||
}
|
||||
|
||||
void FuzzerSolverInterface::addLEConstraint(LinearExpression _lhs)
|
||||
{
|
||||
// Move constant to RHS
|
||||
if (_lhs[0])
|
||||
_lhs[0] = -_lhs[0];
|
||||
m_solvingState.constraints.push_back({move(_lhs), false});
|
||||
}
|
||||
|
||||
void FuzzerSolverInterface::addEQConstraint(LinearExpression _lhs)
|
||||
{
|
||||
// Move constant to RHS
|
||||
if (_lhs[0])
|
||||
_lhs[0] = -_lhs[0];
|
||||
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);
|
||||
}
|
||||
lexp.resize(_factors.size());
|
||||
for (auto&& [index, value]: _factors | ranges::views::enumerate)
|
||||
// Move constant term to RHS.
|
||||
if (index == 0)
|
||||
lexp[index] = -rational{value};
|
||||
else
|
||||
lexp += variable(f, "x" + to_string(count++));
|
||||
}
|
||||
lexp[index] = rational{value};
|
||||
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);
|
||||
m_solvingState.constraints.push_back({linearExpression(move(_constraint.second)), _constraint.first});
|
||||
}
|
||||
|
||||
void FuzzerSolverInterface::addConstraints(vector<pair<bool, vector<int>>> _constraints)
|
||||
@ -121,16 +76,3 @@ string FuzzerSolverInterface::lpResult(LPResult _result)
|
||||
return "infeasible";
|
||||
}
|
||||
}
|
||||
|
||||
size_t FuzzerSolverInterface::variableIndex(string const& _name)
|
||||
{
|
||||
if (m_solvingState.variableNames.empty())
|
||||
m_solvingState.variableNames.emplace_back("");
|
||||
auto index = findOffset(m_solvingState.variableNames, _name);
|
||||
if (!index)
|
||||
{
|
||||
index = m_solvingState.variableNames.size();
|
||||
m_solvingState.variableNames.emplace_back(_name);
|
||||
}
|
||||
return *index;
|
||||
}
|
||||
|
@ -36,33 +36,6 @@ class FuzzerSolverInterface
|
||||
public:
|
||||
FuzzerSolverInterface(bool _supportModels);
|
||||
|
||||
/// @returns constant rational.
|
||||
solidity::util::LinearExpression constant(solidity::util::rational _rationalConstant);
|
||||
|
||||
/// @returns linear expression that equals zero.
|
||||
solidity::util::LinearExpression zero()
|
||||
{
|
||||
return constant(0);
|
||||
}
|
||||
|
||||
/// @returns product of a rational factor and variable.
|
||||
solidity::util::LinearExpression variable(
|
||||
solidity::util::rational _factor,
|
||||
std::string const& _variable
|
||||
);
|
||||
|
||||
/// Adds less-than-equal-zero constraint to solver.
|
||||
void addLEConstraint(solidity::util::LinearExpression _lhs);
|
||||
|
||||
/// 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);
|
||||
|
||||
@ -79,9 +52,6 @@ public:
|
||||
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);
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user