Fixed RelationalTaintAbstractDomain to support head and tail indices in constructors and methods

Author: merendamattia

src/main/java/it/unipr/crosschain/taint/AccessControlIncompletenessAbstractDomain.java

@@ -7,16 +7,16 @@
 
 public class AccessControlIncompletenessAbstractDomain extends RelationalTaintAbstractDomain {
 	private static final AccessControlIncompletenessAbstractDomain TOP = new AccessControlIncompletenessAbstractDomain(
-			createFilledArray(RelationalTaintAbstractDomain.STACK_LIMIT, RelationalTaintElement.BOTTOM),
+			createFilledArray(RelationalTaintAbstractDomain.STACK_LIMIT, RelationalTaintElement.BOTTOM), 0, 0,
 			RelationalTaintElement.CLEAN);
 	private static final AccessControlIncompletenessAbstractDomain BOTTOM = new AccessControlIncompletenessAbstractDomain(
-			null, RelationalTaintElement.BOTTOM);
+			null, 0, 0, RelationalTaintElement.BOTTOM);
 
 	/**
 	 * Builds an initial symbolic stack.
 	 */
 	public AccessControlIncompletenessAbstractDomain() {
-		this(createFilledArray(STACK_LIMIT, RelationalTaintElement.BOTTOM), RelationalTaintElement.CLEAN);
+		this(createFilledArray(STACK_LIMIT, RelationalTaintElement.BOTTOM), 0, 0, RelationalTaintElement.CLEAN);
 	}
 
 	/**
@@ -26,8 +26,9 @@ public AccessControlIncompletenessAbstractDomain() {
 	 * @param stack  the stack of values
 	 * @param memory the taint associated with linear memory
 	 */
-	protected AccessControlIncompletenessAbstractDomain(RelationalTaintElement[] stack, RelationalTaintElement memory) {
-		super(stack, memory);
+	protected AccessControlIncompletenessAbstractDomain(RelationalTaintElement[] stack, int head, int tail,
+			RelationalTaintElement memory) {
+		super(stack, head, tail, memory);
 	}
 
 	@Override
@@ -56,7 +57,8 @@ public AccessControlIncompletenessAbstractDomain bottom() {
 	}
 
 	@Override
-	public RelationalTaintAbstractDomain mk(RelationalTaintElement[] stack, RelationalTaintElement memory) {
-		return new AccessControlIncompletenessAbstractDomain(stack, memory);
+	public RelationalTaintAbstractDomain mk(RelationalTaintElement[] stack, int head, int tail,
+			RelationalTaintElement memory) {
+		return new AccessControlIncompletenessAbstractDomain(stack, head, tail, memory);
 	}
 }

src/main/java/it/unipr/crosschain/taint/RelationalTaintAbstractDomain.java

@@ -75,10 +75,26 @@ public abstract class RelationalTaintAbstractDomain
 	 * @param memory the memory element
 	 */
 	protected RelationalTaintAbstractDomain(RelationalTaintElement[] stack, RelationalTaintElement memory) {
+		this(stack, 0, 0, memory);
+	}
+
+	/**
+	 * Builds a taint abstract stack starting from a given stack, a list of
+	 * elements that push taint, the head and the tail of the given stack.
+	 * 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
+	 * @param head   the head index of the circular stack
+	 * @param tail   the tail index of the circular stack
+	 */
+	protected RelationalTaintAbstractDomain(RelationalTaintElement[] stack, int head, int tail,
+			RelationalTaintElement memory) {
 		this.stack = stack;
 		this.memory = memory;
-		this.head = 0;
-		this.tail = 0;
+		this.head = head;
+		this.tail = tail;
 	}
 
 	@Override
@@ -185,7 +201,7 @@ public RelationalTaintAbstractDomain smallStepSemantics(ValueExpression expressi
 
 					Statement stmt = (Statement) pp;
 					if (this.isTainted(stmt))
-						return mk(resultStack.stack, RelationalTaintElement
+						return mk(resultStack.stack, resultStack.head, resultStack.tail, RelationalTaintElement
 								.newRelationalTaintedElement(((ProgramCounterLocation) stmt.getLocation()).getPc()));
 
 					return resultStack;
@@ -235,7 +251,7 @@ else if (memory.isClean())
 					RelationalTaintElement value = resultStack.pop();
 
 					if (value.isTaint())
-						return mk(resultStack.stack,
+						return mk(resultStack.stack, resultStack.head, resultStack.tail,
 								RelationalTaintElement.newRelationalTaintedElement(value.getProgramPoints()));
 					else if (value.isClean())
 						return resultStack;
@@ -766,7 +782,7 @@ public RelationalTaintAbstractDomain glbAux(RelationalTaintAbstractDomain other)
 		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, head, tail, this.memory.glb(other.memory));
 	}
 
 	/**
@@ -784,7 +800,7 @@ public RelationalTaintAbstractDomain lubAux(RelationalTaintAbstractDomain other)
 		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, head, tail, this.memory.lub(other.memory));
 	}
 
 	/**
@@ -876,7 +892,7 @@ public boolean hasBottomUntil(int x) {
 	@Override
 	public RelationalTaintAbstractDomain clone() {
 		RelationalTaintElement[] newArray = stack.clone();
-		RelationalTaintAbstractDomain copy = mk(newArray, memory);
+		RelationalTaintAbstractDomain copy = mk(newArray, head, tail, memory);
 		copy.head = this.head;
 		copy.tail = this.tail;
 		return copy;
@@ -979,5 +995,6 @@ else if (isTop())
 	 *
 	 * @return a new concrete instance of {@link RelationalTaintAbstractDomain}
 	 */
-	public abstract RelationalTaintAbstractDomain mk(RelationalTaintElement[] stack, RelationalTaintElement memory);
+	public abstract RelationalTaintAbstractDomain mk(RelationalTaintElement[] stack, int head, int tail,
+			RelationalTaintElement memory);
 }