summaryrefslogtreecommitdiff
path: root/instr-to-kodkod
diff options
context:
space:
mode:
Diffstat (limited to 'instr-to-kodkod')
-rw-r--r--instr-to-kodkod/Makefile138
-rw-r--r--instr-to-kodkod/cfg-to-paths/Makefile35
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/ControlFlow.java142
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/Main.java114
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/Node.java104
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/Parameters.java72
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/Path.java102
-rw-r--r--instr-to-kodkod/cfg-to-paths/src/QuickParser.java58
8 files changed, 728 insertions, 37 deletions
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 9823919..815c527 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,60 +1,124 @@
-## Target(s) Configuration #####################################################
-#MODEL_FILES = $(wildcard ../data/instructions/*.mod)
-MODEL_FILES = \
- ../ast-to-instr/structural.mod \
- ../ast-to-instr/depths.mod \
- $(wildcard ../ast-to-instr/cfg_*.mod) \
- $(wildcard ../cfg-to-paths/*.mod)
-MAP_FILES = $(wildcard ../ast-to-instr/*.map)
-LEVEL_DIR = $(wildcard ../data/level/*.lvl)
+## Parameters ##################################################################
+#### Where to find the level files
+ifndef LEVEL_FILES
+LEVEL_FILES =
+endif
-PROPERTIES = $(wildcard ../data/property/cnes/*.pro)
+#### Where to find the properties to verify
+ifndef PROPERTY_FILES
+PROPERTY_FILES =
+endif
-## Executables #################################################################
-JAVAC = javac
+#### Where to find the model
+ifndef MODEL_DIR
+MODEL_DIR =
+endif
+
+#### Where to store the CFG models
+ifndef CFG_MODEL_DIR
+CFG_MODEL_DIR = $(MODEL_DIR)/cfg/
+endif
+
+#### Where to output the solutions.
+ifndef SOL_DIR
+SOL_DIR =
+endif
+
+#### Where to get the missing Jar files.
+ifndef JAR_SOURCE
+JAR_SOURCE = "https://noot-noot.org/tabellion/jar/"
+endif
+
+#### Binaries
+###### JRE binary
+ifndef JAVA
JAVA = java
+endif
+
+###### JDK binary
+ifndef JAVAC
+JAVAC = javac
+endif
+
+##### Downloader
+ifndef DOWNLOADER
DOWNLOADER = wget
+endif
-## Java Config #################################################################
-CLASSPATH = "kodkod.jar:./src/:./parser/:org.sat4j.core.jar:antlr-4.7-complete.jar"
+## Parameters Sanity Check #####################################################
+ifeq ($(strip $(LEVEL_FILES)),)
+$(error No LEVEL_FILES defined as parameter.)
+endif
+
+ifeq ($(strip $(PROPERTY_FILES)),)
+$(error No PROPERTY_FILES defined as parameter.)
+endif
+
+ifeq ($(strip $(MODEL_DIR)),)
+$(error No MODEL_DIR defined as parameter.)
+endif
+
+ifeq ($(strip $(CFG_MODEL_DIR)),)
+$(error No CFG_MODEL_DIR defined as parameter.)
+endif
-## Dependencies ################################################################
-JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
+ifeq ($(strip $(SOL_DIR)),)
+$(error No SOL_DIR defined as parameter.)
+endif
+
+ifeq ($(strip $(JAR_SOURCE)),)
+$(error No JAR_SOURCE defined as parameter.)
+endif
+
+ifeq ($(strip $(JAVA)),)
+$(error No Java executable defined as parameter.)
+endif
+
+ifeq ($(strip $(JAVAC)),)
+$(error No Java compiler defined as parameter.)
+endif
+
+ifeq ($(strip $(DOWNLOADER)),)
+$(error No Java executable defined as parameter.)
+endif
+
+################################################################################
+CLASSPATH = "kodkod.jar:./src/:./parser/:org.sat4j.core.jar:antlr-4.7-complete.jar"
REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar
## Makefile Magic ##############################################################
-GLOBAL_INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(MAP_FILES)
-SOURCES = $(wildcard src/*.java parser/*.java)
-GRAMMARS = $(wildcard parser/*.g4)
+SOURCES = $(wildcard src/*.java)
CLASSES = $(SOURCES:.java=.class)
-SOLUTIONS = $(PROPERTIES:.pro=.sol)
+SOLUTION_FILES = $(addprefix $(SOL_DIR)/,$(notdir $(PROPERTY_FILES:.pro=.sol)))
+MODEL_FILES = \
+ $(MODEL_DIR)/structural.mod \
+ $(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/*.mod))
+export
## Makefile Rules ##############################################################
-run: $(SOLUTIONS)
+run: cfg-generator parser $(SOLUTION_FILES)
+
+cfg-generator:
+ $(MAKE) -C cfg-to-paths
-all: parser/PropertyParser.java $(CLASSES)
+parser: antlr-4.7-complete.jar
$(MAKE) -C parser
- $(MAKE) -C ../ast-to-instr
- $(MAKE) -C ../cfg-to-paths
clean:
- rm -f $(CLASSES)
$(MAKE) -C parser clean
- $(MAKE) -C ../ast-to-instr clean
- $(MAKE) -C ../cfg-to-paths clean
+ $(MAKE) -C cfg-to-paths clean
+ rm -f $(CLASSES)
-%.sol: %.pro parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS)
- echo "Solving \"$<\"..."
- $(MAKE) -C ../ast-to-instr
- $(MAKE) -C ../cfg-to-paths
- $(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES) -v
+%.sol: cfg-generator parser $(CLASSES) $(PROPERTY_FILES) $(MODEL_FILES) $(LEVEL_FILES)
+ $(JAVA) -cp $(CLASSPATH) Main $@ \
+ $(filter %$(basename $(notdir $@)).pro,$(PROPERTY_FILES)) \
+ $(LEVEL_FILES) \
+ $(MODEL_FILES)
+ -v
-%.class: %.java $(REQUIRED_JARS) parser/PropertyParser.java
+%.class: %.java $(REQUIRED_JARS) parser
$(JAVAC) -cp $(CLASSPATH) $<
%.jar:
- echo "Attempting to download missing jar '$@'"
+ echo "Attempting to download missing jar '$@'..."
$(DOWNLOADER) "$(JAR_SOURCE)/$@"
-
-parser/PropertyParser.java: antlr-4.7-complete.jar $(GRAMMAR)
- $(MAKE) -C parser
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");
+ }
+}