Driver.java Source File

00001 package edu.ksu.cis.bandera.bui;
00002 
00003 /* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
00004  * Bandera, a Java(TM) analysis and transformation toolkit           *
00005  * Copyright (C) 2000, 2001 Roby Joehanes (robbyjo@cis.ksu.edu)      *
00006  * Copyright (C) 2000   Robby (robby@cis.ksu.edu)                    *
00007  * All rights reserved.                                              *
00008  *                                                                   *
00009  * This work was done as a project in the SAnToS Laboratory,         *
00010  * Department of Computing and Information Sciences, Kansas State    *
00011  * University, USA (http://www.cis.ksu.edu/santos).                  *
00012  * It is understood that any modification not identified as such is  *
00013  * not covered by the preceding statement.                           *
00014  *                                                                   *
00015  * This work is free software; you can redistribute it and/or        *
00016  * modify it under the terms of the GNU Library General Public       *
00017  * License as published by the Free Software Foundation; either      *
00018  * version 2 of the License, or (at your option) any later version.  *
00019  *                                                                   *
00020  * This work is distributed in the hope that it will be useful,      *
00021  * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
00022  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
00023  * Library General Public License for more details.                  *
00024  *                                                                   *
00025  * You should have received a copy of the GNU Library General Public *
00026  * License along with this toolkit; if not, write to the             *
00027  * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
00028  * Boston, MA  02111-1307, USA.                                      *
00029  *                                                                   *
00030  * Java is a trademark of Sun Microsystems, Inc.                     *
00031  *                                                                   *
00032  * To submit a bug report, send a comment, or get the latest news on *
00033  * this project and other SAnToS projects, please visit the web-site *
00034  *                http://www.cis.ksu.edu/santos                      *
00035  * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
00036 import java.io.*;
00037 import java.util.*;
00038 import javax.swing.*;
00039 import ca.mcgill.sable.soot.*;
00040 import ca.mcgill.sable.soot.jimple.*;
00041 import gov.nasa.arc.ase.jpf.*;
00042 import gov.nasa.arc.ase.jpf.iVirtualMachine;
00043 import gov.nasa.arc.ase.jpf.Engine;
00044 import gov.nasa.arc.ase.jpf.tools.*;
00045 import edu.ksu.cis.bandera.abstraction.*;
00046 import edu.ksu.cis.bandera.abstraction.gui.*;
00047 import edu.ksu.cis.bandera.abstraction.options.*;
00048 import edu.ksu.cis.bandera.abstraction.typeinference.*;
00049 import edu.ksu.cis.bandera.annotation.*;
00050 import edu.ksu.cis.bandera.bir.*;
00051 import edu.ksu.cis.bandera.birc.*;
00052 import edu.ksu.cis.bandera.birc.PredicateSet;
00053 import edu.ksu.cis.bandera.bofa.BOFA;
00054 import edu.ksu.cis.bandera.bui.counterexample.*;
00055 import edu.ksu.cis.bandera.bui.session.*;
00056 import edu.ksu.cis.bandera.bui.session.datastructure.*;
00057 import edu.ksu.cis.bandera.dspin.*;
00058 import edu.ksu.cis.bandera.jjjc.*;
00059 import edu.ksu.cis.bandera.jjjc.decompiler.*;
00060 import edu.ksu.cis.bandera.jjjc.optimizer.*;
00061 import edu.ksu.cis.bandera.jjjc.symboltable.*;
00062 import edu.ksu.cis.bandera.jjjc.symboltable.Package;
00063 import edu.ksu.cis.bandera.jext.*;
00064 import edu.ksu.cis.bandera.pdgslicer.*;
00065 import edu.ksu.cis.bandera.pdgslicer.dependency.*;
00066 import edu.ksu.cis.bandera.pdgslicer.datastructure.*;
00067 import edu.ksu.cis.bandera.specification.Compiler;
00068 import edu.ksu.cis.bandera.specification.*;
00069 import edu.ksu.cis.bandera.specification.assertion.*;
00070 import edu.ksu.cis.bandera.specification.assertion.datastructure.*;
00071 import edu.ksu.cis.bandera.specification.pattern.*;
00072 import edu.ksu.cis.bandera.specification.pattern.datastructure.*;
00073 import edu.ksu.cis.bandera.specification.predicate.*;
00074 import edu.ksu.cis.bandera.specification.predicate.datastructure.*;
00075 import edu.ksu.cis.bandera.specification.predicate.node.*;
00076 import edu.ksu.cis.bandera.specification.predicate.lexer.*;
00077 import edu.ksu.cis.bandera.specification.predicate.parser.*;
00078 import edu.ksu.cis.bandera.specification.datastructure.*;
00079 import edu.ksu.cis.bandera.specification.node.*;
00080 import edu.ksu.cis.bandera.report.*;
00081 import edu.ksu.cis.bandera.smv.*;
00082 import edu.ksu.cis.bandera.spin.*;
00083 import edu.ksu.cis.bandera.prog.*;
00084 import edu.ksu.cis.bandera.util.*;
00085 
00086 public class Driver extends Thread {
00087     private Hashtable importedAssertion = new Hashtable();
00088     private Hashtable importedAssertionSet = new Hashtable();
00089     private Hashtable predNodeGrimpTable = new Hashtable();
00090     private HashSet placeHolders = new HashSet();
00091     private static HashSet predicates = new HashSet();
00092     private HashSet stmtsVector = new HashSet();
00093     private static HashSet quantifierSliceInterests = new HashSet();
00094     private edu.ksu.cis.bandera.bir.TransSystem sys;
00095     private static boolean isCodeChanged = false;
00096     private boolean isRecompiled = false;
00097     private static boolean isNotRoboto = true;
00098     private StringBuffer execSummary = new StringBuffer();
00099     private static boolean isDumped = false;
00100     private static boolean genReport = false;
00101     private TypeTable typeTable = new TypeTable();
00102     private static boolean isWindows = System.getProperty("os.name").indexOf("Windows") >= 0;
00103     private Hashtable options; // **
00104     private LinkedList qList = new LinkedList(); // robbyjo's patch: To store class/quantified vars info.
00105     private static boolean isGUI = true;
00106     private ReportManager rm = new ReportManager();
00107     private static String expectedResultPath;
00108 /**
00109  * 
00110  */
00111 public Driver() {
00112     predicates = new HashSet();
00113     quantifierSliceInterests = new HashSet();
00114 }
00115 /**
00116    *
00117    */
00118 private void dump(String phase) {
00119     String path = getTempDir(phase);
00120     if (!BanderaUtil.mkdirs(path))
00121     {
00122         String errmsg = "***Can't make temporary directory for dumping jimple!";
00123         System.out.println(errmsg);
00124         if (isGUI && isNotRoboto)
00125             JOptionPane.showMessageDialog(null,errmsg, "Error", JOptionPane.ERROR_MESSAGE);
00126         else execSummary.append(errmsg);
00127         return;
00128     }
00129     StoredBody bd = new StoredBody(ca.mcgill.sable.soot.jimple.Jimple.v());
00130     for (Enumeration e = CompilationManager.getCompiledClasses().elements(); e.hasMoreElements();) {
00131         SootClass sc = (SootClass) e.nextElement();
00132         String className = sc.getName();
00133         try {
00134             java.io.File jimpFile = new java.io.File(path + File.separator + className + ".jimple");
00135             java.io.FileOutputStream jimpOut = new java.io.FileOutputStream(jimpFile);
00136             sc.printTo(bd, new java.io.PrintWriter(jimpOut, true));
00137             jimpOut.close();
00138         } catch (java.io.IOException ex) {
00139             if (isGUI && isNotRoboto)
00140                 JOptionPane.showMessageDialog(null, ex.getMessage(), "Error", JOptionPane.ERROR_MESSAGE);
00141             else execSummary.append("***Can't dump! "+ex.getMessage()+"\n");
00142         }
00143     }
00144 }
00145 /**
00146    *
00147    */
00148 private void dumpJimpleTrace(JimpleTrace trace) {
00149     AnnotationManager am = CompilationManager.getAnnotationManager();
00150     Stmt[] stmts = trace.getStatements();
00151     Annotation prevAnn = null;
00152     for (int i = 0; i < stmts.length; i++) {
00153         try {
00154             Annotation a = am.getContainingAnnotation(stmts[i]);
00155             if (prevAnn != a) {
00156                 prevAnn = a;
00157                 System.out.println("****************************************");
00158                 System.out.println("****************************************");
00159                 System.out.println("Step #: " + i);
00160                 SootMethod sm = ((MethodDeclarationAnnotation) am.getMethodAnnotationContainingAnnotation(a)).getSootMethod();
00161                 JimpleStore store = trace.getStore(i);
00162                 System.out.println("Control at method: " + sm + ", stmt: " + stmts[i]);
00163                 System.out.println("Annotation: " + a);
00164                 //store.print();
00165             }
00166         } catch (Exception e) {
00167             System.out.println(e.getMessage());
00168         }
00169     }
00170 }
00171 /**
00172  * 
00173  * @param tempSuffix java.lang.String
00174  */
00175 private String generateJava(String tempSuffix) {
00176     String path = getTempDir(tempSuffix);
00177     if (!BanderaUtil.mkdirs(path))
00178     {
00179         String errmsg = "***Can't make temporary directory for dumping jimple!";
00180         System.out.println(errmsg);
00181         if (isGUI && isNotRoboto)
00182             JOptionPane.showMessageDialog(null,errmsg, "Error", JOptionPane.ERROR_MESSAGE);
00183         else execSummary.append(errmsg);
00184         return "";
00185     }
00186     Decompiler decompiler = new Decompiler(CompilationManager.getCompiledClasses(), CompilationManager.getAnnotationManager(), path, "java");
00187     decompiler.decompile();
00188     if (tempSuffix.equals("JPF"))
00189         CompilationManager.getAnnotationManager().setFilenameLinePairAnnotationTable(decompiler.getLineToAnnotationTable());
00190     return (new File(path)).getAbsolutePath();
00191 }
00192 /**
00193  * 
00194  * @return ca.mcgill.sable.soot.SootClass[]
00195  */
00196 private SootClass[] getClassesForBIRC() {
00197     HashSet set = getMethodsForInliner();
00198     SootClass[] result = new SootClass[set.size()];
00199     int i = 0;
00200     for (Iterator j = set.iterator(); j.hasNext(); i++) {
00201         result[i] = ((SootMethod) j.next()).getDeclaringClass();
00202     }
00203     return result;
00204 }
00205 /**
00206  * 
00207  * @return java.util.HashSet
00208  */
00209 private HashSet getMethodsForInliner() {
00210     HashSet result = new HashSet();
00211     ca.mcgill.sable.util.LinkedList args = new ca.mcgill.sable.util.LinkedList();
00212     args.add(ca.mcgill.sable.soot.ArrayType.v(RefType.v("java.lang.String"), 1));
00213     ca.mcgill.sable.util.LinkedList args2 = new ca.mcgill.sable.util.LinkedList();
00214 
00215     HashSet rClasses = IdentifyRunnableClasses.identify(CompilationManager.getCompiledClasses().elements());
00216     for (Iterator rcIt = rClasses.iterator(); rcIt.hasNext();) {
00217         SootClass sc = (SootClass) rcIt.next();
00218         if (sc.declaresMethod("main", args)) {
00219             result.add(sc.getMethod("main", args));
00220         } else if (sc.declaresMethod("run", args2)) {
00221             result.add(sc.getMethod("run", args2));
00222         }
00223     }
00224 
00225     return result;
00226 }
00227 /**
00228  * 
00229  * @return java.util.Vector
00230  */
00231 public static Vector getSliceInterests() {
00232     Vector v = (Vector) AssertionSliceInterestCollector.collect(new Vector());
00233     v.addAll(PredicateSliceInterestCollector.collect(predicates));
00234     v.addAll(quantifierSliceInterests);
00235     return v;
00236 }
00237 /**
00238  * 
00239  * @return ca.mcgill.sable.soot.SootClass[]
00240  */
00241 private SootClass[] getSootClassesForBIRC() {
00242     Hashtable table = CompilationManager.getCompiledClasses();
00243     Vector v = new Vector();
00244     v.add(CompilationManager.getMainSootClass());
00245     for (Enumeration e = table.elements(); e.hasMoreElements();) {
00246         SootClass sc = (SootClass) e.nextElement();
00247         if (sc.declaresMethod("run")) {
00248             v.add(sc);
00249         }
00250     }
00251     SootClass[] result = new SootClass[v.size()];
00252     int i = 0;
00253     for (Enumeration e = v.elements(); e.hasMoreElements(); i++) {
00254         result[i] = (SootClass) e.nextElement();
00255     }
00256     return result;
00257 }
00258 public String getSummary() { return execSummary.toString(); }
00259 private String getTempDir(String suffix)
00260 {
00261     String s = System.getProperty("user.dir") + File.separator + "temp$" + BUI.sessions.getActiveSession().getName();
00262     if (suffix == null || suffix.equals("")) return s;
00263     return s + File.separator + suffix;
00264 }
00265 /**
00266  * 
00267  */
00268 public void initAssertions() throws Exception {
00269     for (Iterator i = BUI.property.getImportedAssertion().iterator(); i.hasNext();) {
00270         Name name = (Name) i.next();
00271         Assertion as = AssertionSet.getAssertion(name);
00272         this.importedAssertion.put(name, as);
00273     }
00274     
00275     for (Iterator i = BUI.property.getImportedAssertionSet().iterator(); i.hasNext();) {
00276         Name name = (Name) i.next();
00277         AssertionSet as = AssertionSet.getAssertionSet(name);
00278         this.importedAssertionSet.put(name, as);
00279     }
00280 }
00281 public void initCmdLine(Session ses, boolean dump, boolean report, String expectedPath) {
00282     isGUI = false;
00283     isDumped = dump;
00284     genReport = report;
00285     isNotRoboto = true;
00286     expectedResultPath = expectedPath;
00287     BUI.sessions.putSession(ses);
00288     BUI.sessions.setActiveSession(ses);
00289 
00290     // Prepare the Compilation Manager
00291     CompilationManager.reset();
00292     CompilationManager.setFilename(ses.getFilename());
00293     CompilationManager.setClasspath(ses.getClasspath());
00294     CompilationManager.setIncludedPackagesOrTypes(ses.getIncludedPackagesOrTypes());
00295     AssertionSet.reset();
00296     edu.ksu.cis.bandera.specification.predicate.datastructure.PredicateSet.reset();
00297 
00298     // Load Specification File
00299     String spec = ses.getSpecFilename();
00300     Property prop = new Property();
00301     if ((spec != null) && (spec.length() > 0)) {
00302         try {
00303             prop = new SpecificationSaverLoader().load(spec);
00304             execSummary.append("   Spec loaded");
00305             String activeProp = ses.getActiveTemporal();
00306             if (activeProp != null) {
00307                 TemporalLogicProperty tlp = prop.getTemporalLogicProperty(activeProp);
00308                 if ((tlp != null) && (!prop.isActivated(tlp))) {
00309                     prop.activateOrDeactivateTemporalLogicProperty(tlp);
00310                 }
00311             }
00312             HashSet activeAssertion = ses.getActiveAssertions();
00313             if ((activeAssertion != null) && (!activeAssertion.isEmpty())) {
00314                 for (Iterator i = activeAssertion.iterator(); i.hasNext();) {
00315                     String curActiveAssertion = (String) i.next();
00316                     if (curActiveAssertion != null) {
00317                         AssertionProperty assn = prop.getAssertionProperty(curActiveAssertion);
00318                         if ((assn != null) && (!prop.isActivated(assn))) {
00319                             prop.activateOrDeactivateAssertionProperty(assn);
00320                         }
00321                     }
00322                 }
00323             }
00324             execSummary.append(" and activated\n");
00325         } catch (Exception e) {
00326             execSummary.append("   Cannot load '" + spec + "' specification!\n");
00327         }
00328     }
00329     BUI.property = prop;
00330 
00331     // Load the options
00332     BUI.doJJJC = true;
00333     BUI.doSLABS = ses.isDoSLABS();
00334     BUI.doChecker = ses.isDoChecker();
00335     BUI.doSlicer = ses.isDoSlicer();
00336     //if (ses.isUseJPF()) BUI.jpfOption.parseOptions(ses.getJpfOptions());
00337     if (ses.isUseSPIN())
00338         SpinOption.spinOptions.parseOptions(ses.getSpinOptions());
00339     //if (ses.isUseDSPIN()) DSpinOption.spinOptions.parseOptions(ses.getDspinOptions());
00340     //if (ses.isUseSMV())
00341 }
00342 /**
00343  * 
00344  * @param dump boolean
00345  * @param report boolean
00346  * @param expectedPath java.lang.String
00347  */
00348 public static void initRoboto(boolean dump, boolean report, String expectedPath) {
00349     isNotRoboto = false;
00350     isGUI = true;
00351     isDumped = dump;
00352     genReport = report;
00353     expectedResultPath = expectedPath;
00354 }
00355 private boolean isCompilationNeeded()
00356 {
00357     if (isCodeChanged || (BUI.irOptions.getSLABSJavaCheckBox().isSelected() && !BUI.doSLABS)) return true;
00358     Hashtable compClasses = CompilationManager.getCompiledClasses();
00359     for (Enumeration e = compClasses.keys(); e.hasMoreElements();)
00360     {
00361         String name = (String) e.nextElement();
00362         try {
00363             if (!(new File(name+".class")).exists()) return true;
00364         } catch (Exception ex)
00365         {
00366             System.out.println(name+".class doesn't exist!");
00367         }
00368     }
00369     return false;
00370 }
00371 /**
00372  * 
00373  * @return edu.ksu.cis.bandera.jjjc.symboltable.Name
00374  * @param name edu.ksu.cis.bandera.jjjc.symboltable.Name
00375  */
00376 public Assertion resolveAssertionName(Name name) throws Exception {
00377     Assertion a = (Assertion) importedAssertion.get(name);
00378     if (a != null)
00379         return a;
00380 
00381     if (!name.isSimpleName()) {
00382         try {
00383             return AssertionSet.getAssertion(name);
00384         } catch (Exception e) {
00385             throw new Exception("Can't resolve assertion with name '" + name + "'");
00386         }
00387     }
00388 
00389     Vector v = new Vector();
00390 
00391     for (Enumeration e = importedAssertionSet.elements(); e.hasMoreElements();) {
00392         AssertionSet as = (AssertionSet) e.nextElement();
00393         if (as.getAssertionTable().get(new Name(as.getName(), name)) != null) {
00394             v.add(as);
00395         }
00396     }
00397 
00398     if (v.size() > 1)
00399         throw new Exception("Ambiguous assertion with name '" + name + "'");
00400     if (v.size() < 1)
00401         throw new Exception("Can't resolve assertion with name '" + name + "'");
00402 
00403     AssertionSet as = (AssertionSet) v.firstElement();
00404     a = (Assertion) as.getAssertionTable().get(new Name(as.getName(), name));
00405     return a;
00406 }
00407 /**
00408  * 
00409  */
00410 public void run() {
00411     System.out.println("*** BEGIN ***");
00412     Session session = BUI.sessions.getActiveSession();
00413     if ((session == null) && isGUI && isNotRoboto) {
00414         JOptionPane.showMessageDialog(BUI.bui, "There is no active session to be executed", "Information", JOptionPane.INFORMATION_MESSAGE);
00415         BUI.isExecuting = false;
00416         return;
00417     }
00418     //Logger.dump(session);
00419     System.out.println("-------------------------------------------------------------------------------");
00420     System.out.println("| ** Session " + session.getName() + " is selected. **");
00421     System.out.println("-------------------------------------------------------------------------------");
00422     System.setProperty("user.dir", BUI.originalUserDir);
00423     try {
00424         BOFA.reset();
00425     } catch (Exception e) {
00426     }
00427     execSummary.append("   BOFA is reset");
00428     if (BUI.doJJJC) {
00429         if (!runJJJC()) {
00430             //Logger.keep();
00431             return;
00432         }
00433         execSummary.append("   JJJC OK");
00434         if (isDumped || (isGUI && BUI.irOptions.getJJJCCheckBox().isSelected())) {
00435             dump("original");
00436             execSummary.append(" and dumped");
00437         }
00438         execSummary.append("\n");
00439     }
00440 
00441     // Bandera SL
00442     if (true || BUI.doSlicer || BUI.doSLABS || BUI.doChecker) {
00443         if (!runBSL()) {
00444             //Logger.keep();
00445             return;
00446         }
00447         execSummary.append("   BSL OK");
00448         if (isDumped || (isGUI && BUI.irOptions.getBSLCheckBox().isSelected())) {
00449             dump("bsl");
00450             execSummary.append(", dumped");
00451         }
00452         if (isDumped || (isGUI && BUI.irOptions.getBSLJavaCheckBox().isSelected())) {
00453             generateJava("bsl");
00454             execSummary.append(" and decompiled");
00455         }
00456         execSummary.append("   Spec Compiled\n");
00457         //dump("BSL");
00458     }
00459 
00460     // Slicer
00461     if (BUI.doSlicer) {
00462         if (!runSlicer()) {
00463             //Logger.keep();
00464             return;
00465         }
00466         execSummary.append("   Slicer OK");
00467         if (isDumped || (isGUI && BUI.irOptions.getSlicingCheckBox().isSelected())) {
00468             dump("sliced");
00469             execSummary.append(", dumped");
00470         }
00471         if (isDumped || (isGUI && BUI.irOptions.getSlicingJavaCheckBox().isSelected())) {
00472             generateJava("sliced");
00473             execSummary.append(" and decompiled");
00474         }
00475         execSummary.append("\n");
00476     }
00477 
00478     // BABS or Inliner
00479     if (isGUI) {
00480         if (isRecompiled) {
00481             Vector v = new Vector();
00482             for (Enumeration e = CompilationManager.getCompiledClasses().elements(); e.hasMoreElements();) {
00483                 v.add(e.nextElement());
00484             }
00485             BUI.typeGUI.setClasses(v);
00486             String absFile = session.getAbsFilename();
00487             if ((absFile == null) || ("".equals(absFile))) {
00488                 options = BUI.typeGUI.getOptions();
00489             } else {
00490                 try {
00491                     options = OptionsSaverLoader.load(CompilationManager.getSootClassManager(), new FileReader(absFile));
00492                     BUI.typeGUI.setSelectedTypes(options, new File(absFile).getAbsolutePath());
00493                 } catch (Exception e) {
00494                      e.printStackTrace();
00495                 }
00496             }
00497         }
00498     } else {
00499         if (BUI.doSLABS) {
00500             String absFile = session.getAbsFilename();
00501             if ((absFile == null) || ("".equals(absFile))) {
00502                 execSummary.append("***WARNING: Abstraction Option is not specified!");
00503                 options = new Hashtable();
00504             } else {
00505                 try {
00506                     options = OptionsSaverLoader.load(CompilationManager.getSootClassManager(), new FileReader(absFile));
00507                 } catch (Exception e) {
00508                      e.printStackTrace();
00509                 }
00510             }
00511         }
00512     }
00513     if (BUI.doSLABS) {
00514         if (!runSLABS()) {
00515             //Logger.keep();
00516             return;
00517         }
00518         execSummary.append("   SLABS OK");
00519         if (isDumped || (isGUI && BUI.irOptions.getSLABSCheckBox().isSelected())) {
00520             dump("abstracted");
00521             execSummary.append(", dumped");
00522         }
00523         if (isDumped || (isGUI && BUI.irOptions.getSLABSJavaCheckBox().isSelected())) {
00524             generateJava("abstracted");
00525             execSummary.append(" and decompiled");
00526         }
00527         execSummary.append("\n");
00528     }
00529 
00530     // Checker
00531     {
00532         if (BUI.sessions.getActiveSession().isUseJPF())
00533             runJPF();
00534         else
00535         {
00536             if (BUI.sessions.getActiveSession().isUseSPIN() || BUI.sessions.getActiveSession().isUseSMV() || BUI.sessions.getActiveSession().isUseDSPIN() ||
00537                 (isDumped || (isGUI && BUI.irOptions.getBIRCheckBox().isSelected()))) {
00538                 runBIRC();
00539             }
00540         }
00541         if (isGUI) {
00542             BUI.bui.getSpinLabel().setIcon(IconLibrary.spinIcon);
00543             BUI.bui.getJPFLabel().setIcon(IconLibrary.jpfIcon);
00544             BUI.bui.getNuSMVLabel().setIcon(IconLibrary.smvIcon);
00545         }
00546     }
00547     
00548     writeReport();
00549 
00550     // END
00551     CompilationManager.setQuantifiers(new Vector());
00552     BUI.isExecuting = false;
00553     System.out.println("*** END ***");
00554 }
00555 /**
00556  * 
00557  */
00558 private void runBIRC() {
00559     String defaultName = "";
00560     try {
00561         AnnotationManager am = CompilationManager.getAnnotationManager();
00562         Inline.typeTable = typeTable;
00563         for (Iterator i = getMethodsForInliner().iterator(); i.hasNext();) {
00564             SootMethod sm = (SootMethod) i.next();
00565             Inline.inline(sm, am);
00566         }
00567         Inline.typeTable = null;
00568         KSUOptimizing.packLocalsForClasses(getSootClassesForBIRC());
00569         if (isDumped || (isGUI && BUI.irOptions.getBIRCCheckBox().isSelected())) {
00570             dump("inlined");
00571         }
00572         PredicateSet ps = new PredicateSet();
00573         defaultName = BUI.sessions.getActiveSession().getOutputName();
00574         if (isWindows && defaultName.length() > 8)
00575             defaultName = defaultName.substring(0, 8);
00576         String workingDir = BUI.sessions.getActiveSession().getWorkingDirectory();
00577         for (Enumeration keys = predNodeGrimpTable.keys(); keys.hasMoreElements();) {
00578             Object key = keys.nextElement();
00579             Value value = (Value) predNodeGrimpTable.get(key);
00580             try {
00581                 value = PredicateUpdate.update(value);
00582             } catch (Exception e) {
00583                 throw new RuntimeException("Predicate '" + key + "' is not reachable in the code");
00584             }
00585             predNodeGrimpTable.put(key, value);
00586         }
00587         TemporalLogicProperty tlp = BUI.property.getActivatedTemporalLogicProperty();
00588         String birName = defaultName + ".bir";
00589 
00590         if (tlp != null && (BUI.sessions.getActiveSession().isUseSPIN() ||
00591             BUI.sessions.getActiveSession().isUseSMV() ||
00592             BUI.sessions.getActiveSession().isUseDSPIN())) {
00593             Pattern pattern = PatternSaverLoader.getPattern(tlp.getPatternName(), tlp.getPatternScope());
00594             Compiler compiler = new Compiler(predNodeGrimpTable, placeHolders, pattern, tlp.getNode());
00595             String ltlFormula = "!(" + compiler.getFormula("LTL") + ")";
00596             Hashtable parameterTable = compiler.getParameterTable();
00597             SpecificationAbstractor sa = new SpecificationAbstractor();
00598             sa.abstractLTL(new CoercionManager(AbstractionLibraryManager.getAbstractions()), typeTable, ltlFormula, parameterTable);
00599             ltlFormula = sa.getLtlFormula();
00600             parameterTable = sa.getParameterTable();
00601             for (Enumeration e = parameterTable.keys(); e.hasMoreElements();) {
00602                 String key = (String) e.nextElement();
00603                 ca.mcgill.sable.soot.jimple.Expr value = (ca.mcgill.sable.soot.jimple.Expr) parameterTable.get(key);
00604                 ps.addValuePredicate(key, value);
00605                 
00606                 //if (isDumped) {
00607                 //  ((BSLReport) rm.getReport("BSL")).addLTLPredicate(key, value);
00608                 //}
00609             }
00610             //if (isDumped) {
00611             //  ((BSLReport) rm.getReport("BSL")).setLTL(ltlFormula);
00612             //}
00613             System.out.println("");
00614             System.out.println("Never claim: " + ltlFormula);
00615             ps.print();
00616             System.out.println("");
00617             PrintWriter pw = new PrintWriter(new FileWriter(defaultName + ".ltl"));
00618             pw.print(ltlFormula);
00619             pw.close();
00620         } else {
00621             if (isGUI) {
00622                 BUI.spinOption.setApplyNeverClaim(false);
00623                 BUI.spinOption.setAcceptanceCycles(false);
00624                 BUI.spinOption.setSafety(true);
00625             }
00626             SpinOption.spinOptions.setApplyNeverClaim(false);
00627             SpinOption.spinOptions.setAcceptanceCycles(false);
00628             SpinOption.spinOptions.setSafety(true);
00629         }
00630         /*      int fromval = ((IntLit) ((Range) edu.ksu.cis.bandera.bir.Type.defaultRangeType).getFromVal()).getValue();
00631         int toval = ((IntLit) ((Range) edu.ksu.cis.bandera.bir.Type.defaultRangeType).getToVal()).getValue();
00632         int arlen = Builder.MAX_ARRAY_LENGTH;
00633         int colsize = Builder.COLLECTION_SIZE;*/
00634 
00635         String tempPath = getTempDir("birc");
00636         if (!BanderaUtil.mkdirs(tempPath)) {
00637             String errmsg = "***Can't make temporary directory to store model checker output!";
00638             System.out.println(errmsg);
00639             if (isGUI && isNotRoboto)
00640                 JOptionPane.showMessageDialog(null, errmsg, "Error", JOptionPane.ERROR_MESSAGE);
00641             else
00642                 execSummary.append(errmsg);
00643             return;
00644         }
00645 
00646         int fromval = BUI.sessions.getActiveSession().getBirMinIntRange();
00647         int toval = BUI.sessions.getActiveSession().getBirMaxIntRange();
00648         int arlen = BUI.sessions.getActiveSession().getBirMaxArrayLen();
00649         int colsize = BUI.sessions.getActiveSession().getBirMaxInstances();
00650         sys = edu.ksu.cis.bandera.birc.Builder.createTransSystem(getSootClassesForBIRC(), defaultName, arlen, colsize, fromval, toval, ps);
00651         if (isDumped || (isGUI && BUI.irOptions.getBIRCheckBox().isSelected())) {
00652             PrintWriter out = new PrintWriter(new FileWriter(birName));
00653             BirPrinter.print(sys, out);
00654             out.flush();
00655             out.close();
00656         }
00657         if (BUI.sessions.getActiveSession().isUseSPIN()) {
00658             edu.ksu.cis.bandera.bir.Type.booleanType = new edu.ksu.cis.bandera.bir.Bool(); // need to reset this
00659             runSpin();
00660         }
00661         if (BUI.sessions.getActiveSession().isUseSMV()) {
00662             edu.ksu.cis.bandera.bir.Type.booleanType = new edu.ksu.cis.bandera.bir.Bool(); // need to reset this
00663             runSMV();
00664         }
00665         if (BUI.sessions.getActiveSession().isUseDSPIN()) {
00666             edu.ksu.cis.bandera.bir.Type.booleanType = new edu.ksu.cis.bandera.bir.Bool(); // need to reset this
00667             runDSpin();
00668         }
00669     } catch (Throwable e) {
00670         e.printStackTrace();
00671         //Logger.keep();
00672         if (isGUI && isNotRoboto) {
00673             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "BIRC Phase --- Error", JOptionPane.ERROR_MESSAGE);
00674             updateTrees();
00675         } else
00676             execSummary.append("   BIRC phase error: " + e.getMessage() + "\n");
00677     } finally {
00678         defaultName = BUI.sessions.getActiveSession().getOutputName();
00679     }
00680 }
00681 /**
00682  * 
00683  */
00684 private boolean runBSL() {
00685     if (isDumped) { // generate report if dumped
00686         BSLReport bslReport = new BSLReport();
00687         bslReport.addAssertionsAndPredicates();
00688         rm.addReport("BSL", bslReport);
00689     }
00690     try {
00691         Property property = BUI.property;
00692         Hashtable assertionTable = new Hashtable();
00693         initAssertions();
00694         for (Iterator i = property.getActivatedAssertionProperties().iterator(); i.hasNext();) {
00695             AssertionProperty ap = (AssertionProperty) i.next();
00696             for (Iterator j = ap.getAssertions().iterator(); j.hasNext();) {
00697                 assertionTable.put(resolveAssertionName((Name) j.next()), new HashSet());
00698             }
00699         }
00700         int numOfQuantifiers = 0;
00701         HashSet v = new HashSet();
00702         TemporalLogicProperty tlp = property.getActivatedTemporalLogicProperty();
00703         if (tlp != null) {
00704             tlp.validate(property.getImportedType(), property.getImportedPackage(), property.getImportedAssertion(), property.getImportedAssertionSet(), property.getImportedPredicate(), property.getImportedPredicateSet());
00705             if (tlp.getExceptions().size() > 0) {
00706                 StringBuffer buffer = new StringBuffer();
00707                 for (Iterator i = tlp.getExceptions().iterator(); i.hasNext();) {
00708                     buffer.append(i.next() + "\n");
00709                 }
00710                 if (isGUI && isNotRoboto) {
00711                     JOptionPane.showMessageDialog(BUI.bui, buffer.toString(), "Error", JOptionPane.ERROR_MESSAGE);
00712                     BUI.isExecuting = false;
00713                 } else
00714                     execSummary.append("   Spec compilation failed!\n");
00715                 return false;
00716             }
00717             Hashtable qTable = tlp.getQuantifiersTable();
00718             numOfQuantifiers = qTable.size();
00719             for (Enumeration e = qTable.elements(); e.hasMoreElements();) {
00720                 v.add((QuantifiedVariable) e.nextElement());
00721             }
00722         }
00723         if ((assertionTable.size() > 0) || (numOfQuantifiers > 0)) {
00724             CompilationManager.setQuantifiers(tlp.getQuantifiedVariables());
00725             CompilationManager.setModifiedMethodTable(AssertionProcessor.process(assertionTable));
00726             isRecompiled = true;
00727             CompilationManager.compile();
00728             isCodeChanged = true;
00729             if (CompilationManager.getExceptions().size() > 0)
00730                 throw new Exception("Errors occured when compiling the program");
00731             SootClass mainClass = CompilationManager.getMainSootClass();
00732             for (Iterator i = CompilationManager.getQuantifiers().iterator(); i.hasNext();) {
00733                 QuantifiedVariable qv = (QuantifiedVariable) i.next();
00734                 String name = "quantification$" + qv.getName();
00735                 SootField sf = CompilationManager.getFieldForQuantifier(name);
00736                 mainClass.addField(sf);
00737                 SootClass sc = sf.getDeclaringClass(); // robbyjo's patch
00738                 quantifierSliceInterests.add(new SliceField(sc, sf)); // robbyjo's patch
00739                 // robbyjo's patch: Store class and field association
00740                 qList.add(new QuantifierClassPair(sc.getName(), name));
00741             }
00742             CompilationManager.setModifiedMethodTable(new Hashtable());
00743         }
00744 
00745         // Compile predicates to Grimp
00746         if (tlp != null) {
00747             StringBuffer sb = new StringBuffer();
00748             tlp.validate(property.getImportedType(), property.getImportedPackage(), property.getImportedAssertion(), property.getImportedAssertionSet(), property.getImportedPredicate(), property.getImportedPredicateSet());
00749             Hashtable pTable = tlp.getPredicatesTable();
00750             Hashtable pqTable = tlp.getPredicateQuantifierTable();
00751             Hashtable qphTable = new Hashtable();
00752             SootClass mainClass = CompilationManager.getMainSootClass();
00753             Jimple jimple = Jimple.v();
00754             HashSet visitedP = new HashSet();
00755             for (Enumeration e = pTable.keys(); e.hasMoreElements();) {
00756                 Object key = e.nextElement();
00757                 Predicate p = (Predicate) pTable.get(key);
00758                 if (p.getExceptions().size() > 0) {
00759                     if (visitedP.contains(p))
00760                         continue;
00761                     visitedP.add(p);
00762                     sb.append("In '" + p + "':\n");
00763                     for (Iterator i = p.getExceptions().iterator(); i.hasNext();) {
00764                         sb.append("* " + ((Exception) i.next()).getMessage() + "\n");
00765                     }
00766                     continue;
00767                 }
00768                 Vector qvs = (Vector) pqTable.get(key);
00769                 Value phThis = null;
00770                 Hashtable phParams = new Hashtable();
00771                 for (int i = 0; i < qvs.size(); i++) {
00772                     QuantifiedVariable q = (QuantifiedVariable) qvs.elementAt(i);
00773                     Value cph = null;
00774                     if (q != null) {
00775                         if (qphTable.get(q) == null) {
00776                             String name = "quantification$" + q.getName();
00777                             cph = jimple.newStaticFieldRef(mainClass.getField(name));
00778                             qphTable.put(q, cph);
00779                             placeHolders.add(cph);
00780                         } else {
00781                             cph = (Value) qphTable.get(q);
00782                         }
00783                         if ((i == 0) && (!p.isStatic())) {
00784                             phThis = cph;
00785                         } else {
00786                             phParams.put(p.isStatic() ? p.getParams().elementAt(i) : p.getParams().elementAt(i - 1), cph);
00787                         }
00788                     }
00789                 }
00790                 Value value = PredicateProcessor.process(phThis, phParams, p);
00791                 if (!(p instanceof ExpressionPredicate)) {
00792                     if (value instanceof LocationTestExpr) {
00793                         LocationTestExpr lte = (LocationTestExpr) value;
00794                         stmtsVector.add(lte.getStmts());
00795                     } else {
00796                         LocationTestExpr lte = (LocationTestExpr) ((LogicalAndExpr) value).getOp1();
00797                         stmtsVector.add(lte.getStmts());
00798                     }
00799                 }
00800                 predNodeGrimpTable.put(key, value);
00801                 predicates.add(p);
00802                 if (isDumped) // add compiled predicate to report if dumped
00803                      ((BSLReport) rm.getReport("BSL")).addCompiledPredicate(p, value);
00804             }
00805             String s = sb.toString();
00806             if (s.length() > 0)
00807                 throw new RuntimeException(s.substring(0, s.length() - 1));
00808         }
00809     } catch (Exception e) {
00810         CompilationManager.setModifiedMethodTable(new Hashtable());
00811         CompilationManager.setQuantifiers(new Vector());
00812         if (isGUI && isNotRoboto) {
00813             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "BSL Phase --- Error", JOptionPane.ERROR_MESSAGE);
00814             BUI.isExecuting = false;
00815             updateTrees();
00816         } else {
00817             execSummary.append("   Spec compilation failed: " + e.getMessage() + "\n");
00818         }
00819         return false;
00820     }
00821     if (isGUI)
00822         updateTrees();
00823     return true;
00824 }
00825 /**
00826  * 
00827  */
00828 private void runDSpin() {
00829     if (BUI.doChecker) {
00830         DSpinTrans spinTrans = DSpinTrans.translate(sys, DSpinOption.spinOptions);
00831         spinTrans.runSpin();
00832         JimpleTrace trace = Builder.interpretTrace(spinTrans.parseOutput());
00833         if (trace.isVerified()) {
00834             if (isGUI && isNotRoboto)
00835                 JOptionPane.showMessageDialog(BUI.bui, "Verified", "Verification Phase", JOptionPane.INFORMATION_MESSAGE);
00836             else
00837                 execSummary.append("   DSpin OK, verified\n");
00838         } else {
00839             //dumpJimpleTrace(trace);
00840             if (isGUI && isNotRoboto) {
00841                 CounterExample ce = new CounterExample(new BIRCTraceManager(trace, typeTable));
00842                 ce.pack();
00843                 ce.setVisible(true);
00844             } else
00845                 execSummary.append("   DSpin OK, has a counter example\n");
00846     }
00847 }
00848 }
00849 /**
00850  * 
00851  */
00852 private boolean runJJJC() {
00853     try {
00854         isCodeChanged = false;
00855         isRecompiled = true;
00856         CompilationManager.compile();
00857         if (CompilationManager.getExceptions().size() > 0)
00858             throw new Exception("Errors occured when compiling the program");
00859     } catch (Throwable e) {
00860         if (isGUI && isNotRoboto) {
00861             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "JJJC Phase --- Error", JOptionPane.ERROR_MESSAGE);
00862             BUI.isExecuting = false;
00863             updateTrees();
00864         } else
00865             execSummary.append("   JJJC failed: " + CompilationManager.getExceptions() + "\n");
00866         return false;
00867     }
00868     if (isGUI) {
00869         updateTrees();
00870     }
00871     return true;
00872 }
00873 /**
00874  * Run the JPF, do the necessary preprocessing (precompiling and process the predicates)
00875  */
00876 private void runJPF() {
00877     // Save the current classpath and current directory
00878     String oldClasspath = System.getProperty("java.class.path");
00879     String oldUserDir = System.getProperty("user.dir");
00880     String classpath;
00881     String tempDir = ".";
00882     String ltlFormula = null;
00883     try {
00884         // Check whether recompilation is needed (esp. after slicing and abstraction)
00885         // If the source code is not compiled, then compile it anyway.
00886         // However, to avoid naming conflict, we just spit out the files into the
00887         // temporary directory temp$<session_name>/JPF
00888 
00889         // Then, we set our working directory and class path accordingly
00890         if (isCompilationNeeded()) {
00891             tempDir = generateJava("JPF");
00892             if (tempDir.equals("")) {
00893                 throw new Exception("Error in dumping Java files for JPF");
00894             }
00895             System.setProperty("user.dir", tempDir);
00896             classpath = tempDir + File.pathSeparator +  Preferences.getJPFHomeDir() + File.pathSeparator + Preferences.getBanderaHomeDir() + File.pathSeparator + Preferences.getAbstractionPath();
00897             BanderaUtil.runJavac(classpath, tempDir + File.separator + new Name(CompilationManager.getMainSootClass().getName()).getLastIdentifier() + ".java");
00898             System.setProperty("java.class.path", classpath);
00899         } else {
00900             System.setProperty("user.dir", tempDir);
00901             classpath = CompilationManager.getClasspath();
00902             System.setProperty("java.class.path", classpath);
00903         }
00904         //System.out.println(JPFOption.jpfOption.getOptions());
00905 
00906         // If we don't do checking, just quit. We only need the decompiler stuff
00907         // to work for debugging...
00908         if (!BUI.doChecker) return;
00909 
00910         // Do we have temporal properties to check?
00911         TemporalLogicProperty tlp = BUI.property.getActivatedTemporalLogicProperty();
00912         if (tlp != null) // Yes.
00913         {
00914             // So, compile the temporal properties and get the LTL formula
00915             JPFLTLCompiler comp = new JPFLTLCompiler(tempDir, tlp, qList);
00916             comp.compile();
00917             ltlFormula = comp.getFormula("LTL");
00918             System.out.println("JPF LTL Formula = " + ltlFormula);
00919         }
00920 
00921         System.out.println("Invoking JPF with classpath: " + System.getProperty("java.class.path"));
00922         // Fetch the option from the current active session and add -bandera to it
00923         String opt = "-bandera " + ((isGUI) ? BUI.jpfOption.getOptions() : BUI.sessions.getActiveSession().getJpfOptions());
00924 
00925         StringTokenizer t = new StringTokenizer(opt, " ");
00926         int maxOption = t.countTokens() + 1;
00927 
00928         // Make sure we have enough space if we have an LTL formula from specification
00929         if (ltlFormula != null) maxOption += 2;
00930         String[] options = new String[maxOption];
00931 
00932         // Place all options into the string array (to pass it into JPF)
00933         int i = 0;
00934         while (t.hasMoreTokens()) {
00935             options[i++] = t.nextToken();
00936         }
00937 
00938         // Then inject our LTL switch if we have the LTL formula
00939         if (ltlFormula != null)
00940         {
00941             options[i++] = "-ltl";
00942             options[i++] = ltlFormula;
00943         }
00944 
00945         // Supply the class file name to check (without the .class extension)
00946         options[i] = CompilationManager.getMainSootClass().getName();
00947 
00948         // If it is under GUI mode, display JPF logo
00949         if (isGUI) BUI.bui.getJPFLabel().setIcon(IconLibrary.jpfSelectedIcon);
00950 
00951         // Off we go! Invoke JPF
00952         gov.nasa.arc.ase.jpf.jvm.Main.main(options);
00953 
00954         // Pick up the result from the current Virtual Machine
00955         iVirtualMachine vm = Engine.getJPF().vm;
00956 
00957         if (Engine.getJPF().search.hasFailed()) { // Uh oh, something's wrong...
00958             ((JPFOptions) Engine.options).debug = true;
00959             if (isGUI && isNotRoboto) {
00960                 // Display counter example if we're in GUI mode
00961                 CounterExample ce = new CounterExample(new JPFTraceManager(vm, typeTable)); 
00962                 ce.pack();
00963                 ce.setVisible(true);
00964             } else
00965                 execSummary.append("   JPF OK, has a counter example\n");
00966         } else {
00967             // Otherwise: we just say: JPF runs happily. But if JPF complains, we don't know (yet).
00968             if (isGUI && isNotRoboto)
00969                 JOptionPane.showMessageDialog(BUI.bui, "Verified", "Verification Phase", JOptionPane.INFORMATION_MESSAGE);
00970             else
00971                 execSummary.append("   JPF OK, verified\n");
00972         }
00973     } catch (Exception e) {
00974         // Something wrong in the process and log 'em
00975         if (isGUI && isNotRoboto) {
00976             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "Verification Phase --- Error", JOptionPane.ERROR_MESSAGE);
00977             BUI.isExecuting = false;
00978             updateTrees();
00979         } else
00980             execSummary.append("   JPF failed: " + e.getMessage() + "\n");
00981         //Logger.keep();
00982     }
00983     // Restore the old values
00984     System.setProperty("java.class.path", oldClasspath);
00985 //  System.setProperty("user.dir", oldUserDir);   // Won't work! Bugg!!
00986 }
00987 /**
00988  * 
00989  */
00990 private boolean runSLABS() {
00991     if (isDumped) { // generate report if dumped
00992         SLABSReport slabsReport = new SLABSReport();
00993         rm.addReport("SLABS", slabsReport);
00994     }
00995     try {
00996         isCodeChanged = true;
00997         Session session = BUI.sessions.getActiveSession();
00998         TypeInference ti = new TypeInference();
00999         typeTable = ti.type(CompilationManager.getSootClassManager(), options);
01000         Vector v = new Vector();
01001         for (Enumeration e = CompilationManager.getCompiledClasses().elements(); e.hasMoreElements();) {
01002             v.add(e.nextElement());
01003         }
01004         if (isGUI)
01005             BUI.typeGUI.setInferredTypes(typeTable);
01006         if (isDumped) // add type info to the report if dumped
01007              ((SLABSReport) rm.getReport("SLABS")).setTypeTable(typeTable);
01008         new SLABS(CompilationManager.getAnnotationManager(), typeTable, ti.getInterfaceMethodMethod()).abstractClasses(v);
01009         return true;
01010     } catch (Exception e) {
01011         if (isGUI && isNotRoboto) {
01012              e.printStackTrace();
01013             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "SLABS Phase --- Error", JOptionPane.ERROR_MESSAGE);
01014             BUI.isExecuting = false;
01015             updateTrees();
01016         } else
01017             execSummary.append("   SLABS failed: " + e.getMessage() + "\n");
01018         return false;
01019     }
01020 }
01021 /**
01022  * 
01023  */
01024 private boolean runSlicer() {
01025     try {
01026         SootClass[] sootClasses = new SootClass[CompilationManager.getCompiledClasses().size()];
01027         int i = 0;
01028         for (Enumeration e = CompilationManager.getCompiledClasses().elements(); e.hasMoreElements(); i++) {
01029             sootClasses[i] = (SootClass) e.nextElement();
01030         }
01031         Vector v = (Vector) AssertionSliceInterestCollector.collect(new Vector());
01032         v.addAll(PredicateSliceInterestCollector.collect(predicates));
01033         v.addAll(quantifierSliceInterests);
01034         Slicer slicer = new Slicer(sootClasses, v, CompilationManager.getAnnotationManager());
01035         slicer.run();
01036         v = new Vector();
01037         SootClass[] result = slicer.result();
01038         for (i = 0; i < result.length; i++) {
01039             v.add(result[i]);
01040         }
01041         isCodeChanged = true;
01042         Hashtable table = CompilationManager.getCompiledClasses();
01043         Vector removed = new Vector();
01044         for (Enumeration e = table.keys(); e.hasMoreElements();) {
01045             Object key = e.nextElement();
01046             Object value = table.get(key);
01047             if (!v.contains(value))
01048                 removed.add(key);
01049         }
01050         for (Enumeration e = removed.elements(); e.hasMoreElements();) {
01051             table.remove(e.nextElement());
01052         }
01053     } catch (Exception e) {
01054         if (isGUI && isNotRoboto) {
01055             JOptionPane.showMessageDialog(BUI.bui, e.getMessage(), "Slicer Phase --- Error", JOptionPane.ERROR_MESSAGE);
01056             BUI.isExecuting = false;
01057             updateTrees();
01058         } else
01059             execSummary.append("   Slicer failed: " + e.getMessage() + "\n");
01060         return false;
01061     }
01062     if (isGUI) {
01063         updateTrees();
01064     }
01065     return true;
01066 }
01067 /**
01068  * 
01069  */
01070 private void runSMV() {
01071     if (BUI.doChecker) {
01072         SmvOptions options = new SmvOptions();
01073         options.setSafety(true);
01074         options.setInterleaving(true);
01075         options.setProperty(false);
01076         SmvTrans trans = SmvTrans.translate(sys, options);
01077         if (isGUI)
01078             BUI.bui.getNuSMVLabel().setIcon(IconLibrary.smvSelectedIcon);
01079         trans.runSmv();
01080         JimpleTrace trace = Builder.interpretTrace(trans.parseOutput());
01081         if (trace.isVerified()) {
01082             if (isGUI && isNotRoboto)
01083                 JOptionPane.showMessageDialog(BUI.bui, "Verified", "Verification Phase", JOptionPane.INFORMATION_MESSAGE);
01084             else
01085                 execSummary.append("   SMV OK, verified\n");
01086         } else
01087             if (trace.isLimitViolation()) {
01088                 if (isGUI && isNotRoboto)
01089                     JOptionPane.showMessageDialog(BUI.bui, "Resource Limit Exceeded : " + trace.getTrapName(), "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01090                 else
01091                     execSummary.append("   SMV OK, limit exceeded\n");
01092             } else
01093                 if (!trace.isComplete()) {
01094                     if (isGUI && isNotRoboto)
01095                         JOptionPane.showMessageDialog(BUI.bui, "Checker Did Not Complete", "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01096                     else
01097                         execSummary.append("   SMV FAILED, not complete\n");
01098                 } else {
01099                     //dumpJimpleTrace(trace);
01100                     if (isGUI && isNotRoboto) {
01101                         CounterExample ce = new CounterExample(new BIRCTraceManager(trace, typeTable));
01102                         ce.pack();
01103                         ce.setVisible(true);
01104                     } else
01105                         execSummary.append("   SMV OK, has a counter example\n");
01106     }
01107 }
01108 }
01109 /**
01110  * 
01111  */
01112 private void runSpin() {
01113     if (BUI.doChecker) {
01114         String tempPath = getTempDir("birc");
01115         SpinTrans spinTrans = SpinTrans.translate(sys, SpinOption.spinOptions, tempPath);
01116         if (isGUI)
01117             BUI.bui.getSpinLabel().setIcon(IconLibrary.spinSelectedIcon);
01118         spinTrans.runSpin();
01119         JimpleTrace trace = Builder.interpretTrace(spinTrans.parseOutput());
01120         if (trace.isVerified()) {
01121             if (isGUI && isNotRoboto)
01122                 JOptionPane.showMessageDialog(BUI.bui, "Verified", "Verification Phase", JOptionPane.INFORMATION_MESSAGE);
01123             else
01124                 execSummary.append("   SPIN OK, verified\n");
01125         } else
01126             if (trace.isOutOfMemory()) {
01127                 if (isGUI && isNotRoboto)
01128                     JOptionPane.showMessageDialog(BUI.bui, "Out of Memory : modify spin options", "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01129                 else
01130                     execSummary.append("   SPIN FAILED, out of memory\n");
01131             } else
01132                 if (trace.isVectorExceeded()) {
01133                     if (isGUI && isNotRoboto)
01134                         JOptionPane.showMessageDialog(BUI.bui, "State Vector Width Exceeded : modify spin options", "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01135                     else
01136                         execSummary.append("   SPIN FAILED, vector width exceeded\n");
01137                 } else
01138                     if (trace.isDepthExceeded()) {
01139                         if (isGUI && isNotRoboto)
01140                             JOptionPane.showMessageDialog(BUI.bui, "Depth Limit Exceeded : modify spin options", "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01141                         else
01142                             execSummary.append("   SPIN FAILED, depth limit exceeded\n");
01143                     } else
01144                         if (trace.isLimitViolation()) {
01145                             if (isGUI & isNotRoboto)
01146                                 JOptionPane.showMessageDialog(BUI.bui, "Resource Limit Exceeded : " + trace.getTrapName(), "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01147                             else
01148                                 execSummary.append("   SPIN OK, limit exceeded\n");
01149                         } else
01150                             if (!trace.isComplete()) {
01151                                 if (isGUI && isNotRoboto)
01152                                     JOptionPane.showMessageDialog(BUI.bui, "Checker Did Not Complete", "Verification Phase Error", JOptionPane.INFORMATION_MESSAGE);
01153                                 else
01154                                     execSummary.append("   SPIN FAILED, not complete\n");
01155                             } else {
01156                                 //dumpJimpleTrace(trace);
01157                                 if (isGUI && isNotRoboto) {
01158                                     CounterExample ce = new CounterExample(new BIRCTraceManager(trace, typeTable));
01159                                     ce.pack();
01160                                     ce.setVisible(true);
01161                                 } else
01162                                     execSummary.append("   SPIN OK, has a counter example\n");
01163     }
01164 }
01165 }
01166 /**
01167  * 
01168  */
01169 private void updateTrees() {
01170     if (isGUI) {
01171         BUI.sessionPane.updateLeftTree();
01172         BUI.predicateBrowser.updateTree();
01173         BUI.assertionBrowser.updateTree();
01174     }
01175 }
01176 /**
01177  * 
01178  */
01179 private void writeReport() {
01180     if (!BanderaUtil.mkdirs(getTempDir("report"))) {
01181         String errmsg = "***Can't make temporary directory for dumping report!";
01182         System.out.println(errmsg);
01183         if (isGUI && isNotRoboto)
01184             JOptionPane.showMessageDialog(null, errmsg, "Error", JOptionPane.ERROR_MESSAGE);
01185         else
01186             execSummary.append(errmsg);
01187         return;
01188     }
01189     for (Enumeration e = rm.getReportTable().elements(); e.hasMoreElements();) {
01190         Report r = (Report) e.nextElement();
01191         String path = getTempDir("report") + File.separator + r.getFilename();
01192         try {
01193             PrintWriter pw = new PrintWriter(new FileWriter(path));
01194             System.out.println("Writing " + path);
01195             pw.print(r.getTextRepresentation());
01196             pw.close();
01197         } catch (IOException ioe) {
01198             System.out.println("Error writing " + path);
01199         }
01200     }
01201     if (genReport) {
01202         String expectedDir = expectedResultPath + File.separator + "temp$" + BUI.sessions.getActiveSession().getName();
01203         String resultDir = "temp$" + BUI.sessions.getActiveSession().getName();
01204         String htmlPath = resultDir + File.separator + "index.html";
01205         HTMLReportGenerator.generateSessionSummary(htmlPath, BUI.sessions.getActiveSession(), expectedDir, resultDir);
01206     }
01207 }
01208 }