TRAIAN 3.3 released on February 28, 2021



The CONVECS team is pleased to announce that version 3.3 of the TRAIAN compiler for LOTOS NT is available.

Release Notes

TRAIAN 3.3 has been prepared by Hubert Garavel, Frederic Lang, and Wendelin Serwe. It was released four months after version 3.2 of TRAIAN.

TRAIAN 3.3 brings six language changes, six compiler changes, eight code-generation changes, one miscellaneous change, and two bug fixes (see below their description).


Language Changes

TRAIAN 3.3 introduces various changes to the LOTOS NT language in order to further align it with the LNT language supported by the CADP toolbox. The LOTOS NT Reference Manual and the style files for text editors have been updated to reflect these changes.

  1. The Boolean operator "implies" was renamed to "=>". From now on, "implies" is no longer a reserved keyword of LOTOS NT and can thus be used as an identifier. Users are advised to upgrade their source LOTOS NT files using the command:
       traian_upc 2020-LOTNT-IMPLIES [<file> or <directory>]
    
    See item 249 in the HISTORY.txt file.

  2. The short-circuit Boolean operators "andthen" and "orelse" have been renamed to "and then" and "or else", respectively. From now on, "andthen" and "orelse" are no longer reserved keywords of LOTOS NT and can thus be used as identifiers. Users are advised to upgrade their source LOTOS NT files using the two commands:
       traian_upc 2020-LOTNT-ANDTHEN [<file> or <directory>]
       traian_upc 2020-LOTNT-ORELSE [<file> or <directory>]
    
    See item 252 in the HISTORY.txt file.

  3. The six predefined operators "and", "div", "mod", "or", "rem", and "xor", together with the two short-circuit operators "and then" and "or else" must now be written in lower case only. The six operators become reserved LOTOS NT keywords, but can be redefined as (overloaded) function identifiers. The upper case names of these operators ("AND", "DIV", etc.) are no longer predefined and can be used as identifiers. Lower- and upper-case combinations of these operator names ("AnD", "Div", etc.) are no longer forbidden, but trigger warnings. See item 254 in the HISTORY.txt file.

  4. LOTOS NT has been extended with a new "use" instruction, which is similar to that of LNT. See item 256 in the HISTORY.txt file.

  5. The precedences of infix LOTOS NT operators have been redefined, evolving from three levels:
       0. Pseudo-operators "of", "." (field selection and update)
       1. and, and then, /, div, mod, rem, *, **
       2. or, or else, xor, +, -
       3. ==, !=, <, <=, >=, >, =>, <=>
    
    to six levels:
       0. Pseudo-operators "of", "." (field selection and update)
       1. User-defined infix operators
       2. **
       3. *, /, div, mod, rem
       4. +, -
       5. ==, =, !=, <, <=, >=, >
       6. and, and then, or, or else, xor, =>, <=>
    
    Because this change is not backward compatible, TRAIAN 3.3 emits warnings if the new precedence rules modify the way an expression is parsed. Such warnings can be silenced by adding extra parentheses, or by inserting a pragma !update "2021-b" in the file, or by setting the environment variable $LNT_UPDATE to "2021-b". Users are advised to upgrade their source LOTOS NT files using the command:
       traian_upc 2021-LOTNT-PRIORITIES [<file> or <directory>]
    
    See item 259 in the HISTORY.txt file.

  6. The predefined operator "CONCAT" for string concatenation was renamed to "&". Users should upgrade their LOTOS NT programs manually, either by replacing all occurrences of "CONCAT" with "&", or by inserting a backward-compatibility definition of the "CONCAT" function. See item 263 in the HISTORY.txt file.




Compiler Changes

  1. TRAIAN now warns about "case" branches that can never be executed because they occur after a pattern that matches all possible values (e.g., a free variable or an "any" pattern). See item 248 in the HISTORY.txt file.

  2. The error message "variable X not assigned in this branch but in some other branch(es)" was changed to a mere warning, because it expresses a sufficient, yet not necessary condition for correctness and is superseded by data-flow analysis of uninitialized variables. See item 257 in the HISTORY.txt file.

  3. Four error messages about dead code following a "break" instruction, a nonterminating loop, a "raise" instruction, or a "return" instruction have been turned into mere warnings, because dead code is undesirable but not incorrect. See item 258 in the HISTORY.txt file.

  4. TRAIAN now warns about expressions in which infix Boolean operators are combined without parentheses (as in, e.g., "X xor Y and Z"). Such new checks uncovered two subtle bugs in the FSP2LOTOS and SVL compilers, which are written in LOTOS NT and compiled using TRAIAN. See item 260 in the HISTORY.txt file.

  5. TRAIAN also warns about expressions combining, without parentheses, infix logical operators (such as "and", "or", etc.) and infix comparison operators (such as "==", "<", etc.) as in, e.g., "X == Y or Z". See item 261 in the HISTORY.txt file.

  6. TRAIAN also warns about expressions that combine, without parentheses, infix user-defined operators, as in, e.g., "X IsIn Y @ Z"). See item 262 in the HISTORY.txt file.




Code-Generation Changes

  1. The C code generated by TRAIAN was made more readable by adding missing end-of-lines, removing useless ones, removing extra dash lines, and removing "/* empty */" comments generated for the "null" instructions of LOTOS NT. See item 243 in the HISTORY.txt file.

  2. The C code generated for "case" instructions was simplified by removing the conditions "if (ADT_TRUE ())" generated for patterns that match all possible values. See item 244 in the HISTORY.txt file.

  3. The C code generated for "case" instructions was simplified by no longer generating dead code when all "case" branches are statically known to be exhaustive. See item 245 in the HISTORY.txt file.

  4. The C code generated for "case" instructions was simplified by no longer producing duplicated code for "case" branches guarded by multiple patterns. See item 246 in the HISTORY.txt file.

  5. The C code generated for "case" instructions was made more portable by no longer producing GNU-specific "__label__ L" statements. See item 247 in the HISTORY.txt file.

  6. The C code generated for "case" instructions was simplified by gathering the declarations of C variables and eliminating useless nested blocks "{...}". See item 250 in the HISTORY.txt file.

  7. The C code generated for "case" instructions was simplified by no longer generating useless assignments "X = X;", which caused warnings from the Clang compiler. See item 251 in the HISTORY.txt file.

  8. The C code generated for the LOTOS NT variables declared inside loops was simplified, thereby avoiding warnings from the Clang compiler. See item 253 in the HISTORY.txt file.




Miscellaneous Changes

  1. The LOTOS NT code of demo 04 was updated to get it accepted by TRAIAN 3.3. See item 265 in the HISTORY.txt file.




Bug Fixes

  1. The data-flow algorithms inherited from TRAIAN 2.x to statically detect uninitialized variables were not strict enough for "case" instructions and could accept some incorrect LOTOS NT programs. See item 255 in the HISTORY.txt file.

  2. The data-flow algorithms for statically detecting uninitialized variables were too coarse for "trap" instructions and rejected some meaningful LOTOS NT programs. See item 264 in the HISTORY.txt file.




Future Work

TRAIAN 3.3 will continue to evolve, our goal being to merge LOTOS NT and LNT in one single language.


Download

TRAIAN 3.3 can be freely downloaded from the TRAIAN Web Page located at:

http://vasy.inria.fr/traian