- * This class provides static methods to compute proof references. A proof reference is a source - * code member used during proof like methods, instance or class variables or operation contracts. - *
- *- * A found proof reference is an instance of {@link IProofReference}. - *
- *- * Proof references are computed for each {@link Node} separately based on the applied rule. - * Instances of {@link IProofReferencesAnalyst} are used to implement the rule specific extraction - * of such references. - *
- *- * This functionality is used by the Eclipse Projects like Visual DbC. - *
- * - * @author Martin Hentschel - * @see IProofReference - * @see IProofReferencesAnalyst - */ -public final class ProofReferenceUtil { - /** - * The default {@link IProofReferencesAnalyst}s. - */ - public static final ImmutableList- * Computes all proof references in the given {@link Proof} by iterating over all {@link Node}s - * in breath first order. - *
- *- * Changes during computation of the proof tree are not detected and should be avoided. - * Otherwise it is possible that the result is wrong. - *
- * - * @param proof The {@link Proof} to compute its references. - * @return The found {@link IProofReference}s. - */ - public static LinkedHashSet- * Computes all proof references in the given {@link Proof} by iterating over all {@link Node}s - * in breath first order. - *
- *- * Changes during computation of the proof tree are not detected and should be avoided. - * Otherwise it is possible that the result is wrong. - *
- * - * @param proof The {@link Proof} to compute its references. - * @param analysts The {@link IProofReferencesAnalyst} to use. - * @return The found {@link IProofReference}s. - */ - public static LinkedHashSet- * Instances of this class are used to compute {@link IProofReference} for a given {@link Node} - * based on the applied rule. Each instance of this class has the knowledge to extract the - * references for a single rule or a group of similar rules. - *
- *- * The complete extraction is done via static methods of {@link ProofReferenceUtil}. - *
- * - * @author Martin Hentschel - * @see ProofReferenceUtil - * @see IProofReference - */ -public interface IProofReferencesAnalyst { - /** - * Computes the {@link IProofReference} for the given {@link Node} which can be {@code null} or - * an empty set if the applied rule is not supported by this {@link IProofReferencesAnalyst}. - * - * @param node The {@link Node} to compute its {@link IProofReference}s. - * @param services The {@link Services} to use. - * @return The found {@link IProofReference} or {@code null}/empty set if the applied rule is - * not supported. - */ - LinkedHashSet- * A method call which determines the possible implementations of a called method. - *
- *- * References of this kind should provide an {@link IProgramMethod} as target - * ({@link #getTarget()}). - *
- */ - String CALL_METHOD = "Call Method"; - - /** - *- * The proof step "methodBodyExpand" that inlines methods. - *
- *- * References of this kind should provide an {@link IProgramMethod} as target - * ({@link #getTarget()}). - *
- */ - String INLINE_METHOD = "Inline Method"; - - /** - *- * The proof step "Use Operation Contract" which approximates a method call via its method - * contract and also the usage of dependency contracts. - *
- *- * References of this kind should provide a {@link Contract} as target ({@link #getTarget()}). - *
- */ - String USE_CONTRACT = "Use Contract"; - - /** - *- * Read/Write access of a field like instance or class variables during proof. - *
- *- * References of this kind should provide an {@link IProgramVariable} as target - * ({@link #getTarget()}). - *
- */ - String ACCESS = "Access"; - - /** - *- * Used invariants during proof. - *
- *- * References of this kind should provide an {@link ClassInvariant} as target - * ({@link #getTarget()}). - *
- */ - String USE_INVARIANT = "Use Invariant"; - - /** - *- * Used axioms during proof. - *
- *- * References of this kind should provide an {@link ClassAxiom} as target - * ({@link #getTarget()}). - *
- */ - String USE_AXIOM = "Use Axiom"; - - /** - * Returns the reference kind which is a human readable {@link String}. - * - * @return The reference kind as human readable {@link String}. - */ - String getKind(); - - /** - * Returns the {@link Node}s in which the reference was found. - * - * @return The {@link Node}s in which the reference was found. - */ - LinkedHashSet- * This is for instance required for the following rules: - *
- * This is for instance required if a rule is applied on a sub term without a - * {@link FormulaTermLabel} of a parent which has a {@link FormulaTermLabel}. Example rules are: - *
- * This is for instance required if the assumes clause of a rule has a {@link FormulaTermLabel} - * but the application does not have it. Example rules are: - *
- * Computes objects which should be ignored in the state because they are part of the proof - * obligation and not of the source code. - *
- *- * By default the set will contain the exc variable and the backup of arguments and the heap. - *
- * - * @param ignoreExceptionVariable Ignore exception variable? - * @param ignoreOldStateVariables Ignore old state variables? - * @return The objects to ignore. - */ - protected Set- * Computes for each location (value/association of an object) used in the updates of the given - * {@link Sequent} the {@link JTerm}s which allows to compute the object itself and the value of - * the value/association. The result is a {@link Set} of {@link ExtractLocationParameter} which - * contains the computed {@link JTerm}s. - *
- *- * Objects which are created in the heap during symbolic execution and all objects which are - * used on the right side of associations are also collected and stored in the {@link Set}s - * {@code updateCreatedObjectsToFill}/ {@code updateValueObjectsToFill}. - *
- * - * @param sequent The {@link Sequent} which provides the updates to extract locations from. - * @param locationsToFill The location {@link Set} to fill. - * @param updateCreatedObjectsToFill The new created object {@link Set} to fill. - * @param updateValueObjectsToFill The {@link Set} with objects used on right side of updates to - * fill. - * @param objectsToIgnore The objects to ignore. - * @throws ProofInputException Occurred Exception. - */ - protected void collectLocationsFromUpdates(Sequent sequent, - Set- * Computes for each location (value/association of an object) used in the the given - * {@link JTerm} the {@link JTerm}s which allows to compute the object itself and the value of - * the - * value/association. The result is a {@link Set} of {@link ExtractLocationParameter} which - * contains the computed {@link JTerm}s. - *
- *- * Objects which are created in the heap during symbolic execution and all objects which are - * used on the right side of associations are also collected and stored in the {@link Set}s - * {@code updateCreatedObjectsToFill}/ {@code updateValueObjectsToFill}. - *
- * - * @param updateTerm The {@link JTerm} which provides the update to extract locations from. - * @param locationsToFill The location {@link Set} to fill. - * @param updateCreatedObjectsToFill The new created object {@link Set} to fill. - * @param updateValueObjectsToFill The {@link Set} with objects used on right side of updates to - * fill. - * @param objectsToIgnore The objects to ignore. - * @throws ProofInputException Occurred Exception. - */ - protected void collectLocationsFromTerm(JTerm updateTerm, - Set- * Computes for each location (value/association of an object) used in the the given heap update - * {@link JTerm} the {@link JTerm}s which allows to compute the object itself and the value of - * the - * value/association. The result is a {@link Set} of {@link ExtractLocationParameter} which - * contains the computed {@link JTerm}s. - *
- *- * Objects which are created in the heap during symbolic execution and all objects which are - * used on the right side of associations are also collected and stored in the {@link Set}s - * {@code updateCreatedObjectsToFill}/ {@code updateValueObjectsToFill}. - *
- * - * @param term The {@link JTerm} which provides the heap update to extract locations from. - * @param locationsToFill The location {@link Set} to fill. - * @param updateCreatedObjectsToFill The new created object {@link Set} to fill. - * @param updateValueObjectsToFill The {@link Set} with objects used on right side of updates to - * fill. - * @throws ProofInputException Occurred Exception. - */ - protected void collectLocationsFromHeapUpdate(JTerm term, - Set- * Instances of this class provides the {@link JTerm} which are required to compute a location - * (value or association of a given object/state). - *
- *- * Instances of this class can be used to compute the values in each memory layout. So they are - * instantiated during the analyzation phase {@link SymbolicLayoutExtractor#analyse()} once for - * initial and current memory layout. - *
- * - * @author Martin Hentschel - */ - public class ExtractLocationParameter { - /** - * The {@link ProgramVariable} or {@code null} if an array index is used instead. - */ - private final ProgramVariable programVariable; - - /** - * The array index or {@code null} if not used. - */ - private final JTerm arrayIndex; - - /** - * The array start index or {@code null} if not used. - */ - private final JTerm arrayStartIndex; - - /** - * The array end index or {@code null} if not used. - */ - private final JTerm arrayEndIndex; - - /** - * An optional parent object represented as {@link JTerm}. If it is {@code null} an - * {@link IProgramVariable} of the state is represented. - */ - private final JTerm parentTerm; - - /** - * The index of the parent argument in the predicate used in side proof to compute the - * values. - */ - private int parentTermIndexInStatePredicate; - - /** - * The index of the value argument in the predicate used in side proof to compute the - * values. - */ - private int valueTermIndexInStatePredicate; - - /** - * The {@link LocationVariable} which is used to make sure that the defined parent object of - * the initial state is used, because the expression (e.g. {@code x.next}) might refer to - * different objects in the current state. - */ - private final LocationVariable preVariable; - - /** - * Defines if this location should explicitly be shown on the state. - */ - private final boolean stateMember; - - /** - * The constant used to query an array range. - */ - private final JTerm arrayRangeConstant; - - /** - * The constant representing the fact that no value is available. - */ - private final JTerm notAValue; - - /** - * Constructor for cloning purpose. - * - * @param original The original {@link ExtractLocationParameter} to clone. - * @param newParent The new parent {@link JTerm} to be used instead of the original one. - */ - public ExtractLocationParameter(ExtractLocationParameter original, JTerm newParent) { - this.programVariable = original.programVariable; - this.arrayIndex = original.arrayIndex; - this.parentTerm = OriginTermLabel.removeOriginLabels(newParent, getServices()); - this.parentTermIndexInStatePredicate = original.parentTermIndexInStatePredicate; - this.valueTermIndexInStatePredicate = original.valueTermIndexInStatePredicate; - this.preVariable = original.preVariable; - this.stateMember = original.stateMember; - this.arrayStartIndex = original.arrayStartIndex; - this.arrayEndIndex = original.arrayEndIndex; - this.arrayRangeConstant = original.arrayRangeConstant; - this.notAValue = original.notAValue; - } - - /** - * Constructor. - * - * @param programVariable The {@link ProgramVariable}. - * @param stateMember Defines if this location should explicitly be shown on the state. - * @throws ProofInputException Occurred Exception. - */ - public ExtractLocationParameter(ProgramVariable programVariable, boolean stateMember) - throws ProofInputException { - this(programVariable, null, stateMember); - } - - /** - * Constructor. - * - * @param programVariable The {@link ProgramVariable}. - * @param parentTerm The parent object represented as {@link JTerm}. - * @throws ProofInputException Occurred Exception. - */ - public ExtractLocationParameter(ProgramVariable programVariable, JTerm parentTerm) - throws ProofInputException { - this(programVariable, parentTerm, false); - } - - /** - * Constructor. - * - * @param programVariable The {@link ProgramVariable}. - * @param parentTerm The parent object represented as {@link JTerm}. - * @param stateMember Defines if this location should explicitly be shown on the state. - * @throws ProofInputException Occurred Exception. - */ - protected ExtractLocationParameter(ProgramVariable programVariable, JTerm parentTerm, - boolean stateMember) throws ProofInputException { - assert programVariable != null; - this.programVariable = programVariable; - this.parentTerm = OriginTermLabel.removeOriginLabels(parentTerm, getServices()); - this.preVariable = createLocationVariable("Pre" + preVariableIndex++, - parentTerm != null ? parentTerm.sort() : programVariable.sort()); - this.arrayIndex = null; - this.stateMember = stateMember; - this.arrayStartIndex = null; - this.arrayEndIndex = null; - this.arrayRangeConstant = null; - this.notAValue = null; - } - - /** - * Constructor. - * - * @param arrayIndex The array index. - * @param parentTerm The parent object represented as {@link JTerm}. - * @throws ProofInputException Occurred Exception. - */ - public ExtractLocationParameter(JTerm arrayIndex, JTerm parentTerm) - throws ProofInputException { - assert parentTerm != null; - this.programVariable = null; - this.arrayIndex = OriginTermLabel.removeOriginLabels(arrayIndex, getServices()); - this.parentTerm = OriginTermLabel.removeOriginLabels(parentTerm, getServices()); - this.preVariable = - createLocationVariable("Pre" + preVariableIndex++, parentTerm.sort()); - this.stateMember = false; - this.arrayStartIndex = null; - this.arrayEndIndex = null; - this.arrayRangeConstant = null; - this.notAValue = null; - } - - /** - * Constructor. - * - * @param arrayStartIndex The array start index. - * @param arrayEndIndex The array end index. - * @param parentTerm The parent object represented as {@link JTerm}. - * @throws ProofInputException Occurred Exception. - */ - public ExtractLocationParameter(JTerm arrayStartIndex, JTerm arrayEndIndex, - JTerm parentTerm) - throws ProofInputException { - assert arrayStartIndex != null; - assert arrayEndIndex != null; - assert parentTerm != null; - this.programVariable = null; - this.arrayIndex = null; - this.parentTerm = OriginTermLabel.removeOriginLabels(parentTerm, getServices()); - this.preVariable = - createLocationVariable("Pre" + preVariableIndex++, parentTerm.sort()); - this.stateMember = false; - this.arrayStartIndex = - OriginTermLabel.removeOriginLabels(arrayStartIndex, getServices()); - this.arrayEndIndex = OriginTermLabel.removeOriginLabels(arrayEndIndex, getServices()); - TermBuilder tb = getServices().getTermBuilder(); - Function constantFunction = new JFunction( - new Name(tb.newName(ExecutionAllArrayIndicesVariable.ARRAY_INDEX_CONSTANT_NAME)), - getServices().getTypeConverter().getIntegerLDT().targetSort()); - this.arrayRangeConstant = tb.func(constantFunction); - Function notAValueFunction = new JFunction( - new Name(tb.newName(ExecutionAllArrayIndicesVariable.NOT_A_VALUE_NAME)), - JavaDLTheory.ANY); - this.notAValue = tb.func(notAValueFunction); - } - - /** - * Creates a new {@link LocationVariable} with the given name and {@link Sort}. - * - * @param name The name of the new variable. - * @param sort The {@link Sort} of the new variable. - * @return The created {@link LocationVariable}. - * @throws ProofInputException Occurred Exception. - */ - protected LocationVariable createLocationVariable(String name, Sort sort) - throws ProofInputException { - return new LocationVariable(new ProgramElementName(name), sort); - } - - /** - * Checks if this location should explicitly be shown on the state. - * - * @return Show location on state? - */ - public boolean isStateMember() { - return stateMember; - } - - /** - * Checks if an array index is represented. - * - * @return {@code true} is array index, {@code false} is something else. - */ - public boolean isArrayIndex() { - return arrayIndex != null; - } - - /** - * Checks if an array range is represented. - * - * @return {@code true} is array range, {@code false} is something else. - */ - public boolean isArrayRange() { - return arrayStartIndex != null && arrayEndIndex != null; - } - - /** - * Returns the array index. - * - * @return The array index. - */ - public JTerm getArrayIndex() { - return arrayIndex; - } - - /** - * Returns the array start index. - * - * @return The array start index. - */ - public JTerm getArrayStartIndex() { - return arrayStartIndex; - } - - /** - * Returns the array end index. - * - * @return The array end index. - */ - public JTerm getArrayEndIndex() { - return arrayEndIndex; - } - - /** - * Returns the constant used to query an array range. - * - * @return The constant used to query an array range. - */ - public JTerm getArrayRangeConstant() { - return arrayRangeConstant; - } - - /** - * Returns the constant representing the fact that no value is available. - * - * @return The constant representing the fact that no value is available. - */ - public JTerm getNotAValue() { - return notAValue; - } - - /** - * Returns the pre variable. - * - * @return The pre variable. - */ - public LocationVariable getPreVariable() { - return preVariable; - } - - /** - * Returns the right side of the update created by {@link #createPreUpdate()}. - * - * @return The right side of the update created by {@link #createPreUpdate()}. - */ - public JTerm getPreUpdateTarget() { - return parentTerm != null ? parentTerm - : getServices().getTermBuilder().var(programVariable); - } - - /** - * Creates the pre update to make sure that the parent object defined by the expression is - * evaluated on the initial state because it might be changed in the current state due to - * updates. - * - * @return The created {@link JTerm} with the pre update. - */ - public JTerm createPreUpdate() { - JTerm originalTerm = getPreUpdateTarget(); - return getServices().getTermBuilder().elementary(preVariable, originalTerm); - } - - /** - * Creates the {@link JTerm} to compute the parent object with help of the pre update. - * - * @return The {@link JTerm} to compute the parent object with help of the pre update. - */ - public JTerm createPreParentTerm() { - return getServices().getTermBuilder().var(preVariable); - } - - /** - * Computes the {@link JTerm} to compute the value with help of the pre update. - * - * @return The {@link JTerm} to compute the value with help of the pre update. - */ - public JTerm createPreValueTerm() { - final TermBuilder tb = getServices().getTermBuilder(); - if (parentTerm != null) { - if (isArrayRange()) { - JTerm arrayRange = tb.and(tb.geq(arrayRangeConstant, arrayStartIndex), - tb.leq(arrayRangeConstant, arrayEndIndex)); - return tb.ife(arrayRange, tb.dotArr(parentTerm, arrayRangeConstant), notAValue); - } else if (isArrayIndex()) { - return tb.dotArr(parentTerm, arrayIndex); - } else { - if (getServices().getJavaInfo().getArrayLength() == programVariable) { - // Special handling for length attribute of arrays - Function function = - getServices().getTypeConverter().getHeapLDT().getLength(); - return tb.func(function, createPreParentTerm()); - } else { - Function function = - getServices().getTypeConverter().getHeapLDT().getFieldSymbolForPV( - (LocationVariable) programVariable, getServices()); - return tb.dot(programVariable.sort(), createPreParentTerm(), function); - } - } - } else { - if (programVariable.isStatic()) { - Function function = getServices().getTypeConverter().getHeapLDT() - .getFieldSymbolForPV((LocationVariable) programVariable, getServices()); - return tb.staticDot(programVariable.sort(), function); - } else { - return tb.var(programVariable); - } - } - } - - /** - * Returns the {@link ProgramVariable} or {@code null} if an array index is used instead. - * - * @return The {@link ProgramVariable} or {@code null} if an array index is used instead. - */ - public ProgramVariable getProgramVariable() { - return programVariable; - } - - /** - * Returns the optional parent object represented as {@link JTerm}. If it is {@code null} an - * {@link IProgramVariable} of the state is represented. - * - * @return The optional parent object represented as {@link JTerm}. If it is {@code null} an - * {@link IProgramVariable} of the state is represented. - */ - public JTerm getParentTerm() { - return parentTerm; - } - - /** - * Returns the index of the parent argument in the predicate used in side proof to compute - * the values. - * - * @return The index of the parent argument in the predicate used in side proof to compute - * the values. - */ - public int getParentTermIndexInStatePredicate() { - return parentTermIndexInStatePredicate; - } - - /** - * Sets the index of the parent argument in the predicate used in side proof to compute the - * values. - * - * @param selectParentTermIndexInStatePredicate The index of the parent argument in the - * predicate used in side proof to compute the values. - */ - public void setParentTermIndexInStatePredicate(int selectParentTermIndexInStatePredicate) { - this.parentTermIndexInStatePredicate = selectParentTermIndexInStatePredicate; - } - - /** - * Returns the index of the value argument in the predicate used in side proof to compute - * the values. - * - * @return The index of the value argument in the predicate used in side proof to compute - * the values. - */ - public int getValueTermIndexInStatePredicate() { - return valueTermIndexInStatePredicate; - } - - /** - * Sets the index of the value argument in the predicate used in side proof to compute the - * values. - * - * @param selectValueTermIndexInStatePredicate The index of the value argument in the - * predicate used in side proof to compute the values. - */ - public void setValueTermIndexInStatePredicate(int selectValueTermIndexInStatePredicate) { - this.valueTermIndexInStatePredicate = selectValueTermIndexInStatePredicate; - } - - /** - * {@inheritDoc} - */ - @Override - public String toString() { - if (isArrayRange()) { - return "[" + arrayStartIndex + " to " + arrayEndIndex + "] " - + (parentTerm != null ? " of " + parentTerm : ""); - } else if (isArrayIndex()) { - return "[" + arrayIndex + "] " + (parentTerm != null ? " of " + parentTerm : ""); - } else { - return programVariable + (parentTerm != null ? " of " + parentTerm : ""); - } - } - - /** - * {@inheritDoc} - */ - @Override - public boolean equals(Object obj) { - if (obj instanceof ExtractLocationParameter other) { - return Objects.equals(arrayIndex, other.arrayIndex) - && stateMember == other.stateMember - && Objects.equals(parentTerm, other.parentTerm) - && Objects.equals(programVariable, other.programVariable); - } else { - return false; - } - } - - /** - * {@inheritDoc} - */ - @Override - public int hashCode() { - int result = 17; - result = 31 * result + (arrayIndex != null ? arrayIndex.hashCode() : 0); - result = 31 * result + (stateMember ? 1 : 0); - result = 31 * result + (parentTerm != null ? parentTerm.hashCode() : 0); - result = 31 * result + (programVariable != null ? programVariable.hashCode() : 0); - return result; - } - } - - /** - *- * The method starts a side proof with the given arguments to compute the values and objects of - * the requested memory layout. The {@link ExecutionVariableValuePair} together with the memory - * layout term defines how to access the side proof result. - *
- *- * The next step is the result extraction from side proof which results in a {@link Set} of - * {@link ExecutionVariableValuePair} instances. Each instance defines a value or association of - * a parent object or the state itself. - *
- * - * @param layoutCondition An optional condition to consider. - * @param layoutTerm The result term to use in side proof. - * @param locations The locations to compute in side proof. - * @param currentLayout {@code true} current layout, {@code false} initial layout. - * @param simplifyConditions {@code true} simplify conditions, {@code false} do not simplify - * conditions. - * @return The computed {@link ExecutionVariableValuePair}s. - * @throws ProofInputException Occurred Exception. - */ - protected Set- * The implemented algorithm works as follows: - *
- * Represents a location (value or association of a given object/state) in a concrete memory - * layout of the initial or current state. - *
- *- * They are instantiated lazily when a concrete memory layout is requested the first during - * lazily computation - * {@link SymbolicLayoutExtractor#lazyComputeLayout}. - * The instances exists only temporary until the concrete {@link ISymbolicLayout} was created - * from them. - *
- * - * @author Martin Hentschel - */ - public static class ExecutionVariableValuePair { - /** - * The {@link ProgramVariable} or {@code null} if an array index is used instead. - */ - private final ProgramVariable programVariable; - - /** - * The array index or {@code null} if not used. - */ - private final JTerm arrayIndex; - - /** - * The array start index or {@code null} if not used. - */ - private final JTerm arrayStartIndex; - - /** - * The array end index or {@code null} if not used. - */ - private final JTerm arrayEndIndex; - - /** - * An optional parent object or {@code null} if it is a value/association of the state. - */ - private final JTerm parent; - - /** - * The value or association target. - */ - private final JTerm value; - - /** - * Defines if this location should explicitly be shown on the state. - */ - private final boolean stateMember; - - /** - * An optional condition under which the value is valid. - */ - private final JTerm condition; - - /** - * The {@link Node} on which this result is based on. - */ - private final Node goalNode; - - /** - * Constructor. - * - * @param programVariable The {@link ProgramVariable}. - * @param parent An optional parent object or {@code null} if it is a value/association of - * the state. - * @param value The value or association target. - * @param condition An optional condition under which the value is valid. - * @param stateMember Defines if this location should explicitly be shown on the state. - */ - public ExecutionVariableValuePair(ProgramVariable programVariable, JTerm parent, - JTerm value, - JTerm condition, boolean stateMember, Node goalNode) { - assert programVariable != null; - assert value != null; - this.programVariable = programVariable; - this.parent = parent; - this.value = value; - this.condition = condition; - this.arrayIndex = null; - this.stateMember = stateMember; - this.goalNode = goalNode; - this.arrayStartIndex = null; - this.arrayEndIndex = null; - } - - /** - * Constructor. - * - * @param arrayIndex The array index. - * @param parent The parent object. - * @param value The value or association target. - * @param condition An optional condition under which the value is valid. - * @param stateMember Defines if this location should explicitly be shown on the state. - */ - public ExecutionVariableValuePair(JTerm arrayIndex, JTerm parent, JTerm value, - JTerm condition, - boolean stateMember, Node goalNode) { - assert parent != null; - assert value != null; - this.programVariable = null; - this.arrayIndex = arrayIndex; - this.parent = parent; - this.value = value; - this.condition = condition; - this.stateMember = stateMember; - this.goalNode = goalNode; - this.arrayStartIndex = null; - this.arrayEndIndex = null; - } - - /** - * Constructor. - * - * @param arrayStartIndex The array start index. - * @param arrayEndIndex The array end index. - * @param arrayRangeConstant The constant used to query an array range. - * @param parent The parent object. - * @param value The value or association target. - * @param condition An optional condition under which the value is valid. - * @param stateMember Defines if this location should explicitly be shown on the state. - */ - public ExecutionVariableValuePair(JTerm arrayStartIndex, JTerm arrayEndIndex, - JTerm arrayRangeConstant, JTerm parent, JTerm value, JTerm condition, - boolean stateMember, Node goalNode) { - assert parent != null; - assert value != null; - this.programVariable = null; - this.arrayIndex = arrayRangeConstant; - this.parent = parent; - this.value = value; - this.condition = condition; - this.stateMember = stateMember; - this.goalNode = goalNode; - this.arrayStartIndex = arrayStartIndex; - this.arrayEndIndex = arrayEndIndex; - } - - /** - * Returns the {@link ProgramVariable} or {@code null} if an array index is used instead. - * - * @return The {@link ProgramVariable} or {@code null} if an array index is used instead. - */ - public ProgramVariable getProgramVariable() { - return programVariable; - } - - /** - * Returns the optional parent object or {@code null} if it is a value/association of the - * state. - * - * @return The optional parent object or {@code null} if it is a value/association of the - * state. - */ - public JTerm getParent() { - return parent; - } - - /** - * Returns the value or association target. - * - * @return The value or association target. - */ - public JTerm getValue() { - return value; - } - - /** - * Checks if an array index is represented. - * - * @return {@code true} is array index, {@code false} is something else. - */ - public boolean isArrayIndex() { - return arrayIndex != null && (arrayStartIndex == null || arrayEndIndex == null); - } - - /** - * Checks if an array range is represented. - * - * @return {@code true} is array range, {@code false} is something else. - */ - public boolean isArrayRange() { - return arrayStartIndex != null && arrayEndIndex != null; - } - - /** - * Returns the array index. - * - * @return The array index. - */ - public JTerm getArrayIndex() { - return arrayIndex; - } - - /** - * Returns the array start index. - * - * @return The array start index. - */ - public JTerm getArrayStartIndex() { - return arrayStartIndex; - } - - /** - * Returns the array end index. - * - * @return The array end index. - */ - public JTerm getArrayEndIndex() { - return arrayEndIndex; - } - - /** - * Checks if this location should explicitly be shown on the state. - * - * @return Show location on state? - */ - public boolean isStateMember() { - return stateMember; - } - - /** - * Returns the optional condition under which the value is valid. - * - * @return The optional condition under which the value is valid. - */ - public JTerm getCondition() { - return condition; - } - - /** - * Returns the {@link Node} on which this result is based on. - * - * @return The {@link Node} on which this result is based on. - */ - public Node getGoalNode() { - return goalNode; - } - - /** - * {@inheritDoc} - */ - @Override - public boolean equals(Object obj) { - if (obj instanceof ExecutionVariableValuePair other) { - return isArrayRange() - ? (getArrayStartIndex().equals(other.getArrayStartIndex()) - && getArrayEndIndex().equals(other.getArrayEndIndex())) - : (isArrayIndex() ? getArrayIndex().equals(other.getArrayIndex()) - : getProgramVariable().equals(other.getProgramVariable())) - && getParent() != null - ? getParent().equals(other.getParent()) - : other.getParent() == null && getCondition() != null - ? getCondition().equals(other.getCondition()) - : other.getCondition() == null - && getValue().equals(other.getValue()) - && getGoalNode() - .equals(other.getGoalNode()); - } else { - return false; - } - } - - /** - * {@inheritDoc} - */ - @Override - public int hashCode() { - int result = 17; - if (isArrayRange()) { - result = 31 * result + getArrayStartIndex().hashCode(); - result = 31 * result + getArrayEndIndex().hashCode(); - } else if (isArrayIndex()) { - result = 31 * result + getArrayIndex().hashCode(); - } else { - result = 31 * result + getProgramVariable().hashCode(); - } - result = 31 * result + (getParent() != null ? getParent().hashCode() : 0); - result = 31 * result + (getCondition() != null ? getCondition().hashCode() : 0); - result = 31 * result + getValue().hashCode(); - result = 31 * result + getGoalNode().hashCode(); - return result; - } - - /** - * {@inheritDoc} - */ - @Override - public String toString() { - if (isArrayRange()) { - return "[" + getArrayIndex() + "]" + " between " + getArrayStartIndex() + " and " - + getArrayEndIndex() + (getParent() != null ? " of " + getParent() : "") - + " is " + getValue() - + (getCondition() != null ? " under condition " + getCondition() : "") - + " at goal " + goalNode.serialNr(); - } else if (isArrayIndex()) { - return "[" + getArrayIndex() + "]" - + (getParent() != null ? " of " + getParent() : "") + " is " + getValue() - + (getCondition() != null ? " under condition " + getCondition() : "") - + " at goal " + goalNode.serialNr(); - } else { - return getProgramVariable() + (getParent() != null ? " of " + getParent() : "") - + " is " + getValue() - + (getCondition() != null ? " under condition " + getCondition() : "") - + " at goal " + goalNode.serialNr(); - } - } - } -} diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java deleted file mode 100644 index e519e28039f..00000000000 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/AbstractWriter.java +++ /dev/null @@ -1,140 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.symbolic_execution; - -import java.util.Map; -import java.util.Map.Entry; - -import org.key_project.util.java.StringUtil; -import org.key_project.util.java.XMLUtil; - -/** - * Provides the basic functionality for classes like {@link ExecutionNodeWriter} and - * {@link SymbolicLayoutWriter} which encodes an object structure as XML. - * - * @author Martin Hentschel - */ -public abstract class AbstractWriter { - /** - * New line. - */ - public static final String NEW_LINE = StringUtil.NEW_LINE; - - /** - * The used leading white space in each level. - */ - public static final String LEADING_WHITE_SPACE_PER_LEVEL = " "; - - /** - * The default encoding. - */ - public static final String DEFAULT_ENCODING = "UTF-8"; - - /** - * Attribute name to store encodings. - */ - public static final String ATTRIBUTE_ENCODING = "encoding"; - - /** - * Attribute name to store the XML ID. - */ - public static final String ATTRIBUTE_XML_ID = "xml:id"; - - /** - * Appends an empty tag to the given {@link StringBuilder}. - * - * @param level The level. - * @param tagName The tag name. - * @param attributeValues The attributes. - * @param sb The {@link StringBuilder} to append to. - */ - protected void appendEmptyTag(int level, String tagName, Map- * Iterates preorder over the whole sub tree of a given {@link IExecutionNode}. - *
- *- * Instances of this class should always be used instead of recursive method calls because they - * cause {@link StackOverflowError}s even in small programs. - *
- *- * Attention: The iteration process does not take care of changes in the model. If the - * containment hierarchy changes during iteration it is possible that elements are left or visited - * multiple times. For this reason it is forbidden to change the model during iteration. But the - * developer has to take care about it. - *
- * - * @author Martin Hentschel - */ -public class ExecutionNodePreorderIterator { - /** - * The element at that the iteration has started used as end condition to make sure that only - * over the subtree of the element is iterated. - */ - private final IExecutionNode start; - - /** - * The next element or {@code null} if no more elements exists. - */ - private IExecutionNode next; - - /** - * Constructor. - * - * @param start The {@link IExecutionNode} to iterate over its sub tree. - */ - public ExecutionNodePreorderIterator(IExecutionNode start) { - this.start = start; - this.next = start; - } - - /** - * Checks if more elements are available. - * - * @return {@code true} has more elements, {@code false} has not more elements. - */ - public boolean hasNext() { - return next != null; - } - - /** - * Returns the next {@link IExecutionNode} in the containment hierarchy. - * - * @return The next {@link IExecutionNode}. - */ - public IExecutionNode next() { - IExecutionNode oldNext = next; - updateNext(); - return oldNext; - } - - /** - * Computes the next element and updates {@link #next()}. - */ - protected void updateNext() { - IExecutionNode newNext = null; - IExecutionNode[] children = next.getChildren(); - if (children.length >= 1) { - newNext = children[0]; - } else { - newNext = getNextOnParent(next); - } - this.next = newNext; - } - - /** - * Returns the next element to select if all children of the given {@link IExecutionNode} are - * visited. - * - * @param node The visited {@link IExecutionNode}. - * @return The next {@link IExecutionNode} to visit. - */ - protected IExecutionNode getNextOnParent(IExecutionNode node) { - IExecutionNode parent = node.getParent(); - while (parent != null) { - boolean IExecutionNodeFound = false; // Indicates that IExecutionNode was found on the - // parent. - IExecutionNode[] children = parent.getChildren(); - IExecutionNode nextChildOnParent = null; // The next child on the parent or the last - // child after iteration has finished - for (IExecutionNode child : children) { - nextChildOnParent = child; - if (nextChildOnParent == start) { - return null; - } - if (IExecutionNodeFound) { - return nextChildOnParent; - } - if (nextChildOnParent == node) { - IExecutionNodeFound = true; - } - } - if (nextChildOnParent != start) { - node = parent; // Continue search on parent without recursive call! - parent = parent.getParent(); - } else { - return null; - } - } - return null; // No more parents available. - } -} diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java deleted file mode 100644 index 1d1f21eda66..00000000000 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/ExecutionNodeReader.java +++ /dev/null @@ -1,3232 +0,0 @@ -/* This file is part of KeY - https://key-project.org - * KeY is licensed under the GNU General Public License Version 2 - * SPDX-License-Identifier: GPL-2.0-only */ -package de.uka.ilkd.key.symbolic_execution; - -import java.io.File; -import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStream; -import java.util.*; -import java.util.Map.Entry; -import javax.xml.parsers.ParserConfigurationException; -import javax.xml.parsers.SAXParser; -import javax.xml.parsers.SAXParserFactory; - -import de.uka.ilkd.key.java.*; -import de.uka.ilkd.key.java.ast.*; -import de.uka.ilkd.key.java.ast.expression.Expression; -import de.uka.ilkd.key.java.ast.reference.MethodReference; -import de.uka.ilkd.key.java.ast.statement.*; -import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.op.IProgramMethod; -import de.uka.ilkd.key.logic.op.IProgramVariable; -import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.proof.NodeInfo; -import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.init.InitConfig; -import de.uka.ilkd.key.proof.init.ProofInputException; -import de.uka.ilkd.key.speclang.BlockContract; -import de.uka.ilkd.key.speclang.Contract; -import de.uka.ilkd.key.speclang.LoopSpecification; -import de.uka.ilkd.key.symbolic_execution.model.*; -import de.uka.ilkd.key.symbolic_execution.model.IExecutionTermination.TerminationKind; -import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicEquivalenceClass; -import de.uka.ilkd.key.symbolic_execution.object_model.ISymbolicLayout; - -import org.key_project.logic.sort.Sort; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.Pair; -import org.key_project.util.java.CollectionUtil; - -import org.xml.sax.Attributes; -import org.xml.sax.SAXException; -import org.xml.sax.helpers.DefaultHandler; - -/** - * Allows to read XML files which contains an symbolic execution tree written via an - * {@link ExecutionNodeWriter}. - * - * @author Martin Hentschel - * @see ExecutionNodeWriter - */ -public class ExecutionNodeReader { - /** - * Reads the given {@link File}. - * - * @param file The {@link File} to read. - * @return The root of the read symbolic execution tree. - * @throws ParserConfigurationException Occurred Exception. - * @throws SAXException Occurred Exception. - * @throws IOException Occurred Exception. - */ - public IExecutionNode read(File file) - throws ParserConfigurationException, SAXException, IOException { - return read(new FileInputStream(file)); - } - - /** - * Reads from the given {@link InputStream} and closes it. - * - * @param in The {@link InputStream} to read from. - * @return The root of the read symbolic execution tree. - * @throws ParserConfigurationException Occurred Exception. - * @throws SAXException Occurred Exception. - * @throws IOException Occurred Exception. - */ - public IExecutionNode read(InputStream in) - throws ParserConfigurationException, SAXException, IOException { - if (in != null) { - try (in) { - // Parse XML file - SAXParserFactory factory = SAXParserFactory.newInstance(); - factory.setNamespaceAware(true); - SAXParser saxParser = factory.newSAXParser(); - SEDSAXHandler handler = new SEDSAXHandler(); - saxParser.parse(in, handler); - // Get root - IExecutionNode root = handler.getRoot(); - // Construct call stacks - Set