diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java index d75df8a3831..7d8a2c95bf2 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java @@ -865,7 +865,6 @@ public static boolean isCharArray(final ICType cTypeRaw) { || cPrimitive.getType() == CPrimitives.SCHAR); } - @Override public IMemoryPointer getMemoryPointer() { return mMemoryPointer; } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java index ae457a033fb..420458775b8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java @@ -29,26 +29,21 @@ import java.math.BigInteger; import java.util.Collection; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * The interface defining the functions for the different memory addressing schemes. @@ -73,40 +68,40 @@ public interface IMemoryAdressing { List getMetaDataDeclarations(); /** - * Constructs a list of expressions that are used in the specifications of malloc. + * Constructs the specification of malloc. * - * @return The expressions. + * @return a record representing the specification */ - List>> constructMallocSpecificationExpressions(ILocation tuLoc, - MemoryArea memoryArea, RequiredMemoryModelFeatures requiredMemoryModelFeatures, + AllocationProcedureSpec constructMallocSpecification(ILocation tuLoc, MemoryArea memoryArea, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs a list of expressions that are used in the specifications of dealloc. + * Constructs the specification of dealloc. * - * @return The expressions. + * @return a record representing the specification */ - List, Boolean>> constructDeallocSpecificationExpressions(ILocation tuLoc, + AllocationProcedureSpec constructDeallocSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Returns a list of statements that are part of Ultimate.Init. + * Constructs the specification of allocInit. * - * @return The statements. + * @return a record representing the specification */ - List constructUltimateInitStatements(ILocation loc, + AllocationProcedureSpec constructAllocInitSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs the expressions used in the specifications for allocInit. + * Returns a list of statements that are part of Ultimate.Init. * - * @return The expressions. + * @return The statements. */ - List>> constructAllocInitSpecificationExpressions(ILocation tuLoc, + List constructUltimateInitStatements(ILocation loc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); /** * Add or subtracts a pointer and an integer. @@ -123,14 +118,6 @@ Expression doPointerArithmetic(final int operator, final ILocation loc, final Ex */ BigInteger getFixedAddressCounterCountingStep(final Expression size); - /** - * Returns the address for a field in a struct. - * - * @return The address. - */ - Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT); - /** * Adds an integer to a pointer. * @@ -139,16 +126,6 @@ Expression constructAddressForStructField(final ILocation loc, final Expression Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant); - /** - * Constructs the specifications that the pointer base address is valid. - * - * @return The specifications. - */ - List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** * Constructs the pointer base validity check expression. * @@ -163,9 +140,8 @@ Expression constructPointerValidityCheckExpr(final ILocation loc, final Expressi * * @return The specifications. */ - List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, Expression ptr, final Expression size, + final boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** @@ -173,8 +149,8 @@ List constructPointerTargetFullyAllocatedCheck(final ILocation lo * * @return The statements. */ - List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** @@ -205,14 +181,6 @@ List getChecksForFreeCall(final ILocation loc, final RValue pointerTo */ Expression addExpressionToPointer(final ILocation loc, final Expression ptrExpr, final Expression expr); - /** - * Returns a pointer to the last character of a string. - * - * @return The pointer. - */ - Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue); - /** * Creates the assume statement used in the handling of strchr. * @@ -223,16 +191,6 @@ AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expres final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** - * Constructs assert / assume statements for ptr memsafety checks. - * - * @return The statements. - */ - List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - /** * Construct the assume to check that src and dest don't overlap. * @@ -276,6 +234,11 @@ List constructReallocBodyStatements(final ILocation loc, final String final RequiredMemoryModelFeatures requiredFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); - Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + /** + * Constructs a boolean expression that, when evaluated at the end of a procedure invocation, results in + * {@code true} iff no memory is allocated that was not already allocated at the beginning of the invocation. + */ + Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java index cb22499ef54..df7310cc82a 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java @@ -27,15 +27,17 @@ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; import java.math.BigInteger; +import java.util.ArrayList; +import java.util.Collections; import java.util.List; +import java.util.Objects; import java.util.Set; +import de.uni_freiburg.informatik.ultimate.boogie.ast.EnsuresSpecification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This interface defines the functions for different memory management strategies. E.g. counting up, counting down, or @@ -45,20 +47,29 @@ */ public interface IMemoryManagementStrategy { /** - * Constructs a list of expressions that are used in the specifications of malloc. + * Constructs the specification of malloc. * - * @return The expressions. + * @return a record representing the specification */ - List>> constructMallocSpecificationExpressions(ILocation tuLoc, - MemoryArea memoryArea, RequiredMemoryModelFeatures requiredMemoryModelFeatures, + AllocationProcedureSpec constructMallocSpecification(ILocation tuLoc, MemoryArea memoryArea, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, + MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + + /** + * Constructs the specification of dealloc. + * + * @return a record representing the specification + */ + AllocationProcedureSpec constructDeallocSpecification(ILocation tuLoc, + RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); /** - * Constructs a list of expressions that are used in the specifications of dealloc. + * Constructs the specification for allocInit. * - * @return The expressions. + * @return a record representing the specification */ - List, Boolean>> constructDeallocSpecificationExpressions(ILocation tuLoc, + AllocationProcedureSpec constructAllocInitSpecification(ILocation tuLoc, RequiredMemoryModelFeatures requiredMemoryModelFeatures, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); @@ -72,11 +83,49 @@ List constructUltimateInitStatements(ILocation loc, MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, BigInteger fixedAddressCounter); /** - * Constructs the expressions used in the specifications for allocInit. + * Encapsulates the specification for an allocation procedure. + * + * Currently, we do not allow allocation procedures to have "requires" clauses. * - * @return The expressions. + * @param ensures + * the "ensures" clauses for the procedure + * @param freeEnsures + * the "free ensures" clauses for the procedure + * @param modifies + * the set of modified global variables of the procedure */ - List>> constructAllocInitSpecificationExpressions(ILocation tuLoc, - RequiredMemoryModelFeatures requiredMemoryModelFeatures, - MemoryModelDeclarationsHandler memoryModelDeclarationsHandler); + record AllocationProcedureSpec(List ensures, List freeEnsures, Set modifies) { + /** + * Convenience constructor for specs that do not have "free ensures" clauses. + */ + AllocationProcedureSpec(final List ensures, final Set modifies) { + this(ensures, Collections.emptyList(), modifies); + } + + public AllocationProcedureSpec { + Objects.requireNonNull(ensures); + Objects.requireNonNull(freeEnsures); + Objects.requireNonNull(modifies); + } + + /** + * Constructs "requires" resp. "free requires" clauses from the expressions stored in this specification. + * + * Note: Do not forget to handle the "modifies" clauses separately! + * + * @param loc + * the location for the specification clauses + * @return the list of clauses + */ + List constructSpecificationClauses(final ILocation loc) { + final var result = new ArrayList(); + for (final Expression ens : ensures) { + result.add(new EnsuresSpecification(loc, false, ens)); + } + for (final Expression freeEns : freeEnsures) { + result.add(new EnsuresSpecification(loc, true, freeEns)); + } + return result; + } + } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java index 1292c1c13f0..14a3cb38ba3 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java @@ -40,8 +40,6 @@ public interface IMemoryStructure { String getReadProcedureName(final CPrimitives primitive); - String getUncheckedReadProcedureName(final CPrimitives primitive); - String getWriteProcedureName(final CPrimitives primitive); String getUncheckedWriteProcedureName(final CPrimitives primitive); @@ -50,8 +48,6 @@ public interface IMemoryStructure { String getReadPointerProcedureName(); - String getUncheckedReadPointerProcedureName(); - String getWritePointerProcedureName(); String getUncheckedWritePointerProcedureName(); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java index 5329fecd005..e3080454170 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java @@ -1089,8 +1089,8 @@ public HeapLValue constructAddressForStructField(final ILocation loc, final Heap final CStructOrUnion cStructType = (CStructOrUnion) baseAddress.getCType().getUnderlyingType(); final var fieldOffset = mTypeSetAndOffsetComputer.constructOffsetForField(loc, cStructType, fieldIndex); - final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, baseAddress.getAddress(), - fieldOffset, mTypeSetAndOffsetComputer.getSizeT()); + final Expression newPointer = + mMemoryHandler.constructAddressForStructField(loc, baseAddress.getAddress(), fieldOffset); return LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, cStructType.getFieldTypes()[fieldIndex], null); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java index 658caefdf55..441d2742b78 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java @@ -45,7 +45,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.TranslationSettings; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; @@ -100,17 +99,6 @@ public BigInteger getFixedAddressCounterCountingStep(final Expression size) { return mTypeSizes.extractIntegerValue(size, new CPrimitive(CPrimitives.LONG)); } - @Override - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - - final Expression pointerBase = mMemoryPointer.getPointerAddress(baseAddress, loc); - final Expression sum = mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, - pointerBase, sizeT, fieldOffset.getAddressOffsetAsExpression(loc), sizeT); - - return mMemoryPointer.createPointerFromBase(sum, loc); - } - @Override public Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant) { @@ -146,16 +134,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryPointer.createPointerFromBase(basePlus, loc); } - @Override - public Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, - IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len), sizeT, - mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); - - return mMemoryPointer.createPointerFromBase(lenMinusOne, loc); - } - @Override public AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expression tmpExpr, final Expression argSPtr, final Expression nullPtrExpr, @@ -207,20 +185,4 @@ public List constructReallocBodyStatements(final ILocation loc, final return stmts; } - - @Override - public Expression constructPointerValidityCheckExpr(final ILocation loc, final Expression ptr, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - throw new UnsupportedOperationException("The pointer validity check is not available with the 1D Addressing"); - - } - - @Override - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - throw new UnsupportedOperationException( - "The valid array is not part of the metadata values from the 1D Addressing"); - - } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java index 1f801319401..9c38e4f09e1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing2D.java @@ -32,13 +32,10 @@ import java.math.BigInteger; import java.util.ArrayList; import java.util.Collection; -import java.util.Collections; import java.util.List; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; -import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation; -import de.uni_freiburg.informatik.ultimate.boogie.DeclarationInformation.StorageClass; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.StatementFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayAccessExpression; @@ -46,26 +43,20 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.RequiresSpecification; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; +import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; -import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Spec; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.PointerIntegerConversion; /** @@ -117,19 +108,6 @@ public BigInteger getFixedAddressCounterCountingStep(final Expression size) { return BigInteger.ONE; } - @Override - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - - final Expression pointerBase = mMemoryPointer.getPointerAddress(baseAddress, loc); - final Expression pointerOffset = mMemoryPointer.pointerOffset(baseAddress, loc); - - final Expression sum = mExpressionTranslation.constructArithmeticExpression(loc, IASTBinaryExpression.op_plus, - pointerOffset, sizeT, fieldOffset.getAddressOffsetAsExpression(loc), sizeT); - - return mMemoryPointer.constructPointerFromBaseAndOffset(pointerBase, sum, loc); - } - @Override public Expression addIntegerConstantToPointer(final ILocation loc, final Expression ptrExpr, final BigInteger integerConstant) { @@ -141,44 +119,12 @@ public Expression addIntegerConstantToPointer(final ILocation loc, final Express } @Override - public List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - final Expression ptrExpr = - ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, - new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); - final Expression isValid = constructPointerValidityCheckExpr(loc, ptrExpr, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - - final boolean isFreeRequires = mode == CheckMode.CHECK ? false : true; - - final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, isValid); - final Check check = new Check(Spec.MEMORY_DEREFERENCE); - check.annotate(spec); - return Collections.singletonList(spec); - } - - @Override - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - final Expression ptrExpr = - ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, - new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); - - final Expression ptrBase = mMemoryPointer.getPointerAddress(ptrExpr, loc); - final Expression ptrOffset = mMemoryPointer.pointerOffset(ptrExpr, loc); + final Expression ptrBase = mMemoryPointer.getPointerAddress(ptr, loc); + final Expression ptrOffset = mMemoryPointer.pointerOffset(ptr, loc); final CPrimitive cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); final Expression lengthArray = MemoryMetadataDefault2D.getLengthArray(loc, requiredMemoryModelFeatures, @@ -187,6 +133,7 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca ExpressionFactory.constructNestedArrayAccessExpression(loc, lengthArray, new Expression[] { ptrBase }); final Expression sum = constructPointerBinaryArithmeticExpression(loc, IASTBinaryExpression.op_plus, size, ptrOffset); + // TODO 2026-01-01: Should this be IASTBinaryExpression.op_lessThan ? Expression leq = constructPointerBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessEqual, sum, aae); final Expression zeroNumericLiteral = @@ -206,14 +153,7 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca leq = ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, noOverFlowInSum); } - final Expression offsetInAllocatedRange = - ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, offsetGeqZero); - - final boolean isFreeRequires = mode == CheckMode.CHECK ? false : true; - final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, offsetInAllocatedRange); - final Check check = new Check(Spec.MEMORY_DEREFERENCE); - check.annotate(spec); - return Collections.singletonList(spec); + return ExpressionFactory.newBinaryExpression(loc, BinaryExpression.Operator.LOGICAND, leq, offsetGeqZero); } /** @@ -246,15 +186,11 @@ private Expression constructPointerBinaryComparisonExpression(final ILocation lo } @Override - public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { assert pointerToBeFreed.getCType().getUnderlyingType() instanceof CPointer; - if (!isPointerCheckRequired) { - return Collections.emptyList(); - } - final var cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); final Expression zeroNumericExpr = @@ -269,7 +205,7 @@ public List getChecksForFreeCall(final ILocation loc, final RValue po final Expression addrBase = mMemoryPointer.getPointerAddress(pointerToBeFreed.getValue(), loc); final Expression[] idcFree = { addrBase }; - final List result = new ArrayList<>(); + final List result = new ArrayList<>(); /* * creating the specification according to C99:7.20.3.2-2: The free function causes the space pointed to by ptr @@ -278,32 +214,27 @@ public List getChecksForFreeCall(final ILocation loc, final RValue po * realloc function, or if the space has been deallocated by a call to free or realloc, the behavior is * undefined. */ - final Check check = new Check(Spec.MEMORY_FREE); - // assert (~addr!offset == 0); - final AssertStatement offsetZero = new AssertStatement(loc, - ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrOffset, zeroNumericExpr)); - check.annotate(offsetZero); + // ~addr!offset == 0; + final Expression offsetZero = + ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrOffset, zeroNumericExpr); result.add(offsetZero); // assert (~addr!base < #StackHeapBarrier); final Expression inHeapArea = mExpressionTranslation.constructBinaryComparisonIntegerExpression(loc, IASTBinaryExpression.op_lessThan, addrBase, cTypeOfPointerComponent, stackHeapBarrier, cTypeOfPointerComponent); - final AssertStatement assertInHeapArea = new AssertStatement(loc, inHeapArea); - check.annotate(assertInHeapArea); - result.add(assertInHeapArea); + result.add(inHeapArea); // ~addr!base == 0 final Expression isNullPtr = ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, addrBase, zeroNumericExpr); - // requires ~addr!base == 0 || #valid[~addr!base]; + // ~addr!base == 0 || #valid[~addr!base]; final Expression addrIsValid = mBooleanArrayHelper .compareWithTrue(ExpressionFactory.constructNestedArrayAccessExpression(loc, valid, idcFree)); - final AssertStatement baseValid = new AssertStatement(loc, - ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, isNullPtr, addrIsValid)); - check.annotate(baseValid); + final Expression baseValid = + ExpressionFactory.newBinaryExpression(loc, Operator.LOGICOR, isNullPtr, addrIsValid); result.add(baseValid); return result; @@ -324,7 +255,6 @@ public Expression constructFunctionPointer(final ILocation loc, final BigInteger mTypeSizeAndOffsetComputer.getSizeT(), integerExpr, mTypeSizeAndOffsetComputer.getSizeT()); return mMemoryPointer.constructPointerFromBaseAndOffset(baseExpr, offsetMinus, loc); - } @Override @@ -339,17 +269,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryPointer.constructPointerFromBaseAndOffset(base, offsetPlus, loc); } - @Override - public Expression getLastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, - IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len), sizeT, - mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); - - return mMemoryPointer.constructPointerFromBaseAndOffset(mMemoryPointer.getPointerAddress(returnValue, loc), - lenMinusOne, loc); - } - @Override public AssumeStatement constructStrChrAssumeStatement(final ILocation loc, final Expression tmpExpr, final Expression argSPtr, final Expression nullPtrExpr, @@ -403,64 +322,6 @@ public Expression constructInitialPointerFromPointer(final ILocation loc, final return mMemoryPointer.constructPointerFromBaseAndOffset(mMemoryPointer.getPointerAddress(ptr, loc), zero, loc); } - @Override - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - final List result = new ArrayList<>(); - - if (pointerBaseValid != CheckMode.IGNORE) { - - // valid[s.base] - final Expression validBase = constructPointerValidityCheckExpr(loc, ptr, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - final var stmt = statementDependentOnCheck(loc, pointerBaseValid, validBase); - result.add(stmt); - } - - if (pointerTargetFullyAllocated != CheckMode.IGNORE) { - // s.offset < length[s.base]) - final Expression ptrOffset = mMemoryPointer.pointerOffset(ptr, loc); - final Expression ptrBase = mMemoryPointer.getPointerAddress(ptr, loc); - - final Expression lengthArray = MemoryMetadataDefault2D.getLengthArray(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); - - final Expression aae = ExpressionFactory.constructNestedArrayAccessExpression(loc, lengthArray, - new Expression[] { ptrBase }); - - final Expression offsetSmallerLength = - constructPointerBinaryComparisonExpression(loc, IASTBinaryExpression.op_lessThan, ptrOffset, aae); - - // s.offset >= 0; - final var zeroExpr = mTypeSizes.constructLiteralForIntegerType(loc, - mExpressionTranslation.getCTypeOfPointerComponents(), BigInteger.ZERO); - - final Expression offsetNonnegative = constructPointerBinaryComparisonExpression(loc, - IASTBinaryExpression.op_greaterEqual, ptrOffset, zeroExpr); - - final Expression aAndB = ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, offsetSmallerLength, - offsetNonnegative); - - final var stmt = statementDependentOnCheck(loc, pointerTargetFullyAllocated, aAndB); - result.add(stmt); - } - return result; - } - - private static Statement statementDependentOnCheck(final ILocation loc, final CheckMode check, - final Expression expr) { - if (check == CheckMode.CHECK) { - final AssertStatement assertion = new AssertStatement(loc, expr); - final Check chk = new Check(Spec.MEMORY_DEREFERENCE); - chk.annotate(assertion); - return assertion; - } - assert check == CheckMode.ASSUME : "missed a case?"; - return new AssumeStatement(loc, expr); - } - @Override public Statement checksForStringCopyOverlapping(final ILocation loc, final Expression src, final Expression srcId, final Expression destId, final Expression dest) { @@ -530,8 +391,12 @@ public Expression constructPointerValidityCheckExpr(final ILocation loc, final E } @Override - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return MemoryMetadataDefault2D.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + final Expression validArray = + MemoryMetadataDefault2D.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, validArray, + ExpressionFactory.constructUnaryExpression(loc, UnaryExpression.Operator.OLD, validArray)); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java index 81c8f8755ad..d7062b2fa98 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAdressingBase.java @@ -27,20 +27,17 @@ package de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler; import java.math.BigInteger; -import java.util.Collections; import java.util.List; -import java.util.Set; import org.eclipse.cdt.core.dom.ast.IASTBinaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.ExpressionTranslation; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.IPointerIntegerConversion; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.expressiontranslation.NonBijectiveMapping1D; @@ -54,10 +51,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.PointerIntegerConversion; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * Abstract base class for implementing specific memory addressing schemes based on a memory pointer representation. @@ -114,9 +108,6 @@ yield new OverapproximationUF2D(exprTranslation, functionDeclarations, typeHandl } else { throw new UnsupportedOperationException("Unknown pointer type " + mMemoryPointer.getClass()); } - default: - throw new UnsupportedOperationException( - "Pointer-Integer conversion not yet implemented " + pointerIntegerMode); }; } @@ -141,35 +132,35 @@ private Expression calculateSizeOf(final ILocation loc, final ICType cType) { } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructMallocSpecificationExpressions(tuLoc, memoryArea, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryManagementStrategy.constructMallocSpecification(tuLoc, memoryArea, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructDeallocSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, + return mMemoryManagementStrategy.constructDeallocSpecification(tuLoc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } @Override - public List constructUltimateInitStatements(final ILocation loc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { - return mMemoryManagementStrategy.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler, fixedAddressCounter); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + return mMemoryManagementStrategy.constructAllocInitSpecification(tuLoc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public List constructUltimateInitStatements(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryManagementStrategy.constructAllocInitSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { + return mMemoryManagementStrategy.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler, fixedAddressCounter); } @Override @@ -210,60 +201,34 @@ public Expression[] constructRhsAssignmentStatementHda(final ILocation loc, fina } @Override - public List constructPointerValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, + public Expression constructPointerValidityCheckExpr(final ILocation loc, final Expression ptr, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException("The pointer base validity check is not compatible with the selected: " + this.getClass() + " addressing mode!"); } @Override - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (mode == CheckMode.IGNORE) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException( "The target pointer fully allocated check is not compatible with the selected: " + this.getClass() - + " " + "addressing mode!"); + + " addressing mode!"); } @Override - public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { assert pointerToBeFreed.getCType().getUnderlyingType() instanceof CPointer; - if (!isPointerCheckRequired) { - return Collections.emptyList(); - } - throw new UnsupportedOperationException( "The check if the freed pointer is valid is not compatible with the selected: " + this.getClass() + " addressing mode!"); } - @Override - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - if (pointerBaseValid == CheckMode.IGNORE && pointerTargetFullyAllocated == CheckMode.IGNORE) { - return Collections.emptyList(); - } - - throw new UnsupportedOperationException( - "The MemSafety checks are not compatible with the selected: " + this.getClass() + " addressing mode!"); - } - @Override public Statement checksForStringCopyOverlapping(final ILocation loc, final Expression src, final Expression srcId, final Expression destId, final Expression dest) { @@ -272,6 +237,14 @@ public Statement checksForStringCopyOverlapping(final ILocation loc, final Expre + " addressing mode!"); } + @Override + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + throw new UnsupportedOperationException("The check for memory neutrality is not compatible with the selected: " + + this.getClass() + " addressing mode!"); + } + /** * Creates a valid expression representing a pointer subtractions of a pointer component. The component is either * base or offset. diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java index a82d9d54f19..5cee2d393f3 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryHandler.java @@ -55,6 +55,7 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.ASTType; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayLHS; import de.uni_freiburg.informatik.ultimate.boogie.ast.ArrayType; +import de.uni_freiburg.informatik.ultimate.boogie.ast.AssertStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.AtomicStatement; @@ -74,10 +75,10 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.NamedAttribute; import de.uni_freiburg.informatik.ultimate.boogie.ast.Procedure; import de.uni_freiburg.informatik.ultimate.boogie.ast.QuantifierExpression; +import de.uni_freiburg.informatik.ultimate.boogie.ast.RequiresSpecification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.StructAccessExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.StructConstructor; import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VarList; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableDeclaration; @@ -94,6 +95,7 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.DataRaceChecker; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.FunctionDeclarations; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.TranslationSettings; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.MemoryStructureBase.ReadWriteDefinition; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.memoryhandler.ConstructMemcpyOrMemmove; @@ -121,12 +123,14 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.INameHandler; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; +import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Check; import de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Overapprox; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; +import de.uni_freiburg.informatik.ultimate.core.model.models.annotation.Spec; +import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.MemoryStructure; import de.uni_freiburg.informatik.ultimate.util.datastructures.LinkedScopedHashMap; import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * @author Markus Lindenmann @@ -298,8 +302,8 @@ public List declareMemoryStructureInfrastructure(final CHandler mai declarations .add(constructMemoryArrayDeclaration(tuLoc, heapDataArray.getName(), heapDataArray.getASTType())); // create and add read and write procedure - declarations.addAll(constructWriteProcedures(main, tuLoc, heapDataArrays, heapDataArray)); - declarations.addAll(constructReadProcedures(main, tuLoc, heapDataArray)); + constructWriteProcedures(main, tuLoc, heapDataArrays, heapDataArray); + constructReadProcedures(main, tuLoc, heapDataArray); } // add store function (to be able to assign subarrays at pointer base addresses) @@ -324,11 +328,11 @@ public List declareMemoryStructureInfrastructure(final CHandler mai declareDataOnHeapInitFunction(mMemoryModel.getPointerHeapArray()); } - declarations.addAll(declareDeallocation(main, tuLoc)); + declareDeallocation(main, tuLoc); if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() .contains(MemoryModelDeclarations.ULTIMATE_ALLOC_STACK)) { - declarations.addAll(declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.STACK)); + declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.STACK); } if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() @@ -338,7 +342,7 @@ public List declareMemoryStructureInfrastructure(final CHandler mai if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() .contains(MemoryModelDeclarations.ULTIMATE_ALLOC_HEAP)) { - declarations.addAll(declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.HEAP)); + declareMalloc(main, mTypeHandler, tuLoc, MemoryArea.HEAP); } if (mRequiredMemoryModelFeatures.getRequiredMemoryStructureDeclarations() @@ -508,12 +512,12 @@ public static AssignmentStatement constructOneDimensionalArrayUpdate(final ILoca } /** - * @param loc - * location of translation unit - * @return new IdentifierExpression that represents the #valid array + * Constructs a boolean expression that, when evaluated at the end of a procedure invocation, results in + * {@code true} iff no memory is allocated that was not already allocated at the beginning of the invocation. */ - public Expression getValidArray(final ILocation loc) { - return mMemoryModel.getValidArray(loc, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc) { + return mMemoryModel.constructMemoryNeutralityCheckExpr(loc, mRequiredMemoryModelFeatures, + mMemoryModelDeclarationsHandler); } public Expression getMemoryRaceArray(final ILocation loc) { @@ -528,9 +532,22 @@ public VariableLHS getMemoryRaceArrayLhs(final ILocation loc) { mMemoryModelDeclarationsHandler); } - public Collection getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed) { - return mMemoryModel.getChecksForFreeCall(loc, pointerToBeFreed, mSettings.checkIfFreedPointerIsValid(), + public List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed) { + if (!mSettings.checkIfFreedPointerIsValid()) { + return Collections.emptyList(); + } + + final List checkExpressions = mMemoryModel.getChecksForFreeCall(loc, pointerToBeFreed, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + final List statements = + checkExpressions.stream(). map(expr -> new AssertStatement(loc, expr)).toList(); + + final Check check = new Check(Spec.MEMORY_FREE); + for (final Statement stmt : statements) { + check.annotate(stmt); + } + + return statements; } /** @@ -663,9 +680,9 @@ public ExpressionResult getReadCall(final Expression address, final ICType resul * the address to read from. * @param resultType * the CType of the pointer - * @return an ExpressionResult consisting only of a array access to the memory array. + * @return an array access to the memory array. */ - public ExpressionResult getReadUnchecked(final Expression address, final ICType resultType) { + public Expression getReadUnchecked(final Expression address, final ICType resultType) { final int byteSize; if (resultType instanceof CPointer) { byteSize = mTypeSizes.getSizeOfPointer(); @@ -675,8 +692,7 @@ public ExpressionResult getReadUnchecked(final Expression address, final ICType throw new AssertionError("We only support reading primitive or pointer types"); } final ILocation loc = address.getLocation(); - return new ExpressionResult(new RValue( - readFromHeap(loc, determineMemoryArrayForType(resultType), address, resultType, byteSize), resultType)); + return readFromHeap(loc, determineMemoryArrayForType(resultType), address, resultType, byteSize); } private String determineReadProcedure(final ICType resultType, final ILocation loc) throws AssertionError { @@ -848,8 +864,11 @@ public ExpressionResult doPointerArithmeticWithConversion(final int operator, fi } public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive type) { - return mMemoryModel.constructAddressForStructField(loc, baseAddress, fieldOffset, type); + final Offset fieldOffset) { + if (fieldOffset.isBitfieldOffset()) { + throw new UnsupportedOperationException("Bitfield read"); + } + return mMemoryModel.addExpressionToPointer(loc, baseAddress, fieldOffset.getAddressOffsetAsExpression(loc)); } public void beginScope() { @@ -908,9 +927,8 @@ public void requireMemoryModelFeature(final MemoryModelDeclarations mmDecl) { * caution or improve this method. */ public boolean isNullPointerLiteral(final Expression expr) { - - if (expr instanceof StructConstructor) { - return mMemoryPointer.isNullPointer(expr); + if (mMemoryPointer.isNullPointer(expr)) { + return true; } final BigInteger integerValue = mTypeSizes.extractIntegerValue(expr, new CPrimitive(CPrimitives.LONG)); @@ -1427,26 +1445,19 @@ private VariableDeclaration constructDeclOfPointerIndexedArray(final ILocation l return new VariableDeclaration(loc, new Attribute[0], new VarList[] { varList }); } - private List constructWriteProcedures(final CHandler main, final ILocation loc, + private void constructWriteProcedures(final CHandler main, final ILocation loc, final Collection heapDataArrays, final HeapDataArray heapDataArray) { - final List result = new ArrayList<>(); for (final ReadWriteDefinition rda : mMemoryModel.getReadWriteDefinitionForHeapDataArray(heapDataArray, mRequiredMemoryModelFeatures)) { - final Collection writeDeclaration = - constructWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda); - result.addAll(writeDeclaration); + constructWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda); } - return result; } - private List constructReadProcedures(final CHandler main, final ILocation loc, - final HeapDataArray heapDataArray) { - final List result = new ArrayList<>(); + private void constructReadProcedures(final CHandler main, final ILocation loc, final HeapDataArray heapDataArray) { for (final ReadWriteDefinition rda : mMemoryModel.getReadWriteDefinitionForHeapDataArray(heapDataArray, mRequiredMemoryModelFeatures)) { - result.addAll(constructSingleReadProcedure(main, loc, heapDataArray, rda)); + constructSingleReadProcedure(main, loc, heapDataArray, rda); } - return result; } private VariableDeclaration declarePthreadsForkCount(final ILocation loc) { @@ -1481,7 +1492,7 @@ private VariableDeclaration declarePthreadRwLock(final ILocation loc) { * @param rda * @return */ - private Collection constructWriteProcedure(final CHandler main, final ILocation loc, + private void constructWriteProcedure(final CHandler main, final ILocation loc, final Collection heapDataArrays, final HeapDataArray heapDataArray, final ReadWriteDefinition rda) { if (rda.alsoUncheckedWrite()) { @@ -1491,7 +1502,6 @@ private Collection constructWriteProcedure(final CHandler main, final constructSingleWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda, HeapWriteMode.SELECT); } constructSingleWriteProcedure(main, loc, heapDataArrays, heapDataArray, rda, HeapWriteMode.STORE_CHECKED); - return Collections.emptySet(); } private void constructSingleWriteProcedure(final CHandler main, final ILocation loc, @@ -1653,8 +1663,8 @@ private static List constructConjunctsForWriteEnsuresSpecification(f * whether we should construct an unchecked read procedure (i.e. one that omits validity checks) * @return */ - private List constructSingleReadProcedure(final CHandler main, final ILocation loc, - final HeapDataArray hda, final ReadWriteDefinition rda) { + private void constructSingleReadProcedure(final CHandler main, final ILocation loc, final HeapDataArray hda, + final ReadWriteDefinition rda) { // specification for memory reads final String returnValue = "#value"; final ASTType valueAstType = rda.getASTType(); @@ -1700,8 +1710,6 @@ private List constructSingleReadProcedure(final CHandler main, final mProcedureManager.addSpecificationsToCurrentProcedure(sread); mProcedureManager.endCustomProcedure(main, readProcedureName); - - return Collections.emptyList(); } private Expression readFromHeap(final ILocation loc, final HeapDataArray hda, final Expression address, @@ -1754,13 +1762,13 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p * memory at the base address of the pointer. Furthermore, we check that the offset is greater than or equal to * zero. * - * In case mPointerBaseValidity is CHECK, we construct the requires specification + * In case {@code mSettings.checkPointerDerefValidity()} is CHECK, we construct the requires specification * requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). * - * In case mPointerBaseValidity is CHECK, we construct the free requires specification - * free requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). + * In case {@code mSettings.checkPointerDerefValidity()} is ASSUME, we construct the free requires + * specification free requires (#size + #ptr!offset <= #length[#ptr!base] && 0 <= #ptr!offset). * - * In case mPointerBaseValidity is IGNORE, we construct nothing. + * In case {@code mSettings.checkPointerDerefValidity()} is IGNORE, we construct nothing. * * @param loc * location of translation unit @@ -1772,17 +1780,36 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p */ public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, final String ptrName, final String procedureName) { - return mMemoryModel.constructPointerTargetFullyAllocatedCheck(loc, size, ptrName, procedureName, - mSettings.checkPointerDerefValidity(), mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } + + final Expression ptrExpr = + ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, + new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); + + final Expression offsetInAllocatedRange = mMemoryModel.constructPointerTargetFullyAllocatedCheckExpr(loc, + ptrExpr, size, mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + + final boolean isFreeRequires = mode == CheckMode.ASSUME; + final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, offsetInAllocatedRange); + final Check check = new Check(Spec.MEMORY_DEREFERENCE); + check.annotate(spec); + return Collections.singletonList(spec); } /** - * Construct specification that the pointer base address is valid. In case - * {@link #getPointerBaseValidityCheckMode()} is ASSERTandASSUME, we add the requires specification - * requires #valid[#ptr!base]. In case {@link #getPointerBaseValidityCheckMode()} is ASSERTandASSUME, - * we add the free requires specification free requires #valid[#ptr!base]. In case - * {@link #getPointerBaseValidityCheckMode()} is IGNORE, we add nothing. + * Construct specification that the pointer base address is valid. + * + * In case {@code mSettings.checkPointerDerefValidity()} is CHECK, we add the requires specification + * requires #valid[#ptr!base]. + * + * In case {@code mSettings.checkPointerDerefValidity()} is ASSUME, we add the free requires specification + * free requires #valid[#ptr!base]. + * + * In case {@code mSettings.checkPointerDerefValidity()} is IGNORE, we add nothing. * * @param loc * location of translation unit @@ -1794,21 +1821,24 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca */ public List constructPointerBaseValidityCheck(final ILocation loc, final String ptrName, final String procedureName) { - return mMemoryModel.constructPointerBaseValidityCheck(loc, ptrName, procedureName, - mSettings.checkPointerDerefValidity(), mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); - } + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } - /** - * Compare a pointer component (base or offset) to another expression. - * - * @param op - * One of the comparison operators defined in {@link IASTBinaryExpression}. - */ - private Expression constructPointerBinaryComparisonExpression(final ILocation loc, final int op, - final Expression left, final Expression right) { - return mExpressionTranslation.constructBinaryComparisonExpression(loc, op, left, - mExpressionTranslation.getCTypeOfPointerComponents(), right, - mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression ptrExpr = + ExpressionFactory.constructIdentifierExpression(loc, mTypeHandler.getBoogiePointerType(), ptrName, + new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureName)); + + final Expression isValid = mMemoryModel.constructPointerBaseValidityCheckExpr(loc, ptrExpr, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + + final boolean isFreeRequires = mode == CheckMode.ASSUME; + + final RequiresSpecification spec = new RequiresSpecification(loc, isFreeRequires, isValid); + final Check check = new Check(Spec.MEMORY_DEREFERENCE); + check.annotate(spec); + return Collections.singletonList(spec); } /** @@ -1821,8 +1851,7 @@ private Expression constructPointerBinaryComparisonExpression(final ILocation lo * * @return declaration and implementation of procedure Ultimate_dealloc */ - private List declareDeallocation(final CHandler main, final ILocation tuLoc) { - + private void declareDeallocation(final CHandler main, final ILocation tuLoc) { final Procedure deallocDeclaration = new Procedure(tuLoc, new Attribute[0], MemoryModelDeclarations.ULTIMATE_DEALLOC.getName(), new String[0], new VarList[] { @@ -1831,20 +1860,12 @@ private List declareDeallocation(final CHandler main, final ILocati mProcedureManager.beginCustomProcedure(main, tuLoc, MemoryModelDeclarations.ULTIMATE_DEALLOC.getName(), deallocDeclaration); - final List, Boolean>> deallocSpecificationExpressions = - mMemoryModel.constructDeallocSpecificationExpressions(tuLoc, mRequiredMemoryModelFeatures, - mMemoryModelDeclarationsHandler); - - final List deallocSpecifications = new ArrayList<>(); - - for (final Triple, Boolean> triple : deallocSpecificationExpressions) { - deallocSpecifications.add(mProcedureManager.constructEnsuresSpecification(tuLoc, triple.getThird(), - triple.getFirst(), triple.getSecond())); - } + final AllocationProcedureSpec specification = mMemoryModel.constructDeallocSpecification(tuLoc, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - mProcedureManager.addSpecificationsToCurrentProcedure(deallocSpecifications); mProcedureManager.endCustomProcedure(main, MemoryModelDeclarations.ULTIMATE_DEALLOC.getName()); - return Collections.emptyList(); } /** @@ -1857,8 +1878,8 @@ private List declareDeallocation(final CHandler main, final ILocati * * @return declaration and implementation of procedure ~malloc */ - private ArrayList declareMalloc(final CHandler main, final ITypeHandler typeHandler, - final ILocation tuLoc, final MemoryArea memArea) { + private void declareMalloc(final CHandler main, final ITypeHandler typeHandler, final ILocation tuLoc, + final MemoryArea memArea) { final MemoryModelDeclarations alloc = memArea.getMemoryStructureDeclaration(); final ASTType intType = typeHandler.cType2AstType(tuLoc, mExpressionTranslation.getCTypeOfPointerComponents()); final Procedure allocDeclaration = new Procedure(tuLoc, new Attribute[0], alloc.getName(), new String[0], @@ -1868,22 +1889,12 @@ private ArrayList declareMalloc(final CHandler main, final ITypeHan mProcedureManager.beginCustomProcedure(main, tuLoc, alloc.getName(), allocDeclaration); - final List>> mallocSpecificationExpressions = - mMemoryModel.constructMallocSpecificationExpressions(tuLoc, memArea, mRequiredMemoryModelFeatures, - mMemoryModelDeclarationsHandler); - - final List mallocSpecifications = new ArrayList<>(); - - for (final Pair> pair : mallocSpecificationExpressions) { - mallocSpecifications.add( - mProcedureManager.constructEnsuresSpecification(tuLoc, false, pair.getFirst(), pair.getSecond())); - } - - mProcedureManager.addSpecificationsToCurrentProcedure(mallocSpecifications); + final AllocationProcedureSpec specification = mMemoryModel.constructMallocSpecification(tuLoc, memArea, + mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - final ArrayList result = new ArrayList<>(); mProcedureManager.endCustomProcedure(main, alloc.getName()); - return result; } /** @@ -1893,26 +1904,19 @@ private ArrayList declareMalloc(final CHandler main, final ITypeHan */ private void declareAllocInit(final CHandler main, final ITypeHandler typeHandler, final ILocation tuLoc) { final String procedureIdentifier = MemoryModelDeclarations.ULTIMATE_ALLOC_INIT.getName(); - final String pointerBaseIdentifier = "ptrBase"; final ASTType intType = typeHandler.cType2AstType(tuLoc, mExpressionTranslation.getCTypeOfPointerComponents()); final Procedure allocDeclaration = new Procedure(tuLoc, new Attribute[0], procedureIdentifier, new String[0], - new VarList[] { new VarList(tuLoc, new String[] { SFO.SIZE, pointerBaseIdentifier }, intType) }, + new VarList[] { new VarList(tuLoc, new String[] { SFO.SIZE, SFO.ALLOCINIT_PTRBASE }, intType) }, new VarList[0], new Specification[0], null); mProcedureManager.beginCustomProcedure(main, tuLoc, procedureIdentifier, allocDeclaration); - final var allocInitSpecificationExpressions = mMemoryModel.constructAllocInitSpecificationExpressions(tuLoc, + final AllocationProcedureSpec specification = mMemoryModel.constructAllocInitSpecification(tuLoc, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + mProcedureManager.addModifiedGlobalsToCurrentProcedure(specification.modifies()); + mProcedureManager.addSpecificationsToCurrentProcedure(specification.constructSpecificationClauses(tuLoc)); - final List allocInitSpecifications = new ArrayList<>(); - - for (final Pair> pair : allocInitSpecificationExpressions) { - allocInitSpecifications.add( - mProcedureManager.constructEnsuresSpecification(tuLoc, false, pair.getFirst(), pair.getSecond())); - } - - mProcedureManager.addSpecificationsToCurrentProcedure(allocInitSpecifications); mProcedureManager.endCustomProcedure(main, procedureIdentifier); } @@ -1987,8 +1991,7 @@ private List getWriteCallStruct(final ILocation loc, final HeapLValue throw new UnsupportedOperationException("Bitfield write"); } - final Expression newPointer = mMemoryModel.constructAddressForStructField(loc, startAddress, fieldOffset, - mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression newPointer = constructAddressForStructField(loc, startAddress, fieldOffset); final HeapLValue fieldHlv = LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, fieldType, null); final StructAccessExpression sae = ExpressionFactory.constructStructAccessExpression(loc, value, fieldId); @@ -2614,14 +2617,41 @@ private Attribute[] constructExpandAndSmtDefinedAttributesForSubArraySelect(fina /** * Construct assert statements that do memsafety checks for {@link pointerValue} if the corresponding settings are - * active. settings concerned are: - "Pointer base address is valid at dereference" - "Pointer to allocated memory - * at dereference" + * active. */ public List constructMemsafetyChecksForPointerExpression(final ILocation loc, final Expression pointerValue) { - return mMemoryModel.constructMemSafeStatementsForPointerExpression(loc, pointerValue, - mSettings.checkPointerDerefValidity(), mSettings.checkPointerDerefValidity(), + final var mode = mSettings.checkPointerDerefValidity(); + if (mode == CheckMode.IGNORE) { + return Collections.emptyList(); + } + + final List result = new ArrayList<>(); + + final Expression validBase = mMemoryModel.constructPointerBaseValidityCheckExpr(loc, pointerValue, mRequiredMemoryModelFeatures, mMemoryModelDeclarationsHandler); + result.add(statementDependentOnCheck(loc, mode, validBase)); + + final Expression zero = mExpressionTranslation.constructLiteralForIntegerType(loc, + mExpressionTranslation.getCTypeOfPointerComponents(), BigInteger.ZERO); + final Expression pointerTargetFullyAllocated = mMemoryModel.constructPointerTargetFullyAllocatedCheckExpr(loc, + pointerValue, zero, mSettings.isBitvectorTranslation(), mRequiredMemoryModelFeatures, + mMemoryModelDeclarationsHandler); + result.add(statementDependentOnCheck(loc, mode, pointerTargetFullyAllocated)); + + return result; + } + + private static Statement statementDependentOnCheck(final ILocation loc, final CheckMode check, + final Expression expr) { + if (check == CheckMode.CHECK) { + final AssertStatement assertion = new AssertStatement(loc, expr); + final Check chk = new Check(Spec.MEMORY_DEREFERENCE); + chk.annotate(assertion); + return assertion; + } + assert check == CheckMode.ASSUME : "missed a case?"; + return new AssumeStatement(loc, expr); } public List ultimateInitStatements(final ILocation loc) { @@ -2643,11 +2673,6 @@ public final Expression createFunctionPointer(final ILocation loc, final BigInte return mMemoryModel.createFunctionPointer(loc, offset); } - public final Expression lastCharOfString(final ILocation loc, final CPrimitive sizeT, - final IdentifierExpression len, final IdentifierExpression returnValue) { - return mMemoryModel.lastCharOfString(loc, sizeT, len, returnValue); - } - public final Expression initialPointerFromPointer(final ILocation loc, final Expression ptr) { return mMemoryModel.initialPointerFromPointer(loc, ptr); } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java index 16332fae28d..fcd23ed7c9d 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryModel.java @@ -29,18 +29,16 @@ import java.math.BigInteger; import java.util.Collection; import java.util.List; -import java.util.Set; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssumeStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; import de.uni_freiburg.informatik.ultimate.boogie.ast.IdentifierExpression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; +import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryManagementStrategy.AllocationProcedureSpec; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.MemoryStructureBase.ReadWriteDefinition; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.TypeSizeAndOffsetComputer.Offset; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitives; @@ -48,9 +46,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.ExpressionResult; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.result.RValue; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator.preferences.CACSLPreferenceInitializer.CheckMode; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * The memory model consisting of a MemoryAdressing and a MemoryStructure. @@ -79,10 +74,6 @@ public String getReadProcedureName(final CPrimitives primitive) { return mMemoryStructure.getReadProcedureName(primitive); } - public String getUncheckedReadProcedureName(final CPrimitives primitive) { - return mMemoryStructure.getUncheckedReadProcedureName(primitive); - } - public String getWriteProcedureName(final CPrimitives primitive) { return mMemoryStructure.getWriteProcedureName(primitive); } @@ -99,10 +90,6 @@ public String getReadPointerProcedureName() { return mMemoryStructure.getReadPointerProcedureName(); } - public String getUncheckedReadPointerProcedureName() { - return mMemoryStructure.getUncheckedReadPointerProcedureName(); - } - public String getWritePointerProcedureName() { return mMemoryStructure.getWritePointerProcedureName(); } @@ -153,53 +140,51 @@ public List metaDataDeclarations() { } /** - * Constructs the expressions used in the specifications for malloc. + * Constructs the specification of malloc. * - * @return A list of a pair consisting of an expression and a set of the global variables that must be added to the - * modifies clause. + * @return a record representing the specification */ - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructMallocSpecificationExpressions(tuLoc, memoryArea, requiredMemoryModelFeatures, + return mMemoryAddressing.constructMallocSpecification(tuLoc, memoryArea, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** - * Constructs the expressions used in the specifications for dealloc. + * Constructs the specification of dealloc. * - * @return A list of a pair consisting of an expression and a set of the global variables that must be added to the - * modifies clause. + * @return a record representing the specification */ - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructDeallocSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, + return mMemoryAddressing.constructDeallocSpecification(tuLoc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** - * Constructs the statements used in Ultimate.Init. + * Constructs the specification of allocInit. * - * @return The statements. + * @return a record representing the specification */ - List constructUltimateInitStatements(final ILocation loc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { - return mMemoryAddressing.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler, fixedAddressCounter); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { + return mMemoryAddressing.constructAllocInitSpecification(tuLoc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } /** - * Constructs the expressions used in the specifications for allocInit. + * Constructs the statements used in Ultimate.Init. * - * @return The expressions. + * @return The statements. */ - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + List constructUltimateInitStatements(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructAllocInitSpecificationExpressions(tuLoc, requiredMemoryModelFeatures, - memoryModelDeclarationsHandler); + final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler, final BigInteger fixedAddressCounter) { + return mMemoryAddressing.constructUltimateInitStatements(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler, fixedAddressCounter); } /** @@ -222,19 +207,6 @@ public BigInteger fixedAddressCounterCountingStep(final Expression size) { return mMemoryAddressing.getFixedAddressCounterCountingStep(size); } - /** - * Returns the address for struct field. - * - * @return The address. - */ - public Expression constructAddressForStructField(final ILocation loc, final Expression baseAddress, - final Offset fieldOffset, final CPrimitive sizeT) { - if (fieldOffset.isBitfieldOffset()) { - throw new UnsupportedOperationException("Bitfield read"); - } - return mMemoryAddressing.constructAddressForStructField(loc, baseAddress, fieldOffset, sizeT); - } - /** * Adds an integer to a pointer. * @@ -245,25 +217,12 @@ public Expression addIntegerConstantToPointer(final ILocation loc, final Express return mMemoryAddressing.addIntegerConstantToPointer(loc, ptrExpr, integerConstant); } - /** - * Constructs the specifications that the pointer base address is valid. - * - * @return The specifications. - */ - public List constructPointerBaseValidityCheck(final ILocation loc, final String ptrName, - final String procedureName, final CheckMode mode, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructPointerValidityCheck(loc, ptrName, procedureName, mode, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); - } - /** * Constructs the pointer base validity check expression. * * @return The expression. */ - Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expression ptr, + public Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expression ptr, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { return mMemoryAddressing.constructPointerValidityCheckExpr(loc, ptr, requiredMemoryModelFeatures, @@ -275,12 +234,12 @@ Expression constructPointerBaseValidityCheckExpr(final ILocation loc, final Expr * * @return The specifications. */ - public List constructPointerTargetFullyAllocatedCheck(final ILocation loc, final Expression size, - final String ptrName, final String procedureName, final CheckMode mode, - final Boolean isBitVectorTranslation, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructPointerTargetFullyAllocatedCheckExpr(final ILocation loc, final Expression ptr, + final Expression size, final boolean isBitVectorTranslation, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructPointerTargetFullyAllocatedCheck(loc, size, ptrName, procedureName, mode, - isBitVectorTranslation, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.constructPointerTargetFullyAllocatedCheckExpr(loc, ptr, size, isBitVectorTranslation, + requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } /** @@ -288,11 +247,11 @@ public List constructPointerTargetFullyAllocatedCheck(final ILoca * * @return The statements. */ - List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, - final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + List getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.getChecksForFreeCall(loc, pointerToBeFreed, isPointerCheckRequired, - requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.getChecksForFreeCall(loc, pointerToBeFreed, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } /** @@ -333,16 +292,6 @@ public Expression addExpressionToPointer(final ILocation loc, final Expression p return mMemoryAddressing.addExpressionToPointer(loc, ptrExpr, expr); } - /** - * Returns a pointer to the last character of a string. - * - * @return The pointer. - */ - public Expression lastCharOfString(final ILocation loc, final CPrimitive sizeT, final IdentifierExpression len, - final IdentifierExpression returnValue) { - return mMemoryAddressing.getLastCharOfString(loc, sizeT, len, returnValue); - } - /** * Returns a pointer with the same base address but an offset of 0. * @@ -365,19 +314,6 @@ public final AssumeStatement strChrAssumeStatement(final ILocation loc, final Ex requiredMemoryModelFeatures, memoryModelDeclarationsHandler); } - /** - * Constructs assert / assume statements for ptr memsafety checks. - * - * @return The statements. - */ - public List constructMemSafeStatementsForPointerExpression(final ILocation loc, final Expression ptr, - final CheckMode pointerBaseValid, final CheckMode pointerTargetFullyAllocated, - final RequiredMemoryModelFeatures requiredMemoryModelFeatures, - final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.constructMemSafeStatementsForPointerExpression(loc, ptr, pointerBaseValid, - pointerTargetFullyAllocated, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); - } - /** * Construct the assume to check that src and dest don't overlap. * @@ -424,9 +360,11 @@ public List constructReallocBodyStatements(final ILocation loc, final memoryModelDeclarationsHandler); } - public Expression getValidArray(final ILocation loc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public Expression constructMemoryNeutralityCheckExpr(final ILocation loc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return mMemoryAddressing.getValidArray(loc, requiredMemoryModelFeatures, memoryModelDeclarationsHandler); + return mMemoryAddressing.constructMemoryNeutralityCheckExpr(loc, requiredMemoryModelFeatures, + memoryModelDeclarationsHandler); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java index 560cd745864..e5d45d359bc 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer1D.java @@ -147,15 +147,10 @@ public Expression constructPointerRelationExpression(final ILocation loc, final final Expression pointerRelation = constructPointerComponentRelation(loc, op, left.getLrValue().getValue(), right.getLrValue().getValue(), SFO.POINTER_BASE, expressionTranslation); - switch (mPointerSubtractionAndComparisonValidityCheckMode) { - case CHECK: - case ASSUME: - return ExpressionFactory.createBooleanLiteral(loc, true); - case IGNORE: - return pointerRelation; - default: - throw new AssertionError("unknown value"); - } + return switch (mPointerSubtractionAndComparisonValidityCheckMode) { + case CHECK, ASSUME -> ExpressionFactory.createBooleanLiteral(loc, true); + case IGNORE -> pointerRelation; + }; } @Override @@ -167,12 +162,8 @@ public Expression constructPointerComponentRelation(final ILocation loc, final i @Override public boolean isNullPointer(final Expression ptr) { - final StructConstructor sc = (StructConstructor) ptr; - if (sc.getFieldValues().length == 1 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) - && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0]))) { - return true; - } - - return false; + return ptr instanceof final StructConstructor sc && sc.getFieldValues().length == 1 + && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java index bbe6fb2d3d3..aede32205db 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryPointer2D.java @@ -118,8 +118,8 @@ public Expression constructInitialPointer(final ILocation loc, final BigInteger * @return The offset. */ public Expression pointerOffset(final Expression pointer, final ILocation loc) { - if (pointer instanceof StructConstructor) { - return ((StructConstructor) pointer).getFieldValues()[1]; + if (pointer instanceof final StructConstructor sc) { + return sc.getFieldValues()[1]; } return ExpressionFactory.constructStructAccessExpression(loc, pointer, SFO.POINTER_OFFSET); } @@ -144,18 +144,13 @@ public Expression constructPointerRelationExpression(final ILocation loc, final final Expression offsetRelation = constructPointerComponentRelation(loc, op, left.getLrValue().getValue(), right.getLrValue().getValue(), SFO.POINTER_OFFSET, expressionTranslation); - switch (mPointerSubtractionAndComparisonValidityCheckMode) { - case CHECK: - case ASSUME: - return offsetRelation; - case IGNORE: - // use conjunction - return ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, baseEquality, offsetRelation); - // TODO: Do not use conjunction. Use nondeterministic value if baseEquality does not hold. - default: - throw new AssertionError("unknown value"); - } + return switch (mPointerSubtractionAndComparisonValidityCheckMode) { + case CHECK, ASSUME -> offsetRelation; + // use conjunction + // TODO: Do not use conjunction. Use nondeterministic value if baseEquality does not hold. + case IGNORE -> ExpressionFactory.newBinaryExpression(loc, Operator.LOGICAND, baseEquality, offsetRelation); + }; } @Override @@ -167,14 +162,10 @@ public Expression constructPointerComponentRelation(final ILocation loc, final i @Override public boolean isNullPointer(final Expression ptr) { - final StructConstructor sc = (StructConstructor) ptr; - if (sc.getFieldValues().length == 2 && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) + return ptr instanceof final StructConstructor sc && sc.getFieldValues().length == 2 + && sc.getFieldIdentifiers()[0].equals(SFO.POINTER_BASE) && sc.getFieldIdentifiers()[1].equals(SFO.POINTER_OFFSET) && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[0])) - && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1]))) { - return true; - } - - return false; + && BigInteger.ZERO.equals(CTranslationUtil.extractIntegerValue(sc.getFieldValues()[1])); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java index 79d209e6079..1bdb38d89e8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureBase.java @@ -74,11 +74,6 @@ public final String getReadProcedureName(final CPrimitives primitive) { return READ_PROCEDURE_PREFIX + getProcedureSuffix(primitive); } - @Override - public final String getUncheckedReadProcedureName(final CPrimitives primitive) { - return READ_PROCEDURE_PREFIX + UNCHECKED_PREFIX + getProcedureSuffix(primitive); - } - @Override public final String getWriteProcedureName(final CPrimitives primitive) { return WRITE_PROCEDURE_PREFIX + getProcedureSuffix(primitive); @@ -100,12 +95,6 @@ public final String getReadPointerProcedureName() { return READ_PROCEDURE_PREFIX + hda.getName(); } - @Override - public final String getUncheckedReadPointerProcedureName() { - final HeapDataArray hda = mPointerArray; - return READ_PROCEDURE_PREFIX + UNCHECKED_PREFIX + hda.getName(); - } - @Override public final String getWritePointerProcedureName() { final HeapDataArray hda = mPointerArray; diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java index d19d62295f6..f977ba3317e 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureFactory.java @@ -52,19 +52,17 @@ public static IMemoryStructure createMemoryStructure(final TranslationSettings s + " is only available in using the bitprecise translation"); } - switch (memoryStructurePreference) { + return switch (memoryStructurePreference) { case HoenickeLindenmann_1ByteResolution: case HoenickeLindenmann_2ByteResolution: case HoenickeLindenmann_4ByteResolution: case HoenickeLindenmann_8ByteResolution: - return new MemoryStructureSingleBitprecise(memoryStructurePreference.getByteSize(), typeSizes, typeHandler); + yield new MemoryStructureSingleBitprecise(memoryStructurePreference.getByteSize(), typeSizes, typeHandler); case HoenickeLindenmann_Original: if (settings.isBitvectorTranslation()) { - return new MemoryStructureMultiBitprecise(typeSizes, typeHandler); + yield new MemoryStructureMultiBitprecise(typeSizes, typeHandler); } - return new MemoryStructureUnbounded(typeSizes, typeHandler); - default: - throw new UnsupportedOperationException(memoryStructurePreference + " is an invalid memory structure."); - } + yield new MemoryStructureUnbounded(typeSizes, typeHandler); + }; } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java index 5a315821897..032c7920a72 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryStructureMultiBitprecise.java @@ -59,16 +59,11 @@ public MemoryStructureMultiBitprecise(final TypeSizes typeSizes, final ITypeHand @Override public HeapDataArray getDataHeapArray(final CPrimitives primitive) { - switch (primitive.getPrimitiveCategory()) { - case FLOATTYPE: - return getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapFloatingArray); - case INTTYPE: - return getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapIntegerArray); - case VOID: - throw new AssertionError("void on the heap???"); - default: - throw new AssertionError("unknown primitive category"); - } + return switch (primitive.getPrimitiveCategory()) { + case FLOATTYPE -> getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapFloatingArray); + case INTTYPE -> getDataHeapArrayForGivenGeneralType(primitive, mSize2HeapIntegerArray); + case VOID -> throw new AssertionError("void on the heap???"); + }; } private HeapDataArray getDataHeapArrayForGivenGeneralType(final CPrimitives primitive, diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java index 86ee52a8ab2..c1786b016fa 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/NonDetStrategy2D.java @@ -53,12 +53,10 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This strategy is the default strategy for the 2D-memory addressing scheme. The generic parameter is used to ensure - * that this strategy is only instanciated within the 2D addressing class because it is not compatible with other modes. + * that this strategy is only instantiated within the 2D addressing class because it is not compatible with other modes. * Memory addresses get a non-deterministic value, which is not used yet. * * @author Jan Körner @@ -77,8 +75,8 @@ public NonDetStrategy2D(final TypeSizes typeSizes, final ExpressionTranslation e } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, - final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var memoryAreaName = memoryArea.getMemoryStructureDeclaration().getName(); @@ -104,7 +102,7 @@ public List>> constructMallocSpecificationExpr final var resBaseExpr = ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE); - final ArrayList>> expressions = new ArrayList<>(); + final ArrayList expressions = new ArrayList<>(); // old(#valid)[#res!base] == false final var freshLocationCurrentlyNotValidExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, @@ -112,32 +110,30 @@ public List>> constructMallocSpecificationExpr ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, validArrayExpr), new Expression[] { resBaseExpr }), falseExpr); - - expressions.add(new Pair<>(freshLocationCurrentlyNotValidExpr, Collections.emptySet())); + expressions.add(freshLocationCurrentlyNotValidExpr); // #valid == old(#valid)[#res!base := true] final var validUpdateExpr = MemoryModelExpressionHelper.ensuresArrayUpdate(tuLoc, trueExpr, resBaseExpr, validArrayExpr); - expressions.add(new Pair<>(validUpdateExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr)))); + expressions.add(validUpdateExpr); // #res!offset == 0 final var offsetEqualZeroExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, mMemoryAddressing.mMemoryPointer.pointerOffset(resultExpr, tuLoc), zeroNumericValueExpr); - expressions.add(new Pair<>(offsetEqualZeroExpr, Collections.emptySet())); + expressions.add(offsetEqualZeroExpr); // #res!base != 0 final var baseNotEqualZeroExpr = baseNotEqualZeroExpr(tuLoc, resultExpr, zeroNumericValueExpr); - expressions.add(new Pair<>(baseNotEqualZeroExpr, Collections.emptySet())); + expressions.add(baseNotEqualZeroExpr); if (memoryArea == MemoryArea.STACK) { // #StackHeapBarrier < res!base final var baseGreaterThanBarrierExpr = baseGreaterThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseGreaterThanBarrierExpr, Collections.emptySet())); + expressions.add(baseGreaterThanBarrierExpr); } else if (memoryArea == MemoryArea.HEAP) { // res!base < #StackHeapBarrier final var baseSmallerThanBarrierExpr = baseSmallerThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseSmallerThanBarrierExpr, Collections.emptySet())); + expressions.add(baseSmallerThanBarrierExpr); } // #length == old(#length)[#res!base := ~size] @@ -148,15 +144,16 @@ public List>> constructMallocSpecificationExpr tuLoc, ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, lengthArrayExpr), new Expression[] { resBaseExpr }, sizeExpr)); - expressions.add(new Pair<>(lengthUpdateExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(lengthArrayExpr)))); + expressions.add(lengthUpdateExpr); - return expressions; + final var validArrayLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr); + final var lengthArrayLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(lengthArrayExpr); + return new AllocationProcedureSpec(expressions, Set.of(validArrayLHS, lengthArrayLHS)); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var falseExpr = mBooleanArrayHelper.constructFalse(); @@ -178,8 +175,8 @@ public List, Boolean>> constructDeallocSpeci final Expression updateValidArrayExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, validArrayExpr, arrayStoreExpr); - return Collections.singletonList(new Triple<>(updateValidArrayExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr)), true)); + return new AllocationProcedureSpec(Collections.emptyList(), List.of(updateValidArrayExpr), + Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(validArrayExpr))); } @Override @@ -236,10 +233,9 @@ public List constructUltimateInitStatements(final ILocation loc, } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - final var pointerBaseIdentifier = "ptrBase"; final var procedureIdentifier = MemoryModelDeclarations.ULTIMATE_ALLOC_INIT.getName(); final var trueExpr = mBooleanArrayHelper.constructTrue(); @@ -251,21 +247,18 @@ public List>> constructAllocInitSpecificationE SFO.SIZE, new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureIdentifier)); final var ptrBase = ExpressionFactory.constructIdentifierExpression(tuLoc, - mTypeHandler.getBoogieTypeForPointerComponents(), pointerBaseIdentifier, + mTypeHandler.getBoogieTypeForPointerComponents(), SFO.ALLOCINIT_PTRBASE, new DeclarationInformation(StorageClass.PROC_FUNC_INPARAM, procedureIdentifier)); - final ArrayList>> expressions = new ArrayList<>(); // ensures #valid[ptrBase] == true; final var validPtrBaseExpr = MemoryModelExpressionHelper.ensuresArrayHasValue(tuLoc, trueExpr, ptrBase, validArrayExpr); - expressions.add(new Pair<>(validPtrBaseExpr, Collections.emptySet())); // ensures #length[ptrBase] == size; final var lengthPtrBaseSize = MemoryModelExpressionHelper.ensuresArrayHasValue(tuLoc, size, ptrBase, lengthArrayExpr); - expressions.add(new Pair<>(lengthPtrBaseSize, Collections.emptySet())); - return expressions; + return new AllocationProcedureSpec(List.of(validPtrBaseExpr, lengthPtrBaseSize), Collections.emptySet()); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java index 3c0997209ab..64a68a9fbbf 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/ProcedureManager.java @@ -44,9 +44,7 @@ import java.util.stream.Collectors; import de.uni_freiburg.informatik.ultimate.boogie.BoogieVisitor; -import de.uni_freiburg.informatik.ultimate.boogie.ExpressionFactory; import de.uni_freiburg.informatik.ultimate.boogie.ast.AssignmentStatement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.BinaryExpression.Operator; import de.uni_freiburg.informatik.ultimate.boogie.ast.Body; import de.uni_freiburg.informatik.ultimate.boogie.ast.CallStatement; import de.uni_freiburg.informatik.ultimate.boogie.ast.Declaration; @@ -58,7 +56,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.ast.Procedure; import de.uni_freiburg.informatik.ultimate.boogie.ast.Specification; import de.uni_freiburg.informatik.ultimate.boogie.ast.Statement; -import de.uni_freiburg.informatik.ultimate.boogie.ast.UnaryExpression; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableDeclaration; import de.uni_freiburg.informatik.ultimate.boogie.ast.VariableLHS; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.CACSLLocation; @@ -220,14 +217,13 @@ public List computeFinalProcedureDeclarations(final MemoryHandler m // model is required. Maybe we can require the memory model if the list of functions for which we // check memory neutrality is not empty. - final Expression vIe = memoryHandler.getValidArray(loc); + final Expression neutrality = memoryHandler.constructMemoryNeutralityCheckExpr(loc); + final int nrSpec = newSpec.length; final Check check = new Check(Spec.MEMORY_NEUTRAL); final ILocation ensLoc = LocationFactory.createLocation(loc); newSpecWithExtraEnsuresClauses = Arrays.copyOf(newSpec, nrSpec + 1); - newSpecWithExtraEnsuresClauses[nrSpec] = new EnsuresSpecification(ensLoc, false, - ExpressionFactory.newBinaryExpression(loc, Operator.COMPEQ, vIe, - ExpressionFactory.constructUnaryExpression(loc, UnaryExpression.Operator.OLD, vIe))); + newSpecWithExtraEnsuresClauses[nrSpec] = new EnsuresSpecification(ensLoc, false, neutrality); check.annotate(newSpecWithExtraEnsuresClauses[nrSpec]); if (mSettings.isSvcompMemtrackCompatibilityMode()) { new Overapprox(Collections.singletonMap("memtrack", ensLoc)) @@ -457,7 +453,11 @@ public EnsuresSpecification constructEnsuresSpecification(final ILocation loc, f return new EnsuresSpecification(loc, isFree, formula); } - public void addSpecificationsToCurrentProcedure(final List specs) { + public void addModifiedGlobalsToCurrentProcedure(final Set modifiedGlobals) { + mCurrentProcedureInfo.addModifiedGlobals(modifiedGlobals); + } + + public void addSpecificationsToCurrentProcedure(final List specs) { assert !isGlobalScope(); final BoogieProcedureInfo procInfo = mCurrentProcedureInfo; final Procedure oldDecl = procInfo.getDeclaration(); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java index 2c729184ad5..268da36d803 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/SimpleIncreasingStrategy.java @@ -48,8 +48,6 @@ import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.util.SFO; import de.uni_freiburg.informatik.ultimate.cdt.translation.interfaces.handler.ITypeHandler; import de.uni_freiburg.informatik.ultimate.core.model.models.ILocation; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Pair; -import de.uni_freiburg.informatik.ultimate.util.datastructures.relation.Triple; /** * This strategy is the default strategy for the 1D-memory addressing scheme. The generic parameter is used to ensure @@ -69,12 +67,12 @@ public SimpleIncreasingStrategy(final TypeSizes typeSizes, final ExpressionTrans } @Override - public List>> constructMallocSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructMallocSpecification(final ILocation tuLoc, final MemoryArea memoryArea, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { final var cTypeOfPointerComponent = mExpressionTranslation.getCTypeOfPointerComponents(); - final ArrayList>> expressions = new ArrayList<>(); + final ArrayList expressions = new ArrayList<>(); final var memoryAreaName = memoryArea.getMemoryStructureDeclaration().getName(); final var zeroNumericValueExpr = @@ -104,7 +102,7 @@ public List>> constructMallocSpecificationExpr // #res!base == old(counterExpression); final var baseEqualCounterExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, resBaseExpr, ExpressionFactory.constructUnaryExpression(tuLoc, UnaryExpression.Operator.OLD, counterExpression)); - expressions.add(new Pair<>(baseEqualCounterExpr, Collections.emptySet())); + expressions.add(baseEqualCounterExpr); // #res!base > 0; final var baseGreaterZeroExpr = mExpressionTranslation.constructBinaryComparisonIntegerExpression(tuLoc, @@ -112,18 +110,18 @@ public List>> constructMallocSpecificationExpr ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE), cTypeOfPointerComponent, zeroNumericValueExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(baseGreaterZeroExpr, Collections.emptySet())); + expressions.add(baseGreaterZeroExpr); if (memoryArea == MemoryArea.STACK) { // res!base > #StackHeapBarrier final var baseGreaterThanBarrierExpr = baseGreaterThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseGreaterThanBarrierExpr, Collections.emptySet())); + expressions.add(baseGreaterThanBarrierExpr); // #StackAllocations > #StackHeapBarrier; final var stackAllocationsGreaterThanBarrier = mExpressionTranslation .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_greaterThan, counterExpression, cTypeOfPointerComponent, stackHeapBarrierExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsGreaterThanBarrier, Collections.emptySet())); + expressions.add(stackAllocationsGreaterThanBarrier); // #StackAllocations < #32-bit max / 64-bit max if (mIsBitVectorTranslation) { @@ -139,19 +137,19 @@ public List>> constructMallocSpecificationExpr .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_lessThan, counterExpression, cTypeOfPointerComponent, maxExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsSmallerThanMax, Collections.emptySet())); + expressions.add(stackAllocationsSmallerThanMax); } } else if (memoryArea == MemoryArea.HEAP) { // res!base < #StackHeapBarrier final var baseSmallerThanBarrierExpr = baseSmallerThanBarrier(tuLoc, stackHeapBarrierExpr, resultExpr); - expressions.add(new Pair<>(baseSmallerThanBarrierExpr, Collections.emptySet())); + expressions.add(baseSmallerThanBarrierExpr); // #HeapAllocations < #StackHeapBarrier; final var stackAllocationsGreaterThanBarrier = mExpressionTranslation .constructBinaryComparisonIntegerExpression(tuLoc, IASTBinaryExpression.op_lessThan, counterExpression, cTypeOfPointerComponent, stackHeapBarrierExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(stackAllocationsGreaterThanBarrier, Collections.emptySet())); + expressions.add(stackAllocationsGreaterThanBarrier); } // res!base > #InitialAllocation @@ -159,7 +157,7 @@ public List>> constructMallocSpecificationExpr tuLoc, IASTBinaryExpression.op_greaterThan, ExpressionFactory.constructStructAccessExpression(tuLoc, resultExpr, SFO.POINTER_BASE), cTypeOfPointerComponent, initialAllocCounterExpr, cTypeOfPointerComponent); - expressions.add(new Pair<>(baseGreaterThanInitialAllocsExpr, Collections.emptySet())); + expressions.add(baseGreaterThanInitialAllocsExpr); // StackAllocations == old(StackAllocations) + ~size // HeapAllocations == old(HeapAllocations) + ~size @@ -169,18 +167,17 @@ public List>> constructMallocSpecificationExpr oldExpr, cTypeOfPointerComponent, sizeExpr, mTypeSizeAndOffsetComputer.getSizeT()); final var counterUpdateValueExpr = ExpressionFactory.newBinaryExpression(tuLoc, Operator.COMPEQ, counterExpression, sumExpr); + expressions.add(counterUpdateValueExpr); - expressions.add(new Pair<>(counterUpdateValueExpr, - Collections.singleton((VariableLHS) CTranslationUtil.convertExpressionToLHS(counterExpression)))); - - return expressions; + final var counterLHS = (VariableLHS) CTranslationUtil.convertExpressionToLHS(counterExpression); + return new AllocationProcedureSpec(expressions, Set.of(counterLHS)); } @Override - public List, Boolean>> constructDeallocSpecificationExpressions( - final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, + public AllocationProcedureSpec constructDeallocSpecification(final ILocation tuLoc, + final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return Collections.emptyList(); + return new AllocationProcedureSpec(Collections.emptyList(), Collections.emptySet()); } @Override @@ -218,10 +215,10 @@ public List constructUltimateInitStatements(final ILocation loc, } @Override - public List>> constructAllocInitSpecificationExpressions(final ILocation tuLoc, + public AllocationProcedureSpec constructAllocInitSpecification(final ILocation tuLoc, final RequiredMemoryModelFeatures requiredMemoryModelFeatures, final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler) { - return Collections.emptyList(); + return new AllocationProcedureSpec(Collections.emptyList(), Collections.emptySet()); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java index 7b463cd0098..5aac009a694 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/StructHandler.java @@ -130,8 +130,7 @@ public Result handleFieldReference(final IDispatcher main, final ExpressionResul // TODO: different calculations for unions final Expression startAddress = fieldOwnerHlv.getAddress(); - final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, startAddress, fieldOffset, - mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression newPointer = mMemoryHandler.constructAddressForStructField(loc, startAddress, fieldOffset); final BitfieldInformation bi = constructBitfieldInformation(bitfieldWidth); newValue = LRValueFactory.constructHeapLValue(mTypeHandler, newPointer, cFieldType, bi); @@ -197,8 +196,8 @@ private List computeNeighbourFieldsOfUnionField(final ILocatio final Offset fieldOffset = mTypeSizeAndOffsetComputer.constructOffsetForField(loc, foType, neighbourField); - final Expression neighbourFieldAddress = mMemoryHandler.constructAddressForStructField(loc, - unionAddress, fieldOffset, mExpressionTranslation.getCTypeOfPointerComponents()); + final Expression neighbourFieldAddress = + mMemoryHandler.constructAddressForStructField(loc, unionAddress, fieldOffset); builder.setLrValue(LRValueFactory.constructHeapLValue(mTypeHandler, neighbourFieldAddress, foType.getFieldType(neighbourField), null)); @@ -217,11 +216,15 @@ public Result readFieldInTheStructAtAddress(final ILocation loc, final int field final ICType resultType = structType.getFieldTypes()[fieldIndex]; - final ExpressionResult call = unchecked ? mMemoryHandler.getReadUnchecked(newPointer, resultType) - : mMemoryHandler.getReadCall(newPointer, resultType); final ExpressionResultBuilder resultBuilder = new ExpressionResultBuilder(); - resultBuilder.addAllExceptLrValue(call); - resultBuilder.setLrValue(new RValue(call.getLrValue().getValue(), resultType)); + if (unchecked) { + final Expression read = mMemoryHandler.getReadUnchecked(newPointer, resultType); + resultBuilder.setLrValue(new RValue(read, resultType)); + } else { + final ExpressionResult call = mMemoryHandler.getReadCall(newPointer, resultType); + resultBuilder.addAllExceptLrValue(call); + resultBuilder.setLrValue(new RValue(call.getLrValue().getValue(), resultType)); + } return resultBuilder.build(); } @@ -233,8 +236,7 @@ public Expression computeStructFieldAddress(final ILocation loc, final int field } final Offset fieldOffset = mTypeSizeAndOffsetComputer.constructOffsetForField(loc, structType, fieldIndex); - return mMemoryHandler.constructAddressForStructField(loc, address, fieldOffset, - mTypeSizeAndOffsetComputer.getSizeT()); + return mMemoryHandler.constructAddressForStructField(loc, address, fieldOffset); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java index e8d8493d615..07c9c25470c 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizeAndOffsetComputer.java @@ -447,7 +447,7 @@ private interface SizeTValue { Expression asExpression(ILocation loc); } - class SizeTValueInteger implements SizeTValue { + private class SizeTValueInteger implements SizeTValue { private final BigInteger mValue; public SizeTValueInteger(final BigInteger value) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java index 3f831278718..0088684b91b 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/TypeSizes.java @@ -282,8 +282,8 @@ public BigInteger extractIntegerValue(final RValue rval) { } public BigInteger extractIntegerValue(final Expression expr, final ICType cType) { - if (expr instanceof IntegerLiteral) { - final BigInteger value = new BigInteger(((IntegerLiteral) expr).getValue()); + if (expr instanceof final IntegerLiteral intLit) { + final BigInteger value = new BigInteger(intLit.getValue()); final CPrimitive cPrimitive = (CPrimitive) CEnum.replaceEnumWithInt(cType); if (!isUnsigned(cPrimitive)) { return value; @@ -294,8 +294,8 @@ public BigInteger extractIntegerValue(final Expression expr, final ICType cType) final BigInteger maxValuePlusOne = maxValue.add(BigInteger.ONE); return value.mod(maxValuePlusOne); } - if (expr instanceof BitvecLiteral) { - final BigInteger value = new BigInteger(((BitvecLiteral) expr).getValue()); + if (expr instanceof final BitvecLiteral bvLit) { + final BigInteger value = new BigInteger(bvLit.getValue()); final CPrimitive cPrimitive = (CPrimitive) CEnum.replaceEnumWithInt(cType); if (isUnsigned(cPrimitive)) { if (getMinValueOfPrimitiveType(cPrimitive).compareTo(value) > 0) { diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java index da572fa975f..596f6e84e91 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/chandler/memoryhandler/ConstructMemcpyOrMemmove.java @@ -244,14 +244,7 @@ destId, new RValue(loopCtrAux.getExp(), mExpressionTranslation.getCTypeOfPointer for (final CPrimitives cPrim : mMemoryHandler.getRequiredMemoryStructureFeatures() .getDataOnHeapRequired()) { final ICType cPrimType = new CPrimitive(cPrim); - final Expression srcAcc; - { - final ExpressionResult srcAccExpRes = mMemoryHandler.getReadUnchecked(currentSrc, cPrimType); - srcAcc = srcAccExpRes.getLrValue().getValue(); - loopBody.addStatements(srcAccExpRes.getStatements()); - loopBody.addDeclarations(srcAccExpRes.getDeclarations()); - assert srcAccExpRes.getOverapprs().isEmpty(); - } + final Expression srcAcc = mMemoryHandler.getReadUnchecked(currentSrc, cPrimType); { final List writeCall = mMemoryHandler.getWriteCall(ignoreLoc, @@ -293,14 +286,7 @@ destId, new RValue(loopCtrAux.getExp(), mExpressionTranslation.getCTypeOfPointer if (mMemoryHandler.getRequiredMemoryStructureFeatures().isPointerOnHeapRequired()) { final ICType cPointer = CPointer.voidPointer(); - final Expression srcAcc; - { - final ExpressionResult srcAccExpRes = mMemoryHandler.getReadUnchecked(currentSrc, cPointer); - srcAcc = srcAccExpRes.getLrValue().getValue(); - loopBody.addStatements(srcAccExpRes.getStatements()); - loopBody.addDeclarations(srcAccExpRes.getDeclarations()); - assert srcAccExpRes.getOverapprs().isEmpty(); - } + final Expression srcAcc = mMemoryHandler.getReadUnchecked(currentSrc, cPointer); { final List writeCall = mMemoryHandler.getWriteCall(ignoreLoc, diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java index 00ac7b94e2e..6efbc9fbb4f 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/library/FunctionModelHelper.java @@ -342,10 +342,17 @@ public ExpressionResult getNondetStringOrNull(final ILocation loc) { body.add(mMemoryHandler.getUltimateMemAllocCall(len.getExp(), retvar.getLhs(), loc, MemoryArea.HEAP)); final var nullChar = mTypeSizes.constructLiteralForIntegerType(loc, charType, BigInteger.ZERO); - final var lastChar = mMemoryHandler.lastCharOfString(loc, sizeT, len.getExp(), retvar.getExp()); - body.addAll(mMemoryHandler.getWriteCall(loc, - LRValueFactory.constructHeapLValue(mTypeHandler, lastChar, charType, null), nullChar, charType, false)); + // *(retvar + (len - 1)) = '\0'; + { + final var lenMinusOne = mExpressionTranslation.constructArithmeticIntegerExpression(loc, + IASTBinaryExpression.op_minus, mExpressionTranslation.applyWraparound(loc, sizeT, len.getExp()), + sizeT, mTypeSizes.constructLiteralForIntegerType(loc, sizeT, BigInteger.ONE), sizeT); + final Expression lastChar = mMemoryHandler.addExpressionToPointer(loc, retvar.getExp(), lenMinusOne); + body.addAll(mMemoryHandler.getWriteCall(loc, + LRValueFactory.constructHeapLValue(mTypeHandler, lastChar, charType, null), nullChar, charType, + false)); + } final var stmt = StatementFactory.constructIfStatement(loc, new WildcardExpression(loc), new Statement[] { setPtrToNull }, body.toArray(Statement[]::new)); diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java index c82a15ac87e..7bd5907c5a1 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/ExpressionResultTransformer.java @@ -264,9 +264,7 @@ private ExpressionResult switchToRValue(final ExpressionResult expr, final ILoca final ExpressionResultBuilder erb = new ExpressionResultBuilder().addAllExceptLrValue(expr); final RValue newValue; if (underlyingType instanceof CPrimitive || underlyingType instanceof CPointer) { - final ExpressionResult rex = - unchecked ? mMemoryHandler.getReadUnchecked(hlv.getAddress(), underlyingType) - : mMemoryHandler.getReadCall(hlv.getAddress(), underlyingType); + final ExpressionResult rex = readAsExpressionResult(hlv.getAddress(), unchecked, underlyingType); newValue = (RValue) rex.getLrValue(); erb.addAllExceptLrValue(rex); } else if (underlyingType instanceof final CArray cArray) { @@ -389,8 +387,8 @@ private ExpressionResult readStructFromHeap(final ExpressionResult old, final IL throw new UnsupportedOperationException("Bitfield read struct from heap"); } - final var newAddress = mMemoryHandler.constructAddressForStructField(loc, structOnHeapAddress, - innerStructOffset, mExprTrans.getCTypeOfPointerComponents()); + final var newAddress = + mMemoryHandler.constructAddressForStructField(loc, structOnHeapAddress, innerStructOffset); final ExpressionResult fieldRead = readStructFromHeap(old, loc, newAddress, cStructOrUnion, hook, unchecked); @@ -466,10 +464,8 @@ private ExpressionResult readArrayFromHeap(final ExpressionResult old, final ILo final ExpressionResult readRex; if (arrayValueType instanceof final CStructOrUnion cStructOrUnion) { readRex = readStructFromHeap(old, loc, addressExpr, cStructOrUnion, hook, unchecked); - } else if (unchecked) { - readRex = mMemoryHandler.getReadUnchecked(addressExpr, arrayType.getValueType()); } else { - readRex = mMemoryHandler.getReadCall(addressExpr, arrayType.getValueType()); + readRex = readAsExpressionResult(addressExpr, unchecked, arrayType.getValueType()); } builder.addAllExceptLrValue(readRex); builder.setOrResetLrValue(readRex.getLrValue()); @@ -487,6 +483,15 @@ private ExpressionResult readArrayFromHeap(final ExpressionResult old, final ILo return builder.build(); } + private ExpressionResult readAsExpressionResult(final Expression addressExpr, final boolean unchecked, + final ICType resultType) { + if (unchecked) { + final Expression read = mMemoryHandler.getReadUnchecked(addressExpr, resultType); + return new ExpressionResult(new RValue(read, resultType)); + } + return mMemoryHandler.getReadCall(addressExpr, resultType); + } + /** * Convert Expression of some type to an expression of boolean type. If the expression expr *
    diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java index 70499cac6a0..949651f52c8 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/result/LRValue.java @@ -30,7 +30,6 @@ import java.math.BigInteger; import de.uni_freiburg.informatik.ultimate.boogie.ast.Expression; -import de.uni_freiburg.informatik.ultimate.boogie.ast.StructConstructor; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.CTranslationUtil; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; @@ -84,10 +83,10 @@ public boolean isIntFromPointer() { @Override public final String toString() { - if (this instanceof HeapLValue) { - return "address: " + ((HeapLValue) this).getAddress(); - } else if (this instanceof LocalLValue) { - return "lhs: " + ((LocalLValue) this).getLhs(); + if (this instanceof final HeapLValue hlv) { + return "address: " + hlv.getAddress(); + } else if (this instanceof final LocalLValue llv) { + return "lhs: " + llv.getLhs(); } else { return "value: " + getValue(); } @@ -107,8 +106,8 @@ public boolean isNullPointerConstant(final IMemoryPointer memoryPointer) { } final Expression value; - if (this instanceof HeapLValue) { - value = ((HeapLValue) this).getAddress(); + if (this instanceof final HeapLValue hlv) { + value = hlv.getAddress(); throw new AssertionError("unexpected: double check this case"); } value = getValue(); @@ -118,9 +117,6 @@ public boolean isNullPointerConstant(final IMemoryPointer memoryPointer) { return true; } - if (value instanceof StructConstructor) { - return memoryPointer.isNullPointer(value); - } - return false; + return memoryPointer.isNullPointer(value); } } diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java index 43da8260023..8a3d00ce566 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/util/SFO.java @@ -179,13 +179,13 @@ public final class SFO { public static final String MEMCPY_DEST = "dest"; public static final String MEMCPY_SRC = "src"; public static final String MEMCPY_SIZE = "size"; - public static final String MEMCPY = "#memcpy"; public static final String STRCPY_DEST = "dest"; public static final String STRCPY_SRC = "src"; + public static final String ALLOCINIT_PTRBASE = "ptrBase"; + public static final String TO_INT = "#to_int"; - public static final String MEMSET = "ULTIMATE.memset"; /** * used for detecting data races diff --git a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java index cd99b1f7980..1a32f2beb54 100644 --- a/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java +++ b/trunk/source/CACSL2BoogieTranslator/src/de/uni_freiburg/informatik/ultimate/cdt/translation/interfaces/handler/ITypeHandler.java @@ -50,7 +50,6 @@ import de.uni_freiburg.informatik.ultimate.boogie.type.BoogieType; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.FlatSymbolTable; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.IDispatcher; -import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.base.chandler.IMemoryPointer; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.CPrimitive.CPrimitiveCategory; import de.uni_freiburg.informatik.ultimate.cdt.translation.implementation.container.c.ICType; @@ -189,6 +188,4 @@ public interface ITypeHandler { void registerNamedIncompleteType(String incompleteType, String named); void addLibraryTypes(Map libraryTypes); - - IMemoryPointer getMemoryPointer(); }