| summaryrefslogtreecommitdiff |
diff options
| -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 | ||||
| -rw-r--r-- | data/instructions/example_process.pl | 208 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Parameters.java | 2 |
8 files changed, 298 insertions, 95 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; diff --git a/data/instructions/example_process.pl b/data/instructions/example_process.pl new file mode 100644 index 0000000..17eb9f0 --- /dev/null +++ b/data/instructions/example_process.pl @@ -0,0 +1,208 @@ +(add_element node 237) +(expr_reads 237 192) +(add_element string 56) +(set_attribute label 237 56) +(add_element string 238) +(set_attribute kind 237 238) +(set_attribute depth 237 1) +(add_element node 239) +(node_connect 237 239) +(add_element string 56) +(set_attribute label 239 56) +(add_element string 240) +(set_attribute kind 239 240) +(add_element string 241) +(add_option 239 241) +(set_attribute depth 239 2) +(add_element node 242) +(node_connect 239 242) +(add_element string 56) +(set_attribute label 242 56) +(add_element string 59) +(set_attribute kind 242 59) +(add_element string 60) +(add_option 242 60) +(set_attribute depth 242 3) +(expr_writes 242 243) +(expr_reads 242 219) +(add_element node 244) +(node_connect 237 244) +(add_element string 56) +(set_attribute label 244 56) +(add_element string 240) +(set_attribute kind 244 240) +(set_attribute depth 244 2) +(add_element node 245) +(node_connect 244 245) +(add_element string 56) +(set_attribute label 245 56) +(add_element string 59) +(set_attribute kind 245 59) +(add_element string 60) +(add_option 245 60) +(set_attribute depth 245 3) +(expr_writes 245 195) +(expr_reads 245 198) +(add_element node 246) +(node_connect 237 246) +(add_element string 56) +(set_attribute label 246 56) +(add_element string 240) +(set_attribute kind 246 240) +(set_attribute depth 246 2) +(add_element node 247) +(node_connect 246 247) +(add_element string 56) +(set_attribute label 247 56) +(add_element string 59) +(set_attribute kind 247 59) +(add_element string 60) +(add_option 247 60) +(set_attribute depth 247 3) +(expr_writes 247 243) +(expr_reads 247 200) +(add_element node 248) +(node_connect 237 248) +(add_element string 56) +(set_attribute label 248 56) +(add_element string 240) +(set_attribute kind 248 240) +(set_attribute depth 248 2) +(add_element node 249) +(node_connect 248 249) +(add_element string 56) +(set_attribute label 249 56) +(add_element string 59) +(set_attribute kind 249 59) +(add_element string 60) +(add_option 249 60) +(set_attribute depth 249 3) +(expr_writes 249 243) +(expr_reads 249 202) +(add_element node 250) +(node_connect 237 250) +(add_element string 56) +(set_attribute label 250 56) +(add_element string 240) +(set_attribute kind 250 240) +(set_attribute depth 250 2) +(add_element node 251) +(node_connect 250 251) +(add_element string 56) +(set_attribute label 251 56) +(add_element string 59) +(set_attribute kind 251 59) +(add_element string 60) +(add_option 251 60) +(set_attribute depth 251 3) +(expr_writes 251 243) +(expr_reads 251 204) +(add_element node 252) +(node_connect 237 252) +(add_element string 56) +(set_attribute label 252 56) +(add_element string 240) +(set_attribute kind 252 240) +(set_attribute depth 252 2) +(add_element node 253) +(node_connect 252 253) +(add_element string 56) +(set_attribute label 253 56) +(add_element string 59) +(set_attribute kind 253 59) +(add_element string 60) +(add_option 253 60) +(set_attribute depth 253 3) +(expr_writes 253 243) +(expr_reads 253 206) +(add_element node 254) +(node_connect 237 254) +(add_element string 56) +(set_attribute label 254 56) +(add_element string 240) +(set_attribute kind 254 240) +(set_attribute depth 254 2) +(add_element node 255) +(node_connect 254 255) +(add_element string 56) +(set_attribute label 255 56) +(add_element string 59) +(set_attribute kind 255 59) +(add_element string 60) +(add_option 255 60) +(set_attribute depth 255 3) +(expr_writes 255 243) +(expr_reads 255 208) +(add_element node 256) +(node_connect 237 256) +(add_element string 56) +(set_attribute label 256 56) +(add_element string 240) +(set_attribute kind 256 240) +(set_attribute depth 256 2) +(add_element node 257) +(node_connect 256 257) +(add_element string 56) +(set_attribute label 257 56) +(add_element string 59) +(set_attribute kind 257 59) +(add_element string 60) +(add_option 257 60) +(set_attribute depth 257 3) +(expr_writes 257 243) +(expr_reads 257 210) +(add_element node 258) +(node_connect 237 258) +(add_element string 56) +(set_attribute label 258 56) +(add_element string 240) +(set_attribute kind 258 240) +(set_attribute depth 258 2) +(add_element node 259) +(node_connect 258 259) +(add_element string 56) +(set_attribute label 259 56) +(add_element string 59) +(set_attribute kind 259 59) +(add_element string 60) +(add_option 259 60) +(set_attribute depth 259 3) +(expr_writes 259 243) +(expr_reads 259 212) +(add_element node 260) +(node_connect 237 260) +(add_element string 56) +(set_attribute label 260 56) +(add_element string 240) +(set_attribute kind 260 240) +(set_attribute depth 260 2) +(add_element node 261) +(node_connect 260 261) +(add_element string 56) +(set_attribute label 261 56) +(add_element string 59) +(set_attribute kind 261 59) +(add_element string 60) +(add_option 261 60) +(set_attribute depth 261 3) +(expr_writes 261 243) +(expr_reads 261 214) +(add_element node 262) +(node_connect 237 262) +(add_element string 56) +(set_attribute label 262 56) +(add_element string 240) +(set_attribute kind 262 240) +(set_attribute depth 262 2) +(add_element node 263) +(node_connect 262 263) +(add_element string 56) +(set_attribute label 263 56) +(add_element string 59) +(set_attribute kind 263 59) +(add_element string 60) +(add_option 263 60) +(set_attribute depth 263 3) +(expr_writes 263 243) +(expr_reads 263 217) + diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java index 8d0331b..e9dc648 100644 --- a/instr-to-kodkod/src/Parameters.java +++ b/instr-to-kodkod/src/Parameters.java @@ -16,7 +16,7 @@ public class Parameters + "\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)." + + " source files (in Main.java)." ); } |