Support `unsafe` for `to_module`

Đang mở

#4,754 mở ngày 10/2/2025 0 bình luận 0 reaction 1 người được giao Xem trên GitHub

@Stevengre đang làm issue này rồi.

Từ ngày 10/2/2025.

Đánh giá

Issue này chưa được đánh giá.

Mô tả

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.

Ngôn ngữ chính: Python
Star: 591
Fork: 163
Chỉ số merge pull request: Không có pull request nào được merge trong 30 ngày

Chuẩn bị môi trường

Đọc hướng dẫn đóng góp

Bắt đầu từ đâu

Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
Fork repository và làm thay đổi trên một nhánh.
Mở pull request có tham chiếu số hiệu của issue.

Issue khác của runtimeverification/k

Introduce composable symbolic execution interface in pyx
Có thể làm lại được @Stevengre đã nhận 98 ngày trước và không có pull request nào đang mở. Đang mở
- Có gì không ổn?
runtimeverification/k#4939 · 1 người được giao · Mở ngày 24/6/2026
Concolic Explorer
Đang mở
- Có gì không ổn?
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 32/100

runtimeverification/k#4937 · Mở ngày 18/6/2026
All-path reachability proof checker
Đang mở
- Có gì không ổn?
Độ khó 5/5 Hơn một tuần Mức phù hợp với người mới 30/100

runtimeverification/k#4936 · Mở ngày 18/6/2026
Accelerating all-path reachability proofs with one-path reachability proofs
Có thể làm lại được @Stevengre đã nhận 104 ngày trước và không có pull request nào đang mở. Đang mở
- Có gì không ổn?
type:epic

runtimeverification/k#4934 · 4 bình luận · 1 người được giao · Mở ngày 15/6/2026
Support progressive depth halving as a generic policy in `Prover.advance_proof`
Có thể làm lại được @Stevengre đã nhận 123 ngày trước và không có pull request nào đang mở. Đang mở
- Có gì không ổn?
runtimeverification/k#4924 · 1 người được giao · Mở ngày 29/5/2026

Tất cả issue của runtimeverification/k

Issue tương tự

Claiming namespace `apoint`
Đang mở
- Có gì không ổn?
namespace operations

Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 82/100

EclipseFdn/open-vsx.org#13573 · Mở ngày 30/9/2026

Maintainer thường phản hồi trong vòng 1 ngày
[Bug] vRecur has BYWEEKDAY registered but that is not part of the standard
Đang mở
- Có gì không ổn?
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100

collective/icalendar#1854 · Mở ngày 30/9/2026

Maintainer thường phản hồi trong vòng 1 ngày
The no-agent error message is wrong
Đang mở
- Có gì không ổn?
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 72/100

rancher/rancher-ai-agent#412 · Mở ngày 30/9/2026

Maintainer thường phản hồi trong vòng 6 ngày
Add a check in io.py, only check the existence for Path and string objects
Đang mở
- Có gì không ổn?
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 84/100

TUDelftGeodesy/DePSI#134 · Mở ngày 30/9/2026
`American "Acknowledgments" heading is misclassified and rendered after Introduction`
Đang mở
- Có gì không ổn?
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 88/100

HenriquesLab/rxiv-maker#335 · Mở ngày 30/9/2026

Thêm issue về Python

Support `unsafe` for `to_module`

Có gì không ổn?

Đánh giá

Mô tả

Chuẩn bị môi trường

Bắt đầu từ đâu

Issue khác của runtimeverification/k

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Issue tương tự

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Có gì không ổn?

Nhận issue mới trong hộp thư của bạn