Commit 5745a2e8 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add a static Type or TypeMarker element to all VariableTypes. 

jTET needs a large amount of throw away instances of types or their marker
for its work.  Instead of creating a new instance each time, use a static
instance to avoid the work.  It also makes it more obvious when something is
temporary.
parent 0be5eefd

src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java

+2 −3
Original line number Diff line number Diff line
@@ -109,7 +109,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchcialGridChec 
        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType));

        m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type));

        m_currentlyRunning = true;

    }
@@ -129,7 +129,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchcialGridChec 
    @Override

    public void handleLeafCell(Cell cell) {

        // First get the appropriate CVC3 code from matlab.

        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType);

        String newCellCode = MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, BooleanVariableType.Type);



        // Next form the disjoint queries and add to the list.

        for(String otherCellCode : m_currentCompleteQueries) {
@@ -169,6 +169,5 @@ final public class HierarchicalGridCVC3Generator implements HierarchcialGridChec 


    // To fix properly.

    VariableCollection m_variableDefinitions;

    static BooleanVariableType m_booleanType = new BooleanVariableType();

    CVC3Generator m_CVC3Generator = new CVC3Generator();

}

src/main/java/ca/mcscert/jtet/eventbgenerator/HierarchicalGridEventBGenerator.java

+2 −3
Original line number Diff line number Diff line
@@ -101,7 +101,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchcialGridCh 


    @Override

    public void descendIntoGridFromCell(Cell cell) {

        m_parentCellsEventBCode.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, m_booleanType));

        m_parentCellsEventBCode.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, BooleanVariableType.Type));

    }



    @Override
@@ -121,7 +121,7 @@ final public class HierarchicalGridEventBGenerator implements HierarchcialGridCh 
    }



    public String handleCell(Cell cell) {

        return MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, m_booleanType);

        return MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_eventBGenerator, BooleanVariableType.Type);

    }



    @Override
@@ -136,6 +136,5 @@ final public class HierarchicalGridEventBGenerator implements HierarchcialGridCh 
    TwoDimensionalGrid m_outputGrid;

    VariableCollection m_variableDefinitions;

    Deque<String> m_parentCellsEventBCode = new ArrayDeque<String>();

    static BooleanVariableType m_booleanType = new BooleanVariableType();

    EventBGenerator m_eventBGenerator = new EventBGenerator();

}

src/main/java/ca/mcscert/jtet/expression/BinaryOperation.java

+5 −5
Original line number Diff line number Diff line
@@ -34,7 +34,7 @@ public enum BinaryOperation { 
        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == Implies || this == GreaterThen || this == GreaterThenEqual ||

                this == LessThen || this == LessThenEqual || this == Equals || this == NotEquals) {

            if (!outputType.equals(new BooleanVariableType())) {

            if (!outputType.equals(BooleanVariableType.Type)) {

                throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!");

            }

        }
@@ -50,10 +50,10 @@ public enum BinaryOperation { 
            case GreaterThenEqual:

            case LessThen:

            case LessThenEqual:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()});

                return Arrays.asList(new VariableTypeMarker[]{RealVariableType.Type, FixedPointVariableType.TypeMarker});

            case Equals:

            case NotEquals:

                return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker(), new EnumerationVariableType.Marker()});

                return Arrays.asList(new VariableTypeMarker[]{RealVariableType.Type, FixedPointVariableType.TypeMarker, EnumerationVariableType.TypeMarker});

        }

        return Arrays.asList(new VariableTypeMarker[]{outputType});

    }
@@ -61,7 +61,7 @@ public enum BinaryOperation { 
    public VariableType getOutputForInput(VariableType inputType) {

        // Boolean inputs only work with a boolean input!

        if (this == BooleanAnd || this == BooleanOr || this == Implies) {

            if (!inputType.equals(new BooleanVariableType())) {

            if (!inputType.equals(BooleanVariableType.Type)) {

                throw new IllegalArgumentException("Boolean operators require a boolean input type!");

            }

        }
@@ -74,7 +74,7 @@ public enum BinaryOperation { 
            case LessThenEqual:

            case Equals:

            case NotEquals:

                return new BooleanVariableType();

                return BooleanVariableType.Type;

        }

        return inputType;

    }

src/main/java/ca/mcscert/jtet/expression/BooleanVariableType.java

+1 −0
Original line number Diff line number Diff line
@@ -9,6 +9,7 @@ package ca.mcscert.jtet.expression; 
 * @author matthew

 */

public class BooleanVariableType extends VariableType {

    public final static BooleanVariableType Type = new BooleanVariableType();



    @Override

    public boolean equals(Object other) {

src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java

+1 −1
Original line number Diff line number Diff line
@@ -237,7 +237,7 @@ final public class CVC3Generator implements CheckerGenerator{ 
        for(Variable var : vars.values()) {

            if (var.type().subtypePredicate() != null) {

                ret.append("ASSERT ")

                   .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType()))

                   .append(var.type().subtypePredicate().getCheckerOutput(this, BooleanVariableType.Type))

                   .append(";\n");

            }

        }