cerc-io/solidity
11
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

[SMTChecker] Support crypto functions in CHC

Browse Source
This commit is contained in:
Leonardo Alt
2020-10-16 14:57:13 +01:00
parent 25b10b9643
commit 54f76e081a
22 changed files with 308 additions and 51 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/BMC.cpp
+4 -17
View File
@@ -385,13 +385,6 @@ void BMC::endVisit(FunctionCall const& _funCall)
SMTEncoder::endVisit(_funCall);
internalOrExternalFunctionCall(_funCall);
break;
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160:
SMTEncoder::endVisit(_funCall);
abstractFunctionCall(_funCall);
break;
case FunctionType::Kind::Send:
case FunctionType::Kind::Transfer:
{
@@ -408,6 +401,10 @@ void BMC::endVisit(FunctionCall const& _funCall)
SMTEncoder::endVisit(_funCall);
break;
}
case FunctionType::Kind::KECCAK256:
case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160:
case FunctionType::Kind::BlockHash:
case FunctionType::Kind::AddMod:
case FunctionType::Kind::MulMod:
@@ -485,16 +482,6 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
createReturnedExpressions(_funCall);
}
void BMC::abstractFunctionCall(FunctionCall const& _funCall)
{
vector<smtutil::Expression> smtArguments;
for (auto const& arg: _funCall.arguments())
smtArguments.push_back(expr(*arg));
defineExpr(_funCall, (*m_context.expression(_funCall.expression()))(smtArguments));
m_uninterpretedTerms.insert(&_funCall);
setSymbolicUnknownValue(expr(_funCall), _funCall.annotation().type, m_context);
}
void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
{
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
libsolidity/formal/BMC.h
-2
View File
@@ -99,8 +99,6 @@ private:
/// Visits the FunctionDefinition of the called function
/// if available and inlines the return value.
void inlineFunctionCall(FunctionCall const& _funCall);
/// Creates an uninterpreted function call.
void abstractFunctionCall(FunctionCall const& _funCall);
/// Inlines if the function call is internal or external to `this`.
/// Erases knowledge about state variables if external.
void internalOrExternalFunctionCall(FunctionCall const& _funCall);
libsolidity/formal/CHC.cpp
+3 -3
View File
@@ -120,7 +120,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
&_contract
);
addRule(
(*implicitConstructorPredicate)({0, state().thisAddress(), state().tx(), state().state()}),
(*implicitConstructorPredicate)({0, state().thisAddress(), state().crypto(), state().tx(), state().state()}),
implicitConstructorPredicate->functor().name
);
setCurrentBlock(*implicitConstructorPredicate);
@@ -874,7 +874,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state(1)};
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state(1)};
args += state1 +
applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
vector<smtutil::Expression>{state().state(2)} +
@@ -1053,7 +1053,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
return smtutil::Expression(true);
errorFlag().increaseIndex();
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().tx(), state().state()};
vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()};
FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
solAssert(funType.kind() == FunctionType::Kind::Internal, "");
libsolidity/formal/Predicate.cpp
+10 -11
View File
@@ -161,9 +161,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
auto const* fun = programFunction();
solAssert(fun, "");
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockChainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in preInputVars.
vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size());
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size());
vector<string>::const_iterator last = first + static_cast<int>(fun->parameters().size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -188,10 +188,9 @@ string Predicate::formatSummaryCall(vector<string> const& _args) const
vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, txData, preBlockSchainState, postBlockchainState, postStateVars).
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of an implicit constructor summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, postBlockchainState, postStateVars).
/// Here we are interested in postStateVars.
auto stateVars = stateVariables();
solAssert(stateVars.has_value(), "");
@@ -199,12 +198,12 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
vector<string>::const_iterator stateLast;
if (auto const* function = programFunction())
{
stateFirst = _args.begin() + 4 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateFirst = _args.begin() + 5 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else if (programContract())
{
stateFirst = _args.begin() + 5;
stateFirst = _args.begin() + 6;
stateLast = stateFirst + static_cast<int>(stateVars->size());
}
else
@@ -220,7 +219,7 @@ vector<string> Predicate::summaryStateValues(vector<string> const& _args) const
vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in postInputVars.
auto const* function = programFunction();
solAssert(function, "");
@@ -230,7 +229,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
vector<string>::const_iterator last = first + static_cast<int>(inParams.size());
solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -243,7 +242,7 @@ vector<string> Predicate::summaryPostInputValues(vector<string> const& _args) co
vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) const
{
/// The signature of a function summary predicate is: summary(error, this, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// The signature of a function summary predicate is: summary(error, this, cryptoFunctions, txData, preBlockchainState, preStateVars, preInputVars, postBlockchainState, postStateVars, postInputVars, outputVars).
/// Here we are interested in outputVars.
auto const* function = programFunction();
solAssert(function, "");
@@ -253,7 +252,7 @@ vector<string> Predicate::summaryPostOutputValues(vector<string> const& _args) c
auto const& inParams = function->parameters();
vector<string>::const_iterator first = _args.begin() + 4 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
vector<string>::const_iterator first = _args.begin() + 5 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
solAssert(first >= _args.begin() && first <= _args.end(), "");
libsolidity/formal/PredicateInstance.cpp
+5 -5
View File
@@ -30,14 +30,14 @@ namespace solidity::frontend::smt
smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state(0)};
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state(0)};
return _pred(stateExprs + initialStateVariables(_contract, _context));
}
smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.state()};
vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.crypto(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
@@ -54,7 +54,7 @@ smtutil::Expression nondetInterface(Predicate const& _pred, ContractDefinition c
smtutil::Expression implicitConstructor(Predicate const& _pred, ContractDefinition const&, EncodingContext& _context)
{
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
return _pred(stateExprs);
}
@@ -64,7 +64,7 @@ smtutil::Expression constructor(Predicate const& _pred, ContractDefinition const
return _pred(currentFunctionVariables(*constructor, &_contract, _context));
auto& state = _context.state();
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0), state.state()};
vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
return _pred(stateExprs + currentStateVariables(_contract, _context));
}
@@ -118,7 +118,7 @@ vector<smtutil::Expression> currentFunctionVariables(
)
{
auto& state = _context.state();
vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.tx(0), state.state(0)};
vector<smtutil::Expression> exprs{_context.state().errorFlag().currentValue(), state.thisAddress(0), state.crypto(0), state.tx(0), state.state(0)};
exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
exprs += vector<smtutil::Expression>{state.state()};
libsolidity/formal/PredicateSort.cpp
+4 -4
View File
@@ -31,7 +31,7 @@ namespace solidity::frontend::smt
SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
{
return make_shared<FunctionSort>(
vector<SortPointer>{_state.thisAddressSort(), _state.stateSort()} + stateSorts(_contract),
vector<SortPointer>{_state.thisAddressSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
@@ -49,7 +49,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
SortPointer implicitConstructorSort(SymbolicState& _state)
{
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()},
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()},
SortProvider::boolSort
);
}
@@ -60,7 +60,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
return functionSort(*constructor, &_contract, _state);
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + stateSorts(_contract),
SortProvider::boolSort
);
}
@@ -72,7 +72,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
auto inputSorts = applyMap(_function.parameters(), smtSort);
auto outputSorts = applyMap(_function.returnParameters(), smtSort);
return make_shared<FunctionSort>(
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.txSort(), _state.stateSort()} +
vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
varSorts +
inputSorts +
vector<SortPointer>{_state.stateSort()} +
libsolidity/formal/PredicateSort.h
+5 -5
View File
@@ -33,7 +33,7 @@ namespace solidity::frontend::smt
*
* 1. Interface
* The idle state of a contract. Signature:
* interface(this, blockchainState, stateVariables).
* interface(this, cryptoFunctions, blockchainState, stateVariables).
*
* 2. Nondet interface
* The nondeterminism behavior of a contract. Signature:
@@ -41,19 +41,19 @@ namespace solidity::frontend::smt
*
* 3. Implicit constructor
* The implicit constructor of a contract, that is, without input parameters. Signature:
* implicit_constructor(error, this, txData, blockchainState).
* implicit_constructor(error, this, cryptoFunctions, txData, blockchainState).
*
* 4. Constructor entry/summary
* The summary of an implicit constructor. Signature:
* constructor_summary(error, this, txData, blockchainState, blockchainState', stateVariables').
* constructor_summary(error, this, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables').
*
* 5. Function entry/summary
* The entry point of a function definition. Signature:
* function_entry(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
* function_entry(error, this, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
*
* 6. Function body
* Use for any predicate within a function. Signature:
* function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState' ,stateVariables', inputVariables', outputVariables', localVariables).
* function_body(error, this, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
*/
/// @returns the interface predicate sort for _contract.
libsolidity/formal/SMTEncoder.cpp
+33
View File
@@ -633,6 +633,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
case FunctionType::Kind::ECRecover:
case FunctionType::Kind::SHA256:
case FunctionType::Kind::RIPEMD160:
visitCryptoFunction(_funCall);
break;
case FunctionType::Kind::BlockHash:
defineExpr(_funCall, m_context.state().blockhash(expr(*_funCall.arguments().at(0))));
@@ -730,6 +731,38 @@ void SMTEncoder::visitRequire(FunctionCall const& _funCall)
addPathImpliedExpression(expr(*args.front()));
}
void SMTEncoder::visitCryptoFunction(FunctionCall const& _funCall)
{
auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
auto kind = funType.kind();
auto arg0 = expr(*_funCall.arguments().at(0));
optional<smtutil::Expression> result;
if (kind == FunctionType::Kind::KECCAK256)
result = smtutil::Expression::select(m_context.state().cryptoFunction("keccak256"), arg0);
else if (kind == FunctionType::Kind::SHA256)
result = smtutil::Expression::select(m_context.state().cryptoFunction("sha256"), arg0);
else if (kind == FunctionType::Kind::RIPEMD160)
result = smtutil::Expression::select(m_context.state().cryptoFunction("ripemd160"), arg0);
else if (kind == FunctionType::Kind::ECRecover)
{
auto e = m_context.state().cryptoFunction("ecrecover");
auto arg0 = expr(*_funCall.arguments().at(0));
auto arg1 = expr(*_funCall.arguments().at(1));
auto arg2 = expr(*_funCall.arguments().at(2));
auto arg3 = expr(*_funCall.arguments().at(3));
auto inputSort = dynamic_cast<smtutil::ArraySort&>(*e.sort).domain;
auto ecrecoverInput = smtutil::Expression::tuple_constructor(
smtutil::Expression(make_shared<smtutil::SortSort>(inputSort), ""),
{arg0, arg1, arg2, arg3}
);
result = smtutil::Expression::select(e, ecrecoverInput);
}
else
solAssert(false, "");
defineExpr(_funCall, *result);
}
void SMTEncoder::visitGasLeft(FunctionCall const& _funCall)
{
string gasLeft = "gasleft()";
libsolidity/formal/SMTEncoder.h
+1
View File
@@ -136,6 +136,7 @@ protected:
void initFunction(FunctionDefinition const& _function);
void visitAssert(FunctionCall const& _funCall);
void visitRequire(FunctionCall const& _funCall);
void visitCryptoFunction(FunctionCall const& _funCall);
void visitGasLeft(FunctionCall const& _funCall);
virtual void visitAddMulMod(FunctionCall const& _funCall);
void visitObjectCreation(FunctionCall const& _funCall);
libsolidity/formal/SymbolicState.cpp
+1
View File
@@ -76,6 +76,7 @@ void SymbolicState::reset()
m_thisAddress.resetIndex();
m_state.reset();
m_tx.reset();
m_crypto.reset();
}
smtutil::Expression SymbolicState::balances() const
libsolidity/formal/SymbolicState.h
+42
View File
@@ -128,6 +128,16 @@ public:
smtutil::Expression blockhash(smtutil::Expression _blockNumber) const;
//@}
/// Crypto functions.
//@{
/// @returns the crypto functions represented as a tuple of arrays.
smtutil::Expression crypto() const { return m_crypto.value(); }
smtutil::Expression crypto(unsigned _idx) const { return m_crypto.value(_idx); }
smtutil::SortPointer const& cryptoSort() const { return m_crypto.sort(); }
void newCrypto() { m_crypto.newVar(); }
smtutil::Expression cryptoFunction(std::string const& _member) const { return m_crypto.member(_member); }
//@}
private:
/// Adds _value to _account's balance.
void addBalance(smtutil::Expression _account, smtutil::Expression _value);
@@ -171,6 +181,38 @@ private:
},
m_context
};
BlockchainVariable m_crypto{
"crypto",
{
{"keccak256", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(32))
)},
{"sha256", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(32))
)},
{"ripemd160", std::make_shared<smtutil::ArraySort>(
smt::smtSort(*TypeProvider::bytesStorage()),
smtSort(*TypeProvider::fixedBytes(20))
)},
{"ecrecover", std::make_shared<smtutil::ArraySort>(
std::make_shared<smtutil::TupleSort>(
"ecrecover_input_type",
std::vector<std::string>{"hash", "v", "r", "s"},
std::vector<smtutil::SortPointer>{
smt::smtSort(*TypeProvider::fixedBytes(32)),
smt::smtSort(*TypeProvider::uint(8)),
smt::smtSort(*TypeProvider::fixedBytes(32)),
smt::smtSort(*TypeProvider::fixedBytes(32))
}
),
smtSort(*TypeProvider::address())
)}
},
m_context
};
};
}