---

JPFLTLCompiler.java

package edu.ksu.cis.bandera.specification;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 2001   Roby Joehanes (robbyjo@cis.ksu.edu)          *
 * All rights reserved.                                              *
 *                                                                   *
 * This work was done as a project in the SAnToS Laboratory,         *
 * Department of Computing and Information Sciences, Kansas State    *
 * University, USA (http://www.cis.ksu.edu/santos).                  *
 * It is understood that any modification not identified as such is  *
 * not covered by the preceding statement.                           *
 *                                                                   *
 * This work is free software; you can redistribute it and/or        *
 * modify it under the terms of the GNU Library General Public       *
 * License as published by the Free Software Foundation; either      *
 * version 2 of the License, or (at your option) any later version.  *
 *                                                                   *
 * This work is distributed in the hope that it will be useful,      *
 * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
 * Library General Public License for more details.                  *
 *                                                                   *
 * You should have received a copy of the GNU Library General Public *
 * License along with this toolkit; if not, write to the             *
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
 * Boston, MA  02111-1307, USA.                                      *
 *                                                                   *
 * Java is a trademark of Sun Microsystems, Inc.                     *
 *                                                                   *
 * To submit a bug report, send a comment, or get the latest news on *
 * this project and other SAnToS projects, please visit the web-site *
 *                http://www.cis.ksu.edu/santos                      *
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
/**
 * Visitor class to compile pattern for JPF.
 * Creation date: (8/10/01 6:12:38 PM)
 * @author: Roby Joehanes
 */
import java.util.*;
import java.lang.reflect.*;
import java.io.*;
import ca.mcgill.sable.soot.*;
import edu.ksu.cis.bandera.specification.analysis.*;
import edu.ksu.cis.bandera.specification.datastructure.*;
import edu.ksu.cis.bandera.specification.node.*;
import edu.ksu.cis.bandera.specification.pattern.*;
import edu.ksu.cis.bandera.specification.pattern.datastructure.*;
import edu.ksu.cis.bandera.specification.predicate.node.PPropositionDefinition;
import edu.ksu.cis.bandera.specification.predicate.datastructure.*;
import edu.ksu.cis.bandera.annotation.*;
import edu.ksu.cis.bandera.jext.*;
import edu.ksu.cis.bandera.jjjc.*;
import edu.ksu.cis.bandera.util.*;
import gov.nasa.arc.ase.jpf.tools.*;

public class JPFLTLCompiler extends DepthFirstAdapter {
    private String tempDir = ".";
    private TemporalLogicProperty tlp;
    private Hashtable ptab;
    private List qList;
    private Pattern pattern;
    private Iterator patternParamIterator;
    private String currentValue = null;
    private Hashtable patternNodeTable = new Hashtable();
    private Hashtable patternNameTable = new Hashtable();
    private boolean useConstraint;
/**
 * 
 * @param dir java.lang.String To denote output directory where JPF java predicate should be placed
 * @param tl edu.ksu.cis.bandera.specification.datastructure.TemporalLogicProperty The currently active temporal logic property
 * @param q java.util.List The list of quantified variables available.
 */
public JPFLTLCompiler(String dir, TemporalLogicProperty tl, List q)
{
    if (dir != null) tempDir = dir;
    if (tl == null) throw new RuntimeException("Temporal Logic Property may NOT be null!!");
    tlp = tl; qList = q;
}
public void caseABinaryExp(ABinaryExp node)
{
    node.getLeft().apply(this);
    String leftValue = currentValue;
    node.getRight().apply(this);
    String rightValue = currentValue;

    PBinOp binOp = node.getBinOp();
    if (binOp instanceof AAndBinOp) {
        currentValue = "(" + leftValue + " /\\ " + rightValue + ")";
    } else if (binOp instanceof AOrBinOp) {
        currentValue = "(" + leftValue + " \\/ " + rightValue + ")";
    } else {
        currentValue = "(" + leftValue + " -> " + rightValue + ")";
    }
}
public void caseAComplementExp(AComplementExp node)
{
    node.getExp().apply(this);
    if (currentValue == null) currentValue = "(0 != 0)";
    currentValue = "!"+currentValue;
}
public void caseAExpWord(AExpWord node) {
    node.getExp().apply(this);

    try {
        String id = (String) patternParamIterator.next();
        if (currentValue == null) currentValue = "(0 == 0)";
        patternNameTable.put(id, currentValue);
    } catch (Exception e)
    {
        System.out.println("WARNING: Unexpected pattern end!");
    }
}
public void caseAPredicateExp(APredicateExp node) {
    String temp = (String) patternNodeTable.get(node);

    if (temp == null)
    {
        System.out.println("WARNING: Pattern table of "+node+" yields null!");
        temp = "(0 == 0)"; // Injects bogus value
    }
    currentValue = temp;
}
public void compile()
{
    try {
    String classpath = System.getProperty("java.class.path");
    ptab = tlp.getPredicatesTable();
    pattern = PatternSaverLoader.getPattern(tlp.getPatternName(), tlp.getPatternScope());
    patternParamIterator = pattern.getParametersOccurenceOrder().iterator();
    LinkedList processedPreds = new LinkedList();

    // Iterate through the predicate table
    for (Enumeration e = ptab.keys(); e.hasMoreElements(); )
    {
        APredicateExp n = (APredicateExp) e.nextElement();

        // We get the expression and its string representation
        Predicate pred = (Predicate) ptab.get(n);

        // Get the declaring class
        String className = pred.getType().getFullyQualifiedName();
        Class theClass = null;
        try {
            theClass = FileClassLoader.load(className);
        } catch (Exception exx)
        {
            throw new RuntimeException("Can't find class " + className);
        }
        java.lang.reflect.Method theMethod = null;
        Annotation ann = pred.getAnnotation();

        // Does this predicate defined above a method?
        if (ann instanceof MethodDeclarationAnnotation)
        {
            theMethod = getMatchedMethod(theClass, ((MethodDeclarationAnnotation) ann).getSootMethod());
            if (theMethod == null) throw new RuntimeException("Method not found!");
        }
        // So, at this point we get the class and the corresponding method.

        // Resolve Java predicate naming
        PPropositionDefinition node = (PPropositionDefinition) pred.getNode();
        String predFileName = className;
        if (theMethod != null) predFileName += ("$"+theMethod.getName());
        predFileName += ("$" + node.getId().getText());

        // Is this predicate have been processed? (to avoid rewriting files)
        if (!processedPreds.contains(predFileName))
        {
            try {
                // Call JPF's BSL translator
                node.apply(new Translation(theClass, theMethod, tempDir));

                // Compile it
                BanderaUtil.runJavac(classpath, tempDir + File.separator + predFileName + ".java");

                // Mark this as already processed
                processedPreds.add(predFileName);
            } catch (Exception exx)
            {
                throw new RuntimeException("Error: " + exx.getMessage());
            }
        }

        // We then have to inject the correct parameter. (if any)
        if (n.getArgs() != null)
        {
            Hashtable qtab = tlp.getQuantifiersTable();
            String params = "";

            PArgs predArg;

            do {
                predArg = n.getArgs();

                String argId;
                if (predArg instanceof AArgsArgs)
                {
                    AArgsArgs multiArgs = (AArgsArgs) predArg;
                    predArg = multiArgs.getArgs();
                    argId = multiArgs.getId().toString();
                } else if (predArg instanceof AIdArgs)
                {
                    AIdArgs singleArg = (AIdArgs) predArg;
                    argId = singleArg.getId().toString();
                } else {
                    throw new RuntimeException("Unknown predicate parameter: "+predArg);
                }

                try {
                    QuantifiedVariable qv = (QuantifiedVariable) qtab.get(argId.trim());
                    //argId = qv.getType().toString()+".quantification$"+qv.getName();  // No!! We can't do this!
                    argId = getQualifiedNameForQv(qv.getName());  // Because the quantified variable may be placed in different class
                    // Warning: This translation assumes qv.getName() always returns simple name, not fully qualified one.
                } catch (Exception exx)
                {
                    exx.printStackTrace();
                    throw new RuntimeException("Parameter "+argId+" is not in the table:\n"+exx.getMessage());
                }
                if (!"".equals(params)) params = argId + ", "+ params; else params = argId;
            } while (predArg instanceof AArgsArgs);
        
            // Put the name subtitution inside the table
            System.out.println(predFileName + "(" + params + ") added");
            patternNodeTable.put(n, "\"" + predFileName + "(" + params + ")\"");
        } else
        {
            // If there are no parameters, then we simply put the predicate file name.
            patternNodeTable.put(n, "\"" + predFileName + "\"");
        }
    }

    // Up to this point, all .java files needed for JPF predicate
    // evaluation is setup and compiled. We have already had the pattern node symbols table.
    // Then we need to setup pattern name subtitution table: i.e. S->foo, P->baz
    // This can be achieved by visiting the predicate AST node (no other way)
    tlp.getNode().apply(this);

    // Then we need to check whether we have quantified variables
    if (qList != null && qList.size() > 0) // Yes, so we need to build "Select.java" appropriately
    {
        String lineSep = System.getProperty("line.separator");

        StringBuffer selectbuf = new StringBuffer();
        
        // Stamp out the preamble
        selectbuf.append("import gov.nasa.arc.ase.jpf.jvm.State;" + lineSep);
        selectbuf.append("import gov.nasa.arc.ase.jpf.jvm.Reference;" + lineSep);
        selectbuf.append("import gov.nasa.arc.ase.jpf.jvm.Thread;" + lineSep + lineSep);
        selectbuf.append("public class Selected {" + lineSep);
        selectbuf.append("     public static boolean evaluate(State state, Reference _this) {" + lineSep);
        selectbuf.append("          return _this != null");

/*      for (Iterator qi = qList.iterator(); qi.hasNext(); )
        {
            QuantifierClassPair qcp = (QuantifierClassPair) qi.next();
            selectbuf.append("state.getClass(\""+qcp.getClassName()+"\").getObjectField(\""+
                qcp.getFieldName()+"\") != null");
        
            if (qi.hasNext())
                selectbuf.append(" &&" + lineSep + "                      ");
        }
*/
        // Setup the epilogue
        selectbuf.append(";" + lineSep);
/*      selectbuf.append("          } catch (Exception e) {" + lineSep);
        selectbuf.append("               return false;" + lineSep);
        selectbuf.append("          }"+lineSep);
*/
        selectbuf.append("     }"+lineSep);
        selectbuf.append("}" + lineSep);

        // Prepare the file to dump the output
        String completeName = tempDir + File.separator + "Selected.java";
        System.out.println(completeName);
        
        try {
            PrintStream javaPrint = new PrintStream(new FileOutputStream(new File(completeName)));
            javaPrint.print(selectbuf.toString());
            javaPrint.close();

            // Then compile that file
            BanderaUtil.runJavac(classpath, completeName);
        } catch (IOException ex)
        {
            throw new RuntimeException("Cannot create file '" + completeName + "'");
        }
    }
    } catch (Exception suckers)
    {
        suckers.printStackTrace();
    }
}
public String getFormula(String mapping)
{
    if ("LTL".equalsIgnoreCase(mapping))
        return getLTLFormula();


    throw new RuntimeException("Mapping to " + mapping + " is currently not supported");
}
private String getLTLFormula()
{
    // Build our LTL formula
    String ltlFormula;
    
    try {
        ltlFormula = pattern.expandMapping("ltl", patternNameTable);
    } catch (Exception e)
    {
        throw new RuntimeException("Pattern mapping not supported!\nTable:\n"+patternNameTable);
    }

    // If we have quantified variables, we need to modify the
    // LTL Formula into the form:
    // (!Selected U (Selected && Predicate)) || [] (!Selected)
    if (qList != null && qList.size() > 0)
    {
        StringBuffer sel = new StringBuffer();
        for (Iterator qi = qList.iterator(); qi.hasNext(); )
        {
            QuantifierClassPair qcp = (QuantifierClassPair) qi.next();
            sel.append("Selected("+qcp.getClassName()+"."+qcp.getFieldName()+")");

            if (qi.hasNext()) sel.append(" && ");
        }
        String selected = "\"" + sel.toString() + "\"";
        ltlFormula = "(!"+selected+" U ("+selected+" /\\ (" + ltlFormula + "))) \\/ []!"+selected;
    }

    // Notice that JPF's LTL format is incompatible to ours. So convert it first
    int lastpos = 0;

    // convert the && -> /\
    do {
        lastpos = ltlFormula.indexOf("&&", lastpos);
        if (lastpos != -1)
            ltlFormula = ltlFormula.substring(0,lastpos) + "/\\" + ltlFormula.substring(lastpos+2);
    } while (lastpos != -1);

    lastpos = 0;

    // convert the || -> \/
    do {
        lastpos = ltlFormula.indexOf("||", lastpos);
        if (lastpos != -1)
            ltlFormula = ltlFormula.substring(0,lastpos) + "\\/" + ltlFormula.substring(lastpos+2);
    } while (lastpos != -1);

    // At this point, our LTL formula is ready to go!
    return ltlFormula;
}
private Method getMatchedMethod(Class theClass, SootMethod sm)
{
    Method[] methods = theClass.getDeclaredMethods();

    int max = methods.length;
    String name = sm.getName();
    if (name == null) throw new RuntimeException("Error! Bogus Soot Method!");

    for (int i = 0; i < max; i++)
    {
        Method m = methods[i];
        if (!name.equals(m.getName())) continue; // Not the same name
        Class[] params = m.getParameterTypes();
        int maxParams = params.length;
        if (sm.getParameterCount() != maxParams) continue; // Not the same number of params
        boolean found = true;

        for (int j = 0; j < maxParams; j++)
        {
            Class p1 = params[j];
            String sig = getTypeString(p1);
            Type t1 = sm.getParameterType(i);
            if (!sig.equals(t1.toString().trim()))
            {
                found = false; break;
            }
        }
        if (found) return m;
    }

    return null;
}
    private String getQualifiedNameForQv(String v)
    {
        for (Iterator i = qList.iterator(); i.hasNext(); )
        {
            QuantifierClassPair qcp = (QuantifierClassPair) i.next();
            if (qcp.getFieldName().equals("quantification$"+v))
                return qcp.toString();
        }
        return null;
    }
    private String getTypeString(Class c)
    {
        if (c.isArray()) return getTypeString(c.getComponentType())+"[]";
        return c.getName();
    }
}

---