| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/cfg-to-paths')
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/Makefile | 35 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/ControlFlow.java | 142 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Main.java | 114 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Node.java | 104 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Parameters.java | 72 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/Path.java | 102 | ||||
| -rw-r--r-- | instr-to-kodkod/cfg-to-paths/src/QuickParser.java | 58 |
7 files changed, 627 insertions, 0 deletions
diff --git a/instr-to-kodkod/cfg-to-paths/Makefile b/instr-to-kodkod/cfg-to-paths/Makefile new file mode 100644 index 0000000..c9d14be --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/Makefile @@ -0,0 +1,35 @@ +## Target(s) Configuration ##################################################### +MODEL_FILES = $(wildcard ../ast-to-instr/cfg_*.mod) +OUTPUT_FILES = $(patsubst ../ast-to-instr/%.mod,%.cfg.mod,$(MODEL_FILES)) + +## Executables ################################################################# +JAVAC = javac +JAVA = java + +## Java Config ################################################################# +CLASSPATH = "./src/" + +## Makefile Magic ############################################################## +SOURCES = $(wildcard src/*.java) +CLASSES = $(SOURCES:.java=.class) + +## Makefile Rules ############################################################## + +all: $(CLASSES) $(OUTPUT_FILES) + +clean: + rm -f $(CLASSES) + rm -f *.mod + +#run: $(CLASSES) +# $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) $(ROOT_NODE) $(ID_PREFIX) \ +# $(OUTPUT_FILE) + +%.class: %.java + $(JAVAC) -cp $(CLASSPATH) $< + +PATTERN = 's/\(is_start_node ([0-9]+).*/\1/p' + +%.cfg.mod: ../ast-to-instr/%.mod $(CLASSES) + $(eval ROOT_NODE := $(shell cat $< | grep 'is_start_node' | sed -En $(PATTERN))) + $(JAVA) -cp $(CLASSPATH) Main $< $(ROOT_NODE) "p$(ROOT_NODE)_" $@ diff --git a/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java new file mode 100644 index 0000000..93d20ba --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java @@ -0,0 +1,142 @@ +import java.io.*; + +public class ControlFlow +{ + public static boolean load_file + ( + final String filename + ) + throws FileNotFoundException + { + final QuickParser qp; + String[] input; + boolean success; + + qp = new QuickParser(filename); + + for (;;) + { + try + { + input = qp.parse_line(); + + if (input == null) + { + qp.finalize(); + + return false; + } + else if (input.length == 0) + { + qp.finalize(); + + break; + } + } + catch (final IOException e) + { + System.err.println + ( + "[E] IO error while parsing file \"" + + filename + + "\":" + /* FIXME: can be null */ + + e.getMessage() + ); + + return false; + } + + if (input[0].equals("add_element")) + { + success = handle_add_element(input); + } + else if (input[0].equals("node_connect")) + { + success = handle_add_connect_to(input); + } + else if (input[0].equals("is_terminal")) + { + success = handle_is_terminal(input); + } + else + { + continue; + } + + if (!success) + { + System.err.println + ( + "[E] An erroneous instruction was found in file \"" + + filename + + "\"." + ); + + try + { + qp.finalize(); + } + catch (final Exception e) + { + System.err.println("[E] Additionally:"); + e.printStackTrace(); + } + + return false; + } + } + + return true; + } + + private static boolean handle_add_element + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + if (!input[1].equals("node")) + { + return true; + } + + Node.handle_add_node(input[2]); + + return true; + } + + private static boolean handle_is_terminal + ( + final String[] input + ) + { + if (input.length != 2) + { + return false; + } + + Node.handle_is_terminal(input[1]); + + return true; + } + + private static boolean handle_add_connect_to + ( + final String[] input + ) + { + if ((input.length != 3)) + { + return false; + } + + return Node.handle_connect_to(input[1], input[2]); + } + + private ControlFlow () {} /* Utility Class */ +} diff --git a/instr-to-kodkod/cfg-to-paths/src/Main.java b/instr-to-kodkod/cfg-to-paths/src/Main.java new file mode 100644 index 0000000..d5cc650 --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/Main.java @@ -0,0 +1,114 @@ +/* FIXME: Finer imports */ +import java.util.*; + +import java.io.*; + +public class Main +{ + private static Parameters PARAMETERS; + private static int path_counter = 0; + + public static void main (final String... args) + { + final FileWriter output; + final Collection<Path> all_paths; + final Collection<List<Node>> all_subpaths; + + PARAMETERS = new Parameters(args); + + if (!PARAMETERS.are_valid()) + { + return; + } + + try + { + ControlFlow.load_file(PARAMETERS.get_model_file()); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not load model file \"" + + PARAMETERS.get_model_file() + + "\":" + ); + + e.printStackTrace(); + + return; + } + + all_paths = Path.get_all_paths_from(PARAMETERS.get_root_node()); + + all_subpaths = new ArrayList<List<Node>>(); + + for (final Path p: all_paths) + { + all_subpaths.addAll(p.get_all_subpaths()); + } + + try + { + output = new FileWriter(PARAMETERS.get_output_file()); + + for (final List<Node> tuple: all_subpaths) + { + node_tuple_to_predicates(tuple, output); + } + + output.close(); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not write to output file \"" + + PARAMETERS.get_model_file() + + "\":" + ); + + e.printStackTrace(); + + return; + } + } + + private static void node_tuple_to_predicates + ( + final List<Node> tuple, + final FileWriter out + ) + throws IOException + { + final String id; + final int tuple_size; + + tuple_size = tuple.size(); + + id = (PARAMETERS.get_id_prefix() + path_counter); + path_counter += 1; + + out.write("(add_element path " + id + ")\n"); + out.write("(is_path_of " + id + " " + tuple.get(0) + ")\n"); + + for (int i = 0; i < tuple_size; ++i) + { + out.write("(contains_node " + id + " " + tuple.get(i) + ")\n"); + + for (int j = (i + 1); j < tuple_size; ++j) + { + out.write + ( + "(is_before " + + id + + " " + + tuple.get(i) + + " " + + tuple.get(j) + + ")\n" + ); + } + } + } +} diff --git a/instr-to-kodkod/cfg-to-paths/src/Node.java b/instr-to-kodkod/cfg-to-paths/src/Node.java new file mode 100644 index 0000000..3b6f2c1 --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/Node.java @@ -0,0 +1,104 @@ +import java.util.*; + +public class Node +{ + /** Static *****************************************************************/ + private static final Map<String, Node> NODE_FROM_STRING; + + static + { + NODE_FROM_STRING = new HashMap<String, Node>(); + } + + public static Node get_node (final String s) + { + return NODE_FROM_STRING.get(s); + } + + public static boolean handle_add_node (final String a) + { + if (!NODE_FROM_STRING.containsKey(a)) + { + NODE_FROM_STRING.put(a, new Node(a)); + } + + return true; + } + + public static boolean handle_is_terminal (final String a) + { + Node n; + + n = NODE_FROM_STRING.get(a); + + if (n == (Node) null) + { + n = new Node(a); + + NODE_FROM_STRING.put(a, n); + } + + n.set_as_terminal(); + + return true; + } + + public static boolean handle_connect_to (final String a, final String b) + { + final Node n_a, n_b; + + 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; + } + + /** Non-Static *************************************************************/ + private final Collection<Node> next_nodes; + private final String name; + private boolean is_terminal; + + private Node (final String name) + { + this.name = name; + + next_nodes = new ArrayList<Node>(); + is_terminal = false; + } + + private void set_as_terminal () + { + is_terminal = true; + } + + public Collection<Node> next_nodes () + { + return next_nodes; + } + + public boolean is_terminal () + { + return is_terminal; + } + + @Override + public String toString () + { + return name; + } +} diff --git a/instr-to-kodkod/cfg-to-paths/src/Parameters.java b/instr-to-kodkod/cfg-to-paths/src/Parameters.java new file mode 100644 index 0000000..91303d2 --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/Parameters.java @@ -0,0 +1,72 @@ +public class Parameters +{ + 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 () + { + System.out.println + ( + "Instr-to-kodkod\n" + + "USAGE:\n" + + "\tjava Main <INSTRUCTIONS> <ROOT_NODE> <ID_PREFIX> <OUTPUT_FILE>\n" + + "PARAMETERS:\n" + + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n" + + "\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 (final String... args) + { + if (args.length != 4) + { + print_usage(); + + model_file = new String(); + root_node = new String(); + id_prefix = new String(); + output_file = new String(); + + are_valid = false; + } + else + { + model_file = args[0]; + root_node = args[1]; + id_prefix = args[2]; + output_file = args[3]; + are_valid = true; + } + } + + public String get_model_file () + { + return model_file; + } + + public String get_root_node () + { + return root_node; + } + + public String get_id_prefix () + { + return id_prefix; + } + + public String get_output_file () + { + return output_file; + } + + public boolean are_valid () + { + return are_valid; + } +} diff --git a/instr-to-kodkod/cfg-to-paths/src/Path.java b/instr-to-kodkod/cfg-to-paths/src/Path.java new file mode 100644 index 0000000..9e0897f --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/Path.java @@ -0,0 +1,102 @@ +import java.util.*; + +public class Path +{ + private final ArrayList<Node> nodes; + private final Node last_node; + + public static Collection<Path> get_all_paths_from (final String root) + { + 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>(); + + waiting_list.push((new Path(Node.get_node(root)))); + + while (!waiting_list.empty()) + { + final Path current_path; + final Node current_node; + final Collection<Node> next_nodes; + + current_path = waiting_list.pop(); + current_node = current_path.last_node; + next_nodes = current_node.next_nodes(); + + if (next_nodes.isEmpty()) + { + result.add(current_path); + } + else + { + if (current_node.is_terminal()) + { + result.add(current_path); + } + for (final Node next: next_nodes) + { + waiting_list.push(current_path.add_step(next)); + } + } + } + + return result; + } + + private Path (final Node start) + { + nodes = new ArrayList<Node>(); + + nodes.add(start); + + last_node = start; + } + + private Path (final ArrayList<Node> nodes, final Node last_node) + { + this.nodes = nodes; + this.last_node = last_node; + + this.nodes.add(last_node); + } + + @SuppressWarnings("unchecked") + /* 'nodes' is an ArrayList<Node>, and so should be its clone. */ + private Path add_step (final Node n) + { + return new Path((ArrayList<Node>) nodes.clone(), n); + } + + public Collection<List<Node>> get_all_subpaths () + { + final Collection<List<Node>> result; + final int path_length; + + result = new ArrayList<List<Node>>(); + path_length = nodes.size(); + + for (int i = 0; i < path_length; ++i) + { + result.add(nodes.subList(i, path_length)); + } + + return result; + } +} diff --git a/instr-to-kodkod/cfg-to-paths/src/QuickParser.java b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java new file mode 100644 index 0000000..47cea27 --- /dev/null +++ b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java @@ -0,0 +1,58 @@ +/* FIXME: Finer imports */ +import java.io.*; +import java.util.regex.*; +import java.util.*; + +public class QuickParser +{ + private static final Pattern instr_pattern; + private final BufferedReader buffered_reader; + + static + { + instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)"); + } + public QuickParser (final String filename) + throws FileNotFoundException + { + buffered_reader = new BufferedReader(new FileReader(filename)); + } + + public void finalize () + throws IOException + { + buffered_reader.close(); + } + + public String[] parse_line () + throws IOException + { + final List<String> result; + final Matcher matcher; + String line; + + do + { + line = buffered_reader.readLine(); + + if (line == null) + { + return new String[0]; + } + + line = line.replaceAll("\\s+"," "); + } + while (line.length() < 3 || line.startsWith(";")); + + matcher = instr_pattern.matcher(line); + + if (!matcher.find()) + { + System.err.println("[E] Invalid instruction \"" + line + "\""); + + return null; + } + + return matcher.group(1).split(" |\t"); + } +} |