claripy error

[bird8693]

error:

exception: access violation reading 0x00000000000020F5
> i:\project\angr2\lib\site-packages\z3\z3core.py(4139)Z3_solver_check_assumptions()
   4138 def Z3_solver_check_assumptions(a0, a1, a2, a3):
-> 4139   r = lib().Z3_solver_check_assumptions(a0, a1, a2, a3)
   4140   err = lib().Z3_get_error_code(a0)`

callstack:

......
......
......
i:\project\angr2\lib\site-packages\angr\storage\memory.py(756)load()
    755         ):
--> 756             self._constrain_underconstrained_index(addr_e)
    757

  i:\project\angr2\lib\site-packages\angr\storage\memory.py(820)_constrain_underconstrained_index()
    819     def _constrain_underconstrained_index(self, addr_e):
--> 820         if not self.state.uc_manager.is_bounded(addr_e) or self.state.se.max_int(addr_e) - self.state.se.min_int( addr_e) >= self._read_address_range:
    821             # in under-constrained symbolic execution, we'll assign a new memory region for this address

  i:\project\angr2\lib\site-packages\angr\state_plugins\solver.py(145)concrete_shortcut_scalar()
    144         if v is None:
--> 145             return f(self, *args, **kwargs)
    146         else:

  i:\project\angr2\lib\site-packages\angr\state_plugins\sim_action_object.py(53)ast_stripper()
     52         new_kwargs = _raw_ast(kwargs)
---> 53         return f(*new_args, **new_kwargs)
     54     return ast_stripper

  i:\project\angr2\lib\site-packages\angr\state_plugins\solver.py(86)wrapped_f()
     85         try:
---> 86             return f(*args, **kwargs)
     87         except claripy.UnsatError:

  i:\project\angr2\lib\site-packages\angr\state_plugins\solver.py(501)max()
    500             return ar
--> 501         return self._solver.max(e, extra_constraints=self._adjust_constraint_list(extra_constraints), exact=exact)
    502

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\concrete_handler_mixin.py(30)max()
     29         else:
---> 30             return super(ConcreteHandlerMixin, self).max(e, **kwargs)
     31

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\constraint_filter_mixin.py(48)max()
     47         ec = self._constraint_filter(extra_constraints)
---> 48         return super(ConstraintFilterMixin, self).max(e, extra_constraints=ec, **kwargs)
     49

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\sat_cache_mixin.py(84)max()
     83                 e,
---> 84                 extra_constraints=extra_constraints, **kwargs
     85             )

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\simplify_helper_mixin.py(4)max()
      3         self.simplify()
----> 4         return super(SimplifyHelperMixin, self).max(*args, **kwargs)
      5

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\constraint_expansion_mixin.py(24)max()
     23     def max(self, e, extra_constraints=(), exact=None, **kwargs):
---> 24         m = super(ConstraintExpansionMixin, self).max(e, extra_constraints=extra_constraints, exact=exact, **kwargs)
     25         if len(extra_constraints) == 0:

  i:\project\angr2\lib\site-packages\claripy\frontends\composite_frontend.py(300)max()
    299         ms = self._merged_solver_for(e=e, lst=extra_constraints)
--> 300         r = ms.max(e, extra_constraints=extra_constraints, exact=exact)
    301         self._reabsorb_solver(ms)

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\sat_cache_mixin.py(84)max()
     83                 e,
---> 84                 extra_constraints=extra_constraints, **kwargs
     85             )

  i:\project\angr2\lib\site-packages\claripy\frontend_mixins\model_cache_mixin.py(289)max()
    288         else:
--> 289             m = super(ModelCacheMixin, self).max(e, extra_constraints=extra_constraints, **kwargs)
    290             self._max_exhausted.add(e.cache_key)

  i:\project\angr2\lib\site-packages\claripy\frontends\full_frontend.py(137)max()
    136                 solver=self._get_solver(),
--> 137                 model_callback=self._model_hook
    138             )

  i:\project\angr2\lib\site-packages\claripy\backends\__init__.py(543)max()
    542
--> 543         return self._max(self.convert(expr), extra_constraints=self.convert_list(extra_constraints), solver=solver, model_callback=model_callback)
    544

  i:\project\angr2\lib\site-packages\claripy\backends\backend_z3.py(64)z3_condom()
     63                 condom_args = args
---> 64             return f(*condom_args, **kwargs)
     65         except z3.Z3Exception as ze:

  i:\project\angr2\lib\site-packages\claripy\backends\backend_z3.py(746)_max()
    745             l.debug("Doing a check!")
--> 746             if solver.check() == z3.sat:
    747                 l.debug("... still sat")

  i:\project\angr2\lib\site-packages\z3\z3.py(6182)check()
   6181             _assumptions[i] = assumptions[i].as_ast()
-> 6182         r = Z3_solver_check_assumptions(self.ctx.ref(), self.solver, num, _assumptions)
   6183         return CheckSatResult(r)

> i:\project\angr2\lib\site-packages\z3\z3core.py(4139)Z3_solver_check_assumptions()
   4138 def Z3_solver_check_assumptions(a0, a1, a2, a3):
-> 4139   r = lib().Z3_solver_check_assumptions(a0, a1, a2, a3)
   4140   err = lib().Z3_get_error_code(a0)

[rhelmot]

Claripy doesn’t work with python 2 anymore. This is intended. How did you get an installation of claripy version 8 under python 2? I marked it unusable for python 2 in a couple of different ways...

…

On Wed, Oct 17, 2018 at 5:15 AM rain6851 ***@***.***> wrote: Some virtual memory address type may be long — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#97 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ACYg9el4WWB74ozRQjAg5GFvUUFmaXZ9ks5ulx9HgaJpZM4Xjw9L> .

[bird8693]

@rhelmot This error is not about long type. I receive this error, so I use pip install claripy --upgrade to update claripy leading to a error unsupport long. Now I downgrade claripy and this error still occurs.

[rhelmot]

I see. In the future, if you make substantial edits, please leave a comment to this effect, since the edits do not propagate through email.

Your issue looks like a fairly serious installation/loading error with z3. I am unsure how to help you. Is there a testcase that causes this behavior?

[bird8693]

@rhelmot It occurs error with a trace under tracer through a lot of traces test. When I test a single trace, it runs normally. I try to reloading z3 when this error occurs. Thank you.

[rhelmot]

I still do not understand how to help you. How can I reproduce this bug?

[bird8693]

I try to abstract a testcase for you.

[github-actions]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions]

This issue has been closed due to inactivity.