AbstractionGenerator.java Source File

00001 package edu.ksu.cis.bandera.abstraction.specification;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 2000   Robby (robby@cis.ksu.edu)                    *
00006  * All rights reserved.                                              *
00007  *                                                                   *
00008  * This work was done as a project in the SAnToS Laboratory,         *
00009  * Department of Computing and Information Sciences, Kansas State    *
00010  * University, USA (http://www.cis.ksu.edu/santos).                  *
00011  * It is understood that any modification not identified as such is  *
00012  * not covered by the preceding statement.                           *
00013  *                                                                   *
00014  * This work is free software; you can redistribute it and/or        *
00015  * modify it under the terms of the GNU Library General Public       *
00016  * License as published by the Free Software Foundation; either      *
00017  * version 2 of the License, or (at your option) any later version.  *
00018  *                                                                   *
00019  * This work is distributed in the hope that it will be useful,      *
00020  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00021  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00022  * Library General Public License for more details.                  *
00023  *                                                                   *
00024  * You should have received a copy of the GNU Library General Public *
00025  * License along with this toolkit; if not, write to the             *
00026  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00027  * Boston, MA  02111-1307, USA.                                      *
00028  *                                                                   *
00029  * Java is a trademark of Sun Microsystems, Inc.                     *
00030  *                                                                   *
00031  * To submit a bug report, send a comment, or get the latest news on *
00032  * this project and other SAnToS projects, please visit the web-site *
00033  *                http://www.cis.ksu.edu/santos                      *
00034  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00035 import java.util.*;
00036 import java.io.*;
00037 import edu.ksu.cis.bandera.abstraction.*;
00038 import edu.ksu.cis.bandera.abstraction.specification.node.*;
00039 import edu.ksu.cis.bandera.abstraction.specification.lexer.*;
00040 import edu.ksu.cis.bandera.abstraction.specification.parser.*;
00041 import edu.ksu.cis.bandera.abstraction.specification.analysis.*;
00042 public class AbstractionGenerator extends DepthFirstAdapter {
00043     private static final String lineSeparator = System.getProperty("line.separator");
00044     private static final Hashtable opNameTable = new Hashtable();
00045     static {
00046         opNameTable.put("+", "add");
00047         opNameTable.put("-", "sub");
00048         opNameTable.put("*", "mul");
00049         opNameTable.put("/", "div");
00050         opNameTable.put("%", "rem");
00051         opNameTable.put("==", "eq");
00052         opNameTable.put("!=", "ne");
00053         opNameTable.put(">=", "ge");
00054         opNameTable.put("<=", "le");
00055         opNameTable.put(">", "gt");
00056         opNameTable.put("<", "lt");
00057     }
00058 
00059     private Vector errors = new Vector();
00060     private Vector warnings = new Vector();
00061     private String type;
00062     
00063     //
00064     private StringBuffer buffer;
00065     private Node node;
00066     private String superTypeName;
00067     private String packageName;
00068     private String abstractionName;
00069     private Vector tokenSet;
00070     private HashSet one2oneSet;
00071     private Collection tempCollection;
00072     private String[] fields;
00073     private Vector absFunctions;
00074     private String paramAbsFunction;
00075     private boolean foundAnyAbstractDef;
00076     private boolean isTest;
00077     private Hashtable opTable;
00078     private Vector currentOp;
00079     private int[][] opLeftRight;
00080     private int[][] opLeftResult;
00081     private int[][] opRightResult;
00082     private HashSet possibleArguments;
00083 /**
00084  * 
00085  * @param reader
00086  */
00087 public AbstractionGenerator(Reader reader) {
00088     try {
00089         node = new Parser(new Lexer(new PushbackReader(reader))).parse();
00090     } catch (Exception e) {
00091         errors.add("Error occured when generating abstraction: \"" + e.getMessage() + "\"");
00092     }
00093 }
00094 /**
00095  * 
00096  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AAbstractFunction
00097  */
00098 public void caseAAbstractFunction(AAbstractFunction node) {
00099     paramAbsFunction = node.getId().toString().trim();
00100     {
00101         Object temp[] = node.getAbstractDef().toArray();
00102         for (int i = 0; i < temp.length; i++) {
00103             ((PAbstractDef) temp[i]).apply(this);
00104         }
00105     }
00106 }
00107 /**
00108  * 
00109  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AAnyAbstractDef
00110  */
00111 public void caseAAnyAbstractDef(AAnyAbstractDef node) {
00112     if (foundAnyAbstractDef) {
00113         warnings.add("Found '_' before '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00114     } else {
00115         foundAnyAbstractDef = true;
00116         String token = node.getId().toString().trim();
00117         if (tokenSet.contains(token)) {
00118             absFunctions.add("if (n == n) return " + token + ";");
00119         } else {
00120             warnings.add("Invalid token '" + token + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00121         }
00122     }
00123 }
00124 /**
00125  * 
00126  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AAnyPattern
00127  */
00128 public void caseAAnyPattern(AAnyPattern node) {
00129     if (possibleArguments.size() == 0) {
00130         warnings.add("Unnecessary " + (isTest? "test" : "operator") + " pattern '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00131         return;
00132     }
00133     tempCollection = new HashSet();
00134     node.getTokenTokenSet().apply(this);
00135     int result = 0;
00136     if (isTest) {
00137         boolean hasTrue = tempCollection.remove("TRUE");
00138         boolean hasFalse = tempCollection.remove("FALSE");
00139         for (Iterator i = tempCollection.iterator(); i.hasNext();) {
00140             warnings.add("Invalid token '" + i.next() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00141         }
00142         if (hasTrue && hasFalse) {
00143             result = Abstraction.TRUE_OR_FALSE;
00144             currentOp.add("if (left$ == left$) return Abstraction.choose();");
00145         } else
00146             if (hasTrue) {
00147                 result = Abstraction.TRUE;
00148                 currentOp.add("if (left$ == left$) return true;");
00149             } else
00150                 if (hasFalse) {
00151                     result = Abstraction.FALSE;
00152                     currentOp.add("if (left$ == left$) return false;");
00153                 } else {
00154                     warnings.add("Invalid test pattern definition at line " + node.getSemicolon().getLine() + ". Ignored...");
00155                     return;
00156                 }
00157     } else {
00158         int size = 0;
00159         int lastIndex = -1;
00160         for (Iterator i = tempCollection.iterator(); i.hasNext();) {
00161             String token = (String) i.next();
00162             int index = tokenSet.indexOf(token);
00163             if (index != -1) {
00164                 result += (1 << index);
00165                 lastIndex = index;
00166                 size++;
00167             } else {
00168                 warnings.add("Invalid token '" + token + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00169             }
00170         }
00171         if (size == 1) {
00172             currentOp.add("if (left$ == left$) return " + tokenSet.elementAt(lastIndex) + ";");
00173         } else
00174             if (size > 1) {
00175                 currentOp.add("if (left$ == left$) return Abstraction.choose(" + getExpandedString(result) + ");");
00176             } else {
00177                 warnings.add("Invalid test pattern definition at line " + node.getSemicolon().getLine() + ". Ignored...");
00178                 return;
00179             }
00180     }
00181     for (Iterator i = possibleArguments.iterator(); i.hasNext();) {
00182         String tuple = (String) i.next();
00183         int index = tuple.indexOf(":");
00184         int leftArg = tokenSet.indexOf(tuple.substring(0, index));
00185         int rightArg = tokenSet.indexOf(tuple.substring(index + 1));
00186         opLeftResult[leftArg][result] |= (1 <<  rightArg);
00187         opLeftRight[leftArg][rightArg] = result;
00188         opRightResult[rightArg][result] |= (1 << leftArg);
00189     }
00190     possibleArguments.clear();
00191 }
00192 /**
00193  * 
00194  * @param node edu.ksu.cis.bandera.abstraction.specification.node.ADefaultToken
00195  */
00196 public void caseADefaultToken(ADefaultToken node) {
00197     String defaultToken = node.getId().toString().trim();
00198     if (tokenSet.remove(defaultToken)) {
00199         tokenSet.insertElementAt(defaultToken, 0);
00200     } else {
00201         errors.add("Invalid default token '" + defaultToken + "' at line " + node.getSemicolon().getLine());
00202     }
00203 }
00204 /**
00205  * 
00206  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AExpAbstractDef
00207  */
00208 public void caseAExpAbstractDef(AExpAbstractDef node) {
00209     if (foundAnyAbstractDef) {
00210         warnings.add("Found '_' before '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00211     } else {
00212         node.getExp().apply(this);
00213         String token = node.getId().toString().trim();
00214         if (tokenSet.contains(token)) {
00215             absFunctions.add("if (" + node.getExp().toString().trim() + ") return " + token + ";");
00216         } else {
00217             warnings.add("Invalid token '" + token + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00218         }
00219     }
00220 }
00221 /**
00222  * 
00223  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AIdIdList
00224  */
00225 public void caseAIdIdList(AIdIdList node) {
00226     TId tid = node.getId();
00227     String token = tid.toString().trim();
00228     if (tempCollection.contains(token)) {
00229         warnings.add("Duplicate occurence of token '" + token + "' at line " + tid.getLine() + ". Ignored...");
00230     } else {
00231         tempCollection.add(token);
00232     }
00233 }
00234 /**
00235  * 
00236  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AIdPrimaryExp
00237  */
00238 public void caseAIdPrimaryExp(AIdPrimaryExp node) {
00239     String n = node.getId().toString().trim();
00240     if (!n.equals(paramAbsFunction)) {
00241         errors.add("Variable '" + n + "' is undefined at line " + node.getId().getLine());
00242     }
00243 }
00244 /**
00245  * 
00246  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AIdsIdList
00247  */
00248 public void caseAIdsIdList(AIdsIdList node) {
00249     node.getIdList().apply(this);
00250     TId tid = node.getId();
00251     String token = tid.toString().trim();
00252     if (tempCollection.contains(token)) {
00253         warnings.add("Duplicate occurence of token '" + token + "' at line " + tid.getLine() + ". Ignored...");
00254     } else {
00255         tempCollection.add(token);
00256     }
00257 }
00258 /**
00259  * 
00260  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AIntegralType
00261  */
00262 public void caseAIntegralType(AIntegralType node) {
00263     superTypeName = "IntegralAbstraction";
00264     type = "integral";
00265 }
00266 /**
00267  * 
00268  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AOperator
00269  */
00270 public void caseAOperator(AOperator node) {
00271     String op = node.getOp().toString().trim();
00272     currentOp = new Vector();
00273     opLeftRight = new int[fields.length][fields.length];
00274     opLeftResult = new int[fields.length][1 << fields.length];
00275     opRightResult = new int[fields.length][1 << fields.length];
00276     isTest = false;
00277     createPossibleArguments();
00278     /*
00279     for (int i = 0; i < fields.length; i++) {
00280         for (int j = 0; j < (1 << fields.length); i++) {
00281             opLeftResult[i][j] = 0;
00282             opRightResult[i][j] = 0;
00283         }
00284     }
00285     */
00286     {
00287         Object temp[] = node.getPattern().toArray();
00288         for (int i = 0; i < temp.length; i++) {
00289             ((PPattern) temp[i]).apply(this);
00290         }
00291     }
00292     opTable.put(op, new Object[] { opLeftResult, currentOp, opLeftRight, opRightResult });
00293     if (possibleArguments.size() > 0)
00294         warnings.add("Cases " +  possibleArguments + " are not handled in " + abstractionName + "." + opNameTable.get(op));
00295 }
00296 /**
00297  * 
00298  * @param node edu.ksu.cis.bandera.abstraction.specification.node.APatternPattern
00299  */
00300 public void caseAPatternPattern(APatternPattern node) {
00301     if (possibleArguments.size() == 0) {
00302         warnings.add("Unnecessary " + (isTest ? "test" : "operator") + " pattern '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00303         return;
00304     }
00305     tempCollection = new HashSet();
00306     node.getTokenTokenSet().apply(this);
00307     int result = 0;
00308     int lastIndex = -1;
00309     boolean useChoose = false;
00310     //HashSet resultToken = new HashSet();
00311     HashSet otherToken = new HashSet();
00312     if (isTest) {
00313         boolean hasTrue = tempCollection.remove("TRUE");
00314         boolean hasFalse = tempCollection.remove("FALSE");
00315         for (Iterator i = tempCollection.iterator(); i.hasNext();) {
00316             warnings.add("Invalid token '" + i.next() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00317         }
00318         if (hasTrue && hasFalse) {
00319             result = Abstraction.TRUE_OR_FALSE;
00320             useChoose = true;
00321             //resultToken.add("TRUE");
00322             //resultToken.add("FALSE");
00323         } else
00324             if (hasTrue) {
00325                 result = Abstraction.TRUE;
00326                 //resultToken.add("TRUE");
00327             } else
00328                 if (hasFalse) {
00329                     result = Abstraction.FALSE;
00330                     //resultToken.add("FALSE");
00331                 } else {
00332                     warnings.add("Invalid test pattern definition (does not return TRUE/FALSE/T) at line " + node.getSemicolon().getLine() + ". Ignored...");
00333                     return;
00334                 }
00335     } else {
00336         int size = 0;
00337         for (Iterator i = tempCollection.iterator(); i.hasNext();) {
00338             String token = (String) i.next();
00339             int index = tokenSet.indexOf(token);
00340             if (index != -1) {
00341                 result += (1 << index);
00342                 lastIndex = index;
00343                 size++;
00344                 //resultToken.add(token);
00345             } else {
00346                 otherToken.add(token);
00347             }
00348         }
00349         if (size > 1) {
00350             useChoose = true;
00351         }
00352     }
00353     String rid = node.getRId().toString().trim();
00354     String lid = node.getLId().toString().trim();
00355     int caseNo = 0;
00356     if ("_".equals(lid)) {
00357         if ("_".equals(rid)) {
00358             new AAnyPattern(new TAny(), node.getRightarrow(), node.getTokenTokenSet(), node.getSemicolon()).apply(this);
00359         } else
00360             if (tokenSet.contains(rid)) {
00361                 int index = tokenSet.indexOf(rid);
00362                 boolean necessary = false;
00363                 for (int i = 0; i < fields.length; i++) {
00364                     if (possibleArguments.remove(fields[i] + ":" + fields[index])) {
00365                         necessary = true;
00366                         opLeftResult[i][result] |= (1 << index);
00367                         opLeftRight[i][index] = result;
00368                         opRightResult[index][result] |= (1 << i);
00369                     }
00370                 }
00371                 if (necessary) {
00372                     if (isTest) {
00373                         switch (result) {
00374                             case Abstraction.FALSE:
00375                                 currentOp.add("if (right$ == " + rid + ") return false;");
00376                                 break;
00377                             case Abstraction.TRUE:
00378                                 currentOp.add("if (right$ == " + rid + ") return true;");
00379                                 break;
00380                             case Abstraction.TRUE_OR_FALSE:
00381                                 currentOp.add("if (right$ == " + rid + ") return Abstraction.choose();");
00382                                 break;
00383                             default: throw new RuntimeException();
00384                         }
00385                     } else {
00386                         for (Iterator i = otherToken.iterator(); i.hasNext();) {
00387                             warnings.add("Invalid token '" + i.next() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00388                         }
00389                         if (result == 0) {
00390                             warnings.add("Invalid operator pattern definition (no valid result) at line " + node.getSemicolon().getLine() + ". Ignored...");
00391                             return;
00392                         }
00393                         if (useChoose) {
00394                             currentOp.add("if (right$ == " + rid + ") return Abstraction.choose(" + getExpandedString(result) + ");");
00395                         } else {
00396                             currentOp.add("if (right$ == " + rid + ") return " + fields[lastIndex] + ";");
00397                         }
00398                     }
00399                 } else {
00400                     warnings.add("Unnecessary " + (isTest ? "test" : "operator") + " pattern '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00401                     return;
00402                 }
00403             } else {
00404                 warnings.add("Invalid " + (isTest ? "test" : "operator") + " pattern definition (mixing Wild and Var) at line " + node.getSemicolon().getLine() + ". Ignored...");
00405             }
00406     } else
00407         if ("_".equals(rid)) {
00408             if (tokenSet.contains(lid)) {
00409                 int index = tokenSet.indexOf(lid);
00410                 boolean necessary = false;
00411                 for (int i = 0; i < fields.length; i++) {
00412                     if (possibleArguments.remove(fields[index] + ":" + fields[i])) {
00413                         necessary = true;
00414                         opLeftResult[index][result] |= (1 << i);
00415                         opLeftRight[index][i] = result;
00416                         opRightResult[i][result] |= (1 << index);
00417                     }
00418                 }
00419                 if (necessary) {
00420                     if (isTest) {
00421                         switch (result) {
00422                             case Abstraction.FALSE:
00423                                 currentOp.add("if (left$ == " + lid + ") return false;");
00424                                 break;
00425                             case Abstraction.TRUE:
00426                                 currentOp.add("if (left$ == " + lid + ") return true;");
00427                                 break;
00428                             case Abstraction.TRUE_OR_FALSE:
00429                                 currentOp.add("if (left$ == " + lid + ") return Abstraction.choose(); // [TRUE, FALSE]");
00430                                 break;
00431                             default: throw new RuntimeException();
00432                         }
00433                     } else {
00434                         if (useChoose) {
00435                             currentOp.add("if (left$ == " + lid + ") return Abstraction.choose(" + getExpandedString(result) + ");");
00436                         } else {
00437                             currentOp.add("if (left$ == " + lid + ") return " + fields[lastIndex] + ";");
00438                         }
00439                     }
00440                 } else {
00441                     warnings.add("Unnecessary " + (isTest ? "test" : "operator") + " pattern '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00442                     return;
00443                 }
00444             } else {
00445                 warnings.add("Invalid " + (isTest ? "test" : "operator") + " pattern definition (mixing Wild and Var) at line " + node.getSemicolon().getLine() + ". Ignored...");
00446             }
00447         } else
00448             if (!tokenSet.contains(lid)) {
00449                 if (isTest) {
00450                     warnings.add("Invalid test pattern definition (using Var) at line " + node.getSemicolon().getLine() + ". Ignored...");
00451                     return;
00452                 }
00453                 if (!tokenSet.contains(rid)) {
00454                     warnings.add("Invalid operator pattern definition (using two Vars) at line " + node.getSemicolon().getLine() + ". Ignored...");
00455                     return;
00456                 } else {
00457                     if ((otherToken.size() == 1) && (result == 0) && (otherToken.iterator().next().equals(lid))) {
00458                         int index = tokenSet.indexOf(rid);
00459                         boolean necessary = false;
00460                         for (int i = 0; i < fields.length; i++) {
00461                             if (possibleArguments.remove(fields[i] + ":" + fields[index])) {
00462                                 necessary = true;
00463                                 opLeftResult[i][result] |= (1 << index);
00464                                 opLeftRight[i][index] = result;
00465                                 opRightResult[index][result] |= (1 << i);
00466                             }
00467                         }
00468                         if (necessary) {
00469                             currentOp.add("if (right$ == " + rid + ") return left$;");
00470                         } else {
00471                             warnings.add("Invalid operator pattern definition (Var declared but not used) at line " + node.getSemicolon().getLine() + ". Ignored...");
00472                             return;
00473                         }
00474                     }
00475                 }
00476             } else
00477                 if (!tokenSet.contains(rid)) {
00478                     if (isTest) {
00479                         warnings.add("Invalid test pattern definition (using Var) at line " + node.getSemicolon().getLine() + ". Ignored...");
00480                         return;
00481                     }
00482                     if ((otherToken.size() == 1) && (result == 0) && (otherToken.iterator().next().equals(rid))) {
00483                         int index = tokenSet.indexOf(lid);
00484                         boolean necessary = false;
00485                         for (int i = 0; i < fields.length; i++) {
00486                             if (possibleArguments.remove(fields[index] + ":" + fields[i])) {
00487                                 necessary = true;
00488                                 opLeftResult[index][result] |= (1 << i);
00489                                 opLeftResult[index][i] = result;
00490                                 opRightResult[i][result] |= (1 << index);
00491                             }
00492                         }
00493                         if (necessary) {
00494                             currentOp.add("if (left$ == " + lid + ") return right$;");
00495                         } else {
00496                             warnings.add("Invalid operator pattern definition (Var declared but not used) at line " + node.getSemicolon().getLine() + ". Ignored...");
00497                             return;
00498                         }
00499                     }
00500                 } else {
00501                     if (possibleArguments.remove(lid + ":" + rid)) {
00502                         if (isTest) {
00503                             switch (result) {
00504                                 case Abstraction.FALSE:
00505                                     currentOp.add("if (left$ == " + lid + " && right$ == " + rid + ") return false;");
00506                                     break;
00507                                 case Abstraction.TRUE:
00508                                     currentOp.add("if (left$ == " + lid + " && right$ == " + rid + ") return true;");
00509                                     break;
00510                                 case Abstraction.TRUE_OR_FALSE:
00511                                     currentOp.add("if (left$ == " + lid + " && right$ == " + rid + ") return Abstraction.choose();");
00512                                     break;
00513                                 default: throw new RuntimeException();
00514                             }
00515                             int lidx = tokenSet.indexOf(lid);
00516                             int ridx = tokenSet.indexOf(rid);
00517                             opLeftResult[lidx][result] |= (1 << ridx);
00518                             opLeftRight[lidx][ridx] = result;
00519                             opRightResult[ridx][result] |= (1 << lidx);
00520                         } else {
00521                             for (Iterator i = otherToken.iterator(); i.hasNext();) {
00522                                 warnings.add("Invalid token '" + i.next() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00523                             }
00524                             if (result == 0) {
00525                                 warnings.add("Invalid operator pattern definition (no valid result) at line " + node.getSemicolon().getLine() + ". Ignored...");
00526                                 return;
00527                             }
00528                             int lidx = tokenSet.indexOf(lid);
00529                             int ridx = tokenSet.indexOf(rid);
00530                             opLeftResult[lidx][result] |= (1 << ridx);
00531                             opLeftRight[lidx][ridx] = result;
00532                             opRightResult[ridx][result] |= (1 << lidx);
00533                             if (useChoose) {
00534                                 currentOp.add("if (left$ == " + lid + " && right$ == " + rid + ") return Abstraction.choose(" + getExpandedString(result) + ");");
00535                             } else {
00536                                 currentOp.add("if (left$ == " + lid + " && right$ == " + rid + ") return " + fields[lastIndex] + ";");
00537                             }
00538                         }
00539                     } else {
00540                         warnings.add("Unnecessary " + (isTest ? "test" : "operator") + " pattern '" + node.toString() + "' at line " + node.getSemicolon().getLine() + ". Ignored...");
00541                         return;
00542                     }
00543                 }
00544 }
00545 /**
00546  * 
00547  * @param node edu.ksu.cis.bandera.abstraction.specification.node.ARealType
00548  */
00549 public void caseARealType(ARealType node) {
00550     superTypeName = "RealAbstraction";
00551     type = "real";
00552 }
00553 /**
00554  * 
00555  * @param node edu.ksu.cis.bandera.abstraction.specification.node.ATest
00556  */
00557 public void caseATest(ATest node) {
00558     String op = node.getTOp().toString().trim();
00559     currentOp = new Vector();
00560     opLeftRight = new int[fields.length][fields.length];
00561     opLeftResult = new int[fields.length][3];
00562     opRightResult = new int[fields.length][3];
00563     isTest = true;
00564     createPossibleArguments();
00565     for (int i = 0; i < fields.length; i++) {
00566         for (int j = 0; j < fields.length; j++) {
00567             opLeftRight[i][j] = -1;
00568         }
00569     }
00570     
00571     {
00572         Object temp[] = node.getPattern().toArray();
00573         for (int i = 0; i < temp.length; i++) {
00574             ((PPattern) temp[i]).apply(this);
00575         }
00576     }
00577     opTable.put(op, new Object[] {opLeftResult, currentOp, opLeftRight, opRightResult});
00578     if (possibleArguments.size() > 0)
00579         warnings.add("Cases " +  possibleArguments + " are not handled in " + abstractionName + "." + opNameTable.get(op));
00580 }
00581 /**
00582  * 
00583  * @param node edu.ksu.cis.bandera.abstraction.specification.node.ATokenTokenTokenSet
00584  */
00585 public void caseATokenTokenTokenSet(ATokenTokenTokenSet node) {
00586     String token = node.getId().toString().trim();
00587     if ("T".equals(token)) {
00588         if (isTest) {
00589             tempCollection.add("TRUE");
00590             tempCollection.add("FALSE");
00591         } else {
00592             for (int i = 0; i < fields.length; i++) {
00593                 tempCollection.add(fields[i]);
00594             }
00595         }
00596     } else {
00597         tempCollection.add(token);
00598     }
00599 }
00600 /**
00601  * 
00602  * @param node edu.ksu.cis.bandera.abstraction.specification.node.AUnit
00603  */
00604 public void caseAUnit(AUnit node) {
00605     node.getType().apply(this);
00606     
00607     abstractionName = node.getId().toString().trim();
00608 
00609     tempCollection = new Vector();
00610         
00611     node.getTokenSet().apply(this);
00612 
00613     tokenSet = (Vector) tempCollection;
00614 
00615     if (node.getDefaultToken() != null) {
00616         node.getDefaultToken().apply(this);
00617     } else {
00618         errors.add("Default token is undefined");
00619     }
00620 
00621     fields = new String[tokenSet.size()];
00622     
00623     System.arraycopy(tokenSet.toArray(), 0, fields, 0, tokenSet.size());
00624 
00625     tempCollection = new HashSet();
00626     
00627     if (node.getOne2oneSet() != null)
00628         node.getOne2oneSet().apply(this);
00629 
00630     one2oneSet = new HashSet();
00631 
00632     for (Iterator i = tempCollection.iterator(); i.hasNext();) {
00633         String token = (String) i.next();
00634         if (tokenSet.contains(token)) {
00635             one2oneSet.add(token);
00636         } else {
00637             warnings.add("Invalid token '" + token + "' at ONE2ONE token set definition");
00638         }
00639     }
00640 
00641     absFunctions = new Vector();
00642     
00643     node.getAbstractFunction().apply(this);
00644 
00645     opTable = new Hashtable();
00646     
00647     {
00648         Object temp[] = node.getOperatorTest().toArray();
00649         for (int i = 0; i < temp.length; i++) {
00650             ((POperatorTest) temp[i]).apply(this);
00651         }
00652     }
00653 }
00654 /**
00655  * 
00656  */
00657 private void createPossibleArguments() {
00658     possibleArguments = new HashSet();
00659     for (int i = 0; i < fields.length; i++) {
00660         for (int j = 0; j < fields.length; j++) {
00661             possibleArguments.add(fields[i] + ":" + fields[j]);
00662         }
00663     }
00664 }
00665 /**
00666  * 
00667  * @return java.lang.String
00668  */
00669 public String generate(String packageName) {
00670     if (node != null) node.apply(this);
00671     if (errors.size() > 0) return null;
00672 
00673     buffer = new StringBuffer("// This file was generated by Bandera (http://www.cis.ksu.edu/santos/bandera)." + lineSeparator);
00674 
00675     if (warnings.size() > 0) {
00676         println("//");
00677         println("// WARNING:");
00678         println("// --------");
00679         for (Iterator i = warnings.iterator(); i.hasNext();) {
00680             println("// * " + i.next());
00681         }
00682         println("//");
00683         println("//");
00684     }
00685     
00686     String typeName = abstractionName;
00687 
00688     if (packageName != null) {
00689         if ("".equals(packageName))
00690             this.packageName = type;
00691         else
00692             this.packageName = packageName + ("." + type);
00693         println("package " + this.packageName + ";");
00694     }
00695     println("import edu.ksu.cis.bandera.abstraction.*;");
00696     println("public class " + typeName + " extends " + superTypeName + " {");
00697     println("  private static final " + typeName + " v = new " + typeName + "();");
00698 
00699     for (int i = 0; i < fields.length; i++) {
00700         println("  public static final int " + fields[i] + " = " + i + ";");
00701     }
00702 
00703     println("  private " + typeName + "() {");
00704     println("  }");
00705 
00706     println("  public static " + typeName + " v() {");
00707     println("    return v;");
00708     println("  }");
00709 
00710     println("  public static int getNumOfTokens() {");
00711     println("    return " + fields.length + ";");
00712     println("  }");
00713     
00714 
00715     println("  public static String getToken(int value) {");
00716     println("    switch(value) {");
00717     for (int i = 0; i < fields.length; i++) {
00718         println("      case " + fields[i] + ": return \"" + abstractionName + "." + fields[i] + "\";");
00719     }
00720     println("    }");
00721     println("    return \"" + abstractionName + ".???\";");
00722     println("  }");
00723 
00724     println("  public static boolean isOne2One(int value) {");
00725     if (one2oneSet.size() > 0) {
00726         println("    switch(value) {");
00727         for (Iterator i = one2oneSet.iterator(); i.hasNext();) {
00728             println("      case " + i.next() + ": return true;");
00729         }
00730         println("    }");
00731     }
00732     println("    return false;");
00733     println("  }");
00734 
00735     println("  public static int abs(" + ("integral".equals(type) ? "long " : "double ") + paramAbsFunction + ") {");
00736     for (Iterator i = absFunctions.iterator(); i.hasNext();) {
00737         println("    " + i.next());
00738     }
00739     println("    throw new RuntimeException(\"" + typeName + " cannot abstract value '\" + " + paramAbsFunction + " + \"'\");");
00740     println("  }");
00741 
00742     generateOperators();
00743     
00744     generateBASL();
00745     
00746     println("  public static String getName() {");
00747     println("    return \"" + abstractionName + "\";");
00748     println("  }");
00749     println("  public String toString() {");
00750     println("    return getName();");
00751     println("  }");
00752     println("}");
00753 
00754     return buffer.toString();
00755 }
00756 /**
00757  * 
00758  */
00759 private void generateBASL() {
00760     println("  public static String getBASLRepresentation() {");
00761     println("    return");
00762     try {
00763         LineNumberReader r = new LineNumberReader(new StringReader(AbstractionPrinter.print((Start) node, true)));
00764         String line = r.readLine();
00765         println("      \"" + line + "\\n\"");
00766         while ((line = r.readLine()) != null) {
00767             println("      + \"" + line + "\\n\"");
00768         }
00769     } catch (Exception e) {
00770     }
00771     println("    ;");
00772     println("  }");
00773 }
00774 /**
00775  * 
00776  */
00777 private void generateOperators() {
00778     String typeName = abstractionName;
00779     
00780     for (Enumeration e = opNameTable.keys(); e.hasMoreElements();) {
00781         String op = (String) e.nextElement();
00782         String opName = (String) opNameTable.get(op);
00783         boolean isTest = (op.length() > 1) || ">".equals(op) || "<".equals(op); 
00784         Object[] o = (Object[]) opTable.get(op);
00785         if (o == null) continue;
00786         opLeftResult = (int[][]) o[0];
00787         currentOp = (Vector) o[1];
00788         opLeftRight = (int[][]) o[2];
00789         opRightResult = (int[][]) o[3];
00790 
00791         if (isTest) {
00792             println("  public static boolean " + opName + "(int left$, int right$) {");
00793         } else {
00794             println("  public static int " + opName + "(int left$, int right$) {");
00795         }
00796         for (Iterator j = currentOp.iterator(); j.hasNext();) {
00797             println("    " + j.next());
00798         }
00799         println("    throw new RuntimeException(\"" + typeName + "." + opName + "(\" + left$ + \", \" + right$ + \") is undefined\");"); 
00800         println("  }");
00801 
00802         if (isTest) {
00803             println("  private static byte " + opName + "NoChoose(int left, int right) {");
00804             println("    byte result = -1;");
00805         } else {
00806             println("  private static int " + opName + "NoChoose(int left, int right) {");
00807             println("    int result = 0;");
00808         }
00809         println("    switch (left) {");
00810         for (int i = 0; i < fields.length; i++) {
00811             println("      case " + i + ":");
00812             println("        switch (right) {");
00813             for (int j = 0; j < fields.length; j++) {
00814                 if ((!isTest && opLeftRight[i][j] != 0) || (isTest && opLeftRight[i][j] != -1)) {
00815                     println("          case " + j + ":");
00816                     println("            result = " + opLeftRight[i][j] + ";");
00817                     println("            break;");
00818                 }
00819             }
00820             println("        }");
00821             println("        break;");
00822         }
00823         println("    }");
00824         if (isTest) {
00825             println("    if (result == -1) throw new RuntimeException(\"" + typeName + "." + opName + "NoChoose(\" + left + \", \" + right + \") is undefined\");");
00826         } else {
00827             println("    if (result == 0) throw new RuntimeException(\"" + typeName + "." + opName + "NoChoose(\" + left + \", \" + right + \") is undefined\");");
00828         }
00829         println("    return result;"); 
00830         println("  }");
00831         
00832 
00833         if (isTest) {
00834             println("  public static byte " + opName + "Set(int leftTokens, int rightTokens) {");
00835             println("    byte result = -1;");
00836         } else {
00837             println("  public static int " + opName + "Set(int leftTokens, int rightTokens) {");
00838             println("    int result = -1;");
00839         }
00840         println("    for (int left = 0; (1 << left) <= leftTokens; left++) {");
00841         println("      if ((leftTokens & (1 << left)) == 0) continue;");
00842         println("      for (int right = 0; (1 << right) <= rightTokens; right++) {");
00843         println("        if ((rightTokens & (1 << right)) != 0) {");
00844         println("          if (result == -1) result = " + opName + "NoChoose(left, right);");
00845         if (isTest) {
00846             println("          else result = Abstraction.meetTest(result, " + opName + "NoChoose(left, right));");
00847         } else {
00848             println("          else result = Abstraction.meetArith(result, " + opName + "NoChoose(left, right));");
00849         }
00850         println("        }");
00851         println("      }");
00852         println("    }");
00853         println("    return result;");
00854         println("  }");
00855         
00856         /*
00857         println("  public static int " + opName + "LeftArg(int rightArg, int result) {");
00858         println("    switch (rightArg) {");
00859         for (int j = 0; j < fields.length; j++) {
00860             println("      case " + fields[j] + ":");
00861             println("        switch (result) {");
00862             if (isTest) {
00863                 for (int k = 0; k < 3; k++) {
00864                     println("          case " + (k == 0 ? "FALSE" : (k == 1 ? "TRUE" : "TRUE_OR_FALSE")) + ": return " + getExpandedString(opRightResult[j][k]) + ";");
00865                 }
00866             } else {
00867                 for (int k = 1; k < (1 << fields.length); k++) {
00868                     println("          case " + getExpandedString(k) + ": return " + getExpandedString(opRightResult[j][k]) + ";");
00869                 }
00870             }
00871             println("        }");
00872             println("        break;");
00873         }
00874         println("    }");
00875         println("    return -1;");
00876         println("  }");
00877 
00878         println("  public static int " + opName + "RightArg(int leftArg, int result) {");
00879         println("    switch (leftArg) {");
00880         for (int j = 0; j < fields.length; j++) {
00881             println("      case " + fields[j] + ":");
00882             println("        switch (result) {");
00883             if (isTest) {
00884                 for (int k = 0; k < 3; k++) {
00885                     println("          case " + (k == 0 ? "FALSE" : (k == 1 ? "TRUE" : "TRUE_OR_FALSE")) + ": return " + getExpandedString(opLeftResult[j][k]) + ";");
00886                 }
00887             } else {
00888                 for (int k = 1; k < (1 << fields.length); k++) {
00889                     println("          case " + getExpandedString(k) + ": return " + getExpandedString(opLeftResult[j][k]) + ";");
00890                 }
00891             }
00892             println("        }");
00893             println("        break;");
00894         }
00895         println("    }");
00896         println("    return -1;");
00897         println("  }");
00898         */
00899     }
00900 }
00901 /**
00902  * 
00903  */
00904 private void generateOperatorSetTable() {
00905     /*
00906     String typeName = abstractionName;
00907     for (Enumeration e = opNameTable.keys(); e.hasMoreElements();) {
00908         String op = (String) e.nextElement();
00909         String opName = (String) opNameTable.get(op);
00910         opLeftRight = (int[][]) ((Object[]) opTable.get(op))[2];
00911         int size = 1 << fields.length;
00912         boolean isTest = (op.length() > 1) || ">".equals(op) || "<".equals(op); 
00913         println("  private static int[][] " + opName + "SetTable = {");
00914         for (int i = 1; i < size; i++) {
00915             print("    {");
00916             for (int j = 1; j < size; j++) {
00917                 int result = -1;
00918                 for (int left = 0; left < fields.length; left++) {
00919                     for (int right = 0; right < fields.length; right++) {
00920                         if (((i & (1 << left)) == (1 << left)) && ((j & (1 << right)) == (1 << right))) {
00921                             if (result == -1)
00922                                 result = opLeftRight[left][right];
00923                             else
00924                                 result = Abstraction.meet(result, opLeftRight[left][right], isTest);
00925                         }
00926                     }
00927                 }
00928                 if (j + 1 == size) {
00929                     print(result + "}");
00930                     if (i + 1 != size) {
00931                         println(",");
00932                     }   else {
00933                         println("");
00934                     }
00935                 } else {
00936                     print(result + ", ");
00937                 }
00938             }
00939         }
00940         println("  };");
00941     }
00942     */
00943 }
00944 /**
00945  * 
00946  */
00947 private void generateOperatorsTable() {
00948     /*
00949     String typeName = abstractionName;
00950     for (Enumeration e = opNameTable.keys(); e.hasMoreElements();) {
00951         String op = (String) e.nextElement();
00952         String opName = (String) opNameTable.get(op);
00953         opLeftRight = (int[][]) ((Object[]) opTable.get(op))[2];
00954         boolean isTest = (op.length() > 1) || ">".equals(op) || "<".equals(op);
00955 
00956         if (isTest) {
00957             println("  private static byte[][] " + opName + "Table = {");
00958         } else {
00959             println("  private static int[][] " + opName + "Table = {");
00960         }
00961         for (int i = 0; i < fields.length; i++) {
00962             print("    {");
00963             for (int j = 0; j < fields.length; j++) {
00964                 if (j + 1 == fields.length) {
00965                     print(Integer.toString(opLeftRight[i][j]));
00966                 } else {
00967                     print(opLeftRight[i][j] + ", ");
00968                 }
00969             }
00970             if (i + 1 == fields.length) {
00971                 println("}");
00972             } else {
00973                 println("},");
00974             }
00975         }
00976         println("  };");
00977     }
00978     */
00979 }
00980 /**
00981  * 
00982  * @return java.lang.String
00983  */
00984 public String getAbstractionFullyQualifiedName() {
00985     return packageName + "." + getAbstractionName();
00986 }
00987 /**
00988  * 
00989  * @return java.lang.String
00990  */
00991 public String getAbstractionName() {
00992     return abstractionName;
00993 }
00994 /**
00995  * 
00996  * @return java.lang.String
00997  */
00998 public String getAbstractionType() {
00999     return type;
01000 }
01001 /**
01002  * 
01003  * @return java.util.Vector
01004  */
01005 public Vector getErrors() {
01006     return errors;
01007 }
01008 /**
01009  * 
01010  * @return java.lang.String
01011  * @param values int
01012  */
01013 private String getExpandedString(int values) {
01014     HashSet set = new HashSet();
01015     for (int l = 0, mask = 1; l < fields.length; l++, mask <<= 1) {
01016         if ((values & mask) == mask) {
01017             set.add(fields[l]);
01018         }
01019     }
01020     switch (set.size()) {
01021         case 0:
01022             return "NOTHING";
01023         case 1:
01024             return "(1 << " + set.iterator().next() + ")";
01025         default:
01026             Iterator i = set.iterator();
01027             String result = (String) ("(1 << " + i.next() + ")");
01028             while (i.hasNext()) result += (" | (1 << " + i.next() + ")");
01029             return result;          
01030     }
01031 }
01032 /**
01033  * 
01034  * @return edu.ksu.cis.bandera.abstraction.specification.node.Start
01035  */
01036 public Start getNode() {
01037     return (Start) node;
01038 }
01039 /**
01040  * 
01041  * @return java.util.Vector
01042  */
01043 public Vector getWarnings() {
01044     return warnings;
01045 }
01046 /**
01047  * 
01048  * @param s java.lang.String
01049  */
01050 private void print(String s) {
01051     buffer.append(s);
01052 }
01053 /**
01054  * 
01055  * @param s java.lang.String
01056  */
01057 private void println(String s) {
01058     buffer.append(s + lineSeparator);
01059 }
01060 }