Question: Performance of BV RotateLeft when number of rotations is symbolic, or: how to extract bitvector slice with symbolic offset #7673
Labels
Comments
|
Variable shifts/rotates result in inherently complex circuits. A classic idea is to use a barrel shifter. I use this in SBV and it performs better in general. (Though don't expect miracles!) |
|
Thanks for the info and pointers! Would you happen to know if |
|
That's really a question for @NikolajBjorner When I worked on this some years ago, that wasn't the case. But maybe things have changed in the mean time. |
|
The implementation is very inefficient. First: It uses a call to urem instead of just extracting log(sz) bits for the rotation amount. |
NikolajBjorner
added a commit
that referenced
this issue
Jun 6, 2025
|
@smolkaj - does it improve? |
|
@qobilidop will give this a try shortly, thanks a lot in advance! |
|
I have done a quick experiment, but unfortunately it seems to become worse with the patch applied. We'll take a deeper look to further investigate. |
|
I did another more isolated experiment, and the patch actually helps improving the performance a lot! So it's likely there were some other issues in my previous experiment code. For future reference, my benchmark results are:
Here's my benchmark code: import time
import z3
def sym_extract(
src: z3.BitVecRef, offset: z3.BitVecRef, size: int
) -> z3.BitVecRef:
assert src.size() >= offset.size()
offset = z3.ZeroExt(src.size() - offset.size(), offset)
src = z3.RotateLeft(src, offset)
field = z3.Extract(
high=src.size() - 1,
low=src.size() - size,
a=src,
)
return z3.simplify(field)
def run_experiment(
src_size: int,
len_fi
8000
eld_size: int,
match_field_size: int,
rep: int = 1,
) -> None:
# Create a source buffer to solve for.
src = z3.BitVec("src", src_size)
offset = z3.BitVecVal(0, src_size.bit_length())
constraint = z3.BoolVal(True)
for _ in range(rep):
# Extract a length field and skip over the length amount.
len_field = sym_extract(src, offset, len_field_size)
assert offset.size() >= len_field_size
len_field = z3.ZeroExt(offset.size() - len_field_size, len_field)
offset = offset + len_field.size() + len_field
# Extract a match field and encode a constraint.
match_field = sym_extract(src, offset, match_field_size)
offset = offset + match_field.size()
constraint = z3.And(
constraint,
match_field == z3.BitVecVal(0x42, match_field.size()),
)
constraint = z3.simplify(constraint)
print("Constraint to solve:")
print(constraint)
solver = z3.Solver()
solver.add(constraint)
t0 = time.monotonic()
print("solver.check() starts")
solver.check()
print(f"solver.check() finishes in {time.monotonic() - t0:.3f} seconds")
if __name__ == "__main__":
run_experiment(
src_size=1024,
len_field_size=8,
match_field_size=8,
rep=2,
)Output (after the patch): |
|
I did some further investigation and have a reproducible case now where the patch seems to make things worse. Before the patch, this case finishes ~ 20s. After the patch, the solver hangs in the import time
import z3
SOLVER_SEXPR = """
(declare-fun packet_buffer () (_ BitVec 6144))
(assert (let ((a!1 (bvadd #b0000001000000
(concat (bvadd #b1000110
((_ extract 5638 5632) packet_buffer))
#b000000))))
(let ((a!2 (= ((_ extract 6135 6128)
(ext_rotate_left packet_buffer
(concat #b00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
a!1)))
#x06)))
(and (= ((_ extract 6047 6032) packet_buffer) #x86dd)
(= ((_ extract 5983 5976) packet_buffer) #x11)
(= ((_ extract 5695 5681) packet_buffer) #b0000001111
8000
10100)
(= ((_ extract 5639 5632) packet_buffer) #x04)
(= ((_ extract 5617 5617) packet_buffer) #b1)
(= ((_ extract 5647 5640) packet_buffer) #x04)
a!2))))
"""
if __name__ == "__main__":
solver = z3.Solver()
solver.from_string(SOLVER_SEXPR)
print(solver)
t0 = time.monotonic()
print("solver.check() starts")
solver.check()
print(f"solver.check() finishes in {time.monotonic() - t0:.3f} seconds")Output (before the patch): @NikolajBjorner Any insights why this no longer works after the patch? |
|
added perf improvement per common code path simplification |
|
Thanks @NikolajBjorner for the lightning fast fix! With your latest patch, my experiment now finishes in 0.064 seconds, an improvement from 20.053 seconds! I'll continue to do more testing. Might bother you again if other issue emerges. Or we'll let you know if everything works as expected on our side. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Apologies if I'm posing this question in the wrong place -- please let me know if there is a better place to ask.
We're using the theory of bitvectors. We're trying to extract a slice/subvector of a vector
b, where the lengthlof the slice is constant but the offsetomay be symbolic. In Python notation:If
ois a constant, using the Python API, we can useExtractand doz3.Extract(o + l - 1, o, b).If
ois symbolic,Extractwill throw an error because it disallows symbolic indices, but we figured out the following workaround usingRotateRight, which does allow symbolic rotation:However, empirically we're observing poor performance using this encoding when
ois indeed symbolic.I am wondering if this is expected and if there are any known approaches to address this issue, e.g. more clever encodings?
I am also curious how
RotateRightworks in the first place when the rotation is symbolic...does this just translate down to a # bit-wise case split or something more clever?cc @qobilidop @jonathan-dilorenzo @kheradmandG
The text was updated successfully, but these errors were encountered: