Call resolution information in semantic checks

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

@@ -43,7 +43,7 @@ public class LiSAConfiguration {
 	/**
 	 * The collection of semantic checks to execute
 	 */
-	private final Collection<SemanticCheck> semanticChecks;
+	private final Collection<SemanticCheck<?, ?, ?>> semanticChecks;
 
 	/**
 	 * The callgraph to use during the analysis
@@ -179,7 +179,7 @@ public LiSAConfiguration addSyntacticChecks(Collection<SyntacticCheck> checks) {
 	 * 
 	 * @return the current (modified) configuration
 	 */
-	public LiSAConfiguration addSemanticCheck(SemanticCheck check) {
+	public LiSAConfiguration addSemanticCheck(SemanticCheck<?, ?, ?> check) {
 		semanticChecks.add(check);
 		return this;
 	}
@@ -192,7 +192,7 @@ public LiSAConfiguration addSemanticCheck(SemanticCheck check) {
 	 * 
 	 * @return the current (modified) configuration
 	 */
-	public LiSAConfiguration addSemanticChecks(Collection<SemanticCheck> checks) {
+	public LiSAConfiguration addSemanticChecks(Collection<SemanticCheck<?, ?, ?>> checks) {
 		semanticChecks.addAll(checks);
 		return this;
 	}
@@ -469,7 +469,7 @@ public Collection<SyntacticCheck> getSyntacticChecks() {
 	 * 
 	 * @return the semantic checks
 	 */
-	public Collection<SemanticCheck> getSemanticChecks() {
+	public Collection<SemanticCheck<?, ?, ?>> getSemanticChecks() {
 		return semanticChecks;
 	}
 
@@ -672,7 +672,7 @@ public String toString() {
 				.append(semanticChecks.size())
 				.append(" semantic checks to execute")
 				.append((semanticChecks.isEmpty() ? "" : ":"));
-		for (SemanticCheck check : semanticChecks)
+		for (SemanticCheck<?, ?, ?> check : semanticChecks)
 			res.append("\n      ")
 					.append(check.getClass().getSimpleName());
 		return res.toString();

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

@@ -16,12 +16,16 @@
 import it.unive.lisa.analysis.nonrelational.value.ValueEnvironment;
 import it.unive.lisa.analysis.numeric.Interval;
 import it.unive.lisa.analysis.value.ValueDomain;
+import it.unive.lisa.interprocedural.ContextBasedAnalysis;
+import it.unive.lisa.interprocedural.ContextSensitivityToken;
 import it.unive.lisa.interprocedural.InterproceduralAnalysis;
 import it.unive.lisa.interprocedural.ModularWorstCaseAnalysis;
+import it.unive.lisa.interprocedural.RecursionFreeToken;
 import it.unive.lisa.interprocedural.callgraph.CallGraph;
 import it.unive.lisa.interprocedural.callgraph.RTACallGraph;
 import java.lang.reflect.Constructor;
 import java.lang.reflect.InvocationTargetException;
+import java.lang.reflect.Method;
 import java.lang.reflect.Modifier;
 import java.lang.reflect.ParameterizedType;
 import java.lang.reflect.Type;
@@ -76,14 +80,30 @@ public final class LiSAFactory {
 		DEFAULT_IMPLEMENTATIONS.put(ValueDomain.class, Interval.class);
 		DEFAULT_IMPLEMENTATIONS.put(AbstractState.class, SimpleAbstractState.class);
 		DEFAULT_PARAMETERS.put(SimpleAbstractState.class, new Class[] { MonolithicHeap.class, Interval.class });
+		DEFAULT_PARAMETERS.put(ContextBasedAnalysis.class, new Class[] { RecursionFreeToken.class });
 	}
 
 	private LiSAFactory() {
 		// this class is just a static holder
 	}
 
+	@SuppressWarnings("unchecked")
 	private static <T> T construct(Class<T> component, Class<?>[] argTypes, Object[] params)
 			throws AnalysisSetupException {
+		if (ContextSensitivityToken.class.isAssignableFrom(component)) {
+			// tokens use the getSingleton() pattern for construction
+			try {
+				Method method = component.getMethod("getSingleton");
+				if (!Modifier.isStatic(method.getModifiers()))
+					throw new AnalysisSetupException(
+							"Unable to instantiate " + component.getSimpleName() + ": getSingleton() is not static");
+				return (T) method.invoke(null);
+			} catch (NoSuchMethodException | SecurityException | IllegalAccessException | IllegalArgumentException
+					| InvocationTargetException e) {
+				throw new AnalysisSetupException("Unable to instantiate " + component.getSimpleName(), e);
+			}
+		}
+
 		try {
 			Constructor<T> constructor = component.getConstructor(argTypes);
 			return constructor.newInstance(params);

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

@@ -11,6 +11,7 @@
 import it.unive.lisa.caches.Caches;
 import it.unive.lisa.checks.ChecksExecutor;
 import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults;
+import it.unive.lisa.checks.semantic.SemanticCheck;
 import it.unive.lisa.checks.syntactic.CheckTool;
 import it.unive.lisa.checks.warnings.Warning;
 import it.unive.lisa.interprocedural.InterproceduralAnalysis;
@@ -152,11 +153,13 @@ Collection<Warning> run(Program program, FileManager fileManager) {
 			for (CFG cfg : allCFGs)
 				results.put(cfg, interproc.getAnalysisResultsOf(cfg));
 
-			if (!conf.getSemanticChecks().isEmpty()) {
+			@SuppressWarnings({ "rawtypes", "unchecked" })
+			Collection<SemanticCheck<A, H, V>> semanticChecks = (Collection) conf.getSemanticChecks();
+			if (!semanticChecks.isEmpty()) {
 				CheckToolWithAnalysisResults<A, H,
-						V> toolWithResults = new CheckToolWithAnalysisResults<>(tool, results);
-				tool = toolWithResults;
-				ChecksExecutor.executeAll(toolWithResults, program, conf.getSemanticChecks());
+						V> tool2 = new CheckToolWithAnalysisResults<>(tool, results, callGraph);
+				tool = tool2;
+				ChecksExecutor.executeAll(tool2, program, semanticChecks);
 			} else
 				LOG.warn("Skipping semantic checks execution since none have been provided");
 		} else
@@ -191,10 +194,13 @@ private void analyze(Collection<CFG> allCFGs, FileManager fileManager) {
 	private void inferTypes(FileManager fileManager, Program program, Collection<CFG> allCFGs) {
 		T typesState = this.typeState.top();
 		InterproceduralAnalysis<T, HT, VT> typesInterproc;
+		CallGraph typesCg;
 		try {
+			typesCg = getInstance(callGraph.getClass());
 			typesInterproc = getInstance(interproc.getClass());
-			typesInterproc.init(program, callGraph);
-		} catch (AnalysisSetupException | InterproceduralAnalysisException e) {
+			typesCg.init(program);
+			typesInterproc.init(program, typesCg);
+		} catch (AnalysisSetupException | InterproceduralAnalysisException | CallGraphConstructionException e) {
 			throw new AnalysisExecutionException("Unable to initialize type inference", e);
 		}
 

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

@@ -224,6 +224,8 @@ public final AnalysisState<A, H, V> getAbstractResultOf(CFGCall call, AnalysisSt
 
 		token = token.popToken();
 
+		callgraph.registerCall(call);
+
 		return result;
 	}
 

lisa/lisa-core/src/test/java/it/unive/lisa/cron/nonInterference/NonInterferenceTest.java

@@ -1,13 +1,11 @@
 package it.unive.lisa.cron.nonInterference;
 
-import static it.unive.lisa.LiSAFactory.getDefaultFor;
-
 import it.unive.lisa.AnalysisSetupException;
 import it.unive.lisa.AnalysisTestExecutor;
 import it.unive.lisa.LiSAConfiguration;
-import it.unive.lisa.analysis.AbstractState;
 import it.unive.lisa.analysis.CFGWithAnalysisResults;
-import it.unive.lisa.analysis.heap.HeapDomain;
+import it.unive.lisa.analysis.SimpleAbstractState;
+import it.unive.lisa.analysis.heap.MonolithicHeap;
 import it.unive.lisa.analysis.nonInterference.NonInterference;
 import it.unive.lisa.analysis.nonrelational.inference.InferenceSystem;
 import it.unive.lisa.checks.semantic.CheckToolWithAnalysisResults;
@@ -30,60 +28,78 @@ public class NonInterferenceTest extends AnalysisTestExecutor {
 	@Test
 	public void testConfidentialityNI() throws AnalysisSetupException {
 		LiSAConfiguration conf = new LiSAConfiguration().setDumpAnalysis(true)
-				.setAbstractState(getDefaultFor(AbstractState.class,
-						getDefaultFor(HeapDomain.class), new NonInterference()))
+				.setAbstractState(
+						new SimpleAbstractState<>(new MonolithicHeap(), new InferenceSystem<>(new NonInterference())))
 				.addSemanticCheck(new NICheck());
 		perform("non-interference/confidentiality", "program.imp", conf);
 	}
 
 	@Test
 	public void testIntegrityNI() throws AnalysisSetupException {
 		LiSAConfiguration conf = new LiSAConfiguration().setDumpAnalysis(true)
-				.setAbstractState(getDefaultFor(AbstractState.class,
-						getDefaultFor(HeapDomain.class), new NonInterference()))
+				.setAbstractState(
+						new SimpleAbstractState<>(new MonolithicHeap(), new InferenceSystem<>(new NonInterference())))
 				.addSemanticCheck(new NICheck());
 		perform("non-interference/integrity", "program.imp", conf);
 	}
 
 	@Test
 	public void testDeclassification() throws AnalysisSetupException {
 		LiSAConfiguration conf = new LiSAConfiguration().setDumpAnalysis(true)
-				.setAbstractState(getDefaultFor(AbstractState.class,
-						getDefaultFor(HeapDomain.class), new NonInterference()))
+				.setAbstractState(
+						new SimpleAbstractState<>(new MonolithicHeap(), new InferenceSystem<>(new NonInterference())))
 				.setCallGraph(new RTACallGraph())
 				.setInterproceduralAnalysis(new ContextBasedAnalysis<>(RecursionFreeToken.getSingleton()))
 				.addSemanticCheck(new NICheck());
 		perform("non-interference/interproc", "program.imp", conf);
 	}
 
-	private static class NICheck implements SemanticCheck {
+	private static class NICheck
+			implements SemanticCheck<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+					MonolithicHeap, InferenceSystem<NonInterference>> {
 
 		@Override
-		public void beforeExecution(CheckToolWithAnalysisResults<?, ?, ?> tool) {
+		public void beforeExecution(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool) {
 		}
 
 		@Override
-		public void afterExecution(CheckToolWithAnalysisResults<?, ?, ?> tool) {
+		public void afterExecution(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool) {
 		}
 
 		@Override
-		public boolean visitCompilationUnit(CheckToolWithAnalysisResults<?, ?, ?> tool, CompilationUnit unit) {
+		public boolean visitCompilationUnit(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool,
+				CompilationUnit unit) {
 			return true;
 		}
 
 		@Override
-		public void visitGlobal(CheckToolWithAnalysisResults<?, ?, ?> tool, Unit unit, Global global,
+		public void visitGlobal(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool,
+				Unit unit, Global global,
 				boolean instance) {
 		}
 
 		@Override
-		public boolean visit(CheckToolWithAnalysisResults<?, ?, ?> tool, CFG graph) {
+		public boolean visit(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool,
+				CFG graph) {
 			return true;
 		}
 
 		@Override
 		@SuppressWarnings({ "unchecked" })
-		public boolean visit(CheckToolWithAnalysisResults<?, ?, ?> tool, CFG graph, Statement node) {
+		public boolean visit(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool,
+				CFG graph, Statement node) {
 			if (!(node instanceof Assignment))
 				return true;
 
@@ -119,7 +135,10 @@ public boolean visit(CheckToolWithAnalysisResults<?, ?, ?> tool, CFG graph, Stat
 		}
 
 		@Override
-		public boolean visit(CheckToolWithAnalysisResults<?, ?, ?> tool, CFG graph, Edge edge) {
+		public boolean visit(
+				CheckToolWithAnalysisResults<SimpleAbstractState<MonolithicHeap, InferenceSystem<NonInterference>>,
+						MonolithicHeap, InferenceSystem<NonInterference>> tool,
+				CFG graph, Edge edge) {
 			return true;
 		}
 

lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/CheckToolWithAnalysisResults.java

@@ -5,7 +5,12 @@
 import it.unive.lisa.analysis.heap.HeapDomain;
 import it.unive.lisa.analysis.value.ValueDomain;
 import it.unive.lisa.checks.syntactic.CheckTool;
+import it.unive.lisa.interprocedural.callgraph.CallGraph;
+import it.unive.lisa.interprocedural.callgraph.CallResolutionException;
 import it.unive.lisa.program.cfg.CFG;
+import it.unive.lisa.program.cfg.CodeMember;
+import it.unive.lisa.program.cfg.statement.call.Call;
+import it.unive.lisa.program.cfg.statement.call.UnresolvedCall;
 import java.util.Collection;
 import java.util.Map;
 
@@ -25,26 +30,33 @@ public class CheckToolWithAnalysisResults<A extends AbstractState<A, H, V>,
 
 	private final Map<CFG, Collection<CFGWithAnalysisResults<A, H, V>>> results;
 
+	private final CallGraph callgraph;
+
 	/**
 	 * Builds the tool, storing the given results.
 	 * 
-	 * @param results the results to store
+	 * @param results   the results to store
+	 * @param callgraph the callgraph that has been built during the analysis
 	 */
-	public CheckToolWithAnalysisResults(Map<CFG, Collection<CFGWithAnalysisResults<A, H, V>>> results) {
-		super();
+	public CheckToolWithAnalysisResults(Map<CFG, Collection<CFGWithAnalysisResults<A, H, V>>> results,
+			CallGraph callgraph) {
 		this.results = results;
+		this.callgraph = callgraph;
 	}
 
 	/**
 	 * Builds the tool, copying the given tool and storing the given results.
 	 * 
-	 * @param other   the tool to copy
-	 * @param results the results to store
+	 * @param other     the tool to copy
+	 * @param results   the results to store
+	 * @param callgraph the callgraph that has been built during the analysis
 	 */
 	public CheckToolWithAnalysisResults(CheckTool other,
-			Map<CFG, Collection<CFGWithAnalysisResults<A, H, V>>> results) {
+			Map<CFG, Collection<CFGWithAnalysisResults<A, H, V>>> results,
+			CallGraph callgraph) {
 		super(other);
 		this.results = results;
+		this.callgraph = callgraph;
 	}
 
 	/**
@@ -58,4 +70,59 @@ public CheckToolWithAnalysisResults(CheckTool other,
 	public Collection<CFGWithAnalysisResults<A, H, V>> getResultOf(CFG cfg) {
 		return results.get(cfg);
 	}
+
+	/**
+	 * Yields all the {@link CodeMember}s that call the given one, according to
+	 * the {@link CallGraph} that has been built during the analysis.
+	 * 
+	 * @param cm the target code member
+	 * 
+	 * @return the collection of callers code members
+	 */
+	public Collection<CodeMember> getCallers(CodeMember cm) {
+		return callgraph.getCallers(cm);
+	}
+
+	/**
+	 * Yields all the {@link CodeMember}s that are called by the given one,
+	 * according to the {@link CallGraph} that has been built during the
+	 * analysis.
+	 * 
+	 * @param cm the target code member
+	 * 
+	 * @return the collection of called code members
+	 */
+	public Collection<CodeMember> getCallees(CodeMember cm) {
+		return callgraph.getCallees(cm);
+	}
+
+	/**
+	 * Yields all the {@link Call}s that targets the given {@link CodeMember},
+	 * according to the {@link CallGraph} that has been built during the
+	 * analysis.
+	 * 
+	 * @param cm the target code member
+	 * 
+	 * @return the collection of calls that target the code member
+	 */
+	public Collection<Call> getCallSites(CodeMember cm) {
+		return callgraph.getCallSites(cm);
+	}
+
+	/**
+	 * Yields the resolved version of the given call, according to the
+	 * {@link CallGraph} that has been built during the analysis. Yields
+	 * {@code null} if the call cannot be resolved (i.e. an exception happened).
+	 * 
+	 * @param call the call to resolve
+	 * 
+	 * @return the resolved version of the given call, or {@code null}
+	 */
+	public Call getResolvedVersion(UnresolvedCall call) {
+		try {
+			return callgraph.resolve(call);
+		} catch (CallResolutionException e) {
+			return null;
+		}
+	}
 }

lisa/lisa-sdk/src/main/java/it/unive/lisa/checks/semantic/SemanticCheck.java

@@ -1,5 +1,8 @@
 package it.unive.lisa.checks.semantic;
 
+import it.unive.lisa.analysis.AbstractState;
+import it.unive.lisa.analysis.heap.HeapDomain;
+import it.unive.lisa.analysis.value.ValueDomain;
 import it.unive.lisa.checks.Check;
 
 /**
@@ -9,6 +12,12 @@
  * as auxiliary tool during the inspection.
  * 
  * @author <a href="mailto:luca.negrini@unive.it">Luca Negrini</a>
+ * 
+ * @param <A> the type of {@link AbstractState} contained in the results
+ * @param <H> the type of {@link HeapDomain} contained in the results
+ * @param <V> the type of {@link ValueDomain} contained in the results
  */
-public interface SemanticCheck extends Check<CheckToolWithAnalysisResults<?, ?, ?>> {
+public interface SemanticCheck<A extends AbstractState<A, H, V>,
+		H extends HeapDomain<H>,
+		V extends ValueDomain<V>> extends Check<CheckToolWithAnalysisResults<A, H, V>> {
 }