Z3JavaTranslator: widen IntNum/ArithExpr coercion across binary BV ops#1
Open
jon-bell wants to merge 2 commits into
Open
Z3JavaTranslator: widen IntNum/ArithExpr coercion across binary BV ops#1jon-bell wants to merge 2 commits into
jon-bell wants to merge 2 commits into
Conversation
… BIT_AND BIT_AND only coerced IntNum rhs when lhs was BitVecExpr. A symbolic byte-array tagged with BVVariable(..., 32) flowing through Knarr's path constraints hit the reverse shape (BitVecExpr rhs, IntNum lhs) and Z3JavaTranslator crashed with "ClassCastException: IntNum cannot be cast to BitVecExpr" inside the mkBVAND call. A second shape — BIT_AND with an ArithExpr (IntExpr) side that came from an I2R or related conversion — also reached the casts. Add mkInt2BV widening for that case so the BVAND always sees two BitVecExprs of the same sort. Together with Knarr's Symbolicator fix that now tags byte[] elements as BitVec(32) (matching Z3JavaTranslator's byte-array range sort), this lets byte-array concolic execution complete the solver round-trip. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Several binary BV cases in postVisit had incomplete sort coercion: some handled IntNum on only one side, and none handled non-literal IntExpr (ArithExpr) operands via mkInt2BV. This mirrors the fix applied to BIT_AND in 7f2b048 across all remaining binary BV operators so that either operand may be an IntNum or IntExpr and the pair is normalized to matching BV sort before invoking the Z3 BV API. Ops updated: BIT_OR, BIT_XOR, ADD, SUB, MUL, DIV, MOD, LT, LE, GT, GE, SHIFTL, SHIFTR, SHIFTUR. BIT_AND already done upstream. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Z3JavaTranslator.postVisit(Operation)had asymmetric and incomplete coercion of non-BitVec operands to BitVec for several binary bit-vector operators. Two failure modes surfaced in downstream use (Knarr concolic execution on Apache Commons Compress):BIT_ANDonly coercedIntNumon the rhs when the lhs was aBitVecExpr. The mirror shape (IntNumlhs,BitVecExprrhs) fell through to the casts and crashed withClassCastException: IntNum cannot be cast to BitVecExpr.BIT_OR,BIT_XOR,ADD,SUB,MUL,DIV,MOD,LT,LE,GT,GE,SHIFTL,SHIFTR,SHIFTUR) had related holes — either handlingIntNumon only one side, or missing theIntExpr(non-literalArithExpr) case that arises when a sub-expression came throughI2R/BV2I.This PR mirrors the existing
BIT_ORpattern uniformly across every binary BV op: for each operator, coerceIntNumon either side viamkBV(...getInt64(), sortSize)(bumped fromgetInt()so 32-bit masks like0xFFFFFFFFdon't lose bits), and convertIntExprviamkInt2BV(sortSize, intExpr)on either side.Changes
BIT_AND— symmetricIntNumcoercion +IntExpr → BVwidening (the bug that surfaced the issue).BIT_OR,BIT_XOR,ADD,SUB,MUL,DIV,MOD,LT,LE,GT,GE,SHIFTL,SHIFTR,SHIFTUR. LeftBIT_NOT(unary),BIT_CONCAT(special-cased for strings),SELECT/STORE(sort-dependent on the array type) alone.Ops NOT widened — flagged for follow-up if they ever matter:
RealExpron a BV op path would stillClassCastException. Semantics for mixing real and BV are dubious.SeqExpr/ArrayExpron BV op paths — ill-typed input rather than missing coercion.SeqExpr-with-IntNum(character-range) branches;SeqExpr+ non-literalIntExprisn't covered.Test plan
🤖 Generated with Claude Code