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

Reorganizing code for better readability, moving log files into separate...

Reorganizing code for better readability, moving log files into separate folder so that they will not appear to be updated every time you run the script
parent 618905d6
// $ANTLR 2.7.7 (20060906): "rbac.g" -> "RBACParser.java"$ // $ANTLR 2.7.7 (20060906): "rbac.g" -> "RBACParser.java"$
package mohawk; package mohawk.rbac;
public interface RBACParserTokenTypes { public interface RBACParserTokenTypes {
......
/** /**
* RBACSpecReader reads an RBAC spec file and returns an RBACInstance. * RBACSpecReader reads an RBAC spec file and returns an RBACInstance.
*/ */
package mohawk; package mohawk.rbac;
import java.io.File; import java.io.File;
import java.io.FileNotFoundException; import java.io.FileNotFoundException;
......
...@@ -21,11 +21,13 @@ ...@@ -21,11 +21,13 @@
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
* THE SOFTWARE. * THE SOFTWARE.
*/ */
package mohawk; package mohawk.refine;
import java.io.File; import java.io.File;
import mohawk.collections.NuSMVMode; import mohawk.collections.NuSMVMode;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
/** /**
* @author Karthick Jayaraman, Jonathan Shahen * @author Karthick Jayaraman, Jonathan Shahen
......
...@@ -22,7 +22,7 @@ ...@@ -22,7 +22,7 @@
* THE SOFTWARE. * THE SOFTWARE.
*/ */
package mohawk; package mohawk.refine;
import java.util.HashMap; import java.util.HashMap;
import java.util.HashSet; import java.util.HashSet;
...@@ -31,6 +31,11 @@ import java.util.Map; ...@@ -31,6 +31,11 @@ import java.util.Map;
import java.util.Set; import java.util.Set;
import java.util.Vector; import java.util.Vector;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
/** /**
* @author Karthick Jayaraman * @author Karthick Jayaraman
* *
......
/** /**
* *
*/ */
package mohawk; package mohawk.refine;
import java.io.FileWriter; import java.io.FileWriter;
import java.io.IOException; import java.io.IOException;
...@@ -14,6 +14,15 @@ import java.util.Vector; ...@@ -14,6 +14,15 @@ import java.util.Vector;
import mohawk.collections.NuSMVMode; import mohawk.collections.NuSMVMode;
import mohawk.collections.RoleDepTree; import mohawk.collections.RoleDepTree;
import mohawk.helper.MohawkResult;
import mohawk.math.CalculateDiameter;
import mohawk.nusmv.NuSMV;
import mohawk.output.WriteNuSMV;
import mohawk.output.WriteRBACSpec;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
/** /**
* @author kjayaram * @author kjayaram
...@@ -301,13 +310,11 @@ public class RolesAbsRefine { ...@@ -301,13 +310,11 @@ public class RolesAbsRefine {
return result; return result;
} }
public void absrefineloop() { public MohawkResult absrefineloop() {
int fileno = 1; int fileno = 1;
try { try {
while (refine()) { while (refine()) {
WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno, WriteNuSMV nusmv = new WriteNuSMV("rbacinstancefile" + fileno,
"smvtemplate"); "smvtemplate");
nusmv.fillAttributes(nextinstance); nusmv.fillAttributes(nextinstance);
...@@ -338,22 +345,24 @@ public class RolesAbsRefine { ...@@ -338,22 +345,24 @@ public class RolesAbsRefine {
System.out.println("Found counter example in step " System.out.println("Found counter example in step "
+ (fileno)); + (fileno));
WriteMapping(nextinstance, "ROLEMAPPING"); WriteMapping(nextinstance, "ROLEMAPPING");
return; return MohawkResult.GOAL_REACHABLE;
} else } else {
System.out System.out
.println("No counter example found in refinement step " .println("No counter example found in refinement step "
+ fileno); + fileno);
}
fileno++; fileno++;
} }
System.out.println("No counter example found in " + (fileno - 1)
+ " refinement steps");
} catch (Exception e) { } catch (Exception e) {
// TODO Auto-generated catch block // TODO Auto-generated catch block
e.printStackTrace(); e.printStackTrace();
return MohawkResult.ERROR_OCCURRED;
} }
System.out.println("No counter example found in " + (fileno - 1)
+ " refinement steps");
return MohawkResult.GOAL_UNREACHABLE;
} }
/** /**
......
/** /**
* *
*/ */
package mohawk; package mohawk.slicer;
import java.util.Collection; import java.util.Collection;
import java.util.Collections; import java.util.Collections;
...@@ -12,6 +12,11 @@ import java.util.LinkedHashSet; ...@@ -12,6 +12,11 @@ import java.util.LinkedHashSet;
import java.util.Map; import java.util.Map;
import java.util.Vector; import java.util.Vector;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
/** /**
* @author kjayaram * @author kjayaram
* *
......
/** /**
* *
*/ */
package mohawk; package mohawk.slicer;
import java.util.HashMap; import java.util.HashMap;
import java.util.Iterator; import java.util.Iterator;
import java.util.Map; import java.util.Map;
import java.util.Vector; import java.util.Vector;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.rbac.RBACInstance;
/** /**
* @author kjayaram * @author kjayaram
* *
......
package mohawk.testing;
import mohawk.helper.MohawkResult;
import org.junit.Test;
/**
* Run these JUnit tests before adding any branch to master
*
* @author Jonathan Shahen
*
*/
public class RegressionTests {
@Test
public void runMixedTest3SMV() {
String parameter = "-loglevel debug -rbacspec ./data/testcases/mixed/test3.spec -run smv -smvfile test3.spec.smv";
MohawkResult expectedResult = MohawkResult.GOAL_REACHABLE;
}
}
...@@ -2,9 +2,10 @@ package mohawk.testing; ...@@ -2,9 +2,10 @@ package mohawk.testing;
import java.util.concurrent.Callable; import java.util.concurrent.Callable;
import mohawk.RolesAbsRefine; import mohawk.helper.MohawkResult;
import mohawk.refine.RolesAbsRefine;
public class RunTest implements Callable<String> { public class RunTest implements Callable<MohawkResult> {
RolesAbsRefine absrefine; RolesAbsRefine absrefine;
public RunTest(RolesAbsRefine absrefine) { public RunTest(RolesAbsRefine absrefine) {
...@@ -12,10 +13,10 @@ public class RunTest implements Callable<String> { ...@@ -12,10 +13,10 @@ public class RunTest implements Callable<String> {
} }
@Override @Override
public String call() throws Exception { public MohawkResult call() throws Exception {
absrefine.absrefineloop(); MohawkResult result = absrefine.absrefineloop();
return "done"; return result;
} }
} }
...@@ -12,12 +12,13 @@ import java.util.concurrent.TimeoutException; ...@@ -12,12 +12,13 @@ import java.util.concurrent.TimeoutException;
import java.util.logging.Level; import java.util.logging.Level;
import java.util.logging.Logger; import java.util.logging.Logger;
import mohawk.RBACInstance;
import mohawk.RBACSpecReader;
import mohawk.RolesAbsRefine;
import mohawk.collections.NuSMVMode; import mohawk.collections.NuSMVMode;
import mohawk.helper.MohawkResult;
import mohawk.helper.SMVSpecHelper; import mohawk.helper.SMVSpecHelper;
import mohawk.logging.MohawkTiming; import mohawk.logging.MohawkTiming;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
import mohawk.refine.RolesAbsRefine;
public class TestingSuite { public class TestingSuite {
public final static Logger logger = Logger.getLogger("mohawk"); public final static Logger logger = Logger.getLogger("mohawk");
...@@ -46,6 +47,8 @@ public class TestingSuite { ...@@ -46,6 +47,8 @@ public class TestingSuite {
* @throws IOException * @throws IOException
*/ */
public void runTests() throws IOException { public void runTests() throws IOException {
logger.entering(getClass().getName(), "runTests()");
ArrayList<NuSMVMode> modes = new ArrayList<NuSMVMode>(); ArrayList<NuSMVMode> modes = new ArrayList<NuSMVMode>();
switch (smvHelper.mode) { switch (smvHelper.mode) {
case 3: // Both case 3: // Both
...@@ -63,46 +66,74 @@ public class TestingSuite { ...@@ -63,46 +66,74 @@ public class TestingSuite {
+ new Integer(smvHelper.mode)); + new Integer(smvHelper.mode));
} }
timing.startTimer("smvHelper.loadSpecFiles"); /* TIMING */timing.startTimer("smvHelper.loadSpecFiles");
smvHelper.loadSpecFiles(); smvHelper.loadSpecFiles();
timing.stopTimer("smvHelper.loadSpecFiles"); /* TIMING */timing.stopTimer("smvHelper.loadSpecFiles");
/* TIMING */timing.startTimer("runTests.mainLoop");
ExecutorService executor = Executors.newSingleThreadExecutor(); ExecutorService executor = Executors.newSingleThreadExecutor();
for (int i = 0; i < smvHelper.specFiles.size(); i++) { for (Integer i = 0; i < smvHelper.specFiles.size(); i++) {
for (int j = 0; j < modes.size(); j++) { /* TIMING */timing.startTimer("runTests.mainLoop (" + i + ")");
for (Integer j = 0; j < modes.size(); j++) {
String specFile = smvHelper.specFiles.get(i).getAbsolutePath(); String specFile = smvHelper.specFiles.get(i).getAbsolutePath();
timing.startTimer(specFile); String timerName = "runTests.mainLoop (" + i + ") - "
+ smvHelper.specFiles.get(i).getName() + " ("
+ modes.get(j) + ")";
/* TIMING */timing.startTimer(timerName);
RBACSpecReader reader = new RBACSpecReader(specFile); RBACSpecReader reader = new RBACSpecReader(specFile);
RBACInstance rbac = reader.getRBAC(); RBACInstance rbac = reader.getRBAC();
RolesAbsRefine absrefine = new RolesAbsRefine(rbac); RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
absrefine.setMode(modes.get(j)); absrefine.setMode(modes.get(j));
// Return Result
MohawkResult result;
// Setup Timeout Timer // Setup Timeout Timer
Future<String> future = executor.submit(new RunTest(absrefine)); Future<MohawkResult> future = executor.submit(new RunTest(
absrefine));
try { try {
future.get(smvHelper.TIMEOUT_SECONDS, TimeUnit.SECONDS); logger.info("[RUNNING] Running Mohawk on a testcase:");
logger.info("[COMPLETED] The following spec file is completed testing for mode " result = future.get(smvHelper.TIMEOUT_SECONDS,
+ modes.get(j) + ": " + specFile); TimeUnit.SECONDS);
timing.stopTimer(specFile); logger.info("[COMPLETED] Result: " + result
+ ", for the following spec file (in mode "
+ modes.get(j) + "): " + specFile);
/* TIMING */timing.stopTimer(timerName);
} catch (TimeoutException e) { } catch (TimeoutException e) {
logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: " logger.warning("[TIMEOUT] Mohawk has timed out for SPEC file: "
+ specFile); + specFile);
timing.cancelTimer(specFile);
result = MohawkResult.TIMEOUT;
/* TIMING */timing.cancelTimer(timerName);
} catch (OutOfMemoryError e) {
logger.warning("[OUT OF MEMORY] Mohawk has ran out of memory out for SPEC file: "
+ specFile);
result = MohawkResult.OUT_OF_MEMORY;
/* TIMING */timing.cancelTimer(timerName);
} catch (InterruptedException e) { } catch (InterruptedException e) {
if (logger.getLevel() == Level.FINEST) { if (logger.getLevel() == Level.FINEST) {
e.printStackTrace(); e.printStackTrace();
} }
/* TIMING */timing.cancelTimer(timerName);
logger.severe(e.getMessage()); logger.severe(e.getMessage());
} catch (ExecutionException e) { } catch (ExecutionException e) {
if (logger.getLevel() == Level.FINEST) { if (logger.getLevel() == Level.FINEST) {
e.printStackTrace(); e.printStackTrace();
} }
/* TIMING */timing.cancelTimer(timerName);
logger.severe(e.getMessage()); logger.severe(e.getMessage());
} }
} }
/* TIMING */timing.stopTimer("runTests.mainLoop (" + i + ")");
} }
/* TIMING */timing.stopTimer("runTests.mainLoop");
logger.exiting(getClass().getName(), "runTests()");
} }
/** /**
...@@ -114,7 +145,8 @@ public class TestingSuite { ...@@ -114,7 +145,8 @@ public class TestingSuite {
* @throws IOException * @throws IOException
*/ */
public void onlyConvertSpecToSmvFormat() throws IOException { public void onlyConvertSpecToSmvFormat() throws IOException {
logger.fine("Converting SPEC to NuSMV files..."); logger.entering(getClass().getName(), "onlyConvertSpecToSmvFormat()");
smvHelper.loadSpecFiles(); smvHelper.loadSpecFiles();
for (int i = 0; i < smvHelper.specFiles.size(); i++) { for (int i = 0; i < smvHelper.specFiles.size(); i++) {
...@@ -133,7 +165,8 @@ public class TestingSuite { ...@@ -133,7 +165,8 @@ public class TestingSuite {
nusmvFile.delete(); nusmvFile.delete();
} }
} }
logger.fine("... Done converting SPEC to NuSMV files");
logger.exiting(getClass().getName(), "onlyConvertSpecToSmvFormat()");
} }
} }
/** /**
* *
*/ */
package mohawk; package mohawk.util;
import java.io.File; import java.io.File;
import java.io.FileReader; import java.io.FileReader;
import java.io.IOException; import java.io.IOException;
import java.io.Reader; import java.io.Reader;
import mohawk.output.WriteRBACSpec;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACLexer;
import mohawk.rbac.RBACParser;
import antlr.RecognitionException; import antlr.RecognitionException;
/** /**
......
package mohawk.util;
package mohawk; import java.io.File;
import java.io.IOException;
import java.util.HashMap; import java.util.HashMap;
import java.util.Map; import java.util.Map;
import java.util.Vector; import java.util.Vector;
public class Replicator { import mohawk.output.WriteRBACSpec;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
import mohawk.rbac.RBACSpecReader;
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");
}
File rbacfile = new File(args[0]);
if (!rbacfile.exists()) {
System.out.println("The RBAC specification file " + rbacfile
+ " does not exists.");
return;
}
String nusmvfile = args[1];
int times = Integer.parseInt(args[2]);
RBACSpecReader rbacreader = new RBACSpecReader(args[0]);
RBACInstance rbac = rbacreader.getRBAC();
Replicator replica = new Replicator(rbac);
RBACInstance newrbac = replica.replicatePolicy(times);
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
try {
writer.Write2File(newrbac, nusmvfile);
} catch (IOException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
}
}
class Replicator {
public Replicator(RBACInstance in_rbac) { public Replicator(RBACInstance in_rbac) {
...@@ -15,36 +63,31 @@ public class Replicator { ...@@ -15,36 +63,31 @@ public class Replicator {
public boolean isRole(String inRole) { public boolean isRole(String inRole) {
if (inRole.equalsIgnoreCase("Employee") if (inRole.equalsIgnoreCase("Employee")
|| inRole.equalsIgnoreCase("Admin")) || inRole.equalsIgnoreCase("Admin")) {
{
return false; return false;
} } else {
else
{
return true; return true;
} }
} }
public Map<String, Vector<Integer>> modifyUA(Vector<String> newRoles) { public Map<String, Vector<Integer>> modifyUA(Vector<String> newRoles) {
Map<String, Vector<Integer>> originalUA = rbac.getUA(); Map<String, Vector<Integer>> originalUA = rbac.getUA();
Map<String, Vector<Integer>> newUA = new HashMap<String, Vector<Integer>>(); Map<String, Vector<Integer>> newUA = new HashMap<String, Vector<Integer>>();
for(String strKey : originalUA.keySet()) for (String strKey : originalUA.keySet()) {
{
Vector<Integer> oldroleindices = originalUA.get(strKey); Vector<Integer> oldroleindices = originalUA.get(strKey);
Vector<Integer> newroleindices = new Vector<Integer>(); Vector<Integer> newroleindices = new Vector<Integer>();