Open
Description
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.