diff --git a/README.md b/README.md index 4daade4961..077aeeb6c0 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), [`cfa2dot`](subprojects/cfa2dot) | [`sts-cli`](subprojects/sts-cli) | [`xta-cli`](subprojects/xta-cli) | +| **Tools** | | [`cfa-cli`](subprojects/cfa-cli), [`cfa-metrics`](subprojects/cfa-metrics) | [`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/settings.gradle.kts b/settings.gradle.kts index 04bc815e4b..2dd083ded0 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -3,7 +3,6 @@ rootProject.name = "theta" include( "analysis", "cfa", - "cfa2dot", "cfa-analysis", "cfa-cli", "cfa-metrics", diff --git a/subprojects/cfa-cli/README.md b/subprojects/cfa-cli/README.md index 7db086b6bb..98bf22706b 100644 --- a/subprojects/cfa-cli/README.md +++ b/subprojects/cfa-cli/README.md @@ -75,8 +75,11 @@ In general, values between `5` to `50` perform well (see Section 3.1.1 of [our J - `CONJUNCTS`: Split predicates into conjuncts. - `ATOMS`: Split predicates into atoms. - `--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. + - `GLOBAL`: The same precision is applied in each location of the CFA. + - `LOCAL`: Each location can have a possibly different precision. +- `--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. ### For developer usage 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 0fed92d5a1..bca8498d31 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 @@ -41,6 +41,7 @@ import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.PredSplit; import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Refinement; import hu.bme.mit.theta.cfa.analysis.config.CfaConfigBuilder.Search; +import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer; import hu.bme.mit.theta.cfa.dsl.CfaDslManager; import hu.bme.mit.theta.common.logging.ConsoleLogger; import hu.bme.mit.theta.common.logging.Logger; @@ -48,6 +49,8 @@ import hu.bme.mit.theta.common.logging.NullLogger; import hu.bme.mit.theta.common.table.BasicTableWriter; 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.solver.*; import hu.bme.mit.theta.solver.z3.*; @@ -99,6 +102,9 @@ public class CfaCli { @Parameter(names = "--header", description = "Print only a header (for benchmarks)", help = true) boolean headerOnly = false; + @Parameter(names = "--visualize", description = "Visualize CFA to this file without running the algorithm") + String visualize = null; + private Logger logger; public CfaCli(final String[] args) { @@ -122,6 +128,11 @@ private void run() { return; } + if (visualize != null) { + visualize(); + return; + } + if (headerOnly) { printHeader(); return; @@ -145,6 +156,36 @@ private void run() { } } + private void visualize() { + try { + final CFA cfa = loadModel(); + final Graph graph = CfaVisualizer.visualize(cfa); + String ext = getFileExtension(visualize.toLowerCase()); + switch(ext) { + case "pdf": + GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.PDF); + break; + case "png": + GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.PNG); + break; + case "svg": + GraphvizWriter.getInstance().writeFile(graph, visualize, GraphvizWriter.Format.SVG); + break; + default: + GraphvizWriter.getInstance().writeFile(graph, visualize); + break; + } + } catch (final Throwable ex) { + printError(ex); + } + } + + private String getFileExtension(String name) { + int lastIndexOf = name.lastIndexOf("."); + if (lastIndexOf == -1) return ""; + return name.substring(lastIndexOf + 1); + } + private void printHeader() { final String[] header = new String[]{"Result", "TimeMs", "AlgoTimeMs", "AbsTimeMs", "RefTimeMs", "Iterations", "ArgSize", "ArgDepth", "ArgMeanBranchFactor", "CexLen"}; diff --git a/subprojects/cfa2dot/bin/.gitignore b/subprojects/cfa2dot/bin/.gitignore deleted file mode 100644 index ddf9c65631..0000000000 --- a/subprojects/cfa2dot/bin/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/main/ diff --git a/subprojects/cfa2dot/build.gradle.kts b/subprojects/cfa2dot/build.gradle.kts deleted file mode 100644 index fa9570823c..0000000000 --- a/subprojects/cfa2dot/build.gradle.kts +++ /dev/null @@ -1,12 +0,0 @@ -plugins { - id("java-common") - id("cli-tool") -} - -dependencies { - compile(project(":theta-cfa-analysis")) -} - -application { - mainClassName = "hu.bme.mit.theta.cfa.cfa2dot.CfaToDotMain" -} diff --git a/subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java b/subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java deleted file mode 100644 index cd78aa9975..0000000000 --- a/subprojects/cfa2dot/src/main/java/hu/bme/mit/theta/cfa/cfa2dot/CfaToDotMain.java +++ /dev/null @@ -1,86 +0,0 @@ -/* - * Copyright 2017 Budapest University of Technology and Economics - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -package hu.bme.mit.theta.cfa.cfa2dot; - -import java.io.FileInputStream; -import java.io.IOException; -import java.io.InputStream; - -import com.beust.jcommander.JCommander; -import com.beust.jcommander.Parameter; -import com.beust.jcommander.ParameterException; - -import hu.bme.mit.theta.cfa.CFA; -import hu.bme.mit.theta.cfa.dsl.CfaDslManager; -import hu.bme.mit.theta.cfa.analysis.utils.CfaVisualizer; -import hu.bme.mit.theta.common.visualization.Graph; -import hu.bme.mit.theta.common.visualization.writer.GraphvizWriter; - -public final class CfaToDotMain { - private static final String JAR_NAME = "theta-cfa2dot.jar"; - private final String[] args; - - @Parameter(names = {"-c", "--cfa"}, description = "Path of the input cfa", required = true) - String cfapath; - - @Parameter(names = {"-d", "--dot"}, description = "Path of the output dot", required = false) - String dotpath; - - public CfaToDotMain(final String[] args) { - this.args = args; - } - - public static void main(final String[] args) { - final CfaToDotMain mainApp = new CfaToDotMain(args); - mainApp.run(); - } - - private void run() { - try { - JCommander.newBuilder().addObject(this).programName(JAR_NAME).build().parse(args); - } catch (final ParameterException ex) { - System.out.println(ex.getMessage()); - ex.usage(); - return; - } - - try { - final CFA cfa = loadModel(cfapath); - final Graph graph = CfaVisualizer.visualize(cfa); - if (dotpath == null) { - dotpath = cfapath.substring(0, cfapath.lastIndexOf('.')) + ".dot"; - } - GraphvizWriter.getInstance().writeFile(graph, dotpath); - return; - } catch (final Throwable ex) { - printError(ex); - } - - } - - private static CFA loadModel(final String path) throws IOException { - final InputStream inputStream = new FileInputStream(path); - final CFA cfa = CfaDslManager.createCfa(inputStream); - return cfa; - } - - private static void printError(final Throwable ex) { - final String message = ex.getMessage() == null ? "" : ": " + ex.getMessage(); - System.out.println("Exception occured: " + ex.getClass().getSimpleName()); - System.out.println("Message: " + message); - } - -}