如何扩展Z3的BitVec加法无溢出检查至任意数量操作数？

问题背景 #

现有一个Z3的BitVec加法溢出检查函数，但只能处理两个输入，没法直接用来检查任意数量BitVec相加是否溢出。原函数代码如下：

def bvadd_no_overflow(x, y, signed=False):
    assert x.ctx_ref()==y.ctx_ref()
    a, b = z3._coerce_exprs(x, y)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), 
         b.as_ast(), signed))

问题出在z3._coerce_exprs(x, y)只能接收两个参数，没法直接适配多输入场景。

解决方案 #

咱们可以用逐步累加+每步检查溢出的思路来扩展这个函数。道理很简单：多个数相加不溢出，等价于从第一个数开始，每次加下一个数的过程都不发生溢出。

扩展后的完整代码 #

from z3 import *

# 保留原有的两元素溢出检查函数
def bvadd_no_overflow(x, y, signed=False):
    assert x.ctx_ref() == y.ctx_ref()
    a, b = _coerce_exprs(x, y)
    return BoolRef(Z3_mk_bvadd_no_overflow(a.ctx_ref(), a.as_ast(), b.as_ast(), signed))

# 新增支持任意数量BitVec的溢出检查函数
def bvadds_no_overflow(args, signed=False):
    if len(args) < 2:
        # 单个元素或者空列表，根本不会有溢出问题
        return BoolVal(True)
    
    # 先确认所有BitVec都在同一个Z3上下文里，避免报错
    ctx = args[0].ctx_ref()
    for arg in args[1:]:
        assert arg.ctx_ref() == ctx
    
    current_sum = args[0]
    # 初始化无溢出条件为真，后续逐步叠加检查
    no_overflow = BoolVal(True)
    
    for num in args[1:]:
        # 检查当前累加和与下一个数相加是否溢出
        step_safe = bvadd_no_overflow(current_sum, num, signed)
        no_overflow = And(no_overflow, step_safe)
        # 更新当前累加和，继续下一步检查
        current_sum = current_sum + num
    
    return no_overflow

代码说明 #

• 当输入的BitVec列表长度小于2时，直接返回True——单个元素相加或者没元素，压根不存在溢出的可能。
• 先校验所有BitVec属于同一个Z3上下文，避免上下文不一致导致的错误。
• 通过循环逐个累加元素，每一步都调用原有的两元素溢出检查函数，把所有步骤的无溢出条件用And连起来：只要有一步溢出，整个表达式就会返回False。

实际使用示例 #

# 创建3个3位有符号BitVec变量
a = BitVec('a', 3, signed=True)
b = BitVec('b', 3, signed=True)
c = BitVec('c', 3, signed=True)

# 检查a+b+c是否不会溢出
s = Solver()
s.add(bvadds_no_overflow([a, b, c], signed=True))
# 赋值：3+2+1=6，3位有符号BitVec的范围是-4到3，明显溢出
s.add(a == 3, b == 2, c == 1)
print(s.check())  # 结果是unsat，说明这个组合会溢出

内容的提问来源于stack exchange，提问作者maja