diff --git a/README.md b/README.md index 077aeeb6c0..4b8c0b2491 100644 --- a/README.md +++ b/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) | diff --git a/build.gradle.kts b/build.gradle.kts index d20af0de63..ddebee8b35 100644 --- a/build.gradle.kts +++ b/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")) } diff --git a/settings.gradle.kts b/settings.gradle.kts index 2dd083ded0..ffe97173ff 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -5,7 +5,6 @@ include( "cfa", "cfa-analysis", "cfa-cli", - "cfa-metrics", "common", "core", "solver", diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md index 98bf22706b..68af87d76b 100644 --- a/subprojects/cfa-cli/README.md +++ b/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. diff --git a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java b/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java index bca8498d31..1ea7653c6e 100644 --- a/subprojects/cfa-cli/src/main/java/hu/bme/mit/theta/cfa/cli/CfaCli.java +++ b/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 visited = new HashSet<>(); + int components = 0; + + for (final CFA.Loc loc : cfa.getLocs()) { + if (!visited.contains(loc)) { + components++; + visited.add(loc); + final Queue 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(); diff --git a/subprojects/cfa-metrics/bin/.gitignore b/subprojects/cfa-metrics/bin/.gitignore deleted file mode 100644 index ddf9c65631..0000000000 --- a/subprojects/cfa-metrics/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/main/ diff --git a/subprojects/cfa-metrics/build.gradle.kts b/subprojects/cfa-metrics/build.gradle.kts deleted file mode 100644 index bfa75701f8..0000000000 --- a/subprojects/cfa-metrics/build.gradle.kts +++ /dev/null @@ -1,12 +0,0 @@ -plugins { - id("java-common") - id("cli-tool") -} - -dependencies { - compile(project(":theta-cfa")) -} - -application { - mainClassName = "hu.bme.mit.theta.cfa.metrics.CfaMetrics" -} diff --git a/subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java b/subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java deleted file mode 100644 index 219c538ebd..0000000000 --- a/subprojects/cfa-metrics/src/main/java/hu/bme/mit/theta/cfa/metrics/CfaMetrics.java +++ /dev/null @@ -1,81 +0,0 @@ -package hu.bme.mit.theta.cfa.metrics; - -import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStream; -import java.util.HashSet; -import java.util.LinkedList; -import java.util.Queue; -import java.util.Set; - -import hu.bme.mit.theta.cfa.CFA; -import hu.bme.mit.theta.cfa.CFA.Edge; -import hu.bme.mit.theta.cfa.CFA.Loc; -import hu.bme.mit.theta.cfa.dsl.CfaDslManager; -import hu.bme.mit.theta.common.table.BasicTableWriter; -import hu.bme.mit.theta.common.table.TableWriter; -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; - -/** - * A command line tool for getting metrics of a CFA. - */ -public class CfaMetrics { - - public static void main(final String[] args) throws IOException { - final TableWriter writer = new BasicTableWriter(System.out, ",", "\"", "\""); - - if (args.length == 1 && "--header".equals(args[0])) { - writer.cell("Model").cell("Vars").cell("BoolVars").cell("IntVars").cell("Locs").cell("Edges") - .cell("CyclomaticComplexity").cell("Assigns").cell("Assumes").cell("Havocs"); - writer.newRow(); - return; - } - - final InputStream inputStream = new FileInputStream(args[0]); - final CFA cfa = CfaDslManager.createCfa(inputStream); - inputStream.close(); - - writer.cell(args[0]); - writer.cell(cfa.getVars().size()); - writer.cell(cfa.getVars().stream().filter(v -> v.getType().equals(BoolExprs.Bool())).count()); - writer.cell(cfa.getVars().stream().filter(v -> v.getType().equals(IntExprs.Int())).count()); - writer.cell(cfa.getLocs().size()); - writer.cell(cfa.getEdges().size()); - writer.cell(cfa.getEdges().size() - cfa.getLocs().size() + 2 * getComponents(cfa)); - writer.cell(cfa.getEdges().stream().filter(e -> e.getStmt() instanceof AssignStmt).count()); - writer.cell(cfa.getEdges().stream().filter(e -> e.getStmt() instanceof AssumeStmt).count()); - writer.cell(cfa.getEdges().stream().filter(e -> e.getStmt() instanceof HavocStmt).count()); - writer.newRow(); - } - - public static int getComponents(final CFA cfa) { - final Set visited = new HashSet<>(); - int components = 0; - - for (final Loc loc : cfa.getLocs()) { - if (!visited.contains(loc)) { - components++; - visited.add(loc); - final Queue queue = new LinkedList<>(); - queue.add(loc); - while (!queue.isEmpty()) { - final Loc next = queue.remove(); - for (final Edge edge : next.getOutEdges()) { - if (!visited.contains(edge.getTarget())) { - visited.add(edge.getTarget()); - queue.add(edge.getTarget()); - } - } - } - } - } - - return components; - - } - -}