Skip to content

Commit ea27871

Browse files
VincenzoArceriVincenzoArceri
authored
Merge pull request #155 from UniVE-SSV/general-bugfixing
General bugfixing
2 parents b066107 + d31f0f3 commit ea27871

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

54 files changed

+307
-156
lines changed

‎lisa/lisa-core/src/main/java/it/unive/lisa/analysis/combination/CartesianProduct.java‎

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ public boolean equals(Object obj) {
8888
}
8989

9090
@Override
91-
public final String toString() {
91+
public String toString() {
9292
if (left instanceof Environment && right instanceof Environment) {
9393
Environment<?, ?, ?, ?> leftEnv = (Environment<?, ?, ?, ?>) left;
9494
Environment<?, ?, ?, ?> rightEnv = (Environment<?, ?, ?, ?>) right;
@@ -129,33 +129,33 @@ public final String toString() {
129129
protected abstract C mk(T1 left, T2 right);
130130

131131
@Override
132-
public final DomainRepresentation representation() {
132+
public DomainRepresentation representation() {
133133
return new PairRepresentation(left.representation(), right.representation());
134134
}
135135

136136
@Override
137-
public final C assign(I id, E expression, ProgramPoint pp) throws SemanticException {
137+
public C assign(I id, E expression, ProgramPoint pp) throws SemanticException {
138138
T1 newLeft = left.assign(id, expression, pp);
139139
T2 newRight = right.assign(id, expression, pp);
140140
return mk(newLeft, newRight);
141141
}
142142

143143
@Override
144-
public final C smallStepSemantics(E expression, ProgramPoint pp) throws SemanticException {
144+
public C smallStepSemantics(E expression, ProgramPoint pp) throws SemanticException {
145145
T1 newLeft = left.smallStepSemantics(expression, pp);
146146
T2 newRight = right.smallStepSemantics(expression, pp);
147147
return mk(newLeft, newRight);
148148
}
149149

150150
@Override
151-
public final C assume(E expression, ProgramPoint pp) throws SemanticException {
151+
public C assume(E expression, ProgramPoint pp) throws SemanticException {
152152
T1 newLeft = left.assume(expression, pp);
153153
T2 newRight = right.assume(expression, pp);
154154
return mk(newLeft, newRight);
155155
}
156156

157157
@Override
158-
public final C forgetIdentifier(Identifier id) throws SemanticException {
158+
public C forgetIdentifier(Identifier id) throws SemanticException {
159159
T1 newLeft = left.forgetIdentifier(id);
160160
T2 newRight = right.forgetIdentifier(id);
161161
return mk(newLeft, newRight);
@@ -177,27 +177,27 @@ public C popScope(ScopeToken scope) throws SemanticException {
177177
}
178178

179179
@Override
180-
public final Satisfiability satisfies(E expression, ProgramPoint pp) throws SemanticException {
180+
public Satisfiability satisfies(E expression, ProgramPoint pp) throws SemanticException {
181181
return left.satisfies(expression, pp).and(right.satisfies(expression, pp));
182182
}
183183

184184
@Override
185-
public final C lub(C other) throws SemanticException {
185+
public C lub(C other) throws SemanticException {
186186
return mk(left.lub(other.left), right.lub(other.right));
187187
}
188188

189189
@Override
190-
public final C widening(C other) throws SemanticException {
190+
public C widening(C other) throws SemanticException {
191191
return mk(left.widening(other.left), right.widening(other.right));
192192
}
193193

194194
@Override
195-
public final boolean lessOrEqual(C other) throws SemanticException {
195+
public boolean lessOrEqual(C other) throws SemanticException {
196196
return left.lessOrEqual(other.left) && right.lessOrEqual(other.right);
197197
}
198198

199199
@Override
200-
public final C top() {
200+
public C top() {
201201
return mk(left.top(), right.top());
202202
}
203203

@@ -207,7 +207,7 @@ public boolean isTop() {
207207
}
208208

209209
@Override
210-
public final C bottom() {
210+
public C bottom() {
211211
return mk(left.bottom(), right.bottom());
212212
}
213213

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/CallGraphBasedAnalysis.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,13 +41,13 @@ public abstract class CallGraphBasedAnalysis<A extends AbstractState<A, H, V>,
4141
protected Program program;
4242

4343
@Override
44-
public final void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException {
44+
public void init(Program program, CallGraph callgraph) throws InterproceduralAnalysisException {
4545
this.callgraph = callgraph;
4646
this.program = program;
4747
}
4848

4949
@Override
50-
public final Call resolve(UnresolvedCall unresolvedCall) throws CallResolutionException {
50+
public Call resolve(UnresolvedCall unresolvedCall) throws CallResolutionException {
5151
return callgraph.resolve(unresolvedCall);
5252
}
5353

@@ -62,7 +62,7 @@ public final Call resolve(UnresolvedCall unresolvedCall) throws CallResolutionEx
6262
*
6363
* @throws SemanticException if the analysis fails
6464
*/
65-
protected final AnalysisState<A, H, V> prepareEntryStateOfEntryPoint(AnalysisState<A, H, V> entryState, CFG cfg)
65+
protected AnalysisState<A, H, V> prepareEntryStateOfEntryPoint(AnalysisState<A, H, V> entryState, CFG cfg)
6666
throws SemanticException {
6767
AnalysisState<A, H, V> prepared = entryState;
6868

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextBasedAnalysis.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -82,7 +82,7 @@ public ContextBasedAnalysis(ContextSensitivityToken token) {
8282
}
8383

8484
@Override
85-
public final void fixpoint(
85+
public void fixpoint(
8686
AnalysisState<A, H, V> entryState,
8787
Class<? extends WorkingSet<Statement>> fixpointWorkingSet,
8888
int wideningThreshold)
@@ -150,7 +150,7 @@ private void fixpointAux(AnalysisState<A, H, V> entryState,
150150
}
151151

152152
@Override
153-
public final Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg) {
153+
public Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg) {
154154
if (results.contains(cfg))
155155
return results.getState(cfg).getAll();
156156
else
@@ -169,7 +169,7 @@ private Pair<AnalysisState<A, H, V>, AnalysisState<A, H, V>> getEntryAndExit(CFG
169169
}
170170

171171
@Override
172-
public final AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
172+
public AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
173173
ExpressionSet<SymbolicExpression>[] parameters)
174174
throws SemanticException {
175175
ScopeToken scope = new ScopeToken(call);

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ContextInsensitiveToken.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
* A context sensitive token that is always the same (aka, do not track any
77
* information about the call stack).
88
*/
9-
public final class ContextInsensitiveToken implements ContextSensitivityToken {
9+
public class ContextInsensitiveToken implements ContextSensitivityToken {
1010

1111
private static final ContextInsensitiveToken singleton = new ContextInsensitiveToken();
1212

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ public ModularWorstCaseAnalysis() {
6969
}
7070

7171
@Override
72-
public final void fixpoint(AnalysisState<A, H, V> entryState,
72+
public void fixpoint(AnalysisState<A, H, V> entryState,
7373
Class<? extends WorkingSet<Statement>> fixpointWorkingSet,
7474
int wideningThreshold) throws FixpointException {
7575
for (CFG cfg : IterationLogger.iterate(LOG, program.getAllCFGs(), "Computing fixpoint over the whole program",
@@ -91,12 +91,12 @@ public final void fixpoint(AnalysisState<A, H, V> entryState,
9191
}
9292

9393
@Override
94-
public final Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg) {
94+
public Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg) {
9595
return Collections.singleton(results.get(cfg).orElse(null));
9696
}
9797

9898
@Override
99-
public final AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
99+
public AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
100100
ExpressionSet<SymbolicExpression>[] parameters)
101101
throws SemanticException {
102102
if (call.getStaticType().isVoidType())

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/RecursionFreeToken.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@
1010
* A context sensitive token representing an entire call chain up until a
1111
* recursion.
1212
*/
13-
public final class RecursionFreeToken implements ContextSensitivityToken {
13+
public class RecursionFreeToken implements ContextSensitivityToken {
1414

1515
private static final RecursionFreeToken singleton = new RecursionFreeToken(null);
1616

‎lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/SingleScopeToken.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
/**
77
* A context sensitive token representing a single {@link ScopeToken}.
88
*/
9-
public final class SingleScopeToken implements ContextSensitivityToken {
9+
public class SingleScopeToken implements ContextSensitivityToken {
1010

1111
private static final SingleScopeToken singleton = new SingleScopeToken(null);
1212

‎lisa/lisa-core/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java‎

Lines changed: 27 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,9 @@
4848
import it.unive.lisa.program.cfg.statement.PluggableStatement;
4949
import it.unive.lisa.program.cfg.statement.Ret;
5050
import it.unive.lisa.program.cfg.statement.Statement;
51+
import it.unive.lisa.program.cfg.statement.call.Call;
52+
import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
53+
import it.unive.lisa.program.cfg.statement.call.resolution.StaticTypesResolution;
5154
import it.unive.lisa.symbolic.SymbolicExpression;
5255
import it.unive.lisa.symbolic.value.HeapLocation;
5356
import it.unive.lisa.symbolic.value.Identifier;
@@ -69,11 +72,14 @@
6972
import java.lang.reflect.Modifier;
7073
import java.util.Collection;
7174
import java.util.HashSet;
75+
import java.util.LinkedList;
76+
import java.util.List;
7277
import java.util.Set;
7378
import java.util.function.Consumer;
7479
import nl.jqno.equalsverifier.EqualsVerifier;
7580
import nl.jqno.equalsverifier.Warning;
7681
import nl.jqno.equalsverifier.api.SingleTypeEqualsVerifierApi;
82+
import org.apache.commons.collections4.ListUtils;
7783
import org.apache.commons.lang3.tuple.Pair;
7884
import org.graphstream.graph.implementations.SingleGraph;
7985
import org.junit.AfterClass;
@@ -97,6 +103,10 @@ public class EqualityContractVerificationTest {
97103
private static final DomainRepresentation dr2 = new StringRepresentation("bar");
98104
private static final SingleGraph g1 = new SingleGraph("a");
99105
private static final SingleGraph g2 = new SingleGraph("b");
106+
private static final UnresolvedCall uc1 = new UnresolvedCall(cfg1, loc, StaticTypesResolution.INSTANCE, false,
107+
"foo");
108+
private static final UnresolvedCall uc2 = new UnresolvedCall(cfg2, loc, StaticTypesResolution.INSTANCE, false,
109+
"bar");
100110

101111
private static final Collection<Class<?>> tested = new HashSet<>();
102112

@@ -169,6 +179,7 @@ private static <T> void verify(Class<T> clazz, boolean getClass, Consumer<Single
169179
.withPrefabValues(DomainRepresentation.class, dr1, dr2)
170180
.withPrefabValues(Pair.class, Pair.of(1, 2), Pair.of(3, 4))
171181
.withPrefabValues(NonInterference.class, new NonInterference().top(), new NonInterference().bottom())
182+
.withPrefabValues(UnresolvedCall.class, uc1, uc2)
172183
.withPrefabValues(org.graphstream.graph.Graph.class, g1, g2);
173184

174185
if (getClass)
@@ -246,20 +257,28 @@ public void testStatements() {
246257
// suppress nullity: the verifier will try to pass in a code location
247258
// with null fields (not possible) and this would cause warnings
248259

260+
List<String> statementFields = List.of("cfg", "offset");
261+
List<String> expressionFields = ListUtils.union(statementFields,
262+
List.of("runtimeTypes", "parent", "metaVariables"));
263+
249264
Reflections scanner = mkReflections();
250265
for (Class<? extends Statement> st : scanner.getSubTypesOf(Statement.class))
251266
// the ignored fields are either mutable or auxiliary
252-
if (Expression.class.isAssignableFrom(st))
267+
if (Expression.class.isAssignableFrom(st)) {
268+
List<String> extra = new LinkedList<>();
253269
if (PluggableStatement.class.isAssignableFrom(st)
254270
// string statements are already pluggable-friendly
255271
|| st.getPackageName().equals("it.unive.lisa.program.cfg.statement.string"))
256-
verify(st, verifier -> verifier.withIgnoredFields("cfg", "offset", "runtimeTypes", "parent",
257-
"metaVariables", "originating"), Warning.NULL_FIELDS);
258-
else
259-
verify(st, verifier -> verifier.withIgnoredFields("cfg", "offset", "runtimeTypes", "parent",
260-
"metaVariables"), Warning.NULL_FIELDS);
261-
else
262-
verify(st, verifier -> verifier.withIgnoredFields("cfg", "offset"), Warning.NULL_FIELDS);
272+
extra.add("originating");
273+
if (Call.class.isAssignableFrom(st))
274+
extra.add("source");
275+
verify(st,
276+
verifier -> verifier
277+
.withIgnoredFields(ListUtils.union(expressionFields, extra).toArray(String[]::new)),
278+
Warning.NULL_FIELDS);
279+
} else
280+
verify(st, verifier -> verifier.withIgnoredFields(statementFields.toArray(String[]::new)),
281+
Warning.NULL_FIELDS);
263282
}
264283

265284
@Test

‎lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/BaseLattice.java‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ public abstract class BaseLattice<L extends BaseLattice<L>> implements Lattice<L
1414

1515
@Override
1616
@SuppressWarnings("unchecked")
17-
public final L lub(L other) throws SemanticException {
17+
public L lub(L other) throws SemanticException {
1818
if (other == null || other.isBottom() || this.isTop() || this == other || this.equals(other))
1919
return (L) this;
2020

@@ -46,7 +46,7 @@ public final L lub(L other) throws SemanticException {
4646

4747
@Override
4848
@SuppressWarnings("unchecked")
49-
public final L widening(L other) throws SemanticException {
49+
public L widening(L other) throws SemanticException {
5050
if (other == null || other.isBottom() || this.isTop() || this == other || this.equals(other))
5151
return (L) this;
5252

@@ -77,7 +77,7 @@ public final L widening(L other) throws SemanticException {
7777
protected abstract L wideningAux(L other) throws SemanticException;
7878

7979
@Override
80-
public final boolean lessOrEqual(L other) throws SemanticException {
80+
public boolean lessOrEqual(L other) throws SemanticException {
8181
if (other == null)
8282
return false;
8383

‎lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/CFGWithAnalysisResults.java‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -118,7 +118,7 @@ public void setId(String id) {
118118
*
119119
* @throws SemanticException if the lub operator fails
120120
*/
121-
public final AnalysisState<A, H, V> getAnalysisStateBefore(Statement st) throws SemanticException {
121+
public AnalysisState<A, H, V> getAnalysisStateBefore(Statement st) throws SemanticException {
122122
if (getEntrypoints().contains(st))
123123
return entryStates.getState(st);
124124
return lub(predecessorsOf(st), false);
@@ -131,7 +131,7 @@ public final AnalysisState<A, H, V> getAnalysisStateBefore(Statement st) throws
131131
*
132132
* @return the result computed at the given statement
133133
*/
134-
public final AnalysisState<A, H, V> getAnalysisStateAfter(Statement st) {
134+
public AnalysisState<A, H, V> getAnalysisStateAfter(Statement st) {
135135
return results.getState(st);
136136
}
137137

@@ -142,7 +142,7 @@ public final AnalysisState<A, H, V> getAnalysisStateAfter(Statement st) {
142142
*
143143
* @throws SemanticException if the lub operator fails
144144
*/
145-
public final AnalysisState<A, H, V> getEntryState() throws SemanticException {
145+
public AnalysisState<A, H, V> getEntryState() throws SemanticException {
146146
return lub(this.getEntrypoints(), true);
147147
}
148148

@@ -153,7 +153,7 @@ public final AnalysisState<A, H, V> getEntryState() throws SemanticException {
153153
*
154154
* @throws SemanticException if the lub operator fails
155155
*/
156-
public final AnalysisState<A, H, V> getExitState() throws SemanticException {
156+
public AnalysisState<A, H, V> getExitState() throws SemanticException {
157157
return lub(this.getNormalExitpoints(), false);
158158
}
159159

0 commit comments

Comments
 (0)