summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--data/template/test.pp2
-rw-r--r--prop-to-pred/Makefile81
-rw-r--r--prop-to-pred/src/ParserEntry.java173
4 files changed, 256 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index e8242d7..a45b11d 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ AST_TO_INSTR ?= ast-to-instr
INST_CALC ?= instance-calculator
SOLVER ?= instr-to-kodkod
PRETTY_PRINTER ?= sol-pretty-printer
-PROP_TO_PRED ?= prop_to_pred
+PROP_TO_PRED ?= prop-to-pred
export
diff --git a/data/template/test.pp b/data/template/test.pp
index 4ce45d7..28a3b89 100644
--- a/data/template/test.pp
+++ b/data/template/test.pp
@@ -1 +1 @@
-$ps.LABEL$ is suspicious.
+Process $ps.LABEL$ was tagged by the 'test' property.
diff --git a/prop-to-pred/Makefile b/prop-to-pred/Makefile
new file mode 100644
index 0000000..bb48bfe
--- /dev/null
+++ b/prop-to-pred/Makefile
@@ -0,0 +1,81 @@
+## Parameters ##################################################################
+TO_PRED_TEMPLATE_DIR ?=
+INFERRED_LEVEL_FILE ?=
+PARSING_SCRIPT ?= java -cp "./src" ParserEntry
+PROPERTIES_DIR ?=
+#### Where to find the properties to verify
+ALL_PROPERTY_FILES ?= $(wildcard $(PROPERTIES_DIR)/*.pro)
+
+#### Binaries
+###### JRE binary
+JAVA ?= java
+
+###### JDK binary
+JAVAC ?= javac
+
+## Parameters Sanity Check #####################################################
+ifeq ($(strip $(PARSING_SCRIPT)),)
+$(error No PARSING_SCRIPT 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)
+
+PRED_TO_INFER = \
+ $(addsuffix .pp,$(addprefix $(TO_PRED_TEMPLATE_DIR)/,$(notdir $(basename $(ALL_PROPERTY_FILES)))))
+ADDITIONAL_MAKEFILES = \
+ $(addsuffix .deps,$(addprefix $(DEPENDENCIES_DIR)/,$(basename $(notdir $(ALL_PROPERTY_FILES)))))
+
+export
+## Makefile Rules ##############################################################
+compile: $(CLASSES) $(PRED_TO_INFER) $(ADDITIONAL_MAKEFILES)
+
+model:
+
+solutions:
+
+clean:
+ rm -f $(CLASSES)
+ rm -f $(TO_PRED_TEMPLATE_DIR)/*
+ rm -f $(INFERRED_LEVEL_FILE)
+
+clean_model:
+
+clean_solutions:
+ rm -f $(TO_PRED_TEMPLATE_DIR)/*
+ rm -f $(INFERRED_LEVEL_FILE)
+
+########
+$(TO_PRED_TEMPLATE_DIR)/%.pp: $(PROPERTIES_DIR)/%.pro
+ cat $< | sed 's/.*;;.*//g' | tr -d "\n\r" \
+ | sed -n 's/.*(tag_existing[ \t]\+([ \t]*\(\([ \t]*([^)]\+)\)\+\)[ \t]*.*)/\1/p' \
+ | sed 's/)/)\n/g' | sed 's/[ \t]\+/ /g' | tr -d "()" \
+ | $(PARSING_SCRIPT) \
+ $(patsubst %.pp,%,$(notdir $(basename $@))) \
+ $@ \
+ $(INFERRED_LEVEL_FILE)
+ $(MAKE) $(DEPENDENCIES_DIR)/$(patsubst %.pp,%,$(notdir $(basename $@))).deps
+
+$(DEPENDENCIES_DIR)/%.deps: $(PROPERTIES_DIR)/%.pro
+ printf "$(SOL_DIR)/$(notdir $(basename $@)).sol.ready: " > $@
+ for dep in `sed -n 's/^#require \"\(.*\)\"$$/\1/p' $<` ; do \
+ printf "$(SOL_DIR)/$$dep.sol " >> $@ ; \
+ done
+ printf "\n\t touch $(SOL_DIR)/$(notdir $(basename $@)).sol.ready\n\n" >> $@
+
+
+########
+%.class: %.java
+ $(JAVAC) -cp $(CLASSPATH) $<
diff --git a/prop-to-pred/src/ParserEntry.java b/prop-to-pred/src/ParserEntry.java
new file mode 100644
index 0000000..f10baf0
--- /dev/null
+++ b/prop-to-pred/src/ParserEntry.java
@@ -0,0 +1,173 @@
+import java.io.BufferedWriter;
+import java.io.FileWriter;
+import java.io.File;
+import java.io.IOException;
+
+import java.util.List;
+import java.util.ArrayList;
+import java.util.Scanner;
+
+public class ParserEntry
+{
+ private static final List<ParserEntry> ALL_ENTRIES;
+ private static String predicate_name;
+ private static String output_template_filename;
+ private static BufferedWriter output_template_file;
+ private static String inferred_level_filename;
+ private static BufferedWriter inferred_level_file;
+
+ static
+ {
+ ALL_ENTRIES = new ArrayList<ParserEntry>();
+ }
+
+ private static int parse_arguments (final String args[])
+ {
+ if (args.length != 3)
+ {
+ System.err.println
+ (
+ "usage: java ParserEntry <predicate_name> <output_template_filename>"
+ + " inferred_level_filename"
+ );
+
+ return -1;
+ }
+
+ predicate_name = args[0];
+ output_template_filename = args[1];
+ inferred_level_filename = args[2];
+
+ return 0;
+ }
+
+ private static void parse_file ()
+ throws IOException
+ {
+ final Scanner s;
+
+ s = new Scanner(System.in);
+
+ while (s.hasNextLine())
+ {
+ final String line;
+ final String[] line_data;
+ final ParserEntry p;
+
+ line = s.nextLine().trim();
+
+ line_data = line.replaceAll("\\s+", " ").split(" ");
+
+ p = new ParserEntry(line_data[0].trim(), line_data[1].trim());
+
+ ALL_ENTRIES.add(p);
+
+ inferred_level_file.write("(add_type ");
+ inferred_level_file.write(p.get_var_type());
+ inferred_level_file.write(")\n");
+ }
+ /*/while */
+
+ inferred_level_file.write("(add_predicate _");
+ inferred_level_file.write(predicate_name);
+
+ for (final ParserEntry pe: ALL_ENTRIES)
+ {
+ inferred_level_file.write(" ");
+ inferred_level_file.write(pe.get_var_type());
+ }
+
+ inferred_level_file.write(")\n");
+ }
+
+ private static void create_template ()
+ throws IOException
+ {
+ final StringBuilder sb;
+
+ sb = new StringBuilder();
+
+ for (final ParserEntry pe: ALL_ENTRIES)
+ {
+ final String new_id;
+
+ if (pe.get_var_type().equals("waveform"))
+ {
+ new_id = ("$" + pe.get_var_name() + ".WFM_ID$");
+ }
+ else
+ {
+ new_id = ("$" + pe.get_var_name() + ".ID$");
+ }
+
+ sb.append(" ");
+ sb.append(new_id);
+
+ output_template_file.write("(add_element ");
+ output_template_file.write(pe.get_var_type());
+ output_template_file.write(" ");
+ output_template_file.write(new_id);
+ output_template_file.write(")\n");
+ }
+
+ output_template_file.write("(_");
+ output_template_file.write(predicate_name);
+ output_template_file.write(sb.toString());
+ output_template_file.write(")\n");
+ }
+
+ public static void main (final String args[])
+ throws IOException
+ {
+ File f;
+
+ if (parse_arguments(args) < 0)
+ {
+ System.exit(-1);
+ }
+
+ f = new File(output_template_filename);
+
+ if (!f.exists())
+ {
+ f.createNewFile();
+ }
+
+ output_template_file = new BufferedWriter(new FileWriter(f));
+
+ f = new File(inferred_level_filename);
+
+ if (!f.exists())
+ {
+ f.createNewFile();
+ }
+
+ inferred_level_file = new BufferedWriter(new FileWriter(f, true));
+
+ parse_file();
+ create_template();
+
+ output_template_file.close();
+ inferred_level_file.close();
+ }
+
+ /***************************************************************************/
+ private final String var_name;
+ private final String var_type;
+
+ private ParserEntry (final String var_name, final String var_type)
+ {
+ this.var_name = var_name;
+ this.var_type = var_type;
+ }
+
+ private String get_var_type ()
+ {
+ return var_type;
+ }
+
+ private String get_var_name ()
+ {
+ return var_name;
+ }
+}