PIPS
|
#include <stdio.h>
#include <string.h>
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "workspace-util.h"
#include "effects-util.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "misc.h"
#include "properties.h"
#include "vecteur.h"
#include "contrainte.h"
#include "transformer.h"
#include "semantics.h"
Go to the source code of this file.
Macros | |
#define | IS_LOWER_BOUND 0 |
#define | IS_UPPER_BOUND 1 |
|
static |
NOT USED.
NOT FULLY IMPLEMENTED YET. SHOULD BE REDUNDANT WITH whileloop_to_tramsformer() Recompute a fixpoint conditionnally to a valid precondition for all iterations Could/Should be later called from whileloop_to_postcondition()
Definition at line 2403 of file loop.c.
References pips_assert, and transformer_undefined.
|
static |
FI: could be moved somewhere else, e.g.
in transformer library. lower_or_upper: 0 for lower, 1 for upper, i.e. upper_p
check that v is not affected by tfb: N = 10 DO I = 1, N N = 1 {1<=I<=N} !wrong! T(I) = 0. ENDDO and make sure that aliasings (I,J) and (I,X) are correctly handled
Achtung: value_mappings_compatible_vector_p() has a side effect on its argument; it has to be evaluated before the second half of the test else effects would be wrongly interpreted in case of equivalences
Definition at line 580 of file loop.c.
References entity_to_new_value(), IS_LOWER_BOUND, transformer_affect_linear_p(), transformer_inequality_add(), value_mappings_compatible_vector_p(), VALUE_MONE, VALUE_ONE, vect_add_elem(), vect_chg_sgn(), vect_dup(), vect_rm(), and VECTEUR_UNDEFINED.
Referenced by add_index_bound_conditions().
|
static |
loop bounds can be kept as preconditions for the loop body if the loop increment is numerically known and if they are linear and if they are loop body invariant, i.e. indices are accepted
arg. tf is unused, it was replaced by tfb to correct a bug
Only OK if transformers already have been computed
transformer tfb = load_statement_transformer(b);
New version to deal with complex do loop bounds?
Old version
Definition at line 790 of file loop.c.
References add_index_range_conditions(), effects_to_transformer(), free_transformer(), load_cumulated_rw_effects_list(), loop_body, loop_bound_evaluation_to_transformer(), loop_index, loop_range, pips_debug, and transformer_apply().
Referenced by loop_to_postcondition(), loop_to_total_precondition(), and loop_to_transformer().
|
static |
Side effect on pre.
lower_or_upper: 0 for lower, 1 for upper, i.e. upper_p
It is assumed on entry that index has values recognized by the semantics analysis
pips_assert("add_index_bound_conditions", entity_has_values_p(index));
Old implementation, careful about the impact of the loop body but not about side effets in bound
tfb does not take into account the index incrementation
Why not use loop_bound_evaluation_to_transformer()?
An inequation between index and bv should be added
FI: Fixt the result of the intersection in case of side effects in loop range
Make sure the loop body does not modify the loop bounds
FI: we need a side effect on pre...
Likely memory leak here: arguments_union may allocate a new list
This might or not make sense, depending on the caller transformer_arguments(pre) = arguments_difference(arguments_union(transformer_arguments(pre), transformer_arguments(npre)), transformer_arguments(tfb));
When dealing with the loop body precondition, there is no reasons to remove the arguments of tfb, as tfb is part of the definition of pre
Definition at line 624 of file loop.c.
References add_affine_bound_conditions(), arguments_add_entity(), arguments_union(), entity_type, free_predicate(), free_transformer(), make_local_temporary_value_entity(), NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, predicate_undefined, reset_temporary_value_counter(), safe_any_expression_to_transformer(), safe_transformer_projection(), transformer_add_inequality(), transformer_arguments, transformer_consistent_p(), transformer_dup(), transformer_range(), transformer_range_intersection(), transformer_relation, transformer_temporary_value_projection(), transformer_undefined, and ultimate_type().
Referenced by add_index_range_conditions().
transformer add_index_range_conditions | ( | transformer | pre, |
entity | i, | ||
range | r, | ||
transformer | tfb | ||
) |
if tfb is not undefined, then it is a loop; loop bounds can be kept as preconditions for the loop body if the loop increment is numerically known and if they are linear and if they are loop body invariant, i.e. indices are accepted
is the loop increment numerically known? Is its sign known?
incr == 0 is used below as a give-up condition
When lost, try to exploit type information thanks to unsigned variables
find the real upper and lower bounds
try to add the lower bound
try to add the upper bound
pre | re |
tfb | fb |
Definition at line 711 of file loop.c.
References add_index_bound_conditions(), entity_has_values_p(), expression_and_precondition_to_integer_interval(), free_transformer(), IS_LOWER_BOUND, IS_UPPER_BOUND, negative_expression_p(), pips_debug, pips_user_error, positive_expression_p(), range_increment, range_lower, range_upper, simple_dead_loop_p(), and transformer_empty().
Referenced by add_good_loop_conditions(), comp_regions_of_implied_do(), and loop_to_transformer().
transformer add_loop_index_exit_value | ( | transformer | post, |
loop | l, | ||
transformer | pre | ||
) |
The exit value is known if.
Affine increments can be handled when their signs only are known.
For instance, for increment==k: i >= ub i-k <= ub-1
Note the simplification when k==1.
But, first of all, the value of the loop index in post must be incremented. This changes its relationship with induction variables.
Most tests here are redundant because this function is only called if it has been proved that the loop was executed which implies that the upper and lower bounds are affine, that the increment is affine and that the increment sign is known.
Always returns a newly allocated value precondition on loop entrance
This part should be useless because post really is a loop postcondition. There should be no need for an index incrementation or anything. It is used to recover some of the fix-point failures:-(
In fact, it may be useful. The loop transformer and its invariant are computed without knowledge about the number of iteration, which may be zero. By adding one execution of the loop body and the index incrementation, we change b* into b+ which should add effective information.
Do not apply an extra iteration!
post = transformer_apply(t_body, post);
v_i - v_incr == v_ub, regardless of the sign
v_i - v_incr <= v_ub < v_i or: v_i - v_incr - v_ub <= 0, v_ub - v_i + 1 <= 0
v_i - v_incr >= v_ub > v_i
or:
should never happen!
post | ost |
l | postcondition of the last iteration |
pre | loop to process |
Definition at line 878 of file loop.c.
References ABS, affine_increment_to_transformer(), args_to_transformer(), CONS, ENTITY, entity_has_values_p(), entity_local_name(), entity_to_new_value(), expression_and_precondition_to_integer_interval(), ifdebug, load_statement_transformer(), loop_body, loop_index, loop_range, NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, pips_debug, print_transformer, range_increment, range_upper, TCST, transformer_affect_linear_p(), transformer_apply(), transformer_dup(), transformer_equality_add(), transformer_free(), transformer_inequality_add(), transformer_undefined, value_mappings_compatible_vector_p(), value_to_variable(), vect_add_elem(), vect_cl(), vect_new(), vect_substract(), and VECTEUR_UNDEFINED.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
|
static |
Always returns newly allocated memory.
Definition at line 825 of file loop.c.
References any_scalar_assign_to_transformer(), effects_to_transformer(), expression_to_proper_constant_path_effects(), free_transformer(), init, loop_index, loop_range, range_lower, transformer_apply(), transformer_free(), transformer_range(), and transformer_undefined.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), and loop_to_postcondition().
transformer add_loop_skip_condition | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
tf and pre are a unique data structure when preconditions are computed
It is assumed that loop l is not entered
EXPRESSION_TO_TRANSFORMER() should be used
is the loop increment numerically known? Is its sign known?
incr == 0 is used below as a give-up condition
find the real upper and lower bounds
exchange bounds
ub < lb, i.e. ub + lb + 1 <= 0
tf | f |
pre | re |
Definition at line 495 of file loop.c.
References debug(), expression_and_precondition_to_integer_interval(), external_value_name(), ifdebug, loop_range, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_debug, print_transformer, range_increment, range_lower, range_upper, TCST, transformer_inequality_add(), user_error, value_mappings_compatible_vector_p(), vect_add_elem(), vect_fprint(), and vect_substract().
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
transformer any_loop_to_k_transformer | ( | transformer | t_init, |
transformer | t_enter, | ||
transformer | t_next, | ||
statement | body, | ||
list __attribute__((unused)) | lel, | ||
transformer | post_init, | ||
int | k | ||
) |
Processing of loops for transformers, preconditions and transformer lists.
semantic analysis: processing of loops include "constants.h" include "control.h" General handling of structured loops: while, repeat, for, do.
Because the functions for "do" loops pre-existed this framework, they have not (yet) been reimplemented with it. Their implementations are likely to be more CPU efficient because only useful objects are computed whereas the general case requires the computation and use of neutral and absorbent elements such as tranformer_identity() and transformer_empty(). The functions for "while" loops have been rewritten to check the genericity.
Slightly different equations are used for the repeat loop, which executes once or at least twice instead of zero or at least once. These equations are given in the corresponding module, complete_repeatloop_transformer() and repeatloop_to_postcondition().
The transformer associated to any kind of loop, but the repeat_loop, is defined by equation:
t_loop = t_init ; t_skip + t_init ; t_enter ; (t_body ; t_next)* ; t_body ; t_inc; t_exit
where ";" is the combine operator and "+" the union. Note already that t_init is not factored out because the union usually loses information and its use must be postponed as much as possible.
Transformers t_init, t_skip, t_inc, t_next and t_exit are dependent on the kind of loops. For instance, t_skip is transformer_empty for a repeat loop and t_next may include the incrementation (t_inc) and the looping condition (for loop) or just the looping condition (while loop). When no incrementation occurs, t_inc is t_identity and
t_next = t_continue. Elsewhere:
t_next = t_inc ; t_continue
Because transformers are used to compute preconditions, we need to preserve:
t_body_star = t_init ; t_enter ;(t_body ; t_next)*
to compute the body preconditions as t_body_star(pre). But it might be better to use equation
.t_init ; t_enter(pre) + (t_init ; t_enter ;(t_body ; t_next)* ; t_body ; t_next)(pre)
to reduce the approximation in the * operator (see below).
Since we store only one transformer per statement (no such thing as proper and cumulated effects), we store t_body_star instead of t_loop. Note that the range of t_body_star can be restricted by the union of the ranges of t_enter and t_continue (or t_next) which are the last transitions to occur in t_body_star.
But to obtain a correct transformer for the bottom-up composition of transformers, we fix the resulting transformer in statement_to_transformer with the equation:
t_loop = t_init ; t_skip + t_body_star ; t_body ; t_inc; t_exit
When computing the loop postcondition, we do not use t_loop either because we want to postpone the use of "+":
post = (t_init ; t_skip)(pre) + (t_body_star ; t_body ; t_inc ; t_exit) (pre)
When computing the body precondition, we use the following equation
p_body = (t_init ; t_enter)(pre) + (t_body_star ; t_body ; t_next) (pre)
in order to avoid t_body_star imprecision due to a union with t_identity and to delay it in the precondition domain whose dimension is half of the transformer domain dimension.
Note also that the different transformers are computed relatively to a current precondition. So t_init, t_skip etc... may have different values at differente stages. This happens more when transformers are computed in context (setproprety SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT true) and even more when they are recomputed (apply REFINE_TRANSFORMERS). For this reason, a first crude precondition is computed with effects information to be used to compute the body transformer. And since t_enter cannot be computed without its precondition, the later is passed as post_init instead of the loop precondition pre:
post_init = t_init(pre)
A new transformer is allocated. None of the arguments are modified.
The source code has been restructured with a lot of the processing moved into any_transformer_to_k_closure Would be nicer with a proper graph. The transformer associated to a loop in a PIPS print out is the transformer leading from the loop precondition to the loop invariant, t_????. But the transformer recursively returned is t_loop, leading from the loop precondition to the loop postcondition. Designed in West Palm Beach, Dec. 2009. Notations may have sliglhty changed during the coding.
x loop precondition----------------------------------— | t_init | t_????? | t_loop v | |
x post_init | |
---|---|
-----------------------— |
| | t_enter | | | t_skip v | | | x post_enter | | | | identity | | | v | | | -> x <---------—loop invariant | | tf_body_star/__/| t_body | | | v | | | x | | | | t_inc | | | v | | | x | ! | | | | | ---------------— | | | | t_exit | t_continue | | v v v | | ------— x-----------— | | | v | x loop postcondition <-------------------------------—
The same scheme is used for all kinds of loops. Of course, t_inc, t_exit, t_skip and t_continue have to be adapted to the loop kind. k is the periodicity sought. The normal standard default value is
This is obsolete and k should always be equal to 1. When a different value of k is required, call directly any_transformer_to_k_closure().
Compute a first rough body precondition, pre_body, using different heuristics:
Add the loop body execution condition
Compute the body transformer
Any transformer or other data structure to free?
Definition at line 203 of file loop.c.
References any_transformer_to_k_closure(), copy_transformer(), effects_to_transformer(), fprintf(), free_transformer(), ifdebug, load_statement_transformer(), print_transformer, statement_to_transformer(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_range(), and transformer_undefined.
Referenced by any_loop_to_transformer(), and new_whileloop_to_k_transformer().
transformer any_loop_to_postcondition | ( | statement | body, |
transformer | t_init, | ||
transformer | t_enter, | ||
transformer | t_skip, | ||
transformer | t_body_star, | ||
transformer | t_body, | ||
transformer | t_next, | ||
transformer | t_inc, | ||
transformer | t_exit, | ||
transformer | pre | ||
) |
The precondition to propagate in the body is:
p_body = (t_init ; t_enter)(pre) + (t_body_star ; t_body ; t_next) (pre)
The loop postcondition to return is:
post = (t_init ; t_skip)(pre) + (t_body_star ; t_body ; t_inc ; t_exit) (pre)
To restrict the state at the beginning of the last iteration: should be part of t_body_star
Decompose the computation of p_body
Decompose the computation of post
a_post should be used because it is more accurate than direct recomputation, but we chose for the time being to recompute post entirely
Get rid of now useless transformers
body | ody |
t_init | _init |
t_enter | _enter |
t_skip | _skip |
t_body_star | _body_star |
t_body | _body |
t_next | _next |
t_inc | _inc |
t_exit | _exit |
pre | re |
Definition at line 2634 of file loop.c.
References free_transformer(), statement_to_postcondition(), transformer_apply(), transformer_convex_hull(), and transformer_undefined.
Referenced by forloop_to_postcondition(), and repeatloop_to_postcondition().
transformer any_loop_to_transformer | ( | transformer | t_init, |
transformer | t_enter, | ||
transformer | t_next, | ||
statement | body, | ||
list __attribute__((unused)) | lel, | ||
transformer | post_init | ||
) |
Definition at line 316 of file loop.c.
References any_loop_to_k_transformer().
Referenced by forloop_to_transformer(), new_loop_to_transformer(), new_whileloop_to_transformer(), and repeatloop_to_transformer().
transformer complete_any_loop_transformer | ( | transformer | t_init, |
transformer __attribute__((unused)) | t_enter, | ||
transformer | t_skip, | ||
transformer | t_body_star, | ||
transformer | t_body, | ||
transformer __attribute__((unused)) | t_continue, | ||
transformer | t_inc, | ||
transformer | t_exit | ||
) |
Reduce the transformer list associated to a loop to a unique transformer using a convex hull.
An empty list is converted into an empty transformer. The input list is freed.
Definition at line 1662 of file loop.c.
References complete_any_loop_transformer_list(), gen_free_list(), transformer_list_to_transformer(), and transformer_undefined.
Referenced by complete_forloop_transformer(), and complete_forloop_transformer_list().
list complete_any_loop_transformer_list | ( | transformer | t_init, |
transformer | t_skip, | ||
transformer | t_body_star, | ||
transformer | t_body, | ||
transformer | t_inc, | ||
transformer | t_exit | ||
) |
FI: used to be complete_any_loop_transformer() with a direct reduction by convex hull.
t_loop = t_init ; t_skip + t_bodystar ; t_body ; t_inc; t_exit
Before entering t_body, t_enter or t_next have been applied which let us restrict the set of state modified by t_body. But this information should already been included in t_body_star.
Several cases must be tested:
These cases are checked with complete01.c, complete02.c,... complete05.c
loop skipped transformer
add loop entered transformer/condition: should already be in t_body_star
combine both cases in a transformer list
t_init | _init |
t_skip | _skip |
t_body_star | _body_star |
t_body | _body |
t_inc | _inc |
t_exit | _exit |
Definition at line 1578 of file loop.c.
References copy_transformer(), fprintf(), ifdebug, NIL, print_transformer, print_transformers(), transformer_combine(), transformer_normalize(), and two_transformers_to_list().
Referenced by complete_any_loop_transformer(), and new_complete_whileloop_transformer_list().
transformer complete_forloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
forloop | fl | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
t_body_star | _body_star |
pre | re |
fl | l |
Definition at line 1686 of file loop.c.
References complete_any_loop_transformer(), complete_statement_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), load_statement_transformer(), safe_expression_to_transformer(), transformer_apply(), and transformer_undefined.
Referenced by generic_complete_statement_transformer().
list complete_forloop_transformer_list | ( | transformer | t_body_star, |
transformer | pre, | ||
forloop | fl | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
t_body_star | _body_star |
pre | re |
fl | l |
Definition at line 1732 of file loop.c.
References complete_any_loop_transformer(), complete_statement_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), list_undefined, load_statement_transformer(), pips_internal_error, safe_expression_to_transformer(), transformer_apply(), and transformer_undefined.
Referenced by instruction_to_transformer_list().
transformer complete_loop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
loop | l | ||
) |
The transformer computed and stored for a loop is useful to compute the loop body precondition, but it is not useful to analyze a higher level construct, which need the loop transformer with the exit condition.
Only Fortran DO loops are handled here. The need for nested WHILE loops has not been identified yet. The index variable is always initialized and then the loop is either entered and exited or not entered
loop body transformer
compute the loop body transformer
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
compute the loop body precondition
You do not need a range to recurse. A full precondition with arguments is expected by complete_loop_transformer(). Maybe, but it's much easier to debug with ranges as they only carry the useful information. And the result is correct for Semantics-New/for03.c and 04.c
The final index incrementation is performed later by add_loop_index_exit_value()
btf = transformer_add_loop_index_incrementation(btf, l, pre);
compute the transformer when the loop is entered: T o T*
Semantics-New/for04.c: this leads to t_enter == empty_transformer because the same conditions on the initial values of cpi and cpj are preserved in both ltf, which is OK, and btf, which is not OK.
add the entry condition
but it seems to be in t already
t_enter = transformer_add_loop_index_initialization(t_enter, l);
It would make sense to apply the incrementation, but this is performed as a side effect by add_loop_index_exit_value(), which avoids unfeasability wrt the final loop bound.
add the exit condition, without any information pre to estimate the increment
FI: oops, pre is used in spite of previous comment
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
pre cannot be used as such. the loop initialization must be applied first: the previous comment seems to be correct.
ltf | tf |
pre | re |
Definition at line 1927 of file loop.c.
References add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), empty_range_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, load_statement_transformer(), loop_body, loop_range, non_empty_range_wrt_precondition_p(), pips_debug, print_transformer, statement_instruction, statement_loop_p(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by complete_loop_transformer_list(), generic_complete_statement_transformer(), and old_complete_whileloop_transformer().
list complete_loop_transformer_list | ( | transformer | ltf, |
transformer | pre, | ||
loop | l | ||
) |
loop body transformer
compute the loop body transformer
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
compute the loop body precondition
You do not need a range to recurse. A full precondition with arguments is expected by complete_loop_transformer().
The final index incrementation is performed later by add_loop_index_exit_value()
btf = transformer_add_loop_index_incrementation(btf, l, pre);
compute the transformer when the loop is entered: T o T*
add the entry condition
but it seems to be in t already
t_enter = transformer_add_loop_index_initialization(t_enter, l);
It would make sense to apply the incrementation, but this is performed as a side effect by add_loop_index_exit_value(), which avoids unfeasability wrt the final loop bound.
add the exit condition, without any information pre to estimate the increment
FI: oops, pre is used in spite of previous comment
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
ltf | tf |
pre | re |
Definition at line 2061 of file loop.c.
References add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), complete_loop_transformer(), empty_range_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, list_undefined, load_statement_transformer(), loop_body, loop_range, non_empty_range_wrt_precondition_p(), pips_debug, pips_internal_error, print_transformer, statement_instruction, statement_loop_p(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), transformer_identity(), transformer_normalize(), transformer_undefined, and transformer_undefined_p.
Referenced by instruction_to_transformer_list().
transformer complete_repeatloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
whileloop | wl | ||
) |
t_body_star | _body_star |
pre | re |
wl | l |
Definition at line 1910 of file loop.c.
References complete_repeatloop_transformer_list(), and transformer_list_to_transformer().
Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().
list complete_repeatloop_transformer_list | ( | transformer | t_body_star, |
transformer __attribute__((unused)) | pre, | ||
whileloop | wl | ||
) |
An effort could be made to compute the precondition for t_exit
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
The generic equation is not adpated to repeat loops, which may execute once or at least twice instead of zero or twice
The equation is: t_loop = (t_body ; t_exit) + (t_body ; t_continue ; t_body_star ; t_body ; t_exit)
where we assume that t_body_star includes the continuation condition.
Definition at line 1845 of file loop.c.
References complete_statement_transformer(), condition_to_transformer(), copy_transformer(), free_transformer(), load_statement_transformer(), NIL, transformer_apply(), transformer_combine(), transformer_empty(), transformer_identity(), transformer_undefined, two_transformers_to_list(), whileloop_body, and whileloop_condition.
Referenced by complete_repeatloop_transformer(), and complete_whileloop_transformer_list().
transformer complete_whileloop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | wl | ||
) |
FI: I'm not sure this function is useful.
ltf | tf |
pre | re |
wl | l |
Definition at line 2183 of file loop.c.
References complete_repeatloop_transformer(), evaluation_before_p, new_complete_whileloop_transformer(), transformer_undefined, and whileloop_evaluation.
Referenced by old_complete_whileloop_transformer().
list complete_whileloop_transformer_list | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | wl | ||
) |
ltf | tf |
pre | re |
wl | l |
Definition at line 2198 of file loop.c.
References complete_repeatloop_transformer_list(), evaluation_before_p, new_complete_whileloop_transformer_list(), NIL, and whileloop_evaluation.
Referenced by instruction_to_transformer_list().
transformer forloop_to_postcondition | ( | transformer | pre, |
forloop | fl, | ||
transformer | t_body_star | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Clean up memory
pre | re |
fl | l |
t_body_star | _body_star |
Definition at line 2707 of file loop.c.
References any_loop_to_postcondition(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), load_statement_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_dup(), and transformer_undefined.
Referenced by instruction_to_postcondition().
transformer forloop_to_transformer | ( | forloop | fl, |
transformer | pre, | ||
list | flel | ||
) |
effects of forloop fl
t_body_star = t_init ; t_enter ;(t_body ; t_next)*
Deal with initialization expression
Deal with condition expression
An effort could be made to compute the precondition for t_continue, especially if the precondition to t_inc is available.
Deal with increment expression
An effort could be made to compute the precondition for t_inc
Let's clean up the memory
fl | l |
pre | re |
flel | lel |
Definition at line 326 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), and transformer_undefined.
Referenced by instruction_to_transformer().
list forloop_to_transformer_list | ( | forloop l | __attribute__(unused), |
transformer pre | __attribute__(unused), | ||
list e | __attribute__(unused) | ||
) |
Definition at line 371 of file loop.c.
References NIL, and pips_internal_error.
|
static |
FI: I do not have one test case to show that this function is of some use.
add information about the old value of tfb as convex hull of the entry precondition and of tfb's own image. For instance, if variable I is equal to 0 on entry and set ot either 0 or 1, the loop is always started with in [0, 1]
Definition at line 2412 of file loop.c.
References free_transformer(), ifdebug, pips_debug, print_transformer, transformer_convex_hull(), transformer_domain_intersection(), and transformer_range().
Referenced by standard_whileloop_to_transformer().
transformer loop_bound_evaluation_to_transformer | ( | loop | l, |
transformer | pre | ||
) |
Side effects in loop bounds and increment are taken into account.
The conditions on the loop index are given by the range of this transformer.
pre | re |
Definition at line 1203 of file loop.c.
References any_expression_to_transformer(), entity_has_values_p(), entity_to_expression(), entity_to_new_value(), entity_type, expression_and_precondition_to_integer_interval(), free_expression(), loop_index, loop_initialization_to_transformer(), loop_range, make_local_temporary_value_entity(), range_increment, range_lower, range_upper, reset_temporary_value_counter(), transformer_inequality_add(), transformer_safe_apply(), transformer_safe_image_intersection(), transformer_safe_intersection(), transformer_temporary_value_projection(), transformer_undefined, VALUE_MONE, VALUE_ONE, vect_add_elem(), vect_multiply(), and vect_new().
Referenced by add_good_loop_conditions().
transformer loop_initialization_to_transformer | ( | loop | l, |
transformer | pre | ||
) |
Note: It used to be implemented by computing the effect list of the lower bound expression and and new allocated effect for the loop index definition.
It turns out to be very heavy, because cells must be of kind preference to be usable by several functions because macro effect_reference() expects so without testing it.
However, it is also difficult to add a variable to the transformer t_init because of aliasing. So let's stick to the initial implementation.
over-approximation of effects
free_effects() is not enough, because it is a persistant reference
pre | re |
Definition at line 1266 of file loop.c.
References any_scalar_assign_to_transformer(), cell_preference, CONS, EFFECT, effect_cell, expression_to_proper_constant_path_effects(), free_effect(), free_reference(), free_transformer(), gen_free_list(), gen_nconc(), ifdebug, is_cell_preference, list_undefined, loop_index, loop_range, make_action_write_memory(), make_approximation_exact(), make_cell(), make_descriptor_none(), make_effect(), make_preference(), make_reference(), NIL, preference_reference, print_effects, range_lower, transformer_safe_range(), and transformer_undefined.
Referenced by loop_bound_evaluation_to_transformer(), loop_to_postcondition(), loop_to_total_precondition(), and loop_to_transformer().
transformer loop_to_continue_transformer | ( | loop | l, |
transformer | pre | ||
) |
FI: the function transformer_add_loop_index_incrementation should be rewritten to exploit preconditions better.
pre | re |
Definition at line 1501 of file loop.c.
References free_transformer(), loop_to_enter_transformer(), transformer_add_loop_index_incrementation(), transformer_combine(), and transformer_identity().
Referenced by new_loop_to_transformer().
transformer loop_to_enter_transformer | ( | loop | l, |
transformer | pre | ||
) |
Transformer expressiong the conditions between the index and the loop bounds according to the sign of the increment.
A zero increment is not legal because the Fortran standard imposes a division by the increment.
Only the loop bopy statement number is available...
Assumption: no side effect in loop bound expressions
The increment is strictly positive
The increment is strictly negative
The sign of the increment is unknown, no information is available
No information is available for loop indices that are not integer
This could be improved, but floating point indices should never be used.
pre | re |
Definition at line 1442 of file loop.c.
References entity_type, free_transformers(), integer_expression_and_precondition_to_integer_interval(), loop_index, loop_range, make_local_temporary_value_entity(), pips_user_error, range_increment, range_lower, range_upper, safe_integer_expression_to_transformer(), scalar_integer_type_p(), transformer_add_inequality_with_linear_term(), transformer_identity(), transformer_intersection(), transformer_normalize(), and transformer_temporary_value_projection().
Referenced by loop_to_continue_transformer(), and new_loop_to_transformer().
transformer loop_to_initialization_transformer | ( | loop | l, |
transformer | pre | ||
) |
Transformer expression the loop initialization.
pre | re |
Definition at line 1430 of file loop.c.
References assigned_expression_to_transformer(), loop_index, loop_range, and range_lower.
Referenced by new_loop_to_transformer().
transformer loop_to_postcondition | ( | transformer | pre, |
loop | l, | ||
transformer | tf | ||
) |
pips_internal_error("Equality option not implemented");
the standard version should be OK for SEMANTICS_EQUALITY_INVARIANTS...
basic cheap version: add information on loop index in pre and propagate preb downwards in the loop body; compute the loop postcondition independently using the loop transformer
preb = precondition for loop body; includes a lousy fix-point
Get rid of information related to variables modified in iterations of the loop body (including loop indices).
Apparently, the loop index incrementation is not in tf... according to a test with DO I = I, N although it should be... according to the caller of this function and the display of loop transformers!
Triolet's good loop algorithm
It might be useful to normalize preb and to detect unfeasibility. I choose not to do it because:
So basically, I shift the burden from precondition computation to dead code elimination. Dead loop testing must use a strong feasibility test.
If this decision is reversed, dead code elimination can be speeded-up.
Note that add_good_loop_conditions() can test trivial cases automatically generated.
Decision reverted: Francois Irigoin, 4 June 1997
preb can now be used to obtain a refined tf, for instance to show that a variable is monotonically increasing.
FI: this is not correct when an invariant is found; we should add one more incrementation of I (to modify the output of the invariant and express the fact that the loop bound is no more true, at least when the increment is one. 6 July 1993
Note 1: this comments was wrong! See Validation/Semantics/induc1.f Note 2: but the result was wrong anyway because it assumed that at least one iteration always was performed. Note 3: This is fixed by reverting the above decision.
propagate an impossible precondition in the loop body
The loop body precondition is not useful any longer
propagate preconditions in the loop body and compute its postcondition...
... or compute directly the postcondition using the loop body transformer. This second approach is slightly less precise because the transformer cannot use preconditions to avoid some convex approximations.
post = transformer_apply(tf, pre);
The loop body effects should be passed as fourth argument to check that the value of the upper bound expression is not modified when the body is executed. But it is not available and it is not yet used by ad_loop_index_exit_value()!
First version: OK, but could be better!
transformer postloop = transformer_apply(tf, pre);
pre must be copied because sc_convex_hull updates is arguments and may make them inconsistent when the two bases are merged to perform the convex hull in a common vector space
Second version: assume it is empty or non-empty and perform the convex hull of both (should be checked on Validation/Semantics/induc1.f)
propagate preconditions in the loop body
post_al = transformer_apply(tf, pre);
We should add (when possible) the non-entry condition in post_ne! For instance, DO I = 1, N leads to N <= 0
FI: Cannot be freed because it was stored for statement s: transformer_free(preb); did I mean to free pre, which is useless since it was changed into preb?
pre | re |
tf | f |
Definition at line 2841 of file loop.c.
References add_good_loop_conditions(), add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), debug(), empty_range_wrt_precondition_p(), fprintf(), free_transformer(), get_bool_property(), ifdebug, loop_body, loop_initialization_to_transformer(), loop_range, non_empty_range_wrt_precondition_p(), pips_debug, pips_flag_p, pips_internal_error, print_transformer, recompute_loop_transformer(), SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_range(), and transformer_undefined.
Referenced by instruction_to_postcondition().
transformer loop_to_total_precondition | ( | transformer | t_post, |
loop | l, | ||
transformer | tf, | ||
transformer | context | ||
) |
Triolet's good loop algorithm
preb = transformer_dup(pre);
The loop is never executed
impact of loop index initialization, i.e. I = IT(J),.. or I = K/L,..
the loop may be entered for sure, or entered or not
We need a fix_point without the initial condition but with the exit condition
Also performs last incrementation
free_transformer(b_t_pre); it is associated to the loop body!
The loop is always entered
The loop may be skipped or entered
skipped case computed here too
t_post | _post |
tf | f |
context | ontext |
Definition at line 3023 of file loop.c.
References add_good_loop_conditions(), add_loop_index_exit_value(), add_loop_skip_condition(), empty_range_wrt_precondition_p(), fprintf(), free_transformer(), get_bool_property(), ifdebug, load_statement_transformer(), loop_body, loop_initialization_to_transformer(), loop_range, non_empty_range_wrt_precondition_p(), pips_assert, pips_debug, print_transformer, recompute_loop_transformer(), statement_to_total_precondition(), transformer_add_loop_index_incrementation(), transformer_combine(), transformer_consistency_p(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_inverse_apply(), transformer_to_domain(), and transformer_undefined.
Referenced by instruction_to_total_precondition().
transformer loop_to_transformer | ( | loop | l, |
transformer | pre, | ||
list | e | ||
) |
The transformer associated to a DO loop does not include the exit condition because it is used to compute the precondition for any loop iteration.
There is only one attachment for the unbounded transformer and for the bounded one.
loop transformer tf = tfb* or tf = tfb+ or ...
loop body transformer
approximate loop transformer, including loop index updates
loop body precondition
Information about loop local variables is lost
range r = loop_range(l);
eliminate all information about local variables
Mostly useful for Fortran code.
In C, variables declared in the loop body do not exist before the loop is entered and so do not have to be projected. But local variables may have been introduced by a privatization phase.
compute the loop body transformer under loop body precondition preb
add indexation step under loop precondition pre
compute tfb's fix point according to pips flags
restrict the domain of tf by the range of pre, except for the loop index which is assigned in between
add initialization for the unconditional initialization of the loop index variable
we have a problem here: to compute preconditions within the loop body we need a tf using private variables; to return the loop transformer, we need a filtered out tf; only one hook is available in the ri..; let'a assume there are no private variables and that if they are privatizable they are not going to get in our way
pre | re |
Definition at line 1319 of file loop.c.
References add_good_loop_conditions(), add_index_range_conditions(), CONS, effects_to_transformer(), ENTITY, external_value_name(), fprint_transformer(), fprintf(), free_transformer(), gen_free_list(), get_bool_property(), ifdebug, invariant_wrt_transformer(), load_statement_transformer(), loop_body, loop_index, loop_initialization_to_transformer(), loop_locals, loop_range, NIL, pips_debug, print_transformer, safe_transformer_projection(), statement_to_transformer(), transformer_add_loop_index_incrementation(), transformer_combine(), transformer_domain_intersection(), transformer_dup(), transformer_filter(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by instruction_to_transformer().
list loop_to_transformer_list | ( | loop l | __attribute__(unused), |
transformer pre | __attribute__(unused), | ||
list e | __attribute__(unused) | ||
) |
transformer new_complete_whileloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
whileloop | wl, | ||
bool | entered_p | ||
) |
entered_p is used to for the execution of at least one iteration
t_body_star | _body_star |
pre | re |
wl | l |
entered_p | ntered_p |
Definition at line 1833 of file loop.c.
References new_complete_whileloop_transformer_list(), and transformer_list_to_transformer().
Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().
list new_complete_whileloop_transformer_list | ( | transformer | t_body_star, |
transformer | pre, | ||
whileloop | wl, | ||
bool entered_p | __attribute__(__unused__) | ||
) |
entered_p is used to for the execution of at least one iteration
An effort could be made to compute the preconditions for t_continue and t_exit: see while04.c.
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
Should we instead compute recursively a transformer list?
Definition at line 1781 of file loop.c.
References complete_any_loop_transformer_list(), complete_statement_transformer(), condition_to_transformer(), free_transformer(), load_statement_transformer(), NIL, transformer_apply(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by complete_whileloop_transformer_list(), and new_complete_whileloop_transformer().
transformer new_loop_to_transformer | ( | loop | l, |
transformer | pre, | ||
list | lel | ||
) |
loop_to_transformer() was developed first but is not as powerful as the new algorithm used for all kinds of loops.
See flip-flop01.c.
Equation:
t_body_star = t_init ; t_enter ;(t_body ; t_inc; t_continue)*
t_init, t_enter and t_continue, which includes t_inc, must be computed from the loop and its precondition, pre, and extended body effects, lel. In case the loop index appears in the bound or increment expressions, the Fortran standard should be used to determine the precondition to use. The same is true in case of side-effects in the loop expressions.
t_body must be computed from the loop body and a preliminary loop invariant.
Deal with initialization expression, which may be included in the condition as in while(i++, j=0, i<m)? No because the expression is going to be evaluated at each cycle. The ised effects must be part of the condition transformer, tcond
Deal with enter transformers
An effort could be made to compute the precondition for t_continue. Precondition pre and the loop effect list lel could be used.
approximate loop transformer, including loop index updates
first approximation of the loop body precondition
FI: could do better with body_transformer
Let's clean up the memory
pre | re |
lel | el |
Definition at line 1516 of file loop.c.
References any_loop_to_transformer(), effects_to_transformer(), free_transformer(), invariant_wrt_transformer(), loop_body, loop_to_continue_transformer(), loop_to_enter_transformer(), loop_to_initialization_transformer(), transformer_apply(), transformer_range(), and transformer_undefined.
transformer new_whileloop_to_k_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel, | ||
int | k | ||
) |
t_body_star = t_init ; t_enter ;(t_body ; t_next)*
Deal with initialization expression
Deal with condition expression
An effort could be made to compute the precondition for t_continue.
Let's clean up the memory
wl | l |
pre | re |
wlel | lel |
k | effects of whileloop wl |
Definition at line 416 of file loop.c.
References any_loop_to_k_transformer(), condition_to_transformer(), free_transformer(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_k_transformer().
transformer new_whileloop_to_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel | ||
) |
effects of whileloop wl
Equation:
t_body_star = t_init ; t_enter ;(t_body ; t_continue)*
Deal with initialization expression, which may be included in the condition as in while(i++, j=0, i<m)? No because the expression is going to be evaluated at each cycle. The ised effects must be part of the condition transformer, tcond
Deal with condition expression
An effort could be made to compute the precondition for t_continue.
Let's clean up the memory
wl | l |
pre | re |
wlel | lel |
Definition at line 380 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), free_transformer(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_transformer().
transformer old_complete_whileloop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | l | ||
) |
loop body transformer
Recompute the exact loop body transformer. This is weird: it should have already been done by statement_to_transformer and propagated bask. However, we need to recompute it because it has not been stored and cannot be retrieved. It might be better to use complete_statement_transformer(retrieved t, preb, s).
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
The proper transformer has been stored.
btf = transformer_add_condition_information(btf, cond, preb, true);
add the exit condition
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
ltf | tf |
pre | re |
Definition at line 2213 of file loop.c.
References complete_loop_transformer(), complete_whileloop_transformer(), condition_false_wrt_precondition_p(), condition_true_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, instruction_whileloop, invariant_wrt_transformer(), load_statement_transformer(), pips_debug, print_transformer, statement_instruction, statement_loop_p(), statement_whileloop_p(), transformer_add_condition_information(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_identity(), transformer_undefined, transformer_undefined_p, whileloop_body, and whileloop_condition.
transformer precondition_filter_old_values | ( | transformer | pre | ) |
pre | re |
Definition at line 1065 of file loop.c.
References BASE_NULLE_P, BASE_UNDEFINED, old_value_entity_p(), pips_assert, predicate_system, transformer_relation, vecteur_succ, and vecteur_var.
|
static |
Recompute a fixpoint conditionnally to a valid precondition for all iterations.
get rid of information modified by the loop body or the loop header
get rid of old values in preb which are meaning less in tf
do not try to eliminate the same variable twice
Not all values can be projected in preb because some may appear in tf and not in preb
add the remaining conditional information to the loop transformer
Definition at line 2310 of file loop.c.
References arguments_add_entity(), arguments_difference(), dup_arguments(), external_value_name(), free_transformer(), gen_free_list(), gen_list_and(), gen_list_and_not(), gen_nconc(), ifdebug, list_undefined, load_statement_transformer(), loop_body, loop_index, pips_assert, pips_debug, predicate_system, print_arguments(), print_transformer, sc_append(), sc_fprint(), transformer_add_loop_index_incrementation(), transformer_add_loop_index_initialization(), transformer_arguments, transformer_dup(), transformer_internal_consistency_p(), transformer_projectable_values(), transformer_projection(), transformer_relation, transformer_undefined, variables_to_old_values(), and variables_to_values().
Referenced by loop_to_postcondition(), and loop_to_total_precondition().
transformer repeatloop_to_postcondition | ( | transformer | pre, |
whileloop | wl, | ||
transformer | t_body_star | ||
) |
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
The repeat loop does not fit well in the current generic approach. Most of the basic transformers such as t_init, t_skip, t_enter,... are meaningless. Instead of dealing with zero or at least one iteration, we have to deal with one or at least two.
post = (t_body_c ; t_exit)(pre) + (t_body_c ; t_continue ; t_body_star ; t_body_c ; t_exit)(pre)
where we assume that t_body_star includes the continuation condition.
Clean up memory
pre | re |
wl | l |
t_body_star | _body_star |
Definition at line 2760 of file loop.c.
References any_loop_to_postcondition(), complete_statement_transformer(), condition_to_transformer(), copy_transformer(), free_transformer(), load_statement_transformer(), transformer_apply(), transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by instruction_to_postcondition().
transformer repeatloop_to_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel | ||
) |
effects of whileloop wl
t_body_star = t_init ; t_enter ; (t_body ; t_next)+
t_once = t_body; t_exit
t_repeat = t_body_star + t_once
An effort could be made to compute the precondition for t_continue, especially if the precondition to t_inc is available.
FI: it should be computed with the postcondition of the body
The loop is executed at least twice; FI: I'm note sure the twice is captured
FI: example dowhile02 seems to show this is wrong with t_next empty, in spite of the star
The loop is executed only once
global transformer
wl | l |
pre | re |
wlel | lel |
Definition at line 449 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), copy_transformer(), load_statement_transformer(), transformer_combine(), transformer_convex_hull(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_transformer().
bool simple_dead_loop_p | ( | expression | lower, |
expression | upper | ||
) |
lower | ower |
upper | pper |
Definition at line 1028 of file loop.c.
References NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, term_cst, value_gt, value_neg_p, value_pos_p, VECTEUR_NUL_P, vecteur_succ, and vecteur_val.
Referenced by add_index_range_conditions().
transformer standard_whileloop_to_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e | ||
) |
This function computes the effect of K loop iteration, with K positive.
This function does not take the loop exit into account because its result is used to compute the precondition of the loop body. Hence the loop exit condition only is added when preconditions are computed. This is confusing when transformers are prettyprinted with the source code.
loop transformer tf = tfb* or tf = tfb+ or ...
loop body transformer
Make sure not to leave too much information in pre. Perform a very simplistic fix point based on effects.
If the while entry condition is usable, it must be added on the old values
I'd like to use pre_n as context to evaluate the condition cond, but I'm not sure it's safe (Francois Irigoin)
Side effects in cond are ignored!
compute the whileloop body transformer, including the initial conditions
The convex hull of the image of pre and of the image of tfb can be added as conditions on tfb's domain, if some information is available in pre
compute tfb's fix point according to pips flags
The second clause is probably stronger than the first one
The loop is never entered
Side effects of the condition evaluation should be taken into account
A temporary variable is expected as first argument. There is something to fix.
tf = any_expression_to_transformer();
The loop is never exited, e.g. because there is a STOP or an infinite loop inside
Dirty looking fix for a fix point computation error: sometimes, the basis is restricted to a subset of the integer scalar variables. Should be useless with proper fixpoint opertors.
we have a problem here: to compute preconditions within the whileloop body we need a tf using private variables; to return the loop transformer, we need a filtered out tf; only one hook is available in the ri..; let'a assume there are no private variables and that if they are privatizable they are not going to get in our way
basic cheap version: do not use the whileloop body transformer and avoid fix-points; local variables do not have to be filtered out because this was already done while computing effects
The loop body transformers could benefit from pre_n instead of transformer_undefined, but who would think of combining these two options?
pre | re |
Definition at line 2456 of file loop.c.
References condition_false_wrt_precondition_p(), effects_to_transformer(), external_value_name(), fprint_transformer(), fprintf(), free_transformer(), ifdebug, invariant_wrt_transformer(), loop_body_transformer_add_entry_and_iteration_information(), pips_debug, pips_flag_p, precondition_add_condition_information(), predicate_system, print_transformer, sc_append(), SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_transformer(), transformer_dup(), transformer_empty(), transformer_empty_p(), transformer_equality_fix_point(), transformer_fix_point_operator, transformer_halbwachs_fix_point(), transformer_identity(), transformer_relation, transformer_undefined, transformer_undefined_p, whileloop_body, and whileloop_condition.
transformer transformer_add_loop_index_incrementation | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
SHOULD BE REWRITTEN WITH EXPRESSION_TO_TRANSFORMER
it does not contain the loop index update the loop increment expression must be linear to find inductive variables related to the loop index
tf | f |
pre | re |
Definition at line 1136 of file loop.c.
References arguments_add_entity(), base_add_variable(), base_dimension, entity_has_values_p(), entity_local_name(), entity_to_new_value(), entity_to_old_value(), expression_to_affine(), loop_index, loop_range, pips_assert, pips_user_warning, predicate_system, range_increment, transformer_add_variable_incrementation(), transformer_arguments, transformer_consistency_p(), transformer_relation, value_mappings_compatible_vector_p(), VECTEUR_UNDEFINED, and VECTEUR_UNDEFINED_P.
Referenced by loop_to_continue_transformer(), loop_to_total_precondition(), loop_to_transformer(), and recompute_loop_transformer().
transformer transformer_add_loop_index_initialization | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
The loop initialization is performed before tf.
EXPRESSION_TO_TRANSFORMER SHOULD BE USED
The new variables in eq must be added to sc; otherwise, further consistency checks core dump. bc.
sc_add_egalite(sc, eq);
The call to sc_projection_with_eq frees eq
FI: a NULL is not acceptable; I assume that we cannot end up with a SC_EMPTY...
Get rid of the initial value since it is unknowable
tf | f |
pre | re |
Definition at line 1082 of file loop.c.
References base_dimension, base_rm, base_union(), CONS, contrainte_make(), CONTRAINTE_UNDEFINED, ENTITY, entity_has_values_p(), entity_to_old_value(), eq, loop_index, loop_range, make_base_from_vect(), newgen_Psysteme, NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, predicate_system, predicate_system_, range_lower, sc_make(), transformer_projection(), transformer_relation, VALUE_MONE, vect_add_elem(), and vect_dup().
Referenced by recompute_loop_transformer().
transformer whileloop_to_k_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e, | ||
int | k | ||
) |
pre | re |
k | effects of whileloop l |
Definition at line 2617 of file loop.c.
References evaluation_before_p, new_whileloop_to_k_transformer(), pips_internal_error, transformer_undefined, and whileloop_evaluation.
Referenced by whileloop_to_postcondition().
transformer whileloop_to_postcondition | ( | transformer | pre, |
whileloop | l, | ||
transformer | tf | ||
) |
propagate an impossible precondition in the loop body
do not add the exit condition since it is redundant with pre, but take care of side effects in the condition c
transformer_apply() generates a lot of warnings
The loop may be entered at least once.
The standard transformer tb is not enough, especially if the loop body s is a loop since then it is not even the statement transformer, but more generally we do not want the identity to be taken into account in tb since it is already added with P0. So we would like to guarantee that at least one state change occurs: we are not interested in identity iterations. For instance, if s is a loop, this means that the loop is entered, except if the loop condition has side effects.
To recompute this transformer, we use a pre_fuzzy=T*(P0) because we have nothing better.
complete_statement_transformer() is not really useful here because we usually do not have tighly nested while loops.
Nothing special in the loop body: no tests, no while,...
Recompute the body transformer without taking identity transformers into account. This is not enough because the decision about "activity" should be made dimension by dimension. We cannot get good result in general with a convex hull performed here: only specific cases are handled. We need instead a complex formulae to compute the loop precondition as a function of p_0 and all t_i
btl is copied because the function below frees at least its components
The loop fix point transformer T* could be used to obtain the set of stores for any number of iterations, including 0. Instead, use T+ and a convex hull with the precondition for the first iteration, which preserves more information when the fixpoint is not precise:
P^* = P_0 U cond(c)(tb(cond(c)(tb^*(P_0))))
Bertrand Jeannet suggests that we compute P0 U T(P0) U T^2(P0) U T_3(P0) where T_3 is the transitive closure obtained for iterations 3 to infinity by setting the initial iteration number k to 3 before projection. NSAD 2010. No test case has been forwarded to show that this would be useful.
We need the loop effects to recompute the unrolled transformer. Let's use NIL to start with... disaster. Let's use the body effects and hope for no side effects in loop condition.
FI: since pre_next is no longer useful, pre_next2 could be avoided. It just makes debugging easier.
propagate preconditions in the loop body and get its postcondition
At least one iteration is executed. The postcondition can be computed into three different ways:
or use both and use their intersection as unique postcondition (the added redundant information seems to result in less information after a projection for w09.f, Halbwachs car example).
The second way is more likely to suffer from non-convexity as it uses many more steps.
Also, note that precondition_add_condition_information() is more geared towards Fortran as it assumes no side effects in the condition evaluation. However, it is better at handling non-convex condition than condition_to_transformer(), but condition_to_transformer(), which is built on top of precondition_add_condition_information() could be improved/might be improvable... In case the condition is not convex, there is no single transformer which fits it. But the postcondition can be updated with different convex components and then different results united in a unique postcondition by a convex hull.
Let's execute the last iteration since it certainly exists
Assume the loop is entered, post_al, or not, post_ne, and perform the convex hull of both
The loop is executed at least once: let's execute the last iteration
The loop is never executed
pre | re |
tf | f |
Definition at line 3141 of file loop.c.
References active_transformer_list_to_transformer(), CAR, complete_statement_transformer(), condition_to_transformer(), copy_transformer(), empty_transformer(), false_condition_wrt_precondition_p(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), get_int_property(), ifdebug, int, list_undefined, load_cumulated_rw_effects_list(), load_statement_transformer(), pips_debug, pips_flag_p, pips_internal_error, pips_user_error, precondition_add_condition_information(), print_transformer, SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), statement_to_transformer_list(), TRANSFORMER, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_identity(), transformer_intersection(), transformer_list_multiple_closure_to_precondition(), transformer_list_to_active_transformer_list(), transformer_range(), transformer_undefined, true_condition_wrt_precondition_p(), whileloop_body, whileloop_condition, and whileloop_to_k_transformer().
Referenced by instruction_to_postcondition().
transformer whileloop_to_total_precondition | ( | transformer | t_post, |
whileloop | l, | ||
transformer | tf, | ||
transformer | context | ||
) |
transformer_dup(pre)
Apply the loop fix point transformer T* to obtain the set of stores for any number of iteration, including 0.
propagate an impossible precondition in the loop body
The loop body precondition is not useful any longer
do not add the exit condition since it is redundant with pre
post = transformer_dup(pre);
At least one iteration is executed. The transformer of the loop body is not useful!
transformer tb = load_statement_transformer(s);
propagate preconditions in the loop body
ntl = transformer_apply(tf, pre);
Let's execute the last iteration since it certainly exists
post = transformer_apply(tb, ntl);
post = precondition_add_condition_information(post, c, post, false);
Assume the loop is entered, post_al, or not, post_ne, and perform the convex hull of both
= transformer_dup(pre)
propagate preconditions in the loop body
The loop is executed at least once: let's execute the last iteration
The loop is never executed
post = transformer_convex_hull(post_ne, post_al);
t_post | _post |
tf | f |
context | ontext |
Definition at line 3439 of file loop.c.
References false_condition_wrt_precondition_p(), free_transformer(), ifdebug, load_statement_transformer(), pips_assert, pips_debug, pips_flag_p, pips_internal_error, precondition_add_condition_information(), print_transformer, SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), transformer_apply(), transformer_combine(), transformer_empty(), transformer_free(), transformer_undefined, true_condition_wrt_precondition_p(), whileloop_body, and whileloop_condition.
Referenced by instruction_to_total_precondition().
transformer whileloop_to_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e | ||
) |
effects of whileloop l
pre | re |
Definition at line 2583 of file loop.c.
References evaluation_before_p, new_whileloop_to_transformer(), repeatloop_to_transformer(), transformer_undefined, and whileloop_evaluation.
Referenced by instruction_to_transformer().