Skip to content
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

Harmonize integer div/mod semantics #230

Merged
merged 2 commits into from
Oct 23, 2023
Merged

Harmonize integer div/mod semantics #230

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ebbb6bf
adjusted integer division to solver semantics
s0mark Oct 21, 2023
be73b18
added conversion of C integer division and modulo
s0mark Oct 22, 2023
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
11 changes: 10 additions & 1 deletion subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/inttype/IntLitExpr.java
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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