angr / claripy

An abstraction layer for constraint solvers.
BSD 2-Clause "Simplified" License
275 stars 90 forks source link

Fix incorrect merge in composite solver when child solvers are empty #340

Open ekedaigle opened 1 year ago

ekedaigle commented 1 year ago

Simple example to reproduce:

s1 = claripy.SolverComposite()
s2 = claripy.SolverComposite()
m = claripy.BVS("m", 8)
w = claripy.BVS("w", 8)
s1.add(w == 0)
_, sm = s1.merge([s2], [m == 0, m == 1])
sm.eval(w, 2) # returns (0,), despite w being unconstrained in s2

This can also be reproduced though some fairly trivial merges in angr:

s1 = angr.SimState(arch='ARM', mode='symbolic')
x = s1.solver.BVS('x', 32)
s1.regs.r0 = x
s1.add_constraints(s1.regs.r0 == 42)

s2 = s1.copy()
y = s2.solver.BVS('y', 32)
s2.regs.r0 = y
s2.add_constraints(s2.regs.r0 == 43)

m, _, merged = s1.merge(s2)
print(m.solver.eval_upto(m.regs.r0, 10)) # prints [42], but it should be [42, 43]

I will admit I have not been working with claripy all that long, so let me know if there's something fundamental about this I'm misunderstanding. Thanks!

rhelmot commented 1 year ago

This looks fine to me, but I'm not familiar enough with this part of the code to sign off on it. Please someone review this, or else I will merge it and this will be my fault. Don't make it my fault!