test_all.py errors

[fishfacegit]

python3 test_all.py results in z3 error: Is this a bug?

ERROR z3_ir.py
Traceback (most recent call last):
  File "../miasm/test/ir/translators/z3_ir.py", line 117, in <module>
    check_interp(model[memb.get_mem_array(32)],
  File "../miasm/test/ir/translators/z3_ir.py", line 31, in check_interp
    assert addr in constraints
AssertionError

[serpilliere]

Hi @fishfacegit ! The script you are running is tested in the regressions tests on each miasm commits. So maybe there is a problem somewhere in your setup? Can you provide some information like OS python version, ... Can you modify this script to print addr and constaints before the assert?

[fishfacegit]

Hi! can you reproduce the error in this Python 3.10.6 environment?

uname -a 5.19.0-41-generic #42~22.04.1-Ubuntu SMP PREEMPT_DYNAMIC

(venv-miasm):$ python3 -m pip freeze asttokens==2.2.1 backcall==0.2.0 boto==2.49.0 comm==0.1.3 debugpy==1.6.7 decorator==5.1.1 executing==1.2.0 future==0.18.3 ipykernel==6.22.0 ipython==8.13.1 jedi==0.18.2 jupyter_client==8.2.0 jupyter_core==5.3.0 llvmlite==0.39.1 matplotlib-inline==0.1.6 -e git+https://github.com/cea-sec/miasm.git@2b8366aaa88679609ae56e738ebf9e2f47aa53fc#egg=miasm nest-asyncio==1.5.6 packaging==23.1 parameterized==0.9.0 parso==0.8.3 pexpect==4.8.0 pickleshare==0.7.5 platformdirs==3.5.0 prompt-toolkit==3.0.38 psutil==5.9.5 ptyprocess==0.7.0 pure-eval==0.2.2 pycparser==2.21 Pygments==2.15.1 pyparsing==2.4.7 python-dateutil==2.8.2 pyzmq==25.0.2 six==1.16.0 stack-data==0.6.2 tornado==6.3.1 traitlets==5.9.0 wcwidth==0.2.6 z3-solver==4.12.1.0

[serpilliere]

The main differences from the regression tests (https://github.com/cea-sec/miasm/actions/runs/4794027291/jobs/8527003012) are python version:

Run actions/setup-python@v4
  with:
    python-version: 3.10
    check-latest: false
    token: ***
    update-environment: true
    allow-prereleases: false
Installed versions
  Successfully set up CPython (3.10.11)

The z3 version is z3-solver==4.8.7.0 So the problem may not come the z3

[fishfacegit]

Maybe trouble z3 solver.model() returning another value than expected?

addr: 0xdeadbef0
contraints:
        0xdeadbef2: 2

Traceback (most recent call last):
  File "../miasm/test/ir/translators/z3_ir.py", line 121, in <module>
    check_interp(model[memb.get_mem_array(32)],
  File "../miasm/test/ir/translators/z3_ir.py", line 35, in check_interp
    assert addr in constraints
AssertionError