Commit 89185bf4 authored by Jonathan Shahen's avatar Jonathan Shahen

Add timing to old code and update the TestingResult to add the return code

parent 8c735bb6
......@@ -85,18 +85,20 @@ public class SMVSpecHelper {
}
try {
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate");
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(), "smvtemplate", settings.timing,
"convertSpecToSMVFormat(" + specFile.getName() + ")");
RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath());
RBACInstance rbac = reader.getRBAC();
if (settings.sliceRBAC) {
logger.info("[Slicing] Slicing the Spec File");
RoleSlicer roleslicer = new RoleSlicer(rbac);
RoleSlicer roleslicer = new RoleSlicer(rbac, settings.timing,
"convertSpecToSMVFormat(" + specFile.getName() + ")");
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles() + "; Number of Rules: "
+ (rbac.getCA().size() + rbac.getCR().size()));
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles() +
"; Number of Rules: " + (rbac.getCA().size() + rbac.getCR().size()));
}
if (settings.sliceRBACQuery) {
......@@ -109,7 +111,8 @@ public class SMVSpecHelper {
if (settings.skipRefine) {
nusmv.fillAttributes(rbac);
} else {
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
RolesAbsRefine absrefine = new RolesAbsRefine(rbac, settings.timing,
"convertSpecToSMVFormat(" + specFile.getName() + ")");
RBACInstance rbac_refined = absrefine.refineOnly();
nusmv.fillAttributes(rbac_refined);
......
......@@ -14,6 +14,7 @@ import java.util.logging.Level;
import org.stringtemplate.v4.ST;
import mohawk.global.pieces.mohawk.*;
import mohawk.global.timing.MohawkTiming;
import mohawk.rbac.RBACInstance;
/*
......@@ -55,14 +56,22 @@ public class WriteNuSMV {
*/
public Level logLevel = Level.WARNING;
public Integer userTransistionVersion = 1;
public boolean includeRuleComment = true;
public Integer roleWithRules;
public Integer roleWithoutRules;
// Timing
public MohawkTiming timing;
public String timingPrefix;
/*
* The constructor should initialize the target file and the filename for the template.
*/
public WriteNuSMV(String fname, String tname) {
public WriteNuSMV(String fname, String tname, MohawkTiming timing, String timingPrefix) {
this.timing = timing;
this.timingPrefix = timingPrefix;
filename = fname;
done = false;
roleWithRules = 0;
......@@ -147,29 +156,54 @@ public class WriteNuSMV {
* 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 {
public void fillAttributes(RBACInstance inRbac) throws Exception {
/* TIMING */timing.startTimer(timingPrefix + " (fillAttributes)");
rbac = inRbac;
// StringTemplate StrTSmvspec = new StringTemplate(strtemplate);
// StringTemplate strTrans = new StringTemplate(transtemplate);
System.out.println("Setting up user arrays");
this.setupUsers(strTCodeTemplate);
System.out.println("Setting up UA");
this.setupUA(strTCodeTemplate);
System.out.println("Setting up CA-CR rules");
this.setupUserTransitions(strTCodeTemplate);
System.out.println("[START] WriteNuSMV.fillAttributes()");
System.out.println("[START] Setting up user arrays...");
/* TIMING */timing.startTimer(timingPrefix + " (Setting up user arrays)");
setupUsers(strTCodeTemplate);
/* TIMING */timing.stopTimer(timingPrefix + " (Setting up user arrays)");
System.out.println("[START] Setting up UA...");
/* TIMING */timing.startTimer(timingPrefix + " (Setting up UA)");
setupUA(strTCodeTemplate);
/* TIMING */timing.stopTimer(timingPrefix + " (Setting up UA)");
System.out.println("[START] Setting up CA-CR rules...");
/* TIMING */timing.startTimer(timingPrefix + " (Setting up CA-CR rules v" + userTransistionVersion + ")");
switch (userTransistionVersion) {
case 1:
setupUserTransitionsv1(strTCodeTemplate);
break;
case 2:
setupUserTransitionsv2(strTCodeTemplate);
break;
}
/* TIMING */timing.stopTimer(timingPrefix + " (Setting up CA-CR rules v" + userTransistionVersion + ")");
// Setup LTLSPEC
System.out.println("Setting up SPEC");
System.out.println("[START] Setting up SPEC...");
/* TIMING */timing.startTimer(timingPrefix + " (Setting up SPEC)");
String strUser = rbac.getSpec().get(0);
String strRole = rbac.getSpec().get(1);
setupSpec(strTCodeTemplate, strUser, strRole);
/* TIMING */timing.stopTimer(timingPrefix + " (Setting up SPEC)");
// this.setupTransactions(this.strCodeTemplate, this.strCodeTemplate);
System.out.println("[START] Rendering SMV Code...");
/* TIMING */timing.startTimer(timingPrefix + " (Rendering SMV Code)");
smvcode = strTCodeTemplate.render();
/* TIMING */timing.stopTimer(timingPrefix + " (Rendering SMV Code)");
done = true;
/* TIMING */timing.stopTimer(timingPrefix + " (fillAttributes)");
}
public void setupUsers(ST inSmvSpec) {
......@@ -241,7 +275,203 @@ public class WriteNuSMV {
}
}
public void setupUserTransitions(ST strTCodeTemplate) {
public void setupUserTransitionsv2(ST strTCodeTemplate) throws Exception {
Vector<String> vUsers = rbac.getUsers();
String strTransitions = this.setupEachUserv2(vUsers);
strTCodeTemplate.add("transitions", strTransitions);
}
public String setupEachUserv2(Vector<String> vUsers) throws Exception {
Vector<String> vRoles = rbac.getRoles();
String strUserSection = null;
for (int i = 0; i < vRoles.size(); i++) {
String strRole = vRoles.get(i);
Vector<CAEntry> vCA = getMatchingCA(strRole);
Vector<CREntry> vCR = getMatchingCR(strRole);
StringBuilder transitions = null;
String strTmpUser = null;
ST strTTrans = new ST(strTransTemplate, '$', '$');
if (vCA != null) {
for (int j = 0; j < vCA.size(); j++) {
String strTmpTrans = addCAEntryv2(vUsers, vCA.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (vCR != null) {
for (int j = 0; j < vCR.size(); j++) {
String strTmpTrans = addCREntryv2(vUsers, vCR.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
} else {
transitions.append("\n");
transitions.append(strTmpTrans);
// transitions = transitions + "\n" + strTmpTrans;
}
}
}
if (transitions != null) {
strTTrans.add("rolename", strRole);
strTTrans.add("transition", transitions);
strTTrans.add("trueWord", getTrue());
strTmpUser = "";
for (String u : vUsers) {
strTTrans.add("roleindex1", u + "[" + i + "]");
strTTrans.add("roleindex2", u + "[" + i + "]");
strTmpUser += strTTrans.render() + "\n";
}
roleWithRules++;
} else {
strTmpUser = "";
for (String u : vUsers) {
strTmpUser += "-- " + strRole + "\nnext(" + u + "[" + i + "]) := " + u + "[" + i + "];\n";
}
roleWithoutRules++;
}
if (strUserSection == null) {
strUserSection = strTmpUser;
} else {
strUserSection = strUserSection + "\n\n" + strTmpUser;
}
}
return strUserSection;
}
public String addCAEntryv2(Vector<String> vUsers, CAEntry inCAEntry) throws Exception {
Vector<String> vAdminUsers = rbac.getAdmin();
PreCondition pcPreCond = inCAEntry.getPreConditions();
String strTransition = null;
String strPreCond = null;
String strCond = null;
int iDestRoleIndex = 0;
int adminRoleIndex = 0;
iDestRoleIndex = rbac.getRoleIndex(inCAEntry.getRole());
adminRoleIndex = rbac.getRoleIndex(inCAEntry.getAdminRole());
if (pcPreCond.size() != 0) {
for (int iroleindex : pcPreCond.keySet()) {
int value = pcPreCond.getConditional(iroleindex);
if (value == 1) {
strCond = "$user$[" + iroleindex + "]=$True$";
} else {
strCond = "$user$[" + iroleindex + "]=$False$";
}
if (strPreCond == null) {
strPreCond = strCond;
} else {
strPreCond = strPreCond + " & " + strCond;
}
}
} else {
strPreCond = getTrue();
}
String strTemp = "user = $user$ & " +
"admin = $admin$ & " +
"$admin$[$adminRoleIndex$] = $True$ & " +
strPreCond + " & " +
"role = " + iDestRoleIndex + " & " +
"act = ADD: " + getTrue() + ";";
for (String vAdminUser : vAdminUsers) {
for (String vUser : vUsers) {
ST strTTrans = new ST(strTemp, '$', '$');
strTTrans.add("user", shortenUser(vUser));
strTTrans.add("admin", shortenUser(vAdminUser));
strTTrans.add("True", getTrue());
strTTrans.add("False", getFalse());
strTTrans.add("adminRoleIndex", adminRoleIndex);
if (strTransition == null) {
strTransition = strTTrans.render();
} else {
strTransition = strTransition + "\n" + strTTrans.render();
}
}
}
if (includeRuleComment) {
strTransition = "-- CA Rule: " + inCAEntry + "\n" + strTransition;
}
return strTransition;
}
public String addCREntryv2(Vector<String> vUsers, CREntry crentry) {
int adminRoleIndex = 0;
Vector<String> vAdminUsers = rbac.getAdmin();
String strTransition = null;
int iDestRoleIndex = 0;
try {
iDestRoleIndex = rbac.getRoleIndex(crentry.getStrRole());
if (crentry.getPreCond().equalsIgnoreCase("true")) {
adminRoleIndex = -1;
} else if (crentry.getPreCond().equalsIgnoreCase("false")) {
adminRoleIndex = -2;
} else {
adminRoleIndex = rbac.getRoleIndex(crentry.getPreCond());
}
} catch (Exception e) {
e.printStackTrace();
}
String strTemp;
strTemp = "user = $user$ & admin = $admin$ & $precondition$ & role = " + iDestRoleIndex + " & act = REMOVE: "
+ getFalse() + ";";
for (String vAdminUser : vAdminUsers) {
for (String vUser : vUsers) {
ST strTTrans = new ST(strTemp, '$', '$');
strTTrans.add("user", shortenUser(vUser));
strTTrans.add("admin", shortenUser(vAdminUser));
if (adminRoleIndex == -1)
strTTrans.add("precondition", getTrue());
else if (adminRoleIndex == -2)
strTTrans.add("precondition", getFalse());
else
strTTrans.add("precondition", vAdminUser + "[" + adminRoleIndex + "]=" + getTrue());
if (strTransition == null) {
strTransition = strTTrans.render();
} else {
strTransition = strTransition + "\n" + strTTrans.render();
}
}
}
if (includeRuleComment) {
strTransition = "-- CR Rule: " + crentry + "\n" + strTransition;
}
return strTransition;
}
// OLD Versions
public void setupUserTransitionsv1(ST strTCodeTemplate) {
Vector<String> vUsers = rbac.getUsers();
for (int i = 0; i < vUsers.size(); i++) {
......@@ -249,13 +479,13 @@ public class WriteNuSMV {
System.out.println("Writing for user " + vUsers.get(i));
}
String strUser = vUsers.get(i);
String strTransitions = this.setupEachUser(strUser);
String strTransitions = this.setupEachUserv1(strUser);
strTCodeTemplate.add("transitions", strTransitions);
}
}
public String setupEachUser(String inUser) {
public String setupEachUserv1(String inUser) {
Vector<String> vRoles = rbac.getRoles();
String strUserSection = null;
......@@ -270,7 +500,7 @@ public class WriteNuSMV {
if (vCA != null) {
for (int j = 0; j < vCA.size(); j++) {
String strTmpTrans = addCAEntry(inUser, vCA.get(j));
String strTmpTrans = addCAEntryv1(inUser, vCA.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
......@@ -284,7 +514,7 @@ public class WriteNuSMV {
if (vCR != null) {
for (int j = 0; j < vCR.size(); j++) {
String strTmpTrans = addCREntry(inUser, vCR.get(j));
String strTmpTrans = addCREntryv1(inUser, vCR.get(j));
if (transitions == null) {
transitions = new StringBuilder();
transitions = transitions.append(strTmpTrans);
......@@ -319,7 +549,7 @@ public class WriteNuSMV {
return strUserSection;
}
public String addCAEntry(String inUser, CAEntry inCAEntry) {
public String addCAEntryv1(String inUser, CAEntry inCAEntry) {
Vector<String> vAdminUsers = rbac.getAdmin();
String strTransition = null;
......@@ -394,7 +624,7 @@ public class WriteNuSMV {
return strTransition;
}
public String addCREntry(String inUser, CREntry crentry) {
public String addCREntryv1(String inUser, CREntry crentry) {
int adminRoleIndex = 0;
Vector<String> vAdminUsers = rbac.getAdmin();
......
......@@ -12,6 +12,7 @@ import mohawk.collections.RoleDepTree;
import mohawk.global.nusmv.NuSMV;
import mohawk.global.pieces.mohawk.*;
import mohawk.global.results.ExecutionResult;
import mohawk.global.timing.MohawkTiming;
import mohawk.math.CalculateDiameter;
import mohawk.output.WriteNuSMV;
import mohawk.output.WriteRBACSpec;
......@@ -46,10 +47,15 @@ public class RolesAbsRefine {
private NuSMVMode mode;// mode
public boolean skipSMVFile = false;
private Integer returnValue = null;
public RolesAbsRefine(RBACInstance inRbac) {
// Timing
public MohawkTiming timing;
public String timingPrefix;
public RolesAbsRefine(RBACInstance inRbac, MohawkTiming timing, String timingPrefix) {
this.timing = timing;
this.timingPrefix = timingPrefix;
mode = NuSMVMode.BMC;// Default mode is BMC
k = 2;
......@@ -89,8 +95,9 @@ public class RolesAbsRefine {
return sAdminRoles;
}
public Boolean getResult(RBACInstance curInstance, Integer fileno) throws IOException, InterruptedException {
WriteNuSMV nusmv = new WriteNuSMV("logs/smvinstancefile" + fileno + ".txt", "smvtemplate");
public Boolean getResult(RBACInstance curInstance, Integer fileno) throws Exception {
WriteNuSMV nusmv = new WriteNuSMV("logs/smvinstancefile" + fileno + ".txt", "smvtemplate",
timing, timingPrefix);
nusmv.fillAttributes(curInstance);
if (!skipSMVFile) {
......@@ -196,25 +203,25 @@ public class RolesAbsRefine {
}
public boolean refineRoles() {
if (nextsetroles.size() == allroles.size())
return false;
if (nextsetroles.size() == allroles.size()) { return false; }
// Set<String> incrementRoles = rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>();// =
// rdeptree.getRoles(refinementstep);
Set<String> incrementRoles = new HashSet<String>();// = rdeptree.getRoles(refinementstep);
for (int i = 0; i < k; i++) {
Set<String> sNextQueue = this.rdeptree.getRoles(lastpriority);
if (sNextQueue != null) {
incrementRoles.addAll(sNextQueue);
lastpriority++;
} else
} else {
break;
}
}
if (incrementRoles.size() == 0)
if (incrementRoles.size() == 0) {
return false;
else
} else {
nextsetroles.addAll(incrementRoles);
}
refinementstep++;
......
......@@ -7,6 +7,7 @@ import java.util.*;
import java.util.logging.Logger;
import mohawk.global.pieces.mohawk.*;
import mohawk.global.timing.MohawkTiming;
import mohawk.rbac.RBACInstance;
/**
......@@ -33,13 +34,18 @@ public class RoleSlicer {
private Vector<String> vPositiveDeps;
private Vector<String> vNegativeDeps;
// Timing
public MohawkTiming timing;
public String timingPrefix;
/*
* This is a map between role indices of unsliced roles and and sliced roles.
*/
private Map<Integer, Integer> mapRoleIndex;
public RoleSlicer(RBACInstance inRbac) {
public RoleSlicer(RBACInstance inRbac, MohawkTiming timing, String timingPrefix) {
this.timing = timing;
this.timingPrefix = timingPrefix;
unsliced = inRbac;
strRole = unsliced.getSpec().get(1);
strUser = unsliced.getSpec().get(0);
......@@ -48,20 +54,41 @@ public class RoleSlicer {
}
public RBACInstance getSlicedPolicy() throws Exception {
/* TIMING */timing.startTimer(timingPrefix + " (slicingTotal)");
System.out.println("Slicing roles");
System.out.println("[START] getSlicedPolicy()");
System.out.println("[START] Slicing roles");
/* TIMING */timing.startTimer(timingPrefix + " (slicing roles)");
slicedRoles = createSlicedRoles();
System.out.println("Slicing users");
/* TIMING */timing.stopTimer(timingPrefix + " (slicing roles)");
System.out.println("[START] Slicing users");
/* TIMING */timing.startTimer(timingPrefix + " (slicing users)");
slicedUsers = sliceUsers();
System.out.println("Slicing admin");
/* TIMING */timing.stopTimer(timingPrefix + " (slicing users)");
System.out.println("[START] Slicing admin");
/* TIMING */timing.startTimer(timingPrefix + " (slicing admin)");
slicedAdmin = unsliced.getAdmin();
System.out.println("Slicing UA");
/* TIMING */timing.stopTimer(timingPrefix + " (slicing admin)");
System.out.println("[START] Slicing UA");
/* TIMING */timing.startTimer(timingPrefix + " (slicing UA)");
slicedUA = sliceUA();
System.out.println("Slicing CA");
/* TIMING */timing.stopTimer(timingPrefix + " (slicing UA)");
System.out.println("[START] Slicing CA");
/* TIMING */timing.startTimer(timingPrefix + " (slicing CA)");
slicedCA = sliceCA();
System.out.println("Slicing CR");
/* TIMING */timing.stopTimer(timingPrefix + " (slicing CA)");
System.out.println("[START] Slicing CR");
/* TIMING */timing.startTimer(timingPrefix + " (slicing CR)");
slicedCR = sliceCR();
/* TIMING */timing.stopTimer(timingPrefix + " (slicing CR)");
/* TIMING */timing.stopTimer(timingPrefix + " (slicingTotal)");
return new RBACInstance(slicedRoles, slicedUsers, slicedAdmin, slicedUA, slicedCR, slicedCA,
unsliced.getSpec());
}
......
......@@ -45,7 +45,7 @@ public class TestRunner implements Callable<TestingResult> {
logger.info("[TestRunner] Running the Abstraction-Refinement Step");
result = absrefine.absrefineloop();
}
return new TestingResult(result, (long) 0, "", "Return Result: " + absrefine.getReturnValue());
return new TestingResult(result, (long) 0, "", absrefine.getReturnValue(), "");
}
}
......@@ -108,7 +108,7 @@ public class TestingSuite {
logger.info("[Slicing] Slicing the Spec File");
/* TIMING */settings.timing.startTimer(timerName + " (slicing)");
RoleSlicer roleslicer = new RoleSlicer(rbac);
RoleSlicer roleslicer = new RoleSlicer(rbac, settings.timing, timerName);
rbac = roleslicer.getSlicedPolicy();
logger.info("[DETAILS] After Slicing -> Number of Roles: " + rbac.getNumRoles()
......@@ -133,7 +133,7 @@ public class TestingSuite {
logger.severe(e.getMessage());
}
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
RolesAbsRefine absrefine = new RolesAbsRefine(rbac, settings.timing, timerName);
absrefine.setMode(modes.get(j));
// Setup Timeout Timer
......@@ -142,20 +142,15 @@ public class TestingSuite {
logger.info("[RUNNING] Running Mohawk on testcase " + (i + 1) + "/" + numSpecFiles + " (mode="
+ modes.get(j) + "):");
/* TIMING */settings.timing.startTimer(timerName + " (TestRunner)");
if (settings.TIMEOUT_SECONDS == 0) {
settings.lastResult = future.get();
} else {
settings.lastResult = future.get(settings.TIMEOUT_SECONDS, TimeUnit.SECONDS);
}
System.out
.println("Result: " + settings.lastResult + " for role '" + absrefine.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ absrefine.getSpecRole()
+ "' in following spec file (in mode "
+ modes.get(j) + "): " + specFile);
/* TIMING */settings.timing.stopTimer(timerName + " (TestRunner)");
/* TIMING */settings.timing.stopTimer(timerName);
settings.lastResult._duration = settings.timing.getLastElapsedTime();
settings.lastResult._filename = settings.smvHelper.specFiles.get(i).getAbsolutePath();
if (settings.lastResult._comment == null || settings.lastResult._comment.isEmpty()) {
......@@ -163,6 +158,14 @@ public class TestingSuite {
} else {
settings.lastResult._comment += "; " + comment;
}
System.out.println("Result: " + settings.lastResult +
" for role '" + absrefine.getSpecRole() + "'");
logger.info("[COMPLETED] Result: " + settings.lastResult + ", for the Spec Role: '"
+ absrefine.getSpecRole()
+ "' in following spec file (in mode "
+ modes.get(j) + "): " + specFile);
settings.results.add(settings.lastResult);
settings.results.writeOutLast(resultsFW);
} catch (TimeoutException e) {
......@@ -172,8 +175,9 @@ public class TestingSuite {
settings.lastResult = new TestingResult(ExecutionResult.TIMEOUT,
settings.timing.getLastElapsedTime(),
settings.smvHelper.specFiles.get(i),
comment + "; Retun Value: timeout");
"timeout", comment);
settings.results.writeOutLast(resultsFW);
} catch (OutOfMemoryError e) {
logger.warning("[OUT OF MEMORY] Mohawk has ran out of memory out for SPEC file: " + specFile);
/* TIMING */settings.timing.cancelTimer(timerName);
......@@ -181,8 +185,9 @@ public class TestingSuite {
settings.lastResult = new TestingResult(ExecutionResult.OUT_OF_MEMORY,
settings.timing.getLastElapsedTime(),
settings.smvHelper.specFiles.get(i),
comment + "; Retun Value: out_of_memory");
"out_of_memory", comment);
settings.results.writeOutLast(resultsFW);
} catch (InterruptedException e) {
if (logger.getLevel() == Level.FINEST) {
e.printStackTrace();
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment