| summaryrefslogtreecommitdiff |
path: root/cfg-to-paths
diff options
Diffstat (limited to 'cfg-to-paths')
| -rw-r--r-- | cfg-to-paths/Makefile | 26 | ||||
| -rw-r--r-- | cfg-to-paths/src/ControlFlow.java | 2 | ||||
| -rw-r--r-- | cfg-to-paths/src/Main.java | 76 | ||||
| -rw-r--r-- | cfg-to-paths/src/Node.java | 13 | ||||
| -rw-r--r-- | cfg-to-paths/src/Parameters.java | 45 | ||||
| -rw-r--r-- | cfg-to-paths/src/Path.java | 21 |
6 files changed, 89 insertions, 94 deletions
diff --git a/cfg-to-paths/Makefile b/cfg-to-paths/Makefile index 6db785e..c4d71e2 100644 --- a/cfg-to-paths/Makefile +++ b/cfg-to-paths/Makefile @@ -1,17 +1,15 @@ ## Target(s) Configuration ##################################################### -MODEL_FILE = "../data/instructions/example_1.sl" -LEVEL_DIR = "../data/level/" +MODEL_FILE = "../data/instructions/example_process.pl" +ROOT_NODE = "237" +ID_PREFIX = "p237_" +OUTPUT_FILE = "$(MODEL_FILE).kk" + ## Executables ################################################################# JAVAC = javac JAVA = java -DOWNLOADER = wget ## Java Config ################################################################# -CLASSPATH = "kodkod.jar:./src/:org.sat4j.core.jar" - -## Dependencies ################################################################ -JAR_SOURCE = https://noot-noot.org/onera_2017/jar/ -REQUIRED_JARS = kodkod.jar org.sat4j.core.jar +CLASSPATH = "./src/" ## Makefile Magic ############################################################## SOURCES = $(wildcard src/*.java) @@ -24,13 +22,9 @@ all: $(CLASSES) clean: rm -f $(CLASSES) -run: $(CLASSES) $(REQUIRED_JARS) - $(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE) +run: $(CLASSES) + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) $(ROOT_NODE) $(ID_PREFIX) \ + $(OUTPUT_FILE) -%.class: %.java $(REQUIRED_JARS) +%.class: %.java $(JAVAC) -cp $(CLASSPATH) $< - -%.jar: - echo "Attempting to download missing jar '$@'" - $(DOWNLOADER) "$(JAR_SOURCE)/$@" - diff --git a/cfg-to-paths/src/ControlFlow.java b/cfg-to-paths/src/ControlFlow.java index 629ac49..a0863d8 100644 --- a/cfg-to-paths/src/ControlFlow.java +++ b/cfg-to-paths/src/ControlFlow.java @@ -96,7 +96,7 @@ public class ControlFlow return false; } - if (input[1] != "node") + if (!input[1].equals("node")) { return true; } diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java index ec55450..f81b22f 100644 --- a/cfg-to-paths/src/Main.java +++ b/cfg-to-paths/src/Main.java @@ -1,38 +1,14 @@ /* FIXME: Finer imports */ -import kodkod.ast.*; +import java.util.*; -import kodkod.engine.*; -import kodkod.engine.config.*; -import kodkod.engine.satlab.*; - -import kodkod.instance.*; public class Main { private static Parameters PARAMETERS; - private static Formula get_formula (final VHDLModel model) - { - final Variable w; - - w = Variable.unary("w"); - - return - w.join - ( - model.get_predicate_as_relation("is_accessed_by") - ).no().forSome(w.oneOf(model.get_type_as_relation("waveform"))); - } - public static void main (final String... args) { - final VHDLModel model; - - final Universe univ; - final TupleFactory tf; - final Bounds bounds; - - final Solver solver; - final Solution sol; + final Collection<Path> all_paths; + final Collection<List<Node>> all_subpaths; PARAMETERS = new Parameters(args); @@ -41,51 +17,31 @@ public class Main return; } - model = new VHDLModel(); - try { - VHDLLevel.add_to_model - ( - model, - ( - PARAMETERS.get_levels_directory() - + "/structural_level.data" - ) - ); + ControlFlow.load_file(PARAMETERS.get_model_file()); } catch (final Exception e) { - System.err.println("[E] Could not load structural level:"); - e.printStackTrace(); - - return; - } + System.err.println + ( + "[E] Could not load model file \"" + + PARAMETERS.get_model_file() + + "\":" + ); - try - { - model.parse_file(PARAMETERS.get_model_file()); - } - catch (final Exception e) - { - System.err.println("[E] Could not load instructions:"); e.printStackTrace(); return; } - univ = new Universe(model.get_atoms()); - tf = univ.factory(); - bounds = new Bounds(univ); - - model.add_to_bounds(bounds, tf); + all_paths = Path.get_all_paths_from(PARAMETERS.get_root_node()); - solver = new Solver(); - solver.options().setSolver(SATFactory.DefaultSAT4J); - solver.options().setReporter(new ConsoleReporter()); + all_subpaths = new ArrayList<List<Node>>(); - sol = solver.solve(get_formula(model), bounds); - - System.out.println(sol); + for (final Path p: all_paths) + { + all_subpaths.addAll(p.get_all_subpaths()); + } } } diff --git a/cfg-to-paths/src/Node.java b/cfg-to-paths/src/Node.java index 6f9083d..5f82f64 100644 --- a/cfg-to-paths/src/Node.java +++ b/cfg-to-paths/src/Node.java @@ -51,6 +51,19 @@ public class Node n_a = NODE_FROM_STRING.get(a); n_b = NODE_FROM_STRING.get(b); + if ((n_a == null) || (n_b == null)) + { + System.err.println + ( + "[E] Causality issue: Nodes \"" + + a + + "\" or \"" + + b + + "\" used but not defined." + ); + + return false; + } n_a.next_nodes.add(n_b); return true; diff --git a/cfg-to-paths/src/Parameters.java b/cfg-to-paths/src/Parameters.java index 8d0331b..710b1f7 100644 --- a/cfg-to-paths/src/Parameters.java +++ b/cfg-to-paths/src/Parameters.java @@ -1,7 +1,9 @@ public class Parameters { - private final String levels_dir; private final String model_file; + private final String root_node; + private final String id_prefix; + private final String output_file; private final boolean are_valid; public static void print_usage () @@ -10,42 +12,57 @@ public class Parameters ( "Instr-to-kodkod\n" + "USAGE:\n" - + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS>\n" + + "\tjava Main <INSTRUCTIONS> <ROOT_NODE> <ID_PREFIX> <OUTPUT_FILE>\n" + "PARAMETERS:\n" - + "\t<LEVELS_DIR>\tDirectory containing the level definitions.\n" + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n" - + "NOTES:\n" - + "\tThe properties to be verified still have to be hand coded in the" - + "source files (in Main.java)." + + "\t<ROOT_NODE>\tID of the root node for this DAG.\n" + + "\t<ID_PREFIX>\tPrefix for the IDs of generated paths.\n" + + "\t<OUTPUT_FILE>\tFile in which to output the generated" + + " instructions." ); } public Parameters (String... args) { - if (args.length != 2) + if (args.length != 4) { print_usage(); - levels_dir = new String(); model_file = new String(); + root_node = new String(); + id_prefix = new String(); + output_file = new String(); + are_valid = false; } else { - levels_dir = args[0]; - model_file = args[1]; + model_file = args[0]; + root_node = args[1]; + id_prefix = args[2]; + output_file = args[3]; are_valid = true; } } - public String get_levels_directory () + public String get_model_file () { - return levels_dir; + return model_file; } - public String get_model_file () + public String get_root_node () { - return model_file; + return root_node; + } + + public String get_id_prefix () + { + return id_prefix; + } + + public String get_output_file () + { + return output_file; } public boolean are_valid () diff --git a/cfg-to-paths/src/Path.java b/cfg-to-paths/src/Path.java index 80b433f..76ba28a 100644 --- a/cfg-to-paths/src/Path.java +++ b/cfg-to-paths/src/Path.java @@ -31,6 +31,21 @@ public class Path { final Collection<Path> result; final Stack<Path> waiting_list; + final Node root_node; + + root_node = Node.get_node(root); + + if (root_node == null) + { + System.err.println + ( + "[E] Could not find root node \"" + + root + + "\"." + ); + + return null; + } result = new ArrayList<Path>(); waiting_list = new Stack<Path>(); @@ -63,17 +78,17 @@ public class Path return result; } - public static Collection<List<Node>> get_subpaths (final Path p) + public Collection<List<Node>> get_all_subpaths () { final Collection<List<Node>> result; final int path_length; result = new ArrayList<List<Node>>(); - path_length = p.nodes.size(); + path_length = nodes.size(); for (int i = 0; i < path_length; ++i) { - result.add(p.nodes.subList(i, path_length)); + result.add(nodes.subList(i, path_length)); } return result; |