Skip to content

GitLab

mohawk-2.0
mohawk-2.0
Commit 0e40a234 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files
Options

Updated to ANTLR 4.4 and StringTemplate V4; tested by running AHN's test and... 

Updated to ANTLR 4.4 and StringTemplate V4; tested by running AHN's test and by running every test under data/testcases/positive/ (with  abstraction refinement on)
parent 4d32f444
Hide whitespace changes
Inline Side-by-side
Showing with 227 additions and 457 deletions
.classpath
View file @ 0e40a234
......@@ -2,11 +2,6 @@
<classpath>
<classpathentry kind="src" path="src"/>
<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
<classpathentry kind="lib" path="lib/antlr-3.2.jar">
<attributes>
<attribute name="javadoc_location" value="http://www.antlr.org/api/Java/"/>
</attributes>
</classpathentry>
<classpathentry kind="lib" path="lib/commons-cli-1.2.jar">
<attributes>
<attribute name="javadoc_location" value="http://commons.apache.org/proper/commons-cli/javadocs/api-1.2/"/>
......@@ -28,6 +23,7 @@
<attribute name="javadoc_location" value="http://www.stringtemplate.org/api/"/>
</attributes>
</classpathentry>
<classpathentry kind="lib" path="lib/antlr-4.4-complete.jar"/>
<classpathentry combineaccessrules="false" kind="src" path="/Mohawk-T Globals"/>
<classpathentry kind="output" path="bin"/>
</classpath>
build.xml
View file @ 0e40a234
......@@ -16,10 +16,13 @@
<property name="dist" location="${bin}/dist" />
<property name="qtest" location="${data}/testcases" />
<property name="mohawksrc" location="${src}/mohawk" />
<property name="antlr-script" location="${mohawksrc}/rbac/generated" />
<property name="template" location="${mohawksrc}/output" />
<property name="rbac" location="${mohawksrc}/rbac/generated" />
<property name="antlr" location="${lib}/antlr-3.2.jar" />
<property name="antlr" location="${lib}/antlr-4.4-complete.jar" />
<property name="junit" location="${lib}/junit-4.12.jar" />
<property name="parser-package" value="mohawk.rbac.generated" />
<!-- Customize this line to point to the 'Mohawk-T Globals' Project's source folder -->
<property name="src.globals" location="../Mohawk-T Globals/src" />
......@@ -43,11 +46,20 @@
<target name="parser" depends="init" description="generate parser files">
<!-- Create the parser files -->
<antlr target="${rbac}/rbac.g" outputdirectory="${rbac}">
<!--
<antlr target="${rbac}/Mohawk.g4" outputdirectory="${rbac}">
<classpath>
<pathelement location="${antlr}" />
</classpath>
</antlr>
-->
<java jar="${antlr}" fork="true">
<arg value="-o" />
<arg value="${antlr-script}" />
<arg value="-package" />
<arg value="${parser-package}" />
<arg value="${antlr-script}/Mohawk.g4" />
</java>
</target>
<target name="compile" depends="parser" description="compile the source ">
......
data/ahn/test.st 0 → 100644
View file @ 0e40a234
CONFIG 16 5
GOAL 15 2
can_assign 1 , t3 , 9 -2 ; t2 , 15
can_assign true , t3 , true ; t3 , 1
can_assign 1 , t3 , true ; t2 , 9
can_enable true , t4 , true ; t3 , 1
can_enable true , t4 , true ; t2 , 15
data/ahn/test.st.mohawk.T.mohawk 0 → 100644
View file @ 0e40a234
Roles role1_COMBINED_AL3_t3 role1_COMBINED_AL1_t2 role1_COMBINED_AL1_t3 role1_COMBINED_AL1_t4 role2_AL3_t2 role1_AL3_t3 role2_AL1_t2 role1_AL1_t3 __u0goalRole_t2 role1_ENABLED_AL3_t3 role1_COMBINED__UAT__ALx2_t2 role1_COMBINED__UAT__ALx2_t3 role15_ENABLED_AL3_t2 role15_ENABLED_AL1_t2 role1_COMBINED__UAT__ALx2_t4 role15_AL1_t2 role1_COMBINED__UAT__ALx0_t3 role15_AL3_t2 role1_ENABLED_AL1_t3 role9_AL2_t2 role1_COMBINED_AL2_t2 role1_COMBINED_AL2_t3 role1_COMBINED_AL2_t4 role2_AL2_t2 role1_COMBINED_AL0_t3 role1_COMBINED_AL0_t2 role1_AL0_t3 role1_AL2_t3 role1_COMBINED__UAT__ALx3_t3 role15_ENABLED_AL2_t2 role1_COMBINED__UAT__ALx3_t2 role1_COMBINED__UAT__ALx1_t2 role15_ENABLED_AL0_t2 role1_COMBINED__UAT__ALx1_t3 role1_COMBINED__UAT__ALx3_t4 role1_COMBINED__UAT__ALx1_t4 role1_ENABLED__UAT__ALx0_t1 role1_ENABLED_AL0_t3 role15_AL2_t2 role9_AL1_t2 role1_ENABLED_AL2_t3 role9_AL3_t2 role1__UAT__ALx0_t1 role1_COMBINED_AL0_t4 AdminRole;
Users AdminUser User;
UA <AdminUser,AdminRole>;
CR ;
CA <AdminRole,TRUE,role1_AL0_t3> <AdminRole,TRUE,role1_ENABLED_AL0_t3> <AdminRole,TRUE,role15_ENABLED_AL0_t2> <AdminRole,role1__UAT__ALx0_t1&role1_ENABLED__UAT__ALx0_t1,role1_COMBINED__UAT__ALx0_t3> <AdminRole,role1__UAT__ALx0_t1&role1_ENABLED__UAT__ALx0_t1,role1_COMBINED__UAT__ALx0_t3> <AdminRole,role9_AL1_t2&-role2_AL1_t2&role1_COMBINED__UAT__ALx1_t3,role15_AL1_t2> <AdminRole,role9_AL2_t2&-role2_AL2_t2&role1_COMBINED__UAT__ALx2_t3,role15_AL2_t2> <AdminRole,role9_AL3_t2&-role2_AL3_t2&role1_COMBINED__UAT__ALx3_t3,role15_AL3_t2> <AdminRole,TRUE,role1_AL1_t3> <AdminRole,TRUE,role1_AL2_t3> <AdminRole,TRUE,role1_AL3_t3> <AdminRole,role1_COMBINED__UAT__ALx1_t3,role9_AL1_t2> <AdminRole,role1_COMBINED__UAT__ALx2_t3,role9_AL2_t2> <AdminRole,role1_COMBINED__UAT__ALx3_t3,role9_AL3_t2> <AdminRole,TRUE,role1_ENABLED_AL1_t3> <AdminRole,TRUE,role1_ENABLED_AL2_t3> <AdminRole,TRUE,role1_ENABLED_AL3_t3> <AdminRole,TRUE,role15_ENABLED_AL1_t2> <AdminRole,TRUE,role15_ENABLED_AL2_t2> <AdminRole,TRUE,role15_ENABLED_AL3_t2> <AdminRole,role1_AL1_t3&role1_ENABLED_AL1_t3,role1_COMBINED_AL1_t3> <AdminRole,role1_AL2_t3&role1_ENABLED_AL2_t3,role1_COMBINED_AL2_t3> <AdminRole,role1_AL3_t3&role1_ENABLED_AL3_t3,role1_COMBINED_AL3_t3> <AdminRole,role1_AL1_t3&role1_ENABLED_AL1_t3,role1_COMBINED_AL1_t3> <AdminRole,role1_AL2_t3&role1_ENABLED_AL2_t3,role1_COMBINED_AL2_t3> <AdminRole,role1_AL3_t3&role1_ENABLED_AL3_t3,role1_COMBINED_AL3_t3> <AdminRole,role1_COMBINED_AL0_t2,role1_COMBINED__UAT__ALx1_t2> <AdminRole,role1_COMBINED_AL0_t3,role1_COMBINED__UAT__ALx1_t3> <AdminRole,role1_COMBINED_AL0_t4,role1_COMBINED__UAT__ALx1_t4> <AdminRole,role1_COMBINED__UAT__ALx1_t2,role1_COMBINED__UAT__ALx2_t2> <AdminRole,role1_COMBINED__UAT__ALx1_t2,role1_COMBINED__UAT__ALx2_t3> <AdminRole,role1_COMBINED__UAT__ALx1_t2,role1_COMBINED__UAT__ALx2_t4> <AdminRole,role1_COMBINED_AL1_t2,role1_COMBINED__UAT__ALx2_t2> <AdminRole,role1_COMBINED_AL1_t3,role1_COMBINED__UAT__ALx2_t3> <AdminRole,role1_COMBINED_AL1_t4,role1_COMBINED__UAT__ALx2_t4> <AdminRole,role1_COMBINED__UAT__ALx2_t2,role1_COMBINED__UAT__ALx3_t2> <AdminRole,role1_COMBINED__UAT__ALx2_t2,role1_COMBINED__UAT__ALx3_t3> <AdminRole,role1_COMBINED__UAT__ALx2_t2,role1_COMBINED__UAT__ALx3_t4> <AdminRole,role1_COMBINED_AL2_t2,role1_COMBINED__UAT__ALx3_t2> <AdminRole,role1_COMBINED_AL2_t3,role1_COMBINED__UAT__ALx3_t3> <AdminRole,role1_COMBINED_AL2_t4,role1_COMBINED__UAT__ALx3_t4> <AdminRole,role15_AL3_t2,__u0goalRole_t2>;
ADMIN AdminUser;
SPEC User __u0goalRole_t2;
data/testcases/positive/test01.mohawk
View file @ 0e40a234
/*
* test01.mohawk
* Expected Result: REACHABLE
*/
Roles role0 role1 role2 role3;
Users user0 user1 user2 user3 user4;
......@@ -6,7 +10,16 @@ UA <user4,role3>;
CR <FALSE,role0> <FALSE,role2>;
CA <role3,role2,role0> <role3,role2&role1,role0> <role3,role2&role0,role1> <role3,TRUE,role1> <role3,role0,role1> <role3,role1&role0,role2> <role3,role0,role2> <role3,role1,role2> <role3,TRUE,role2>;
CA
/* CA 1 */ <role3,role2,role0>
/* CA 2 */ <role3,role2&role1,role0>
/* CA 3 */ <role3,role2&role0,role1>
/* CA 4 */ <role3,TRUE,role1>
/* CA 5 */ <role3,role0,role1>
/* CA 6 */ <role3,role1&role0,role2>
/* CA 7 */ <role3,role0,role2>
/* CA 8 */ <role3,role1,role2>
/* CA 9 */ <role3,TRUE,role2>;
ADMIN user4;
......
src/mohawk/output/WriteNuSMV.java
View file @ 0e40a234
......@@ -6,21 +6,15 @@
*/
package mohawk.output;
import java.io.BufferedReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.*;
import java.util.Map;
import java.util.Vector;
import java.util.logging.Level;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
import org.stringtemplate.v4.ST;
import org.antlr.stringtemplate.StringTemplate;
import mohawk.pieces.*;
import mohawk.rbac.RBACInstance;
/*
* This class is in charge of writing the NuSMV specification to a file using
......@@ -52,7 +46,7 @@ public class WriteNuSMV {
// RBAC Instance
private RBACInstance rbac;
private StringTemplate strTCodeTemplate;
private ST strTCodeTemplate;
private String strTransTemplate;
......@@ -69,14 +63,15 @@ public class WriteNuSMV {
done = false;
try {
strTCodeTemplate = new StringTemplate(getTemplateStr("smvtemplate.st"));
// String template = ConvertTo.readFile(this.getClass().getResource("smvtemplate.st"));
strTCodeTemplate = new ST(getTemplateStr("smvtemplate.st"), '$', '$');
strTransTemplate = getTemplateStr("transitions.st");
} catch (IOException e) {
e.printStackTrace();
}
}
public void setupUsers(StringTemplate inSmvSpec) {
public void setupUsers(ST inSmvSpec) {
int noRoles = rbac.getRoles().size();
Vector<String> vUsers = rbac.getUsers();
......@@ -84,24 +79,24 @@ public class WriteNuSMV {
for (int i = 0; i < vUsers.size(); i++) {
String user = vUsers.get(i);
inSmvSpec.setAttribute("userarrays", user + " : array 0.." + (noRoles - 1) + " of boolean");
inSmvSpec.add("userarrays", user + " : array 0.." + (noRoles - 1) + " of boolean");
if (olderVersion) {
inSmvSpec.setAttribute("users", user);
inSmvSpec.add("users", user);
} else {
inSmvSpec.setAttribute("users", shortenUser(user));
inSmvSpec.add("users", shortenUser(user));
}
}
for (int i = 0; i < vAdmin.size(); i++) {
String user = vAdmin.get(i);
if (olderVersion) {
inSmvSpec.setAttribute("admin", user);
inSmvSpec.add("admin", user);
} else {
inSmvSpec.setAttribute("admin", shortenUser(user));
inSmvSpec.add("admin", shortenUser(user));
}
}
inSmvSpec.setAttribute("role", "0 .. " + (noRoles - 1));
inSmvSpec.add("role", "0 .. " + (noRoles - 1));
}
......@@ -113,7 +108,7 @@ public class WriteNuSMV {
}
}
public void setupUA(StringTemplate inSmvSpec) {
public void setupUA(ST inSmvSpec) {
Vector<String> vUsers = rbac.getUsers();
Vector<String> vRoles = rbac.getRoles();
......@@ -139,7 +134,7 @@ public class WriteNuSMV {
}
String uaassign = "init(" + user + "[" + j + "]" + ") := " + value;
inSmvSpec.setAttribute("ua", uaassign);
inSmvSpec.add("ua", uaassign);
}
// mUA.remove(user);
}
......@@ -194,14 +189,14 @@ public class WriteNuSMV {
+ " & act = ADD: " + getTrue() + ";";
for (int i = 0; i < vAdminUsers.size(); i++) {
StringTemplate strTTrans = new StringTemplate(strTemp);
ST strTTrans = new ST(strTemp, '$', '$');
if (olderVersion) {
strTTrans.setAttribute("user", inUser);
strTTrans.setAttribute("admin", vAdminUsers.get(i));
strTTrans.add("user", inUser);
strTTrans.add("admin", vAdminUsers.get(i));
} else {
strTTrans.setAttribute("user", shortenUser(inUser));
strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
strTTrans.add("user", shortenUser(inUser));
strTTrans.add("admin", shortenUser(vAdminUsers.get(i)));
}
PreCondition pcPreCond = inCAEntry.getPreConditions();
String strPreCond = null;
......@@ -215,7 +210,7 @@ public class WriteNuSMV {
String strAdminCondRole = vAdminUsers.get(i) + "[" + adminRoleIndex + "] = " + getTrue();
strTTrans.setAttribute("admincond", strAdminCondRole);
strTTrans.add("admincond", strAdminCondRole);
if (pcPreCond.size() != 0) {
for (int iroleindex : pcPreCond.keySet()) {
......@@ -239,12 +234,12 @@ public class WriteNuSMV {
strPreCond = getTrue();
}
strTTrans.setAttribute("precondition", strPreCond);
strTTrans.add("precondition", strPreCond);
if (strTransition == null)
strTransition = strTTrans.toString();
strTransition = strTTrans.render();
else
strTransition = strTransition + "\n" + strTTrans.toString();
strTransition = strTransition + "\n" + strTTrans.render();
}
return strTransition;
......@@ -277,27 +272,27 @@ public class WriteNuSMV {
+ getFalse() + ";";
for (int i = 0; i < vAdminUsers.size(); i++) {
StringTemplate strTTrans = new StringTemplate(strTemp);
ST strTTrans = new ST(strTemp, '$', '$');
if (olderVersion) {
strTTrans.setAttribute("user", inUser);
strTTrans.setAttribute("admin", vAdminUsers.get(i));
strTTrans.add("user", inUser);
strTTrans.add("admin", vAdminUsers.get(i));
} else {
strTTrans.setAttribute("user", shortenUser(inUser));
strTTrans.setAttribute("admin", shortenUser(vAdminUsers.get(i)));
strTTrans.add("user", shortenUser(inUser));
strTTrans.add("admin", shortenUser(vAdminUsers.get(i)));
}
if (adminRoleIndex == -1)
strTTrans.setAttribute("precondition", getTrue());
strTTrans.add("precondition", getTrue());
else if (adminRoleIndex == -2)
strTTrans.setAttribute("precondition", getFalse());
strTTrans.add("precondition", getFalse());
else
strTTrans.setAttribute("precondition", vAdminUsers.get(i) + "[" + adminRoleIndex + "]=" + getTrue());
strTTrans.add("precondition", vAdminUsers.get(i) + "[" + adminRoleIndex + "]=" + getTrue());
if (strTransition == null)
strTransition = strTTrans.toString();
strTransition = strTTrans.render();
else
strTransition = strTransition + "\n" + strTTrans.toString();
strTransition = strTransition + "\n" + strTTrans.render();
}
return strTransition;
......@@ -322,7 +317,7 @@ public class WriteNuSMV {
Vector<CREntry> vCR = getMatchingCR(strRole);
StringBuilder transitions = null;
String strTmpUser = null;
StringTemplate strTTrans = new StringTemplate(strTransTemplate);
ST strTTrans = new ST(strTransTemplate, '$', '$');
if (vCA != null) {
for (int j = 0; j < vCA.size(); j++) {
......@@ -353,11 +348,11 @@ public class WriteNuSMV {
}
if (transitions != null) {
strTTrans.setAttribute("transition", transitions);
strTTrans.setAttribute("trueWord", getTrue());
strTTrans.setAttribute("roleindex1", inUser + "[" + i + "]");
strTTrans.setAttribute("roleindex2", inUser + "[" + i + "]");
strTmpUser = strTTrans.toString();
strTTrans.add("transition", transitions);
strTTrans.add("trueWord", getTrue());
strTTrans.add("roleindex1", inUser + "[" + i + "]");
strTTrans.add("roleindex2", inUser + "[" + i + "]");
strTmpUser = strTTrans.render();
} else {
strTmpUser = "next(" + inUser + "[" + i + "]) := " + inUser + "[" + i + "];";
}
......@@ -371,7 +366,7 @@ public class WriteNuSMV {
return strUserSection;
}
public void setupUserTransitions(StringTemplate strTCodeTemplate) {
public void setupUserTransitions(ST strTCodeTemplate) {
Vector<String> vUsers = rbac.getUsers();
for (int i = 0; i < vUsers.size(); i++) {
......@@ -381,11 +376,11 @@ public class WriteNuSMV {
String strUser = vUsers.get(i);
String strTransitions = this.setupEachUser(strUser);
strTCodeTemplate.setAttribute("transitions", strTransitions);
strTCodeTemplate.add("transitions", strTransitions);
}
}
public void setupSpec(StringTemplate strTCodeTemplate, String inStrUser, String inStrRole) {
public void setupSpec(ST strTCodeTemplate, String inStrUser, String inStrRole) {
int roleindex = 0;
try {
......@@ -394,9 +389,9 @@ public class WriteNuSMV {
e.printStackTrace();
}
strTCodeTemplate.setAttribute("user", inStrUser);
strTCodeTemplate.setAttribute("roleindex", roleindex);
strTCodeTemplate.setAttribute("falseWord", getFalse());
strTCodeTemplate.add("user", inStrUser);
strTCodeTemplate.add("roleindex", roleindex);
strTCodeTemplate.add("falseWord", getFalse());
}
......@@ -444,7 +439,7 @@ public class WriteNuSMV {
setupSpec(strTCodeTemplate, strUser, strRole);
// this.setupTransactions(this.strCodeTemplate, this.strCodeTemplate);
smvcode = strTCodeTemplate.toString();
smvcode = strTCodeTemplate.render();
done = true;
}
......
src/mohawk/output/WriteRBACSpec.java
View file @ 0e40a234
......@@ -3,20 +3,14 @@
*/
package mohawk.output;
import java.io.BufferedReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.*;
import java.util.Map;
import java.util.Vector;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.pieces.PreCondition;
import mohawk.rbac.RBACInstance;
import org.stringtemplate.v4.ST;
import org.antlr.stringtemplate.StringTemplate;
import mohawk.pieces.*;
import mohawk.rbac.RBACInstance;
/**
* @author Karthick Jayaraman This class is for writing an a generated RBAC instance to file.
......@@ -24,7 +18,7 @@ import org.antlr.stringtemplate.StringTemplate;
public class WriteRBACSpec {
// StringTemplate for RBAC instance
private StringTemplate STRBACSpec;
private ST STRBACSpec;
// RBAC instance to write to file.
private RBACInstance rbacinstance;
......@@ -32,7 +26,7 @@ public class WriteRBACSpec {
public WriteRBACSpec(String filename) {
try {
String strTemplateString = this.getTemplateStr(filename);
STRBACSpec = new StringTemplate(strTemplateString);
STRBACSpec = new ST(strTemplateString, '$', '$');
} catch (IOException e) {
e.printStackTrace();
}
......@@ -60,7 +54,7 @@ public class WriteRBACSpec {
for (int i = 0; i < vecRoles.size(); i++) {
String strRole = vecRoles.get(i);
this.STRBACSpec.setAttribute("roles", strRole);
this.STRBACSpec.add("roles", strRole);
}
}
......@@ -69,10 +63,10 @@ public class WriteRBACSpec {
Vector<String> vecAUsers = rbacinstance.getAdmin();
for (int i = 0; i < vecNUsers.size(); i++)
this.STRBACSpec.setAttribute("users", vecNUsers.get(i));
this.STRBACSpec.add("users", vecNUsers.get(i));
for (int i = 0; i < vecAUsers.size(); i++)
this.STRBACSpec.setAttribute("adminusers", vecAUsers.get(i));
this.STRBACSpec.add("adminusers", vecAUsers.get(i));
}
public void writeUA() {
......@@ -83,11 +77,11 @@ public class WriteRBACSpec {
Vector<Integer> vecUserUA = mUA.get(user);
for (int i = 0; i < vecUserUA.size(); i++) {
StringTemplate STUA = new StringTemplate("<$userroles; separator=\",\"$>");
ST STUA = new ST("<$userroles; separator=\",\"$>", '$', '$');
String role = rbacinstance.getRoles().get(vecUserUA.get(i));
STUA.setAttribute("userroles", user);
STUA.setAttribute("userroles", role);
this.STRBACSpec.setAttribute("ua", STUA.toString());
STUA.add("userroles", user);
STUA.add("userroles", role);
this.STRBACSpec.add("ua", STUA.render());
}
}
......@@ -95,7 +89,7 @@ public class WriteRBACSpec {
// write CR to the file.
public void writeCR() {
boolean setOne = false;
Map<String, Vector<CREntry>> mCR = rbacinstance.getCR();
// When the RBACInstance is created, it does not create CR rules of the
......@@ -105,43 +99,49 @@ public class WriteRBACSpec {
Vector<CREntry> vecCR = mCR.get(targetrole);
for (int i = 0; i < vecCR.size(); i++) {
CREntry cre = vecCR.get(i);
StringTemplate STCR = new StringTemplate("<$crrule; separator=\",\"$>");
ST STCR = new ST("<$crrule; separator=\",\"$>", '$', '$');
if (i < 2) {
// if(rndGen.nextInt(2) == 1)
// vecCR.get(i).setPreCond("FALSE");
STCR.setAttribute("crrule", cre.getPreCond());
STCR.add("crrule", cre.getPreCond());
}
STCR.setAttribute("crrule", cre.getStrRole());
STRBACSpec.setAttribute("cr", STCR.toString());
STCR.add("crrule", cre.getStrRole());
STRBACSpec.add("cr", STCR.render());
setOne = true;
}
}
if (setOne == false) {
// Removes error: "context [anonymous] 7:4 attribute cr isn't defined"
STRBACSpec.add("cr", "");
}
}
// write CA to the file.
public void writeCA() {
boolean setOne = false;
Map<String, Vector<CAEntry>> mCA = rbacinstance.getCA();
for (String targetrole : mCA.keySet()) {
Vector<CAEntry> vCA = mCA.get(targetrole);
for (int i = 0; i < vCA.size(); i++) {
StringTemplate STCR = new StringTemplate("<$crrule; separator=\",\"$>");
ST STCR = new ST("<$carule; separator=\",\"$>", '$', '$');
CAEntry cae = vCA.get(i);
String strAdminRole = cae.getAdminRole();
PreCondition PreCnd = cae.getPreConditions();
String strRole = cae.getRole();
STCR.setAttribute("crrule", strAdminRole);
STCR.add("carule", strAdminRole);
StringBuffer strPreCnd = null;
if (PreCnd.size() == 0) {
strPreCnd = new StringBuffer();
strPreCnd.append("TRUE"); // If there are no conditionals in
// the PreCondition, set the
// precondition to TRUE
// the PreCondition, set the
// precondition to TRUE
} else {
for (int key : PreCnd.keySet()) {
String tmpRole;
......@@ -161,17 +161,22 @@ public class WriteRBACSpec {
}
}
STCR.setAttribute("crrule", strPreCnd);
STCR.setAttribute("crrule", strRole);
this.STRBACSpec.setAttribute("ca", STCR.toString());
STCR.add("carule", strPreCnd.toString());
STCR.add("carule", strRole);
this.STRBACSpec.add("ca", STCR.render());
setOne = true;
}
}
if (setOne == false) {
// Removes error: "context [anonymous] 7:4 attribute ca isn't defined"
STRBACSpec.add("ca", "");
}
}
public void writeSpec() {
Vector<String> vSpec = rbacinstance.getSpec();
STRBACSpec.setAttribute("spec", vSpec.get(0));
STRBACSpec.setAttribute("spec", vSpec.get(1));
STRBACSpec.add("spec", vSpec.get(0));
STRBACSpec.add("spec", vSpec.get(1));
}
public void Write2File(RBACInstance inrbacinstance, String filename) throws IOException {
......@@ -191,7 +196,7 @@ public class WriteRBACSpec {
writeCA();
System.out.println("Writing SPEC");
writeSpec();
String filestring = STRBACSpec.toString();
String filestring = STRBACSpec.render();
file.write(filestring);
file.close();
......
src/mohawk/output/rbac.st
View file @ 0e40a234
......@@ -2,11 +2,11 @@ Roles $roles; separator=" "$;
Users $users; separator=" "$;
UA $ua; separator=" "$;
UA $ua; separator="\n"$;
CR $cr; separator=" "$;
CR $cr; separator="\n"$;
CA $ca; separator=" "$;
CA $ca; separator="\n"$;
ADMIN $adminusers; separator=" "$;
......
src/mohawk/rbac/RBAC2SMV.java
View file @ 0e40a234
......@@ -28,22 +28,16 @@
*/
package mohawk.rbac;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
import java.io.Reader;
import java.util.Collection;
import java.util.Iterator;
import java.util.Map;
import java.util.Vector;
import java.io.*;
import java.util.*;
import org.antlr.v4.runtime.*;
import mohawk.output.WriteNuSMV;
import mohawk.pieces.CAEntry;
import mohawk.pieces.CREntry;
import mohawk.rbac.generated.RBACLexer;
import mohawk.rbac.generated.RBACParser;
import antlr.RecognitionException;
import antlr.TokenStreamException;
import mohawk.rbac.generated.MohawkLexer;
import mohawk.rbac.generated.MohawkParser;
/**
* @author Karthick Jayaraman This is the main class that will serve as an entry point to the tool.
......@@ -88,29 +82,19 @@ public class RBAC2SMV {
String nusmvfile = args[1];
Reader reader = new FileReader(args[0]);
RBACLexer lexer = new RBACLexer(reader);
RBACParser parser = new RBACParser(lexer);
InputStream is = new FileInputStream(args[0]);
ANTLRInputStream input = new ANTLRInputStream(is);
MohawkLexer lexer = new MohawkLexer(input);
CommonTokenStream tokens = new CommonTokenStream(lexer);
MohawkParser parser = new MohawkParser(tokens);
RBACInstance rbac = null;
parser.initRbac();
try {
parser.roles();
parser.users();
parser.ua();
parser.cr();
parser.ca();
parser.admin();
parser.spec();
parser.init();
rbac = parser.getRBAC();
} catch (RecognitionException e) {
......
src/mohawk/rbac/RBACPAT.java
View file @ 0e40a234
......@@ -3,25 +3,15 @@
*/
package mohawk.rbac;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.Reader;