Working on a way to CTL over DAG in Kodkod.

10 files changed, 543 insertions, 12 deletions

diff --git a/cfg-to-paths/Makefile b/cfg-to-paths/Makefile
new file mode 100644
index 0000000..6db785e
--- /dev/null
+++ b/cfg-to-paths/Makefile
@@ -0,0 +1,36 @@
+## Target(s) Configuration #####################################################
+MODEL_FILE = "../data/instructions/example_1.sl"
+LEVEL_DIR = "../data/level/"
+## 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
+
+## Makefile Magic ##############################################################
+SOURCES = $(wildcard src/*.java)
+CLASSES = $(SOURCES:.java=.class)
+
+## Makefile Rules ##############################################################
+
+all: $(CLASSES)
+
+clean:
+	rm -f $(CLASSES)
+
+run: $(CLASSES) $(REQUIRED_JARS)
+	$(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE)
+
+%.class: %.java $(REQUIRED_JARS)
+	$(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
new file mode 100644
index 0000000..629ac49
--- /dev/null
+++ b/cfg-to-paths/src/ControlFlow.java
@@ -0,0 +1,121 @@
+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("connect_to"))
+         {
+            success = handle_add_connect_to(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] != "node")
+      {
+         return true;
+      }
+
+      Node.handle_add_node(input[2]);
+
+      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]);
+   }
+}
diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
new file mode 100644
index 0000000..ec55450
--- /dev/null
+++ b/cfg-to-paths/src/Main.java
@@ -0,0 +1,91 @@
+/* FIXME: Finer imports */
+import kodkod.ast.*;
+
+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;
+
+      PARAMETERS = new Parameters(args);
+
+      if (!PARAMETERS.are_valid())
+      {
+         return;
+      }
+
+      model = new VHDLModel();
+
+      try
+      {
+         VHDLLevel.add_to_model
+         (
+            model,
+            (
+               PARAMETERS.get_levels_directory()
+               + "/structural_level.data"
+            )
+         );
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load structural level:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      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);
+
+      solver = new Solver();
+      solver.options().setSolver(SATFactory.DefaultSAT4J);
+      solver.options().setReporter(new ConsoleReporter());
+
+      sol = solver.solve(get_formula(model), bounds);
+
+      System.out.println(sol);
+   }
+}
diff --git a/cfg-to-paths/src/Node.java b/cfg-to-paths/src/Node.java
new file mode 100644
index 0000000..6f9083d
--- /dev/null
+++ b/cfg-to-paths/src/Node.java
@@ -0,0 +1,58 @@
+import java.util.*;
+
+public class Node
+{
+   private static final Map<String, Node> NODE_FROM_STRING;
+   private final Collection<Node> next_nodes;
+
+   private final String name;
+
+   static
+   {
+      NODE_FROM_STRING = new HashMap<String, Node>();
+   }
+
+   private Node (final String name)
+   {
+      this.name = name;
+      next_nodes = new ArrayList<Node>();
+   }
+
+   public Collection<Node> next_nodes ()
+   {
+      return next_nodes;
+   }
+
+   @Override
+   public String toString ()
+   {
+      return name;
+   }
+
+   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_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);
+
+      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
new file mode 100644
index 0000000..8d0331b
--- /dev/null
+++ b/cfg-to-paths/src/Parameters.java
@@ -0,0 +1,55 @@
+public class Parameters
+{
+   private final String levels_dir;
+   private final String model_file;
+   private final boolean are_valid;
+
+   public static void print_usage ()
+   {
+      System.out.println
+      (
+         "Instr-to-kodkod\n"
+         + "USAGE:\n"
+         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS>\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)."
+      );
+   }
+
+   public Parameters (String... args)
+   {
+      if (args.length != 2)
+      {
+         print_usage();
+
+         levels_dir = new String();
+         model_file = new String();
+         are_valid = false;
+      }
+      else
+      {
+         levels_dir = args[0];
+         model_file = args[1];
+         are_valid = true;
+      }
+   }
+
+   public String get_levels_directory ()
+   {
+      return levels_dir;
+   }
+
+   public String get_model_file ()
+   {
+      return model_file;
+   }
+
+   public boolean are_valid ()
+   {
+      return are_valid;
+   }
+}
diff --git a/cfg-to-paths/src/Path.java b/cfg-to-paths/src/Path.java
new file mode 100644
index 0000000..80b433f
--- /dev/null
+++ b/cfg-to-paths/src/Path.java
@@ -0,0 +1,81 @@
+import java.util.*;
+
+public class Path
+{
+   private final ArrayList<Node> nodes;
+   private final Node last_node;
+
+   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);
+   }
+
+   private Path add_step (final Node n)
+   {
+      return new Path((ArrayList<Node>) nodes.clone(), n);
+   }
+
+   public static Collection<Path> get_all_paths_from (final String root)
+   {
+      final Collection<Path> result;
+      final Stack<Path> waiting_list;
+
+      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
+         {
+            for (final Node next: next_nodes)
+            {
+               waiting_list.push(current_path.add_step(next));
+            }
+         }
+      }
+
+      return result;
+   }
+
+   public static Collection<List<Node>> get_subpaths (final Path p)
+   {
+      final Collection<List<Node>> result;
+      final int path_length;
+
+      result = new ArrayList<List<Node>>();
+      path_length = p.nodes.size();
+
+      for (int i = 0; i < path_length; ++i)
+      {
+         result.add(p.nodes.subList(i, path_length));
+      }
+
+      return result;
+   }
+}
diff --git a/cfg-to-paths/src/QuickParser.java b/cfg-to-paths/src/QuickParser.java
new file mode 100644
index 0000000..47cea27
--- /dev/null
+++ b/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");
+   }
+}
diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.data
new file mode 100644
index 0000000..a880606
--- /dev/null
+++ b/data/level/control_flow_level.data
@@ -0,0 +1,18 @@
+;; Control Flow Level
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(add_type node)
+(add_type node_depth)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_predicate has_kind node string)
+(add_predicate has_option node string)
+(add_predicate has_depth node node_depth)
+(add_predicate node_connect node node)
+(add_predicate expr_writes node waveform)
+(add_predicate expr_reads node waveform)
diff --git a/data/level/control_flow_level_kodkod.data b/data/level/control_flow_level_kodkod.data
new file mode 100644
index 0000000..987b63e
--- /dev/null
+++ b/data/level/control_flow_level_kodkod.data
@@ -0,0 +1,13 @@
+;; Control Flow Level, Kodkod additions
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(add_type path)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+(add_predicate is_path_of path node)
+(add_predicate contains_node path node)
diff --git a/instr-scripts/process_internals.py b/instr-scripts/process_internals.py
index e323300..a58fc5a 100644
--- a/instr-scripts/process_internals.py
+++ b/instr-scripts/process_internals.py
@@ -128,7 +128,7 @@ class Process_Internals:
             xml.attrib.get("label")
         )
         self.output.write(
-            "(set_attribute label "
+            "(set_function label "
             + cond_node_id
             + " "
             + string_id
@@ -145,7 +145,7 @@ class Process_Internals:
             "IF"
         )
         self.output.write(
-            "(set_attribute kind "
+            "(set_function kind "
             + cond_node_id
             + " "
             + string_id
@@ -165,7 +165,7 @@ class Process_Internals:
 
         #### Depth
         self.output.write(
-            "(set_attribute depth "
+            "(set_function depth "
             + cond_node_id
             + " "
             + str(node_depth + 1)
@@ -223,7 +223,7 @@ class Process_Internals:
             xml.attrib.get("label")
         )
         self.output.write(
-            "(set_attribute label "
+            "(set_function label "
             + node_id
             + " "
             + string_id
@@ -240,7 +240,7 @@ class Process_Internals:
             "INSTRUCTION"
         )
         self.output.write(
-            "(set_attribute kind "
+            "(set_function kind "
             + node_id
             + " "
             + string_id
@@ -260,7 +260,7 @@ class Process_Internals:
 
         #### Depth
         self.output.write(
-            "(set_attribute depth "
+            "(set_function depth "
             + node_id
             + " "
             + str(node_depth)
@@ -339,7 +339,7 @@ class Process_Internals:
             xml.attrib.get("label")
         )
         self.output.write(
-            "(set_attribute label "
+            "(set_function label "
             + cond_node_id
             + " "
             + string_id
@@ -356,7 +356,7 @@ class Process_Internals:
             "CASE"
         )
         self.output.write(
-            "(set_attribute kind "
+            "(set_function kind "
             + cond_node_id
             + " "
             + string_id
@@ -376,7 +376,7 @@ class Process_Internals:
 
         #### Depth
         self.output.write(
-            "(set_attribute depth "
+            "(set_function depth "
             + cond_node_id
             + " "
             + str(node_depth + 1)
@@ -458,7 +458,7 @@ class Process_Internals:
             ""
         )
         self.output.write(
-            "(set_attribute label "
+            "(set_function label "
             + node_id
             + " "
             + string_id
@@ -475,7 +475,7 @@ class Process_Internals:
             "WHEN"
         )
         self.output.write(
-            "(set_attribute kind "
+            "(set_function kind "
             + node_id
             + " "
             + string_id
@@ -495,7 +495,7 @@ class Process_Internals:
 
         #### Depth
         self.output.write(
-            "(set_attribute depth "
+            "(set_function depth "
             + node_id
             + " "
             + str(node_depth)