Skip to content

Commit

Permalink
Merge pull request #259 from lisa-analyzer/base-interfaces
Browse files Browse the repository at this point in the history
Base interfaces
  • Loading branch information
VincenzoArceri authored Dec 14, 2022
2 parents e3f8730 + 2cbda41 commit 7abfaf2
Show file tree
Hide file tree
Showing 49 changed files with 452 additions and 299 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -36,8 +36,7 @@
public class SimpleAbstractState<H extends HeapDomain<H>,
V extends ValueDomain<V>,
T extends TypeDomain<T>>
extends BaseLattice<SimpleAbstractState<H, V, T>>
implements AbstractState<SimpleAbstractState<H, V, T>, H, V, T> {
implements BaseLattice<SimpleAbstractState<H, V, T>>, AbstractState<SimpleAbstractState<H, V, T>, H, V, T> {

/**
* The domain containing information regarding heap structures
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
public abstract class NonRelationalValueCartesianProduct<C extends NonRelationalValueCartesianProduct<C, T1, T2>,
T1 extends NonRelationalValueDomain<T1>,
T2 extends NonRelationalValueDomain<T2>>
extends BaseNonRelationalValueDomain<C> {
implements BaseNonRelationalValueDomain<C> {

/**
* The left-hand side abstract domain.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
* @author <a href="mailto:[email protected]">Luca Negrini</a>
*/
@FallbackImplementation
public class MonolithicHeap extends BaseHeapDomain<MonolithicHeap> {
public class MonolithicHeap implements BaseHeapDomain<MonolithicHeap> {

private static final MonolithicHeap TOP = new MonolithicHeap();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@
*
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class TypeBasedHeap extends BaseHeapDomain<TypeBasedHeap> {
public class TypeBasedHeap implements BaseHeapDomain<TypeBasedHeap> {

private static final TypeBasedHeap TOP = new TypeBasedHeap();

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
* @see <a href=
* "https://mitpress.mit.edu/books/introduction-static-analysis">https://mitpress.mit.edu/books/introduction-static-analysis</a>
*/
public class PointBasedHeap extends BaseHeapDomain<PointBasedHeap> {
public class PointBasedHeap implements BaseHeapDomain<PointBasedHeap> {

/**
* An heap environment tracking which allocation sites are associated to
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
* @see <a href=
* "https://en.wikipedia.org/wiki/Non-interference_(security)">Non-interference</a>
*/
public class NonInterference extends BaseInferredValue<NonInterference> {
public class NonInterference implements BaseInferredValue<NonInterference> {

/**
* The annotation used to mark low confidentiality variables.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@
*
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class IntegerConstantPropagation extends BaseNonRelationalValueDomain<IntegerConstantPropagation> {
public class IntegerConstantPropagation implements BaseNonRelationalValueDomain<IntegerConstantPropagation> {

private static final IntegerConstantPropagation TOP = new IntegerConstantPropagation(true, false);
private static final IntegerConstantPropagation BOTTOM = new IntegerConstantPropagation(false, true);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
@FallbackImplementation
public class Interval extends BaseNonRelationalValueDomain<Interval> {
public class Interval implements BaseNonRelationalValueDomain<Interval> {

/**
* The abstract zero ({@code [0, 0]}) element.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
*
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class Parity extends BaseNonRelationalValueDomain<Parity> {
public class Parity implements BaseNonRelationalValueDomain<Parity> {

/**
* The abstract even element.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@
*
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class Sign extends BaseNonRelationalValueDomain<Sign> {
public class Sign implements BaseNonRelationalValueDomain<Sign> {

/**
* The abstract positive element.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@
* "https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34">
* https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34</a>
*/
public class CharInclusion extends BaseNonRelationalValueDomain<CharInclusion> {
public class CharInclusion implements BaseNonRelationalValueDomain<CharInclusion> {

private final Set<Character> certainlyContained;

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
* "https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34">
* https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34</a>
*/
public class Prefix extends BaseNonRelationalValueDomain<Prefix> {
public class Prefix implements BaseNonRelationalValueDomain<Prefix> {

private final static Prefix TOP = new Prefix();
private final static Prefix BOTTOM = new Prefix(null);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
* "https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34">
* https://link.springer.com/chapter/10.1007/978-3-642-24559-6_34</a>
*/
public class Suffix extends BaseNonRelationalValueDomain<Suffix> {
public class Suffix implements BaseNonRelationalValueDomain<Suffix> {

private final static Suffix TOP = new Suffix();
private final static Suffix BOTTOM = new Suffix(null);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,6 @@
import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
import it.unive.lisa.symbolic.value.operator.binary.StringConcat;
import it.unive.lisa.symbolic.value.operator.binary.StringContains;
import it.unive.lisa.symbolic.value.operator.ternary.TernaryOperator;
import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
import java.util.Objects;
import java.util.Set;
import java.util.SortedSet;
Expand All @@ -23,7 +21,7 @@
* @author <a href="mailto:[email protected]">Simone Leoni</a>
* @author <a href="mailto:[email protected]">Vincenzo Arceri</a>
*/
public class FSA extends BaseNonRelationalValueDomain<FSA> {
public class FSA implements BaseNonRelationalValueDomain<FSA> {
/**
* Used to store the string representation
*/
Expand Down Expand Up @@ -119,12 +117,7 @@ public FSA evalNonNullConstant(Constant constant, ProgramPoint pp) throws Semant
return top();
}

@Override
public FSA evalUnaryExpression(UnaryOperator operator, FSA arg, ProgramPoint pp) throws SemanticException {
// TODO
return super.evalUnaryExpression(operator, arg, pp);
}

// TODO unary and ternary and all other binary
@Override
public FSA evalBinaryExpression(BinaryOperator operator, FSA left, FSA right, ProgramPoint pp)
throws SemanticException {
Expand All @@ -133,13 +126,6 @@ public FSA evalBinaryExpression(BinaryOperator operator, FSA left, FSA right, Pr
return top();
}

@Override
public FSA evalTernaryExpression(TernaryOperator operator, FSA left, FSA middle, FSA right, ProgramPoint pp)
throws SemanticException {
// TODO
return super.evalTernaryExpression(operator, left, middle, right, pp);
}

@Override
public SemanticDomain.Satisfiability satisfiesBinaryExpression(BinaryOperator operator, FSA left, FSA right,
ProgramPoint pp) throws SemanticException {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
* @author <a href="mailto:[email protected]">Luca Negrini</a>
*/
@FallbackImplementation
public class InferredTypes extends BaseNonRelationalTypeDomain<InferredTypes> {
public class InferredTypes implements BaseNonRelationalTypeDomain<InferredTypes> {

private static final InferredTypes BOTTOM = new InferredTypes(null, Collections.emptySet());

Expand Down Expand Up @@ -114,7 +114,7 @@ public InferredTypes top() {

@Override
public boolean isTop() {
return super.isTop() || isTop;
return BaseNonRelationalTypeDomain.super.isTop() || isTop;
}

@Override
Expand All @@ -124,7 +124,7 @@ public InferredTypes bottom() {

@Override
public boolean isBottom() {
return super.isBottom() || BOTTOM.elements.equals(elements);
return BaseNonRelationalTypeDomain.super.isBottom() || BOTTOM.elements.equals(elements);
}

@Override
Expand All @@ -141,7 +141,7 @@ public DomainRepresentation representation() {
@Override
public InferredTypes evalIdentifier(Identifier id, TypeEnvironment<InferredTypes> environment,
ProgramPoint pp) throws SemanticException {
InferredTypes eval = super.evalIdentifier(id, environment, pp);
InferredTypes eval = BaseNonRelationalTypeDomain.super.evalIdentifier(id, environment, pp);
if (!eval.isTop() && !eval.isBottom())
return eval;
TypeSystem types = pp.getProgram().getTypes();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@
*
* @author <a href="mailto:[email protected]">Luca Negrini</a>
*/
public class StaticTypes extends BaseNonRelationalTypeDomain<StaticTypes> {
public class StaticTypes implements BaseNonRelationalTypeDomain<StaticTypes> {

private static final StaticTypes BOTTOM = new StaticTypes(null, null);

Expand Down Expand Up @@ -103,7 +103,7 @@ public DomainRepresentation representation() {
@Override
public StaticTypes evalIdentifier(Identifier id, TypeEnvironment<StaticTypes> environment,
ProgramPoint pp) throws SemanticException {
StaticTypes eval = super.evalIdentifier(id, environment, pp);
StaticTypes eval = BaseNonRelationalTypeDomain.super.evalIdentifier(id, environment, pp);
if (!eval.isTop() && !eval.isBottom())
return eval;
return new StaticTypes(pp.getProgram().getTypes(), id.getStaticType());
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@

public class BaseInferredValueTest {

private static class Sample extends BaseInferredValue<Sample> {
private static class Sample implements BaseInferredValue<Sample> {

@Override
public DomainRepresentation representation() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@

public class BaseNonRelationalTypeDomainTest {

private static class Sample extends BaseNonRelationalTypeDomain<Sample> {
private static class Sample implements BaseNonRelationalTypeDomain<Sample> {

@Override
public DomainRepresentation representation() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@

public class BaseNonRelationalValueDomainTest {

private static class Sample extends BaseNonRelationalValueDomain<Sample> {
private static class Sample implements BaseNonRelationalValueDomain<Sample> {

@Override
public DomainRepresentation representation() {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@
import it.unive.lisa.program.annotations.values.StringAnnotationValue;
import java.util.ArrayList;
import java.util.List;
import java.util.Set;
import java.util.TreeSet;

/**
* An {@link IMPParserBaseVisitor} that will parse annotations from IMP code.
Expand All @@ -33,7 +35,7 @@ public class IMPAnnotationVisitor extends IMPParserBaseVisitor<Object> {
public Annotations visitAnnotations(AnnotationsContext ctx) {
if (ctx == null)
return new Annotations();
List<Annotation> anns = new ArrayList<>();
Set<Annotation> anns = new TreeSet<>();
for (int i = 0; i < ctx.annotation().size(); i++)
anns.add(visitAnnotation(ctx.annotation(i)));
return new Annotations(anns);
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ public class AnalysisState<A extends AbstractState<A, H, V, T>,
H extends HeapDomain<H>,
V extends ValueDomain<V>,
T extends TypeDomain<T>>
extends BaseLattice<AnalysisState<A, H, V, T>> implements
implements BaseLattice<AnalysisState<A, H, V, T>>,
SemanticDomain<AnalysisState<A, H, V, T>, SymbolicExpression, Identifier> {

/**
Expand Down
Loading

0 comments on commit 7abfaf2

Please sign in to comment.