Merge cfa-metrics into cfa-cli

README.md

@@ -56,7 +56,7 @@ Each project contains a README.md in its root directory describing its purpose i
 
 |  | Common | CFA | STS | XTA |
 |--|--|--|--|--|
-| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli), [`cfa-metrics`](subprojects/cfa-metrics) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) |
+| **Tools** |  | [`cfa-cli`](subprojects/cfa-cli) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) |
 | **Analyses** | [`analysis`](subprojects/analysis) | [`cfa-analysis`](subprojects/cfa-analysis) | [`sts-analysis`](subprojects/sts-analysis) | [`xta-analysis`](subprojects/xta-analysis) |
 | **Formalisms** | [`core`](subprojects/core), [`common`](subprojects/common) | [`cfa`](subprojects/cfa) | [`sts`](subprojects/sts) | [`xta`](subprojects/xta) |
 | **SMT solvers** | [`solver`](subprojects/solver), [`solver-z3`](subprojects/solver-z3) |

build.gradle.kts

@@ -10,7 +10,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.inf.theta"
-    version = "1.0.1"
+    version = "1.1.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

settings.gradle.kts

@@ -5,7 +5,6 @@ include(
         "cfa",
         "cfa-analysis",
         "cfa-cli",
-        "cfa-metrics",
         "common",
         "core",
         "solver",

subprojects/cfa-cli/README.md

@@ -77,6 +77,7 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J
 - `--precgranularity`: Granularity of the precision, possible values:
   - `GLOBAL`: The same precision is applied in each location of the CFA.
   - `LOCAL`: Each location can have a possibly different precision.
+- `--metrics`: Print metrics about the CFA without running the algorithm.
 - `--visualize`: Visualize the CFA without running the algorithm.
 If the extension of the output file is `pdf`, `png` or `svg` an automatic visualization is performed, for which [GraphViz](../../doc/Build.md) has to be available on `PATH`.
 Otherwise, the output is simply in `dot` format.

subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java

@@ -16,6 +16,10 @@
 package hu.bme.mit.theta.cfa.cli;
 
 import java.io.*;
+import java.util.HashSet;
+import java.util.LinkedList;
+import java.util.Queue;
+import java.util.Set;
 import java.util.concurrent.TimeUnit;
 
 import com.beust.jcommander.JCommander;
@@ -51,6 +55,11 @@
 import hu.bme.mit.theta.common.table.TableWriter;
 import hu.bme.mit.theta.common.visualization.Graph;
 import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter;
+import hu.bme.mit.theta.core.stmt.AssignStmt;
+import hu.bme.mit.theta.core.stmt.AssumeStmt;
+import hu.bme.mit.theta.core.stmt.HavocStmt;
+import hu.bme.mit.theta.core.type.booltype.BoolExprs;
+import hu.bme.mit.theta.core.type.inttype.IntExprs;
 import hu.bme.mit.theta.solver.*;
 import hu.bme.mit.theta.solver.z3.*;
 
@@ -105,6 +114,9 @@ public class CfaCli {
 	@Parameter(names = "--visualize", description = "Visualize CFA to this file without running the algorithm")
 	String visualize = null;
 
+	@Parameter(names = "--metrics", description = "Print metrics about the CFA without running the algorithm")
+	boolean metrics = false;
+
 	private Logger logger;
 
 	public CfaCli(final String[] args) {
@@ -133,6 +145,11 @@ private void run() {
 			return;
 		}
 
+		if (metrics) {
+			printMetrics();
+			return;
+		}
+
 		if (headerOnly) {
 			printHeader();
 			return;
@@ -156,6 +173,47 @@ private void run() {
 		}
 	}
 
+	private void printMetrics(){
+		try {
+			final CFA cfa = loadModel();
+			logger.write(Level.RESULT, "Vars: %s%n" , cfa.getVars().size());
+			logger.write(Level.RESULT, "Bool vars: %s%n" , cfa.getVars().stream().filter(v -> v.getType().equals(BoolExprs.Bool())).count());
+			logger.write(Level.RESULT, "Int vars: %s%n" , cfa.getVars().stream().filter(v -> v.getType().equals(IntExprs.Int())).count());
+			logger.write(Level.RESULT, "Locs: %s%n" , cfa.getLocs().size());
+			logger.write(Level.RESULT, "Edges: %s%n" , cfa.getEdges().size());
+			logger.write(Level.RESULT, "Cyclomatic complexity: %s%n" , cfa.getEdges().size() - cfa.getLocs().size() + 2 * getCfaComponents(cfa));
+			logger.write(Level.RESULT, "Assignments: %s%n" , cfa.getEdges().stream().filter(e -> e.getStmt() instanceof AssignStmt).count());
+			logger.write(Level.RESULT, "Assumptions: %s%n" , cfa.getEdges().stream().filter(e -> e.getStmt() instanceof AssumeStmt).count());
+			logger.write(Level.RESULT, "Havocs: %s%n" , cfa.getEdges().stream().filter(e -> e.getStmt() instanceof HavocStmt).count());
+		} catch (final Throwable ex) {
+			printError(ex);
+		}
+	}
+
+	public static int getCfaComponents(final CFA cfa) {
+		final Set<CFA.Loc> visited = new HashSet<>();
+		int components = 0;
+
+		for (final CFA.Loc loc : cfa.getLocs()) {
+			if (!visited.contains(loc)) {
+				components++;
+				visited.add(loc);
+				final Queue<CFA.Loc> queue = new LinkedList<>();
+				queue.add(loc);
+				while (!queue.isEmpty()) {
+					final CFA.Loc next = queue.remove();
+					for (final CFA.Edge edge : next.getOutEdges()) {
+						if (!visited.contains(edge.getTarget())) {
+							visited.add(edge.getTarget());
+							queue.add(edge.getTarget());
+						}
+					}
+				}
+			}
+		}
+		return components;
+	}
+
 	private void visualize() {
 		try {
 			final CFA cfa = loadModel();