Support `unsafe` for `to_module`
@Stevengre ya está trabajando en esto.
Desde el 10/2/2025.
Evaluación
Este issue todavía no se ha evaluado.
Descripción
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.
- Lenguaje dominante
- Python
- Estrellas
- 598
- Forks
- 164
- Métricas de merge de PR
- Sin PR fusionados en 30 d
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Sin plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de runtimeverification/k
-
Dificultad 4/5 3-5 días Aptitud para principiantes 43/100
runtimeverification/k#4942 ·
-
bug
Dificultad 3/5 Medio día Aptitud para principiantes 75/100
runtimeverification/k#4941 ·
-
Introduce composable symbolic execution interface in pyxQuizá libre de nuevo @Stevengre la tomó hace 124 días y no hay ningún pull request abierto. Abierto
runtimeverification/k#4939 · 1 asignado ·
-
Concolic ExplorerAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 32/100
runtimeverification/k#4937 ·
-
Dificultad 5/5 Más de una semana Aptitud para principiantes 30/100
runtimeverification/k#4936 ·
Todos los issues de runtimeverification/k
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
nansencenter/geodataset#39 ·
-
bug
Dificultad 2/5 1-3 horas Aptitud para principiantes 76/100
awslabs/visual-asset-management-system#804 ·
Los mantenedores suelen responder en 1 día
-
follow-up
Dificultad 2/5 1-3 horas Aptitud para principiantes 65/100
Los mantenedores suelen responder en 1 día
-
[18.0] werkzeug: AttributeErrorAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
odoo/odoo#297927 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
link-rot
Dificultad 1/5 Menos de una hora Aptitud para principiantes 67/100