Investigate unexpected branch splitting for some rules during opcode summarization.
Nessuno ha ancora preso questa issue.
Valutazione
Questa issue non è ancora stata valutata.
Descrizione
Changes in evm.md in PR https://github.com/runtimeverification/evm-semantics/pull/2727 are introduced due to unexpected remainder caused by the previous rules.
During the summarization for BALANCE, rules ->
rule <k> #access [ OP , AOP ] => #gasAccess(SCHED, AOP) ~> #deductGas ... </k>
<schedule> SCHED </schedule>
requires Ghasaccesslist << SCHED >> andBool #usesAccessList(OP)
rule <k> #access [ _ , _ ] => .K ... </k> <schedule> _ </schedule> [owise]
will generate a correct branch with Ghasaccesslist << SCHED >> andBool #usesAccessList(OP) and an unexpected branch with unchanged state and condition of the split source. Finally, the unexpected branch leads to infinite splits for this case.
During summarizing SLOAD and SSTORE, rules ->
rule <k> #accessStorage ACCT INDEX => .K ... </k>
<accessedStorage> ... ACCT |-> (TS:Set => TS |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 >>
lead to a similar result. For this one, the backend doesn't know these three rules cover all the possibilities, but leave a condition with Ghasaccesslist << SCHED >> andBool ACCT in_keys(TS).
- Lingua principale
- KCL
- Stelle
- 592
- Fork
- 156
- Merge medio
- 2h 19m
- PR unite (30g)
- 1
Preparare l'ambiente
Non abbiamo ancora controllato i file di configurazione di questo progetto. Parti dal suo README e consulta la nostra guida al primo contributo per i passaggi generali.
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di runtimeverification/evm-semantics
-
Difficoltà 1/5 Meno di un'ora Idoneità per principianti 78/100
runtimeverification/evm-semantics#1190 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 45/100
runtimeverification/evm-semantics#2879 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2869 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100
runtimeverification/evm-semantics#2832 ·
-
Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100
runtimeverification/evm-semantics#2824 ·