From b61691a4c5f30a30efeebe04499c29cefb3397c7 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Tue, 3 Sep 2024 15:26:18 -0500 Subject: [PATCH] Revert "For loops (#21)" This reverts commit 03488cb70dd31e53c5616897b8954a58fe514e03. --- src/solidity-syntax.md | 9 ++-- src/statement.md | 3 -- test/regression/for.ref | 100 ----------------------------------- test/regression/for.sol | 14 ----- test/regression/for.txn | 1 - test/regression/function.ref | 6 +-- 6 files changed, 8 insertions(+), 125 deletions(-) delete mode 100644 test/regression/for.ref delete mode 100644 test/regression/for.sol delete mode 100644 test/regression/for.txn diff --git a/src/solidity-syntax.md b/src/solidity-syntax.md index 71a3205..61035bc 100644 --- a/src/solidity-syntax.md +++ b/src/solidity-syntax.md @@ -168,7 +168,7 @@ In each code block, various statments and nested blocks can be present. | VariableDeclarationStatement | ExpressionStatement | IfStatement - | WhileStatement + | ForStatement | EmitStatement | ReturnStatement | RevertStatement @@ -188,9 +188,10 @@ Following is a list of supported statements. syntax IfStatement ::= "if" "(" Expression ")" Statement [strict(1)] | "if" "(" Expression ")" Statement "else" Statement [avoid, strict(1)] - syntax WhileStatement ::= "while" "(" Expression ")" Statement - syntax Block ::= "for" "(" VariableDeclarationStatement Expression ";" Expression ")" Statement [function] - rule for (Init Cond ; Post) Body => { Init while(Cond) { Body Post; } } + syntax ForStatement ::= "for" "(" InitStatement ConditionStatement PostLoopStatement ")" Statement + syntax InitStatement ::= VariableDeclarationStatement | ExpressionStatement | ";" + syntax ConditionStatement ::= ExpressionStatement | ";" + syntax PostLoopStatement ::= Expression | "" syntax EmitStatement ::= "emit" Expression "(" CallArgumentList ")" ";" [strict(2)] diff --git a/src/statement.md b/src/statement.md index c26453e..37b2d7f 100644 --- a/src/statement.md +++ b/src/statement.md @@ -45,7 +45,4 @@ module SOLIDITY-STATEMENT rule restoreEnv(E) => .K ... _ => E - // while statement - rule while (Cond) Body => if (Cond) {Body while(Cond) Body} else {.Statements} - endmodule diff --git a/test/regression/for.ref b/test/regression/for.ref deleted file mode 100644 index e95ea60..0000000 --- a/test/regression/for.ref +++ /dev/null @@ -1,100 +0,0 @@ - - - .K - - - ForTest - - - .IfaceCellMap - - - - - ForTest - - - .Map - - - .List - - - - - constructor - - - public - - - .List - - - .List - - - .List - - - .List - - - uint256 x = 5 ; uint256 y = 0 ; { uint256 x = 0 ; while ( x < 10 ) { { y = y + 2 ; .Statements } x = x + 1 ; .Statements } .Statements } require ( y == 20 , "" , .TypedVals ) ; require ( x == 5 , "" , .TypedVals ) ; .Statements - - - - - .ContractEventCellMap - - - - - - 1p160 - - - 0p256 - - - 1p160 - - - 2p160 - - - ForTest - - - x |-> var ( 0 , uint256 ) - y |-> var ( 1 , uint256 ) - - - 0 |-> 5p256 - 1 |-> 20p256 - 2 |-> 10p256 - - - .List - - - - - 2p160 - - - ForTest - - - .Map - - - - - .List - - - 3p160 - - - diff --git a/test/regression/for.sol b/test/regression/for.sol deleted file mode 100644 index 81abc3c..0000000 --- a/test/regression/for.sol +++ /dev/null @@ -1,14 +0,0 @@ -pragma solidity ^0.8.24; - -contract ForTest { - - constructor() { - uint x = 5; - uint y = 0; - for (uint x = 0; x < 10; x = x + 1) { - y = y + 2; - } - require(y == 20, ""); - require(x == 5, ""); - } -} diff --git a/test/regression/for.txn b/test/regression/for.txn deleted file mode 100644 index b324409..0000000 --- a/test/regression/for.txn +++ /dev/null @@ -1 +0,0 @@ -create(1, 0, ForTest, ) diff --git a/test/regression/function.ref b/test/regression/function.ref index b6cee27..b27ccbc 100644 --- a/test/regression/function.ref +++ b/test/regression/function.ref @@ -987,7 +987,7 @@ .List - { uint256 i ; while ( i < path . length - 1 ) { { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2Library_sortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2Library_pairFor ( output , path [ i + 2 ] , .TypedVals ) : _to ; UniswapV2Pair ( uniswapV2Library_pairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + for ( uint256 i ; i < path . length - 1 ; i ++ ) { address input = path [ i ] ; address output = path [ i + 1 ] ; address [ ] memory tokens = uniswapV2Library_sortTokens ( input , output , .TypedVals ) ; uint256 amountOut = amounts [ i + 1 ] ; uint256 amount0Out = input == tokens [ 0 ] ? uint256 ( 0 , .TypedVals ) : amountOut ; uint256 amount1Out = input == tokens [ 0 ] ? amountOut : uint256 ( 0 , .TypedVals ) ; address to = i < path . length - 2 ? uniswapV2Library_pairFor ( output , path [ i + 2 ] , .TypedVals ) : _to ; UniswapV2Pair ( uniswapV2Library_pairFor ( input , output , .TypedVals ) , .TypedVals ) . swap ( amount0Out , amount1Out , to , .TypedVals ) ; .Statements } .Statements @@ -1213,7 +1213,7 @@ ListItem ( amounts ) - require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; { uint256 i = path . length - 1 ; while ( i > 0 ) { { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2Library_getAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i -- ; .Statements } .Statements } .Statements + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ amounts . length - 1 ] = amountOut ; for ( uint256 i = path . length - 1 ; i > 0 ; i -- ) { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i - 1 ] , path [ i ] , .TypedVals ) ; amounts [ i - 1 ] = uniswapV2Library_getAmountIn ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } .Statements @@ -1237,7 +1237,7 @@ ListItem ( amounts ) - require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; { uint256 i ; while ( i < path . length - 1 ) { { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2Library_getAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } i ++ ; .Statements } .Statements } .Statements + require ( path . length >= 2 , "UniswapV2Library: INVALID_PATH" , .TypedVals ) ; amounts = new uint256 [ ] ( path . length , .TypedVals ) ; amounts [ 0 ] = amountIn ; for ( uint256 i ; i < path . length - 1 ; i ++ ) { uint256 [ ] memory reserves = uniswapV2Library_getReserves ( path [ i ] , path [ i + 1 ] , .TypedVals ) ; amounts [ i + 1 ] = uniswapV2Library_getAmountOut ( amounts [ i ] , reserves [ 0 ] , reserves [ 1 ] , .TypedVals ) ; .Statements } .Statements