From 7f2b048aba5421fe27a2b183337dfa9f6a2f477c Mon Sep 17 00:00:00 2001 From: Jonathan Bell Date: Sun, 19 Apr 2026 23:03:34 +0000 Subject: [PATCH 1/2] Z3JavaTranslator: symmetric IntNum coercion and ArithExpr widening in BIT_AND MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- .../src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java b/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java index 914b0b0..bbed15c 100644 --- a/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java +++ b/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java @@ -773,6 +773,12 @@ else if (r instanceof IntNum) case BIT_AND: if (l instanceof BitVecExpr && r instanceof IntNum) r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVAND((BitVecExpr)l, (BitVecExpr)r)); break; case BIT_NOT: From 4bf8a460821945a294b3eaea13471713073f7235 Mon Sep 17 00:00:00 2001 From: Jonathan Bell Date: Mon, 20 Apr 2026 11:30:40 +0000 Subject: [PATCH 2/2] Z3JavaTranslator: widen IntNum/ArithExpr coercion to all binary BV ops 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) --- .../cs/green/service/z3/Z3JavaTranslator.java | 165 +++++++++++++----- 1 file changed, 122 insertions(+), 43 deletions(-) diff --git a/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java b/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java index bbed15c..8bafe08 100644 --- a/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java +++ b/green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java @@ -438,6 +438,16 @@ else if(r instanceof BitVecExpr && l instanceof IntNum) l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); stack.push(context.mkBVSLT((BitVecExpr) l, (BitVecExpr) r)); } + else if(l instanceof BitVecExpr && r instanceof IntExpr) + { + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); + stack.push(context.mkBVSLT((BitVecExpr) l, (BitVecExpr) r)); + } + else if(r instanceof BitVecExpr && l instanceof IntExpr) + { + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + stack.push(context.mkBVSLT((BitVecExpr) l, (BitVecExpr) r)); + } else if(l instanceof BitVecExpr && r instanceof BitVecExpr) { stack.push(context.mkBVSLT((BitVecExpr) l, (BitVecExpr) r)); @@ -478,12 +488,22 @@ else if(r instanceof IntNum && l instanceof SeqExpr) } else if(l instanceof BitVecExpr && r instanceof IntNum) { - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); stack.push(context.mkBVSLE((BitVecExpr) l, (BitVecExpr) r)); } else if(r instanceof BitVecExpr && l instanceof IntNum) { - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + stack.push(context.mkBVSLE((BitVecExpr) l, (BitVecExpr) r)); + } + else if(l instanceof BitVecExpr && r instanceof IntExpr) + { + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); + stack.push(context.mkBVSLE((BitVecExpr) l, (BitVecExpr) r)); + } + else if(r instanceof BitVecExpr && l instanceof IntExpr) + { + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); stack.push(context.mkBVSLE((BitVecExpr) l, (BitVecExpr) r)); } else if(l instanceof BitVecExpr && r instanceof BitVecExpr) @@ -536,6 +556,16 @@ else if(r instanceof BitVecExpr && l instanceof IntNum) l = context.mkBV(val, sortSize); stack.push(context.mkBVSGT((BitVecExpr) l, (BitVecExpr) r)); } + else if(l instanceof BitVecExpr && r instanceof IntExpr) + { + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); + stack.push(context.mkBVSGT((BitVecExpr) l, (BitVecExpr) r)); + } + else if(r instanceof BitVecExpr && l instanceof IntExpr) + { + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + stack.push(context.mkBVSGT((BitVecExpr) l, (BitVecExpr) r)); + } else if(r instanceof BitVecExpr && l instanceof BitVecExpr) stack.push(context.mkBVSGT((BitVecExpr) l, (BitVecExpr) r)); else @@ -570,9 +600,9 @@ else if(r instanceof IntNum && l instanceof SeqExpr) throw new NotSatException(); stack.push(exp); } - else if(l instanceof BitVecExpr && r instanceof IntExpr) + else if(l instanceof BitVecExpr && r instanceof IntNum) { - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); stack.push(context.mkBVSGE((BitVecExpr) l, (BitVecExpr) r)); } else if(r instanceof BitVecExpr && l instanceof IntNum) @@ -580,6 +610,16 @@ else if(r instanceof BitVecExpr && l instanceof IntNum) l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); stack.push(context.mkBVSGE((BitVecExpr) l, (BitVecExpr) r)); } + else if(l instanceof BitVecExpr && r instanceof IntExpr) + { + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); + stack.push(context.mkBVSGE((BitVecExpr) l, (BitVecExpr) r)); + } + else if(r instanceof BitVecExpr && l instanceof IntExpr) + { + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + stack.push(context.mkBVSGE((BitVecExpr) l, (BitVecExpr) r)); + } else if (l instanceof BitVecExpr && r instanceof BitVecExpr) stack.push(context.mkBVSGE((BitVecExpr) l, (BitVecExpr) r)); else @@ -599,10 +639,14 @@ else if (l instanceof BitVecExpr && r instanceof BitVecExpr) break; case ADD: if (l.isBV() || r.isBV()) { - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVAdd((BitVecExpr) l, (BitVecExpr) r)); } else { stack.push(context.mkAdd((ArithExpr) l, (ArithExpr) r)); @@ -610,11 +654,14 @@ else if (r instanceof IntNum) break; case SUB: if (l.isBV() || r.isBV()) { - if (r instanceof IntNum) + if (l instanceof BitVecExpr && r instanceof IntNum) r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); - else if (l instanceof IntNum) + if (r instanceof BitVecExpr && l instanceof IntNum) l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); - + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVSub((BitVecExpr) l, (BitVecExpr) r)); } else { stack.push(context.mkSub((ArithExpr) l, (ArithExpr) r)); @@ -622,11 +669,14 @@ else if (l instanceof IntNum) break; case MUL: if (l.isBV() || r.isBV()) { - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); - + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVMul((BitVecExpr) l, (BitVecExpr) r)); } else { stack.push(context.mkMul((ArithExpr) l, (ArithExpr) r)); @@ -634,35 +684,45 @@ else if (r instanceof IntNum) break; case DIV: if (l.isBV() || r.isBV()) { - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); - + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVSDiv((BitVecExpr) l, (BitVecExpr) r)); } else stack.push(context.mkDiv((ArithExpr) l, (ArithExpr) r)); break; case MOD: if (l.isBV() || r.isBV()) { - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); - + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVSRem((BitVecExpr)l, (BitVecExpr)r)); } else stack.push(context.mkMod((IntExpr) l, (IntExpr) r)); break; case SHIFTL: if (r instanceof BitVecExpr && l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (l instanceof BitVecExpr || r instanceof BitVecExpr) { + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof BitVecExpr || r instanceof BitVecExpr) { - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - else if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); BitVecExpr bvl = (BitVecExpr)l; BitVecExpr bvr = (BitVecExpr)r; @@ -693,20 +753,32 @@ else if (r instanceof IntNum) break; case SHIFTR: if (l instanceof BitVecExpr && r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); BitVecExpr bl = (BitVecExpr) l; BitVecExpr br = (BitVecExpr) r; - + br = context.mkExtract(5, 0, br); br = context.mkZeroExt(bl.getSortSize() - 6, br); stack.push(context.mkBVASHR(bl, br)); break; case SHIFTUR: if (l instanceof BitVecExpr && r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); bl = (BitVecExpr) l; br = (BitVecExpr) r; - + br = context.mkExtract(5, 0, br); br = context.mkZeroExt(bl.getSortSize() - 6, br); stack.push(context.mkBVLSHR(bl, br)); @@ -765,9 +837,13 @@ else if (r instanceof IntNum) break; case BIT_OR: if (l instanceof BitVecExpr && r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); if (r instanceof BitVecExpr && l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVOR((BitVecExpr)l, (BitVecExpr)r)); break; case BIT_AND: @@ -785,11 +861,14 @@ else if (r instanceof IntNum) stack.push(context.mkBVNot((BitVecExpr)l)); break; case BIT_XOR: - if (l instanceof IntNum) - l = context.mkBV(((IntNum)l).getInt(), ((BitVecExpr)r).getSortSize()); - if (r instanceof IntNum) - r = context.mkBV(((IntNum)r).getInt(), ((BitVecExpr)l).getSortSize()); - + if (l instanceof BitVecExpr && r instanceof IntNum) + r = context.mkBV(((IntNum)r).getInt64(), ((BitVecExpr)l).getSortSize()); + if (r instanceof BitVecExpr && l instanceof IntNum) + l = context.mkBV(((IntNum)l).getInt64(), ((BitVecExpr)r).getSortSize()); + if (l instanceof IntExpr && r instanceof BitVecExpr) + l = context.mkInt2BV(((BitVecExpr)r).getSortSize(), (IntExpr)l); + if (r instanceof IntExpr && l instanceof BitVecExpr) + r = context.mkInt2BV(((BitVecExpr)l).getSortSize(), (IntExpr)r); stack.push(context.mkBVXOR((BitVecExpr)l, (BitVecExpr)r)); break; case BV2I: