| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | ast-to-instr/src/Expressions.java | 28 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLCSNode.java | 9 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLISNode.java | 9 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLSSASNode.java | 9 | ||||
| -rw-r--r-- | ast-to-instr/src/VHDLWNode.java | 9 | ||||
| -rw-r--r-- | data/level/control_flow_level.lvl | 4 | ||||
| -rw-r--r-- | data/level/structural_level.lvl | 27 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 3 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyLexer.g4 | 2 | ||||
| -rw-r--r-- | instr-to-kodkod/parser/PropertyParser.g4 | 195 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLLevel.java | 14 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLModel.java | 52 | ||||
| -rw-r--r-- | instr-to-kodkod/src/VHDLPredicate.java | 14 |
13 files changed, 205 insertions, 170 deletions
diff --git a/ast-to-instr/src/Expressions.java b/ast-to-instr/src/Expressions.java index 0ea741b..90b0fff 100644 --- a/ast-to-instr/src/Expressions.java +++ b/ast-to-instr/src/Expressions.java @@ -19,6 +19,7 @@ public class Expressions private static final XPathExpression XPE_GET_INDEX_LIST; private static final XPathExpression XPE_GET_NAMED_ENTITY; private static final XPathExpression XPE_GET_PREFIX_NAMED_ENTITY; + private static final XPathExpression XPE_GET_PREFIX; static { @@ -29,7 +30,7 @@ public class Expressions XPE_GET_FUN_PARAMETERS = XMLManager.compile_or_die ( - "./parameter_association_chain/el" + "./parameter_association_chain/el/actual" ); XPE_GET_INDEX_LIST = XMLManager.compile_or_die("./index_list/el"); @@ -40,6 +41,8 @@ public class Expressions ( "./prefix/named_entity" ); + + XPE_GET_PREFIX = XMLManager.compile_or_die("./prefix"); } private static enum Operator @@ -266,7 +269,7 @@ public class Expressions final int params_length; named_entity = - (Node) XPE_GET_PREFIX_NAMED_ENTITY.evaluate + (Node) XPE_GET_PREFIX/*_NAMED_ENTITY*/.evaluate ( current_node, XPathConstants.NODE @@ -274,18 +277,27 @@ public class Expressions structure.append("(?"); + /* + * TODO: Handle functions better, like: + elements.add + ( + IDs.get_id_from_xml_id + ( + XMLManager.get_attribute(named_entity, "ref"), + null + ) + ); + * But for now, we'll just use the function's name as string: + */ elements.add ( - Waveforms.get_associated_waveform_id + Strings.get_id_from_string ( - IDs.get_id_from_xml_id - ( - XMLManager.get_attribute(named_entity, "ref"), - null - ) + XMLManager.get_attribute(named_entity, "identifier") ) ); + params = (NodeList) XPE_GET_FUN_PARAMETERS.evaluate ( diff --git a/ast-to-instr/src/VHDLCSNode.java b/ast-to-instr/src/VHDLCSNode.java index 3e991f0..f500345 100644 --- a/ast-to-instr/src/VHDLCSNode.java +++ b/ast-to-instr/src/VHDLCSNode.java @@ -75,7 +75,6 @@ public class VHDLCSNode extends VHDLNode handle_function_label(local_id); handle_function_kind(local_id); handle_function_depth(local_id); - handle_function_expression(local_id); /** Predicates **********************************************************/ handle_predicate_has_option(local_id); @@ -138,14 +137,6 @@ public class VHDLCSNode extends VHDLNode ); } - private void handle_function_expression - ( - final IDs local_id - ) - { - /* TODO */ - } - /***************************************************************************/ /** Predicates *************************************************************/ /***************************************************************************/ diff --git a/ast-to-instr/src/VHDLISNode.java b/ast-to-instr/src/VHDLISNode.java index 62fc3da..3c293cd 100644 --- a/ast-to-instr/src/VHDLISNode.java +++ b/ast-to-instr/src/VHDLISNode.java @@ -74,7 +74,6 @@ public class VHDLISNode extends VHDLNode handle_function_label(local_id); handle_function_kind(local_id); handle_function_depth(local_id); - handle_function_expression(local_id); /** Predicates **********************************************************/ handle_predicate_has_option(local_id); @@ -136,14 +135,6 @@ public class VHDLISNode extends VHDLNode ); } - private void handle_function_expression - ( - final IDs local_id - ) - { - /* TODO */ - } - /***************************************************************************/ /** Predicates *************************************************************/ /***************************************************************************/ diff --git a/ast-to-instr/src/VHDLSSASNode.java b/ast-to-instr/src/VHDLSSASNode.java index ef08f6f..b638f81 100644 --- a/ast-to-instr/src/VHDLSSASNode.java +++ b/ast-to-instr/src/VHDLSSASNode.java @@ -68,7 +68,6 @@ public class VHDLSSASNode extends VHDLNode handle_function_label(local_id); handle_function_kind(local_id); handle_function_depth(local_id); - handle_function_expression(local_id); /** Predicates **********************************************************/ handle_predicate_has_option(local_id); @@ -130,14 +129,6 @@ public class VHDLSSASNode extends VHDLNode ); } - private void handle_function_expression - ( - final IDs local_id - ) - { - /* TODO */ - } - /***************************************************************************/ /** Predicates *************************************************************/ /***************************************************************************/ diff --git a/ast-to-instr/src/VHDLWNode.java b/ast-to-instr/src/VHDLWNode.java index 84cebb9..4052229 100644 --- a/ast-to-instr/src/VHDLWNode.java +++ b/ast-to-instr/src/VHDLWNode.java @@ -67,7 +67,6 @@ public class VHDLWNode extends VHDLNode handle_function_label(local_id); handle_function_kind(local_id); handle_function_depth(local_id); - handle_function_expression(local_id); /** Predicates **********************************************************/ handle_predicate_has_option(local_id); @@ -125,14 +124,6 @@ public class VHDLWNode extends VHDLNode ); } - private void handle_function_expression - ( - final IDs local_id - ) - { - /* TODO */ - } - /***************************************************************************/ /** Predicates *************************************************************/ /***************************************************************************/ diff --git a/data/level/control_flow_level.lvl b/data/level/control_flow_level.lvl index 9408409..3b11efe 100644 --- a/data/level/control_flow_level.lvl +++ b/data/level/control_flow_level.lvl @@ -28,3 +28,7 @@ (add_predicate is_read_element node string waveform) (add_predicate is_read_element node string string) (add_predicate is_terminal node) + +(add_function label node string) +(add_function kind node string) +(add_function depth node string) diff --git a/data/level/structural_level.lvl b/data/level/structural_level.lvl index 193eca4..40aa455 100644 --- a/data/level/structural_level.lvl +++ b/data/level/structural_level.lvl @@ -30,6 +30,9 @@ (add_predicate end_has_reserved_id entity) (add_predicate end_has_identifier entity) (add_predicate is_simulation_scenario entity) +(add_function line entity string) +(add_function column entity string) +(add_function identifier entity string) ;;;; Port ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_port_of port entity) @@ -45,6 +48,9 @@ (add_predicate has_open_flag port) (add_predicate has_guarded_signal_flag port) (add_predicate is_of_kind port string) +(add_function line port string) +(add_function column port string) +(add_function identifier port string) ;;;; Generic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_generic_of generic entity) @@ -54,8 +60,11 @@ (add_predicate has_visible_flag generic) (add_predicate has_after_drivers_flag generic) (add_predicate is_of_type generic type) +(add_function line generic string) +(add_function column generic string) +(add_function identifier generic string) -;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;; Architecture ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_in_file architecture file) (add_predicate is_architecture_of architecture entity) (add_predicate has_foreign_flag architecture) @@ -63,6 +72,9 @@ (add_predicate is_within_flag architecture) (add_predicate end_has_reserved_id architecture) (add_predicate end_has_identifier architecture) +(add_function line architecture string) +(add_function column architecture string) +(add_function identifier architecture string) ;;;; Signal ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate belongs_to_architecture signal architecture) @@ -77,6 +89,9 @@ (add_predicate has_guarded_flag signal) (add_predicate is_of_kind signal string) (add_predicate is_of_type signal type) +(add_function line signal string) +(add_function column signal string) +(add_function identifier signal string) ;;;; Process ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate belongs_to_architecture process architecture) @@ -92,17 +107,27 @@ (add_predicate end_has_reserved_id process) (add_predicate end_has_identifier process) (add_predicate is_explicit_process process) +(add_function line process string) +(add_function column process string) +(add_function label process string) + +;;;; File ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_function filename file string) ;;;; Component ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate is_component_of component entity) (add_predicate belongs_to_architecture component architecture) (add_predicate port_maps component waveform port) +(add_function line component string) +(add_function column component string) +(add_function label component string) ;;;; 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) +(add_predicate is_waveform_of waveform generic) ;;;; String ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (add_predicate string_matches string string) diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index bb52959..1b59ccd 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -5,8 +5,9 @@ MAP_FILES = $(wildcard ../ast-to-instr/*.map) LEVEL_DIR = $(wildcard ../data/level/*.lvl) #PROPERTY_FILE = ../data/property/unread_waveforms.pro #PROPERTY_FILE = ../data/property/impossible_processes.pro -PROPERTY_FILE = ../data/property/incrementer.pro +#PROPERTY_FILE = ../data/property/incrementer.pro #PROPERTY_FILE = ../data/property/combinational_processes.pro +PROPERTY_FILE = ../data/property/likely_a_clock.pro VAR_PREFIX = "_anon_" ## Executables ################################################################# diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4 index 46aa30f..9fcad29 100644 --- a/instr-to-kodkod/parser/PropertyLexer.g4 +++ b/instr-to-kodkod/parser/PropertyLexer.g4 @@ -4,6 +4,8 @@ fragment SEP: [ \t\r\n]+; L_PAREN : '('; R_PAREN : ')'; +L_BRAKT: ']'; +R_BRAKT: '['; TAG_EXISTING_KW: '(tag_existing' SEP; diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4 index 82eb429..29e91d2 100644 --- a/instr-to-kodkod/parser/PropertyParser.g4 +++ b/instr-to-kodkod/parser/PropertyParser.g4 @@ -116,7 +116,7 @@ tag_item } ; -id_or_string +id_or_string_or_fun [Variable current_node] returns [Expression value] : @@ -138,9 +138,15 @@ id_or_string $value = Main.get_string_manager().get_string_as_relation(($STRING.text)); System.out.println("Using (STR \"" + ($STRING.text) + "\" " + ($value) + ")"); } + + | + function[current_node] + { + $value = ($function.result); + } ; -id_list +id_list [Variable current_node] returns [List<Expression> list, boolean has_joker] @init @@ -152,14 +158,14 @@ id_list : ( (WS)+ - id_or_string + id_or_string_or_fun[current_node] { - if (($id_or_string.value) == (Expression) null) + if (($id_or_string_or_fun.value) == (Expression) null) { used_joker = true; } - result.add(($id_or_string.value)); + result.add(($id_or_string_or_fun.value)); } )* @@ -169,16 +175,12 @@ id_list } ; -/******************************************************************************/ -/** Structural Level **********************************************************/ -/******************************************************************************/ - -sl_predicate +predicate [Variable current_node] returns [Formula result]: (WS)* L_PAREN ID - id_list + id_list[current_node] (WS)* R_PAREN { @@ -198,7 +200,7 @@ sl_predicate ( "[F] The property uses an unknown predicate: \"" + ($ID.text) - + "\" at structural level. (l." + + "\" (l." + ($ID.getLine()) + " c." + ($ID.getCharPositionInLine()) @@ -212,17 +214,30 @@ sl_predicate { final List<IntExpression> columns; final int params_length; + final int offset; ids = new ArrayList<Expression>(); columns = new ArrayList<IntExpression>(); params_length = ($id_list.list).size(); + if (current_node == null) + { + offset = 0; + } + else + { + offset = 1; + + ids.add(current_node); + columns.add(IntConstant.constant(0)); + } + for (int i = 0; i < params_length; ++i) { if (($id_list.list).get(i) != (Expression) null) { - columns.add(IntConstant.constant(i)); + columns.add(IntConstant.constant(i + offset)); ids.add(($id_list.list).get(i)); } } @@ -237,12 +252,85 @@ sl_predicate { predicate = predicate_as_relation; ids = ($id_list.list); + + if (current_node != null) + { + ids.add(0, current_node); + } } $result = Expression.product(ids).in(predicate); } ; +function [Variable current_node] + returns [Expression result]: + + (WS)* L_BRAKT + ID + id_list[current_node] + (WS)* R_BRAKT + + { + final Expression predicate; + final List<Expression> ids; + final Relation predicate_as_relation; + + predicate_as_relation = + Main.get_model().get_predicate_as_relation + ( + ($ID.text) + ); + + if (predicate_as_relation == (Relation) null) + { + System.err.println + ( + "[F] The property uses an unknown predicate: \"" + + ($ID.text) + + "\" (l." + + ($ID.getLine()) + + " c." + + ($ID.getCharPositionInLine()) + + ")." + ); + + System.exit(-1); + } + + if (($id_list.has_joker)) + { + System.err.println + ( + "[F] The property uses a joker inside a function: \"" + + ($ID.text) + + "\" (l." + + ($ID.getLine()) + + " c." + + ($ID.getCharPositionInLine()) + + ")." + ); + + System.exit(-1); + } + else + { + predicate = predicate_as_relation; + ids = ($id_list.list); + + if (current_node != null) + { + ids.add(0, current_node); + } + + $result = Expression.product(ids).join(predicate); + } + } +; + +/******************************************************************************/ +/** Structural Level **********************************************************/ +/******************************************************************************/ sl_non_empty_formula_list returns [List<Formula> list] @@ -466,9 +554,9 @@ sl_ctl_verifies_operator sl_formula returns [Formula result]: - sl_predicate + predicate[null] { - $result = ($sl_predicate.result); + $result = ($predicate.result); } | sl_and_operator @@ -510,79 +598,6 @@ sl_formula /******************************************************************************/ /** Behavioral Level **********************************************************/ /******************************************************************************/ -bl_predicate [Variable current_node] - returns [Formula result]: - - (WS)* L_PAREN - ID - id_list - (WS)* R_PAREN - - { - final Expression predicate; - final List<Expression> ids; - final Relation predicate_as_relation; - - predicate_as_relation = - Main.get_model().get_predicate_as_relation - ( - ($ID.text) - ); - - if (predicate_as_relation == (Relation) null) - { - System.err.println - ( - "[F] The property uses an unknown predicate: \"" - + ($ID.text) - + "\" at behavioral level (l." - + ($ID.getLine()) - + " c." - + ($ID.getCharPositionInLine()) - + ")." - ); - - System.exit(-1); - } - - if (($id_list.has_joker)) - { - final List<IntExpression> columns; - final int params_length; - - ids = new ArrayList<Expression>(); - columns = new ArrayList<IntExpression>(); - - params_length = ($id_list.list).size(); - - /* We always keep the node id. */ - columns.add(IntConstant.constant(0)); - - for (int i = 0; i < params_length; ++i) - { - if (($id_list.list).get(i) != (Expression) null) - { - columns.add(IntConstant.constant(i + 1)); // Offset for the node - ids.add(($id_list.list).get(i)); - } - } - - predicate = - predicate_as_relation.project - ( - columns.toArray(new IntExpression[columns.size()]) - ); - } - else - { - predicate = predicate_as_relation; - ids = ($id_list.list); - } - - $result = current_node.product(Expression.product(ids)).in(predicate); - } -; - bl_formula_list [Variable current_node] returns [List<Formula> list] @@ -1017,9 +1032,9 @@ bl_eu_operator [Variable current_node] bl_formula [Variable current_node] returns [Formula result]: - bl_predicate[current_node] + predicate[current_node] { - $result = ($bl_predicate.result); + $result = ($predicate.result); } | bl_and_operator[current_node] { diff --git a/instr-to-kodkod/src/VHDLLevel.java b/instr-to-kodkod/src/VHDLLevel.java index 738adaf..57bb8c4 100644 --- a/instr-to-kodkod/src/VHDLLevel.java +++ b/instr-to-kodkod/src/VHDLLevel.java @@ -60,7 +60,11 @@ public class VHDLLevel } else if (input[0].equals("add_predicate")) { - success = handle_add_predicate(input, m); + success = handle_add_predicate(input, m, false); + } + else if (input[0].equals("add_function")) + { + success = handle_add_predicate(input, m, true); } else { @@ -128,7 +132,8 @@ public class VHDLLevel private static boolean handle_add_predicate ( final String[] cmd, - final VHDLModel m + final VHDLModel m, + final boolean is_function ) { final String[] signature; @@ -137,7 +142,8 @@ public class VHDLLevel { System.err.println ( - "[E] Badly formed \"add_predicate\" instruction: \"" + "[E] Badly formed \"add_predicate\" or \"add_function\"" + + " instruction: \"" + String.join(" ", cmd) + "\"." ); @@ -152,6 +158,6 @@ public class VHDLLevel signature[i - 2] = cmd[i]; } - return m.add_predicate(cmd[1], signature); + return m.add_predicate(cmd[1], signature, is_function); } } diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java index ea024b8..4b6e053 100644 --- a/instr-to-kodkod/src/VHDLModel.java +++ b/instr-to-kodkod/src/VHDLModel.java @@ -25,7 +25,12 @@ public class VHDLModel } } - public boolean add_predicate (final String name, final String[] signature) + public boolean add_predicate + ( + final String name, + final String[] signature, + final boolean is_function + ) { final VHDLPredicate p; final VHDLType[] true_signature; @@ -55,7 +60,11 @@ public class VHDLModel if (p == null) { - predicates.put(name, new VHDLPredicate(name, true_signature)); + predicates.put + ( + name, + new VHDLPredicate(name, true_signature, false) + ); } else { @@ -113,7 +122,15 @@ public class VHDLModel } else if (input[0].equals("set_function")) { - success = handle_set_function(input); + if (input.length < 2) + { + success = false; + } + success = + handle_predicate + ( + Arrays.copyOfRange(input, 1, input.length) + ); } else { @@ -126,7 +143,9 @@ public class VHDLModel ( "[E] An erroneous instruction was found in file \"" + filename - + "\"." + + "\": \"(" + + String.join(" ", input) + + ")\")" ); try @@ -186,30 +205,6 @@ public class VHDLModel 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; @@ -256,7 +251,6 @@ public class VHDLModel 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])) diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java index 3605e76..0ff388b 100644 --- a/instr-to-kodkod/src/VHDLPredicate.java +++ b/instr-to-kodkod/src/VHDLPredicate.java @@ -14,11 +14,18 @@ public class VHDLPredicate private final String name; private final int arity; private final Relation as_relation; + private final boolean is_function; private boolean is_used; - public VHDLPredicate (final String name, final VHDLType[] signature) + public VHDLPredicate + ( + final String name, + final VHDLType[] signature, + final boolean is_function + ) { this.name = name; + this.is_function = is_function; arity = signature.length; signatures = new ArrayList<VHDLType[]>(); @@ -45,6 +52,11 @@ public class VHDLPredicate return arity; } + public boolean is_function () + { + return is_function; + } + public Relation get_as_relation () { if (!is_used) |