ssa encoding

This commit is contained in:
chriseth 2022-04-17 17:46:20 +02:00
parent dc6eecd4ba
commit 86fde5d357
5 changed files with 164 additions and 114 deletions

View File

@ -18,7 +18,6 @@
#include <libyul/optimiser/ReasoningBasedSimplifier.h>
#include <libyul/optimiser/SMTSolver.h>
#include <libyul/optimiser/SSAValueTracker.h>
#include <libyul/optimiser/Semantics.h>
#include <libyul/AST.h>
#include <libyul/Dialect.h>
@ -41,8 +40,7 @@ using namespace solidity::smtutil;
void ReasoningBasedSimplifier::run(OptimiserStepContext& _context, Block& _ast)
{
set<YulString> ssaVars = SSAValueTracker::ssaVariables(_ast);
ReasoningBasedSimplifier simpl{_context.dialect, ssaVars};
ReasoningBasedSimplifier simpl{_context.dialect};
// Hack to inject the boolean lp solver.
simpl.m_solver = make_unique<BooleanLPSolver>();
simpl(_ast);
@ -58,14 +56,120 @@ void ReasoningBasedSimplifier::operator()(VariableDeclaration& _varDecl)
SMTSolver::encodeVariableDeclaration(_varDecl);
}
void ReasoningBasedSimplifier::operator()(Assignment& _assignment)
{
SMTSolver::encodeVariableAssignment(_assignment);
}
void ReasoningBasedSimplifier::operator()(If& _if)
{
checkIfConditionRedundant(_if);
decltype(m_variableSequenceCounter) oldCounters(m_variableSequenceCounter);
optional<smtutil::Expression> oldPathCondition = m_pathCondition;
// TODO do not call encode again - assert it is a variable
smtutil::Expression ifCondition = encodeExpression(*_if.condition);
smtutil::Expression branchCondition = (ifCondition >= 1);
if (m_pathCondition)
m_pathCondition = *m_pathCondition && branchCondition;
else
m_pathCondition = branchCondition;
ASTModifier::operator()(_if.body);
// join control flow
for (auto& var: oldCounters)
if (m_variableSequenceCounter.at(var.first) != var.second)
{
YulString const& name = var.first;
size_t oldCounter = var.second;
size_t branchCounter = m_variableSequenceCounter.at(name);
size_t newCounter = branchCounter + 1;
m_solver->newVariable(variableNameAtIndex(name, newCounter), defaultSort());
// TODO full path condition?
m_solver->addAssertion(
ifCondition == 0 ||
variableExpressionAtIndex(name, newCounter) == variableExpressionAtIndex(name, branchCounter)
);
m_solver->addAssertion(
ifCondition >= 1 ||
variableExpressionAtIndex(name, newCounter) == variableExpressionAtIndex(name, oldCounter)
);
var.second = newCounter;
}
m_variableSequenceCounter = move(oldCounters);
m_pathCondition = move(oldPathCondition);
}
void ReasoningBasedSimplifier::operator()(ForLoop& _for)
{
// TODO handle break / continue
decltype(m_variableSequenceCounter) oldCounters(m_variableSequenceCounter);
optional<smtutil::Expression> oldPathCondition = m_pathCondition;
// TODO do not call encode again - assert it is a variable
smtutil::Expression forCondition = encodeExpression(*_for.condition);
smtutil::Expression branchCondition = (forCondition >= 1);
if (m_pathCondition)
m_pathCondition = *m_pathCondition && branchCondition;
else
m_pathCondition = branchCondition;
yulAssert(_for.pre.statements.empty());
ASTModifier::operator()(_for.body);
// TODO clear modified variables!
ASTModifier::operator()(_for.post);
// join control flow
for (auto& var: oldCounters)
if (m_variableSequenceCounter.at(var.first) != var.second)
{
var.second++;
m_solver->newVariable(variableNameAtIndex(var.first, var.second), defaultSort());
restrictToEVMWord(currentVariableExpression(var.first));
}
m_variableSequenceCounter = move(oldCounters);
m_pathCondition = move(oldPathCondition);
}
void ReasoningBasedSimplifier::operator()(FunctionCall& _fun)
{
ASTModifier::operator()(_fun);
// TODO do not forget to add path condition!
// TODO and(x, 0xfff) -> x if x <= 0xfff
// TODO if _fun is not returning, assert that the path condition is aflse
}
void ReasoningBasedSimplifier::operator()(FunctionDefinition& _fun)
{
ScopedSaveAndRestore counters(m_variableSequenceCounter, {});
ScopedSaveAndRestore pathCond(m_pathCondition, true);
ASTModifier::operator()(_fun);
}
ReasoningBasedSimplifier::ReasoningBasedSimplifier(
Dialect const& _dialect
):
SMTSolver(_dialect)
{
}
void ReasoningBasedSimplifier::checkIfConditionRedundant(If& _if)
{
if (!SideEffectsCollector{m_dialect, *_if.condition}.movable())
return;
cout << "Checking if condition can be false" << endl;
// TODO should not call encode, but instead check if it is
// a variable and use its name / value
smtutil::Expression condition = encodeExpression(*_if.condition);
m_solver->push();
// TODO find a way so that we do not have to do that all the time.
if (m_pathCondition)
m_solver->addAssertion(*m_pathCondition);
m_solver->addAssertion(condition == constantValue(0));
cout << " running check" << endl;
CheckResult result = m_solver->check({}).first;
@ -81,7 +185,9 @@ void ReasoningBasedSimplifier::operator()(If& _if)
{
cout << "Checking if condition can be true" << endl;
m_solver->push();
// TODO change this to >= 1 for simplicity?
// TODO find a way so that we do not have to do that all the time.
if (m_pathCondition)
m_solver->addAssertion(*m_pathCondition);
m_solver->addAssertion(condition >= 1);
cout << " running check" << endl;
CheckResult result2 = m_solver->check({}).first;
@ -93,83 +199,9 @@ void ReasoningBasedSimplifier::operator()(If& _if)
falseCondition.debugData = debugDataOf(*_if.condition);
_if.condition = make_unique<yul::Expression>(move(falseCondition));
_if.body = yul::Block{};
// Nothing left to be done.
return;
}
cout << " unknown :(" << endl;
}
m_solver->push();
cout << "Setting condition true inside body" << endl;
m_solver->addAssertion(condition >= constantValue(1));
ASTModifier::operator()(_if.body);
m_solver->pop();
// TODO if the body is non-continuing, we could assert that the condition is false
// but this might not be true anymore once we join with another control-flow.
// maybe it is best to let the conditional simplifier and the data flow analyzer do this for us.
}
void ReasoningBasedSimplifier::operator()(ForLoop& _for)
{
// TODO handle break / continue
if (!SideEffectsCollector{m_dialect, *_for.condition}.movable())
return;
cout << "Checking if condition can be false" << endl;
smtutil::Expression condition = encodeExpression(*_for.condition);
m_solver->push();
m_solver->addAssertion(condition <= constantValue(0));
cout << " running check" << endl;
CheckResult result = m_solver->check({}).first;
m_solver->pop();
if (result == CheckResult::UNSATISFIABLE)
{
cout << " unsat => cannot be false!" << endl;
Literal trueCondition = m_dialect.trueLiteral();
trueCondition.debugData = debugDataOf(*_for.condition);
_for.condition = make_unique<yul::Expression>(move(trueCondition));
}
else
{
cout << "Checking if condition can be true" << endl;
m_solver->push();
m_solver->addAssertion(condition >= constantValue(1));
cout << " running check" << endl;
CheckResult result2 = m_solver->check({}).first;
m_solver->pop();
if (result2 == CheckResult::UNSATISFIABLE)
{
cout << " unsat => cannot be true!" << endl;
Literal falseCondition = m_dialect.zeroLiteralForType(m_dialect.boolType);
falseCondition.debugData = debugDataOf(*_for.condition);
_for.condition = make_unique<yul::Expression>(move(falseCondition));
_for.body = yul::Block{};
// Nothing left to be done.
return;
}
}
m_solver->push();
cout << "Setting condition true inside body" << endl;
m_solver->addAssertion(condition >= constantValue(1));
ASTModifier::operator()(_for.body);
ASTModifier::operator()(_for.post);
m_solver->pop();
}
ReasoningBasedSimplifier::ReasoningBasedSimplifier(
Dialect const& _dialect,
set<YulString> const& _ssaVariables
):
SMTSolver(_ssaVariables, _dialect),
m_dialect(_dialect)
{
}

View File

@ -58,14 +58,16 @@ public:
using ASTModifier::operator();
void operator()(VariableDeclaration& _varDecl) override;
void operator()(Assignment& _assignment) override;
void operator()(If& _if) override;
void operator()(ForLoop& _for) override;
void operator()(FunctionCall& _fun) override;
void operator()(FunctionDefinition& _fun) override;
private:
explicit ReasoningBasedSimplifier(
Dialect const& _dialect,
std::set<YulString> const& _ssaVariables
);
explicit ReasoningBasedSimplifier(Dialect const& _dialect);
void checkIfConditionRedundant(If& _if);
smtutil::Expression encodeEVMBuiltin(
evmasm::Instruction _instruction,
@ -74,8 +76,6 @@ private:
smtutil::Expression newZeroOneVariable();
void restrictToEVMWord(smtutil::Expression _value);
Dialect const& m_dialect;
};
}

View File

@ -33,8 +33,7 @@ using namespace solidity::smtutil;
using namespace solidity;
using namespace std;
SMTSolver::SMTSolver(set<YulString> const& _ssaVariables, Dialect const& _dialect):
m_ssaVariables(_ssaVariables),
SMTSolver::SMTSolver(Dialect const& _dialect):
m_solver(make_unique<smtutil::SMTPortfolio>()),
m_dialect(_dialect)
{ }
@ -51,13 +50,7 @@ smtutil::Expression SMTSolver::encodeExpression(Expression const& _expression)
},
[&](Identifier const& _identifier)
{
if (
m_ssaVariables.count(_identifier.name) &&
m_variables.count(_identifier.name)
)
return m_variables.at(_identifier.name);
else
return newRestrictedVariable();
return currentVariableExpression(_identifier.name);
},
[&](Literal const& _literal)
{
@ -76,6 +69,21 @@ smtutil::Expression SMTSolver::bv2int(smtutil::Expression _arg)
return smtutil::Expression::bv2int(std::move(_arg));
}
string SMTSolver::variableNameAtIndex(YulString const& _name, size_t _index) const
{
return "yul_" + to_string(_index) + "_"s + _name.str();
}
smtutil::Expression SMTSolver::variableExpressionAtIndex(YulString const& _name, size_t _index) const
{
return smtutil::Expression(variableNameAtIndex(_name, _index), {}, defaultSort());
}
smtutil::Expression SMTSolver::currentVariableExpression(YulString const& _name) const
{
return variableExpressionAtIndex(_name, m_variableSequenceCounter.at(_name));
}
smtutil::Expression SMTSolver::newVariable()
{
return m_solver->newVariable(uniqueName(), defaultSort());
@ -149,18 +157,25 @@ void SMTSolver::encodeVariableDeclaration(VariableDeclaration const& _varDecl)
{
if (
_varDecl.variables.size() == 1 &&
_varDecl.value &&
m_ssaVariables.count(_varDecl.variables.front().name)
_varDecl.value
)
{
YulString const& variableName = _varDecl.variables.front().name;
bool const inserted = m_variables.insert({
variableName,
m_solver->newVariable("yul_" + variableName.str(), defaultSort())
}).second;
yulAssert(inserted, "");
m_solver->addAssertion(
m_variables.at(variableName) == encodeExpression(*_varDecl.value)
);
}
encodeVariableUpdate(_varDecl.variables.front().name, *_varDecl.value);
}
void SMTSolver::encodeVariableAssignment(Assignment const& _assignment)
{
if (_assignment.variableNames.size() == 1)
encodeVariableUpdate(_assignment.variableNames.front().name, *_assignment.value);
}
void SMTSolver::encodeVariableUpdate(YulString const& _name, Expression const& _value)
{
smtutil::Expression value = encodeExpression(_value);
if (m_variableSequenceCounter.count(_name))
++m_variableSequenceCounter[_name];
else
m_variableSequenceCounter[_name] = 1;
m_solver->newVariable(variableNameAtIndex(_name, m_variableSequenceCounter[_name]), defaultSort());
m_solver->addAssertion(currentVariableExpression(_name) == value);
}

View File

@ -47,13 +47,12 @@ namespace solidity::yul
class SMTSolver
{
protected:
SMTSolver(
std::set<YulString> const& _ssaVariables,
Dialect const& _dialect
);
SMTSolver(Dialect const& _dialect);
/// Helper function that encodes VariableDeclaration
void encodeVariableDeclaration(VariableDeclaration const& _varDecl);
void encodeVariableAssignment(Assignment const& _assignment);
void encodeVariableUpdate(YulString const& _name, Expression const& _value);
/// The encoding for a builtin. The type of encoding determines what we are
/// solving for.
@ -67,6 +66,10 @@ protected:
static smtutil::Expression int2bv(smtutil::Expression _arg);
static smtutil::Expression bv2int(smtutil::Expression _arg);
std::string variableNameAtIndex(YulString const& _name, size_t _index) const;
smtutil::Expression variableExpressionAtIndex(YulString const& _name, size_t _index) const;
smtutil::Expression currentVariableExpression(YulString const& _name) const;
smtutil::Expression newVariable();
smtutil::Expression newBooleanVariable();
virtual smtutil::Expression newRestrictedVariable(bigint _maxValue = (bigint(1) << 256) - 1);
@ -81,9 +84,9 @@ protected:
static smtutil::Expression signedToTwosComplement(smtutil::Expression _value);
smtutil::Expression wrap(smtutil::Expression _value);
std::set<YulString> const& m_ssaVariables;
std::unique_ptr<smtutil::SolverInterface> m_solver;
std::map<YulString, smtutil::Expression> m_variables;
std::map<YulString, size_t> m_variableSequenceCounter;
std::optional<smtutil::Expression> m_pathCondition;
Dialect const& m_dialect;

View File

@ -11,6 +11,6 @@
// {
// let x := sub(0, 7)
// let y := 2
// if 1 { }
// if 0 { }
// if iszero(add(sdiv(x, y), 3)) { }
// if iszero(add(sdiv(x, y), 4)) { }
// }