TRAIAN 3.7 released on June 30, 2022



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

Release Notes

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

TRAIAN 3.7 brings four language changes, four library changes, ten static-semantics changes, five code-generation changes, and nineteen bug fixes (see below their description).


Language Changes

TRAIAN 3.7 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 demo examples have been updated to reflect these changes.

  1. A type pragma "!nopointer" was added to LOTOS NT, with associated semantic restrictions, namely: self-recursive types should not have this pragma and, in every set of mutually-recursive types, at least one type should not have this pragma. See item 392 in the HISTORY.txt file.

  2. Type pragmas of the form "!pointer N", where N is a natural number, have been removed from LOTOS NT. However, type pragmas of the form "!pointer" are kept.

    Users are advised to upgrade their LOTOS NT programs by running the following command:
       traian_upc 2022-LOTNT-POINTER [<file> or <directory>]
    
    that will perform the following actions:
    • "!pointer" pragmas (without parameter N) are kept unchanged.
    • "!pointer 0" pragmas are replaced by "!nopointer".
    • "!pointer 1" pragmas are replaced by "!pointer".
    • "!pointer N" pragmas (with N > 1) are replaced by "!card N".
    See item 393 in the HISTORY.txt file.

  3. Extra-checks on the use of type pragmas have been added for certain classes of LOTOS NT types:
    • The pragma "!list" must not be attached to non-list types.
    • The pragmas "!bits" and "!card" must not be attached to singleton or enumerated types.
    • The pragmas "!pointer" and "!nopointer" must not be attached to singleton, enumerated, or numeral types.
    See item 402 in the HISTORY.txt file.

  4. To further align the LNT and LOTOS NT languages, the syntax of LOTOS NT was extended to introduce array accesses, noted "X [V]", and array assignments, noted "X [V] := V0", in both LOTOS NT functions and processes. Notice that code generation for arrays is not implemented yet.

    The array syntax introduces ambiguity in expressions, as "Z1 [Z2]" can be understood either as an access to the Z2-th element of array Z1, or as a call to some constant function Z1 with a single event parameter Z2.

    To avoid such ambiguity, from now on, a call to some function F with a single event parameter E and no variable parameter should no longer be noted "F [E]" (which is now parsed by TRAIAN as an array access), but "F [E] ()". The same constraint applies to functions with multiple event parameters, i.e., "F [E0, ..., En]" should now be written "F [E0, ..., En] ()".

    Users will have to upgrade their specifications manually, since the change is too complex to be performed by the script "traian_upc". See item 404 in the HISTORY.txt file.




Library Changes

  1. The primitives of the "lotosnt_exceptions" library have been simplified:
    • The following four functions are no longer exported: TRAIAN_ADTI_exception_get_line(), TRAIAN_ADTI_exception_get_column(), TRAIAN_ADTI_exception_get_file(), TRAIAN_ADTI_exception_get_kind() (they are now declared to be "static").
    • The macro TRAIAN_ADTI_raise_exception_with_data, which was deprecated, has been removed.
    See item 368 in the HISTORY.txt file.

  2. The include file "lotosnt_predefined.h" was modified to use the standard definition of Booleans provided by <stdbool.h>. Consequently, it is no longer possible to use "bool", "false", and "true" as C identifiers in LOTOS NT pragmas such as "!implementedby", "!comparedby", etc. See item 369 in the HISTORY.txt file.

  3. The directory "ext/gtk3" was renamed to "ext/gtk" and the instructions for the Gtk editors (Gedit, Pluma, etc.) have been updated, so that the style files for LOTOS NT can also be used for Gtk4 (more recent) and Gtk5 (forthcoming). See item 403 in the HISTORY.txt file.

  4. Style files for supporting the Sublime Text editor have been added in directory "$LNTDIR/ext/sublime". See item 408 in the HISTORY.txt file.




Static-Semantics Changes

  1. The binding of loop identifiers was added in LOTOS NT processes. Although binding of identifiers in processes had been introduced in TRAIAN 3.6, binding of loop identifiers was still missing. See item 375 in the HISTORY.txt file.

  2. Dataflow analysis for LOTOS NT processes was undertaken. From now on, TRAIAN emits the following errors and warnings for processes:
       - variable X may be uninitialized
       - variable X never used
       - useless assignment to X
       - "in" parameter X modified (should be an "in var" parameter)
       - "in var" parameter X never modified (should be an "in" parameter)
       - "in var" parameter X overwritten before used (should be a local variable)
       - process with "out" parameter(s) but no normal termination
       - "out" parameter X both used and modified (should be an "out var" parameter)
       - process with "in out" parameter(s) but no normal termination
       - "out var" parameter X never used (should be an "out" parameter)
       - dead code after "raise" behaviour
       - loop label L never used
       - loop body is executed at most once
    
    etc. See item 377 in the HISTORY.txt file.

  3. Dataflow analysis was for event parameters of LOTOS NT processes. Consequently, TRAIAN may emit new warnings, such as:
       event parameter PRINT never used
    
    See item 381 in the HISTORY.txt file.

  4. Dataflow analysis of LOTOS NT processes was extended to handle loops, "case", "hide", "select", and "disrupt" behaviours. From now on, TRAIAN emits error messages when uninitialized variables are used in such constructs, and warnings for useless assignments to variables in processes. See item 389 in the HISTORY.txt file.

  5. Dataflow analysis was added for the "par" operator in LOTOS NT processes. From now on, new error messages are emitted, e.g.,
       - variable Y may be uninitialized
       - write-write conflict for variable X:
         X is assigned in the 1st and 2nd parallel branches
       - read-write conflict for variable X:
         X is modified in the 1st, 3rd, and 5th parallel branches
         but used in the 2nd, 4th, and 6th parallel branches
    
    etc. See item 394 in the HISTORY.txt file.

  6. TRAIAN was enhanced to accept LOTOS NT programs that were previously rejected, e.g.:
       process MAIN [PRINT: any] is
          var X, Y : BOOL in
             X := any Bool;
             if X then
    	    Y := not (X)
             else
    	    stop
             end if;
             PRINT (Y)
          end var
       end process
    
    This program was rejected with an error message stating that variable Y was possibly uninitialized in PRINT (Y). From now on, such programs are accepted, as TRAIAN discards the "else" branch, since no execution can take place after "stop". See item 395 in the HISTORY.txt file.

  7. Warnings have been added about unused variables declared in "case" instructions of LOTOS NT processes (such warnings were already implemented in LOTOS NT functions). For instance:
       process P [PRINT : any] (X : T) is
          case X
          var Y : nat in
    	 C1 -> PRINT ("C1")
          |  C2 (any) -> PRINT ("C2")
          end case
       end process
    
    triggers the following warning:
       variable Y never used
    
    See item 397 in the HISTORY.txt file.

  8. Dataflow analysis and dead-code detection were added for the "trap" instructions of LOTOS NT processes, leading to warnings of the following form:
       - dead code after infinite loop
       - dead code after "raise" and "stop" behaviours
       - dead code after "stop" behaviour
    
    See item 399 in the HISTORY.txt file.

  9. Checks have been added on "for" loops present in LOTOS NT processes. In particular, the "stop" behaviour, if used in the initialization or progression of a "for" loop now triggers warnings of the following form:
       illegal behaviour in initialization of "for" loop
    
    See item 400 in the HISTORY.txt file.

  10. A warning was for the events declared, but never accessed, in a "hide" operator:
       hidden event G never accessed
    
    See item 401 in the HISTORY.txt file.




Code-Generation Changes

  1. The C code generation was extended to support the following kinds of behaviours that may occur in LOTOS NT process definitions:
    • "var" ... "end var" definitions,
    • assignment of variables,
    • events having more than one parameter.
    Thus, TRAIAN may handle more LOTOS NT specifications, removing a few error messages of the following form:
       processes not yet fully implemented
    
    See item 366 in the HISTORY.txt file.

  2. The C code generated by TRAIAN for ordinary types was enhanced by initializing statically allocated C structures. Such initialization, achieved by a call to a new macro TRAIAN_CLEAR(), avoids warnings emitted by Gcc. See item 370 in the HISTORY.txt file.

  3. The former versions of TRAIAN, in case of an error, could leave incompletely generated "*_f.h" and "*_t.h" files in the working directory. From now on, TRAIAN removes such incomplete files when compilation aborts. These files are only removed if they contain the tag:
       /* generated by traian 3.7 */
    
    which prevents unintended deletion of user files that would be also named "*_f.h" or "*_t.h". See item 383 in the HISTORY.txt file.

  4. The C code generator of TRAIAN now takes into account the "!card N" pragmas attached to LOTOS NT types. Previously, these pragmas had no effect. From now on, they have the same meaning as "!pointer N" pragmas (which will soon be deprecated). See item 390 in the HISTORY.txt file.

  5. The C code generator of TRAIAN now take into account the "!bits N" pragmas attached to tuple and ordinary types. See item 391 in the HISTORY.txt file.




Bug Fixes

  1. When a LOTOS NT channel had several profiles, TRAIAN could report that some event offers were wrongly typed. For instance, given the following LOTOS NT code:
       channel C is
          (x1: INT),
          (x1, x2: INT)
       end channel
       ...
       hide G:C in
          G (0)
       end hide
    
    TRAIAN emitted the following error message:
       event G used with incorrect type
       ...
       channel C cannot match the offer type:
         (NAT|INT)
    
    From now on, TRAIAN accepts the above code without errors, as the profiles of channel C are used to resolve overloading of constant 0, the type of which is either NAT or INT. See item 367 in the HISTORY.txt file.

  2. The dataflow-analysis rules for "trap" instructions have been corrected, as TRAIAN 3.6 accepted incorrect LOTOS NT programs, such as:
       trap
          exception E is
             return Y
       in
          for X := N while X -[E] M > 1 by X := X -[UNEXPECTED] M
          loop
             Y := X;
             use Y
          end loop
       end trap
    
    where variable Y is used in the event handler for event E, but could be uninitialized at this point, because E can be triggered from the "while" condition of the "for" loop (possibly before the first iteration), whereas Y is only initialized in the loop body. From now on, the events raised in the "while" condition of a loop are taken into account by the dataflow analysis. See item 371 in the HISTORY.txt file.

  3. The dataflow-analysis rules for "trap" instructions have been modified, as TRAIAN 3.6 rejected correct programs such as:
       trap
          exception E is
             return X
       in
          eval P (?X);
          raise E
       end trap
    
    by reporting that X was not initialized in the event handler, because all variables passed as "out" parameters to a function without result (e.g., "?X" in the above example) were not taken into account when determining the variables initialized before an event is raised. See item 372 in the HISTORY.txt file.

  4. The dataflow-analysis rules for "trap" instructions have been modified, as TRAIAN 3.6 accepted incorrect LOTOS NT programs, such as:
       trap
          exception E is
             return Y
       in
          eval Y := F [E] (!?X)
       end trap
    
    where variable Y could be used before being initialized in the handler for event E. From now on, the events raised in procedure calls are more finely analyzed. See item 373 in the HISTORY.txt file.

  5. The dataflow analysis in LOTOS NT functions was modified, so as to take into account the occurrences of variables in "require" and "ensure" clauses, which were formerly ignored. Consequently, more warnings can be emitted. See item 374 in the HISTORY.txt file.

  6. An issue was fixed in dataflow analysis for variables, since TRAIAN rejected correct programs such as:
       function F (in var X: BOOL) : BOOL is
          var Y: BOOL in
             for null while X by X := Y loop
    	    Y := false
             end loop;
             return X
          end var
       end function
    
    where some variable Y was properly initialized in the body of a "for" loop and used in the "by" clause of this loop. See item 376 in the HISTORY.txt file.

  7. An issue was fixed in the dataflow analysis of TRAIAN 3.6, which was accepting incorrect LOTOS NT programs such as:
       function F (X : bool) : bool is
          var Y : bool in
             for null while X by null loop
    	    Y := true
             end loop;
             return Y -- not initialized if X is false
          end var
       end function
    
    From now on, TRAIAN no longer assumes that the body of a "for" loop is executed at least once, which is not certain, and emits the following error message:
       variable Y may be uninitialized
    
    for the above example. See item 378 in the HISTORY.txt file.

  8. When binding event identifiers, TRAIAN wrongly considered that an event declared by an "exception" clause was visible inside this clause. Thus, TRAIAN accepted incorrect LOTOS NT programs such as:
       function F : BOOL is
          trap
             exception Y is
    	    raise Y
          in
             ...
          end trap
       end function
    
    See item 379 in the HISTORY.txt file.

  9. Due to an issue in the typing of process calls. TRAIAN 3.6 could reject correct LOTOS NT programs with error messages such as:
       process P called with incorrect profile
       in behaviour
          P [E]
       the call uses process profile:
          P [none]
       but the called process has profile:
          P [any]
    
    See item 380 in the HISTORY.txt file.

  10. Due to an issue in dataflow analysis for event parameters of functions, TRAIAN 3.6 could emit spurious warnings such as:
      event parameter E never accessed
    
    even if E was used in the "raise" part of a "require" or "ensure" clause of the function where E was declared. From now on, pre- and post-conditions are taken into account when analyzing event parameters. See item 382 in the HISTORY.txt file.

  11. TRAIAN did not take into account "access" clauses when checking whether an event parameter of a function is used; thus, the dataflow analysis could emit incorrect warnings such as:
       event parameter E never accessed
    
    even if an "access E" instruction was present. See item 384 in the HISTORY.txt file.

  12. Due to a dataflow-analysis issue, TRAIAN 3.6 could accept incorrect LOTOS NT programs such as:
       function F (out X:NAT, Y:NAT) : BOOL is
          loop
             if Y > 0 then 
    	    loop
    	       null
    	    end loop
             end if;
             return false
          end loop
       end function
    
    Formerly, only a warning was displayed:
       function with "out" parameter(s) but no normal termination
    
    From now on, a fatal error message is emitted:
       function F may return without assigning parameter X
    
    See item 385 in the HISTORY.txt file.

  13. Stricter checks have been implemented in the syntax of C identifiers introduced by pragmas such as "!implementedby", etc. Formerly, TRAIAN did not perform stringent verifications and accepted invalid C identifiers such as "||", "or else", "FILE *", etc. See item 386 in the HISTORY.txt file.

  14. The previous versions of TRAIAN accepted incorrect LOTOS NT programs such as:
       function F (out X : BOOL) is
          return;
          X := false
       end function
    
    From now on, occurrences in dead code of assignments to "out" parameters are ignored, so that the above program triggers an error message of the following form:
       function F may return without assigning parameter X
    
    See item 387 in the HISTORY.txt file.

  15. A bug was fixed in dataflow analysis, which rejected correct LOTOS NT programs such as:
       function F (X : BOOL) : BOOL is
          loop L in
             return not (X);
             break L -- (this is dead code)
          end loop
       end function
    
    with the following error message:
       function F may terminate without returning a value
    
    From now on, such programs are accepted by TRAIAN, as dataflow analysis no longer considers occurrences of "break" instructions in dead code. See item 388 in the HISTORY.txt file.

  16. The dataflow analysis for event handlers was revised, so as to accept programs that were previously rejected, e.g.:
       function F (X : NAT) : NAT is
          var X1, X2 : NAT in
             trap
    	    exception E is
    	       return X1 + X2
             in
    	    X2 := 0;
    	    if X < 3 then
    	       X1 := 0;
    	       raise E
    	    else
    	       return 0
    	    end if
             end trap
          end var
       end function
    
    for which TRAIAN 3.6 emitted an error message:
       variable X1 may be uninitialized
    
    in the event handler. From now on, dataflow analysis for "raise" is aligned on the analysis for "break" intructions. See item 396 in the HISTORY.txt file.

  17. The dataflow analysis was modified to avoid producing spurious warnings about useless assignments to variables in loops, when these variables are used after the loop but not inside the loop. For instance, the following LOTOS NT functions now compile without warning:
       function F1 (X : Bool) : Bool is
          var Y : Bool in
             loop L in
    	    if X then
    	       break L
    	    end if;
    	    Y := not (X) -- no more warning here
             end loop;
             return Y
          end var
       end function
    
       function F2 [E : none] (X : T, out Y : BOOL, Z : BOOL) is
          loop L in
             case X in
    	    NIL ->
    	       if Z then
    	          raise E
    	       else
    	          Y := false; -- no more warning here
    	          break L
    	       end if
             |  any ->
    	       Y := true -- no more warning here
             end case
          end loop
       end function
    
    See item 398 in the HISTORY.txt file.

  18. The definition of iterators on numeral types was modified to lower the upper bound (ADT_INT_MAX was replaced by ADT_INT_MAX - 1), thus avoiding an overflow that caused Gcc warnings of the following form:
       integer overflow detected: op "+"
    
    The implementation of the succ() and card() functions for these types have been updated accordingly. See item 405 in the HISTORY.txt file.

  19. The C code generated was simplified, by removing
       #ifdef lint
       ...
       #endif
    
    directives that caused Gcc 10 warnings. See item 406 in the HISTORY.txt file.




Future Work

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


Download

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

http://vasy.inria.fr/traian