Fixed DIV

lisa-analyzer · Mar 3, 2024 · 0e594a0 · 0e594a0
1 parent 7d775ad
commit 0e594a0
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 12 deletions.
diff --git a/src/main/java/it/unipr/analysis/EVMAbstractState.java b/src/main/java/it/unipr/analysis/EVMAbstractState.java
@@ -475,8 +475,16 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 						AbstractStack resultStack = stack.clone();
 						KIntegerSet opnd1 = resultStack.pop();
 						KIntegerSet opnd2 = resultStack.pop();
-
-						resultStack.push(opnd1.div(opnd2));
+//						System.err.println(opnd1 + " " + opnd2);
+//						System.err.println(opnd2.equals(KIntegerSet.ZERO) && !opnd1.isTop());
+//						
+//						resultStack.push(opnd1.div(opnd2));
+//						resultStack.push(opnd2.equals(KIntegerSet.ZERO) && !opnd1.isTop() ? KIntegerSet.ZERO : opnd1.div(opnd2));
+						try {
+							resultStack.push(opnd1.div(opnd2));
+						} catch (ArithmeticException e) {
+							resultStack.push(KIntegerSet.ZERO);
+						}
 						result.add(resultStack);
 					}
 
@@ -490,7 +498,12 @@ public EVMAbstractState smallStepSemantics(ValueExpression expression, ProgramPo
 						KIntegerSet opnd1 = resultStack.pop();
 						KIntegerSet opnd2 = resultStack.pop();
 
-						resultStack.push(opnd1.div(opnd2));
+//						resultStack.push(opnd2.equals(KIntegerSet.ZERO) && !opnd1.isTop() ? KIntegerSet.ZERO : opnd1.div(opnd2));
+						try {
+							resultStack.push(opnd1.div(opnd2));
+						} catch (ArithmeticException e) {
+							resultStack.push(KIntegerSet.ZERO);
+						}
 						result.add(resultStack);
 					}
 

diff --git a/src/main/java/it/unipr/analysis/KIntegerSet.java b/src/main/java/it/unipr/analysis/KIntegerSet.java
@@ -5,6 +5,7 @@
 import java.math.BigInteger;
 import java.util.Collections;
 import java.util.HashSet;
+import java.util.Iterator;
 import java.util.Set;
 
 public class KIntegerSet extends SetLattice<KIntegerSet, Number> {
@@ -27,7 +28,7 @@ public KIntegerSet(Number i) {
 	}
 
 	public KIntegerSet(Integer i) {
-		this(new Integer[] { i });
+		this(new Number(i.intValue()));
 	}
 
 	public KIntegerSet(Integer... ints) {
@@ -101,14 +102,29 @@ public int hashCode() {
 		return super.hashCode();
 	}
 
+	// TODO check
 	@Override
 	public boolean equals(Object obj) {
 		if (this == obj)
 			return true;
-		if (!super.equals(obj))
+		if (obj == null)
 			return false;
 		if (getClass() != obj.getClass())
 			return false;
+
+		KIntegerSet other = (KIntegerSet) obj;
+
+		if(this.elements.size() != other.elements.size())
+			return false;
+
+		Iterator<Number> it = this.elements.iterator();
+		Iterator<Number> ot = other.elements.iterator();
+
+		while(it.hasNext() && ot.hasNext()) {
+			if(!it.next().equals(ot.next()))
+				return false;
+		}
+
 		return true;
 	}
 

diff --git a/src/main/java/it/unipr/analysis/Number.java b/src/main/java/it/unipr/analysis/Number.java
@@ -103,9 +103,12 @@ public Number multiply(Number other) {
 	public Number divide(Number other) {
 		if(this.getType() == other.getType() && other.getType() == Type.INT)
 			return new Number(i / other.getInt());
-		if(this.getType() == other.getType() && other.getType() == Type.LONG)
+		if(this.getType() == other.getType() && other.getType() == Type.LONG) {
+//			System.err.println("this: " + getInt() + " " + getLong() + " " + getBigInteger());
+//			System.err.println("other: " + other.getInt() + " " + other.getLong() + " " + other.getBigInteger());
 			return new Number(l / other.getLong());
-
+		}
+
 		BigInteger me = toBigInteger(this);
 		BigInteger ot = toBigInteger(other);
 
@@ -179,13 +182,13 @@ public String toString() {
 	public int compareTo(Number other) {
 		if(this.getType() == other.getType() && other.getType() == Type.INT)
 			return i > other.getInt() ? (+1) : i < other.getInt() ? (-1) : 0;
-			if(this.getType() == other.getType() && other.getType() == Type.LONG)
-				return i > other.getLong() ? (+1) : i < other.getLong() ? (-1) : 0;
+		if(this.getType() == other.getType() && other.getType() == Type.LONG)
+			return i > other.getLong() ? (+1) : i < other.getLong() ? (-1) : 0;
 
-				BigInteger me = toBigInteger(this);
-				BigInteger ot = toBigInteger(other);
+			BigInteger me = toBigInteger(this);
+			BigInteger ot = toBigInteger(other);
 
-				return me.compareTo(ot);
+			return me.compareTo(ot);
 	}
 
 	@Override