Skip to content

Commit

Permalink
Moved exposed ops to AbstractState to prepare for generics elimination
Browse files Browse the repository at this point in the history
  • Loading branch information
@lucaneg
lucaneg committed Sep 7, 2023
1 parent 55dac3b commit 4dbd26d
Show file tree
Hide file tree
Showing 12 changed files with 226 additions and 302 deletions.
72 changes: 58 additions & 14 deletions lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/SimpleAbstractState.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,11 @@
package it.unive.lisa.analysis;

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

import it.unive.lisa.DefaultParameters;
import it.unive.lisa.FallbackImplementation;
import it.unive.lisa.analysis.heap.HeapDomain;
Expand All @@ -18,11 +24,7 @@
import it.unive.lisa.symbolic.value.Identifier;
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.type.Type;
import java.util.Collection;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;
import java.util.function.Predicate;
import it.unive.lisa.type.Untyped;

/**
* An abstract state of the analysis, composed by a heap state modeling the
Expand All @@ -42,6 +44,27 @@ public class SimpleAbstractState<H extends HeapDomain<H>,
T extends TypeDomain<T>>
implements BaseLattice<SimpleAbstractState<H, V, T>>, AbstractState<SimpleAbstractState<H, V, T>, H, V, T> {

/**
* The key that should be used to store the instance of {@link HeapDomain}
* inside the {@link DomainRepresentation} returned by
* {@link #representation()}.
*/
public static final String HEAP_REPRESENTATION_KEY = "heap";

/**
* The key that should be used to store the instance of {@link TypeDomain}
* inside the {@link DomainRepresentation} returned by
* {@link #representation()}.
*/
public static final String TYPE_REPRESENTATION_KEY = "type";

/**
* The key that should be used to store the instance of {@link ValueDomain}
* inside the {@link DomainRepresentation} returned by
* {@link #representation()}.
*/
public static final String VALUE_REPRESENTATION_KEY = "value";

/**
* The domain containing information regarding heap structures
*/
Expand Down Expand Up @@ -76,17 +99,14 @@ public SimpleAbstractState(H heapState, V valueState, T typeState) {
this.typeState = typeState;
}

@Override
public H getHeapState() {
return heapState;
}

@Override
public V getValueState() {
return valueState;
}

@Override
public T getTypeState() {
return typeState;
}
Expand Down Expand Up @@ -394,17 +414,41 @@ public String toString() {
}

@Override
public SimpleAbstractState<H, V, T> withTopHeap() {
return new SimpleAbstractState<>(heapState.top(), valueState, typeState);
public ExpressionSet<SymbolicExpression> rewrite(
SymbolicExpression expression,
ProgramPoint pp)
throws SemanticException {
Set<SymbolicExpression> rewritten = new HashSet<>();
rewritten.addAll(heapState.rewrite(expression, pp).elements());
return new ExpressionSet<>(rewritten);
}

@Override
public ExpressionSet<SymbolicExpression> rewrite(
ExpressionSet<SymbolicExpression> expressions,
ProgramPoint pp)
throws SemanticException {
Set<SymbolicExpression> rewritten = new HashSet<>();
for (SymbolicExpression expression : expressions)
rewritten.addAll(heapState.rewrite(expression, pp).elements());
return new ExpressionSet<>(rewritten);
}

@Override
public SimpleAbstractState<H, V, T> withTopValue() {
return new SimpleAbstractState<>(heapState, valueState.top(), typeState);
public Set<Type> getRuntimeTypesOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException {
Set<Type> types = new HashSet<>();
for (SymbolicExpression ex : rewrite(e, pp))
types.addAll(typeState.getRuntimeTypesOf((ValueExpression) ex, pp));
return types;
}

@Override
public SimpleAbstractState<H, V, T> withTopType() {
return new SimpleAbstractState<>(heapState, valueState, typeState.top());
public Type getDynamicTypeOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException {
Set<Type> types = new HashSet<>();
for (SymbolicExpression ex : rewrite(e, pp))
types.add(typeState.getDynamicTypeOf((ValueExpression) ex, pp));
if (types.isEmpty())
return Untyped.INSTANCE;
return Type.commonSupertype(types, Untyped.INSTANCE);
}
}
149 changes: 61 additions & 88 deletions lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/traces/TracePartitioning.java
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,19 @@
package it.unive.lisa.analysis.traces;

import java.util.Collection;
import java.util.HashSet;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.function.Predicate;

import it.unive.lisa.analysis.AbstractState;
import it.unive.lisa.analysis.Lattice;
import it.unive.lisa.analysis.ScopeToken;
import it.unive.lisa.analysis.SemanticDomain;
import it.unive.lisa.analysis.SemanticException;
import it.unive.lisa.analysis.heap.HeapDomain;
import it.unive.lisa.analysis.lattices.ExpressionSet;
import it.unive.lisa.analysis.lattices.FunctionalLattice;
import it.unive.lisa.analysis.representation.DomainRepresentation;
import it.unive.lisa.analysis.representation.MapRepresentation;
Expand All @@ -18,10 +26,8 @@
import it.unive.lisa.program.cfg.controlFlow.Loop;
import it.unive.lisa.symbolic.SymbolicExpression;
import it.unive.lisa.symbolic.value.Identifier;
import java.util.Collection;
import java.util.Map;
import java.util.Map.Entry;
import java.util.function.Predicate;
import it.unive.lisa.type.Type;
import it.unive.lisa.type.Untyped;

/**
* The trace partitioning abstract domain that splits execution traces to
Expand Down Expand Up @@ -281,122 +287,89 @@ public DomainRepresentation representation() {
}

@Override
public H getHeapState() {
if (isTop())
return lattice.getHeapState().top();

H result = lattice.getHeapState().bottom();
if (isBottom() || function == null)
return result;

try {
for (Entry<ExecutionTrace, A> trace : this)
result = result.lub(trace.getValue().getHeapState());
} catch (SemanticException e) {
return result.bottom();
}
return result;
}

@Override
public V getValueState() {
if (isTop())
return lattice.getValueState().top();

V result = lattice.getValueState().bottom();
if (isBottom() || function == null)
return result;

try {
for (Entry<ExecutionTrace, A> trace : this)
result = result.lub(trace.getValue().getValueState());
} catch (SemanticException e) {
return result.bottom();
}
return result;
public TracePartitioning<A, H, V, T> mk(A lattice, Map<ExecutionTrace, A> function) {
return new TracePartitioning<>(lattice, function);
}

@Override
public T getTypeState() {
/**
* Collapses all of the traces contained in this domain, returning a unique
* abstract state that over-approximates all of them.
*
* @return the collapsed state
*/
public A collapse() {
if (isTop())
return lattice.getTypeState().top();
return lattice.top();

T result = lattice.getTypeState().bottom();
A result = lattice.bottom();
if (isBottom() || function == null)
return result;

try {
for (Entry<ExecutionTrace, A> trace : this)
result = result.lub(trace.getValue().getTypeState());
result = result.lub(trace.getValue());
} catch (SemanticException e) {
return result.bottom();
}
return result;
}

@Override
public TracePartitioning<A, H, V, T> withTopHeap() {
if (isTop() || isBottom() || function == null)
return this;

Map<ExecutionTrace, A> result = mkNewFunction(null, false);
for (Entry<ExecutionTrace, A> trace : this)
result.put(trace.getKey(), trace.getValue().withTopHeap());
return new TracePartitioning<>(lattice, result);
public String toString() {
return representation().toString();
}

@Override
public TracePartitioning<A, H, V, T> withTopValue() {
if (isTop() || isBottom() || function == null)
return this;
public ExpressionSet<SymbolicExpression> rewrite(SymbolicExpression expression, ProgramPoint pp)
throws SemanticException {
if (isTop())
return lattice.top().rewrite(expression, pp);
else if (isBottom() || function == null)
return lattice.bottom().rewrite(expression, pp);

Map<ExecutionTrace, A> result = mkNewFunction(null, false);
for (Entry<ExecutionTrace, A> trace : this)
result.put(trace.getKey(), trace.getValue().withTopValue());
return new TracePartitioning<>(lattice, result);
Set<SymbolicExpression> result = new HashSet<>();
for (A dom : getValues())
result.addAll(dom.rewrite(expression, pp).elements());
return new ExpressionSet<>(result);
}

@Override
public TracePartitioning<A, H, V, T> withTopType() {
if (isTop() || isBottom() || function == null)
return this;
public ExpressionSet<SymbolicExpression> rewrite(ExpressionSet<SymbolicExpression> expressions, ProgramPoint pp)
throws SemanticException {
if (isTop())
return lattice.top().rewrite(expressions, pp);
else if (isBottom() || function == null)
return lattice.bottom().rewrite(expressions, pp);

Map<ExecutionTrace, A> result = mkNewFunction(null, false);
for (Entry<ExecutionTrace, A> trace : this)
result.put(trace.getKey(), trace.getValue().withTopType());
return new TracePartitioning<>(lattice, result);
Set<SymbolicExpression> result = new HashSet<>();
for (A dom : getValues())
result.addAll(dom.rewrite(expressions, pp).elements());
return new ExpressionSet<>(result);
}

@Override
public TracePartitioning<A, H, V, T> mk(A lattice, Map<ExecutionTrace, A> function) {
return new TracePartitioning<>(lattice, function);
}

/**
* Collapses all of the traces contained in this domain, returning a unique
* abstract state that over-approximates all of them.
*
* @return the collapsed state
*/
public A collapse() {
public Set<Type> getRuntimeTypesOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException {
if (isTop())
return lattice.top();

A result = lattice.bottom();
if (isBottom() || function == null)
return result;
return lattice.top().getRuntimeTypesOf(e, pp);
else if (isBottom() || function == null)
return lattice.bottom().getRuntimeTypesOf(e, pp);

try {
for (Entry<ExecutionTrace, A> trace : this)
result = result.lub(trace.getValue());
} catch (SemanticException e) {
return result.bottom();
}
Set<Type> result = new HashSet<>();
for (A dom : getValues())
result.addAll(dom.getRuntimeTypesOf(e, pp));
return result;
}

@Override
public String toString() {
return representation().toString();
public Type getDynamicTypeOf(SymbolicExpression e, ProgramPoint pp) throws SemanticException {
if (isTop())
return lattice.top().getDynamicTypeOf(e, pp);
else if (isBottom() || function == null)
return lattice.bottom().getDynamicTypeOf(e, pp);

Set<Type> result = new HashSet<>();
for (A dom : getValues())
result.add(dom.getDynamicTypeOf(e, pp));
return Type.commonSupertype(result, Untyped.INSTANCE);
}
}
4 changes: 2 additions & 2 deletions lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -112,8 +112,8 @@ public boolean visit(
AnalysisState<?, ?, ?, ?> postR = result.getAnalysisStateAfter(assign.getRight());
InferenceSystem<NonInterference> right = postR.getDomainInstance(InferenceSystem.class);

for (SymbolicExpression l : postL.rewrite(postL.getComputedExpressions(), assign))
for (SymbolicExpression r : postR.rewrite(postR.getComputedExpressions(), assign)) {
for (SymbolicExpression l : postL.getState().rewrite(postL.getComputedExpressions(), assign))
for (SymbolicExpression r : postR.getState().rewrite(postR.getComputedExpressions(), assign)) {
NonInterference ll = left.eval((ValueExpression) l, assign.getLeft());
NonInterference rr = right.eval((ValueExpression) r, assign.getRight());

Expand Down
2 changes: 1 addition & 1 deletion lisa/lisa-analyses/src/test/java/it/unive/lisa/cron/taint/TaintAnalysesTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ public boolean visit(
MonolithicHeap, ValueEnvironment<T>,
TypeEnvironment<InferredTypes>> post = result
.getAnalysisStateAfter(call.getParameters()[i]);
for (SymbolicExpression e : post.rewrite(post.getComputedExpressions(),
for (SymbolicExpression e : post.getState().rewrite(post.getComputedExpressions(),
node)) {
T stack = post
.getState()
Expand Down
16 changes: 4 additions & 12 deletions lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAssert.java
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,7 @@
package it.unive.lisa.imp.expressions;

import java.util.Set;

import it.unive.lisa.analysis.AbstractState;
import it.unive.lisa.analysis.AnalysisState;
import it.unive.lisa.analysis.SemanticException;
Expand All @@ -14,7 +16,6 @@
import it.unive.lisa.program.cfg.statement.UnaryStatement;
import it.unive.lisa.symbolic.SymbolicExpression;
import it.unive.lisa.symbolic.value.Skip;
import it.unive.lisa.symbolic.value.ValueExpression;
import it.unive.lisa.type.Type;

/**
Expand All @@ -38,7 +39,6 @@ public IMPAssert(CFG cfg, String sourceFile, int line, int col, Expression expre
}

@Override
@SuppressWarnings("unchecked")
public <A extends AbstractState<A, H, V, T>,
H extends HeapDomain<H>,
V extends ValueDomain<V>,
Expand All @@ -48,16 +48,8 @@ T extends TypeDomain<T>> AnalysisState<A, H, V, T> unarySemantics(
SymbolicExpression expr,
StatementStore<A, H, V, T> expressions)
throws SemanticException {
Type type = null;
T typedom = (T) state.getDomainInstance(TypeDomain.class);
for (SymbolicExpression e : state.rewrite(expr, this)) {
Type inferred = typedom.getDynamicTypeOf((ValueExpression) e, this);
if (type == null)
type = inferred;
else
type = type.commonSupertype(inferred);
}
if (!type.isBooleanType())
Set<Type> types = state.getState().getRuntimeTypesOf(expr, this);
if (types.stream().noneMatch(Type::isBooleanType))
return state.bottom();
return state.smallStepSemantics(new Skip(getLocation()), this);
}
Expand Down
Loading

0 comments on commit 4dbd26d

Please sign in to comment.