Skip to content

Commit

Permalink
Harmonize integer div/mod semantics
Browse files Browse the repository at this point in the history 
Fix the discrepancies between the semantics of integer division and modulo in C, Z3 and Theta (see issue #209 and PR #230).
  • Loading branch information
@s0mark
s0mark authored Oct 23, 2023
2 parents f904031 + be73b18 commit 455a89c
Show file tree
Hide file tree
Showing 3 changed files with 80 additions and 20 deletions.
11 changes: 10 additions & 1 deletion subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,16 @@ public IntLitExpr pos() {
}

public IntLitExpr div(final IntLitExpr that) {
return IntLitExpr.of(this.value.divide(that.value));
// Semantics:
// 5 div 3 = 1
// 5 div -3 = -1
// -5 div 3 = -2
// -5 div -3 = 2
var result = this.value.divide(that.value);
if (this.value.compareTo(BigInteger.ZERO) < 0 && this.value.mod(that.value.abs()).compareTo(BigInteger.ZERO) != 0) {
result = result.subtract(BigInteger.valueOf(that.value.signum()));
}
return IntLitExpr.of(result);
}

public IntLitExpr mod(final IntLitExpr that) {
Expand Down
13 changes: 13 additions & 0 deletions subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/EvaluationTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,19 @@ public void testIntToRat() {
}
}

@Test
public void testDiv() {
assertEquals(Int(1), evaluate(Div(Int(5), Int(3))));
assertEquals(Int(-1), evaluate(Div(Int(5), Int(-3))));
assertEquals(Int(-2), evaluate(Div(Int(-5), Int(3))));
assertEquals(Int(2), evaluate(Div(Int(-5), Int(-3))));

assertEquals(Int(2), evaluate(Div(Int(6), Int(3))));
assertEquals(Int(-2), evaluate(Div(Int(6), Int(-3))));
assertEquals(Int(-2), evaluate(Div(Int(-6), Int(3))));
assertEquals(Int(2), evaluate(Div(Int(-6), Int(-3))));
}

@Test
public void testMod() {
assertEquals(Int(2), evaluate(Mod(Int(2), Int(3))));
Expand Down
76 changes: 57 additions & 19 deletions ...n/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,17 +24,16 @@
import hu.bme.mit.theta.core.type.LitExpr;
import hu.bme.mit.theta.core.type.Type;
import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs;
import hu.bme.mit.theta.core.type.abstracttype.DivExpr;
import hu.bme.mit.theta.core.type.abstracttype.ModExpr;
import hu.bme.mit.theta.core.type.anytype.IteExpr;
import hu.bme.mit.theta.core.type.anytype.RefExpr;
import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr;
import hu.bme.mit.theta.core.type.booltype.BoolExprs;
import hu.bme.mit.theta.core.type.booltype.BoolType;
import hu.bme.mit.theta.core.type.bvtype.BvAndExpr;
import hu.bme.mit.theta.core.type.bvtype.BvExprs;
import hu.bme.mit.theta.core.type.bvtype.BvOrExpr;
import hu.bme.mit.theta.core.type.bvtype.BvType;
import hu.bme.mit.theta.core.type.bvtype.BvXorExpr;
import hu.bme.mit.theta.core.type.bvtype.*;
import hu.bme.mit.theta.core.type.fptype.FpLitExpr;
import hu.bme.mit.theta.core.type.inttype.IntType;
import hu.bme.mit.theta.core.utils.BvUtils;
import hu.bme.mit.theta.core.utils.FpUtils;
import hu.bme.mit.theta.frontend.ParseContext;
Expand All @@ -43,11 +42,7 @@
import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor;
import hu.bme.mit.theta.frontend.transformation.grammar.type.TypeVisitor;
import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration;
import hu.bme.mit.theta.frontend.transformation.model.statements.CAssignment;
import hu.bme.mit.theta.frontend.transformation.model.statements.CCall;
import hu.bme.mit.theta.frontend.transformation.model.statements.CCompound;
import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr;
import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement;
import hu.bme.mit.theta.frontend.transformation.model.statements.*;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray;
import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer;
Expand All @@ -56,16 +51,11 @@
import org.kframework.mpfr.BinaryMathContext;

import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Deque;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.*;
import java.util.stream.Collectors;

import static com.google.common.base.Preconditions.checkState;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite;
import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*;
import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpType;
import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int;
import static hu.bme.mit.theta.core.utils.TypeUtils.cast;
Expand Down Expand Up @@ -371,10 +361,18 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
expr = AbstractExprs.Mul(leftExpr, rightExpr);
break;
case "/":
expr = AbstractExprs.Div(leftExpr, rightExpr);
if (leftExpr.getType() instanceof IntType && rightExpr.getType() instanceof IntType) {
expr = createIntDiv(leftExpr, rightExpr);
} else {
expr = AbstractExprs.Div(leftExpr, rightExpr);
}
break;
case "%":
expr = AbstractExprs.Mod(leftExpr, rightExpr);
if (leftExpr.getType() instanceof IntType && rightExpr.getType() instanceof IntType) {
expr = createIntMod(leftExpr, rightExpr);
} else {
expr = AbstractExprs.Mod(leftExpr, rightExpr);
}
break;
default:
throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText());
Expand All @@ -388,6 +386,46 @@ public Expr<?> visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon
return ctx.castExpression(0).accept(this);
}

/**
* Conversion from C (/) semantics to solver (div) semantics.
* @param a dividend
* @param b divisor
* @return expression representing C division semantics with solver operations
*/
private Expr<?> createIntDiv(Expr<?> a, Expr<?> b) {
DivExpr<?> aDivB = Div(a, b);
return Ite(Geq(a, Int(0)), // if (a >= 0)
aDivB, // a div b
// else
Ite(Neq(Mod(a, b), Int(0)), // if (a mod b != 0)
Ite(Geq(b, Int(0)), // if (b >= 0)
Add(aDivB, Int(1)), // a div b + 1
// else
Sub(aDivB, Int(1)) // a div b - 1
), // else
aDivB // a div b
)
);
}

/**
* Conversion from C (%) semantics to solver (mod) semantics.
* @param a dividend
* @param b divisor
* @return expression representing C modulo semantics with solver operations
*/
private Expr<?> createIntMod(Expr<?> a, Expr<?> b) {
ModExpr<?> aModB = Mod(a, b);
return Ite(Geq(a, Int(0)), // if (a >= 0)
aModB, // a mod b
// else
Ite(Geq(b, Int(0)), // if (b >= 0)
Sub(aModB, b), // a mod b - b
Add(aModB, b) // a mod b + b
)
);
}

@Override
public Expr<?> visitCastExpressionUnaryExpression(CParser.CastExpressionUnaryExpressionContext ctx) {
return ctx.unaryExpression().accept(this);
Expand Down

0 comments on commit 455a89c

Please sign in to comment.