Skip to content

Commit

Permalink
Minor optimizations (#31)
Browse files Browse the repository at this point in the history
* optimize decision tree heuristic

* optimize isKResult

* discard events for now rather than printing them

* use bison parser for config var

* update out files
  • Loading branch information
dwightguth authored Sep 12, 2024
1 parent c01a219 commit b8d3e5e
Show file tree
Hide file tree
Showing 9 changed files with 9 additions and 15,202 deletions.
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ TRANSACTIONS = $(shell find $(TRANSACTIONS_DIR) -name "*.txn")
EXAMPLE_TESTS = $(patsubst %.txn, %.out, $(TRANSACTIONS))

build: $(SEMANTICS_DIR)/$(SEMANTICS_FILE)
kompile $(SEMANTICS_DIR)/$(SEMANTICS_FILE) --main-module $(MAIN_MODULE) --gen-glr-bison-parser -O2
kompile $(SEMANTICS_DIR)/$(SEMANTICS_FILE) --main-module $(MAIN_MODULE) --gen-glr-bison-parser -O2 --heuristic pbaL

clean:
rm -Rf $(SEMANTICS_FILE_NAME)-kompiled
Expand Down
2 changes: 1 addition & 1 deletion bin/kparse-bool
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
#!/bin/bash
kparse -d "$(dirname "$0")/../solidity-kompiled" -s Bool -m SOLIDITY-DATA-SYNTAX "$(cat "$1")"
kparse -d "$(dirname "$0")/../solidity-kompiled" -s Bool -m BOOL-SYNTAX "$(cat "$1")"
2 changes: 1 addition & 1 deletion src/solidity-syntax.md
Original file line number Diff line number Diff line change
Expand Up @@ -207,7 +207,7 @@ Following is a list of supported statements.
`CallArgumentList` keeps a list of arguments for function calls and such (`revert()`, `emit()`, etc.)

```k
syntax CallArgumentList ::= List{Expression, ","} [overload(exps), strict, hybrid]
syntax CallArgumentList ::= List{Expression, ","} [overload(exps), strict]
```

Expand Down
6 changes: 3 additions & 3 deletions src/solidity.md
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ module SOLIDITY-CONFIGURATION
configuration
<solidity>
<k parser="TXN, SOLIDITY-DATA-SYNTAX"> $PGM:Program ~> $TXN:Transactions </k>
<summarize> $ISUNISWAP:Bool </summarize>
<summarize parser="ISUNISWAP, BOOL-SYNTAX"> $ISUNISWAP:Bool </summarize>
<compile>
<current-body> Id </current-body>
<ifaces>
Expand Down Expand Up @@ -117,10 +117,10 @@ module SOLIDITY-DATA
syntax Id ::= "constructor" [token]
syntax TypedVal ::= v(Value, TypeName) | lv(BaseRef, List, TypeName) | Int | String | "void"
syntax TypedVals ::= List{TypedVal, ","} [overload(exps), hybrid, strict]
syntax TypedVals ::= List{TypedVal, ","} [overload(exps), strict]
syntax Expression ::= TypedVal
syntax CallArgumentList ::= TypedVals
syntax KResult ::= TypedVal
syntax KResult ::= TypedVal | TypedVals
syntax Value ::= MInt{8} | MInt{32} | MInt{112} | MInt{160} | MInt{256} | Bool | String | List | Map
syntax BaseRef ::= Id | Int
Expand Down
4 changes: 3 additions & 1 deletion src/statement.md
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ module SOLIDITY-STATEMENT
<store> S => S [ !I <- default(T) ] </store>
// emit statement
rule <k> emit X:Id ( ARGS ) ; => #log(Event2String(ARGS, ((.StringBuffer +String Id2String(X)) +String "("))) ...</k>
rule <k> emit X:Id ( ARGS ) ; => discard(Event2String(ARGS, ((.StringBuffer +String Id2String(X)) +String "("))) ...</k>
requires isKResult(ARGS)
syntax String ::= Event2String(CallArgumentList, StringBuffer) [function]
Expand All @@ -65,6 +65,8 @@ module SOLIDITY-STATEMENT
rule Event2String(v(V:MInt{112}, _), ARGS, SB) => Event2String(ARGS, (SB +String Int2String(MInt2Unsigned(V))) +String ", ") [owise]
rule Event2String(v(V:MInt{160}, _), ARGS, SB) => Event2String(ARGS, (SB +String Int2String(MInt2Unsigned(V))) +String ", ") [owise]
rule Event2String(v(V:MInt{256}, _), ARGS, SB) => Event2String(ARGS, (SB +String Int2String(MInt2Unsigned(V))) +String ", ") [owise]
syntax K ::= discard(String) [function]
rule discard(_) => .K
// if statement
rule if ( v(true, bool ) ) S => S
Expand Down
1 change: 0 additions & 1 deletion test/regression/emit.ref
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
Approval(1, 0, 2)
<solidity>
<k>
.K
Expand Down
Loading

0 comments on commit b8d3e5e

Please sign in to comment.