-
Notifications
You must be signed in to change notification settings - Fork 151
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
Support gas cost summarization for all supported opcode. #2727
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -1597,16 +1597,11 @@ The various `CALL*` (and other inter-contract control flow) operations will be d | |
syntax KItem ::= "#accessStorage" Account Int | ||
// --------------------------------------------- | ||
rule <k> #accessStorage ACCT INDEX => .K ... </k> | ||
<accessedStorage> ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... </accessedStorage> | ||
<accessedStorage> TS => TS[ACCT <- {TS[ACCT] orDefault .Set}:>Set |Set SetItem(INDEX)] </accessedStorage> | ||
<schedule> SCHED </schedule> | ||
requires Ghasaccesslist << SCHED >> | ||
[preserves-definedness] | ||
|
||
rule <k> #accessStorage ACCT INDEX => .K ... </k> | ||
<accessedStorage> TS => TS[ACCT <- SetItem(INDEX)] </accessedStorage> | ||
<schedule> SCHED </schedule> | ||
requires Ghasaccesslist << SCHED >> andBool notBool ACCT in_keys(TS) | ||
|
||
rule <k> #accessStorage _ _ => .K ... </k> | ||
<schedule> SCHED </schedule> | ||
requires notBool Ghasaccesslist << SCHED >> | ||
|
@@ -2310,7 +2305,8 @@ Access List Gas | |
<schedule> SCHED </schedule> | ||
requires Ghasaccesslist << SCHED >> andBool #usesAccessList(OP) | ||
|
||
rule <k> #access [ _ , _ ] => .K ... </k> <schedule> _ </schedule> [owise] | ||
rule <k> #access [ OP , _ ] => .K ... </k> <schedule> SCHED </schedule> | ||
requires notBool (Ghasaccesslist << SCHED >> andBool #usesAccessList(OP)) | ||
Comment on lines
+2308
to
+2309
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This is for |
||
|
||
syntax InternalOp ::= #gasAccess ( Schedule, OpCode ) [symbol(#gasAccess)] | ||
// -------------------------------------------------------------------------- | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -433,8 +433,7 @@ def _build_spec( | |
# This is because #push doesn't handle `.Account`. And it's okay to be Int for other opcodes. | ||
_init_subst['CALLER_CELL'] = KVariable('CALLER_CELL', KSort('Int')) # CALLER_CELL should be Int for CALLER. | ||
_init_subst['ORIGIN_CELL'] = KVariable('ORIGIN_CELL', KSort('Int')) # ORIGIN_CELL should be Int for ORIGIN. | ||
inf_gas_cell = KEVM.inf_gas(KVariable('GAS_CELL', KSort('Gas'))) | ||
_init_subst['GAS_CELL'] = inf_gas_cell # inf_gas to reduce the computation cost. | ||
_init_subst['GAS_CELL'] = KEVM.inf_gas(KVariable('GAS_CELL', 'Gas')) # SLOAD & SSTORE must use infinite gas. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. SLOAD ERROR MESSAGE
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. SSTORE ERROR MESSAGE
|
||
_init_subst.update(init_map) | ||
init_subst = CSubst(Subst(_init_subst), init_constraints) | ||
|
||
|
@@ -467,6 +466,9 @@ def _le(a: KInner, b: KInner) -> KInner: | |
init_subst: dict[str, KInner] = {} | ||
final_subst: dict[str, KInner] = {} | ||
|
||
if opcode_symbol == 'SSTORE': | ||
init_subst['STATIC_CELL'] = KToken('false', KSort('Bool')) | ||
|
||
if opcode_symbol in NOT_USEGAS_OPCODES: | ||
# TODO: Should allow infGas to calculate gas. Skip for now. | ||
init_subst['USEGAS_CELL'] = KToken('false', KSort('Bool')) | ||
|
@@ -572,7 +574,7 @@ def create_kcfg_explore() -> KCFGExplore: | |
proof, | ||
create_kcfg_explore=create_kcfg_explore, | ||
max_depth=1, | ||
max_iterations=None, | ||
max_iterations=300, | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This can help me to investigate the issues. |
||
cut_point_rules=KEVMSemantics.cut_point_rules( | ||
break_on_jumpi=False, | ||
break_on_jump=False, | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
The backend cannot generate
Ghasaccesslist << SCHED >> andBool ACCT in_keys(TS)
condition forSLOAD
andSSTORE
's gas cost summarization. Therefore, it will be endless ndbranches without this change.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Are these changes to
evm.md
requried for this PR? They may cause issues with Kontrol for example.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Without these changes in
evm.md
, the gas cost summarization will not end with infininte branches.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
For this one, the backend don't know that
ACCT in_keys(TS)
for the first rule.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Here, I started a CI to check if this change will harm kontrol or not.
runtimeverification/kontrol#996
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It passed all the CI checks.