00001 package gov.nasa.arc.ase.jpf.tools;
00002
00003
00004 import edu.ksu.cis.bandera.specification.predicate.analysis.*;
00005 import edu.ksu.cis.bandera.specification.predicate.node.*;
00006 import gov.nasa.arc.ase.jpf.JPFErrorException;
00007 import java.io.*;
00008 import java.lang.reflect.*;
00009 import java.util.Hashtable;
00010
00011 public class Translation extends DepthFirstAdapter {
00012 public Class thisType;
00013 public Method thisMethod;
00014 public Hashtable params;
00015 public PrintStream out;
00016 public static String dir = ".";
00017 public Translation(Class c, Method m) {
00018 thisType = c;
00019 thisMethod = m;
00020 params = new Hashtable();
00021 }
00022 public Translation(Class c, Method m, String d)
00023 {
00024 this(c,m);
00025 if (d != null) dir = d;
00026 }
00027 public void caseAExpressionPropositionDefinition(AExpressionPropositionDefinition node) {
00028 String id = node.getId().getText();
00029 String cname = getClassName(thisType == null ? null : thisType.getName(),
00030 null, id);
00031 out = getClassFile(cname);
00032
00033 printHeader(cname);
00034 printParams(node.getParams());
00035
00036 out.print(" return ");
00037 printExpression(node.getColonExp());
00038 out.println(";");
00039
00040 out.println(" }");
00041
00042 out.println("}");
00043 }
00044 public void caseAInvokePropositionDefinition(AInvokePropositionDefinition node) {
00045 String id = node.getId().getText();
00046 String cname = getClassName(thisType.getName(), Signature.getSignature(thisMethod), id);
00047 out = getClassFile(cname);
00048
00049 printHeader(cname);
00050 printParams(node.getParams());
00051
00052 out.println(" int nt = s.getThreadCount();");
00053 out.println();
00054 out.println(" for(int i = 0; i < nt; i++) {");
00055 out.println(" Thread t = s.getThread(i);");
00056 out.println();
00057 if(Modifier.isStatic(thisMethod.getModifiers()))
00058 out.print(" if(");
00059 else {
00060 out.println(" if(t.isCalleeThis(" + classNameOf(thisType.getName()) + "$this) &&");
00061 out.print(" ");
00062 }
00063 out.println("t.atInvoke(\"" + thisType.getName() + "." + Signature.getSignature(thisMethod) + "\"))");
00064 if(node.getColonExp() != null) {
00065 out.print(" if(");
00066 printExpression(node.getColonExp());
00067 out.println(")");
00068 out.println(" return true;");
00069 } else
00070 out.println(" return true;");
00071 out.println(" }");
00072 out.println();
00073 out.println(" return false;");
00074 out.println(" }");
00075 out.println();
00076 out.println(" public static String observable() {");
00077 out.println(" return \"invoke." + thisType.getName() + "." + Signature.getSignature(thisMethod) + "\";");
00078 out.println(" }");
00079 out.println();
00080 out.println("}");
00081 }
00082 public void caseALocationPropositionDefinition(ALocationPropositionDefinition node) {
00083 String id = node.getId().getText();
00084 String cname = getClassName(thisType.getName(), Signature.getSignature(thisMethod), id);
00085 out = getClassFile(cname);
00086
00087 printHeader(cname);
00088 printParams(node.getParams());
00089
00090 out.println(" int nt = s.getThreadCount();");
00091 out.println();
00092 out.println(" for(int i = 0; i < nt; i++) {");
00093 out.println(" Thread t = s.getThread(i);");
00094 out.println();
00095 if(Modifier.isStatic(thisMethod.getModifiers()))
00096 out.print(" if(");
00097 else {
00098 out.println(" if(t.isThis(" + classNameOf(thisType.getName()) + "$this) &&");
00099 out.print(" ");
00100 }
00101 out.println("t.atLabel(\"" + node.getId().getText() + "\"))");
00102 if(node.getColonExp() != null) {
00103 out.print(" if(");
00104 printExpression(node.getColonExp());
00105 out.println(")");
00106 out.println(" return true;");
00107 } else
00108 out.println(" return true;");
00109 out.println(" }");
00110 out.println();
00111 out.println(" return false;");
00112 out.println(" }");
00113 out.println();
00114 out.println(" public static String observable() {");
00115 out.println(" return \"label." + node.getId().getText() + "\";");
00116 out.println(" }");
00117 out.println();
00118 out.println("}");
00119 }
00120 public void caseAReturnPropositionDefinition(AReturnPropositionDefinition node) {
00121 String id = node.getId().getText();
00122 String cname = getClassName(thisType.getName(), Signature.getSignature(thisMethod), id);
00123 out = getClassFile(cname);
00124
00125 printHeader(cname);
00126 printParams(node.getParams());
00127
00128 out.println(" int nt = s.getThreadCount();");
00129 out.println();
00130 out.println(" for(int i = 0; i < nt; i++) {");
00131 out.println(" Thread t = s.getThread(i);");
00132 out.println();
00133 if(Modifier.isStatic(thisMethod.getModifiers()))
00134 out.print(" if(");
00135 else {
00136 out.println(" if(t.isThis(" + classNameOf(thisType.getName()) + "$this) &&");
00137 out.print(" ");
00138 }
00139 out.println("t.atReturn() && t.atMethod(\"" + thisType.getName() + "." + Signature.getSignature(thisMethod) + "\"))");
00140 if(node.getColonExp() != null) {
00141 out.print(" if(");
00142 printExpression(node.getColonExp());
00143 out.println(")");
00144 out.println(" return true;");
00145 } else
00146 out.println(" return true;");
00147 out.println(" }");
00148 out.println();
00149 out.println(" return false;");
00150 out.println(" }");
00151 out.println();
00152 out.println(" public static String observable() {");
00153 out.println(" return \"return." + thisType.getName() + "." + Signature.getSignature(thisMethod) + "\";");
00154 out.println(" }");
00155 out.println();
00156 out.println("}");
00157 }
00158 private static String classNameOf(String name) {
00159 if(name.indexOf('.') == -1) return name;
00160
00161 return name.substring(name.lastIndexOf('.')+1);
00162 }
00163 private static String getBaseName(String mname) {
00164 if(mname.indexOf('(') != -1)
00165 return mname.substring(0, mname.indexOf('('));
00166 else
00167 return mname;
00168 }
00169 private static PrintStream getClassFile(String name) {
00170 try {
00171 PrintStream out = new PrintStream(new FileOutputStream(new File(dir, classNameOf(name) + ".java")));
00172 System.out.println(name + ":");
00173 return out;
00174 } catch(IOException e) {
00175 throw new JPFErrorException("Can't create file " + classNameOf(name) + ".java");
00176 }
00177 }
00178 private String getClassName(String cname, String method, String id) {
00179 if(cname != null)
00180 if(method != null)
00181 return cname+ "$" + getBaseName(method) + "$" + id;
00182 else
00183 return cname + "$" + id;
00184 else
00185 return id;
00186 }
00187 private static String packageNameOf(String name) {
00188 if(name.indexOf('.') == -1) return null;
00189
00190 return name.substring(0, name.lastIndexOf('.'));
00191 }
00192 private void printExpression(Node node) {
00193 if(node != null) {
00194 if(thisType != null) out.print(classNameOf(thisType.getName()) + "$this != null && ");
00195 node.apply(new Expression(this));
00196 }
00197 }
00198 private void printHeader(String name) {
00199 if(packageNameOf(name) != null) {
00200 out.println("package " + packageNameOf(name) + ";");
00201 out.println();
00202 }
00203 out.println("import gov.nasa.arc.ase.jpf.jvm.State;");
00204 out.println("import gov.nasa.arc.ase.jpf.jvm.Reference;");
00205 out.println("import gov.nasa.arc.ase.jpf.jvm.Thread;");
00206 out.println();
00207 out.println("public class " + classNameOf(name) + " {");
00208 }
00209 private void printParams(Node node) {
00210 out.print(" public static boolean evaluate(State s");
00211 if(node != null)
00212 node.apply(new Parameters(this));
00213 out.println(") {");
00214 }
00215 }
