From be73b184b385f15d4ba6a47b6d614d06ca84c259 Mon Sep 17 00:00:00 2001 From: s0mark Date: Sun, 22 Oct 2023 22:35:00 +0200 Subject: [PATCH] added conversion of C integer division and modulo --- .../grammar/expression/ExpressionVisitor.java | 76 ++++++++++++++----- 1 file changed, 57 insertions(+), 19 deletions(-) diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 099c5466e4..90dd48cbce 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -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; @@ -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; @@ -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; @@ -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()); @@ -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);