PIPS
|
#include <stdlib.h>
#include <stdio.h>
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "ri-util.h"
#include "misc.h"
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "ray_dte.h"
#include "sommet.h"
#include "sg.h"
#include "polyedre.h"
#include "matrice.h"
#include "transformer.h"
Go to the source code of this file.
Functions | |
transformer | transformer_halbwachs_fix_point (transformer tf) |
static void | build_transfer_matrix (matrice *, Pcontrainte, int, Pbase) |
Must be declared explicity to keep a logical order in this C file. More... | |
transformer | transformer_equality_fix_point (transformer tf) |
Let A be the affine loop transfert function. More... | |
void | build_transfer_equations (Pcontrainte leq, Pcontrainte *plteq, Pbase *pb_new) |
bool | transfer_equation_p (Pvecteur eq) |
A transfer equation is an explicit equation giving one new value as a function of old values and a constant term. More... | |
entity | new_value_in_transfer_equation (Pvecteur eq) |
bool | sub_basis_p (Pbase b1, Pbase b2) |
FI: should be moved in base.c. More... | |
void | equations_to_bases (Pcontrainte lteq, Pbase *pb_new, Pbase *pb_old) |
transformer | transformer_pattern_fix_point (transformer tf) |
This fixpoint function was developped to present a talk at FORMA. More... | |
Pvecteur | look_for_the_best_counter (Pcontrainte egs) |
Try to identify a loop counter among the equation egs. More... | |
Psysteme | sc_eliminate_constant_terms (Psysteme sc, Pvecteur v) |
Eliminate all constant terms in sc using v. More... | |
Pcontrainte | constraints_eliminate_constant_terms (Pcontrainte lc, Pvecteur v) |
Psysteme | sc_keep_invariants_only (Psysteme sc) |
This function cannot be moved into the Linear library. More... | |
Pcontrainte | constraints_keep_invariants_only (Pcontrainte lc) |
bool | invariant_vector_p (Pvecteur v) |
A vector (in fact, a constraint) represents an invariant if it is a sum of delta for each variable. More... | |
Psysteme | sc_multiply_constant_terms (Psysteme sc, Variable ik, bool star_p) |
Specific for the derivative fix point: each constant term in the constraints is multiplied by ik which is not in sc's basis, and ik is added to the basis is necessary. More... | |
transformer | transformer_derivative_fix_point (transformer tf) |
Computation of a transitive closure using constraints on the discrete derivative. More... | |
list | transformers_derivative_fix_point (list tl) |
transformer | transformer_basic_fix_point (transformer tf) |
Computation of a fix point: drop all constraints, remember which variables are changed. More... | |
transformer | any_transformer_to_k_closure (transformer t_init, transformer t_enter, transformer t_next, transformer t_body, transformer post_init, int k, bool assume_previous_iteration_p) |
Derived from any_loop_to_k_transformer() More... | |
Variables | |
transformer(* | transformer_fix_point_operator )(transformer) |
transformer package - fix-point or transitive closure computations More... | |
transformer any_transformer_to_k_closure | ( | transformer | t_init, |
transformer | t_enter, | ||
transformer | t_next, | ||
transformer | t_body, | ||
transformer | post_init, | ||
int | k, | ||
bool | assume_previous_iteration_p | ||
) |
Derived from any_loop_to_k_transformer()
The recursive computation of the loop transformer is not performed here.
Complete the body transformer with t_next (t_body is modified by side effects into t_fbody)
Compute the fix point
Compute t_body_star = t_init ; t_enter
and add the continuation condition, pre_iteration improved with knowledge about the body, npre_iteration. Note that pre_iteration would also provide correct results, although less accurate.
FI: this is a very strong normalization
obvious redundancy like 0<=x, x<=y, 0<=y is detected
Integer redundancy elimination is aso used and leads potentially to larger coefficients and ultimately to an accuracy reduction when a convex hull is performed.
Any transformer or other data structure to free?
t_init | _init |
t_enter | _enter |
t_next | _next |
t_body | _body |
post_init | ost_init |
assume_previous_iteration_p | ssume_previous_iteration_p |
Definition at line 1304 of file fix_point.c.
References copy_transformer(), fprintf(), free_transformer(), ifdebug, print_transformer, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_intersect_range_with_domain(), transformer_range(), and transformer_undefined.
Referenced by any_loop_to_k_transformer().
void build_transfer_equations | ( | Pcontrainte | leq, |
Pcontrainte * | plteq, | ||
Pbase * | pb_new | ||
) |
FI: this is the simplest version; It would be possible to build a larger set of transfer equations by adding indirect transfer equations using a new basis till the set is stable, and then by removing equations containing old values which are not defined, again till the result is stable
I guess that these new equations would not change the fix-point and/or the preconditions.
derive the new basis and the old basis
check that the old basis is included in the new basis (else no fix-point!)
Remove equations as long b_old is not included in b_new
could be avoided by using only lteq...
leq | eq |
plteq | lteq |
pb_new | b_new |
Definition at line 433 of file fix_point.c.
References base_contains_variable_p(), base_difference(), base_fprint(), BASE_NULLE, BASE_NULLE_P, base_rm, BASE_UNDEFINED, contrainte_dup(), contrainte_rm, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, egalites_fprint(), eq, equations_to_bases(), external_value_name(), ifdebug, pips_debug, pips_internal_error, sub_basis_p(), Scontrainte::succ, Svecteur::succ, transfer_equation_p(), VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by transformer_equality_fix_point().
|
static |
Must be declared explicity to keep a logical order in this C file.
Also, the matrice type is now obsolete and should not appear in transformer.h. Hence buil_transfer_matrix() must be static.
add the homogeneous coordinate
Definition at line 601 of file fix_point.c.
References ACCESS, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, eq, matrice_new, matrice_nulle(), new_value_entity_p(), new_value_in_transfer_equation(), old_value_to_new_value(), pips_assert, pips_debug, rank_of_variable(), Scontrainte::succ, Svecteur::succ, TCST, VALUE_ONE, value_one_p, value_uminus, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by transformer_equality_fix_point().
Pcontrainte constraints_eliminate_constant_terms | ( | Pcontrainte | lc, |
Pvecteur | v | ||
) |
cv may now be the null vector
lc | c |
Definition at line 865 of file fix_point.c.
References abort, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, TCST, vect_cl(), vect_coeff(), and vect_multiply().
Referenced by sc_eliminate_constant_terms().
Pcontrainte constraints_keep_invariants_only | ( | Pcontrainte | lc | ) |
lc | c |
Definition at line 910 of file fix_point.c.
References contrainte_succ, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, invariant_vector_p(), vect_rm(), and VECTEUR_NUL.
Referenced by sc_keep_invariants_only().
void equations_to_bases | ( | Pcontrainte | lteq, |
Pbase * | pb_new, | ||
Pbase * | pb_old | ||
) |
lteq | teq |
pb_new | b_new |
pb_old | b_old |
Definition at line 660 of file fix_point.c.
References BASE_UNDEFINED, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, eq, new_value_entity_p(), old_value_to_new_value(), Scontrainte::succ, Svecteur::succ, TCST, vect_add_variable(), VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by build_transfer_equations().
A vector (in fact, a constraint) represents an invariant if it is a sum of delta for each variable.
Let di = i::new - i::old. If v = sigma (di) = 0, v can be used to build a loop invariant.
It is assumed that constant terms have been substituted earlier using a loop counter.
OK, you could argue for invariant = false, but this would not help my debugging!
if v_sum is non zero, you might try to bound it wrt the loop precondition?
Definition at line 934 of file fix_point.c.
References bool_to_string(), entity_name, external_value_name(), ifdebug, new_value_entity_p(), old_value_entity_p(), pips_debug, pips_internal_error, TCST, value_to_variable(), vect_add(), vect_add_elem(), vect_fprint(), vect_rm(), VECTEUR_NUL, VECTEUR_NUL_P, vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by constraints_keep_invariants_only().
Pvecteur look_for_the_best_counter | ( | Pcontrainte | egs | ) |
Try to identify a loop counter among the equation egs.
If the transformer has been build naively, a loop counter should have a transformer equation like i::new = i::old + K_i where K_i is a numerical constant.
Since the loop counter is later used to eliminate constant terms in other constraints, variable i with the minimal absolute value K_i shuold be chosen.
egs | gs |
Definition at line 797 of file fix_point.c.
References ABS, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, entity_local_name(), entity_undefined, entity_undefined_p, int, new_value_entity_p(), old_value_entity_p(), pips_internal_error, TCST, value_to_variable(), vect_size(), vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by transformer_pattern_fix_point().
for gcc
eq | q |
Definition at line 570 of file fix_point.c.
References entity_undefined, eq, new_value_entity_p(), pips_assert, Svecteur::succ, TCST, value_mone_p, value_one_p, value_oppose, VALUE_ZERO, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by build_transfer_matrix().
Eliminate all constant terms in sc using v.
No sharing between sc and v is assumed as sc is updated!
This function should be located in Linear/sc
sc | c |
Definition at line 853 of file fix_point.c.
References assert, constraints_eliminate_constant_terms(), TCST, and vect_coeff().
Referenced by transformer_pattern_fix_point().
This function cannot be moved into the Linear library.
It relies on the concepts of old and new values.
It could be improved by using an approximate initial fix-point to evaluate v_sum (see invariant_vector_p) and to degrade equations into inequalities or to relax inequalities.
For instance, p = p + a won't generate an invariant. However, if the lousy fix-point is sufficient to prove a >= 0, it is possible to derive p::new >= p::old. Or even better if a's value turns out to be known.
sc | c |
Definition at line 902 of file fix_point.c.
References constraints_keep_invariants_only().
Referenced by transformer_pattern_fix_point().
Specific for the derivative fix point: each constant term in the constraints is multiplied by ik which is not in sc's basis, and ik is added to the basis is necessary.
This possible only if ik is positive. Constraint ik>=0 is added if star_p is true because the function is used to compute T*. Else, contraint ik>=1 is added because the function is used to compute T+.
Also used in transformer_list.c
add constraint ik >= 0 to compute T*. Would be ik>=1 if T+ were sought.
sc | c |
ik | k |
star_p | tar_p |
Definition at line 1013 of file fix_point.c.
References Ssysteme::base, base_add_dimension, base_contains_variable_p(), contrainte_make(), CONTRAINTE_UNDEFINED_P, Ssysteme::dimension, Ssysteme::egalites, Ssysteme::inegalites, pips_assert, sc_add_inegalite(), Scontrainte::succ, Svecteur::succ, TCST, VALUE_MONE, VALUE_ONE, var_of, vect_add_elem(), vect_new(), Scontrainte::vecteur, and VECTEUR_NUL_P.
Referenced by transformer_derivative_fix_point(), and transformer_list_generic_transitive_closure().
FI: should be moved in base.c.
sub_basis_p(Pbase b1, Pbase b2): check if b1 is included in b2
b1 | 1 |
b2 | 2 |
Definition at line 648 of file fix_point.c.
References b1, b2, base_contains_variable_p(), Svecteur::succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by build_transfer_equations().
A transfer equation is an explicit equation giving one new value as a function of old values and a constant term.
Because we are using diophantine equations, the coefficient of the new value must one or minus one. We assume that the equation is reduced (i.e. gcd(coeffs) == 1).
FI: Non-unary coefficients may appear because equations were combined, for instance by a previous internal fix-point as in KINETI of mdg-fi.f (Perfect Club). Maybe, something could be done for these nested fix-points.
eq | q |
Definition at line 552 of file fix_point.c.
References eq, new_value_entity_p(), Svecteur::succ, TCST, value_mone_p, value_one_p, VALUE_ZERO, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by build_transfer_equations().
transformer transformer_basic_fix_point | ( | transformer | tf | ) |
Computation of a fix point: drop all constraints, remember which variables are changed.
Except if the transformer is syntactically empty since its fix point is easy to compute. Without normalization, mathematically empty transformers are lost.
get rid of equalities and inequalities but keep the basis
tf | f |
Definition at line 1280 of file fix_point.c.
References CONTRAINTE_UNDEFINED, contraintes_free(), copy_transformer(), eq, predicate_system, transformer_empty_p(), and transformer_relation.
Referenced by select_fix_point_operator().
transformer transformer_derivative_fix_point | ( | transformer | tf | ) |
Computation of a transitive closure using constraints on the discrete derivative.
See http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Implicit equations, n::new - n::old = 0, are not added. Instead, invariant constraints in tf are obtained by projection and added.
Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old
I tried to use the standard procedure but arguments are not removed when the transformer tf is not feasible. Since we compute the * fix point and not the + fix point, the fix point is the identity.
sc is going to be modified and destroyed and eventually replaced in fix_tf
Do not handle variable which do not appear explicitly in constraints!
initial and final basis
basis vector
basis of difference vectors
Compute constraints with difference equations
Only generate difference equations if the old value is used
Project all variables but differences to get T'
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 fix_tf
Add constraints about invariant variables. This could be avoided if implicit equalities were added before the derivative are processed: each invariant variable would generate an implicit null difference.
Such invariant constraints do not exist in general. We have them when array references are trusted.
This is wrong because we compute f* and not f+ and this is not true for the initial store.
What can be done instead is to refine fix_tf as :
dom(tf) U tf(fix_tf(dom(tf)))
But this fails because tf loops back to the beginning of the next iteration. Hence, the domain of tf implies two iterations instead of one. For instance, "i<n" becomes "i<=n-2" for a while loop such as "while(i<n) i++;".
So this refinement should be performed at a higher level where t_init and t_enter are know... so as to have:
dom_tf = transformer_range(t_enter(t_init)).
That's all!
tf | f |
Definition at line 1067 of file fix_point.c.
References Ssysteme::base, base_add_variable(), base_dup(), BASE_NULLE, BASE_NULLE_P, base_remove_variable(), base_rm, contrainte_make(), CONTRAINTE_UNDEFINED, Ssysteme::dimension, entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), fprint_transformer(), free_transformer(), ifdebug, make_local_temporary_integer_value_entity(), old_value_entity_p(), pips_debug, predicate_system, sc_equation_add(), sc_fprint(), sc_multiply_constant_terms(), sc_to_minimal_basis(), Svecteur::succ, TCST, transformer_consistency_p(), transformer_dup(), transformer_empty_p(), transformer_identity(), transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), vect_size(), VECTEUR_NUL, and vecteur_var.
Referenced by invariant_wrt_transformer(), select_fix_point_operator(), and transformers_derivative_fix_point().
transformer transformer_equality_fix_point | ( | transformer | tf | ) |
Let A be the affine loop transfert function.
The affine transfer fix-point T is such that T(A-I) = 0
T A = 0 also gives a fix-point when merged with the initial state. It can only be used to compute preconditions.
Algorithm (let H be A's Smith normal form):
A = A - I (if necessary) H = P A Q A = P^-1 H Q^-1 T A = T P^-1 H Q^-1 = 0 T P^-1 H = 0 (by multipliying by Q)
Soit X t.q. X H = 0 A basis for all solutions is given by X chosen such that X is a rectangular matrix (0 I) selecting the zero submatrix of H
Note: I (FI) believe this functions is wrong because it does not return the appropriate arguments. The fix point transformer should modify as many variables as the input tf. A new basis should not be recomputed according to the transition matrix. This problem seems to be fixed in the callers, see loop_to_transformer() and whileloop_to_transformer().
result
do not modify an input argument
number of transfer equalities plus the homogeneous constraint which states that 1 == 1
use a matrix a to store these equalities in a dense form
Pbase t = BASE_UNDEFINED;
If the input transformer is not feasible, so is not its fixpoint because the number of iterations may be zero which implies identity.
fix_tf = transformer_identity();
find or build explicit transfer equations: v::new = f(v1::old, v2::old,...) and the corresponding sub-basis
FI: for each constant variable, whose constance is implictly implied by not having it in the argument field, an equation should be added...
lieq = build_implicit_equalities(tf); lieq->succ = leq; leq = lieq;
build matrix a from lteq and b_new: this should be moved in a function
Subtract the identity matrix
Compute the Smith normal form: H = P A Q
Find out the number of invariants n_inv
Convert p's last n_inv rows into constraints
FI: maybe I should retrieve fix_tf system...
is it a non-trivial invariant?
Set fix_tf's argument list
Fix the basis and the dimension
get rid of dense matrices
tf | f |
Definition at line 266 of file fix_point.c.
References ACCESS, base_dimension, base_dup(), BASE_NULLE, build_transfer_equations(), build_transfer_matrix(), contrainte_make(), CONTRAINTE_UNDEFINED, DENOMINATOR, dup_arguments(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, make_predicate(), matrice_fprint(), matrice_free, matrice_new, matrice_smith(), MATRICE_UNDEFINED, new_value_to_old_value(), pips_assert, pips_debug, predicate_system, sc_add_egalite(), sc_creer_base(), sc_fprint(), sc_new(), transformer_arguments, transformer_dup(), transformer_empty_p(), transformer_identity(), transformer_relation, value_notzero_p, VALUE_ONE, value_substract, value_uminus, value_zero_p, variable_of_rank(), vect_add_elem(), and VECTEUR_NUL.
Referenced by select_fix_point_operator(), and standard_whileloop_to_transformer().
transformer transformer_halbwachs_fix_point | ( | transformer | tf | ) |
THIS FUNCTION WAS NEVER CORRECT AND HAS NOT BEEN REWRITTEN FOR THE NEW VALUE PACKAGE
simple fix-point for inductive variables: loop bounds are ignored
cons * args = effects_to_arguments(e);
tf1: transformer for one loop iteration
tf2: transformer for two loop iterations
tf12: transformer for one or two loop iterations
tf23: transformer for two or three loop iterations
tf_star: transformer for one, two, three,... loop iterations should be called tf_plus by I do not use the one_trip flag
preserve transformer of loop body s
temporarily commented out
duplicate tf1 because transformer_combine might not be able to use twice the same argument
input/output relation for one or two iteration of the loop
apply one iteration on tf12
fix-point
should be done again based on Chenikova
tf_star = transformer_fix_point(tf12, tf23);
free useless transformers
tf | f |
Definition at line 143 of file fix_point.c.
References fprintf(), ifdebug, pips_internal_error, print_transformer, transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), and transformer_undefined.
Referenced by standard_whileloop_to_transformer().
transformer transformer_pattern_fix_point | ( | transformer | tf | ) |
This fixpoint function was developped to present a talk at FORMA.
I used examples published by Pugh and I realized that the fixpoint constraints were obvious in the loop body transformer. You just had to identify them. This is not a clever algorithm. It certainly would not resist any messing up with the constraints, i.e. a change of basis. But it provides very good result for a class of applications.
Algorithm:
Let d_i = i::new - i::old. An invariant constraint is a sum of d_i which is equal to zero or greater than zero. Such a constraint is its own fixpoint: if you combine it with itself after renaming i::new as i::int on one hand and i::old as i::int on the other, the global sum for and equation or its sign for an inequality is unchanged.
result
Look for the best loop counter: the smallest increment is chosen
eliminate sharing between v_inc and fix_sc
Replace constant terms in equalities and inequalities by loop counter differences
Remove all constraints to build the invariant transformer
tf | f |
Definition at line 709 of file fix_point.c.
References CONTRAINTE_UNDEFINED, contraintes_free(), external_value_name(), fprint_transformer(), ifdebug, look_for_the_best_counter(), pips_debug, predicate_system, sc_elim_redund(), sc_eliminate_constant_terms(), sc_fprint(), sc_keep_invariants_only(), transformer_dup(), transformer_relation, vect_dup(), vect_fprint(), VECTEUR_UNDEFINED, and VECTEUR_UNDEFINED_P.
Referenced by select_fix_point_operator().
tl | l |
Definition at line 1262 of file fix_point.c.
References CONS, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_derivative_fix_point().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
transformer(* transformer_fix_point_operator) (transformer) | ( | transformer | ) |
transformer package - fix-point or transitive closure computations
Interface between the untyped database manager and clean code and between pipsmake and clean code.
Several algorithms are available:
a fix point algorithm combining the last two algorithms above. This algorithm adds difference variables d_i = i::new - i::old for each variable i. All non d_i variables are thn projected. If the projection algorithm is sophisticated enough, the projection ordering will be "good". Left over inequalities are invariant or useless. Let N be the strictly positive iteration count:
sum ai di <= -k implies N sum ai di <= -Nk <= -k (OK)
sum ai di <= k implies N sum ai di <= Nk <= infinity (useless unless k == 0)
Left over equations can stay equations if the constant term is 0, or be degraded into an inequation if not. The nw inequation depends on the sign of the constant:
sum ai di == -k implies N sum ai di == -Nk <= -k
sum ai di == k implies N sum ai di == Nk >= k
sum ai di == 0 implies N sum ai di == 0
In a second step, the constant terms are eliminated to obtain new constraints leading to new invariants, using the same rules as above.
This algorithm was designed for while loops such as:
WHILE( I > 0 ) J = J + I I = I - 1
to find as loop transformer T(I,J) {I::new <= I::old - 1, J::new >= J::old + 1, I::new+J::new >= I::old + J::old}
Note that the second constraint is redundant with the other two, but the last one cannot be found before the constant terms are eliminated.
The current algorithm, the derivative version, is published and describes in NSAD 2010, A/426/CRI. See also A/429/CRI: http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Francois Irigoin, 21 April 1990 The fixpoint operator is selected according to properties
Definition at line 114 of file fix_point.c.
Referenced by select_fix_point_operator(), and standard_whileloop_to_transformer().