Some memory model simplifications #768

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft

maul-esel wants to merge 20 commits into dev from wip/dk/memory-model-simplifications

+450 −733

.../de/uni_freiburg/informatik/ultimate/cdt/translation/implementation/base/TypeHandler.java

-Original file line number
+Diff line change
@@ Expand Up / @@ -865,7 +865,6 @@ public static boolean isCharArray(final ICType cTypeRaw) { @@
     						|| cPrimitive.getType() == CPrimitives.SCHAR);
     	}
-    	@Override
     	public IMemoryPointer getMemoryPointer() {
     		return mMemoryPointer;
     	}
@@ Expand Down @@

...rg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryAdressing.java

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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<MemoryModelDeclarations> 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<Pair<Expression, Set<VariableLHS>>> 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<Triple<Expression, Set<VariableLHS>, 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<Statement> 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<Pair<Expression, Set<VariableLHS>>> constructAllocInitSpecificationExpressions(ILocation tuLoc,

    	List<Statement> 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<Specification> 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,18 +140,17 @@ Expression constructPointerValidityCheckExpr(final ILocation loc, final Expressi
  
    	 *

    	 * @return The specifications.

    	 */

    	List<Specification> 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);

    	/**

    	 * Constructs the statements used for the check if a freed pointer was valid.

    	 *

    	 * @return The statements.

    	 */

    	List<Statement> getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed,

    			final boolean isPointerCheckRequired, final RequiredMemoryModelFeatures requiredMemoryModelFeatures,

    	List<Expression> getChecksForFreeCall(final ILocation loc, final RValue pointerToBeFreed,

    			final RequiredMemoryModelFeatures requiredMemoryModelFeatures,

    			final MemoryModelDeclarationsHandler memoryModelDeclarationsHandler);

    	/**

    @@ -205,14 +181,6 @@ List<Statement> 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<Statement> 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<Statement> 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);

    }

...atik/ultimate/cdt/translation/implementation/base/chandler/IMemoryManagementStrategy.java

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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<Pair<Expression, Set<VariableLHS>>> 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<Triple<Expression, Set<VariableLHS>, Boolean>> constructDeallocSpecificationExpressions(ILocation tuLoc,

    	AllocationProcedureSpec constructAllocInitSpecification(ILocation tuLoc,

    			RequiredMemoryModelFeatures requiredMemoryModelFeatures,

    			MemoryModelDeclarationsHandler memoryModelDeclarationsHandler);

    @@ -72,11 +83,49 @@ List<Statement> 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<Pair<Expression, Set<VariableLHS>>> constructAllocInitSpecificationExpressions(ILocation tuLoc,

    			RequiredMemoryModelFeatures requiredMemoryModelFeatures,

    			MemoryModelDeclarationsHandler memoryModelDeclarationsHandler);

    	record AllocationProcedureSpec(List<Expression> ensures, List<Expression> freeEnsures, Set<VariableLHS> modifies) {

    		/**

    		 * Convenience constructor for specs that do not have "free ensures" clauses.

    		 */

    		AllocationProcedureSpec(final List<Expression> ensures, final Set<VariableLHS> 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<EnsuresSpecification> constructSpecificationClauses(final ILocation loc) {

    			final var result = new ArrayList<EnsuresSpecification>();

    			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;

    		}

    	}

    }

...rg/informatik/ultimate/cdt/translation/implementation/base/chandler/IMemoryStructure.java

-Original file line number
+Diff line change
@@ Expand Up / @@ -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);
@@ Expand All / @@ -50,8 +48,6 @@ public interface IMemoryStructure { @@
     	String getReadPointerProcedureName();
-    	String getUncheckedReadPointerProcedureName();
     	String getWritePointerProcedureName();
     	String getUncheckedWritePointerProcedureName();
@@ Expand Down @@

...formatik/ultimate/cdt/translation/implementation/base/chandler/InitializationHandler.java

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -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);

.../informatik/ultimate/cdt/translation/implementation/base/chandler/MemoryAddressing1D.java

-Original file line number
+Diff line change
@@ Expand Up / @@ -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;
@@ Expand Down Expand Up @@
     		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) {
@@ Expand Down Expand Up @@
     		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,
@@ Expand Down Expand Up @@
     		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");
-    	}
     }

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Some memory model simplifications #768

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Some memory model simplifications #768

Are you sure you want to change the base?

Some memory model simplifications #768

Uh oh!

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!