diff --git a/.gitignore b/.gitignore index b1711bc18d455f3cba6d098e5158a235f84ec053..5d9916c315825d5df29fbd8dacb0847ae055babb 100644 --- a/.gitignore +++ b/.gitignore @@ -1,5 +1 @@ -/jTET/target/ -/jTET/gen/ -.idea/ -.pvscontext -/jTET/jtet.iml +/jTET/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar diff --git a/jTET/README b/jTET/README new file mode 100644 index 0000000000000000000000000000000000000000..80aa08fc05b2cc9f7cab9c124a1f2a0381e5affa --- /dev/null +++ b/jTET/README @@ -0,0 +1,4 @@ +This folder needs a copy of the jTET library, currently available at: +https://groke.mcmaster.ca/gitlab/tables/jtet/ +Place the target/jtet-1.0-SNAPSHOT-jar-with-dependencies.jar file in this +directory and the TET will automatically pick it up. diff --git a/jTET/pom.xml b/jTET/pom.xml deleted file mode 100644 index 79d1e2884c7d3d2a232d83a6cb6140157714fbce..0000000000000000000000000000000000000000 --- a/jTET/pom.xml +++ /dev/null @@ -1,121 +0,0 @@ - - 4.0.0 - - 3.0 - - - ca.mcscert.jtet - jtet - 1.0-SNAPSHOT - jar - - jTET - http://maven.apache.org - - - UTF-8 - - - - - junit - junit - 4.11 - test - - - org.antlr - antlr4-runtime - 4.2.2 - - - org.apache.commons - commons-lang3 - 3.3.2 - - - - - - - org.antlr - antlr4-maven-plugin - 4.2.2 - - src/main/java - - - - - antlr4 - - - - - - org.apache.maven.plugins - maven-compiler-plugin - 3.1 - - true - 1.6 - 1.6 - - - - org.apache.maven.plugins - maven-assembly-plugin - 2.4 - - - jar-with-dependencies - - - - - package - - single - - - - - - org.apache.maven.plugins - maven-clean-plugin - 2.5 - - - org.apache.maven.plugins - maven-deploy-plugin - 2.8.1 - - - org.apache.maven.plugins - maven-install-plugin - 2.5.1 - - - org.apache.maven.plugins - maven-jar-plugin - 2.4 - - - org.apache.maven.plugins - maven-resources-plugin - 2.6 - - - org.apache.maven.plugins - maven-site-plugin - 3.3 - - - org.apache.maven.plugins - maven-surefire-plugin - 2.17 - - - - diff --git a/jTET/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java b/jTET/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java deleted file mode 100644 index 4b5a44133f2db73da1f6fc7771b1a273d4da6379..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3Generator.java +++ /dev/null @@ -1,174 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.cvc3generator; - -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.MatlabParser; -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.tablularexpression.Cell; -import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator; -import java.util.ArrayList; -import java.util.ArrayDeque; -import java.util.Deque; -import java.util.List; - -import org.apache.commons.lang3.StringUtils; - -/** - * - * @author Matthew Dawson - */ -final public class HierarchicalGridCVC3Generator implements HierarchcialGridCheckerGenerator { - - public HierarchicalGridCVC3Generator(VariableCollection variableDefinitions, int queryCountStart) { - m_variableDefinitions = variableDefinitions; - m_currentTCC = queryCountStart; - } - - private String generateQueryPrefix() { - if (!m_parentCellsCVC3Code.isEmpty()){ - String output = "("; - output += StringUtils.join(m_parentCellsCVC3Code, " AND "); - output += ") => "; - return output; - } - return ""; - } - - private void outputCells() { - // First is disjoint testing. - m_output += "ECHO \"begin" + m_currentTCC + "\";\n"; - m_output += "PUSH;\n"; - - String query = "QUERY "; - query += generateQueryPrefix(); - query += "(" + StringUtils.join(m_currentDisjointQueries, " AND\n"); - query += ");"; - m_queries.add(query); - m_output += query + "\n"; - - m_output += "POP;\n"; - m_output += "ECHO \"end" + m_currentTCC + "\";\n"; - - // Finished first TCC, increment counter. - m_currentTCC++; - - // Next is complete. - m_output += "ECHO \"begin" + m_currentTCC + "\";\n"; - m_output += "PUSH;\n"; - - query = "QUERY "; - query += generateQueryPrefix(); - query += "(" + StringUtils.join(m_currentCompleteQueries, " OR "); - query += ");"; - m_queries.add(query); - m_output += query + "\n"; - - m_output += "POP;\n"; - m_output += "ECHO \"end" + m_currentTCC + "\";\n"; - - // Finished other TCC, increment counter. - m_currentTCC++; - - m_currentlyRunning = false; - - // And finally clear the running list of current queries. - m_currentCompleteQueries.clear(); - m_currentDisjointQueries.clear(); - } - - @Override - public void descendIntoGridFromCell(Cell cell) { - if (m_currentlyRunning) { - outputCells(); - } - m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType)); - m_currentlyRunning = true; - } - - @Override - public void ascendFromGrid() { - if (m_currentlyRunning) { - outputCells(); - } - m_parentCellsCVC3Code.removeFirst(); - } - - @Override - public void handleEdgeCell(Cell cell) { - handleLeafCell(cell); - } - - @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); - - // Next form the disjoint queries and add to the list. - for(String otherCellCode : m_currentCompleteQueries) { - String newDisjointQuery = "NOT ( " + otherCellCode + " AND " + newCellCode + " )"; - m_currentDisjointQueries.add(newDisjointQuery); - } - - // Lastly add the cell to the list for the complete query - m_currentCompleteQueries.add(newCellCode); - } - - @Override - public String getFinalString() { - if (m_currentlyRunning) { - outputCells(); - } - return m_output; - } - - public List getFinalQueries() { - if (m_currentlyRunning) { - outputCells(); - } - return m_queries; - } - - Deque m_parentCellsCVC3Code = new ArrayDeque(); - - List m_currentDisjointQueries = new ArrayList(); - List m_currentCompleteQueries = new ArrayList(); - - boolean m_currentlyRunning = true; - int m_currentTCC = 1; - - String m_output = ""; - List m_queries = new ArrayList(); - - // To fix properly. - VariableCollection m_variableDefinitions; - static BooleanVariableType m_booleanType = new BooleanVariableType(); - CVC3Generator m_CVC3Generator = new CVC3Generator(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/BinaryOperation.java b/jTET/src/main/java/ca/mcscert/jtet/expression/BinaryOperation.java deleted file mode 100644 index 1b679d3e78d0956d2c183b0831c892b173ca3922..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/BinaryOperation.java +++ /dev/null @@ -1,81 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import java.util.Arrays; -import java.util.Collection; - -/** - * - * @author matthew - */ -public enum BinaryOperation { - - Addition, - Minus, - Multiplication, - Division, - Exponentiation, - - GreaterThen, - GreaterThenEqual, - LessThen, - LessThenEqual, - Equals, - NotEquals, - - Implies, - BooleanAnd, - BooleanOr; - - Collection getInputTypeForOutput(VariableTypeMarker outputType) { - // 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())) { - throw new IllegalArgumentException("Boolean operators and comparisons require a boolean output type!"); - } - } - if (outputType instanceof EnumerationVariableType) { - if (this != Equals && this != NotEquals) { - throw new IllegalArgumentException("Enumeration types can only be checked for equality!"); - } - } - - // Comparisions produce boolean outputs! - switch(this) { - case GreaterThen: - case GreaterThenEqual: - case LessThen: - case LessThenEqual: - return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker()}); - case Equals: - case NotEquals: - return Arrays.asList(new VariableTypeMarker[]{new RealVariableType(), new FixedPointVariableType.Marker(), new EnumerationVariableType.Marker()}); - } - return Arrays.asList(new VariableTypeMarker[]{outputType}); - } - - 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())) { - throw new IllegalArgumentException("Boolean operators require a boolean input type!"); - } - } - - // Comparisions produce boolean outputs! - switch(this) { - case GreaterThen: - case GreaterThenEqual: - case LessThen: - case LessThenEqual: - case Equals: - case NotEquals: - return new BooleanVariableType(); - } - return inputType; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/BooleanVariableType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/BooleanVariableType.java deleted file mode 100644 index dc04eaff3663894e50623a90d1a00ea2082fc8b1..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/BooleanVariableType.java +++ /dev/null @@ -1,27 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public class BooleanVariableType extends VariableType { - - @Override - public boolean equals(Object other) { - return other instanceof BooleanVariableType; - } - - @Override - public int hashCode() { - return 0; - } - - @Override - public boolean canCastToType(VariableType type) { - return false; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java b/jTET/src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java deleted file mode 100644 index 38142aa3683787a0fe437c5c17c363c562dc94be..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/CVC3Generator.java +++ /dev/null @@ -1,283 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import java.math.BigDecimal; -import java.math.BigInteger; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - -import org.apache.commons.lang3.StringUtils; - -/** - * - * @author matthew - */ -final public class CVC3Generator implements CheckerGenerator{ - - // For operations that don't have specific signed/unsigned representations, use this function. - private static String GetIndifferentFixedPointFunctionFor(BinaryOperation op) { - switch (op) { - case Addition: - return "BVPLUS("; - case Minus: - return "BVSUB("; - case Multiplication: - return "BVMULT("; - } - throw new IllegalArgumentException("Operation " + op + " doesn't have a fixed point function!"); - } - - private static String GetSignedFixedPointFunctionFor(BinaryOperation op) { - switch (op) { - case Division: - return "BVSDIV("; - case GreaterThen: - return "BVSGT("; - case GreaterThenEqual: - return "BVSGE("; - case LessThen: - return "BVSLT("; - case LessThenEqual: - return "BVSLE("; - } - return GetIndifferentFixedPointFunctionFor(op); - } - - private static String GetUnsignedFixedPointFunctionFor(BinaryOperation op) { - switch (op) { - case Division: - return "BVUDIV("; - case GreaterThen: - return "BVGT("; - case GreaterThenEqual: - return "BVGE("; - case LessThen: - return "BVLT("; - case LessThenEqual: - return "BVLE("; - } - return GetIndifferentFixedPointFunctionFor(op); - } - - private static String GetInfixSymbolFor(BinaryOperation op) { - switch (op) { - case Addition: - return "+"; - case Minus: - return "-"; - case Multiplication: - return "*"; - case Division: - return "/"; - case Exponentiation: - return "^"; - case GreaterThen: - return ">"; - case GreaterThenEqual: - return ">="; - case LessThen: - return "<"; - case LessThenEqual: - return "<="; - case Equals: - return "="; - case NotEquals: - return "/="; - case BooleanAnd: - return "AND"; - case BooleanOr: - return "OR"; - case Implies: - return "=>"; - } - throw new RuntimeException("Should never happen!"); - } - - protected static String ConvertToOutputOp(BinaryOperation op, VariableType type) { - switch (OpTypeForVariableType(op, type)) { - case Function: - String func = GetSignedFixedPointFunctionFor(op); - if (!((FixedPointVariableType) type).isSigned()) { - func = GetUnsignedFixedPointFunctionFor(op); - } - if (op == BinaryOperation.Addition || op == BinaryOperation.Multiplication) { - FixedPointVariableType typeF = (FixedPointVariableType) type; - return func + typeF.digits() + ","; - } else { - return func; - } - case CenterOp: - return GetInfixSymbolFor(op); - default: - throw new IllegalStateException("CVC3 Operation type asked for that doesn't exist!"); - } - } - - private static OperationType OpTypeForVariableType(BinaryOperation op, VariableType type) { - if (type instanceof FixedPointVariableType && op != BinaryOperation.Equals && op != BinaryOperation.NotEquals) { - if (op == BinaryOperation.Exponentiation) { - throw new IllegalArgumentException("Cannot generate exponential functions in fixed point!"); - } - return OperationType.Function; - } else { - return OperationType.CenterOp; - } - } - - @Override - public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) { - switch (CVC3Generator.OpTypeForVariableType(op, usedType)) { - case CenterOp: - return "(" + lhsExp + " " + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + rhsExp + ")"; - case Function: - return CVC3Generator.ConvertToOutputOp(op, usedType) + lhsExp + "," + rhsExp + ")"; - default: - throw new IllegalStateException("Cannot output expression operation for requested operation type."); - } - } - - private static String GetUnaryOperationSymbolFor(UnaryOperation op) { - switch (op) { - case Negation: - return "NOT"; - case Minus: - return "-"; - } - throw new RuntimeException("Should never happen! Asked for unhandled op: " + op + "!"); - } - - @Override - public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) { - switch (CVC3Generator.OpTypeForVariableType(op, usedType)) { - case PrefixOp: - return "(" + CVC3Generator.ConvertToOutputOp(op, usedType) + " " + expression + ")"; - case Function: - return CVC3Generator.ConvertToOutputOp(op, usedType) + "(" + expression + ")"; - default: - throw new IllegalStateException("Cannot output expression operation for requested operation type."); - } - } - - private static OperationType OpTypeForVariableType(UnaryOperation op, VariableType usedType) { - if (usedType instanceof FixedPointVariableType) { - return OperationType.Function; - } - return OperationType.PrefixOp; - } - - private static String ConvertToOutputOp(UnaryOperation op, VariableType usedType) { - switch (op) { - case Negation: - return "NOT"; - case Minus: - if (usedType instanceof FixedPointVariableType) { - return "BVUMINUS"; - } else { - return "-"; - } - } - throw new IllegalArgumentException("Unhandled operation: " + op); - } - - public String GenerateVariableType(VariableType type) { - if (type instanceof RealVariableType) { - return "REAL"; - } else if (type instanceof FixedPointVariableType) { - return "BITVECTOR(" + ((FixedPointVariableType) type).digits() + ")"; - } else if (type instanceof BooleanVariableType) { - return "BOOLEAN"; - } else if (type instanceof EnumerationVariableType) { - return ((EnumerationVariableType) type).name(); - } else { - throw new IllegalArgumentException("CVC3 Doesn't handle this variable type (Class: " + type.getClass().getName() + ")"); - } - } - - @Override - public String GenerateVariablesDeclaration(VariableCollection variableCollection) { - Map vars = variableCollection.getVariables(); - Set emittedEnumerations = new HashSet(); - - StringBuilder ret = new StringBuilder(); - // First generate all the enumeration types. - for(Variable var : vars.values()) { - if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) { - EnumerationVariableType enumType = (EnumerationVariableType) var.type(); - ret.append("DATATYPE\n ") - .append((enumType).name()) - .append(" = "); - - boolean firstValue = false; - for(String enumValue : enumType.enumerationValues()) { - if (firstValue == true) { - ret.append(" | "); - } - firstValue = true; - ret.append(enumValue); - } - ret.append("\nEND;\n"); - - emittedEnumerations.add(enumType); - } - } - - // Then generate all the variables. - for(Variable var : vars.values()) { - ret.append(var.name()) - .append(":") - .append(GenerateVariableType(var.type())) - .append(";\n"); - } - - // Then generate the variable predicates. This ensures any dependent variables are declared. - for(Variable var : vars.values()) { - if (var.type().subtypePredicate() != null) { - ret.append("ASSERT ") - .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType())) - .append(";\n"); - } - } - - return ret.toString(); - } - - @Override - public String GenerateLiterlaValue(String value, VariableType requestedType) { - if (requestedType instanceof RealVariableType) { - if (value.contains(".")) { - String[] fraction = value.split("\\."); - - String res = "("; - res += StringUtils.join(fraction, ""); - res += "/1" + StringUtils.repeat('0', fraction[1].length()) + ")"; - - return res; - } else { - return value; - } - } else if (requestedType instanceof FixedPointVariableType) { - FixedPointVariableType type = (FixedPointVariableType) requestedType; - BigDecimal decimal = new BigDecimal(value); - decimal = decimal.multiply(BigDecimal.valueOf(1 << type.fractionPart())); - BigInteger intOut = decimal.toBigIntegerExact(); - - //This gets the two's compliment representation. Ugly for loop, but best I could find. - String bits = ""; - for (int i = intOut.bitLength() - 1; i >= 0; --i) { - bits += (intOut.testBit(i)) ? '1' : '0'; - } - - if (intOut.signum() < 0) { - return "0bin" + StringUtils.repeat('1', type.digits() - bits.length()) + bits; - } else { - return "0bin" + StringUtils.repeat('0', type.digits() - bits.length()) + bits; - } - } else { - throw new IllegalArgumentException("Can't cast literal to that type!"); - } - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/CheckerGenerator.java b/jTET/src/main/java/ca/mcscert/jtet/expression/CheckerGenerator.java deleted file mode 100644 index a9ef037073972e1495dc8cd9c1369bdd69560366..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/CheckerGenerator.java +++ /dev/null @@ -1,16 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public interface CheckerGenerator { - public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType); - public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType); - public String GenerateLiterlaValue(String value, VariableType requestedType); - public String GenerateVariablesDeclaration(VariableCollection vars); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/EnumerationVariableType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/EnumerationVariableType.java deleted file mode 100644 index 5eaf52c5d9ced18907cfe75a9a2fb3c950fda162..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/EnumerationVariableType.java +++ /dev/null @@ -1,65 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import java.util.LinkedHashSet; -import java.util.Set; - -/** - * - * @author matthew - */ -final public class EnumerationVariableType extends VariableType { - public EnumerationVariableType(String name) { - m_name = name; - } - - public Set enumerationValues() { - return m_values; - } - - public String name() { - return m_name; - } - - @Override - public boolean canCastToType(VariableType type) { - return false; - } - - private final Set m_values = new LinkedHashSet(); - private final String m_name; - - public static class Marker implements VariableTypeMarker { - @Override - public boolean isMarkerFor(VariableType m_type) { - return m_type instanceof EnumerationVariableType; - } - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/Expression.java b/jTET/src/main/java/ca/mcscert/jtet/expression/Expression.java deleted file mode 100644 index 05a64bd1175e4bfdbc620f7c43a146617ba1f4d6..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/Expression.java +++ /dev/null @@ -1,19 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public interface Expression { - - /* This methods returns an actual variable type for the requested input type. If due to the setup of the system, - * this is not possible, then this function should return null. - */ - VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType); - - String getCheckerOutput(CheckerGenerator generator, VariableType requestedType); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionBinaryOperation.java b/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionBinaryOperation.java deleted file mode 100644 index 691e528ad631ad0ed4c5107443dcba737ed63dc6..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionBinaryOperation.java +++ /dev/null @@ -1,85 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import java.util.Collection; - -/** - * - * @author matthew - */ -public final class ExpressionBinaryOperation implements Expression, ExpressionWithSubExpression { - - public ExpressionBinaryOperation(Expression lhs, BinaryOperation op, Expression rhs) { - m_lhs = lhs; - m_rhs = rhs; - m_op = op; - } - - public void setLHS(Expression expr) { - m_lhs = expr; - } - - public void setRHS(Expression expr) { - m_rhs = expr; - } - - private VariableType getInputTypeForOutput(VariableTypeMarker requestedType) { - Collection allowedInputTypes = m_op.getInputTypeForOutput(requestedType); - for(VariableTypeMarker allowedType : allowedInputTypes) { - VariableType inputType = m_lhs.actualOutputTypeForRequestedOutput(allowedType); - if(inputType != null && - m_rhs.actualOutputTypeForRequestedOutput(inputType) != null) { - return inputType; - } - inputType = m_rhs.actualOutputTypeForRequestedOutput(allowedType); - if(inputType != null && - m_lhs.actualOutputTypeForRequestedOutput(inputType) != null) { - return inputType; - } - } - return null; - } - - @Override - public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) { - VariableType inputType = getInputTypeForOutput(requestedType); - if (inputType != null) { - return m_op.getOutputForInput(inputType); - } - return null; - } - - @Override - public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) { - VariableType inputType = getInputTypeForOutput(requestedType); - if (inputType == null) { - throw new IllegalArgumentException("Requested output type is not valid for the expression's output type (" + requestedType.getClass().getSimpleName() + "!"); - } - - String lhsExp = m_lhs.getCheckerOutput(generator, inputType); - String rhsExp = m_rhs.getCheckerOutput(generator, inputType); - - return generator.GenerateBinaryOperation(m_op, lhsExp, rhsExp, inputType); - } - - @Override - public Expression getSubExpression() { - return m_rhs; - } - - @Override - public void setSubExpression(Expression subExpression) { - m_rhs = subExpression; - } - - @Override - public String toString() { - return "(" + m_lhs.toString() + " " + m_op.toString() + " " + m_rhs.toString() + ")"; - } - - private Expression m_lhs, m_rhs; - private BinaryOperation m_op; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionUnaryOperation.java b/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionUnaryOperation.java deleted file mode 100644 index 10fcf8f631b9f380dc101e47eddb4f8186848805..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionUnaryOperation.java +++ /dev/null @@ -1,55 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public final class ExpressionUnaryOperation implements Expression, ExpressionWithSubExpression { - - public ExpressionUnaryOperation(UnaryOperation op, Expression rhs) { - m_expr = rhs; - m_op = op; - } - - void setExpression(Expression expr) { - m_expr = expr; - } - - @Override - public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) { - return m_expr.actualOutputTypeForRequestedOutput(requestedType); - } - - @Override - public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) { - if (actualOutputTypeForRequestedOutput(requestedType) == null) { - throw new IllegalArgumentException("Can generate output for requested type!"); - } - - String expression = m_expr.getCheckerOutput(generator, requestedType); - - return generator.GenerateUnaryOperation(m_op, expression, requestedType); - } - - @Override - public Expression getSubExpression() { - return m_expr; - } - - @Override - public void setSubExpression(Expression subExpression) { - m_expr = subExpression; - } - - @Override - public String toString() { - return "( " + m_op + " " + m_expr + ")"; - } - - private Expression m_expr; - private UnaryOperation m_op; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionValue.java b/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionValue.java deleted file mode 100644 index 3fc78ae474a9adda9a5ceb35895b6b8334f5e19b..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionValue.java +++ /dev/null @@ -1,14 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** This interface means the expression is a value with no further expansion possible. - * This is just a marker to mean an expression is only a value. - * - * @author matthew - */ -public interface ExpressionValue extends Expression { - -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionWithSubExpression.java b/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionWithSubExpression.java deleted file mode 100644 index bb668c69e1ef6e993d7ca17168d0842044acb4bb..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/ExpressionWithSubExpression.java +++ /dev/null @@ -1,14 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public interface ExpressionWithSubExpression { - public Expression getSubExpression(); - public void setSubExpression(Expression subExpression); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/FixedPointVariableType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/FixedPointVariableType.java deleted file mode 100644 index a4a356d3f9e8ba4525b2e6a9245516a04611c17f..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/FixedPointVariableType.java +++ /dev/null @@ -1,71 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -final public class FixedPointVariableType extends VariableType { - - public FixedPointVariableType(boolean signed, int digits, int fractionPart) { - m_isSigned = signed; - m_digits = digits; - m_fractionPart = fractionPart; - } - - public boolean isSigned() { - return m_isSigned; - } - - public int digits() { - return m_digits; - } - - public int fractionPart() { - return m_fractionPart; - } - - @Override - public boolean canCastToType(VariableType type) { - return false; - } - - @Override - public boolean equals(Object othero) { - if (!(othero instanceof FixedPointVariableType)) { - return false; - } else { - FixedPointVariableType other = (FixedPointVariableType) othero; - if (other.m_isSigned == m_isSigned - && other.m_digits == m_digits - && other.m_fractionPart == m_fractionPart) { - return true; - } else { - return false; - } - } - } - - @Override - public int hashCode() { - int hash = 0; - hash += (this.m_isSigned ? 1 : 0); - hash = 2 * hash + this.m_fractionPart; - hash = 83 * hash + this.m_digits; - return hash; - } - - private final int m_fractionPart; - private final int m_digits; - private final boolean m_isSigned; - - public static class Marker implements VariableTypeMarker { - @Override - public boolean isMarkerFor(VariableType m_type) { - return m_type instanceof FixedPointVariableType; - } - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/Literal.java b/jTET/src/main/java/ca/mcscert/jtet/expression/Literal.java deleted file mode 100644 index 6b174dcbad66c7517ce465b047352d2858f2109d..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/Literal.java +++ /dev/null @@ -1,37 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public final class Literal implements Expression, ExpressionValue { - - public Literal(String value) { - m_value = value; - } - - @Override - public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) { - if (requestedType instanceof RealVariableType || - requestedType instanceof FixedPointVariableType) { - return (VariableType)requestedType; - } - return null; - } - - @Override - public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) { - return generator.GenerateLiterlaValue(m_value, requestedType); - } - - @Override - public String toString() { - return m_value; - } - - final String m_value; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/OperationType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/OperationType.java deleted file mode 100644 index 2c147c409ee86d4996ed46ad146648e3e7e1ca71..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/OperationType.java +++ /dev/null @@ -1,16 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public enum OperationType { - CenterOp, - PrefixOp, - PostfixOp, - Function; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/RealVariableType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/RealVariableType.java deleted file mode 100644 index 3dd464dbe63d959b16d56c11afa73470df5c17a5..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/RealVariableType.java +++ /dev/null @@ -1,26 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public final class RealVariableType extends VariableType { - @Override - public boolean equals(Object other) { - return other instanceof RealVariableType; - } - - @Override - public int hashCode() { - return 0; - } - - @Override - public boolean canCastToType(VariableType type) { - return false; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/SMTLIBGenerator.java b/jTET/src/main/java/ca/mcscert/jtet/expression/SMTLIBGenerator.java deleted file mode 100644 index 967613f4a8faed44234d8257e3d5aca28f040c29..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/SMTLIBGenerator.java +++ /dev/null @@ -1,196 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - -/** - * - * @author Matthew Dawson - */ -public class SMTLIBGenerator implements CheckerGenerator { - @Override - public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) { - return "(" + SMTLIBGenerator.GetUnaryOperationSymbolFor(op) + " " + expression + ")"; //To change body of implemented methods use File | Settings | File Templates. - } - - @Override - public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) { - return "(" + SMTLIBGenerator.GetBinaryOperationSymbolFor(op) + " " + lhsExp + " " + rhsExp + ")"; - } - - @Override - public String GenerateLiterlaValue(String value, VariableType requestedType) { - if (requestedType instanceof RealVariableType) { - if (value.contains(".")) { - return value; - } else { - return value + ".0"; - } - } else { - throw new IllegalArgumentException("Can't cast literal to that type!"); - } - } - - @Override - public String GenerateVariablesDeclaration(VariableCollection variableCollection) { - Map vars = variableCollection.getVariables(); - Set emittedEnumerations = new HashSet(); - - StringBuilder ret = new StringBuilder(); - // First generate all the enumeration types. - for(Variable var : vars.values()) { - if (var.type() instanceof EnumerationVariableType && !emittedEnumerations.contains(var.type())) { - // For each enumeration, first emit the actual enumeration type name. - EnumerationVariableType enumType = (EnumerationVariableType)var.type(); - ret.append("(declare-sort ") - .append(enumType.name()) - .append(" 0)\n"); - - // Next, emit the enumeration values, using the enumeration type. - for(String enumValue : enumType.enumerationValues()) { - ret.append("(declare-fun ") - .append(enumValue) - .append(" () ") - .append(enumType.name()) - .append(")\n"); - } - - // Restrict the enumeration values so that they are all considered different. - ret.append("(assert (distinct"); - for(String enumValue : enumType.enumerationValues()) { - ret.append(" ") - .append(enumValue); - } - ret.append("))\n"); - - // Finally, emit a function that ensure any enumeration variable can only be the values given. - ret.append("(define-fun is") - .append(enumType.name()) - .append(" ((val ") - .append(enumType.name()) - .append(")) Bool (or"); - for(String enumValue : enumType.enumerationValues()) { - ret.append(" (= val ") - .append(enumValue) - .append(")"); - } - ret.append("))\n"); - - emittedEnumerations.add(enumType); - } - } - - // Then generate all the variables. - for (Variable var : vars.values()) { - ret.append("(declare-fun ") - .append(var.name()) - .append(" () ") - .append(GenerateVariableType(var.type())) - .append(")\n"); - - // If variable is an enumeration, make sure that it is limited to only enumeration values. - if (var.type() instanceof EnumerationVariableType) { - ret.append("(assert (is") - .append(((EnumerationVariableType) var.type()).name()) - .append(" ") - .append(var.name()) - .append("))\n"); - } - } - - // Then generate the variable predicates. This ensures any dependent variables are declared. - for(Variable var : vars.values()) { - if (var.type().subtypePredicate() != null) { - ret.append("(assert ") - .append(var.type().subtypePredicate().getCheckerOutput(this, new BooleanVariableType())) - .append(")\n"); - } - } - return ret.toString(); - } - - public static String GenerateVariableType(VariableType type) { - if (type instanceof RealVariableType) { - return "Real"; - } else if (type instanceof BooleanVariableType) { - return "Bool"; - } else if (type instanceof EnumerationVariableType) { - return ((EnumerationVariableType) type).name(); - } else { - throw new IllegalArgumentException("SMT-LIB Doesn't handle this variable type (Class: " + type.getClass().getName() + ")"); - } - } - - private static String GetBinaryOperationSymbolFor(BinaryOperation op) { - switch (op) { - case Addition: - return "+"; - case Minus: - return "-"; - case Multiplication: - return "*"; - case Division: - return "/"; - case Exponentiation: - return "^"; - case GreaterThen: - return ">"; - case GreaterThenEqual: - return ">="; - case LessThen: - return "<"; - case LessThenEqual: - return "<="; - case Equals: - return "="; - case NotEquals: - return "distinct"; - case BooleanAnd: - return "and"; - case BooleanOr: - return "or"; - case Implies: - return "=>"; - } - throw new RuntimeException("Should never happen! Asked for unhandled op: " + op + "!"); - } - - private static String GetUnaryOperationSymbolFor(UnaryOperation op) { - switch (op) { - case Negation: - return "not"; - case Minus: - return "-"; - } - throw new RuntimeException("Should never happen! Asked for unhandled op: " + op + "!"); - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/UnaryOperation.java b/jTET/src/main/java/ca/mcscert/jtet/expression/UnaryOperation.java deleted file mode 100644 index 8e0f23ae916f974c65f59003ea70e2fbf37649b2..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/UnaryOperation.java +++ /dev/null @@ -1,15 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public enum UnaryOperation { - - Minus, - Negation; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/Variable.java b/jTET/src/main/java/ca/mcscert/jtet/expression/Variable.java deleted file mode 100644 index 998b6606136aca7d2ab1dd661aa118d2d775090d..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/Variable.java +++ /dev/null @@ -1,48 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public class Variable implements Expression, ExpressionValue { - public Variable(String name, VariableType type) { - m_name = name; - m_type = type; - } - - public String name() { - return m_name; - } - - public VariableType type() { - return m_type; - } - - @Override - public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) { - if (requestedType.isMarkerFor(m_type)) { - return m_type; - } - return null; - } - - private String m_name; - private VariableType m_type; - - @Override - public String getCheckerOutput(CheckerGenerator generator, VariableType requestedType) { - if (!type().equals(requestedType)) { - throw new IllegalArgumentException("Requested output type is not the expression's output type!"); - } - return m_name; - } - - @Override - public String toString() { - return m_name; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableCollection.java b/jTET/src/main/java/ca/mcscert/jtet/expression/VariableCollection.java deleted file mode 100644 index 0e988d030df9cf9a226e7c47810647619443c1b6..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableCollection.java +++ /dev/null @@ -1,73 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import java.util.HashMap; -import java.util.Map; -import java.util.Set; - -/** - * @author Matthew Dawson - */ -final public class VariableCollection { - public VariableCollection(Map variables, Set enumerationTypes) { - m_variables = variables; - if (m_variables != null) { - for(Map.Entry var : m_variables.entrySet()) { - m_variablesAndEnumeratedValues.put(var.getKey(), var.getValue()); - } - } - - if (enumerationTypes != null) { - for(EnumerationVariableType enumType : enumerationTypes) { - for(String enumValue : enumType.enumerationValues()) { - if (m_variablesAndEnumeratedValues.containsKey(enumValue)) { - new IllegalArgumentException("Enumerated value conflicts with existing variable!"); - } - m_variablesAndEnumeratedValues.put(enumValue, new Variable(enumValue, enumType)); - } - } - } - } - - public VariableCollection(Map variables) { - this(variables, null); - } - - public Map getVariablesAndEnumeratedValues() { - return m_variablesAndEnumeratedValues; - } - - public Map getVariables() { - return m_variables; - } - - private final Map m_variables; - private final Map m_variablesAndEnumeratedValues = new HashMap(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableType.java b/jTET/src/main/java/ca/mcscert/jtet/expression/VariableType.java deleted file mode 100644 index a114b79cda0e6292e9be2e9f11e178954df094ea..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableType.java +++ /dev/null @@ -1,38 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -/** - * - * @author matthew - */ -public abstract class VariableType implements VariableTypeMarker { - /** - * Marks whether the type can be cast to this type. Certain values may be - * castable to a different type. If possible, this method will mark it as - * such. - * @param type The type this variable type should cast to. - * @return True if this type can act like the other type. False otherwise. - */ - abstract public boolean canCastToType(VariableType type); - - /* By default, all types are their own markers. Thus by default implement isMarkerFor to represent that. Override - * if further behaviour is necessary. - */ - @Override - 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; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableTypeMarker.java b/jTET/src/main/java/ca/mcscert/jtet/expression/VariableTypeMarker.java deleted file mode 100644 index 4060722bb6a751565d96a2e6c7f43cb67c2fa752..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/expression/VariableTypeMarker.java +++ /dev/null @@ -1,36 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -/** - * @author Matthew Dawson - */ -interface VariableTypeMarker { - boolean isMarkerFor(VariableType m_type); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.g4 b/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.g4 deleted file mode 100644 index f20e7dc1d527fb3ba55574535ac4d838a1dd7ab4..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.g4 +++ /dev/null @@ -1,678 +0,0 @@ -grammar MatlabParser; - -/* - -Things to fix: - -0) lots of warnings. This is because of anonymous function handles; see details in appropriate XXX comment. - if you comment out one line, all of the warnings go away. I believe that even with the warnings, - the grammar is doing the right thing. -1) "clear" statements can accept wildcards as part of IDs, but we can't (due to the way lexing happens) -2) control flow statements require a newline or comma to resolve an ambiguity (but matlab doesn't) -3) vector construction requires comma delimiters because of whitespace madness (but matlab doesn't) -4) matrix transpose doesn't work (again because of lexing, and distinguishing strings from transposes). -5) block comments don't work (and I can't figure out why) - -For each case, see the appropriate XXX comment below. - -*/ - -/*options { - output=AST; -} - -tokens { - // imaginary nodes for our AST - PROGRAM; - FUNCTION; - FUNCTION_RETURN; - PARAMETER_LIST; - FUNCTION_PARAMETER_LIST; - STATEMENT_LIST; - EXPRESSION; - EXPR_STMT; - NULL_STMT; - ASSIGN; - APPLY; - FIELDACCESS; - DYNFIELDACCESS; - CELLACCESS; - MATRIX; - VECTOR; - CELL; - CLEAR; - LHS; - RHS; - ID_NODE; - PARENS; -}*/ - -@parser::members{ - -// This scans backwards in the token stream looking for a hidden newline. -// The newline must occur after the last visible token and before the current token. - -// C IMPLEMENTATION -/* - - int check_for_hidden_newline( pmatlabParser ctx ) { - - pANTLR3_TOKEN_STREAM ts = ctx->pParser->tstream; - - int tok_ind = INDEX(); // this is the index of LT(1) - pANTLR3_COMMON_TOKEN cur_tok = LT(1); - - ANTLR3_UINT32 cur_tok_chan = cur_tok->getChannel( cur_tok ); // this is the current channel. - - int rval = 0; - - while ( tok_ind > 0 ) { - tok_ind--; - cur_tok = ts->get( ts, tok_ind ); - if ( cur_tok->getChannel( cur_tok ) == cur_tok_chan ) { - // uh-oh. we found a non-hidden token further back in the stream, but no newline in between. fail. - break; - } - if ( cur_tok->getType( cur_tok ) == NL ) { - // found it! - rval = 1; - break; - } - } - - return rval; - } - - - -*/ -// JAVA IMPLEMENTATION -// Useful for debugging. NOTE: UNCOMMENT THE RELEVANT LINE IN hidden_nl! - - -boolean check_for_hidden_newline( TokenStream input ) { - int tok_ind = input.index(); // this is the index of LT(1) - Token cur_tok = input.LT(1); - int cur_tok_chan = cur_tok.getChannel(); // this is the current channel. - - boolean rval = false; - - while ( tok_ind > 0 ) { - tok_ind--; - cur_tok = input.get( tok_ind ); - - if ( cur_tok.getChannel() == cur_tok_chan ) { - // uh-oh. we found a non-hidden token further back in the stream, but no newline in between. fail. - break; - } - if ( cur_tok.getType() == NL ) { - // found it! - rval = true; - break; - } - } - - return rval; -} - - - -} // end of parser::members - -// -// ================================================================== -// -// PARSER RULES -// - -// we mostly want to ignore whitespace, but every now and then -// it's significant -- as a statement delimiter, as part of -// matrix construction, etc. This checks the hiddent channel for a newline. - -hidden_nl - // Java - : ( { check_for_hidden_newline( _input ) }? ) - // C - //: ( { check_for_hidden_newline( ctx ) }? ) - ; - -nloc : ( hidden_nl | COMMA ); // mnemonic: newline or comma -nlos : ( hidden_nl | SEMI ); // mnemonic: newline or semicolon - -// -// scripts and m-files -// - -mfile : function_definition+; - -scriptfile: statement_list; - -program : func_or_statement_list; - -// -// functions and statements -// - -function_definition - : FUNCTION function_return? ID parameter_list? nloc - func_or_statement_list - END - ; - -function_return - : ID EQ - | LSBRACE (ID COMMA?)+? RSBRACE EQ - ; - -// the contents of a function (or a .m file) are statements and function definitions -func_or_statement: ( function_definition | statement ); -func_or_statement_list: func_or_statement*; - -// there are times when you can have a list of statements, but not function -// definitions -- for example, inside of an "if" block. -statement_list - : statement* - ; - -parameter_list - : LPAREN ( ID COMMA? )* RPAREN - ; - -// Note: there is a functional difference between terminating a statement with a -// newline vs. a semicolon, so we have to remember the appropriate token in the AST. - -statement - : assignment nlosoc - | expression nlosoc - | if_statement - | for_statement - | while_statement - | switch_statement - | try_statement - | return_statement - | break_statement - | continue_statement - | clear_statement - | global_statement - | persistent_statement - | SEMI // a null statement - ; - -// Add an assignment statement. This avoids some ugliness regarding case sensitive file systems. -assignment: lhs EQ rhs; - -nlosoc : ( hidden_nl | SEMI | COMMA ); - -lhs: id_plus_indexers; -rhs: expression; - -/* -XXX CONTROL FLOW AMBIGUITIES: - -The statement - while a (5) end; -is parsed as - while (a(5)) - [empty] - end; -and not - while a - (5) - end; -but I can't seem to get a non-ambiguous grammar to do that. -so, I enforce a newline or a comma after the expression to -delimit it from the body of the statements. everywhere you -see a "nloc" below, you shouldn't really need one; this -grammar therefore parses only a subset of "true" matlab. -(Of course, *I* think that reasonable code wouldn't have -such ambiguities, don't you? :) ) - -Similarly: - -The statement - while 1 -5, end; -is parsed as - while (1) - -5, - end; -while the statement - while 1 - 5, end; -is parsed as - while (1-5) - [empty] - end; - -NOTE : THIS FEELS A LOT LIKE THE VECTOR AMBIGUITIES BELOW. -Perhaps solving one solves them both, since both are essentially -'space-delimited expressions' ambiguities. - -*/ - -if_statement - : IF expression nloc statement_list elseif_statement* else_statement? END - ; - -elseif_statement - : ELSEIF expression nloc statement_list - ; - -else_statement - : ELSE statement_list - ; - -for_statement - : FOR ID EQ expression nloc statement_list END - ; - -while_statement - : WHILE expression nloc statement_list END - ; - -switch_statement - : SWITCH expression nloc case_statement* otherwise_statement? END - ; - -case_statement - : CASE expression nloc statement_list - ; - -otherwise_statement - : OTHERWISE nloc statement_list - ; - -try_statement - : TRY statement_list catch_statement? END - ; - -catch_statement - : CATCH ID? nlosoc statement_list - ; - -return_statement - : RETURNS nlosoc - ; - -break_statement - : BREAK nlosoc - ; - -continue_statement - : CONTINUE nlosoc - ; - -global_statement - : GLOBAL (ID COMMA?)+? nlosoc - ; - -persistent_statement - : PERSISTENT (ID COMMA?)+? nlosoc - ; - -/* -XXX CLEAR STATEMENT WILDCARDS - -How can we fix wildcards in clear statements? -For example, "clear foo* bob" ought to be parsed as - clear (foo*) (bob) -but this is hard since the '*' is lexed as its own -character, and we've discarded the fact that there is -whitespace between '*' and 'bob', but not between -'foo' and '*'. This means we can't tell that it's supposed -to be part of the foo identifier. - -Options for solving: -1) parser-context sensitive lexing? (I don't think this is right) -2) poke around in the hidden channel to find out where the whitespace is. - this is probably the best solution, but seems like a pain. - -*/ - - -clear_statement - : CLEAR (ID COMMA?)*? nlosoc - ; - -// -// =============================== -// - -// a precedence hierarchy for parsing expressions - -// these are groups of operators that have equivalent precedences -g1 : ( NEQ | DOUBLE_EQ | GRTE | GRT | LSTE | LST ); -g2 : ( PLUS | MINUS ); -g3 : ( LEFTDIV | RIGHTDIV | TIMES | EL_LEFTDIV | EL_RIGHTDIV | EL_TIMES ); -g4 : ( EXP | EL_EXP ); - - -/* - -XXX MATRIX TRANSPOSE PROBLEM. - -The single quote operator is problematic because of things like this: - -aa' + foo('some string here')+bb' - -Right now, the operator is placed in the correct place in the grammar, -and the grammar checks out just fine, but you get lexing errors if you -try to use it. - -*/ - -postfix_operator - : ( CCT | EL_CCT ); -prefix_operator - : ( PLUS | MINUS | NEG ); - -// the hierarchy is defined from LOWEST to HIGHEST priority. - -expression : e0; - -e0 : e1; - -e1 : e2 (LOG_OR e2)*; -e2 : e3 (LOG_AND e3)*; -e3 : e4 (BIN_OR e4)*; -e4 : e5 (BIN_AND e5)*; -e5 : e6 (g1 e6)*; -e6 : e7 (COLON e7)*; -e7 : e8 (g2 e8)*; -e8 : e9 (g3 e9)*; -e9 : prefix_operator e9 | e10; -e10 : e11 (g4 e11)*; // note: in matlab, exponentiation is left-associative -e11 : unary_expression postfix_operator?; - -unary_expression - : base_expression #BASE_EXPRESIION - | LPAREN expression RPAREN # PARENS_EXPRESSION - ; - -base_expression - : id_plus_indexers - | literal_number - | STRING - | anon_func_handle - | cell - | matrix - ; - -literal_number - : INT - | FLOAT - ; - -/* -XXX ANONYMOUS EXPRESSION AMBIGUITIES - -This generates a ton of warnings, but it does the right thing. -At least, I think it does. - -We want anonymous expressions to be "greedy". - -The statement - a+@()x+y -parses as - a+( @()x+y ) -and not as - a+ ( @()x ) +y -but I can't seem to make the right behavior explicit. The way that -ANTLR is disabling the alternatives seems to result in the right -behavior, though. - -If you comment out the second alternative here, the grammar should -check out perfectly clean. -*/ - -anon_func_handle - : AT ID - | AT parameter_list (expression)? - ; - -// this captures things like foo.(bar){3,4}.baz -id_plus_indexers - : ( i1=ID ) - ( DOT ( i2=ID ) - | LPAREN expression RPAREN - | LPAREN fpl1=function_parameter_list? RPAREN - | LBRACE fpl2=function_parameter_list RBRACE - )* - ; - -// also permits the use of the colon as an "expression" -function_parameter_list - : function_parameter ( COMMA function_parameter )* - ; - -function_parameter : expression | COLON ; - -matrix : LSBRACE vector? ( nlos vector )* RSBRACE; - -cell : LBRACE vector? ( nlos vector )* RBRACE; - -/* - -XXX - -I think the rule is the following - -1) if a +/- does not have any space to the right, it's interpreted - as a unary op -2) if there's no whitespace to the left of the operator, it's - grouped to the left. -3) if there's whitespace to the right and left, it's treated as - a binary op, and expressions are required on the right and left. - -Vectors are pretty crazy. Because you have a list of expressions -that can be separated by nothing but whitespace, all sorts of parsing -ambiguities start happening. Whitespace becomes syntactically -meaningful in strange ways that are not totally context free. -For example, - -[ a + b ] is parsed as [ (a+b) ] -[ a+b ] is parsed as [ (a+b) ] -[ a +b ] is parsed as [ (a) (+b) ] - -A longer example: - -[ 1+ 2+ 3 ] parses to 6 -[ 1 + 2+ 3 ] 6 -[ 1 +2+ 3 ] 1 5 -[ 1+ 2 + 3 ] 6 -[ 1 + 2 + 3 ] 6 -[ 1 +2 + 3 ] 1 5 -[ 1+ 2 +3 ] 3 3 -[ 1 + 2 +3 ] 3 3 -[ 1 +2 +3 ] 1 2 3 - -So, the weird thing is that we can't just look for the absence of a -space between '+' and the next character to determine if it's a binary -or unary operator -- we also have to know if there's a space to the -left of it. - -This is mostly a problem for prefix operators which can be ambiguous -in this context, but it also shows up in things like cell arrays -of anonymous function expressions. - -size( { @()a+b } ) is [ 1 1 ] -size( { @()a +b } ) is [ 1 2 ] -size( { @()a + b } ) is [ 1 1 ] - -NOTE : this feels like the control flow ambiguities above, -since both are essentially "whitespace-delimited expression" problems. - -*/ - -// XXX The COMMA should really have a ? after it!!! -// vector : ( expression COMMA? )+; -vector : expression ( COMMA expression )*; - -// -// ================================================================== -// -// LEXER RULES -// - -// -// language keywords -// - -BREAK : 'break'; -CASE : 'case'; -CATCH : 'catch'; -CONTINUE: 'continue'; -ELSE : 'else'; -ELSEIF : 'elseif'; -END : 'end'; -FOR : 'for'; -FUNCTION: 'function'; -GLOBAL : 'global'; -IF : 'if'; -OTHERWISE: 'otherwise'; -PERSISTENT: 'persistent'; -RETURNS : 'return'; // not "RETURN" to avoid #define conflicts with readline.h -SWITCH : 'switch'; -TRY : 'try'; -VARARGIN: 'varargin'; -WHILE : 'while'; -CLEAR : 'clear'; - -ENDS : END SEMI? ; - -// -// operators and assignments -// - -DOUBLE_EQ : '=='; - -LOG_OR : '||'; -LOG_AND : '&&'; -LSTE : '<='; -GRTE : '>='; -NEQ : '~='; - -EL_TIMES : '.*'; -EL_LEFTDIV : './'; -EL_RIGHTDIV : '.\\'; -EL_EXP : '.^'; -EL_CCT : '.\''; - -EQ : '='; - -BIN_OR : '|'; -BIN_AND : '&'; - -LST : '<'; -GRT : '>'; - -COLON : ':'; - -PLUS : '+'; -MINUS : '-'; -NEG : '~'; -TIMES : '*'; - -LEFTDIV : '/'; -RIGHTDIV: '\\'; - -EXP : '^'; - -CCT : '\''; - -// -// Other useful language snippets -// - -SEMI : ';'; -LPAREN : '('; -RPAREN : ')'; -LBRACE : '{'; -RBRACE : '}'; -LSBRACE : '['; -RSBRACE : ']'; -AT : '@'; -DOT : '.'; -COMMA : ','; - -// -// comments -// - -NL : '\r'? '\n' -> channel(HIDDEN); // newline - -// XXX I can't seem to get block comments to work. The problem is that -// no matter what I do, the linecomment ends up "overriding" the block -// comment, and I get a lex error. I've tried syntactic predicates, -// but they didn't help... -// If I comment out the LINECOMMENT rule, the BLOCKCOMMENT works fine. -// So, since I can only seem to have one or the other, I'm commenting -// out BLOCKCOMMENT for now. - -//BLOCKCOMMENT -// : '%{' (options{greedy=false;} : .)* '%}' { $channel = HIDDEN; } -// ; - -LINECOMMENT - : '%' .*? NL -> channel(HIDDEN) - ; - -// I think this is how to use syntactic predicates, but it doesn't seem to work. -//COMMENT -// : ( '%{' ) => '%{' (options{greedy=false;}: .)* '%}' { $channel = HIDDEN; } -// | ( '%' (options{greedy=false;}: .)* NL ) { $channel = HIDDEN; } -// ; - - -THREEDOTS - : ( '...' NL ) -> channel(HIDDEN) - ; - -// -// identifiers, strings, numbers, whitespace -// - -ID : ('a'..'z'|'A'..'Z') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ; - -INT : '0'..'9'+ ; - -FLOAT - : ('0'..'9')+ '.' ('0'..'9')* EXPONENT? - | '.' ('0'..'9')+ EXPONENT? - | ('0'..'9')+ EXPONENT - ; - -STRING - : '\'' ( ESC_SEQ | ~('\\'|'\'') )* '\'' - ; - -WS - : ( ' ' - | '\t' - ) -> skip - ; - -fragment -EXPONENT - : ('e'|'E') ('+'|'-')? ('0'..'9')+ ; - -fragment -HEX_DIGIT - : ('0'..'9'|'a'..'f'|'A'..'F') ; - -fragment -ESC_SEQ - : '\\' ('b'|'t'|'n'|'f'|'r'|'\"'|'\''|'\\') - | UNICODE_ESC - | OCTAL_ESC - ; - -fragment -OCTAL_ESC - : '\\' ('0'..'3') ('0'..'7') ('0'..'7') - | '\\' ('0'..'7') ('0'..'7') - | '\\' ('0'..'7') - ; - -fragment -UNICODE_ESC - : '\\' 'u' HEX_DIGIT HEX_DIGIT HEX_DIGIT HEX_DIGIT - ; diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.java b/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.java deleted file mode 100644 index 85659aafe19c9117c6264cfbccd205b0fceb850c..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/MatlabParser.java +++ /dev/null @@ -1,385 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers; - -import ca.mcscert.jtet.expression.BinaryOperation; -import ca.mcscert.jtet.expression.Expression; -import ca.mcscert.jtet.expression.ExpressionUnaryOperation; -import ca.mcscert.jtet.expression.ExpressionValue; -import ca.mcscert.jtet.expression.ExpressionBinaryOperation; -import ca.mcscert.jtet.expression.ExpressionWithSubExpression; -import ca.mcscert.jtet.expression.Literal; -import ca.mcscert.jtet.expression.UnaryOperation; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.MatlabParserParser.G1Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.G2Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.G3Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.G4Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E0Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E1Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E2Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E3Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E4Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E5Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E6Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E7Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E8Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E9Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E10Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.E11Context; -import ca.mcscert.jtet.parsers.MatlabParserParser.Literal_numberContext; -import ca.mcscert.jtet.parsers.MatlabParserParser.Id_plus_indexersContext; -import ca.mcscert.jtet.parsers.MatlabParserParser.Prefix_operatorContext; -import java.util.ArrayDeque; -import java.util.Deque; -import java.util.Map; - -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; - -/** - * - * @author matthew - */ -final public class MatlabParser { - - private MatlabParser() { - } - - public static Expression parseMatlabCode(VariableCollection variableListing, String matlabCode) { - // create a CharStream that reads from standard input - ANTLRInputStream input = new ANTLRInputStream(matlabCode + "\n"); - - // create a lexer that feeds off of input CharStream - MatlabParserLexer lexer = new MatlabParserLexer(input); - - // create a buffer of tokens pulled from the lexer - CommonTokenStream tokens = new CommonTokenStream(lexer); - - // create a parser that feeds off the tokens buffer - MatlabParserParser parser = new MatlabParserParser(tokens); - - ParseTree tree = parser.expression(); - ParseTreeWalker walker = new ParseTreeWalker(); - MatlabParserToExpressions listener = new MatlabParserToExpressions(variableListing.getVariablesAndEnumeratedValues()); - walker.walk(listener, tree); - - return listener.m_rootExpression; - } - - private static class MatlabParserToExpressions extends MatlabParserBaseListener implements ExpressionWithSubExpression { - - MatlabParserToExpressions(Map 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.Exponentiation; - } 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("~=")) { - return BinaryOperation.NotEquals; - } else if (text.equals("&&")) { - return BinaryOperation.BooleanAnd; - } else if (text.equals("||")) { - return BinaryOperation.BooleanOr; - } else { - throw new IllegalArgumentException("No such binary matlab operation defined (" + text + ")!"); - } - } - - private static UnaryOperation getUnaryOpForSymbol(String text) { - if (text.equals("~")) { - return UnaryOperation.Negation; - } else if (text.equals("-")) { - return UnaryOperation.Minus; - } else { - throw new IllegalArgumentException("No such unary matlab 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(); - if (ctx.LOG_OR().size() > 0) { - enqueHiddenOp(BinaryOperation.BooleanOr, ctx.LOG_OR().size()); - } - } - - @Override - public void enterE2(E2Context ctx) { - incrementLevel(); - if (ctx.LOG_AND().size() > 0) { - enqueHiddenOp(BinaryOperation.BooleanAnd, ctx.LOG_AND().size()); - } - } - - @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 enterE9(E9Context ctx) { - incrementLevel(); - } - - @Override - public void enterE10(E10Context ctx) { - incrementLevel(); - } - - @Override - public void enterE11(E11Context 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 exitE9(E9Context ctx) { - decrementLevel(); - } - - @Override - public void exitE10(E10Context ctx) { - decrementLevel(); - } - - @Override - public void exitE11(E11Context 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) { - addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null)); - } - - @Override - public void enterG4(G4Context ctx) { - addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null)); - } - @Override - public void enterPrefix_operator(Prefix_operatorContext ctx) { - addPrefixUnaryOperation(new ExpressionUnaryOperation(getUnaryOpForSymbol(ctx.getText()), null)); - } - - @Override - public void exitPrefix_operator(Prefix_operatorContext ctx) { - } - - @Override - public void enterLiteral_number(Literal_numberContext ctx) { - addExpressionValue(new Literal(ctx.getText())); - } - - @Override - public void enterId_plus_indexers(Id_plus_indexersContext ctx) { - addExpressionValue(m_variableParser.get(ctx.getText())); - } - - public Expression m_rootExpression; - private int m_level = 0; - private Map 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 m_opStack = new ArrayDeque(); - - 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 m_hiddenOpStack = new ArrayDeque(); - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.g4 b/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.g4 deleted file mode 100644 index ffddd18c512ac72e0853e2937ffa74fb729a04fc..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.g4 +++ /dev/null @@ -1,105 +0,0 @@ -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: IMPLIES; -g2: LOG_OR; -g3: LOG_AND; -g4: NEG; -g5: ( NEQ | EQ | GRTE | GRT | LSTE | LST ); -g6: ( PLUS | MINUS ); -g7: ( LEFTDIV | TIMES ); -g8: MINUS; -g9: EXPONENTIATION; - -// the hierarchy is defined from LOWEST to HIGHEST priority. - -expression : e0; - -e0 : e1 g1 e0 | e1; // Implies -e1 : e2 g2 e1 | e2; // Logic OR -e2 : e3 g3 e2 | e3; // Logc AND -e3 : g4 e4 | e4; // Logc NOT -e4 : e4 g5 e5 | e5; // Comparison -e5 : e5 g6 e6 | e6; // Addition/Subtraction -e6 : e6 g7 e7 | e7; // Multiplication/Division -e7 : g8 e8 | e8; // Unary Minus -e8 : e8 g9 e9 | e9; // note: in PVS, exponentiation is left-associative -e9 : 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 -// - -IMPLIES : '=>'; -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')+ ; diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.java b/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.java deleted file mode 100644 index d77896c3002b09e633fe5da5d2064588894e9046..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/PVSSimpleParser.java +++ /dev/null @@ -1,370 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers; - -import ca.mcscert.jtet.expression.BinaryOperation; -import ca.mcscert.jtet.expression.Expression; -import ca.mcscert.jtet.expression.ExpressionBinaryOperation; -import ca.mcscert.jtet.expression.ExpressionUnaryOperation; -import ca.mcscert.jtet.expression.ExpressionValue; -import ca.mcscert.jtet.expression.ExpressionWithSubExpression; -import ca.mcscert.jtet.expression.Literal; -import ca.mcscert.jtet.expression.UnaryOperation; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E0Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E1Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E2Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E3Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E4Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E5Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E6Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E7Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E8Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.E9Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G1Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G2Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G3Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G4Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G5Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G6Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G7Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G8Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.G9Context; -import ca.mcscert.jtet.parsers.PVSSimpleParserParser.IdContext; -import ca.mcscert.jtet.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(VariableCollection 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.getVariablesAndEnumeratedValues()); - walker.walk(listener, tree); - - return listener.m_rootExpression; - } - - private static class PVSParserToExpressions extends PVSSimpleParserBaseListener implements ExpressionWithSubExpression { - - PVSParserToExpressions(Map 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.Exponentiation; - } 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("/=")) { - return BinaryOperation.NotEquals; - } else if (text.equals("=>")) { - return BinaryOperation.Implies; - } 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 enterE9(E9Context 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 exitE9(E9Context 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) { - addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null)); - } - - @Override - public void enterG4(G4Context ctx) { - addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Negation, null)); // This is always negation. - } - - @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) { - addExpressionBinaryOperation(new ExpressionBinaryOperation(null, getBinaryOpForSymbol(ctx.getText()), null)); - } - - @Override - public void enterG8(G8Context ctx) { - addPrefixUnaryOperation(new ExpressionUnaryOperation(UnaryOperation.Minus, null)); // This is always minus. - } - - @Override - public void enterG9(G9Context 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 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 m_opStack = new ArrayDeque(); - - 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 m_hiddenOpStack = new ArrayDeque(); - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java b/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java deleted file mode 100644 index 52a6d22dda2e66dcafadf877a070b1326e6947ec..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParser.java +++ /dev/null @@ -1,173 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.EnumerationVariableType; -import ca.mcscert.jtet.expression.FixedPointVariableType; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.VariableParserParser.Bool_typeContext; -import ca.mcscert.jtet.parsers.VariableParserParser.DefaulttypeContext; -import ca.mcscert.jtet.parsers.VariableParserParser.Fixed_typeContext; -import ca.mcscert.jtet.parsers.VariableParserParser.Real_typeContext; -import ca.mcscert.jtet.parsers.VariableParserParser.VarContext; -import java.util.HashMap; -import java.util.HashSet; -import java.util.LinkedHashMap; -import java.util.Map; -import java.util.Set; - -import ca.mcscert.jtet.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; - -/** - * - * @author Matthew Dawson - */ -final public class VariableParser { - - public VariableCollection parseVariables(String variables) { - // create a CharStream that reads from standard input - ANTLRInputStream input = new ANTLRInputStream(variables) { - - @Override - public int LA(int i) { - return Character.toLowerCase(super.LA(i)); - } - - }; - - // create a lexer that feeds off of input CharStream - VariableParserLexer lexer = new VariableParserLexer(input); - - // create a buffer of tokens pulled from the lexer - CommonTokenStream tokens = new CommonTokenStream(lexer); - - // create a parser that feeds off the tokens buffer - VariableParserParser parser = new VariableParserParser(tokens); - - ParseTree tree = parser.varlist(); - ParseTreeWalker walker = new ParseTreeWalker(); - VariablesParserToVariables listener = new VariablesParserToVariables(); - walker.walk(listener, tree); - - return listener.m_variableCollection; - } - - public void addCustomType(String typeName, VariableType type) { - m_customTypes.put(typeName, type); - } - - private final Map m_customTypes = new HashMap(); - - private class VariablesParserToVariables extends VariableParserParserBaseListener { - private String currentName; - private VariableType currentType; - private limitingExpressionData currentLimitingExpression; - - @Override - public void enterVar(VarContext ctx) { - currentName = ctx.ID().getText(); - } - - @Override - public void enterDefaulttype(DefaulttypeContext ctx) { - currentType = new RealVariableType(); - } - - @Override - public void enterReal_type(Real_typeContext ctx) { - currentType = new RealVariableType(); - } - - @Override - public void enterBool_type(Bool_typeContext ctx) { - currentType = new BooleanVariableType(); - } - - @Override - public void enterUnknown_type(@NotNull VariableParserParser.Unknown_typeContext ctx) { - currentType = m_customTypes.get(ctx.UNKNOWN_TYPE().getText()); - if (currentType == null) { // Assume this unknown. For now, pretend a real is wanted. - currentType = new RealVariableType(); - } else if (currentType instanceof EnumerationVariableType) { - m_usedEnumerationTypes.add((EnumerationVariableType)currentType); - } - } - - @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; - int digits = Integer.parseInt(ctx.NAT(1).getText()); - int fractionPart = 0; - TerminalNode fractionNode; - if ((fractionNode = ctx.NAT(2)) != null) { - fractionPart = Integer.parseInt(fractionNode.getText()); - } - currentType = new FixedPointVariableType(signed, digits, fractionPart); - } - - @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 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())); - - VariableCollection variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes); - m_variables.get(limitingExpression.getKey()).type().setSubtypePredicate(PVSSimpleParser.parsePVSCode(variableCollection, subtypeExpression)); - - // Undo the variables hack, to avoid having unused variables bleed into the verification scripts! - m_variables.remove(subtypeVar); - } - - m_variableCollection = new VariableCollection(m_variables, m_usedEnumerationTypes); - } - - private Map m_variables = new LinkedHashMap(); - private Set m_usedEnumerationTypes = new HashSet(); - public VariableCollection m_variableCollection; - - private Map m_variableLimitingExpressions = new HashMap(); - } - private static class limitingExpressionData { - public String expression; - public String variableName; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserLexer.g4 b/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserLexer.g4 deleted file mode 100644 index 64b15663d6bb57e2e8f24be1033e3640e3e52a8c..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserLexer.g4 +++ /dev/null @@ -1,43 +0,0 @@ -lexer grammar VariableParserLexer; - -tokens { ID } - -fragment IDRule: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed. - -REGULAR_ID: IDRule -> type(ID), pushMode(VARIABLE_TYPE); - -fragment WS : [ \t\r\n]+; // skip spaces, tabs, newlines -WS1: WS -> skip ; - - -mode PVS_EXPR_MODE; -PVS_EXPR: ~[\{\}]+ -> popMode; - - -mode VARIABLE_TYPE; -VAR_SEPARATOR: ',' -> popMode; -COLON: ':'; -BOOL_TYPE: 'bool'; -REAL_TYPE: 'real'; -FIXEDT: 'fixedt' -> pushMode(FIXED_TYPE); -UNKNOWN_TYPE: [a-zA-Z_]+; - -OPEN_SUBTYPE: '{' -> pushMode(ID_FETCH); -PVS_EXPR_BEGIN: '|' -> pushMode(PVS_EXPR_MODE); -CLOSE_SUBTYPE: '}'; - -WS2: WS -> skip; - -mode FIXED_TYPE; -NAT_SEPARATOR: ','; -OPEN_BRACKET: '('; -CLOSE_BRACKET: ')' -> popMode; -NAT: [0-9]+; - -WS3: WS -> skip; - - -mode ID_FETCH; -SUBTYPE_ID: IDRule -> type(ID), popMode; - -WS4: WS -> skip; diff --git a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserParser.g4 b/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserParser.g4 deleted file mode 100644 index cd74b44da0fac5f37ed643c06454377f573efe8a..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/parsers/VariableParserParser.g4 +++ /dev/null @@ -1,32 +0,0 @@ -parser grammar VariableParserParser; -options { tokenVocab=VariableParserLexer; } - -varlist: var (VAR_SEPARATOR var)*; //Build list of variables -var: ID vartype; -vartype: ':' type_info - | defaulttype; - -defaulttype: ; - -type_info: simple_type_info - | '{' subtype '}'; - -subtype: subtype_var '|' pvs_expr; -subtype_var: ID subtype_vartype; -subtype_vartype: ':' simple_type_info - | defaulttype; -pvs_expr: PVS_EXPR; - -simple_type_info: bool_type - | real_type - | fixed_type - | unknown_type; - -bool_type: BOOL_TYPE; - -real_type: 'real'; - -fixed_type: 'fixedt' '(' NAT NAT_SEPARATOR NAT ')' - | 'fixedt' '(' NAT NAT_SEPARATOR NAT NAT_SEPARATOR NAT ')'; - -unknown_type: UNKNOWN_TYPE; diff --git a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunner.java b/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunner.java deleted file mode 100644 index 2b134328c6d304d31133a49c0ccfdb2f984513dc..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunner.java +++ /dev/null @@ -1,248 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator; -import ca.mcscert.jtet.tablularexpression.HierarchicalGrid; -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 java.io.BufferedReader; -import java.io.IOException; -import java.io.InputStreamReader; -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 - */ -final public class CheckerRunner { - public static List RunZ3(HierarchicalGrid grid, VariableCollection vars) { - List ret = new ArrayList(); - - // 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.getVariables().values()) { - GetValueRequestBuilder.append(var.name()).append(' '); - } - GetValueRequestBuilder.append("))\n"); - String GetValueRequestString = GetValueRequestBuilder.toString(); - - try { - String VarDef = new SMTLIBGenerator().GenerateVariablesDeclaration(vars); - 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("unknown")) { - // Z3 failed to prove. Throw a failure to check for now. - CheckerRunnerResult result = new CheckerRunnerResult(); - result.Query = query; - result.SampleValues = null; - 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 parseSMTLIBOutput(Reader reader) throws IOException { - if(reader.markSupported() == false) { - throw new IllegalArgumentException("Reader must support marks!"); - } - final Map ret = new HashMap(); - - StringBuilder input = new StringBuilder(); - - int bracketMismatch = 1; // This starts with a (, so we immediately have a a mismatch. - char nextChar = getNextChar(reader); - if (nextChar != '(') { // Should start with a ( for output. - throw new IllegalStateException("Bad input, wanted a ( to start, got " + nextChar); - } - input.append(nextChar); - while(bracketMismatch != 0) { - nextChar = getNextChar(reader); - switch (nextChar) { - case '(': - bracketMismatch++; - break; - case ')': - bracketMismatch--; - break; - } - input.append(nextChar); - } - - // Finally, clear the new line, so the output is now clear. - do { - reader.mark(5); - nextChar = getNextChar(reader); - } while(isWhitespace(nextChar) && nextChar != '\n'); - if(!isWhitespace(nextChar)) { - reader.reset(); - } - - ANTLRInputStream antlrInput = new ANTLRInputStream(input.toString()); - - // create a lexer that feeds off of input CharStream - SMTLibOutParserLexer lexer = new SMTLibOutParserLexer(antlrInput); - - // create a buffer of tokens pulled from the lexer - CommonTokenStream tokens = new CommonTokenStream(lexer); - - // create a parser that feeds off the tokens buffer - SMTLibOutParserParser parser = new SMTLibOutParserParser(tokens); - - ParseTree tree = parser.valuelist(); - ParseTreeWalker walker = new ParseTreeWalker(); - SMTLibOutParserListener listener = new SMTLibOutParserBaseListener() { - @Override - public void enterValue(@NotNull SMTLibOutParserParser.ValueContext ctx) { - id = ctx.ID().getText(); - value = ""; - } - - @Override - public void enterNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) { - value = "(- "; - } - - @Override - public void exitSingle(@NotNull SMTLibOutParserParser.SingleContext ctx) { - value += ctx.getText(); - } - - @Override - public void exitFraction(@NotNull SMTLibOutParserParser.FractionContext ctx) { - value += "(" + ctx.RATIONAL(0).getText() + " / " + ctx.RATIONAL(1).getText() + ")"; - } - - @Override - public void exitNegative(@NotNull SMTLibOutParserParser.NegativeContext ctx) { - value += ')'; - } - - @Override - public void exitExpr(@NotNull SMTLibOutParserParser.ExprContext ctx) { - ret.put(id, value); - } - - String id = ""; - String value; - }; - walker.walk(listener, tree); - 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; - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResult.java b/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResult.java deleted file mode 100644 index 798039459d3b5abc05e506dac4711a2f003b8f66..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResult.java +++ /dev/null @@ -1,51 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import java.util.Map; - -/** - * @author Matthew Dawson - */ -final public class CheckerRunnerResult { - public String Query; - public Map SampleValues; - - public String GenerateMatlabVariableDeclarations() { - StringBuilder ret = new StringBuilder(); - for(Map.Entry var: SampleValues.entrySet()) { - ret. - append(var.getKey()). - append(" = "). - append(var.getValue()). - append(";\n"); - } - return ret.toString(); - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGenerator.java b/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGenerator.java deleted file mode 100644 index 1566bcc5c915f335dfdf796f78b5deae2c1cb01b..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGenerator.java +++ /dev/null @@ -1,174 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.MatlabParser; -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import ca.mcscert.jtet.tablularexpression.Cell; -import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerGenerator; -import org.apache.commons.lang3.StringUtils; - -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Deque; -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -final public class HierarchicalGridSMTLIBGenerator implements HierarchcialGridCheckerGenerator { - - public HierarchicalGridSMTLIBGenerator(VariableCollection variableDefinitions) { - m_variableDefinitions = variableDefinitions; - } - - private String generateQueryPrefix() { - if (!m_parentCellsCVC3Code.isEmpty()){ - String output = "(and "; - output += StringUtils.join(m_parentCellsCVC3Code, " ") + " "; - return output; - } - return "(and true "; - } - - private void outputCells() { - // First is disjoint testing. - m_output += "(push 1)\n"; - - String query = "(assert "; - query += generateQueryPrefix(); - if (m_currentDisjointQueries.isEmpty()) { - query += "false"; - } else if (m_currentDisjointQueries.size() == 1) { - query += m_currentDisjointQueries.get(0); - } else { - query += "(or " + StringUtils.join(m_currentDisjointQueries, '\n') + ")"; - } - query += "))"; - m_queries.add(query); - m_output += query + "\n"; - - m_output += "(check-sat)\n(pop 1)\n"; - - // Next is complete. - m_output += "(push 1)\n"; - - query = "(assert "; - query += generateQueryPrefix(); - query += "(not "; - if (m_currentCompleteQueries.isEmpty()) { - query += "true"; - } else if (m_currentCompleteQueries.size() == 1) { - query += m_currentCompleteQueries.get(0); - } else { - query += "(or " + StringUtils.join(m_currentCompleteQueries, " ") + ")"; - } - query += ")))"; - m_queries.add(query); - m_output += query + "\n"; - - m_output += "(check-sat)\n(pop 1)\n"; - - m_currentlyRunning = false; - - // And finally clear the running list of current queries. - m_currentCompleteQueries.clear(); - m_currentDisjointQueries.clear(); - } - - @Override - public void descendIntoGridFromCell(Cell cell) { - if (m_currentlyRunning) { - outputCells(); - } - m_parentCellsCVC3Code.addFirst(MatlabParser.parseMatlabCode(m_variableDefinitions, cell.contents()).getCheckerOutput(m_CVC3Generator, m_booleanType)); - m_currentlyRunning = true; - } - - @Override - public void ascendFromGrid() { - if (m_currentlyRunning) { - outputCells(); - } - m_parentCellsCVC3Code.removeFirst(); - } - - @Override - public void handleEdgeCell(Cell cell) { - handleLeafCell(cell); - } - - @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); - - // Next form the disjoint queries and add to the list. - for(String otherCellCode : m_currentCompleteQueries) { - String newDisjointQuery = "(and " + otherCellCode + " " + newCellCode + ")"; - m_currentDisjointQueries.add(newDisjointQuery); - } - - // Lastly add the cell to the list for the complete query - m_currentCompleteQueries.add(newCellCode); - } - - @Override - public String getFinalString() { - if (m_currentlyRunning) { - outputCells(); - } - return m_output; - } - - public List getFinalQueries() { - if (m_currentlyRunning) { - outputCells(); - } - return m_queries; - } - - Deque m_parentCellsCVC3Code = new ArrayDeque(); - - List m_currentDisjointQueries = new ArrayList(); - List m_currentCompleteQueries = new ArrayList(); - - boolean m_currentlyRunning = true; - - String m_output = ""; - List m_queries = new ArrayList(); - - // To fix properly. - VariableCollection m_variableDefinitions; - static BooleanVariableType m_booleanType = new BooleanVariableType(); - SMTLIBGenerator m_CVC3Generator = new SMTLIBGenerator(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLibOutParser.g4 b/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLibOutParser.g4 deleted file mode 100644 index 9899bdb19206df2093e74ac51d576ce7e6f3764c..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/smtlibchecker/SMTLibOutParser.g4 +++ /dev/null @@ -1,17 +0,0 @@ -grammar SMTLibOutParser; - -valuelist: '(' value+ ')'; //Build list of variables -value: '(' ID expr ')'; - -expr: single | - fraction | - negative; - -negative: '(-' fraction ')' | - '(-' single ')'; -single: RATIONAL; -fraction: '(/' RATIONAL RATIONAL ')'; - -ID: [a-zA-Z][a-zA-Z0-9]*; //Variable identifier. Start with letter, then alpha numerical allowed. -RATIONAL: [0-9]+('.'[0-9]+)?; -WS : [ \t\r\n]+ -> skip ; // skip spaces, tabs, newlines diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/Cell.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/Cell.java deleted file mode 100644 index 2f51df4cc3a5db75d195164a7caa71e331c3b473..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/Cell.java +++ /dev/null @@ -1,26 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.tablularexpression; - -/** - * - * @author Matthew Dawson - */ -public class Cell { - Cell() {} - Cell(String initialContents) { - m_contents = initialContents; - } - - public void setContents(String contents) { - m_contents = contents; - } - - public String contents() { - return m_contents; - } - - private String m_contents; -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerGenerator.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerGenerator.java deleted file mode 100644 index 7679357206ac374539baee8a915d6c4d7c534fed..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerGenerator.java +++ /dev/null @@ -1,43 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression; - -/** - * - * @author Matthew Dawson - */ -public interface HierarchcialGridCheckerGenerator { - void descendIntoGridFromCell(Cell cell); - void ascendFromGrid(); - - void handleLeafCell(Cell cell); - void handleEdgeCell(Cell cell); - - String getFinalString(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerWalkerGenerator.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerWalkerGenerator.java deleted file mode 100644 index d8c39ac570fc8eb1a784ea75f7fa3ff6fe3e8f04..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchcialGridCheckerWalkerGenerator.java +++ /dev/null @@ -1,66 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression; - -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -public class HierarchcialGridCheckerWalkerGenerator { - - private static void HandleGrid(SubHierarchyFetcher grid, HierarchcialGridCheckerGenerator generator) { - List cells = grid.getSubHiearchy(); - for (int i = 0; i < cells.size(); ++i) { - HierarchicalCell cell = cells.get(i); - - if (cell.getSubHiearchy().isEmpty()) { - generator.handleLeafCell(cell); - } else { - generator.handleEdgeCell(cell); - } - } - - for (int i = 0; i < cells.size(); ++i) { - HierarchicalCell cell = cells.get(i); - - if (!cell.getSubHiearchy().isEmpty()) { - generator.descendIntoGridFromCell(cell); - HandleGrid(cell, generator); - generator.ascendFromGrid(); - } - } - } - - public static String GenerateCheckerFromGrid(HierarchicalGrid grid, HierarchcialGridCheckerGenerator generator) { - HandleGrid(grid, generator); - return generator.getFinalString(); - } -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalCell.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalCell.java deleted file mode 100644 index 3e8ba6cb653d3069a62d64e8b92f5474301266a8..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalCell.java +++ /dev/null @@ -1,26 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.tablularexpression; - -import java.util.ArrayList; -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -public class HierarchicalCell extends Cell implements SubHierarchyFetcher { - public HierarchicalCell() {} - public HierarchicalCell(String initialContents) { - super(initialContents); - } - - @Override - public List getSubHiearchy() { - return m_subHiearchy; - } - - private List m_subHiearchy = new ArrayList(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGrid.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGrid.java deleted file mode 100644 index ea5e9bfd20728351377f8abc683f2f6843699864..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/HierarchicalGrid.java +++ /dev/null @@ -1,21 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.tablularexpression; - -import java.util.ArrayList; -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -public class HierarchicalGrid implements SubHierarchyFetcher { - @Override - public List getSubHiearchy() { - return m_subHiearchy; - } - - private List m_subHiearchy = new ArrayList(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/SubHierarchyFetcher.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/SubHierarchyFetcher.java deleted file mode 100644 index de0849a5c278bf3723eb93409bacdd5524fd74d1..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/SubHierarchyFetcher.java +++ /dev/null @@ -1,39 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression; - -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -public interface SubHierarchyFetcher { - List getSubHiearchy(); -} diff --git a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/TwoDimensionalGrid.java b/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/TwoDimensionalGrid.java deleted file mode 100644 index db3ca2d1c4835a9827fd3b14662e031bb37e95c6..0000000000000000000000000000000000000000 --- a/jTET/src/main/java/ca/mcscert/jtet/tablularexpression/TwoDimensionalGrid.java +++ /dev/null @@ -1,90 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression; - -import java.util.ArrayList; -import java.util.List; - -/** - * - * @author Matthew Dawson - */ -public final class TwoDimensionalGrid { - // Creates a 1x1 grid. - public TwoDimensionalGrid() { - this(1, 1); - } - - public TwoDimensionalGrid(int sizeX, int sizeY) { - resize(sizeX, sizeY); - - } - - // Note that this class assumes the grid is never empty. - // Whenever logically possible, cell contents are preserved at the correct location. - public void resize(int sizeX, int sizeY) { - if (sizeX <= 0 || sizeY <= 0) { - throw new IllegalArgumentException("This grid must have positive sizes in both dimensions! Given (" + - sizeX + ", " + sizeY + ")."); - } - if (m_grid.size() > sizeX) { - m_grid.subList(sizeX, m_grid.size()).clear(); - } else { - while(m_grid.size() != sizeX) { - m_grid.add(new ArrayList()); - } - } - for(int i = 0; i < sizeX; ++i) { - List currentList = m_grid.get(i); - if(currentList.size() > sizeY) { - currentList.subList(sizeY, currentList.size()).clear(); - } else { - while(currentList.size() != sizeY) { - currentList.add(new Cell()); - } - } - } - } - - public int sizeX() { - return m_grid.size(); - } - - public int sizeY() { - return m_grid.get(0).size(); - } - - public Cell get(int x, int y) { - return m_grid.get(x).get(y); - } - - // Indexed as m_grid[x][y], for reasons. All access should be hidden behind api, so that can be changed if - // performance suffers. - private List> m_grid = new ArrayList>(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java b/jTET/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java deleted file mode 100644 index 8ea977774e15f07d6de2a7f523f259d5b1c9e7d8..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/cvc3generator/HierarchicalGridCVC3GeneratorTest.java +++ /dev/null @@ -1,105 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.cvc3generator; - -import ca.mcscert.jtet.parsers.VariableParser; -import ca.mcscert.jtet.tablularexpression.HierarchicalCell; -import ca.mcscert.jtet.tablularexpression.HierarchicalGrid; -import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator; -import java.util.List; -import static org.junit.Assert.*; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -/** - * - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class HierarchicalGridCVC3GeneratorTest { - - // Exercise the cvc3 generator using a table designed in matlab. - @Test - public void exerciseCVC3Generator() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("0 > x")); - - List nextGrid = topCells.get(1).getSubHiearchy(); - nextGrid.add(new HierarchicalCell("z > 0")); - nextGrid.add(new HierarchicalCell("z == 0")); - nextGrid.add(new HierarchicalCell("0 > z")); - - nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0")); - - String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridCVC3Generator(variableParser.parseVariables("x,z"), 1)); - - String expected = "ECHO \"begin1\";\n"+ -"PUSH;\n"+ -"QUERY (NOT ( (x > 0) AND (x = 0) ) AND\n"+ -"NOT ( (x > 0) AND (0 > x) ) AND\n"+ -"NOT ( (x = 0) AND (0 > x) ));\n"+ -"POP;\n"+ -"ECHO \"end1\";\n"+ -"ECHO \"begin2\";\n"+ -"PUSH;\n"+ -"QUERY ((x > 0) OR (x = 0) OR (0 > x));\n"+ -"POP;\n"+ -"ECHO \"end2\";\n"+ -"ECHO \"begin3\";\n"+ -"PUSH;\n"+ -"QUERY ((x = 0)) => (NOT ( (z > 0) AND (z = 0) ) AND\n"+ -"NOT ( (z > 0) AND (0 > z) ) AND\n"+ -"NOT ( (z = 0) AND (0 > z) ));\n"+ -"POP;\n"+ -"ECHO \"end3\";\n"+ -"ECHO \"begin4\";\n"+ -"PUSH;\n"+ -"QUERY ((x = 0)) => ((z > 0) OR (z = 0) OR (0 > z));\n"+ -"POP;\n"+ -"ECHO \"end4\";\n"+ -"ECHO \"begin5\";\n"+ -"PUSH;\n"+ -"QUERY ((z = 0) AND (x = 0)) => ();\n"+ -"POP;\n"+ -"ECHO \"end5\";\n"+ -"ECHO \"begin6\";\n"+ -"PUSH;\n"+ -"QUERY ((z = 0) AND (x = 0)) => ((z = 0));\n"+ -"POP;\n"+ -"ECHO \"end6\";\n"; - assertEquals(expected, out); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/CVC3GeneratorTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/CVC3GeneratorTest.java deleted file mode 100644 index 0bb77de328c1b5540bee18235956edd351b083bf..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/CVC3GeneratorTest.java +++ /dev/null @@ -1,37 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; -import static org.junit.Assert.*; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class CVC3GeneratorTest { - /** - * Test of addition operation. - */ - @Test - public void testAdditionOpConverstion() { - BinaryOperation op = BinaryOperation.Addition; - assertEquals("+", CVC3Generator.ConvertToOutputOp(op, new RealVariableType())); - assertEquals("BVPLUS(13,", CVC3Generator.ConvertToOutputOp(op, new FixedPointVariableType(true, 13, 5))); - } - /** - * Test of literals containing decimals. - * - * All decimals must be represented as fractions. Ensure that this happens. - */ - @Test - public void testLiteralRationalsAreFractions() { - Literal literal = new Literal("4.56"); - assertEquals("(456/100)", literal.getCheckerOutput(new CVC3Generator(), new RealVariableType())); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/EnumerationVariableTypeGenerationTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/EnumerationVariableTypeGenerationTest.java deleted file mode 100644 index 05f5f5e136b4b1f8e7ed11ff9c29fbc80f145379..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/EnumerationVariableTypeGenerationTest.java +++ /dev/null @@ -1,105 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import ca.mcscert.jtet.parsers.PVSSimpleParser; -import ca.mcscert.jtet.parsers.VariableParser; -import org.junit.Before; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import java.util.Arrays; -import java.util.Collection; - -import static org.junit.Assert.*; - -/** - * @author Matthew Dawson - */ -@RunWith(Parameterized.class) -public class EnumerationVariableTypeGenerationTest { - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - {new SMTLIBGenerator(), - "(= x e1)", - "(distinct x e1)", - }, - {new CVC3Generator(), - "(x = e1)", - "(x /= e1)", - } - }); - } - - static private VariableType outputType = new BooleanVariableType(); - - @Parameter(value = 0) - public CheckerGenerator generator; - - @Parameter(value = 1) - public String EqualExpectedOutput; - - @Parameter(value = 2) - public String NotEqualExpectedOutput; - - @Before - public void setUp() throws Exception { - EnumerationVariableType enumType = new EnumerationVariableType("enum"); - enumType.enumerationValues().add("e1"); - - variableParser.addCustomType("enum", enumType); - } - - @Test - public void EqualTest() { - VariableCollection vars = variableParser.parseVariables("x:enum"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, "x = e1"); - assertEquals(EqualExpectedOutput, expr.getCheckerOutput(generator, outputType)); - } - - @Test - public void NotEqualTest() { - VariableCollection vars = variableParser.parseVariables("x:enum"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, "x /= e1"); - assertEquals(NotEqualExpectedOutput, expr.getCheckerOutput(generator, outputType)); - } - - @Test(expected=IllegalArgumentException.class) - public void OtherOperatorsFailTest() { - VariableCollection vars = variableParser.parseVariables("x:enum"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, "x + e1"); - expr.getCheckerOutput(generator, vars.getVariables().get("x").type()); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/FixedPointVariableTypeTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/FixedPointVariableTypeTest.java deleted file mode 100644 index 798099011956ce4af712023601e517fa4cc0fba5..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/FixedPointVariableTypeTest.java +++ /dev/null @@ -1,59 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import static org.junit.Assert.*; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class FixedPointVariableTypeTest { - /** - * Test of constructor in class FixedPointType. - */ - @Test - public void testConstructor() { - FixedPointVariableType instance = new FixedPointVariableType(true, 19, 9); - assertEquals(true, instance.isSigned()); - assertEquals(19, instance.digits()); - assertEquals(9, instance.fractionPart()); - } - /** - * Test of getCVC3Definition method, of class FixedPointType. - */ - @Test - public void testGetCVC3Definition() { - CVC3Generator generator = new CVC3Generator(); - FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8); - assertEquals("BITVECTOR(16)", generator.GenerateVariableType(instance)); - } - - /** - * Test of canCastToType method, of class FixedPointType. - */ - @Test - public void testCanCastToType() { - FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8); - assertFalse(instance.canCastToType(new RealVariableType())); - } - - /** - * Test of equals method, of class FixedPointType. - */ - @Test - public void testEquals() { - FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8); - assertEquals(new FixedPointVariableType(true, 16, 8), instance); - assertFalse(instance.equals(new FixedPointVariableType(false, 16, 8))); - assertFalse(instance.equals(new FixedPointVariableType(true, 15, 8))); - assertFalse(instance.equals(new FixedPointVariableType(true, 16, 7))); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/GenericOperationGeneratorTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/GenericOperationGeneratorTest.java deleted file mode 100644 index facd05c04e1deb45de685e7fcaf2100d2e132e5a..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/GenericOperationGeneratorTest.java +++ /dev/null @@ -1,107 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import ca.mcscert.jtet.parsers.PVSSimpleParser; -import ca.mcscert.jtet.parsers.VariableParser; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import java.util.Arrays; -import java.util.Collection; - -import static org.junit.Assert.*; - -/** - * @author Matthew Dawson - */ -@RunWith(Parameterized.class) -public class GenericOperationGeneratorTest { - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - {new SMTLIBGenerator(), - "(=> (or (= (* x 5.0) (/ 1.0 (- 4.0))) (or (and (> x (+ 8.0 3.0)) (< 9.0 (- x 2.0))) (or (>= x 12.0) (or (not (<= 34.0 (- x))) (> 5.0 4.0))))) (distinct x 5.0))", - null, - null}, - {new CVC3Generator(), - "((((x * 5) = (1 / (- 4))) OR (((x > (8 + 3)) AND (9 < (x - 2))) OR ((x >= 12) OR ((NOT (34 <= (- x))) OR (5 > 4))))) => (x /= 5))", - "(((BVMULT(8,x,0bin00010100) = BVSDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVSGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVSLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVSGE(x,0bin00110000) OR ((NOT BVSLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))", - "(((BVMULT(8,x,0bin00010100) = BVUDIV(0bin00000100,BVUMINUS(0bin00010000))) OR ((BVGT(x,BVPLUS(8,0bin00100000,0bin00001100)) AND BVLT(0bin00100100,BVSUB(x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))" - } - }); - } - - static private String query = "(x * 5) = (1 / -4) OR ((x > (8 + 3)) AND (9 < x - 2)) OR x >= 12 OR NOT (34 <= -x) OR (5 > 4) => (x /= 5)"; - static private VariableType outputType = new BooleanVariableType(); - - @Parameter(value = 0) - public CheckerGenerator generator; - - @Parameter(value = 1) - public String RealExpectedOutput; - - @Parameter(value = 2) - public String SignedFixedPointExpectedOutput; - - @Parameter(value = 3) - public String UnsignedFixedPointExpectedOutput; - - @Test - public void RealTest() { - if (RealExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, query); - assertEquals(RealExpectedOutput, expr.getCheckerOutput(generator, outputType)); - } - } - - @Test - public void SignedFixedPointTest() { - if (SignedFixedPointExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:fixedt(1, 8, 2)"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, query); - assertEquals(SignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType)); - } - } - - @Test - public void UnsignedFixedPointTest() { - if (UnsignedFixedPointExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:fixedt(0, 8, 2)"); - Expression expr = PVSSimpleParser.parsePVSCode(vars, query); - assertEquals(UnsignedFixedPointExpectedOutput, expr.getCheckerOutput(generator, outputType)); - } - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/GenericVariableDeclarationGeneratorTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/GenericVariableDeclarationGeneratorTest.java deleted file mode 100644 index b6716e3fcfd80f2ee807633d8cd46a4874858ce2..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/GenericVariableDeclarationGeneratorTest.java +++ /dev/null @@ -1,155 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression; - -import ca.mcscert.jtet.parsers.VariableParser; -import org.junit.Before; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import java.util.*; - -import static org.junit.Assert.*; - -/** - * @author Matthew Dawson - */ -@RunWith(Parameterized.class) -public class GenericVariableDeclarationGeneratorTest { - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - {new SMTLIBGenerator(), - "(declare-fun x () Real)\n", - null, - null, - "(declare-sort MyEnum 0)\n" + - "(declare-fun e1 () MyEnum)\n" + - "(declare-fun e2 () MyEnum)\n" + - "(declare-fun e3 () MyEnum)\n" + - "(assert (distinct e1 e2 e3))\n" + - "(define-fun isMyEnum ((val MyEnum)) Bool (or (= val e1) (= val e2) (= val e3)))\n" + - "(declare-fun x () MyEnum)\n" + - "(assert (isMyEnum x))\n", - "(declare-sort MyEnum 0)\n" + - "(declare-fun e1 () MyEnum)\n" + - "(declare-fun e2 () MyEnum)\n" + - "(declare-fun e3 () MyEnum)\n" + - "(assert (distinct e1 e2 e3))\n" + - "(define-fun isMyEnum ((val MyEnum)) Bool (or (= val e1) (= val e2) (= val e3)))\n" + - "(declare-fun x () MyEnum)\n" + - "(assert (isMyEnum x))\n" + - "(declare-fun y () MyEnum)\n" + - "(assert (isMyEnum y))\n" - }, - {new CVC3Generator(), - "x:REAL;\n", - "x:BITVECTOR(8);\n", - "x:BITVECTOR(8);\n", - "DATATYPE\n MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\n", - "DATATYPE\n MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\ny:MyEnum;\n" - } - }); - } - @Parameter(value = 0) - public CheckerGenerator generator; - - @Parameter(value = 1) - public String RealExpectedOutput; - - @Parameter(value = 2) - public String SignedFixedPointExpectedOutput; - - @Parameter(value = 3) - public String UnsignedFixedPointExpectedOutput; - - @Parameter(value = 4) - public String SingleVariableSingleEnumerationExpectedOutput; - - @Parameter(value = 5) - public String MultipleVariableSingleEnumerationExpectedOutput; - - @Test - public void RealTest() { - if (RealExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x"); - assertEquals(RealExpectedOutput, generator.GenerateVariablesDeclaration(vars)); - } - } - - @Test - public void SignedFixedPointTest() { - if (SignedFixedPointExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:fixedt(1, 8, 2)"); - assertEquals(SignedFixedPointExpectedOutput, generator.GenerateVariablesDeclaration(vars)); - } - } - - @Test - public void UnsignedFixedPointTest() { - if (UnsignedFixedPointExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:fixedt(0, 8, 2)"); - assertEquals(UnsignedFixedPointExpectedOutput, generator.GenerateVariablesDeclaration(vars)); - } - } - - @Test - public void SingleVariableSingleEnumerationTest() { - if (SingleVariableSingleEnumerationExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:MyEnum"); - assertEquals(SingleVariableSingleEnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars)); - } - } - - // This ensures that the enumeration definition is only emitted once. Other variable generations don't have this, - // as they don't emit type information. - @Test - public void MultipleVariableSingleEnumerationTest() { - if (MultipleVariableSingleEnumerationExpectedOutput != null) { - VariableCollection vars = variableParser.parseVariables("x:MyEnum, y:MyEnum"); - - assertEquals(MultipleVariableSingleEnumerationExpectedOutput, generator.GenerateVariablesDeclaration(vars)); - } - } - - @Before - public void SetupVariableParser() { - EnumerationVariableType myEnum = new EnumerationVariableType("MyEnum"); - myEnum.enumerationValues().add("e1"); - myEnum.enumerationValues().add("e2"); - myEnum.enumerationValues().add("e3"); - - variableParser.addCustomType("MyEnum", myEnum); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/MatlabExpressionBinaryOperationTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/MatlabExpressionBinaryOperationTest.java deleted file mode 100644 index 2cda25edb2402d7f0c1b1958a1a3959704f4f39d..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/MatlabExpressionBinaryOperationTest.java +++ /dev/null @@ -1,128 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import static org.junit.Assert.*; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class MatlabExpressionBinaryOperationTest { - /** - * Test of type method, of class ExpressionBinaryOperation. - */ - @Test - public void testWithSimpleRealVariablesAddedTogether() { - Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType()); - ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r); - - String CVC3Output = "(a + b)"; - VariableType expressionType = new RealVariableType(); - - assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType)); - assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType)); - } - /** - * Test of type method, of class ExpressionBinaryOperation. - */ - @Test - public void testWithSimpleFixedPointVariablesAddedTogether() { - Variable l = new Variable("a", new FixedPointVariableType(true, 17, 4)), r = new Variable("b", new FixedPointVariableType(true, 17, 4)); - ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r); - - String CVC3Output = "BVPLUS(17,a,b)"; - VariableType expressionType = new FixedPointVariableType(true, 17, 4); - - assertEquals(CVC3Output, instance.getCheckerOutput(generator, expressionType)); - assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType)); - } - /** - * Test of setLHS/RHS, verify they set variables correctly. - */ - @Test - public void testSettingsLHSAndRHS() { - Variable l = new Variable("a", new RealVariableType()), r = new Variable("b", new RealVariableType()); - ExpressionBinaryOperation instance = new ExpressionBinaryOperation(l, BinaryOperation.Addition, r); - - //Reverse a+b to b+a. - instance.setLHS(r); - instance.setRHS(l); - - String CVC3Output = "(b + a)"; - VariableType expressionType = new RealVariableType(); - - assertEquals(expressionType, instance.actualOutputTypeForRequestedOutput(expressionType)); - assertEquals(CVC3Output, instance.getCheckerOutput(new CVC3Generator(), expressionType)); - } - - /** - * Test when RHS/LHS have different castable types. - */ - @Test - public void testCastableTypes() { - Literal lit = new Literal("5"); - Variable var = new Variable("A", new RealVariableType()); - VariableType exprType; - - // Test when adding a Real var to a lit, type always becomes Real. - exprType = new RealVariableType(); - assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Addition, var).actualOutputTypeForRequestedOutput(exprType)); - assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Addition, lit).actualOutputTypeForRequestedOutput(exprType)); - - // Test when comparing a Real var to a lit, type always becomes boolean. - exprType = new BooleanVariableType(); - assertEquals(exprType, new ExpressionBinaryOperation(lit, BinaryOperation.Equals, var).actualOutputTypeForRequestedOutput(exprType)); - assertEquals(exprType, new ExpressionBinaryOperation(var, BinaryOperation.Equals, lit).actualOutputTypeForRequestedOutput(exprType)); - } - - /** - * Test operations changing types (== doing REAL+REAL -> BOOLEAN) - */ - @Test - public void testCastingOperations() { - Literal l = new Literal("5"), r = new Literal("6"); - ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r); - - // Test when adding a Real var to a lit, type always becomes Real. - VariableType expressionType = new BooleanVariableType(); - assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType)); - assertEquals("(5 = 6)", exp.getCheckerOutput(generator, expressionType)); - } - - /** - * Test operations fails when a requested type is invalid! - */ - @Test(expected=IllegalArgumentException.class) - public void testInvalidOutputType() { - Literal l = new Literal("5"), r = new Literal("6"); - ExpressionBinaryOperation exp = new ExpressionBinaryOperation(l, BinaryOperation.Equals, r); - - exp.getCheckerOutput(generator, new RealVariableType()); //Returns a boolean, so will fail. - } - - /** - * Test doing multiple boolean operations AND'd together. - */ - @Test - public void testBooleanAndFromComparision() { - Expression l = new Variable("a", new RealVariableType()), r = new Literal("6"), - l2 = new Variable("b", new RealVariableType()), r2 = new Literal("8"); - ExpressionBinaryOperation exp = new ExpressionBinaryOperation(new ExpressionBinaryOperation(l, BinaryOperation.Equals, r), - BinaryOperation.BooleanAnd, - new ExpressionBinaryOperation(l2, BinaryOperation.Equals, r2)); - - // Test when adding a Real var to a lit, type always becomes Real. - VariableType expressionType = new BooleanVariableType(); - assertEquals(expressionType, exp.actualOutputTypeForRequestedOutput(expressionType)); - assertEquals("((a = 6) AND (b = 8))", exp.getCheckerOutput(generator, expressionType)); - } - - CheckerGenerator generator = new CVC3Generator(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/VariableTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/VariableTest.java deleted file mode 100644 index a4511d35344557c7a7538a81bf01001d19623d86..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/VariableTest.java +++ /dev/null @@ -1,83 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression; - -import static org.hamcrest.CoreMatchers.is; -import static org.junit.Assert.*; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.HashMap; -import java.util.Map; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class VariableTest { - @Test - public void exerciseVariable() { - String name = "Var"; - VariableType type = new RealVariableType(); - - Variable var = new Variable(name, type); - - assertSame(name, var.name()); - assertSame(type, var.type()); - assertEquals(name, var.getCheckerOutput(null, new RealVariableType())); - - Map varList = new HashMap(); - varList.put(name, var); - VariableCollection variableCollection = new VariableCollection(varList); - - CheckerGenerator generator = new CVC3Generator(); - assertEquals(name+":REAL;\n", generator.GenerateVariablesDeclaration(variableCollection)); - - generator = new SMTLIBGenerator(); - assertEquals("(declare-fun " +name+ " () Real)\n", generator.GenerateVariablesDeclaration(variableCollection)); - } - - @Test - public void testSubtypePredicate() { - // Construct a basic variable. Assume it is correct due to the above test. - Variable var = new Variable("var", new RealVariableType()); - - // Next create a subtype predicate. For now, make it work over positive reals (excluding 0) - Expression predicate = new ExpressionBinaryOperation(var, BinaryOperation.GreaterThen, new Literal("0")); - var.type().setSubtypePredicate(predicate); - - // Verify the predicate took. - assertThat(var.type().subtypePredicate(), is(predicate)); - - // Make a variable list for the generators. - Map varList = new HashMap(); - varList.put("var", var); - VariableCollection variableCollection = new VariableCollection(varList); - - CheckerGenerator generator = new CVC3Generator(); - String varDecl = generator.GenerateVariablesDeclaration(variableCollection); - - assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n")); - - generator = new SMTLIBGenerator(); - varDecl = generator.GenerateVariablesDeclaration(variableCollection); - - assertThat(varDecl, is("(declare-fun var () Real)\n(assert (> var 0.0))\n")); - } - - // Verify handling of invalid type to getCheckerOutput - @Test(expected=IllegalArgumentException.class) - public void testInvalidOutputType() { - String name = "Var"; - VariableType type = new BooleanVariableType(); - - Variable var = new Variable(name, type); - - var.getCheckerOutput(null, new RealVariableType()); //Returns a boolean, so will fail. - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/test/BooleanVariableTypeTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/test/BooleanVariableTypeTest.java deleted file mode 100644 index 500b1482549373f2cabffbe682083a9b454a0091..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/test/BooleanVariableTypeTest.java +++ /dev/null @@ -1,79 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression.test; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import org.junit.Test; -import static org.junit.Assert.*; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class BooleanVariableTypeTest { - - /** - * Test of getCVC3Definition method, of class RealVariableType. - */ - @Test - public void testGetCVC3Definition() { - CVC3Generator generator = new CVC3Generator(); - String variableName = "test_variable"; - BooleanVariableType instance = new BooleanVariableType(); - String expResult = "BOOLEAN"; - String result = generator.GenerateVariableType(instance); - assertEquals(expResult, result); - } - - /** - * Test of SMT-LIB generation of boolean type. - */ - @Test - public void testGetSMTLIBDefinition() { - SMTLIBGenerator generator = new SMTLIBGenerator(); - String variableName = "test_variable"; - BooleanVariableType instance = new BooleanVariableType(); - String expResult = "Bool"; - String result = generator.GenerateVariableType(instance); - assertEquals(expResult, result); - } - - /** - * Test of equals method, of class RealVariableType. - */ - @Test - public void testEquals() { - BooleanVariableType test = new BooleanVariableType(); - assertTrue(test.equals(new BooleanVariableType())); - assertTrue(test.equals(test)); - assertFalse(test.equals(new Object())); - } - - /** - * Test of hashCode method, of class RealVariableType. - */ - @Test - public void testHashCode() { - BooleanVariableType instance = new BooleanVariableType(); - assertEquals(0, instance.hashCode()); - } - - /** - * Test of canCastToType method, of class RealVariableType. Reals (for now) - * don't cast. - */ - @Test - public void testCanCastToType() { - BooleanVariableType instance = new BooleanVariableType(); - assertFalse(instance.canCastToType(new RealVariableType())); - assertFalse(instance.canCastToType(new BooleanVariableType())); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/test/MatlabLiteralTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/test/MatlabLiteralTest.java deleted file mode 100644 index 490127ea125dedb7b9d3e92e5d5b1b76b194cf8a..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/test/MatlabLiteralTest.java +++ /dev/null @@ -1,63 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression.test; - -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.CheckerGenerator; -import ca.mcscert.jtet.expression.FixedPointVariableType; -import ca.mcscert.jtet.expression.Literal; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.VariableType; -import org.junit.Test; -import static org.junit.Assert.*; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class MatlabLiteralTest { - /** - * Test of canHandleOutputType method, of class Literal. - */ - @Test - public void testType() { - Literal instance = new Literal(null); - VariableType exprType = new RealVariableType(); - assertEquals(exprType, instance.actualOutputTypeForRequestedOutput(exprType)); - } - - /** - * Test of getCVC3Output method, of class Literal. Test only natural numbers; - */ - @Test - public void testGetCVC3Output() { - Literal instance = new Literal("5"); - assertEquals("5", instance.getCheckerOutput(generator, new RealVariableType())); - assertEquals("0bin00101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0))); - assertEquals("0bin01010", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1))); - } - - /** - * Test of getCVC3Output method, of class Literal. Test fun fixed point number; - */ - @Test - public void testCVC3OutputOnInterestingFixedPoint() { - Literal instance = new Literal("0"); - assertEquals("0bin00000", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1))); - - instance = new Literal("5.5"); - assertEquals("0bin01011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1))); - - instance = new Literal("-5.5"); - assertEquals("0bin10101", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 1))); - - instance = new Literal("-5"); - assertEquals("0bin11011", instance.getCheckerOutput(generator, new FixedPointVariableType(true, 5, 0))); - } - CheckerGenerator generator = new CVC3Generator(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/test/RealVariableTypeTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/test/RealVariableTypeTest.java deleted file mode 100644 index fcaead09e6ae413bb84eadd888372b924ea87958..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/test/RealVariableTypeTest.java +++ /dev/null @@ -1,79 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.expression.test; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import org.junit.Test; -import static org.junit.Assert.*; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class RealVariableTypeTest { - - /** - * Test of getCVC3Definition method, of class RealVariableType. - */ - @Test - public void testGetCVC3Definition() { - CVC3Generator generator = new CVC3Generator(); - String variableName = "test_variable"; - RealVariableType instance = new RealVariableType(); - String expResult = "REAL"; - String result = generator.GenerateVariableType(instance); - assertEquals(expResult, result); - } - - /** - * Test SMTLIB generates the correct type. - */ - @Test - public void testGetSMTLIBDefinition() { - SMTLIBGenerator generator = new SMTLIBGenerator(); - String variableName = "test_variable"; - RealVariableType instance = new RealVariableType(); - String expResult = "Real"; - String result = generator.GenerateVariableType(instance); - assertEquals(expResult, result); - } - - /** - * Test of equals method, of class RealVariableType. - */ - @Test - public void testEquals() { - RealVariableType test = new RealVariableType(); - assertTrue(test.equals(new RealVariableType())); - assertTrue(test.equals(test)); - assertFalse(test.equals(new Object())); - } - - /** - * Test of hashCode method, of class RealVariableType. - */ - @Test - public void testHashCode() { - RealVariableType instance = new RealVariableType(); - assertEquals(0, instance.hashCode()); - } - - /** - * Test of canCastToType method, of class RealVariableType. Reals (for now) - * don't cast. - */ - @Test - public void testCanCastToType() { - RealVariableType instance = new RealVariableType(); - assertFalse(instance.canCastToType(new RealVariableType())); - assertFalse(instance.canCastToType(new BooleanVariableType())); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/expression/test/VariableCollectionTest.java b/jTET/src/test/java/ca/mcscert/jtet/expression/test/VariableCollectionTest.java deleted file mode 100644 index d3610731bd3bc38a2c67eb32148c244a1be54479..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/expression/test/VariableCollectionTest.java +++ /dev/null @@ -1,134 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.expression.test; - -import ca.mcscert.jtet.expression.EnumerationVariableType; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.expression.VariableType; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.HashMap; -import java.util.HashSet; -import java.util.Map; -import java.util.Set; - -import static org.hamcrest.CoreMatchers.*; -import static org.junit.Assert.assertThat; - -/** - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class VariableCollectionTest { - - private void AssertsForVariablesAreInBothLists(VariableCollection toTest) { - assertThat(toTest.getVariables().size(), is(1)); - assertThat(toTest.getVariablesAndEnumeratedValues().size(), is(1)); - - assertThat(toTest.getVariables().get("a").name(), is("a")); - assertThat(toTest.getVariables().get("a").type(), is((VariableType)new RealVariableType())); - assertThat(toTest.getVariables(), is(toTest.getVariablesAndEnumeratedValues())); - } - - @Test - public void VariablesAreInBothLists() { - Map vars = new HashMap(); - vars.put("a", new Variable("a", new RealVariableType())); - - AssertsForVariablesAreInBothLists(new VariableCollection(vars)); - AssertsForVariablesAreInBothLists(new VariableCollection(vars, null)); - AssertsForVariablesAreInBothLists(new VariableCollection(vars, new HashSet())); - } - - @Test - public void EnumeratedValuesAreInOneList() { - EnumerationVariableType type = new EnumerationVariableType("myenum"); - type.enumerationValues().add("e1"); - type.enumerationValues().add("e2"); - type.enumerationValues().add("e3"); - - Set enums = new HashSet(); - enums.add(type); - - VariableCollection vars = new VariableCollection(new HashMap(), enums); - - assertThat(vars.getVariables().size(), is(0)); - - assertThat(vars.getVariablesAndEnumeratedValues().size(), is(3)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e1").name(), is("e1")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e1").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e2").name(), is("e2")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e2").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e3").name(), is("e3")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e3").type(), is((VariableType) type)); - } - - @Test - public void EnumeratedValuesAndVariablesAreSeparate() { - EnumerationVariableType type = new EnumerationVariableType("enumtype"); - type.enumerationValues().add("e1"); - type.enumerationValues().add("e2"); - type.enumerationValues().add("e3"); - - Set enums = new HashSet(); - enums.add(type); - - Map var = new HashMap(); - var.put("a", new Variable("a", type)); - - VariableCollection vars = new VariableCollection(var, enums); - - assertThat(vars.getVariables().size(), is(1)); - - assertThat(vars.getVariables().get("a").name(), is("a")); - assertThat(vars.getVariables().get("a").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().size(), is(4)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("a").name(), is("a")); - assertThat(vars.getVariablesAndEnumeratedValues().get("a").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e1").name(), is("e1")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e1").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e2").name(), is("e2")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e2").type(), is((VariableType)type)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("e3").name(), is("e3")); - assertThat(vars.getVariablesAndEnumeratedValues().get("e3").type(), is((VariableType)type)); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/MatlabParserTest.java b/jTET/src/test/java/ca/mcscert/jtet/parsers/test/MatlabParserTest.java deleted file mode 100644 index 89409a434c8c22e72c64e170564550012202dc97..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/MatlabParserTest.java +++ /dev/null @@ -1,160 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers.test; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.CheckerGenerator; -import ca.mcscert.jtet.expression.Expression; -import ca.mcscert.jtet.expression.Literal; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.MatlabParser; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.parsers.VariableParser; -import ca.mcscert.jtet.expression.VariableType; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; -import static org.junit.Assert.*; - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class MatlabParserTest { - @Test - public void testSimpleNumberParse() { - Expression expr = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(null), "~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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(null), "4*5+6*7\n"); - Expression expr2 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(new VariableCollection(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 = MatlabParser.parseMatlabCode(variableParser.parseVariables("x,z,y"), "z == 1 && x == 0 && 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 (and (= z 1.0) (= x 0.0)) (= y 2.0))", expr.getCheckerOutput(generator, variableType)); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/PVSSimpleParserTest.java b/jTET/src/test/java/ca/mcscert/jtet/parsers/test/PVSSimpleParserTest.java deleted file mode 100644 index d7e7a2cf50c48f46271705f4eeeb0c9ea7d93058..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/PVSSimpleParserTest.java +++ /dev/null @@ -1,162 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers.test; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.CheckerGenerator; -import ca.mcscert.jtet.expression.Expression; -import ca.mcscert.jtet.expression.Literal; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.SMTLIBGenerator; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.expression.VariableType; -import ca.mcscert.jtet.parsers.PVSSimpleParser; -import ca.mcscert.jtet.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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(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(new VariableCollection(null), "4*5+6*7\n"); - Expression expr2 = PVSSimpleParser.parsePVSCode(new VariableCollection(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(new VariableCollection(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)); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/ParserOperatorParseTest.java b/jTET/src/test/java/ca/mcscert/jtet/parsers/test/ParserOperatorParseTest.java deleted file mode 100644 index 05e26a563588a8262ae6d9cebd8add494da23365..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/ParserOperatorParseTest.java +++ /dev/null @@ -1,123 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.parsers.test; - -import ca.mcscert.jtet.expression.BinaryOperation; -import ca.mcscert.jtet.expression.ExpressionBinaryOperation; -import ca.mcscert.jtet.expression.ExpressionUnaryOperation; -import ca.mcscert.jtet.expression.UnaryOperation; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.parsers.MatlabParser; -import ca.mcscert.jtet.parsers.PVSSimpleParser; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import java.lang.reflect.InvocationTargetException; -import java.lang.reflect.Method; -import java.util.Arrays; -import java.util.Collection; - -import static org.hamcrest.CoreMatchers.is; -import static org.junit.Assert.assertThat; - -/** This test simply tests that each operator parses correctly. - * - * This is a simply parametrized test set that only deals only with testing the individual operators. It avoids - * all the other details (it just uses literals for input). It also avoids any dependency on generators. - * - * @author Matthew Dawson - */ -@RunWith(Parameterized.class) -public class ParserOperatorParseTest { - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - {"+", "+", BinaryOperation.Addition, null}, - {"-", "-", BinaryOperation.Minus, null}, - {"*", "*", BinaryOperation.Multiplication, null}, - {"/", "/", BinaryOperation.Division, null}, - {"^", "^", BinaryOperation.Exponentiation, null}, - {">", ">", BinaryOperation.GreaterThen, null}, - {">=", ">=", BinaryOperation.GreaterThenEqual, null}, - {"<", "<", BinaryOperation.LessThen, null}, - {"<=", "<=", BinaryOperation.LessThenEqual, null}, - {"==", "=", BinaryOperation.Equals, null}, - {"~=", "/=", BinaryOperation.NotEquals, null}, - {null, "=>", BinaryOperation.Implies, null}, - {"&&", "AND", BinaryOperation.BooleanAnd, null}, - {"||", "OR", BinaryOperation.BooleanOr, null}, - {"~", "NOT", null, UnaryOperation.Negation}, - {"-", "-", null, UnaryOperation.Minus} - }); - } - @Parameter - public String matlabInputSymbol; - - @Parameter(value = 1) - public String pvsInputSymbol; - - @Parameter(value = 2) - public BinaryOperation bop; - - @Parameter(value = 3) - public UnaryOperation uop; - - private void doTest(String expr, Method method) throws InvocationTargetException, IllegalAccessException { - if (expr == null) { - // No symbol for this parser. Thus skip this test. - return ; - } - if (bop != null) { - // Binary op to test ... - ExpressionBinaryOperation exp = (ExpressionBinaryOperation)method.invoke(null, fakeVariableCollection, "1 " + expr + " 2\n"); - - assertThat(exp.toString(), is("(1 " + bop.toString() + " 2)")); - } else { - // Unary op to test ... - ExpressionUnaryOperation exp = (ExpressionUnaryOperation)method.invoke(null, fakeVariableCollection, expr + " 3\n"); - - assertThat(exp.toString(), is("( " + uop.toString() + " 3)")); - } - } - - @Test - public void testMatlabParser() throws NoSuchMethodException, InvocationTargetException, IllegalAccessException { - doTest(matlabInputSymbol, MatlabParser.class.getMethod("parseMatlabCode", VariableCollection.class, String.class)); - } - - @Test - public void testPVSSimpleParser() throws NoSuchMethodException, InvocationTargetException, IllegalAccessException { - doTest(pvsInputSymbol, PVSSimpleParser.class.getMethod("parsePVSCode", VariableCollection.class, String.class)); - } - - private VariableCollection fakeVariableCollection = new VariableCollection(null); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java b/jTET/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java deleted file mode 100644 index adf529bb010a2146e1f35f175dcbc23bc0f3efef..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/parsers/test/VariableParserTest.java +++ /dev/null @@ -1,187 +0,0 @@ -/* - * To change this template, choose Tools | Templates - * and open the template in the editor. - */ -package ca.mcscert.jtet.parsers.test; - -import ca.mcscert.jtet.expression.BooleanVariableType; -import ca.mcscert.jtet.expression.CVC3Generator; -import ca.mcscert.jtet.expression.CheckerGenerator; -import ca.mcscert.jtet.expression.EnumerationVariableType; -import ca.mcscert.jtet.expression.FixedPointVariableType; -import ca.mcscert.jtet.expression.RealVariableType; -import ca.mcscert.jtet.expression.Variable; -import ca.mcscert.jtet.expression.VariableCollection; -import ca.mcscert.jtet.expression.VariableType; -import ca.mcscert.jtet.parsers.VariableParser; - -import static org.hamcrest.CoreMatchers.*; -import static org.junit.Assert.*; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.Map; - - -/** - * - * @author matthew - */ -@RunWith(JUnit4.class) -public class VariableParserTest { - @Test - public void testSimpleVariable() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a"); - Map vars = variableCollection.getVariables(); - Variable a = vars.get("a"); - assertEquals("a", a.name()); - assertEquals(new RealVariableType(), a.type()); - assertThat(vars, is(variableCollection.getVariablesAndEnumeratedValues())); - } - @Test - public void testRealVariable() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a: real"); - Map vars = variableCollection.getVariables(); - Variable a = vars.get("a"); - assertEquals("a", a.name()); - assertEquals(new RealVariableType(), a.type()); - } - @Test - public void testBooleanVariable() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a: bool"); - Map vars = variableCollection.getVariables(); - Variable a = vars.get("a"); - assertEquals("a", a.name()); - assertEquals(new BooleanVariableType(), a.type()); - } - @Test - public void testFixedPointNoDecimalVariable() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a: fixedt(1, 16)"); - Map vars = variableCollection.getVariables(); - Variable a = vars.get("a"); - FixedPointVariableType type = (FixedPointVariableType)a.type(); - assertEquals("a", a.name()); - assertNotNull(type); - assertEquals(true, type.isSigned()); - assertEquals(16, type.digits()); - assertEquals(0, type.fractionPart()); - - vars = variableParser.parseVariables("a: fixedt(0, 15, 4)").getVariables(); - a = vars.get("a"); - type = (FixedPointVariableType)a.type(); - assertEquals("a", a.name()); - assertNotNull(type); - assertEquals(false, type.isSigned()); - assertEquals(15, type.digits()); - assertEquals(4, type.fractionPart()); - } - @Test - public void testCaseInsensitivtySearch() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a: ReAl"); - Map vars = variableCollection.getVariables(); - Variable a = vars.get("a"); - assertEquals("a", a.name()); - assertEquals(new RealVariableType(), a.type()); - - vars = variableParser.parseVariables("A: REAL").getVariables(); - a = vars.get("A"); - assertEquals("A", a.name()); - assertEquals(new RealVariableType(), a.type()); - } - @Test - public void testMultiVariableOutput() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("a,b"); - assertEquals("a:REAL;\nb:REAL;\n", generator.GenerateVariablesDeclaration(variableCollection)); - - variableCollection = variableParser.parseVariables("a:fixedt(1,16,9),b"); - assertEquals("a:BITVECTOR(16);\nb:REAL;\n", generator.GenerateVariablesDeclaration(variableCollection)); - } - @Test - public void testSubtypeTypeExtraction() { - VariableParser variableParser = new VariableParser(); - VariableCollection variableCollection = variableParser.parseVariables("d:{y|c OR y > 5},a,b:{x:real|x>5},c:bool,z:{x:bool|x /= c}"); - Map vars = variableCollection.getVariables(); - 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)")); - } - - @Test - public void testCustomType() { - VariableParser variableParser = new VariableParser(); - variableParser.addCustomType("myreal", new RealVariableType()); - BooleanVariableType customBool = new BooleanVariableType(); - customBool.setSubtypePredicate(new Variable("c", new BooleanVariableType())); - variableParser.addCustomType("mybool", customBool); - - Map vars = variableParser.parseVariables("a:myreal,b:mybool").getVariables(); - assertThat(vars.size(), is(2)); - - assertThat(vars.get("a").name(), is("a")); - assertThat(vars.get("a").type(), is((VariableType) new RealVariableType())); - - assertThat(vars.get("b").name(), is("b")); - assertThat(vars.get("b").type(), is((VariableType) new BooleanVariableType())); - assertThat(vars.get("b").type().subtypePredicate().toString(), is("c")); - } - - @Test - public void testUnknownCustomType() { - VariableParser variableParser = new VariableParser(); - - Map vars = variableParser.parseVariables("a:unknowntype").getVariables(); - assertThat(vars.size(), is(1)); - - assertThat(vars.get("a").name(), is("a")); - assertThat(vars.get("a").type(), is((VariableType) new RealVariableType())); - } - - @Test - public void testEnumerationsAreAvailable() { - EnumerationVariableType enumType = new EnumerationVariableType("enumtype"); - enumType.enumerationValues().add("enum1"); - enumType.enumerationValues().add("enum2"); - - VariableParser variableParser = new VariableParser(); - variableParser.addCustomType("enumtype", enumType); - - VariableCollection vars = variableParser.parseVariables("a:enumtype"); - - assertThat(vars.getVariables().size(), is(1)); - assertThat(vars.getVariablesAndEnumeratedValues().size(), is(3)); - - assertThat(vars.getVariables().get("a").type(), is((VariableType)enumType)); - assertThat(vars.getVariablesAndEnumeratedValues().get("a").type(), is((VariableType)enumType)); - - assertThat(vars.getVariablesAndEnumeratedValues().get("enum1").type(), is((VariableType)enumType)); - assertThat(vars.getVariablesAndEnumeratedValues().get("enum2").type(), is((VariableType)enumType)); - } - - CheckerGenerator generator = new CVC3Generator(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResultTest.java b/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResultTest.java deleted file mode 100644 index da2c05be811184163ff67926235085bdc9a44c19..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerResultTest.java +++ /dev/null @@ -1,54 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.LinkedHashMap; - -import static org.junit.Assert.*; - -/** - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class CheckerRunnerResultTest { - @Test - public void TestGenerateMatlabVariableDeclarations() { - CheckerRunnerResult instance = new CheckerRunnerResult(); - - instance.SampleValues = new LinkedHashMap(); - instance.SampleValues.put("x", "5.0"); - instance.SampleValues.put("z", "STRCONST"); - - assertEquals("x = 5.0;\nz = STRCONST;\n", instance.GenerateMatlabVariableDeclarations()); - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerTest.java b/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerTest.java deleted file mode 100644 index f4ca4f00b459b664fdea7c72015fdc33cc907278..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/CheckerRunnerTest.java +++ /dev/null @@ -1,128 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import ca.mcscert.jtet.parsers.VariableParser; -import ca.mcscert.jtet.tablularexpression.HierarchicalCell; -import ca.mcscert.jtet.tablularexpression.HierarchicalGrid; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.List; - -import static org.junit.Assert.*; - -/** - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class CheckerRunnerTest { - @Test - public void TestRunningZ3() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("0 > x")); - - List nextGrid = topCells.get(1).getSubHiearchy(); - nextGrid.add(new HierarchicalCell("z > 0")); - nextGrid.add(new HierarchicalCell("z == 1")); - nextGrid.add(new HierarchicalCell("0 > z")); - - //nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0")); - - List res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x,z")); - assertEquals(2, res.size()); - assertEquals(2, res.get(0).SampleValues.size()); - assertEquals("0.0", res.get(0).SampleValues.get("x")); - assertEquals("1.0", res.get(0).SampleValues.get("z")); - - assertEquals(2, res.get(1).SampleValues.size()); - assertEquals("0.0", res.get(1).SampleValues.get("x")); - assertEquals("0.0", res.get(1).SampleValues.get("z")); - } - @Test - public void TestRunningZ3WithNegative() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("0 > x")); - - List nextGrid = topCells.get(1).getSubHiearchy(); - nextGrid.add(new HierarchicalCell("z > 0")); - nextGrid.add(new HierarchicalCell("z == 0")); - nextGrid.add(new HierarchicalCell("z == -1")); - nextGrid.add(new HierarchicalCell("0 > z")); - - //nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0")); - - List res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x,z")); - assertEquals(1, res.size()); - assertEquals(2, res.get(0).SampleValues.size()); - assertEquals("0.0", res.get(0).SampleValues.get("x")); - assertEquals("(- 1.0)", res.get(0).SampleValues.get("z")); - } - @Test - public void TestRunningZ3WithFractionalReturn() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("x == 2.5")); - topCells.add(new HierarchicalCell("0 > x")); - - List res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x")); - assertEquals(1, res.size()); - assertEquals(1, res.get(0).SampleValues.size()); - assertEquals("(5.0 / 2.0)", res.get(0).SampleValues.get("x")); - } - @Test - public void TestRunningZ3WithNegativeFractionalReturn() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("x == -2.5")); - topCells.add(new HierarchicalCell("0 > x")); - - List res = CheckerRunner.RunZ3(grid, variableParser.parseVariables("x")); - assertEquals(1, res.size()); - assertEquals(1, res.get(0).SampleValues.size()); - assertEquals("(- (5.0 / 2.0))", res.get(0).SampleValues.get("x")); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGeneratorTest.java b/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGeneratorTest.java deleted file mode 100644 index fccf908089ad25a55d366d8193a71a0a1467ef63..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/smtlibchecker/HierarchicalGridSMTLIBGeneratorTest.java +++ /dev/null @@ -1,121 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.smtlibchecker; - -import ca.mcscert.jtet.parsers.VariableParser; -import ca.mcscert.jtet.tablularexpression.HierarchcialGridCheckerWalkerGenerator; -import ca.mcscert.jtet.tablularexpression.HierarchicalCell; -import ca.mcscert.jtet.tablularexpression.HierarchicalGrid; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import java.util.List; - -import static org.junit.Assert.assertEquals; - -/** - * - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class HierarchicalGridSMTLIBGeneratorTest { - - // Exercise the smtlib generator using a table designed in matlab. - @Test - public void exerciseSMTLIBGenerator() { - HierarchicalGrid grid = new HierarchicalGrid(); - List topCells = grid.getSubHiearchy(); - - topCells.add(new HierarchicalCell("x > 0")); - topCells.add(new HierarchicalCell("x == 0")); - topCells.add(new HierarchicalCell("0 > x")); - - List nextGrid = topCells.get(1).getSubHiearchy(); - nextGrid.add(new HierarchicalCell("z > 0")); - nextGrid.add(new HierarchicalCell("z == 0")); - nextGrid.add(new HierarchicalCell("0 > z")); - - nextGrid.get(1).getSubHiearchy().add(new HierarchicalCell("z == 0")); - - String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridSMTLIBGenerator(variableParser.parseVariables("x,z"))); - - String expected = "(push 1)\n" + - "(assert (and true (or (and (> x 0.0) (= x 0.0))\n" + - "(and (> x 0.0) (> 0.0 x))\n" + - "(and (= x 0.0) (> 0.0 x)))))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and true (not (or (> x 0.0) (= x 0.0) (> 0.0 x)))))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and (= x 0.0) (or (and (> z 0.0) (= z 0.0))\n" + - "(and (> z 0.0) (> 0.0 z))\n" + - "(and (= z 0.0) (> 0.0 z)))))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and (= x 0.0) (not (or (> z 0.0) (= z 0.0) (> 0.0 z)))))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and (= z 0.0) (= x 0.0) false))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and (= z 0.0) (= x 0.0) (not (= z 0.0))))\n" + - "(check-sat)\n" + - "(pop 1)\n"; - - assertEquals(expected, out); - } - - // Test the smtlib generator using an empty table - @Test - public void testEmptyTable() { - HierarchicalGrid grid = new HierarchicalGrid(); - - String out = HierarchcialGridCheckerWalkerGenerator.GenerateCheckerFromGrid(grid, new HierarchicalGridSMTLIBGenerator(variableParser.parseVariables("x,z"))); - - String expected = "(push 1)\n" + - "(assert (and true false))\n" + - "(check-sat)\n" + - "(pop 1)\n" + - "(push 1)\n" + - "(assert (and true (not true)))\n" + - "(check-sat)\n" + - "(pop 1)\n"; - - assertEquals(expected, out); - } - - VariableParser variableParser = new VariableParser(); -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridResizeTest.java b/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridResizeTest.java deleted file mode 100644 index db5bc4ba748ecf768208ee4504266a67c22fff9b..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridResizeTest.java +++ /dev/null @@ -1,139 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression.test; - -import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.Parameterized; -import org.junit.runners.Parameterized.Parameter; -import org.junit.runners.Parameterized.Parameters; - -import java.util.Arrays; -import java.util.Collection; - -import static org.hamcrest.CoreMatchers.is; -import static org.hamcrest.CoreMatchers.notNullValue; -import static org.junit.Assert.assertThat; - -/** - * - * @author Matthew Dawson - */ -@RunWith(Parameterized.class) -public class TwoDimensionalGridResizeTest { - @Parameters - public static Collection data() { - return Arrays.asList(new Object[][]{ - { - 1, 1, - 4, 5 - }, - { - 3, 3, - 5, 3 - }, - { - 3, 3, - 3, 5 - }, - { - 3, 3, - 5, 3 - }, - { - 4, 4, - 2, 2 - }, - { - 4, 4, - 2, 4 - }, - { - 4, 4, - 4, 2 - }, - { - 4, 4, - 2, 6 - }, - { - 4, 4, - 6, 2 - } - }); - } - - @Parameter(value = 0) - public int initialX; - - @Parameter(value = 1) - public int initialY; - - @Parameter(value = 2) - public int newX; - - @Parameter(value = 3) - public int newY; - - @Test - public void doTest() - { - TwoDimensionalGrid grid = new TwoDimensionalGrid(initialX, initialY); - //Verify proper creation (should never fail ...) - assertThat(grid.sizeX(), is(initialX)); - assertThat(grid.sizeY(), is(initialY)); - // Setup cell contents for the next test. - int i = 0; - for (int x = 0; x < initialX; ++x) { - for (int y = 0; y < initialY; ++y) { - grid.get(x, y).setContents("" + (i++)); - } - } - - //And do the resize - grid.resize(newX, newY); - // Verify new sizes - assertThat(grid.sizeX(), is(newX)); - assertThat(grid.sizeY(), is(newY)); - // And verify a cell exists at the maximum size. - assertThat(grid.get(newX - 1, newY - 1), is(notNullValue())); - // And that the original cells are still there. - i = -1; - for (int x = 0; x < initialX; ++x) { - for (int y = 0; y < initialY; ++y) { - i++; - if (x >= newX || y >= newY) { - continue; - } - assertThat(grid.get(x, y).contents(), is("" + i)); - } - } - } -} diff --git a/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridTest.java b/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridTest.java deleted file mode 100644 index f8e9f005419480c5b55489b7ee4a85a4e2e5928e..0000000000000000000000000000000000000000 --- a/jTET/src/test/java/ca/mcscert/jtet/tablularexpression/test/TwoDimensionalGridTest.java +++ /dev/null @@ -1,87 +0,0 @@ -/* - * Copyright (C) 2013 Matthew Dawson - * - * Redistribution and use in source and binary forms, with or without - * modification, are permitted provided that the following conditions are - * met: - * - * * Redistributions of source code must retain the above copyright - * notice, this list of conditions and the following disclaimer. - * * Redistributions in binary form must reproduce the above copyright - * notice, this list of conditions and the following disclaimer in - * the documentation and/or other materials provided with the distribution - * * Neither the name of the McMaster Centre for Software Certification nor the names - * of its contributors may be used to endorse or promote products derived - * from this software without specific prior written permission. - * - * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" - * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE - * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE - * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE - * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR - * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF - * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS - * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN - * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) - * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE - * POSSIBILITY OF SUCH DAMAGE. - */ -package ca.mcscert.jtet.tablularexpression.test; - -import ca.mcscert.jtet.tablularexpression.Cell; -import ca.mcscert.jtet.tablularexpression.TwoDimensionalGrid; -import org.junit.Test; -import org.junit.runner.RunWith; -import org.junit.runners.JUnit4; - -import static org.hamcrest.CoreMatchers.*; -import static org.junit.Assert.*; - -/** - * - * @author Matthew Dawson - */ -@RunWith(JUnit4.class) -public class TwoDimensionalGridTest { - @Test - public void testEmptyConstructor() { - TwoDimensionalGrid grid = new TwoDimensionalGrid(); - - // By default, we should have a 1x1 grid. Test that. - assertThat(grid.sizeX(), is(1)); - assertThat(grid.sizeY(), is(1)); - Cell cell = grid.get(0,0); - assertThat(cell, is(notNullValue())); - assertThat(grid.get(0,0), is(cell)); - } - - @Test(expected = IllegalArgumentException.class) - public void testNonPositiveXSize() { - new TwoDimensionalGrid(-1, 2); - } - - @Test(expected = IllegalArgumentException.class) - public void testNonPositiveYSize() { - new TwoDimensionalGrid(2, -1); - } - - @Test(expected = IllegalArgumentException.class) - public void testNonPositiveBothSides() { - new TwoDimensionalGrid(-1, -2); - } - - @Test(expected = IllegalArgumentException.class) - public void testZeroSize() { - new TwoDimensionalGrid(0, 2); - } - - @Test(expected = IllegalArgumentException.class) - public void testZeroYSize() { - new TwoDimensionalGrid(2, 0); - } - - @Test(expected = IllegalArgumentException.class) - public void testZeroBothSides() { - new TwoDimensionalGrid(0, 0); - } -}