| summaryrefslogtreecommitdiff |
diff options
| -rw-r--r-- | Makefile | 8 | ||||
| -rw-r--r-- | data/level/instances.lvl | 23 | ||||
| -rw-r--r-- | data/property/simple_flip_flop.pro | 1 | ||||
| -rw-r--r-- | data/property/test-case/fast.pp | 6 | ||||
| -rw-r--r-- | data/property/test-case/fast.pro | 57 | ||||
| -rw-r--r-- | data/property/test-case/slow.pp | 6 | ||||
| -rw-r--r-- | data/property/test-case/slow.pro | 60 | ||||
| -rw-r--r-- | instance-calculator/Makefile | 75 | ||||
| -rw-r--r-- | instance-calculator/src/.java_classpath | 1 | ||||
| -rw-r--r-- | instance-calculator/src/Main.java | 121 | ||||
| -rw-r--r-- | instance-calculator/src/ModelFile.java | 310 | ||||
| -rw-r--r-- | instance-calculator/src/OutputFile.java | 135 | ||||
| -rw-r--r-- | instance-calculator/src/Parameters.java | 64 | ||||
| -rw-r--r-- | instance-calculator/src/QuickParser.java | 62 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLArchitecture.java | 179 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLComponent.java | 146 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLEntity.java | 150 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLProcess.java | 253 | ||||
| -rw-r--r-- | instance-calculator/src/VHDLWaveform.java | 190 | ||||
| -rw-r--r-- | instance-calculator/src/Waveforms.java | 74 | ||||
| -rw-r--r-- | instr-to-kodkod/Makefile | 6 |
21 files changed, 1925 insertions, 2 deletions
@@ -8,10 +8,12 @@ AST_FILE = ${CURDIR}/data/ast/best_chronometer_ever.xml TMP_DIR = /tmp/tabellion MODEL_DIR = $(TMP_DIR)/mod +MODEL_INSTANCES_DIR = $(MODEL_DIR)/instance SOL_DIR = $(TMP_DIR)/sol ## Sub-programs ################################################################ AST_TO_INSTR = ast-to-instr +INST_CALC = instance-calculator SOLVER = instr-to-kodkod PRETTY_PRINTER = sol-pretty-printer @@ -24,31 +26,37 @@ all: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) compile: $(MAKE) -C $(AST_TO_INSTR) compile + $(MAKE) -C $(INST_CALC) compile $(MAKE) -C $(SOLVER) compile $(MAKE) -C $(PRETTY_PRINTER) compile model: $(MAKE) -C $(AST_TO_INSTR) model + $(MAKE) -C $(INST_CALC) model $(MAKE) -C $(SOLVER) model $(MAKE) -C $(PRETTY_PRINTER) model solutions: $(TMP_DIR) $(MODEL_DIR) $(SOL_DIR) $(MAKE) -C $(AST_TO_INSTR) solutions + $(MAKE) -C $(INST_CALC) solutions $(MAKE) -C $(SOLVER) solutions $(MAKE) -C $(PRETTY_PRINTER) solutions clean: $(MAKE) -C $(AST_TO_INSTR) clean + $(MAKE) -C $(INST_CALC) clean $(MAKE) -C $(SOLVER) clean $(MAKE) -C $(PRETTY_PRINTER) clean clean_model: $(MAKE) -C $(AST_TO_INSTR) clean_model + $(MAKE) -C $(INST_CALC) clean_model $(MAKE) -C $(SOLVER) clean_model $(MAKE) -C $(PRETTY_PRINTER) clean_model clean_solutions: $(MAKE) -C $(AST_TO_INSTR) clean_solutions + $(MAKE) -C $(INST_CALC) clean_solutions $(MAKE) -C $(SOLVER) clean_solutions $(MAKE) -C $(PRETTY_PRINTER) clean_solutions diff --git a/data/level/instances.lvl b/data/level/instances.lvl new file mode 100644 index 0000000..ad6e93f --- /dev/null +++ b/data/level/instances.lvl @@ -0,0 +1,23 @@ +;; Instances + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; TYPES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_type wfm_instance) +(add_type ps_instance) + +;; Redundancies +(add_type entity) +(add_type process) +(add_type waveform) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; PREDICATES DECLARATION ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(add_predicate is_wfm_instance_of wfm_instance waveform) +(add_predicate is_visible_in wfm_instance entity) + +(add_predicate is_ps_instance_of ps_instance process) +(add_predicate is_visible_in ps_instance entity) + +(add_predicate process_instance_maps ps_instance wfm_instance waveform) diff --git a/data/property/simple_flip_flop.pro b/data/property/simple_flip_flop.pro index e1621c1..b054c7f 100644 --- a/data/property/simple_flip_flop.pro +++ b/data/property/simple_flip_flop.pro @@ -5,6 +5,7 @@ (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) ) (and + (not (eq clk reg)) (is_explicit_process ps) (is_in_sensitivity_list clk ps) (CTL_verifies ps diff --git a/data/property/test-case/fast.pp b/data/property/test-case/fast.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/fast.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/fast.pro b/data/property/test-case/fast.pro new file mode 100644 index 0000000..10bc135 --- /dev/null +++ b/data/property/test-case/fast.pro @@ -0,0 +1,57 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (kind "if") + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/data/property/test-case/slow.pp b/data/property/test-case/slow.pp new file mode 100644 index 0000000..b460eec --- /dev/null +++ b/data/property/test-case/slow.pp @@ -0,0 +1,6 @@ +The component described by the entity $ent.IDENTIFIER$ (declared in $ent.FILE$, +line $ent.LINE$, column $ent.COLUMN$) has a simple flip-flop described by the +process $ps.LABEL$ (declared in $ps.FILE$, l. $ps.LINE$, c. $ps.COLUMN$), +controlled by $clk.IDENTIFIER$ (declared in $clk.FILE$, l. $clk.LINE$, +c. $clk.COLUMN$), and with output $reg.IDENTIFIER$ (declared in $reg.FILE$, +l. $reg.LINE$, c. $reg.COLUMN$). diff --git a/data/property/test-case/slow.pro b/data/property/test-case/slow.pro new file mode 100644 index 0000000..2566a6f --- /dev/null +++ b/data/property/test-case/slow.pro @@ -0,0 +1,60 @@ +(tag_existing + ( + (ent entity STRUCT_ENTITY) + (reg waveform STRUCT_SIMPLE_FLIP_FLOP_OUTPUT) + (clk waveform STRUCT_SIMPLE_FLIP_FLOP_CLOCK) + (ps process STRUCT_SIMPLE_FLIP_FLOP_PROCESS) + ) + (and + (not (eq reg clk)) + (is_explicit_process ps) + ;; debt: )) + ;; Get ps instance + (exists i_ps ps_instance + (and + (is_visible_in i_ps ent) + (is_ps_instance_of i_ps ps) + ;; debt: )) )) + ;; Get a local waveform matching a clk instance + (exists i_clk wfm_instance + (and + (process_instance_maps i_ps i_clk _) + ;; (is_visible_in i_clk ent) + (is_wfm_instance_of i_clk clk) + (exists local_clk waveform + (and + (process_instance_maps i_ps i_clk local_clk) + (is_in_sensitivity_list local_clk ps) + ;; debt: )))) )))) + ;; Get a local waveform matching a reg instance + (exists i_reg wfm_instance + (and + (process_instance_maps i_ps i_reg _) + ;; (is_visible_in i_reg ent) + (is_wfm_instance_of i_reg reg) + (exists local_reg waveform + (and + (process_instance_maps i_ps i_reg local_reg) + ;; debt: )))) )))))))) + ;; Analyze ps using the local waveforms + (CTL_verifies ps + (AF + ;; using local_clk or local_reg here makes the property take forever to verify.... + (and + (kind "if") + (is_read_element "1" local_clk) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) + ) +) diff --git a/instance-calculator/Makefile b/instance-calculator/Makefile new file mode 100644 index 0000000..9dddc88 --- /dev/null +++ b/instance-calculator/Makefile @@ -0,0 +1,75 @@ +## Parameters ################################################################## +#### Where to find the model +ifndef MODEL_DIR +MODEL_DIR = +endif + +#### Where to store the Instance model +ifndef MODEL_INSTANCES_DIR +MODEL_INSTANCES_DIR = +endif + +#### Binaries +###### JRE binary +ifndef JAVA +JAVA = java +endif + +###### JDK binary +ifndef JAVAC +JAVAC = javac +endif + +## Parameters Sanity Check ##################################################### +ifeq ($(strip $(MODEL_DIR)),) +$(error No MODEL_DIR defined as parameter.) +endif + +ifeq ($(strip $(MODEL_INSTANCES_DIR)),) +$(error No MODEL_INSTANCES_DIR defined as parameter.) +endif + +ifeq ($(strip $(JAVA)),) +$(error No Java executable defined as parameter.) +endif + +ifeq ($(strip $(JAVAC)),) +$(error No Java compiler defined as parameter.) +endif + +################################################################################ +CLASSPATH = "./src/" + +## Makefile Magic ############################################################## +SOURCES = $(wildcard src/*.java) +CLASSES = $(SOURCES:.java=.class) +MODEL_FILE = $(MODEL_DIR)/structural.mod +OUTPUT_FILE = $(MODEL_INSTANCES_DIR)/witness + +## Makefile Rules ############################################################## +compile: $(CLASSES) + +model: $(CLASSES) $(MODEL_INSTANCES_DIR) $(OUTPUT_FILE) + +solutions: + +clean: + rm -f $(CLASSES) + rm -f $(MODEL_INSTANCES_DIR)/* + +clean_model: + rm -f $(MODEL_INSTANCES_DIR)/* + +clean_solutions: + +######## +%.class: %.java + $(JAVAC) -cp $(CLASSPATH) $< + +$(OUTPUT_FILE): $(MODEL_FILE) $(CLASSES) + $(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) "inst_" $(MODEL_INSTANCES_DIR) + touch $(OUTPUT_FILE) + +$(MODEL_INSTANCES_DIR): + mkdir -p $(MODEL_INSTANCES_DIR) + diff --git a/instance-calculator/src/.java_classpath b/instance-calculator/src/.java_classpath new file mode 100644 index 0000000..5e14ac9 --- /dev/null +++ b/instance-calculator/src/.java_classpath @@ -0,0 +1 @@ +../kodkod.jar diff --git a/instance-calculator/src/Main.java b/instance-calculator/src/Main.java new file mode 100644 index 0000000..b66a63b --- /dev/null +++ b/instance-calculator/src/Main.java @@ -0,0 +1,121 @@ +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Deque; + +import java.io.FileWriter; + +public class Main +{ + private static Parameters PARAMETERS; + + public static void main (final String... args) + { + final FileWriter output; + + PARAMETERS = new Parameters(args); + + if (!PARAMETERS.are_valid()) + { + return; + } + + try + { + ModelFile.load_file(PARAMETERS.get_model_file()); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not load model file \"" + + PARAMETERS.get_model_file() + + "\":" + ); + + e.printStackTrace(); + + return; + } + + create_instances(); + OutputFile.close_all(); + } + + private static void create_instances () + { + final Collection<VHDLEntity> futur_candidates; + final Deque<VHDLEntity> candidates; + final Collection<VHDLEntity> processed_candidates; + boolean is_stuck; + + futur_candidates = new ArrayList<VHDLEntity>(); + candidates = new ArrayDeque<VHDLEntity>(); + processed_candidates = new ArrayList<VHDLEntity>(); + + futur_candidates.addAll(VHDLEntity.get_all()); + + while (!futur_candidates.isEmpty()) + { + is_stuck = true; + + candidates.addAll(futur_candidates); + futur_candidates.clear(); + + while (!candidates.isEmpty()) + { + final VHDLEntity e; + boolean is_ready; + + e = candidates.pop(); + + is_ready = true; + + for (final VHDLComponent cmp: e.get_architecture().get_components()) + { + if (!processed_candidates.contains(cmp.get_destination())) + { + is_ready = false; + + break; + } + } + + if (is_ready) + { + is_stuck = false; + + e.generate_instance(); + + e.write_predicates(); + processed_candidates.add(e); + } + else + { + futur_candidates.add(e); + } + } + + if (is_stuck) + { + System.err.println("[F] Unable to create all the instances..."); + System.err.println + ( + "[E] The following entites might form a circular dependency:" + ); + + for (final VHDLEntity e: futur_candidates) + { + System.err.println("[E] Entity " + e.get_id()); + } + + System.exit(-1); + } + } + } + + public static Parameters get_parameters () + { + return PARAMETERS; + } +} diff --git a/instance-calculator/src/ModelFile.java b/instance-calculator/src/ModelFile.java new file mode 100644 index 0000000..be84674 --- /dev/null +++ b/instance-calculator/src/ModelFile.java @@ -0,0 +1,310 @@ +import java.io.IOException; +import java.io.FileNotFoundException; + +public class ModelFile +{ + public static boolean load_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("is_accessed_by")) + { + success = handle_is_accessed_by(input); + } + else if (input[0].equals("is_waveform_of")) + { + success = handle_is_waveform_of(input); + } + else if (input[0].equals("is_port_of")) + { + success = handle_is_port_of(input); + } + else if (input[0].equals("is_architecture_of")) + { + success = handle_is_architecture_of(input); + } + else if (input[0].equals("belongs_to_architecture")) + { + success = handle_belongs_to_architecture(input); + } + else if (input[0].equals("is_component_of")) + { + success = handle_is_component_of(input); + } + else if (input[0].equals("port_maps")) + { + success = handle_port_maps(input); + } + else + { + continue; + } + + 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; + } + } + + VHDLArchitecture.resolve_all_waveforms(); + + return true; + } + + private static boolean handle_add_element + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + if (input[1].equals("entity")) + { + VHDLEntity.add_element(input[2]); + } + else if (input[1].equals("architecture")) + { + VHDLArchitecture.add_element(input[2]); + } + else if (input[1].equals("waveform")) + { + VHDLWaveform.add_element(input[2]); + } + else if (input[1].equals("process")) + { + VHDLProcess.add_element(input[2]); + } + else if (input[1].equals("component")) + { + VHDLComponent.add_element(input[2]); + } + + return true; + } + + private static boolean handle_is_accessed_by + ( + final String[] input + ) + { + final VHDLProcess ps; + final VHDLWaveform wfm; + + if (input.length != 3) + { + return false; + } + + ps = VHDLProcess.get_from_id(input[2]); + wfm = VHDLWaveform.find(input[1]); + + if (wfm != null) + { + /* + * Assumes that otherwise it's a string, but that could also be due to + * an inconsistent model. + */ + + ps.add_accessed_wfm(wfm); + } + + return true; + } + + private static boolean handle_is_waveform_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + Waveforms.register_map(input[1], input[2]); + + return true; + } + + private static boolean handle_is_port_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLEntity.get_from_id(input[2]).add_port(input[1]); + + return true; + } + + private static boolean handle_is_architecture_of + ( + final String[] input + ) + { + final VHDLEntity e; + final VHDLArchitecture arch; + + if (input.length != 3) + { + return false; + } + + e = VHDLEntity.get_from_id(input[2]); + arch = VHDLArchitecture.get_from_id(input[1]); + + e.set_architecture(arch); + arch.set_entity(e); + + return true; + } + + private static boolean handle_belongs_to_architecture + ( + final String[] input + ) + { + final VHDLArchitecture arch; + final VHDLProcess ps; + final VHDLComponent cmp; + + if (input.length != 3) + { + return false; + } + + arch = VHDLArchitecture.get_from_id(input[2]); + + ps = VHDLProcess.find(input[1]); + + if (ps != null) + { + arch.add_process(ps); + ps.set_architecture(arch); + + return true; + } + + cmp = VHDLComponent.find(input[1]); + + if (cmp != null) + { + arch.add_component(cmp); + cmp.set_architecture(arch); + + return true; + } + + arch.add_futur_waveform(input[1]); + + return true; + } + + private static boolean handle_is_component_of + ( + final String[] input + ) + { + if (input.length != 3) + { + return false; + } + + VHDLComponent.get_from_id(input[1]).set_destination + ( + VHDLEntity.get_from_id(input[2]) + ); + + return true; + } + + private static boolean handle_port_maps + ( + final String[] input + ) + { + if (input.length != 4) + { + return false; + } + + VHDLComponent.get_from_id(input[1]).add_port_map + ( + input[2], + input[3] + ); + + return true; + } + + private ModelFile () {} /* Utility Class */ +} diff --git a/instance-calculator/src/OutputFile.java b/instance-calculator/src/OutputFile.java new file mode 100644 index 0000000..201ca2b --- /dev/null +++ b/instance-calculator/src/OutputFile.java @@ -0,0 +1,135 @@ +import java.util.ArrayList; +import java.util.Collection; + +import java.io.File; +import java.io.FileWriter; +import java.io.BufferedWriter; + +public class OutputFile +{ + private static Collection<OutputFile> ALL_OUTPUT_FILES; + + static + { + ALL_OUTPUT_FILES = new ArrayList<OutputFile>(); + } + + public static void close_all () + { + for (final OutputFile f: ALL_OUTPUT_FILES) + { + f.close(); + } + } + + public static OutputFile new_output_file (final String filename) + { + final OutputFile result; + + result = + new OutputFile + ( + Main.get_parameters().get_output_directory() + + "/" + + filename + ); + + ALL_OUTPUT_FILES.add(result); + + return result; + } + + /** Non-Static *************************************************************/ + private final String filename; + private final BufferedWriter buffered_writer; + + private OutputFile (final String filename) + { + BufferedWriter bf; + + this.filename = filename; + + try + { + bf = new BufferedWriter(new FileWriter(new File(filename))); + } + catch (final Exception e) + { + bf = null; + + System.err.println + ( + "[F] Could not create new output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + + buffered_writer = bf; + } + + public void write (final String data) + { + try + { + buffered_writer.write(data); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + public void insert_newline () + { + try + { + buffered_writer.newLine(); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + private void close () + { + try + { + buffered_writer.close(); + } + catch (final Exception e) + { + System.err.println + ( + "[E] Could not properly close output file \"" + + filename + + "\":" + ); + + e.printStackTrace(); + } + } +} diff --git a/instance-calculator/src/Parameters.java b/instance-calculator/src/Parameters.java new file mode 100644 index 0000000..b8bba30 --- /dev/null +++ b/instance-calculator/src/Parameters.java @@ -0,0 +1,64 @@ +public class Parameters +{ + private final String model_file; + private final String id_prefix; + private final String output_dir; + private final boolean are_valid; + + public static void print_usage () + { + System.out.println + ( + "Instance-Calculator\n" + + "USAGE:\n" + + "\tjava Main <INSTRUCTIONS> <ID_PREFIX> <OUTPUT_DIR>\n" + + "PARAMETERS:\n" + + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n" + + "\t<ID_PREFIX>\tPrefix for the IDs of generated paths.\n" + + "\t<OUTPUT_DIR>\tDirectory in which to output the generated" + + " instruction files." + ); + } + + public Parameters (final String... args) + { + if (args.length != 3) + { + print_usage(); + + model_file = new String(); + id_prefix = new String(); + output_dir = new String(); + + are_valid = false; + } + else + { + model_file = args[0]; + id_prefix = args[1]; + output_dir = args[2]; + + are_valid = true; + } + } + + public String get_model_file () + { + return model_file; + } + + public String get_id_prefix () + { + return id_prefix; + } + + public String get_output_directory () + { + return output_dir; + } + + public boolean are_valid () + { + return are_valid; + } +} diff --git a/instance-calculator/src/QuickParser.java b/instance-calculator/src/QuickParser.java new file mode 100644 index 0000000..383373e --- /dev/null +++ b/instance-calculator/src/QuickParser.java @@ -0,0 +1,62 @@ +import java.io.BufferedReader; +import java.io.FileReader; +import java.io.IOException; +import java.io.FileNotFoundException; + +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class QuickParser +{ + private static final Pattern instr_pattern; + private final BufferedReader buffered_reader; + + static + { + instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)"); + } + public QuickParser (final String filename) + throws FileNotFoundException + { + buffered_reader = new BufferedReader(new FileReader(filename)); + } + + public void finalize () + throws IOException + { + buffered_reader.close(); + } + + public String[] parse_line () + throws IOException + { + final List<String> result; + final Matcher matcher; + String line; + + do + { + line = buffered_reader.readLine(); + + if (line == null) + { + return new String[0]; + } + + line = line.replaceAll("\\s+"," "); + } + while (line.length() < 3 || line.startsWith(";")); + + matcher = instr_pattern.matcher(line); + + if (!matcher.find()) + { + System.err.println("[E] Invalid instruction \"" + line + "\""); + + return null; + } + + return matcher.group(1).split(" |\t"); + } +} diff --git a/instance-calculator/src/VHDLArchitecture.java b/instance-calculator/src/VHDLArchitecture.java new file mode 100644 index 0000000..a3aa7ac --- /dev/null +++ b/instance-calculator/src/VHDLArchitecture.java @@ -0,0 +1,179 @@ +import java.util.ArrayDeque; +import java.util.ArrayList; +import java.util.Collection; +import java.util.Deque; +import java.util.Map; +import java.util.HashMap; + +public class VHDLArchitecture +{ + private static final Map<String, VHDLArchitecture> FROM_ID; + + static + { + FROM_ID = new HashMap<String, VHDLArchitecture>(); + } + + public static void resolve_all_waveforms () + { + for (final VHDLArchitecture arch: FROM_ID.values()) + { + arch.resolve_waveforms(); + } + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLArchitecture(id)); + } + } + + public static VHDLArchitecture get_from_id (final String id) + { + final VHDLArchitecture result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like an architecture, but is not declared as such" + + " before that use." + ); + + System.exit(-1); + } + + return result; + } + + public static VHDLArchitecture find (final String id) + { + return FROM_ID.get(id); + } + +/******************************************************************************/ + private final Collection<VHDLProcess> processes; + private final Collection<VHDLComponent> components; + private final Collection<VHDLWaveform> waveforms; + private final Deque<String> futur_waveforms; + private final String id; + + private VHDLEntity entity; + + private VHDLArchitecture (final String id) + { + this.id = id; + + processes = new ArrayList<VHDLProcess>(); + components = new ArrayList<VHDLComponent>(); + waveforms = new ArrayList<VHDLWaveform>(); + futur_waveforms = new ArrayDeque<String>(); + } + + public VHDLEntity get_entity () + { + return entity; + } + + public void set_entity (final VHDLEntity e) + { + entity = e; + } + + public void add_process (final VHDLProcess ps) + { + if (!processes.contains(ps)) + { + processes.add(ps); + } + } + + public void add_component (final VHDLComponent cmp) + { + if (!components.contains(cmp)) + { + components.add(cmp); + } + } + + public Collection<VHDLComponent> get_components () + { + return components; + } + + public void add_waveform (final VHDLWaveform wfm) + { + if (!waveforms.contains(wfm)) + { + waveforms.add(wfm); + } + } + + public void add_futur_waveform (final String fwfm) + { + if (!futur_waveforms.contains(fwfm)) + { + futur_waveforms.add(fwfm); + } + } + + public void resolve_waveforms () + { + while (!futur_waveforms.isEmpty()) + { + final String src_id, wfm_id; + + src_id = futur_waveforms.pop(); + + wfm_id = Waveforms.get_waveform_id_from_id(src_id); + add_waveform(VHDLWaveform.get_from_id(wfm_id)); + } + } + + public void add_instance_to + ( + final Collection<VHDLProcess.Instance> process_instances, + final Collection<VHDLWaveform.Instance> waveform_instances, + final Map<VHDLWaveform, VHDLWaveform.Instance> local_conversion + ) + { + for (final VHDLWaveform wfm: waveforms) + { + final VHDLWaveform.Instance i_wfm; + + i_wfm = wfm.add_instance(entity); + + waveform_instances.add(i_wfm); + + local_conversion.put(wfm, i_wfm); + } + + for (final VHDLProcess ps: processes) + { + process_instances.add + ( + ps.generate_base_instance + ( + entity, + waveform_instances + ) + ); + } + + for (final VHDLComponent cmp: components) + { + cmp.add_instance_content_to + ( + process_instances, + waveform_instances, + local_conversion + ); + } + } +} diff --git a/instance-calculator/src/VHDLComponent.java b/instance-calculator/src/VHDLComponent.java new file mode 100644 index 0000000..76b1dc9 --- /dev/null +++ b/instance-calculator/src/VHDLComponent.java @@ -0,0 +1,146 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; + +public class VHDLComponent +{ + private static final Map<String, VHDLComponent> FROM_ID; + + static + { + FROM_ID = new HashMap<String, VHDLComponent>(); + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLComponent(id)); + } + } + + public static VHDLComponent get_from_id (final String id) + { + final VHDLComponent result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a component instantiation, but is not declared as" + + " such before that use." + ); + + System.exit(-1); + } + + return result; + } + + public static VHDLComponent find (final String id) + { + return FROM_ID.get(id); + } + +/******************************************************************************/ + private final Map<String, String> reverse_port_map; + private final String id; + + private VHDLEntity destination; + private VHDLArchitecture parent; + + public void set_destination (final VHDLEntity dest) + { + destination = dest; + } + + public VHDLEntity get_destination () + { + return destination; + } + + public void set_architecture (final VHDLArchitecture arch) + { + parent = arch; + } + + public void add_port_map (final String src, final String dest) + { + reverse_port_map.put(dest, src); + } + + public void add_instance_content_to + ( + final Collection<VHDLProcess.Instance> process_instances, + final Collection<VHDLWaveform.Instance> waveform_instances, + final Map<VHDLWaveform, VHDLWaveform.Instance> local_conversion + ) + { + final Collection<VHDLProcess.Instance> dest_process_instances; + final Collection<VHDLWaveform.Instance> dest_waveform_instances; + final Map<VHDLWaveform.Instance, VHDLWaveform.Instance> wfm_map; + + dest_process_instances = destination.get_process_instances(); + dest_waveform_instances = destination.get_waveform_instances(); + + wfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform.Instance>(); + + for (final VHDLWaveform.Instance i_wfm: dest_waveform_instances) + { + final String src_wfm, dest_port; + final VHDLWaveform.Instance replacement; + + dest_port = + Waveforms.get_id_from_waveform_id + ( + i_wfm.get_parent().get_id() + ); + + src_wfm = reverse_port_map.get(dest_port); + + if (src_wfm == null) + { + /* i_wfm is not linked to a port, so it needs a new instance. */ + replacement = i_wfm.get_parent().add_instance(parent.get_entity()); + } + else + { + /* + * i_wfm is linked to a port. Replace it by what's connected to the + * port. + */ + replacement = + local_conversion.get + ( + VHDLWaveform.get_from_id + ( + src_wfm + ) + ); + } + + wfm_map.put(i_wfm, replacement); + waveform_instances.add(replacement); + } + + for (final VHDLProcess.Instance i_ps: dest_process_instances) + { + process_instances.add + ( + i_ps.add_instance(parent.get_entity(), wfm_map) + ); + } + } + + private VHDLComponent (final String id) + { + this.id = id; + + reverse_port_map = new HashMap<String, String>(); + } +} diff --git a/instance-calculator/src/VHDLEntity.java b/instance-calculator/src/VHDLEntity.java new file mode 100644 index 0000000..d2a8e07 --- /dev/null +++ b/instance-calculator/src/VHDLEntity.java @@ -0,0 +1,150 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; + +public class VHDLEntity +{ + private static final Map<String, VHDLEntity> FROM_ID; + + static + { + FROM_ID = new HashMap<String, VHDLEntity>(); + } + + public static Collection<VHDLEntity> get_all () + { + return FROM_ID.values(); + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLEntity(id)); + } + } + + public static VHDLEntity get_from_id (final String id) + { + final VHDLEntity result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like an entity, but is not declared as such before that" + + " use." + ); + + System.exit(-1); + } + + return result; + } + + public static VHDLEntity find (final String id) + { + return FROM_ID.get(id); + } + +/******************************************************************************/ + private final Collection<VHDLProcess.Instance> process_instances; + private final Collection<VHDLWaveform.Instance> waveform_instances; + + private final OutputFile output_file; + private final Collection<String> ports; + private final String id; + + private VHDLArchitecture architecture; + + private VHDLEntity (final String id) + { + this.id = id; + ports = new ArrayList<String>(); + + architecture = null; + + this.process_instances = new ArrayList<VHDLProcess.Instance>(); + this.waveform_instances = new ArrayList<VHDLWaveform.Instance>(); + + output_file = OutputFile.new_output_file("instances_in_" + id + ".mod"); + } + + public String get_id () + { + return id; + } + + public void add_port (final String pt) + { + if (!ports.contains(pt)) + { + ports.add(pt); + } + } + + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; + } + + public VHDLArchitecture get_architecture () + { + return architecture; + } + + public Collection<VHDLProcess.Instance> get_process_instances () + { + return process_instances; + } + + public Collection<VHDLWaveform.Instance> get_waveform_instances () + { + return waveform_instances; + } + + public void generate_instance () + { + final Map<VHDLWaveform, VHDLWaveform.Instance> local_conversion; + + local_conversion = new HashMap<VHDLWaveform, VHDLWaveform.Instance>(); + + for (final String pt: ports) + { + final VHDLWaveform wfm; + final VHDLWaveform.Instance i_wfm; + + wfm = VHDLWaveform.get_from_id(Waveforms.get_waveform_id_from_id(pt)); + i_wfm = wfm.add_instance(this); + + waveform_instances.add(i_wfm); + + local_conversion.put(wfm, i_wfm); + } + + architecture.add_instance_to + ( + process_instances, + waveform_instances, + local_conversion + ); + } + + public void write_predicates () + { + for (final VHDLWaveform.Instance iwfm: waveform_instances) + { + iwfm.write_predicates_to(output_file); + } + + for (final VHDLProcess.Instance ips: process_instances) + { + ips.write_predicates_to(output_file); + } + } +} diff --git a/instance-calculator/src/VHDLProcess.java b/instance-calculator/src/VHDLProcess.java new file mode 100644 index 0000000..a4f150e --- /dev/null +++ b/instance-calculator/src/VHDLProcess.java @@ -0,0 +1,253 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; +import java.util.Set; + +public class VHDLProcess +{ + private static final Map<String, VHDLProcess> FROM_ID; + + static + { + FROM_ID = new HashMap<String, VHDLProcess>(); + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLProcess(id)); + } + } + + public static VHDLProcess get_from_id (final String id) + { + final VHDLProcess result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a process, but is not declared as such before that" + + " use." + ); + + System.exit(-1); + } + + return result; + } + + public static VHDLProcess find (final String id) + { + return FROM_ID.get(id); + } + +/******************************************************************************/ + private final Collection<VHDLWaveform> accessed_wfm; + private final Collection<VHDLProcess.Instance> instances; + private final String id; + private int instances_count; + + private VHDLArchitecture architecture; + + private VHDLProcess (final String id) + { + this.id = id; + accessed_wfm = new ArrayList<VHDLWaveform>(); + instances = new ArrayList<VHDLProcess.Instance>(); + instances_count = 0; + architecture = null; + } + + public String get_id () + { + return id; + } + + public void add_accessed_wfm (final VHDLWaveform wfm) + { + if (!accessed_wfm.contains(wfm)) + { + accessed_wfm.add(wfm); + } + } + + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; + } + + public VHDLProcess.Instance generate_base_instance + ( + final VHDLEntity visibility, + final Collection<VHDLWaveform.Instance> waveform_instances + ) + { + final VHDLProcess.Instance result; + final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map; + + iwfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform>(); + + for (final VHDLWaveform.Instance i_wfm: waveform_instances) + { + if (accessed_wfm.contains(i_wfm.get_parent())) + { + iwfm_map.put(i_wfm, i_wfm.get_parent()); + } + } + + result = + new VHDLProcess.Instance + ( + this, + visibility, + iwfm_map + ); + + instances_count += 1; + + return result; + } + + public static class Instance + { + private static int instances_count; + + static + { + instances_count = 0; + } + + private final String id; + private final VHDLProcess parent; + private final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map; + private final VHDLEntity visibility; + + private Instance + ( + final VHDLProcess parent, + final VHDLEntity visibility, + final Map<VHDLWaveform.Instance, VHDLWaveform> iwfm_map + ) + { + this.id = + ( + Main.get_parameters().get_id_prefix() + + "ps_" + + instances_count + ); + + instances_count += 1; + + this.parent = parent; + this.visibility = visibility; + this.iwfm_map = iwfm_map; + } + + public VHDLProcess get_parent () + { + return parent; + } + + public VHDLProcess.Instance add_instance + ( + final VHDLEntity visibility, + final Map<VHDLWaveform.Instance, VHDLWaveform.Instance> convertion + ) + { + final VHDLProcess.Instance result; + final Set<Map.Entry<VHDLWaveform.Instance, VHDLWaveform>> iwfm_set; + final Map<VHDLWaveform.Instance, VHDLWaveform> new_iwfm_map; + + iwfm_set = iwfm_map.entrySet(); + + new_iwfm_map = new HashMap<VHDLWaveform.Instance, VHDLWaveform>(); + + for + ( + final Map.Entry<VHDLWaveform.Instance, VHDLWaveform> me: iwfm_set + ) + { + new_iwfm_map.put + ( + convertion.get(me.getKey()), + me.getValue() + ); + } + + result = + new VHDLProcess.Instance + ( + parent, + visibility, + new_iwfm_map + ); + + parent.instances_count += 1; + + return result; + } + + public void write_predicates_to (final OutputFile of) + { + final Set<Map.Entry<VHDLWaveform.Instance, VHDLWaveform>> iwfm_set; + + iwfm_set = iwfm_map.entrySet(); + + try + { + of.write("(add_element ps_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_ps_instance_of "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(")"); + of.insert_newline(); + + of.write("(is_visible_in "); + of.write(id); + of.write(" "); + of.write(visibility.get_id()); + of.write(")"); + of.insert_newline(); + + for + ( + final Map.Entry<VHDLWaveform.Instance, VHDLWaveform> iwfm: + iwfm_set + ) + { + of.write("(process_instance_maps "); + of.write(id); + of.write(" "); + of.write(iwfm.getKey().get_id()); + of.write(" "); + of.write(iwfm.getValue().get_id()); + of.write(")"); + of.insert_newline(); + } + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file:" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + } +} diff --git a/instance-calculator/src/VHDLWaveform.java b/instance-calculator/src/VHDLWaveform.java new file mode 100644 index 0000000..feb1e51 --- /dev/null +++ b/instance-calculator/src/VHDLWaveform.java @@ -0,0 +1,190 @@ +import java.util.ArrayList; +import java.util.Collection; +import java.util.Map; +import java.util.HashMap; + +public class VHDLWaveform +{ + private static final Map<String, VHDLWaveform> FROM_ID; + + static + { + FROM_ID = new HashMap<String, VHDLWaveform>(); + } + + public static void add_element (final String id) + { + if (!FROM_ID.containsKey(id)) + { + FROM_ID.put(id, new VHDLWaveform(id)); + } + } + + public static VHDLWaveform get_from_id (final String id) + { + final VHDLWaveform result; + + result = FROM_ID.get(id); + + if (result == null) + { + System.err.println + ( + "[E] Element " + + id + + " is used like a waveform, but is not declared as such before" + + " that use." + ); + + new Exception().printStackTrace(); + + System.exit(-1); + } + + return result; + } + + public static VHDLWaveform find (final String id) + { + return FROM_ID.get(id); + } + +/******************************************************************************/ + private final Collection<String> accessed_wfm; + private final Collection<VHDLWaveform.Instance> instances; + private final String id; + private int instances_count; + + private VHDLArchitecture architecture; + + private VHDLWaveform (final String id) + { + this.id = id; + accessed_wfm = new ArrayList<String>(); + instances = new ArrayList<VHDLWaveform.Instance>(); + instances_count = 0; + architecture = null; + } + + public VHDLWaveform.Instance add_instance + ( + final VHDLEntity visibility + ) + { + final VHDLWaveform.Instance result; + + result = + new VHDLWaveform.Instance + ( + this, + visibility + ); + + instances.add(result); + + instances_count += 1; + + return result; + } + + public String get_id () + { + return id; + } + + public void set_architecture (final VHDLArchitecture arch) + { + architecture = arch; + } + + @Override + public String toString () + { + return id; + } + + public static class Instance + { + private static int instances_count; + + static + { + instances_count = 0; + } + + private final String id; + private final VHDLWaveform parent; + private final VHDLEntity visibility; + + private Instance + ( + final VHDLWaveform parent, + final VHDLEntity visibility + ) + { + this.id = + ( + Main.get_parameters().get_id_prefix() + + "wfm_" + + instances_count + ); + + instances_count += 1; + + this.parent = parent; + this.visibility = visibility; + } + + public String get_id () + { + return id; + } + + public VHDLWaveform get_parent () + { + return parent; + } + + public void write_predicates_to (final OutputFile of) + { + try + { + of.write("(add_element wfm_instance "); + of.write(id); + of.write(")"); + of.insert_newline(); + + of.write("(is_wfm_instance_of "); + of.write(id); + of.write(" "); + of.write(parent.get_id()); + of.write(")"); + of.insert_newline(); + + of.write("(is_visible_in "); + of.write(id); + of.write(" "); + of.write(visibility.get_id()); + of.write(")"); + of.insert_newline(); + } + catch (final Exception e) + { + System.err.println + ( + "[F] Could not write to output file:" + ); + + e.printStackTrace(); + + System.exit(-1); + } + } + + @Override + public String toString () + { + return id; + } + } +} diff --git a/instance-calculator/src/Waveforms.java b/instance-calculator/src/Waveforms.java new file mode 100644 index 0000000..9492d16 --- /dev/null +++ b/instance-calculator/src/Waveforms.java @@ -0,0 +1,74 @@ +import java.util.Map; +import java.util.HashMap; + +public class Waveforms +{ + private static final Map<String, String> FROM_WAVEFORM; + private static final Map<String, String> TO_WAVEFORM; + + static + { + FROM_WAVEFORM = new HashMap<String, String>(); + TO_WAVEFORM = new HashMap<String, String>(); + } + + private Waveforms () {} /* Utility class. */ + + public static void register_map (final String wfm_id, final String elem_id) + { + FROM_WAVEFORM.put(wfm_id, elem_id); + TO_WAVEFORM.put(elem_id, wfm_id); + } + + public static String get_id_from_waveform_id (final String wfm_id) + { + final String result; + + result = FROM_WAVEFORM.get(wfm_id); + + if (result == null) + { + System.err.println + ( + "[F] There is no element associated with waveform \"" + + wfm_id + + "\". Is the model complete?" + ); + + System.exit(-1); + } + + return result; + } + + public static String get_waveform_id_from_id (final String src_id) + { + final String result; + + result = TO_WAVEFORM.get(src_id); + + if (result == null) + { + System.err.println + ( + "[F] There is no waveform associated with the element \"" + + src_id + + "\". Is the model complete?" + ); + + System.exit(-1); + } + + return result; + } + + public static String find_id_from_waveform_id (final String wfm_id) + { + return FROM_WAVEFORM.get(wfm_id); + } + + public static String find_waveform_id_from_id (final String src_id) + { + return TO_WAVEFORM.get(src_id); + } +} diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile index 03e451a..08af039 100644 --- a/instr-to-kodkod/Makefile +++ b/instr-to-kodkod/Makefile @@ -95,7 +95,8 @@ MODEL_FILES = \ $(MODEL_DIR)/structural.mod \ $(MODEL_DIR)/depths.mod \ $(MODEL_DIR)/string_to_instr.map \ - $(filter-out %structural.mod,$(wildcard $(MODEL_DIR)/cfg_*.mod)) + $(wildcard $(MODEL_DIR)/cfg_*.mod) \ + $(wildcard $(MODEL_INSTANCES_DIR)/*.mod) PARSER_SOURCES = $(wildcard parser/*.g4) PARSER_CLASSES = $(PARSER_SOURCES:.g4=.class) @@ -106,7 +107,8 @@ compile: $(PARSER_CLASSES) $(CLASSES) model: cfg-generator -solutions: cfg-generator $(PARSER_CLASSES) $(CLASSES) $(SOLUTION_FILES) +solutions: cfg-generator $(REQUIRED_JARS) $(PARSER_CLASSES) $(CLASSES) \ + $(SOLUTION_FILES) clean: $(MAKE) -C parser clean |