9.2.47: various failing tests
Closed this issue · 4 comments
dvzrv commented
Description
Hi! I'm currently upgrading this package for the Python 3.11 rebuild on Arch Linux.
I ran into multiple failing tests of which I am unsure what the reason is.
FTR: the failures also occur on Python 3.10!
Here are relevant test logs (full logs attached below):
=================================== FAILURES =================================== [880/9277]
________________ StandardTests.test_simplification_annotations _________________
self = <test_solver.StandardTests testMethod=test_simplification_annotations>
def test_simplification_annotations(self):
s = claripy.Solver()
x = claripy.BVS("x", 32)
s.add(x > 10)
s.add(x > 11)
s.add((x > 12).annotate(claripy.SimplificationAvoidanceAnnotation()))
assert len(s.constraints) == 3
s.simplify()
> assert len(s.constraints) == 2
E assert 3 == 2
E + where 3 = len([<Bool x_178_32 > 0xc>, <Bool True>, <Bool !(x_178_32[31:4] == 0x0) || !(x_178_32[3:0] <= 11)>])
E + where [<Bool x_178_32 > 0xc>, <Bool True>, <Bool !(x_178_32[31:4] == 0x0) || !(x_178_32[3:0] <= 11)>] = <claripy.solvers.Solver object at 0x7fbca0cc3210>.constraints
tests/test_solver.py:536: AssertionError
______________________ TestSolver.test_solver_with_reuse _______________________
self = <test_solver.TestSolver testMethod=test_solver_with_reuse>
def test_solver_with_reuse(self):
> raw_solver(self.solver, True)
tests/test_solver.py:623:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.Solver'>, reuse_z3_solver = True
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
> assert len(shards) == 2
E assert 3 == 2
E + where 3 = len([<claripy.solvers.Solver object at 0x7fbca0cd8750>, <claripy.solvers.Solver object at 0x7fbca11e7990>, <claripy.solvers.Solver object at 0x7fbca0f49990>])
tests/test_solver.py:128: AssertionError
_____________________ TestSolver.test_solver_without_reuse _____________________
self = <test_solver.TestSolver testMethod=test_solver_without_reuse>
def test_solver_without_reuse(self):
> raw_solver(self.solver, False)
tests/test_solver.py:626:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.Solver'>, reuse_z3_solver = False
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
> assert len(shards) == 2
E assert 3 == 2
E + where 3 = len([<claripy.solvers.Solver object at 0x7fbca0de0190>, <claripy.solvers.Solver object at 0x7fbca0caf0d0>, <claripy.solvers.Solver object at 0x7fbca0cae250>])
tests/test_solver.py:128: AssertionError
_________________ TestSolverReplacement.test_solver_with_reuse _________________
self = <test_solver.TestSolverReplacement testMethod=test_solver_with_reuse>
def test_solver_with_reuse(self):
> raw_solver(self.solver, True)
tests/test_solver.py:623:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverReplacement'>
reuse_z3_solver = True
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_233_32[31:5] == 0x0) || !(x_233_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_233_32[31:5] == 0x0) || !(x_233_32[4:0] <= 20)>] = <claripy.solvers.SolverReplacement object at 0x7fbca0fc3050>.constraints
tests/test_solver.py:154: AssertionError
_______________ TestSolverReplacement.test_solver_without_reuse ________________
self = <test_solver.TestSolverReplacement testMethod=test_solver_without_reuse>
def test_solver_without_reuse(self):
> raw_solver(self.solver, False)
tests/test_solver.py:626:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverReplacement'>
reuse_z3_solver = False
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_236_32[31:5] == 0x0) || !(x_236_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_236_32[31:5] == 0x0) || !(x_236_32[4:0] <= 20)>] = <claripy.solvers.SolverReplacement object at 0x7fbca1061010>.constraints
tests/test_solver.py:154: AssertionError
______________________ TestHybrid.test_solver_with_reuse _______________________
self = <test_solver.TestHybrid testMethod=test_solver_with_reuse>
def test_solver_with_reuse(self):
> raw_solver(self.solver, True)
tests/test_solver.py:623:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverHybrid'>, reuse_z3_solver = True
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
> assert len(shards) == 2
E assert 3 == 2
E + where 3 = len([<claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca0d5d250>, <claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca0f5dd10>, <claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca119bb90>])
tests/test_solver.py:128: AssertionError
_____________________ TestHybrid.test_solver_without_reuse _____________________
self = <test_solver.TestHybrid testMethod=test_solver_without_reuse>
def test_solver_without_reuse(self):
> raw_solver(self.solver, False)
tests/test_solver.py:626:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverHybrid'>, reuse_z3_solver = False
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
> assert len(shards) == 2
E assert 3 == 2
E + where 3 = len([<claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca11e4f50>, <claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca11e58d0>, <claripy.frontends.hybrid_frontend.HybridFrontend object at 0x7fbca0ccd190>])
tests/test_solver.py:128: AssertionError
_____________________ TestComposite.test_solver_with_reuse _____________________
self = <test_solver.TestComposite testMethod=test_solver_with_reuse>
def test_solver_with_reuse(self):
> raw_solver(self.solver, True)
tests/test_solver.py:623:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverComposite'>, reuse_z3_solver = True
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_376_32[31:5] == 0x0) || !(x_376_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_376_32[31:5] == 0x0) || !(x_376_32[4:0] <= 20)>] = <SolverComposite 7fbca1114c10, 1 children>.constraints
tests/test_solver.py:154: AssertionError
___________________ TestComposite.test_solver_without_reuse ____________________
self = <test_solver.TestComposite testMethod=test_solver_without_reuse>
def test_solver_without_reuse(self):
> raw_solver(self.solver, False)
tests/test_solver.py:626:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverComposite'>, reuse_z3_solver = False
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_379_32[31:5] == 0x0) || !(x_379_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_379_32[31:5] == 0x0) || !(x_379_32[4:0] <= 20)>] = <SolverComposite 7fbca13cc390, 1 children>.constraints
tests/test_solver.py:154: AssertionError
__________________ TestSolverCacheless.test_solver_with_reuse __________________
self = <test_solver.TestSolverCacheless testMethod=test_solver_with_reuse>
def test_solver_with_reuse(self):
> raw_solver(self.solver, True)
tests/test_solver.py:623:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverCacheless'>, reuse_z3_solver = True
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_402_32[31:5] == 0x0) || !(x_402_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_402_32[31:5] == 0x0) || !(x_402_32[4:0] <= 20)>] = <claripy.solvers.SolverCacheless object at 0x7fbca135a850>.constraints
tests/test_solver.py:154: AssertionError
________________ TestSolverCacheless.test_solver_without_reuse _________________
self = <test_solver.TestSolverCacheless testMethod=test_solver_without_reuse>
def test_solver_without_reuse(self):
> raw_solver(self.solver, False)
tests/test_solver.py:626:
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _
solver_type = <class 'claripy.solvers.SolverCacheless'>, reuse_z3_solver = False
def raw_solver(solver_type, reuse_z3_solver):
# bc = claripy.backends.BackendConcrete(clrp)
# bz = claripy.backends.BackendZ3(clrp)
# claripy.expression_backends = [ bc, bz, ba ]
claripy._backend_z3.reuse_z3_solver = reuse_z3_solver
s = solver_type()
s.simplify()
x = claripy.BVS("x", 32)
y = claripy.BVS("y", 32)
z = claripy.BVS("z", 32)
l.debug("adding constraints")
s.add(x == 10)
s.add(y == 15)
# Batch evaluation
results = s.batch_eval([x + 5, x + 6, 3], 2)
assert len(results) == 1
assert results[0][0] == 15
assert results[0][1] == 16
assert results[0][2] == 3
l.debug("checking")
assert s.satisfiable()
assert not s.satisfiable(extra_constraints=[x == 5])
assert s.eval(x + 5, 1)[0] == 15
assert s.solution(x + 5, 15)
assert s.solution(x, 10)
assert s.solution(y, 15)
assert not s.solution(y, 13)
shards = s.split()
assert len(shards) == 2
assert len(shards[0].variables) == 1
assert len(shards[1].variables) == 1
if isinstance(s, claripy.frontend_mixins.ConstraintExpansionMixin) or (
isinstance(s, claripy.frontends.HybridFrontend)
and isinstance(s._exact_frontend, claripy.frontend_mixins.ConstraintExpansionMixin)
): # the hybrid frontend actually uses the exact frontend for the split
assert {len(shards[0].constraints), len(shards[1].constraints)} == {
2,
1,
} # adds the != from the solution() check
if isinstance(s, claripy.frontends.ReplacementFrontend):
assert {len(shards[0].constraints), len(shards[1].constraints)} == {1, 1}
# test result caching
s = solver_type()
s.add(x == 10)
s.add(y == 15)
assert not s.satisfiable(extra_constraints=(x == 5,))
assert s.satisfiable()
s = solver_type()
# claripy.expression_backends = [ bc, ba, bz ]
s.add(claripy.UGT(x, 10))
s.add(claripy.UGT(x, 20))
s.simplify()
> assert len(s.constraints) == 1
E assert 2 == 1
E + where 2 = len([<Bool True>, <Bool !(x_405_32[31:5] == 0x0) || !(x_405_32[4:0] <= 20)>])
E + where [<Bool True>, <Bool !(x_405_32[31:5] == 0x0) || !(x_405_32[4:0] <= 20)>] = <claripy.solvers.SolverCacheless object at 0x7fbca0eddb50>.constraints
tests/test_solver.py:154: AssertionError
[..] // skipping warning output
=========================== short test summary info ============================
FAILED tests/test_solver.py::StandardTests::test_simplification_annotations
FAILED tests/test_solver.py::TestSolver::test_solver_with_reuse - assert 3 == 2
FAILED tests/test_solver.py::TestSolver::test_solver_without_reuse - assert 3...
FAILED tests/test_solver.py::TestSolverReplacement::test_solver_with_reuse - ...
FAILED tests/test_solver.py::TestSolverReplacement::test_solver_without_reuse
FAILED tests/test_solver.py::TestHybrid::test_solver_with_reuse - assert 3 == 2
FAILED tests/test_solver.py::TestHybrid::test_solver_without_reuse - assert 3...
FAILED tests/test_solver.py::TestComposite::test_solver_with_reuse - assert 2...
FAILED tests/test_solver.py::TestComposite::test_solver_without_reuse - asser...
FAILED tests/test_solver.py::TestSolverCacheless::test_solver_with_reuse - as...
FAILED tests/test_solver.py::TestSolverCacheless::test_solver_without_reuse
=========== 11 failed, 235 passed, 60 skipped, 73 warnings in 15.89s ===========
python-claripy-9.2.47-1-x86_64-build.log
python-claripy-9.2.47-1-x86_64-check.log
Steps to reproduce the bug
python -m build --wheel --no-isolation
PYTHONPATH=build/lib pytest -vv
Environment
Arch Linux
- python 3.11.3
- python-cachetools 5.3.0
- python-decorator 5.1.1
- python-pysmt 0.9.5
- python-z3-solver 4.12.1
Additional context
cc @anthraxx
rhelmot commented
The problem is that you're attempting to run claripy with an unpinned version of z3. The new version of z3 is known to produce these issues, and we haven't been able to invest the time in figuring out if it's our fault or z3's fault. See #341
dvzrv commented
Ah, that makes sense. Too bad 😢
We've unfortunately already updated to a later version of z3 and since Arch Linux is rolling release we can't really deal with version pinning that well either.
anthraxx commented
@rhelmot Is there any possibility that you may find time to take a look? When packaging angr on a distro level, we don't really have the option of following that strict pinning as David described. I understand its none trivial but we and the distro package users would very highly appreciate it. 🐱 ❤️
twizmwazin commented
We are currently using the latest stable version of z3. No promises that we will be able to immediately update when new versions release, but for now this issue should be resolved.