angr / claripy Goto Github PK

View Code? Open in Web Editor NEW

270.0 24.0 90.0 6.25 MB

An abstraction layer for constraint solvers.

License: BSD 2-Clause "Simplified" License

Python 100.00%

claripy's Introduction

claripy

Claripy is an abstracted constraint-solving wrapper.

Project Links

Project repository: https://github.com/angr/claripy

Documentation: https://api.angr.io/projects/claripy/en/latest/

Usage

It is usable!

General usage is similar to Z3:

>>> import claripy
>>> a = claripy.BVV(3, 32)
>>> b = claripy.BVS('var_b', 32)
>>> s = claripy.Solver()
>>> s.add(b > a)
>>> print(s.eval(b, 1)[0])

claripy's People

Contributors

Stargazers

Watchers

Forkers

chubbymaggie zhuyue1314 avain pombredanne lowks pewpewsecure tiffanyb shadown windhl juk80x redragonvn xybsoft iamahuman palkeo neighty hypersimple iv4n550 xennygrimmato drone29a tyb0807 domenukk codemaxx jarsp sjcomeau43543 codingsf lixuan2416 bannsec m1ghtym0 techlord-rce crpdm ercoppa fullwaywang lukas-dresel bennofs bkosciarz f0829 mkornbluth hase-project fiberx kwalberg c0frex danse-macabre sweetvishnya donggeliu kyle-kyle cdisselkoen saykim0727 yhzx2013 saullocarvalho kbittick gernst fmagin mephi42 ababook embg rainoftime edmcman 5l1v3r1 aos002 ccassedy vishalbelsare degrigis charlybvo recursivemake hwu71 bonnie1256 shingarov cancebeci 01100101011011010110100101101110 kina4uc mborgerson matthewpruett lukeserne minhyuk samkenxstream fantasquex capuanob c4dt mayhemheroes koh-ts mounir-khaled ekedaigle syheliel hazimeh draperlaboratory minroco amesianx lerr1uqs salls

claripy's Issues

Bitwise and simplifier can reduce bitvector size

Describe the bug
Performing a bitwise and on two bitvectors of the same length may cause the result to be shorter than the operands are. My suspicion is that this problem arises when this condition and the one that follows are both true and when the number of arguments to the concat AST is greater than two. This simplification seems to operate under the assumption that there will only ever be two arguments, but when using angr this does not always seem to be the case.

Environment Information

$ python -m angr.misc.bug_report
angr environment report
=============================
Date: 2019-01-30 17:55:16.751118
Running in virtual environment at /home/tgduckworth/.virtualenvs/angr
Platform: linux-x86_64
Python version: 3.5.2 (default, Nov 12 2018, 13:43:14) 
[GCC 5.4.0 20160609]
######## angr #########
Python found it in /home/tgduckworth/dev/angr-dev/angr/angr
Pip version angr 8.18.10.25
Git info:
    Current commit 865a5dc0a5695cba4cbf79a91a171e7fb8d460cb from branch master
    Checked out from remote origin: https://github.com/angr/angr
######## ailment #########
Python found it in /home/tgduckworth/dev/angr-dev/ailment/ailment
Pip version ailment 8.18.10.25
Git info:
    Current commit 284a67b1b5db5c950bebf4b6a096a127318474e8 from branch master
    Checked out from remote origin: https://github.com/angr/ailment
######## cle #########
Python found it in /home/tgduckworth/dev/angr-dev/cle/cle
Pip version cle 8.18.10.25
Git info:
    Current commit 28cbf5c5888b374b173410ef2e508b4eab7c02aa from branch master
    Checked out from remote origin: https://github.com/angr/cle
######## pyvex #########
Python found it in /home/tgduckworth/dev/angr-dev/pyvex/pyvex
Pip version pyvex 8.18.10.25
Git info:
    Current commit 36ba7fefbece6c11a27933b5151b450a87856302 from branch master
    Checked out from remote origin: https://github.com/angr/pyvex
######## claripy #########
Python found it in /home/tgduckworth/dev/angr-dev/claripy/claripy
Pip version claripy 8.18.10.25
Git info:
    Current commit 16457ff5b60f348b9246d4e2df4ff62052f89cc6 from branch master
    Checked out from remote origin: https://github.com/angr/claripy
######## archinfo #########
Python found it in /home/tgduckworth/dev/angr-dev/archinfo/archinfo
Pip version archinfo 8.18.10.25
Git info:
    Current commit bbac424873989d9cc4ce3ed01b7003ace04b4756 from branch master
    Checked out from remote origin: https://github.com/angr/archinfo
######## ana #########
Python found it in /home/tgduckworth/.virtualenvs/angr/lib/python3.5/site-packages/ana
Pip version ana 0.5
Couldn't find git info
######## z3 #########
Python found it in /home/tgduckworth/.virtualenvs/angr/lib/python3.5/site-packages/z3
Pip version not found!
Couldn't find git info
######## unicorn #########
Python found it in /home/tgduckworth/.virtualenvs/angr/lib/python3.5/site-packages/unicorn
Pip version unicorn 1.0.1
Couldn't find git info
######### Native Module Info ##########
z3: <CDLL '/home/tgduckworth/.virtualenvs/angr/lib/python3.5/site-packages/z3/lib/libz3.so', handle 38f6e20 at 0x7fd4c9fed668>
unicorn: <CDLL '/home/tgduckworth/.virtualenvs/angr/lib/python3.5/site-packages/unicorn/lib/libunicorn.so', handle 28c1000 at 0x7fd4c76ecef0>
angr: <CDLL '/home/tgduckworth/dev/angr-dev/angr/angr/lib/angr_native.so', handle 2f4c7c0 at 0x7fd4c3cb3ac8>
pyvex: <cffi.api._make_ffi_library.<locals>.FFILibrary object at 0x7fd4c836cb70>

To Reproduce

import angr

malloc = angr.SIM_PROCEDURES['libc']['malloc']()
proj = angr.Project("/bin/true", auto_load_libs=False)
s = proj.factory.blank_state()
p = malloc.execute(s, arguments=[40]).ret_expr
v = s.solver.BVS("v", 32)
s.memory.store(p, v)

# loading preserves value
x = s.memory.load(p, 4)
assert s.solver.is_true(x == v)

# let's modify the middle of it
y = s.memory.load(p, 2)
y = y | 0x10
print(y)  # <BV16 v_2_32[31:16] | 0x10>
s.memory.store(p, y)

# we now have a concat with three args
z = s.memory.load(p, 4)
assert z.op == "Concat"
assert len(z.args) == 3
print(z)  # <BV32 v_2_32[31:21] .. 1 .. v_2_32[19:0]>

# an operand of no particular significance
b = s.solver.BVV(2 ** (z.size() - z.args[0].size()) - 1, 32)
assert s.solver.is_true(b == 0x1fffff)
print(b)  # <BV32 0x1fffff>

trouble = z & b
print(trouble)  # <BV12 0x1>
s.memory.store(p, trouble)

# Traceback (most recent call last):
#   File "/home/tgduckworth/dev/misc/claripy_bug.py", line 35, in <module>
#     s.memory.store(p, trouble)
#   File "/home/tgduckworth/dev/angr-dev/angr/angr/storage/memory.py", line 516, in store
#     raise SimMemoryError("Attempting to store non-byte data to memory")
# angr.errors.SimMemoryError: Attempting to store non-byte data to memory

Additional context
I'm not too familiar with the design of claripy, so I'm not sure whether this is a problem with the claripy simplifier or whether concat is supposed to be a binary operator, with angr incorrectly constructing concat ASTs with more than two arguments. I suspect it is the former, but wanted to open this issue for discussion with someone who might be able to hone in on the problem a bit further.

How to check if a variable can be negative?

Hi,
I'm trying to understand how to check if a number can be negative.

I write this piece of code but I'm note that it is correct:

import claripy
a = claripy.BVV(0xffffffff, 32)
b = claripy.BVS('var_b', 32)
s = claripy.Solver()
s.add(claripy.SLT(b, a))

print s.satisfiable()
print s.eval(b, 1)

The output was:

True
(4294967294L,)

The goal is to check if b can be negative.

is it the proper way of doing it?

Thanks

DiscreteStridedIntervalSet doesn't consider the ESI.

Describe the bug
DiscreteStridedIntervalSet doesn't consider the ESI.

#claripy-8.18.10.25
import claripy
claripy.vsa.strided_interval.allow_dsis = True
solver = claripy.SolverVSA()
a = claripy.ESI(32)
b = claripy.SI('b', 32, 0, 10, 1)
c = a.union(b)
e = c + 1
print (e._model_vsa)
'''
<32>0x1[0x0, 0xffffffff]
'''

Environment Information
I test it in claripy-8.18.10.25.

Add check for unicode string value in BVV

I was playing around and ran into some trouble while processing a unicode string at [1]. It's not too hard to handle a unicode string here. Obtaining the correct byte length for multi-byte unicode characters should still work with len on unicode strings. It should also return the correct hex encoded representation.

However, I haven't checked elsewhere for similar issues. Would the better solution be to create a hex string in my program before passing it in? Ex: '\xc3\xab\xcc\x81a\xc3\xba' instead of 'ë́aú'

I can submit a pull-request if you'd like the change that handles unicode.

Thank you!

[1] https://github.com/angr/claripy/blob/master/claripy/ast/bv.py#L182

VSA .add() API inconsistent

We discussed this somewhat on irc some weeks ago.

This is the test code:

sv = claripy.FullFrontend(claripy.backends.z3)
x = claripy.BVS('x', 32)
sv.add(x < 50000) 
sv.add(x < 30000) 
sv.add(x > 20000)
print sv.max(x),"-",sv.min(x)

sv = claripy.FullFrontend(claripy.backends.z3)
x = claripy.BVS('x', 32)
sv.add([x < 50000, x < 30000, x > 20000])
print sv.max(x),"-",sv.min(x)

Which yields the following (correct) results:

29999 - 20001
29999 - 20001

If I replace the solver to vsa:

sv = claripy.ReplacementFrontend(claripy.LightFrontend(claripy.backends.vsa), replace_constraints=True, complex_auto_replace=True)
x = claripy.BVS('x', 32)
sv.add(x < 50000) 
sv.add(x < 30000) 
sv.add(x > 20000)
print sv.max(x),"-",sv.min(x)

sv = claripy.ReplacementFrontend(claripy.LightFrontend(claripy.backends.vsa), replace_constraints=True, complex_auto_replace=True)
x = claripy.BVS('x', 32)
sv.add([x < 50000, x < 30000, x > 20000])
print sv.max(x),"-",sv.min(x)

Yields the following:

49999 - 0
29999 - 19999

It seems, that VSA only uses the first specified constraint (first add call), when calculating its result.
[This seems inconsistent with the functionality of add function if the backend is set to Z3.]

If we specify all the constraints in one add call, then it works, but it miscalculates the UGT(>) expression (probably when inverting it).

Exposing solvers returning `unknown`

So, @rhelmot , @zardus , @ltfish: we have an interesting dilemma on our hands now where we implemented a portfolio frontend dishing the constraints out to multiple different solvers and returning the first answers received by any of the solvers.

However, some solvers, e.g. CVC4, return unknown almost immediately for some constraints they can't deal with. This means we now need to be able to differentiate between unknown, unsat and sat results returned from solvers in order to only accept answers in the portfolio that are certain. What do you think is the best way to deal with this?

Claripy not respecting max

I found something that's either a bug, or the documentation needs to be updated:

import claripy

a = claripy.BVS('test', 8, max=42)
s = claripy.Solver()
s.max(a)

Excpected: 42. Actual: 255.
The max is also not respected if I add a conflicting constraint and use eval().

z3 symbolic read using z3.Functions

@ltfish To accomplish this effort, we will need to

demonstrate whether or not the development investment is a time payoff for average use-cases (static memory vs dynamic memory)
implement a new claripy node for the z3.Function
write into the z3 backend how to convert the node into z3 objects
long-term goal: auto-detect the usecases where this functionality is most effective

claripy error

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)

bug: RecursionError: maximum recursion depth exceeded

The test code:

import angr
import claripy


def check(binary_path):
    proj = angr.Project(binary_path, use_sim_procedures=True, default_analysis_mode='symbolic_approximating', auto_load_libs=False)
    cfg = proj.analyses.CFGEmulated(keep_state=True, enable_advanced_backward_slicing=True, context_sensitivity_level=4)
    vfg = proj.analyses.VFG(cfg, function_start=proj.entry, context_sensitivity_level=2, interfunction_level=4, remove_options={angr.options.OPTIMIZE_IR})
     

if __name__ == '__main__':
    test_program = './test'
    check(test_program)

Error:

  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 887, in ite_excavated
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in _excavate_ite
  File "/home/wgh/.virtualenvs/angr/lib/python3.5/site-packages/claripy-8.18.10.25-py3.5.egg/claripy/ast/base.py", line 831, in <listcomp>
RecursionError: maximum recursion depth exceeded

test.zip
The testing binary is attached.

OverflowError: long int too large to convert to int

Hi,
while creating the CFG for pngpixel ( see attached ) I have the following error:

my code is something like:

pngpixel = angr.Project(filename, load_options={'skip_libs': ['libpng12.so.0.54.0', 'libz.so.1.2.8'],'auto_load_libs': True})
...
self._cfg = self.project.analyses.CFGAccurate(context_sensitivity_level=1, keep_state=True)

line 201, in BVV
    value &= (1 << size) -1
OverflowError: long int too large to convert to int
[pngpixel.zip](https://github.com/angr/claripy/files/802210/pngpixel.zip)

I'm using the latest version of claripy

I hope this can help to fix this issue. Happy to retest the fix once applied.

Thanks

Claripy needs concrete floats implemented with something other than python doubles

So correct me if I'm wrong here, but I've been looking at the solver tutorials/documentation, and I came across this:
"If you want to specify the rounding mode for an operation, use the fp operation explicitly (solver.fpAdd for example) with a rounding mode (one of solver.fp.RM_*) as the first argument."

However, looking at the code itself for fpAdd, fpSub, etc., it doesn't look like the solvers actually support any rounding modes.
For example, if I try fpAdd w/ RTZ on two floating points, I will still get back an un-truncated float.

Am I using this incorrectly or is this an issue?

Thanks.

Throw errors when passing bad types of objects into BVV

currently, you can say claripy.BVV(claripy.BVS('hell', 8), 8) and nobody will complain until we try to push that value into z3 and then we get a really really weird error

can angr be configured to use STP instead of Z3 for constraint solving?

AS TITLE.

Claripy right shift incorrect

The claripy right shift operator (>>/__rshift__) is incorrect in certain cases (and doesn't seem to reflect any sort of shift/rotate). Looks like when the highest bit is set it fills it down.
For instance:

In [57]: claripy.BVV(0x80, 8) >> 3
Out[57]: <BV8 240>

claripy.LShR is correct:

In [4]: claripy.LShR(BVV(0x80,8),3)
Out[4]: <BV8 16>

The left shift operator seems fine.

Tested with 8.19.2.4 (and a couple of older versions).

Recursion in Z3 back end can exhaust Python's stack for very deep expressions

I've encountered this exception a few times in my angr application. I can't trigger it deterministically yet but I am adding some logging to hopefully help:

ERROR   | 2020-02-04 09:27:44,201 | angr.exploration_techniques.oppologist | Original block hit an unsupported error
Traceback (most recent call last):
  File "/home/ed/.virtualenvs/angr/lib/python3.6/site-packages/cachetools/cache.py", line 39, in __getitem__
    return self.__data[key]
KeyError: 686789272

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/ed/Documents/angr-dev/angr/angr/exploration_techniques/oppologist.py", line 82, in successors
    return simgr.successors(state, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/misc/hookset.py", line 80, in __call__
    return self.func(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/sim_manager.py", line 421, in successors
    return self._project.factory.successors(state, **run_args)
  File "/home/ed/Documents/angr-dev/angr/angr/factory.py", line 58, in successors
    return self.default_engine.process(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/slicing.py", line 19, in process
    return super().process(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/engine.py", line 143, in process
    self.process_successors(self.successors, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/failure.py", line 21, in process_successors
    return super().process_successors(successors, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/syscall.py", line 18, in process_successors
    return super().process_successors(successors, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/hook.py", line 54, in process_successors
    return super().process_successors(successors, procedure=procedure, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/unicorn.py", line 90, in process_successors
    return super().process_successors(successors, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/soot/engine.py", line 64, in process_successors
    return super().process_successors(successors, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/heavy.py", line 135, in process_successors
    self.handle_vex_block(irsb)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/super_fastpath.py", line 19, in handle_vex_block
    super().handle_vex_block(irsb)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/slicing.py", line 26, in handle_vex_block
    super().handle_vex_block(irsb)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/actions.py", line 18, in handle_vex_block
    super().handle_vex_block(irsb)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/inspect.py", line 45, in handle_vex_block
    super().handle_vex_block(irsb)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 406, in handle_vex_block
    self._handle_vex_stmt(stmt)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/slicing.py", line 30, in _handle_vex_stmt
    super()._handle_vex_stmt(stmt)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/inspect.py", line 40, in _handle_vex_stmt
    super()._handle_vex_stmt(stmt)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/resilience.py", line 36, in inner
    return getattr(super(VEXResilienceMixin, self), func)(*iargs, **ikwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/heavy.py", line 199, in _handle_vex_stmt
    super()._handle_vex_stmt(stmt)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 50, in _handle_vex_stmt
    handler(stmt)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 187, in _handle_vex_stmt_WrTmp
    self._analyze_vex_stmt_WrTmp_data(stmt.data)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 183, in _analyze_vex_stmt_WrTmp_data
    def _analyze_vex_stmt_WrTmp_data(self, *a, **kw): return self. _handle_vex_expr(*a, **kw)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/inspect.py", line 31, in _handle_vex_expr
    return super()._handle_vex_expr(expr)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 54, in _handle_vex_expr
    result = handler(expr)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/light/light.py", line 86, in _handle_vex_expr_Load
    expr.end)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/actions.py", line 96, in _perform_vex_expr_Load
    result = super()._perform_vex_expr_Load(addr, ty, end, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/heavy.py", line 279, in _perform_vex_expr_Load
    result = super()._perform_vex_expr_Load(addr, ty, endness, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/claripy/datalayer.py", line 54, in _perform_vex_expr_Load
    res = super()._perform_vex_expr_Load(addr, ty, endness, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/engines/vex/heavy/heavy.py", line 28, in _perform_vex_expr_Load
    return self.state.memory.load(addr, self._ty_to_bytes(ty), endness=endness, action=action, inspect=inspect)
  File "/home/ed/Documents/angr-dev/angr/angr/storage/memory.py", line 789, in load
    events=not disable_actions, ret_on_segv=ret_on_segv)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/symbolic_memory.py", line 576, in _load
    addrs = self.concretize_read_addr(dst)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/symbolic_memory.py", line 427, in concretize_read_addr
    return self._apply_concretization_strategies(addr, strategies, 'load')
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/symbolic_memory.py", line 375, in _apply_concretization_strategies
    a = s.concretize(self, e)
  File "/home/ed/Documents/angr-dev/angr/angr/concretization_strategies/__init__.py", line 57, in concretize
    return self._concretize(memory, addr)
  File "/home/ed/Documents/angr-dev/angr/angr/concretization_strategies/range.py", line 13, in _concretize
    mn,mx = self._range(memory, addr)
  File "/home/ed/Documents/angr-dev/angr/angr/concretization_strategies/__init__.py", line 49, in _range
    return (self._min(memory, addr, **kwargs), self._max(memory, addr, **kwargs))
  File "/home/ed/Documents/angr-dev/angr/angr/concretization_strategies/__init__.py", line 25, in _min
    return memory.state.solver.min(addr, exact=kwargs.pop('exact', self._exact), **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/solver.py", line 144, in concrete_shortcut_scalar
    return f(self, *args, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/sim_action_object.py", line 57, in ast_stripper
    return f(*new_args, **new_kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/solver.py", line 87, in wrapped_f
    return f(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/angr/angr/state_plugins/solver.py", line 539, in min
    return self._solver.min(e, extra_constraints=self._adjust_constraint_list(extra_constraints), exact=exact)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/concrete_handler_mixin.py", line 37, in min
    return super(ConcreteHandlerMixin, self).min(e, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/constraint_filter_mixin.py", line 52, in min
    return super(ConstraintFilterMixin, self).min(e, extra_constraints=ec, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/sat_cache_mixin.py", line 98, in min
    extra_constraints=extra_constraints, **kwargs
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/simplify_helper_mixin.py", line 7, in min
    self.simplify()
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/constraint_deduplicator_mixin.py", line 22, in simplify
    added = super(ConstraintDeduplicatorMixin, self).simplify(**kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/sat_cache_mixin.py", line 34, in simplify
    new_constraints = super(SatCacheMixin, self).simplify()
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/simplify_skipper_mixin.py", line 36, in simplify
    return super(SimplifySkipperMixin, self).simplify(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontends/composite_frontend.py", line 396, in simplify
    s.simplify()
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/constraint_deduplicator_mixin.py", line 22, in simplify
    added = super(ConstraintDeduplicatorMixin, self).simplify(**kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/sat_cache_mixin.py", line 34, in simplify
    new_constraints = super(SatCacheMixin, self).simplify()
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/simplify_skipper_mixin.py", line 36, in simplify
    return super(SimplifySkipperMixin, self).simplify(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontend_mixins/model_cache_mixin.py", line 112, in simplify
    results = super(ModelCacheMixin, self).simplify(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontends/full_frontend.py", line 80, in simplify
    ConstrainedFrontend.simplify(self)
  File "/home/ed/Documents/angr-dev/claripy/claripy/frontends/constrained_frontend.py", line 117, in simplify
    simplified = simplify(And(*to_simplify)).split(['And']) #pylint:disable=no-member
  File "/home/ed/Documents/angr-dev/claripy/claripy/ast/base.py", line 1016, in simplify
    s = e._first_backend('simplify')
  File "/home/ed/Documents/angr-dev/claripy/claripy/ast/base.py", line 951, in _first_backend
    try: return getattr(b, what)(self)
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 70, in z3_condom
    return f(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 1017, in simplify
    o = self._abstract(s)
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 70, in z3_condom
    return f(*args, **kwargs)
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 393, in _abstract
    return self._abstract_internal(e.ctx.ctx, e.ast)
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in _abstract_internal
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in <listcomp>
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in _abstract_internal
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in <listcomp>
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in _abstract_internal
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 427, in <listcomp>
    children = [ self._abstract_internal(ctx, z3.Z3_get_app_arg(ctx, ast, i), new_split_on) for i in range(num_args) ]
[lots more removed]
  File "/home/ed/Documents/angr-dev/claripy/claripy/backends/backend_z3.py", line 409, in _abstract_internal
    cached_ast, _ = self._ast_cache[h]
  File "/home/ed/.virtualenvs/angr/lib/python3.6/site-packages/cachetools/lru.py", line 14, in __getitem__
    value = cache_getitem(self, key)
  File "/home/ed/.virtualenvs/angr/lib/python3.6/site-packages/cachetools/cache.py", line 41, in __getitem__
    return self.__missing__(key)
  File "/home/ed/.virtualenvs/angr/lib/python3.6/site-packages/cachetools/cache.py", line 68, in __missing__
    raise KeyError(key)
RecursionError: maximum recursion depth exceeded while calling a Python object

Concrete backend should be able to handle extremely simple symbolic cases

evaluating x when x == 4 should not touch z3
evaluating y when y == x and x == 4 should not touch z3
evaluating x when x[15:0] == 4 and x[31:16] == 5 should not touch z3
max(x) when x <= 5 (and no other constraints on x) should not touch z3
max(x) when x <= y and y <= 5 (and no other constraints on x and y) should not touch z3

DiscreteStridedIntervalSet.reverse() seems to have no effect

Consider the following example:

In [1]: from claripy.vsa.strided_interval import StridedInterval                                                                                                              

In [2]: from claripy.vsa.discrete_strided_interval_set import DiscreteStridedIntervalSet                                                                                      

In [3]: a = StridedInterval('a', 32, 0, 0xffff0000, 0xffff0000)                                                                                                               

In [4]: b = StridedInterval('b', 32, 0, 0xffff0001, 0xffff0001)                                                                                                               

In [5]: c = DiscreteStridedIntervalSet('c', 32, {a, b})                                                                                                                      

In [6]: c                                                                                                                                                                    
Out[6]: c<32>(2){<32>0x0[0xffff0000, 0xffff0000], <32>0x0[0xffff0001, 0xffff0001]}

In [7]: d = c.reverse()

In[8]: d                                                                                                                                                      
Out[9]: DSIS_0<32>(2){<32>0x0[0xffff0000, 0xffff0000], <32>0x0[0xffff0001, 0xffff0001]}

In [15]: from claripy.solvers import SolverVSA                                                                                                                                

In [16]: solver = SolverVSA()

In [22]: import monkeyhex                                                                                                                                                     

In [23]: solver.eval(d, 3)                                                                                                                                                    
Out[23]: (0xffff0000, 0xffff0001)

In [24]: solver.eval(c, 3)                                                                                                                                                    
Out[24]: (0xffff0000, 0xffff0001)

It also seems that the reversed_processor() is never called (i.e., the breakpoint I made there was never triggered). As far as I understand, that is not the expected behavior of the reverse() operation.

This leads to a situation where it's not possible to resolve a fairly simple indirect jump (please take a look at the example below) using the VSA:

.text:000000000000395C                 cmp     r12, 9          ; switch 10 cases
.text:0000000000003960                 ja      loc_3CA0        ; jumptable 0000000000003974 default case
.text:0000000000003960
.text:0000000000003966                 lea     rdx, off_5420
.text:000000000000396D                 movsxd  rax, dword ptr [rdx+r12*4]
.text:0000000000003971                 add     rax, rdx
.text:0000000000003974                 jmp     rax             ; switch jump

In[4]: state.ip  # state.history.addr == 0x3996
Out[5]: <BV64 SignExt(32, Reverse(union(union(union(union(union(union(union(union(union(unnamed_66_32, 0x48e6ffff), 0x88e6ffff), 0xd0e6ffff), 0x20e7ffff), 0x78e7ffff), 0xa8e7ffff), 0x10e8ffff), 0x60e5ffff), 0xe8e5ffff))) + 0x5420>

In[5]: state.solver.eval_upto(state.ip, 513)
Out[6]: 
[0x40e7541f,
 0x48e7541f,
 0xffffffff88e7541f,
 0xffffffffd0e7541f,
 0x20e8541f,
 0x78e8541f,
 0xffffffffa8e8541f,
 0x10e9541f,
 0x60e6541f,
 0xffffffffe8e6541f]

The state.ip value seems to be correct, but the solver is unable to evaluate any correct values out of it.

Here is the environment I'm working with:

angr environment report
=============================
Date: 2018-10-05 14:52:10.253721
Running in virtual environment at /home/user/.virtualenv/angr-dev
Platform: linux-x86_64
Python version: 3.5.3 (fdd60ed87e94, Apr 24 2018, 06:10:04)
[PyPy 6.0.0 with GCC 6.2.0 20160901]
######## angr #########
Python found it in /home/user/angr-dev/angr/angr
Pip version angr 8.18.10.1
Git info:
	Current commit 63b6b4eeb456c6c27fd96a839d5c601b8b99914b from branch master
	Checked out from remote origin: ssh://[email protected]/angr/angr
######## ailment #########
Python found it in /home/user/angr-dev/ailment/ailment
Pip version ailment 8.18.10.1
Git info:
	Current commit 966d5c57dd04f2e43f73b165ddca18166b249f85 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/ailment
######## cle #########
Python found it in /home/user/angr-dev/cle/cle
Pip version cle 8.18.10.1
Git info:
	Current commit c56152f6b8e199bd897b80115e0a9cf43bb70f5d from branch master
	Checked out from remote origin: ssh://[email protected]/angr/cle
######## pyvex #########
Python found it in /home/user/angr-dev/pyvex/pyvex
Pip version pyvex 8.18.10.1
Git info:
	Current commit 14169efac878bad0b10d9e7333efbb49c45921d0 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/pyvex
######## claripy #########
Python found it in /home/user/angr-dev/claripy/claripy
Pip version claripy 8.18.10.1
Git info:
	Current commit f4f2cbe47ddfe1c2cda9725846b3e9562c30ca92 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/claripy
######## archinfo #########
Python found it in /home/user/angr-dev/archinfo/archinfo
Pip version archinfo 8.18.10.1
Git info:
	Current commit 0b8bf512c88ecfef6ac7bfe78fb9f263f88e54e5 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/archinfo
######## ana #########
Python found it in /home/user/angr-dev/ana/ana
Pip version ana 0.5
Git info:
	Current commit 48657dc6500e33f5818b98003f1f179bfe03e1cc from branch master
	Checked out from remote origin: https://git:@github.com/zardus/ana
######## z3 #########
Python found it in /home/user/.virtualenv/angr-dev/site-packages/z3
Pip version not found!
Couldn't find git info
######## unicorn #########
Python found it in /home/user/.virtualenv/angr-dev/site-packages/unicorn
Pip version unicorn 1.0.1
Couldn't find git info

What is the purpose of ReplacementFrontend._replacement_cache?

The problem is, when I try to evaluate an expression using the solver from the state, that is a result of "slicecution," I get only unconstrained values because the replacement cache is empty due to the state being downsized during the execution.

I've already mitigated this issue by introducing the suspend_states option to the Slicecutor. However it doesn't seem like a good solution.

Another solution I came up with is to make the _replacement() method to look for replacements directly in the _replacements dictionary, but I believe that there was some reason why the _replacement_cache was introduced in the first place.

Hence the question.

Throw a different exception for when a solver timeout is hit

While solving a challenge I noticed that the solver always throws an UnSatError exception even when the timeout is hit.

I think it should be treated in a different way. I'll try to look it up myself.

Use claripy on ARM

Hi,
I have installed angr using PIP on my tablet but when I try to import it I have an error at the instruction:

cannot import z3core

Can someone help me to fix it please? I have installed angr-z3 manually compiling the code...

Thanks

Some floating-point stuff broke during the z3 upgrade

I just upgraded the z3 distribution to the latest version and, as per usual, it seems to have broken a few things. The following code worked before the upgrade and no longer does:

import claripy
s = claripy.Solver()
a = claripy.FPS('a', claripy.fp.FSORT_FLOAT)
s.eval(a.raw_to_bv(), 1)

Something along these lines is currently causing our CI to fail.

I would appreciate it if someone could take this issue on.

Is division signed or unsigned ?

If I create these variables :
a = claripy.BVV(5, 8)
b = claripy.BVV(254, 8)

Then, "a / b" is zero. So it's like the division is unsigned.

However, if now I set b to be a claripy.BVS('denominator', 8)
Then I instantiate a claripy.Solver, add a constraint that "a / b > 10" and that "b > 0", it is satisfiable, and it tells me that it works with b being 254.

So, I suppose this is not coherent.
Maybe you could make it more explicit, and you could also support both signed/unsigned divisions ?

Thanks !

TypeError: unsupported operand type(s) for /: 'FP' and 'FP'

import angr, claripy

s = claripy.Solver()

b = claripy.FPS('b', claripy.FSORT_DOUBLE)
c = claripy.FPS('c', claripy.FSORT_DOUBLE)

s.add(b / c)

When I try to execute above script I get following error:

Traceback (most recent call last):
File "exploit.py", line 8, in
s.add(b / c)
TypeError: unsupported operand type(s) for /: 'FP' and 'FP'

It seems that only operator / is broken for FPS() class, other operators work just fine.

I'm working in virtual env on latest angr form apt repository.

TypeError: 'BackendError' object cannot be interpreted as an integer

Caught this error while trying to execute some state with KEEP_MEMORY_READS_DISCRETE option enabled. I'm unable to provide a sample at this time, but here is a script to reproduce the issue:

from claripy.vsa.strided_interval import StridedInterval

si_set = set()
si_set.add(StridedInterval('x', 32, 0, 0, 0))
si_set.add(StridedInterval('y', 64, 0, 0x48e6ffff, 0x48e6ffff))

ret = set()
for si in si_set:
    ret.add(si.extract(63, 32))  # raises TypeError

The original place where this problem was encountered is located here:

claripy/claripy/vsa/discrete_strided_interval_set.py

Line 339 in 04972f3

ret.add(si.extract(high_bit, low_bit))

... and the TypeError is thrown here:

claripy/claripy/vsa/bool_result.py

Line 12 in 04972f3

return BackendError()

Currently, I'm working in the following environment:

angr environment report
=============================
Date: 2018-10-05 14:52:10.253721
Running in virtual environment at /home/user/.virtualenv/angr-dev
Platform: linux-x86_64
Python version: 3.5.3 (fdd60ed87e94, Apr 24 2018, 06:10:04)
[PyPy 6.0.0 with GCC 6.2.0 20160901]
######## angr #########
Python found it in /home/user/angr-dev/angr/angr
Pip version angr 8.18.10.1
Git info:
	Current commit 63b6b4eeb456c6c27fd96a839d5c601b8b99914b from branch master
	Checked out from remote origin: ssh://[email protected]/angr/angr
######## ailment #########
Python found it in /home/user/angr-dev/ailment/ailment
Pip version ailment 8.18.10.1
Git info:
	Current commit 966d5c57dd04f2e43f73b165ddca18166b249f85 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/ailment
######## cle #########
Python found it in /home/user/angr-dev/cle/cle
Pip version cle 8.18.10.1
Git info:
	Current commit c56152f6b8e199bd897b80115e0a9cf43bb70f5d from branch master
	Checked out from remote origin: ssh://[email protected]/angr/cle
######## pyvex #########
Python found it in /home/user/angr-dev/pyvex/pyvex
Pip version pyvex 8.18.10.1
Git info:
	Current commit 14169efac878bad0b10d9e7333efbb49c45921d0 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/pyvex
######## claripy #########
Python found it in /home/user/angr-dev/claripy/claripy
Pip version claripy 8.18.10.1
Git info:
	Current commit f4f2cbe47ddfe1c2cda9725846b3e9562c30ca92 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/claripy
######## archinfo #########
Python found it in /home/user/angr-dev/archinfo/archinfo
Pip version archinfo 8.18.10.1
Git info:
	Current commit 0b8bf512c88ecfef6ac7bfe78fb9f263f88e54e5 from branch master
	Checked out from remote origin: ssh://[email protected]/angr/archinfo
######## ana #########
Python found it in /home/user/angr-dev/ana/ana
Pip version ana 0.5
Git info:
	Current commit 48657dc6500e33f5818b98003f1f179bfe03e1cc from branch master
	Checked out from remote origin: https://git:@github.com/zardus/ana
######## z3 #########
Python found it in /home/user/.virtualenv/angr-dev/site-packages/z3
Pip version not found!
Couldn't find git info
######## unicorn #########
Python found it in /home/user/.virtualenv/angr-dev/site-packages/unicorn
Pip version unicorn 1.0.1
Couldn't find git info

How to use extra_constraints

Hi,
thanks in advance for your help:

my code is the following:

import claripy
s = claripy.Solver()
x = claripy.BVS("x",64)
ten = claripy.BVV(10,64)
s.add(x==ten)
print s.satisfiable()
print s.satisfiable(extra_constraints=(x == 2))

The first satisfiable returns True as expected but for the second I have the following error:

Traceback (most recent call last):
  File "a.py", line 12, in <module>
    print s.satisfiable(extra_constraints=(x == 2))
  File "/usr/local/lib/python2.7/dist-packages/claripy/frontend_mixins/constraint_filter_mixin.py", line 30, in satisfiable
    ec = self._constraint_filter(extra_constraints)
  File "/usr/local/lib/python2.7/dist-packages/claripy/frontend_mixins/constraint_filter_mixin.py", line 3, in _constraint_filter
    if len(constraints) == 0:
TypeError: object of type 'Bool' has no len()

Could you tell me how to add properly that kind of extra constraint?

Thanks

Document the relation between AST/Frontend/FrontendMixin/Backend

The following is quoted from @zardus in the Slack channel. We should put them in the documentation.

generally speaking:

claripy abstracts expressions using claripy.AST objects
Frontends provide different paradigms for handling those expressions. The FullFrontend (should really be named SolverFrontend or something) handles them using something like an SMT solver, LightFrontend (should really be named ApproximationFrontend or something) handles them by using an abstract (and approximating) data domain.
each Frontend needs to, at some point, do actual operation and evaluations on the AST. ASTs don't support this on their own. Instead, Backends translate ASTs into BackendObjects (i.e., python primitives, Z3 expressions, strided intervals for VSA, etc) and also handle the appropriate state-tracking objects (such as Z3 solvers)
Frontends take ASTs as inputs and use Backends to backend.convert() those ASTs into BackendObjects that can be evaluated and otherwise reasoned about
FrontendMixins customize the operation of Frontends. For example, ModelCacheMixin caches solutions from an SMT solver

How t programmatically add constraints?

Hi all,
let's supposed i have created the 2 claripy.BV() objects called A and B. Supposed that as a parameter I receive O that is just the operation. Is it possible to do something like:

s.add(A O B)

so if O is < s.add(A< B) will be added instead if O is > s.add(A > B) would added?

So, I do need to specify the operation at runtime but I would not use if in the code.

Thanks

Make solver able to solve what returned by mem[...]

As discussed on Slack, state.mem returns "something" that you cannot use with state.solver.
Example:

In [23]: a.mem[a.regs.rcx+40].int
Out[23]: <int (32 bits) <BV32 0xfc18eda3> at 0xc0000fef
In [24]: a.memory.load(a.regs.rcx+40,size=4)
Out[24]: <BV32 0xa3ed18fc>

but

In [21]: hex(a.solver.eval_one(a.memory.load(a.regs.rcx+40,size=4)))
Out[21]: '0xa3ed18fc'
In [22]: hex(a.solver.eval_one(a.mem[a.regs.rcx+40].int))
...

~/angr-dev/angr/angr/state_plugins/view.py in __getattr__(self, k)
    206         if k in SimMemView.types:
    207             return self._deeper(ty=SimMemView.types[k].with_arch(self.state.arch))
--> 208         raise AttributeError(k)
    209 
    210     def __setattr__(self, k, v):
AttributeError: cache_key

ClaripyZeroDivisionError in the cache mixin

There is a bug in the mixin that do caching. Here is how to reproduce it:

import claripy
 
num = claripy.BVS('num', 256)
denum = claripy.BVS('denum', 256)
e = claripy.BVS('e', 256)
 
# s = claripy.SolverCacheless()  # With this solver, it succeeds
s = claripy.Solver()  # With this solver, it fails
 
s.add(e == 8)
s.satisfiable()
s.add(claripy.If(denum == 0, 0, num / denum) == e)
s.satisfiable()

As you can see, with a SolverCacheless() instance, the script works fine. With a Solver() (or CompositeSolver()), it raises an exception in the cache mixin.

a check is added to disrupt the z3 backend

In the backends/backend_z3.py, the function _add() has a check added recently to avoids to add some already seen constraints(?), which seems to me, does not make much sense, and causes abnormal behavior like generating conflicting constraints, I believe this is the root cause of angr/angr#1517.
simply remove this check should fix this issue.

   def _add(self, s, c, track=False):
        if track:
            for constraint in c:
                name = str(hash(constraint))
                if name not in self._hash_to_constraint: // why is this line added?
                    self._hash_to_constraint[name] = constraint
                    s.assert_and_track(constraint, name)
        else:
            s.add(*c)

Unable to import claripy in MAC

I installed claripy with pip using pip install claripy

After installation, I tried importing it and then I got this error

Traceback (most recent call last):
File "", line 1, in
File "/Library/Python/2.7/site-packages/claripy/init.py", line 17, in
from . import backends as _backends_module
File "/Library/Python/2.7/site-packages/claripy/backends/init.py", line 1, in
from .backend_z3 import BackendZ3
File "/Library/Python/2.7/site-packages/claripy/backends/backend_z3.py", line 43, in
z3.init(z3_path)
AttributeError: 'module' object has no attribute 'init'

Constrained bytes in files vs. bytes in symbolic variables difference

When a byte in a file is constrained the bit index in the constraint starts at 0, e.g. file[7:0] for the first byte of the file. When a byte in a variable is constrained the bit index starts at VARIABLE_LENGTH-1, e.g. arg[39:32] for a variable that is 40 bits long. This appears to be a recent change.

I have code that attempts to answer the question is byte X in file/arg constrained. It would help if there was some consistency in how bytes are represented as constraints.

Restore docstrings lost during the solver redesign

We lost all the docstrings on claripy.Frontend. It would be great to restore them, and propagate them through the inheritance tree to the various Solvers (in claripy/solvers.py).

Small bug in replacement solver

I believe Line 82 of replacement_frontend.py incorrectly iterates over the self._replacements dictionary:

Original:
self._replacements = {k: v for k, v in self._replacements if k not in old_entries}

Probably intended behavior:
self._replacements = {k: v for k, v in self._replacements.iteritems() if k not in old_entries}

The current code will throw an exception on use (so I'm guessing it's not actually being used?).

Threading error in z3

The following scriptto solve level 6 of the CMU binary bomb causes a segfault in z3 when using more than one thread.
z3 should be thread safe unless the Context object is shared between threads.

import angr
import logging
import claripy
import simuvex
from struct import unpack
from IPython import embed
from ipdb import set_trace

stored_ints_addr = 0
bvs = None


class custom_hook(simuvex.SimProcedure):

    def run(self, s1_addr, int_addr):
        print "read_six_numbers hook"
        global stored_ints_addr
        global bvs
        for i in range(6):
            bvs = self.state.se.BVS(
                "int{}".format(i), 8 * 4, explicit_name=True)
            self.state.add_constraints(bvs >= 1, bvs < 6)
            self.state.memory.store(int_addr + i * 4, bvs,
                                    endness=self.state.arch.memory_endness)
            # let's keep this for later
            stored_ints_addr = int_addr

            return self.state.se.BVV(6, self.state.arch.bits)


def solve_flag_6():

    start = 0x4010f4
    read_num = 0x40145c
    find = 0x4011f7
    avoid = (0x4011e9, 0x401140, 0x401123,)

    p = angr.Project("./bomb", load_options={'auto_load_libs': False})
    p.hook(read_num, custom_hook)
    state = p.factory.blank_state(
        addr=start, remove_options={simuvex.o.LAZY_SOLVES})
    pg = p.factory.path_group(state, threads=4)
    pg.explore(find=find, avoid=avoid)
    found = pg.found[0].state
    set_trace()

    return unpack('IIIIII', found.se.any_str(found.memory.load(stored_ints_addr, 24)))


def main():
    print("Flag 6:" + str(solve_flag_6()))

if __name__ == '__main__':
    # logging.getLogger('angr.path_group').setLevel(logging.DEBUG)
    main()

Unable to find libz3.so

When importing angr I get an error in Claripy. I have z3 installed and I can import it. Here's the error I get:

  File "<stdin>", line 1, in <module>
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/angr/__init__.py", line 7, in <module>
    from .project import *
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/angr/project.py", line 10, in <module>
    import cle
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/cle/__init__.py", line 4, in <module>
    from .loader import *
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/cle/loader.py", line 8, in <module>
    import claripy
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/claripy/__init__.py", line 16, in <module>
    from . import backends as _backends_module
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/claripy/backends/__init__.py", line 1, in <module>
    from .backend_z3 import BackendZ3
  File "(home directory).virtualenvs/angr/lib/python2.7/site-packages/claripy/backends/backend_z3.py", line 57, in <module>
    raise ClaripyZ3Error("Unable to find %s", z3_library_file)
claripy.errors.ClaripyZ3Error: ('Unable to find %s', 'libz3.so')

Need a concept of operator precedence in claripy op rendering

It would be nice to extend the way Base._op_repr worked to make it so that it put parentheses only where they needed to go.

Satisfiability bug with CompositeFrontend

Hello !

I have found a sequence of step that makes the CompositeFrontend return invalid satisfiability.

I will just drop you the script to reproduce the issue :

import claripy

full_frontend = claripy.FullFrontend(claripy.backends.z3)
s =  claripy.CompositeFrontend(full_frontend)

#s = claripy.Solver()

c = claripy.BVS('test', 32)
s.add(c[7:0] != 0)

print(s.satisfiable())

s.add(c == 0)

s.satisfiable(extra_constraints=[claripy.BVS('lol', 32)==0])

print(s.satisfiable())

You can see that at the end, the constraints are clearly not satisfiable (c must be null but not null), but my satisfiable() call with extra_constraints containing another variable seems to confuse the CompositeFrontend.

If you remove that satisfiable(extra_constraints=...), or if you use the default claripy.Solver(), the bug will not appear.

Thanks :)

Base.nonzero breaks Base.depth

I have a use case where I was checking the depth of a constraint. In Base._depth the following code is executed,

angr/claripy/ast/base.py

389        for a in ast_args:
390            if a not in memoized:

If a is an AST with depth 1 and memoized contains an element whose key is another AST with depth 1, then Base.__nonzero__ will eventually be called causing a ClaripyOperationError due to the truthness of the AST being tested.

  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 377, in depth
    return self._depth()
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 391, in _depth
    memoized[a] = a._depth(memoized)
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 390, in _depth
    if a not in memoized:
  File "/usr/local/lib/python2.7/dist-packages/claripy/ast/base.py", line 537, in __nonzero__
    raise ClaripyOperationError('testing Expressions for truthiness does not do what you want, as these expressions can be symbolic')
ClaripyOperationError: testing Expressions for truthiness does not do what you want, as these expressions can be symbolic
Uncaught exception. Entering post mortem debugging
Running 'cont' or 'step' will restart the program
> /usr/local/lib/python2.7/dist-packages/claripy/ast/base.py(537)__nonzero__()
-> raise ClaripyOperationError('testing Expressions for truthiness does not do what you want, as these expressions can be symbolic')

Since the python stack trace did not show a direct call to Base.__nonzero__ I traced python to see where the call was made.

Breakpoint 1, PyObject_IsTrue (v=v@entry=<Bool at remote 0x7f45238e7e90>)
    at ../Objects/object.c:1568
1568    in ../Objects/object.c
(gdb) info stack
#0  PyObject_IsTrue (v=v@entry=<Bool at remote 0x7f45238e7e90>)
    at ../Objects/object.c:1568
#1  0x0000000000562761 in PyObject_RichCompareBool (v=<optimized out>, 
    w=<optimized out>, op=<optimized out>) at ../Objects/object.c:1010
#2  0x0000000000562908 in lookdict.18241 (mp=0x7f452f5f86e0, 
    key=<optimized out>, hash=-4146926773084927565)
    at ../Objects/dictobject.c:342
#3  0x0000000000522dd7 in PyDict_Contains (
    op={<BV at remote 0x7f452f1a12a8>: 1, <BV at remote 0x7f4524bc12a8>: 2, <BV at remote 0x7f452e6da438>: 1, <BV at remote 0x7f452e914d98>: 1, <Bool at remote 0x7f4524ba2b90>: 3}, key=<optimized out>) at ../Objects/dictobject.c:2292

It appears that PyObject_RichCompareBool decides that if the object is not a bool then it will check to see if it is true, which results in the call to Base.__nonzero__.

Is Base.__nonzero__ still necessary or can it be removed to fix this issue?

extracting constraints in smt2 format for z3

I am trying to extract all the constraints passed to the z3 solver even in case of timeout, exception, etc. I thus considered the backend_z3 and in particular the __batch_eval() function. I want the output in a smt2 syntax so that I can then process the extracted constraints with the standalone version of z3.

I thus added the following code in __batch_eval() just before the end of the function.

            smt_file = open("/results/be-query.smt2", 'a')
            mysolver = solver
            mysolver.add(self._op_raw_Not(self._op_raw_And(*[(ex == ex_v) for ex, ex_v in zip(exprs, r)])))
            f = mysolver
            v = (z3.Ast * 0)()
            if isinstance(f, z3.Solver):
                # print "solver is an instance of z3.Solver"
                a = f.assertions()
                if len(a) == 0:
                    f = z3.BoolVal(True)
                else:
                    f = z3.And(*a)
            z3.Z3_set_ast_print_mode(f.ctx_ref(), z3.Z3_PRINT_SMTLIB2_COMPLIANT)
            ste_expr = z3.Z3_benchmark_to_smtlib_string(f.ctx_ref(), "", "QF_AUFBV", None, "", 0, v, f.as_ast())
            smt_file.write(ste_expr)
            smt_file.write('\n')
            smt_file.close()

I tried it with a set of binaries and it works pretty well. The extracted smt2 files can be easily used with the standalone version of z3.

Unfortunately, extending my test with a large dataset of real malware, I found that I do not always have a consistent behaviour. A large number of binary (about 75%) do not produce any smt2 file. In other cases, when the smt2 file is generated, re-running angr on the same binary: I could have no file or the produced smt2 files differ significantly.

Missed easy simplification opportunity?

I have a rather complicated symbolic expression:

In [70]: sttest.regs.rbx                                                                                                                                                                     
Out[70]: <BV64 ((if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 190)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 180)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 222)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 192)))))))))) .. 0x0 .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then loadme_55_8 else 0))))))))) + stack2_59_64>

If I concretize it:

In [72]: hex(sttest.solver.eval(stack1))                                                                                                                                                         
Out[72]: '0x601006'

In [74]: sttest.add_constraints(stack1 == 0x601006)                                                                                                                                          

In [75]: sttest.WARNING | 2020-02-07 15:26:50,783 | angr.state_plugins.abstract_memory | Option "REGION_MAPPING" must be enabled when using SimAbstractMemory as the memory model. The option is added to state options as a courtesy.
CRITICAL | 2020-02-07 15:26:50,813 | angr.sim_state | The name state.se is deprecated; please use state.solver.
In [75]: sttest.satisfiable()                                                                                                                                                                
Out[75]: True

In [76]: sttest.regs.rbx                                                                                                                                                                     
Out[76]: <BV64 ((if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 190)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 180)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 222)))))))))) .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then 0 else (if stack1_58_64 == 0x601009 then 0 else (if stack1_58_64 == 0x601008 then 0 else 192)))))))))) .. 0x0 .. (if stack1_58_64 == 0x60100d then 0 else (if stack1_58_64 == 0x601007 then 0 else (if stack1_58_64 == 0x60100c then 0 else (if stack1_58_64 == 0x601006 then 0 else (if stack1_58_64 == 0x60100b then 0 else (if stack1_58_64 == 0x601005 then 0 else (if stack1_58_64 == 0x60100a then 0 else (if stack1_58_64 == 0x601004 then loadme_55_8 else 0))))))))) + stack2_59_64>

So after concretizing stack1 the complicated expression based on it is not simplified.

Indeed:

In [81]: sttest.solver.is_true(stack1 == 0x60100d)                                                                                                                                           
Out[81]: False

Am I doing something wrong? Is there a better way to concretize a symbolic variable to concrete bitvector so that simplifications can happen?

Get result from simplify()

Simplify, which is overloaded in every backends, only prints its result and returns None. Is it a problem if I try to make it return its result ? (if it is possible in its actual implementation)

Missing docstrings (Claripy)

There are lots of missing module, class, and function docstrings in the angr module. Here is the list. We desperately need help with this from the community, if someone wants to contribute!

Here is the list:

************* Module claripy.balancer
- balancer.py:1 - 
- balancer.py:33 - Balancer.compat_ret
- balancer.py:36 - Balancer._replacements_iter
- balancer.py:47 - Balancer._add_lower_bound
- balancer.py:62 - Balancer._add_upper_bound
- balancer.py:78 - Balancer.replacements
- balancer.py:85 - Balancer._same_bound_bv
- balancer.py:92 - Balancer._cardinality
- balancer.py:96 - Balancer._min
- balancer.py:102 - Balancer._max
- balancer.py:107 - Balancer._range
- balancer.py:111 - Balancer._invert_comparison
- balancer.py:118 - Balancer._align_truism
- balancer.py:146 - Balancer._reverse_comparison
- balancer.py:166 - Balancer._align_bv
- balancer.py:176 - Balancer._align___sub__
- balancer.py:219 - Balancer._queue_truism
- balancer.py:225 - Balancer._queue_truisms
- balancer.py:283 - Balancer._unpack_truisms_And
- balancer.py:286 - Balancer._unpack_truisms_Not
- balancer.py:294 - Balancer._unpack_truisms_Or
- balancer.py:326 - Balancer._balance
- balancer.py:359 - Balancer._balance_Reverse
- balancer.py:366 - Balancer._balance___add__
- balancer.py:374 - Balancer._balance___sub__
- balancer.py:382 - Balancer._balance_ZeroExt
- balancer.py:394 - Balancer._balance_SignExt
- balancer.py:408 - Balancer._balance_Extract
- balancer.py:443 - Balancer._balance_Concat
- balancer.py:457 - Balancer._balance_If
- balancer.py:495 - Balancer._handle
- balancer.py:550 - Balancer._handle___eq__
- balancer.py:564 - Balancer._handle___ne__
- balancer.py:575 - Balancer._handle_If
- balancer.py:594 - is_true
- balancer.py:595 - is_false
************* Module claripy.frontend
- frontend.py:1 - 
- frontend.py:8 - Frontend
- frontend.py:17 - Frontend.uuid
- frontend.py:26 - Frontend.branch
- frontend.py:29 - Frontend._blank_copy
- frontend.py:36 - Frontend.finalize
- frontend.py:39 - Frontend.merge
- frontend.py:42 - Frontend.combine
- frontend.py:45 - Frontend.split
- frontend.py:48 - Frontend.add
- frontend.py:51 - Frontend.simplify
- frontend.py:54 - Frontend.solve
- frontend.py:57 - Frontend.satisfiable
- frontend.py:60 - Frontend.eval_to_ast
- frontend.py:63 - Frontend.eval
- frontend.py:66 - Frontend.batch_eval
- frontend.py:69 - Frontend.max
- frontend.py:72 - Frontend.min
- frontend.py:75 - Frontend.solution
- frontend.py:78 - Frontend.is_true
- frontend.py:81 - Frontend.is_false
- frontend.py:84 - Frontend.downsize
************* Module claripy.annotation
- annotation.py:1 - 
************* Module claripy.ast.vs
- ast/vs.py:1 - 
- ast/vs.py:3 - VS
************* Module claripy.ast.base
- ast/base.py:1 - 
- ast/base.py:21 - _inner_repr
- ast/base.py:27 - ASTCacheKey
- ast/base.py:38 - _make_name
- ast/base.py:172 - Base._get_hashables
- ast/base.py:234 - Base.uuid
- ast/base.py:241 - Base.cache_key
- ast/base.py:273 - Base.make_like
- ast/base.py:280 - Base._rename
- ast/base.py:290 - Base._apply_to_annotations
- ast/base.py:369 - Base.dbg_repr
- ast/base.py:386 - Base._type_name
- ast/base.py:389 - Base.shallow_repr
- ast/base.py:494 - Base.recursive_children_asts
- ast/base.py:503 - Base.recursive_leaf_asts
- ast/base.py:506 - Base._recursive_leaf_asts
- ast/base.py:522 - Base.dbg_is_looped
- ast/base.py:702 - Base._check_replaceability
- ast/base.py:708 - Base._identify_vars
- ast/base.py:720 - Base.canonicalize
- ast/base.py:736 - Base._burrow_ite
- ast/base.py:772 - Base._excavate_ite
- ast/base.py:844 - Base._first_backend
- ast/base.py:853 - Base.singlevalued
- ast/base.py:857 - Base.multivalued
- ast/base.py:861 - Base.cardinality
- ast/base.py:865 - Base.concrete
- ast/base.py:897 - Base.model
- ast/base.py:922 - simplify
************* Module claripy.ast.int
- ast/int.py:1 - 
- ast/int.py:3 - Int
************* Module claripy.ast.fp
- ast/fp.py:1 - 
- ast/fp.py:4 - FP
- ast/fp.py:5 - FP.to_fp
- ast/fp.py:11 - FP.raw_to_fp
- ast/fp.py:14 - FP.to_bv
- ast/fp.py:18 - FP.sort
- ast/fp.py:53 - _fp_length_calc
- ast/fp.py:73 - _fp_cmp_check
- ast/fp.py:85 - _fp_binop_check
- ast/fp.py:87 - _fp_binop_length
************* Module claripy.ast.bits
- ast/bits.py:1 - 
- ast/bits.py:3 - Bits
- ast/bits.py:17 - Bits.size
************* Module claripy.ast.bv
- ast/bv.py:1 - 
- ast/bv.py:8 - cleanup
- ast/bv.py:14 - BV
- ast/bv.py:108 - BV._from_int
- ast/bv.py:112 - BV._from_long
- ast/bv.py:116 - BV._from_str
- ast/bv.py:120 - BV._from_BVV
- ast/bv.py:123 - BV.signed_to_fp
- ast/bv.py:129 - BV.unsigned_to_fp
- ast/bv.py:134 - BV.raw_to_fp
- ast/bv.py:138 - BV.to_bv
- ast/bv.py:201 - SI
- ast/bv.py:210 - TSI
- ast/bv.py:214 - ESI
- ast/bv.py:217 - ValueSet
- ast/bv.py:222 - DSIS
************* Module claripy.ast.bool
- ast/bool.py:1 - 
- ast/bool.py:10 - cleanup
- ast/bool.py:16 - Bool
- ast/bool.py:18 - Bool._from_bool
- ast/bool.py:48 - BoolV
- ast/bool.py:76 - If
- ast/bool.py:130 - is_true
- ast/bool.py:138 - is_false
- ast/bool.py:146 - ite_dict
- ast/bool.py:149 - ite_cases
************* Module claripy.ast
- ast/__init__.py:1 - 
- ast/__init__.py:13 - _import
************* Module claripy.errors
- errors.py:1 - 
- errors.py:1 - ClaripyError
- errors.py:4 - UnsatError
- errors.py:7 - ClaripyFrontendError
- errors.py:10 - ClaripySerializationError
- errors.py:13 - BackendError
- errors.py:16 - ClaripyZ3Error
- errors.py:19 - ClaripyBackendVSAError
- errors.py:26 - ClaripyASTError
- errors.py:29 - ClaripyBalancerError
- errors.py:32 - ClaripyBalancerUnsatError
- errors.py:35 - ClaripyTypeError
- errors.py:38 - ClaripyValueError
- errors.py:41 - ClaripySizeError
- errors.py:44 - ClaripyOperationError
- errors.py:47 - ClaripyReplacementError
- errors.py:50 - ClaripyRecursionError
************* Module claripy.backend_manager
- backend_manager.py:1 - 
- backend_manager.py:1 - BackendManager
- backend_manager.py:9 - BackendManager._register_backend
- backend_manager.py:25 - BackendManager.downsize
************* Module claripy.vsa.errors
- vsa/errors.py:1 - 
- vsa/errors.py:4 - ClaripyVSAError
- vsa/errors.py:7 - ClaripyVSAOperationError
************* Module claripy.vsa.abstract_location
- vsa/abstract_location.py:1 - 
- vsa/abstract_location.py:3 - Segment
- vsa/abstract_location.py:11 - AbstractLocation
- vsa/abstract_location.py:21 - AbstractLocation._add_segment
- vsa/abstract_location.py:73 - AbstractLocation.basicblock_key
- vsa/abstract_location.py:77 - AbstractLocation.statement_id
- vsa/abstract_location.py:81 - AbstractLocation.region
- vsa/abstract_location.py:85 - AbstractLocation.segments
- vsa/abstract_location.py:88 - AbstractLocation.update
- vsa/abstract_location.py:93 - AbstractLocation.copy
- vsa/abstract_location.py:97 - AbstractLocation.merge
************* Module claripy.vsa.bool_result
- vsa/bool_result.py:1 - 
- vsa/bool_result.py:3 - BoolResult
- vsa/bool_result.py:8 - BoolResult.value
- vsa/bool_result.py:26 - BoolResult.identical
- vsa/bool_result.py:35 - BoolResult.union
- vsa/bool_result.py:38 - BoolResult.size
- vsa/bool_result.py:42 - BoolResult.is_maybe
- vsa/bool_result.py:49 - BoolResult.has_true
- vsa/bool_result.py:56 - BoolResult.has_false
- vsa/bool_result.py:63 - BoolResult.is_true
- vsa/bool_result.py:70 - BoolResult.is_false
- vsa/bool_result.py:76 - TrueResult
- vsa/bool_result.py:121 - FalseResult
- vsa/bool_result.py:161 - MaybeResult
************* Module claripy.vsa.valueset
- vsa/valueset.py:1 - 
- vsa/valueset.py:5 - normalize_types
- vsa/valueset.py:21 - normalize_types_one_arg
- vsa/valueset.py:36 - ValueSet
- vsa/valueset.py:69 - ValueSet.name
- vsa/valueset.py:73 - ValueSet.regions
- vsa/valueset.py:77 - ValueSet.reversed
- vsa/valueset.py:81 - ValueSet.unique
- vsa/valueset.py:85 - ValueSet.bits
- vsa/valueset.py:89 - ValueSet.cardinality
- vsa/valueset.py:97 - ValueSet.set_si
- vsa/valueset.py:103 - ValueSet.get_si
- vsa/valueset.py:109 - ValueSet.items
- vsa/valueset.py:112 - ValueSet.size
- vsa/valueset.py:116 - ValueSet.merge_si
- vsa/valueset.py:123 - ValueSet.remove_si
- vsa/valueset.py:254 - ValueSet.eval
- vsa/valueset.py:263 - ValueSet.copy
- vsa/valueset.py:270 - ValueSet.reverse
- vsa/valueset.py:279 - ValueSet.is_empty
- vsa/valueset.py:311 - ValueSet.concat
- vsa/valueset.py:328 - ValueSet.union
- vsa/valueset.py:343 - ValueSet.widen
************* Module claripy.vsa.discrete_strided_interval_set
- vsa/discrete_strided_interval_set.py:1 - 
- vsa/discrete_strided_interval_set.py:8 - apply_on_each_si
- vsa/discrete_strided_interval_set.py:10 - apply_on_each_si.operator
- vsa/discrete_strided_interval_set.py:35 - convert_operand_to_si
- vsa/discrete_strided_interval_set.py:37 - convert_operand_to_si.converter
- vsa/discrete_strided_interval_set.py:47 - collapse_operand
- vsa/discrete_strided_interval_set.py:49 - collapse_operand.collapser
- vsa/discrete_strided_interval_set.py:109 - DiscreteStridedIntervalSet.number_of_values
- vsa/discrete_strided_interval_set.py:120 - DiscreteStridedIntervalSet.should_collapse
- vsa/discrete_strided_interval_set.py:571 - DiscreteStridedIntervalSet._update_bounds
- vsa/discrete_strided_interval_set.py:587 - DiscreteStridedIntervalSet._update_bits
************* Module claripy.vsa.strided_interval
- vsa/strided_interval.py:1 - 
- vsa/strided_interval.py:11 - reversed_processor
- vsa/strided_interval.py:12 - reversed_processor.processor
- vsa/strided_interval.py:21 - normalize_types
- vsa/strided_interval.py:325 - StridedInterval.copy
- vsa/strided_interval.py:336 - StridedInterval.nameless_copy
- vsa/strided_interval.py:347 - StridedInterval.normalize
- vsa/strided_interval.py:405 - StridedInterval._normalize_top
- vsa/strided_interval.py:1074 - StridedInterval.name
- vsa/strided_interval.py:1078 - StridedInterval.reversed
- vsa/strided_interval.py:1082 - StridedInterval.size
- vsa/strided_interval.py:1087 - StridedInterval.cardinality
- vsa/strided_interval.py:1130 - StridedInterval.lower_bound
- vsa/strided_interval.py:1138 - StridedInterval.upper_bound
- vsa/strided_interval.py:1146 - StridedInterval.bits
- vsa/strided_interval.py:1150 - StridedInterval.stride
- vsa/strided_interval.py:1188 - StridedInterval.unique
- vsa/strided_interval.py:1191 - StridedInterval._min_bits
- vsa/strided_interval.py:1234 - StridedInterval.is_interval
- vsa/strided_interval.py:1239 - StridedInterval.n_values
- vsa/strided_interval.py:1247 - StridedInterval._modular_add
- vsa/strided_interval.py:1251 - StridedInterval._modular_sub
- vsa/strided_interval.py:1255 - StridedInterval._modular_mul
- vsa/strided_interval.py:1286 - StridedInterval.highbit
- vsa/strided_interval.py:1290 - StridedInterval.min_bits
- vsa/strided_interval.py:1308 - StridedInterval.max_int
- vsa/strided_interval.py:1312 - StridedInterval.min_int
- vsa/strided_interval.py:1316 - StridedInterval.signed_max_int
- vsa/strided_interval.py:1321 - StridedInterval.signed_min_int
- vsa/strided_interval.py:1326 - StridedInterval._to_negative
- vsa/strided_interval.py:1406 - StridedInterval.empty
- vsa/strided_interval.py:2036 - StridedInterval.bitwise_and.number_of_ones
- vsa/strided_interval.py:2082 - StridedInterval._pre_shift
- vsa/strided_interval.py:2090 - StridedInterval._pre_shift.get_range.round
- vsa/strided_interval.py:2167 - StridedInterval.lshift
- vsa/strided_interval.py:2195 - StridedInterval.cast_low
- vsa/strided_interval.py:2249 - StridedInterval.concat
- vsa/strided_interval.py:2271 - StridedInterval.extract
- vsa/strided_interval.py:2453 - StridedInterval._ntz.bits
- vsa/strided_interval.py:2513 - StridedInterval._union
- vsa/strided_interval.py:2697 - StridedInterval.sign
- vsa/strided_interval.py:2729 - StridedInterval.diop_natural_solution_linear.get_intersection
- vsa/strided_interval.py:2882 - StridedInterval.intersection
- vsa/strided_interval.py:2891 - StridedInterval._multi_valued_intersection
- vsa/strided_interval.py:3077 - StridedInterval.widen
************* Module claripy.vsa
- vsa/__init__.py:1 - 
************* Module claripy.backend
- backend.py:1 - 
- backend.py:63 - Backend._object_cache
- backend.py:70 - Backend._make_raw_ops
- backend.py:185 - Backend.convert_list
- backend.py:243 - Backend.simplify
- backend.py:248 - Backend._simplify
- backend.py:760 - Backend.singlevalued
- backend.py:763 - Backend.multivalued
************* Module claripy.frontends.replacement_frontend
- frontends/replacement_frontend.py:1 - 
- frontends/replacement_frontend.py:11 - ReplacementFrontend
- frontends/replacement_frontend.py:26 - ReplacementFrontend.add_replacement
- frontends/replacement_frontend.py:54 - ReplacementFrontend._replacement
- frontends/replacement_frontend.py:66 - ReplacementFrontend._add_solve_result
- frontends/replacement_frontend.py:130 - ReplacementFrontend._replace_list
************* Module claripy.frontends.light_frontend
- frontends/light_frontend.py:1 - 
- frontends/light_frontend.py:8 - LightFrontend
************* Module claripy.frontends.constrained_frontend
- frontends/constrained_frontend.py:1 - 
- frontends/constrained_frontend.py:10 - ConstrainedFrontend
- frontends/constrained_frontend.py:36 - ConstrainedFrontend.independent_constraints
- frontends/constrained_frontend.py:72 - ConstrainedFrontend._satisfiable
************* Module claripy.frontends.composite_frontend
- frontends/composite_frontend.py:1 - 
- frontends/composite_frontend.py:9 - CompositeFrontend
- frontends/composite_frontend.py:33 - CompositeFrontend._solver_list
- frontends/composite_frontend.py:43 - CompositeFrontend.variables
- frontends/composite_frontend.py:47 - CompositeFrontend.constraints
- frontends/composite_frontend.py:50 - CompositeFrontend._solvers_for_variables
- frontends/composite_frontend.py:62 - CompositeFrontend._merged_solver_for
- frontends/composite_frontend.py:87 - CompositeFrontend._variable_sets
- frontends/composite_frontend.py:90 - CompositeFrontend._shared_varsets
- frontends/composite_frontend.py:99 - CompositeFrontend._add_dependent_constraints
- frontends/composite_frontend.py:149 - CompositeFrontend._all_variables
- frontends/composite_frontend.py:229 - CompositeFrontend.timeout
- frontends/composite_frontend.py:240 - CompositeFrontend._solver_backend
************* Module claripy.frontends.full_frontend
- frontends/full_frontend.py:1 - 
- frontends/full_frontend.py:11 - FullFrontend
- frontends/full_frontend.py:38 - FullFrontend._get_solver
************* Module claripy.frontends.caching_frontend
- frontends/caching_frontend.py:1 - 
- frontends/caching_frontend.py:11 - CachingFrontend
- frontends/caching_frontend.py:87 - CachingFrontend._filter_single_constraint
- frontends/caching_frontend.py:99 - CachingFrontend._constraint_filter
- frontends/caching_frontend.py:113 - CachingFrontend._add_constraints
- frontends/caching_frontend.py:116 - CachingFrontend._simplify
- frontends/caching_frontend.py:119 - CachingFrontend._solve
- frontends/caching_frontend.py:122 - CachingFrontend._eval
- frontends/caching_frontend.py:125 - CachingFrontend._batch_eval
- frontends/caching_frontend.py:128 - CachingFrontend._min
- frontends/caching_frontend.py:131 - CachingFrontend._max
- frontends/caching_frontend.py:134 - CachingFrontend._solution
- frontends/caching_frontend.py:137 - CachingFrontend._is_true
- frontends/caching_frontend.py:140 - CachingFrontend._is_false
- frontends/caching_frontend.py:159 - CachingFrontend._cache_eval
- frontends/caching_frontend.py:167 - CachingFrontend._cache_max
- frontends/caching_frontend.py:174 - CachingFrontend._cache_min
- frontends/caching_frontend.py:291 - CachingFrontend._eager_resolution
************* Module claripy.frontends.hybrid_frontend
- frontends/hybrid_frontend.py:1 - 
- frontends/hybrid_frontend.py:11 - HybridFrontend
- frontends/hybrid_frontend.py:26 - HybridFrontend.constraints
- frontends/hybrid_frontend.py:30 - HybridFrontend.variables
- frontends/hybrid_frontend.py:34 - HybridFrontend.result
- frontends/hybrid_frontend.py:45 - HybridFrontend._hook_exact_frontend
- frontends/hybrid_frontend.py:46 - HybridFrontend._hook_exact_frontend.constraint_hook
- frontends/hybrid_frontend.py:70 - HybridFrontend._hybrid_call
- frontends/hybrid_frontend.py:158 - hybrid_vsa_z3
************* Module claripy.frontends
- frontends/__init__.py:1 - 
************* Module claripy.backend_object
- backend_object.py:1 - 
************* Module claripy.backends.backendremote
- backends/backendremote.py:1 - 
- backends/backendremote.py:10 - TrackingSolver
- backends/backendremote.py:15 - TrackingSolver.plus_extra
- backends/backendremote.py:19 - get
- backends/backendremote.py:25 - BackendRemote
- backends/backendremote.py:44 - BackendRemote.resolve
************* Module claripy.backends.backend_z3_parallel
- backends/backend_z3_parallel.py:1 - 
- backends/backend_z3_parallel.py:12 - BackendZ3Parallel
- backends/backend_z3_parallel.py:19 - BackendZ3Parallel._background
- backends/backend_z3_parallel.py:74 - BackendZ3Parallel._synchronize
- backends/backend_z3_parallel.py:86 - BackendZ3Parallel._translate
- backends/backend_z3_parallel.py:105 - BackendZ3Parallel.abstract
- backends/backend_z3_parallel.py:119 - BackendZ3Parallel.resolve
************* Module claripy.backends.backend_vsa
- backends/backend_vsa.py:1 - 
- backends/backend_vsa.py:9 - arg_filter
- backends/backend_vsa.py:11 - arg_filter.filter
- backends/backend_vsa.py:18 - normalize_arg_order
- backends/backend_vsa.py:20 - normalize_arg_order.normalizer
- backends/backend_vsa.py:33 - normalize_reversed_arguments
- backends/backend_vsa.py:35 - normalize_reversed_arguments.normalizer
- backends/backend_vsa.py:70 - BackendVSA
- backends/backend_vsa.py:95 - BackendVSA._op_add
- backends/backend_vsa.py:98 - BackendVSA._op_sub
- backends/backend_vsa.py:101 - BackendVSA._op_mul
- backends/backend_vsa.py:104 - BackendVSA._op_or
- backends/backend_vsa.py:107 - BackendVSA._op_xor
- backends/backend_vsa.py:110 - BackendVSA._op_and
- backends/backend_vsa.py:203 - BackendVSA._unique
- backends/backend_vsa.py:221 - BackendVSA.BVV
- backends/backend_vsa.py:228 - BackendVSA.BoolV
- backends/backend_vsa.py:232 - BackendVSA.And
- backends/backend_vsa.py:236 - BackendVSA.Not
- backends/backend_vsa.py:241 - BackendVSA.ULT
- backends/backend_vsa.py:246 - BackendVSA.ULE
- backends/backend_vsa.py:251 - BackendVSA.UGT
- backends/backend_vsa.py:256 - BackendVSA.UGE
- backends/backend_vsa.py:261 - BackendVSA.SLT
- backends/backend_vsa.py:266 - BackendVSA.SLE
- backends/backend_vsa.py:271 - BackendVSA.SGT
- backends/backend_vsa.py:276 - BackendVSA.SGE
- backends/backend_vsa.py:280 - BackendVSA.BVS
- backends/backend_vsa.py:287 - BackendVSA.If
- backends/backend_vsa.py:298 - BackendVSA.Or
- backends/backend_vsa.py:311 - BackendVSA.LShR
- backends/backend_vsa.py:315 - BackendVSA.Concat
- backends/backend_vsa.py:333 - BackendVSA.Extract
- backends/backend_vsa.py:346 - BackendVSA.SignExt
- backends/backend_vsa.py:356 - BackendVSA.ZeroExt
- backends/backend_vsa.py:366 - BackendVSA.Reverse
- backends/backend_vsa.py:373 - BackendVSA.union
- backends/backend_vsa.py:385 - BackendVSA.intersection
- backends/backend_vsa.py:399 - BackendVSA.widen
- backends/backend_vsa.py:410 - BackendVSA.CreateTopStridedInterval
- backends/backend_vsa.py:413 - BackendVSA.constraint_to_si
************* Module claripy.backends.backend_concrete
- backends/backend_concrete.py:1 - 
- backends/backend_concrete.py:7 - BackendConcrete
- backends/backend_concrete.py:26 - BackendConcrete.BVV
- backends/backend_concrete.py:32 - BackendConcrete.FPV
- backends/backend_concrete.py:36 - BackendConcrete._op_add
- backends/backend_concrete.py:39 - BackendConcrete._op_sub
- backends/backend_concrete.py:42 - BackendConcrete._op_mul
- backends/backend_concrete.py:45 - BackendConcrete._op_or
- backends/backend_concrete.py:48 - BackendConcrete._op_xor
- backends/backend_concrete.py:51 - BackendConcrete._op_and
- backends/backend_concrete.py:55 - BackendConcrete.BVS
- backends/backend_concrete.py:70 - BackendConcrete._If
- backends/backend_concrete.py:122 - BackendConcrete._to_primitive
************* Module claripy.backends.celeryconfig
- backends/celeryconfig.py:1 - 
************* Module claripy.backends.backend_z3
- backends/backend_z3.py:1 - 
- backends/backend_z3.py:57 - condom
- backends/backend_z3.py:70 - _raw_caller
- backends/backend_z3.py:73 - _raw_caller.raw_caller
- backends/backend_z3.py:77 - BackendZ3
- backends/backend_z3.py:115 - BackendZ3._context
- backends/backend_z3.py:123 - BackendZ3._ast_cache
- backends/backend_z3.py:131 - BackendZ3._var_cache
- backends/backend_z3.py:139 - BackendZ3._sym_cache
- backends/backend_z3.py:147 - BackendZ3._simplification_cache_key
- backends/backend_z3.py:155 - BackendZ3._simplification_cache_val
- backends/backend_z3.py:187 - BackendZ3.BVS
- backends/backend_z3.py:200 - BackendZ3.BVV
- backends/backend_z3.py:209 - BackendZ3.FPS
- backends/backend_z3.py:213 - BackendZ3.FPV
- backends/backend_z3.py:231 - BackendZ3.BoolS
- backends/backend_z3.py:235 - BackendZ3.BoolV
- backends/backend_z3.py:294 - BackendZ3._abstract_internal
- backends/backend_z3.py:438 - BackendZ3._abstract_to_primitive
- backends/backend_z3.py:479 - BackendZ3._check_and_model
- backends/backend_z3.py:500 - BackendZ3._primitive_from_model
- backends/backend_z3.py:766 - BackendZ3._op_add
- backends/backend_z3.py:769 - BackendZ3._op_sub
- backends/backend_z3.py:772 - BackendZ3._op_mul
- backends/backend_z3.py:775 - BackendZ3._op_or
- backends/backend_z3.py:778 - BackendZ3._op_xor
- backends/backend_z3.py:781 - BackendZ3._op_and
- backends/backend_z3.py:784 - BackendZ3._op_raw_And
- backends/backend_z3.py:787 - BackendZ3._op_raw_Or
- backends/backend_z3.py:790 - BackendZ3._op_raw_Not
- backends/backend_z3.py:793 - BackendZ3._op_raw_If
- backends/backend_z3.py:797 - BackendZ3._op_raw_fpToSBV
- backends/backend_z3.py:801 - BackendZ3._op_raw_fpToUBV
- backends/backend_z3.py:833 - BackendZ3._op_raw_Reverse
- backends/backend_z3.py:843 - BackendZ3._op_raw_SLT
- backends/backend_z3.py:848 - BackendZ3._op_raw_SLE
- backends/backend_z3.py:853 - BackendZ3._op_raw_SGT
- backends/backend_z3.py:858 - BackendZ3._op_raw_SGE
************* Module claripy.backends.remotetasks
- backends/remotetasks.py:1 - 
- backends/remotetasks.py:21 - init_z3_and_conns
- backends/remotetasks.py:27 - flip_dict
- backends/remotetasks.py:30 - canonicalize_all
- backends/remotetasks.py:35 - split_and_canonicalize
- backends/remotetasks.py:48 - check
- backends/remotetasks.py:81 - eval
- backends/remotetasks.py:88 - batch_eval
- backends/remotetasks.py:94 - rename_model
- backends/remotetasks.py:104 - report_sat
- backends/remotetasks.py:106 - report_sat.wrapped
- backends/remotetasks.py:112 - mongo_superset
- backends/remotetasks.py:118 - results
- backends/remotetasks.py:182 - min
- backends/remotetasks.py:189 - max
************* Module claripy.backends
- backends/__init__.py:1 - 
************* Module claripy.ops
- ops.py:1 - 
- ops.py:8 - AbstractLocation
************* Module claripy.operations
- operations.py:1 - 
- operations.py:2 - op
- operations.py:10 - op._type_fixer
- operations.py:36 - op._op
- operations.py:86 - reversed_op
- operations.py:87 - reversed_op._reversed_op
- operations.py:96 - preprocess_union
- operations.py:117 - if_simplifier
- operations.py:124 - concat_simplifier
- operations.py:190 - rshift_simplifier
- operations.py:194 - lshift_simplifier
- operations.py:200 - eq_simplifier
- operations.py:254 - ne_simplifier
- operations.py:298 - boolean_reverse_simplifier
- operations.py:322 - boolean_and_simplifier
- operations.py:338 - boolean_or_simplifier
- operations.py:354 - _flatten_simplifier
- operations.py:363 - bitwise_add_simplifier
- operations.py:371 - bitwise_mul_simplifier
- operations.py:374 - bitwise_sub_simplifier
- operations.py:380 - bitwise_xor_simplifier
- operations.py:390 - bitwise_or_simplifier
- operations.py:402 - bitwise_and_simplifier
- operations.py:414 - boolean_not_simplifier
- operations.py:453 - zeroext_simplifier
- operations.py:457 - signext_simplifier
- operations.py:463 - extract_simplifier
- operations.py:572 - length_same_check
- operations.py:575 - basic_length_calc
- operations.py:578 - extract_check
- operations.py:588 - extract_length_calc
- operations.py:591 - ext_length_calc
- operations.py:594 - concat_length_calc
************* Module claripy.fp
- fp.py:1 - 
- fp.py:7 - compare_sorts
- fp.py:9 - compare_sorts.compare_guard
- fp.py:16 - normalize_types
- fp.py:18 - normalize_types.normalize_helper
- fp.py:29 - RM
- fp.py:31 - RM.default
- fp.py:35 - RM.from_name
- fp.py:50 - FSort
- fp.py:63 - FSort.length
- fp.py:67 - FSort.from_size
- fp.py:76 - FSort.from_params
- fp.py:88 - FPV
- fp.py:217 - fpToFP
- fp.py:238 - fpToFPUnsigned
- fp.py:242 - fpToIEEEBV
- fp.py:255 - fpFP
- fp.py:271 - fpToSBV
- fp.py:282 - fpToUBV
- fp.py:294 - fpEQ
- fp.py:297 - fpNE
- fp.py:300 - fpGT
- fp.py:303 - fpGEQ
- fp.py:306 - fpLT
- fp.py:309 - fpLEQ
- fp.py:312 - fpAbs
- fp.py:315 - fpNeg
- fp.py:318 - fpSub
- fp.py:321 - fpAdd
- fp.py:324 - fpMul
- fp.py:327 - fpDiv
************* Module claripy.bv
- bv.py:1 - 
- bv.py:5 - compare_bits
- bv.py:7 - compare_bits.compare_guard
- bv.py:17 - compare_bits_0_length
- bv.py:19 - compare_bits_0_length.compare_guard
- bv.py:26 - normalize_types
- bv.py:28 - normalize_types.normalize_helper
- bv.py:42 - BVV
- bv.py:69 - BVV.value
- bv.py:77 - BVV.signed
- bv.py:247 - BVV.size
- bv.py:257 - BitVecVal
- bv.py:260 - ZeroExt
- bv.py:263 - SignExt
- bv.py:266 - Extract
- bv.py:269 - Concat
- bv.py:278 - RotateRight
- bv.py:281 - RotateLeft
- bv.py:284 - Reverse
- bv.py:303 - ULT
- bv.py:308 - UGT
- bv.py:313 - ULE
- bv.py:318 - UGE
- bv.py:323 - SLT
- bv.py:328 - SGT
- bv.py:333 - SLE
- bv.py:338 - SGE
- bv.py:346 - BoolV
- bv.py:349 - And
- bv.py:352 - Or
- bv.py:355 - Not
- bv.py:359 - normalizer
- bv.py:362 - If
- bv.py:369 - LShR
************* Module claripy.result
- result.py:1 - 
- result.py:7 - Result
- result.py:20 - Result.resolve_cache
- result.py:26 - Result.backend_model
- result.py:32 - Result.branch
- result.py:49 - Result.downsize
- result.py:52 - UnsatResult
- result.py:55 - SatResult
************* Module claripy
- __init__.py:1 - 
- __init__.py:67 - BV
- __init__.py:92 - downsize
- __init__.py:95 - Solver

Endless loop in claripy

Hi! I've got this stacktrace while doing a VFG. This is with the current HEAD (235a7a9) version, so the line numbers should be correct.

Should I submit my binary and the code running the VFG?
Or should I try to create a simplified testcase for this?

Traceback (most recent call last):
  File "vfg.py", line 1227, in _get_simrun
    sim_run = self.project.factory.sim_run(current_path.state, jumpkind=jumpkind, num_inst=num_inst)
  File "/usr/local/lib/python2.7/dist-packages/angr/factory.py", line 173, in sim_run
    r = self.sim_block(state, addr=addr, **block_opts)
  File "/usr/local/lib/python2.7/dist-packages/angr/factory.py", line 95, in sim_block
    force_bbl_addr=force_bbl_addr)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/vex/irsb.py", line 69, in __init__
    self._handle_irsb()
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/vex/irsb.py", line 102, in _handle_irsb
    self._handle_statements()
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/vex/irsb.py", line 248, in _handle_statements
    e = self.add_successor(self.state.copy(), s_stmt.target, s_stmt.guard, s_stmt.jumpkind, stmt_idx)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/s_run.py", line 100, in add_successor
    state.add_constraints(guard)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/s_state.py", line 294, in add_constraints
    if self.se.is_false(arg):
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/plugins/solver.py", line 135, in concrete_shortcut_not_bool
    return f(self, *args, **kwargs)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/s_action_object.py", line 53, in ast_stripper
    return f(*new_args, **new_kwargs)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/plugins/solver.py", line 86, in wrapped_f
    return f(*args, **kwargs)
  File "/usr/local/lib/python2.7/dist-packages/simuvex-5.6.8.22-py2.7.egg/simuvex/plugins/solver.py", line 421, in is_false
    return self._solver.is_false(e, extra_constraints=self._adjust_constraint_list(extra_constraints), exact=exact)
  File "/usr/local/lib/python2.7/dist-packages/claripy/frontend_mixins/concrete_handler_mixin.py", line 60, in is_false
    return super(ConcreteHandlerMixin, self).is_false(e, **kwargs)
  File "/usr/local/lib/python2.7/dist-packages/claripy/frontend_mixins/constraint_filter_mixin.py", line 61, in is_false
    return super(ConstraintFilterMixin, self).is_false(e, extra_constraints=ec, **kwargs)
  File "/usr/local/lib/python2.7/dist-packages/claripy/frontends/light_frontend.py", line 77, in is_false
    return self._solver_backend.is_false(e)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 291, in is_false
    f = self._is_false(self.convert(e), extra_constraints=extra_constraints, solver=solver, model_callback=model_callback)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 96, in convert
    return Backend.convert(self, expr.ite_excavated if isinstance(expr, Base) else expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 161, in convert
    r = self.call(expr.op, expr.args)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 195, in call
    converted = self.convert_list(args)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 183, in convert_list
    return [ self.convert(a) for a in args ]
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 96, in convert
    return Backend.convert(self, expr.ite_excavated if isinstance(expr, Base) else expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 161, in convert
    r = self.call(expr.op, expr.args)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 195, in call
    converted = self.convert_list(args)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 183, in convert_list
    return [ self.convert(a) for a in args ]
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 96, in convert
    return Backend.convert(self, expr.ite_excavated if isinstance(expr, Base) else expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 158, in convert
    r = self._op_expr[expr.op](expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 43, in converter
    raw_args[i] = self.convert(raw_args[i])
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 96, in convert
    return Backend.convert(self, expr.ite_excavated if isinstance(expr, Base) else expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 158, in convert
    r = self._op_expr[expr.op](expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 43, in converter
    raw_args[i] = self.convert(raw_args[i])
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/backend_vsa.py", line 96, in convert
    return Backend.convert(self, expr.ite_excavated if isinstance(expr, Base) else expr)
  File "/usr/local/lib/python2.7/dist-packages/claripy/backends/__init__.py", line 158, in convert

STP backend for Claripy

Hi,
I'm trying to write a Claripy Backend for STP. I'm able to register the new backend by
_backend_manager.backends._register_backend

but when I create a new BVS or BVV, Claripy always calls the Z3 Backend. How can I select the backend that I would like to use?

Thank you

new String class shadows "replace" method

String.replace should be renamed since ASTs have a .replace method which replaces elements in the tree.

Light solver can't handle this eval() on armv7 or 8

trying to get a pretty print from a block in some final state , but i get this exception
it works fine on armv5 but not on armv7 or v8!
can i extend the solver so it can handle this?
final_state.block().pp()
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/sim_state.py", line 416, in block
kwargs['addr'] = self.addr
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/sim_state.py", line 231, in addr
return self.solver.eval_one(self.regs._ip)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 721, in eval_one
return self.eval_exact(e, 1, **{k: v for (k, v) in kwargs.iteritems() if k != 'default'})[0]
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 772, in eval_exact
r = self.eval_upto(e, n + 1, **kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 689, in eval_upto
cast_vals = [self._cast_to(e, v, cast_to) for v in self._eval(e, n, **kwargs)]
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 155, in concrete_shortcut_tuple
return f(self, *args, **kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/sim_action_object.py", line 53, in ast_stripper
return f(*new_args, **new_kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 86, in wrapped_f
return f(*args, **kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/angr/state_plugins/solver.py", line 481, in _eval
return self._solver.eval(e, n, extra_constraints=self._adjust_constraint_list(extra_constraints), exact=exact)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/claripy/frontend_mixins/concrete_handler_mixin.py", line 7, in eval
return super(ConcreteHandlerMixin, self).eval(e, n, **kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/claripy/frontend_mixins/constraint_filter_mixin.py", line 40, in eval
return super(ConstraintFilterMixin, self).eval(e, n, extra_constraints=ec, **kwargs)
File "/home/benylopo/anaconda22/lib/python2.7/site-packages/claripy/frontends/light_frontend.py", line 42, in eval
raise ClaripyFrontendError("Light solver can't handle this eval().")
SimSolverModeError: ('Translated claripy error:', <class 'claripy.errors.ClaripyFrontendError'>, ClaripyFrontendError("Light solver can't handle this eval().",))

Logic error in claripy z3 min function

Located here.
The return statement causes extra_constraints to not be removed from the z3 solver.

Also, consider using the z3 optimize object as it works quite well and will probably out perform your multiple evals.

Claripy eval causes python crash with segmentation fault

I am running the latest version fetched with angr-dev

python --version
Python 2.7.6

running pip install -I -e claripy mentions
claripy 5.6.10.5

import pickle
import claripy

with open('smallcrash','rb') as f:
     d = pickle.load(f)

s = claripy.Solver()
s.add(d['a'])
s.eval(d['vars'],1,extra_constraints=(claripy.Not(d['b']),))

smallcrash.gz

Sorry for the large example-constraints, they are pulled directly from my crashing input.

angr / claripy Goto Github PK

claripy's Introduction

claripy

Project Links

Usage

claripy's People

Contributors

Stargazers

Watchers

Forkers

claripy's Issues

Recommend Projects

Recommend Topics

Recommend Org