BirBuilder.java Source File

00001 package edu.ksu.cis.bandera.birp;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 1998, 1999   James Corbett (corbett@hawaii.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 edu.ksu.cis.bandera.bir.*;
00036 import edu.ksu.cis.bandera.bir.Collection;
00037 import edu.ksu.cis.bandera.birp.analysis.*;
00038 import edu.ksu.cis.bandera.birp.node.*;
00039 import edu.ksu.cis.bandera.birp.parser.*;
00040 import edu.ksu.cis.bandera.birp.lexer.*;
00041 
00042 import java.io.*;
00043 import java.util.*;
00044 
00045 public class BirBuilder extends DepthFirstAdapter implements BirConstants
00046 {
00047     TransSystem system;
00048     Hashtable globalVars;
00049     Hashtable localVars;
00050     Hashtable threadLocs;
00051     Hashtable threadLocTables;
00052     Hashtable threadLocalVarTables;
00053     Hashtable threads;
00054     Vector refTypes = new Vector();
00055     BirThread currentThread;
00056     Location currentLoc;
00057     ActionVector currentActions;
00058     Enumerated currentEnumerated;
00059     Record currentRecord;
00060     PrintAction currentPrintAction;
00061     boolean error;
00062     boolean inPredicate = false;
00063     String fileName;
00064     public BirBuilder(String fileName) {
00065     this.fileName = fileName;
00066     }
00067     LengthExpr arrayLength(Expr array, Token len) {
00068     Type arrayType = array.getType();
00069     if (arrayType.isKind(REF))
00070         arrayType = ((Ref)arrayType).getTargetType();
00071     if (! arrayType.isKind(ARRAY))
00072         error(len, "prefix of .length not array");
00073     if (array.getType().isKind(ARRAY))
00074         return new LengthExpr(array);
00075     else
00076         return new LengthExpr(new DerefExpr(array));
00077     }
00078     ArrayExpr arraySelect(Expr array, Expr index, Token bracket) {
00079     Type arrayType = array.getType();
00080     if (arrayType.isKind(REF))
00081         arrayType = ((Ref)arrayType).getTargetType();
00082     if (! arrayType.isKind(ARRAY))
00083         error(bracket, "prefix of [] not array");
00084     if (! index.getType().isKind(RANGE))
00085         error(bracket, "index of [] not range type");
00086     if (array.getType().isKind(ARRAY))
00087         return new ArrayExpr(array, index);
00088     else
00089         return new ArrayExpr(new DerefExpr(array), index);
00090     }
00091     void checkDecl(Token ident) {
00092     String name = ident.getText();
00093     Object existingDecl = (currentThread != null) ? 
00094         localVars.get(name) : globalVars.get(name);
00095     if (existingDecl != null) 
00096         error(ident, "redefinition of name: " + name);
00097     }
00098     StateVar declareVar(Token ident, Type type, Expr initVal) {
00099     String name = ident.getText();
00100     if ((initVal != null) && ! type.containsValue(initVal))
00101         error(ident, "bad initial value: " + initVal);
00102     checkDecl(ident);
00103     String key = (currentThread == null) ? name : 
00104         currentThread.getName() + "." + name;
00105     Expr initValue = (initVal == null) ? type.defaultVal() : initVal;
00106     StateVar var = system.declareVar(key, name, currentThread,
00107                      type, initValue);
00108     if (currentThread != null)
00109         localVars.put(name, var);
00110     else 
00111         globalVars.put(name, var);
00112     return var;
00113     }
00114     StateVar error(Token tok, String msg) {
00115     System.out.println(fileName + ":" + tok.getLine() + ": " + msg);
00116     error = true;
00117     return null;
00118     }
00119     RecordExpr fieldSelect(Expr rec, Token id) {
00120     String name = id.getText();
00121     Type recType = rec.getType();
00122     if (recType.isKind(REF))
00123         recType = ((Ref)recType).getTargetType();
00124     if (! recType.isKind(RECORD))
00125         error(id, "prefix of " + name + " is not record type");
00126     Field field = ((Record)recType).getField(name);
00127     if (field == null)
00128         error(id, "field " + name + " not found");
00129     if (rec.getType().isKind(RECORD)) 
00130         return new RecordExpr(rec, field);
00131     else 
00132         return new RecordExpr(new DerefExpr(rec), field);
00133     }
00134     Expr getDecl(Token ident) {
00135     String name = ident.getText();
00136     if (currentThread != null) {
00137         Object var = localVars.get(name);
00138         if (var != null)
00139         return (StateVar) var;
00140     }
00141     Object var = globalVars.get(name);
00142     if (var != null)
00143         if ((var instanceof StateVar) || (var instanceof Constant))
00144         return (Expr) var;
00145         else
00146         error(ident, "not a value: " + name);
00147     return error(ident, "undefined name: " + name);
00148     }
00149     public void inAEmptyLiveset(AEmptyLiveset node)
00150     {
00151         currentLoc.setLiveVars(new StateVarVector(1));
00152     }
00153     public void inAEnumeratedTypespec(AEnumeratedTypespec node)
00154     {
00155     currentEnumerated = system.enumeratedType();
00156     }
00157     public void inALocation(ALocation node)
00158     {
00159     String label = node.getId().getText();
00160     currentLoc = (Location) threadLocs.get(label);
00161     currentLoc.setLabel(label);
00162     }
00163     public void inANonemptyLiveset(ANonemptyLiveset node)
00164     {
00165         currentLoc.setLiveVars(new StateVarVector());
00166     StateVar var = (StateVar) getDecl(node.getFirst());
00167     if (var.getThread() == null)
00168         error(node.getFirst(), "variables in live clause must be local");
00169     else
00170         currentLoc.getLiveVars().addElement(var);
00171     }
00172     public void inAPredicates(APredicates node)
00173     {
00174         inPredicate = true;
00175     }
00176     public void inAPrintaction(APrintaction node)
00177     {
00178         currentPrintAction = new PrintAction();
00179     }
00180     public void inAProcess(AProcess node)
00181     {
00182     String name = node.getStartname().getText();
00183     system = new TransSystem(name);
00184     globalVars = new Hashtable();
00185     threads = new Hashtable();
00186     threadLocTables = new Hashtable();
00187     threadLocalVarTables = new Hashtable();
00188     // Create all threads so they can reference each other
00189     Object threadNodes[] = node.getThreads().toArray();
00190     for(int i = 0; i < threadNodes.length; i++) {
00191         AThread threadNode = (AThread) threadNodes[i];
00192         String threadName = threadNode.getStartname().getText();
00193         threads.put(threadName, 
00194             system.createThread(threadName, threadName)); 
00195     }
00196     }
00197     public void inARecordTypespec(ARecordTypespec node)
00198     {
00199         currentRecord = system.recordType();
00200     }
00201     public void inAThread(AThread node)
00202     {
00203         // When we first encounter a thread declaration,
00204         // go back and resolve the targets of the ref types
00205         if (refTypes != null) {
00206         for (int i = 0; i < refTypes.size(); i++) {
00207         Ref refType = (Ref) refTypes.elementAt(i);
00208         refType.resolveTargets();
00209         }
00210         refTypes = null;
00211     }
00212 
00213         // Set up the context for building the thread
00214     localVars = new Hashtable();
00215     threadLocs = new Hashtable();
00216     String name = node.getStartname().getText();
00217     ALocation startLocation = (ALocation) node.getStartloc();
00218     String startLabel = startLocation.getId().getText();
00219     currentThread = system.threadOfKey(name); 
00220     Location startLoc = 
00221         system.locationOfKey(startLabel + "#" + name, currentThread);
00222     currentThread.setStartLoc(startLoc);
00223     threadLocs.put(startLabel, startLoc);
00224     if (node.getMain() != null)
00225         currentThread.setMain(true);
00226 
00227     // Create all the locations 
00228     Object locs[] = node.getLocations().toArray();
00229     for(int i = 0; i < locs.length; i++) {
00230         ALocation aloc = (ALocation) locs[i];
00231         String locLabel = aloc.getId().getText();
00232         if (threadLocs.get(locLabel) != null)
00233         error(aloc.getId(), "loc " + locLabel 
00234           + " defined more than once");
00235         Location loc = 
00236         system.locationOfKey(locLabel + "#" + name, currentThread);
00237         threadLocs.put(locLabel,loc);
00238     }
00239     threadLocTables.put(currentThread,threadLocs);
00240     threadLocalVarTables.put(currentThread,localVars);
00241     }
00242     public void inATransformation(ATransformation node)
00243     {
00244     currentActions = new ActionVector();
00245     }
00246     public void inStart(Start node)
00247     {
00248     error = false;
00249     }
00250     public void outAAllocation(AAllocation node)
00251     {
00252     Expr arg = getDecl(node.getId());
00253     if (! (arg instanceof StateVar))
00254         error(node.getId(), "'new' can be invoked only on collections");
00255     StateVar collection = (StateVar) arg;
00256     if (! collection.getType().isKind(COLLECTION))
00257         error(node.getId(), "'new' can be invoked only on collections");
00258     Expr var = (Expr) getOut(node.getLhs());
00259     if (! var.getType().isKind(REF))
00260         error(node.getId(), "lhs of 'new' assignment must be reference");
00261     else if (! ((Ref)var.getType()).getTargets().contains(collection))
00262         error(node.getId(), "ref cannot point to collection allocated");
00263     Expr rhs;
00264     Collection colType = (Collection) collection.getType();
00265     if (node.getArraylength() != null) {
00266         if (! colType.getBaseType().isKind(ARRAY))
00267         error(node.getId(),"not an array collection");
00268         Expr arrayLen = (Expr) getOut(node.getArraylength());
00269         rhs = new NewArrayExpr(collection,arrayLen);
00270     } else {
00271         if (! colType.getBaseType().isKind(RECORD))
00272         error(node.getId(),"not an record collection");
00273         rhs = new NewExpr(collection);
00274     }
00275     setOut(node, new AssignAction(var, rhs));
00276     }
00277     public void outAAllocationAction(AAllocationAction node)
00278     {
00279     Action action = (Action) getOut(node.getAllocation());
00280     currentActions.addElement(action);
00281     }
00282     public void outAAndExpr6(AAndExpr6 node)
00283     {
00284     Expr arg1 = (Expr) getOut(node.getExpr6());
00285     Expr arg2 = (Expr) getOut(node.getExpr5());
00286         setOut(node, new AndExpr(arg1, arg2));
00287     if (! (arg1.getType().isKind(BOOL) && arg2.getType().isKind(BOOL)))
00288         error(node.getAnd(), "arguments to && must be boolean");
00289     }
00290     public void outAArraylength(AArraylength node)
00291     {
00292         setOut(node, getOut(node.getExpr()));
00293     }
00294     public void outAArraylengthExpr0(AArraylengthExpr0 node)
00295     {
00296     Expr array = (Expr) getOut(node.getExpr0());
00297     setOut(node, arrayLength(array,node.getLength()));        
00298     }
00299     public void outAArraylengthLhs(AArraylengthLhs node)
00300     {
00301     Expr array = (Expr) getOut(node.getLhs());
00302     setOut(node, arrayLength(array,node.getLength()));        
00303     }
00304     public void outAArrayselectExpr0(AArrayselectExpr0 node)
00305     {
00306     Expr array = (Expr) getOut(node.getExpr0());
00307     Expr index = (Expr) getOut(node.getExpr());
00308     setOut(node, arraySelect(array,index,node.getLbrack()));
00309     }
00310     public void outAArrayselectLhs(AArrayselectLhs node)
00311     {
00312     Expr array = (Expr) getOut(node.getLhs());
00313     Expr index = (Expr) getOut(node.getExpr());
00314     setOut(node, arraySelect(array,index,node.getLbrack()));
00315     }
00316     public void outAArrayTypespec(AArrayTypespec node)
00317     {
00318     Type baseType = (Type) getOut(node.getType());
00319     ConstExpr size = (ConstExpr) getOut(node.getConst());
00320     setOut(node, system.arrayType(baseType, size));
00321     }
00322     public void outAAssertaction(AAssertaction node)
00323     {
00324     Expr cond = (Expr) getOut(node.getExpr());
00325     if (! cond.getType().isKind(BOOL))
00326         error(node.getAssert(),"assert expression must be boolean");
00327     setOut(node, new AssertAction(cond));
00328     }
00329     public void outAAssertactionAction(AAssertactionAction node)
00330     {
00331     Action action = (Action) getOut(node.getAssertaction());
00332     currentActions.addElement(action);
00333     }
00334     public void outAAssignment(AAssignment node)
00335     {
00336     Expr var = (Expr) getOut(node.getLhs());
00337     Expr expr = (Expr) getOut(node.getExpr());
00338     setOut(node, new AssignAction(var, expr));
00339     if (! var.getType().compatibleWith(expr.getType()))
00340         error(node.getAssign(), "incompatible type in assignment");
00341     if (! var.getType().isKind(RANGE|BOOL|ENUMERATED|REF))
00342         error(node.getAssign(), "only range, boolean, enumerated, and ref types can be assigned");
00343     }
00344     public void outAAssignmentAction(AAssignmentAction node)
00345     {
00346     Action action = (Action) getOut(node.getAssignment());
00347     currentActions.addElement(action);
00348     }
00349     public void outAAtlocationThreadtest(AAtlocationThreadtest node)
00350     {
00351     if (! inPredicate)
00352         error(node.getThreadname(),
00353           "Thread location tests can only be used in predicates");
00354     String threadName = node.getThreadname().getText();
00355     BirThread thread = (BirThread)threads.get(threadName);
00356     if (thread == null)
00357         error(node.getThreadname(), "thread not yet declared: " + 
00358           threadName);
00359     String locLabel = node.getLocname().getText();
00360     Hashtable threadLocTable = (Hashtable) threadLocTables.get(thread);
00361     Location loc = (Location) threadLocTable.get(locLabel);
00362     if (loc == null)
00363         error(node.getLocname(),"no location " + locLabel + " in thread " 
00364           + threadName);
00365     setOut(node, new ThreadLocTest(loc));
00366     }
00367     public void outABooleanTypespec(ABooleanTypespec node)
00368     {
00369     setOut(node, system.booleanType());
00370     }
00371     public void outABoolValue(ABoolValue node)
00372     {
00373     setOut(node, getOut(node.getBool()));
00374     }
00375     public void outAChoice(AChoice node)
00376     {
00377     Expr var = (Expr) getOut(node.getLhs());
00378     Expr firstChoice = (Expr) getOut(node.getValue());
00379     ChooseExpr choose = new ChooseExpr(firstChoice);
00380     Object temp[] = node.getRest().toArray();
00381     for(int i = 0; i < temp.length; i++) {
00382         Expr choice = (Expr) getOut(((AChoicetail) temp[i]).getValue());
00383         if (choice.getType() != choose.getType()) 
00384         error(node.getChoose(), "incompatible types in choose: "); 
00385         choose.addChoice(choice);
00386     }
00387     setOut(node, new AssignAction(var, choose));
00388     }
00389     public void outAChoiceAction(AChoiceAction node)
00390     {
00391     Action action = (Action) getOut(node.getChoice());
00392     currentActions.addElement(action);
00393     }
00394     public void outACollection(ACollection node)
00395     {
00396     Type baseType = (Type) getOut(node.getType());
00397         ConstExpr size = (ConstExpr) getOut(node.getConst());
00398     Collection collection = system.collectionType(baseType,size);
00399     declareVar(node.getId(), collection, null);
00400     }
00401     public void outAConstantDefinition(AConstantDefinition node)
00402     {
00403     String proposedName = node.getId().getText();
00404     checkDecl(node.getId());
00405     int val = parseInt(node.getInt().getText());
00406     String name = system.createName(null, proposedName);
00407     Constant constant = new Constant(name, val, Type.intType);
00408     globalVars.put(name, constant);
00409     system.define(name, constant);
00410     }
00411     public void outADefinedType(ADefinedType node)
00412     {
00413     Object def = globalVars.get(node.getId().getText());
00414     if (def == null) 
00415         error(node.getId(), "type undefined: " + node.getId().getText());
00416     else if (!( def instanceof Type))
00417         error(node.getId(), "not a type: " + node.getId().getText());
00418     else
00419         setOut(node, def);
00420     }
00421     public void outADivExpr2(ADivExpr2 node)
00422     {
00423     Expr arg1 = (Expr) getOut(node.getExpr2());
00424     Expr arg2 = (Expr) getOut(node.getExpr1());
00425         setOut(node, new DivExpr(arg1, arg2));
00426     if (! (arg1.getType().isKind(RANGE) && arg2.getType().isKind(RANGE)))
00427         error(node.getDiv(), "arguments to '/' must be integer");
00428     }
00429     public void outAEnumeratedTypespec(AEnumeratedTypespec node)
00430     {
00431     setOut(node, currentEnumerated);
00432     currentEnumerated = null;
00433     }
00434     public void outAEqExpr5(AEqExpr5 node)
00435     {
00436     Expr arg1 = (Expr) getOut(node.getExpr5());
00437     Expr arg2 = (Expr) getOut(node.getExpr4());
00438     if (! (arg1.getType().isKind(BOOL|RANGE|ENUMERATED|REF) 
00439            && arg2.getType().isKind(BOOL|RANGE|ENUMERATED|REF)))
00440         error(node.getEq(), "arguments to == must be ref, boolean, range, or enumerated");
00441         setOut(node, new EqExpr(arg1, arg2));
00442     }
00443     public void outAExitThreadop(AExitThreadop node)
00444     {
00445         setOut(node, new Integer(EXIT));
00446     }
00447     public void outAExpr(AExpr node)
00448     {
00449         setOut(node, getOut(node.getExpr7()));
00450     }
00451     public void outAExpr0Expr1(AExpr0Expr1 node)
00452     {
00453         setOut(node, getOut(node.getExpr0()));  
00454     }
00455     public void outAExpr1Expr2(AExpr1Expr2 node)
00456     {
00457         setOut(node, getOut(node.getExpr1()));  
00458     }
00459     public void outAExpr2Expr3(AExpr2Expr3 node)
00460     {
00461         setOut(node, getOut(node.getExpr2()));  
00462     }
00463     public void outAExpr3Expr4(AExpr3Expr4 node)
00464     {
00465         setOut(node, getOut(node.getExpr3()));  
00466     }
00467     public void outAExpr4Expr5(AExpr4Expr5 node)
00468     {
00469         setOut(node, getOut(node.getExpr4()));  
00470     }
00471     public void outAExpr5Expr6(AExpr5Expr6 node)
00472     {
00473         setOut(node, getOut(node.getExpr5()));  
00474     }
00475     public void outAExpr6Expr7(AExpr6Expr7 node)
00476     {
00477         setOut(node, getOut(node.getExpr6()));  
00478     }
00479     public void outAFalseBool(AFalseBool node)
00480     {
00481         setOut(node, new BoolLit(false));
00482     }
00483     public void outAField(AField node)
00484     {
00485         String name = node.getId().getText();
00486     Type type = (Type) getOut(node.getType());
00487     currentRecord.addField(name,type);
00488     }
00489     public void outAFieldselectExpr0(AFieldselectExpr0 node)
00490     {
00491     setOut(node, fieldSelect((Expr) getOut(node.getExpr0()),
00492                  node.getId()));
00493     }
00494     public void outAFieldselectLhs(AFieldselectLhs node)
00495     {
00496     setOut(node, fieldSelect((Expr) getOut(node.getLhs()),
00497                  node.getId()));
00498     }
00499     public void outAGeExpr4(AGeExpr4 node)
00500     {
00501     Expr arg1 = (Expr) getOut(node.getExpr4());
00502     Expr arg2 = (Expr) getOut(node.getExpr3());
00503         setOut(node, new LeExpr(arg2, arg1));
00504     if (! (arg1.getType().isKind(RANGE | ENUMERATED) 
00505            && arg2.getType().isKind(RANGE | ENUMERATED)))
00506         error(node.getGe(), "arguments to '>=' must be integer");
00507     }
00508     public void outAGtExpr4(AGtExpr4 node)
00509     {
00510     Expr arg1 = (Expr) getOut(node.getExpr4());
00511     Expr arg2 = (Expr) getOut(node.getExpr3());
00512         setOut(node, new LtExpr(arg2, arg1));
00513     if (! (arg1.getType().isKind(RANGE | ENUMERATED) 
00514            && arg2.getType().isKind(RANGE | ENUMERATED)))
00515         error(node.getGt(), "arguments to '>' must be integer");
00516     }
00517     public void outAHaslockLocktestop(AHaslockLocktestop node)
00518     {
00519         setOut(node, new Integer(HAS_LOCK));
00520     }
00521     public void outAIdConst(AIdConst node)
00522     {
00523     Object def = globalVars.get(node.getId().getText());
00524     if (def == null) 
00525         error(node.getId(), "constant undefined: " + node.getId().getText());
00526     else if (!( def instanceof Constant))
00527         error(node.getId(), "not a constant: " + node.getId().getText());
00528     else
00529         setOut(node, def);
00530     }
00531     public void outAIdValue(AIdValue node)
00532     {
00533         setOut(node, getDecl(node.getId()));
00534     }
00535     public void outAInitializer(AInitializer node)
00536     {
00537         if (node.getAssign() != null) 
00538         setOut(node, getOut(node.getValue()));
00539     else
00540         setOut(node, null);
00541     }
00542     public void outAInstanceofExpr0(AInstanceofExpr0 node)
00543     {
00544     Expr refExpr = (Expr) getOut(node.getExpr0());
00545     Object decl = globalVars.get(node.getId().getText());
00546     if (! refExpr.getType().isKind(REF))
00547         error(node.getInstanceof(), "first argument of 'instanceof' must be a reference");
00548     if ((decl == null) || ! (decl instanceof Ref))
00549         error(node.getInstanceof(), "second argument of 'instanceof' must be a reference type");
00550     else {
00551         Ref refType = (Ref) decl;
00552         setOut(node, new InstanceOfExpr(refExpr, refType));
00553     }
00554     }
00555     public void outAIntConst(AIntConst node)
00556     {
00557     setOut(node, new IntLit(parseInt(node.getInt().getText())));
00558     }
00559     public void outAIntegerValue(AIntegerValue node)
00560     {
00561     setOut(node, new IntLit(parseInt(node.getInt().getText())));
00562     }
00563     public void outAJoinThreadop(AJoinThreadop node)
00564     {
00565         setOut(node, new Integer(JOIN));
00566     }
00567     public void outALeExpr4(ALeExpr4 node)
00568     {
00569     Expr arg1 = (Expr) getOut(node.getExpr4());
00570     Expr arg2 = (Expr) getOut(node.getExpr3());
00571         setOut(node, new LeExpr(arg1, arg2));
00572     if (! (arg1.getType().isKind(RANGE | ENUMERATED) 
00573            && arg2.getType().isKind(RANGE | ENUMERATED)))
00574         error(node.getLe(), "arguments to '<=' must be integer");
00575     }
00576     public void outALivevar(ALivevar node)
00577     {
00578     StateVar var = (StateVar) getDecl(node.getId());
00579     if (var.getThread() == null)
00580         error(node.getId(), "variables in live clause must be local");
00581     else
00582         currentLoc.getLiveVars().addElement(var);
00583     }
00584     public void outALocation(ALocation node)
00585     {
00586     currentLoc = null;
00587     }
00588     public void outALockavailableLocktestop(ALockavailableLocktestop node)
00589     {
00590     setOut(node, new Integer(LOCK_AVAILABLE));
00591     }
00592     public void outALockLockOp(ALockLockOp node)
00593     {
00594         setOut(node, new Integer(LOCK));
00595     }
00596     public void outALocktest(ALocktest node)
00597     {
00598     Expr lock = (Expr) getOut(node.getLhs());
00599     int operation = ((Integer)getOut(node.getLocktestop())).intValue();
00600     setOut(node, new LockTest(lock, operation, currentThread));
00601     }
00602     public void outALocktestExpr0(ALocktestExpr0 node)
00603     {
00604     setOut(node, getOut(node.getLocktest()));
00605     }
00606     public void outALockTypespec(ALockTypespec node)
00607     {
00608     boolean wait = (node.getWait() != null);
00609     boolean reentrant = (node.getReentrant() != null);
00610     setOut(node, system.lockType(wait,reentrant));
00611     }
00612     public void outALockupdate(ALockupdate node)
00613     {
00614     Expr lock = (Expr) getOut(node.getLhs());
00615     int operation = ((Integer)getOut(node.getLockOp())).intValue();
00616     setOut(node, new LockAction(lock, operation, currentThread));
00617     }
00618     public void outALockupdateAction(ALockupdateAction node)
00619     {
00620     Action action = (Action) getOut(node.getLockupdate());
00621     currentActions.addElement(action);
00622     }
00623     public void outALtExpr4(ALtExpr4 node)
00624     {
00625     Expr arg1 = (Expr) getOut(node.getExpr4());
00626     Expr arg2 = (Expr) getOut(node.getExpr3());
00627         setOut(node, new LtExpr(arg1, arg2));
00628     if (! (arg1.getType().isKind(RANGE | ENUMERATED) 
00629            && arg2.getType().isKind(RANGE | ENUMERATED)))
00630         error(node.getLt(), "arguments to '<' must be integer");
00631     }
00632     public void outAMinusExpr1(AMinusExpr1 node)
00633     {
00634     Expr arg1 = new IntLit(0);
00635     Expr arg2 = (Expr) getOut(node.getExpr1());
00636         setOut(node, new SubExpr(arg1, arg2));  
00637     if (! arg1.getType().isKind(RANGE))
00638         error(node.getMinus(), "argument to '-' must be integer");
00639     }
00640     public void outAMinusExpr3(AMinusExpr3 node)
00641     {
00642     Expr arg1 = (Expr) getOut(node.getExpr3());
00643     Expr arg2 = (Expr) getOut(node.getExpr2());
00644         setOut(node, new SubExpr(arg1, arg2));
00645     if (! (arg1.getType().isKind(RANGE) && arg2.getType().isKind(RANGE)))
00646         error(node.getMinus(), "arguments to '-' must be integer");
00647     }
00648     public void outAModExpr2(AModExpr2 node)
00649     {
00650     Expr arg1 = (Expr) getOut(node.getExpr2());
00651     Expr arg2 = (Expr) getOut(node.getExpr1());
00652         setOut(node, new RemExpr(arg1, arg2));
00653     if (! (arg1.getType().isKind(RANGE) && arg2.getType().isKind(RANGE)))
00654         error(node.getMod(), "arguments to '%' must be integer");
00655     }
00656     public void outAMultExpr2(AMultExpr2 node)
00657     {
00658     Expr arg1 = (Expr) getOut(node.getExpr2());
00659     Expr arg2 = (Expr) getOut(node.getExpr1());
00660         setOut(node, new MulExpr(arg1, arg2));
00661     if (! (arg1.getType().isKind(RANGE) && arg2.getType().isKind(RANGE)))
00662         error(node.getMult(), "arguments to '*' must be integer");
00663     }
00664     public void outANameEnumconst(ANameEnumconst node)
00665     {
00666     checkDecl(node.getId());
00667     String name = system.createName(null, node.getId().getText());
00668     Constant constant = currentEnumerated.add(name);
00669     globalVars.put(name, constant);
00670     }
00671     public void outANamevalueEnumconst(ANamevalueEnumconst node)
00672     {
00673     checkDecl(node.getId());
00674     String name = system.createName(null, node.getId().getText());
00675     int value = parseInt(node.getInt().getText());
00676         Constant constant = currentEnumerated.add(name, value);
00677     globalVars.put(name, constant);
00678     }
00679     public void outANoteqExpr5(ANoteqExpr5 node)
00680     {
00681     Expr arg1 = (Expr) getOut(node.getExpr5());
00682     Expr arg2 = (Expr) getOut(node.getExpr4());
00683     if (! (arg1.getType().isKind(BOOL|RANGE|ENUMERATED|REF) 
00684            && arg2.getType().isKind(BOOL|RANGE|ENUMERATED|REF)))
00685         error(node.getNoteq(), "arguments to != must be ref, boolean, range, or enumerated");
00686         setOut(node, new NeExpr(arg1, arg2));
00687     }
00688     public void outANotExpr1(ANotExpr1 node)
00689     {
00690     Expr arg1 = (Expr)getOut(node.getExpr1());
00691     setOut(node, new NotExpr(arg1));
00692     if (! arg1.getType().isKind(BOOL))
00693         error(node.getNot(), "argument to ! must be boolean");
00694     }
00695     public void outANotifyallLockOp(ANotifyallLockOp node)
00696     {
00697     setOut(node, new Integer(NOTIFYALL));
00698     }
00699     public void outANotifyLockOp(ANotifyLockOp node)
00700     {
00701     setOut(node, new Integer(NOTIFY));
00702     }
00703     public void outANullValue(ANullValue node)
00704     {
00705     setOut(node, new NullExpr(system));
00706     }
00707     public void outAOrExpr7(AOrExpr7 node)
00708     {
00709     Expr arg1 = (Expr) getOut(node.getExpr7());
00710     Expr arg2 = (Expr) getOut(node.getExpr6());
00711         setOut(node, new OrExpr(arg1, arg2));
00712     if (! (arg1.getType().isKind(BOOL) && arg2.getType().isKind(BOOL)))
00713         error(node.getOr(), "arguments to || must be boolean");
00714     }
00715     public void outAParenexprExpr0(AParenexprExpr0 node)
00716     {
00717     setOut(node, getOut(node.getExpr()));
00718     }
00719     public void outAPlusExpr1(APlusExpr1 node)
00720     {
00721     setOut(node, getOut(node.getExpr1()));
00722     }
00723     public void outAPlusExpr3(APlusExpr3 node)
00724     {
00725     Expr arg1 = (Expr) getOut(node.getExpr3());
00726     Expr arg2 = (Expr) getOut(node.getExpr2());
00727         setOut(node, new AddExpr(arg1, arg2));
00728     if (! (arg1.getType().isKind(RANGE) && arg2.getType().isKind(RANGE)))
00729         error(node.getPlus(), "arguments to '+' must be integer");
00730     }
00731     public void outAPredicate(APredicate node)
00732     {
00733     String predName = node.getId().getText();
00734     Expr predExpr = (Expr) getOut(node.getExpr());
00735     system.declarePredicate(predName,predExpr);
00736     }
00737     public void outAPrintaction(APrintaction node)
00738     {
00739     setOut(node,currentPrintAction);
00740     currentPrintAction = null;
00741     }
00742     public void outAPrintactionAction(APrintactionAction node)
00743     {
00744     Action action = (Action) getOut(node.getPrintaction());
00745     currentActions.addElement(action);
00746     }
00747     public void outAProcess(AProcess node)
00748     {
00749     String name = node.getStartname().getText();
00750     String endName = node.getEndname().getText();
00751     if (! name.equals(endName))
00752         error(node.getEndname(),
00753           "process " + name + " ended with end " + endName);
00754     system.numberLocations();
00755         setOut(node, system);
00756     }
00757     public void outAProgram(AProgram node)
00758     {
00759       setOut(node, getOut(node.getProcess()));
00760     }
00761     public void outARangeTypespec(ARangeTypespec node) {
00762     ConstExpr lo = (ConstExpr) getOut(node.getLow());
00763     ConstExpr hi = (ConstExpr) getOut(node.getHi());
00764     setOut(node, system.rangeType(lo,hi));
00765     }
00766     public void outARecordTypespec(ARecordTypespec node)
00767     {
00768         system.addType(currentRecord); // Robbyjo's patch
00769     setOut(node, currentRecord);
00770         currentRecord = null;
00771     }
00772     public void outARefTypespec(ARefTypespec node)
00773     {
00774     Ref refType = system.refType();
00775     refType.addTarget(node.getFirst().getText());
00776     Object temp[] = node.getRest().toArray();
00777     for(int i = 0; i < temp.length; i++)
00778         refType.addTarget(((AReftail) temp[i]).getId().getText());
00779     refTypes.addElement(refType);
00780     setOut(node, refType);
00781     }
00782     public void outARefValue(ARefValue node)
00783     {
00784     Expr arg = getDecl(node.getId());
00785     if (! (arg instanceof StateVar))
00786         error(node.getId(), "'ref' can be invoked only on a variable");
00787     StateVar singleton = (StateVar) arg;
00788     if (! singleton.getType().isKind(ARRAY|RECORD))
00789         error(node.getId(), "'ref' can be invoked only on arrays/records");
00790     setOut(node, new RefExpr(singleton));
00791     }
00792     public void outARemoterefExpr0(ARemoterefExpr0 node)
00793     {
00794     if (! inPredicate)
00795         error(node.getThreadname(),
00796           "Remote references can only be used in predicates");
00797     String threadName = node.getThreadname().getText();
00798     BirThread thread = (BirThread)threads.get(threadName);
00799     if (thread == null)
00800         error(node.getThreadname(), "thread not declared: " + threadName);
00801     String localName = node.getLocalname().getText();
00802     Hashtable threadLocalVars =(Hashtable)threadLocalVarTables.get(thread);
00803     Object var = threadLocalVars.get(localName);
00804     if (var == null || !(var instanceof StateVar))
00805         error(node.getLocalname(),"invalid local: " + localName);
00806     setOut(node, var);
00807     }
00808     public void outAStartThreadop(AStartThreadop node)
00809     {
00810         setOut(node, new Integer(START));
00811     }
00812     public void outAStringPrintarg(AStringPrintarg node)
00813     {
00814     String s = node.getString().getText();
00815         currentPrintAction.addPrintItem(s.substring(1,s.length() - 1));
00816     }
00817     public void outATerminatedThreadtest(ATerminatedThreadtest node)
00818     {
00819     BirThread thread = (BirThread)threads.get(node.getId().getText());
00820     if (thread == null)
00821         error(node.getId(), "thread not yet declared: " + 
00822           node.getId().getText());
00823     int operation = THREAD_TERMINATED;
00824     setOut(node, new ThreadTest(thread, operation, currentThread));
00825     }
00826     public void outAThread(AThread node)
00827     {
00828     String name = node.getStartname().getText();
00829     String endName = node.getEndname().getText();
00830     if (! name.equals(endName))
00831         error(node.getEndname(),
00832           "thread " + name + " ended with end " + endName);
00833     localVars = null;
00834     currentThread = null;   
00835     threadLocs = null;
00836     }
00837     public void outAThreadtestExpr0(AThreadtestExpr0 node)
00838     {
00839     setOut(node, getOut(node.getThreadtest()));
00840     }
00841     public void outAThreadupdate(AThreadupdate node)
00842     {
00843     String threadArg = node.getId().getText();
00844     BirThread thread = (BirThread)threads.get(node.getId().getText());
00845     if (thread == null)
00846         error(node.getId(), "thread not yet declared: " + threadArg);
00847     int operation = ((Integer)getOut(node.getThreadop())).intValue();
00848     if (operation == EXIT && thread != currentThread)
00849         error(node.getId(), "can only exit current thread " + threadArg);
00850     setOut(node, new ThreadAction(thread, operation, currentThread));
00851     }
00852     public void outAThreadupdateAction(AThreadupdateAction node)
00853     {
00854     Action action = (Action) getOut(node.getThreadupdate());
00855     currentActions.addElement(action);
00856     }
00857     public void outATransformation(ATransformation node)
00858     {
00859     Location toLoc = (Location) threadLocs.get(node.getId().getText());
00860     if (toLoc == null)
00861         error(node.getId(), "target of goto not found: " + 
00862           node.getId().getText());
00863     Expr guard = (Expr) getOut(node.getExpr());
00864     if (! guard.getType().isKind(BOOL)) 
00865         error(node.getWhen(), "guard expression must be boolean" +
00866           node.getExpr());
00867     Transformation trans = currentLoc.addTrans(toLoc,guard,currentActions);
00868     trans.setVisible(node.getInvisible() == null);
00869     currentActions = null;
00870     }
00871     public void outATrueBool(ATrueBool node)
00872     {
00873         setOut(node, new BoolLit(true));
00874     }
00875     public void outATypedefDefinition(ATypedefDefinition node)
00876     {
00877     String name = node.getId().getText();
00878     checkDecl(node.getId());
00879     Type type = (Type) getOut(node.getTypespec());
00880     type.setName(name);
00881     globalVars.put(name, type);
00882     system.define(name, type);  
00883     }
00884     public void outATypespecType(ATypespecType node)
00885     {
00886     setOut(node, getOut(node.getTypespec()));
00887     }
00888     public void outAUnlockLockOp(AUnlockLockOp node)
00889     {
00890         setOut(node, new Integer(UNLOCK));
00891     }
00892     public void outAUnwaitLockOp(AUnwaitLockOp node)
00893     {
00894     setOut(node, new Integer(UNWAIT));
00895     }
00896     public void outAValueExpr0(AValueExpr0 node)
00897     {
00898         setOut(node, getOut(node.getValue()));        
00899     }
00900     public void outAValueLhs(AValueLhs node)
00901     {
00902         setOut(node, getDecl(node.getId()));
00903     }
00904     public void outAVariable(AVariable node)
00905     {
00906     Expr initVal = (node.getInitializer() == null) ? null : 
00907         (Expr) getOut(node.getInitializer());
00908     declareVar(node.getId(), (Type) getOut(node.getType()), initVal);
00909     }
00910     public void outAVarPrintarg(AVarPrintarg node)
00911     {
00912     Expr arg = getDecl(node.getId());
00913     if (! (arg instanceof StateVar))
00914         error(node.getId(), "can only print variables");
00915     StateVar var = (StateVar) arg;
00916     if (! var.getType().isKind(BOOL|RANGE|ENUMERATED))
00917         error(node.getId(), "can only print boolean, range, or enum types");
00918         currentPrintAction.addPrintItem(var);   
00919     }
00920     public void outAWaitLockOp(AWaitLockOp node)
00921     {
00922     setOut(node, new Integer(WAIT));
00923     }
00924     public void outAWasnotifiedLocktestop(AWasnotifiedLocktestop node)
00925     {
00926     setOut(node, new Integer(WAS_NOTIFIED));
00927     }
00928     public void outStart(Start node)
00929     {
00930       setOut(node, getOut(node.getPProgram()));
00931     }
00932     public static TransSystem parse(String birSource) {
00933     TransSystem result = null;
00934     try {
00935         // Robbyjo's patch begin
00936         if (birSource == null) throw new RuntimeException("Null filename detected!");
00937         String fileName = birSource;
00938         if (!fileName.toLowerCase().endsWith(".bir")) fileName += ".bir";
00939         // Robbyjo's patch end
00940         File birFile = new File(fileName);
00941         FileInputStream streamIn = new FileInputStream(birFile);
00942         InputStreamReader streamRead = new InputStreamReader(streamIn);
00943         PushbackReader pushRead = new PushbackReader(streamRead, 1024);
00944         Lexer lex = new Lexer(pushRead);
00945         Parser parser = new Parser(lex);
00946         Start tree = parser.parse();
00947         BirBuilder builder = new BirBuilder(fileName);
00948         tree.apply(builder);
00949         result = (TransSystem) builder.getOut(tree);
00950         streamIn.close();
00951         return result;
00952         } catch(IOException e) {
00953             throw new RuntimeException("Could not open BIR source file (" + e + ")");
00954         } catch(LexerException e) {
00955         System.out.println("Lexical error:\n" + e);
00956     } catch(ParserException e) {
00957         System.out.println("Syntax error:\n" + e);
00958     }
00959     return null;
00960   }  
00961     int parseInt(String s) {
00962     try {
00963         int result = Integer.parseInt(s);
00964         return result;
00965     } catch (NumberFormatException e) {
00966         throw new RuntimeException("Integer didn't parse: " + s);
00967     }
00968     }
00969     public static TransSystem parseString(String birSource) {
00970     TransSystem result = null;
00971     try {
00972         if (birSource == null) throw new RuntimeException("Null filename detected!");
00973         String fileName = "";
00974         PushbackReader pushRead = new PushbackReader(new StringReader(birSource), 1024);
00975         Lexer lex = new Lexer(pushRead);
00976         Parser parser = new Parser(lex);
00977         Start tree = parser.parse();
00978         BirBuilder builder = new BirBuilder(fileName);
00979         tree.apply(builder);
00980         result = (TransSystem) builder.getOut(tree);
00981         return result;
00982         } catch(IOException e) {
00983             throw new RuntimeException("Could not open BIR source file (" + e + ")");
00984         } catch(LexerException e) {
00985         System.out.println("Lexical error:\n" + e);
00986     } catch(ParserException e) {
00987         System.out.println("Syntax error:\n" + e);
00988     }
00989     return null;
00990   }    
00991 }