Ready to implement the Ranise reduction

.gitignore

@@ -2,3 +2,4 @@
 target/
 src/mohawk/converter/generated/*.java
 src/mohawk/converter/generated/*.tokens
+logs/

data/testcases/simple/simple1.spec

 /* Taken from sharelatex's "Working Files/Mohawk Examples/old-simple-tests.txt"
  * 
  * Converted simple_test1.txt into the new format
-*/
+ */
 CanAssign {
-    // <Admin role, starting timeslot - end timeslot for admin role, role preconditions, [time slot rule gives role to user for, another time slot (optional)...],role to give to the user>
+    /* <Admin role, 
+     * starting timeslot - end timeslot for admin role, 
+     * role preconditions, 
+     * [time slot rule gives role to user for, another time slot (optional)...],
+     * role to give to the user>
+     */
     <role0,t0-t0,TRUE,[t0],role1>		//(1)
     <role0,t0-t0,role1,[t0],role2>		//(2)
 }

logs/README.txt

+Please direct all logs to go into this folder so that they do not accidently get added into the repo.
\ No newline at end of file

src/mohawk/converter/ConverterInstance.java

@@ -3,15 +3,19 @@ package mohawk.converter;
 import java.io.File;
 import java.io.FileOutputStream;
 import java.io.IOException;
-import java.util.ArrayList;
 import java.util.logging.ConsoleHandler;
 import java.util.logging.FileHandler;
 import java.util.logging.Level;
 import java.util.logging.Logger;
 
+import mohawk.converter.generated.MohawkTARBACParser;
+import mohawk.converter.helper.SpecHelper;
 import mohawk.converter.logging.MohawkCSVFileFormatter;
 import mohawk.converter.logging.MohawkConsoleFormatter;
 import mohawk.converter.logging.MohawkTiming;
+import mohawk.converter.to.mohawk.ConvertToMohawk;
+import mohawk.converter.to.ranise.ConvertToRanise;
+import mohawk.converter.to.uzun.ConvertToUzun;
 
 import org.apache.commons.cli.BasicParser;
 import org.apache.commons.cli.CommandLine;
@@ -23,7 +27,8 @@ import org.apache.commons.cli.ParseException;
 import org.apache.commons.lang3.StringUtils;
 
 public class ConverterInstance {
-    private final String VERSION = "v0.0.2";
+    private static final String VERSION = "v0.0.2";
+    private static final String AUTHORS = "Jonathan Shahen <jmshahen@uwaterloo.ca>";
     // Logger Fields
     public static final Logger logger = Logger.getLogger("mohawk-converter");
     private String Logger_filepath = "mohawk-converter.log";
@@ -32,59 +37,86 @@ public class ConverterInstance {
     private Level LoggerLevel;
     private FileHandler fileHandler;
     private Boolean WriteCSVFileHeader = true;
-    private String resultsFile = "latestMohawk-TConverterResults.csv";
+    private String resultsFile = "latest_Mohawk-T_Converter_Results.csv";
+
+    // Helpers
+    public SpecHelper specHelper = new SpecHelper();
+    public MohawkTiming timing = new MohawkTiming();
 
     public int run(String[] args) {
         try {
             Options options = new Options();
             setupOptions(options, args);
 
-            CommandLineParser parser = new BasicParser();
-            CommandLine cmd = parser.parse(options, args);
+            CommandLineParser cmdParser = new BasicParser();
+            CommandLine cmd = cmdParser.parse(options, args);
 
             setupLoggerOptions(cmd, options, args);
 
             if (setupReturnImmediatelyOptions(cmd, options, args)) { return 0; }
 
-            MohawkTiming timing = new MohawkTiming();
-            ArrayList<File> specFiles = new ArrayList<File>();
-
             /* Timing */timing.startTimer("totalTime");
 
+            setupUserPreferenceOptions(cmd, options, args);
+
+            setupSmvSpecOptions(cmd, options, args);
+
+            setupResultOptions(cmd, options, args);
+
             /* Timing */timing.startTimer("loadFile");
             if (cmd.hasOption("bulk")) {
-                // TODO: Load in all SPEC files from folder under -rbacspec
-            } else {
-                // TODO: load in single file
+                specHelper.bulk = true;
             }
+            specHelper.loadSpecFiles();
             /* Timing */timing.stopTimer("loadFile");
 
-            logger.info("Spec File(s) to Coinvert: " + specFiles);
+            logger.info("Spec File(s) to Convert: " + specHelper.specFiles);
 
-            if (cmd.hasOption("ranise") || cmd.hasOption("all")) {
-                /* Timing */timing.startTimer("convertToRanise");
+            for (Integer i = 1; i <= specHelper.specFiles.size(); i++) {
+                File specFile = specHelper.specFiles.get(i - 1);
 
-                // TODO: Convert imported spec files to Ranise format
+                /* Timing */timing.startTimer("parseFile (" + i + ")");
+                logger.info("Processing File (" + i + "/" + specHelper.specFiles.size() + "): "
+                        + specFile.getAbsolutePath());
 
-                /* Timing */timing.stopTimer("convertToRanise");
-            }
+                MohawkTARBACParser parser = specHelper.parseSpecFile(specFile);
+                /* Timing */timing.stopTimer("parseFile (" + i + ")");
 
-            if (cmd.hasOption("uzun") || cmd.hasOption("all")) {
-                /* Timing */timing.startTimer("convertToUzun");
+                if (specHelper.error.errorFound) {
+                    logger.warning("[PARSING ERROR] Skipping this file due to a parsing error");
+                    continue;
+                }
 
-                // TODO: Convert imported spec files to Uzun format
+                if (cmd.hasOption("ranise") || cmd.hasOption("all")) {
+                    /* Timing */timing.startTimer("convertToRanise (" + i + ")");
 
-                /* Timing */timing.stopTimer("convertToUzun");
-            }
+                    // TODO: Convert imported spec files to Ranise format
+                    ConvertToRanise toRanise = new ConvertToRanise();
+                    int rainseError = toRanise.convert(parser, specFile);
 
-            if (cmd.hasOption("mohawk") || cmd.hasOption("all")) {
-                /* Timing */timing.startTimer("convertToMohawk");
+                    /* Timing */timing.stopTimer("convertToRanise (" + i + ")");
+                }
 
-                // TODO: Convert imported spec files to Mohawk format
+                if (cmd.hasOption("uzun") || cmd.hasOption("all")) {
+                    /* Timing */timing.startTimer("convertToUzun (" + i + ")");
 
-                /* Timing */timing.stopTimer("convertToMohawk");
-            }
+                    // TODO: Convert imported spec files to Uzun format
+                    ConvertToUzun toUzun = new ConvertToUzun();
+                    int uzunError = toUzun.convert(parser, specFile);
 
+                    /* Timing */timing.stopTimer("convertToUzun (" + i + ")");
+                }
+
+                if (cmd.hasOption("mohawk") || cmd.hasOption("all")) {
+                    /* Timing */timing.startTimer("convertToMohawk (" + i + ")");
+
+                    // TODO: Convert imported spec files to Mohawk format
+                    ConvertToMohawk toMohawk = new ConvertToMohawk();
+                    int rainseError = toMohawk.convert(parser, specFile);
+
+                    /* Timing */timing.stopTimer("convertToMohawk (" + i + ")");
+                }
+            }
             /* Timing */timing.stopTimer("totalTime");
 
             logger.info(timing.toString());
@@ -112,6 +144,7 @@ public class ConverterInstance {
     private void setupOptions(Options options, String[] args) {
         // Add Information Options
         options.addOption("help", false, "Print this message");
+        options.addOption("authors", false, "Prints the authors");
         options.addOption("version", false, "Prints the version (" + VERSION + ") information");
         options.addOption("checknusmv", false,
                 "Checks that NuSMV is on the system and displays which version is installed");
@@ -148,13 +181,19 @@ public class ConverterInstance {
                 .withDescription("Path to the RBAC Spec file or Folder if the 'bulk' option is set").hasArg()
                 .create("rbacspec"));
 
+        options.addOption(OptionBuilder
+                .withArgName("extension")
+                .withDescription(
+                        "File extention used when searching for SPEC files when the 'bulk' option is used. Default:'"
+                                + specHelper.specFileExt + "'").hasArg().create("specext"));
+
         // Add Functional Options
         options.addOption("bulk", false, "Use the folder that rbacspec points to and run against all *.spec");
 
-        options.addOption("ranise", false, "Convert input SPEC file to Ranise's format");
-        options.addOption("uzun", false, "Convert input SPEC file to Uzun's format");
-        options.addOption("mohawk", false, "Convert input SPEC file to Mohawk's RBAC format");
-        options.addOption("all", false, "Convert input SPEC file to All formats");
+        options.addOption("to_ranise", false, "Convert input SPEC file to Ranise's format");
+        options.addOption("to_uzun", false, "Convert input SPEC file to Uzun's format");
+        options.addOption("to_mohawk", false, "Convert input SPEC file to Mohawk's RBAC format");
+        options.addOption("to_all", false, "Convert input SPEC file to All formats (Mohawk, Ranise, Uzun)");
 
     }
 
@@ -254,9 +293,10 @@ public class ConverterInstance {
             if (cmd.hasOption("maxw")) {
                 try {
                     Integer maxw = Integer.decode(cmd.getOptionValue("maxw"));
-                    f.printHelp(maxw, "mohawk", StringUtils.repeat("-", maxw), options, StringUtils.repeat("-", maxw),
-                            true);
+                    f.printHelp(maxw, "mohawk", StringUtils.repeat("-", maxw) + "\nAuthors: " + AUTHORS + "\n"
+                            + StringUtils.repeat("-", 20), options, StringUtils.repeat("-", maxw), true);
                 } catch (Exception e) {
+                    e.printStackTrace();
                     System.out.println("An error occured when trying to print out the help options!");
                 }
 
@@ -272,7 +312,84 @@ public class ConverterInstance {
             return true;
         }
 
+        if (cmd.hasOption("authors")) {
+            // keep it as simple as possible for the version
+            System.out.println(AUTHORS);
+            return true;
+        }
+
         return false;
     }
 
+    private void setupSmvSpecOptions(CommandLine cmd, Options options, String[] args) {
+        // Load in SPEC Files
+        // SMV File
+        if (cmd.hasOption("smvfile")) {
+            if (cmd.getOptionValue("smvfile").equals("n")) {
+                logger.fine("[OPTION] Using temporary SMV Files - will be deleted after each use");
+                specHelper.smvDeleteFile = true;
+            } else {
+                logger.fine("[OPTION] Using a specific SMV File: " + cmd.getOptionValue("smvfile"));
+                specHelper.smvFilepath = cmd.getOptionValue("smvfile");
+            }
+        } else {
+            logger.fine("[OPTION] No SMV Filename included, saving file under: " + specHelper.smvFilepath);
+        }
+
+        // Grab the SPEC file
+        if (cmd.hasOption("rbacspec")) {
+            logger.fine("[OPTION] Using a specific SPEC File: " + cmd.getOptionValue("rbacspec"));
+            specHelper.specFile = cmd.getOptionValue("rbacspec");
+        } else {
+            logger.fine("[OPTION] No Spec File included");
+        }
+
+        if (cmd.hasOption("specext")) {
+            logger.fine("[OPTION] Using a specific SPEC File Extension: " + cmd.getOptionValue("specext"));
+            specHelper.specFileExt = cmd.getOptionValue("specext");
+        } else {
+            logger.fine("[OPTION] Using the default SPEC File Extension: " + specHelper.specFileExt);
+        }
+
+        // Load more than one file from the SPEC File?
+        if (cmd.hasOption("bulk")) {
+            logger.fine("[OPTION] Bulk SPEC File inclusion: Enabled");
+            specHelper.bulk = true;
+        } else {
+            logger.fine("[OPTION] Bulk SPEC File inclusion: Disabled");
+        }
+    }
+
+    private void setupUserPreferenceOptions(CommandLine cmd, Options options, String[] args) {
+        // Set the Console's Max Width
+        if (cmd.hasOption("maxw")) {
+            logger.fine("[OPTION] Setting the console's maximum width");
+            String maxw = "";
+            try {
+                maxw = cmd.getOptionValue("maxw");
+                ((MohawkConsoleFormatter) consoleHandler.getFormatter()).maxWidth = Integer.decode(maxw);
+            } catch (NumberFormatException e) {
+                logger.severe("[ERROR] Could not decode 'maxw': " + maxw + ";\n" + e.getMessage());
+            }
+        } else {
+            logger.fine("[OPTION] Default Console Maximum Width Used");
+        }
+
+        // Set the Console's Wrap String
+        if (cmd.hasOption("linestr")) {
+            logger.fine("[OPTION] Setting the console's new line string");
+            ((MohawkConsoleFormatter) consoleHandler.getFormatter()).newLineStr = cmd.getOptionValue("linestr");
+        } else {
+            logger.fine("[OPTION] Default Line String Used");
+        }
+
+    }
+
+    private void setupResultOptions(CommandLine cmd, Options options, String[] args) {
+        if (cmd.hasOption("results")) {
+            logger.fine("[OPTION] Changing the results file");
+            resultsFile = cmd.getOptionValue("results");
+        }
+        logger.info("Results File: " + resultsFile);
+    }
 }

src/mohawk/converter/generated/mohawktarbac.g4

@@ -36,7 +36,7 @@ import mohawk.converter.pieces.*;
 	public CanDisable canDisable = new CanDisable();
 	
 	public Query query = new Query();
-	public ExpectedResult expectedResult;
+	public ExpectedResult expectedResult = ExpectedResult.UNKNOWN;
 	
 	
 	private void logmsg(String msg) {

src/mohawk/converter/helper/SpecHelper.java

+package mohawk.converter.helper;
+
+import java.io.File;
+import java.io.FileInputStream;
+import java.io.IOException;
+import java.util.ArrayList;
+import java.util.logging.Logger;
+
+import mohawk.converter.generated.MohawkTARBACParser;
+import mohawk.converter.testing.BooleanErrorListener;
+import mohawk.converter.testing.RegressionTests;
+
+public class SpecHelper {
+    public final static Logger logger = Logger.getLogger("mohawk");
+    public String smvFilepath = "latestRBAC2SMV.smv";
+    public Boolean smvDeleteFile = false;
+    public String specFile = "";
+    public String specFileExt = ".spec";
+    public ArrayList<File> specFiles = new ArrayList<File>();
+    public boolean bulk = false;
+    public int mode = 3; // 1 for bmc, 2 for smc, 3 for both
+    public Long TIMEOUT_SECONDS = (long) 120; // Default 2 minutes
+
+    public BooleanErrorListener error = new BooleanErrorListener();
+
+    public void loadSpecFiles() throws IOException {
+        if (this.bulk == true) {
+            this.loadSpecFilesFromFolder(this.specFile);
+        } else {
+            this.addSpecFile(this.specFile);
+        }
+    }
+
+    public void loadSpecFilesFromFolder(String path) {
+        if (path == null || path == "") {
+            logger.severe("[ERROR] No SPEC Folder provided");
+        }
+
+        File folder = new File(path);
+
+        if (!folder.exists()) {
+            logger.severe("[ERROR] Spec Folder: '" + path + "' does not exists!");
+        }
+        if (!folder.isDirectory()) {
+            logger.severe("[ERROR] Spec Folder: '" + path + "' is not a folder and the 'bulk' option is present. "
+                    + "Try removing the '-bulk' option if you wish to use "
+                    + "a specific file, or change the option to point to a folder");
+        }
+
+        for (File f : folder.listFiles()) {
+            if (f.getName().endsWith(specFileExt)) {
+                logger.fine("Adding file to specFiles: " + f.getAbsolutePath());
+                specFiles.add(f);
+            }
+        }
+    }
+
+    public void addSpecFile(String path) throws IOException {
+        if (path == null || path.equals("")) {
+            logger.severe("[ERROR] No SPEC File provided");
+        }
+
+        File file2 = new File(path);
+        if (!file2.exists()) {
+            logger.severe("[ERROR] Spec File: '" + path + "' does not exists!");
+        }
+        if (!file2.isFile()) {
+            logger.severe("[ERROR] Spec File: '" + path + "' is not a file and the 'bulk' option was not set. "
+                    + "Try setting the '-bulk' option if you wish to search "
+                    + "through the folder, or change the option to point to a specific file");
+        }
+
+        logger.info("[FILE IO] Using SPEC File: " + file2.getCanonicalPath());
+        specFiles.add(file2);
+    }
+
+    public File getSmvFile(File specFile2) {
+        File nusmvFile = null;
+        if (smvDeleteFile) {
+            try {
+                nusmvFile = File.createTempFile("smvTempFile", ".smv");
+            } catch (IOException e) {
+                logger.severe("[ERROR] Unable to create a temporary SMV file in the current working directory: "
+                        + new File("").getAbsoluteFile());
+            }
+            return nusmvFile;
+        }
+
+        if (bulk) {
+            nusmvFile = new File(new File(smvFilepath).getAbsolutePath() + File.pathSeparator + specFile2.getName()
+                    + ".smv");
+        } else {
+            nusmvFile = new File(smvFilepath);
+        }
+
+        if (!nusmvFile.exists()) {
+            try {
+                nusmvFile.createNewFile();
+            } catch (IOException e) {
+                logger.severe("[ERROR] Unable to create a SMV file in the current working directory: "
+                        + new File("").getAbsoluteFile());
+            }
+        }
+        return nusmvFile;
+    }
+
+    public MohawkTARBACParser parseSpecFile(File specFile) throws IOException {
+        FileInputStream fis = new FileInputStream(specFile);
+
+        error.errorFound = false; // reset the error listener
+        MohawkTARBACParser parser = RegressionTests.runParser(fis, error);
+
+        if (error.errorFound) {
+            logger.warning("Unable to parse the file: " + specFile.getAbsolutePath());
+        }
+
+        return parser;
+    }
+}

src/mohawk/converter/testing/RegressionTests.java

@@ -14,6 +14,7 @@ import mohawk.converter.generated.MohawkTARBACLexer;
 import mohawk.converter.generated.MohawkTARBACParser;
 
 import org.antlr.v4.runtime.ANTLRInputStream;
+import org.antlr.v4.runtime.BaseErrorListener;
 import org.antlr.v4.runtime.CommonTokenStream;
 import org.apache.commons.lang3.StringUtils;
 import org.junit.Before;
@@ -113,7 +114,7 @@ public class RegressionTests {
         String str = "";
 
         error.errorFound = false;
-        runParser(new ByteArrayInputStream(str.getBytes()));
+        runParser(new ByteArrayInputStream(str.getBytes()), error);
 
         // Check for Parsing errors
         assertTrue("The empty string passed the parser!", error.errorFound);
@@ -122,10 +123,10 @@ public class RegressionTests {
     private MohawkTARBACParser loadfile(String file) throws IOException {
         FileInputStream fis = new FileInputStream(folderbase + file);
 
-        return runParser(fis);
+        return runParser(fis, error);
     }
 
-    private MohawkTARBACParser runParser(InputStream is) throws IOException {
+    public static MohawkTARBACParser runParser(InputStream is, BaseErrorListener errorListener) throws IOException {
         ANTLRInputStream input = new ANTLRInputStream(is);
         MohawkTARBACLexer lexer = new MohawkTARBACLexer(input);
         CommonTokenStream tokens = new CommonTokenStream(lexer);
@@ -134,17 +135,17 @@ public class RegressionTests {
         System.out.println(tokens.getText());
 
         parser.removeErrorListeners();
-        parser.addErrorListener(error);
+        parser.addErrorListener(errorListener);
         parser.init();
 
         System.out.println("Roles: " + parser.roles);
         System.out.println("Timeslots: " + parser.timeslots);
-        System.out.println(parser.query);
-        System.out.println(parser.expectedResult);
-        System.out.println(parser.canAssign);
-        System.out.println(parser.canDisable);
-        System.out.println(parser.canEnable);
-        System.out.println(parser.canRevoke);
+        System.out.println(parser.query.toString());
+        System.out.println(parser.expectedResult.toString());
+        System.out.println(parser.canAssign.toString());
+        System.out.println(parser.canDisable.toString());
+        System.out.println(parser.canEnable.toString());
+        System.out.println(parser.canRevoke.toString());
 
         return parser;
     }

src/mohawk/converter/to/ConvertTo.java

+package mohawk.converter.to;
+
+import java.io.File;
+
+import mohawk.converter.generated.MohawkTARBACParser;
+
+public interface ConvertTo {
+    public int convert(MohawkTARBACParser p, File f);
+}

src/mohawk/converter/to/mohawk/ConvertToMohawk.java

+package mohawk.converter.to.mohawk;
+
+import java.io.File;
+
+import mohawk.converter.generated.MohawkTARBACParser;
+import mohawk.converter.to.ConvertTo;
+
+public class ConvertToMohawk implements ConvertTo {
+
+    @Override
+    public int convert(MohawkTARBACParser p, File f) {
+        // TODO Auto-generated method stub
+        return 0;
+    }
+
+}

src/mohawk/converter/to/ranise/ConvertToRanise.java

+package mohawk.converter.to.ranise;
+
+import java.io.File;
+
+import mohawk.converter.generated.MohawkTARBACParser;
+import mohawk.converter.to.ConvertTo;
+
+public class ConvertToRanise implements ConvertTo {
+
+    @Override
+    public int convert(MohawkTARBACParser p, File f) {
+        // TODO Auto-generated method stub
+        return 0;
+    }
+
+}

src/mohawk/converter/to/uzun/ConvertToUzun.java

+package mohawk.converter.to.uzun;
+
+import java.io.File;
+
+import mohawk.converter.generated.MohawkTARBACParser;
+import mohawk.converter.to.ConvertTo;
+
+public class ConvertToUzun implements ConvertTo {
+
+    @Override
+    public int convert(MohawkTARBACParser p, File f) {
+        // TODO Auto-generated method stub
+        return 0;
+    }
+
+}

src/mohawk/converter/to_mohawk/ConvertToRBAC.java

-package mohawk.converter.to_mohawk;
-
-public class ConvertToRBAC {
-
-}

src/mohawk/converter/to_ranise/ConvertToRanise.java

-package mohawk.converter.to_ranise;
-
-public class ConvertToRanise {
-
-}

src/mohawk/converter/to_uzun/ConvertToUzun.java

-package mohawk.converter.to_uzun;
-
-public class ConvertToUzun {
-
-}