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