diff --git a/src/main/java/it/unipr/analysis/taint/RandomnessDependencyAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/RandomnessDependencyAbstractDomain.java index 5bcb3a865..c08e526e5 100644 --- a/src/main/java/it/unipr/analysis/taint/RandomnessDependencyAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/RandomnessDependencyAbstractDomain.java @@ -6,26 +6,32 @@ import java.util.Set; public class RandomnessDependencyAbstractDomain extends TaintAbstractDomain { + private static final RandomnessDependencyAbstractDomain TOP = new RandomnessDependencyAbstractDomain( - createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); - private static final RandomnessDependencyAbstractDomain BOTTOM = new RandomnessDependencyAbstractDomain(null, + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), 0, 0, TaintElement.CLEAN); + private static final RandomnessDependencyAbstractDomain BOTTOM = new RandomnessDependencyAbstractDomain(null, 0, 0, TaintElement.BOTTOM); /** - * Builds an initial symbolic stack. + * Constructs a new {@code RandomnessDependencyAbstractDomain} with an empty + * (BOTTOM) stack, zero head/tail, and CLEAN memory state. */ public RandomnessDependencyAbstractDomain() { - this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), 0, 0, TaintElement.CLEAN); } /** - * Builds a taint abstract stack starting from a given stack and a list of - * elements that push taint. + * Constructs a new {@code RandomnessDependencyAbstractDomain} with the + * given stack state, stack pointers, and memory state. * - * @param stack the stack of values + * @param stack the stack array containing taint information for each + * element + * @param head the current head pointer of the stack + * @param tail the current tail pointer of the stack + * @param memory the taint state of the memory */ - protected RandomnessDependencyAbstractDomain(TaintElement[] stack, TaintElement memory) { - super(stack, memory); + protected RandomnessDependencyAbstractDomain(TaintElement[] stack, int head, int tail, TaintElement memory) { + super(stack, head, tail, memory); } @Override @@ -52,8 +58,7 @@ public RandomnessDependencyAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(TaintElement[] stack, TaintElement memory) { - return new RandomnessDependencyAbstractDomain(stack, memory); + public TaintAbstractDomain mk(TaintElement[] stack, int head, int tail, TaintElement memory) { + return new RandomnessDependencyAbstractDomain(stack, head, tail, memory); } - } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java index 7a73c465d..ae7215557 100644 --- a/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TaintAbstractDomain.java @@ -74,18 +74,30 @@ public abstract class TaintAbstractDomain private final TaintElement memory; /** - * Builds a taint abstract stack starting from a given stack and a list of - * elements that push taint. Builds a taint abstract stack starting from a - * given stack and a memory element. + * Builds a taint abstract stack starting from a given stack and a taint + * memory. Builds a taint abstract stack starting from a given stack and a + * memory element. * * @param stack the stack of values * @param memory the memory element */ protected TaintAbstractDomain(TaintElement[] stack, TaintElement memory) { + this(stack, 0, 0, memory); + } + + /** + * Builds a taint abstract stack starting from a given stack, its head + * index, its tail index and a taint memory. Builds a taint abstract stack + * starting from a given stack and a memory element. + * + * @param stack the stack of values + * @param memory the memory element + */ + protected TaintAbstractDomain(TaintElement[] stack, int head, int tail, TaintElement memory) { this.stack = stack; this.memory = memory; - this.head = 0; - this.tail = 0; + this.head = head; + this.tail = tail; } @Override @@ -187,7 +199,7 @@ public TaintAbstractDomain smallStepSemantics(ValueExpression expression, Progra resultStack.popX(3); if (this.isTainted((Statement) pp)) - return mk(resultStack.stack, TaintElement.TAINT); + return mk(resultStack.stack, resultStack.head, resultStack.tail, TaintElement.TAINT); return resultStack; } @@ -233,7 +245,7 @@ else if (memory.isClean()) TaintElement value = resultStack.pop(); if (value.isTaint()) - return mk(resultStack.stack, TaintElement.TAINT); + return mk(resultStack.stack, resultStack.head, resultStack.tail, TaintElement.TAINT); else if (value.isClean()) return resultStack; } @@ -749,7 +761,7 @@ public TaintAbstractDomain glbAux(TaintAbstractDomain other) throws SemanticExce for (int i = 0; i < STACK_LIMIT; i++) { result[i] = this.get(i).glb(other.get(i)); } - return mk(result, this.memory.glb(other.memory)); + return mk(result, this.head, this.tail, this.memory.glb(other.memory)); } /** @@ -767,7 +779,7 @@ public TaintAbstractDomain lubAux(TaintAbstractDomain other) throws SemanticExce for (int i = 0; i < STACK_LIMIT; i++) { result[i] = this.get(i).lub(other.get(i)); } - return mk(result, this.memory.lub(other.memory)); + return mk(result, this.head, this.tail, this.memory.lub(other.memory)); } /** @@ -859,7 +871,7 @@ public boolean hasBottomUntil(int x) { @Override public TaintAbstractDomain clone() { TaintElement[] newArray = stack.clone(); - TaintAbstractDomain copy = mk(newArray, memory); + TaintAbstractDomain copy = mk(newArray, head, tail, memory); copy.head = this.head; copy.tail = this.tail; return copy; @@ -955,12 +967,14 @@ else if (isTop()) /** * Utility for creating a concrete instance of {@link TaintAbstractDomain} - * given the stack and the memory. + * given the stack, its head index, its tail index and the memory. * * @param stack the stack + * @param head the head index + * @param tail the tail index * @param memory the memory * * @return a new concrete instance of {@link TaintAbstractDomain} */ - public abstract TaintAbstractDomain mk(TaintElement[] stack, TaintElement memory); + public abstract TaintAbstractDomain mk(TaintElement[] stack, int head, int tail, TaintElement memory); } \ No newline at end of file diff --git a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java index 83fc3980e..5edc4aef4 100644 --- a/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java +++ b/src/main/java/it/unipr/analysis/taint/TxOriginAbstractDomain.java @@ -8,24 +8,29 @@ public class TxOriginAbstractDomain extends TaintAbstractDomain { private static final TxOriginAbstractDomain TOP = new TxOriginAbstractDomain( - createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); - private static final TxOriginAbstractDomain BOTTOM = new TxOriginAbstractDomain(null, TaintElement.BOTTOM); + createFilledArray(TaintAbstractDomain.STACK_LIMIT, TaintElement.BOTTOM), 0, 0, TaintElement.CLEAN); + private static final TxOriginAbstractDomain BOTTOM = new TxOriginAbstractDomain(null, 0, 0, TaintElement.BOTTOM); /** - * Builds an initial symbolic stack. + * Constructs a new {@code TxOriginAbstractDomain} with an empty (BOTTOM) + * stack, zero head/tail, and CLEAN memory state. */ public TxOriginAbstractDomain() { - this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), TaintElement.CLEAN); + this(createFilledArray(STACK_LIMIT, TaintElement.BOTTOM), 0, 0, TaintElement.CLEAN); } /** - * Builds a taint abstract stack starting from a given stack and a list of - * elements that push taint. + * Constructs a new {@code TxOriginAbstractDomain} with the given stack + * state, stack pointers, and memory state. * - * @param stack the stack of values + * @param stack the stack array containing taint information for each + * element + * @param head the current head pointer of the stack + * @param tail the current tail pointer of the stack + * @param memory the taint state of the memory */ - protected TxOriginAbstractDomain(TaintElement[] stack, TaintElement memory) { - super(stack, memory); + protected TxOriginAbstractDomain(TaintElement[] stack, int head, int tail, TaintElement memory) { + super(stack, head, tail, memory); } @Override @@ -49,7 +54,7 @@ public TxOriginAbstractDomain bottom() { } @Override - public TaintAbstractDomain mk(TaintElement[] stack, TaintElement memory) { - return new TxOriginAbstractDomain(stack, memory); + public TaintAbstractDomain mk(TaintElement[] stack, int head, int tail, TaintElement memory) { + return new TxOriginAbstractDomain(stack, head, tail, memory); } }