TRAIAN 3.10 released on June 30, 2023

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

Release Notes

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

With TRAIAN 3.10, the convergence between LOTOS NT and LNT is nearly complete. Measured on a test suite of 13,500+ correct LNT programs totalling more than 9 million non-blank lines of LNT code, TRAIAN 3.10 syntactically accepts 100% of these programs and semantically accepts 93.5% of them (whereas TRAIAN 3.9 accepted 89.3% of them).

TRAIAN 3.10 brings seven language changes, six compiler changes, four code-generation changes, six library changes, two release changes, and thirteen bug fixes (see below their description).

Language Changes

LOTOS NT and TRAIAN have been extended to enable one attaching !implementedby pragmas to the NIL and CONS constructors of list types, so as to force TRAIAN using user-specified C identifiers for these functions. This is now possible by mentioning these constructors in the "with" clauses of list types, e.g.:
```
   type T is
      list of Nat
   with
      == !implementedby "EQ_T",
      NIL !implementedby "NIL_T",
      CONS !implementedby "CONS_T"
   end type
```
Formerly, such definitions were rejected by TRAIAN 3.9 with the following error messages:
```
   error: unknown function NIL in "with" clause of type T
   error: unknown function CONS in "with" clause of type T
```
See item 493 in the HISTORY.txt file.

The syntax of LOTOS NT patterns was enhanced. Formerly, only the unary "-" operator could be used without parentheses (e.g., "- X") while all other unary operators required parentheses. From now on, all unary operators with non-alphabetic identifiers can be used without parentheses. For instance, it is now possible to write "+ X", "++ X", "& X", etc., whereas this would formerly cause syntax errors; one had to write "+ (X)", "++ (X)", "& (X)", etc.
This change has minor side effects. For instance, the pattern:
```
   X * any T + Y
```
which was formally rejected with a syntax error, is now syntactically accepted and parsed as follows:
```
   (X * any) T (+ Y)
```
possibly followed by an error if function T is undefined. Similarly, the pattern:
```
   X as any T + Y
```
which was formally rejected, is now syntactically correct. See item 495 in the HISTORY.txt file.

The syntax of LOTOS NT patterns was modified to give higher precedence to "of" over unary prefix operators. For instance, pattern (-2 of Int) was previously parsed as (-2) of Int, because "of" was considered as some kind of binary operator, whereas it is now parsed as -(2 of Int), because "of" is now considered as a unary postfix operator (like the field selection operator "."). See item 496 in the HISTORY.txt file.

LOTOS NT and TRAIAN have been extended to permit attaching !external pragmas to the "with" clauses of non-external types. For instance, the following type definition:
```
   type T is
      A, B, C
      with > !external !implementedby "C:GT"
   end type
```
was formerly rejected with an error message:
```
   error: unexpected pragma !external for predefined operation >
```
From now on, this type definition is accepted. TRAIAN does not generate any C code for the external function, but inserts a C comment stating that the user should provide an implementation for this function in the ".fnt" file.
Also, if the !external pragma does not come together with an !implementedby pragma, e.g.:
```
   type T is
      A, B, C
      with > !external
   end type
```
TRAIAN now emits the following warning:
```
   warning: missing pragma !implementedby "C:..." for external function >
```
The TRAIAN Reference Manual was updated accordingly. See item 510 in the HISTORY.txt file.

LOTOS NT and TRAIAN have been modified to allow external types to have "with" clauses. For instance, the following type definition:
```
   type T is
      !external !implementedby "T"
      with ==, !=
   end type
```
was formerly rejected with the following error message:
```
   error: unexpected "with" clause for external type T
```
From now on, it is accepted, under the following rules:
- The functions that can be declared in the "with" clause of an external type are those that can be declared in the "with" clause of a general type given by its constructors.
- All functions declared in the "with" clause of an external type are themselves external. They should be implemented in the ".tnt" or ".fnt" file, as TRAIAN will not generate C code for them.
- Such functions should not have an !external pragma attached to them. Otherwise, TRAIAN will emit the following warning:
```
     warning: redundant pragma !external for function ==
```
- But such functions should have an !implementedby pragma attached to them. Otherwise, TRAIAN will emit the following warning:
```
    warning: missing pragma !implemented for function ==
```
The TRAIAN Reference Manual was updated accordingly. See item 511 in the HISTORY.txt file.

LOTOS NT and TRAIAN have been modified to solve the following issue: when a module M containing an external type T has a "with" clause that defines some function F, this function is implicitly defined for type T and is automatically external. It is therefore needed to attach an !implemented pragma for this function to specify the name of the C function that implements F.
From now on, it is permitted to add, in the definition of any type T (external or not), a "with" clause that defines some function F, already listed in the "with" clause of the module, with an !implementedby pragma attached to F. For instance, the following module definition:
```
   module M with == is
      ...
      type T is
         set of Bool
      with
         == !implementedby "EQ_T",
         != !implementedby "NE_T"
      end type
      ...
   end module
```
which formerly triggered a warning:
```
   warning: redundant clause "with ==" for type T (already present for the module)
```
is now accepted without warning if the "with ==" clause comes with pragmas, among which an !implementedby pragma must be present.
Also, if the type T is external and contains no "with" clause for the function "==", e.g.:
```
   module M with == is
      ...
      type T is
         !external !implementedby "T"
      with
         != !implementedby "NE_T"
      end type
      ...
   end module
```
a new warning will be emitted by TRAIAN:
```
   warning: missing clause: with == !implementedby "C:..."
```
See item 512 in the HISTORY.txt file.

Formerly, it was not permitted to attach !external pragmas to list types, because TRAIAN is in charge of implementing list types. For instance, the following type definition is forbidden:
```
   type T is
      !external
      list of int
   end type
```
LOTOS NT and TRAIAN have been modified to forbid as well attaching !external pragmas to arrays, ranges, sets, sorted lists, and predicate types. In such cases, TRAIAN now emits new error messages:
```
   error: unexpected pragma !external for array type T
   error: unexpected pragma !external for range type T
   error: unexpected pragma !external for set type T
   error: unexpected pragma !external for sorted list type T
   error: unexpected pragma !external for where type T
```
See item 514 in the HISTORY.txt file.

Compiler Changes

Several warnings emitted by TRAIAN about lists having a single element have been simplified. For instance, given the following LOTOS NT fragment:
```
   PRINT (?true)
```
TRAIAN no longer displays this warning:
```
   warning: useless "?" symbol before 1st offer (no variable present)
```
but the following, simpler one:
```
   warning: useless "?" symbol before offer (no variable present)
```
See item 482 in the HISTORY.txt file.

TRAIAN was modified to warn about patterns of the form "P where V" when neither P, nor the patterns located on the left-hand side of P if P occurs in a list of patterns, contain variables. For instance, the following pattern:

   0, CONS ('a', NIL), any where X > 0

now triggers the following message:

   warning: unexpected "where" in 3rd pattern (no variable before this condition)

Similarly, the following statement:

   case X in
      0 -> return FALSE
   |  any where X > 10 -> return TRUE
   |  any -> return FALSE
   end case

now triggers the following message:

   warning: unexpected "where" in pattern (no variable before this condition)

and should be rewritten as follows:

   case X in
      0 -> return FALSE
   |  any -> return X > 10
   end case

See item 483 in the HISTORY.txt file.

The way TRAIAN checks the "with" clauses of modules was enhanced. If a module M contains a "with F" clause, then:
- TRAIAN triggers a (fatal) error if no existing scheme has a function named F.
- TRAIAN emits a warning if at least one scheme has a function named F, but none of the schemes having this function F are used in M. In such case, the following warning is issued:
```
   warning: useless clause "with F" in module M
```
See item 490 in the HISTORY.txt file.

TRAIAN was made stricter with respect to the files included by a "library" clause. From now on, these files must have a ".lnt" suffix, which is added if it is not explicitly present in the "library" clause. See item 491 in the HISTORY.txt file.

The handling of scheme files (located in lib/scheme_*.lnt) was further developed tin several ways. From now on:
- The expansion of list types uses the NIL and CONS constructors defined in file "scheme_list.lnt", rather than generating NIL and CONS constructors "hard-coded" in the expansion algorithm.
- TRAIAN expands the generic type parameters LNT_T1 and LNT_T2 present in scheme functions.
- TRAIAN performs data-flow analysis in the bodies of scheme functions.
- TRAIAN performs C code generation for the (non-"null") bodies of scheme functions.
The consequences of these changes are not yet visible to end users (since most scheme functions have a "null" body at the moment) but will become manifest in future releases of TRAIAN. See item 492 in the HISTORY.txt file.

TRAIAN no longer emits warnings when some module M containing only external types has a "with" clause. Formerly, the following module definition:
```
   module M with == is
      type T is
         !external !implementedby "T"
      end type
   end module
```
would generate a message:
```
   warning: useless clause "with ==" in module M
```
This message is no longer emitted because the "with" clause now applies to type T, defining a function ==: T, T -> BOOL. From now on, the warning will only be emitted for modules that do not contain any type definition. See item 513 in the HISTORY.txt file.

Code-Generation Changes

The output of TRAIAN was modified by replacing the two files "FILE_t.h" and "FILE_f.h" generated so far for each LOTOS NT program "FILE.lnt" by a single file "FILE.c". Thus, users should simplify their handwritten C files by replacing:
```
   #include "FILE_t.h"
   #include "FILE_f.h"
```
with:
```
   #include "FILE.c"
```
The "traian_delete" command and the TRAIAN demo examples have been updated accordingly. See item 502 in the HISTORY.txt file.

The structure of the C code generated by TRAIAN was enhanced by moving to the end of the C file the declarations and definitions of the C functions generated for the LOTOS NT functions "<", "<=", ">", ">=", and "!=" declared in "with" clauses. See item 503 in the HISTORY.txt file.

A restriction inherited from TRAIAN 2 was removed: from now on, the functions "hash", "pred", and "succ" declared in the "with" clause of an infinite (i.e., recursive) type are implemented in C. Formerly, no code was generated by TRAIAN for such functions. See item 505 in the HISTORY.txt file.

The C code generated by TRAIAN was modified to use new-style prototypes instead of old-style (i.e., Kernighan and Ritchie) ones. This has two benefits: prototypes will be mandatory in the forthcoming C23 standard, and they allow to detect mistakes in hand-written C code that is combined with the C code generated by TRAIAN. See item 517 in the HISTORY.txt file.

Library Changes

The C code of the two library functions ADT_TO_NAT_STRING() and ADT_TO_INT_STRING() that implement the two predefined LOTOS NT functions NAT: STRING -> NAT and INT: STRING -> INT has been rewritten.
Formerly, these functions relied on the POSIX functions strtoul() and strtol(), which only support C constants, but not all features of LOTOS NT natural and integer constants. Moreover, only the valid prefix of the string was checked, meaning that inputs of the form "10A", were accepted and recognized as 10. Leading and trailing spaces are accepted and eliminated.
The new implementations support binary constants (starting with "0b"), octal constants (starting with "0o"), hexadecimal constants (starting with "0x"), as well as the presence of underscores in number notations. They also forbid useless initial zeros (e.g., "007") and check the entire input string (rather than a prefix). An exception is raised if the input is incorrect.
For instance, the following sequence of actions:
```
   PRINT (NAT (" 1_0  "));
   PRINT (NAT ("10_345"));
   PRINT (NAT ("0b1001_00_1"));
   PRINT (NAT ("0o1701_20_345"));
   PRINT (NAT ("0xAB_CD"))
```
now produces the following output:
```
   "PRINT !10"
   "PRINT !10345"
   "PRINT !73"
   "PRINT !31498469"
   "PRINT !43981"
```
whereas, formerly, it was generating:
```
   "PRINT !1"
   "PRINT !10"
   "PRINT !0"
   "PRINT !0"
   "PRINT !0"
```
See item 499 in the HISTORY.txt file.

The C code of the library function ADT_TO_REAL_STRING() that implements the predefined LOTOS NT function REAL: STRING -> REAL. From now on, this function accepts inputs matching the syntax of LOTOS NT real constants (e.g., with underscores), possibly enclosed between spaces. For instance, the following sequence of actions:
```
   PRINT (REAL ("  1_0.0_0_0_1  "));
   PRINT (REAL ("       -1_0.1"));
   PRINT (REAL ("+1_0E01_1 "))
```
now produces the following output:
```
   "PRINT !10.0001"
   "PRINT !-10.1"
   "PRINT !1e+12"
```
whereas, formerly, it was generating:
```
   "PRINT !1"
   "PRINT !-1"
   "PRINT !1"
```
See item 500 in the HISTORY.txt file.

The include files "incl/lotosnt_hash.h" and "incl/lotosnt_predefined.h" have been updated to replace old-style (i.e., Kernighan & Ritchie) prototypes by new-style ones. See item 506 in the HISTORY.txt file.

The "lotosnt_exceptions" library of TRAIAN was simplified in several ways:
- The include file "lotosnt_exceptions.h" was made cleaner and more abstract by moving into "lotosnt_exceptions.c" all the type definitions that should not be seen and manipulated by the users of the library.
- The type TRAIAN_ADTI_EXCEPTION_CONTEXT was removed, since it was identical to jmp_buf. From now on, the latter is used in place of TRAIAN_ADTI_EXCEPTION_CONTEXT.
- The parameter of function TRAIAN_ADTI_exception_get_data() was deleted, since it was not used.
- The first parameter of function TRAIAN_ADTI_TRAP_ERROR() was deleted, since it was not used.
- The parameter of function TRAIAN_ADTI_exception_endtrap() was removed, since it was useless.
- The "column" parameter of function TRAIAN_ADTI_raise_event() was deleted.
- Function TRAIAN_ADTI_raise_exception() now has one parameter instead of four.
The code generation part of TRAIAN was updated to take these changes into account. See item 507 in the HISTORY.txt file.

A number of renamings have been performed in the "lotosnt_exceptions" library of TRAIAN, in order to ensure that all the identifiers exported by this library start with the "TRAIAN_LIB_" prefix. Precisely, the following renamings have been done:

   _exception_loc -> TRAIAN_LIB_EVENT_STRUCT
   NONE_EXCEPTION_DATA -> TRAIAN_LIB_NO_DATA
   TRAIAN_ADTI_EXCEPTION -> TRAIAN_LIB_EVENT
   TRAIAN_ADTI_do_raise_exception() -> TRAIAN_LIB_EVENT_RAISING()
   TRAIAN_ADTI_exception_endtrap() -> TRAIAN_LIB_TRAP_LEAVE()
   TRAIAN_ADTI_exception_trap() -> TRAIAN_LIB_TRAP_ENTRY()
   TRAIAN_ADTI_free_exception() -> TRAIAN_LIB_EVENT_DELETE()
   TRAIAN_ADTI_init_exceptions() -> TRAIAN_LIB_EVENT_INIT()
   TRAIAN_ADTI_KIND_* -> TRAIAN_LIB_KIND_*
   TRAIAN_ADTI_new_exception() -> TRAIAN_LIB_EVENT_CREATE()
   TRAIAN_ADTI_not_reached() -> TRAIAN_LIB_UNREACHEABLE()
   TRAIAN_ADTI_exception_get_data() -> TRAIAN_LIB_EXCEPTION_DATA()
   TRAIAN_ADTI_raise_event() -> TRAIAN_LIB_EVENT_RAISE()
   TRAIAN_ADTI_raise_exception() -> TRAIAN_LIB_EVENT_TRIGGER()
   TRAIAN_ADTI_TRAP_ERROR -> TRAIAN_LIB_TRAP_DUMP
   TRAIAN_ADTx_RANGE_ERROR -> TRAIAN_LIB_NO_EVENT
   TRAIAN_LIB_TRAP_ENTRY() -> TRAIAN_LIB_TRAP_ENTERING()

The C code generated by TRAIAN was updated accordingly. See item 508 in the HISTORY.txt file.

The include file "lotosnt_exceptions.h" was modified to insert a pragma "does_not_return" that removes "Likely uninitialized read" warnings emitted by the SunC 5.15 compiler. See item 509 in the HISTORY.txt file.

Release Changes

The syntax of the scheme files (located in lib/scheme_*.lnt) was extended to allow the presence of pragmas, essentially "!version" pragmas at the moment. These pragmas now appear in the C code generated by TRAIAN, under the form of "what-strings", e.g.:
```
   "@(#)TRAIAN -- 1.4 -- 2023/02/28 10:57:21 -- scheme_list.lnt"
```
See item 486 in the HISTORY.txt file.

The demo_04 (SIMPROC compiler) was enhanced in several ways:
- The code was simplified to be more readable and aligned with the recent changes of the SYNTAX compiler generator. In particular, the TABC tool was renamed to SEMC.
- The "examples" directory was renamed to "test" and a script "run-test" was added, which performs non-regression checks.
- The makefile was entirely rewritten, so that demo_04, which is also part of the SYNTAX examples, can compile in both the TRAIAN and SYNTAX distributions. To be coherent with SYNTAX, the Makefile of each TRAIAN demo has been renamed to makefile.
- The file =READ_ME.txt was entirely rewritten and renamed (as well as all the other =READ_ME.txt files contained in the TRAIAN distribution) to README.txt, for consistency with the SYNTAX demo examples.
See item 501 in the HISTORY.txt file.

Bug Fixes

A bug was fixed, which caused memory faults when running TRAIAN on certain LOTOS NT programs containing !implementedby "LOTOS:..." pragmas. The number of such pragmas was not always counted properly, possibly entailing out-of-bound table accesses. See item 480 in the HISTORY.txt file.

A bug was fixed, which caused segmentation violations when a LOTOS NT module M contains a global "with" clause that defines some function F, and when M also contains a type T defined using some scheme for which F is not a predefined function. For instance, the bug occurred on the following LOTOS NT example:
```
   module M with subset is
   ...
   type T is
      list of ...
   end type
   ...
   end module
```
because "subset" is not a predefined function defined over lists. From now on, no "subset" function is created for type T. See item 481 in the HISTORY.txt file.

The grammar of TRAIAN was modified to ensure that the recently added operators "<>" have the same precedence as the operators "!=". See item 484 in the HISTORY.txt file.

A bug was fixed in the generation of C identifiers for the recently added LOTOS NT comparison operators "=" and "<>". In a few cases, TRAIAN would generate incorrect C identifiers, e.g., TRAIAN_=_T instead of TRAIAN_EQ_T. See item 485 in the HISTORY.txt file.

An issue (already present in TRAIAN 2) was fixed in the code generation algorithms of TRAIAN 3.9. For certain kinds of LOTOS NT types (e.g., singletons, tuples, etc.), the !implementedby pragmas attached to the comparison functions "==" and "!=" were not properly taken into account in the generated C code. For instance, given the following tuple type definition:
```
   type T is
       !implementedby "T"
       C (X, Y: INT)
   with
      == !implementedby "EQ", 
      != !implementedby "NE"
   end type
```
TRAIAN generated two comparison functions named, respectively, TRAIAN_EQ_T() and TRAIAN_NE_T() instead of EQ() and NE(). See item 487 in the HISTORY.txt file.

A data-flow analysis issue was fixed, which caused TRAIAN to emit irrelevant warnings about useless assignments of arrays. For instance, given the following definitions:

   type T is array [1..2] of NAT end type
   var A: T

the following code fragments triggered improper warnings:

   1)
      A := T (0, 0);   -- here, warning: useless assignment to A
      A [0] := 1;
      use A

   2)
      A := T (0, 0); -- here, warning: useless assignment to A
      A [0] := 1;    -- here, warning: useless assignment to A
      A [1] := 1;
      use A

   3)
      A := T (0, 0); -- here, warning: useless assignment to A
      if X then
         A := T (1, 1) -- here, warning: useless assignment to A
      end if;
      A [0] := 1;
      use A

   4)
      A := T (0); -- here, warning: useless assignment to A
      if X then
         A := T (1, 1) -- here, warning: useless assignment to A
      end if;
      A [0] := 1;
      use A

This issue has been solved by better distinguishing between "total" assignments (to all the elements of an array) and "partial" assignments (to one particular element of an array). See item 488 in the HISTORY.txt file.

An issue was fixed in the static analysis checks performed by TRAIAN on arrays: before assigning an individual element of an array, the entire array should have been initialized. From now on, TRAIAN emits a new error message when this rule is not respected:
```
   error: array X may be (partially) uninitialized
```
See item 489 in the HISTORY.txt file.

The checks done by TRAIAN for the exhaustiveness of LOTOS NT patterns have been enhanced. Formerly, the former implementation did not take into account the presence of non-constructor functions properly, and could fail displaying messages such as:
```
  warning: possibly incomplete patterns in "case" instruction
  some values of type Int might not be matched by the given constants
  (an "any" pattern might be necessary to match the missing cases)
```
This issue is now solved and these warnings are emitted. See item 494 in the HISTORY.txt file.

An error was fixed in the generation of C code for the STRING functions defined in "with" clauses: the !implementedby pragmas attached to such functions were not taken into account. For instance, given the following type definition:
```
   type T is
      A, B, C
   with
      STRING !implementedby "S"
   end type
```
the C function generated for STRING was not named S(), but TRAIAN_STRING_T(). See item 497 in the HISTORY.txt file.

Another bug was fixed: the !implementedby pragmas attached to the comparison functions "<", "<=", ">", and ">=" defined in "with" clauses of types were not taken into account. For instance, given the following type definition:
```
   type T is
      nil, cons (h: Bool, t: T)
   with
      >= !implementedby "GE"
   end type
```
the C function generated for >= was named TRAIAN_GE_T() instead of GE(). See item 498 in the HISTORY.txt file.

A bug was fixed, which occurred for LOTOS NT files containing more that 2^24 lines. For such files, error messages would contain incorrect line numbers, e.g.:
```
  FILE.lnt:0: error: type T is not defined
```
or:
```
  FILE.lnt:38866: error: type T is not defined
```
After fixing the bug, the error message becomes:
```
  FILE.lnt:16777217: error: type T is not defined
```
See item 504 in the HISTORY.txt file.

The grammar of TRAIAN was simplified by removing two syntactic predicates that were useless and, on two incorrect LOTOS NT examples, caused a memory error (followed by a core dump on Solaris and macOS). See item 515 in the HISTORY.txt file.

The syntactic grammar of TRAIAN was too permissive and accepted non-alphabetic identifiers (i.e. function identifiers such as "&", "***", etc.) on the left-hand side of arrows of event parameter lists and value parameter lists in patterns, function calls, and process calls. For instance, the following function definition was accepted:
```
   function F (X : BOOL) is
      return G (*** -> 0)
   end function
```
The grammar was made stricter and the above example is now rejected. See item 516 in the HISTORY.txt file.

Future Work

For many years, TRAIAN has been used to develop compilers, including those of the CADP toolbox. At present, it is also intensively used to check LNT specifications of concurrent systems, allowing to catch mistakes not detected by the "lightweight" approach of the LNT2LOTOS translator.

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

Download

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

http://vasy.inria.fr/traian