loonwerks / formal-methods-workbench

Other
20 stars 7 forks source link

AGREE does not handle base type implementations #17

Closed kfhoech closed 5 years ago

kfhoech commented 5 years ago

Translation to Lustre model does not handle AADL typing constructs as illustrated below.

First the declarations of types:

package Alpha::Bravo
public
    with Data_Model;
    with Base_Types;

    data Delta1 extends Base_Types::Integer
    end Delta1;

    data implementation Delta1.impl
    end Delta1.impl;

    data Charlie
        properties
            Data_Model::Data_Representation => Struct;
    end Charlie;

    data implementation Charlie.impl
        subcomponents
            id : data Delta1.impl;
    end Charlie.impl;

end Alpha::Bravo;

and use in:

package Scratch
public
    with Alpha::Bravo;

    system ScratchSys
        features
            sout : out event data port Alpha::Bravo::Charlie.impl;
        annex agree {**
            const id : Alpha::Bravo::Delta1.impl = 123456;
            guarantee "sout id is set" : sout.id = id;
        **};
    end ScratchSys;

end Scratch;

The validator issues the message that the types are mismatched (at the declaration of the constant). But, this should be a valid constant declaration.

In translation the implementation of the base type is apparently incorrectly rendered as a JLustre record type with zero elements (which is illegal in JLustre) and an inappropriate rendering of a primitive.

kfhoech commented 5 years ago

Also note that multiple extensions are not handled correctly. The type inference must be able to recurse these to the primitive base type as appropriate.

Here's another simple package that illustrates the problem:

package PrimRecTypeProblem
public

    with Base_Types;

    data unsigned_long extends Base_Types::Unsigned_32
    end unsigned_long;

    data implementation unsigned_long.impl
    end unsigned_long.impl;

    data NumericID extends unsigned_long
    end NumericID;

    data implementation NumericID.impl extends unsigned_long.impl
    end NumericID.impl;

    data NumericGUID extends NumericID
    end NumericGUID;

    data implementation NumericGUID.impl extends NumericID.impl
    end NumericGUID.impl;

    annex agree {**
        -- Ok
        const btu0 : Base_Types::Unsigned_32 = 400;

        -- Incorrect type inference results in error:
        -- The assumed type of constant statement 'ul0' is 'com.rockwellcollins.atc.agree.AgreeTypeSystem$RecordTypeDef@733f0615'
        -- but the actual type is 'IntTypeDef'
        const ul0 : unsigned_long.impl = 400;

        -- Ok
        const ul1 : unsigned_long = 400;

        -- Incorrect type inference results in error:
        -- The assumed type of constant statement 'idNum0' is 'com.rockwellcollins.atc.agree.AgreeTypeSystem$RecordTypeDef@7bea7885'
        -- but the actual type is 'IntTypeDef'
        const idNum0 : NumericId.impl = 400;

        -- Incorrect type inference results in error:
        -- The assumed type of constant statement 'idNum1' is 'ErrorTypeDef'
        -- but the actual type is 'IntTypeDef'
        const idNum1 : NumericId = 400;

        -- Incorrect type inference results in error:
        -- The assumed type of constant statement 'guidNum0' is 'com.rockwellcollins.atc.agree.AgreeTypeSystem$RecordTypeDef@2ebf6744'
        -- but the actual type is 'IntTypeDef'
        const guidNum0 : NumericGUID.impl = 400;

        -- Incorrect type inference results in error:
        -- The assumed type of constant statement 'guidNum1' is 'ErrorTypeDef'
        -- but the actual type is 'IntTypeDef'
        const guidNum1 : NumericGUID = 400;
    **};

end PrimRecTypeProblem;
kfhoech commented 5 years ago

Resolved by commit bbf1420505d360b127f11f93f28657dd416ad23a.