Variable views

The Siemens PLC programming languages allow the declaration of variable views. A variable view behaves as a variable in the local scope, however it is mapped to the memory area of another variable. Therefore the storage variable and its referencing variable view will always contain the same value (on the bit level) SCL definition, Sec. 8.4, p. 8-5. The two variables may have different data types (in fact this is the purpose of variable views).

Example.

    VAR
        storage : WORD;
        view AT storage : ARRAY[0..15] OF BOOL;
    END_VAR

In this example, storage is a real variable, and view is a variable view at storage. In the local scope both storage and view can be used, but the modification of one of them will be reflected by the other. For example, after the variable assignment storage := WORD#16#FFFF; all bits of the array view will be set to TRUE.

[info] Endianness

Note that ("classic") Siemens S7 PLCs use big endian memory representation. This means that the MSB is towards the lower part of the address range, the LSB is towards the higher part of the address range. This is also true for the bit numbering within a byte: bit 0 that is the LSB for an integer is at the higher part of the address range. This bit addressing will be used for arrays too. In case of an ARRAY[0..15] OF BOOL, the element [0] will be at byte 0, bit 0; [1] at byte 0, bit 1; [7] at byte 0, bit 7; [8] at byte 1, bit 0, etc. However, it means that the bits in the memory will not follow the "natural order" for the array elements. Notice that at the byte boundary the adjacent bits are byte 0, bit 0 and byte 1, bit 7; corresponding to the array elements [0] and [15]. Consequently, in this example storage := 1 will make view[8] true (all other bits of the array will be false); storage := 256 will make view[0] true.

Memory representation
Figure: Memory representation

Example. A more comprehensive example is shown below.

VAR
  s : DWORD;

  a AT s : STRUCT
      a1 : WORD;
      a2 : WORD;
    END_STRUCT;

  b AT s : STRUCT
      b1 : BYTE;
      b2 : BYTE;
      b3 : BYTE;
      b4 : BYTE;
    END_STRUCT;

  c AT s : ARRAY[0..3] OF BYTE;

  d AT s : ARRAY[0..31] OF BOOL;
END_VAR
Memory representation
Figure: Memory representation

Important properties

  • The variable views are only visible in the block that are declaring them. Consequently, variable views cannot be used in function calls.
  • Transitive variable views are not permitted. However, multiple views at the same storage variable are permitted.

    Example.

        VAR
            v1 : WORD;
            v2 AT v1 : ARRAY[0..15] OF BOOL;
            v3 AT v2 : ARRAY[0..15] OF BOOL; // invalid, view at a view
        END_VAR
    
    • The offset of the array is not taken into account.

      See the following example:

        VAR
            array1 : ARRAY[0..15] OF BOOL;
            array2 AT array1 : ARRAY[100..115] OF BOOL;
        END_VAR
        BEGIN
            array1[0] := TRUE; // side effect: array2[100] became TRUE too
            ...
      

      Memory representation

  • It is possible to have variable views between complex types.

    Example.

        VAR
            struct1 : STRUCT
                        a : WORD;
                        b : BOOL;
                    END_STRUCT;
            struct2 AT struct1 : STRUCT
                        a2 : ARRAY[0..15] OF BOOL;
                        b2 : BOOL;
                    END_STRUCT;            
        END_VAR
    

    Memory representation

    Example.

        VAR
            storage : STRUCT
                        s1 : WORD;
                      END_STRUCT; 
            view AT storage : STRUCT
                        v1 : BYTE;
                        v2 : BYTE;
                      END_STRUCT;
        END_VAR
    

    Memory representation

  • It is possible to have variable views across variable boundaries.

    Example.

        VAR
            storage : STRUCT
                        s1 : BYTE;
                        s2 : WORD;
                        s3 : BYTE;
                      END_STRUCT; 
            view AT storage : STRUCT
                        v1 : WORD;
                        v2 : ARRAY[0..15] OF BOOL;
                      END_STRUCT;
        END_VAR
    

[warning] Memory layout and byte alignment

The compiler follows certain rules when it maps the variables to memory addresses. In this example above,
there will be one byte of unused space ("filling byte") between variables storage.s1 and storage.s2, in order to align the WORD variable s2 to an odd byte. This filling byte will have an unknown value. Consequently, the lower byte of view.v1 will be mapped to this uninitialized memory area.

Memory representation

PLCverif DOES NOT take this behavior into account.

Example for a similar issue: Memory representation

    VAR
        storage : STRUCT
                    s1 : BYTE;
                    s2 : WORD;
                  END_STRUCT; 
        view AT storage : STRUCT
                    v1 : BYTE;
                    v2 : BYTE;
                    v3 : BYTE;
                    v4 : BYTE;
                  END_STRUCT;
    END_VAR

Representation in CFA

Vocabulary

  • An elementary variable (or just variable) is a unit of data having SCL elementary type, e.g. BOOL or WORD. An SCL variable having STRUCT or ARRAY type is not an elementary variable. An element of an array is also considered as an elementary variable.
  • A slice is a part (consecutive bits) of an elementary CFA field (which itself represents an elementary variable), identified by the start and end bit indices.
    • The length of a slice is end bit - start bit + 1.
    • A slice with length 1 is simply called bit.
    • The whole elementary field is also considered as a slice, starting at bit 0 and ending at data length - 1. The slice is sometimes referred to as complete slice or whole slice.
  • A data mapping is a definition of a slice based on some expression.
    • The defined data is the field or slice that is defined by the data mapping.
    • The definition is the expression that is used to define the defined data.
    • A data mapping is invalidated if its definition changes value.
    • A data mapping is enforced or its defined data refreshed, when the mapping is re-established by performing the necessary assignments.

Representation overview

The top-level variable views are identified on the AST (i.e. s1 AT s2 is identified, but not the implicit mapping between s1.a and s2.a). Then the representation is done at the CFA level (on the CFA declaration).

To provide support for a rich feature set, the variable views of the PLC programs are represented according to the following principles.

  • Both the view and storage variables are represented as fields (viewer field and storage field in the following).
  • The connection between the view and storage fields is represented by data mappings. These data mappings are unidirectional, i.e. they represent a mapping in only one direction. For example, a data mapping may require that "if field a changes, the field b shall be refreshed based on a, according to this mapping". The field that is updated is the defined field, the expression defining the value of this field is the definition or defining expression. E.g. in the previous example, b is the defined field, a is the definition expression.
    • Data mappings are defined between elementary fields or slices of elementary fields. I.e., no data mapping is created to represent the mapping between s1 and s2 in the example above; instead mappings between the elementary fields s1.a and s2.a will be created.
    • Note the due to the different sizes of elementary fields, a data mapping may need to define a (non-complete) slice of a field.
    • For each variable view, two sets of data mappings will be created: one defining the viewer based on the storage, and another one defining the storage between the viewer.
  • At the beginning of each automata all viewer fields are refreshed based on the values of the storage fields.
  • After the modification of a storage or viewer field, the corresponding data mappings (both regular and inverse) are enforced by inserting their representation into the automaton.
    • Note that at this stage the direction of the data constraint does not matter, i.e. it does not matter if it is a regular or an inverse constraint. All mappings will be refreshed where any field used in the definition was updated.
    • If due to the modification of a viewer field, the corresponding storage field was refreshed, the eventual other viewers of the same storage field are refreshed too.

Implementation details

The (top-level) variable views are identified on the AST by the AstVarView.collect methods which generate AstVarView instances.

The CFA data mappings are created by the CfaDataMappingBuilder class. It first locates the (potentially non-elementary) fields corresponding to the AST variables (in method CfaDataMappingBuilder.createMappings).

Then the CfaDataMappingBuilder.createElementaryMappings method will locate the memory areas corresponding to each other. This will result in the biggest slices corresponding to each other. To facilitate this, MemoryArea objects will be created. Each MemoryArea object represents an elementary field, starting at a given bit position in the memory. (The start positions are relative to the start of the top-level variable view to be represented.) The data mappings for the determined slice-pairs will be created by representMapping, calling CfaDataMapping.create.

There are various classes describing the required data mappings on the CFA level.

CfaDataMappingBitDefinedByBoolExprFieldDefinedByExpressionBitDefinedByBoolFieldBitDefinedByBitFieldDefinedByFieldBoolFieldDefinedByBit

  • CfaDataMapping: generic class to represent data mappings in one direction. The defined data can be a whole elementary field or a part of a field.
    • FieldDefinedByExpression: data mapping that defines a whole elementary field, based on some expression.
      • FieldDefinedByField: data mapping that defines a whole elementary field, based on another whole elementary field.
      • BoolFieldDefinedByBit: data mapping that defines a (whole) Boolean elementary field, based on a given bit of an elementary field.
    • BitDefinedByBoolExpr: data mapping that defines a one-bit-long slice of an elementary field, based on some (Boolean) expression.
      • BitDefinedByBoolField: data mapping that defines a one-bit-long slice of an elementary field, based on a Boolean field.
      • BitDefinedByBit: data mapping that defines a one-bit-long slice of an elementary field, based on a given bit of an elementary field.

See Javadoc

The CfaDataMapping.create method will determine which CFA mapping type is appropriate to represent the mapping between the two given slices. Several cases are possible

  • There can be a one-to-one mapping between two fields (i.e. the defining and the defined slices are both complete fields). In this case, a single FieldDefinedByField will be created, practically representing a defined <- defining mapping.
  • A whole field can be defined based on a slice of another field.
    • If the slices are one bit long, then the defined field is a Boolean field. In such case, a BoolFieldDefinedByBit object will be created.
    • Otherwise, a field is defined based on a non-zero-length slice. It will be represented by creating one BitDefinedByBit mapping for each corresponding bit-pairs in the slice-pair.
  • The defined slice can be a non-whole field, defined by a (whole or non-whole) slice. If the length of the slices is one bit, then a BitDefinedByBoolVar mapping will be created, otherwise it will be represented by creating one BitDefinedByBit mapping for each corresponding bit-pairs in the slice-pair.

Common cases:

  • Defining a Boolean array a based on a word w: For each elementary field of the array a, a BoolFieldDefinedByBit will be created.
  • Defining a word w based on a Boolean array a: For each bit of the word w, a BitDefinedByBoolField will be created.
    • Note that refreshing such CFA data mapping will be represented as a conditional branch, essentially meaning IF a[N] THEN w := w OR 00..0100..0; ELSE w := w AND 11..1011..1; END_IF;.
  • One-to-one elementary field mapping (e.g. s1.a mapped to s2.a), without type change (same CFA types): a FieldDefinedByField is created.

Current limitations

  • Multi-dimensional arrays are not tested.
  • ANY data type is not supported.
  • Byte alignment is not taken into account.
  • REAL AT WORD is not handled correctly. To handle REAL AT WORD correctly, bit-level representation of IEEE floating-point numbers would be needed that is not planned for the moment.

    Example.

    VAR
        r : REAL;
        w AT r : WORD;
    END_VAR
    BEGIN
      r := 3.1415;
      // value of w is now 0x40490E56 = 0b01000000 01001001 00001110 01010110
      //    --> sign: '1'
      //              +
      //    --> exponent: '10000000'
      //                  (128-127) = 1
      //    --> mantissa: '10010010000111001010110'
      //                  1 + 1/2 + 1/16 + 1/128 + 1/4096 + 1/8192 + 1/16384 + 1/131072 + 1/524288 + 1/1048576 = 1.57075023651
      //    ==> 1.57075023651 * 2^1 = 3.14150047302
    
  • Check what happens if type conversion is needed (e.g. INT AT WORD).

results matching ""

    No results matching ""