By default, the semantic analysis is restricted to scalar integer variables as they are key variables to understand scientific code behavior. However it is possible to analyze scalar variables with other data types. Fortran LOGICAL variables are represented as 0/1 integers. Character string constants and floating point constants are represented as undefined values.
The analysis is thus limited to constant propagation for character strings and floating point values whereas integer and boolean variables are processed with a relational analysis.
Character string constants of fixed maximal length could be translated into integers but the benefit is not yet assessed because they are not much used in the benchmark and commercial applications we have studied. The risk is to increase significantly the number of overflows encountered during the analysis.
SEMANTICS_ANALYZE_SCALAR_INTEGER_VARIABLES TRUE
SEMANTICS_ANALYZE_SCALAR_BOOLEAN_VARIABLES FALSE
SEMANTICS_ANALYZE_SCALAR_STRING_VARIABLES FALSE
SEMANTICS_ANALYZE_SCALAR_FLOAT_VARIABLES FALSE
SEMANTICS_ANALYZE_SCALAR_COMPLEX_VARIABLES FALSE
For every module, array declaration are assumed to be correct with respect to the standard: the upper bound must be greater than or equal to the lower bound. When implicit, the lower bound is one. The star upper bound is neglected.
This property is turned off by default because it might slow down PIPS quite a lot without adding any useful information because loop bounds are usually different from array bounds.
SEMANTICS_TRUST_ARRAY_DECLARATIONS FALSE
For every module, array references are assumed to be correct with respect to the declarations: the subscript expressions must have values lower than or equal to the upper bound and greater than or equal to the lower bound.
This property is turned off by default because it might slow down PIPS quite a lot without adding any useful information.
SEMANTICS_TRUST_ARRAY_REFERENCES FALSE
Perform ``meet'' operations for semantics analysis. This property is managed by pipsmake/ which often sets it to TRUE. See comments in pipsmake/ documentation to turn off convex hull operations for a module or more if they last too long.
SEMANTICS_FLOW_SENSITIVE FALSE
Complex control flow graph may require excessive computation resources. This may happen when analyzing a parser for instance.
SEMANTICS_ANALYZE_UNSTRUCTURED TRUE
To reduce execution time, this property is complemented with a heuristics to turn off the analysis of very complex unstructured.
If the control flow graph counts more than SEMANTICS_MAX_CFG_SIZE1
vertices, use effects only.
SEMANTICS_MAX_CFG_SIZE2 20
If the control flow graph counts more than SEMANTICS_MAX_CFG_SIZE1
but less than SEMANTICS_MAX_CFG_SIZE2
vertices, perform the convex hull of its elementary transformers and take
the fixpoint of it. Note that SEMANTICS_MAX_CFG_SIZE2 is assumed to
be greater than or equal to SEMANTICS_MAX_CFG_SIZE1.
SEMANTICS_MAX_CFG_SIZE1 20
Without preconditions, transformers can be precise only for affine expressions. Approximate transformers can sometimes be derived for other expressions, involving for instance products of variables or divisions.
However, a precondition of an expression can be used to refine the approximation. For instance, some non-linear expressions can become affine because some of the variables have constant values, and some non-linear expressions can be better approximated because the variables signs or ranges are known.
To be backward compatible and to be conservative for PIPS execution time, the default value is false.
Not implemented yet.
SEMANTICS_RECOMPUTE_EXPRESSION_TRANSFORMERS FALSE
Intraprocedural preconditions can be computed at the same time as transformers and used to improve the accuracy of expression and statement transformers. Non-linear expressions can sometimes have linear approximations over the subset of all possible stores defined by a precondition. In the same way, the number of convex hulls can be reduced if a test branch is never used or if a loop is always entered.
SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT FALSE
The default value is false for reverse compatibility and for speed.
To be refined later; basically, use callees transformers instead of callees effects when computing transformers bottom-up in the call graph; when going top-down with preconditions, should we care about unique call site and/or perform meet operation on call site preconditions ?
SEMANTICS_INTERPROCEDURAL FALSE
This property is used internally and is not user selectable.
CPU time and memory space are cheap enough to compute loop fix points for transformers. This property implies SEMANTICS_FLOW_SENSITIVE and is not user-selectable. Its default value is false.
SEMANTICS_FIX_POINT FALSE
The default fix point operator, called transfer, is good for induction variables but it is not good for all kinds of code. The default fix point operator is based on the transition function associated to a loop body. A computation of eigenvectors for eigenvalue 1 is used to detect loop invariants. This fails when no transition function but only a transition relation is available. Only equations can be found.
The second fix point operator, called pattern, is based on a pattern matching of elementary equations and inequalities of the loop body transformer. Obvious invariants are detected. This fix point operator is not better than the previous one for induction variables but it can detect invariant equations and inequalities.
A third fix point operator, called derivative, is based on finite differences. It was developed to handled DO loops desugared into WHILE loops as well as standard DO loops. The loop body transformer on variable values is projected onto their finite differences. Invariants, both equations and inequalities, are deduced directly from the constraints on the differences and after integration. This third fix point operator should be able to find at least as many invariants as the two previous one, but at least some inequalities are missed because of the technique used. For instance, constraints on a flip-flop variable can be missed. Unlike Cousot-Halbwachs fix point (see below), it does not use Chernikova steps and it should not slow down analyses.
This property is user selectable and its default value is transfer. The default value is the only one which has been seriously validated.
SEMANTICS_FIX_POINT_OPERATOR "transfer"
The property SEMANTICS_PATTERN_MATCHING_FIX_POINT has been removed
and replaced by option pattern of the previous property.
This property was defined to select one of Cousot-Halbwachs's heuristics and to compute fix points with inequalities and equalities for loops. These heuristics could be used to compute fix points for transformers and/or preconditions. This option implies SEMANTICS_FIX_POINT and SEMANTICS_FLOW_SENSITIVE. It has not been implemented yet in PIPS2 because its accuracy has not yet been required, but is now badly named because there is no direct link between inequality and Halbwachs. Its default value is false and it is not user selectable.
SEMANTICS_INEQUALITY_INVARIANT FALSE
Because of convexity, some fix points may be improved by using some of the information carried by the preconditions. Hence, it may be profitable to recompute loop fix point transformer when preconditions are being computed.
The default value is false because this option slows down PIPS and does not seem to add much useful information in general.
SEMANTICS_RECOMPUTE_FIX_POINTS_WITH_PRECONDITIONS FALSE
Preconditions reflect by default all knowledge gathered about the current state (i.e. store). However, it is possible to restrict the information to variables actually read or written, directly or indirectly, by the statement following the precondition.
SEMANTICS_FILTERED_PRECONDITIONS FALSE
Output semantics results on stdout
SEMANTICS_STDOUT FALSE
Debug level for semantics used to be controlled by a property. A Shell
variable, SEMANTICS_DEBUG_LEVEL, is used instead.