From 70b40bfb6c032c0dead7069b2178a43e63a8e563 Mon Sep 17 00:00:00 2001 From: Nathanael Sensfelder Date: Wed, 19 Jul 2017 10:29:52 +0200 Subject: First shot at the framework (it does compile). --- data/instructions/example_process.pl.kk | 88 ++++++++++++++++++++++ data/level/control_flow_level.data | 19 ----- data/level/control_flow_level.lvl | 24 ++++++ data/level/control_flow_level_kodkod.data | 14 ---- data/level/control_flow_level_kodkod.lvl | 17 +++++ data/level/structural_level.data | 112 ---------------------------- data/level/structural_level.lvl | 112 ++++++++++++++++++++++++++++ data/property/unread_waveforms.pro | 10 +++ instr-to-kodkod/Makefile | 7 +- instr-to-kodkod/parser/Makefile | 8 ++ instr-to-kodkod/parser/PropertyParser.g4 | 70 ++++++++++++++++-- instr-to-kodkod/src/Main.java | 118 +++++++++++++++++++++--------- instr-to-kodkod/src/Parameters.java | 114 ++++++++++++++++++++++++----- instr-to-kodkod/src/VHDLProperty.java | 31 ++++++++ 14 files changed, 535 insertions(+), 209 deletions(-) create mode 100644 data/instructions/example_process.pl.kk delete mode 100644 data/level/control_flow_level.data create mode 100644 data/level/control_flow_level.lvl delete mode 100644 data/level/control_flow_level_kodkod.data create mode 100644 data/level/control_flow_level_kodkod.lvl delete mode 100644 data/level/structural_level.data create mode 100644 data/level/structural_level.lvl create mode 100644 data/property/unread_waveforms.pro create mode 100644 instr-to-kodkod/parser/Makefile create mode 100644 instr-to-kodkod/src/VHDLProperty.java diff --git a/data/instructions/example_process.pl.kk b/data/instructions/example_process.pl.kk new file mode 100644 index 0000000..c4f07b3 --- /dev/null +++ b/data/instructions/example_process.pl.kk @@ -0,0 +1,88 @@ +(add_element path p237_0) +(is_path_of p237_0 237) +(contains_node p237_0 262) +(is_before p237_0 262 263) +(contains_node p237_0 263) +(add_element path p237_1) +(is_path_of p237_1 262) +(contains_node p237_1 263) +(add_element path p237_2) +(is_path_of p237_2 237) +(contains_node p237_2 260) +(is_before p237_2 260 261) +(contains_node p237_2 261) +(add_element path p237_3) +(is_path_of p237_3 260) +(contains_node p237_3 261) +(add_element path p237_4) +(is_path_of p237_4 237) +(contains_node p237_4 258) +(is_before p237_4 258 259) +(contains_node p237_4 259) +(add_element path p237_5) +(is_path_of p237_5 258) +(contains_node p237_5 259) +(add_element path p237_6) +(is_path_of p237_6 237) +(contains_node p237_6 256) +(is_before p237_6 256 257) +(contains_node p237_6 257) +(add_element path p237_7) +(is_path_of p237_7 256) +(contains_node p237_7 257) +(add_element path p237_8) +(is_path_of p237_8 237) +(contains_node p237_8 254) +(is_before p237_8 254 255) +(contains_node p237_8 255) +(add_element path p237_9) +(is_path_of p237_9 254) +(contains_node p237_9 255) +(add_element path p237_10) +(is_path_of p237_10 237) +(contains_node p237_10 252) +(is_before p237_10 252 253) +(contains_node p237_10 253) +(add_element path p237_11) +(is_path_of p237_11 252) +(contains_node p237_11 253) +(add_element path p237_12) +(is_path_of p237_12 237) +(contains_node p237_12 250) +(is_before p237_12 250 251) +(contains_node p237_12 251) +(add_element path p237_13) +(is_path_of p237_13 250) +(contains_node p237_13 251) +(add_element path p237_14) +(is_path_of p237_14 237) +(contains_node p237_14 248) +(is_before p237_14 248 249) +(contains_node p237_14 249) +(add_element path p237_15) +(is_path_of p237_15 248) +(contains_node p237_15 249) +(add_element path p237_16) +(is_path_of p237_16 237) +(contains_node p237_16 246) +(is_before p237_16 246 247) +(contains_node p237_16 247) +(add_element path p237_17) +(is_path_of p237_17 246) +(contains_node p237_17 247) +(add_element path p237_18) +(is_path_of p237_18 237) +(contains_node p237_18 244) +(is_before p237_18 244 245) +(contains_node p237_18 245) +(add_element path p237_19) +(is_path_of p237_19 244) +(contains_node p237_19 245) +(add_element path p237_20) +(is_path_of p237_20 237) +(contains_node p237_20 239) +(is_before p237_20 239 242) +(contains_node p237_20 242) +(add_element path p237_21) +(is_path_of p237_21 239) +(contains_node p237_21 242) diff --git a/data/level/control_flow_level.data b/data/level/control_flow_level.data deleted file mode 100644 index a7cc9c0..0000000 --- a/data/level/control_flow_level.data +++ /dev/null @@ -1,19 +0,0 @@ -;; Control Flow Level - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(add_type node) -(add_type node_depth) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_start_node node process) -(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.lvl b/data/level/control_flow_level.lvl new file mode 100644 index 0000000..516f9ef --- /dev/null +++ b/data/level/control_flow_level.lvl @@ -0,0 +1,24 @@ +;; Control Flow Level + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type node) +(add_type node_depth) + +;; Redundancies +(add_type process) +(add_type string) +(add_type waveform) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_start_node node process) +(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 deleted file mode 100644 index ed11735..0000000 --- a/data/level/control_flow_level_kodkod.data +++ /dev/null @@ -1,14 +0,0 @@ -;; 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) -(add_predicate is_before path node node) diff --git a/data/level/control_flow_level_kodkod.lvl b/data/level/control_flow_level_kodkod.lvl new file mode 100644 index 0000000..949f69f --- /dev/null +++ b/data/level/control_flow_level_kodkod.lvl @@ -0,0 +1,17 @@ +;; Control Flow Level, Kodkod additions + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type path) + +;; Redundancies +(add_type node) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_path_of path node) +(add_predicate contains_node path node) +(add_predicate is_before path node node) diff --git a/data/level/structural_level.data b/data/level/structural_level.data deleted file mode 100644 index 75c4ac9..0000000 --- a/data/level/structural_level.data +++ /dev/null @@ -1,112 +0,0 @@ -;; Structural Level - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(add_type entity) -(add_type port) -(add_type port_mode) -(add_type generic) -(add_type architecture) -(add_type signal) -(add_type process) -(add_type file) -(add_type component) -(add_type waveform) -(add_type string) -(add_type type) -(add_type type_kind) -(add_type signal_kind) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;;;; Entity ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_file entity file) -(add_predicate has_begin entity) -(add_predicate has_visible_flag entity) -(add_predicate end_has_reserved_id entity) -(add_predicate end_has_identifier entity) -(add_predicate is_simulation_scenario entity) - -;;;; Port ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_port_of port entity) -(add_predicate has_disconnect_flag port) -(add_predicate is_of_mode port string) -(add_predicate has_class port) -(add_predicate is_ref port) -(add_predicate has_active_flag port) -(add_predicate has_identifier_list port) -(add_predicate has_visible_flag port) -(add_predicate has_after_drivers_flag port) -(add_predicate has_use_flag port) -(add_predicate has_open_flag port) -(add_predicate has_guarded_signal_flag port) -(add_predicate is_of_kind port string) - -;;;; Generic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_generic_of generic entity) -(add_predicate has_class generic) -(add_predicate is_ref generic) -(add_predicate has_identifier_list generic) -(add_predicate has_visible_flag generic) -(add_predicate has_after_drivers_flag generic) -(add_predicate is_of_type generic type) - -;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_file architecture file) -(add_predicate is_architecture_of architecture entity) -(add_predicate has_foreign_flag architecture) -(add_predicate has_visible_flag architecture) -(add_predicate is_within_flag architecture) -(add_predicate end_has_reserved_id architecture) -(add_predicate end_has_identifier architecture) - -;;;; Signal ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate belongs_to_architecture signal architecture) -(add_predicate has_disconnect_flag signal) -(add_predicate is_ref signal) -(add_predicate has_active_flag signal) -(add_predicate has_identifier_list signal) -(add_predicate has_visible_flag signal) -(add_predicate has_after_drivers signal) -(add_predicate has_use_flag signal) -(add_predicate has_open_flag signal) -(add_predicate has_guarded_flag signal) -(add_predicate is_of_kind signal string) -(add_predicate is_of_type signal type) - -;;;; Process ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate belongs_to_architecture process architecture) -(add_predicate has_seen_flag process) -(add_predicate end_has_postboned process) -(add_predicate has_postboned_flag process) -(add_predicate is_ref process) -(add_predicate has_passive_flag process) -(add_predicate has_visible_flag process) -(add_predicate is_within_flag process) -(add_predicate has_label process) -(add_predicate has_is process) -(add_predicate end_has_reserved_id process) -(add_predicate end_has_identifier process) -(add_predicate is_explicit_process process) - -;;;; Component ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_component_of component entity) -(add_predicate belongs_to_architecture component architecture) -(add_predicate port_maps component waveform port) - -;;;; Waveform ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_in_sensitivity_list waveform process) -(add_predicate is_accessed_by waveform process) -(add_predicate is_waveform_of waveform signal) -(add_predicate is_waveform_of waveform port) - -;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate string_matches string string) - -;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(add_predicate is_approved_type type) -(add_predicate is_of_kind type string) diff --git a/data/level/structural_level.lvl b/data/level/structural_level.lvl new file mode 100644 index 0000000..75c4ac9 --- /dev/null +++ b/data/level/structural_level.lvl @@ -0,0 +1,112 @@ +;; Structural Level + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(add_type entity) +(add_type port) +(add_type port_mode) +(add_type generic) +(add_type architecture) +(add_type signal) +(add_type process) +(add_type file) +(add_type component) +(add_type waveform) +(add_type string) +(add_type type) +(add_type type_kind) +(add_type signal_kind) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;;; Entity ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_file entity file) +(add_predicate has_begin entity) +(add_predicate has_visible_flag entity) +(add_predicate end_has_reserved_id entity) +(add_predicate end_has_identifier entity) +(add_predicate is_simulation_scenario entity) + +;;;; Port ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_port_of port entity) +(add_predicate has_disconnect_flag port) +(add_predicate is_of_mode port string) +(add_predicate has_class port) +(add_predicate is_ref port) +(add_predicate has_active_flag port) +(add_predicate has_identifier_list port) +(add_predicate has_visible_flag port) +(add_predicate has_after_drivers_flag port) +(add_predicate has_use_flag port) +(add_predicate has_open_flag port) +(add_predicate has_guarded_signal_flag port) +(add_predicate is_of_kind port string) + +;;;; Generic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_generic_of generic entity) +(add_predicate has_class generic) +(add_predicate is_ref generic) +(add_predicate has_identifier_list generic) +(add_predicate has_visible_flag generic) +(add_predicate has_after_drivers_flag generic) +(add_predicate is_of_type generic type) + +;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_file architecture file) +(add_predicate is_architecture_of architecture entity) +(add_predicate has_foreign_flag architecture) +(add_predicate has_visible_flag architecture) +(add_predicate is_within_flag architecture) +(add_predicate end_has_reserved_id architecture) +(add_predicate end_has_identifier architecture) + +;;;; Signal ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate belongs_to_architecture signal architecture) +(add_predicate has_disconnect_flag signal) +(add_predicate is_ref signal) +(add_predicate has_active_flag signal) +(add_predicate has_identifier_list signal) +(add_predicate has_visible_flag signal) +(add_predicate has_after_drivers signal) +(add_predicate has_use_flag signal) +(add_predicate has_open_flag signal) +(add_predicate has_guarded_flag signal) +(add_predicate is_of_kind signal string) +(add_predicate is_of_type signal type) + +;;;; Process ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate belongs_to_architecture process architecture) +(add_predicate has_seen_flag process) +(add_predicate end_has_postboned process) +(add_predicate has_postboned_flag process) +(add_predicate is_ref process) +(add_predicate has_passive_flag process) +(add_predicate has_visible_flag process) +(add_predicate is_within_flag process) +(add_predicate has_label process) +(add_predicate has_is process) +(add_predicate end_has_reserved_id process) +(add_predicate end_has_identifier process) +(add_predicate is_explicit_process process) + +;;;; Component ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_component_of component entity) +(add_predicate belongs_to_architecture component architecture) +(add_predicate port_maps component waveform port) + +;;;; Waveform ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_in_sensitivity_list waveform process) +(add_predicate is_accessed_by waveform process) +(add_predicate is_waveform_of waveform signal) +(add_predicate is_waveform_of waveform port) + +;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate string_matches string string) + +;;;; Type ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_approved_type type) +(add_predicate is_of_kind type string) diff --git a/data/property/unread_waveforms.pro b/data/property/unread_waveforms.pro new file mode 100644 index 0000000..b53862b --- /dev/null +++ b/data/property/unread_waveforms.pro @@ -0,0 +1,10 @@ +(tag_existing + ( + (wf waveform UNREAD_WAVEFORM) + ) + (not + (exists ps process + (is_accessed_by wf ps) + ) + ) +) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 2611f28..073fe58 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -19,12 +19,13 @@ CLASSES = $(SOURCES:.java=.class) ## Makefile Rules ############################################################## -all: $(CLASSES) +all: parser/PropertyParser.java $(CLASSES) clean: rm -f $(CLASSES) + $(MAKE) -C parser clean -run: $(CLASSES) $(REQUIRED_JARS) +run: parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS) $(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE) %.class: %.java $(REQUIRED_JARS) @@ -34,3 +35,5 @@ run: $(CLASSES) $(REQUIRED_JARS) echo "Attempting to download missing jar '$@'" $(DOWNLOADER) "$(JAR_SOURCE)/$@" +parser/PropertyParser.java: antlr-4.7-complete.jar + $(MAKE) -C parser diff --git a/instr-to-kodkod/parser/Makefile b/instr-to-kodkod/parser/Makefile new file mode 100644 index 0000000..8f36479 --- /dev/null +++ b/instr-to-kodkod/parser/Makefile @@ -0,0 +1,8 @@ +PropertyParser.java: PropertyLexer.g4 PropertyParser.g4 + java -jar ../antlr-4.7-complete.jar PropertyLexer.g4 PropertyParser.g4 + +clean: + rm -f *.java *.class *.tokens + +#test_run: +# java -cp ".:../antlr-4.7-complete.jar" org.antlr.v4.gui.TestRig Property prog -gui diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 63939d7..5e1ed11 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -20,26 +20,80 @@ options /* of the class */ } -prog: - tag_existing -; +tag_existing + returns [Formula result]: -tag_existing: (WS)* TAG_EXISTING_KW L_PAREN - (tag_item)+ + tag_list R_PAREN (WS)* sl_formula (WS)* R_PAREN + + { + final List tags; + + $result = ($sl_formula.result); + + tags = ($tag_list.list); + + for (final String[] tag_var: tags) + { + $result = + $result.forSome + ( + Main.get_variable_manager().get_variable + ( + tag_var[0] + ).oneOf + ( + Main.get_model().get_type_as_relation(tag_var[1]) + ) + ); + + Main.get_variable_manager().tag_variable(tag_var[0], tag_var[2]); + } + } ; -tag_item: +tag_list + returns [List list] + + @init + { + final List result = new ArrayList(); + } + + : + ( + tag_item + { + result.add(($tag_item.result)); + } + )+ + + { + $list = result; + } +; + +tag_item + returns [String[] result]: + (WS)* L_PAREN (WS)* var=ID (WS)+ type=ID (WS)+ tag=ID (WS)* R_PAREN (WS)* + + { + $result = new String[3]; + + $result[0] = ($var.text); + $result[1] = ($type.text); + $result[2] = ($tag.text); + } ; id_list @@ -53,9 +107,9 @@ id_list : ( (WS)+ - var=ID + ID { - result.add(Main.get_variable_manager().get_variable($var.text)); + result.add(Main.get_variable_manager().get_variable(($ID.text))); } )* 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 level_files; + private final List 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 \n" + + "\tjava Main +\n" + "PARAMETERS:\n" - + "\t\tDirectory containing the level definitions.\n" - + "\t\tInstruction file describing the model.\n" - + "\t\tPrefix for anonymous variables (e.g. \"_anon_\").\n" + + "\t- \tPrefix for anonymous variables (e.g. \"_anon_\").\n" + + "\t- \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 .\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(); + model_files = new ArrayList(); + + 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 get_level_files () + { + return level_files; } - public String get_levels_directory () + public List 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; + } +} -- cgit v1.2.3-70-g09d2