|
|
||
|
The FMT relies functionally on several predefined values and decisions. The particular choices, even though intended to reasonably represent the typical usage, are arbitrary and as such might not fit the needs of all users. An example of such predefined value is the range of standard integer type, which is 32-bit, signed. Some of such values can be changed by means of configuration options - the following sections describe all of them.
User-configurable options and their default values are defined in the “FMTOptions`” package. If these values need to be overridden and the new settings have permanent nature, it is reasonable to modify the defaults right in the FMTOptions.wl file - otherwise, in case of temporary settings, the new value can be set by one of the dedicated functions: setOption or setOptions.
The setOption function allows to override just a single setting in the context of some given model and the new setting is remembered and used by further operations performed on that model, for example:
The above invocation establishes new (narrower, 16-bit) range for the standard integer type within the sys model. This setting has no impact on other existing models or on models that will be created in the future (new models always pick default option values).
Another possibility is to set the whole set of options, which is defined by an association object. That object can be built from scratch, or by modifying the copy of the default set:
The setOptions function replaces all options at once, which might overwrite some options that were modified already - to prevent this when only a single modification is intended, another pattern can be used, picking the current set of options instead of the default one:
The choice of particular option setting method is mostly a matter of personal taste.
Code generators have their own set of policies, which can be set as optional parameters in the invocation of code-generation functions. They will be described in the following subsections as well.
This option is identified by symbol showInteractiveButtons from “FMTOptions`” and its default value is True, meaning that after defining new operations (or replacing existing definitions), the grammar, names and flow checks are automatically performed and if any errors are found, the user is presented with buttons that allow to further inspect the problem.
The default behaviour can be seen in these examples:
Above, operation op1 is correct and the message in green confirms that, while operation op2 is not correct and the red message is displayed, together with a button that allows the user to perform some further inspections.
This behaviour is reasonable in interactive sessions with Mathematica notebooks as it gives instant feedback and speeds up typical user actions. But it would be wasteful with long series of definitions that are automatically added to the model, perhaps within a continuous integration setup or from console scripts. The showInteractiveButtons option, when set to False, allows to speed up such automated definitions by preventing automatic correctness checks from being performed:
Of course, all checks can be still performed on demand, via dedicated FMT functions.
The choice of range for the standard integer type was already shown above. The default value, which is a two-element list with lower and upper bound, was chosen for 32-bit, signed representation. Typical overriding choices can be (for 16-bit and 64-bit, respectively):
These values are used in automatically generated proof statements to ensure that newly computed or assigned integer values are within the requested range. It is important to note, however, that this option has no impact on the mapping for standard integer type in the final generated code - generator policy settings can and should be used to influence this mapping instead, as described in further sections.
The integer rounding function, which is governed by the integerRoundingFunction option with default value IntegerPart, is used by the proof engine to implement the rounding of results of integer division. For example, in the following sequence of operations:
the expected result for object y is 2, as the fractional part is dropped in integer operations. The IntegerPart is a standard Wolfram function that implements this rounding, but can be changed to some other operation if needed.
The first array index value is a subject of flame wars between programmers using different programming languages - for example, arrays in C start at 0, while in Ada they can start at arbitrary index value, with 1 being a popular choice. FMT does not force any arbitrary choice and since it supports both C and Ada as target languages, it allows the users to pick the starting index that will lead to the most readable and convenient generated code. The array starting index, keyed by arrayIndexOffset, has default value of 0 and can be changed to one with the following:
This setting is used by both code as well as proof statement generators. In particular, since the starting index value in C is always 0, appropriate offsets are automatically added in generated C code.
And example definitions that demonstrate this setting are:
With default setting for the starting index value (0), the accessArray operation modifies the second element in array.
The array type definition in Ada is (10 elements, from 0 to 9):
type My_Array_Type is array (0 .. 9) of Integer;
and the access operation is translated as:
A(1) := 42;
Similarly, the C++ array type definition is:
typedef std::int32_t my_array_type[10];
and the access operation is translated as:
a[1] = 42;
Changing the option value to 1 will mean that the first element is accessed instead and this is reflected in both languages.
Ada type definition (still 10 elements, but now from 1 to 10):
type My_Array_Type is array (1 .. 10) of Integer;
and Ada access (without change):
A(1) := 42;
C++ type definition (no change, as the initial index is not part of the type definition anyway):
typedef std::int32_t my_array_type[10];
and finally, C++ element access, properly translated to point at the first array element:
a[1 - 1] = 42;
This mechanism is intended to work properly with arbitrary values for the initial index, but it is expected that the most commonly used values will be 0 and 1. In any case, the generated code is always functionally consistent with generated proof statements and between target programming languages.
The array index offset setting has the model scope - that is, it applies to all arrays defined within the given model. This means that it is not possible to have different initial index values for different arrays.
The grammar preprocessor option, keyed by the grammarPreprocessor symbol from “FMTOptions`”, allows to install user-provided preprocessor hooks.
Grammar preprocessors are functions that take the complete operation body as input and return a possibly transformed body. One possible use of preprocessors is to extend the core modeling grammar with new syntax and control structures.
User-defined preprocessor can be installed with:
The default preprocessor, implemented in “FMTOptions`”, extends the core modeling language with support for the For loops.
Grammar preprocessors are explained in a dedicated chapter of this documentation.
Formula formatter, keyed by the formulaFormatter symbol, is a function that is used to format statements and expressions in reports. By default the StandardForm function is used.
The following example demonstrates the impact of this setting:
In the report above the expressions in the second and third column are formatted according to the default choice for formula formatter option.
More mathematically-oriented users might prefer the following setting instead:
With this setting, the expressions are formatted in a way that is less programming-centered:
Any other formatter can be installed this way, although the two presented above are probably the most straightforward and readily accessible.
Indent size is a configuration option that belongs to the family of code generation policies. They are not set in the same way as other options described earlier and they are not persistent within the model - instead, they can be provided when the code generation is requested and their impact is always temporary.
The indent size can be demonstrated with the following simple operation:
When the code is generated without any explicit settings, the indent size is 4 spaces by default in C and C++:
#include "my_package.h"
#include <cstdint>
using namespace my_package;
// Operation definitions.
void my_package::op()
{
std::int32_t temp;
temp = 42;
}
In Ada, however, the default indent size is 3 spaces:
package body My_Package is
-- Operation definitions.
procedure Op is
Temp : Integer;
begin
Temp := 42;
end Op;
end My_Package;
These values can be changed by providing the optional translationPolicies parameter, which is supposed to be an Association object with overriding configuration values, for example:
#include "my_package.h"
#include <stdint.h>
/* Operation definitions. */
void my_package_op(void)
{
int32_t temp;
temp = 42;
}
The same option can be used in Ada, too:
package body My_Package is
-- Operation definitions.
procedure Op is
Temp : Integer;
begin
Temp := 42;
end Op;
end My_Package;
Maximum line length is another option that is common to all target programming languages. The following example can demonstrate its effects:
This type definition is short enough to fit in the default line length of 80 characters:
#ifndef FILE_MY_PACKAGE_H_INCLUDED
#define FILE_MY_PACKAGE_H_INCLUDED
namespace my_package
{
// This package does not need body.
// Type definitions.
enum my_enum {black, red, green, blue, grey, white, transparent};
} // namespace my_package
#endif // FILE_MY_PACKAGE_H_INCLUDED
When the max line length is set to some lower value, however, the lines will be broken to fit the limited length:
#ifndef FILE_MY_PACKAGE_H_INCLUDED
#define FILE_MY_PACKAGE_H_INCLUDED
namespace my_package
{
// This package does not need body.
// Type definitions.
enum my_enum {black, red, green,
blue, grey, white, transparent};
} // namespace my_package
#endif // FILE_MY_PACKAGE_H_INCLUDED
The maxLineLength value is a soft limit, so there is no guarantee that the generated code will never exceed it - it is only used to influence decisions on line breaks and some constructs are “rigid” enough to overrun it. For example, when the value is really small, only some of the lines from the code above will be affected, others will retain their original lengths:
#ifndef FILE_MY_PACKAGE_H_INCLUDED
#define FILE_MY_PACKAGE_H_INCLUDED
namespace my_package
{
// This package does not need body.
// Type definitions.
enum my_enum
{black,
red, green,
blue,
grey,
white,
transparent};
} // namespace my_package
#endif // FILE_MY_PACKAGE_H_INCLUDED
This code generation policy is a function that takes a package name as its only argument and returns a list of two strings - the name of specification file and the name of implementation file for the given package.
The default implementation for Ada follows the standard GNAT convention and both C and C++ use that convention as well, with appropriate file name extensions (“.ads”, ”.adb”, ”.h” and ”.c” or ”.cpp”). The following are representative examples of default package name to file name translations:
The file name translation policy can be changed to some user-defined function, although handling all the details requires significant amount of logic and string processing. A simple example with an anonymous function that just forces file names to some hard-coded values is:
The name from symbol code translation policy, keyed by nameFromSymbol name, allows to define custom schemes for translating all entity names. Default implementations detect the camel-case convention and translate case changes into underscores and follows standard name casing, so for example myVariable in the model is translated into “My_Variable” in Ada and “my_variable” in C and C++.
Users can install their own symbol translators, but similarly to file name translation, proper implementations can be quite involving and are different for each target language. In C, the translator expects a single argument, which is a fully-qualified symbol name. In Ada and C++, there are two parameters: fully-qualified symbol name and the name of the currently processed package (this is used to generate shorter, non-qualified names if they are from the same package). Existing code from respective generator packages can be used for inspiration when implementing custom translators.
As a special case FMT accepts also a regular Association object as a user policy, which can provide mappings for selected symbols - those symbols that are found in such a lookup table are translated according to provided mapping and all other symbols are translated using the default routine. For example:
This association object contains mappings for selected symbols only and can be used in any target language:
#ifndef FILE_MY_PACKAGE_H_INCLUDED
#define FILE_MY_PACKAGE_H_INCLUDED
namespace my_package
{
// This package does not need body.
// Type definitions.
enum my_enum {BLACK, red, green, blue, grey, WHITE, transparent};
} // namespace my_package
#endif // FILE_MY_PACKAGE_H_INCLUDED
package My_Package is -- This package does not need body. pragma Pure (My_Package); -- Type definitions. type My_Enum is (BLACK, Red, Green, Blue, Grey, WHITE, Transparent); end My_Package;
Above, only two selected symbols were translated with explicitly specified mappings, all others followed the default translation scheme. This approach can be used for all symbols, including type, variable and operation names. In actual projects such mappings can be read from configuration files or external databases.
The integer target type is a policy that is relevant for C and C++ only. Its value is a string, by default “int32_t” for C and “std::int32_t” for C++. This policy specifies the name of the target type for the standard integer type.
This translation policy will be of interest to those users who also want to change the range of standard integer type. The range influences the correctness checks, but has no impact on code translation.
In order to use 16-bit integers and after the range was properly defined, the translation can be configured as:
#include "my_package.h"
#include <stdint.h>
/* Operation definitions. */
void my_package_op(void)
{
int16_t temp;
temp = 42;
}
The policy setting forced the use of “int16_t” for the standard integer type. This setting will be usually combined with appropriate range settings, as described in earlier sections.
This policy is relevant for C and C++ only. The policy has name arrayCopyOperation and is a function that generates code for copying array objects. By default array copying is performed with the use of standard memmove function and the policy allows to implement this operation by other means.
The implementations in respective generator packages can be used as a starting point for implementing customized translations.
Source files are by default generated without any header comments. These can be added with the fileHeaderComment translation policy, which should be a function that takes three parameters: package name, translated package name and file name, and returns the complete string for the header comment.
An example policy that uses all three values to parameterize the comment can be:
This simple function can be installed when the code is generated:
//
// File my_package.cpp
// generated for package my_package,
// from model package MyPackage`.
//
#include "my_package.h"
#include <cstdint>
using namespace my_package;
// Operation definitions.
void my_package::op()
{
std::int32_t temp;
temp = 42;
}
The header comment was injected at the beginning of the translated file and proper values were used in the template. The function uses lineBreakT and verticalSpaceT tokens, which are recognized by the internal formatter and ensure that the following code is correctly joined with a single vertical space separating the comment from the rest.
Previous: Code generation, next: Generating MISRA-compliant code
See also Table of Contents.