Commit 9f25430d authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add a simple PVS parser for use in subtyping. 

The subtypes given in tables are given in PVS syntax.  To use these in other
languages, the TET needs to parse PVS expressions.  Note that this parser
is very basic, and only handles the bare minimum needed.  It only handles
basic Math expressions, similar to Matlab.  It doesn't do /= yet, due to missing
support further down the stack.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.g4

0 → 100644
+102 −0
Original line number Diff line number Diff line 
grammar PVSSimpleParser;



/* This is a simple PVS syntax parser.  It is designed to be able to parser simple math statements from PVS, instead of

a full blown parser that could be used to re-implement PVS.  This file is roughly based on MatlabParser.g4, without all

the extra pieces from it.  It is also modified to make the associated pieces in Java simpler. */



//

// ===============================

//



// a precedence hierarchy for parsing expressions



// these are groups of operators that have equivalent precedences

g1: LOG_OR;

g2: LOG_AND;

g3: NEG;

g4: ( NEQ | EQ | GRTE | GRT | LSTE | LST );

g5: ( PLUS | MINUS );

g6: ( LEFTDIV | TIMES );

g7: MINUS;

g8: EXPONENTIATION;



// the hierarchy is defined from LOWEST to HIGHEST priority.



expression : e0;



e0	: e1 g1 e0 | e1; // Logic OR

e1	: e2 g2 e1 | e2; // Logc AND

e2	: g3 e3 | e3; // Logc NOT

e3	: e3 g4 e4 | e4; // Comparison

e4	: e4 g5 e5 | e5; // Addition/Subtraction

e5	: e5 g6 e6 | e6; // Multiplication/Division

e6	: g7 e7 | e7; // Unary Minus

e7	: e7 g8 e8 | e8; // note: in PVS, exponentiation is left-associative

e8	: unary_expression;



unary_expression

	: base_expression #BASE_EXPRESIION

	| LPAREN expression RPAREN # PARENS_EXPRESSION

	;



base_expression

	: id

	| literal_number

	;



literal_number

        : INT

        | FLOAT

        ;



id:	i1=ID;



//

// operators and assignments

//



LOG_OR	: 'OR';

LOG_AND	: 'AND';

LSTE	: '<=';

GRTE	: '>=';

NEQ	: '/=';



EQ	: '=';



NEG	:   'NOT';



LST	: '<';

GRT	: '>';





PLUS	: '+';

MINUS	: '-';

TIMES	: '*';

LEFTDIV	: '/';



EXPONENTIATION: '^';





LPAREN	: '(';

RPAREN	: ')';



ID	: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier.  Start with letter, then alpha numerical allowed.



INT	: '0'..'9'+ ;



FLOAT

	: ('0'..'9')+ '.' ('0'..'9')* EXPONENT?

	| '.' ('0'..'9')+ EXPONENT?

	| ('0'..'9')+ EXPONENT

	;



WS

	: ( ' '

        | '\t'

        | '\n'

        ) -> skip

	;



fragment

EXPONENT

	: ('e'|'E') ('+'|'-')? ('0'..'9')+ ;

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/PVSSimpleParser.java

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

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;



import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BinaryOperation;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionBinaryOperation;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionUnaryOperation;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionValue;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.ExpressionWithSubExpression;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.UnaryOperation;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E0Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E1Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E2Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E3Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E4Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E5Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E6Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E7Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.E8Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G1Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G2Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G3Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G4Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G5Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G6Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G7Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.G8Context;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.IdContext;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParserParser.Literal_numberContext;

import org.antlr.v4.runtime.ANTLRInputStream;

import org.antlr.v4.runtime.CommonTokenStream;

import org.antlr.v4.runtime.tree.ParseTree;

import org.antlr.v4.runtime.tree.ParseTreeWalker;



import java.util.ArrayDeque;

import java.util.Deque;

import java.util.Map;



/**

 *

 * @author matthew

 */

final public class PVSSimpleParser {



    private PVSSimpleParser() {

    }



    public static Expression parsePVSCode(Map<String, Variable> variableListing, String pvsCode) {

        // create a CharStream that reads from standard input

        ANTLRInputStream input = new ANTLRInputStream(pvsCode + "\n");



        // create a lexer that feeds off of input CharStream

        PVSSimpleParserLexer lexer = new PVSSimpleParserLexer(input);



        // create a buffer of tokens pulled from the lexer

        CommonTokenStream tokens = new CommonTokenStream(lexer);



        // create a parser that feeds off the tokens buffer

        PVSSimpleParserParser parser = new PVSSimpleParserParser(tokens);



        ParseTree tree = parser.expression();

        ParseTreeWalker walker = new ParseTreeWalker();

        PVSParserToExpressions listener = new PVSParserToExpressions(variableListing);

        walker.walk(listener, tree);



        return listener.m_rootExpression;

    }



    private static class PVSParserToExpressions extends PVSSimpleParserBaseListener implements ExpressionWithSubExpression {



        PVSParserToExpressions(Map<String, Variable> variableListing) {

            m_variableParser = variableListing;

            m_opStack.addFirst(new ExpressionStackContainer(0, this));

        }



        private void incrementLevel() {

            this.m_level++;

        }



        private void decrementLevel() {

            this.m_level--;

            if (!m_hiddenOpStack.isEmpty() && m_hiddenOpStack.peekFirst().level == m_level) {

                // We have a hidden op here.  The normal methods won't find it, so make use of it!

                HiddenOpStackContainer hiddenOp = m_hiddenOpStack.peekFirst();

                addExpressionBinaryOperation(new ExpressionBinaryOperation(null, hiddenOp.op, null));

                if (--hiddenOp.count == 0) {

                    m_hiddenOpStack.removeFirst();

                }

            }



            if (!m_opStack.isEmpty() && m_opStack.peekFirst().level > m_level) {

                m_opStack.removeFirst();

            }

        }



        private void enqueHiddenOp(BinaryOperation op, int count) {

            m_hiddenOpStack.addFirst(new HiddenOpStackContainer(m_level, op, count));

        }



        private void addExpressionValue(ExpressionValue expressionValue) {

            m_opStack.peekFirst().op.setSubExpression(expressionValue);

        }



        private void addExpressionBinaryOperation(ExpressionBinaryOperation op) {

            if (m_rootExpression == null) {

                throw new IllegalStateException("It should not be possible to have"

                        + "an op where the left hand side is a null expression!");

            } else {

                if (m_opStack.peekFirst().level >= m_level) { //This current op happens after the root expression op.  Pull it up.

                    op.setLHS((Expression) m_opStack.removeFirst().op);

                    m_opStack.peekFirst().op.setSubExpression(op);

                } else { //This op happens before.  Push it down the tree.

                    op.setLHS(m_opStack.peekFirst().op.getSubExpression());

                    m_opStack.peekFirst().op.setSubExpression(op);

                }

                m_opStack.addFirst(new ExpressionStackContainer(m_level, op));

            }

        }



        private void addPrefixUnaryOperation(ExpressionUnaryOperation op) {

        /* Unlike Binary operations, unary operations just always insert

         * themselves into the operation stack exactly where they appear.

         * The whole left hand side handling never happens, since there is no

         * left hand side.  So just put it in place.

         *

         * Also, an unary operation is allowed to deal with a null root expression,

         * since it doesn't use it!

         */

            m_opStack.peekFirst().op.setSubExpression(op);

            m_opStack.addFirst(new ExpressionStackContainer(m_level, op));

        }



        private static BinaryOperation getBinaryOpForSymbol(String text) {

            if (text.equals("+")) {

                return BinaryOperation.Addition;

            } else if (text.equals("-")) {

                return BinaryOperation.Minus;

            } else if (text.equals("*")) {

                return BinaryOperation.Multiplication;

            } else if (text.equals("/")) {

                return BinaryOperation.Division;

            } else if (text.equals(">")) {

                return BinaryOperation.GreaterThen;

            } else if (text.equals(">=")) {

                return BinaryOperation.GreaterThenEqual;

            } else if (text.equals("<")) {

                return BinaryOperation.LessThen;

            } else if (text.equals("<=")) {

                return BinaryOperation.LessThenEqual;

            } else if (text.equals("=")) {

                return BinaryOperation.Equals;

            } else if (text.equals("AND")) {

                return BinaryOperation.BooleanAnd;

            } else if (text.equals("OR")) {

                return BinaryOperation.BooleanOr;

            } else {

                throw new IllegalArgumentException("No such binary PVS operation defined (" + text + ")!");

            }

        }



        @Override

        public Expression getSubExpression() {

            return m_rootExpression;

        }



        @Override

        public void setSubExpression(Expression subExpression) {

            m_rootExpression = subExpression;

        }





        @Override

        public void enterE0(E0Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE1(E1Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE2(E2Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE3(E3Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE4(E4Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE5(E5Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE6(E6Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE7(E7Context ctx) {

            incrementLevel();

        }



        @Override

        public void enterE8(E8Context ctx) {

            incrementLevel();

        }



        @Override

        public void exitE0(E0Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE1(E1Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE2(E2Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE3(E3Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE4(E4Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE5(E5Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE6(E6Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE7(E7Context ctx) {

            decrementLevel();

        }



        @Override

        public void exitE8(E8Context ctx) {

            decrementLevel();

        }



        @Override

        public void enterG1(G1Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG2(G2Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG3(G3Context ctx) {

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation.

        }



        @Override

        public void enterG4(G4Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG5(G5Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG6(G6Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterG7(G7Context ctx) {

            addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus.

        }



        @Override

        public void enterG8(G8Context ctx) {

            addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null));

        }



        @Override

        public void enterLiteral_number(Literal_numberContext ctx) {

            addExpressionValue(new Literal(ctx.getText()));

        }



        @Override

        public void enterId(IdContext ctx) {

            addExpressionValue(m_variableParser.get(ctx.getText()));

        }



        public Expression m_rootExpression;

        private int m_level = 0;

        private Map<String, Variable> m_variableParser;



        private static class ExpressionStackContainer {



            public int level;

            public ExpressionWithSubExpression op;



            public ExpressionStackContainer(int level, ExpressionWithSubExpression op) {

                this.level = level;

                this.op = op;

            }

        }

        Deque<ExpressionStackContainer> m_opStack = new ArrayDeque<ExpressionStackContainer>();



        private static class HiddenOpStackContainer {



            public int level, count;

            public BinaryOperation op;



            public HiddenOpStackContainer(int level, BinaryOperation op, int count) {

                this.level = level;

                this.op = op;

                this.count = count;

            }

        }

        Deque<HiddenOpStackContainer> m_hiddenOpStack = new ArrayDeque<HiddenOpStackContainer>();

    }

}

Matlab2SMT/src/test/java/ca/mcmaster/cas/tabularexpressiontoolbox/parsers/test/PVSSimpleParserTest.java

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

 * To change this template, choose Tools | Templates

 * and open the template in the editor.

 */

package ca.mcmaster.cas.tabularexpressiontoolbox.parsers.test;



import ca.mcmaster.cas.tabularexpressiontoolbox.expression.BooleanVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CVC3Generator;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Expression;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Literal;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.RealVariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.SMTLIBGenerator;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.PVSSimpleParser;

import ca.mcmaster.cas.tabularexpressiontoolbox.parsers.VariableParser;

import org.junit.Test;

import org.junit.runner.RunWith;

import org.junit.runners.JUnit4;



import static org.junit.Assert.assertEquals;

import static org.junit.Assert.assertSame;



/**

 *

 * @author matthew

 */

@RunWith(JUnit4.class)

public class PVSSimpleParserTest {

    @Test

    public void testSimpleNumberParse() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "5\n");

        VariableType variableType = new RealVariableType();



        assertSame(Literal.class, expr.getClass());

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("5", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("5.0", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testSimpleRealVariableParse() {

        Expression expr = PVSSimpleParser.parsePVSCode(VariableParser.parseVariables("a"), "a\n");



        assertSame(Variable.class, expr.getClass());

        CheckerGenerator generator = new CVC3Generator();

        VariableType variableType = new RealVariableType();

        assertEquals("a", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("a", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testSimpleAdditionWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4+5\n");



        CheckerGenerator generator = new CVC3Generator();

        VariableType variableType = new RealVariableType();

        assertEquals("(4 + 5)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(+ 4.0 5.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testSimpleMultiplicationWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4*5\n");



        VariableType variableType = new RealVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(4 * 5)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(* 4.0 5.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testSimpleNegationWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "NOT 0\n");



        VariableType variableType = new RealVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(NOT 0)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(not 0.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testDoubleAdditionWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4+5+6\n");



        VariableType variableType = new RealVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("((4 + 5) + 6)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(+ (+ 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testMultiplyThenAddWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4*5+6\n");



        VariableType variableType = new RealVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("((4 * 5) + 6)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(+ (* 4.0 5.0) 6.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testAddThenMultiplyWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4+5*6\n");



        VariableType variableType = new RealVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(4 + (5 * 6))", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(+ 4.0 (* 5.0 6.0))", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testInsanseExpressionsWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "4*5+6*7\n");

        Expression expr2 = PVSSimpleParser.parsePVSCode(null, "4+5+6*7*8\n");



        CheckerGenerator cvc3generator = new CVC3Generator();

        CheckerGenerator smtlibgenerator = new SMTLIBGenerator();



        VariableType variableType = new RealVariableType();

        assertEquals("((4 * 5) + (6 * 7))", expr.getCheckerOutput(cvc3generator, variableType));

        assertEquals("(+ (* 4.0 5.0) (* 6.0 7.0))", expr.getCheckerOutput(smtlibgenerator, variableType));



        assertEquals("((4 + 5) + ((6 * 7) * 8))", expr2.getCheckerOutput(cvc3generator, variableType));

        assertEquals("(+ (+ 4.0 5.0) (* (* 6.0 7.0) 8.0))", expr2.getCheckerOutput(smtlibgenerator, variableType));

    }



    @Test

    public void testSimpleConditionalsWithLiterals() {

        Expression expr = PVSSimpleParser.parsePVSCode(null, "5 > 5\n");



        VariableType variableType = new BooleanVariableType();

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("(5 > 5)", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(> 5.0 5.0)", expr.getCheckerOutput(generator, variableType));

    }



    @Test

    public void testInsanseExpressionsWithLiteralsAndVariables() {

        Expression expr = PVSSimpleParser.parsePVSCode(VariableParser.parseVariables("x,z,y"), "z = 1 AND x = 0 AND y = 2");



        VariableType variableType = new BooleanVariableType();

        assertEquals(variableType, expr.actualOutputTypeForRequestedOutput(variableType));

        CheckerGenerator generator = new CVC3Generator();

        assertEquals("((z = 1) AND ((x = 0) AND (y = 2)))", expr.getCheckerOutput(generator, variableType));

        generator = new SMTLIBGenerator();

        assertEquals("(and (= z 1.0) (and (= x 0.0) (= y 2.0)))", expr.getCheckerOutput(generator, variableType));

    }

}