Commit 0941ddf5 authored by Matthew Dawson's avatar Matthew Dawson
Browse files

Add the ability for a variable to have a different output name. 

At least for the SAL generator for SimCheck, I need to transform the variable
names.  Thus add the ability for Variables to have different names outputed
during generation.  This ensures that a given variable always has its name
match as expected.

Also update the various tests to exercise this new functionality.
parent 5745a2e8

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

+1 −1
Original line number Diff line number Diff line
@@ -227,7 +227,7 @@ final public class CVC3Generator implements CheckerGenerator{ 


        // Then generate all the variables.

        for(Variable var : vars.values()) {

            ret.append(var.name())

            ret.append(var.outputName())

               .append(":")

               .append(GenerateVariableType(var.type()))

               .append(";\n");

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

+4 −4
Original line number Diff line number Diff line
@@ -136,8 +136,8 @@ final public class EventBGenerator implements CheckerGenerator{ 


        //generate all the variables one by one.

        for(Variable var : vars.values()) {

            ret += generateVariableXmlPre(var.name());

            ret += var.name();

            ret += generateVariableXmlPre(var.outputName());

            ret += var.outputName();

            ret += variableXmlPost;

        }
@@ -161,7 +161,7 @@ final public class EventBGenerator implements CheckerGenerator{ 
        //generate all the Invariants one by one.

        for (Variable var : vars.values()) {

            ret += generateInvariantXmlPre(invariantsNum);

            ret += var.name();

            ret += var.outputName();

            ret += " ∈ ";

            ret += GenerateVariableType(var.type());

            ret += invariantXmlPost;
@@ -207,7 +207,7 @@ final public class EventBGenerator implements CheckerGenerator{ 
        for (Variable var : vars.values()) {

            actionNo++;

            ret += generateInitEventActionXmlPre(actionNo);

            ret += var.name();

            ret += var.outputName();

            ret += " ≔ 0";

            ret += generateInitEventActionXmlPost(actionNo);

            ret += "\n";

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

+2 −2
Original line number Diff line number Diff line
@@ -112,7 +112,7 @@ public class SMTLIBGenerator implements CheckerGenerator { 
        // Then generate all the variables.

        for (Variable var : vars.values()) {

            ret.append("(declare-fun ")

               .append(var.name())

               .append(var.outputName())

               .append(" () ")

               .append(GenerateVariableType(var.type()))

               .append(")\n");
@@ -122,7 +122,7 @@ public class SMTLIBGenerator implements CheckerGenerator { 
                ret.append("(assert (is")

                        .append(((EnumerationVariableType) var.type()).name())

                        .append(" ")

                        .append(var.name())

                        .append(var.outputName())

                        .append("))\n");

            }

        }

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

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

public class Variable implements Expression, ExpressionValue {

    public Variable(String name, VariableType type) {

        m_name = name;

        m_outputName = m_name = name;

        m_type = type;

    }
@@ -22,6 +22,22 @@ public class Variable implements Expression, ExpressionValue { 
        return m_type;

    }



    public String outputName()

    {

        return m_outputName;

    }



    /* This changes the variable as outputed by a CheckerGenerator.

     *

     * There are times when a user wants to rename a variable used in an Expression.  However, it would be weird to change

     * the actual name, as then the VariableCollection would be weird.  Instead, use a special output name, that is used

     * when generating code but is otherwise the same.

     */

    public void setOutputName(String outputName)

    {

        this.m_outputName = outputName;

    }



    @Override

    public VariableType actualOutputTypeForRequestedOutput(VariableTypeMarker requestedType) {

        if (requestedType.isMarkerFor(m_type)) {
@@ -30,15 +46,16 @@ public class Variable implements Expression, ExpressionValue { 
        return null;

    }



    private String m_name;

    private VariableType m_type;

    final private String m_name;

    private String m_outputName;

    final 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;

        return m_outputName;

    }



    @Override

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

+44 −3
Original line number Diff line number Diff line
@@ -50,6 +50,7 @@ public class GenericVariableDeclarationGeneratorTest { 
        return Arrays.asList(new Object[][]{

                {new SMTLIBGenerator(),

                        "(declare-fun x () Real)\n",

                        "(declare-fun new_x_name () Real)\n",

                        null,

                        null,

                        "(declare-sort MyEnum 0)\n" +
@@ -60,6 +61,14 @@ public class GenericVariableDeclarationGeneratorTest { 
                                "(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 new_x_name () MyEnum)\n" +

                                "(assert (isMyEnum new_x_name))\n",

                        "(declare-sort MyEnum 0)\n" +

                                "(declare-fun e1 () MyEnum)\n" +

                                "(declare-fun e2 () MyEnum)\n" +
@@ -73,9 +82,11 @@ public class GenericVariableDeclarationGeneratorTest { 
                },

                {new CVC3Generator(),

                        "x:REAL;\n",

                        "new_x_name: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;\nnew_x_name:MyEnum;\n",

                        "DATATYPE\n  MyEnum = e1 | e2 | e3\nEND;\nx:MyEnum;\ny:MyEnum;\n"

                },

                {new EventBGenerator(),
@@ -84,6 +95,12 @@ public class GenericVariableDeclarationGeneratorTest { 
                        "<org.eventb.core.event name=\"Event0\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"INITIALISATION\">\n" +

                        "<org.eventb.core.action name=\"InitAction1\" org.eventb.core.assignment=\"x ≔ 0\" org.eventb.core.label=\"act1\"/>\n" +

                        "</org.eventb.core.event>\n",

                        "<org.eventb.core.variable de.prob.units.inferredUnitPragmaAttribute=\"\" de.prob.units.unitPragmaAttribute=\"\" name=\"new_x_name\" org.eventb.core.identifier=\"new_x_name\"/>\n" +

                            "<org.eventb.core.invariant name=\"Invariant1\" org.eventb.core.label=\"inv1\" org.eventb.core.predicate=\"new_x_name ∈ ℤ\"/>\n" +

                            "<org.eventb.core.event name=\"Event0\" org.eventb.core.convergence=\"0\" org.eventb.core.extended=\"false\" org.eventb.core.label=\"INITIALISATION\">\n" +

                            "<org.eventb.core.action name=\"InitAction1\" org.eventb.core.assignment=\"new_x_name ≔ 0\" org.eventb.core.label=\"act1\"/>\n" +

                            "</org.eventb.core.event>\n",

                        null,

                        null,

                        null,

                        null,
@@ -98,15 +115,21 @@ public class GenericVariableDeclarationGeneratorTest { 
    public String RealExpectedOutput;



    @Parameter(value = 2)

    public String SignedFixedPointExpectedOutput;

    public String RealExpectedOutputWithNameChange;



    @Parameter(value = 3)

    public String UnsignedFixedPointExpectedOutput;

    public String SignedFixedPointExpectedOutput;



    @Parameter(value = 4)

    public String SingleVariableSingleEnumerationExpectedOutput;

    public String UnsignedFixedPointExpectedOutput;



    @Parameter(value = 5)

    public String SingleVariableSingleEnumerationExpectedOutput;



    @Parameter(value = 6)

    public String SingleVariableSingleEnumerationExpectedWithNameChangeOutput;



    @Parameter(value = 7)

    public String MultipleVariableSingleEnumerationExpectedOutput;



    @Test
@@ -117,6 +140,15 @@ public class GenericVariableDeclarationGeneratorTest { 
        }

    }



    @Test

    public void RealWithNameChangeTest() {

        if (RealExpectedOutputWithNameChange != null) {

            VariableCollection vars = variableParser.parseVariables("x");

            vars.getVariables().get("x").setOutputName("new_x_name");

            assertEquals(RealExpectedOutputWithNameChange, generator.GenerateVariablesDeclaration(vars));

        }

    }



    @Test

    public void SignedFixedPointTest() {

        if (SignedFixedPointExpectedOutput != null) {
@@ -141,6 +173,15 @@ public class GenericVariableDeclarationGeneratorTest { 
        }

    }



    @Test

    public void SingleVariableSingleEnumerationWithNameChangeTest() {

        if (SingleVariableSingleEnumerationExpectedWithNameChangeOutput != null) {

            VariableCollection vars = variableParser.parseVariables("x:MyEnum");

            vars.getVariables().get("x").setOutputName("new_x_name");

            assertEquals(SingleVariableSingleEnumerationExpectedWithNameChangeOutput, 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