Commit 537186b9 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Implement subtype predicate parsing. 

The subtype given for variables are now properly parsed into the entire system.
Currently they are not actually used when generating the checker statements.
The expressions are fully parsed expressions, ready for output however.

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

Matlab2SMT/src/main/java/ca/mcmaster/cas/tabularexpressiontoolbox/expression/VariableType.java

+10 −0
Original line number Diff line number Diff line
@@ -25,4 +25,14 @@ public abstract class VariableType implements VariableTypeMarker { 
    public boolean isMarkerFor(VariableType m_type) {

        return this.equals(m_type);

    }



    public Expression subtypePredicate() {

        return m_subtypePredicate;

    }



    public void setSubtypePredicate(Expression subtypePredicate) {

        m_subtypePredicate = subtypePredicate;

    }



    private Expression m_subtypePredicate;

}

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

+42 −0
Original line number Diff line number Diff line
@@ -5,6 +5,7 @@ 
package ca.mcmaster.cas.tabularexpressiontoolbox.parsers;



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

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

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

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

import ca.mcmaster.cas.tabularexpressiontoolbox.expression.Variable;
@@ -19,6 +20,7 @@ import java.util.Map; 
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.VariableType;

import org.antlr.v4.runtime.ANTLRInputStream;

import org.antlr.v4.runtime.CommonTokenStream;

import org.antlr.v4.runtime.misc.NotNull;

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

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

import org.antlr.v4.runtime.tree.TerminalNode;
@@ -62,6 +64,7 @@ final public class VariableParser { 
    private static class VariablesParserToVariables extends VariableParserParserBaseListener {

        private String currentName;

        private VariableType currentType;

        private limitingExpressionData currentLimitingExpression;



        @Override

        public void enterVar(VarContext ctx) {
@@ -83,6 +86,17 @@ final public class VariableParser { 
            currentType = new BooleanVariableType();

        }



        @Override

        public void enterSubtype_var(@NotNull VariableParserParser.Subtype_varContext ctx) {

            currentLimitingExpression = new limitingExpressionData();

            currentLimitingExpression.variableName = ctx.ID().getText();

        }



        @Override

        public void enterPvs_expr(@NotNull VariableParserParser.Pvs_exprContext ctx) {

            currentLimitingExpression.expression = ctx.PVS_EXPR().getText();

        }



        @Override

        public void enterFixed_type(Fixed_typeContext ctx) {

            boolean signed = (ctx.NAT(0).getText().equals("0"))?false:true;
@@ -98,10 +112,38 @@ final public class VariableParser { 
        @Override

        public void exitVar(VarContext ctx) {

            m_variables.put(currentName, new Variable(currentName, currentType));

            if (currentLimitingExpression != null) {

                m_variableLimitingExpressions.put(currentName, currentLimitingExpression);

            }

            currentName = null;

            currentType = null;

            currentLimitingExpression = null;

        }



        @Override

        public void exitVarlist(@NotNull VariableParserParser.VarlistContext ctx) {

            for(Map.Entry<String, limitingExpressionData> limitingExpression : m_variableLimitingExpressions.entrySet()) {

                String subtypeVar = limitingExpression.getValue().variableName;

                String subtypeExpression = limitingExpression.getValue().expression;

                if (m_variables.containsKey(limitingExpression.getValue().variableName)) {

                    throw new IllegalStateException("Reused variable name for subtype declaration!");

                }

                // Get the variable we are working on, and use it for the variable used in the subtype expression.  This

                // effectively means the expression can just be emitted into the verification system to limit it.

                m_variables.put(subtypeVar, m_variables.get(limitingExpression.getKey()));



                m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(m_variables, subtypeExpression));



                // Undo the variables hack, to avoid having unused variables bleed into the verification scripts!

                m_variables.remove(subtypeVar);

            }

        }



        public Map<String, Variable>  m_variables = new HashMap<String, Variable>();

        private static class limitingExpressionData {

            public String expression;

            public String variableName;

        }

        private Map<String, limitingExpressionData> m_variableLimitingExpressions = new HashMap<String, limitingExpressionData>();

    }

}

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

+28 −0
Original line number Diff line number Diff line
@@ -10,7 +10,10 @@ import ca.mcmaster.cas.tabularexpressiontoolbox.expression.CheckerGenerator; 
import ca.mcmaster.cas.tabularexpressiontoolbox.expression.FixedPointVariableType;

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

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

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

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



import static org.hamcrest.CoreMatchers.*;

import static org.junit.Assert.*;



import org.junit.Test;
@@ -97,6 +100,31 @@ public class VariableParserTest { 
            assertEquals("b:REAL;\na:BITVECTOR(16);\n", generator.GenerateVariablesDeclaration(vars));

        }

    }

    @Test

    public void testSubtypeTypeExtraction() {

        Map<String, Variable> vars = VariableParser.parseVariables("d:{y|c OR y > 5},a,b:{x:real|x>5},c:bool,z:{x:bool|x /= c}");

        assertThat(vars.size(), is(5));



        assertThat(vars.get("d").name(), is("d"));

        assertThat(vars.get("d").type(), is((VariableType) new RealVariableType()));

        assertThat(vars.get("d").type().subtypePredicate().toString(), is("(c BooleanOr (d GreaterThen 5))"));



        assertThat(vars.get("a").name(), is("a"));

        assertThat(vars.get("a").type(), is((VariableType) new RealVariableType()));

        assertThat(vars.get("a").type().subtypePredicate(), is((Object)null));



        assertThat(vars.get("b").name(), is("b"));

        assertThat(vars.get("b").type(), is((VariableType) new RealVariableType()));

        assertThat(vars.get("b").type().subtypePredicate().toString(), is("(b GreaterThen 5)"));



        assertThat(vars.get("c").name(), is("c"));

        assertThat(vars.get("c").type(), is((VariableType) new BooleanVariableType()));

        assertThat(vars.get("c").type().subtypePredicate(), is((Object)null));



        assertThat(vars.get("z").name(), is("z"));

        assertThat(vars.get("z").type(), is((VariableType) new BooleanVariableType()));

        assertThat(vars.get("z").type().subtypePredicate().toString(), is("(z NotEquals c)"));

    }



    CheckerGenerator generator = new CVC3Generator();

}