Merge pull request #314 from lisa-analyzer/release-roundup

Release roundup

lisa/gradle.properties

@@ -1,6 +1,6 @@
 # project properties
 group = 'it.unive'
-version = 0.1b9
+version = 0.1
 
 # gradle build properties
 org.gradle.caching=true

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/TypeBasedHeap.java

@@ -259,7 +259,8 @@ public ExpressionSet visit(
 			ProgramPoint pp = (ProgramPoint) params[0];
 			SemanticOracle oracle = (SemanticOracle) params[1];
 
-			for (SymbolicExpression rec : receiver)
+			for (SymbolicExpression rec : receiver) {
+				rec = removeTypingExpressions(rec);
 				if (rec instanceof MemoryPointer) {
 					MemoryPointer pid = (MemoryPointer) rec;
 					for (Type t : oracle.getRuntimeTypesOf(pid, pp, oracle))
@@ -270,6 +271,7 @@ public ExpressionSet visit(
 							result.add(e);
 						}
 				}
+			}
 			return new ExpressionSet(result);
 		}
 
@@ -298,7 +300,8 @@ public ExpressionSet visit(
 			ProgramPoint pp = (ProgramPoint) params[0];
 			SemanticOracle oracle = (SemanticOracle) params[1];
 
-			for (SymbolicExpression refExp : ref)
+			for (SymbolicExpression refExp : ref) {
+				refExp = removeTypingExpressions(refExp);
 				if (refExp instanceof HeapLocation) {
 					Set<Type> rt = oracle.getRuntimeTypesOf(refExp, pp, oracle);
 					Type sup = Type.commonSupertype(rt, Untyped.INSTANCE);
@@ -308,6 +311,7 @@ public ExpressionSet visit(
 							refExp.getCodeLocation());
 					result.add(e);
 				}
+			}
 
 			return new ExpressionSet(result);
 		}
@@ -323,6 +327,7 @@ public ExpressionSet visit(
 			SemanticOracle oracle = (SemanticOracle) params[1];
 
 			for (SymbolicExpression derefExp : deref) {
+				derefExp = removeTypingExpressions(derefExp);
 				if (derefExp instanceof Variable) {
 					Variable var = (Variable) derefExp;
 					for (Type t : oracle.getRuntimeTypesOf(var, pp, oracle))

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSite.java

@@ -179,4 +179,14 @@ public String getField() {
 	 */
 	public abstract AllocationSite withField(
 			SymbolicExpression field);
+
+	/**
+	 * Yields a modified version of this allocation site with the given type.
+	 * 
+	 * @param type the new type
+	 * 
+	 * @return the modified allocation site
+	 */
+	public abstract AllocationSite withType(
+			Type type);
 }

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/AllocationSiteBasedAnalysis.java

@@ -320,7 +320,8 @@ public ExpressionSet visit(
 				Object... params)
 				throws SemanticException {
 			Set<SymbolicExpression> result = new HashSet<>();
-			for (SymbolicExpression rec : receiver)
+			for (SymbolicExpression rec : receiver) {
+				rec = removeTypingExpressions(rec);
 				if (rec instanceof MemoryPointer) {
 					MemoryPointer pid = (MemoryPointer) rec;
 					AllocationSite site = (AllocationSite) pid.getReferencedLocation();
@@ -347,7 +348,8 @@ public ExpressionSet visit(
 
 					result.add(e);
 				} else if (rec instanceof AllocationSite)
-					result.add(rec);
+					result.add(((AllocationSite) rec).withType(expression.getStaticType()));
+			}
 
 			return new ExpressionSet(result);
 		}
@@ -387,7 +389,8 @@ public ExpressionSet visit(
 				throws SemanticException {
 			Set<SymbolicExpression> result = new HashSet<>();
 
-			for (SymbolicExpression loc : arg)
+			for (SymbolicExpression loc : arg) {
+				loc = removeTypingExpressions(loc);
 				if (loc instanceof AllocationSite) {
 					AllocationSite allocSite = (AllocationSite) loc;
 					MemoryPointer e = new MemoryPointer(
@@ -403,6 +406,7 @@ public ExpressionSet visit(
 					result.add(e);
 				} else
 					result.add(loc);
+			}
 			return new ExpressionSet(result);
 		}
 
@@ -414,7 +418,8 @@ public ExpressionSet visit(
 				throws SemanticException {
 			Set<SymbolicExpression> result = new HashSet<>();
 
-			for (SymbolicExpression ref : arg)
+			for (SymbolicExpression ref : arg) {
+				ref = removeTypingExpressions(ref);
 				if (ref instanceof MemoryPointer)
 					result.add(((MemoryPointer) ref).getReferencedLocation());
 				else if (ref instanceof Identifier) {
@@ -444,6 +449,7 @@ else if (id.getStaticType().isInMemoryType() || id.getStaticType().isUntyped())
 					}
 				} else
 					result.add(ref);
+			}
 
 			return new ExpressionSet(result);
 		}

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/FieldSensitivePointBasedHeap.java

@@ -288,14 +288,16 @@ public ExpressionSet visit(
 				throws SemanticException {
 			Set<SymbolicExpression> result = new HashSet<>();
 
-			for (SymbolicExpression rec : receiver)
+			for (SymbolicExpression rec : receiver) {
+				rec = removeTypingExpressions(rec);
 				if (rec instanceof MemoryPointer) {
 					AllocationSite site = (AllocationSite) ((MemoryPointer) rec).getReferencedLocation();
 					populate(expression, child, result, site);
 				} else if (rec instanceof AllocationSite) {
 					AllocationSite site = (AllocationSite) rec;
 					populate(expression, child, result, site);
 				}
+			}
 
 			return new ExpressionSet(result);
 		}

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/HeapAllocationSite.java

@@ -88,4 +88,10 @@ public AllocationSite withField(
 			throw new IllegalStateException("Cannot add a field to an allocation site that already has one");
 		return new HeapAllocationSite(getStaticType(), getLocationName(), field, isWeak(), getCodeLocation());
 	}
+
+	@Override
+	public AllocationSite withType(
+			Type type) {
+		return new HeapAllocationSite(type, getLocationName(), getField(), isWeak(), getCodeLocation());
+	}
 }

lisa/lisa-analyses/src/main/java/it/unive/lisa/analysis/heap/pointbased/StackAllocationSite.java

@@ -88,4 +88,10 @@ public AllocationSite withField(
 			throw new IllegalStateException("Cannot add a field to an allocation site that already has one");
 		return new StackAllocationSite(getStaticType(), getLocationName(), field, isWeak(), getCodeLocation());
 	}
+
+	@Override
+	public AllocationSite withType(
+			Type type) {
+		return new StackAllocationSite(type, getLocationName(), getField(), isWeak(), getCodeLocation());
+	}
 }

lisa/lisa-analyses/src/test/java/it/unive/lisa/TestParameterProvider.java

@@ -271,16 +271,22 @@ public static <R> R provideParam(
 			return (R) new ValueEnvironment<>(new SampleNRVD());
 		if (param == SampleNRVD.class || param == BaseNonRelationalValueDomain.class)
 			return (R) new SampleNRVD();
+		if (param == BaseNonRelationalValueDomain[].class)
+			return (R) new BaseNonRelationalValueDomain[0];
 
 		if (param == InferenceSystem.class)
 			return (R) new InferenceSystem<>(new SampleIV());
 		if (param == SampleIV.class || param == BaseInferredValue.class)
 			return (R) new SampleIV();
+		if (param == BaseInferredValue[].class)
+			return (R) new BaseInferredValue[0];
 
 		if (param == TypeEnvironment.class)
 			return (R) new TypeEnvironment<>(new SampleNRTD());
 		if (param == SampleNRTD.class || param == BaseNonRelationalTypeDomain.class)
 			return (R) new SampleNRTD();
+		if (param == BaseNonRelationalTypeDomain[].class)
+			return (R) new BaseNonRelationalTypeDomain[0];
 
 		if (param == SemanticOracle.class)
 			return (R) DefaultConfiguration.defaultAbstractState();

lisa/lisa-analyses/src/test/java/it/unive/lisa/analysis/heap/pointbased/PointBasedHeapTest.java

@@ -17,6 +17,7 @@
 import it.unive.lisa.program.cfg.CodeLocation;
 import it.unive.lisa.program.cfg.ProgramPoint;
 import it.unive.lisa.program.type.Int32Type;
+import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
 import it.unive.lisa.symbolic.heap.HeapDereference;
 import it.unive.lisa.symbolic.heap.HeapExpression;
@@ -29,7 +30,9 @@
 import it.unive.lisa.symbolic.value.OutOfScopeIdentifier;
 import it.unive.lisa.symbolic.value.Variable;
 import it.unive.lisa.symbolic.value.operator.binary.NumericNonOverflowingAdd;
+import it.unive.lisa.symbolic.value.operator.binary.TypeConv;
 import it.unive.lisa.type.Type;
+import it.unive.lisa.type.TypeTokenType;
 import it.unive.lisa.type.Untyped;
 import java.util.Collections;
 import java.util.HashSet;
@@ -459,4 +462,21 @@ public void testHeapDereferenceRewrite() throws SemanticException {
 		expectedRewritten = new ExpressionSet(expectedUnknownAlloc);
 		assertEquals(expectedRewritten, xAssign.rewrite(deref, pp1, fakeOracle));
 	}
+
+	@Test
+	public void testIssue300() throws SemanticException {
+		// ((type) x) rewritten in x -> pp1 -> pp1
+		PointBasedHeap xAssign = topHeap.assign(x,
+				new HeapReference(untyped,
+						new MemoryAllocation(untyped, loc1), loc1),
+				pp1, fakeOracle);
+		SymbolicExpression e = new AccessChild(intType,
+				new BinaryExpression(untyped,
+						new Constant(new TypeTokenType(Collections.singleton(intType)), intType, loc1), x,
+						TypeConv.INSTANCE,
+						loc1),
+				new Constant(intType, 1, loc1), loc1);
+		ExpressionSet expectedRewritten = new ExpressionSet(alloc1);
+		assertEquals(expectedRewritten, xAssign.rewrite(e, pp1, fakeOracle));
+	}
 }

lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/heap/BaseHeapDomain.java

@@ -18,6 +18,8 @@
 import it.unive.lisa.symbolic.value.TernaryExpression;
 import it.unive.lisa.symbolic.value.UnaryExpression;
 import it.unive.lisa.symbolic.value.ValueExpression;
+import it.unive.lisa.symbolic.value.operator.TypeOperator;
+import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
 import java.util.HashSet;
 import java.util.List;
 import java.util.Set;
@@ -148,6 +150,28 @@ public abstract H semanticsOf(
 	 */
 	public abstract static class Rewriter implements ExpressionVisitor<ExpressionSet> {
 
+		/**
+		 * Extracts the inner expressions from casts/conversions. If {@code e}
+		 * is of the form {@code (type) e1}, this method returns
+		 * {@code removeTypingExpressions(e1)}. Otherwise, {@code e} is returned
+		 * with no modifications.
+		 * 
+		 * @param e the expression to strip from type operators
+		 * 
+		 * @return the inner expression, if needed
+		 */
+		protected SymbolicExpression removeTypingExpressions(
+				SymbolicExpression e) {
+			if (e instanceof BinaryExpression) {
+				BinaryExpression be = (BinaryExpression) e;
+				BinaryOperator op = be.getOperator();
+				if (op instanceof TypeOperator)
+					return removeTypingExpressions(be.getRight());
+			}
+
+			return e;
+		}
+
 		@Override
 		public ExpressionSet visit(
 				UnaryExpression expression,
@@ -240,5 +264,25 @@ public ExpressionSet visit(
 				throws SemanticException {
 			return new ExpressionSet(expression);
 		}
+
+		@Override
+		public ExpressionSet visit(
+				HeapExpression expression,
+				ExpressionSet[] subExpressions,
+				Object... params)
+				throws SemanticException {
+			throw new SemanticException(
+					"No rewriting rule for heap expression of type " + expression.getClass().getName());
+		}
+
+		@Override
+		public ExpressionSet visit(
+				ValueExpression expression,
+				ExpressionSet[] subExpressions,
+				Object... params)
+				throws SemanticException {
+			throw new SemanticException(
+					"No rewriting rule for value expression of type " + expression.getClass().getName());
+		}
 	}
 }

lisa/lisa-sdk/src/main/java/it/unive/lisa/analysis/nonrelational/inference/BaseInferredValue.java

@@ -9,6 +9,7 @@
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
 import it.unive.lisa.symbolic.heap.HeapDereference;
+import it.unive.lisa.symbolic.heap.HeapExpression;
 import it.unive.lisa.symbolic.heap.HeapReference;
 import it.unive.lisa.symbolic.heap.MemoryAllocation;
 import it.unive.lisa.symbolic.value.BinaryExpression;
@@ -30,6 +31,7 @@
 import it.unive.lisa.symbolic.value.operator.unary.LogicalNegation;
 import it.unive.lisa.symbolic.value.operator.unary.UnaryOperator;
 import it.unive.lisa.type.Type;
+import java.lang.reflect.Array;
 import java.util.Set;
 
 /**
@@ -68,6 +70,15 @@ public EvaluationVisitor(
 			this.singleton = singleton;
 		}
 
+		@Override
+		public InferredPair<T> visit(
+				HeapExpression expression,
+				InferredPair<T>[] subExpressions,
+				Object... params)
+				throws SemanticException {
+			throw new SemanticException(CANNOT_PROCESS_ERROR);
+		}
+
 		@Override
 		public InferredPair<T> visit(
 				AccessChild expression,
@@ -213,6 +224,29 @@ public InferredPair<T> visit(
 					(SemanticOracle) params[2]);
 		}
 
+		@Override
+		public InferredPair<T> visit(
+				ValueExpression expression,
+				InferredPair<T>[] subExpressions,
+				Object... params)
+				throws SemanticException {
+			T[] subs = null;
+			if (subExpressions != null && subExpressions.length > 0) {
+				subs = (T[]) Array.newInstance(subExpressions[0].getInferred().getClass(), subExpressions.length);
+				for (int i = 0; i < subExpressions.length; i++) {
+					if (subExpressions[i].isBottom())
+						return subExpressions[i];
+					subs[i] = subExpressions[i].getInferred();
+				}
+			}
+
+			return singleton.evalValueExpression(expression,
+					subs,
+					((InferenceSystem<T>) params[0]).getExecutionState(),
+					(ProgramPoint) params[1],
+					(SemanticOracle) params[2]);
+		}
+
 	}
 
 	@Override
@@ -600,6 +634,41 @@ default InferredPair<T> evalTernaryExpression(
 		return new InferredPair<>(top, top, top);
 	}
 
+	/**
+	 * Yields the evaluation of a generic {@link ValueExpression}, where the
+	 * recursive evaluation of its sub-expressions, if any, has already happened
+	 * and is passed in the {@code subExpressions} parameters. It is guaranteed
+	 * that no element of {@code subExpressions} is {@link #bottom()}.<br>
+	 * <br>
+	 * This method allows evaluating frontend-defined expressions. For all
+	 * standard expressions defined within LiSA, the corresponding evaluation
+	 * method will be invoked instead.
+	 * 
+	 * @param expression     the expression to evaluate
+	 * @param subExpressions the instances of this domain representing the
+	 *                           abstract values of all its sub-expressions, if
+	 *                           any; if there are no sub-expressions, this
+	 *                           parameter can be {@code null} or empty
+	 * @param state          the current execution state
+	 * @param pp             the program point that where this operation is
+	 *                           being evaluated
+	 * @param oracle         the oracle for inter-domain communication
+	 * 
+	 * @return the evaluation of the expression
+	 * 
+	 * @throws SemanticException if an error occurs during the computation
+	 */
+	default InferredPair<T> evalValueExpression(
+			ValueExpression expression,
+			T[] subExpressions,
+			T state,
+			ProgramPoint pp,
+			SemanticOracle oracle)
+			throws SemanticException {
+		T top = top();
+		return new InferredPair<>(top, top, top);
+	}
+
 	/**
 	 * Yields the satisfiability of an abstract value of type {@code <T>}.
 	 *