Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Uniswap: summary of initialization of configuration #30

Merged
merged 9 commits into from
Sep 12, 2024
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -82,6 +82,6 @@ $(REGRESSION_TESTS): %.out: %.sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/ti
test-examples: ${EXAMPLE_TESTS}

.SECONDEXPANSION:
$(EXAMPLE_TESTS): %.out: $$(subst $(TRANSACTIONS_DIR), $(EXAMPLES_DIR), $$(@D)).sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/timestamp
ulimit -s 65536 && bin/krun-sol $< $*.txn > $*.out 2>&1
$(EXAMPLE_TESTS): %.out: $$(subst $(TRANSACTIONS_DIR), $(EXAMPLES_DIR), $$(@D)).sol %.txn %.ref %.smr $(SEMANTICS_FILE_NAME)-kompiled/timestamp
ulimit -s 65536 && bin/krun-sol $< $*.txn $*.smr > $*.out 2>&1
diff -U3 -w $*.ref $*.out
2 changes: 2 additions & 0 deletions bin/kparse-bool
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
#!/bin/bash
kparse -d "$(dirname "$0")/../solidity-kompiled" -s Bool -m SOLIDITY-DATA-SYNTAX "$(cat "$1")"
14 changes: 13 additions & 1 deletion bin/krun-sol
Original file line number Diff line number Diff line change
@@ -1,5 +1,17 @@
#!/bin/bash
contract="$1"
txn="$2"

if [ "$#" -lt 3 ]; then
isuniswap=""
else
isuniswap="$3"
shift
fi
shift; shift
krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" --no-expand-macros "$@"

if [ -z "${isuniswap}" ]; then
krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="false" --no-expand-macros "$@"
else
krun -d "$(dirname "$0")/../solidity-kompiled" "$contract" -cTXN="$txn" -pTXN="$(dirname "$0")/kparse-txn" -cISUNISWAP="$isuniswap" -pISUNISWAP="$(dirname "$0")/kparse-bool" --no-expand-macros "$@"
fi
6 changes: 5 additions & 1 deletion src/solidity.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ requires "contract.md"
requires "transaction.md"
requires "expression.md"
requires "statement.md"
requires "uniswap-summaries.md"

module SOLIDITY-CONFIGURATION
imports SOLIDITY-DATA
Expand All @@ -17,6 +18,7 @@ module SOLIDITY-CONFIGURATION
configuration
<solidity>
<k parser="TXN, SOLIDITY-DATA-SYNTAX"> $PGM:Program ~> $TXN:Transactions </k>
<summarize> $ISUNISWAP:Bool </summarize>
<compile>
<current-body> Id </current-body>
<ifaces>
Expand Down Expand Up @@ -178,8 +180,10 @@ module SOLIDITY
imports SOLIDITY-TRANSACTION
imports SOLIDITY-EXPRESSION
imports SOLIDITY-STATEMENT
imports SOLIDITY-UNISWAP-INIT-SUMMARY

rule _:PragmaDefinition Ss:SourceUnits => Ss
rule <k> _:PragmaDefinition Ss:SourceUnits => Ss ...</k>
<summarize> false </summarize>
rule S:SourceUnit Ss:SourceUnits => S ~> Ss
rule .SourceUnits => .K
rule C:ContractBodyElement Cc:ContractBodyElements => C ~> Cc
Expand Down
2,399 changes: 2,399 additions & 0 deletions src/uniswap-summaries.md

Large diffs are not rendered by default.

3 changes: 3 additions & 0 deletions test/regression/arithmetic.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
TestArithmetic
Expand Down
3 changes: 3 additions & 0 deletions test/regression/arraystestcontract.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
TestArraysContract
Expand Down
3 changes: 3 additions & 0 deletions test/regression/block.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
BlockTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/boolean.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
BoolTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/contract.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
UniswapV2Swap
Expand Down
3 changes: 3 additions & 0 deletions test/regression/emit.ref
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,9 @@ Approval(1, 0, 2)
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
EmitTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/eventtestcontract.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
TestEventsContract
Expand Down
3 changes: 3 additions & 0 deletions test/regression/for.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
ForTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/function.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
UniswapV2SwapTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/if.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
IfTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/increment.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
IncTest
Expand Down
3 changes: 3 additions & 0 deletions test/regression/mapstestcontract.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,9 @@
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
TestMapsContract
Expand Down
3 changes: 3 additions & 0 deletions test/regression/swaps.ref
Original file line number Diff line number Diff line change
Expand Up @@ -15002,6 +15002,9 @@ Swap(7, 1000000000000000000, 0, 0, 332669001559828603, 2)
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
UniswapV2SwapTest
Expand Down
3 changes: 3 additions & 0 deletions test/transactions/swaps/UniswapV2Swap/UniswapTest.ref
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,9 @@ Transfer(6, 2, 1999999999998955749)
<k>
.K
</k>
<summarize>
false
</summarize>
<compile>
<current-body>
UniswapV2SwapTest
Expand Down
1 change: 1 addition & 0 deletions test/transactions/swaps/UniswapV2Swap/UniswapTest.smr
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
false
Original file line number Diff line number Diff line change
Expand Up @@ -99,6 +99,9 @@ transferEvent(6, 2, 1999999999998955749)
<k>
.K
</k>
<summarize>
true
</summarize>
<compile>
<current-body>
uniswapV2SwapTest
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
true