PIPS
|
#include <stdio.h>
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "ri-util.h"
#include "properties.h"
#include "misc.h"
#include "transformer.h"
Go to the source code of this file.
Functions | |
list | merge_transformer_lists (list tl1, list tl2) |
Functions to deal with transformer lists. More... | |
bool | check_transformer_list (list tl) |
What do we want to impose? More... | |
list | combine_transformer_lists (list tl1, list tl2) |
each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer. More... | |
list | apply_transformer_lists_generic (list tl1, list tl2, bool exclude_p) |
each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer. More... | |
list | apply_transformer_lists (list tl1, list tl2) |
list | apply_transformer_lists_with_exclusion (list tl1, list tl2) |
list | clean_up_transformer_list (list tfl) |
Eliminate empty transformers and keep at most one identity transformer, placed as first list element. More... | |
list | two_transformers_to_list (transformer t1, transformer t2) |
Transformer two transformers into a correct transformer list. More... | |
transformer | generic_transformer_list_to_transformer (list ltl, bool active_p) |
Reduce the transformer list with the convex hull operator. More... | |
transformer | transformer_list_to_transformer (list ltl) |
Reduce the transformer list ltl to one transformer using the convex hull operator. More... | |
transformer | active_transformer_list_to_transformer (list ltl) |
Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator. More... | |
list | transformer_list_to_active_transformer_list (list tl) |
static transformer | transformer_list_closure_to_precondition_depth_two (list tl, transformer c_t, transformer p_0) |
Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t. More... | |
static transformer | transformer_list_closure_to_precondition_max_depth (list tl, transformer c_t, transformer p_0) |
Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t. More... | |
transformer | transformer_list_closure_to_precondition (list tl, transformer c_t, transformer p_0) |
Relay to select a heuristic. More... | |
list | transformer_list_safe_variables_projection (list tl, list proj) |
Returns a new list of newly allocated projected transformers. More... | |
list | transformer_list_to_argument (list tl) |
Returns the list of variables modified by at least one transformer in tl. More... | |
list | transformer_list_with_effect (list tl, entity v) |
build a sublist sl of the transformer list tl with transformers that modify the value of variable v More... | |
list | transformer_list_preserved_variables (list vl, list tl, list tl_v) |
returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v. More... | |
transformer | transformer_list_multiple_closure_to_precondition (list tl, transformer c_t, transformer p_0) |
When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition. More... | |
Psysteme | transformer_derivative_constraints (transformer t) |
Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x') More... | |
transformer | transformer_list_generic_transitive_closure (list tfl, bool star_p) |
Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers. More... | |
transformer | transformer_list_transitive_closure (list tfl) |
Compute (U tfl)*. More... | |
transformer | transformer_list_transitive_closure_plus (list tfl) |
Compute (U tfl)+. More... | |
static list | transformer_list_add_combination (int tn, transformer ta[tn], int n, transformer ct, int past) |
Internal recursive function. More... | |
static list | __attribute__ ((unused)) |
compute all combinations of n different transformers t from transformer list tl. More... | |
|
static |
compute all combinations of n different transformers t from transformer list tl.
No check is performed on the content of list tl. Empty transformers and identity transformers should have been removed before this call.
tl | a non-empty list of transformers |
int n: a strictly positive integer, smaller than the length of tl
Definition at line 1226 of file transformer_list.c.
References FOREACH, free_transformer(), gen_length(), NIL, pips_assert, TRANSFORMER, transformer_identity(), and transformer_list_add_combination().
transformer active_transformer_list_to_transformer | ( | list | ltl | ) |
Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator.
An active transformer is a transformer with argument(s): at least one value is changed.
Note: a hidden identity transformer such as T(i) {i==i::init} is not detected.
ltl | tl |
Definition at line 447 of file transformer_list.c.
References generic_transformer_list_to_transformer().
Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and whileloop_to_postcondition().
tl1 | l1 |
tl2 | l2 |
Definition at line 269 of file transformer_list.c.
References apply_transformer_lists_generic().
each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer.
If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list. Empty preconditions are not preserved in the returned list. An empty list is unfeasible.
if exclude_p==false, return U_i1 U_i2 apply(t_i1, p_i2); else return U_i1 U_i2!=i1 apply(t_i1, p_i2);
tl1 | l1 |
tl2 | l2 |
exclude_p | xclude_p |
Definition at line 223 of file transformer_list.c.
References check_transformer_list(), CONS, FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_apply(), and transformer_empty_p().
Referenced by apply_transformer_lists(), and apply_transformer_lists_with_exclusion().
tl1 | l1 |
tl2 | l2 |
Definition at line 274 of file transformer_list.c.
References apply_transformer_lists_generic().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
What do we want to impose?
The empty transformer list is used to represent the empty transformer...
It must be the first one
tl | l |
Definition at line 140 of file transformer_list.c.
References CAR, ENDP, FOREACH, pips_internal_error, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().
Referenced by apply_transformer_lists_generic(), combine_transformer_lists(), and merge_transformer_lists().
Eliminate empty transformers and keep at most one identity transformer, placed as first list element.
check_transformer_list(ntfl) should be TRUE.
tfl is fully destroyed (to avoid memory leaks and nightmares); to be more efficient, the transformers moved from the input list into the output list should be detached from the input list and then the input list could be fully destroyed without having to copy any transformers; but FOREACH operates at too high a level for this.
tfl | fl |
Definition at line 290 of file transformer_list.c.
References CONS, copy_transformer(), FOREACH, gen_full_free_list(), gen_nreverse(), NIL, TRANSFORMER, transformer_empty_p(), transformer_identity(), and transformer_identity_p().
Referenced by block_to_transformer_list().
each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer.
If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list.
tl1 | l1 |
tl2 | l2 |
Definition at line 180 of file transformer_list.c.
References check_transformer_list(), CONS, copy_transformer(), FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_combine(), transformer_empty_p(), and transformer_normalize().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
transformer generic_transformer_list_to_transformer | ( | list | ltl, |
bool | active_p | ||
) |
Reduce the transformer list with the convex hull operator.
If active_p is true, skip transformers that do not update the state. Beyond the identity transformer, any transformer without arguments does not really update the state, although it may restrict it.
A new transformer is always allocated. The transformers in the transformer list ltl are freed.
Look for the first useful transformer in the list
Only range conditions have been found: the store is restricted but not changed.
Take care of the following useful transformers
Look for the next useful transformer in the list
ltl | tl |
active_p | ctive_p |
Definition at line 384 of file transformer_list.c.
References copy_transformer(), ENDP, FOREACH, free_transformer(), POP, TRANSFORMER, transformer_arguments, transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_undefined, and transformer_undefined_p.
Referenced by active_transformer_list_to_transformer(), and transformer_list_to_transformer().
Functions to deal with transformer lists.
Tansformer lists are used to delay convex hulls and to refine the precondition computation of loops by putting aside the identity transformer.
If there is an identity transformer in the list, it is supposed to be the first one in the list.
However, some control paths are almost identity transformers because the store is apparently unchanged. However, they contain predicates on the possible values. Although they have no arguments, and hence, the store is left unchanged, they are different from the identity transformer bebcause the relation is smaller.
So it should be up to the function using the transformer list to decide how to cope with transformers that restrict the identity transition. Must not be used, beware of library cycles: include "semantics.h" Union of two lists
If the list includes the identity transformer, it must be the first in the list and be nowehere else
It is not clear if transformer lists will be stored in hash tables... Hence I do not know if the input list should be freed, reused or left unshared. To be conservative, no alias is created.
Do we have to worry about different bases in transformers?
Too much information is sometimes lost with this simplification
tl1 | l1 |
tl2 | l2 |
Definition at line 74 of file transformer_list.c.
References CAR, CDR, check_transformer_list(), CONS, ENDP, gen_full_copy_list(), gen_length(), gen_nconc(), ifdebug, NIL, pips_assert, TRANSFORMER, transformer_identity(), and transformer_identity_p().
Referenced by test_to_transformer_list().
Psysteme transformer_derivative_constraints | ( | transformer | t | ) |
Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x')
FI: this function should/might be located in fix_point.c
sc is going to be modified and returned
Do not handle variable which do not appear explicitly in constraints!
basis vector
Compute constraints with difference equations
Only generate difference equations if the old value is used
Project all variables but differences to get T'
Definition at line 891 of file transformer_list.c.
References BASE_NULLE, BASE_NULLE_P, contrainte_make(), CONTRAINTE_UNDEFINED, entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), ifdebug, old_value_entity_p(), pips_debug, predicate_system, sc_copy(), sc_equation_add(), sc_fprint(), sc_to_minimal_basis(), Svecteur::succ, TCST, transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), VECTEUR_NUL, and vecteur_var.
Referenced by transformer_list_generic_transitive_closure().
|
static |
Internal recursive function.
Should be used as transformer_list_combination(). As long as n is not zero, choose all unused transformation numbers in past and call yourself recursively after updating past and ct. past is a bit field. Each bit of past is set to 1 initially because no transformer has been used yet. It is reset to 0 when the transformation has been used. The selected transformer is combined to ct.
tn | is the number of transformers that can be chosen to be combined |
ta[tn] | is an array containing the tn transformers to combine |
n | is the number of combinations to perform. It is less than tn. |
ct | is the current combination of past transformers |
past | is a bit field used to keep track of transformers alreasy used to build ct |
Definition at line 1175 of file transformer_list.c.
References CONS, copy_transformer(), free_transformer(), gen_nconc(), NIL, pips_assert, TRANSFORMER, transformer_combine(), transformer_empty_p(), and transformer_normalize().
Referenced by __attribute__().
transformer transformer_list_closure_to_precondition | ( | list | tl, |
transformer | c_t, | ||
transformer | p_0 | ||
) |
Relay to select a heuristic.
tl | l |
c_t | _t |
p_0 | _0 |
Definition at line 705 of file transformer_list.c.
References get_string_property(), pips_assert, pips_user_error, transformer_consistency_p(), transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and transformer_undefined.
Referenced by transformer_list_multiple_closure_to_precondition().
|
static |
Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t.
The precondition of iteration 0 is p_0.
We need a developped formulae for P*=(U_i T_i)^*P_0... to postpone the convex hulls as much as possible
For instance, and this is a heuristics:
P_0 is known as pre_init
P_1 = U_i T_i(P_0)
P_2 = U_i U_j T_i(T_j(P_0))
P_3^s = U_i T_i^+(P_0) — only one path is used
P_3^+ = U_i U_j!=i T^+_i(T_j(T^*(P_1))) — at least two paths are used
which would make more sense when i and j are in [0..1]. Note that in P_3, T_j and T^+_i could be recomputed wrt P_1 instead of pre_fuzzy... which is not provided
Maybe T^*=(U_i T_i)^* could/should be computed as (U_i T_i*)* but it is not clear how all the useful conditions could be taken into account.
A more accurate approach would use several developped formulae for P* and an intersection of their results.
Definition at line 501 of file transformer_list.c.
References active_transformer_list_to_transformer(), apply_transformer_lists_with_exclusion(), combine_transformer_lists(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), ifdebug, one_to_one_transformers_combine(), pips_assert, pips_debug, print_transformer, transformer_apply(), transformer_consistency_p(), transformer_convex_hull(), transformer_list_to_transformer(), transformer_list_transitive_closure(), transformer_undefined, transformers_apply(), transformers_apply_and_keep_all(), transformers_combine(), and transformers_derivative_fix_point().
Referenced by transformer_list_closure_to_precondition().
|
static |
Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t.
The precondition of iteration 0 is p_0.
We need a developped formulae for P*=(U_i T_i)^*P_0... to postpone the convex hulls as much as possible
For instance, and this is a heuristics:
P_0 is known as pre_init
P_l = U_i T_i(P_0)
P_2 = U_i U_j T_i(T_j(P_0))
P_3^s = U_i T_i^+(P_0) — only one path is used
P_3^+ = U_i U_j!=i T^+_i(T_j(T^*(P_1))) — at least two paths are used
which would make more sense when i and j are in [0..1]. Note that in P_3, T_j and T^+_i could be recomputed wrt P_1 instead of pre_fuzzy... which is not provided
Maybe T^*=(U_i T_i)^* could/should be computed as (U_i T_i*)* but it is not clear how all the useful conditions could be taken into account.
A more accurate approach would use several developped formulae for P* and an intersection of their results.
Definition at line 618 of file transformer_list.c.
References active_transformer_list_to_transformer(), apply_transformer_lists_with_exclusion(), combine_transformer_lists(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), ifdebug, one_to_one_transformers_combine(), pips_assert, pips_debug, print_transformer, transformer_apply(), transformer_convex_hull(), transformer_list_to_transformer(), transformer_list_transitive_closure(), transformer_undefined, transformers_apply(), transformers_apply_and_keep_all(), transformers_combine(), and transformers_derivative_fix_point().
Referenced by transformer_list_closure_to_precondition().
transformer transformer_list_generic_transitive_closure | ( | list | tfl, |
bool | star_p | ||
) |
Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers.
Each transformer is used to compute its derivative and the derivatives are unioned by convex hull.
The reason for doing this is D(T1) U D(T2) == D(T1 U T2) but the complexity is lower
See http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Implicit equations, n::new - n::old = 0, are added because they are necessary for the convex hull.
Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old This code was cut-and-pasted from transformer_derivative_fix_point() but is more general and subsume it transformer transformer_derivative_fix_point(transformer tf)
Since we compute the * transitive closure and not the + transitive closure, the fix point is the identity.
basis of difference vectors
Compute the global argument list and the global base b
Cannot use arguments_union() because a new list is allocated
For each transformer t in list tl
compute its derivative constraint system
add the equations for the unchanged variables
compute its convex hull with the current value of sc if sc is already defined
Add corresponding equation
This could be optimized by using the convex hull of a Psystemes list and by keeping the dual representation of the result instead of converting it several time back and forth.
Multiply the constant terms by the iteration number ik and add a positivity constraint for the iteration number ik and then eliminate the iteration number ik to get T*(dx).
Difference variables must substituted back to differences between old and new values.
Only generate difference equations if the old value is used
Project all difference variables
The full basis must be used again
Plug sc back into tc_tf
That's all!
tfl | fl |
star_p | tar_p |
Definition at line 960 of file transformer_list.c.
References arguments_add_entity(), Ssysteme::base, base_add_variable(), BASE_NULLE, BASE_NULLE_P, base_remove_variable(), base_rm, base_union(), contrainte_make(), CONTRAINTE_UNDEFINED, cute_convex_union(), Ssysteme::dimension, ENDP, ENTITY, entity_is_argument_p(), entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), FOREACH, fprint_transformer(), ifdebug, make_local_temporary_integer_value_entity(), NIL, old_value_entity_p(), pips_debug, predicate_system, print_transformers(), sc_copy(), sc_empty(), sc_equation_add(), sc_fprint(), sc_free(), sc_multiply_constant_terms(), sc_to_minimal_basis(), Svecteur::succ, TCST, TRANSFORMER, transformer_arguments, transformer_consistency_p(), transformer_derivative_constraints(), transformer_empty(), transformer_identity(), transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), vect_size(), VECTEUR_NUL, and vecteur_var.
Referenced by transformer_list_transitive_closure(), and transformer_list_transitive_closure_plus().
transformer transformer_list_multiple_closure_to_precondition | ( | list | tl, |
transformer | c_t, | ||
transformer | p_0 | ||
) |
When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition.
The preconditions obtained with the different projections are intersected.
FI: this may be useless when derivatives are computed before the convex union. No. This was due to a bug in the computation of list of derivatives.
FI: this should be mathematically useless but it useful when a heuristic is used to compute the invariant. The number of transitions is reduced and hence a limited number of combinations is more likely to end up with a precise result.
tl | l |
c_t | _t |
p_0 | _0 |
Definition at line 826 of file transformer_list.c.
References arguments_difference(), arguments_subset_p(), copy_transformer(), ENTITY, FOREACH, free_transformer(), gen_copy_seq(), gen_free_list(), gen_full_free_list(), gen_length(), get_bool_property(), pips_assert, safe_transformer_projection(), transformer_arguments, transformer_consistency_p(), transformer_consistent_p(), transformer_intersection(), transformer_list_closure_to_precondition(), transformer_list_preserved_variables(), transformer_list_safe_variables_projection(), transformer_list_to_argument(), transformer_list_with_effect(), and transformer_range().
Referenced by whileloop_to_postcondition().
returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v.
tl_v is assumed to be a subset of tl.
vl | l |
tl | l |
tl_v | l_v |
Definition at line 786 of file transformer_list.c.
References CONS, ENTITY, entity_is_argument_p(), FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
Returns a new list of newly allocated projected transformers.
If a value of a variable in list proj appears in t of tl, it is projected. New transformers are allocated to build the projection list.
tl | l |
proj | roj |
Definition at line 730 of file transformer_list.c.
References CONS, copy_transformer(), ENTITY, entity_is_argument_p(), entity_to_old_value(), FOREACH, gen_free_list(), gen_nreverse(), NIL, safe_transformer_projection(), TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
tl | l |
Definition at line 454 of file transformer_list.c.
References CONS, copy_transformer(), ENDP, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by whileloop_to_postcondition().
Returns the list of variables modified by at least one transformer in tl.
tl | l |
Definition at line 753 of file transformer_list.c.
References CONS, ENTITY, FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
transformer transformer_list_to_transformer | ( | list | ltl | ) |
Reduce the transformer list ltl to one transformer using the convex hull operator.
ltl | tl |
Definition at line 434 of file transformer_list.c.
References generic_transformer_list_to_transformer().
Referenced by complete_any_loop_transformer(), complete_repeatloop_transformer(), new_complete_whileloop_transformer(), transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
transformer transformer_list_transitive_closure | ( | list | tfl | ) |
Compute (U tfl)*.
tfl | fl |
Definition at line 1141 of file transformer_list.c.
References transformer_list_generic_transitive_closure().
Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and unstructured_to_flow_insensitive_transformer().
transformer transformer_list_transitive_closure_plus | ( | list | tfl | ) |
Compute (U tfl)+.
tfl | fl |
Definition at line 1147 of file transformer_list.c.
References transformer_list_generic_transitive_closure().
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().
build a sublist sl of the transformer list tl with transformers that modify the value of variable v
tl | l |
Definition at line 771 of file transformer_list.c.
References CONS, entity_is_argument_p(), FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
list two_transformers_to_list | ( | transformer | t1, |
transformer | t2 | ||
) |
Transformer two transformers into a correct transformer list.
Could be generalized to any number of transformers using a varargs... and more thinking.
Two transformers are obtained for loops that may be skipped or entered and for tests whose condition is not statically decidable.
This is a very dangerous step that should not always be taken. It is useful to ease the detection of identity paths, but it looses a lot of information. So almost identity path might simply be better identified elsewhere
t1 | 1 |
t2 | 2 |
Definition at line 316 of file transformer_list.c.
References CONS, free_transformer(), NIL, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().
Referenced by complete_any_loop_transformer_list(), and complete_repeatloop_transformer_list().