Merge pull request #59 from lisa-analyzer/fix/mk-method-in-taint-analysis

Add head and tail parameters to constructors and mk methods

Author: VincenzoArceri

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);
 	}
-
 }

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);
 }

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);
 	}
 }