Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Segmentation fault with satisfy_one function call on a large boolean expression #188

Open
azewiusz opened this issue Jun 10, 2024 · 1 comment
Open

Segmentation fault with satisfy_one function call on a large boolean expression #188

azewiusz opened this issue Jun 10, 2024 · 1 comment

Comments

@azewiusz
Copy link

I do not have much to show as expression is in size of several GB but found out this GDB / Python trace that I would like to understand:
It fails teh same on Windows 10 machine and on Linux one (Ubuntu) Linux dev 6.8.0-35-generic #35-Ubuntu SMP PREEMPT_DYNAMIC Mon May 20 15:51:52 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux

Thread 1 "python3.11" received signal SIGSEGV, Segmentation fault.
Downloading source file /build/python3.11-khintT/python3.11-3.11.9/build-static/../Objects/obmalloc.c
0x000000000051cd33 in pymalloc_alloc (ctx=<optimized out>, nbytes=32)           
    at ../Objects/obmalloc.c:1979
warning: 1979	../Objects/obmalloc.c: No such file or directory
(gdb) bt
#0  0x000000000051cd33 in pymalloc_alloc (ctx=<optimized out>, nbytes=32)
    at ../Objects/obmalloc.c:1979
#1  _PyObject_Malloc (nbytes=32, ctx=<optimized out>)
    at ../Objects/obmalloc.c:1998
#2  PyMem_Malloc (size=32) at ../Objects/obmalloc.c:623
#3  0x00007ffff7bd8357 in new (ps=ps@entry=0x2cdab00, size=size@entry=32)
    at thirdparty/picosat/picosat.c:949
#4  0x00007ffff7bdb6d6 in new_clause (learned=1, size=1, ps=<optimized out>)
    at thirdparty/picosat/picosat.c:1292
#5  add_simplified_clause (ps=ps@entry=0x2cdab00, learned=learned@entry=1)
    at thirdparty/picosat/picosat.c:2345
#6  0x00007ffff7bda09b in resolve_top_level_unit (reason=0x2cdab70, 
    lit=0x1a1327820, ps=<optimized out>) at thirdparty/picosat/picosat.c:1890
#7  assign_forced (ps=ps@entry=0x2cdab00, lit=0x1a1327820, reason=0x2cdab70)
    at thirdparty/picosat/picosat.c:1975
#8  0x00007ffff7bdbc0d in prop2 (this=0x1a1327825, ps=0x2cdab00)
    at thirdparty/picosat/picosat.c:3895
#9  bcp (ps=ps@entry=0x2cdab00) at thirdparty/picosat/picosat.c:4299
#10 0x00007ffff7be21b7 in bcp (ps=0x2cdab00)
    at thirdparty/picosat/picosat.c:4291
#11 sat (l=-1, ps=0x2cdab00) at thirdparty/picosat/picosat.c:5868
#12 picosat_sat (ps=ps@entry=0x2cdab00, l=-1)
    at thirdparty/picosat/picosat.c:7109
--Type <RET> for more, q to quit, c to continue without paging--
#13 0x00007ffff7bd7dfb in _satisfy_one (self=<optimized out>, 
    args=<optimized out>, kwargs=<optimized out>)
    at pyeda/boolalg/picosatmodule.c:383
#14 0x000000000055394b in cfunction_call (
    func=<built-in method satisfy_one of module object at remote 0x7ffff73938d0>, args=<optimized out>, kwargs=<optimized out>)
    at ../Objects/methodobject.c:542
#15 0x000000000052e6d3 in _PyObject_MakeTpCall (
    tstate=0xa53198 <_PyRuntime+166328>, 
    callable=<built-in method satisfy_one of module object at remote 0x7ffff73938d0>, args=<optimized out>, nargs=<optimized out>, keywords=0x0)
    at ../Objects/call.c:214
#16 0x000000000053bf0d in _PyEval_EvalFrameDefault (tstate=<optimized out>, 
    frame=<optimized out>, throwflag=<optimized out>) at ../Python/ceval.c:4769
#17 0x000000000060eb9d in _PyEval_EvalFrame (throwflag=0, 
    frame=0x7ffff7fb2020, tstate=0xa53198 <_PyRuntime+166328>)
    at ../Include/internal/pycore_ceval.h:73
#18 _PyEval_Vector (tstate=tstate@entry=0xa53198 <_PyRuntime+166328>, 
    func=func@entry=0x7ffff7415ee0, 
    locals=locals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__fi--Type <RET> for more, q to quit, c to continue without paging--
le__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), args=args@entry=0x0, argcount=argcount@entry=0, 
    kwnames=kwnames@entry=0x0) at ../Python/ceval.c:6434
#19 0x000000000060e348 in PyEval_EvalCode (co=<code at remote 0xe16480>, 
    globals=<optimized out>, 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton--Type <RET> for more, q to quit, c to continue without paging--
 that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated)) at ../Python/ceval.c:1148
#20 0x000000000062d9cc in run_eval_code_obj (
    tstate=0xa53198 <_PyRuntime+166328>, co=0xe16480, 
    globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotatio--Type <RET> for more, q to quit, c to continue without paging--
ns__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated)) at ../Python/pythonrun.c:1741
#21 0x0000000000629c66 in run_mod (mod=<optimized out>, 
    filename=<optimized out>, 
    globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleto--Type <RET> for more, q to quit, c to continue without paging--
n that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), flags=<optimized out>, arena=<optimized out>)
    at ../Python/pythonrun.c:1762
#22 0x000000000063e687 in pyrun_file (fp=fp@entry=0xabf860, 
    filename=filename@entry='/home/dev/Desktop/number_games/sha256/sharun_tse.py', start=start@entry=257, 
    globals=globals@entry={'__name__': '__main__', '__doc__': None, '__package__--Type <RET> for more, q to quit, c to continue without paging--
': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals=locals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``--Type <RET> for more, q to quit, c to continue without paging--
, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), closeit=closeit@entry=1, flags=0x7fffffffdb08)
    at ../Python/pythonrun.c:1657
#23 0x000000000063dd49 in _PyRun_SimpleFileObject (fp=fp@entry=0xabf860, 
    filename=filename@entry='/home/dev/Desktop/number_games/sha256/sharun_tse.py', closeit=closeit@entry=1, flags=flags@entry=0x7fffffffdb08)
    at ../Python/pythonrun.c:440
#24 0x000000000063dabf in _PyRun_AnyFileObject (fp=0xabf860, 
    filename='/home/dev/Desktop/number_games/sha256/sharun_tse.py', closeit=1, 
    flags=0x7fffffffdb08) at ../Python/pythonrun.c:79
#25 0x00000000006385c7 in pymain_run_file_obj (skip_source_first_line=0, 
    filename='/home/dev/Desktop/number_games/sha256/sharun_tse.py', 
    program_name='/home/dev/Desktop/number_games/venv/bin/python3.11')
    at ../Modules/main.c:360
#26 pymain_run_file (config=0xa391e0 <_PyRuntime+59904>)
    at ../Modules/main.c:379
#27 pymain_run_python (exitcode=0x7fffffffdb04) at ../Modules/main.c:601
#28 Py_RunMain () at ../Modules/main.c:680
#29 0x00000000005ff63d in Py_BytesMain (argc=<optimized out>, 
    argv=<optimized out>) at ../Modules/main.c:734
#30 0x00007ffff7c2a1ca in __libc_start_call_main (
--Type <RET> for more, q to quit, c to continue without paging--
    main=main@entry=0x5ff590 <main>, argc=argc@entry=2, 
    argv=argv@entry=0x7fffffffdd48)
    at ../sysdeps/nptl/libc_start_call_main.h:58
#31 0x00007ffff7c2a28b in __libc_start_main_impl (main=0x5ff590 <main>, 
    argc=2, argv=0x7fffffffdd48, init=<optimized out>, fini=<optimized out>, 
    rtld_fini=<optimized out>, stack_end=0x7fffffffdd38)
    at ../csu/libc-start.c:360
#32 0x00000000005ff4c5 in _start ()
(gdb) py-bt
Traceback (most recent call first):
  <built-in method satisfy_one of module object at remote 0x7ffff73938d0>
  File "/home/dev/Desktop/number_games/venv/lib/python3.11/site-packages/pyeda/boolalg/expr.py", line 1385, in satisfy_one
    return picosat.satisfy_one(self.nvars, self.clauses, assumptions,
  File "/home/dev/Desktop/number_games/venv/lib/python3.11/site-packages/pyeda/boolalg/expr.py", line 738, in satisfy_one
    soln = cnf.satisfy_one(assumptions)
  File "/home/dev/Desktop/number_games/sha256/sharun_tse.py", line ?, in <module>
    (failed to get frame line number)
@azewiusz
Copy link
Author

Just to mention it fails for sure on
pyeda 0.29.0

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@azewiusz