Split the CVC3VariablesDeclarationGenerator from CVC3ExpressionGenerator. (178a3893) · Commits · tables / jtet

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

+3 −63

Original line number	Diff line number	Diff line
		@@ -17,7 +17,9 @@ import org.apache.commons.lang3.StringUtils;
		*
		* @author matthew
		*/
		final public class CVC3ExpressionGenerator implements VariablesDeclarationGenerator, ExpressionGenerator {
		final public class CVC3ExpressionGenerator implements ExpressionGenerator {
		public final static CVC3ExpressionGenerator Generator = new CVC3ExpressionGenerator();

		// For operations that don't have specific signed/unsigned representations, use this function.
		private static String GetIndifferentFixedPointFunctionFor(BinaryOperation op) {
		switch (op) {
		@@ -183,68 +185,6 @@ final public class CVC3ExpressionGenerator implements VariablesDeclarationGenera
		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<String, Variable> vars = variableCollection.getVariables();
		Set<EnumerationVariableType> emittedEnumerations = new HashSet<EnumerationVariableType>();

		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.outputName())
		.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, BooleanVariableType.Type))
		.append(";\n");
		}
		}

		return ret.toString();
		}

		@Override
		public String GenerateLiteralValue(String value, VariableType requestedType) {
		if (requestedType instanceof RealVariableType) {

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

0 → 100644

+108 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2013 Matthew Dawson <matthew@mjdsystems.ca>
		*
		* 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.*;

		import java.util.HashSet;
		import java.util.Map;
		import java.util.Set;

		/**
		*
		* @author matthew
		*/
		final public class CVC3VariablesDeclarationGenerator implements VariablesDeclarationGenerator {
		public final static CVC3VariablesDeclarationGenerator Generator = new CVC3VariablesDeclarationGenerator();

		@Override
		public String GenerateVariablesDeclaration(VariableCollection variableCollection) {
		Map<String, Variable> vars = variableCollection.getVariables();
		Set<EnumerationVariableType> emittedEnumerations = new HashSet<EnumerationVariableType>();

		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.outputName())
		.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(CVC3ExpressionGenerator.Generator, BooleanVariableType.Type))
		.append(";\n");
		}
		}

		return ret.toString();
		}

		/**@deprecated
		* it is only public for unit tests, and will be made private eventually
		*/
		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() + ")");
		}
		}
		}

src/test/java/ca/mcscert/jtet/expression/FixedPointVariableTypeTest.java

+2 −2

Original line number	Diff line number	Diff line
		@@ -4,7 +4,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;
		import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.JUnit4;
		@@ -32,7 +32,7 @@ public class FixedPointVariableTypeTest {
		*/
		@Test
		public void testGetCVC3Definition() {
		CVC3ExpressionGenerator generator = new CVC3ExpressionGenerator();
		CVC3VariablesDeclarationGenerator generator = new CVC3VariablesDeclarationGenerator();
		FixedPointVariableType instance = new FixedPointVariableType(true, 16, 8);
		assertEquals("BITVECTOR(16)", generator.GenerateVariableType(instance));
		}

src/test/java/ca/mcscert/jtet/expression/GenericVariablesDeclarationGeneratorTest.java

+2 −2

Original line number	Diff line number	Diff line
		@@ -28,7 +28,7 @@
		*/
		package ca.mcscert.jtet.expression;

		import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;
		import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;
		import ca.mcscert.jtet.parsers.VariableParser;
		import org.junit.Before;
		import org.junit.Test;
		@@ -83,7 +83,7 @@ public class GenericVariablesDeclarationGeneratorTest {
		"(declare-fun y () MyEnum)\n" +
		"(assert (isMyEnum y))\n"
		},
		{new CVC3ExpressionGenerator(),
		{new CVC3VariablesDeclarationGenerator(),
		"x:REAL;\n",
		"new_x_name:REAL;\n",
		"x:REAL;\nASSERT (x > 0);\n",

src/test/java/ca/mcscert/jtet/expression/VariableTest.java

+3 −3

Original line number	Diff line number	Diff line
		@@ -7,7 +7,7 @@ package ca.mcscert.jtet.expression;
		import static org.hamcrest.CoreMatchers.is;
		import static org.junit.Assert.*;

		import ca.mcscert.jtet.cvc3generator.CVC3ExpressionGenerator;
		import ca.mcscert.jtet.cvc3generator.CVC3VariablesDeclarationGenerator;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.JUnit4;
		@@ -36,7 +36,7 @@ public class VariableTest {
		varList.put(name, var);
		VariableCollection variableCollection = new VariableCollection(varList);

		VariablesDeclarationGenerator generator = new CVC3ExpressionGenerator();
		VariablesDeclarationGenerator generator = new CVC3VariablesDeclarationGenerator();
		assertEquals(name+":REAL;\n", generator.GenerateVariablesDeclaration(variableCollection));

		generator = new SMTLIBGenerator();
		@@ -60,7 +60,7 @@ public class VariableTest {
		varList.put("var", var);
		VariableCollection variableCollection = new VariableCollection(varList);

		VariablesDeclarationGenerator generator = new CVC3ExpressionGenerator();
		VariablesDeclarationGenerator generator = new CVC3VariablesDeclarationGenerator();
		String varDecl = generator.GenerateVariablesDeclaration(variableCollection);

		assertThat(varDecl, is("var:REAL;\nASSERT (var > 0);\n"));