Initial commit.

6 files changed, 803 insertions, 0 deletions

diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
new file mode 100644
index 0000000..d692ecd
--- /dev/null
+++ b/instr-to-kodkod/src/Main.java
@@ -0,0 +1,82 @@
+/* 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 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;
+
+      if (args.length != 1)
+      {
+         System.out.println("Use: java Main <instructions_file>");
+
+         return;
+      }
+
+      model = new VHDLModel();
+
+      try
+      {
+         VHDLLevel.add_to_model(model, "./structural_level.data");
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[E] Could not load structural level:");
+         e.printStackTrace();
+
+         return;
+      }
+
+      try
+      {
+         model.parse_file(args[0]);
+      }
+      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/instr-to-kodkod/src/QuickParser.java b/instr-to-kodkod/src/QuickParser.java
new file mode 100644
index 0000000..47cea27
--- /dev/null
+++ b/instr-to-kodkod/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/instr-to-kodkod/src/VHDLLevel.java b/instr-to-kodkod/src/VHDLLevel.java
new file mode 100644
index 0000000..738adaf
--- /dev/null
+++ b/instr-to-kodkod/src/VHDLLevel.java
@@ -0,0 +1,157 @@
+/* FIXME: Finer imports */
+import java.util.*;
+
+import java.io.*;
+
+public class VHDLLevel
+{
+   /* Utility Class */
+   private VHDLLevel () {}
+
+   public static boolean add_to_model
+   (
+      final VHDLModel m,
+      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_type"))
+         {
+            success = handle_add_type(input, m);
+         }
+         else if (input[0].equals("add_predicate"))
+         {
+            success = handle_add_predicate(input, m);
+         }
+         else
+         {
+            System.err.println
+            (
+               "[E] Unknown instruction type \""
+               + input[0]
+               + "\"  in file \""
+               + filename
+               + "\"."
+            );
+
+            return false;
+         }
+
+         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_type
+   (
+      final String[] cmd,
+      final VHDLModel m
+   )
+   {
+      if (cmd.length != 2)
+      {
+         System.err.println
+         (
+            "[E] Badly formed \"add_type\" instruction: \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      m.add_type(cmd[1]);
+
+      return true;
+   }
+
+   private static boolean handle_add_predicate
+   (
+      final String[] cmd,
+      final VHDLModel m
+   )
+   {
+      final String[] signature;
+
+      if (cmd.length < 2)
+      {
+         System.err.println
+         (
+            "[E] Badly formed \"add_predicate\" instruction: \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      signature = new String[cmd.length - 2];
+
+      for (int i = 2; i < cmd.length; ++i)
+      {
+         signature[i - 2] = cmd[i];
+      }
+
+      return m.add_predicate(cmd[1], signature);
+   }
+}
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
new file mode 100644
index 0000000..bdb5e4b
--- /dev/null
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -0,0 +1,336 @@
+/* FIXME: Finer imports */
+import java.util.*;
+
+import java.io.*;
+
+import kodkod.ast.*;
+import kodkod.instance.*;
+
+public class VHDLModel
+{
+   private final Map<String, VHDLType> types;
+   private final Map<String, VHDLPredicate> predicates;
+
+   public VHDLModel ()
+   {
+      types = new HashMap<String, VHDLType>();
+      predicates = new HashMap<String, VHDLPredicate>();
+   }
+
+   public void add_type (final String name)
+   {
+      if (!types.containsKey(name))
+      {
+         types.put(name, new VHDLType(name));
+      }
+   }
+
+   public boolean add_predicate (final String name, final String[] signature)
+   {
+      final VHDLPredicate p;
+      final VHDLType[] true_signature;
+
+      true_signature = new VHDLType[signature.length];
+
+      for (int i = 0; i < signature.length; ++i)
+      {
+         true_signature[i] = types.get(signature[i]);
+
+         if (true_signature[i] == null)
+         {
+            System.err.println
+            (
+               "[E] The predicate \""
+               + name
+               + "\" uses an unknown type \""
+               + signature[i]
+               + "\""
+            );
+
+            return false;
+         }
+      }
+
+      p = predicates.get(name);
+
+      if (p == null)
+      {
+         predicates.put(name, new VHDLPredicate(name, true_signature));
+      }
+      else
+      {
+         return p.add_signature(true_signature);
+      }
+
+      return true;
+   }
+
+   public boolean parse_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("set_function"))
+         {
+            success = handle_set_function(input);
+         }
+         else
+         {
+            success = handle_predicate(input);
+         }
+
+         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 boolean handle_add_element (final String... cmd)
+   {
+      final VHDLType t;
+
+      if (cmd.length != 3)
+      {
+         System.err.println
+         (
+            "[E] Badly formed \"add_element\" instruction: \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      t = types.get(cmd[1]);
+
+      if (t == null)
+      {
+         System.err.println
+         (
+            "[E] Instruction to add element to unknown type \""
+            + cmd[1]
+            + "\": \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      t.add_member(cmd[2]);
+
+      return true;
+   }
+
+   private boolean handle_set_function (final String... cmd)
+   {
+      if (cmd.length != 4)
+      {
+         System.err.println
+         (
+            "[E] Badly formed \"set_function\" instruction: \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      /*
+      System.err.println
+      (
+         "[W] \"set_function\" instructions are ignored."
+      );
+      */
+
+      return true;
+   }
+
+   private boolean handle_predicate (final String... cmd)
+   {
+      final VHDLPredicate p;
+      final String[] params;
+
+      params = new String[cmd.length - 1];
+
+      p = predicates.get(cmd[0]);
+
+      if (p == null)
+      {
+         System.err.println
+         (
+            "[E] Instruction with an unknown predicate (\""
+            + cmd[0]
+            + "\"): \""
+            + String.join(" ", cmd)
+            + "\"."
+         );
+
+         return false;
+      }
+
+      if (params.length != p.get_arity())
+      {
+         System.err.println
+         (
+            "[E] Predicate \""
+            + cmd[0]
+            + "\" is of arity "
+            + p.get_arity()
+            + ", making the instruction: \""
+            + String.join(" ", cmd)
+            + "\" invalid."
+         );
+
+         return false;
+      }
+
+      for (int i = 0; i < params.length; ++i)
+      {
+         /* TODO: check if the IDs are registered in the corresponding type. */
+         params[i] = cmd[i + 1];
+
+         if (!p.accepts_as_nth_param(i, params[i]))
+         {
+            System.err.println
+            (
+               "[E] The predicate \""
+               + p.get_name()
+               + "\" has no signature allowing the element \""
+               + params[i]
+               + "\" as "
+               + i
+               + "th parameter, making the instruction: \""
+               + String.join(" ", cmd)
+               + "\" invalid."
+            );
+
+            return false;
+         }
+      }
+
+      p.add_member(params);
+
+      return true;
+   }
+
+   public Collection<String> get_atoms ()
+   {
+      final Collection<String> result;
+
+      result = new ArrayList<String>();
+
+      for (final VHDLType t: types.values())
+      {
+         result.addAll(t.get_all_members_as_atoms());
+      }
+
+      return result;
+   }
+
+   public void add_to_bounds (final Bounds b, final TupleFactory f)
+   {
+      for (final VHDLType t: types.values())
+      {
+         t.add_to_bounds(b, f);
+      }
+
+      for (final VHDLPredicate p: predicates.values())
+      {
+         p.add_to_bounds(b, f);
+      }
+   }
+
+   public Relation get_predicate_as_relation (final String name)
+   {
+      final VHDLPredicate p;
+
+      p = predicates.get(name);
+
+      if (p == null)
+      {
+         return null;
+      }
+      else
+      {
+         return p.get_as_relation();
+      }
+   }
+
+   public Relation get_type_as_relation (final String name)
+   {
+      final VHDLType t;
+
+      t = types.get(name);
+
+      if (t == null)
+      {
+         return null;
+      }
+      else
+      {
+         return t.get_as_relation();
+      }
+   }
+}
diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java
new file mode 100644
index 0000000..a94e5ec
--- /dev/null
+++ b/instr-to-kodkod/src/VHDLPredicate.java
@@ -0,0 +1,94 @@
+/* FIXME: Finer imports */
+import java.util.*;
+
+import kodkod.ast.*;
+import kodkod.ast.operator.*;
+
+import kodkod.instance.*;
+
+
+public class VHDLPredicate
+{
+   private final Collection<VHDLType[]> signatures;
+   private final Collection<String[]> members;
+   private final String name;
+   private final int arity;
+   private final Relation as_relation;
+
+   public VHDLPredicate (final String name, final VHDLType[] signature)
+   {
+      this.name = name;
+      arity = signature.length;
+
+      signatures = new ArrayList<VHDLType[]>();
+      members = new ArrayList<String[]>();
+
+      as_relation = Relation.nary(name, arity);
+
+      signatures.add(signature);
+   }
+
+   public void add_member (final String[] tuple)
+   {
+      members.add(tuple);
+   }
+
+   public int get_arity ()
+   {
+      return arity;
+   }
+
+   public Relation get_as_relation ()
+   {
+      return as_relation;
+   }
+
+   /* pre: i < get_arity() */
+   public boolean accepts_as_nth_param (final int i, final String id)
+   {
+      for (VHDLType[] sig: signatures)
+      {
+         if (sig[i].get_member_as_relation(id) != null)
+         {
+            return true;
+         }
+      }
+
+      return false;
+   }
+
+   public boolean add_signature (final VHDLType[] signature)
+   {
+      if (signature.length != get_arity())
+      {
+         return false;
+      }
+
+      signatures.add(signature);
+
+      return true;
+   }
+
+   public String get_name ()
+   {
+      return name;
+   }
+
+   public void add_to_bounds (final Bounds b, final TupleFactory f)
+   {
+      final TupleSet as_tuples;
+
+      /* Empty tuple set, will contain tuples of the right arity. */
+      as_tuples = f.noneOf(get_arity());
+
+      /* For every member of this predicate ... */
+      for (final Object[] ref: members)
+      {
+         /* add a new tuple to the tuple set representing the predicate. */
+         as_tuples.add(f.tuple(ref));
+      }
+
+      /* We now have the exact definition of the predicate as a relation */
+      b.boundExactly(as_relation, as_tuples);
+   }
+}
diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java
new file mode 100644
index 0000000..c4c1b0f
--- /dev/null
+++ b/instr-to-kodkod/src/VHDLType.java
@@ -0,0 +1,76 @@
+/* FIXME: Finer imports */
+import java.util.*;
+
+import kodkod.ast.*;
+import kodkod.ast.operator.*;
+
+import kodkod.instance.*;
+
+
+public class VHDLType
+{
+   private final Map<String, Relation> members;
+   private final String name;
+   private final Relation as_relation;
+
+   public VHDLType (final String name)
+   {
+      members = new HashMap<String, Relation>();
+
+      this.name = name;
+      as_relation = Relation.unary(name);
+   }
+
+   public void add_member (final String id)
+   {
+      members.put(id, Relation.unary(id));
+   }
+
+   public String get_name ()
+   {
+      return name;
+   }
+
+   public Relation get_as_relation ()
+   {
+      return as_relation;
+   }
+
+
+   public Relation get_member_as_relation (final String id)
+   {
+      return members.get(id);
+   }
+
+   public Collection<String> get_all_members_as_atoms ()
+   {
+      return members.keySet();
+   }
+
+   public Formula generate_declarations ()
+   {
+      Formula result;
+
+      result = Formula.TRUE;
+
+      return result;
+   }
+
+   public void add_to_bounds (final Bounds b, final TupleFactory f)
+   {
+      final Set<Map.Entry<String, Relation>> members_as_set;
+
+      members_as_set = members.entrySet();
+
+      for (final Map.Entry<String, Relation> member: members_as_set)
+      {
+         b.boundExactly(member.getValue(), f.setOf(member.getKey()));
+      }
+
+      /*
+       * the toArray() is required to avoid the collection being considered as
+       * a single atom.
+       */
+      b.boundExactly(as_relation, f.setOf(get_all_members_as_atoms().toArray()));
+   }
+}