Commit b22626e6 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

cleanup

parent 13b2f982
......@@ -12,11 +12,11 @@ import java.util.logging.FileHandler;
import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.global.MohawkCSVFileFormatter;
import mohawk.global.MohawkConsoleFormatter;
import mohawk.global.MohawkTiming;
import mohawk.global.formatter.MohawkCSVFileFormatter;
import mohawk.global.formatter.MohawkConsoleFormatter;
import mohawk.global.results.MohawkResults;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.testing.TestingResults;
import mohawk.testing.TestingSuite;
import org.apache.commons.cli.BasicParser;
......@@ -51,7 +51,7 @@ public class MohawkInstance {
private String NuSMV_filepath = "NuSMV";
// Helpers
private TestingResults results;
private MohawkResults results;
private MohawkTiming timing;
private TestingSuite tests;
private SMVSpecHelper SMV_helper = new SMVSpecHelper();
......@@ -78,7 +78,7 @@ public class MohawkInstance {
// Execute the test cases
if (cmd.hasOption("run")) {
logger.info("[ACTION] Run paramter detected");
results = new TestingResults(resultsFile);
results = new MohawkResults();
timing = new MohawkTiming();
tests = new TestingSuite(SMV_helper, results, timing);
......@@ -99,8 +99,6 @@ public class MohawkInstance {
tests.done();
logger.info("[TIMING] " + tests.timing);
results.done();
}
} catch (ParseException e) {
StringWriter errors = new StringWriter();
......@@ -314,11 +312,11 @@ public class MohawkInstance {
// Logging Level
logger.setUseParentHandlers(false);
consoleHandler.setFormatter(new MohawkConsoleFormatter());
setLoggerLevel(Level.WARNING); // Default Level
setLoggerLevel(Level.INFO); // Default Level
if (cmd.hasOption("loglevel")) {
String loglevel = cmd.getOptionValue("loglevel");
if (loglevel.equalsIgnoreCase("quiet")) {
setLoggerLevel(Level.SEVERE);
setLoggerLevel(Level.WARNING);
} else if (loglevel.equalsIgnoreCase("debug")) {
setLoggerLevel(Level.FINEST);
} else if (loglevel.equalsIgnoreCase("verbose")) {
......
......@@ -19,8 +19,6 @@ public class BTreeDriver {
* @throws Exception
*/
public static void main(String[] args) throws Exception {
// TODO Auto-generated method stub
Vector<BitVector> vecUA;
Map<Integer, String> map = new HashMap<Integer, String>();
......
......@@ -11,7 +11,7 @@ import java.util.Vector;
/*
* This class abstracts a bit vector. Internally it contains a vector of Boolean.
* Supports bitwise operations such as AND and OR.
* TODO: May extend to additional operations in the future.
* May extend to additional operations in the future.
*/
public class BitVector {
......
......@@ -19,7 +19,7 @@ public class SMVSpecHelper {
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 Long TIMEOUT_SECONDS = (long) 0; // Default infinite
public void loadSpecFiles() throws IOException {
if (this.bulk == true) {
......
......@@ -32,7 +32,7 @@ public class CalculateDiameter {
}
/*
* Reader reader = null; try { reader = new FileReader(rbacfile); } catch (FileNotFoundException e) { // TODO
* Reader reader = null; try { reader = new FileReader(rbacfile); } catch (FileNotFoundException e) {
* Auto-generated catch block e.printStackTrace(); }
*/
// RBACLexer lexer = new RBACLexer(reader);
......@@ -102,7 +102,7 @@ public class CalculateDiameter {
}
/*
* Reader reader = null; try { reader = new FileReader(rbacfile); } catch (FileNotFoundException e) { // TODO
* Reader reader = null; try { reader = new FileReader(rbacfile); } catch (FileNotFoundException e) {
* Auto-generated catch block e.printStackTrace(); }
*/
// RBACLexer lexer = new RBACLexer(reader);
......
......@@ -98,7 +98,6 @@ public class CalculateRMax {
try {
roleindex = rbac_instance.getRoleIndex(tmpCAE1.getRole());
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......
......@@ -98,7 +98,6 @@ public class CalculateRplusOnly {
try {
iRoleIndex = rbac_instance.getRoleIndex(strRole);
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
Set<String> sNegRoles = new HashSet<String>();
......
......@@ -42,7 +42,6 @@ public class NuSMV {
*
*/
public NuSMV() {
// TODO Auto-generated constructor stub
}
// Function to call the symbolic model checker
......
......@@ -67,7 +67,6 @@ public class WriteNuSMV {
strTCodeTemplate = new StringTemplate(getTemplateStr("smvtemplate.st"));
strTransTemplate = getTemplateStr("transitions.st");
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
......@@ -169,7 +168,6 @@ public class WriteNuSMV {
try {
iDestRoleIndex = rbac.getRoleIndex(inCAEntry.getRole());
} catch (Exception e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
......@@ -187,7 +185,6 @@ public class WriteNuSMV {
adminRoleIndex = rbac.getRoleIndex(inCAEntry.getAdminRole());
} catch (Exception e) {
System.out.println(inCAEntry.getAdminRole());
// TODO Auto-generated catch block
e.printStackTrace();
}
......@@ -242,7 +239,6 @@ public class WriteNuSMV {
else
adminRoleIndex = rbac.getRoleIndex(crentry.getPreCond());
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......@@ -347,7 +343,6 @@ public class WriteNuSMV {
try {
roleindex = rbac.getRoleIndex(inStrRole);
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......@@ -377,7 +372,7 @@ public class WriteNuSMV {
/*
* Fill attributes in the StringTemplate
*
* TODO: This function should be passed an object that represents the RBAC state. The parameters should be plugged
* Maybe This function should be passed an object that represents the RBAC state. The parameters should be plugged
* into the template based on the RBAC state.
*/
public void fillAttributes(RBACInstance inRbac) throws IOException {
......
......@@ -17,7 +17,7 @@ import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
import org.antlr.stringtemplate.*;
import org.antlr.stringtemplate.StringTemplate;
/**
* @author Karthick Jayaraman This class is for writing an a generated RBAC instance to file.
......@@ -38,7 +38,6 @@ public class WriteRBACSpec {
String strTemplateString = this.getTemplateStr(filename);
STRBACSpec = new StringTemplate(strTemplateString);
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
// Initialize Random number generator
......
......@@ -73,7 +73,6 @@ public class RBAC2SMV {
*/
public static void main(String[] args) throws Exception {
// TODO Auto-generated method stub
if (args.length < 2) {
System.out.println("Usage: java -cp ./mohawk.jar mohawk.RBAC2SMV <rbacspec> <smvfile>");
......@@ -114,7 +113,6 @@ public class RBAC2SMV {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......
......@@ -36,7 +36,6 @@ public class RBACPAT {
}
public StringBuffer getRBACPAT() throws Exception {
// TODO Auto-generated method stub
File rbacfile = new File(filename);
......@@ -77,7 +76,6 @@ public class RBACPAT {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......
......@@ -45,10 +45,8 @@ public class RBACSpecReader {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (TokenStreamException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
......@@ -66,7 +64,6 @@ public class RBACSpecReader {
try {
reader = new FileReader(filename);
} catch (FileNotFoundException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
RBACLexer lexer = new RBACLexer(reader);
......@@ -87,10 +84,8 @@ public class RBACSpecReader {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (TokenStreamException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
......
......@@ -14,7 +14,7 @@ import java.util.Vector;
import mohawk.collections.NuSMVMode;
import mohawk.collections.RoleDepTree;
import mohawk.global.TestResult;
import mohawk.global.results.ExecutionResult;
import mohawk.math.CalculateDiameter;
import mohawk.nusmv.NuSMV;
import mohawk.output.WriteNuSMV;
......@@ -73,7 +73,6 @@ public class RolesAbsRefine {
try {
sliceUA();
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......@@ -287,7 +286,6 @@ public class RolesAbsRefine {
try {
sliceUA();
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
sliceCA();
......@@ -302,7 +300,7 @@ public class RolesAbsRefine {
return result;
}
public TestResult absrefineloop() {
public ExecutionResult absrefineloop() {
int fileno = 1;
try {
......@@ -314,7 +312,6 @@ public class RolesAbsRefine {
try {
writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
} catch (IOException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
......@@ -334,7 +331,7 @@ public class RolesAbsRefine {
if (result) {
System.out.println("Found counter example in step " + (fileno));
WriteMapping(nextinstance, "ROLEMAPPING");
return TestResult.GOAL_REACHABLE;
return ExecutionResult.GOAL_REACHABLE;
} else {
System.out.println("No counter example found in refinement step " + fileno);
}
......@@ -342,13 +339,12 @@ public class RolesAbsRefine {
fileno++;
}
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
return TestResult.ERROR_OCCURRED;
return ExecutionResult.ERROR_OCCURRED;
}
System.out.println("No counter example found in " + (fileno - 1) + " refinement steps");
return TestResult.GOAL_UNREACHABLE;
return ExecutionResult.GOAL_UNREACHABLE;
}
/**
......
......@@ -106,7 +106,6 @@ public class RoleSlicer {
@Override
public int compare(String o1, String o2) {
// TODO Auto-generated method stub
return o1.compareTo(o2);
}
}
......
......@@ -2,7 +2,7 @@ package mohawk.testing;
import static org.junit.Assert.assertEquals;
import mohawk.MohawkInstance;
import mohawk.global.TestResult;
import mohawk.global.results.ExecutionResult;
import org.junit.Test;
......@@ -19,7 +19,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive1() {
String param = "-rbacspec data/regressiontests/positive1.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -30,7 +30,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive2() {
String param = "-rbacspec data/regressiontests/positive2.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -41,7 +41,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive3() {
String param = "-rbacspec data/regressiontests/positive3.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......@@ -52,7 +52,7 @@ public class MohawkRegressionTests {
@Test
public void runPositive4() {
String param = "-rbacspec data/regressiontests/positive4.spec -run all -mode bmc";
TestResult expectedResult = TestResult.GOAL_REACHABLE;
ExecutionResult expectedResult = ExecutionResult.GOAL_REACHABLE;
MohawkInstance mohawk = new MohawkInstance();
mohawk.run(params(param));
......
......@@ -2,19 +2,19 @@ package mohawk.testing;
import java.util.concurrent.Callable;
import mohawk.global.TestResult;
import mohawk.global.results.ExecutionResult;
import mohawk.refine.RolesAbsRefine;
public class RunTest implements Callable<TestResult> {
public class TestRunner implements Callable<ExecutionResult> {
RolesAbsRefine absrefine;
public RunTest(RolesAbsRefine absrefine) {
public TestRunner(RolesAbsRefine absrefine) {
this.absrefine = absrefine;
}
@Override
public TestResult call() throws Exception {
TestResult result = absrefine.absrefineloop();
public ExecutionResult call() throws Exception {
ExecutionResult result = absrefine.absrefineloop();
return result;
}
......
package mohawk.testing;
import java.io.File;
import java.io.FileOutputStream;
import java.io.IOException;
import java.util.ArrayList;
import java.util.logging.Logger;
import mohawk.global.TestResult;
/**
*
* @author Jonathan Shahen
*
*/
public class TestingResults {
public final static Logger logger = Logger.getLogger("mohawk");
public FileOutputStream writer = null;
public ArrayList<TestResult> history = new ArrayList<TestResult>();
public TestingResults(String resultsFile) {
try {
File test = new File(resultsFile);
// Create the file if it doesn't exists
if (!test.exists()) {
test.createNewFile();
}
writer = new FileOutputStream(resultsFile, true);
} catch (IOException e) {
logger.severe("[ERROR] Unable to create the results file: '" + resultsFile + "'");
}
}
public void done() {
try {
if (writer != null) {
writer.close();
}
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
}
public void addTestResult(TestResult result) {
this.addTestResults(result, true, true);
}
public void addTestResults(TestResult result, boolean writeToConsole, boolean writeToFile) {
history.add(result);
if (writeToConsole == true) {
writeToConsole(result);
}
if (writeToFile == true) {
writeToFile(result);
}
}
public void writeToConsole(TestResult results) {
// TODO Auto-generated method stub
}
public void writeToFile(TestResult results) {
// TODO Auto-generated method stub
}
}
......@@ -13,8 +13,9 @@ import java.util.logging.Level;
import java.util.logging.Logger;
import mohawk.collections.NuSMVMode;
import mohawk.global.MohawkTiming;
import mohawk.global.TestResult;
import mohawk.global.results.ExecutionResult;
import mohawk.global.results.MohawkResults;
import mohawk.global.timing.MohawkTiming;
import mohawk.helper.SMVSpecHelper;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
......@@ -23,15 +24,15 @@ import mohawk.refine.RolesAbsRefine;
public class TestingSuite {
public final static Logger logger = Logger.getLogger("mohawk");
public TestingResults results;
public MohawkResults results;
public MohawkTiming timing;
public SMVSpecHelper smvHelper;
public TestResult lastResult;
public ExecutionResult lastResult;
public String timingResultsFile = "logs/mohawkTimingResults.csv";
public String testingResultsFile = "logs/mohawkTestingResults.csv";
public TestingSuite(SMVSpecHelper smvHelper, TestingResults results, MohawkTiming timing) {
public TestingSuite(SMVSpecHelper smvHelper, MohawkResults results, MohawkTiming timing) {
this.smvHelper = smvHelper;
this.results = results;
this.timing = timing;
......@@ -100,12 +101,16 @@ public class TestingSuite {
absrefine.setMode(modes.get(j));
// Setup Timeout Timer
Future<TestResult> future = executor.submit(new RunTest(absrefine));
Future<ExecutionResult> future = executor.submit(new TestRunner(absrefine));
try {
logger.info("[RUNNING] Running Mohawk on testcase " + i + " (mode=" + modes.get(j) + "):");
lastResult = future.get(smvHelper.TIMEOUT_SECONDS, TimeUnit.SECONDS);
if (smvHelper.TIMEOUT_SECONDS == 0) {
lastResult = future.get();
} else {
lastResult = future.get(smvHelper.TIMEOUT_SECONDS, TimeUnit.SECONDS);
}
// System.out.println("Result: " + lastResult);
logger.info("[COMPLETED] Result: " + lastResult + ", for the following spec file (in mode "
+ modes.get(j) + "): " + specFile);
......@@ -113,13 +118,13 @@ public class TestingSuite {
} catch (TimeoutException e) {
logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: " + specFile);
lastResult = TestResult.TIMEOUT;
lastResult = ExecutionResult.TIMEOUT;
/* TIMING */timing.cancelTimer(timerName);
} catch (OutOfMemoryError e) {
logger.warning("[OUT OF MEMORY] Mohawk has ran out of memory out for SPEC file: " + specFile);
lastResult = TestResult.OUT_OF_MEMORY;
lastResult = ExecutionResult.OUT_OF_MEMORY;
/* TIMING */timing.cancelTimer(timerName);
} catch (InterruptedException e) {
......
......@@ -24,8 +24,6 @@ public class RemoveCR {
* @param args
*/
public static void main(String[] args) throws Exception {
// TODO Auto-generated method stub
File rbacfile = new File(args[0]);
if (!rbacfile.exists()) {
......@@ -61,7 +59,6 @@ public class RemoveCR {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......@@ -71,7 +68,6 @@ public class RemoveCR {
try {
writer.Write2File(rbac, outputfile);
} catch (IOException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
......
......@@ -19,7 +19,6 @@ public class Replicate {
* @param args
*/
public static void main(String[] args) {
// TODO Auto-generated method stub
if (args.length < 2) {
System.out.println("Usage: java -jar ./rbac2smv.jar Slicer rbacspec nusmvfile");
......@@ -45,7 +44,6 @@ public class Replicate {
try {
writer.Write2File(newrbac, nusmvfile);
} catch (IOException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
}
......
......@@ -25,8 +25,6 @@ public class RoleAnalysis {
* @param args
*/
public static void main(String[] args) {
// TODO Auto-generated method stub
int oldroles, oldusers, oldcarules, oldcrrules;
if (args.length < 2) {
......@@ -67,7 +65,6 @@ public class RoleAnalysis {
try {
tmprbac = roleslicer.getSlicedPolicy();
} catch (Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......
......@@ -30,8 +30,6 @@ public class SizeOfRBAC {
* @throws FileNotFoundException
*/
public static void main(String[] args) throws Exception {
// TODO Auto-generated method stub
File rbacfile = new File(args[0]);
if (!rbacfile.exists()) {
......@@ -65,7 +63,6 @@ public class SizeOfRBAC {
rbac = parser.getRBAC();
} catch (RecognitionException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
......
......@@ -28,7 +28,6 @@ public class Slicer {
* @param args
*/