Skip to content

Commit

Permalink
Misc fixes (#25)
Browse files Browse the repository at this point in the history
* fix call to interface

* fix bug in internal call

* add assert

* retesteth tests for uniswap

* add compile cell

* update test outputs

* diff without whitespace

* add test output

* fix test output

* set ulimit
  • Loading branch information
dwightguth authored Sep 4, 2024
1 parent bd3e161 commit eea9f8c
Show file tree
Hide file tree
Showing 23 changed files with 24,646 additions and 3,171 deletions.
4 changes: 2 additions & 2 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -64,5 +64,5 @@ test-aave:
test-regression: ${REGRESSION_TESTS}

%.out: %.sol %.txn %.ref $(SEMANTICS_FILE_NAME)-kompiled/timestamp
bin/krun-sol $*.sol $*.txn > $*.out
diff -U3 $*.ref $*.out
ulimit -s 65536 && bin/krun-sol $*.sol $*.txn > $*.out
diff -U3 -w $*.ref $*.out
4 changes: 4 additions & 0 deletions bin/fill-tests
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
#!/bin/bash -ex
dretesteth.sh -t GeneralStateTests -- --clients t8ntool --fillchain --filltests --testfile /tests/swaps/uniswap01Filler.yml --testpath "$(realpath "$(dirname "$0")/../test/retesteth/")"
dretesteth.sh -t GeneralStateTests -- --clients t8ntool --fillchain --filltests --testfile /tests/swaps/uniswap02Filler.yml --testpath "$(realpath "$(dirname "$0")/../test/retesteth/")"
sudo chown -R "$USER":"$(id -gn)" test/retesteth/swaps/filled
7 changes: 5 additions & 2 deletions src/expression.md
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ module SOLIDITY-EXPRESSION
// external call
context HOLE . _ ( _:CallArgumentList )
context (_ . _) ( HOLE:CallArgumentList )
rule <k> v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
rule <k> v(ADDR, _) . F:Id ( ARGS ) ~> K => bind(S, PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
<msg-sender> FROM => THIS </msg-sender>
<msg-value> VALUE => 0p256 </msg-value>
<this> THIS => ADDR </this>
Expand Down Expand Up @@ -235,6 +235,8 @@ module SOLIDITY-EXPRESSION
<env> E => .Map </env>
<store> S </store>
<call-stack>... .List => ListItem(frame(K, E)) </call-stack>
<this-type> TYPE </this-type>
<contract-id> TYPE </contract-id>
<contract-fn-id> F </contract-fn-id>
<contract-fn-param-names> PARAMS </contract-fn-param-names>
<contract-fn-arg-types> TYPES </contract-fn-arg-types>
Expand Down Expand Up @@ -344,8 +346,9 @@ module SOLIDITY-EXPRESSION
rule I1:Int >= I2:Int => v(I1 >=Int I2, bool)
// require expression
syntax Id ::= "require" [token]
syntax Id ::= "require" [token] | "assert" [token]
rule require(v(true, bool), _) => void
rule assert(v(true, bool)) => void
// ternary expression
rule v(true, bool) ? X : _ => X
Expand Down
82 changes: 42 additions & 40 deletions src/solidity.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,46 +17,48 @@ module SOLIDITY-CONFIGURATION
configuration
<solidity>
<k parser="TXN, SOLIDITY-DATA-SYNTAX"> $PGM:Program ~> $TXN:Transactions </k>
<current-body> Id </current-body>
<ifaces>
<iface multiplicity="*" type="Map">
<iface-id> Id </iface-id>
<iface-fns>
<iface-fn multiplicity="*" type="Map">
<iface-fn-id> Id </iface-fn-id>
<iface-fn-arg-types> .List </iface-fn-arg-types>
<iface-fn-return-types> .List </iface-fn-return-types>
</iface-fn>
</iface-fns>
</iface>
</ifaces>
<contracts>
<contract multiplicity="*" type="Map">
<contract-id> Id </contract-id>
<contract-state> .Map </contract-state>
<contract-init> .List </contract-init>
<contract-fns>
<contract-fn multiplicity="*" type="Map">
<contract-fn-id> Id </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<contract-fn-arg-types> .List </contract-fn-arg-types>
<contract-fn-param-names> .List </contract-fn-param-names>
<contract-fn-return-types> .List </contract-fn-return-types>
<contract-fn-return-names> .List </contract-fn-return-names>
<contract-fn-payable> false </contract-fn-payable>
<contract-fn-body> .Statements </contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
<contract-event multiplicity="*" type="Map">
<contract-event-id> Id </contract-event-id>
<contract-event-arg-types> .List </contract-event-arg-types>
<contract-event-param-names> .List </contract-event-param-names>
<contract-event-indexed-pos> .Set </contract-event-indexed-pos>
</contract-event>
</contract-events>
</contract>
</contracts>
<compile>
<current-body> Id </current-body>
<ifaces>
<iface multiplicity="*" type="Map">
<iface-id> Id </iface-id>
<iface-fns>
<iface-fn multiplicity="*" type="Map">
<iface-fn-id> Id </iface-fn-id>
<iface-fn-arg-types> .List </iface-fn-arg-types>
<iface-fn-return-types> .List </iface-fn-return-types>
</iface-fn>
</iface-fns>
</iface>
</ifaces>
<contracts>
<contract multiplicity="*" type="Map">
<contract-id> Id </contract-id>
<contract-state> .Map </contract-state>
<contract-init> .List </contract-init>
<contract-fns>
<contract-fn multiplicity="*" type="Map">
<contract-fn-id> Id </contract-fn-id>
<contract-fn-visibility> public </contract-fn-visibility>
<contract-fn-arg-types> .List </contract-fn-arg-types>
<contract-fn-param-names> .List </contract-fn-param-names>
<contract-fn-return-types> .List </contract-fn-return-types>
<contract-fn-return-names> .List </contract-fn-return-names>
<contract-fn-payable> false </contract-fn-payable>
<contract-fn-body> .Statements </contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
<contract-event multiplicity="*" type="Map">
<contract-event-id> Id </contract-event-id>
<contract-event-arg-types> .List </contract-event-arg-types>
<contract-event-param-names> .List </contract-event-param-names>
<contract-event-indexed-pos> .Set </contract-event-indexed-pos>
</contract-event>
</contract-events>
</contract>
</contracts>
</compile>
<exec>
<msg-sender> 0p160 </msg-sender>
<msg-value> 0p256 </msg-value>
Expand Down
102 changes: 52 additions & 50 deletions test/regression/arithmetic.ref
Original file line number Diff line number Diff line change
Expand Up @@ -2,56 +2,58 @@
<k>
.K
</k>
<current-body>
TestArithmetic
</current-body>
<ifaces>
.IfaceCellMap
</ifaces>
<contracts>
<contract>
<contract-id>
TestArithmetic
</contract-id>
<contract-state>
.Map
</contract-state>
<contract-init>
.List
</contract-init>
<contract-fns>
<contract-fn>
<contract-fn-id>
constructor
</contract-fn-id>
<contract-fn-visibility>
public
</contract-fn-visibility>
<contract-fn-arg-types>
.List
</contract-fn-arg-types>
<contract-fn-param-names>
.List
</contract-fn-param-names>
<contract-fn-return-types>
.List
</contract-fn-return-types>
<contract-fn-return-names>
.List
</contract-fn-return-names>
<contract-fn-payable>
false
</contract-fn-payable>
<contract-fn-body>
uint8 i8_1 = 2 ; uint8 i8_2 = 2 ; uint8 i32_1 = 2 ; uint8 i32_2 = 2 ; uint8 i112_1 = 2 ; uint8 i112_2 = 2 ; uint8 i256_1 = 2 ; uint8 i256_2 = 2 ; require ( i8_1 + i8_2 == 4 , "" , .TypedVals ) ; require ( i32_1 + i32_2 == 4 , "" , .TypedVals ) ; require ( i112_1 + i112_2 == 4 , "" , .TypedVals ) ; require ( i256_1 + i256_2 == 4 , "" , .TypedVals ) ; require ( i8_1 + 2 == 4 , "" , .TypedVals ) ; require ( 2 + i8_2 == 4 , "" , .TypedVals ) ; require ( 2 + 2 == 4 , "" , .TypedVals ) ; require ( i8_1 - i8_2 == 0 , "" , .TypedVals ) ; require ( i32_1 - i32_2 == 0 , "" , .TypedVals ) ; require ( i112_1 - i112_2 == 0 , "" , .TypedVals ) ; require ( i256_1 - i256_2 == 0 , "" , .TypedVals ) ; require ( i8_1 - 2 == 0 , "" , .TypedVals ) ; require ( 2 - i8_2 == 0 , "" , .TypedVals ) ; require ( 2 - 2 == 0 , "" , .TypedVals ) ; require ( i8_1 * i8_2 == 4 , "" , .TypedVals ) ; require ( i32_1 * i32_2 == 4 , "" , .TypedVals ) ; require ( i112_1 * i112_2 == 4 , "" , .TypedVals ) ; require ( i256_1 * i256_2 == 4 , "" , .TypedVals ) ; require ( i8_1 * 2 == 4 , "" , .TypedVals ) ; require ( 2 * i8_2 == 4 , "" , .TypedVals ) ; require ( 2 * 2 == 4 , "" , .TypedVals ) ; require ( i8_1 / i8_2 == 1 , "" , .TypedVals ) ; require ( i32_1 / i32_2 == 1 , "" , .TypedVals ) ; require ( i112_1 / i112_2 == 1 , "" , .TypedVals ) ; require ( i256_1 / i256_2 == 1 , "" , .TypedVals ) ; require ( i8_1 / 2 == 1 , "" , .TypedVals ) ; require ( 2 / i8_2 == 1 , "" , .TypedVals ) ; require ( 2 / 2 == 1 , "" , .TypedVals ) ; require ( i8_1 == i8_2 , "" , .TypedVals ) ; require ( i32_1 == i32_2 , "" , .TypedVals ) ; require ( i112_1 == i112_2 , "" , .TypedVals ) ; require ( i256_1 == i256_2 , "" , .TypedVals ) ; require ( 2 == i8_2 , "" , .TypedVals ) ; require ( 2 == 2 , "" , .TypedVals ) ; require ( i8_1 <= i8_2 , "" , .TypedVals ) ; require ( i32_1 <= i32_2 , "" , .TypedVals ) ; require ( i112_1 <= i112_2 , "" , .TypedVals ) ; require ( i256_1 <= i256_2 , "" , .TypedVals ) ; require ( i8_1 <= 2 , "" , .TypedVals ) ; require ( 2 <= i8_2 , "" , .TypedVals ) ; require ( 2 <= 2 , "" , .TypedVals ) ; require ( i8_1 >= i8_2 , "" , .TypedVals ) ; require ( i32_1 >= i32_2 , "" , .TypedVals ) ; require ( i112_1 >= i112_2 , "" , .TypedVals ) ; require ( i256_1 >= i256_2 , "" , .TypedVals ) ; require ( i8_1 >= 2 , "" , .TypedVals ) ; require ( 2 >= i8_2 , "" , .TypedVals ) ; require ( 2 >= 2 , "" , .TypedVals ) ; i8_2 = 4 ; i32_2 = 4 ; i112_2 = 4 ; i256_2 = 4 ; require ( i8_1 ** i8_2 == 16 , "" , .TypedVals ) ; require ( i32_1 ** i32_2 == 16 , "" , .TypedVals ) ; require ( i112_1 ** i112_2 == 16 , "" , .TypedVals ) ; require ( i256_1 ** i256_2 == 16 , "" , .TypedVals ) ; require ( i8_1 ** 4 == 16 , "" , .TypedVals ) ; require ( 2 ** i8_2 == 16 , "" , .TypedVals ) ; require ( 2 ** 4 == 16 , "" , .TypedVals ) ; require ( i8_1 < i8_2 , "" , .TypedVals ) ; require ( i32_1 < i32_2 , "" , .TypedVals ) ; require ( i112_1 < i112_2 , "" , .TypedVals ) ; require ( i256_1 < i256_2 , "" , .TypedVals ) ; require ( i8_1 < 4 , "" , .TypedVals ) ; require ( 2 < i8_2 , "" , .TypedVals ) ; require ( 2 < 4 , "" , .TypedVals ) ; require ( i8_1 != i8_2 , "" , .TypedVals ) ; require ( i32_1 != i32_2 , "" , .TypedVals ) ; require ( i112_1 != i112_2 , "" , .TypedVals ) ; require ( i256_1 != i256_2 , "" , .TypedVals ) ; require ( i8_1 != 4 , "" , .TypedVals ) ; require ( 2 != i8_2 , "" , .TypedVals ) ; require ( 2 != 4 , "" , .TypedVals ) ; require ( i8_2 > i8_1 , "" , .TypedVals ) ; require ( i32_2 > i32_1 , "" , .TypedVals ) ; require ( i112_2 > i112_1 , "" , .TypedVals ) ; require ( i256_2 > i256_1 , "" , .TypedVals ) ; require ( i8_2 > 2 , "" , .TypedVals ) ; require ( 4 > i8_1 , "" , .TypedVals ) ; require ( 4 > 2 , "" , .TypedVals ) ; .Statements
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
.ContractEventCellMap
</contract-events>
</contract>
</contracts>
<compile>
<current-body>
TestArithmetic
</current-body>
<ifaces>
.IfaceCellMap
</ifaces>
<contracts>
<contract>
<contract-id>
TestArithmetic
</contract-id>
<contract-state>
.Map
</contract-state>
<contract-init>
.List
</contract-init>
<contract-fns>
<contract-fn>
<contract-fn-id>
constructor
</contract-fn-id>
<contract-fn-visibility>
public
</contract-fn-visibility>
<contract-fn-arg-types>
.List
</contract-fn-arg-types>
<contract-fn-param-names>
.List
</contract-fn-param-names>
<contract-fn-return-types>
.List
</contract-fn-return-types>
<contract-fn-return-names>
.List
</contract-fn-return-names>
<contract-fn-payable>
false
</contract-fn-payable>
<contract-fn-body>
uint8 i8_1 = 2 ; uint8 i8_2 = 2 ; uint8 i32_1 = 2 ; uint8 i32_2 = 2 ; uint8 i112_1 = 2 ; uint8 i112_2 = 2 ; uint8 i256_1 = 2 ; uint8 i256_2 = 2 ; require ( i8_1 + i8_2 == 4 , "" , .TypedVals ) ; require ( i32_1 + i32_2 == 4 , "" , .TypedVals ) ; require ( i112_1 + i112_2 == 4 , "" , .TypedVals ) ; require ( i256_1 + i256_2 == 4 , "" , .TypedVals ) ; require ( i8_1 + 2 == 4 , "" , .TypedVals ) ; require ( 2 + i8_2 == 4 , "" , .TypedVals ) ; require ( 2 + 2 == 4 , "" , .TypedVals ) ; require ( i8_1 - i8_2 == 0 , "" , .TypedVals ) ; require ( i32_1 - i32_2 == 0 , "" , .TypedVals ) ; require ( i112_1 - i112_2 == 0 , "" , .TypedVals ) ; require ( i256_1 - i256_2 == 0 , "" , .TypedVals ) ; require ( i8_1 - 2 == 0 , "" , .TypedVals ) ; require ( 2 - i8_2 == 0 , "" , .TypedVals ) ; require ( 2 - 2 == 0 , "" , .TypedVals ) ; require ( i8_1 * i8_2 == 4 , "" , .TypedVals ) ; require ( i32_1 * i32_2 == 4 , "" , .TypedVals ) ; require ( i112_1 * i112_2 == 4 , "" , .TypedVals ) ; require ( i256_1 * i256_2 == 4 , "" , .TypedVals ) ; require ( i8_1 * 2 == 4 , "" , .TypedVals ) ; require ( 2 * i8_2 == 4 , "" , .TypedVals ) ; require ( 2 * 2 == 4 , "" , .TypedVals ) ; require ( i8_1 / i8_2 == 1 , "" , .TypedVals ) ; require ( i32_1 / i32_2 == 1 , "" , .TypedVals ) ; require ( i112_1 / i112_2 == 1 , "" , .TypedVals ) ; require ( i256_1 / i256_2 == 1 , "" , .TypedVals ) ; require ( i8_1 / 2 == 1 , "" , .TypedVals ) ; require ( 2 / i8_2 == 1 , "" , .TypedVals ) ; require ( 2 / 2 == 1 , "" , .TypedVals ) ; require ( i8_1 == i8_2 , "" , .TypedVals ) ; require ( i32_1 == i32_2 , "" , .TypedVals ) ; require ( i112_1 == i112_2 , "" , .TypedVals ) ; require ( i256_1 == i256_2 , "" , .TypedVals ) ; require ( 2 == i8_2 , "" , .TypedVals ) ; require ( 2 == 2 , "" , .TypedVals ) ; require ( i8_1 <= i8_2 , "" , .TypedVals ) ; require ( i32_1 <= i32_2 , "" , .TypedVals ) ; require ( i112_1 <= i112_2 , "" , .TypedVals ) ; require ( i256_1 <= i256_2 , "" , .TypedVals ) ; require ( i8_1 <= 2 , "" , .TypedVals ) ; require ( 2 <= i8_2 , "" , .TypedVals ) ; require ( 2 <= 2 , "" , .TypedVals ) ; require ( i8_1 >= i8_2 , "" , .TypedVals ) ; require ( i32_1 >= i32_2 , "" , .TypedVals ) ; require ( i112_1 >= i112_2 , "" , .TypedVals ) ; require ( i256_1 >= i256_2 , "" , .TypedVals ) ; require ( i8_1 >= 2 , "" , .TypedVals ) ; require ( 2 >= i8_2 , "" , .TypedVals ) ; require ( 2 >= 2 , "" , .TypedVals ) ; i8_2 = 4 ; i32_2 = 4 ; i112_2 = 4 ; i256_2 = 4 ; require ( i8_1 ** i8_2 == 16 , "" , .TypedVals ) ; require ( i32_1 ** i32_2 == 16 , "" , .TypedVals ) ; require ( i112_1 ** i112_2 == 16 , "" , .TypedVals ) ; require ( i256_1 ** i256_2 == 16 , "" , .TypedVals ) ; require ( i8_1 ** 4 == 16 , "" , .TypedVals ) ; require ( 2 ** i8_2 == 16 , "" , .TypedVals ) ; require ( 2 ** 4 == 16 , "" , .TypedVals ) ; require ( i8_1 < i8_2 , "" , .TypedVals ) ; require ( i32_1 < i32_2 , "" , .TypedVals ) ; require ( i112_1 < i112_2 , "" , .TypedVals ) ; require ( i256_1 < i256_2 , "" , .TypedVals ) ; require ( i8_1 < 4 , "" , .TypedVals ) ; require ( 2 < i8_2 , "" , .TypedVals ) ; require ( 2 < 4 , "" , .TypedVals ) ; require ( i8_1 != i8_2 , "" , .TypedVals ) ; require ( i32_1 != i32_2 , "" , .TypedVals ) ; require ( i112_1 != i112_2 , "" , .TypedVals ) ; require ( i256_1 != i256_2 , "" , .TypedVals ) ; require ( i8_1 != 4 , "" , .TypedVals ) ; require ( 2 != i8_2 , "" , .TypedVals ) ; require ( 2 != 4 , "" , .TypedVals ) ; require ( i8_2 > i8_1 , "" , .TypedVals ) ; require ( i32_2 > i32_1 , "" , .TypedVals ) ; require ( i112_2 > i112_1 , "" , .TypedVals ) ; require ( i256_2 > i256_1 , "" , .TypedVals ) ; require ( i8_2 > 2 , "" , .TypedVals ) ; require ( 4 > i8_1 , "" , .TypedVals ) ; require ( 4 > 2 , "" , .TypedVals ) ; .Statements
</contract-fn-body>
</contract-fn>
</contract-fns>
<contract-events>
.ContractEventCellMap
</contract-events>
</contract>
</contracts>
</compile>
<exec>
<msg-sender>
1p160
Expand Down
Loading

0 comments on commit eea9f8c

Please sign in to comment.