Skip to content

Z3JavaTranslator: widen IntNum/ArithExpr coercion across binary BV ops #1

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jon-bell wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Z3JavaTranslator: widen IntNum/ArithExpr coercion across binary BV ops #1

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
7f2b048
Z3JavaTranslator: symmetric IntNum coercion and ArithExpr widening in…
jon-bell Apr 19, 2026
4bf8a46
Z3JavaTranslator: widen IntNum/ArithExpr coercion to all binary BV ops
jon-bell Apr 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
171 changes: 128 additions & 43 deletions green/src/za/ac/sun/cs/green/service/z3/Z3JavaTranslator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -570,16 +600,26 @@ 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)
{
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
Expand All @@ -599,70 +639,90 @@ 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));
}
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));
}
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));
}
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;
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -765,25 +837,38 @@ 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:
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:
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:
Expand Down