angr / claripy Goto Github PK
View Code? Open in Web Editor NEWAn abstraction layer for constraint solvers.
License: BSD 2-Clause "Simplified" License
An abstraction layer for constraint solvers.
License: BSD 2-Clause "Simplified" License
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.
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).
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)
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?
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
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
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()
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)
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 !
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:
... and the TypeError is thrown here:
claripy/claripy/vsa/bool_result.py
Line 12 in 04972f3
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
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
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)
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.
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 :)
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).
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')
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
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?
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
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.
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.
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']),))
Sorry for the large example-constraints, they are pulled directly from my crashing input.
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.
The following is quoted from @zardus in the Slack channel. We should put them in the documentation.
generally speaking:
claripy.AST
objectsFrontend
s 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.Frontend
needs to, at some point, do actual operation and evaluations on the AST
. AST
s don't support this on their own. Instead, Backend
s translate AST
s into BackendObject
s (i.e., python primitives, Z3 expressions, strided intervals for VSA, etc) and also handle the appropriate state-tracking objects (such as Z3 solvers)Frontend
s take AST
s as inputs and use Backend
s to backend.convert()
those AST
s into BackendObjects
that can be evaluated and otherwise reasoned aboutFrontendMixin
s customize the operation of Frontend
s. For example, ModelCacheMixin
caches solutions from an SMT solverWe 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
).
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().
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
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
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.
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'
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().",))
@ltfish To accomplish this effort, we will need to
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.
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
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?).
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.
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.
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.
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
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.
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
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
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
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
AS TITLE.
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?
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.
String.replace should be renamed since ASTs have a .replace method which replaces elements in the tree.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.