Skip to content

Commit

Permalink
Changing formatting style and applying spotless + javadoc
Browse files Browse the repository at this point in the history
  • Loading branch information
lucaneg committed Sep 28, 2023
1 parent db68abb commit 1f05cbe
Show file tree
Hide file tree
Showing 476 changed files with 6,695 additions and 2,695 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,10 @@ public static MonolithicHeap defaultHeapDomain() {
*/
public static <H extends HeapDomain<H>,
V extends ValueDomain<V>,
T extends TypeDomain<T>> SimpleAbstractState<H, V, T> simpleState(H heap, V value, T type) {
T extends TypeDomain<T>> SimpleAbstractState<H, V, T> simpleState(
H heap,
V value,
T type) {
return new SimpleAbstractState<>(heap, value, type);
}

Expand Down
63 changes: 37 additions & 26 deletions lisa/lisa-analyses/src/main/java/it/unive/lisa/LiSAFactory.java
Original file line number Diff line number Diff line change
@@ -1,5 +1,22 @@
package it.unive.lisa;

import it.unive.lisa.analysis.AbstractState;
import it.unive.lisa.analysis.dataflow.DataflowElement;
import it.unive.lisa.analysis.dataflow.DefiniteForwardDataflowDomain;
import it.unive.lisa.analysis.dataflow.PossibleForwardDataflowDomain;
import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
import it.unive.lisa.analysis.nonrelational.heap.NonRelationalHeapDomain;
import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
import it.unive.lisa.analysis.nonrelational.inference.InferredValue;
import it.unive.lisa.analysis.nonrelational.value.NonRelationalTypeDomain;
import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain;
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
import it.unive.lisa.analysis.type.TypeDomain;
import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
import it.unive.lisa.interprocedural.callgraph.CallGraph;
import java.lang.reflect.Constructor;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
Expand All @@ -14,30 +31,11 @@
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.apache.commons.lang3.ArrayUtils;
import org.apache.commons.lang3.StringUtils;
import org.reflections.Reflections;
import org.reflections.scanners.SubTypesScanner;

import it.unive.lisa.analysis.AbstractState;
import it.unive.lisa.analysis.dataflow.DataflowElement;
import it.unive.lisa.analysis.dataflow.DefiniteForwardDataflowDomain;
import it.unive.lisa.analysis.dataflow.PossibleForwardDataflowDomain;
import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.nonrelational.heap.HeapEnvironment;
import it.unive.lisa.analysis.nonrelational.heap.NonRelationalHeapDomain;
import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
import it.unive.lisa.analysis.nonrelational.inference.InferredValue;
import it.unive.lisa.analysis.nonrelational.value.NonRelationalTypeDomain;
import it.unive.lisa.analysis.nonrelational.value.NonRelationalValueDomain;
import it.unive.lisa.analysis.nonrelational.value.TypeEnvironment;
import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
import it.unive.lisa.analysis.type.TypeDomain;
import it.unive.lisa.analysis.value.ValueDomain;
import it.unive.lisa.interprocedural.InterproceduralAnalysis;
import it.unive.lisa.interprocedural.callgraph.CallGraph;

/**
* An utility class for instantiating analysis components, that is, modular
* pieces of the analysis that have several implementations. A specific instance
Expand All @@ -54,7 +52,10 @@ private LiSAFactory() {
}

@SuppressWarnings("unchecked")
private static <T> T construct(Class<T> component, Class<?>[] argTypes, Object[] params)
private static <T> T construct(
Class<T> component,
Class<?>[] argTypes,
Object[] params)
throws AnalysisSetupException {
if (argTypes.length == 0)
try {
Expand All @@ -79,7 +80,9 @@ private static <T> T construct(Class<T> component, Class<?>[] argTypes, Object[]
}
}

private static Class<?>[] findConstructorSignature(Class<?> component, Object[] params)
private static Class<?>[] findConstructorSignature(
Class<?> component,
Object[] params)
throws AnalysisSetupException {
Map<Constructor<?>, List<Integer>> candidates = new IdentityHashMap<>();
Class<?>[] types;
Expand Down Expand Up @@ -114,7 +117,9 @@ else if (!types[i].isAssignableFrom(params[i].getClass()))
return candidates.keySet().iterator().next().getParameterTypes();
}

private static boolean needsWrapping(Class<?> actual, Class<?> desired) {
private static boolean needsWrapping(
Class<?> actual,
Class<?> desired) {
if (NonRelationalHeapDomain.class.isAssignableFrom(actual) && desired.isAssignableFrom(HeapDomain.class))
return true;
else if (NonRelationalValueDomain.class.isAssignableFrom(actual) && desired.isAssignableFrom(ValueDomain.class))
Expand All @@ -130,7 +135,8 @@ else if (DataflowElement.class.isAssignableFrom(actual) && desired.isAssignableF
}

@SuppressWarnings({ "rawtypes", "unchecked" })
private static Object wrapParam(Object param) {
private static Object wrapParam(
Object param) {
if (NonRelationalHeapDomain.class.isAssignableFrom(param.getClass()))
return new HeapEnvironment((NonRelationalHeapDomain<?>) param);
else if (NonRelationalValueDomain.class.isAssignableFrom(param.getClass()))
Expand Down Expand Up @@ -172,7 +178,10 @@ else if (((ParameterizedType) domain).getRawType() == DefiniteForwardDataflowDom
*
* @throws AnalysisSetupException if the component cannot be created
*/
public static <T> T getInstance(Class<T> component, Object... params) throws AnalysisSetupException {
public static <T> T getInstance(
Class<T> component,
Object... params)
throws AnalysisSetupException {
try {
if (params != null && params.length != 0)
return construct(component, findConstructorSignature(component, params), params);
Expand Down Expand Up @@ -203,7 +212,8 @@ public static final class ConfigurableComponent {
private final Class<?> component;
private final Set<Class<?>> alternatives;

private ConfigurableComponent(Class<?> component) {
private ConfigurableComponent(
Class<?> component) {
this.component = component;
this.alternatives = new HashSet<>();

Expand Down Expand Up @@ -249,7 +259,8 @@ public int hashCode() {
}

@Override
public boolean equals(Object obj) {
public boolean equals(
Object obj) {
if (this == obj)
return true;
if (obj == null)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,5 @@
package it.unive.lisa.analysis;

import java.util.Collection;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.function.Predicate;

import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.heap.HeapSemanticOperation.HeapReplacement;
import it.unive.lisa.analysis.lattices.ExpressionSet;
Expand All @@ -19,6 +13,11 @@
import it.unive.lisa.type.Type;
import it.unive.lisa.util.representation.ObjectRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;
import java.util.Collection;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.function.Predicate;

/**
* An abstract state of the analysis, composed by a heap state modeling the
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,5 @@
package it.unive.lisa.analysis.combination;

import java.util.Collection;
import java.util.function.Predicate;

import it.unive.lisa.analysis.Lattice;
import it.unive.lisa.analysis.ScopeToken;
import it.unive.lisa.analysis.SemanticDomain;
Expand All @@ -14,6 +11,8 @@
import it.unive.lisa.symbolic.value.Identifier;
import it.unive.lisa.util.representation.ListRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;
import java.util.Collection;
import java.util.function.Predicate;

/**
* A generic Cartesian product abstract domain between two non-communicating
Expand Down Expand Up @@ -55,7 +54,9 @@ public abstract class CartesianProduct<C extends CartesianProduct<C, T1, T2, E,
* @param left the left-hand side of the Cartesian product
* @param right the right-hand side of the Cartesian product
*/
public CartesianProduct(T1 left, T2 right) {
public CartesianProduct(
T1 left,
T2 right) {
this.left = left;
this.right = right;
}
Expand All @@ -70,7 +71,8 @@ public int hashCode() {
}

@Override
public boolean equals(Object obj) {
public boolean equals(
Object obj) {
if (this == obj)
return true;
if (obj == null)
Expand Down Expand Up @@ -130,80 +132,114 @@ public String toString() {
*
* @return the new instance of product
*/
public abstract C mk(T1 left, T2 right);
public abstract C mk(
T1 left,
T2 right);

@Override
public StructuredRepresentation representation() {
return new ListRepresentation(left.representation(), right.representation());
}

@Override
public C assign(I id, E expression, ProgramPoint pp, SemanticOracle oracle) throws SemanticException {
public C assign(
I id,
E expression,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
T1 newLeft = left.assign(id, expression, pp, oracle);
T2 newRight = right.assign(id, expression, pp, oracle);
return mk(newLeft, newRight);
}

@Override
public C smallStepSemantics(E expression, ProgramPoint pp, SemanticOracle oracle) throws SemanticException {
public C smallStepSemantics(
E expression,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
T1 newLeft = left.smallStepSemantics(expression, pp, oracle);
T2 newRight = right.smallStepSemantics(expression, pp, oracle);
return mk(newLeft, newRight);
}

@Override
public C assume(E expression, ProgramPoint src, ProgramPoint dest, SemanticOracle oracle) throws SemanticException {
public C assume(
E expression,
ProgramPoint src,
ProgramPoint dest,
SemanticOracle oracle)
throws SemanticException {
T1 newLeft = left.assume(expression, src, dest, oracle);
T2 newRight = right.assume(expression, src, dest, oracle);
return mk(newLeft, newRight);
}

@Override
public C forgetIdentifier(Identifier id) throws SemanticException {
public C forgetIdentifier(
Identifier id)
throws SemanticException {
T1 newLeft = left.forgetIdentifier(id);
T2 newRight = right.forgetIdentifier(id);
return mk(newLeft, newRight);
}

@Override
public C forgetIdentifiersIf(Predicate<Identifier> test) throws SemanticException {
public C forgetIdentifiersIf(
Predicate<Identifier> test)
throws SemanticException {
T1 newLeft = left.forgetIdentifiersIf(test);
T2 newRight = right.forgetIdentifiersIf(test);
return mk(newLeft, newRight);
}

@Override
public C pushScope(ScopeToken scope) throws SemanticException {
public C pushScope(
ScopeToken scope)
throws SemanticException {
T1 newLeft = left.pushScope(scope);
T2 newRight = right.pushScope(scope);
return mk(newLeft, newRight);
}

@Override
public C popScope(ScopeToken scope) throws SemanticException {
public C popScope(
ScopeToken scope)
throws SemanticException {
T1 newLeft = left.popScope(scope);
T2 newRight = right.popScope(scope);
return mk(newLeft, newRight);

}

@Override
public Satisfiability satisfies(E expression, ProgramPoint pp, SemanticOracle oracle) throws SemanticException {
public Satisfiability satisfies(
E expression,
ProgramPoint pp,
SemanticOracle oracle)
throws SemanticException {
return left.satisfies(expression, pp, oracle).and(right.satisfies(expression, pp, oracle));
}

@Override
public C lub(C other) throws SemanticException {
public C lub(
C other)
throws SemanticException {
return mk(left.lub(other.left), right.lub(other.right));
}

@Override
public C widening(C other) throws SemanticException {
public C widening(
C other)
throws SemanticException {
return mk(left.widening(other.left), right.widening(other.right));
}

@Override
public boolean lessOrEqual(C other) throws SemanticException {
public boolean lessOrEqual(
C other)
throws SemanticException {
return left.lessOrEqual(other.left) && right.lessOrEqual(other.right);
}

Expand All @@ -228,7 +264,8 @@ public boolean isBottom() {
}

@Override
public <T extends SemanticDomain<?, ?, ?>> Collection<T> getAllDomainInstances(Class<T> domain) {
public <T extends SemanticDomain<?, ?, ?>> Collection<T> getAllDomainInstances(
Class<T> domain) {
Collection<T> result = SemanticDomain.super.getAllDomainInstances(domain);
result.addAll(left.getAllDomainInstances(domain));
result.addAll(right.getAllDomainInstances(domain));
Expand Down
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
package it.unive.lisa.analysis.combination;

import java.util.Map.Entry;

import it.unive.lisa.analysis.SemanticDomain.Satisfiability;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.SemanticOracle;
Expand All @@ -14,6 +12,7 @@
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.util.representation.ListRepresentation;
import it.unive.lisa.util.representation.StructuredRepresentation;
import java.util.Map.Entry;

/**
* A generic Cartesian product abstract domain between two non-communicating
Expand Down
Loading

0 comments on commit 1f05cbe

Please sign in to comment.