diff --git a/.gitignore b/.gitignore index 09f79570026..a7422cbd74b 100644 --- a/.gitignore +++ b/.gitignore @@ -96,7 +96,6 @@ trunk/examples/concurrent/bpl/weaver-benchmarks/weaver /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/Decreases.java /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/Ensures.java /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/Expression.java -/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/FakePointerExpression.java /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/FieldAccessExpression.java /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/FreeableExpression.java /trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/FunctionApplication.java diff --git a/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ACSLPrettyPrinter.java b/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ACSLPrettyPrinter.java index fdb56f113f7..b892b94617f 100644 --- a/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ACSLPrettyPrinter.java +++ b/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ACSLPrettyPrinter.java @@ -41,7 +41,6 @@ import de.uni_freiburg.informatik.ultimate.model.acsl.ast.CodeAnnotStmt; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.Ensures; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.Expression; -import de.uni_freiburg.informatik.ultimate.model.acsl.ast.FakePointerExpression; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.FieldAccessExpression; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.GhostDeclaration; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.GhostUpdate; @@ -111,8 +110,6 @@ private static String printExpression(final Expression expression) { case final BooleanLiteral boolLit -> "\\" + boolLit.getValue(); case final CastExpression cast -> "(%s) %s".formatted(cast.getCastedType().getTypeName(), printExpression(cast.getExpression())); - case final FakePointerExpression pointer -> - "{%s:%s}".formatted(printExpression(pointer.getBase()), printExpression(pointer.getOffset())); case final FieldAccessExpression f -> "(%s).%s".formatted(printExpression(f.getStruct()), f.getField()); // TODO FreeableExpression // TODO FunctionApplication diff --git a/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/acsl.ast b/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/acsl.ast index a50aa817198..3a77d4c3e37 100644 --- a/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/acsl.ast +++ b/trunk/source/ACSLParser/src/de/uni_freiburg/informatik/ultimate/model/acsl/ast/acsl.ast @@ -274,11 +274,6 @@ Expression ::= | { /** This can be used as call forall parameter, or as if or * while condition. In all other places it is forbidden. */ WildcardExpression } - | { /** This is used to represent addresses in backtranslated program executions. - * There is no corresponding grammar rule for the parser. */ - FakePointerExpression } - base : Expression - offset : Expression ); ACSLType ::= diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/BacktranslatedACSLValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/BacktranslatedACSLValue.java new file mode 100644 index 00000000000..6e176a4c101 --- /dev/null +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/BacktranslatedACSLValue.java @@ -0,0 +1,88 @@ +/* + * Copyright (C) 2024 Frank Schüssele (schuessf@informatik.uni-freiburg.de) + * Copyright (C) 2025 Dominik Klumpp (klumpp@informatik.uni-freiburg.de) + * Copyright (C) 2024-2025 University of Freiburg + * + * This file is part of the ULTIMATE CACSL2BoogieTranslator plug-in. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is free software: you can redistribute it and/or modify + * it under the terms of the GNU Lesser General Public License as published + * by the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * The ULTIMATE CACSL2BoogieTranslator plug-in is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU Lesser General Public License for more details. + * + * You should have received a copy of the GNU Lesser General Public License + * along with the ULTIMATE CACSL2BoogieTranslator plug-in. If not, see . + * + * Additional permission under GNU GPL version 3 section 7: + * If you modify the ULTIMATE CACSL2BoogieTranslator plug-in, or any covered work, by linking + * or combining it with Eclipse RCP (or a modified version of Eclipse RCP), + * containing parts covered by the terms of the Eclipse Public License, the + * licensors of the ULTIMATE CACSL2BoogieTranslator plug-in grant you additional permission + * to convey the resulting work. + */ +package de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator; + +import java.math.BigInteger; +import java.util.Objects; + +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CType; +import de.uni_freiburg.informatik.ultimate.model.acsl.ACSLPrettyPrinter; +import de.uni_freiburg.informatik.ultimate.model.acsl.ast.Expression; +import de.uni_freiburg.informatik.ultimate.util.datastructures.BigInterval; + +/** + * Represents a value resulting from the backtranslation from Boogie to C/ACSL. + */ +public sealed interface BacktranslatedACSLValue { + /** + * Represents a backtranslated value in the form of an ACSL expression. + * + * Such expressions may be used for the backtranslation of invariants and procedure contracts, as well as for + * program states. + */ + public record BacktranslatedExpression(Expression expression, CType cType, BigInterval range) + implements BacktranslatedACSLValue { + public BacktranslatedExpression(final Expression expression) { + this(expression, null, BigInterval.unbounded()); + } + + public BacktranslatedExpression { + Objects.requireNonNull(expression); + Objects.requireNonNull(range); + // cType is allowed to be null + } + + @Override + public String toString() { + return ACSLPrettyPrinter.print(expression); + } + } + + /** + * Represents a backtranslated value for a memory address in our memory model, consisting of a base address and an + * offset. + * + * This is not a real ACSL expression, and should only be used in the backtranslation of program states, not in + * invariants or contracts. Moreover, it must only be used for the values in a program state, not as a key (it does + * not represent a variable). + * + * While these values do not make sense outside of our tool (and thus should never make it into witnesses etc), they + * can be used for log output and can be helpful when debugging a feasible error trace reported by Ultimate. + */ + public record FakePointer(BigInteger base, BigInteger offset) implements BacktranslatedACSLValue { + public FakePointer { + Objects.requireNonNull(base); + Objects.requireNonNull(offset); + } + + @Override + public String toString() { + return "{%s:%s}".formatted(base, offset); + } + } +} diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java index ae8073f7d27..5f422f6b93b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/Boogie2ACSL.java @@ -31,7 +31,6 @@ import java.math.BigInteger; import java.util.Arrays; import java.util.List; -import java.util.Objects; import java.util.Optional; import java.util.Set; import java.util.function.Consumer; @@ -53,7 +52,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.ISOIEC9899TC3; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.model.acsl.ACSLPrettyPrinter; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.ACSLResultExpression; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.ArrayAccessExpression; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.AtLabelExpression; @@ -67,6 +65,7 @@ import de.uni_freiburg.informatik.ultimate.model.acsl.ast.OldValueExpression; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.RealLiteral; import de.uni_freiburg.informatik.ultimate.model.acsl.ast.UnaryExpression; +import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.BacktranslatedACSLValue.BacktranslatedExpression; import de.uni_freiburg.informatik.ultimate.util.datastructures.BigInterval; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; @@ -126,7 +125,7 @@ public BacktranslatedExpression translateEnsuresExpression( final var oldVarEqualities = computeOldVarEqualities(cFun, modifiableGlobals); if (oldVarEqualities.isPresent()) { return new BacktranslatedExpression( - new BinaryExpression(Operator.LOGICAND, mainExpression.getExpression(), oldVarEqualities.get()), + new BinaryExpression(Operator.LOGICAND, mainExpression.expression(), oldVarEqualities.get()), new CPrimitive(CPrimitives.INT), BigInterval.booleanRange()); } @@ -135,7 +134,9 @@ public BacktranslatedExpression translateEnsuresExpression( private Optional computeOldVarEqualities(final String proc, final Set modifiableGlobals) { - final var modifiableNames = modifiableGlobals.stream().map(e -> e.getIdentifier()).collect(Collectors.toSet()); + final var modifiableNames = modifiableGlobals.stream() + .map(de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression::getIdentifier) + .collect(Collectors.toSet()); final boolean modifiesMemory = modifiableNames.stream().anyMatch(name -> name.startsWith(SFO.MEMORY)); return mSymbolTable.getGlobalScope().entrySet().stream().flatMap( @@ -348,63 +349,63 @@ private BacktranslatedExpression translateFunctionApplication( case "NaN": return new BacktranslatedExpression(new RealLiteral(String.valueOf(Float.NaN))); case "bvadd": - final Expression addition = new BinaryExpression(Operator.ARITHPLUS, translatedArguments[0].getExpression(), - translatedArguments[1].getExpression()); + final Expression addition = new BinaryExpression(Operator.ARITHPLUS, translatedArguments[0].expression(), + translatedArguments[1].expression()); return new BacktranslatedExpression(new BinaryExpression(Operator.ARITHMOD, addition, new IntegerLiteral(String.valueOf(1L << bitSize)))); case "bvmul": return new BacktranslatedExpression(new BinaryExpression(Operator.ARITHMUL, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsub": - final Expression sub = new BinaryExpression(Operator.ARITHMINUS, translatedArguments[0].getExpression(), - translatedArguments[1].getExpression()); + final Expression sub = new BinaryExpression(Operator.ARITHMINUS, translatedArguments[0].expression(), + translatedArguments[1].expression()); return new BacktranslatedExpression( new BinaryExpression(Operator.ARITHMOD, sub, new IntegerLiteral(String.valueOf(1L << bitSize)))); case "bvand": return new BacktranslatedExpression(new BinaryExpression(Operator.BITAND, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvor": return new BacktranslatedExpression(new BinaryExpression(Operator.BITOR, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvxor": return new BacktranslatedExpression(new BinaryExpression(Operator.BITXOR, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvshl": return new BacktranslatedExpression(new BinaryExpression(Operator.BITSHIFTLEFT, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvashr": return new BacktranslatedExpression(new BinaryExpression(Operator.BITSHIFTRIGHT, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvslt": case "bvult": return new BacktranslatedExpression(new BinaryExpression(Operator.COMPLT, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsle": case "bvule": return new BacktranslatedExpression(new BinaryExpression(Operator.COMPLEQ, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsgt": case "bvugt": return new BacktranslatedExpression(new BinaryExpression(Operator.COMPGT, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsge": case "bvuge": return new BacktranslatedExpression(new BinaryExpression(Operator.COMPGEQ, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsdiv": case "bvudiv": return new BacktranslatedExpression(new BinaryExpression(Operator.ARITHDIV, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvsrem": case "bvurem": return new BacktranslatedExpression(new BinaryExpression(Operator.ARITHMOD, - translatedArguments[0].getExpression(), translatedArguments[1].getExpression())); + translatedArguments[0].expression(), translatedArguments[1].expression())); case "bvneg": return new BacktranslatedExpression( - new UnaryExpression(UnaryExpression.Operator.MINUS, translatedArguments[0].getExpression())); + new UnaryExpression(UnaryExpression.Operator.MINUS, translatedArguments[0].expression())); case "bvnot": - return new BacktranslatedExpression(new UnaryExpression(UnaryExpression.Operator.LOGICCOMPLEMENT, - translatedArguments[0].getExpression())); + return new BacktranslatedExpression( + new UnaryExpression(UnaryExpression.Operator.LOGICCOMPLEMENT, translatedArguments[0].expression())); default: mReporter.accept("Missing case for function " + function); return null; @@ -462,11 +463,11 @@ private BacktranslatedExpression translateIntegerLiteral(final BigInteger value) final var split = value.abs().divideAndRemainder(mTypeSizes.getMaxValueOfPrimitiveType(ulonglong).add(BigInteger.ONE)); final Expression upper = new CastExpression(AcslTypeUtils.translateCTypeToAcslType(resultType), - translateIntegerLiteral(split[0]).getExpression()); + translateIntegerLiteral(split[0]).expression()); final Expression shift = new IntegerLiteral(String.valueOf(8 * mTypeSizes.getSize(ulonglong.getType()))); Expression result = new BinaryExpression(Operator.BITSHIFTLEFT, upper, shift); if (split[1].signum() != 0) { - result = new BinaryExpression(Operator.BITOR, result, translateIntegerLiteral(split[1]).getExpression()); + result = new BinaryExpression(Operator.BITOR, result, translateIntegerLiteral(split[1]).expression()); } if (value.signum() < 0) { result = new UnaryExpression(UnaryExpression.Operator.MINUS, result); @@ -523,24 +524,22 @@ private BacktranslatedExpression translateDiv(final BacktranslatedExpression lhs if (lhs == null || rhs == null) { return null; } - final BigInterval leftRange = lhs.getRange(); - final BigInterval rightRange = rhs.getRange(); + final BigInterval leftRange = lhs.range(); + final BigInterval rightRange = rhs.range(); final BigInterval resultRange = leftRange.euclideanDivide(rightRange); - final Expression baseExpr = new BinaryExpression(Operator.ARITHDIV, lhs.getExpression(), rhs.getExpression()); + final Expression baseExpr = new BinaryExpression(Operator.ARITHDIV, lhs.expression(), rhs.expression()); if (leftRange.isNonNegative()) { if (resultRange.isSingleton()) { return translateIntegerLiteral(resultRange.getMinValue()); } - return new BacktranslatedExpression(baseExpr, lhs.getCType(), resultRange); + return new BacktranslatedExpression(baseExpr, lhs.cType(), resultRange); } // If the left operand might be negative, we need to translate euclidian modulo to remainder // (they only coincide, if the left operand is positive) final Expression posExpr = new BinaryExpression(Operator.ARITHMINUS, - new BinaryExpression(Operator.ARITHDIV, lhs.getExpression(), rhs.getExpression()), - new IntegerLiteral("1")); + new BinaryExpression(Operator.ARITHDIV, lhs.expression(), rhs.expression()), new IntegerLiteral("1")); final Expression negExpr = new BinaryExpression(Operator.ARITHPLUS, - new BinaryExpression(Operator.ARITHDIV, lhs.getExpression(), rhs.getExpression()), - new IntegerLiteral("1")); + new BinaryExpression(Operator.ARITHDIV, lhs.expression(), rhs.expression()), new IntegerLiteral("1")); final Expression expr; if (rightRange.isNonNegative()) { expr = posExpr; @@ -548,15 +547,15 @@ private BacktranslatedExpression translateDiv(final BacktranslatedExpression lhs expr = negExpr; } else { expr = new IfThenElseExpression( - new BinaryExpression(Operator.COMPGEQ, rhs.getExpression(), new IntegerLiteral("0")), posExpr, + new BinaryExpression(Operator.COMPGEQ, rhs.expression(), new IntegerLiteral("0")), posExpr, negExpr); } if (leftRange.isNonPositive()) { - return new BacktranslatedExpression(expr, lhs.getCType(), resultRange); + return new BacktranslatedExpression(expr, lhs.cType(), resultRange); } return new BacktranslatedExpression(new IfThenElseExpression( - new BinaryExpression(Operator.COMPGEQ, lhs.getExpression(), new IntegerLiteral("0")), baseExpr, expr), - lhs.getCType(), resultRange); + new BinaryExpression(Operator.COMPGEQ, lhs.expression(), new IntegerLiteral("0")), baseExpr, expr), + lhs.cType(), resultRange); } private BacktranslatedExpression translateModulo(final BacktranslatedExpression lhs, @@ -564,8 +563,8 @@ private BacktranslatedExpression translateModulo(final BacktranslatedExpression if (lhs == null || rhs == null) { return null; } - final BigInterval leftRange = lhs.getRange(); - final BigInterval rightRange = rhs.getRange(); + final BigInterval leftRange = lhs.range(); + final BigInterval rightRange = rhs.range(); if (rightRange.isStrictlyPositive()) { final var minModRange = new BigInterval(BigInteger.ZERO, rightRange.getMinValue().subtract(BigInteger.ONE)); if (minModRange.contains(leftRange)) { @@ -573,17 +572,17 @@ private BacktranslatedExpression translateModulo(final BacktranslatedExpression return lhs; } } - final Expression baseExpr = new BinaryExpression(Operator.ARITHMOD, lhs.getExpression(), rhs.getExpression()); + final Expression baseExpr = new BinaryExpression(Operator.ARITHMOD, lhs.expression(), rhs.expression()); final BigInterval resultRange = leftRange.euclideanModulo(rightRange); if (leftRange.isNonNegative()) { - return new BacktranslatedExpression(baseExpr, lhs.getCType(), resultRange); + return new BacktranslatedExpression(baseExpr, lhs.cType(), resultRange); } // If the left operand might be negative, we need to translate euclidian modulo to remainder // (they only coincide, if the left operand is positive) final Expression posExpr = new BinaryExpression(Operator.ARITHPLUS, - new BinaryExpression(Operator.ARITHMOD, lhs.getExpression(), rhs.getExpression()), rhs.getExpression()); + new BinaryExpression(Operator.ARITHMOD, lhs.expression(), rhs.expression()), rhs.expression()); final Expression negExpr = new BinaryExpression(Operator.ARITHMINUS, - new BinaryExpression(Operator.ARITHMOD, lhs.getExpression(), rhs.getExpression()), rhs.getExpression()); + new BinaryExpression(Operator.ARITHMOD, lhs.expression(), rhs.expression()), rhs.expression()); final Expression expr; if (rightRange.isNonNegative()) { expr = posExpr; @@ -591,15 +590,15 @@ private BacktranslatedExpression translateModulo(final BacktranslatedExpression expr = negExpr; } else { expr = new IfThenElseExpression( - new BinaryExpression(Operator.COMPGEQ, rhs.getExpression(), new IntegerLiteral("0")), posExpr, + new BinaryExpression(Operator.COMPGEQ, rhs.expression(), new IntegerLiteral("0")), posExpr, negExpr); } if (leftRange.isNonPositive()) { - return new BacktranslatedExpression(expr, lhs.getCType(), resultRange); + return new BacktranslatedExpression(expr, lhs.cType(), resultRange); } return new BacktranslatedExpression(new IfThenElseExpression( - new BinaryExpression(Operator.COMPGEQ, lhs.getExpression(), new IntegerLiteral("0")), baseExpr, expr), - lhs.getCType(), resultRange); + new BinaryExpression(Operator.COMPGEQ, lhs.expression(), new IntegerLiteral("0")), baseExpr, expr), + lhs.cType(), resultRange); } private BacktranslatedExpression translateBinaryExpression( @@ -607,10 +606,10 @@ private BacktranslatedExpression translateBinaryExpression( final boolean isNegated) { final BacktranslatedExpression lhs = translateExpression(expression.getLeft(), context, isNegated); final BacktranslatedExpression rhs = translateExpression(expression.getRight(), context, isNegated); - final BigInterval leftRange = lhs == null ? BigInterval.unbounded() : lhs.getRange(); - final BigInterval rightRange = rhs == null ? BigInterval.unbounded() : rhs.getRange(); - final CType leftType = lhs == null ? null : lhs.getCType(); - final CType rightType = rhs == null ? null : rhs.getCType(); + final BigInterval leftRange = lhs == null ? BigInterval.unbounded() : lhs.range(); + final BigInterval rightRange = rhs == null ? BigInterval.unbounded() : rhs.range(); + final CType leftType = lhs == null ? null : lhs.cType(); + final CType rightType = rhs == null ? null : rhs.cType(); final Operator operator; final BigInterval range; CType resultType; @@ -709,14 +708,14 @@ private BacktranslatedExpression translateBinaryExpression( if (range.isSingleton()) { return translateIntegerLiteral(range.getMinValue()); } - Expression resultingLhs = lhs.getExpression(); + Expression resultingLhs = lhs.expression(); if (!fitsInType(range, resultType)) { resultType = determineTypeForRange(range); if (resultType != null) { resultingLhs = new CastExpression(AcslTypeUtils.translateCTypeToAcslType(resultType), resultingLhs); } } - final Expression resultExpr = new BinaryExpression(operator, resultingLhs, rhs.getExpression()); + final Expression resultExpr = new BinaryExpression(operator, resultingLhs, rhs.expression()); return new BacktranslatedExpression(resultExpr, resultType, range); } @@ -732,9 +731,9 @@ private BacktranslatedExpression translateUnaryExpression( if (innerTrans == null) { return null; } - range = innerTrans.getRange().negate(); - resultExpr = new UnaryExpression(UnaryExpression.Operator.MINUS, innerTrans.getExpression()); - cType = innerTrans.getCType(); + range = innerTrans.range().negate(); + resultExpr = new UnaryExpression(UnaryExpression.Operator.MINUS, innerTrans.expression()); + cType = innerTrans.cType(); break; } case LOGICNEG: { @@ -743,8 +742,8 @@ private BacktranslatedExpression translateUnaryExpression( return null; } range = BigInterval.booleanRange(); - resultExpr = new UnaryExpression(UnaryExpression.Operator.LOGICNEG, innerTrans.getExpression()); - cType = innerTrans.getCType(); + resultExpr = new UnaryExpression(UnaryExpression.Operator.LOGICNEG, innerTrans.expression()); + cType = innerTrans.cType(); break; } case OLD: { @@ -752,16 +751,16 @@ private BacktranslatedExpression translateUnaryExpression( if (innerTrans == null) { return null; } - range = innerTrans.getRange(); + range = innerTrans.range(); // In ACSL \old is only allowed in function contracts. // Therefore we translate an old-expression old(x) in Boogie to either \old(x), if the context is a function // (which means that the expression is present in a contract), or \at(x, Pre) otherwise. if (isFunctionDefinition(context)) { - resultExpr = new OldValueExpression(innerTrans.getExpression()); + resultExpr = new OldValueExpression(innerTrans.expression()); } else { - resultExpr = new AtLabelExpression(innerTrans.getExpression(), "Pre"); + resultExpr = new AtLabelExpression(innerTrans.expression(), "Pre"); } - cType = innerTrans.getCType(); + cType = innerTrans.cType(); break; } default: @@ -802,54 +801,17 @@ private BacktranslatedExpression translateArrayAccess( mReporter.accept("Cannot backtranslate array access to array " + expression.getArray()); return null; } - Expression result = array.getExpression(); - CType resultType = array.getCType(); + Expression result = array.expression(); + CType resultType = array.cType(); for (final var index : expression.getIndices()) { final BacktranslatedExpression translatedIndex = translateExpression(index, context); if (translatedIndex == null) { return null; } - result = new ArrayAccessExpression(result, translatedIndex.getExpression()); + result = new ArrayAccessExpression(result, translatedIndex.expression()); resultType = ((CArray) resultType).getValueType(); } final var range = getRangeForCType(resultType); return new BacktranslatedExpression(result, resultType, range); } - - public static final class BacktranslatedExpression { - private final Expression mExpression; - private final CType mCType; - private final BigInterval mRange; - - public BacktranslatedExpression(final Expression expression) { - this(expression, null, BigInterval.unbounded()); - } - - public BacktranslatedExpression(final Expression expression, final CType cType, final BigInterval range) { - mExpression = expression; - mCType = cType; - mRange = Objects.requireNonNull(range); - } - - public Expression getExpression() { - return mExpression; - } - - public CType getCType() { - return mCType; - } - - public BigInterval getRange() { - return mRange; - } - - @Override - public String toString() { - return ACSLPrettyPrinter.print(mExpression); - } - - public BacktranslatedExpression asOldExpression() { - return new BacktranslatedExpression(new OldValueExpression(mExpression), mCType, mRange); - } - } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java index 9d5e14ca7f1..3f8cc8018ff 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSL2BoogieBacktranslator.java @@ -28,6 +28,7 @@ */ package de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator; +import java.math.BigInteger; import java.util.ArrayDeque; import java.util.ArrayList; import java.util.Arrays; @@ -98,8 +99,8 @@ import de.uni_freiburg.informatik.ultimate.core.model.translation.IBacktranslatedCFG; import de.uni_freiburg.informatik.ultimate.core.model.translation.IProgramExecution; import de.uni_freiburg.informatik.ultimate.core.model.translation.IProgramExecution.ProgramState; -import de.uni_freiburg.informatik.ultimate.model.acsl.ast.FakePointerExpression; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.Boogie2ACSL.BacktranslatedExpression; +import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.BacktranslatedACSLValue.BacktranslatedExpression; +import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.BacktranslatedACSLValue.FakePointer; import de.uni_freiburg.informatik.ultimate.util.datastructures.DataStructureUtils; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; @@ -109,7 +110,7 @@ * @author dietsch@informatik.uni-freiburg.de */ public class CACSL2BoogieBacktranslator extends - DefaultTranslator { + DefaultTranslator { /** * Throw error in cases where we know that the backtranslation is not exact. @@ -129,7 +130,7 @@ public class CACSL2BoogieBacktranslator extends public CACSL2BoogieBacktranslator(final IUltimateServiceProvider services, final TypeSizes typeSizes, final CACSL2BoogieBacktranslatorMapping mapping, final LocationFactory locationFactory, final FlatSymbolTable symbolTable) { - super(BoogieASTNode.class, CACSLLocation.class, Expression.class, BacktranslatedExpression.class); + super(BoogieASTNode.class, CACSLLocation.class, Expression.class, BacktranslatedACSLValue.class); mServices = services; mLogger = mServices.getLoggingService().getLogger(Activator.PLUGIN_ID); mMapping = mapping; @@ -151,7 +152,7 @@ public List translateTrace(final List trace) { .collect(Collectors.toList()); final IProgramExecution tracePE = new BoogieProgramExecution(Collections.emptyMap(), ateTrace, false); - final IProgramExecution translatedPE = + final IProgramExecution translatedPE = translateProgramExecution(tracePE); final List translatedTrace = new ArrayList<>(); @@ -164,7 +165,7 @@ public List translateTrace(final List trace) { } @Override - public IProgramExecution + public IProgramExecution translateProgramExecution(final IProgramExecution oldPE) { assert checkCallStackSourceProgramExecution(mLogger, oldPE) : "callstack of initial program execution already broken"; @@ -175,7 +176,7 @@ assert checkCallStackTargetProgramExecution(mLogger, translated) } @Override - public Lasso> + public Lasso> translateLassoProgramExecution(final Lasso> oldPE) { assert checkCallStackSourceLassoProgramExecution(mLogger, oldPE) : "callstack of initial program execution already broken"; @@ -190,11 +191,11 @@ assert checkCallStackTargetLassoProgramExecution(mLogger, translated) translateProgramExecutionInternal(final IProgramExecution oldPE) { // initial state - ProgramState initialState = translateProgramState(oldPE.getInitialProgramState()); + ProgramState initialState = translateProgramState(oldPE.getInitialProgramState()); // translate trace and program state in tandem final List> translatedATEs = new ArrayList<>(); - final List> translatedProgramStates = new ArrayList<>(); + final List> translatedProgramStates = new ArrayList<>(); for (int i = 0; i < oldPE.getLength(); ++i) { final AtomicTraceElement ate = oldPE.getTraceElement(i); @@ -295,10 +296,10 @@ assert checkCallStackTargetLassoProgramExecution(mLogger, translated) // reason must be the null node itself // remove all ATEs where the step node is null final Iterator> iter = translatedATEs.iterator(); - final Iterator> iterPs = translatedProgramStates.iterator(); + final Iterator> iterPs = translatedProgramStates.iterator(); while (iter.hasNext()) { final CACSLLocation step = iter.next().getStep(); - final ProgramState programStateAfter = iterPs.next(); + final ProgramState programStateAfter = iterPs.next(); if (!(step instanceof CLocation)) { continue; } @@ -373,7 +374,7 @@ private AtomicTraceElement handleLoopConditional(final AtomicTrac private int handleCASTFunctionCallExpression(final IProgramExecution programExecution, final int index, final CASTFunctionCallExpression fcall, final CLocation cloc, final List> translatedAtoTraceElems, - final List> translatedProgramStates) { + final List> translatedProgramStates) { // directly after the function call expression we find // for each argument a CASTFunctionDefinition / AssignmentStatement that // maps the input variable to a new local one (because boogie function @@ -435,7 +436,7 @@ assert checkCallStackTarget(mLogger, private int handleNonCallDuringCASTFunctionCallExpression( final IProgramExecution programExecution, final int index, final CLocation cloc, final List> translatedAtoTraceElems, - final List> translatedProgramStates, + final List> translatedProgramStates, final AtomicTraceElement currentATE, final BoogieASTNode currentTraceElement) { // this is some special case, e.g. an assert false or a havoc or a fork or a join final EnumSet stepInfo; @@ -564,13 +565,13 @@ private static int findMergeSequence(final IProgramExecution translateProgramState(final ProgramState programState) { + public ProgramState translateProgramState(final ProgramState programState) { if (programState == null) { // cannot translate nothin' return null; } - final Map> translatedStateMap = new HashMap<>(); - final ProgramState compressedProgramState = compressProgramState(programState); + final Map> compressedProgramState = + compressProgramState(programState); // Suppress backtranslation warnings for program states // We just skip variables like pointers or aux-vars in the programs states @@ -578,28 +579,28 @@ public ProgramState translateProgramState(final Progra final boolean generateOld = mGenerateBacktranslationWarnings; final boolean warnedOld = mBacktranslationWarned; mGenerateBacktranslationWarnings = false; - for (final ExpressionOrPointer varName : compressedProgramState.getVariables()) { - translateProgramStateEntry(varName, compressedProgramState, translatedStateMap); + final Map> translatedStateMap = new HashMap<>(); + for (final var entry : compressedProgramState.entrySet()) { + translateProgramStateEntry(entry, translatedStateMap); } mGenerateBacktranslationWarnings = generateOld; mBacktranslationWarned = warnedOld; - return new ProgramState<>(translatedStateMap, BacktranslatedExpression.class); + return new ProgramState<>(translatedStateMap, BacktranslatedACSLValue.class); } - private void translateProgramStateEntry(final ExpressionOrPointer varName, - final ProgramState compressedProgramState, - final Map> translatedStateMap) { + private void translateProgramStateEntry(final Map.Entry> entry, + final Map> translatedStateMap) { // first, translate name - final BacktranslatedExpression newVarName = translateExpressionForProgramState(varName); + final BacktranslatedExpression newVarName = translateExpression(entry.getKey()); if (newVarName == null) { return; } + // then, translate values - final Collection varValues = compressedProgramState.getValues(varName); - final Collection newVarValues = new ArrayList<>(); - for (final ExpressionOrPointer varValue : varValues) { - final BacktranslatedExpression newVarValue = translateExpressionForProgramState(varValue); + final Collection newVarValues = new ArrayList<>(); + for (final ExpressionOrPointer varValue : entry.getValue()) { + final BacktranslatedACSLValue newVarValue = translateExpressionForProgramState(varValue); if (newVarValue != null) { newVarValues.add(newVarValue); } @@ -607,7 +608,7 @@ private void translateProgramStateEntry(final ExpressionOrPointer varName, // finally, merge with possibly existing values for this name if (!newVarValues.isEmpty()) { - final Collection oldVarValues = translatedStateMap.put(newVarName, newVarValues); + final Collection oldVarValues = translatedStateMap.put(newVarName, newVarValues); if (oldVarValues != null) { newVarValues.addAll(oldVarValues); } @@ -615,39 +616,38 @@ private void translateProgramStateEntry(final ExpressionOrPointer varName, } /** - * Replace base and offset with one {@link Pointer} + * Replace separate values for base and offset of a pointer with one {@link PointerValue} * * @param programState * May not be null */ - private ProgramState compressProgramState(final ProgramState programState) { + private Map> + compressProgramState(final ProgramState programState) { final List>> oldEntries = new ArrayList<>(); - final List>> newEntries = new ArrayList<>(); + final List>> newEntries = new ArrayList<>(); for (final Expression var : programState.getVariables()) { final Pair> entry = new Pair<>(var, programState.getValues(var)); oldEntries.add(entry); } - int x = -1; - int y = 0; - while (x < y) { - // collect all pointers - x = newEntries.size(); - extractTemporaryPointerExpression(oldEntries, newEntries); - y = newEntries.size(); + // collect all pointers + var extractedPointer = extractTemporaryPointerExpression(oldEntries); + while (extractedPointer != null) { + newEntries.add(extractedPointer); + extractedPointer = extractTemporaryPointerExpression(oldEntries); } + // wrap non-pointers for (final var oldEntry : oldEntries) { - final var wrappedValues = oldEntry.getValue().stream(). map(WrappedExpression::new) - .collect(Collectors.toList()); - final Pair> wrappedEntry = - new Pair<>(new WrappedExpression(oldEntry.getFirst()), wrappedValues); - newEntries.add(wrappedEntry); + final var wrappedValues = + oldEntry.getValue().stream(). map(WrappedExpression::new).toList(); + newEntries.add(new Pair<>(oldEntry.getFirst(), wrappedValues)); } - final Map> map = new HashMap<>(); - for (final Pair> entry : newEntries) { + // merge duplicates and collect everything in a Map + final Map> map = new HashMap<>(); + for (final Pair> entry : newEntries) { final Collection newValues = entry.getSecond(); final Collection oldValues = map.put(entry.getFirst(), entry.getSecond()); if (oldValues != null) { @@ -655,85 +655,76 @@ private ProgramState compressProgramState(final ProgramStat } } - return new ProgramState<>(map, ExpressionOrPointer.class); + return map; } - private void extractTemporaryPointerExpression(final List>> oldEntries, - final List>> newEntries) { + private Pair> + extractTemporaryPointerExpression(final List>> oldEntries) { + // Find pointer base expressions in oldEntries, merge them with matching pointer offset expressions, + // and move the combined expression to newEntries. + // (We do a reversed by-index iteration over oldEntries so we can safely call remove() for the index.) for (int i = oldEntries.size() - 1; i >= 0; i--) { final Pair> entry = oldEntries.get(i); - boolean isPointerBase = false; - boolean isOld = false; - if (isPointerBase(entry.getFirst())) { - isPointerBase = true; - isOld = false; - } else if (isOldPointerBase(entry.getFirst())) { - isPointerBase = true; - isOld = true; + // Check if the current entry is the base of a pointer struct + final var pointerVariable = PointerVariable.fromBaseExpression(entry.getFirst()); + if (pointerVariable == null) { + continue; } - if (isPointerBase) { - final String name = getPointerName(entry.getFirst(), isOld); - for (int j = oldEntries.size() - 1; j >= 0; j--) { - final Pair> otherentry = oldEntries.get(j); - if (!isPointerOffsetFor(otherentry.getFirst(), name, isOld)) { - continue; - } - final var tmpPointerVar = assemblePointer(entry.getFirst(), otherentry.getFirst(), isOld); - if (entry.getSecond().size() != 1 || otherentry.getSecond().size() != 1) { - reportUnfinishedBacktranslation("Pointers with multiple values"); - } - final var valueBase = DataStructureUtils.getOneAndOnly(entry.getSecond(), "pointer base"); - final var valueOffset = DataStructureUtils.getOneAndOnly(otherentry.getSecond(), "pointer offset"); - final var tmpPointerValue = new Pointer(entry.getFirst().getLocation(), valueBase, valueOffset); - - final Pair> newEntry = - new Pair<>(tmpPointerVar, new ArrayList<>()); - newEntry.getSecond().add(tmpPointerValue); - newEntries.add(newEntry); - oldEntries.remove(entry); - oldEntries.remove(otherentry); - return; + // Find a matching offset expression for the same pointer struct. + // (We do a reversed by-index iteration over oldEntries so we can safely call remove() for the offset.) + for (int j = oldEntries.size() - 1; j >= 0; j--) { + final Pair> otherentry = oldEntries.get(j); + if (!pointerVariable.isMatchingPointerOffset(otherentry.getFirst())) { + continue; } + + if (entry.getSecond().size() != 1 || otherentry.getSecond().size() != 1) { + reportUnfinishedBacktranslation("Pointers with multiple values"); + } + final var valueBase = DataStructureUtils.getOneAndOnly(entry.getSecond(), "pointer base"); + final var valueOffset = DataStructureUtils.getOneAndOnly(otherentry.getSecond(), "pointer offset"); + final var pointerValue = new PointerValue(valueBase, valueOffset); + + // Remove the now obsolete entries. + oldEntries.remove(entry); + oldEntries.remove(otherentry); + + // must be a mutable list, so do not use List.of(pointerValue) here + final var values = new ArrayList(); + values.add(pointerValue); + return new Pair<>(pointerVariable.toExpression(), values); } } + return null; } - private static boolean isPointerBase(final Expression expr) { - return expr instanceof final IdentifierExpression id && id.getIdentifier().endsWith(SFO.POINTER_BASE); - } - - private static boolean isOldPointerBase(final Expression expr) { - return expr instanceof final UnaryExpression unary && unary.getOperator() == Operator.OLD - && isPointerBase(unary.getExpr()); + private BacktranslatedACSLValue translateExpressionForProgramState(final ExpressionOrPointer expression) { + return switch (expression) { + case final PointerValue pointer -> translatePointer(pointer); + case WrappedExpression(final var expr) -> translateExpression(expr); + }; } - private static boolean isPointerOffsetFor(final Expression expr, final String name, final boolean isOld) { - if (isOld && expr instanceof final UnaryExpression uexp) { - return uexp.getOperator() == Operator.OLD && isPointerOffsetFor(uexp.getExpr(), name, false); - } - if (!isOld && expr instanceof final IdentifierExpression idExpr) { - final var identifier = idExpr.getIdentifier(); - return identifier.startsWith(name) && identifier.endsWith(SFO.POINTER_OFFSET); + private FakePointer translatePointer(final PointerValue pointer) { + final BacktranslatedExpression base = translateExpression(pointer.base()); + if (!base.range().isSingleton()) { + reportUnfinishedBacktranslation("Pointer with non-unique base value"); + return null; } - return false; - } + final BigInteger baseValue = base.range().getMinValue(); - private static String getPointerName(final Expression base, final boolean isOld) { - if (isOld) { - return getPointerName(((UnaryExpression) base).getExpr(), false); + final BacktranslatedExpression offset = translateExpression(pointer.offset()); + if (!offset.range().isSingleton()) { + reportUnfinishedBacktranslation("Pointer with non-unique base value"); + return null; } - final String baseName = ((IdentifierExpression) base).getIdentifier(); - return baseName.substring(0, baseName.length() - SFO.POINTER_BASE.length()); - } + final BigInteger offsetValue = offset.range().getMinValue(); - private Pointer assemblePointer(final Expression base, final Expression offset, final boolean isOld) { - if (isOld) { - return assemblePointer(((UnaryExpression) base).getExpr(), ((UnaryExpression) offset).getExpr(), false) - .asOldExpression(); - } - return new Pointer(base.getLoc(), base, offset); + // Create a value like {base:offset} + // This is not a real ACSL expression, so we wrap it into FakePointer. + return new FakePointer(baseValue, offsetValue); } @Override @@ -781,7 +772,7 @@ private Multigraph translateCFGEdge( } @Override - public ProcedureContract translateProcedureContract( + public ProcedureContract translateProcedureContract( final ProcedureContract oldContract, final ILocation context) { if (context instanceof final CACSLLocation loc && loc.ignoreDuringBacktranslation()) { return null; @@ -915,33 +906,6 @@ private void reduceCFG(final IExplicitEdgesMultigraph { + implements IBacktranslationValueProvider { @Override public int getStartLineNumberFromStep(final CACSLLocation step) { @@ -114,8 +113,9 @@ public String getStringFromTraceElement(final CACSLLocation traceelement) { } @Override - public String getStringFromExpression(final BacktranslatedExpression expression) { - return ACSLPrettyPrinter.print(expression.getExpression()); + public String getStringFromExpression(final BacktranslatedACSLValue expression) { + // Both BacktranslatedExpression and FakePointer have suitable toString() implementations. + return expression.toString(); } private String getStringFromIASTNode(final IASTNode currentStepNode) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSLProgramExecution.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSLProgramExecution.java index 878b205dd4c..592fba1565d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSLProgramExecution.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/plugins/generator/cacsl2boogietranslator/CACSLProgramExecution.java @@ -35,23 +35,22 @@ import de.uni_freiburg.informatik.ultimate.core.model.translation.AtomicTraceElement; import de.uni_freiburg.informatik.ultimate.core.model.translation.IBacktranslationValueProvider; import de.uni_freiburg.informatik.ultimate.core.model.translation.IProgramExecution; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.Boogie2ACSL.BacktranslatedExpression; /** * * @author dietsch@informatik.uni-freiburg.de * */ -public class CACSLProgramExecution implements IProgramExecution { +public class CACSLProgramExecution implements IProgramExecution { - private final ProgramState mInitialState; - private final List> mProgramStates; + private final ProgramState mInitialState; + private final List> mProgramStates; private final List> mTrace; private final boolean mIsConcurrent; - public CACSLProgramExecution(final ProgramState initialState, + public CACSLProgramExecution(final ProgramState initialState, final Collection> trace, - final Collection> programStates, final boolean isConcurrent) { + final Collection> programStates, final boolean isConcurrent) { assert trace != null; assert programStates != null; assert trace.size() == programStates.size() : "Need a program state after each atomic trace element"; @@ -84,18 +83,18 @@ public AtomicTraceElement getTraceElement(final int i) { } @Override - public ProgramState getProgramState(final int i) { + public ProgramState getProgramState(final int i) { return mProgramStates.get(i); } @Override - public ProgramState getInitialProgramState() { + public ProgramState getInitialProgramState() { return mInitialState; } @Override - public Class getExpressionClass() { - return BacktranslatedExpression.class; + public Class getExpressionClass() { + return BacktranslatedACSLValue.class; } @Override @@ -105,13 +104,13 @@ public Class getTraceElementClass() { @Override public String toString() { - final ProgramExecutionFormatter pef = + final ProgramExecutionFormatter pef = new ProgramExecutionFormatter<>(new CACSLBacktranslationValueProvider()); return pef.formatProgramExecution(this); } @Override - public IBacktranslationValueProvider getBacktranslationValueProvider() { + public IBacktranslationValueProvider getBacktranslationValueProvider() { return new CACSLBacktranslationValueProvider(); }