| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/src/VHDLModel.java')
| -rw-r--r-- | instr-to-kodkod/src/VHDLModel.java | 336 |
1 files changed, 336 insertions, 0 deletions
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(); + } + } +} |