Merge pull request #132 from UniVE-SSV/type-inference-config

Configurability of the `AbstractState` used for type inference

Author: VincenzoArceri

lisa/lisa-core/src/main/java/it/unive/lisa/LiSA.java

@@ -2,17 +2,24 @@
 
 import static it.unive.lisa.LiSAFactory.getDefaultFor;
 
+import it.unive.lisa.analysis.AbstractState;
+import it.unive.lisa.analysis.heap.HeapDomain;
+import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
+import it.unive.lisa.analysis.types.InferredTypes;
 import it.unive.lisa.checks.warnings.Warning;
 import it.unive.lisa.interprocedural.InterproceduralAnalysis;
 import it.unive.lisa.interprocedural.callgraph.CallGraph;
 import it.unive.lisa.logging.TimerLogger;
 import it.unive.lisa.outputs.JsonReport;
 import it.unive.lisa.program.Program;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.util.collections.externalSet.ExternalSet;
 import it.unive.lisa.util.file.FileManager;
 import java.io.IOException;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
+import java.util.function.Function;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
@@ -90,7 +97,19 @@ public void run(Program program) throws AnalysisException {
 			throw new AnalysisExecutionException("Unable to create default interprocedural analysis", e);
 		}
 
-		LiSARunner runner = new LiSARunner(conf, interproc, callGraph, conf.getState());
+		AbstractState inferenceState = conf.getTypeInferenceState();
+		Function<AbstractState<?, ?, ?>, ExternalSet<Type>> typeExtractor = conf.getTypeExtractor();
+		if (conf.isInferTypes() && inferenceState == null) {
+			// these are used only if type inference is requested
+			// we can skip configuration otherwise
+			inferenceState = getDefaultFor(AbstractState.class, getDefaultFor(HeapDomain.class),
+					new InferenceSystem<>(new InferredTypes()));
+			typeExtractor = s -> ((InferenceSystem<InferredTypes>) s.getValueState()).getInferredValue()
+					.getRuntimeTypes();
+		}
+
+		LiSARunner runner = new LiSARunner(conf, interproc, callGraph, conf.getAbstractState(),
+				inferenceState, typeExtractor);
 
 		try {
 			warnings.addAll(TimerLogger.execSupplier(LOG, "Analysis time", () -> runner.run(program, fileManager)));

lisa/lisa-core/src/main/java/it/unive/lisa/LiSAConfiguration.java

@@ -9,12 +9,17 @@
 import it.unive.lisa.interprocedural.callgraph.CallGraph;
 import it.unive.lisa.program.cfg.CFG;
 import it.unive.lisa.program.cfg.statement.Statement;
+import it.unive.lisa.symbolic.SymbolicExpression;
+import it.unive.lisa.type.Type;
+import it.unive.lisa.util.collections.externalSet.ExternalSet;
 import it.unive.lisa.util.collections.workset.FIFOWorkingSet;
 import it.unive.lisa.util.collections.workset.WorkingSet;
 import java.nio.file.Paths;
 import java.util.Collection;
 import java.util.Collections;
+import java.util.Objects;
 import java.util.concurrent.ConcurrentHashMap;
+import java.util.function.Function;
 
 /**
  * A holder for the configuration of a {@link LiSA} analysis.
@@ -50,10 +55,23 @@ public class LiSAConfiguration {
 	 */
 	private InterproceduralAnalysis<?, ?, ?> interproceduralAnalysis;
 
+	/**
+	 * The abstract state to run during the type inference
+	 */
+	private AbstractState<?, ?, ?> typeInferenceState;
+
+	/**
+	 * The function that, given a state computed during type inference, yield
+	 * the set of types computed for the processed {@link SymbolicExpression}.
+	 * This value will be considered as the set of runtime types for the
+	 * {@link Statement} that generated such expression.
+	 */
+	private Function<AbstractState<?, ?, ?>, ExternalSet<Type>> typeExtractor;
+
 	/**
 	 * The abstract state to run during the analysis
 	 */
-	private AbstractState<?, ?, ?> state;
+	private AbstractState<?, ?, ?> abstractState;
 
 	/**
 	 * Whether or not type inference should be executed before the analysis
@@ -205,6 +223,31 @@ public LiSAConfiguration setInterproceduralAnalysis(InterproceduralAnalysis<?, ?
 		return this;
 	}
 
+	/**
+	 * Sets the {@link AbstractState} to use for the type inference. Any
+	 * existing value is overwritten.
+	 * 
+	 * @param state         the abstract state to use
+	 * @param typeExtractor the function that, given a state computed during
+	 *                          type inference, yield the set of types computed
+	 *                          for the processed {@link SymbolicExpression}.
+	 *                          This value will be considered as the set of
+	 *                          runtime types for the {@link Statement} that
+	 *                          generated such expression.
+	 * 
+	 * @return the current (modified) configuration
+	 */
+	public LiSAConfiguration setTypeInferenceState(AbstractState<?, ?, ?> state,
+			Function<AbstractState<?, ?, ?>, ExternalSet<Type>> typeExtractor) {
+		this.typeInferenceState = state;
+		this.typeExtractor = typeExtractor;
+
+		if (state != null)
+			Objects.requireNonNull(typeExtractor, "A type extractor is needed for a custom type inference state");
+
+		return this;
+	}
+
 	/**
 	 * Sets the {@link AbstractState} to use for the analysis. Any existing
 	 * value is overwritten.
@@ -214,7 +257,7 @@ public LiSAConfiguration setInterproceduralAnalysis(InterproceduralAnalysis<?, ?
 	 * @return the current (modified) configuration
 	 */
 	public LiSAConfiguration setAbstractState(AbstractState<?, ?, ?> state) {
-		this.state = state;
+		this.abstractState = state;
 		return this;
 	}
 
@@ -377,14 +420,37 @@ public CallGraph getCallGraph() {
 		return interproceduralAnalysis;
 	}
 
+	/**
+	 * Yields the {@link AbstractState} for the type inference. Might be
+	 * {@code null} if none was set. If this is not {@code null}, then
+	 * {@link #getTypeExtractor()} is not {@code null} either.
+	 * 
+	 * @return the abstract state for the type inference
+	 */
+	public AbstractState<?, ?, ?> getTypeInferenceState() {
+		return typeInferenceState;
+	}
+
+	/**
+	 * Yields the function that, given a state computed during type inference,
+	 * yield the set of types computed for the processed
+	 * {@link SymbolicExpression}. This value will be considered as the set of
+	 * runtime types for the {@link Statement} that generated such expression.
+	 * 
+	 * @return the function that is used to extract types
+	 */
+	public Function<AbstractState<?, ?, ?>, ExternalSet<Type>> getTypeExtractor() {
+		return typeExtractor;
+	}
+
 	/**
 	 * Yields the {@link AbstractState} for the analysis. Might be {@code null}
 	 * if none was set.
 	 * 
 	 * @return the abstract state for the analysis
 	 */
-	public AbstractState<?, ?, ?> getState() {
-		return state;
+	public AbstractState<?, ?, ?> getAbstractState() {
+		return abstractState;
 	}
 
 	/**
@@ -500,7 +566,9 @@ public int hashCode() {
 		result = prime * result + ((interproceduralAnalysis == null) ? 0 : interproceduralAnalysis.hashCode());
 		result = prime * result + (jsonOutput ? 1231 : 1237);
 		result = prime * result + ((semanticChecks == null) ? 0 : semanticChecks.hashCode());
-		result = prime * result + ((state == null) ? 0 : state.hashCode());
+		result = prime * result + ((typeInferenceState == null) ? 0 : typeInferenceState.hashCode());
+		result = prime * result + ((typeExtractor == null) ? 0 : typeExtractor.hashCode());
+		result = prime * result + ((abstractState == null) ? 0 : abstractState.hashCode());
 		result = prime * result + ((syntacticChecks == null) ? 0 : syntacticChecks.hashCode());
 		result = prime * result + wideningThreshold;
 		result = prime * result + ((workdir == null) ? 0 : workdir.hashCode());
@@ -546,10 +614,20 @@ public boolean equals(Object obj) {
 				return false;
 		} else if (!semanticChecks.equals(other.semanticChecks))
 			return false;
-		if (state == null) {
-			if (other.state != null)
+		if (typeInferenceState == null) {
+			if (other.typeInferenceState != null)
+				return false;
+		} else if (!typeInferenceState.equals(other.typeInferenceState))
+			return false;
+		if (typeExtractor == null) {
+			if (other.typeExtractor != null)
+				return false;
+		} else if (!typeExtractor.equals(other.typeExtractor))
+			return false;
+		if (abstractState == null) {
+			if (other.abstractState != null)
 				return false;
-		} else if (!state.equals(other.state))
+		} else if (!abstractState.equals(other.abstractState))
 			return false;
 		if (syntacticChecks == null) {
 			if (other.syntacticChecks != null)

lisa/lisa-core/src/main/java/it/unive/lisa/LiSARunner.java

@@ -6,10 +6,7 @@
 import it.unive.lisa.analysis.AnalysisState;
 import it.unive.lisa.analysis.CFGWithAnalysisResults;
 import it.unive.lisa.analysis.SemanticException;
-import it.unive.lisa.analysis.SimpleAbstractState;
 import it.unive.lisa.analysis.heap.HeapDomain;
-import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
-import it.unive.lisa.analysis.types.InferredTypes;
 import it.unive.lisa.analysis.value.ValueDomain;
 import it.unive.lisa.caches.Caches;
 import it.unive.lisa.checks.ChecksExecutor;
@@ -48,16 +45,25 @@
  * 
  * @author <a href="mailto:[email protected]">Luca Negrini</a>
  * 
- * @param <A> the type of {@link AbstractState} contained into the analysis
- *                state that will be used in the fixpoints
- * @param <H> the type of {@link HeapDomain} contained into the computed
- *                abstract state that will be used in the fixpoints
- * @param <V> the type of {@link ValueDomain} contained into the computed
- *                abstract state that will be used in the fixpoints
+ * @param <A>  the type of {@link AbstractState} contained into the analysis
+ *                 state that will be used in the analysis fixpoint
+ * @param <H>  the type of {@link HeapDomain} contained into the abstract state
+ *                 that will be used in the analysis fixpoint
+ * @param <V>  the type of {@link ValueDomain} contained into the abstract state
+ *                 that will be used in the analysis fixpoint
+ * @param <T>  the type of {@link AbstractState} contained into the analysis
+ *                 state that will be used in the type inference fixpoint
+ * @param <HT> the type of {@link HeapDomain} contained into the abstract state
+ *                 that will be used in the type inference fixpoint
+ * @param <VT> the type of {@link ValueDomain} contained into the abstract state
+ *                 that will be used in the type inference fixpoint
  */
 public class LiSARunner<A extends AbstractState<A, H, V>,
 		H extends HeapDomain<H>,
-		V extends ValueDomain<V>> {
+		V extends ValueDomain<V>,
+		T extends AbstractState<T, HT, VT>,
+		HT extends HeapDomain<HT>,
+		VT extends ValueDomain<VT>> {
 
 	private static final String FIXPOINT_EXCEPTION_MESSAGE = "Exception during fixpoint computation";
 
@@ -71,20 +77,30 @@ public class LiSARunner<A extends AbstractState<A, H, V>,
 
 	private final A state;
 
+	private final T typeState;
+
+	private final Function<T, ExternalSet<Type>> typeExtractor;
+
 	/**
 	 * Builds the runner.
 	 * 
-	 * @param conf      the configuration of the analysis
-	 * @param interproc the interprocedural analysis to use
-	 * @param callGraph the call graph to use
-	 * @param state     the abstract state to use
+	 * @param conf          the configuration of the analysis
+	 * @param interproc     the interprocedural analysis to use
+	 * @param callGraph     the call graph to use
+	 * @param state         the abstract state to use for the analysis
+	 * @param typeState     the abstract state to use for type inference
+	 * @param typeExtractor the abstract state to use the function that can
+	 *                          extract runtime types from {@code typeState}
+	 *                          instances
 	 */
 	LiSARunner(LiSAConfiguration conf, InterproceduralAnalysis<A, H, V> interproc, CallGraph callGraph,
-			A state) {
+			A state, T typeState, Function<T, ExternalSet<Type>> typeExtractor) {
 		this.conf = conf;
 		this.interproc = interproc;
 		this.callGraph = callGraph;
 		this.state = state;
+		this.typeState = typeState;
+		this.typeExtractor = typeExtractor;
 	}
 
 	/**
@@ -173,14 +189,9 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
 
 	@SuppressWarnings("unchecked")
 	private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs) {
-		SimpleAbstractState<H, InferenceSystem<InferredTypes>> typesState;
-		InterproceduralAnalysis<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H,
-				InferenceSystem<InferredTypes>> typesInterproc;
+		T typesState = this.typeState.top();
+		InterproceduralAnalysis<T, HT, VT> typesInterproc;
 		try {
-			// type inference is executed with the simplest abstract state
-			InferenceSystem<InferredTypes> types = new InferenceSystem<>(new InferredTypes());
-			HeapDomain<?> heap = state == null ? LiSAFactory.getDefaultFor(HeapDomain.class) : state.getHeapState();
-			typesState = getInstance(SimpleAbstractState.class, heap, types).top();
 			typesInterproc = getInstance(interproc.getClass());
 			typesInterproc.init(program, callGraph);
 		} catch (AnalysisSetupException | InterproceduralAnalysisException e) {
@@ -202,18 +213,15 @@ private void inferTypes(FileManager fileManager, Program program, Collection<CFG
 				? "Dumping type analysis and propagating it to cfgs"
 				: "Propagating type information to cfgs";
 		for (CFG cfg : IterationLogger.iterate(LOG, allCFGs, message, "cfgs")) {
-			Collection<CFGWithAnalysisResults<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H,
-					InferenceSystem<InferredTypes>>> results = typesInterproc.getAnalysisResultsOf(cfg);
+			Collection<CFGWithAnalysisResults<T, HT, VT>> results = typesInterproc.getAnalysisResultsOf(cfg);
 			if (results.isEmpty()) {
 				LOG.warn("No type information computed for '{}': it is unreachable", cfg);
 				continue;
 			}
 
-			CFGWithAnalysisResults<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H,
-					InferenceSystem<InferredTypes>> result = null;
+			CFGWithAnalysisResults<T, HT, VT> result = null;
 			try {
-				for (CFGWithAnalysisResults<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H,
-						InferenceSystem<InferredTypes>> res : results)
+				for (CFGWithAnalysisResults<T, HT, VT> res : results)
 					if (result == null)
 						result = res;
 					else
@@ -222,36 +230,33 @@ private void inferTypes(FileManager fileManager, Program program, Collection<CFG
 				throw new AnalysisExecutionException("Unable to compute type information for " + cfg, e);
 			}
 
-			cfg.accept(new TypesPropagator<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H>(), result);
+			cfg.accept(new TypesPropagator(), result);
 
-			CFGWithAnalysisResults<SimpleAbstractState<H, InferenceSystem<InferredTypes>>, H,
-					InferenceSystem<InferredTypes>> r = result;
+			CFGWithAnalysisResults<T, HT, VT> r = result;
 			if (conf.isDumpTypeInference())
 				dumpCFG(fileManager, "typing___", r, st -> r.getAnalysisStateAfter(st).toString());
 		}
 	}
 
-	private static class TypesPropagator<A extends AbstractState<A, H, InferenceSystem<InferredTypes>>,
-			H extends HeapDomain<H>>
+	private class TypesPropagator
 			implements
-			GraphVisitor<CFG, Statement, Edge, CFGWithAnalysisResults<A, H, InferenceSystem<InferredTypes>>> {
+			GraphVisitor<CFG, Statement, Edge, CFGWithAnalysisResults<T, HT, VT>> {
 
 		@Override
-		public boolean visit(CFGWithAnalysisResults<A, H, InferenceSystem<InferredTypes>> tool, CFG graph) {
+		public boolean visit(CFGWithAnalysisResults<T, HT, VT> tool, CFG graph) {
 			return true;
 		}
 
 		@Override
-		public boolean visit(CFGWithAnalysisResults<A, H, InferenceSystem<InferredTypes>> tool, CFG graph, Edge edge) {
+		public boolean visit(CFGWithAnalysisResults<T, HT, VT> tool, CFG graph, Edge edge) {
 			return true;
 		}
 
 		@Override
-		public boolean visit(CFGWithAnalysisResults<A, H, InferenceSystem<InferredTypes>> tool, CFG graph,
+		public boolean visit(CFGWithAnalysisResults<T, HT, VT> tool, CFG graph,
 				Statement node) {
 			if (tool != null && node instanceof Expression)
-				((Expression) node).setRuntimeTypes(tool.getAnalysisStateAfter(node).getState().getValueState()
-						.getInferredValue().getRuntimeTypes());
+				((Expression) node).setRuntimeTypes(typeExtractor.apply(tool.getAnalysisStateAfter(node).getState()));
 			return true;
 		}
 	}