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

Rename VariableType to Type. 

With the upcoming changes to VariableType, it is really no longer tied to
variables at all.  Thus rename to Type to better represent its role.
parent f340dd27

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

+15 −15
Original line number Diff line number Diff line
@@ -99,15 +99,15 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
        throw new RuntimeException("Should never happen!");

    }



    public static String ConvertToOutputOp(BinaryOperation op, VariableType type) {

    public static String ConvertToOutputOp(BinaryOperation op, Type type) {

        switch (OpTypeForVariableType(op, type)) {

            case Function:

                String func = GetSignedFixedPointFunctionFor(op);

                if (!((FixedPointVariableType) type).isSigned()) {

                if (!((FixedPointType) type).isSigned()) {

                    func = GetUnsignedFixedPointFunctionFor(op);

                }

                if (op == BinaryOperation.Addition || op == BinaryOperation.Minus || op == BinaryOperation.Multiplication) {

                    FixedPointVariableType typeF = (FixedPointVariableType) type;

                    FixedPointType typeF = (FixedPointType) type;

                    return func + typeF.digits() + ",";

                } else {

                    return func;
@@ -119,8 +119,8 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
        }

    }



    private static OperationType OpTypeForVariableType(BinaryOperation op, VariableType type) {

        if (type instanceof FixedPointVariableType && op != BinaryOperation.Equals && op != BinaryOperation.NotEquals) {

    private static OperationType OpTypeForVariableType(BinaryOperation op, Type type) {

        if (type instanceof FixedPointType && op != BinaryOperation.Equals && op != BinaryOperation.NotEquals) {

            if (op == BinaryOperation.Exponentiation) {

                throw new IllegalArgumentException("Cannot generate exponential functions in fixed point!");

            }
@@ -131,7 +131,7 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
    }



    @Override

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, Type usedType) {

        switch (CVC3ExpressionGenerator.OpTypeForVariableType(op, usedType)) {

            case CenterOp:

                return "(" + lhsExp + " " + CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")";
@@ -153,7 +153,7 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
    }



    @Override

    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {

    public String GenerateUnaryOperation(UnaryOperation op, String expression, Type usedType) {

        switch (CVC3ExpressionGenerator.OpTypeForVariableType(op, usedType)) {

            case PrefixOp:

                return "(" + CVC3ExpressionGenerator.ConvertToOutputOp(op, usedType) + " " + expression + ")";
@@ -164,19 +164,19 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
        }

    }



    private static OperationType OpTypeForVariableType(UnaryOperation op, VariableType usedType) {

        if (usedType instanceof FixedPointVariableType) {

    private static OperationType OpTypeForVariableType(UnaryOperation op, Type usedType) {

        if (usedType instanceof FixedPointType) {

            return OperationType.Function;

        }

        return OperationType.PrefixOp;

    }



    private static String ConvertToOutputOp(UnaryOperation op, VariableType usedType) {

    private static String ConvertToOutputOp(UnaryOperation op, Type usedType) {

        switch (op) {

            case Negation:

                return "NOT";

            case Minus:

                if (usedType instanceof FixedPointVariableType) {

                if (usedType instanceof FixedPointType) {

                    return "BVUMINUS";

                } else {

                    return "-";
@@ -186,8 +186,8 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
    }



    @Override

    public String GenerateLiteralValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {

    public String GenerateLiteralValue(String value, Type requestedType) {

        if (requestedType instanceof RealType) {

            if (value.contains(".")) {

                String[] fraction = value.split("\\.");
@@ -199,8 +199,8 @@ final public class CVC3ExpressionGenerator implements ExpressionGenerator { 
            } else {

                return value;

            }

        } else if (requestedType instanceof FixedPointVariableType) {

            FixedPointVariableType type = (FixedPointVariableType) requestedType;

        } else if (requestedType instanceof FixedPointType) {

            FixedPointType type = (FixedPointType) requestedType;

            BigDecimal decimal = new BigDecimal(value);

            decimal = decimal.multiply(BigDecimal.valueOf(1 << type.fractionPart()));

            BigInteger intOut = decimal.toBigIntegerExact();

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

+6 −6
Original line number Diff line number Diff line
@@ -29,9 +29,9 @@ 
 */

package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.EnumerationVariableType;

import ca.mcscert.jtet.expression.EnumerationType;

import ca.mcscert.jtet.expression.Type;

import ca.mcscert.jtet.expression.TypeDeclarationGenerator;

import ca.mcscert.jtet.expression.VariableType;



import java.util.Set;
@@ -41,12 +41,12 @@ import java.util.Set; 
 */

final public class CVC3TypeDeclarationGenerator implements TypeDeclarationGenerator {

    @Override

    public String GenerateTypeDeclaration(Set<VariableType> types) {

    public String GenerateTypeDeclaration(Set<Type> types) {

        StringBuilder ret = new StringBuilder();

        // Generate all the enumeration types.

        for(VariableType type : types) {

            if (type instanceof EnumerationVariableType) {

                EnumerationVariableType enumType = (EnumerationVariableType) type;

        for(Type type : types) {

            if (type instanceof EnumerationType) {

                EnumerationType enumType = (EnumerationType) type;

                ret.append("DATATYPE\n  ")

                        .append((enumType).name())

                        .append(" = ");

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

+8 −8
Original line number Diff line number Diff line
@@ -57,7 +57,7 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara 
        for(Variable var : variables) {

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

                ret.append("ASSERT ")

                   .append(var.type().subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanVariableType.Type))

                   .append(var.type().subtypePredicate().getCheckerOutput(CVC3ExpressionGenerator.Generator, BooleanType.Type))

                   .append(";\n");

            }

        }
@@ -68,15 +68,15 @@ final public class CVC3VariablesDeclarationGenerator implements VariablesDeclara 
    /**@deprecated

     * it is only public for unit tests, and will be made private eventually

     */

    public String GenerateVariableType(VariableType type) {

        if (type instanceof RealVariableType) {

    public String GenerateVariableType(Type type) {

        if (type instanceof RealType) {

            return "REAL";

        } else if (type instanceof FixedPointVariableType) {

            return "BITVECTOR(" + ((FixedPointVariableType) type).digits() + ")";

        } else if (type instanceof BooleanVariableType) {

        } else if (type instanceof FixedPointType) {

            return "BITVECTOR(" + ((FixedPointType) type).digits() + ")";

        } else if (type instanceof BooleanType) {

            return "BOOLEAN";

        } else if (type instanceof EnumerationVariableType) {

            return ((EnumerationVariableType) type).name();

        } else if (type instanceof EnumerationType) {

            return ((EnumerationType) type).name();

        } else {

            throw new IllegalArgumentException("CVC3 Doesn't handle this variable type (Class: " + type.getClass().getName() + ")");

        }

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

+5 −5
Original line number Diff line number Diff line
@@ -101,7 +101,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
        if (m_currentlyRunning) {

            outputCells();

        }

        m_parentCellsCVC3Code.addFirst(cellExpression.getCheckerOutput(m_CVC3ExpressionGenerator, BooleanVariableType.Type));

        m_parentCellsCVC3Code.addFirst(cellExpression.getCheckerOutput(m_CVC3ExpressionGenerator, BooleanType.Type));

        m_currentlyRunning = true;

    }
@@ -122,11 +122,11 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
    public void handleLeafCell(Expression inputCellExpression) {

        // First get the appropriate CVC3 code from matlab.  Capture generation for further processing.

        ExpressionGeneratorSpy spy = new ExpressionGeneratorSpy(m_CVC3ExpressionGenerator);

        String newCellCode = inputCellExpression.getCheckerOutput(spy, BooleanVariableType.Type);

        String newCellCode = inputCellExpression.getCheckerOutput(spy, BooleanType.Type);



        // Next, find all the fixed point expressions and handle them.

        for(ExpressionGeneratorSpy.SpiedBinaryOp op : spy.getBinaryOps()) {

            if (op.usedType instanceof FixedPointVariableType) {

            if (op.usedType instanceof FixedPointType) {

                generateOverflowTCC(op);

            }

        }
@@ -152,7 +152,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
            case NotEquals:

                return;

        }

        FixedPointVariableType type = (FixedPointVariableType) binaryOp.usedType;

        FixedPointType type = (FixedPointType) binaryOp.usedType;

        if (!type.isSigned() && binaryOp.op == BinaryOperation.Division) {

            return ; // Skip this generation.  Unsigned division requires no checks, since it never over/under flows.

        }
@@ -161,7 +161,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridBrea 
        m_output += "PUSH;\n";



        String query = null;

        if (((FixedPointVariableType) binaryOp.usedType).isSigned()) {

        if (((FixedPointType) binaryOp.usedType).isSigned()) {

            switch (binaryOp.op) {

                case Addition:

                    // Verify the sign bit doesn't change as appropriate.  Only on the sign bits being equal can an error occur, and only if the output sign differs.

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

+4 −4
Original line number Diff line number Diff line
@@ -78,12 +78,12 @@ final public class EventBExpressionGenerator implements ExpressionGenerator { 
    }



    @Override

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {

    public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, Type usedType) {

          return "(" + lhsExp + " " + EventBExpressionGenerator.ConvertToOutputOp(op) + " " + rhsExp + ")";

    }



    @Override

    public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {

    public String GenerateUnaryOperation(UnaryOperation op, String expression, Type usedType) {

          return "(" + EventBExpressionGenerator.ConvertToOutputOp(op) + " " + expression + ")";

    }
@@ -99,8 +99,8 @@ final public class EventBExpressionGenerator implements ExpressionGenerator { 
    }



    @Override

    public String GenerateLiteralValue(String value, VariableType requestedType) {

        if (requestedType instanceof RealVariableType) {

    public String GenerateLiteralValue(String value, Type requestedType) {

        if (requestedType instanceof RealType) {

            if (value.contains(".")) {

                String[] fraction = value.split("\\.");