Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

Support `unsafe` for `to_module`

Aperta
  • Qualcosa non va?
#4,754 0 commenti 0 reazioni 1 assegnatario Vedi su GitHub

@Stevengre ci sta già lavorando.

Dal 10/2/2025.

Valutazione

Questa issue non è ancora stata valutata.

Descrizione

bug kast

Currently, the unsafe argument is only provided by _ml_constraint_to_bool which cannot be setup from the ouside. This can cause problem for printing kast with term like Exist, resulting in the following error info:

Traceback (most recent call last):
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/bin/kevm", line 6, in <module>
    sys.exit(main())
             ^^^^^^
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/__main__.py", line 102, in main
    execute(options)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/__main__.py", line 640, in exec_summarize
    analyze_proof('BALANCE_1', 1)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 614, in analyze_proof
    summarizer.analyze_proof(str(proof_dir / f'{opcode}_SPEC'), node_id)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 555, in analyze_proof
    self.summarize(proof)
  File "/home/zhaoji/evm-semantics/kevm-pyk/src/kevm_pyk/summarizer.py", line 549, in summarize
    for res_line in proof_show.show(proof, to_module=True):
                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/proof/show.py", line 79, in show
    res_lines = self.kcfg_show.show(
                ^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/show.py", line 375, in show
    module = self.to_module(cfg, module_name, omit_cells=omit_cells)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/show.py", line 323, in to_module
    module = cfg.to_module(module_name)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 729, in to_module
    return KFlatModule(module_name, self.to_rules(priority=priority), imports=imports, att=att)
                                    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 717, in to_rules
    return [e.to_rule(_id, priority=priority) for e in self.edges()] + [
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 717, in <listcomp>
    return [e.to_rule(_id, priority=priority) for e in self.edges()] + [
            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kcfg/kcfg.py", line 243, in to_rule
    rule, _ = cterm_build_rule(
              ^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/cterm/cterm.py", line 411, in cterm_build_rule
    return build_rule(
           ^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 773, in build_rule
    init_constraints = [normalize_ml_pred(c) for c in init_constraints]
                       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 773, in <listcomp>
    init_constraints = [normalize_ml_pred(c) for c in init_constraints]
                        ^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 207, in normalize_ml_pred
    return bool_to_ml_pred(simplify_bool(ml_pred_to_bool(pred)))
                                         ^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 170, in ml_pred_to_bool
    return _ml_constraint_to_bool(kast)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 125, in _ml_constraint_to_bool
    return notBool(_ml_constraint_to_bool(_kast.args[0]))
                   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/zhaoji/.cache/pypoetry/virtualenvs/kevm-pyk-9eA2lNH8-py3.11/lib/python3.11/site-packages/pyk/kast/manip.py", line 168, in _ml_constraint_to_bool
    raise ValueError(f'Could not convert ML predicate to sort Bool: {_kast}')
ValueError: Could not convert ML predicate to sort Bool: KApply(label=KLabel(name='#Exists', params=(KSort(name='CodeCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen0', sort=KSort(name='CodeCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='StorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen1', sort=KSort(name='StorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='OrigStorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen2', sort=KSort(name='OrigStorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='TransientStorageCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen3', sort=KSort(name='TransientStorageCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='NonceCell'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='_Gen4', sort=KSort(name='NonceCell')), KApply(label=KLabel(name='#Exists', params=(KSort(name='Int'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='BAL', sort=KSort(name='Int')), KApply(label=KLabel(name='#And', params=(KSort(name='GeneratedTopCell'),)), args=(KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='false', sort=KSort(name='Bool')), KApply(label=KLabel(name='AccountCellMap:in_keys', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KApply(label=KLabel(name='_modInt_', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')), KToken(token='1461501637330902918203684832716283019655932542976', sort=KSort(name='Int')))),)), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))), KApply(label=KLabel(name='#And', params=(KSort(name='GeneratedTopCell'),)), args=(KApply(label=KLabel(name='#Equals', params=(KSort(name='Bool'), KSort(name='GeneratedTopCell'))), args=(KToken(token='false', sort=KSort(name='Bool')), KApply(label=KLabel(name='AccountCellMap:in_keys', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')),)), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))), KApply(label=KLabel(name='#Equals', params=(KSort(name='AccountCellMap'), KSort(name='GeneratedTopCell'))), args=(KVariable(name='DotAccountVar', sort=KSort(name='AccountCellMap')), KApply(label=KLabel(name='_AccountCellMap_', params=()), args=(KApply(label=KLabel(name='<account>', params=()), args=(KApply(label=KLabel(name='<acctID>', params=()), args=(KApply(label=KLabel(name='_modInt_', params=()), args=(KVariable(name='W0', sort=KSort(name='Int')), KToken(token='1461501637330902918203684832716283019655932542976', sort=KSort(name='Int')))),)), KApply(label=KLabel(name='<balance>', params=()), args=(KVariable(name='BAL', sort=KSort(name='Int')),)), KVariable(name='_Gen0', sort=KSort(name='CodeCell')), KVariable(name='_Gen1', sort=KSort(name='StorageCell')), KVariable(name='_Gen2', sort=KSort(name='OrigStorageCell')), KVariable(name='_Gen3', sort=KSort(name='TransientStorageCell')), KVariable(name='_Gen4', sort=KSort(name='NonceCell')))), KVariable(name='AC1_1', sort=KSort(name='AccountCellMap')))))))))))))))))))))

We should add unsafe argument according to this error trace.

Lingua principale
Python
Stelle
591
Fork
163
Nessuna PR unita negli ultimi 30g

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di runtimeverification/k

Tutte le issue di runtimeverification/k

Issue simili

Altre issue su Python

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.