Merge pull request #158 from UniVE-SSV/native-calls-removal

Native calls removal

Author: VincenzoArceri

lisa/build.gradle

@@ -58,18 +58,13 @@ buildscript {
         classpath 'org.ajoberstar.grgit:grgit-core:4.0.2'
         classpath 'org.ajoberstar.grgit:grgit-gradle:4.0.2'
 
-        classpath 'com.github.roroche:plantuml-gradle-plugin:1.0.2'
-        classpath 'gradle.plugin.org.fmiw:plantuml-gradle-plugin:0.1'
-        
         classpath 'com.diffplug.spotless:spotless-plugin-gradle:5.15.0'
     }
 }
 
 subprojects {
     apply plugin: 'java-library'
     apply plugin: 'eclipse'
-    apply plugin: 'com.github.roroche.plantuml' // generation of plantuml from source code (visualization: https://www.planttext.com/)
-    apply plugin: 'org.fmiw.plantuml' // plantuml to png
     apply plugin: 'org.ajoberstar.grgit' // parse git information during the build
     apply plugin: 'com.diffplug.spotless' // code formatting task
     apply plugin: 'checkstyle' // javadoc checking - coding conventions
@@ -78,7 +73,6 @@ subprojects {
     apply plugin: 'jacoco' // coverage reports
 
     apply from: "${project.rootDir}/code-style.gradle"
-    apply from: "${project.rootDir}/doc-extra.gradle"
     apply from: "${project.rootDir}/java.gradle"
     apply from: "${project.rootDir}/publishing.gradle"
 }

lisa/doc-extra.gradle

@@ -103,7 +103,7 @@ public Collection<CFGWithAnalysisResults<A, H, V>> getAnalysisResultsOf(CFG cfg)
 	@Override
 	public AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisState<A, H, V> entryState,
 			ExpressionSet<SymbolicExpression>[] parameters) throws SemanticException {
-		OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getQualifiedName(),
+		OpenCall open = new OpenCall(call.getCFG(), call.getLocation(), call.getTargetName(),
 				call.getStaticType(), call.getParameters());
 		return getAbstractResultOf(open, entryState, parameters);
 	}

lisa/lisa-core/src/main/java/it/unive/lisa/interprocedural/ModularWorstCaseAnalysis.java

@@ -45,6 +45,7 @@
 import it.unive.lisa.program.cfg.controlFlow.ControlFlowStructure;
 import it.unive.lisa.program.cfg.edge.Edge;
 import it.unive.lisa.program.cfg.statement.Expression;
+import it.unive.lisa.program.cfg.statement.NaryExpression;
 import it.unive.lisa.program.cfg.statement.PluggableStatement;
 import it.unive.lisa.program.cfg.statement.Ret;
 import it.unive.lisa.program.cfg.statement.Statement;
@@ -272,6 +273,8 @@ public void testStatements() {
 					extra.add("originating");
 				if (Call.class.isAssignableFrom(st))
 					extra.add("source");
+				if (NaryExpression.class.isAssignableFrom(st))
+					extra.add("order");
 				verify(st,
 						verifier -> verifier
 								.withIgnoredFields(ListUtils.union(expressionFields, extra).toArray(String[]::new)),

lisa/lisa-core/src/test/java/it/unive/lisa/EqualityContractVerificationTest.java

@@ -11,7 +11,6 @@
 import it.unive.lisa.program.SourceCodeLocation;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Expression;
-import it.unive.lisa.program.cfg.statement.call.BinaryNativeCall;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.value.BinaryExpression;
 import it.unive.lisa.symbolic.value.operator.binary.BinaryOperator;
@@ -35,7 +34,7 @@
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  */
-public class IMPAddOrConcat extends BinaryNativeCall {
+public class IMPAddOrConcat extends it.unive.lisa.program.cfg.statement.BinaryExpression {
 
 	/**
 	 * Builds the addition.
@@ -55,14 +54,12 @@ public IMPAddOrConcat(CFG cfg, String sourceFile, int line, int col, Expression
 	protected <A extends AbstractState<A, H, V>,
 			H extends HeapDomain<H>,
 			V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
-					AnalysisState<A, H, V> entryState,
 					InterproceduralAnalysis<A, H, V> interprocedural,
-					AnalysisState<A, H, V> leftState,
+					AnalysisState<A, H, V> state,
 					SymbolicExpression left,
-					AnalysisState<A, H, V> rightState,
 					SymbolicExpression right)
 					throws SemanticException {
-		AnalysisState<A, H, V> result = entryState.bottom();
+		AnalysisState<A, H, V> result = state.bottom();
 		BinaryOperator op;
 
 		for (Type tleft : left.getTypes())
@@ -92,7 +89,7 @@ else if (tright.isNumericType() || tright.isUntyped())
 				if (op == null)
 					continue;
 
-				result = result.lub(rightState.smallStepSemantics(
+				result = result.lub(state.smallStepSemantics(
 						new BinaryExpression(
 								op == StringConcat.INSTANCE
 										? Caches.types().mkSingletonSet(StringType.INSTANCE)

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPAddOrConcat.java

@@ -8,8 +8,8 @@
 import it.unive.lisa.interprocedural.InterproceduralAnalysis;
 import it.unive.lisa.program.SourceCodeLocation;
 import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.statement.BinaryExpression;
 import it.unive.lisa.program.cfg.statement.Expression;
-import it.unive.lisa.program.cfg.statement.call.BinaryNativeCall;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.AccessChild;
 import it.unive.lisa.symbolic.heap.HeapDereference;
@@ -21,7 +21,7 @@
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  */
-public class IMPArrayAccess extends BinaryNativeCall {
+public class IMPArrayAccess extends BinaryExpression {
 
 	/**
 	 * Builds the array access.
@@ -42,20 +42,19 @@ public IMPArrayAccess(CFG cfg, String sourceFile, int line, int col, Expression
 	protected <A extends AbstractState<A, H, V>,
 			H extends HeapDomain<H>,
 			V extends ValueDomain<V>> AnalysisState<A, H, V> binarySemantics(
-					AnalysisState<A, H, V> entryState, InterproceduralAnalysis<A, H, V> interprocedural,
-					AnalysisState<A, H, V> leftState,
+					InterproceduralAnalysis<A, H, V> interprocedural,
+					AnalysisState<A, H, V> state,
 					SymbolicExpression left,
-					AnalysisState<A, H, V> rightState,
 					SymbolicExpression right)
-
 					throws SemanticException {
+
 		if (!left.getDynamicType().isArrayType() && !left.getDynamicType().isUntyped())
-			return entryState.bottom();
+			return state.bottom();
 		// it is not possible to detect the correct type of the field without
 		// resolving it. we rely on the rewriting that will happen inside heap
 		// domain to translate this into a variable that will have its correct
 		// type
 		HeapDereference deref = new HeapDereference(getRuntimeTypes(), left, getLocation());
-		return rightState.smallStepSemantics(new AccessChild(getRuntimeTypes(), deref, right, getLocation()), this);
+		return state.smallStepSemantics(new AccessChild(getRuntimeTypes(), deref, right, getLocation()), this);
 	}
 }

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPArrayAccess.java

@@ -11,7 +11,7 @@
 import it.unive.lisa.program.SourceCodeLocation;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Expression;
-import it.unive.lisa.program.cfg.statement.call.NativeCall;
+import it.unive.lisa.program.cfg.statement.NaryExpression;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.HeapAllocation;
 import it.unive.lisa.symbolic.heap.HeapReference;
@@ -25,7 +25,7 @@
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  */
-public class IMPNewArray extends NativeCall {
+public class IMPNewArray extends NaryExpression {
 
 	/**
 	 * Builds the array allocation.
@@ -39,31 +39,24 @@ public class IMPNewArray extends NativeCall {
 	 */
 	public IMPNewArray(CFG cfg, String sourceFile, int line, int col, Type type, Expression[] dimensions) {
 		super(cfg, new SourceCodeLocation(sourceFile, line, col), "new " + type + "[]",
-				ArrayType.lookup(type, dimensions.length),
-				dimensions);
+				ArrayType.lookup(type, dimensions.length), dimensions);
 	}
 
 	@Override
 	public <A extends AbstractState<A, H, V>,
 			H extends HeapDomain<H>,
-			V extends ValueDomain<V>> AnalysisState<A, H, V> callSemantics(
-					AnalysisState<A, H, V> entryState, InterproceduralAnalysis<A, H, V> interprocedural,
-					AnalysisState<A, H, V>[] computedStates,
+			V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
+					InterproceduralAnalysis<A, H, V> interprocedural,
+					AnalysisState<A, H, V> state,
 					ExpressionSet<SymbolicExpression>[] params)
 					throws SemanticException {
-		// it corresponds to the analysis state after the evaluation of all the
-		// parameters of this call
-		// (the semantics of this call does not need information about the
-		// intermediate analysis states)
-		AnalysisState<A, H,
-				V> lastPostState = computedStates.length == 0 ? entryState : computedStates[computedStates.length - 1];
-		AnalysisState<A, H,
-				V> sem = lastPostState.smallStepSemantics(new HeapAllocation(getRuntimeTypes(), getLocation()), this);
+		HeapAllocation alloc = new HeapAllocation(getRuntimeTypes(), getLocation());
+		AnalysisState<A, H, V> sem = state.smallStepSemantics(alloc, this);
 
-		AnalysisState<A, H, V> result = entryState.bottom();
+		AnalysisState<A, H, V> result = state.bottom();
 		for (SymbolicExpression loc : sem.getComputedExpressions()) {
-			AnalysisState<A, H,
-					V> refSem = sem.smallStepSemantics(new HeapReference(loc.getTypes(), loc, getLocation()), this);
+			HeapReference ref = new HeapReference(loc.getTypes(), loc, getLocation());
+			AnalysisState<A, H, V> refSem = sem.smallStepSemantics(ref, this);
 			result = result.lub(refSem);
 		}
 

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewArray.java

@@ -11,8 +11,8 @@
 import it.unive.lisa.program.SourceCodeLocation;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Expression;
+import it.unive.lisa.program.cfg.statement.NaryExpression;
 import it.unive.lisa.program.cfg.statement.VariableRef;
-import it.unive.lisa.program.cfg.statement.call.NativeCall;
 import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
 import it.unive.lisa.symbolic.SymbolicExpression;
 import it.unive.lisa.symbolic.heap.HeapAllocation;
@@ -32,7 +32,7 @@
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  */
-public class IMPNewObj extends NativeCall {
+public class IMPNewObj extends NaryExpression {
 
 	/**
 	 * Builds the object allocation and initialization.
@@ -51,30 +51,29 @@ public IMPNewObj(CFG cfg, String sourceFile, int line, int col, Type type, Expre
 	@Override
 	public <A extends AbstractState<A, H, V>,
 			H extends HeapDomain<H>,
-			V extends ValueDomain<V>> AnalysisState<A, H, V> callSemantics(
-					AnalysisState<A, H, V> entryState, InterproceduralAnalysis<A, H, V> interprocedural,
-					AnalysisState<A, H, V>[] computedStates,
+			V extends ValueDomain<V>> AnalysisState<A, H, V> expressionSemantics(
+					InterproceduralAnalysis<A, H, V> interprocedural,
+					AnalysisState<A, H, V> state,
 					ExpressionSet<SymbolicExpression>[] params)
 					throws SemanticException {
 		HeapAllocation created = new HeapAllocation(getRuntimeTypes(), getLocation());
 
 		// we need to add the receiver to the parameters
-		VariableRef paramThis = new VariableRef(getCFG(), getLocation(), "this",
-				getStaticType());
-		Expression[] fullExpressions = ArrayUtils.insert(0, getParameters(), paramThis);
+		VariableRef paramThis = new VariableRef(getCFG(), getLocation(), "this", getStaticType());
+		Expression[] fullExpressions = ArrayUtils.insert(0, getSubExpressions(), paramThis);
 		ExpressionSet<SymbolicExpression>[] fullParams = ArrayUtils.insert(0, params, new ExpressionSet<>(created));
 
 		UnresolvedCall call = new UnresolvedCall(getCFG(), getLocation(),
 				IMPFrontend.CALL_STRATEGY, true, getStaticType().toString(), fullExpressions);
-		call.inheritRuntimeTypesFrom(this);
-		AnalysisState<A, H, V> sem = call.callSemantics(entryState, interprocedural, computedStates, fullParams);
+		call.setRuntimeTypes(getRuntimeTypes());
+		AnalysisState<A, H, V> sem = call.expressionSemantics(interprocedural, state, fullParams);
 
 		if (!call.getMetaVariables().isEmpty())
 			sem = sem.forgetIdentifiers(call.getMetaVariables());
 
 		sem = sem.smallStepSemantics(created, this);
 
-		AnalysisState<A, H, V> result = entryState.bottom();
+		AnalysisState<A, H, V> result = state.bottom();
 		for (SymbolicExpression loc : sem.getComputedExpressions())
 			result = result.lub(sem.smallStepSemantics(new HeapReference(loc.getTypes(), loc, getLocation()), call));
 

lisa/lisa-imp/src/main/java/it/unive/lisa/imp/expressions/IMPNewObj.java

@@ -1,6 +1,7 @@
 package it.unive.lisa.checks.warnings;
 
 import it.unive.lisa.program.cfg.CodeLocation;
+import java.util.Objects;
 
 /**
  * A warning reported by LiSA on the program under analysis. This warning is
@@ -17,12 +18,12 @@ public abstract class WarningWithLocation extends Warning {
 	/**
 	 * Builds the warning.
 	 * 
-	 * @param location the location in the source file where this warning is
-	 *                     located. If unknown, use {@code, null}
+	 * @param location the location in the program where this warning is located
 	 * @param message  the message of this warning
 	 */
 	protected WarningWithLocation(CodeLocation location, String message) {
 		super(message);
+		Objects.requireNonNull(location, "The location of a warning with location cannot be null");
 		this.location = location;
 	}
 

lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/warnings/WarningWithLocation.java

@@ -12,9 +12,9 @@
 public interface CodeElement {
 
 	/**
-	 * Yields the location where this code element appears in the source file.
+	 * Yields the location where this code element appears in the program.
 	 * 
-	 * @return the location where this code element apperars in the source file
+	 * @return the location where this code element apperars in the program
 	 */
 	CodeLocation getLocation();
 }