| summaryrefslogtreecommitdiff |
diff options
Diffstat (limited to 'instr-to-kodkod/src')
| -rw-r--r-- | instr-to-kodkod/src/Main.java | 118 | ||||
| -rw-r--r-- | instr-to-kodkod/src/Parameters.java | 114 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLProperty.java | 31 |
3 files changed, 209 insertions, 54 deletions
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java index 41b8ef8..0b1d2e4 100644 --- a/instr-to-kodkod/src/Main.java +++ b/instr-to-kodkod/src/Main.java @@ -6,6 +6,9 @@ import kodkod.engine.config.*; import kodkod.engine.satlab.*; import kodkod.instance.*; + +import java.io.IOException; + public class Main { private static Parameters PARAMETERS; @@ -22,17 +25,80 @@ public class Main return VARIABLE_MANAGER; } - private static Formula get_formula (final VHDLModel model) + private static boolean load_levels () + { + for (final String lvl: PARAMETERS.get_level_files()) + { + try + { + VHDLLevel.add_to_model(MODEL, lvl); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not load level file \"" + + lvl + + "\":" + ); + + e.printStackTrace(); + + return false; + } + } + + return true; + } + + private static Formula load_property () { - final Variable w; + final VHDLProperty pro; - w = Variable.unary("w"); + pro = new VHDLProperty(PARAMETERS.get_property_file()); - return - w.join + try + { + return pro.generate_formula(); + } + catch (final IOException e) + { + System.err.println ( - model.get_predicate_as_relation("is_accessed_by") - ).no().forSome(w.oneOf(model.get_type_as_relation("waveform"))); + "[E] Could not load property file \"" + + PARAMETERS.get_property_file() + + "\":" + ); + e.printStackTrace(); + + return null; + } + } + + private static boolean load_models () + { + for (final String mod: PARAMETERS.get_model_files()) + { + try + { + MODEL.parse_file(mod); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not load instructions from file \"" + + mod + + "\":" + ); + + e.printStackTrace(); + + return false; + } + } + + return true; } public static void main (final String... args) @@ -65,42 +131,26 @@ public class Main MODEL = new VHDLModel(); /* 1/ Load Levels (Types + predicates) */ - try + if (!load_levels()) { - VHDLLevel.add_to_model - ( - MODEL, - ( - PARAMETERS.get_levels_directory() - + "/structural_level.data" - ) - ); + return; } - catch (final Exception e) - { - System.err.println("[E] Could not load structural level:"); - e.printStackTrace(); + /* 2/ Load Properties (will change 'is_used()' on predicates) */ + /* FIXME? Currently only one property, due to the 'is_used' */ + property = load_property(); + + if (property == null) + { return; } - /* 2/ Load Properties (will change 'is_used()' on predicates) */ - property = get_formula(MODEL); - /* TODO */ - - /* 3/ Generate complementary model according to used predicates. */ - /* TODO */ + /* 3/ Generate complementary model according to used predicates. */ + /* TODO */ /* 4/ Load Model, but only for used predicates and types. */ - try - { - MODEL.parse_file(PARAMETERS.get_model_file()); - } - catch (final Exception e) + if (!load_models()) { - System.err.println("[E] Could not load instructions:"); - e.printStackTrace(); - return; } diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java index 1face97..749f0fe 100644 --- a/instr-to-kodkod/src/Parameters.java +++ b/instr-to-kodkod/src/Parameters.java @@ -1,8 +1,13 @@ +import java.util.List; +import java.util.ArrayList; + public class Parameters { - private final String levels_dir; - private final String model_file; + private final List<String> level_files; + private final List<String> model_files; + private final String property_file; private final String var_prefix; + private final boolean are_valid; public static void print_usage () @@ -11,45 +16,114 @@ public class Parameters ( "Instr-to-kodkod\n" + "USAGE:\n" - + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS> <VAR_PREFIX>\n" + + "\tjava Main <VAR_PREFIX> <FILES>+\n" + "PARAMETERS:\n" - + "\t<LEVELS_DIR>\tDirectory containing the level definitions.\n" - + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n" - + "\t<VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n" + + "\t- <VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n" + + "\t- <FILES>\tList of files to be loaded.\n" + "NOTES:\n" - + "\tThe properties to be verified still have to be hand coded in the" - + " source files (in Main.java)." + + "\t- One, single, property file MUST be in <FILES>.\n" + + "\t- Property files have a \".pro\" extension.\n" + + "\t- Model files have a \".mod\" extension.\n" + + "\t- Level files have a \".lvl\" extension.\n" + + "\t- The files may be given in any order." ); } public Parameters (String... args) { - if (args.length != 3) + boolean has_pro_file, has_error; + String prop_file; + + level_files = new ArrayList<String>(); + model_files = new ArrayList<String>(); + + if (args.length < 2) { print_usage(); - levels_dir = new String(); - model_file = new String(); + property_file = new String(); var_prefix = new String(); + are_valid = false; + + return; + } + + has_pro_file = false; + has_error = false; + + var_prefix = args[1]; + prop_file = new String(); + + for (int i = 2; i < args.length; ++i) + { + if (args[i].endsWith(".lvl")) + { + level_files.add(args[i]); + } + else if (args[i].endsWith(".mod")) + { + model_files.add(args[i]); + } + else if (args[i].endsWith(".lvl")) + { + if (has_pro_file) + { + System.err.println + ( + "[E] Both files \"" + + prop_file + + "\" and \"." + + args[i] + + "\" contain a property. Only one can be used at a time." + ); + + has_error = true; + } + else + { + has_pro_file = true; + prop_file = args[i]; + } + } + else + { + System.err.println + ( + "[E] Unknown file type \"" + + args[i] + + "\"." + ); + + has_error = true; + } } - else + + property_file = prop_file; + + if (!has_pro_file) { - levels_dir = args[0]; - model_file = args[1]; - var_prefix = args[2]; - are_valid = true; + System.err.println("[E] There was no property file."); + + has_error = true; } + + are_valid = has_error; + } + + public List<String> get_level_files () + { + return level_files; } - public String get_levels_directory () + public List<String> get_model_files () { - return levels_dir; + return model_files; } - public String get_model_file () + public String get_property_file () { - return model_file; + return property_file; } public String get_variables_prefix () diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java new file mode 100644 index 0000000..a91d25a --- /dev/null +++ b/instr-to-kodkod/src/VHDLProperty.java @@ -0,0 +1,31 @@ +/* FIXME: Finer imports */ +import java.util.*; +import java.io.*; + +import kodkod.ast.*; + +import org.antlr.v4.runtime.*; + +public class VHDLProperty +{ + private final String filename; + + public VHDLProperty (final String filename) + { + this.filename = filename; + } + + public Formula generate_formula () + throws IOException + { + final PropertyLexer lexer; + final CommonTokenStream tokens; + final PropertyParser parser; + + lexer = new PropertyLexer(CharStreams.fromFileName(filename)); + tokens = new CommonTokenStream(lexer); + parser = new PropertyParser(tokens); + + return parser.tag_existing().result; + } +} |