Skip to content

Commit

Permalink
renamed JoinLattice to MeetLattice and joinWith to meetWith etc. beca…
Browse files Browse the repository at this point in the history
…use previously it was all rather confusion: we are, in fact, implementing a meet lattice, so we should also name it that way
  • Loading branch information
Eric Bodden committed Nov 14, 2019
1 parent ba6536c commit 8e59e82
Show file tree
Hide file tree
Showing 10 changed files with 44 additions and 34 deletions.
6 changes: 3 additions & 3 deletions src/heros/EdgeFunction.java
Expand Up @@ -36,12 +36,12 @@ public interface EdgeFunction<V> {
EdgeFunction<V> composeWith(EdgeFunction<V> secondFunction);

/**
* Returns a function that represents that (element-wise) join
* Returns a function that represents that (element-wise) meet
* of this function with otherFunction. Naturally, this is a
* symmetric operation.
* @see JoinLattice#join(Object, Object)
* @see MeetLattice#meet(Object, Object)
*/
EdgeFunction<V> joinWith(EdgeFunction<V> otherFunction);
EdgeFunction<V> meetWith(EdgeFunction<V> otherFunction);

/**
* Returns true is this function represents exactly the same
Expand Down
8 changes: 4 additions & 4 deletions src/heros/IDETabulationProblem.java
Expand Up @@ -17,8 +17,8 @@
* of type D maps at any program point to a value of type V. The functions describe how
* values are transformed when moving from one statement to another.
*
* The problem further defines a {@link JoinLattice}, which describes how values of
* type V are joined (merged) when multiple values are possible.
* The problem further defines a {@link MeetLattice}, which describes how values of
* type V are merged (via a meet operation) when multiple values are possible.
*
* @param <N> The type of nodes in the interprocedural control-flow graph. Typically {@link Unit}.
* @param <D> The type of data-flow facts to be computed by the tabulation problem.
Expand All @@ -35,9 +35,9 @@ public interface IDETabulationProblem<N,D,M,V,I extends InterproceduralCFG<N,M>>
EdgeFunctions<N,D,M,V> edgeFunctions();

/**
* Returns the lattice describing how values of type V need to be joined.
* Returns the lattice describing how to compute the meet of two V values.
*/
JoinLattice<V> joinLattice();
MeetLattice<V> meetLattice();

/**
* Returns a function mapping everything to top.
Expand Down
16 changes: 13 additions & 3 deletions src/heros/JoinLattice.java → src/heros/MeetLattice.java
Expand Up @@ -12,16 +12,26 @@

/**
* This class defines a lattice in terms of its top and bottom elements
* and a join operation.
* and a meet operation. This is meant to be a complete lattice, with a unique top and bottom element.
*
* @param <V> The domain type for this lattice.
*/
public interface JoinLattice<V> {
public interface MeetLattice<V> {

/**
* Returns the unique top element of this lattice.
*/
V topElement();

/**
* Returns the unique bottom element of this lattice.
*/
V bottomElement();

V join(V left, V right);
/**
* Computes the meet of left and right. Note that <pre>meet(top,x) = meet(x,top) = x</pre> and
* <pre>meet(bottom,x) = meet(x,bottom) = bottom</pre>.
*/
V meet(V left, V right);

}
2 changes: 1 addition & 1 deletion src/heros/edgefunc/AllBottom.java
Expand Up @@ -31,7 +31,7 @@ public EdgeFunction<V> composeWith(EdgeFunction<V> secondFunction) {
return secondFunction;
}

public EdgeFunction<V> joinWith(EdgeFunction<V> otherFunction) {
public EdgeFunction<V> meetWith(EdgeFunction<V> otherFunction) {
if(otherFunction == this || otherFunction.equalTo(this)) return this;
if(otherFunction instanceof AllTop) {
return this;
Expand Down
2 changes: 1 addition & 1 deletion src/heros/edgefunc/AllTop.java
Expand Up @@ -29,7 +29,7 @@ public EdgeFunction<V> composeWith(EdgeFunction<V> secondFunction) {
return this;
}

public EdgeFunction<V> joinWith(EdgeFunction<V> otherFunction) {
public EdgeFunction<V> meetWith(EdgeFunction<V> otherFunction) {
return otherFunction;
}

Expand Down
6 changes: 3 additions & 3 deletions src/heros/edgefunc/EdgeIdentity.java
Expand Up @@ -31,16 +31,16 @@ public EdgeFunction<V> composeWith(EdgeFunction<V> secondFunction) {
return secondFunction;
}

public EdgeFunction<V> joinWith(EdgeFunction<V> otherFunction) {
public EdgeFunction<V> meetWith(EdgeFunction<V> otherFunction) {
if(otherFunction == this || otherFunction.equalTo(this)) return this;
if(otherFunction instanceof AllBottom) {
return otherFunction;
}
if(otherFunction instanceof AllTop) {
return this;
}
//do not know how to join; hence ask other function to decide on this
return otherFunction.joinWith(this);
//do not know how to meet; hence ask other function to decide on this
return otherFunction.meetWith(this);
}

public boolean equalTo(EdgeFunction<V> other) {
Expand Down
6 changes: 3 additions & 3 deletions src/heros/solver/BiDiIDESolver.java
Expand Up @@ -17,7 +17,7 @@
import heros.IDETabulationProblem;
import heros.IFDSTabulationProblem;
import heros.InterproceduralCFG;
import heros.JoinLattice;
import heros.MeetLattice;
import heros.solver.IFDSSolver.BinaryDomain;

import java.util.Collections;
Expand Down Expand Up @@ -479,8 +479,8 @@ public EdgeFunction<V> getCallToReturnEdgeFunction(N callSite, AbstractionWithSo
}

@Override
public JoinLattice<V> joinLattice() {
return delegate.joinLattice();
public MeetLattice<V> meetLattice() {
return delegate.meetLattice();
}

@Override
Expand Down
16 changes: 8 additions & 8 deletions src/heros/solver/IDESolver.java
Expand Up @@ -23,7 +23,7 @@
import heros.FlowFunctions;
import heros.IDETabulationProblem;
import heros.InterproceduralCFG;
import heros.JoinLattice;
import heros.MeetLattice;
import heros.SynchronizedBy;
import heros.ZeroedFlowFunctions;
import heros.edgefunc.EdgeIdentity;
Expand Down Expand Up @@ -117,7 +117,7 @@ public class IDESolver<N,D,M,V,I extends InterproceduralCFG<N, M>> {
protected final Map<N,Set<D>> initialSeeds;

@DontSynchronize("stateless")
protected final JoinLattice<V> valueLattice;
protected final MeetLattice<V> valueLattice;

@DontSynchronize("stateless")
protected final EdgeFunction<V> allTop;
Expand Down Expand Up @@ -199,7 +199,7 @@ public IDESolver(IDETabulationProblem<N,D,M,V,I> tabulationProblem, @SuppressWar
this.edgeFunctions = edgeFunctions;
this.initialSeeds = tabulationProblem.initialSeeds();
this.unbalancedRetSites = Collections.newSetFromMap(new ConcurrentHashMap<N, Boolean>());
this.valueLattice = tabulationProblem.joinLattice();
this.valueLattice = tabulationProblem.meetLattice();
this.allTop = tabulationProblem.allTopFunction();
this.jumpFn = new JumpFunctions<N,D,V>(allTop);
this.followReturnsPastSeeds = tabulationProblem.followReturnsPastSeeds();
Expand Down Expand Up @@ -640,7 +640,7 @@ protected void propagate(D sourceVal, N target, D targetVal, EdgeFunction<V> f,
synchronized (jumpFn) {
jumpFnE = jumpFn.reverseLookup(target, targetVal).get(sourceVal);
if(jumpFnE==null) jumpFnE = allTop; //JumpFn is initialized to all-top (see line [2] in SRH96 paper)
fPrime = jumpFnE.joinWith(f);
fPrime = jumpFnE.meetWith(f);
newFunction = !fPrime.equalTo(jumpFnE);
if(newFunction) {
jumpFn.addFunction(sourceVal, target, targetVal, fPrime);
Expand Down Expand Up @@ -746,14 +746,14 @@ private void propagateValueAtCall(Pair<N, D> nAndD, N n) {
}
}

protected V joinValueAt(N unit, D fact, V curr, V newVal) {
return valueLattice.join(curr, newVal);
protected V meetValueAt(N unit, D fact, V curr, V newVal) {
return valueLattice.meet(curr, newVal);
}

private void propagateValue(N nHashN, D nHashD, V v) {
synchronized (val) {
V valNHash = val(nHashN, nHashD);
V vPrime = joinValueAt(nHashN, nHashD, valNHash,v);
V vPrime = meetValueAt(nHashN, nHashD, valNHash,v);
if(!vPrime.equals(valNHash)) {
setVal(nHashN, nHashD, vPrime);
scheduleValueProcessing(new ValuePropagationTask(new Pair<N,D>(nHashN,nHashD)));
Expand Down Expand Up @@ -946,7 +946,7 @@ public void run() {
D d = sourceValTargetValAndFunction.getColumnKey();
EdgeFunction<V> fPrime = sourceValTargetValAndFunction.getValue();
synchronized (val) {
setVal(n,d,valueLattice.join(val(n,d),fPrime.computeTarget(val(sP,dPrime))));
setVal(n,d,valueLattice.meet(val(n,d),fPrime.computeTarget(val(sP,dPrime))));
}
flowFunctionApplicationCount++;
}
Expand Down
8 changes: 4 additions & 4 deletions src/heros/solver/IFDSSolver.java
Expand Up @@ -18,7 +18,7 @@
import heros.IDETabulationProblem;
import heros.IFDSTabulationProblem;
import heros.InterproceduralCFG;
import heros.JoinLattice;
import heros.MeetLattice;
import heros.edgefunc.AllBottom;
import heros.edgefunc.AllTop;
import heros.edgefunc.EdgeIdentity;
Expand Down Expand Up @@ -76,8 +76,8 @@ public EdgeFunctions<N,D,M,BinaryDomain> edgeFunctions() {
return new IFDSEdgeFunctions();
}

public JoinLattice<BinaryDomain> joinLattice() {
return new JoinLattice<BinaryDomain>() {
public MeetLattice<BinaryDomain> meetLattice() {
return new MeetLattice<BinaryDomain>() {

public BinaryDomain topElement() {
return BinaryDomain.TOP;
Expand All @@ -87,7 +87,7 @@ public BinaryDomain bottomElement() {
return BinaryDomain.BOTTOM;
}

public BinaryDomain join(BinaryDomain left, BinaryDomain right) {
public BinaryDomain meet(BinaryDomain left, BinaryDomain right) {
if(left==TOP && right==TOP) {
return TOP;
} else {
Expand Down
8 changes: 4 additions & 4 deletions src/heros/template/DefaultIDETabulationProblem.java
Expand Up @@ -14,7 +14,7 @@
import heros.EdgeFunctions;
import heros.IDETabulationProblem;
import heros.InterproceduralCFG;
import heros.JoinLattice;
import heros.MeetLattice;

/**
* This is a template for {@link IDETabulationProblem}s that automatically caches values
Expand All @@ -31,7 +31,7 @@ public abstract class DefaultIDETabulationProblem<N,D,M,V,I extends Interprocedu
extends DefaultIFDSTabulationProblem<N,D,M,I> implements IDETabulationProblem<N,D,M,V,I>{

private final EdgeFunction<V> allTopFunction;
private final JoinLattice<V> joinLattice;
private final MeetLattice<V> joinLattice;
private final EdgeFunctions<N,D,M,V> edgeFunctions;

public DefaultIDETabulationProblem(I icfg) {
Expand All @@ -43,7 +43,7 @@ public DefaultIDETabulationProblem(I icfg) {

protected abstract EdgeFunction<V> createAllTopFunction();

protected abstract JoinLattice<V> createJoinLattice();
protected abstract MeetLattice<V> createJoinLattice();

protected abstract EdgeFunctions<N,D,M,V> createEdgeFunctionsFactory();

Expand All @@ -53,7 +53,7 @@ public final EdgeFunction<V> allTopFunction() {
}

@Override
public final JoinLattice<V> joinLattice() {
public final MeetLattice<V> meetLattice() {
return joinLattice;
}

Expand Down

0 comments on commit 8e59e82

Please sign in to comment.