2+75 separate SymbolicAnalysis, SymbolicEvaluationVisitor,
SymbolicEvaluationEnvironment
diff --git a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
index 4b3b968..6c10105 100644
--- a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
+++ b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
@@ -141,12 +141,6 @@
<filter id="404000815">
<message_arguments>
<message_argument value="org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment"/>
- <message_argument value="getExecutor()"/>
- </message_arguments>
- </filter>
- <filter id="404000815">
- <message_arguments>
- <message_argument value="org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment"/>
<message_argument value="getParentEvaluationEnvironment()"/>
</message_arguments>
</filter>
@@ -357,7 +351,7 @@
<filter id="404000815">
<message_arguments>
<message_argument value="org.eclipse.ocl.pivot.library.LibraryIteration"/>
- <message_argument value="symbolicEvaluate(AbstractSymbolicEvaluationEnvironment, LoopExp)"/>
+ <message_argument value="symbolicEvaluate(SymbolicEvaluationEnvironment, LoopExp)"/>
</message_arguments>
</filter>
</resource>
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
index df6a49b..0facb9c 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
@@ -33,7 +33,6 @@
*/
public interface EvaluationEnvironmentExtension extends EvaluationEnvironment
{
- @Override
@NonNull ExecutorInternal getExecutor();
@Override
EvaluationEnvironment.@Nullable EvaluationEnvironmentExtension getParentEvaluationEnvironment();
@@ -68,13 +67,6 @@
}
/**
- * @since 1.16
- */
- default @NonNull ExecutorInternal getExecutor() {
- throw new UnsupportedOperationException();
- }
-
- /**
* Returns the value associated with the supplied variable declaration
*
* @param referredVariable
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractEvaluationVisitor.java
index 367e8d0..6a3bc21 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractEvaluationVisitor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractEvaluationVisitor.java
@@ -67,7 +67,7 @@
/** @deprecated Use getExecutor().getEvaluationEnvironment() */
@Deprecated
- protected final @NonNull EvaluationEnvironment evaluationEnvironment;
+ protected EvaluationEnvironment evaluationEnvironment;
/** @deprecated Use environmentFactory.getEvaluationEnvironment() */
@Deprecated
protected final @NonNull CompleteEnvironmentInternal completeEnvironment;
@@ -91,7 +91,7 @@
this.idResolver = environmentFactory.getIdResolver();
this.standardLibrary = environmentFactory.getStandardLibrary();
this.undecoratedVisitor = this; // assume I have no decorator
- this.evaluationEnvironment = executor.getRootEvaluationEnvironment();
+ // this.evaluationEnvironment = executor.getRootEvaluationEnvironment();
this.completeEnvironment = environmentFactory.getCompleteEnvironment();
this.modelManager = executor.getModelManager();
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractSymbolicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractSymbolicEvaluationEnvironment.java
index a354eae..a930881 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractSymbolicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractSymbolicEvaluationEnvironment.java
@@ -14,16 +14,15 @@
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.Element;
-import org.eclipse.ocl.pivot.NamedElement;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.TypedElement;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
-import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
import org.eclipse.ocl.pivot.ids.TypeId;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicContent;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicUnknownValue;
import org.eclipse.ocl.pivot.utilities.ClassUtil;
+import org.eclipse.ocl.pivot.utilities.EnvironmentFactory;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.SymbolicValue;
@@ -35,20 +34,23 @@
*
* @since 1.16
*/
-public abstract class AbstractSymbolicEvaluationEnvironment extends BasicEvaluationEnvironment implements SymbolicEvaluationEnvironment
+public abstract class AbstractSymbolicEvaluationEnvironment implements SymbolicEvaluationEnvironment
{
- private /*@LazyNonNull*/ EvaluationVisitor undecoratedVisitor = null;
+ protected final @NonNull SymbolicAnalysis symbolicAnalysis;
+ protected final @NonNull TypedElement executableObject;
+ protected final @NonNull EnvironmentFactory environmentFactory;
+ protected final @NonNull SymbolicEvaluationVisitor symbolicEvaluationVisitor;
- protected AbstractSymbolicEvaluationEnvironment(@NonNull SymbolicAnalysis executor, @NonNull NamedElement executableObject) {
- super(executor, executableObject);
+ protected AbstractSymbolicEvaluationEnvironment(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull TypedElement executableObject) {
+ this.symbolicAnalysis = symbolicAnalysis;
+ this.executableObject = executableObject;
+ this.environmentFactory = symbolicAnalysis.getEnvironmentFactory();
+ this.symbolicEvaluationVisitor = symbolicAnalysis.createSymbolicEvaluationVisitor(this);
}
- protected AbstractSymbolicEvaluationEnvironment(@NonNull AbstractSymbolicEvaluationEnvironment parent, @NonNull NamedElement element) {
- super(parent, element, element);
- }
-
+ @Override
public @Nullable SymbolicValue basicGetSymbolicValue(@NonNull Element element) {
- CSEElement cseElement = getSymbolicAnalysis().getCSEElement(element);
+ CSEElement cseElement = symbolicAnalysis.getCSEElement(element);
return basicGetSymbolicValue(cseElement);
}
@@ -58,7 +60,6 @@
public @Nullable SymbolicValue checkNotEmpty(@NonNull TypedElement typedElement, @NonNull TypeId typeId) {
SymbolicValue symbolicValue = getSymbolicValue(typedElement);
SymbolicContent symbolicContent = symbolicValue.getContent();
-// symbolicContent.toString(); // XXX
SymbolicValue symbolicSize = symbolicContent.getSize();
if (symbolicSize.isZero()) {
return getKnownValue(ValueUtil.INVALID_VALUE);
@@ -66,9 +67,8 @@
if (!symbolicSize.mayBeZero()) {
return null;
}
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
symbolicAnalysis.addMayBeEmptyHypothesis(typedElement, symbolicValue);
- return getMayBeInvalidValue(typeId);
+ return symbolicAnalysis.getMayBeInvalidValue(typeId);
}
@Override
@@ -80,9 +80,8 @@
if (!symbolicValue.mayBeInvalid()) {
return null;
}
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
symbolicAnalysis.addMayBeInvalidHypothesis(typedElement, symbolicValue);
- return getMayBeInvalidValue(typeId);
+ return symbolicAnalysis.getMayBeInvalidValue(typeId);
}
@Override
@@ -94,25 +93,10 @@
if (!symbolicValue.mayBeNull()) {
return null;
}
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
symbolicAnalysis.addMayBeNullHypothesis(typedElement, symbolicValue);
- return getMayBeInvalidValue(typeId);
+ return symbolicAnalysis.getMayBeInvalidValue(typeId);
}
-/* @Override
- public @Nullable SymbolicValue checkNotSmallerThan(@NonNull TypedElement typedElement, @NonNull SymbolicValue minSizeValue, @NonNull TypeId typeId) {
- SymbolicValue symbolicValue = getSymbolicValue(typedElement);
- if (symbolicValue.isSmallerThan(minSizeValue)) {
- return getKnownValue(ValueUtil.INVALID_VALUE);
- }
- if (!symbolicValue.mayBeSmallerThan(minSizeValue)) {
- return null;
- }
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
- symbolicAnalysis.addMayBeSmallerThanHypothesis(typedElement, symbolicValue, minSizeValue);
- return getMayBeInvalidValue(typeId);
- } */
-
@Override
public @Nullable SymbolicValue checkNotZero(@NonNull TypedElement typedElement, @NonNull TypeId typeId) {
SymbolicValue symbolicValue = getSymbolicValue(typedElement);
@@ -122,45 +106,38 @@
if (!symbolicValue.mayBeZero()) {
return null;
}
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
symbolicAnalysis.addMayBeZeroHypothesis(typedElement, symbolicValue);
- return getMayBeInvalidValue(typeId);
+ return symbolicAnalysis.getMayBeInvalidValue(typeId);
}
+ @Override
public @NonNull SymbolicUnknownValue createUnknownValue(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalid) {
- return new SymbolicUnknownValue(getSymbolicAnalysis().createVariableName(), typeId, mayBeNull, mayBeInvalid);
+ return symbolicAnalysis.createUnknownValue(typeId, mayBeNull, mayBeInvalid);
}
@Override
public @NonNull SymbolicValue createUnknownValue(@NonNull TypedElement typedElement, boolean mayBeNull, boolean mayBeInvalid) {
- return createUnknownValue(typedElement.getTypeId(), mayBeNull, mayBeInvalid);
+ return symbolicAnalysis.createUnknownValue(typedElement, mayBeNull, mayBeInvalid);
}
- public @NonNull SymbolicValue getBaseSymbolicValue(@NonNull CSEElement cseElement) {
- return getBaseSymbolicEvaluationEnvironment().getSymbolicValue(cseElement);
+ @Override
+ public @NonNull EnvironmentFactory getEnvironmentFactory() {
+ return environmentFactory;
}
- public @NonNull SymbolicValue getBaseSymbolicValue(@NonNull TypedElement typedElement) {
- return getBaseSymbolicEvaluationEnvironment().getSymbolicValue(typedElement);
+ @Override
+ public @NonNull ExecutorInternal getExecutor() {
+ return symbolicAnalysis.getExecutor();
}
@Override
public final @NonNull SymbolicValue getKnownValue(@Nullable Object boxedValue) {
- return getSymbolicAnalysis().getKnownValue(boxedValue);
- }
-
- public @Nullable SymbolicValue getMayBeInvalidValue(@NonNull TypeId typeid) {
- return getBaseSymbolicEvaluationEnvironment().getMayBeInvalidValue(typeid);
- }
-
- @Override
- public @Nullable AbstractSymbolicEvaluationEnvironment getParent() {
- return (AbstractSymbolicEvaluationEnvironment) super.getParent();
+ return symbolicAnalysis.getKnownValue(boxedValue);
}
@Override
public final @NonNull SymbolicAnalysis getSymbolicAnalysis() {
- return (SymbolicAnalysis)executor;
+ return symbolicAnalysis;
}
@Override
@@ -172,14 +149,6 @@
return ClassUtil.nonNullState(basicGetSymbolicValue(cseElement));
}
- protected @NonNull EvaluationVisitor getUndecoratedVisitor() {
- EvaluationVisitor undecoratedVisitor2 = undecoratedVisitor;
- if (undecoratedVisitor2 == null) {
- this.undecoratedVisitor = undecoratedVisitor2 = executor.getEvaluationVisitor().getUndecoratedVisitor();
- }
- return undecoratedVisitor2;
- }
-
@Override
public boolean isFalse(@NonNull TypedElement element) {
return getSymbolicValue(element).isFalse();
@@ -224,8 +193,10 @@
public void setDead(@NonNull OCLExpression expression) {}
@Override
- public void toString(@NonNull StringBuilder s) {
- toString(s, 0);
+ public String toString() {
+ StringBuilder s = new StringBuilder();
+ toString(s,0);
+ return s.toString();
}
protected abstract void toString(@NonNull StringBuilder s, int depth);
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BaseSymbolicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BaseSymbolicEvaluationEnvironment.java
index 09ca097..bac65cf 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BaseSymbolicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BaseSymbolicEvaluationEnvironment.java
@@ -24,16 +24,12 @@
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.Element;
import org.eclipse.ocl.pivot.ExpressionInOCL;
-import org.eclipse.ocl.pivot.NamedElement;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.TypedElement;
import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.VariableExp;
-import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
-import org.eclipse.ocl.pivot.ids.TypeId;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
import org.eclipse.ocl.pivot.internal.symbolic.AbstractSymbolicRefinedValue;
-import org.eclipse.ocl.pivot.internal.symbolic.SymbolicUnknownValue;
import org.eclipse.ocl.pivot.utilities.NameUtil;
import org.eclipse.ocl.pivot.utilities.StringUtil;
import org.eclipse.ocl.pivot.utilities.TreeIterable;
@@ -54,21 +50,14 @@
private @NonNull Map<@NonNull CSEElement, @NonNull SymbolicValue> cseElement2symbolicValue = new HashMap<>();
/**
- * The maybe-invalid symbolic value of known TYpeIds.
- */
- private @NonNull Map<@NonNull TypeId, org.eclipse.ocl.pivot.internal.symbolic.SymbolicUnknownValue> typeid2symbolicValue = new HashMap<>();
-
- /**
* The expression-specific refined symbolic values established after contradicting a hypothesis.
*/
private @NonNull Map<@NonNull TypedElement, @NonNull SymbolicValue> expression2refinedSymbolicValue = new HashMap<>();
- public BaseSymbolicEvaluationEnvironment(@NonNull SymbolicAnalysis executor, @NonNull NamedElement executableObject) {
- super(executor, executableObject);
- }
+ private @Nullable HypothesizedSymbolicEvaluationEnvironment hypothesizedSymbolicEvaluationEnvironment = null;
- public BaseSymbolicEvaluationEnvironment(@NonNull AbstractSymbolicEvaluationEnvironment parent, @NonNull TypedElement executableObject) {
- super(parent, executableObject);
+ public BaseSymbolicEvaluationEnvironment(@NonNull SymbolicAnalysis executor, @NonNull ExpressionInOCL expressionInOCL) {
+ super(executor, expressionInOCL);
}
@Override
@@ -77,7 +66,7 @@
if (refinedSymbolicValue != null) {
return refinedSymbolicValue;
}
- CSEElement cseElement = getSymbolicAnalysis().getCSEElement(element);
+ CSEElement cseElement = symbolicAnalysis.getCSEElement(element);
return basicGetSymbolicValue(cseElement);
}
@@ -91,7 +80,7 @@
*/
private void gatherAffectedTypedElements(@NonNull Set<@NonNull TypedElement> affectedExpressions, @NonNull TypedElement typedElement) {
if (typedElement instanceof VariableDeclaration) {
- CSEElement variableCSE = getSymbolicAnalysis().getCSEElement(typedElement);
+ CSEElement variableCSE = symbolicAnalysis.getCSEElement(typedElement);
Iterable<@NonNull OCLExpression> variableExps = variableCSE.getOutputs();
if (variableExps != null) {
for (@NonNull OCLExpression variableExp : variableExps) {
@@ -135,56 +124,26 @@
return cseElement2symbolicValue.keySet();
}
- @Override
- public @Nullable SymbolicValue getMayBeInvalidValue(@NonNull TypeId typeid) {
- SymbolicUnknownValue symbolicUnknownValue = typeid2symbolicValue.get(typeid);
- if (symbolicUnknownValue == null) {
- symbolicUnknownValue = createUnknownValue(typeid, false, true);
- typeid2symbolicValue.put(typeid, symbolicUnknownValue);
- }
- return symbolicUnknownValue;
+ public @NonNull SymbolicEvaluationEnvironment getSymbolicEvaluationEnvironment() {
+ return hypothesizedSymbolicEvaluationEnvironment != null ? hypothesizedSymbolicEvaluationEnvironment : this;
}
- @Override
- public @Nullable Object getValueOf(@NonNull TypedElement variable) {
- Object variableValue = super.getValueOf(variable);
- /* if (variableValue instanceof SymbolicValue) {
- SymbolicValue symbolicValue = (SymbolicValue)variableValue;
- Iterable<@Nullable Object> constraints = getSymbolicConstraints(variable, null);
- if (constraints != null) {
- boolean mayBeInvalid = true;
- boolean mayBeNull = true;
- for (@Nullable Object constraint : constraints) {
- if (!ValueUtil.mayBeInvalid(constraint)) {
- mayBeInvalid = false;
- }
- if (!ValueUtil.mayBeNull(constraint)) {
- mayBeNull = false;
- }
- }
- if ((mayBeInvalid != symbolicValue.mayBeInvalid()) || (mayBeNull != symbolicValue.mayBeNull())) {
- return new SymbolicVariableValueImpl((VariableDeclaration) variable, mayBeNull, mayBeInvalid);
- }
- }
- } */
- return variableValue;
- }
-
- /**
- * Return true if typedElement may have some symbolic constraints. Conversely avoid the need to compute the boxed source and
- * argument lists if there are no such constraints that have been deduced.
- *
- *
- @Override
- public boolean hasSymbolicConstraints(@NonNull TypedElement typedElement) {
- Map<@Nullable List<@Nullable Object>, @NonNull List<@Nullable Object>> values2constraints = typedElement2values2constraints.get(typedElement);
- return values2constraints != null;
- } */
-
public boolean isDead(@NonNull OCLExpression element) {
return basicGetSymbolicValue(element) == null;
}
+ public void popHypothesis() {
+ assert this.hypothesizedSymbolicEvaluationEnvironment != null;
+ hypothesizedSymbolicEvaluationEnvironment = null;
+ // executor.popEvaluationEnvironment();
+ }
+
+ public @NonNull HypothesizedSymbolicEvaluationEnvironment pushHypothesis(@NonNull Hypothesis hypothesis) {
+ assert this.hypothesizedSymbolicEvaluationEnvironment == null;
+ this.hypothesizedSymbolicEvaluationEnvironment = symbolicAnalysis.createHypothesizedSymbolicEvaluationEnvironment(hypothesis);
+ return hypothesizedSymbolicEvaluationEnvironment;
+ }
+
public void refineValue(@NonNull TypedElement typedElement, @NonNull SymbolicValue symbolicValue) {
if (SymbolicAnalysis.HYPOTHESIS.isActive()) {
SymbolicAnalysis.HYPOTHESIS.println(" refined: " + symbolicValue);
@@ -200,12 +159,12 @@
Set<@NonNull TypedElement> affectedExpressionsSet = new HashSet<>();
gatherAffectedTypedElements(affectedExpressionsSet, typedElement);
List<@NonNull TypedElement> affectedExpressionsList = new ArrayList<>(affectedExpressionsSet);
- Collections.sort(affectedExpressionsList, getSymbolicAnalysis().getTypedElementHeightComparator());
+ Collections.sort(affectedExpressionsList, symbolicAnalysis.getTypedElementHeightComparator());
for (@NonNull TypedElement affectedExpression : affectedExpressionsList) {
if (SymbolicAnalysis.HYPOTHESIS.isActive()) {
SymbolicAnalysis.HYPOTHESIS.println(" re-evaluating \"" + affectedExpression + "\" in \"" + affectedExpression.eContainer() + "\"");
}
- SymbolicValue oldValue = getBaseSymbolicValue(affectedExpression);
+ SymbolicValue oldValue = getSymbolicValue(affectedExpression);
if (SymbolicAnalysis.HYPOTHESIS.isActive()) {
SymbolicAnalysis.HYPOTHESIS.println(" old: " + oldValue);
}
@@ -238,8 +197,7 @@
}
Object result;
try {
- EvaluationVisitor undecoratedVisitor = getUndecoratedVisitor();
- result = typedElement.accept(undecoratedVisitor);
+ result = typedElement.accept(symbolicEvaluationVisitor);
}
catch (InvalidValueException e) {
result = e;
@@ -253,21 +211,9 @@
refinedValue = getKnownValue(boxedValue);
}
if (SymbolicAnalysis.HYPOTHESIS.isActive()) {
-// refinedValue.toString(); // XXX
SymbolicAnalysis.HYPOTHESIS.println(" evaluated: \"" + typedElement + "\" as: " + refinedValue);
}
- /* catch (Exception e) {
- // This is a backstop. Library operations should catch their own exceptions
- // and produce a better reason as a result.
- result = new InvalidValueException(e, PivotMessagesInternal.FailedToEvaluate_ERROR_, element, "-", "-");
- }
- catch (AssertionError e) {
- // This is a backstop. Library operations should catch their own exceptions
- // and produce a better reason as a result.
- result = new InvalidValueException(e, PivotMessagesInternal.FailedToEvaluate_ERROR_, element, "-", "-");
- throw e;
- } */
- CSEElement cseElement = getSymbolicAnalysis().getCSEElement(typedElement);
+ CSEElement cseElement = symbolicAnalysis.getCSEElement(typedElement);
return traceSymbolicValue(cseElement, refinedValue); // Record new value
}
@@ -275,8 +221,7 @@
SymbolicValue unrefinedValue = getSymbolicValue(typedElement); // Get the unrefined value
Object result;
try {
- EvaluationVisitor undecoratedVisitor = getUndecoratedVisitor();
- result = typedElement.accept(undecoratedVisitor);
+ result = typedElement.accept(symbolicEvaluationVisitor);
}
catch (InvalidValueException e) {
result = e;
@@ -329,24 +274,8 @@
@Override
public @NonNull SymbolicValue traceSymbolicValue(@NonNull CSEElement cseElement, @NonNull SymbolicValue symbolicValue) {
- if ("self.name".equals(cseElement.toString())) {
- getClass(); // XXX
- }
SymbolicValue old = cseElement2symbolicValue.put(cseElement, symbolicValue);
assert (old == null) || (old == symbolicValue); //old.equals(symbolicValue);
return symbolicValue;
}
-
-// @Override
- public @NonNull SymbolicValue traceValue(@NonNull CSEElement cseElement, @Nullable Object value) {
- SymbolicValue symbolicValue;
- if (value instanceof SymbolicValue) {
- symbolicValue = (SymbolicValue) value;
- }
- else {
- Object boxedValue = environmentFactory.getIdResolver().boxedValueOf(value);
- symbolicValue = getKnownValue(boxedValue);
- }
- return traceSymbolicValue(cseElement, symbolicValue);
- }
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
index 709a29f..7274840 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
@@ -273,7 +273,6 @@
variable2value.put((VariableDeclaration)referredVariable, value);
}
-
/**
* Returns a string representation of the bindings
*/
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/Hypothesis.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/Hypothesis.java
index 3e8abd3..f256dfa 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/Hypothesis.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/Hypothesis.java
@@ -74,10 +74,10 @@
// SymbolicAnalysis.HYPOTHESIS.println(this.toString());
// SymbolicAnalysis.HYPOTHESIS.println(this.toString());
}
- HypothesizedSymbolicEvaluationEnvironment hypothesizedEvaluationEnvironment = symbolicAnalysis.createHypothesizedSymbolicEvaluationEnvironment(this);
- symbolicAnalysis.pushEvaluationEnvironment(hypothesizedEvaluationEnvironment);
+ BaseSymbolicEvaluationEnvironment baseSymbolicEvaluationEnvironment = symbolicAnalysis.getBaseSymbolicEvaluationEnvironment();
+ HypothesizedSymbolicEvaluationEnvironment hypothesizedEvaluationEnvironment = baseSymbolicEvaluationEnvironment.pushHypothesis(this);
isContradiction = hypothesizedEvaluationEnvironment.isContradiction();
- symbolicAnalysis.popEvaluationEnvironment();
+ baseSymbolicEvaluationEnvironment.popHypothesis();
if (isContradiction()) {
refine();
// SymbolicReEvaluationEnvironment refinedEvaluationEnvironment = symbolicAnalysis.createSymbolicReEvaluationEnvironment(this);
@@ -172,7 +172,7 @@
// else if (typeId instanceof MapTypeId) {
// return AbstractRefinedSymbolicValue.createZeroValue(originalValue);
// }
- return symbolicAnalysis.getSymbolicEvaluationEnvironment().getKnownValue(ValueUtil.ZERO_VALUE);
+ return symbolicAnalysis.getKnownValue(ValueUtil.ZERO_VALUE);
}
private static @NonNull SymbolicValue createHypothesizedValue(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull SymbolicValue originalValue) {
@@ -182,7 +182,7 @@
if (!sizeValue.isZero()) {
if (refinedValue == null) {
refinedValue = new SymbolicRefinedContentValue(originalValue);
- sizeValue = symbolicAnalysis.getSymbolicEvaluationEnvironment().getKnownValue(ValueUtil.ZERO_VALUE);
+ sizeValue = symbolicAnalysis.getKnownValue(ValueUtil.ZERO_VALUE);
refinedValue.setSize(sizeValue);
// refinedValue.toString();
}
@@ -234,7 +234,7 @@
public static class MayBeInvalidHypothesis extends Hypothesis
{
public MayBeInvalidHypothesis(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull TypedElement typedElement, @NonNull SymbolicValue originalValue) {
- super(symbolicAnalysis, typedElement, originalValue, symbolicAnalysis.getSymbolicEvaluationEnvironment().getKnownValue(ValueUtil.INVALID_VALUE));
+ super(symbolicAnalysis, typedElement, originalValue, symbolicAnalysis.getKnownValue(ValueUtil.INVALID_VALUE));
}
@Override
@@ -270,7 +270,7 @@
public static class MayBeNullHypothesis extends Hypothesis
{
public MayBeNullHypothesis(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull TypedElement typedElement, @NonNull SymbolicValue originalValue) {
- super(symbolicAnalysis, typedElement, originalValue, symbolicAnalysis.getSymbolicEvaluationEnvironment().getKnownValue(null));
+ super(symbolicAnalysis, typedElement, originalValue, symbolicAnalysis.getKnownValue(null));
}
@Override
@@ -344,7 +344,7 @@
// else if (typeId instanceof MapTypeId) {
// return AbstractRefinedSymbolicValue.createZeroValue(originalValue);
// }
- return symbolicAnalysis.getSymbolicEvaluationEnvironment().getKnownValue(ValueUtil.ZERO_VALUE);
+ return symbolicAnalysis.getKnownValue(ValueUtil.ZERO_VALUE);
}
public MayBeZeroHypothesis(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull TypedElement typedElement, @NonNull SymbolicValue originalValue) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/HypothesizedSymbolicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/HypothesizedSymbolicEvaluationEnvironment.java
index 11adcc0..88bc922 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/HypothesizedSymbolicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/HypothesizedSymbolicEvaluationEnvironment.java
@@ -32,7 +32,6 @@
import org.eclipse.ocl.pivot.TypedElement;
import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.VariableExp;
-import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
import org.eclipse.ocl.pivot.internal.symbolic.AbstractSymbolicRefinedValue;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicStatus;
@@ -43,7 +42,6 @@
import org.eclipse.ocl.pivot.library.logical.BooleanImpliesOperation2;
import org.eclipse.ocl.pivot.library.logical.BooleanOrOperation;
import org.eclipse.ocl.pivot.library.logical.BooleanOrOperation2;
-import org.eclipse.ocl.pivot.utilities.ClassUtil;
import org.eclipse.ocl.pivot.utilities.NameUtil;
import org.eclipse.ocl.pivot.utilities.PivotUtil;
import org.eclipse.ocl.pivot.utilities.StringUtil;
@@ -61,6 +59,7 @@
*/
public class HypothesizedSymbolicEvaluationEnvironment extends AbstractSymbolicEvaluationEnvironment
{
+ protected final @NonNull BaseSymbolicEvaluationEnvironment baseSymbolicEvaluationEnvironment;
protected final @NonNull Hypothesis hypothesis;
/**
@@ -85,8 +84,9 @@
*/
private final @NonNull Map<@NonNull TypedElement, @NonNull SymbolicValue> refinedTypedElements2symbolicValue = new HashMap<>();
- public HypothesizedSymbolicEvaluationEnvironment(@NonNull BaseSymbolicEvaluationEnvironment evaluationEnvironment, @NonNull Hypothesis hypothesis) {
- super(evaluationEnvironment, hypothesis.getTypedElement());
+ public HypothesizedSymbolicEvaluationEnvironment(@NonNull BaseSymbolicEvaluationEnvironment baseSymbolicEvaluationEnvironment, @NonNull Hypothesis hypothesis) {
+ super(baseSymbolicEvaluationEnvironment.getSymbolicAnalysis(), hypothesis.getTypedElement());
+ this.baseSymbolicEvaluationEnvironment = baseSymbolicEvaluationEnvironment;
this.hypothesis = hypothesis;
installHypothesis();
}
@@ -136,14 +136,14 @@
}
}
if (refinedBooleanValue == null) {
- SymbolicValue baseSymbolicValue = getBaseSymbolicValue(refinedExpression);
+ SymbolicValue baseSymbolicValue = baseSymbolicEvaluationEnvironment.getSymbolicValue(refinedExpression);
refinedSymbolicValue = AbstractSymbolicRefinedValue.createNotInvalidOrNullValue(baseSymbolicValue);
}
}
else if (containingTypedElement instanceof NavigationCallExp) {
NavigationCallExp navigationCallExp = (NavigationCallExp)containingTypedElement;
refinedExpression = PivotUtil.getOwnedSource(navigationCallExp);
- SymbolicValue baseSymbolicValue = getBaseSymbolicValue(refinedExpression);
+ SymbolicValue baseSymbolicValue = baseSymbolicEvaluationEnvironment.getSymbolicValue(refinedExpression);
refinedSymbolicValue = AbstractSymbolicRefinedValue.createNotInvalidOrNullValue(baseSymbolicValue);
}
else if (containingTypedElement instanceof LoopExp) {
@@ -155,7 +155,7 @@
// XXX isSafe
}
refinedExpression = PivotUtil.getOwnedSource(loopExp);
- SymbolicValue baseSymbolicValue = getBaseSymbolicValue(refinedExpression);
+ SymbolicValue baseSymbolicValue = baseSymbolicEvaluationEnvironment.getSymbolicValue(refinedExpression);
refinedSymbolicValue = AbstractSymbolicRefinedValue.createNotInvalidOrNullValue(baseSymbolicValue);
}
if (refinedExpression != null) {
@@ -164,7 +164,6 @@
refinedSymbolicValue = getKnownValue(refinedBooleanValue);
}
if (refinedSymbolicValue != null) {
-// putHypothesizedValue(refinedExpression, refinedSymbolicValue, false);
SymbolicValue old = refinedTypedElements2symbolicValue.put(refinedExpression, refinedSymbolicValue);
assert old == null;
}
@@ -208,21 +207,10 @@
@Override
@NonNull
public BaseSymbolicEvaluationEnvironment getBaseSymbolicEvaluationEnvironment() {
- return getParent().getBaseSymbolicEvaluationEnvironment();
- }
-
- @Override
- public @NonNull AbstractSymbolicEvaluationEnvironment getParent() {
- return ClassUtil.nonNullState(super.getParent());
- }
-
- @Override
- public @Nullable Object getValueOf(@NonNull TypedElement referredVariable) {
- return getSymbolicValue(referredVariable); // Re-use old value
+ return baseSymbolicEvaluationEnvironment;
}
private void installHypothesis() {
- SymbolicAnalysis symbolicAnalysis = getSymbolicAnalysis();
//
// Install the directly hypothesized expression.
//
@@ -301,7 +289,7 @@
public boolean isContradiction() {
List<@NonNull TypedElement> affectedTypedElementsList = new ArrayList<>(affectedTypedElements);
if (affectedTypedElementsList.size() > 1) {
- Collections.sort(affectedTypedElementsList, getSymbolicAnalysis().getTypedElementHeightComparator());
+ Collections.sort(affectedTypedElementsList, symbolicAnalysis.getTypedElementHeightComparator());
}
for (@NonNull TypedElement affectedTypedElement : affectedTypedElementsList) {
boolean isCompatible = symbolicReEvaluate(affectedTypedElement);
@@ -311,7 +299,7 @@
}
List<@NonNull TypedElement> typedElementsList = new ArrayList<>(refinedTypedElements2symbolicValue.keySet());
if (typedElementsList.size() > 1) {
- Collections.sort(typedElementsList, getSymbolicAnalysis().getTypedElementHeightComparator());
+ Collections.sort(typedElementsList, symbolicAnalysis.getTypedElementHeightComparator());
}
for (@NonNull TypedElement typedElement : typedElementsList) {
boolean isCompatible = symbolicReEvaluate(typedElement);
@@ -338,8 +326,7 @@
public boolean symbolicReEvaluate(@NonNull TypedElement typedElement) {
Object result = null;
try {
- EvaluationVisitor undecoratedVisitor = getUndecoratedVisitor();
- result = typedElement.accept(undecoratedVisitor);
+ result = symbolicEvaluationVisitor.symbolicEvaluate(typedElement);
}
catch (InvalidValueException e) {
result = e;
@@ -357,7 +344,7 @@
}
SymbolicValue readValue = basicGetSymbolicValue(typedElement); // Get the 'read' value
if (readValue == null) { // If a new evaluation
- CSEElement cseElement = getSymbolicAnalysis().getCSEElement(typedElement);
+ CSEElement cseElement = symbolicAnalysis.getCSEElement(typedElement);
traceSymbolicValue(cseElement, writeValue); // Record re-evaluated value
return true;
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicAnalysis.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicAnalysis.java
index fa437a1..1fb0b3b 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicAnalysis.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicAnalysis.java
@@ -23,25 +23,23 @@
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.Element;
import org.eclipse.ocl.pivot.ExpressionInOCL;
-import org.eclipse.ocl.pivot.NamedElement;
-import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.Type;
import org.eclipse.ocl.pivot.TypedElement;
import org.eclipse.ocl.pivot.Variable;
-import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment.EvaluationEnvironmentExtension;
import org.eclipse.ocl.pivot.evaluation.EvaluationHaltedException;
-import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor.EvaluationVisitorExtension;
+import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
import org.eclipse.ocl.pivot.evaluation.ModelManager;
import org.eclipse.ocl.pivot.ids.CollectionTypeId;
import org.eclipse.ocl.pivot.ids.MapTypeId;
import org.eclipse.ocl.pivot.ids.TypeId;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
import org.eclipse.ocl.pivot.internal.cse.CommonSubExpressionAnalysis;
-import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicContent;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicContent.SymbolicCollectionContent;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicContent.SymbolicMapContent;
import org.eclipse.ocl.pivot.internal.symbolic.SymbolicKnownValue;
+import org.eclipse.ocl.pivot.internal.symbolic.SymbolicUnknownValue;
+import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal;
import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal.EnvironmentFactoryInternalExtension;
import org.eclipse.ocl.pivot.util.PivotPlugin;
import org.eclipse.ocl.pivot.utilities.PivotUtil;
@@ -58,14 +56,18 @@
/**
* @since 1.16
*/
-public class SymbolicAnalysis extends BasicOCLExecutor implements SymbolicExecutor, ExecutorInternal
+public class SymbolicAnalysis /*extends BasicOCLExecutor implements SymbolicExecutor, ExecutorInternal*/
{
public static final @NonNull TracingOption HYPOTHESIS = new TracingOption(PivotPlugin.PLUGIN_ID, "symbolic/hypothesis");
- private @Nullable List<@NonNull HypothesizedSymbolicEvaluationEnvironment> hypothesizedEvaluationEnvironments = null;
-
+ private final @NonNull BasicOCLExecutor executor;
+ protected final EnvironmentFactoryInternal.@NonNull EnvironmentFactoryInternalExtension environmentFactory;
protected final @NonNull ExpressionInOCL expressionInOCL;
protected final @NonNull CommonSubExpressionAnalysis cseAnalysis;
+ protected final @NonNull BaseSymbolicEvaluationEnvironment baseSymbolicEvaluationEnvironment;
+ private final @NonNull EvaluationVisitor evaluationVisitor;
+ private @Nullable List<@NonNull HypothesizedSymbolicEvaluationEnvironment> hypothesizedEvaluationEnvironments = null;
+
/**
* The known symbolic value of known literal values.
@@ -73,6 +75,11 @@
private @NonNull Map<@Nullable Object, org.eclipse.ocl.pivot.internal.symbolic.SymbolicKnownValue> knownValue2symbolicValue = new HashMap<>();
/**
+ * The maybe-invalid symbolic value of known TYpeIds.
+ */
+ private @NonNull Map<@NonNull TypeId, org.eclipse.ocl.pivot.internal.symbolic.SymbolicUnknownValue> typeid2symbolicValue = new HashMap<>();
+
+ /**
* The expressions for which contradicting a hypothesized value allows a more precise re-evaluation.
*/
private @Nullable Map<@NonNull TypedElement, @NonNull List<@NonNull Hypothesis>> typedElement2hypotheses = null;
@@ -93,12 +100,14 @@
* Initializes the symbolic analysis of expressionInOCL that delegates to a non-symbolic evaluation visitor.
*/
public SymbolicAnalysis(@NonNull ExpressionInOCL expressionInOCL, @NonNull EnvironmentFactoryInternalExtension environmentFactory, @NonNull ModelManager modelManager) {
- super(environmentFactory, modelManager);
+ this.executor = new BasicOCLExecutor(environmentFactory, modelManager);
+ this.environmentFactory = environmentFactory;
this.expressionInOCL = expressionInOCL;
this.cseAnalysis = new CommonSubExpressionAnalysis();
+ this.evaluationVisitor = executor.createEvaluationVisitor();
+ this.baseSymbolicEvaluationEnvironment = new BaseSymbolicEvaluationEnvironment(this, expressionInOCL);
}
- @Override
public void addHypothesis(@NonNull TypedElement typedElement, @NonNull Hypothesis hypothesis) {
List<@NonNull Hypothesis> hypotheses = getHypotheses(typedElement);
hypotheses.add(hypothesis);
@@ -134,14 +143,6 @@
}
}
-/* public void addMayBeSmallerThanHypothesis(@NonNull TypedElement typedElement, @NonNull SymbolicValue symbolicValue, @NonNull SymbolicValue minSizeValue) {
- Hypothesis hypothesis = getHypotheses(typedElement, Hypothesis.MayBeSmallerThanHypothesis.class); // minSIze
- if (hypothesis == null) {
- hypothesis = new Hypothesis.MayBeSmallerThanHypothesis(this, typedElement, symbolicValue, minSizeValue);
- addHypothesis(typedElement, hypothesis);
- }
- } */
-
public void addMayBeZeroHypothesis(@NonNull TypedElement typedElement, @NonNull SymbolicValue symbolicValue) {
Hypothesis hypothesis = getHypotheses(typedElement, Hypothesis.MayBeZeroHypothesis.class);
if (hypothesis == null) {
@@ -150,17 +151,13 @@
}
}
- @Override
- protected @NonNull EvaluationVisitorExtension createEvaluationVisitor() {
- EvaluationVisitorExtension evaluationVisitor = super.createEvaluationVisitor();
- SymbolicEvaluationVisitor symbolicEvaluationVisitor = new SymbolicEvaluationVisitor(evaluationVisitor);
+ public @NonNull SymbolicEvaluationVisitor createSymbolicEvaluationVisitor(@NonNull SymbolicEvaluationEnvironment symbolicEvaluationEnvironment) {
+ SymbolicEvaluationVisitor symbolicEvaluationVisitor = new SymbolicEvaluationVisitor(this, evaluationVisitor, symbolicEvaluationEnvironment);
return symbolicEvaluationVisitor;
}
- @Override
public @NonNull HypothesizedSymbolicEvaluationEnvironment createHypothesizedSymbolicEvaluationEnvironment(@NonNull Hypothesis hypothesis) {
- BaseSymbolicEvaluationEnvironment evaluationEnvironment = (BaseSymbolicEvaluationEnvironment) getEvaluationEnvironment();
- HypothesizedSymbolicEvaluationEnvironment hypothesizedEvaluationEnvironment = new HypothesizedSymbolicEvaluationEnvironment(evaluationEnvironment, hypothesis);
+ HypothesizedSymbolicEvaluationEnvironment hypothesizedEvaluationEnvironment = new HypothesizedSymbolicEvaluationEnvironment(baseSymbolicEvaluationEnvironment, hypothesis);
List<@NonNull HypothesizedSymbolicEvaluationEnvironment> hypothesizedEvaluationEnvironments2 = hypothesizedEvaluationEnvironments;
if (hypothesizedEvaluationEnvironments2 == null) {
hypothesizedEvaluationEnvironments = hypothesizedEvaluationEnvironments2 = new ArrayList<>();
@@ -169,27 +166,12 @@
return hypothesizedEvaluationEnvironment;
}
- @Override
- protected @NonNull EvaluationEnvironmentExtension createNestedEvaluationEnvironment(
- @NonNull EvaluationEnvironmentExtension evaluationEnvironment,
- @NonNull NamedElement executableObject, @Nullable Object caller) {
- // TODO Auto-generated method stub
- return super.createNestedEvaluationEnvironment(evaluationEnvironment, executableObject, caller);
+ public @NonNull SymbolicUnknownValue createUnknownValue(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalid) {
+ return new SymbolicUnknownValue(createVariableName(), typeId, mayBeNull, mayBeInvalid);
}
- @Override
- protected @NonNull EvaluationEnvironmentExtension createNestedEvaluationEnvironment(
- @NonNull EvaluationEnvironmentExtension evaluationEnvironment,
- @NonNull NamedElement executableObject,
- @Nullable OCLExpression callingObject) {
- // TODO Auto-generated method stub
- return super.createNestedEvaluationEnvironment(evaluationEnvironment,
- executableObject, callingObject);
- }
-
- @Override
- protected @NonNull AbstractSymbolicEvaluationEnvironment createRootEvaluationEnvironment(@NonNull NamedElement executableObject) {
- return new BaseSymbolicEvaluationEnvironment(this, executableObject);
+ public @NonNull SymbolicValue createUnknownValue(@NonNull TypedElement typedElement, boolean mayBeNull, boolean mayBeInvalid) {
+ return createUnknownValue(typedElement.getTypeId(), mayBeNull, mayBeInvalid);
}
public @NonNull String createVariableName() {
@@ -197,16 +179,19 @@
}
public @NonNull BaseSymbolicEvaluationEnvironment getBaseSymbolicEvaluationEnvironment() {
- return getSymbolicEvaluationEnvironment().getBaseSymbolicEvaluationEnvironment();
+ return baseSymbolicEvaluationEnvironment;
}
public @NonNull CSEElement getCSEElement(@NonNull Element element) {
return cseAnalysis.getElementCSE(element);
}
- @Override
- public @NonNull AbstractSymbolicEvaluationEnvironment getSymbolicEvaluationEnvironment() {
- return (AbstractSymbolicEvaluationEnvironment)super.getEvaluationEnvironment();
+ public @NonNull EnvironmentFactoryInternal getEnvironmentFactory() {
+ return environmentFactory;
+ }
+
+ public @NonNull ExecutorInternal getExecutor() {
+ return executor;
}
private @Nullable Hypothesis getHypotheses(@NonNull TypedElement typedElement, @NonNull Class<?> hypothesisClass) {
@@ -247,7 +232,7 @@
}
}
if (symbolicKnownValue == null) {
- Type type = getEnvironmentFactory().getIdResolver().getStaticTypeOfValue(null, boxedValue);
+ Type type = environmentFactory.getIdResolver().getStaticTypeOfValue(null, boxedValue);
String constantName = "k#" + constantCounter++;
TypeId typeId = type.getTypeId();
SymbolicContent content = null;
@@ -268,37 +253,42 @@
return symbolicKnownValue;
}
+ public @Nullable SymbolicValue getMayBeInvalidValue(@NonNull TypeId typeid) {
+ SymbolicUnknownValue symbolicUnknownValue = typeid2symbolicValue.get(typeid);
+ if (symbolicUnknownValue == null) {
+ symbolicUnknownValue = createUnknownValue(typeid, false, true);
+ typeid2symbolicValue.put(typeid, symbolicUnknownValue);
+ }
+ return symbolicUnknownValue;
+ }
+
+ public @NonNull SymbolicEvaluationEnvironment getSymbolicEvaluationEnvironment() {
+ return baseSymbolicEvaluationEnvironment.getSymbolicEvaluationEnvironment();
+ }
+
public @NonNull Comparator<@NonNull TypedElement> getTypedElementHeightComparator() {
return cseAnalysis.getTypedElementHeightComparator();
}
public void initializeEvaluationEnvironment(@NonNull ExpressionInOCL expressionInOCL, @Nullable Object selfObject, @Nullable Object resultObject, @Nullable Object @Nullable [] parameters) {
- initializeEvaluationEnvironment(expressionInOCL);
+ executor.initializeEvaluationEnvironment(expressionInOCL);
cseAnalysis.analyze(expressionInOCL);
- BaseSymbolicEvaluationEnvironment evaluationEnvironment = getBaseSymbolicEvaluationEnvironment();
- // IdResolver idResolver = environmentFactory.getIdResolver();
Variable contextVariable = expressionInOCL.getOwnedContext();
if (contextVariable != null) {
- // Object contextValue = idResolver.boxedValueOf(contextElement);
- // evaluationEnvironment.add(contextVariable, contextValue);
CSEElement cseElement = getCSEElement(contextVariable);
- evaluationEnvironment.traceValue(cseElement, selfObject);
+ traceValue(cseElement, selfObject);
}
Variable resultVariable = expressionInOCL.getOwnedResult();
if (resultVariable != null) {
- // Object contextValue = idResolver.boxedValueOf(contextElement);
- // evaluationEnvironment.add(contextVariable, contextValue);
CSEElement cseElement = getCSEElement(resultVariable);
- evaluationEnvironment.traceValue(cseElement, resultObject);
+ traceValue(cseElement, resultObject);
}
int i = 0;
assert parameters != null;
for (Variable parameterVariable : PivotUtil.getOwnedParameters(expressionInOCL)) {
Object parameter = parameters[i++];
- // Object parameterValue = idResolver.boxedValueOf(parameter);
- // evaluationEnvironment.add(parameterVariable, parameterValue);
CSEElement cseElement = getCSEElement(parameterVariable);
- evaluationEnvironment.traceValue(cseElement, parameter);
+ traceValue(cseElement, parameter);
}
}
@@ -329,13 +319,16 @@
throw new UnsupportedOperationException();
} */
+ private boolean isCanceled() {
+ return executor.isCanceled();
+ }
+
protected void resolveHypotheses() {
Map<@NonNull TypedElement, @NonNull List<@NonNull Hypothesis>> typedElement2hypotheses2 = typedElement2hypotheses;
if (typedElement2hypotheses2 != null) {
if (SymbolicAnalysis.HYPOTHESIS.isActive()) {
SymbolicAnalysis.HYPOTHESIS.println(" resolving hypotheses");
}
- // AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
List<@NonNull Hypothesis> hypotheses = new ArrayList<>(allHypotheses);
if (hypotheses.size() > 1) {
Collections.sort(hypotheses);
@@ -363,7 +356,7 @@
}
}
Collections.sort(typedElements, getTypedElementHeightComparator());
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getSymbolicEvaluationEnvironment();
+ SymbolicEvaluationEnvironment evaluationEnvironment = getSymbolicEvaluationEnvironment();
for (@NonNull TypedElement typedElement : typedElements) {
evaluationEnvironment.symbolicEvaluate(typedElement);
}
@@ -410,4 +403,17 @@
}
return s.toString();
}
+
+ private @NonNull SymbolicValue traceValue(@NonNull CSEElement cseElement, @Nullable Object value) {
+ SymbolicValue symbolicValue;
+ if (value instanceof SymbolicValue) {
+ symbolicValue = (SymbolicValue) value;
+ }
+ else {
+ Object boxedValue = environmentFactory.getIdResolver().boxedValueOf(value);
+ symbolicValue = getKnownValue(boxedValue);
+ }
+ BaseSymbolicEvaluationEnvironment evaluationEnvironment = getBaseSymbolicEvaluationEnvironment();
+ return evaluationEnvironment.traceSymbolicValue(cseElement, symbolicValue);
+ }
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationEnvironment.java
index a1873d4..cff3993 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationEnvironment.java
@@ -16,18 +16,18 @@
import org.eclipse.ocl.pivot.Element;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.TypedElement;
-import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
import org.eclipse.ocl.pivot.ids.TypeId;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
+import org.eclipse.ocl.pivot.utilities.EnvironmentFactory;
import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
*
* @since 1.16
*/
-public interface SymbolicEvaluationEnvironment extends EvaluationEnvironment.EvaluationEnvironmentExtension
+public interface SymbolicEvaluationEnvironment
{
- // @NonNull SymbolicValue traceValue(@NonNull CSEElement cseElement, @Nullable Object value);
+ @Nullable SymbolicValue basicGetSymbolicValue(@NonNull Element element);
/**
* Return a SymbolicKnownValue for invalid, if typedElement is a collection and empty.
@@ -51,21 +51,17 @@
@Nullable SymbolicValue checkNotNull(@NonNull TypedElement typedElement, @NonNull TypeId typeId);
/**
- * Return a SymbolicKnownValue for invalid, if typedElement is a collection whose size may bee smaller than minSize.
- * Else return null .
- */
-// @Nullable SymbolicValue checkNotSmallerThan(@NonNull TypedElement typedElement, @NonNull SymbolicValue minSizeValue, @NonNull TypeId typeId);
-
- /**
* Return a SymbolicKnownValue for invalid, if typedElement isZero.
* Else return a mayBeNull SymbolicUnknownValue for typeId if typedElement mayBeZero.
* Else return null if typedElement is not zero.
*/
@Nullable SymbolicValue checkNotZero(@NonNull TypedElement typedElement, @NonNull TypeId typeId);
+ @NonNull SymbolicValue createUnknownValue(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalidOrNull);
@NonNull SymbolicValue createUnknownValue(@NonNull TypedElement typedElement, boolean mayBeNull, boolean mayBeInvalid);
-
@NonNull BaseSymbolicEvaluationEnvironment getBaseSymbolicEvaluationEnvironment();
+ @NonNull EnvironmentFactory getEnvironmentFactory();
+ @NonNull ExecutorInternal getExecutor();
@NonNull SymbolicValue getKnownValue(@Nullable Object boxedValue);
@NonNull SymbolicAnalysis getSymbolicAnalysis();
@NonNull SymbolicValue getSymbolicValue(@NonNull Element element);
@@ -80,5 +76,4 @@
void setDead(@NonNull OCLExpression expression);
@NonNull SymbolicValue symbolicEvaluate(@NonNull TypedElement element);
@NonNull SymbolicValue traceSymbolicValue(@NonNull CSEElement cseElement, @NonNull SymbolicValue symbolicValue);
-// @NonNull SymbolicValue traceValue(@NonNull CSEElement cseElement, @Nullable Object value);
}
\ No newline at end of file
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
index 44eeefc..be9fabb 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
@@ -14,15 +14,18 @@
import java.util.List;
import org.eclipse.jdt.annotation.NonNull;
-import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.BooleanLiteralExp;
import org.eclipse.ocl.pivot.CollectionItem;
import org.eclipse.ocl.pivot.CollectionLiteralExp;
import org.eclipse.ocl.pivot.CollectionLiteralPart;
import org.eclipse.ocl.pivot.CollectionRange;
import org.eclipse.ocl.pivot.CollectionType;
import org.eclipse.ocl.pivot.Element;
+import org.eclipse.ocl.pivot.EnumLiteralExp;
import org.eclipse.ocl.pivot.ExpressionInOCL;
import org.eclipse.ocl.pivot.IfExp;
+import org.eclipse.ocl.pivot.IntegerLiteralExp;
+import org.eclipse.ocl.pivot.InvalidLiteralExp;
import org.eclipse.ocl.pivot.Iteration;
import org.eclipse.ocl.pivot.IteratorVariable;
import org.eclipse.ocl.pivot.LetExp;
@@ -30,7 +33,9 @@
import org.eclipse.ocl.pivot.LoopExp;
import org.eclipse.ocl.pivot.MapLiteralExp;
import org.eclipse.ocl.pivot.MapLiteralPart;
+import org.eclipse.ocl.pivot.MapType;
import org.eclipse.ocl.pivot.NavigationCallExp;
+import org.eclipse.ocl.pivot.NullLiteralExp;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.Operation;
import org.eclipse.ocl.pivot.OperationCallExp;
@@ -39,22 +44,25 @@
import org.eclipse.ocl.pivot.ParameterVariable;
import org.eclipse.ocl.pivot.Property;
import org.eclipse.ocl.pivot.PropertyCallExp;
+import org.eclipse.ocl.pivot.RealLiteralExp;
+import org.eclipse.ocl.pivot.ResultVariable;
import org.eclipse.ocl.pivot.ShadowExp;
import org.eclipse.ocl.pivot.ShadowPart;
+import org.eclipse.ocl.pivot.StringLiteralExp;
import org.eclipse.ocl.pivot.TupleLiteralExp;
import org.eclipse.ocl.pivot.TupleLiteralPart;
import org.eclipse.ocl.pivot.Type;
-import org.eclipse.ocl.pivot.TypedElement;
-import org.eclipse.ocl.pivot.VariableDeclaration;
+import org.eclipse.ocl.pivot.TypeExp;
+import org.eclipse.ocl.pivot.UnlimitedNaturalLiteralExp;
+import org.eclipse.ocl.pivot.Variable;
+import org.eclipse.ocl.pivot.VariableExp;
import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
-import org.eclipse.ocl.pivot.evaluation.Executor;
import org.eclipse.ocl.pivot.ids.CollectionTypeId;
import org.eclipse.ocl.pivot.ids.IdResolver;
import org.eclipse.ocl.pivot.ids.TypeId;
import org.eclipse.ocl.pivot.internal.complete.StandardLibraryInternal;
import org.eclipse.ocl.pivot.internal.cse.CSEElement;
import org.eclipse.ocl.pivot.internal.manager.PivotMetamodelManager;
-import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.internal.symbolic.AbstractLeafSymbolicValue.SymbolicNavigationCallValue;
import org.eclipse.ocl.pivot.internal.symbolic.AbstractSymbolicRefinedValue;
import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal;
@@ -62,8 +70,9 @@
import org.eclipse.ocl.pivot.library.LibraryIteration;
import org.eclipse.ocl.pivot.library.LibraryOperation;
import org.eclipse.ocl.pivot.messages.PivotMessages;
+import org.eclipse.ocl.pivot.util.AbstractExtendingVisitor;
+import org.eclipse.ocl.pivot.util.Visitable;
import org.eclipse.ocl.pivot.utilities.ClassUtil;
-import org.eclipse.ocl.pivot.utilities.MetamodelManager;
import org.eclipse.ocl.pivot.utilities.PivotUtil;
import org.eclipse.ocl.pivot.utilities.StringUtil;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
@@ -72,62 +81,58 @@
import org.eclipse.ocl.pivot.values.InvalidValueException;
import org.eclipse.ocl.pivot.values.SymbolicValue;
-import com.google.common.collect.Lists;
-
/**
* A symbolic evaluation decorator for an evaluation visitor.
*
* @since 1.16
*/
-public class SymbolicEvaluationVisitor extends EvaluationVisitorDecorator implements EvaluationVisitor.EvaluationVisitorExtension
+public class SymbolicEvaluationVisitor extends AbstractExtendingVisitor<@NonNull SymbolicValue, @NonNull SymbolicAnalysis>
{
+ protected final @NonNull EvaluationVisitor evaluationVisitor;
protected final @NonNull EnvironmentFactoryInternal environmentFactory;
protected final @NonNull IdResolver idResolver;
protected final @NonNull StandardLibraryInternal standardLibrary;
+ protected final @NonNull SymbolicEvaluationEnvironment symbolicEvaluationEnvironment;
/**
* Initializes the symbolic analysis that delegates to a non-symbolic evaluation visitor.
+ * @param symbolicEvaluationEnvironment
*/
- protected SymbolicEvaluationVisitor(@NonNull EvaluationVisitor visitor) {
- super(visitor);
- this.environmentFactory = (EnvironmentFactoryInternal) visitor.getEnvironmentFactory();
+ public SymbolicEvaluationVisitor(@NonNull SymbolicAnalysis symbolicAnalysis, @NonNull EvaluationVisitor evaluationVisitor, @NonNull SymbolicEvaluationEnvironment symbolicEvaluationEnvironment) {
+ super(symbolicAnalysis);
+ this.evaluationVisitor = evaluationVisitor;
+ this.environmentFactory = symbolicAnalysis.getEnvironmentFactory();
this.idResolver = environmentFactory.getIdResolver();
this.standardLibrary = environmentFactory.getStandardLibrary();
+ this.symbolicEvaluationEnvironment = symbolicEvaluationEnvironment;
}
- protected @Nullable Object doNavigationCallExp(@NonNull NavigationCallExp navigationCallExp) {
- Object result = null;
+ protected @NonNull SymbolicValue doNavigationCallExp(@NonNull NavigationCallExp navigationCallExp) {
Property referredProperty = PivotUtil.getReferredProperty(navigationCallExp);
OCLExpression source = PivotUtil.getOwnedSource(navigationCallExp);
-
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- SymbolicValue sourceValue = evaluationEnvironment.symbolicEvaluate(source);
- @SuppressWarnings("unused")
- List<@Nullable Object> sourceAndArgumentValues = Lists.newArrayList(sourceValue);
+ SymbolicValue sourceValue = symbolicEvaluationEnvironment.symbolicEvaluate(source);
TypeId returnTypeId = navigationCallExp.getTypeId();
- SymbolicValue invalidProblem = evaluationEnvironment.checkNotInvalid(source, returnTypeId);
+ SymbolicValue invalidProblem = symbolicEvaluationEnvironment.checkNotInvalid(source, returnTypeId);
if (invalidProblem != null) {
return invalidProblem;
}
if (sourceValue.isNull()) {
if (navigationCallExp.isIsSafe()) {
- return evaluationEnvironment.getKnownValue(null);
+ return context.getKnownValue(null);
}
else {
- return evaluationEnvironment.getKnownValue(ValueUtil.INVALID_VALUE);
+ return context.getKnownValue(ValueUtil.INVALID_VALUE);
}
}
if (!navigationCallExp.isIsSafe()) {
- SymbolicValue nullSourceProblem = evaluationEnvironment.checkNotNull(source, returnTypeId);
+ SymbolicValue nullSourceProblem = symbolicEvaluationEnvironment.checkNotNull(source, returnTypeId);
if (nullSourceProblem != null) {
return nullSourceProblem;
}
- // Hypothesis hypothesis = new Hypothesis.MayBeNullHypothesis(symbolicAnalysis, source, sourceValue);
- // symbolicAnalysis.addHypothesis(source, hypothesis);
- // return evaluationEnvironment.getMayBeInvalidValue(returnTypeId);
}
if (sourceValue.isKnown()) {
- result = context.internalExecuteNavigationCallExp(navigationCallExp, referredProperty, sourceValue.getKnownValue());
+ Object resultValue = context.getExecutor().internalExecuteNavigationCallExp(navigationCallExp, referredProperty, sourceValue.getKnownValue());
+ return context.getKnownValue(resultValue);
}
else {
boolean isSafe = navigationCallExp.isIsSafe();
@@ -137,15 +142,14 @@
boolean propertyMayBeNull = !referredProperty.isIsRequired();
boolean resultMayBeInvalid = sourceMayBeInvalid || (sourceMayBeNull && !isSafe && !sourceIsMany);
boolean resultMayBeNull = propertyMayBeNull || (sourceMayBeNull && isSafe && !sourceIsMany);
- result = new SymbolicNavigationCallValue(getSymbolicAnalysis().createVariableName(), navigationCallExp, resultMayBeNull, resultMayBeInvalid, sourceValue);
+ return new SymbolicNavigationCallValue(context.createVariableName(), navigationCallExp, resultMayBeNull, resultMayBeInvalid, sourceValue);
}
- return result;
}
/**
* @since 1.12
*/
- protected @Nullable Object doOperationCallExp(@NonNull OperationCallExp operationCallExp) {
+ protected @NonNull SymbolicValue doOperationCallExp(@NonNull OperationCallExp operationCallExp) {
Operation apparentOperation = PivotUtil.getReferredOperation(operationCallExp);
if ("first".equals(apparentOperation.getName())) {
getClass(); // XXX
@@ -155,14 +159,13 @@
//
// Resolve source value catching invalid values for validating operations.
//
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
OCLExpression source = operationCallExp.getOwnedSource();
SymbolicValue sourceValue;
if (source == null) { // Static functions may have null source
sourceValue = null;
}
else { //if (!isValidating) {
- sourceValue = evaluationEnvironment.symbolicEvaluate(source);
+ sourceValue = symbolicEvaluationEnvironment.symbolicEvaluate(source);
}
//
@SuppressWarnings("unused")
@@ -172,12 +175,12 @@
//
if (operationCallExp.isIsSafe() && (source != null)) {
if (sourceValue == null) {
- return null;
+ return context.getKnownValue(null);
}
if (sourceValue.isNull()) {
return sourceValue;
}
- SymbolicValue sourceProblem = evaluationEnvironment.checkNotNull(source, operationCallExp.getTypeId());
+ SymbolicValue sourceProblem = symbolicEvaluationEnvironment.checkNotNull(source, operationCallExp.getTypeId());
if (sourceProblem != null) {
return sourceProblem;
}
@@ -202,7 +205,7 @@
Type onlyType = onlyParameter.getType();
if (onlyType == standardLibrary.getOclSelfType()) {
List<@NonNull OCLExpression> arguments = ClassUtil.nullFree(operationCallExp.getOwnedArguments());
- SymbolicValue onlyArgumentValue = evaluationEnvironment.symbolicEvaluate(arguments.get(0));
+ SymbolicValue onlyArgumentValue = symbolicEvaluationEnvironment.symbolicEvaluate(arguments.get(0));
org.eclipse.ocl.pivot.Class actualArgType = idResolver.getStaticTypeOfValue(onlyType, onlyArgumentValue);
actualSourceType = (org.eclipse.ocl.pivot.Class)actualSourceType.getCommonType(idResolver, actualArgType);
// FIXME direct evaluate using second argument
@@ -212,244 +215,224 @@
actualOperation = actualSourceType.lookupActualOperation(standardLibrary, apparentOperation);
}
LibraryOperation implementation = (LibraryOperation)metamodelManager.getImplementation(actualOperation);
- return implementation.symbolicEvaluate(evaluationEnvironment, operationCallExp);
+ return implementation.symbolicEvaluate(symbolicEvaluationEnvironment, operationCallExp);
}
- @Deprecated /* @deprecated use symbolicEvaluate argument */
- public @Nullable Object evaluate(@NonNull Element element) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- SymbolicValue symbolicValue = evaluationEnvironment.symbolicEvaluate((TypedElement)element);
- if (symbolicValue.isKnown()) {
- return symbolicValue.getKnownValue();
+ public @NonNull SymbolicValue symbolicEvaluate(@NonNull Element element) {
+ try {
+ SymbolicValue resultValue = element.accept(this);
+ return resultValue;
}
- else {
- return symbolicValue;
- }
- }
-
- @Deprecated /* @deprecated use symbolicEvaluate argument */
- @Override
- public @Nullable Object evaluate(@NonNull OCLExpression expression) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- SymbolicValue symbolicValue = evaluationEnvironment.symbolicEvaluate(expression);
- if (symbolicValue.isKnown()) {
- return symbolicValue.getKnownValue();
- }
- else {
- return symbolicValue;
+ catch (InvalidValueException e) {
+ Object boxedValue = idResolver.boxedValueOf(e);
+ return context.getKnownValue(boxedValue);
}
}
@Override
- public @NonNull AbstractSymbolicEvaluationEnvironment getEvaluationEnvironment() {
- return (AbstractSymbolicEvaluationEnvironment)super.getEvaluationEnvironment();
- }
-
- /** @deprecated moved to Executor
- * @since 1.1*/
- @Override
- @Deprecated
- public @NonNull Executor getExecutor() {
- return ((EvaluationVisitor.EvaluationVisitorExtension)delegate).getExecutor();
- }
-
- /** @deprecated moved to Executor */
- @Override
- @Deprecated
- public @NonNull MetamodelManager getMetamodelManager() {
- return delegate.getMetamodelManager();
- }
-
- public @NonNull SymbolicAnalysis getSymbolicAnalysis() {
- assert context != null;
- return (SymbolicAnalysis)context;
- }
-
- public @NonNull SymbolicExecutor getSymbolicExecutor() {
- assert context != null;
- return (SymbolicExecutor)context;
+ public @NonNull SymbolicValue visitBooleanLiteralExp(@NonNull BooleanLiteralExp booleanLiteralExp) {
+ Object resultValue = evaluationVisitor.visitBooleanLiteralExp(booleanLiteralExp);
+ return context.getKnownValue(resultValue);
}
@Override
- public @Nullable Object visitCollectionItem(@NonNull CollectionItem item) {
- return getEvaluationEnvironment().symbolicEvaluate(PivotUtil.getOwnedItem(item));
+ public @NonNull SymbolicValue visitCollectionItem(@NonNull CollectionItem item) {
+ return symbolicEvaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedItem(item));
}
@Override
- public @Nullable Object visitCollectionLiteralExp(@NonNull CollectionLiteralExp literalExp) {
- Object result;
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitCollectionLiteralExp(@NonNull CollectionLiteralExp literalExp) {
+ final boolean isNullFree = ((CollectionType)literalExp.getType()).isIsNullFree();
+ boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
for (@NonNull CollectionLiteralPart part : PivotUtil.getOwnedParts(literalExp)) {
- Object partValue = evaluate(part);
- assert ValueUtil.isBoxed(partValue); // Make sure Integer/Real are boxed, invalid is an exception, null is null
- if (partValue instanceof SymbolicValue) {
- isSymbolic = true;
+ SymbolicValue partValue = symbolicEvaluate(part);
+ if (!partValue.isKnown()) {
+ isKnown = false;
}
- if (ValueUtil.mayBeInvalid(partValue)) {
+ if (partValue.mayBeInvalid()) {
mayBeInvalid = true;
}
- if (ValueUtil.mayBeNull(partValue)) {
+ if (isNullFree && ValueUtil.mayBeNull(partValue)) {
mayBeNull = true;
}
}
- if (isSymbolic) {
- result = getEvaluationEnvironment().createUnknownValue(literalExp, false, mayBeNull || mayBeInvalid);
+ if (isKnown) {
+ Object resultValue = evaluationVisitor.visitCollectionLiteralExp(literalExp);
+ return context.getKnownValue(resultValue);
}
else {
- result = delegate.visitCollectionLiteralExp(literalExp);
+ return context.createUnknownValue(literalExp, false, mayBeInvalid || mayBeNull);
}
- return result;
}
@Override
- public @Nullable Object visitCollectionRange(@NonNull CollectionRange range) {
- Object result;
+ public @NonNull SymbolicValue visitCollectionRange(@NonNull CollectionRange range) {
OCLExpression first = PivotUtil.getOwnedFirst(range);
OCLExpression last = PivotUtil.getOwnedLast(range);
- Object firstValue = evaluate(first);
- Object lastValue = evaluate(last);
- if ((firstValue instanceof SymbolicValue) || (lastValue instanceof SymbolicValue)) {
- boolean mayBeInvalid = ValueUtil.mayBeInvalid(firstValue) || ValueUtil.mayBeInvalid(firstValue);
- boolean mayBeNull = ValueUtil.mayBeNull(lastValue) || ValueUtil.mayBeNull(lastValue);
- result = getEvaluationEnvironment().createUnknownValue(range, false, mayBeNull || mayBeInvalid);
+ SymbolicValue firstValue = symbolicEvaluate(first);
+ SymbolicValue lastValue = symbolicEvaluate(last);
+ if (!firstValue.isKnown() || !lastValue.isKnown()) {
+ boolean mayBeInvalid = firstValue.mayBeInvalid() || firstValue.mayBeInvalid();
+ boolean mayBeNull = lastValue.mayBeNull() || lastValue.mayBeNull();
+ return context.createUnknownValue(range, false, mayBeNull || mayBeInvalid);
+ }
+ Object resultValue;
+ CollectionType type = (CollectionType) ((CollectionLiteralExp)range.eContainer()).getType();
+ CollectionTypeId typeId = type.getTypeId();
+ IntegerValue firstInteger = ValueUtil.asIntegerValue(firstValue);
+ IntegerValue lastInteger = ValueUtil.asIntegerValue(lastValue);
+ // construct a lazy integer list for the range
+ IntegerRange integerRange = ValueUtil.createRange(firstInteger, lastInteger);
+ if (type.isUnique()) {
+ resultValue = ValueUtil.createOrderedSetRange(typeId, integerRange);
}
else {
-// result = delegate.visitCollectionRange(range);
- CollectionType type = (CollectionType) ((CollectionLiteralExp)range.eContainer()).getType();
- CollectionTypeId typeId = type.getTypeId();
- IntegerValue firstInteger = ValueUtil.asIntegerValue(firstValue);
- IntegerValue lastInteger = ValueUtil.asIntegerValue(lastValue);
- // construct a lazy integer list for the range
- IntegerRange integerRange = ValueUtil.createRange(firstInteger, lastInteger);
- if (type.isUnique()) {
- return ValueUtil.createOrderedSetRange(typeId, integerRange);
- }
- else {
- return ValueUtil.createSequenceRange(typeId, integerRange);
- }
+ resultValue = ValueUtil.createSequenceRange(typeId, integerRange);
}
- return result;
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitEnumLiteralExp(@NonNull EnumLiteralExp enumLiteralExp) {
+ Object resultValue = evaluationVisitor.visitEnumLiteralExp(enumLiteralExp);
+ return context.getKnownValue(resultValue);
}
@Override
public @NonNull SymbolicValue visitExpressionInOCL(@NonNull ExpressionInOCL expression) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- return evaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedBody(expression));
+ return symbolicEvaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedBody(expression));
}
@Override
public @NonNull SymbolicValue visitIfExp(@NonNull IfExp ifExp) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
OCLExpression conditionExpression = PivotUtil.getOwnedCondition(ifExp);
OCLExpression thenExpression = PivotUtil.getOwnedThen(ifExp);
OCLExpression elseExpression = PivotUtil.getOwnedElse(ifExp);
- SymbolicValue conditionValue = evaluationEnvironment.symbolicEvaluate(conditionExpression);
+ SymbolicValue conditionValue = symbolicEvaluationEnvironment.symbolicEvaluate(conditionExpression);
if (conditionValue.isTrue()) {
- evaluationEnvironment.setDead(elseExpression);
- return evaluationEnvironment.symbolicEvaluate(thenExpression);
+ symbolicEvaluationEnvironment.setDead(elseExpression);
+ return symbolicEvaluationEnvironment.symbolicEvaluate(thenExpression);
}
else if (conditionValue.isFalse()) {
- evaluationEnvironment.setDead(thenExpression);
- return evaluationEnvironment.symbolicEvaluate(elseExpression);
+ symbolicEvaluationEnvironment.setDead(thenExpression);
+ return symbolicEvaluationEnvironment.symbolicEvaluate(elseExpression);
}
else {
boolean mayBeInvalid = conditionValue.mayBeInvalid();
boolean mayBeNull = conditionValue.mayBeNull();
- SymbolicValue thenValue = evaluationEnvironment.symbolicEvaluate(thenExpression);
+ SymbolicValue thenValue = symbolicEvaluationEnvironment.symbolicEvaluate(thenExpression);
if (thenValue.mayBeInvalid()) {
mayBeInvalid = true;
}
if (thenValue.mayBeNull()) {
mayBeNull = true;
}
- SymbolicValue elseValue = evaluationEnvironment.symbolicEvaluate(elseExpression);
+ SymbolicValue elseValue = symbolicEvaluationEnvironment.symbolicEvaluate(elseExpression);
if (elseValue.mayBeInvalid()) {
mayBeInvalid = true;
}
if (elseValue.mayBeNull()) {
mayBeNull = true;
}
- return evaluationEnvironment.createUnknownValue(ifExp, mayBeNull, mayBeInvalid);
+ return context.createUnknownValue(ifExp, mayBeNull, mayBeInvalid);
}
}
@Override
+ public @NonNull SymbolicValue visitIntegerLiteralExp(@NonNull IntegerLiteralExp integerLiteralExp) {
+ Object resultValue = evaluationVisitor.visitIntegerLiteralExp(integerLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitInvalidLiteralExp(@NonNull InvalidLiteralExp invalidLiteralExp) {
+ Object resultValue = evaluationVisitor.visitInvalidLiteralExp(invalidLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
public @NonNull SymbolicValue visitIteratorVariable(@NonNull IteratorVariable iteratorVariable) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
OCLExpression initExp = iteratorVariable.getOwnedInit();
if (initExp != null) {
- return evaluationEnvironment.symbolicEvaluate(initExp);
+ return symbolicEvaluationEnvironment.symbolicEvaluate(initExp);
}
else {
- // getEvaluationEnvironment().add(parameterVariable, parameterValue);
- CSEElement cseElement = getSymbolicAnalysis().getCSEElement(iteratorVariable);
- SymbolicValue symbolicValue = getEvaluationEnvironment().createUnknownValue(iteratorVariable, !iteratorVariable.isIsRequired(), false);
- return evaluationEnvironment.traceSymbolicValue(cseElement, symbolicValue);
+ CSEElement cseElement = context.getCSEElement(iteratorVariable);
+ SymbolicValue symbolicValue = context.createUnknownValue(iteratorVariable, !iteratorVariable.isIsRequired(), false);
+ return symbolicEvaluationEnvironment.traceSymbolicValue(cseElement, symbolicValue);
}
}
@Override
public @NonNull SymbolicValue visitLetExp(@NonNull LetExp letExp) {
- return getEvaluationEnvironment().symbolicEvaluate(PivotUtil.getOwnedIn(letExp));
+ return symbolicEvaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedIn(letExp));
}
@Override
public @NonNull SymbolicValue visitLetVariable(@NonNull LetVariable letVariable) {
- return getEvaluationEnvironment().symbolicEvaluate(PivotUtil.getOwnedInit(letVariable));
+ return symbolicEvaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedInit(letVariable));
}
@Override
- public Object visitLoopExp(@NonNull LoopExp loopExp) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
+ public @NonNull SymbolicValue visitLoopExp(@NonNull LoopExp loopExp) {
Iteration iteration = PivotUtil.getReferredIteration(loopExp);
LibraryIteration implementation = (LibraryIteration)environmentFactory.getMetamodelManager().getImplementation(iteration);
- return implementation.symbolicEvaluate(evaluationEnvironment, loopExp);
+ return implementation.symbolicEvaluate(symbolicEvaluationEnvironment, loopExp);
}
@Override
- public @Nullable Object visitMapLiteralExp(@NonNull MapLiteralExp literalExp) {
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitMapLiteralExp(@NonNull MapLiteralExp literalExp) {
+ final boolean isKeysAreNullFree = ((MapType)literalExp.getType()).isKeysAreNullFree();
+ final boolean isValuesAreNullFree = ((MapType)literalExp.getType()).isValuesAreNullFree();
+ boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
for (@NonNull MapLiteralPart part : PivotUtil.getOwnedParts(literalExp)) {
- Object keyValue = evaluate(PivotUtil.getOwnedKey(part));
- Object valueValue = evaluate(PivotUtil.getOwnedValue(part));
- assert ValueUtil.isBoxed(keyValue); // Make sure Integer/Real are boxed, invalid is an exception, null is null
- assert ValueUtil.isBoxed(valueValue); // Make sure Integer/Real are boxed, invalid is an exception, null is null
- if ((keyValue instanceof SymbolicValue) || (valueValue instanceof SymbolicValue)) {
- isSymbolic = true;
+ SymbolicValue keyValue = symbolicEvaluate(PivotUtil.getOwnedKey(part));
+ SymbolicValue valueValue = symbolicEvaluate(PivotUtil.getOwnedValue(part));
+ if (!keyValue.isKnown() || !valueValue.isKnown()) {
+ isKnown = false;
}
if (ValueUtil.mayBeInvalid(keyValue) || ValueUtil.mayBeInvalid(valueValue)) {
mayBeInvalid = true;
}
- if (ValueUtil.mayBeNull(keyValue) || ValueUtil.mayBeNull(valueValue)) {
+ if (isKeysAreNullFree && ValueUtil.mayBeNull(keyValue)) {
+ mayBeNull = true;
+ }
+ if (isValuesAreNullFree && ValueUtil.mayBeNull(valueValue)) {
mayBeNull = true;
}
}
- if (isSymbolic) {
- return getEvaluationEnvironment().createUnknownValue(literalExp, false, mayBeNull || mayBeInvalid);
+ if (isKnown) {
+ Object resultValue = evaluationVisitor.visitMapLiteralExp(literalExp);
+ return context.getKnownValue(resultValue);
}
else {
- return delegate.visitMapLiteralExp(literalExp);
+ return context.createUnknownValue(literalExp, false, mayBeNull || mayBeInvalid);
}
}
@Override
- public @Nullable Object visitOperationCallExp(@NonNull OperationCallExp callExp) {
+ public @NonNull SymbolicValue visitNullLiteralExp(@NonNull NullLiteralExp nullLiteralExp) {
+ Object resultValue = evaluationVisitor.visitNullLiteralExp(nullLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitOperationCallExp(@NonNull OperationCallExp callExp) {
return doOperationCallExp(callExp);
}
@Override
- public @Nullable Object visitOppositePropertyCallExp(@NonNull OppositePropertyCallExp oppositePropertyCallExp) {
+ public @NonNull SymbolicValue visitOppositePropertyCallExp(@NonNull OppositePropertyCallExp oppositePropertyCallExp) {
return doNavigationCallExp(oppositePropertyCallExp);
}
@Override
public @NonNull SymbolicValue visitParameterVariable(@NonNull ParameterVariable parameterVariable) {
- AbstractSymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- SymbolicValue symbolicValue = evaluationEnvironment.basicGetSymbolicValue(parameterVariable);
+ SymbolicValue symbolicValue = symbolicEvaluationEnvironment.basicGetSymbolicValue(parameterVariable);
if (symbolicValue == null) {
throw new IllegalStateException(StringUtil.bind("Unbound parameter variable ''{0}''", parameterVariable));
}
@@ -457,20 +440,38 @@
}
@Override
- public @Nullable Object visitPropertyCallExp(@NonNull PropertyCallExp propertyCallExp) {
+ public @NonNull SymbolicValue visitPropertyCallExp(@NonNull PropertyCallExp propertyCallExp) {
return doNavigationCallExp(propertyCallExp);
}
@Override
- public @Nullable Object visitShadowExp(@NonNull ShadowExp shadowExp) {
- SymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitRealLiteralExp(@NonNull RealLiteralExp realLiteralExp) {
+ Object resultValue = evaluationVisitor.visitRealLiteralExp(realLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitResultVariable(@NonNull ResultVariable resultVariable) {
+ OCLExpression initExp = resultVariable.getOwnedInit();
+ if (initExp != null) {
+ return symbolicEvaluationEnvironment.symbolicEvaluate(initExp);
+ }
+ else {
+ CSEElement cseElement = context.getCSEElement(resultVariable);
+ SymbolicValue symbolicValue = context.createUnknownValue(resultVariable, !resultVariable.isIsRequired(), false);
+ return symbolicEvaluationEnvironment.traceSymbolicValue(cseElement, symbolicValue);
+ }
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitShadowExp(@NonNull ShadowExp shadowExp) {
+ boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
for (@NonNull ShadowPart part : PivotUtil.getOwnedParts(shadowExp)) {
- SymbolicValue partValue = evaluationEnvironment.symbolicEvaluate(part);
+ SymbolicValue partValue = symbolicEvaluationEnvironment.symbolicEvaluate(part);
if (!partValue.isKnown()) {
- isSymbolic = true;
+ isKnown = false;
}
if (partValue.mayBeInvalid()) {
mayBeInvalid = true;
@@ -479,53 +480,55 @@
mayBeNull = true;
}
}
- if (isSymbolic) {
- return evaluationEnvironment.createUnknownValue(shadowExp, false, mayBeNull || mayBeInvalid);
+ if (isKnown) {
+ Object resultValue = evaluationVisitor.visitShadowExp(shadowExp);
+ return context.getKnownValue(resultValue);
}
else {
- return delegate.visitShadowExp(shadowExp);
+ return context.createUnknownValue(shadowExp, false, mayBeNull || mayBeInvalid);
}
}
@Override
- public Object visitShadowPart(@NonNull ShadowPart shadowPart) {
- SymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitShadowPart(@NonNull ShadowPart shadowPart) {
+ // boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
- OCLExpression ownedInit = PivotUtil.getOwnedInit(shadowPart); // XXX
- Property partProperty = shadowPart.getReferredProperty();
- boolean isRequired = partProperty.isIsRequired();
- boolean isMany = partProperty.isIsMany();
- SymbolicValue initValue = evaluationEnvironment.symbolicEvaluate(ownedInit);
- if (!initValue.isKnown()) {
- isSymbolic = true;
- }
+ OCLExpression ownedInit = PivotUtil.getOwnedInit(shadowPart);
+ SymbolicValue initValue = symbolicEvaluationEnvironment.symbolicEvaluate(ownedInit);
+ // if (!initValue.isKnown()) {
+ // isKnown = false;
+ // }
if (initValue.mayBeInvalid()) {
mayBeInvalid = true;
}
if (initValue.mayBeNull()) {
mayBeNull = true;
}
- if (isSymbolic) {
- return evaluationEnvironment.createUnknownValue(ownedInit, false, mayBeNull || mayBeInvalid);
- }
- else {
- return evaluationEnvironment.createUnknownValue(ownedInit, false, mayBeNull || mayBeInvalid);
-// return delegate.visitShadowPart(shadowPart);
- }
+ // if (isKnown) {
+ // Object resultValue = evaluationVisitor.visitShadowPart(shadowPart); // -- not supported
+ // return context.getKnownValue(resultValue);
+ // }
+ // else {
+ return context.createUnknownValue(ownedInit, false, mayBeNull || mayBeInvalid);
+ // }
}
@Override
- public @Nullable Object visitTupleLiteralExp(@NonNull TupleLiteralExp literalExp) {
- SymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitStringLiteralExp(@NonNull StringLiteralExp stringLiteralExp) {
+ Object resultValue = evaluationVisitor.visitStringLiteralExp(stringLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitTupleLiteralExp(@NonNull TupleLiteralExp literalExp) {
+ boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
for (@NonNull TupleLiteralPart part : PivotUtil.getOwnedParts(literalExp)) {
- SymbolicValue partValue = evaluationEnvironment.symbolicEvaluate(part);
+ SymbolicValue partValue = symbolicEvaluationEnvironment.symbolicEvaluate(part);
if (!partValue.isKnown()) {
- isSymbolic = true;
+ isKnown = false;
}
if (partValue.mayBeInvalid()) {
mayBeInvalid = true;
@@ -534,23 +537,23 @@
mayBeNull = true;
}
}
- if (isSymbolic) {
- return evaluationEnvironment.createUnknownValue(literalExp, false, mayBeNull || mayBeInvalid);
+ if (isKnown) {
+ Object resultValue = evaluationVisitor.visitTupleLiteralExp(literalExp);
+ return context.getKnownValue(resultValue);
}
else {
- return delegate.visitTupleLiteralExp(literalExp);
+ return context.createUnknownValue(literalExp, false, mayBeNull || mayBeInvalid);
}
}
@Override
- public Object visitTupleLiteralPart(@NonNull TupleLiteralPart part) {
- SymbolicEvaluationEnvironment evaluationEnvironment = getEvaluationEnvironment();
- boolean isSymbolic = false;
+ public @NonNull SymbolicValue visitTupleLiteralPart(@NonNull TupleLiteralPart part) {
+ boolean isKnown = true;
boolean mayBeInvalid = false;
boolean mayBeNull = false;
- SymbolicValue partValue = evaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedInit(part));
+ SymbolicValue partValue = symbolicEvaluationEnvironment.symbolicEvaluate(PivotUtil.getOwnedInit(part));
if (!partValue.isKnown()) {
- isSymbolic = true;
+ isKnown = false;
}
if (partValue.mayBeInvalid()) {
mayBeInvalid = true;
@@ -558,18 +561,49 @@
if (partValue.mayBeNull()) {
mayBeNull = true;
}
- if (isSymbolic) {
- return evaluationEnvironment.createUnknownValue(part, false, mayBeNull || mayBeInvalid);
+ if (isKnown) {
+ Object resultValue = evaluationVisitor.visitTupleLiteralPart(part);
+ return context.getKnownValue(resultValue);
}
else {
- return delegate.visitTupleLiteralPart(part);
+ return context.createUnknownValue(part, false, mayBeNull || mayBeInvalid);
}
}
@Override
- public Object visitVariableDeclaration(@NonNull VariableDeclaration object) {
- // TODO Auto-generated method stub
- // return super.visitVariableDeclaration(object);
- return visiting(object);
+ public @NonNull SymbolicValue visitTypeExp(@NonNull TypeExp typeExp) {
+ Object resultValue = evaluationVisitor.visitTypeExp(typeExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitUnlimitedNaturalLiteralExp(@NonNull UnlimitedNaturalLiteralExp unlimitedNaturalLiteralExp) {
+ Object resultValue = evaluationVisitor.visitUnlimitedNaturalLiteralExp(unlimitedNaturalLiteralExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitVariable(@NonNull Variable iteratorVariable) { // Used for CoIterator
+ OCLExpression initExp = iteratorVariable.getOwnedInit();
+ if (initExp != null) {
+ return symbolicEvaluationEnvironment.symbolicEvaluate(initExp);
+ }
+ else {
+ CSEElement cseElement = context.getCSEElement(iteratorVariable);
+ SymbolicValue symbolicValue = context.createUnknownValue(iteratorVariable, !iteratorVariable.isIsRequired(), false);
+ return symbolicEvaluationEnvironment.traceSymbolicValue(cseElement, symbolicValue);
+ }
+ }
+
+ @Override
+ public @NonNull SymbolicValue visitVariableExp(@NonNull VariableExp variableExp) {
+ Object resultValue = evaluationVisitor.visitVariableExp(variableExp);
+ return context.getKnownValue(resultValue);
+ }
+
+ @Override
+ public @NonNull SymbolicValue visiting(@NonNull Visitable visitable) {
+// return visitable.accept(evaluationVisitor);
+ throw new IllegalArgumentException("Unsupported " + visitable.eClass().getName() + " for SymbolicEvaluationVisitor");
}
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
index 16d99ba..2272f2c 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
@@ -123,7 +123,7 @@
assert argument != null;
boxedSourceAndArgumentValues[1+i] = argumentSymbolicValues.get(i).getKnownValue();
}
- final Object resultObject = evaluate(symbolicAnalysis, callExp, boxedSourceAndArgumentValues);
+ final Object resultObject = evaluate(symbolicAnalysis.getExecutor(), callExp, boxedSourceAndArgumentValues);
return symbolicAnalysis.getKnownValue(resultObject);
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractIteration.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractIteration.java
index 1d6041f..4a36371 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractIteration.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractIteration.java
@@ -23,7 +23,8 @@
import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.evaluation.IterationManager;
import org.eclipse.ocl.pivot.ids.TypeId;
-import org.eclipse.ocl.pivot.internal.evaluation.AbstractSymbolicEvaluationEnvironment;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicAnalysis;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationEnvironment;
import org.eclipse.ocl.pivot.library.LibraryOperation.LibraryOperationExtension2;
import org.eclipse.ocl.pivot.utilities.PivotUtil;
import org.eclipse.ocl.pivot.values.SymbolicValue;
@@ -70,7 +71,7 @@
/**
* @since 1.16
*/
- protected @Nullable SymbolicValue checkPreconditions(@NonNull AbstractSymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
+ protected @Nullable SymbolicValue checkPreconditions(@NonNull SymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
TypeId returnTypeId = loopExp.getTypeId();
OCLExpression source = PivotUtil.getOwnedSource(loopExp);
SymbolicValue invalidSourceProblem = evaluationEnvironment.checkNotInvalid(source, returnTypeId);
@@ -158,7 +159,7 @@
* @since 1.16
*/
@Override
- public @NonNull SymbolicValue symbolicEvaluate(@NonNull AbstractSymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
+ public @NonNull SymbolicValue symbolicEvaluate(@NonNull SymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
SymbolicValue symbolicPreconditionValue = checkPreconditions(evaluationEnvironment, loopExp);
if (symbolicPreconditionValue != null) {
return symbolicPreconditionValue;
@@ -203,17 +204,18 @@
mayBeInvalidOrNull = true;
}
argumentSymbolicValues.add(bodySymbolicValue);
+ SymbolicAnalysis symbolicAnalysis = evaluationEnvironment.getSymbolicAnalysis();
if (isKnown) {
@Nullable Object[] sourceAndArgumentValues = new @Nullable Object[1+argumentsSize];
sourceAndArgumentValues[0] = sourceSymbolicValue.getKnownValue();
for (int i = 0; i < argumentsSize; i++) {
sourceAndArgumentValues[i+1] = argumentSymbolicValues.get(i).getKnownValue();
}
- Object result = ((LibraryOperationExtension2)this).evaluate(evaluationEnvironment.getExecutor(), loopExp, sourceAndArgumentValues);
+ Object result = ((LibraryOperationExtension2)this).evaluate(symbolicAnalysis.getExecutor(), loopExp, sourceAndArgumentValues);
return evaluationEnvironment.getKnownValue(result);
}
else {
- return evaluationEnvironment.createUnknownValue(loopExp.getTypeId(), false, mayBeInvalidOrNull);
+ return symbolicAnalysis.createUnknownValue(loopExp.getTypeId(), false, mayBeInvalidOrNull);
}
/* if (loopExp.isIsMany()) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/LibraryIteration.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/LibraryIteration.java
index e7c03f7..5cdc6a2 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/LibraryIteration.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/LibraryIteration.java
@@ -17,7 +17,7 @@
import org.eclipse.ocl.pivot.evaluation.Executor;
import org.eclipse.ocl.pivot.evaluation.IterationManager;
import org.eclipse.ocl.pivot.ids.TypeId;
-import org.eclipse.ocl.pivot.internal.evaluation.AbstractSymbolicEvaluationEnvironment;
+import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationEnvironment;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.InvalidValueException;
import org.eclipse.ocl.pivot.values.SymbolicValue;
@@ -56,7 +56,7 @@
/**
* @since 1.16
*/
- default @NonNull SymbolicValue symbolicEvaluate(@NonNull AbstractSymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
+ default @NonNull SymbolicValue symbolicEvaluate(@NonNull SymbolicEvaluationEnvironment evaluationEnvironment, @NonNull LoopExp loopExp) {
throw new UnsupportedOperationException();
}
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
index 389f64b..04fec06 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
@@ -901,7 +901,7 @@
public static boolean isBoxed(@Nullable Object object) {
if (object instanceof SymbolicValue) {
- return true;
+ return false;
}
if (object instanceof InvalidValue) {
return true;
diff --git a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/pivot/tests/PivotTestCase.java b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/pivot/tests/PivotTestCase.java
index 9c9dec8..a77b6d6 100644
--- a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/pivot/tests/PivotTestCase.java
+++ b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/pivot/tests/PivotTestCase.java
@@ -241,6 +241,11 @@
}
s1.append("\n");
s1.append(actual);
+ List<?> data = diagnostic.getData();
+ if ((data != null) && (data.size() >= 2) && (data.get(1) instanceof Throwable)) {
+ s1.append("\n\t");
+ s1.append(data.get(1).toString());
+ }
}
else {
expected.put(actual, expectedCount-1);
diff --git a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/SymbolicAnalysisTests.java b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/SymbolicAnalysisTests.java
index 2a26978..eeae058 100644
--- a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/SymbolicAnalysisTests.java
+++ b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/SymbolicAnalysisTests.java
@@ -440,6 +440,11 @@
PropertyCallExp asPropertyCallExp = (PropertyCallExp) asExpressionInOCL.getOwnedBody();
VariableExp asSourceExp = (VariableExp) PivotUtil.getOwnedSource(asPropertyCallExp);
+ // safe maybe-null navigation
+ SymbolicAnalysis symbolicAnalysis399 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, null, new Object[]{new SymbolicUnknownValue("p0", deductionsTypeId, true, false)});
+ checkContents(symbolicAnalysis399, asExpressionInOCL, null, mayBeNulls(asExpressionInOCL, contextVariable, firstParameterVariable,
+ asPropertyCallExp, asSourceExp), null, null);
+
// safe non-null navigation
SymbolicAnalysis symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, null, new Object[]{new SymbolicUnknownValue("p0", deductionsTypeId, false, false)});
checkContents(symbolicAnalysis1, asExpressionInOCL, null, new EObject[]{contextVariable}, null, null);
