Merge remote-tracking branch 'origin/develop' into develop_060

This commit is contained in:
chriseth 2019-12-04 17:01:44 +01:00
commit 42d9a8e962
34 changed files with 261 additions and 114 deletions

View File

@ -34,4 +34,4 @@ for OPTIMIZE in 0 1; do
done done
done done
EVM=constantinople OPTIMIZE=1 ABI_ENCODER_V2=1 ${REPODIR}/.circleci/soltest.sh EVM=istanbul OPTIMIZE=1 ABI_ENCODER_V2=1 ${REPODIR}/.circleci/soltest.sh

View File

@ -48,6 +48,7 @@ Language Features:
Compiler Features: Compiler Features:
* Set the default EVM version to "Istanbul".
* Commandline Interface: Allow translation from yul / strict assembly to EWasm using ``solc --yul --yul-dialect evm --machine eWasm`` * Commandline Interface: Allow translation from yul / strict assembly to EWasm using ``solc --yul --yul-dialect evm --machine eWasm``
* SMTChecker: Add support to constructors including constructor inheritance. * SMTChecker: Add support to constructors including constructor inheritance.
* Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable. * Yul: When compiling via Yul, string literals from the Solidity code are kept as string literals if every character is safely printable.
@ -62,6 +63,7 @@ Bugfixes:
* SMTChecker: Fix internal error when using ``abi.decode``. * SMTChecker: Fix internal error when using ``abi.decode``.
* SMTChecker: Fix internal error when using arrays or mappings of functions. * SMTChecker: Fix internal error when using arrays or mappings of functions.
* SMTChecker: Fix internal error in array of structs type. * SMTChecker: Fix internal error in array of structs type.
* Yul: Consider infinite loops and recursion to be not removable.

View File

@ -120,9 +120,9 @@ at each version. Backward compatibility is not guaranteed between each version.
- ``constantinople`` - ``constantinople``
- Opcodes ``create2`, ``extcodehash``, ``shl``, ``shr`` and ``sar`` are available in assembly. - Opcodes ``create2`, ``extcodehash``, ``shl``, ``shr`` and ``sar`` are available in assembly.
- Shifting operators use shifting opcodes and thus need less gas. - Shifting operators use shifting opcodes and thus need less gas.
- ``petersburg`` (**default**) - ``petersburg``
- The compiler behaves the same way as with constantinople. - The compiler behaves the same way as with constantinople.
- ``istanbul`` - ``istanbul`` (**default**)
- Opcodes ``chainid`` and ``selfbalance`` are available in assembly. - Opcodes ``chainid`` and ``selfbalance`` are available in assembly.
- ``berlin`` (**experimental**) - ``berlin`` (**experimental**)

View File

@ -98,7 +98,7 @@ private:
EVMVersion(Version _version): m_version(_version) {} EVMVersion(Version _version): m_version(_version) {}
Version m_version = Version::Petersburg; Version m_version = Version::Istanbul;
}; };
} }

View File

@ -35,7 +35,7 @@ void CVC4Interface::reset()
m_variables.clear(); m_variables.clear();
m_solver.reset(); m_solver.reset();
m_solver.setOption("produce-models", true); m_solver.setOption("produce-models", true);
m_solver.setTimeLimit(queryTimeout); m_solver.setResourceLimit(resourceLimit);
} }
void CVC4Interface::push() void CVC4Interface::push()

View File

@ -63,6 +63,12 @@ private:
CVC4::ExprManager m_context; CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver; CVC4::SmtEngine m_solver;
std::map<std::string, CVC4::Expr> m_variables; std::map<std::string, CVC4::Expr> m_variables;
// CVC4 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
// The tests start failing for CVC4 with less than 6000,
// so using double that.
static int const resourceLimit = 12000;
}; };
} }

View File

@ -359,10 +359,6 @@ public:
/// @returns how many SMT solvers this interface has. /// @returns how many SMT solvers this interface has.
virtual unsigned solvers() { return 1; } virtual unsigned solvers() { return 1; }
protected:
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
}; };
} }

View File

@ -29,10 +29,9 @@ Z3CHCInterface::Z3CHCInterface():
m_context(m_z3Interface->context()), m_context(m_z3Interface->context()),
m_solver(*m_context) m_solver(*m_context)
{ {
// This needs to be set globally. // These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context. z3::set_param("rlimit", Z3Interface::resourceLimit);
m_context->set("timeout", queryTimeout);
// Spacer options. // Spacer options.
// These needs to be set in the solver. // These needs to be set in the solver.

View File

@ -54,9 +54,6 @@ private:
z3::context* m_context; z3::context* m_context;
// Horn solver. // Horn solver.
z3::fixedpoint m_solver; z3::fixedpoint m_solver;
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
}; };
} }

View File

@ -27,10 +27,9 @@ using namespace dev::solidity::smt;
Z3Interface::Z3Interface(): Z3Interface::Z3Interface():
m_solver(m_context) m_solver(m_context)
{ {
// This needs to be set globally. // These need to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context. z3::set_param("rlimit", resourceLimit);
m_context.set("timeout", queryTimeout);
} }
void Z3Interface::reset() void Z3Interface::reset()

View File

@ -50,6 +50,12 @@ public:
z3::context* context() { return &m_context; } z3::context* context() { return &m_context; }
// Z3 "basic resources" limit.
// This is used to make the runs more deterministic and platform/machine independent.
// The tests start failing for Z3 with less than 20000000,
// so using double that.
static int const resourceLimit = 40000000;
private: private:
void declareFunction(std::string const& _name, Sort const& _sort); void declareFunction(std::string const& _name, Sort const& _sort);

View File

@ -29,7 +29,7 @@ using namespace std;
using namespace dev; using namespace dev;
using namespace yul; using namespace yul;
map<YulString, set<YulString>> CallGraphGenerator::callGraph(Block const& _ast) CallGraph CallGraphGenerator::callGraph(Block const& _ast)
{ {
CallGraphGenerator gen; CallGraphGenerator gen;
gen(_ast); gen(_ast);
@ -38,22 +38,27 @@ map<YulString, set<YulString>> CallGraphGenerator::callGraph(Block const& _ast)
void CallGraphGenerator::operator()(FunctionCall const& _functionCall) void CallGraphGenerator::operator()(FunctionCall const& _functionCall)
{ {
m_callGraph[m_currentFunction].insert(_functionCall.functionName.name); m_callGraph.functionCalls[m_currentFunction].insert(_functionCall.functionName.name);
ASTWalker::operator()(_functionCall); ASTWalker::operator()(_functionCall);
} }
void CallGraphGenerator::operator()(ForLoop const&)
{
m_callGraph.functionsWithLoops.insert(m_currentFunction);
}
void CallGraphGenerator::operator()(FunctionDefinition const& _functionDefinition) void CallGraphGenerator::operator()(FunctionDefinition const& _functionDefinition)
{ {
YulString previousFunction = m_currentFunction; YulString previousFunction = m_currentFunction;
m_currentFunction = _functionDefinition.name; m_currentFunction = _functionDefinition.name;
yulAssert(m_callGraph.count(m_currentFunction) == 0, ""); yulAssert(m_callGraph.functionCalls.count(m_currentFunction) == 0, "");
m_callGraph[m_currentFunction] = {}; m_callGraph.functionCalls[m_currentFunction] = {};
ASTWalker::operator()(_functionDefinition); ASTWalker::operator()(_functionDefinition);
m_currentFunction = previousFunction; m_currentFunction = previousFunction;
} }
CallGraphGenerator::CallGraphGenerator() CallGraphGenerator::CallGraphGenerator()
{ {
m_callGraph[YulString{}] = {}; m_callGraph.functionCalls[YulString{}] = {};
} }

View File

@ -31,24 +31,33 @@
namespace yul namespace yul
{ {
struct CallGraph
{
std::map<YulString, std::set<YulString>> functionCalls;
std::set<YulString> functionsWithLoops;
};
/** /**
* Specific AST walker that generates the call graph. * Specific AST walker that generates the call graph.
* *
* It also generates information about which functions contain for loops.
*
* The outermost (non-function) context is denoted by the empty string. * The outermost (non-function) context is denoted by the empty string.
*/ */
class CallGraphGenerator: public ASTWalker class CallGraphGenerator: public ASTWalker
{ {
public: public:
static std::map<YulString, std::set<YulString>> callGraph(Block const& _ast); static CallGraph callGraph(Block const& _ast);
using ASTWalker::operator(); using ASTWalker::operator();
void operator()(FunctionCall const& _functionCall) override; void operator()(FunctionCall const& _functionCall) override;
void operator()(ForLoop const& _forLoop) override;
void operator()(FunctionDefinition const& _functionDefinition) override; void operator()(FunctionDefinition const& _functionDefinition) override;
private: private:
CallGraphGenerator(); CallGraphGenerator();
std::map<YulString, std::set<YulString>> m_callGraph; CallGraph m_callGraph;
/// The name of the function we are currently visiting during traversal. /// The name of the function we are currently visiting during traversal.
YulString m_currentFunction; YulString m_currentFunction;
}; };

View File

@ -93,11 +93,44 @@ void MSizeFinder::operator()(FunctionCall const& _functionCall)
map<YulString, SideEffects> SideEffectsPropagator::sideEffects( map<YulString, SideEffects> SideEffectsPropagator::sideEffects(
Dialect const& _dialect, Dialect const& _dialect,
map<YulString, std::set<YulString>> const& _directCallGraph CallGraph const& _directCallGraph
) )
{ {
// Any loop currently makes a function non-movable, because
// it could be a non-terminating loop.
// The same is true for any function part of a call cycle.
// In the future, we should refine that, because the property
// is actually a bit different from "not movable".
map<YulString, SideEffects> ret; map<YulString, SideEffects> ret;
for (auto const& call: _directCallGraph) for (auto const& function: _directCallGraph.functionsWithLoops)
{
ret[function].movable = false;
ret[function].sideEffectFree = false;
ret[function].sideEffectFreeIfNoMSize = false;
}
// Detect recursive functions.
for (auto const& call: _directCallGraph.functionCalls)
{
// TODO we could shortcut the search as soon as we find a
// function that has as bad side-effects as we can
// ever achieve via recursion.
auto search = [&](YulString const& _functionName, CycleDetector<YulString>& _cycleDetector, size_t) {
for (auto const& callee: _directCallGraph.functionCalls.at(_functionName))
if (!_dialect.builtin(callee))
if (_cycleDetector.run(callee))
return;
};
if (CycleDetector<YulString>(search).run(call.first))
{
ret[call.first].movable = false;
ret[call.first].sideEffectFree = false;
ret[call.first].sideEffectFreeIfNoMSize = false;
}
}
for (auto const& call: _directCallGraph.functionCalls)
{ {
YulString funName = call.first; YulString funName = call.first;
SideEffects sideEffects; SideEffects sideEffects;
@ -108,11 +141,15 @@ map<YulString, SideEffects> SideEffectsPropagator::sideEffects(
if (BuiltinFunction const* f = _dialect.builtin(_function)) if (BuiltinFunction const* f = _dialect.builtin(_function))
sideEffects += f->sideEffects; sideEffects += f->sideEffects;
else else
for (YulString callee: _directCallGraph.at(_function)) {
if (ret.count(_function))
sideEffects += ret[_function];
for (YulString callee: _directCallGraph.functionCalls.at(_function))
_addChild(callee); _addChild(callee);
} }
}
); );
ret[funName] = sideEffects; ret[funName] += sideEffects;
} }
return ret; return ret;
} }

View File

@ -22,6 +22,7 @@
#include <libyul/optimiser/ASTWalker.h> #include <libyul/optimiser/ASTWalker.h>
#include <libyul/SideEffects.h> #include <libyul/SideEffects.h>
#include <libyul/optimiser/CallGraphGenerator.h>
#include <libyul/AsmData.h> #include <libyul/AsmData.h>
#include <set> #include <set>
@ -85,7 +86,7 @@ class SideEffectsPropagator
public: public:
static std::map<YulString, SideEffects> sideEffects( static std::map<YulString, SideEffects> sideEffects(
Dialect const& _dialect, Dialect const& _dialect,
std::map<YulString, std::set<YulString>> const& _directCallGraph CallGraph const& _directCallGraph
); );
}; };

View File

@ -680,7 +680,8 @@ Allowed options)",
( (
g_strEVMVersion.c_str(), g_strEVMVersion.c_str(),
po::value<string>()->value_name("version"), po::value<string>()->value_name("version"),
"Select desired EVM version. Either homestead, tangerineWhistle, spuriousDragon, byzantium, constantinople, petersburg (default), istanbul or berlin." "Select desired EVM version. Either homestead, tangerineWhistle, spuriousDragon, "
"byzantium, constantinople, petersburg, istanbul (default) or berlin."
) )
(g_argOptimize.c_str(), "Enable bytecode optimizer.") (g_argOptimize.c_str(), "Enable bytecode optimizer.")
( (

View File

@ -900,9 +900,11 @@ BOOST_AUTO_TEST_CASE(evm_version)
BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"constantinople\"") != string::npos); BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"constantinople\"") != string::npos);
result = compile(inputForVersion("\"evmVersion\": \"petersburg\",")); result = compile(inputForVersion("\"evmVersion\": \"petersburg\","));
BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"petersburg\"") != string::npos); BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"petersburg\"") != string::npos);
result = compile(inputForVersion("\"evmVersion\": \"istanbul\","));
BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"istanbul\"") != string::npos);
// test default // test default
result = compile(inputForVersion("")); result = compile(inputForVersion(""));
BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"petersburg\"") != string::npos); BOOST_CHECK(result["contracts"]["fileA"]["A"]["metadata"].asString().find("\"evmVersion\":\"istanbul\"") != string::npos);
// test invalid // test invalid
result = compile(inputForVersion("\"evmVersion\": \"invalid\",")); result = compile(inputForVersion("\"evmVersion\": \"invalid\","));
BOOST_CHECK(result["errors"][0]["message"].asString() == "Invalid EVM version requested."); BOOST_CHECK(result["errors"][0]["message"].asString() == "Invalid EVM version requested.");

View File

@ -18,7 +18,7 @@ contract C {
// executionCost: 1160 // executionCost: 1160
// totalCost: 1121160 // totalCost: 1121160
// external: // external:
// a(): 530 // a(): 1130
// b(uint256): infinite // b(uint256): infinite
// f1(uint256): infinite // f1(uint256): infinite
// f2(uint256[],string[],uint16,address): infinite // f2(uint256[],string[],uint16,address): infinite

View File

@ -21,8 +21,8 @@ contract C {
// executionCost: 638 // executionCost: 638
// totalCost: 606438 // totalCost: 606438
// external: // external:
// a(): 429 // a(): 1029
// b(uint256): 884 // b(uint256): 2084
// f1(uint256): 351 // f1(uint256): 351
// f2(uint256[],string[],uint16,address): infinite // f2(uint256[],string[],uint16,address): infinite
// f3(uint16[],string[],uint16,address): infinite // f3(uint16[],string[],uint16,address): infinite

View File

@ -28,25 +28,25 @@ contract Large {
// executionCost: 670 // executionCost: 670
// totalCost: 637670 // totalCost: 637670
// external: // external:
// a(): 451 // a(): 1051
// b(uint256): 846 // b(uint256): 2046
// f0(uint256): 427 // f0(uint256): 427
// f1(uint256): 40752 // f1(uint256): 41352
// f2(uint256): 20693 // f2(uint256): 21293
// f3(uint256): 20781 // f3(uint256): 21381
// f4(uint256): 20759 // f4(uint256): 21359
// f5(uint256): 20737 // f5(uint256): 21337
// f6(uint256): 20760 // f6(uint256): 21360
// f7(uint256): 20672 // f7(uint256): 21272
// f8(uint256): 20672 // f8(uint256): 21272
// f9(uint256): 20694 // f9(uint256): 21294
// g0(uint256): 313 // g0(uint256): 313
// g1(uint256): 40707 // g1(uint256): 41307
// g2(uint256): 20670 // g2(uint256): 21270
// g3(uint256): 20758 // g3(uint256): 21358
// g4(uint256): 20736 // g4(uint256): 21336
// g5(uint256): 20692 // g5(uint256): 21292
// g6(uint256): 20715 // g6(uint256): 21315
// g7(uint256): 20714 // g7(uint256): 21314
// g8(uint256): 20692 // g8(uint256): 21292
// g9(uint256): 20649 // g9(uint256): 21249

View File

@ -31,25 +31,25 @@ contract Large {
// executionCost: 300 // executionCost: 300
// totalCost: 260900 // totalCost: 260900
// external: // external:
// a(): 398 // a(): 998
// b(uint256): 1105 // b(uint256): 2305
// f0(uint256): 334 // f0(uint256): 334
// f1(uint256): 40874 // f1(uint256): 41474
// f2(uint256): 20940 // f2(uint256): 21540
// f3(uint256): 21028 // f3(uint256): 21628
// f4(uint256): 21006 // f4(uint256): 21606
// f5(uint256): 20984 // f5(uint256): 21584
// f6(uint256): 20896 // f6(uint256): 21496
// f7(uint256): 20676 // f7(uint256): 21276
// f8(uint256): 20808 // f8(uint256): 21408
// f9(uint256): 20830 // f9(uint256): 21430
// g0(uint256): 574 // g0(uint256): 574
// g1(uint256): 40586 // g1(uint256): 41186
// g2(uint256): 20674 // g2(uint256): 21274
// g3(uint256): 20762 // g3(uint256): 21362
// g4(uint256): 20740 // g4(uint256): 21340
// g5(uint256): 20828 // g5(uint256): 21428
// g6(uint256): 20608 // g6(uint256): 21208
// g7(uint256): 20718 // g7(uint256): 21318
// g8(uint256): 20696 // g8(uint256): 21296
// g9(uint256): 20542 // g9(uint256): 21142

View File

@ -15,12 +15,12 @@ contract Medium {
// executionCost: 294 // executionCost: 294
// totalCost: 253494 // totalCost: 253494
// external: // external:
// a(): 428 // a(): 1028
// b(uint256): 846 // b(uint256): 2046
// f1(uint256): 40663 // f1(uint256): 41263
// f2(uint256): 20693 // f2(uint256): 21293
// f3(uint256): 20737 // f3(uint256): 21337
// g0(uint256): 313 // g0(uint256): 313
// g7(uint256): 20692 // g7(uint256): 21292
// g8(uint256): 20670 // g8(uint256): 21270
// g9(uint256): 20626 // g9(uint256): 21226

View File

@ -18,12 +18,12 @@ contract Medium {
// executionCost: 190 // executionCost: 190
// totalCost: 141190 // totalCost: 141190
// external: // external:
// a(): 398 // a(): 998
// b(uint256): 863 // b(uint256): 2063
// f1(uint256): 40654 // f1(uint256): 41254
// f2(uint256): 20698 // f2(uint256): 21298
// f3(uint256): 20742 // f3(uint256): 21342
// g0(uint256): 332 // g0(uint256): 332
// g7(uint256): 20608 // g7(uint256): 21208
// g8(uint256): 20586 // g8(uint256): 21186
// g9(uint256): 20542 // g9(uint256): 21142

View File

@ -11,6 +11,6 @@ contract Small {
// totalCost: 84935 // totalCost: 84935
// external: // external:
// fallback: 129 // fallback: 129
// a(): 383 // a(): 983
// b(uint256): 802 // b(uint256): 2002
// f1(uint256): 40663 // f1(uint256): 41263

View File

@ -14,6 +14,6 @@ contract Small {
// totalCost: 60711 // totalCost: 60711
// external: // external:
// fallback: 118 // fallback: 118
// a(): 376 // a(): 976
// b(uint256): 753 // b(uint256): 1953
// f1(uint256): 40588 // f1(uint256): 41188

View File

@ -87,7 +87,7 @@ TestCase::TestResult FunctionSideEffects::run(ostream& _stream, string const& _l
m_obtainedResult.clear(); m_obtainedResult.clear();
for (auto const& fun: functionSideEffectsStr) for (auto const& fun: functionSideEffectsStr)
m_obtainedResult += fun.first + ": " + fun.second + "\n"; m_obtainedResult += fun.first + ":" + (fun.second.empty() ? "" : " ") + fun.second + "\n";
if (m_expectation != m_obtainedResult) if (m_expectation != m_obtainedResult)
{ {

View File

@ -5,6 +5,6 @@
} }
// ---- // ----
// : movable, sideEffectFree, sideEffectFreeIfNoMSize // : movable, sideEffectFree, sideEffectFreeIfNoMSize
// a: movable, sideEffectFree, sideEffectFreeIfNoMSize // a:
// b: movable, sideEffectFree, sideEffectFreeIfNoMSize // b:
// c: movable, sideEffectFree, sideEffectFreeIfNoMSize // c:

View File

@ -4,5 +4,5 @@
} }
// ---- // ----
// : movable, sideEffectFree, sideEffectFreeIfNoMSize // : movable, sideEffectFree, sideEffectFreeIfNoMSize
// a: movable, sideEffectFree, sideEffectFreeIfNoMSize // a:
// b: movable, sideEffectFree, sideEffectFreeIfNoMSize // b:

View File

@ -3,4 +3,4 @@
} }
// ---- // ----
// : movable, sideEffectFree, sideEffectFreeIfNoMSize // : movable, sideEffectFree, sideEffectFreeIfNoMSize
// a: movable, sideEffectFree, sideEffectFreeIfNoMSize // a:

View File

@ -0,0 +1,9 @@
{
function f() -> x { x := g() }
function g() -> x { for {} 1 {} {} }
pop(f())
}
// ----
// :
// f:
// g:

View File

@ -477,16 +477,15 @@
// pos := add(pos, 0x60) // pos := add(pos, 0x60)
// } // }
// let _3 := mload(64) // let _3 := mload(64)
// let _4 := mload(0x20) // if slt(sub(_3, length), 128) { revert(_1, _1) }
// if slt(sub(_3, _4), 128) { revert(_1, _1) } // let offset := calldataload(add(length, 64))
// let offset := calldataload(add(_4, 64)) // let _4 := 0xffffffffffffffff
// let _5 := 0xffffffffffffffff // if gt(offset, _4) { revert(_1, _1) }
// if gt(offset, _5) { revert(_1, _1) } // let value2 := abi_decode_t_array$_t_uint256_$dyn_memory_ptr(add(length, offset), _3)
// let value2 := abi_decode_t_array$_t_uint256_$dyn_memory_ptr(add(_4, offset), _3) // let offset_1 := calldataload(add(length, 0x60))
// let offset_1 := calldataload(add(_4, 0x60)) // if gt(offset_1, _4) { revert(_1, _1) }
// if gt(offset_1, _5) { revert(_1, _1) } // let value3 := abi_decode_t_array$_t_array$_t_uint256_$2_memory_$dyn_memory_ptr(add(length, offset_1), _3)
// let value3 := abi_decode_t_array$_t_array$_t_uint256_$2_memory_$dyn_memory_ptr(add(_4, offset_1), _3) // sstore(calldataload(length), calldataload(add(length, 0x20)))
// sstore(calldataload(_4), calldataload(add(_4, 0x20)))
// sstore(value2, value3) // sstore(value2, value3)
// sstore(_1, pos) // sstore(_1, pos)
// } // }

View File

@ -0,0 +1,24 @@
{
for {} msize() {
function foo_s_0() -> x_1 { for {} caller() {} {} }
// x_3 used to be a movable loop invariant because `foo_s_0()` used to be movable
let x_3 := foo_s_0()
mstore(192, x_3)
}
{}
}
// ====
// step: fullSuite
// ----
// {
// {
// for { }
// 1
// {
// for { } caller() { }
// { }
// mstore(192, 0)
// }
// { if iszero(msize()) { break } }
// }
// }

View File

@ -0,0 +1,29 @@
{
function f() -> x { x := g() }
function g() -> x { for {} 1 {} {} }
let b := 1
for { let a := 1 } iszero(eq(a, 10)) { a := add(a, 1) } {
let t := f()
let q := g()
}
}
// ====
// step: loopInvariantCodeMotion
// ----
// {
// function f() -> x
// { x := g() }
// function g() -> x_1
// {
// for { } 1 { }
// { }
// }
// let b := 1
// let a := 1
// for { } iszero(eq(a, 10)) { a := add(a, 1) }
// {
// let t := f()
// let q := g()
// }
// }

View File

@ -0,0 +1,26 @@
{
function f() -> x { x := g() }
function g() -> x { x := g() }
let b := 1
for { let a := 1 } iszero(eq(a, 10)) { a := add(a, 1) } {
let t := f()
let q := g()
}
}
// ====
// step: loopInvariantCodeMotion
// ----
// {
// function f() -> x
// { x := g() }
// function g() -> x_1
// { x_1 := g() }
// let b := 1
// let a := 1
// for { } iszero(eq(a, 10)) { a := add(a, 1) }
// {
// let t := f()
// let q := g()
// }
// }