Commit e099404a authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Implement a z3 runner. 

Add a CheckerRunner class with a single static method to run z3.  It uses
the smtlib generators, and the logic can be extended to other smtlib2 compliant
smt solvers.  It uses the copy of z3 in your path for now.

Note that it is very brittle, and if z3 has issue can potentially lock the
thread it is running on, as Java has no easy way to add timeouts to reads
on the stdout of z3.

git-svn-id: https://groke.mcmaster.ca/svn/grad/colin/branches/TableTool_javization@10663 57e6efec-57d4-0310-aeb1-a6c144bb1a8b
parent 6e9bbbd0

Matlab2SMT/src/main/java/ca/mcmaster/cas/smtlibchecker/CheckerRunner.java

0 → 100644
+203 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program 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 General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.smtlibchecker;



import ca.mcmaster.cas.matlab2smt.SMTLIBGenerator;

import ca.mcmaster.cas.matlab2smt.Variable;

import ca.mcmaster.cas.matlab2smt.VariableParser;

import ca.mcmaster.cas.tablularexpression.HierarchcialGridCheckerWalkerGenerator;

import ca.mcmaster.cas.tablularexpression.HierarchicalGrid;

import org.apache.commons.lang3.StringUtils;



import java.io.BufferedReader;

import java.io.IOException;

import java.io.InputStream;

import java.io.InputStreamReader;

import java.io.OutputStream;

import java.io.OutputStreamWriter;

import java.io.Reader;

import java.io.UnsupportedEncodingException;

import java.io.Writer;

import java.util.ArrayList;

import java.util.HashMap;

import java.util.List;

import java.util.Map;



/**

 *

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

final public class CheckerRunner {

    public static List<CheckerRunnerResult> RunZ3(HierarchicalGrid grid, VariableParser vars) {

        List<CheckerRunnerResult> ret = new ArrayList<CheckerRunnerResult>();



        // Get the queries

        HierarchicalGridSMTLIBGenerator queryGenerator = new HierarchicalGridSMTLIBGenerator(vars);

        HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, queryGenerator);



        // Start Z3

        ProcessBuilder pb;

        Process p;

        try {

            pb = new ProcessBuilder("z3", "-smt2", "-in");

            p = pb.start();

        } catch(IOException ex) {

            throw new RuntimeException("Failed to start Z3!", ex);

        }



        // Input/Output refer to the direction from Z3's pov.  So output is Z3's stdout.

        BufferedReader z3Output;

        Writer z3Input;

        try {

            // Sigh ... Java has horrible naming conversions here ...

            z3Output = new BufferedReader(new InputStreamReader(p.getInputStream(), "ISO-8859-1"));

            z3Input = new OutputStreamWriter(p.getOutputStream());

        } catch(UnsupportedEncodingException ex) {

            throw new RuntimeException("Failed to get ISO-8859-1 charset for talking to Z3!", ex);

        }



        StringBuilder GetValueRequestBuilder = new StringBuilder();

        GetValueRequestBuilder.append("(get-value (");

        for(Variable var:vars.getVarList()) {

            GetValueRequestBuilder.append(var.name()).append(' ');

        }

        GetValueRequestBuilder.append("))\n");

        String GetValueRequestString = GetValueRequestBuilder.toString();



        try {

            String VarDef = vars.getCheckerOutput(new SMTLIBGenerator());

            z3Input.write(VarDef);

            for(String query : queryGenerator.getFinalQueries()) {

                z3Input.write("(push 1)");

                z3Input.write(query);

                z3Input.write("(check-sat)\n");

                z3Input.flush();



                String res = z3Output.readLine();

                if(res.equals("sat")) { // Failed query.  Get a the result.

                    z3Input.write(GetValueRequestString);

                    z3Input.flush();



                    CheckerRunnerResult result = new CheckerRunnerResult();

                    result.Query = query;

                    result.SampleValues = parseSMTLIBOutput(z3Output);

                    ret.add(result);

                } else if(!res.equals("unsat")) {

                    // Something went wrong

                    throw new IllegalStateException("Z3 outputed something wrong (" + res + ")!");

                }



                z3Input.write("(pop 1)\r");

            }

        } catch(IOException ex) {

            throw new RuntimeException("Something bad happened ...", ex);

        } finally {

            try {

                z3Input.write("(exit)\n");

                z3Input.flush();



                p.destroy();

                z3Input.close();

                z3Output.close();

            } catch(Exception e) {

                // Don't care here, so just print it out.

                System.out.println(e);

            }

        }



        return ret;

    }



    private static Map<String, String> parseSMTLIBOutput(Reader reader) throws IOException {

        if(reader.markSupported() == false) {

            throw new IllegalArgumentException("Reader must support marks!");

        }

        Map<String, String> ret = new HashMap<String, String>();



        boolean done = false;

        StringBuilder varname = new StringBuilder(), varvalue = new StringBuilder();



        char nextChar = consumeWhitespaceAndReturnNextChar(reader);

        if(nextChar != '(') {

            throw new IllegalArgumentException("Bad input, want (, got " + nextChar + "!");

        }



        nextChar = consumeWhitespaceAndReturnNextChar(reader);

        while(nextChar == '(') {

            varname.setLength(0);

            varvalue.setLength(0);



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

            varname.append(nextChar);

            nextChar = getNextChar(reader);

            while(!isWhitespace(nextChar)) {

                varname.append(nextChar);

                nextChar = getNextChar(reader);

            }



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

            varvalue.append(nextChar);

            nextChar = getNextChar(reader);

            while(!isWhitespace(nextChar) && nextChar != ')') {

                varvalue.append(nextChar);

                nextChar = getNextChar(reader);

            }



            ret.put(varname.toString(), varvalue.toString());



            nextChar = consumeWhitespaceAndReturnNextChar(reader);

        }



        if(nextChar != ')') {

            throw new IllegalArgumentException("Bad input, want (, got " + nextChar + "!");

        }



        do {

            reader.mark(5);

            nextChar = getNextChar(reader);

        } while(isWhitespace(nextChar) && nextChar != '\n');

        if(!isWhitespace(nextChar)) {

            reader.reset();

        }



        return ret;

    }



    private static char getNextChar(Reader reader) throws IOException {

        char[] c = new char[1];

        reader.read(c);

        return c[0];

    }



    private static boolean isWhitespace(char toTest) {

        if(toTest == ' ' ||

                toTest == '\n' ||

                toTest == '\r' ||

                toTest == '\t') {

            return true;

        }

        return false;

    }



    private static char consumeWhitespaceAndReturnNextChar(Reader reader) throws IOException {

        char c = getNextChar(reader);

        while(isWhitespace(c)) {

            c = getNextChar(reader);

        }

        return c;

    }

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/smtlibchecker/CheckerRunnerResultTest.java

0 → 100644
+46 −0
Original line number Diff line number Diff line 
/*

 * Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>

 *

 * This program is free software: you can redistribute it and/or modify

 * it under the terms of the GNU General Public License as published by

 * the Free Software Foundation, either version 3 of the License, or

 * (at your option) any later version.

 *

 * This program 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 General Public License for more details.

 *

 * You should have received a copy of the GNU General Public License

 * along with this program.  If not, see <http://www.gnu.org/licenses/>.

 */

package ca.mcmaster.cas.smtlibchecker;



import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import java.util.HashMap;



import static org.junit.Assert.*;



/**

 * @author Matthew Dawson <matthew@mjdsystems.ca>

 */

@RunWith(JUnit4.class)

public class CheckerRunnerResultTest {

    @Test

    public void TestGenerateMatlabVariableDeclarations() {

        CheckerRunnerResult instance = new CheckerRunnerResult();



        instance.SampleValues = new HashMap<String, String>();

        instance.SampleValues.put("x", "5.0");

        instance.SampleValues.put("z", "STRCONST");



        try {

            assertEquals("x = 5.0;\nz = STRCONST;\n", instance.GenerateMatlabVariableDeclarations());

        } catch(AssertionError e) {

            assertEquals("z = STRCONST;\nx = 5.0;\n", instance.GenerateMatlabVariableDeclarations());

        }

    }

}