| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | ast-to-instr/src/Depths.java | 72 | ||||
| -rw-r--r-- | ast-to-instr/src/Main.java | 2 | ||||
| -rw-r--r-- | ast-to-instr/src/Strings.java | 2 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLCSNode.java | 5 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLISNode.java | 5 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLSSASNode.java | 5 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLWNode.java | 5 | ||||
| -rw-r--r-- | data/level/control_flow_level.lvl | 8 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 6 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyLexer.g4 | 3 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 154 |
11 files changed, 245 insertions, 22 deletions
diff --git a/ast-to-instr/src/Depths.java b/ast-to-instr/src/Depths.java new file mode 100644 index 0000000..ade01c8 --- /dev/null +++ b/ast-to-instr/src/Depths.java @@ -0,0 +1,72 @@ +import java.util.Map; +import java.util.HashMap; + +public class Depths +{ + private static final Map<Integer, IDs> TO_ID; + private static final OutputFile DEPTHS_OUTPUT; + private static int highest_depth; + + static + { + highest_depth = -1; + + TO_ID = new HashMap<Integer, IDs>(); + + /* TODO: filename as a param? */ + DEPTHS_OUTPUT = OutputFile.new_output_file("depths.mod"); + } + + private Depths () {} /* Utility class. */ + + public static IDs get_id_from_depth + ( + final String depth + ) + { + return get_id_from_depth(Integer.valueOf(depth)); + } + + public static IDs get_id_from_depth + ( + final Integer depth + ) + { + IDs result; + + result = TO_ID.get(depth); + + if (result == null) + { + result = IDs.generate_new_id(DEPTHS_OUTPUT, "depth"); + + TO_ID.put(depth, result); + } + + if (depth.intValue() > highest_depth) + { + highest_depth = depth.intValue(); + } + + return result; + } + + public static void generate_predicates () + { + for + ( + int current_depth = highest_depth; + current_depth > 0; + --current_depth + ) + { + Predicates.add_entry + ( + DEPTHS_OUTPUT, + "is_lower_than", + get_id_from_depth(new Integer(current_depth - 1)), + get_id_from_depth(new Integer(current_depth)) + ); + } + } +} diff --git a/ast-to-instr/src/Main.java b/ast-to-instr/src/Main.java index 5bc45a0..0e24f57 100644 --- a/ast-to-instr/src/Main.java +++ b/ast-to-instr/src/Main.java @@ -87,6 +87,8 @@ public class Main parse_content(vhdl_files); + Depths.generate_predicates(); + OutputFile.close_all(); } diff --git a/ast-to-instr/src/Strings.java b/ast-to-instr/src/Strings.java index 67189ad..a03070b 100644 --- a/ast-to-instr/src/Strings.java +++ b/ast-to-instr/src/Strings.java @@ -18,7 +18,7 @@ public class Strings public static IDs get_id_from_string ( - String string + final String string ) { return get_id_from_string(Main.get_main_output(), string); diff --git a/ast-to-instr/src/VHDLCSNode.java b/ast-to-instr/src/VHDLCSNode.java index f500345..6682613 100644 --- a/ast-to-instr/src/VHDLCSNode.java +++ b/ast-to-instr/src/VHDLCSNode.java @@ -130,10 +130,7 @@ public class VHDLCSNode extends VHDLNode output, "depth", local_id, - Strings.get_id_from_string - ( - Integer.toString(depth) - ) + Depths.get_id_from_depth(new Integer(depth)) ); } diff --git a/ast-to-instr/src/VHDLISNode.java b/ast-to-instr/src/VHDLISNode.java index 3c293cd..4883080 100644 --- a/ast-to-instr/src/VHDLISNode.java +++ b/ast-to-instr/src/VHDLISNode.java @@ -128,10 +128,7 @@ public class VHDLISNode extends VHDLNode output, "depth", local_id, - Strings.get_id_from_string - ( - Integer.toString(depth) - ) + Depths.get_id_from_depth(new Integer(depth)) ); } diff --git a/ast-to-instr/src/VHDLSSASNode.java b/ast-to-instr/src/VHDLSSASNode.java index b638f81..944ad18 100644 --- a/ast-to-instr/src/VHDLSSASNode.java +++ b/ast-to-instr/src/VHDLSSASNode.java @@ -122,10 +122,7 @@ public class VHDLSSASNode extends VHDLNode output, "depth", local_id, - Strings.get_id_from_string - ( - Integer.toString(depth) - ) + Depths.get_id_from_depth(new Integer(depth)) ); } diff --git a/ast-to-instr/src/VHDLWNode.java b/ast-to-instr/src/VHDLWNode.java index 4052229..b893c7a 100644 --- a/ast-to-instr/src/VHDLWNode.java +++ b/ast-to-instr/src/VHDLWNode.java @@ -117,10 +117,7 @@ public class VHDLWNode extends VHDLNode output, "depth", local_id, - Strings.get_id_from_string - ( - Integer.toString(depth) - ) + Depths.get_id_from_depth(new Integer(depth)) ); } diff --git a/data/level/control_flow_level.lvl b/data/level/control_flow_level.lvl index 3b11efe..106235d 100644 --- a/data/level/control_flow_level.lvl +++ b/data/level/control_flow_level.lvl @@ -5,7 +5,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_type node) -(add_type node_depth) +(add_type depth) ;; Redundancies (add_type process) @@ -16,9 +16,7 @@ ;; 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) ;;; To be removed soon. @@ -29,6 +27,8 @@ (add_predicate is_read_element node string string) (add_predicate is_terminal node) +(add_predicate is_lower_than depth depth) + (add_function label node string) (add_function kind node string) -(add_function depth node string) +(add_function depth node depth) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 1b59ccd..705f3e2 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -1,6 +1,10 @@ ## Target(s) Configuration ##################################################### #MODEL_FILES = $(wildcard ../data/instructions/*.mod) -MODEL_FILES = ../ast-to-instr/structural.mod $(wildcard ../ast-to-instr/cfg_*.mod) $(wildcard ../cfg-to-paths/*.mod) +MODEL_FILES = \ + ../ast-to-instr/structural.mod \ + ../ast-to-instr/depths.mod \ + $(wildcard ../ast-to-instr/cfg_*.mod) \ + $(wildcard ../cfg-to-paths/*.mod) MAP_FILES = $(wildcard ../ast-to-instr/*.map) LEVEL_DIR = $(wildcard ../data/level/*.lvl) #PROPERTY_FILE = ../data/property/unread_waveforms.pro diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4 index 9fcad29..64fccb0 100644 --- a/instr-to-kodkod/parser/PropertyLexer.g4 +++ b/instr-to-kodkod/parser/PropertyLexer.g4 @@ -28,6 +28,9 @@ EF_OPERATOR_KW: '(EF' SEP; AU_OPERATOR_KW: '(AU' SEP; EU_OPERATOR_KW: '(EU' SEP; +DEPTH_NO_PARENT_OPERATOR_KW: '(does_not_reach_parent_before' SEP; +DEPTH_NO_CHANGE_OPERATOR_KW: '(does_not_change_depth_before' SEP; + WS: SEP; ID: [a-zA-Z0-9_]+; diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 29e91d2..5c93eac 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -1028,6 +1028,152 @@ bl_eu_operator [Variable current_node] } ; +/**** Depth Operators *********************************************************/ +bl_depth_no_parent_operator [Variable current_node] + returns [Formula result] + + @init + { + final Variable node_of_path, node_for_f, chosen_path; + + node_of_path = Main.get_variable_manager().generate_new_variable(); + node_for_f = Main.get_variable_manager().generate_new_variable(); + chosen_path = Main.get_variable_manager().generate_new_variable(); + } + + : + (WS)* DEPTH_NO_PARENT_OPERATOR_KW + bl_formula[node_for_f] + (WS)* R_PAREN + + { + final Relation depth_relation; + + depth_relation = Main.get_model().get_predicate_as_relation("depth"); + + $result = + node_of_path.join + ( + depth_relation + ).product + ( + node_for_f.join(depth_relation) + ).in + ( + Main.get_model().get_predicate_as_relation("is_lower_than") + ).not + ( + /* (not (is_lower_than [depth node_of_path] [depth node_for_f])) */ + ).forAll + ( + node_of_path.oneOf + ( + node_for_f.join + ( + chosen_path.join + ( + Main.get_model().get_predicate_as_relation("is_before") + ).transpose() + ) + ) + ).and + ( + ($bl_formula.result) + ).forSome + ( + node_for_f.oneOf + ( + chosen_path.join + ( + Main.get_model().get_predicate_as_relation("contains_node") + ) + ) + ).forAll + ( + chosen_path.oneOf + ( + current_node.join + ( + Main.get_model().get_predicate_as_relation + ( + "is_path_of" + ).transpose() + ) + ) + ); + } +; + +bl_depth_no_change_operator [Variable current_node] + returns [Formula result] + + @init + { + final Variable node_of_path, node_for_f, chosen_path; + + node_of_path = Main.get_variable_manager().generate_new_variable(); + node_for_f = Main.get_variable_manager().generate_new_variable(); + chosen_path = Main.get_variable_manager().generate_new_variable(); + } + + : + (WS)* DEPTH_NO_PARENT_OPERATOR_KW + bl_formula[node_for_f] + (WS)* R_PAREN + + { + final Relation depth_relation; + + depth_relation = Main.get_model().get_predicate_as_relation("depth"); + + $result = + node_of_path.join + ( + depth_relation + ).eq + ( + node_for_f.join(depth_relation) + /* (eq? [depth node_of_path] [depth node_for_f]) */ + ).forAll + ( + node_of_path.oneOf + ( + node_for_f.join + ( + chosen_path.join + ( + Main.get_model().get_predicate_as_relation("is_before") + ).transpose() + ) + ) + ).and + ( + ($bl_formula.result) + ).forSome + ( + node_for_f.oneOf + ( + chosen_path.join + ( + Main.get_model().get_predicate_as_relation("contains_node") + ) + ) + ).forAll + ( + chosen_path.oneOf + ( + current_node.join + ( + Main.get_model().get_predicate_as_relation + ( + "is_path_of" + ).transpose() + ) + ) + ); + } +; + /**** Formula Definition ******************************************************/ bl_formula [Variable current_node] returns [Formula result]: @@ -1084,4 +1230,12 @@ bl_formula [Variable current_node] { $result = ($bl_eu_operator.result); } + | bl_depth_no_parent_operator[current_node] + { + $result = ($bl_depth_no_parent_operator.result); + } + | bl_depth_no_change_operator[current_node] + { + $result = ($bl_depth_no_change_operator.result); + } ; |