Skip to content
New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom

Fix #2985 by using proper types. #3026

Merged
merged 6 commits into from
Jan 3, 2020
Merged

Fix #2985 by using proper types. #3026

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b0bd0bc
Fix #2985 by using proper types.
wmdietl Jan 2, 2020
effb0c5
Suppress unused variable warning.
wmdietl Jan 2, 2020
332ce99
Use clazz.cast.
wmdietl Jan 2, 2020
6fd5883
Merge branch 'master' of github.com:typetools/checker-framework into …
wmdietl Jan 3, 2020
232afc1
Javadoc for type parameter.
wmdietl Jan 3, 2020
cd5104b
Fix Javadoc.
smillst Jan 3, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 10 additions & 9 deletions framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -767,7 +767,7 @@ private void checkContractsAtMethodDeclaration(
List<String> formalParamNames,
boolean abstractMethod) {
FlowExpressionContext flowExprContext = null;
List<Contract> contracts = contractsUtils.getContracts(methodElement);
Set<Contract> contracts = contractsUtils.getContracts(methodElement);

for (Contract contract : contracts) {
String expression = contract.expression;
Expand Down Expand Up @@ -1400,7 +1400,7 @@ protected void checkVarargs(AnnotatedExecutableType invokedMethod, Tree tree) {
* @param tree the Tree immediately prior to which the preconditions must hold true
* @param preconditions the preconditions to be checked
*/
protected void checkPreconditions(MethodInvocationTree tree, Set<Contract> preconditions) {
protected void checkPreconditions(MethodInvocationTree tree, Set<Precondition> preconditions) {
// This check is needed for the GUI effects and Units Checkers tests to pass.
// TODO: Remove this check and investigate the root cause.
if (preconditions.isEmpty()) {
Expand Down Expand Up @@ -3240,8 +3240,8 @@ private void checkPreAndPostConditions() {

// Check postconditions
ContractsUtils contracts = ContractsUtils.getInstance(atypeFactory);
Set<Contract> superPost = contracts.getPostconditions(overridden.getElement());
Set<Contract> subPost = contracts.getPostconditions(overrider.getElement());
Set<Postcondition> superPost = contracts.getPostconditions(overridden.getElement());
Set<Postcondition> subPost = contracts.getPostconditions(overrider.getElement());
Set<Pair<Receiver, AnnotationMirror>> superPost2 =
resolveContracts(superPost, overridden);
Set<Pair<Receiver, AnnotationMirror>> subPost2 = resolveContracts(subPost, overrider);
Expand All @@ -3257,8 +3257,8 @@ private void checkPreAndPostConditions() {
postmsg);

// Check preconditions
Set<Contract> superPre = contracts.getPreconditions(overridden.getElement());
Set<Contract> subPre = contracts.getPreconditions(overrider.getElement());
Set<Precondition> superPre = contracts.getPreconditions(overridden.getElement());
Set<Precondition> subPre = contracts.getPreconditions(overrider.getElement());
Set<Pair<Receiver, AnnotationMirror>> superPre2 =
resolveContracts(superPre, overridden);
Set<Pair<Receiver, AnnotationMirror>> subPre2 = resolveContracts(subPre, overrider);
Expand All @@ -3274,9 +3274,10 @@ private void checkPreAndPostConditions() {
premsg);

// Check conditional postconditions
Set<Contract> superCPost =
Set<ConditionalPostcondition> superCPost =
contracts.getConditionalPostconditions(overridden.getElement());
Set<Contract> subCPost = contracts.getConditionalPostconditions(overrider.getElement());
Set<ConditionalPostcondition> subCPost =
contracts.getConditionalPostconditions(overrider.getElement());
// consider only 'true' postconditions
Set<Postcondition> superCPostTrue = filterConditionalPostconditions(superCPost, true);
Set<Postcondition> subCPostTrue = filterConditionalPostconditions(subCPost, true);
Expand Down Expand Up @@ -3643,7 +3644,7 @@ private void checkReturnMsg(boolean success) {
* @return all the given conditional postconditions whose {@code result} is {@code b}
*/
private Set<Postcondition> filterConditionalPostconditions(
Set<Contract> conditionalPostconditions, boolean b) {
Set<ConditionalPostcondition> conditionalPostconditions, boolean b) {
Set<Postcondition> result = new LinkedHashSet<>();
for (Contract c : conditionalPostconditions) {
ConditionalPostcondition p = (ConditionalPostcondition) c;
Expand Down
10 changes: 5 additions & 5 deletions framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,6 +68,7 @@
import org.checkerframework.framework.util.AnnotatedTypes;
import org.checkerframework.framework.util.Contract;
import org.checkerframework.framework.util.Contract.ConditionalPostcondition;
import org.checkerframework.framework.util.Contract.Postcondition;
import org.checkerframework.framework.util.Contract.Precondition;
import org.checkerframework.framework.util.ContractsUtils;
import org.checkerframework.framework.util.FlowExpressionParseUtil;
Expand Down Expand Up @@ -514,10 +515,9 @@ protected void addInformationFromPreconditions(
ExecutableElement methodElement) {
ContractsUtils contracts = ContractsUtils.getInstance(analysis.atypeFactory);
FlowExpressionContext flowExprContext = null;
Set<Contract> preconditions = contracts.getPreconditions(methodElement);
Set<Precondition> preconditions = contracts.getPreconditions(methodElement);

for (Contract c : preconditions) {
Precondition p = (Precondition) c;
for (Precondition p : preconditions) {
String expression = p.expression;
AnnotationMirror annotation = p.annotation;

Expand Down Expand Up @@ -998,7 +998,7 @@ private boolean shouldPerformWholeProgramInference(Tree tree, Element elt) {
protected void processPostconditions(
MethodInvocationNode n, S store, ExecutableElement methodElement, Tree tree) {
ContractsUtils contracts = ContractsUtils.getInstance(analysis.atypeFactory);
Set<Contract> postconditions = contracts.getPostconditions(methodElement);
Set<Postcondition> postconditions = contracts.getPostconditions(methodElement);
processPostconditionsAndConditionalPostconditions(n, tree, store, null, postconditions);
}

Expand All @@ -1013,7 +1013,7 @@ protected void processConditionalPostconditions(
S thenStore,
S elseStore) {
ContractsUtils contracts = ContractsUtils.getInstance(analysis.atypeFactory);
Set<Contract> conditionalPostconditions =
Set<ConditionalPostcondition> conditionalPostconditions =
contracts.getConditionalPostconditions(methodElement);
processPostconditionsAndConditionalPostconditions(
n, tree, thenStore, elseStore, conditionalPostconditions);
Expand Down
51 changes: 32 additions & 19 deletions framework/src/main/java/org/checkerframework/framework/util/ContractsUtils.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
import static org.checkerframework.framework.util.Contract.Kind.POSTCONDITION;
import static org.checkerframework.framework.util.Contract.Kind.PRECONDITION;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashSet;
Expand Down Expand Up @@ -66,13 +65,13 @@ public static ContractsUtils getInstance(GenericAnnotatedTypeFactory<?, ?, ?, ?>
}

/**
* Returns all the contracts on method or contstructor {@code executableElement}.
* Returns all the contracts on method or constructor {@code executableElement}.
*
* @param executableElement the method or constructor whose contracts to retrieve
* @return the contracts on {@code executableElement}
*/
public List<Contract> getContracts(ExecutableElement executableElement) {
List<Contract> contracts = new ArrayList<>();
public Set<Contract> getContracts(ExecutableElement executableElement) {
Set<Contract> contracts = new LinkedHashSet<>();
contracts.addAll(getPreconditions(executableElement));
contracts.addAll(getPostconditions(executableElement));
contracts.addAll(getConditionalPostconditions(executableElement));
Expand All @@ -87,8 +86,8 @@ public List<Contract> getContracts(ExecutableElement executableElement) {
* @param executableElement the method whose contracts to return
* @return the contracts on {@code executableElement}
*/
public Set<Contract> getPreconditions(ExecutableElement executableElement) {
return getContracts(executableElement, PRECONDITION);
public Set<Contract.Precondition> getPreconditions(ExecutableElement executableElement) {
return getContracts(executableElement, PRECONDITION, Contract.Precondition.class);
}

/// Postcondition methods (keep in sync with other two types)
Expand All @@ -99,8 +98,8 @@ public Set<Contract> getPreconditions(ExecutableElement executableElement) {
* @param executableElement the method whose contracts to return
* @return the contracts on {@code executableElement}
*/
public Set<Contract> getPostconditions(ExecutableElement executableElement) {
return getContracts(executableElement, POSTCONDITION);
public Set<Contract.Postcondition> getPostconditions(ExecutableElement executableElement) {
return getContracts(executableElement, POSTCONDITION, Contract.Postcondition.class);
}

/// Conditional postcondition methods (keep in sync with other two types)
Expand All @@ -111,8 +110,10 @@ public Set<Contract> getPostconditions(ExecutableElement executableElement) {
* @param methodElement the method whose contracts to return
* @return the contracts on {@code methodElement}
*/
public Set<Contract> getConditionalPostconditions(ExecutableElement methodElement) {
return getContracts(methodElement, CONDITIONALPOSTCONDITION);
public Set<Contract.ConditionalPostcondition> getConditionalPostconditions(
ExecutableElement methodElement) {
return getContracts(
methodElement, CONDITIONALPOSTCONDITION, Contract.ConditionalPostcondition.class);
}

/// Helper methods
Expand All @@ -123,10 +124,13 @@ public Set<Contract> getConditionalPostconditions(ExecutableElement methodElemen
* @param contractAnnotation a {@link RequiresQualifier}, {@link EnsuresQualifier}, {@link
* EnsuresQualifierIf}, or null
* @param kind the kind of {@code contractAnnotation}
* @param clazz the class to determine the return type
* @param <T> the specific type of {@link Contract} to use
* @return the contracts expressed by the given annotation, or the empty set if the argument is
* null
*/
private Set<Contract> getContract(Contract.Kind kind, AnnotationMirror contractAnnotation) {
private <T extends Contract> Set<T> getContract(
wmdietl marked this conversation as resolved.
Show resolved Hide resolved
Contract.Kind kind, AnnotationMirror contractAnnotation, Class<T> clazz) {
if (contractAnnotation == null) {
return Collections.emptySet();
}
Expand All @@ -135,16 +139,19 @@ private Set<Contract> getContract(Contract.Kind kind, AnnotationMirror contractA
if (enforcedQualifier == null) {
return Collections.emptySet();
}
Set<Contract> result = new LinkedHashSet<>();
Set<T> result = new LinkedHashSet<>();
List<String> expressions =
AnnotationUtils.getElementValueArray(
contractAnnotation, "expression", String.class, false);
Boolean annoResult =
AnnotationUtils.getElementValueOrNull(
contractAnnotation, "result", Boolean.class, false);
for (String expr : expressions) {
result.add(
Contract.create(kind, expr, enforcedQualifier, contractAnnotation, annoResult));
T contract =
clazz.cast(
Contract.create(
kind, expr, enforcedQualifier, contractAnnotation, annoResult));
result.add(contract);
}
return result;
}
Expand All @@ -154,14 +161,17 @@ private Set<Contract> getContract(Contract.Kind kind, AnnotationMirror contractA
*
* @param executableElement the method whose contracts to return
* @param kind the kind of contracts to retrieve
* @param clazz the class to determine the return type
* @param <T> the specific type of {@link Contract} to use
* @return the contracts on {@code executableElement}
*/
public Set<Contract> getContracts(ExecutableElement executableElement, Kind kind) {
Set<Contract> result = new LinkedHashSet<>();
private <T extends Contract> Set<T> getContracts(
ExecutableElement executableElement, Kind kind, Class<T> clazz) {
Set<T> result = new LinkedHashSet<>();
// Check for a single contract annotation.
AnnotationMirror frameworkContractAnno =
factory.getDeclAnnotation(executableElement, kind.frameworkContractClass);
result.addAll(getContract(kind, frameworkContractAnno));
result.addAll(getContract(kind, frameworkContractAnno, clazz));

// Check for a wrapper around contract annotations.
AnnotationMirror frameworkContractAnnos =
Expand All @@ -171,7 +181,7 @@ public Set<Contract> getContracts(ExecutableElement executableElement, Kind kind
AnnotationUtils.getElementValueArray(
frameworkContractAnnos, "value", AnnotationMirror.class, false);
for (AnnotationMirror a : frameworkContractAnnoList) {
result.addAll(getContract(kind, a));
result.addAll(getContract(kind, a, clazz));
}
}

Expand All @@ -192,7 +202,10 @@ public Set<Contract> getContracts(ExecutableElement executableElement, Kind kind
Boolean annoResult =
AnnotationUtils.getElementValueOrNull(anno, "result", Boolean.class, false);
for (String expr : expressions) {
result.add(Contract.create(kind, expr, enforcedQualifier, anno, annoResult));
T contract =
clazz.cast(
Contract.create(kind, expr, enforcedQualifier, anno, annoResult));
result.add(contract);
}
}
return result;
Expand Down