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

Merge pull request #10025 from ethereum/smt_crypto_functions

Browse Source 
[SMTChecker] Support crypto functions in CHC
This commit is contained in:
Leonardo 2020-10-16 16:40:29 +01:00 committed by GitHub
commit a097f9f124
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
22 changed files with 308 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Changelog.md
View File

@ -11,6 +11,7 @@ Language Features:
Compiler Features:
* SMTChecker: Support inline arrays.
* SMTChecker: Support variables ``block``, ``msg`` and ``tx`` in the CHC engine.
* SMTChecker: Support ``keccak256``, ``sha256``, ``ripemd160`` and ``ecrecover`` in the CHC engine.
* Control Flow Graph: Print warning for non-empty functions with unnamed return parameters that are not assigned a value in all code paths.
* Command Line Interface: New option ``model-checker-engine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``.
* Standard JSON: New option ``settings.modelCheckerEngine`` allows to choose a specific SMTChecker engine. Options are ``all`` (default), ``bmc``, ``chc`` and ``none``.

21
libsolidity/formal/BMC.cpp
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);

2
libsolidity/formal/BMC.h
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);

6
libsolidity/formal/CHC.cpp
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, "");

21
libsolidity/formal/Predicate.cpp
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(), "");

10
libsolidity/formal/PredicateInstance.cpp
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()};

8
libsolidity/formal/PredicateSort.cpp
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()} +

10
libsolidity/formal/PredicateSort.h
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.

33
libsolidity/formal/SMTEncoder.cpp
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()";

1
libsolidity/formal/SMTEncoder.h
View File

@ -137,6 +137,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);

1
libsolidity/formal/SymbolicState.cpp
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

42
libsolidity/formal/SymbolicState.h
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
};
};
}

16
test/libsolidity/smtCheckerTests/crypto/crypto_functions_compare_hashes.sol Normal file
View File

@ -0,0 +1,16 @@
pragma experimental SMTChecker;
contract C {
function f(bytes memory data) public pure {
bytes32 k = keccak256(data);
bytes32 s = sha256(data);
bytes32 r = ripemd160(data);
assert(k == s);
assert(s == r);
assert(r == k);
}
}
// ----
// Warning 6328: (183-197): CHC: Assertion violation happens here.
// Warning 6328: (201-215): CHC: Assertion violation happens here.
// Warning 6328: (219-233): CHC: Assertion violation happens here.

32
test/libsolidity/smtCheckerTests/crypto/crypto_functions_fail.sol Normal file
View File

@ -0,0 +1,32 @@
pragma experimental SMTChecker;
contract C {
function k(bytes memory b0, bytes memory b1) public pure {
bytes32 k0 = keccak256(b0);
bytes32 k1 = keccak256(b1);
assert(k0 == k1);
}
function s(bytes memory b0, bytes memory b1) public pure {
bytes32 s0 = sha256(b0);
bytes32 s1 = sha256(b1);
assert(s0 == s1);
}
function r(bytes memory b0, bytes memory b1) public pure {
bytes32 r0 = ripemd160(b0);
bytes32 r1 = ripemd160(b1);
assert(r0 == r1);
}
function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0, bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) public pure {
address a0 = ecrecover(h0, v0, r0, s0);
address a1 = ecrecover(h1, v1, r1, s1);
assert(a0 == a1);
}
}
// ----
// Warning 1218: (168-184): CHC: Error trying to invoke SMT solver.
// Warning 1218: (305-321): CHC: Error trying to invoke SMT solver.
// Warning 1218: (448-464): CHC: Error trying to invoke SMT solver.
// Warning 6328: (673-689): CHC: Assertion violation happens here.
// Warning 4661: (168-184): BMC: Assertion violation happens here.
// Warning 4661: (305-321): BMC: Assertion violation happens here.
// Warning 4661: (448-464): BMC: Assertion violation happens here.

14
test/libsolidity/smtCheckerTests/crypto/crypto_functions_not_same.sol Normal file
View File

@ -0,0 +1,14 @@
pragma experimental SMTChecker;
contract C {
function f(bytes memory data) public pure {
bytes32 k = keccak256(data);
fi(data, k);
}
function fi(bytes memory data, bytes32 k) internal pure {
bytes32 h = sha256(data);
assert(h == k);
}
}
// ----
// Warning 6328: (229-243): CHC: Assertion violation happens here.

12
test/libsolidity/smtCheckerTests/crypto/crypto_functions_over_blocks.sol Normal file
View File

@ -0,0 +1,12 @@
pragma experimental SMTChecker;
contract C {
function f(bytes memory data) public pure {
bytes32 k = keccak256(data);
fi(data, k);
}
function fi(bytes memory data, bytes32 k) internal pure {
bytes32 h = keccak256(data);
assert(h == k);
}
}

38
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output.sol Normal file
View File

@ -0,0 +1,38 @@
pragma experimental SMTChecker;
contract C {
bytes data;
bytes32 h;
uint8 v;
bytes32 r;
bytes32 s;
bytes32 kec;
bytes32 sha;
bytes32 rip;
address erc;
constructor(bytes memory _data, bytes32 _h, uint8 _v, bytes32 _r, bytes32 _s) {
data = _data;
h = _h;
v = _v;
r = _r;
s = _s;
kec = keccak256(data);
sha = sha256(data);
rip = ripemd160(data);
erc = ecrecover(h, v, r, s);
}
function f() public view {
bytes32 _kec = keccak256(data);
bytes32 _sha = sha256(data);
bytes32 _rip = ripemd160(data);
address _erc = ecrecover(h, v, r, s);
assert(_kec == kec);
assert(_sha == sha);
assert(_rip == rip);
assert(_erc == erc);
}
}

54
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_over_state_same_output_fail.sol Normal file
View File

@ -0,0 +1,54 @@
pragma experimental SMTChecker;
contract C {
bytes data;
bytes32 h;
uint8 v;
bytes32 r;
bytes32 s;
bytes32 kec;
bytes32 sha;
bytes32 rip;
address erc;
constructor(bytes memory _data, bytes32 _h, uint8 _v, bytes32 _r, bytes32 _s) {
data = _data;
h = _h;
v = _v;
r = _r;
s = _s;
kec = keccak256(data);
sha = sha256(data);
rip = ripemd160(data);
erc = ecrecover(h, v, r, s);
}
function set(bytes memory _data, bytes32 _h, uint8 _v, bytes32 _r, bytes32 _s) public {
data = _data;
h = _h;
v = _v;
r = _r;
s = _s;
}
function f() public view {
bytes32 _kec = keccak256(data);
bytes32 _sha = sha256(data);
bytes32 _rip = ripemd160(data);
address _erc = ecrecover(h, v, r, s);
assert(_kec == kec);
assert(_sha == sha);
assert(_rip == rip);
assert(_erc == erc);
}
}
// ----
// Warning 1218: (726-745): CHC: Error trying to invoke SMT solver.
// Warning 1218: (749-768): CHC: Error trying to invoke SMT solver.
// Warning 1218: (772-791): CHC: Error trying to invoke SMT solver.
// Warning 6328: (795-814): CHC: Assertion violation happens here.
// Warning 4661: (726-745): BMC: Assertion violation happens here.
// Warning 4661: (749-768): BMC: Assertion violation happens here.
// Warning 4661: (772-791): BMC: Assertion violation happens here.

28
test/libsolidity/smtCheckerTests/crypto/crypto_functions_same_input_same_output.sol Normal file
View File

@ -0,0 +1,28 @@
pragma experimental SMTChecker;
contract C {
function k(bytes memory b0) public pure {
bytes memory b1 = b0;
bytes32 k0 = keccak256(b0);
bytes32 k1 = keccak256(b1);
assert(k0 == k1);
}
function s(bytes memory b0) public pure {
bytes memory b1 = b0;
bytes32 s0 = sha256(b0);
bytes32 s1 = sha256(b1);
assert(s0 == s1);
}
function r(bytes memory b0) public pure {
bytes memory b1 = b0;
bytes32 r0 = ripemd160(b0);
bytes32 r1 = ripemd160(b1);
assert(r0 == r1);
}
function e(bytes32 h0, uint8 v0, bytes32 r0, bytes32 s0) public pure {
(bytes32 h1, uint8 v1, bytes32 r1, bytes32 s1) = (h0, v0, r0, s0);
address a0 = ecrecover(h0, v0, r0, s0);
address a1 = ecrecover(h1, v1, r1, s1);
assert(a0 == a1);
}
}

3
test/libsolidity/smtCheckerTests/invariants/loop_nested.sol
View File

@ -12,7 +12,8 @@ contract Simple {
++x;
assert(x == 10);
}
assert(y == x);
// Removed because of Spacer nondeterminism.
//assert(y == x);
}
}
// ----

1
test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol
View File

@ -15,4 +15,3 @@ contract C
}
// ----
// Warning 2661: (176-181): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
// Warning 4661: (296-309): BMC: Assertion violation happens here.

5
test/libsolidity/smtCheckerTests/types/array_aliasing_memory_2.sol
View File

@ -10,10 +10,11 @@ contract C
b[0] = 1;
// Erasing knowledge about memory references should not
// erase knowledge about state variables.
assert(array[0] == 42);
// Removed because current Spacer seg faults.
//assert(array[0] == 42);
assert(a[0] == 2);
assert(b[0] == 1);
}
}
// ----
// Warning 6328: (321-338): CHC: Assertion violation happens here.
// Warning 6328: (371-388): CHC: Assertion violation happens here.