27 #include "pips_config.h"
232 fprintf(stderr,
"post_init:\n");
259 t_next_star = (* transformer_fix_point_operator)(t_next);
271 pre_body = pre_body_2;
309 fprintf(stderr,
"t_body_star:\n");
491 #define IS_LOWER_BOUND 0
492 #define IS_UPPER_BOUND 1
510 pips_debug(8,
"begin with transformer tf=%p\n", tf);
513 pips_debug(8,
"and precondition pre=%p\n", pre);
520 if(incr_lb==incr_ub) {
522 user_error(
"add_loop_skip_condition",
"Illegal null loop increment\n");
527 else if(incr_lb>=1) {
530 else if(incr_ub<=-1) {
558 debug(8,
"add_loop_skip_condition",
"Skip condition:\n");
563 pips_debug(8,
"Non-analyzed variable in loop bound(s)\n");
567 pips_debug(8,
"increment sign unknown or non-affine bound\n");
705 pips_assert(
"The resulting transformer is consistent",
736 if(incr_lb==incr_ub) {
743 else if(incr_lb>=1) {
746 else if(incr_ub<=-1) {
901 pips_debug(8,
"give up because %s has no values:\n",
942 pips_debug(8,
"post after index incrementation:\n");
948 if(lb_inc >= 1 || ub_inc <= -1) {
961 if(lb_inc==ub_inc &&
ABS(lb_inc)==1) {
979 else if(ub_inc<=-1) {
1000 pips_debug(8,
"post with exit conditions:\n");
1006 "post is unchanged because the increment or the upper bound"
1007 " reference unanalyzed variables\n");
1012 "post is unchanged because the increment sign is unknown\n");
1017 "post is unchanged because the upper bound is not affine\n");
1030 bool dead_loop_p =
false;
1107 sc = sc_projection_by_eq(sc,
eq, (
Variable) i_init);
1108 b_tmp = sc_base(sc);
1149 pips_assert(
"Transformer tf is consistent before update",
1164 Pbase b = sc_base(sc);
1183 Pbase b = sc_base(sc);
1193 pips_assert(
"Transformer tf is consistent after update",
1235 if(inc_lb>0 || inc_ub<0) {
1337 pips_debug(8,
"begin with precondition pre=%p\n", pre);
1356 pips_debug(8,
"body precondition preb=%p\n", preb);
1365 pips_debug(8,
"body transformer tfb=%p\n", tfb);
1371 tf = (* transformer_fix_point_operator)(tfb);
1376 pips_debug(8,
"intermediate fix-point tf=\n");
1411 (void)
fprintf(stderr,
"%s: %s\n",
"loop_to_transformer",
1456 if(il==iu && il==0) {
1462 else if(il>0||iu<0) {
1628 fprintf(stderr,
"t_body_star:\n");
1630 fprintf(stderr,
"t_body:inc\n");
1817 ct_body, t_inc, t_exit);
1937 pips_debug(8,
"begin with loop precondition\n");
1980 pips_debug(8,
"entered loop transformer t_enter=\n");
2005 pips_debug(8,
"entered and exited loop transformer t_enter=\n");
2022 pips_debug(8,
"skipped loop transformer t_skip=\n");
2053 pips_debug(8,
"full refined loop transformer tf=\n");
2074 pips_debug(8,
"begin with loop precondition\n");
2109 pips_debug(8,
"entered loop transformer t_enter=\n");
2134 pips_debug(8,
"entered and exited loop transformer t_enter=\n");
2149 pips_debug(8,
"skipped loop transformer t_skip=\n");
2174 pips_debug(8,
"full refined loop transformer tf=\n");
2226 pips_debug(8,
"begin with whileloop precondition\n");
2229 pips_debug(8,
"and whileloop transformer:\n");
2258 pips_debug(8,
"entered loop transformer t_enter=\n");
2266 pips_debug(8,
"entered and exited loop transformer t_enter=\n");
2278 pips_debug(8,
"skipped loop transformer t_skip=\n");
2301 pips_debug(8,
"full refined loop transformer tf=\n");
2339 pips_debug(5,
"Variables eliminated from the preconditions"
2340 " because they are modified by tf:");
2348 pips_debug(5,
"Variables eliminated from the preconditions"
2349 " because they are linked to the module entry point:");
2357 pips_debug(5,
"Values which should be eliminated from the preconditions:");
2365 pips_debug(5,
"Values which can be eliminated from the preconditions:");
2379 pips_assert(
"Conditional loop body transformer is consistent",
2385 new_tf = (* transformer_fix_point_operator)(tfb);
2406 pips_assert(
"To shut up gcc", wl==wl && pre==pre);
2424 pips_debug(5,
"Begin with body transformer:\n");
2442 pips_debug(5,
"End with new body transformer:\n");
2493 pips_debug(8,
"Precondition for loop body pre_n=\n");
2524 transformer ftf = (* transformer_fix_point_operator)(tfb);
2547 pips_debug(8,
"intermediate fix-point tf=\n");
2575 (void)
fprintf(stderr,
"%s: %s\n",
"standard_whileloop_to_transformer",
2920 pips_debug(8,
"The loop is never executed\n");
2932 debug(8,
"loop_to_postcondition",
"The loop certainly is executed\n");
2976 pips_debug(8,
"The loop may be executed or not\n");
2995 (void)
fprintf(stderr,
"%s: %s\n",
"[loop_to_postcondition]",
2996 "Never executed: post_ne %p =");
2998 (void)
fprintf(stderr,
"%s: %s\n",
"[loop_to_postcondition]",
2999 "Always executed: post_al %p = ");
3015 (void)
fprintf(stderr,
"%s: %s\n",
"[loop_to_postcondition]",
3057 pips_debug(8,
"The loop is never executed\n");
3060 pips_assert(
"The body total precondition is consistent",
3083 ltf = (* transformer_fix_point_operator)(btf);
3090 pips_assert(
"The body total precondition is consistent",
3104 pips_debug(8,
"The loop certainly is executed\n");
3108 pips_debug(8,
"The loop may be executed or not\n");
3117 (void)
fprintf(stderr,
"%s: %s\n",
"[loop_to_postcondition]",
3118 "Never executed: t_pre_ne =");
3120 (void)
fprintf(stderr,
"%s: %s\n",
"[loop_to_postcondition]",
3121 "Always executed: post_al =");
3159 pips_debug(8,
"The loop is never executed\n");
3240 pips_debug(8,
"The loop may be executed and preconditions must"
3241 " be propagated in the loop body\n");
3360 pips_debug(8,
"The loop certainly is executed.\n");
3399 pips_debug(8,
"The loop may be executed or not\n");
3449 pips_assert(
"not implemented yet",
false && t_post==t_post);
3465 pips_debug(8,
"The loop is never executed\n");
3481 pips_debug(8,
"The loop certainly is executed\n");
3502 pips_debug(8,
"The loop may be executed or not\n");
int get_int_property(const string)
void free_effect(effect p)
cell make_cell(enum cell_utype tag, void *val)
approximation make_approximation_exact(void)
effect make_effect(cell a1, action a2, approximation a3, descriptor a4)
descriptor make_descriptor_none(void)
void free_transformer(transformer p)
void free_reference(reference p)
reference make_reference(entity a1, list a2)
bool transformer_consistent_p(transformer p)
void free_expression(expression p)
void free_predicate(predicate p)
transformer copy_transformer(transformer p)
TRANSFORMER.
preference make_preference(reference a1)
struct _newgen_struct_entity_ * entity
cons * arguments_union(cons *a1, cons *a2)
cons * arguments_union(cons * a1, cons * a2): returns a = union(a1, a2) where a1 and a2 are lists of ...
cons * dup_arguments(cons *args)
cons * arguments_add_entity(cons *a, entity e)
cons * arguments_difference(cons *a1, cons *a2)
set difference: a1 - a2 ; similar to set intersection
void const char const char const int
#define ABS(x)
was: #define value_mult(v,w) value_direct_multiply(v,w) #define value_product(v,w) value_direct_produ...
Pbase base_add_variable(Pbase b, Variable var)
Pbase base_add_variable(Pbase b, Variable v): add variable v as a new dimension to basis b at the end...
Pbase make_base_from_vect(Pvecteur pv)
Pbase base_union(Pbase b1, Pbase b2)
Pbase base_union(Pbase b1, Pbase b2): compute a new basis containing all elements of b1 and all eleme...
transformer transformer_add_inequality_with_linear_term(transformer tf, entity v, entity x, int a, bool less_than_p)
Add the inequality v <= a x or v >= a x.
transformer transformer_dup(transformer t_in)
transformer package - basic routines
void transformer_free(transformer t)
transformer transformer_inequality_add(transformer tf, Pvecteur i)
transformer transformer_add_variable_incrementation(transformer t, entity i, Pvecteur incr)
transformer transformer_add_loop_index(transformer t, entity i, Pvecteur incr): add the index increme...
transformer transformer_equality_add(transformer tf, Pvecteur i)
transformer empty_transformer(transformer t)
Do not allocate an empty transformer, but transform an allocated transformer into an empty_transforme...
transformer transformer_identity()
Allocate an identity transformer.
bool transformer_consistency_p(transformer t)
FI: I do not know if this procedure should always return or fail when an inconsistency is found.
void free_transformers(transformer t,...)
transformer transformer_empty()
Allocate an empty transformer.
list transformer_projectable_values(transformer tf)
bool transformer_internal_consistency_p(transformer t)
Same as above but equivalenced variables should not appear in the argument list or in the predicate b...
transformer transformer_add_inequality(transformer tf, entity v1, entity v2, bool strict_p)
Add the equality v1 <= v2 or v1 < v2.
#define CONTRAINTE_UNDEFINED
Pcontrainte contrainte_make(Pvecteur pv)
Pcontrainte contrainte_make(Pvecteur pv): allocation et initialisation d'une contrainte avec un vecte...
transformer transformer_equality_fix_point(transformer)
Let A be the affine loop transfert function.
transformer(* transformer_fix_point_operator)(transformer)
Interface between the untyped database manager and clean code and between pipsmake and clean code.
list load_cumulated_rw_effects_list(statement)
list expression_to_proper_constant_path_effects(expression)
action make_action_write_memory(void)
To ease the extension of action with action_kind.
#define cell_preference(x)
#define newgen_Psysteme(p)
bool get_bool_property(const string)
FC 2015-07-20: yuk, moved out to prevent an include cycle dependency include "properties....
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()
transformer transformer_halbwachs_fix_point(transformer tf)
void gen_full_free_list(list l)
void gen_list_and(list *a, const list b)
Compute A = A inter B: complexity in O(n2)
#define NIL
The empty list (nil in Lisp)
size_t gen_length(const list l)
void gen_list_and_not(list *a, const list b)
Compute A = A inter non B:
#define CONS(_t_, _i_, _l_)
List element cell constructor (insert an element at the beginning of a list)
list gen_nconc(list cp1, list cp2)
physically concatenates CP1 and CP2 but do not duplicates the elements
#define CAR(pcons)
Get the value of the first element of a list.
void gen_free_list(list l)
free the spine of the list
#define list_undefined
Undefined list definition :-)
list gen_full_copy_list(list l)
Copy a list structure with element copy.
bool statement_whileloop_p(statement)
bool statement_loop_p(statement)
void vect_fprint(FILE *f, Pvecteur v, get_variable_name_t variable_name)
void vect_fprint(FILE * f, Pvecteur v, char * (*variable_name)()): impression d'un vecteur creux v su...
#define pips_debug
these macros use the GNU extensions that allow variadic macros, including with an empty list.
#define pips_user_warning
#define pips_assert(what, predicate)
common macros, two flavors depending on NDEBUG
#define pips_internal_error
#define user_error(fn,...)
void debug(const int the_expected_debug_level, const char *calling_function_name, const char *a_message_format,...)
ARARGS0.
void print_arguments(list args)
Pvecteur expression_to_affine(expression e)
#define print_transformer(t)
#define SEMANTICS_FIX_POINT
#define pips_flag_p(p)
for upwards compatibility with Francois's modified version
#define SEMANTICS_INEQUALITY_INVARIANT
#define NORMALIZE_EXPRESSION(e)
const char * entity_local_name(entity e)
entity_local_name modified so that it does not core when used in vect_fprint, since someone thought t...
static int init
Maximal value set for Fortran 77.
bool positive_expression_p(expression e)
Use constants and type information to decide if the value of sigma(e) is always positive,...
bool negative_expression_p(expression e)
Use constants and type information to decide if the value of sigma(e) is always negative,...
expression entity_to_expression(entity e)
if v is a constant, returns a constant call.
bool scalar_integer_type_p(type)
#define transformer_undefined
#define transformer_undefined_p(x)
#define normalized_linear_p(x)
#define forloop_initialization(x)
#define TRANSFORMER(x)
TRANSFORMER.
#define forloop_increment(x)
#define instruction_loop(x)
#define whileloop_evaluation(x)
#define range_increment(x)
#define transformer_relation(x)
#define predicate_undefined
#define transformer_arguments(x)
#define preference_reference(x)
#define instruction_whileloop(x)
#define predicate_system_(x)
#define whileloop_body(x)
#define statement_instruction(x)
#define forloop_condition(x)
#define whileloop_condition(x)
#define normalized_linear(x)
#define evaluation_before_p(x)
#define predicate_system(x)
transformer statement_to_postcondition(transformer, statement)
end of the non recursive section
transformer statement_to_total_precondition(transformer, statement)
semantical analysis
struct Ssysteme * Psysteme
Psysteme sc_make(Pcontrainte leg, Pcontrainte lineg)
Psysteme sc_make(Pcontrainte leg, Pcontrainte lineg): allocation et initialisation d'un systeme d'equ...
Pcontrainte eq
element du vecteur colonne du systeme donne par l'analyse
Psysteme sc_append(Psysteme s1, Psysteme s2)
Psysteme sc_append(Psysteme s1, Psysteme s2): calcul de l'intersection des polyedres definis par s1 e...
void sc_fprint(FILE *fp, Psysteme ps, get_variable_name_t nom_var)
void sc_fprint(FILE * f, Psysteme ps, char * (*nom_var)()): cette fonction imprime dans le fichier po...
int fprintf()
test sc_min : ce test s'appelle par : programme fichier1.data fichier2.data ...
void vect_chg_sgn(Pvecteur v)
void vect_chg_sgn(Pvecteur v): multiplie v par -1
Pvecteur vect_multiply(Pvecteur v, Value x)
Pvecteur vect_multiply(Pvecteur v, Value x): multiplication du vecteur v par le scalaire x,...
transformer safe_integer_expression_to_transformer(entity v, expression expr, transformer pre, bool is_internal)
Always return a defined transformer, using effects in case a more precise analysis fails.
transformer affine_increment_to_transformer(entity e, Pvecteur a)
transformer safe_any_expression_to_transformer(entity v, expression expr, transformer pre, bool is_internal)
Always return a usable transformer.
bool false_condition_wrt_precondition_p(expression c, transformer pre)
transformer any_expression_to_transformer(entity v, expression expr, transformer pre, bool is_internal)
A set of functions to compute the transformer associated to an expression evaluated in a given contex...
transformer precondition_add_condition_information(transformer pre, expression c, transformer context, bool veracity)
context might be derivable from pre as transformer_range(pre) but this is sometimes very computationa...
transformer transformer_add_condition_information(transformer pre, expression c, transformer context, bool veracity)
transformer safe_expression_to_transformer(expression exp, transformer pre)
bool true_condition_wrt_precondition_p(expression c, transformer pre)
transformer condition_to_transformer(expression cond, transformer pre, bool veracity)
To capture side effects and to add C twist for numerical conditions.
static transformer loop_body_transformer_add_entry_and_iteration_information(transformer tfb, transformer pre)
FI: I do not have one test case to show that this function is of some use.
transformer loop_to_continue_transformer(loop l, transformer pre)
transformer loop_to_initialization_transformer(loop l, transformer pre)
Transformer expression the loop initialization.
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
transformer old_complete_whileloop_transformer(transformer ltf, transformer pre, whileloop l)
transformer whileloop_to_total_precondition(transformer t_post, whileloop l, transformer tf, transformer context)
transformer standard_whileloop_to_transformer(whileloop l, transformer pre, list e)
This function computes the effect of K loop iteration, with K positive.
static transformer add_good_loop_conditions(transformer pre, loop l)
transformer transformer_add_loop_index_initialization(transformer tf, loop l, transformer pre)
The loop initialization is performed before tf.
transformer repeatloop_to_transformer(whileloop wl, transformer pre, list wlel)
effects of whileloop wl
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.
transformer whileloop_to_postcondition(transformer pre, whileloop l, transformer tf)
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)
static transformer __attribute__((unused))
NOT USED.
transformer repeatloop_to_postcondition(transformer pre, whileloop wl, transformer t_body_star)
list complete_repeatloop_transformer_list(transformer t_body_star, transformer __attribute__((unused)) pre, whileloop wl)
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 ki...
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,...
transformer loop_bound_evaluation_to_transformer(loop l, transformer pre)
Side effects in loop bounds and increment are taken into account.
static transformer add_loop_index_initialization(transformer tf, loop l, transformer pre)
Always returns newly allocated memory.
static transformer recompute_loop_transformer(loop l, transformer pre)
Recompute a fixpoint conditionnally to a valid precondition for all iterations.
transformer whileloop_to_transformer(whileloop l, transformer pre, list e)
effects of whileloop l
list complete_loop_transformer_list(transformer ltf, transformer pre, loop l)
list complete_forloop_transformer_list(transformer t_body_star, transformer pre, forloop fl)
transformer complete_forloop_transformer(transformer t_body_star, transformer pre, forloop fl)
transformer complete_whileloop_transformer(transformer ltf, transformer pre, whileloop wl)
FI: I'm not sure this function is useful.
transformer forloop_to_postcondition(transformer pre, forloop fl, transformer t_body_star)
transformer forloop_to_transformer(forloop fl, transformer pre, list flel)
effects of forloop fl
transformer any_loop_to_transformer(transformer t_init, transformer t_enter, transformer t_next, statement body, list __attribute__((unused)) lel, transformer post_init)
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...
transformer loop_to_postcondition(transformer pre, loop l, transformer tf)
transformer new_whileloop_to_transformer(whileloop wl, transformer pre, list wlel)
effects of whileloop wl
transformer new_whileloop_to_k_transformer(whileloop wl, transformer pre, list wlel, int k)
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 ne...
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 com...
transformer transformer_add_loop_index_incrementation(transformer tf, loop l, transformer pre)
list loop_to_transformer_list(loop l __attribute__((unused)), transformer pre __attribute__((unused)), list e __attribute__((unused)))
list complete_whileloop_transformer_list(transformer ltf, transformer pre, whileloop wl)
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
transformer precondition_filter_old_values(transformer pre)
bool simple_dead_loop_p(expression lower, expression upper)
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.
transformer whileloop_to_k_transformer(whileloop l, transformer pre, list e, int k)
static transformer add_affine_bound_conditions(transformer pre, entity index, Pvecteur v_bound, bool lower_or_upper, transformer tfb)
FI: could be moved somewhere else, e.g.
transformer add_loop_index_exit_value(transformer post, loop l, transformer pre)
The exit value is known if.
list forloop_to_transformer_list(forloop l __attribute__((unused)), transformer pre __attribute__((unused)), list e __attribute__((unused)))
transformer loop_to_total_precondition(transformer t_post, loop l, transformer tf, transformer context)
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.
transformer add_loop_skip_condition(transformer tf, loop l, transformer pre)
tf and pre are a unique data structure when preconditions are computed
static transformer add_index_bound_conditions(transformer pre, entity index, expression bound, int lower_or_upper, transformer tfb)
Side effect on pre.
transformer complete_repeatloop_transformer(transformer t_body_star, transformer pre, whileloop wl)
transformer add_index_range_conditions(transformer pre, entity i, range r, transformer tfb)
bool value_mappings_compatible_vector_p(Pvecteur iv)
transform a vector based on variable entities into a vector based on new value entities when possible...
list variables_to_values(list list_mod)
list variables_to_old_values(list list_mod)
void integer_expression_and_precondition_to_integer_interval(expression, transformer, int *, int *)
Could be used for bool expressions too? Extended to any kind of expression?
bool non_empty_range_wrt_precondition_p(range, transformer)
bool empty_range_wrt_precondition_p(range, transformer)
A range cannot be tested exactly wrt a precondition You can try to prove that it is empty or you can ...
transformer load_statement_transformer(statement)
void expression_and_precondition_to_integer_interval(expression, transformer, int *, int *)
Evaluate expression e in context p, assuming that e is an integer expression.
bool condition_true_wrt_precondition_p(expression, transformer)
A condition cannot be tested exactly wrt a precondition You can try to prove that it is always true (...
bool condition_false_wrt_precondition_p(expression, transformer)
le type des coefficients dans les vecteurs: Value est defini dans le package arithmetique
The structure used to build lists in NewGen.
#define TCST
VARIABLE REPRESENTANT LE TERME CONSTANT.
#define VECTEUR_UNDEFINED
char *(* get_variable_name_t)(Variable)
struct Svecteur * Pvecteur
void * Variable
arithmetique is a requirement for vecteur, but I do not want to inforce it in all pips files....
#define base_dimension(b)
#define VECTEUR_UNDEFINED_P(v)
Pvecteur vect_dup(Pvecteur v_in)
Pvecteur vect_dup(Pvecteur v_in): duplication du vecteur v_in; allocation de et copie dans v_out;.
Pvecteur vect_new(Variable var, Value coeff)
Pvecteur vect_new(Variable var,Value coeff): allocation d'un vecteur colineaire au vecteur de base va...
void vect_rm(Pvecteur v)
void vect_rm(Pvecteur v): desallocation des couples de v;
Pvecteur vect_substract(Pvecteur v1, Pvecteur v2)
Pvecteur vect_substract(Pvecteur v1, Pvecteur v2): allocation d'un vecteur v dont la valeur est la di...
Pvecteur vect_cl(Pvecteur v, Value lambda, Pvecteur u)
void vect_add_elem(Pvecteur *pvect, Variable var, Value val)
void vect_add_elem(Pvecteur * pvect, Variable var, Value val): addition d'un vecteur colineaire au ve...