Say I have 8-BitVectors 1 (#x01) and -2 (#xfe) and I subtract them using Z3_mk_bvsub. When I compute the flag-related quantities I get
nc ≡ Z3_mk_bvsub_no_overflow → true
nu ≡ Z3_mk_bvsub_no_underflow → true
My goal is to understand the meaning of these flags. The confusion arises when I try to compare them with CPU flags because, if I ask the CPU to subtract 1 - (-2)
mov al, 1
sub al, -2
its flags becomeCY = 1 and OV = 0.
My question is this: How can I get CY and OV from Z3 using its subtraction flags? More precisely, what's the boolean expression that will produce CY and OV from the Z3 results nu and nc? My initial guess was OV = ¬ nu and CY = ¬ nc, but that's clearly not the case, at least for the carry.
Note: I didn't have this problem with the addition, where similar equations do hold.
Note 2: Further investigation shows that, in the case of subtraction, it is not possible to deduce the X86/64 CY flag from Z3 flags. The sign of the quantity being subtracted is also required. The OV flag can be deduced though, and the same is true for addition.
The paper to read regarding these operations is https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/z3prefix.pdf
Note that the operations are "reversed." Z3_mk_bvsub_no_overflow will be true if there is no overflow. And similarly for underflow. This double-negation is unfortunate, but that's how the operations are defined.
How these relate to the CPU's OV/CY flags is an interesting question. I think it's best to consider the results of z3 (as explained in the above paper) as mathematical semantics. In z3 parlance, overflow exists when the infinitely precise result lies to the right of the range-covered by the bit-vector size, and underflow exists when it lies to the left.
Your particular architecture (x86 most likely, but not necessarily!), however, might have different rules on how these flags are produced. In particular CPU's do not care (or know) whether the arguments are signed or unsigned. The magic of 2's complement arithmetic allows them to treat the arguments uniformly, and thus there's no direct correspondence with the typed-analysis z3 performs. Here is the description from the x86 manual:
The SUB instruction does not distinguish between signed or unsigned operands. Instead, the processor evaluates the result for both data types and sets the OF and CF flags to indicate a borrow in the signed or unsigned result, respectively. The SF flag indicates the sign of the signed result.
Long story short, you'll have to be very specific about whether you're doing signed/unsigned arithmetic, and look at the precise x86 (or whatever architecture you're on, but I presume they must all be similar), and see what the actual correspondence might be. Keep in mind that the correspondence may not be precise. For legacy/historical reasons, x86 does things in its own idiosyncratic ways, which may not perfectly match the mathematical results that z3 produces based on the above paper.