cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Some experiments.

Browse Source
This commit is contained in:
chriseth 2021-09-27 12:59:25 +02:00
parent e47023a222
commit c518b359a8
2 changed files with 34 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
libsolutil/BooleanLP.cpp
View File

@ -242,14 +242,16 @@ void BooleanLPSolver::addAssertion(Expression const& _expr)
addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1); addAssertion(_expr.arguments.at(0) <= _expr.arguments.at(1) - 1);
else if (_expr.name == ">") else if (_expr.name == ">")
addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0)); addAssertion(_expr.arguments.at(1) < _expr.arguments.at(0));
else
cout << "Unknown operator " << _expr.name << endl;
} }
pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const& _expressionsToEvaluate) pair<CheckResult, vector<string>> BooleanLPSolver::check(vector<Expression> const& _expressionsToEvaluate)
{ {
cout << "Solving boolean constraint system" << endl; // cout << "Solving boolean constraint system" << endl;
cout << toString() << endl; // cout << toString() << endl;
cout << "--------------" << endl; // cout << "--------------" << endl;
if (m_state.back().infeasible) if (m_state.back().infeasible)
return make_pair(CheckResult::UNSATISFIABLE, vector<string>{}); return make_pair(CheckResult::UNSATISFIABLE, vector<string>{});
@ -330,6 +332,8 @@ optional<Literal> BooleanLPSolver::parseLiteral(smtutil::Expression const& _expr
Literal::PositiveVariable, Literal::PositiveVariable,
m_state.back().variables.at(_expr.name) m_state.back().variables.at(_expr.name)
}; };
else
cout << "cannot encode " << _expr.name << " - not a boolean literal variable." << endl;
} }
else if (_expr.name == "not") else if (_expr.name == "not")
return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0))); return negate(parseLiteralOrReturnEqualBoolean(_expr.arguments.at(0)));

30
libyul/optimiser/ReasoningBasedSimplifier.cpp
View File

@ -165,7 +165,7 @@ void ReasoningBasedSimplifier::operator()(If& _if)
if (bodyTerminates) if (bodyTerminates)
{ {
cout << "Body always terminates." << endl; //cout << "Body always terminates." << endl;
if (isBoolean(*_if.condition)) if (isBoolean(*_if.condition))
m_solver->addAssertion(!cond); m_solver->addAssertion(!cond);
else else
@ -267,10 +267,28 @@ void ReasoningBasedSimplifier::handleDeclaration(
} }
//case evmasm::Instruction::MUL: //case evmasm::Instruction::MUL:
// TODO encode constants? // TODO encode constants?
//case evmasm::Instruction::DIV: case evmasm::Instruction::DIV:
m_solver->addAssertion(variable <= *x);
break;
case evmasm::Instruction::ADDMOD: case evmasm::Instruction::ADDMOD:
m_solver->addAssertion(variable < *z); m_solver->addAssertion(variable < *z);
break; break;
case evmasm::Instruction::SHL:
if (holds_alternative<Literal>(_arguments.at(0)))
{
u256 shiftAmount = valueOfLiteral(get<Literal>(_arguments.at(0)));
cout << "shift by " << shiftAmount << endl;
}
break;
case evmasm::Instruction::SHR:
if (holds_alternative<Literal>(_arguments.at(0)))
{
u256 shiftAmount = valueOfLiteral(get<Literal>(_arguments.at(0)));
cout << "shift by " << shiftAmount << endl;
}
break;
case evmasm::Instruction::SAR:
break;
case evmasm::Instruction::LT: case evmasm::Instruction::LT:
m_solver->addAssertion(variable == (*x < *y)); m_solver->addAssertion(variable == (*x < *y));
break; break;
@ -281,7 +299,12 @@ void ReasoningBasedSimplifier::handleDeclaration(
// case evmasm::Instruction::SGT: // case evmasm::Instruction::SGT:
// TODO // TODO
case evmasm::Instruction::EQ: case evmasm::Instruction::EQ:
m_solver->addAssertion(variable == (*x == *y)); if (isBoolean(_arguments.at(0)) == isBoolean(_arguments.at(1)))
m_solver->addAssertion(variable == (*x == *y));
else if (isBoolean(_arguments.at(0)))
m_solver->addAssertion(variable == ((*x && *y >= 1) || (!*x && *y == 0)));
else
m_solver->addAssertion(variable == ((*y && *x >= 1) || (!*y && *x == 0)));
break; break;
case evmasm::Instruction::ISZERO: case evmasm::Instruction::ISZERO:
if (isBoolean(_arguments.at(0))) if (isBoolean(_arguments.at(0)))
@ -313,6 +336,7 @@ void ReasoningBasedSimplifier::handleDeclaration(
break; break;
// TODO all builtins whose return values can be restricted. // TODO all builtins whose return values can be restricted.
default: default:
cout << "Not handling instruction " << evmasm::instructionInfo(_instruction).name << endl;
break; break;
} }
} }