* Fix signed division and remainder in the pcode engine
OpBehaviorIntSdiv and OpBehaviorIntSrem used Claripy's `/` and `%`, which are
unsigned bit-vector operations. For negative operands they therefore produced
the same results as the unsigned INT_DIV and INT_REM behaviors.
INT_SDIV now uses claripy.SDiv (truncation toward zero). INT_SREM is defined as
in1 - SDiv(in1, in2) * in2, giving a remainder with the dividend's sign, which
matches the p-code semantics documented in the class comments.
For 64-bit -5 and 2, INT_SDIV now yields -2 (0xfffffffffffffffe) and INT_SREM
yields -1 (0xffffffffffffffff) instead of large unsigned values.
The arithmetic behavior test table enables both INT_SDIV and INT_SREM with the
matching signed reference expressions, and a new concrete test checks mixed-sign
combinations (-5/2, 5/-2, -5/-2, ...) that an unsigned implementation cannot
satisfy.
* [pre-commit.ci] auto fixes from pre-commit.com hooks
for more information, see https://pre-commit.ci
* Use claripy.SMod for INT_SREM
Per review, INT_SREM uses claripy.SMod directly instead of the equivalent
in1 - claripy.SDiv(in1, in2) * in2. Verified identical to a truncated-toward-zero
reference over 100k random 64-bit pairs, including the INT_MIN / -1 corner.
* Address pcode signed arithmetic review comments
* [pre-commit.ci] auto fixes from pre-commit.com hooks
for more information, see https://pre-commit.ci
---------
Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>
* AIL: Merge likes/matches into a single mode-parameterized walk
* AIL: Make __eq__ idx-aware at every node, not just the root
* AIL: Stop hashing fields that equality does not compare
* AIL: Regression-test the hash/eq contract
* AIL: Compare bits in StringLiteral and Struct
* AIL: Replace the CMP_* constants with a CmpMode enum
* AIL: cargo fmt
* AIL: Compare and hash rounding_mode on Convert and BinaryOp
* Update comments.
arm64g_calculate_flag_c selected the ADC*/SBC* carry-in with `cc_dep2 != 0`
(the second operand). The arm64 flag thunk layout puts the old carry in
cc_dep3 (angr's own comment: "DEP3 = oldC (in LSB)", matching VEX's
guest_arm64_helpers.c). So the C flag after adcs/sbcs was computed from an
operand value instead of the incoming carry.
Random operands usually mask it (cc_dep2 != 0 nearly always holds); the
equal-operand case exposes it, e.g. `sbcs x,y,y` must give C = oldC but
returned a value keyed on y. flag_n/z/v and the arm32 port (which correctly
uses cc_dep3) were unaffected.
- Make SPropagator, SRDA, and BlockSimplifier normal classes instead of Analysis classes.
- Share peephole optimizer instances across BlockSimplifiers.
- BlockSimplifier: Skip unnecessary peephole passes; avoid block-level comparisons for fixpoint determination.
- Add a runtime-only peephole_optimized flag to AIL statements so we skip running peephole optimizations on already optimized statements.
Fixes#6067
pc_actions_UMUL computed the product at operand width, so the extracted
"high half" was always zero and CF/OF (OF = CF) were constantly 0:
lo = (cc_dep1 * cc_dep2)[nbits-1:0] # truncated to nbits
hi = (lo >> nbits)[nbits-1:0] # lo is nbits wide -> always 0
The sibling pc_actions_SMUL is correct because it widens first
(sign_extend). Mirror it with zero_extend: multiply the operands widened to
2*nbits and take the high half. For CC_OP_MUL{B,W,L,Q}, CF = OF =
(high half != 0) per the Intel SDM. This is why `imul` reported CF/OF
correctly while `mul` did not (issue #6067: `mul %ebx` left CF clear).
* Typehoon: index subtype constraint components
* Refactor the code to eliminate weird terminology.
* Fix test cases.
---------
Co-authored-by: Fish <fishw@asu.edu>
* Rewrite the amd64 CondO/CondNO ccall family
amd64g_calculate_condition with cond CondO/CondNO had no rewrite arm at
all, so every jo/jno/seto/cmovno site leaked into the decompilation as an
uncompilable _ccall(0|1, cc_op, ...).
Add arms for the cc_op families that define OF:
LOGIC{B,W,L,Q} and/or/xor always clear OF -> constant 0 / 1
ADD{B,W,L,Q} -> __OFADD__(dep_1, dep_2)
SUB{B,W,L,Q} -> __OFSUB__(dep_1, dep_2)
UMUL{B,W,L,Q} -> __OFUMUL__(dep_1, dep_2)
SMUL{B,W,L,Q} -> __OFSMUL__(dep_1, dep_2)
INC{B,W,L,Q} result == signed minimum
DEC{B,W,L,Q} result == signed maximum
COPY test the stored OF bit
The overflow helpers follow the existing __CFADD__ arm: a named usercall
whose operands carry the operation width. CondNO reuses the same helper
and compares it against zero.
Unsigned multiply overflow is defined as "the high half of the full
2N-bit product is nonzero", i.e. the product does not fit in N unsigned
bits. Note this is NOT the threshold used by the x86 rewriter, which
compares the product against 1 << (N - 1) -- that is the signed
threshold, half the correct unsigned one, and it reports overflow for
every product in [2^(N-1), 2^N - 1] even though those fit. At 8 bits it
misclassifies 820 of 65536 operand pairs, all false positives.
pc_actions_UMUL in the VEX ccall helpers is itself wrong here: it
multiplies two N-bit values without widening, so its `>> nbits` is
always zero and its CF/OF do not agree with the hardware. The rewrite
arm follows the hardware and pc_actions_SMUL's (correct) structure
instead; fixing the helper is left alone.
Every arm was checked exhaustively at 8 bits against
pc_calculate_condition, and the ADD/SUB/UMUL/SMUL arms additionally
against real setcc results.
* Drop the synthetic CondO fixture test
The real gzip and file fixtures already cover the CondO arms; a purpose
built binary added nothing that the unit tests do not already check.
* Cover the CondNO overflow path with a real binary
tar's argp helper guards a multiply with 'mul %rbp; jno', exercising the
CondNO side of UMULQ that gzip and file do not reach. Other cc_op
families still leak a ccall in that function, so only the OF conditions
are asserted.
* Cover the CondO overflow arms with three more real binaries
coreutils cat, grep and zlib's minigzip each carry the xalloc /
__builtin_mul_overflow idiom, between them exercising CondO against
ADDQ, SMULQ and UMULQ across three separate projects. Verified symbols
and addresses are cited on each test.
* Correct the tar overflow test to CondO
The jno there is canonicalized into CondO with an inverted branch, so the
ccall reaching the rewriter carries cond 0, not cond 1. The negation seen
in the output is the structurer's, not the condition's.
`(x << N) >> N` was rewritten into a Convert-of-Convert pair whose outer Convert
zero-extended for BOTH logical (Shr) and arithmetic (Sar) right shifts. For Sar
this is unsound: the idiom sign-extends the low (M-N) bits, but the zero-extending
Convert rendered as a bitmask, so e.g. `(int)(x << 20) >> 20` decompiled to
`x & 0xfff` (and the 64-bit twin to `x & 0xffffffffff`), which drops the
sign bit.
* CFGFast: Tolerate a single leading null byte when scanning for strings.
* CFGFast: Scan for mixed pointers in high-based images during complete scanning.
* Tests: Add a regression test for data detection in a PE32 with data tables in .text.
