Create an expression generator spy. (dec07409) · Commits · tables / jtet

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

0 → 100644

+176 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 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.expression;

		import java.util.ArrayList;
		import java.util.Collections;
		import java.util.List;

		/**
		* This inserts a spy between a given CheckerGenerator and the caller, recording all operations.
		* <p>
		* This is useful if it is wanted to verify that all operations satisfy some property, for instance that all fixed point
		* operations do not under/overflow.
		* @author Matthew Dawson
		*/
		public class CheckerGeneratorSpy implements CheckerGenerator {
		/**
		* Constructs the spy, using the given CheckerGenerator to generate the actual expressions.
		* @param checkerGenerator The CheckerGenerator to use to actually generate the expressions.
		*/
		public CheckerGeneratorSpy(CheckerGenerator checkerGenerator) {
		this.checkerGenerator = checkerGenerator;
		}

		/**
		* {@inheritDoc}
		*/
		@Override
		public String GenerateUnaryOperation(UnaryOperation op, String expression, VariableType usedType) {
		m_spiedUnaryOps.add(new SpiedUnaryOp(op, expression, usedType));
		return checkerGenerator.GenerateUnaryOperation(op, expression, usedType);
		}

		/**
		* {@inheritDoc}
		*/
		@Override
		public String GenerateBinaryOperation(BinaryOperation op, String lhsExp, String rhsExp, VariableType usedType) {
		m_spiedBinaryOps.add(new SpiedBinaryOp(lhsExp, op, rhsExp, usedType));
		return checkerGenerator.GenerateBinaryOperation(op, lhsExp, rhsExp, usedType);
		}

		/**
		* {@inheritDoc}
		* <p>
		* This currently remains unrecorded.
		*/
		@Override
		public String GenerateLiteralValue(String value, VariableType requestedType) {
		return checkerGenerator.GenerateLiteralValue(value, requestedType);
		}

		/**
		* {@inheritDoc}
		* <p>
		* This currently remains unrecorded.
		*/
		@Override
		public String GenerateVariablesDeclaration(VariableCollection vars) {
		return checkerGenerator.GenerateVariablesDeclaration(vars);
		}

		/**
		* Returns an unmodifiable list of all unary operations that have occurred so far.
		* @return All unary operations seen
		*/
		public List<SpiedUnaryOp> getUnaryOps() {
		return Collections.unmodifiableList(m_spiedUnaryOps);
		}

		/**
		* Returns an unmodifiable list of all binary operations that have occurred so far.
		* @return All binary operations seen
		*/
		public List<SpiedBinaryOp> getBinaryOps() {
		return m_spiedBinaryOps;
		}

		/**
		* This class contains the details of a unary operation: The actual operation, the input expression, and the output type.
		*/
		public static class SpiedUnaryOp {
		/**
		* The operator for this operation.
		*/
		public final UnaryOperation op;
		/**
		* The input expression to the operator.
		*/
		public final String expression;
		/**
		* The output type of the expression.
		*/
		public final VariableType usedType;

		/**
		* Constructs a SpiedUnaryOp with the details filled in.
		* @param op The operator for this operation
		* @param expression The input expression to the operator
		* @param usedType The output type of the expression
		*/
		private SpiedUnaryOp(UnaryOperation op, String expression, VariableType usedType) {
		this.op = op;
		this.expression = expression;
		this.usedType = usedType;
		}
		}

		/**
		* This class contains the details of a binary operation: The actual operation, the input expressions, and the output type.
		*/
		public static class SpiedBinaryOp {
		/**
		* The operator for this operation.
		*/
		public final BinaryOperation op;
		/**
		* The expression on the left hand side of the operator.
		*/
		public final String lhsExp;
		/**
		* The expression on the right hand side of the operator.
		*/
		public final String rhsExp;
		/**
		* The output type of the expression.
		*/
		public final VariableType usedType;

		/**
		* Constructs a SpiedBinaryOp with the details filled in.
		* @param lhsExp The expression on the left hand side of the operator
		* @param op The operator for this operation
		* @param rhsExp The expression on the right hand side of the operator
		* @param usedType The output type of the expression
		*/
		private SpiedBinaryOp(String lhsExp, BinaryOperation op, String rhsExp, VariableType usedType) {
		this.lhsExp = lhsExp;
		this.op = op;
		this.rhsExp = rhsExp;
		this.usedType = usedType;
		}
		}

		private final CheckerGenerator checkerGenerator;
		private final List<SpiedUnaryOp> m_spiedUnaryOps = new ArrayList<SpiedUnaryOp>();

		private final List<SpiedBinaryOp> m_spiedBinaryOps = new ArrayList<SpiedBinaryOp>();
		}

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

+5 −0

Original line number	Diff line number	Diff line
		@@ -67,6 +67,11 @@ public class GenericOperationGeneratorTest {
		"((((x ∗ 5) = (1 ÷ (− 4))) ∨ (((x > (8 + 3)) ∧ (9 < (x − 2))) ∨ ((x ≥ 12) ∨ ((¬ (34 ≤ (− x))) ∨ (5 > 4))))) ⇒ (x ≠ 5))",
		null,
		null
		},
		{new CheckerGeneratorSpy(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(8,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(8,x,0bin00001000))) OR (BVGE(x,0bin00110000) OR ((NOT BVLE(0bin10001000,BVUMINUS(x))) OR (5 > 4))))) => (x /= 0bin00010100))"
		}
		});
		}

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

+11 −0

Original line number	Diff line number	Diff line
		@@ -122,6 +122,17 @@ public class GenericVariablesDeclarationGeneratorTest {
		null,
		null,
		null
		},
		{new CheckerGeneratorSpy(new CVC3Generator()),
		"x:REAL;\n",
		"new_x_name:REAL;\n",
		"x:REAL;\nASSERT (x > 0);\n",
		"x:BOOLEAN;\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;\nnew_x_name:MyEnum;\n",
		"DATATYPE\n MyEnum = e1 \| e2 \| e3\nEND;\nx:MyEnum;\ny:MyEnum;\n"
		}
		});
		}

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

0 → 100644

+100 −0

Original line number	Diff line number	Diff line
		/*
		* Copyright (C) 2014 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.expression.test;

		import ca.mcscert.jtet.expression.BinaryOperation;
		import ca.mcscert.jtet.expression.CVC3Generator;
		import ca.mcscert.jtet.expression.CheckerGeneratorSpy;
		import ca.mcscert.jtet.expression.Expression;
		import ca.mcscert.jtet.expression.ExpressionBinaryOperation;
		import ca.mcscert.jtet.expression.ExpressionUnaryOperation;
		import ca.mcscert.jtet.expression.Literal;
		import ca.mcscert.jtet.expression.RealVariableType;
		import ca.mcscert.jtet.expression.UnaryOperation;
		import ca.mcscert.jtet.expression.VariableType;
		import org.junit.Before;
		import org.junit.Test;
		import org.junit.runner.RunWith;
		import org.junit.runners.JUnit4;

		import java.util.List;

		import static org.hamcrest.CoreMatchers.*;
		import static org.junit.Assert.assertThat;

		/**
		* Verifies CheckerGeneratorSpy properly records operations.
		* @author Matthew Dawson
		*/
		@RunWith(JUnit4.class)
		public class CheckerGeneratorSpyTest {
		/**
		* Verify a given ExpressionUnaryOperation will be correctly recorded.
		*/
		@Test
		public void testSimpleUnaryExpression() {
		Expression expression = new ExpressionUnaryOperation(UnaryOperation.Minus, new Literal("5"));
		expression.getCheckerOutput(m_spy, RealVariableType.Type);

		List<CheckerGeneratorSpy.SpiedBinaryOp> binaryOps = m_spy.getBinaryOps();
		List<CheckerGeneratorSpy.SpiedUnaryOp> unaryOps = m_spy.getUnaryOps();
		assertThat(unaryOps.size(), is(1));
		assertThat(binaryOps.size(), is(0));
		assertThat(unaryOps.get(0).expression, is("5"));
		assertThat(unaryOps.get(0).op, is(UnaryOperation.Minus));
		assertThat(unaryOps.get(0).usedType, is((VariableType) RealVariableType.Type));
		}

		/**
		* Verify a given ExpressionBinaryOperation will be correctly recorded.
		*/
		@Test
		public void testSimpleBinaryExpression() {
		Expression expression = new ExpressionBinaryOperation(new Literal("5"), BinaryOperation.Addition, new Literal("6"));
		expression.getCheckerOutput(m_spy, RealVariableType.Type);

		List<CheckerGeneratorSpy.SpiedBinaryOp> binaryOps = m_spy.getBinaryOps();
		List<CheckerGeneratorSpy.SpiedUnaryOp> unaryOps = m_spy.getUnaryOps();
		assertThat(unaryOps.size(), is(0));
		assertThat(binaryOps.size(), is(1));
		assertThat(binaryOps.get(0).lhsExp, is("5"));
		assertThat(binaryOps.get(0).rhsExp, is("6"));
		assertThat(binaryOps.get(0).op, is(BinaryOperation.Addition));
		assertThat(binaryOps.get(0).usedType, is((VariableType) RealVariableType.Type));
		}

		@Before
		public void setUp() {
		m_generator = new CVC3Generator();
		m_spy = new CheckerGeneratorSpy(m_generator);
		}
		private CVC3Generator m_generator;
		private CheckerGeneratorSpy m_spy;
		}