Merge pull request #267 from lisa-analyzer/interval-methods

Add auxiliar interval methods

lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/numeric/IntervalTest.java

@@ -25,7 +25,10 @@
 import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingMul;
 import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingSub;
 import it.unive.lisa.symbolic.value.operator.unary.NumericNegation;
+import it.unive.lisa.util.numeric.InfiniteIterationException;
 import it.unive.lisa.util.numeric.IntInterval;
+import java.util.ArrayList;
+import java.util.List;
 import java.util.Random;
 import org.junit.Test;
 
@@ -648,4 +651,28 @@ public void testAssumeLE() throws SemanticException {
 			assertEquals("assume(" + variable + " <= " + bound + ") did not return " + exp, exp, act);
 		}
 	}
+
+	@Test(expected = InfiniteIterationException.class)
+	public void testIteratorOnTopInterval() {
+		Interval top = new Interval();
+
+		for (Long l : top.interval)
+			System.out.println(l);
+	}
+
+	@Test
+	public void testIterator() throws SemanticException {
+		Interval top = mk(-1, 2);
+		List<Long> values = new ArrayList<>();
+		for (Long l : top.interval)
+			values.add(l);
+
+		List<Long> expected = new ArrayList<>();
+		expected.add((long) -1);
+		expected.add((long) 0);
+		expected.add((long) 1);
+		expected.add((long) 2);
+		assertEquals(values, expected);
+
+	}
 }

lisa/lisa-sdk/src/main/java/it/unive/lisa/util/numeric/InfiniteIterationException.java

@@ -0,0 +1,19 @@
+package it.unive.lisa.util.numeric;
+
+/**
+ * An exception throw when someone tries to iterate over a non-finite
+ * {@link IntInterval}.
+ * 
+ * @author <a href="mailto:vincenzo.arceri@unipr.it">Vincenzo Arceri</a>
+ */
+public class InfiniteIterationException extends RuntimeException {
+
+	/**
+	 * Builds the exception.
+	 * 
+	 * @param i the non-finite interval on which some iterates
+	 */
+	public InfiniteIterationException(IntInterval i) {
+		super("Cannot iterate over the interval " + i);
+	}
+}

lisa/lisa-sdk/src/main/java/it/unive/lisa/util/numeric/IntInterval.java

@@ -1,11 +1,13 @@
 package it.unive.lisa.util.numeric;
 
+import java.util.Iterator;
+
 /**
  * An interval with integer bounds.
  * 
  * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
  */
-public class IntInterval {
+public class IntInterval implements Iterable<Long> {
 
 	/**
 	 * The interval {@code [-Inf, +Inf]}.
@@ -355,4 +357,15 @@ public boolean equals(Object obj) {
 	public String toString() {
 		return "[" + low + ", " + high + "]";
 	}
+
+	@Override
+	public Iterator<Long> iterator() {
+		if (!low.isFinite() || !high.isFinite() || low.isNaN() || high.isNaN())
+			throw new InfiniteIterationException(this);
+		try {
+			return new IntIntervalIterator(low.toLong(), high.toLong());
+		} catch (MathNumberConversionException e) {
+			throw new InfiniteIterationException(this);
+		}
+	}
 }

lisa/lisa-sdk/src/main/java/it/unive/lisa/util/numeric/IntIntervalIterator.java

@@ -0,0 +1,35 @@
+package it.unive.lisa.util.numeric;
+
+import java.util.Iterator;
+
+/**
+ * The {@link IntInterval} iterator.
+ * 
+ * @author <a href="mailto:vincenzo.arceri@unipr.it">Vincenzo Arceri</a>
+ */
+public class IntIntervalIterator implements Iterator<Long> {
+
+	private long init;
+	private final long end;
+
+	/**
+	 * Builds the iterator.
+	 * 
+	 * @param init low bound
+	 * @param end  high bound
+	 */
+	public IntIntervalIterator(long init, long end) {
+		this.init = init;
+		this.end = end;
+	}
+
+	@Override
+	public boolean hasNext() {
+		return init <= end;
+	}
+
+	@Override
+	public Long next() {
+		return init++;
+	}
+}

lisa/lisa-sdk/src/main/java/it/unive/lisa/util/numeric/MathNumber.java

@@ -396,6 +396,90 @@ public MathNumber roundDown() {
 		return cached(new MathNumber(number.setScale(0, RoundingMode.FLOOR)));
 	}
 
+	/**
+	 * Yields the integer value of this math number.
+	 * 
+	 * @return the integer value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public int toInt() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.intValue();
+	}
+
+	/**
+	 * Yields the double value of this math number.
+	 * 
+	 * @return the double value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public double toDouble() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.doubleValue();
+	}
+
+	/**
+	 * Yields the byte value of this math number.
+	 * 
+	 * @return the byte value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public byte toByte() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.byteValue();
+	}
+
+	/**
+	 * Yields the short value of this math number.
+	 * 
+	 * @return the short value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public short toShort() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.shortValue();
+	}
+
+	/**
+	 * Yields the float value of this math number.
+	 * 
+	 * @return the float value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public float toFloat() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.floatValue();
+	}
+
+	/**
+	 * Yields the long value of this math number.
+	 * 
+	 * @return the long value of this math number
+	 * 
+	 * @throws MathNumberConversionException when this math number is NaN or
+	 *                                           infinite
+	 */
+	public long toLong() throws MathNumberConversionException {
+		if (isNaN() || isInfinite())
+			throw new MathNumberConversionException(this);
+		return number.longValue();
+	}
+
 	@Override
 	public int hashCode() {
 		final int prime = 31;

lisa/lisa-sdk/src/main/java/it/unive/lisa/util/numeric/MathNumberConversionException.java

@@ -0,0 +1,19 @@
+package it.unive.lisa.util.numeric;
+
+/**
+ * An exception thrown when a {@link MathNumber} fails to be converted to a
+ * specific Java numerical type.
+ * 
+ * @author <a href="mailto:vincenzo.arceri@unipr.it">Vincenzo Arceri</a>
+ */
+public class MathNumberConversionException extends Exception {
+
+	/**
+	 * Builds the exception.
+	 * 
+	 * @param m the math number that fails to be converted
+	 */
+	public MathNumberConversionException(MathNumber m) {
+		super("Cannot convert " + m + " to numerical value");
+	}
+}