Commit d6cf2f29 authored by Yanjun Jiang's avatar Yanjun Jiang Committed by Matthew Dawson
Browse files

Rename CheckerGeneratorSpy to ExpressionGeneratorSpy. 

Following on the previous rename, also rename CheckerGeneratorSpy to
ExpressionGeneratorSpy.
parent efe61fef

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

+4 −4
Original line number Diff line number Diff line
@@ -29,7 +29,7 @@ 
package ca.mcscert.jtet.cvc3generator;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.expression.CheckerGeneratorSpy;

import ca.mcscert.jtet.expression.ExpressionGeneratorSpy;

import ca.mcscert.jtet.parsers.MatlabParser;

import ca.mcscert.jtet.tablularexpression.Cell;

import ca.mcscert.jtet.tablularexpression.HierarchicalGridCheckerGenerator;
@@ -129,11 +129,11 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec 
    @Override

    public void handleLeafCell(Cell cell) {

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

        CheckerGeneratorSpy spy = new CheckerGeneratorSpy(m_CVC3Generator);

        ExpressionGeneratorSpy spy = new ExpressionGeneratorSpy(m_CVC3Generator);

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



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

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

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

            if (op.usedType instanceof FixedPointVariableType) {

                generateOverflowTCC(op);

            }
@@ -149,7 +149,7 @@ final public class HierarchicalGridCVC3Generator implements HierarchicalGridChec 
        m_currentCompleteQueries.add(newCellCode);

    }



    private void generateOverflowTCC(CheckerGeneratorSpy.SpiedBinaryOp binaryOp) {

    private void generateOverflowTCC(ExpressionGeneratorSpy.SpiedBinaryOp binaryOp) {

        // Comparisons never overflow, so ignore them.

        switch (binaryOp.op) {

            case GreaterThen:

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

+2 −2
Original line number Diff line number Diff line
@@ -40,12 +40,12 @@ import java.util.List; 
 * operations do not under/overflow.

 * @author Matthew Dawson

 */

public class CheckerGeneratorSpy implements ExpressionGenerator {

public class ExpressionGeneratorSpy implements ExpressionGenerator {

    /**

     * Constructs the spy, using the given ExpressionGenerator to generate the actual expressions.

     * @param expressionGenerator The ExpressionGenerator to use to actually generate the expressions.

     */

    public CheckerGeneratorSpy(ExpressionGenerator expressionGenerator) {

    public ExpressionGeneratorSpy(ExpressionGenerator expressionGenerator) {

        this.expressionGenerator = expressionGenerator;

    }

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

+1 −1
Original line number Diff line number Diff line
@@ -68,7 +68,7 @@ public class GenericOperationGeneratorTest { 
                        null,

                        null

                },

                {new CheckerGeneratorSpy(new CVC3Generator()),

                {new ExpressionGeneratorSpy(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

+1 −1
Original line number Diff line number Diff line
@@ -123,7 +123,7 @@ public class GenericVariablesDeclarationGeneratorTest { 
                        null,

                        null

                },

                {new CheckerGeneratorSpy(new CVC3Generator()),

                {new ExpressionGeneratorSpy(new CVC3Generator()),

                        "x:REAL;\n",

                        "new_x_name:REAL;\n",

                        "x:REAL;\nASSERT (x > 0);\n",

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

+8 −9
Original line number Diff line number Diff line
@@ -30,7 +30,6 @@ 
package ca.mcscert.jtet.expression.test;



import ca.mcscert.jtet.expression.*;

import ca.mcscert.jtet.expression.CheckerGeneratorSpy;

import org.junit.Before;

import org.junit.Test;

import org.junit.runner.RunWith;
@@ -42,11 +41,11 @@ import static org.hamcrest.CoreMatchers.*; 
import static org.junit.Assert.assertThat;



/**

 * Verifies CheckerGeneratorSpy properly records operations.

 * Verifies ExpressionGeneratorSpy properly records operations.

 * @author Matthew Dawson

 */

@RunWith(JUnit4.class)

public class CheckerGeneratorSpyTest {

public class ExpressionGeneratorSpyTest {

    /**

     * Verify a given ExpressionUnaryOperation will be correctly recorded.

     */
@@ -55,8 +54,8 @@ public class CheckerGeneratorSpyTest { 
        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();

        List<ExpressionGeneratorSpy.SpiedBinaryOp> binaryOps = m_spy.getBinaryOps();

        List<ExpressionGeneratorSpy.SpiedUnaryOp> unaryOps = m_spy.getUnaryOps();

        assertThat(unaryOps.size(), is(1));

        assertThat(binaryOps.size(), is(0));

        assertThat(unaryOps.get(0).expression, is("5"));
@@ -72,8 +71,8 @@ public class CheckerGeneratorSpyTest { 
        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();

        List<ExpressionGeneratorSpy.SpiedBinaryOp> binaryOps = m_spy.getBinaryOps();

        List<ExpressionGeneratorSpy.SpiedUnaryOp> unaryOps = m_spy.getUnaryOps();

        assertThat(unaryOps.size(), is(0));

        assertThat(binaryOps.size(), is(1));

        assertThat(binaryOps.get(0).lhsExp, is("5"));
@@ -85,8 +84,8 @@ public class CheckerGeneratorSpyTest { 
    @Before

    public void setUp() {

        m_generator = new CVC3Generator();

        m_spy = new CheckerGeneratorSpy(m_generator);

        m_spy = new ExpressionGeneratorSpy(m_generator);

    }

    private CVC3Generator m_generator;

    private CheckerGeneratorSpy m_spy;

    private ExpressionGeneratorSpy m_spy;

}