loop.c File Reference

#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"

Include dependency graph for loop.c:

Go to the source code of this file.

Macros
#define	IS_LOWER_BOUND   0
#define	IS_UPPER_BOUND   1

Functions
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. More...
transformer	any_loop_to_transformer (transformer t_init, transformer t_enter, transformer t_next, statement body, list __attribute__((unused)) lel, transformer post_init)
transformer	forloop_to_transformer (forloop fl, transformer pre, list flel)
	effects of forloop fl More...
list	forloop_to_transformer_list (forloop l __attribute__((unused)), transformer pre __attribute__((unused)), list e __attribute__((unused)))
transformer	new_whileloop_to_transformer (whileloop wl, transformer pre, list wlel)
	effects of whileloop wl More...
transformer	new_whileloop_to_k_transformer (whileloop wl, transformer pre, list wlel, int k)
transformer	repeatloop_to_transformer (whileloop wl, transformer pre, list wlel)
	effects of whileloop wl More...
transformer	add_loop_skip_condition (transformer tf, loop l, transformer pre)
	tf and pre are a unique data structure when preconditions are computed More...
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. More...
static transformer	add_index_bound_conditions (transformer pre, entity index, expression bound, int lower_or_upper, transformer tfb)
	Side effect on pre. More...
transformer	add_index_range_conditions (transformer pre, entity i, range r, transformer tfb)
static transformer	add_good_loop_conditions (transformer pre, loop l)
static transformer	add_loop_index_initialization (transformer tf, loop l, transformer pre)
	Always returns newly allocated memory. More...
transformer	add_loop_index_exit_value (transformer post, loop l, transformer pre)
	The exit value is known if. More...
bool	simple_dead_loop_p (expression lower, expression upper)
transformer	precondition_filter_old_values (transformer pre)
transformer	transformer_add_loop_index_initialization (transformer tf, loop l, transformer pre)
	The loop initialization is performed before tf. More...
transformer	transformer_add_loop_index_incrementation (transformer tf, loop l, transformer pre)
transformer	loop_bound_evaluation_to_transformer (loop l, transformer pre)
	Side effects in loop bounds and increment are taken into account. More...
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. More...
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. More...
list	loop_to_transformer_list (loop l __attribute__((unused)), transformer pre __attribute__((unused)), list e __attribute__((unused)))
transformer	loop_to_initialization_transformer (loop l, transformer pre)
	Transformer expression the loop initialization. More...
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. More...
transformer	loop_to_continue_transformer (loop l, transformer pre)
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. More...
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. More...
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. More...
transformer	complete_forloop_transformer (transformer t_body_star, transformer pre, forloop fl)
list	complete_forloop_transformer_list (transformer t_body_star, transformer pre, forloop fl)
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 More...
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 More...
list	complete_repeatloop_transformer_list (transformer t_body_star, transformer __attribute__((unused)) pre, whileloop wl)
transformer	complete_repeatloop_transformer (transformer t_body_star, transformer pre, whileloop wl)
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. More...
list	complete_loop_transformer_list (transformer ltf, transformer pre, loop l)
transformer	complete_whileloop_transformer (transformer ltf, transformer pre, whileloop wl)
	FI: I'm not sure this function is useful. More...
list	complete_whileloop_transformer_list (transformer ltf, transformer pre, whileloop wl)
transformer	old_complete_whileloop_transformer (transformer ltf, transformer pre, whileloop l)
static transformer	recompute_loop_transformer (loop l, transformer pre)
	Recompute a fixpoint conditionnally to a valid precondition for all iterations. More...
static transformer	__attribute__ ((unused))
	NOT USED. More...
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. More...
transformer	standard_whileloop_to_transformer (whileloop l, transformer pre, list e)
	This function computes the effect of K loop iteration, with K positive. More...
transformer	whileloop_to_transformer (whileloop l, transformer pre, list e)
	effects of whileloop l More...
transformer	whileloop_to_k_transformer (whileloop l, transformer pre, list e, int k)
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)
transformer	forloop_to_postcondition (transformer pre, forloop fl, transformer t_body_star)
transformer	repeatloop_to_postcondition (transformer pre, whileloop wl, transformer t_body_star)
transformer	loop_to_postcondition (transformer pre, loop l, transformer tf)
transformer	loop_to_total_precondition (transformer t_post, loop l, transformer tf, transformer context)
transformer	whileloop_to_postcondition (transformer pre, whileloop l, transformer tf)
transformer	whileloop_to_total_precondition (transformer t_post, whileloop l, transformer tf, transformer context)

Macro Definition Documentation

IS_LOWER_BOUND

#define IS_LOWER_BOUND   0

Definition at line 491 of file loop.c.

IS_UPPER_BOUND

#define IS_UPPER_BOUND   1

Definition at line 492 of file loop.c.

Function Documentation

__attribute__()

static transformer __attribute__ ( (unused)  )

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.

{
  transformer new_tf = transformer_undefined;
  pips_assert("To shut up gcc", wl==wl && pre==pre);
  return new_tf;
}

References pips_assert, and transformer_undefined.

add_affine_bound_conditions()

static transformer add_affine_bound_conditions ( transformer  pre, entity  index, Pvecteur  v_bound, bool  lower_or_upper, transformer  tfb  )

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.

{
  Pvecteur v = vect_dup(v_bound);
 
  /* 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
   */
 
  if(value_mappings_compatible_vector_p(v) &&
     !transformer_affect_linear_p(tfb,v)) {
    if (lower_or_upper == IS_LOWER_BOUND)
      vect_add_elem(&v,
                    (Variable) entity_to_new_value(index), VALUE_MONE);
    else{
      vect_chg_sgn(v);
      vect_add_elem(&v, (Variable) entity_to_new_value(index), VALUE_ONE);
    }
    pre = transformer_inequality_add(pre, v);
  }
  else{
    vect_rm(v);
    v = VECTEUR_UNDEFINED;
  }
  return pre;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

add_good_loop_conditions()

static transformer add_good_loop_conditions ( transformer  pre, loop  l  )

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.

{
  /* 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 */
  statement b = loop_body(l);
  entity i = loop_index(l);
  range r = loop_range(l);
  /* Only OK if transformers already have been computed */
  /* transformer tfb = load_statement_transformer(b); */
  list eb = load_cumulated_rw_effects_list(b);
  transformer tfb = effects_to_transformer(eb);
 
  pips_debug(8, "begin\n");
 
  if(false) { /* New version to deal with complex do loop bounds? */
    transformer lbt = loop_bound_evaluation_to_transformer(l, pre);
    transformer opre = pre;
    pre = transformer_apply(pre, lbt);
    free_transformer(opre);
  }
  else {
    /* Old version */
    pre = add_index_range_conditions(pre, i, r, tfb);
  }
 
  pips_debug(8, "end\n");
 
  return(pre);
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

add_index_bound_conditions()

static transformer add_index_bound_conditions ( transformer  pre, entity  index, expression  bound, int  lower_or_upper, transformer  tfb  )

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.

{
  normalized n = NORMALIZE_EXPRESSION(bound);
 
  /* 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)); */
 
  if(normalized_linear_p(n)) {
    /* Old implementation, careful about the impact of the loop body
       but not about side effets in bound */
    Pvecteur v_bound = (Pvecteur) normalized_linear(n);
    /* tfb does not take into account the index incrementation */
    transformer t_iter = transformer_dup(tfb);
 
    transformer_arguments(t_iter) =
      arguments_add_entity(transformer_arguments(t_iter), index);
 
    add_affine_bound_conditions(pre, index, v_bound, lower_or_upper, t_iter);
    free_transformer(t_iter);
  }
  else { /* Why not use loop_bound_evaluation_to_transformer()? */
    type it = ultimate_type(entity_type(index));
    entity bv = make_local_temporary_value_entity(it);
    transformer pre_r = transformer_range(pre);
    transformer bt = safe_any_expression_to_transformer(bv, bound, pre_r, true);
    transformer br = transformer_range(bt);
    transformer npre = transformer_undefined;
 
    /* An inequation between index and bv should be added */
    if(lower_or_upper)
      br = transformer_add_inequality(br, index, bv, false);
    else
      br = transformer_add_inequality(br, bv, index, false);
 
    br = transformer_temporary_value_projection(br);
    reset_temporary_value_counter();
    br = safe_transformer_projection(br, transformer_arguments(tfb));
 
    /* FI: Fixt the result of the intersection in case of side
       effects in loop range*/
    npre = transformer_range_intersection(pre, br);
    //transformer_arguments(npre) = arguments_union(transformer_arguments(pre),
    //                                   transformer_arguments(npre));
    /* Make sure the loop body does not modify the loop bounds */
    // FI: ipre is not a range, invariant_wrt_transformer() cannot be used
    //npre = invariant_wrt_transformer(ipre, tfb);
    // FI: removes to many variables of ipre or npre; induction
    // variables are lost when computing the preconditions
    //npre = safe_transformer_projection(npre, transformer_arguments(tfb));
    /* FI: we need a side effect on pre... */
    //gen_free_list(transformer_arguments(pre));
    free_predicate(transformer_relation(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 */
    transformer_arguments(pre)
      = arguments_union(transformer_arguments(pre),
                        transformer_arguments(npre));
 
    transformer_relation(pre) = transformer_relation(npre);
    free_transformer(bt);
    free_transformer(br);
    transformer_arguments(npre) = NIL;
    transformer_relation(npre) = predicate_undefined;
    free_transformer(npre);
    free_transformer(pre_r);
  }
 
  pips_assert("The resulting transformer is consistent",
              transformer_consistent_p(pre));
 
  return(pre);
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

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

Parameters

pre	re
tfb	fb

Definition at line 711 of file loop.c.

{
  /* 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 */
 
  expression lb = range_lower(r);
  expression ub = range_upper(r);
  expression e_incr = range_increment(r);
  int incr = 0;
  int incr_lb = 0;
  int incr_ub = 0;
 
  pips_debug(8, "begin\n");
 
  if(entity_has_values_p(i)) {
 
    /* is the loop increment numerically known? Is its sign known? */
    expression_and_precondition_to_integer_interval(e_incr, pre, &incr_lb, &incr_ub);
 
    if(incr_lb==incr_ub) {
      if(incr_lb==0) {
        pips_user_error("Illegal null increment\n");
      }
      else
        incr = incr_lb;
    }
    else if(incr_lb>=1) {
      incr = 1;
    }
    else if(incr_ub<=-1) {
      incr = -1;
    }
    else {
      /* incr == 0 is used below as a give-up condition */
      incr = 0;
    }
 
    /* When lost, try to exploit type information thanks to unsigned variables */
    if(incr==0) {
      if(positive_expression_p(e_incr))
        incr = 1;
      else if(negative_expression_p(e_incr))
        incr = -1;
    }
 
    /* find the real upper and lower bounds */
    if(incr<0) {
      ub = range_lower(r);
      lb = range_upper(r);
    }
 
    if(incr!=0) {
      if(simple_dead_loop_p(lb, ub)) {
        transformer new_pre = transformer_empty();
 
        free_transformer(pre);
        pre = new_pre;
      }
      else {
        /* try to add the lower bound */
        add_index_bound_conditions(pre, i, lb, IS_LOWER_BOUND, tfb);
 
        /* try to add the upper bound */
        add_index_bound_conditions(pre, i, ub, IS_UPPER_BOUND, tfb);
      }
    }
 
  }
 
  pips_debug(8, "end\n");
  return pre;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

add_loop_index_exit_value()

transformer add_loop_index_exit_value	(	transformer	post,
		loop	l,
		transformer	pre
	)

The exit value is known if.

• the loop index is an analyzed integer scalar variable real index are standard-compliant, integer index can be equivalenced to a real variable,...
• the increment is affine (non-necessary assumption made: it is affine if the increment sign is known)
• the increment sign is known
• the body and loop initialization execution does not modify the value of the upper bound
• the upper bound is affine (?)

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:

• v_i + v_incr + v_ub <= 0, - v_ub + v_i + 1 <= 0

should never happen!

Parameters

post	ost
l	postcondition of the last iteration
pre	loop to process

Definition at line 878 of file loop.c.

{
  entity i = loop_index(l);
  expression e_incr = range_increment(loop_range(l));
  normalized n_incr = NORMALIZE_EXPRESSION(e_incr);
  expression e_ub = range_upper(loop_range(l));
  normalized n_ub = NORMALIZE_EXPRESSION(e_ub);
  transformer t_incr = transformer_undefined;
  transformer t_body = load_statement_transformer(loop_body(l));
  list li = CONS(ENTITY, i, NIL);
  int ub_inc = 0;
  int lb_inc = 0;
 
  ifdebug(8) {
    pips_debug(8, "begin with post:\n");
    (void) print_transformer(post);
  }
 
  if(!entity_has_values_p(i)) {
    ifdebug(8) {
      pips_debug(8, "give up because %s has no values:\n",
            entity_local_name(i));
      pips_debug(8, "end with post:\n");
      (void) print_transformer(post);
    }
    return transformer_dup(post);
  }
 
  expression_and_precondition_to_integer_interval(e_incr, pre, &lb_inc, &ub_inc);
 
  /* 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.
   */
  if(normalized_linear_p(n_incr)) {
    Pvecteur v_incr = (Pvecteur) normalized_linear(n_incr);
    if(value_mappings_compatible_vector_p(v_incr)) {
      entity i_new = entity_to_new_value(i);
      entity i_rep = value_to_variable(i_new);
      t_incr = affine_increment_to_transformer(i_rep, v_incr);
    }
    else {
      t_incr = transformer_undefined;
    }
  }
  else {
    t_incr = transformer_undefined;
  }
  if(t_incr==transformer_undefined)
    t_incr = args_to_transformer(li);
  /* Do not apply an extra iteration! */
  /* post = transformer_apply(t_body, post); */
  post = transformer_apply(t_incr, post);
  transformer_free(t_incr);
 
  ifdebug(8) {
    pips_debug(8, "post after index incrementation:\n");
    (void) print_transformer(post);
  }
 
  if(normalized_linear_p(n_ub)
     && !transformer_affect_linear_p(t_body, (Pvecteur) normalized_linear(n_ub))) {
    if(lb_inc >= 1 || ub_inc <= -1) {
      Pvecteur v_ub = (Pvecteur) normalized_linear(n_ub);
      Pvecteur v_incr = (Pvecteur) normalized_linear(n_incr);
 
      if(value_mappings_compatible_vector_p(v_ub)
         && value_mappings_compatible_vector_p(v_incr)) {
        entity i_new = entity_to_new_value(i);
        entity i_rep = value_to_variable(i_new);
        Pvecteur v_i = vect_new((Variable) i_rep, (Value) 1);
        Pvecteur c1 = VECTEUR_UNDEFINED;
        Pvecteur c2 = VECTEUR_UNDEFINED;
 
        pips_assert("The increment is an affine function", normalized_linear_p(n_incr));
        if(lb_inc==ub_inc && ABS(lb_inc)==1) {
          /* v_i - v_incr == v_ub, regardless of the sign */
          c1 = vect_substract(v_i, v_incr);
          c1 = vect_cl(c1, (Value) -1, v_ub);
          transformer_equality_add(post, c1);
        }
        else {
          if(lb_inc>=1) {
            /* v_i - v_incr <= v_ub < v_i
             * or:
             * v_i - v_incr - v_ub <= 0, v_ub - v_i + 1 <= 0
             */
            c1 = vect_substract(v_i, v_incr);
            c2 = vect_substract(v_ub, v_i);
 
            c1 = vect_cl(c1, (Value) -1, v_ub);
            vect_add_elem(&c2, (Variable) TCST, (Value) 1);
          }
          else if(ub_inc<=-1) {
            /* v_i - v_incr >= v_ub > v_i
             *
             * or:
             * - v_i + v_incr + v_ub <= 0, - v_ub + v_i + 1 <= 0
             */
            c1 = vect_substract(v_incr, v_i);
            c2 = vect_substract(v_i, v_ub);
 
            c1 = vect_cl(c1, (Value) 1, v_ub);
            vect_add_elem(&c2, (Variable) TCST, (Value) 1);
          }
          else {
            /* should never happen! */
            pips_assert("add_loop_index_exit_value", false);
          }
          transformer_inequality_add(post, c1);
          transformer_inequality_add(post, c2);
        }
 
        ifdebug(8) {
          pips_debug(8, "post with exit conditions:\n");
          (void) print_transformer(post);
        }
      }
      else {
        pips_debug(8,
              "post is unchanged because the increment or the upper bound"
              " reference unanalyzed variables\n");
      }
    }
    else {
      pips_debug(8,
            "post is unchanged because the increment sign is unknown\n");
    }
  }
  else {
    pips_debug(8,
          "post is unchanged because the upper bound is not affine\n");
  }
 
  ifdebug(8) {
    pips_debug(8, "end: post:\n");
    (void) print_transformer(post);
  }
 
  return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

add_loop_index_initialization()

static transformer add_loop_index_initialization ( transformer  tf, loop  l, transformer  pre  )

static

Always returns newly allocated memory.

Definition at line 825 of file loop.c.

{
    entity i = loop_index(l);
    expression init = range_lower(loop_range(l));
    transformer post = transformer_undefined;
    transformer t_init = transformer_undefined;
    //list lef = expression_to_proper_effects(init);
    list lef = expression_to_proper_constant_path_effects(init);
    transformer pre_r = transformer_range(pre);
 
    t_init = any_scalar_assign_to_transformer(i, init, lef, pre_r);
    free_transformer(pre_r);
 
    if(t_init==transformer_undefined)
        t_init = effects_to_transformer(lef);
    post = transformer_apply(t_init, tf);
 
    transformer_free(t_init);
 
    return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

add_loop_skip_condition()

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

Parameters

tf	f
pre	re

Definition at line 495 of file loop.c.

{
  /* It is assumed that loop l is not entered */
  range r = loop_range(l);
  expression e_lb = range_lower(r);
  expression e_ub = range_upper(r);
  expression e_incr = range_increment(r);
  normalized n_lb = NORMALIZE_EXPRESSION(e_lb);
  normalized n_ub = NORMALIZE_EXPRESSION(e_ub);
  int incr = 0;
  int incr_lb = 0;
  int incr_ub = 0;
 
  /* EXPRESSION_TO_TRANSFORMER() should be used */
 
  pips_debug(8,"begin with transformer tf=%p\n", tf);
  ifdebug(8) {
    (void) print_transformer(tf);
    pips_debug(8,"and precondition pre=%p\n", pre);
    (void) print_transformer(pre);
  }
 
  /* is the loop increment numerically known? Is its sign known? */
  expression_and_precondition_to_integer_interval(e_incr, pre, &incr_lb, &incr_ub);
 
  if(incr_lb==incr_ub) {
    if(incr_lb==0) {
      user_error("add_loop_skip_condition", "Illegal null loop increment\n");
    }
    else
      incr = incr_lb;
  }
  else if(incr_lb>=1) {
    incr = 1;
  }
  else if(incr_ub<=-1) {
    incr = -1;
  }
  else
    incr = 0;
 
  /* incr == 0 is used below as a give-up condition */
 
  /* find the real upper and lower bounds */
  if(incr<0) {
    /* exchange bounds */
    n_lb = NORMALIZE_EXPRESSION(e_ub);
    n_ub = NORMALIZE_EXPRESSION(e_lb);
  }
 
  if(incr!=0 && normalized_linear_p(n_lb) && normalized_linear_p(n_ub)) {
    /* ub < lb, i.e. ub + lb + 1 <= 0 */
    Pvecteur v_ub = (Pvecteur) normalized_linear(n_ub);
    Pvecteur v_lb = (Pvecteur) normalized_linear(n_lb);
 
    if(value_mappings_compatible_vector_p(v_lb)
       && value_mappings_compatible_vector_p(v_ub)) {
      Pvecteur v = vect_substract(v_ub, v_lb);
 
      vect_add_elem(&v, TCST, (Value) 1);
      tf = transformer_inequality_add(tf, v);
 
      ifdebug(8) {
        debug(8,"add_loop_skip_condition","Skip condition:\n");
        vect_fprint(stderr, v, (char * (*)(Variable)) external_value_name);
      }
    }
    else {
      pips_debug(8,"Non-analyzed variable in loop bound(s)\n");
    }
  }
  else {
    pips_debug(8,"increment sign unknown or non-affine bound\n");
  }
 
  ifdebug(8) {
    pips_debug(8,"end with new tf=%p\n", tf);
    (void) print_transformer(tf);
  }
 
  return tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

any_loop_to_k_transformer()

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

1. If k == 1, the body transformer is computed first and the loop transformer is derived from it. If k>1, the body transformer is retrieved and the loop transformer is based on the assumption that the number of iterations executed is always a multiple of k.

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:

• a very approximate fix-point and the conditions met for the body to execute, pre_iteration.
• the convex hull of the precondition holding for the first iteration and the range of the extended body transformer, t_next.

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.

{
  transformer t_body = transformer_undefined; // Body transformer
  transformer t_body_star = transformer_undefined; // result: t_init ; t_enter ; tfbodystar
  transformer pre_body = transformer_undefined;
  transformer post_body = transformer_undefined;
  // This does not include the loop effects, e.g. the index incrementation
  //list bel = load_cumulated_rw_effects_list(body);
  //transformer t_effects = effects_to_transformer(bel);
  transformer t_effects = effects_to_transformer(lel);
  transformer post_enter = transformer_apply(t_enter, post_init);
  //post_enter = transformer_normalize(post_enter, 0);
  transformer post_next = transformer_undefined;
  transformer t_next_star = transformer_undefined;
 
  // They are displayed by any_transformer_to_k_closure()
  ifdebug(9) {
    fprintf(stderr, "t_init:\n");
    print_transformer(t_init);
    fprintf(stderr, "t_enter:\n");
    print_transformer(t_enter);
    fprintf(stderr, "t_next:\n");
    print_transformer(t_next);
    fprintf(stderr, "post_init:\n");
    print_transformer(post_init);
  }
 
  /* Compute a first rough body precondition, pre_body, using
   * different heuristics:
   *
   * - a very approximate fix-point and the conditions met for the
   * body to execute, pre_iteration.
   *
   * -
   *
   * - the convex hull of the precondition holding for the first
   *   iteration and the range of the extended body transformer,
   *   t_next.
   */
  //
  // First heuristics:
  //pre_body = invariant_wrt_transformer(post_enter, t_effects);
  // memory leak for pre_body? for transformer_range(pre_iteration)?
  //pre_body = invariant_wrt_transformer(pre_body, t_next);
  /* Add the loop body execution condition */
  //pre_body = transformer_combine(pre_body, pre_iteration);
  //
  // Second heuristics: either we enter directly or we loop
  post_body = transformer_apply(t_effects, post_enter);
  // temporary memory leaks
  t_next_star = (* transformer_fix_point_operator)(t_next);
  post_next = transformer_range(transformer_apply(transformer_combine(t_next_star, t_next), post_body));
  //post_next = transformer_normalize(post_next, 0);
  transformer pre_body_2 = transformer_range(transformer_convex_hull(post_next, post_enter));
  //
  // Third heuristics: either it is the first iteration, or we are in
  // the range of t_next (added for Semantics-New/flip-flop01.c, but
  // turns out to be useless for flip-flop02)
  // transformer pre_body_3 = transformer_convex_hull(post_enter, transformer_range(t_next));
 
  // pre_body = transformer_intersection(pre_body_2, pre_body_3);
  //free_transformers(pre_body_2, pre_body_3, NULL);
  pre_body = pre_body_2;
 
  /* Compute the body transformer */
  // THIS PART SHOULD BE CLEANED-UP and k not used to avoid
  // recomputing the transformers inside the loop body
  // There is no longer any reason to call this function with k !=1
  // For k == 2, call directly any_transformer_to_k_closure()
  // statement_to_transformer() allocated a new transformer which is not the stored transformer
  //t_body = transformer_dup(statement_to_transformer(body, pre_body));
  if(k==1) {
    t_body = statement_to_transformer(body, pre_body);
    // Experimental: produces wrong results
    // t_body = transformer_intersect_range_with_domain(t_body);
  }
  else // assume k==2
    t_body = copy_transformer(load_statement_transformer(body));
 
 
  // Insert a call to any_transformer_to_k_closure()
  t_body_star = any_transformer_to_k_closure(t_init,
                                             t_enter,
                                             t_next,
                                             t_body,
                                             post_init,
                                             k, // unrollling degree
                                             false); // assume a first
                                                     // execution of t_body
 
  /* Any transformer or other data structure to free? */
  //free_transformer(t_body); FI: no idea if it should be freed or not...
  free_transformer(pre_body);
  free_transformer(post_body);
  free_transformer(post_next);
  free_transformer(t_effects);
  free_transformer(post_enter);
  free_transformer(t_next_star);
 
  ifdebug(8) {
    fprintf(stderr, "t_body_star:\n");
    print_transformer(t_body_star);
  }
 
  return t_body_star;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

any_loop_to_postcondition()

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

Parameters

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.

{
  /* 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)
   */
  transformer p_body = transformer_undefined;
  transformer post = transformer_undefined;
  /* To restrict the state at the beginning of the last iteration:
     should be part of t_body_star */
  //transformer post_enter = transformer_range(t_enter);
  //transformer post_continue = transformer_range(t_next);
  //transformer pre_iteration = transformer_convex_hull(post_enter, post_continue);
  /* Decompose the computation of p_body */
  transformer p_body_1 = transformer_apply(t_enter, transformer_apply(t_init, pre));
  transformer p_body_2 = transformer_apply(t_body_star, pre);
  //transformer p_body_3 = transformer_apply(pre_iteration, p_body_2);
  transformer p_body_4 = transformer_apply(t_body, p_body_2);
  transformer p_body_5 = transformer_apply(t_next, p_body_4);
  transformer a_post = transformer_undefined;
  /* Decompose the computation of post */
  transformer post_1 = transformer_apply(t_skip, transformer_apply(t_init, pre));
  transformer post_2 = transformer_apply(t_body_star, pre);
  //transformer post_3 = transformer_apply(pre_iteration, post_2);
  transformer post_4 = transformer_apply(t_body, post_2);
  transformer post_5 = transformer_apply(t_inc, post_4);
  transformer post_6 = transformer_apply(t_exit, post_5);
 
  p_body = transformer_convex_hull(p_body_1, p_body_5);
  a_post = statement_to_postcondition(p_body, body);
 
  /* a_post should be used because it is more accurate than direct
     recomputation, but we chose for the time being to recompute post
     entirely */
  post = transformer_convex_hull(post_1, post_6);
 
  /* Get rid of now useless transformers */
 
  free_transformer(a_post);
 
  //free_transformer(post_enter);
  //free_transformer(post_continue);
  //free_transformer(pre_iteration);
 
  free_transformer(p_body_1);
  free_transformer(p_body_2);
  //free_transformer(p_body_3);
  free_transformer(p_body_4);
  free_transformer(p_body_5);
 
  free_transformer(post_1);
  free_transformer(post_2);
  //free_transformer(post_3);
  free_transformer(post_4);
  free_transformer(post_5);
  free_transformer(post_6);
 
  return post;
}

References free_transformer(), statement_to_postcondition(), transformer_apply(), transformer_convex_hull(), and transformer_undefined.

Referenced by forloop_to_postcondition(), and repeatloop_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

any_loop_to_transformer()

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.

{
  return any_loop_to_k_transformer(t_init, t_enter, t_next, body, lel, post_init, 1);
}

References any_loop_to_k_transformer().

Referenced by forloop_to_transformer(), new_loop_to_transformer(), new_whileloop_to_transformer(), and repeatloop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_any_loop_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.

{
  transformer ltf = transformer_undefined;
  list ltl = complete_any_loop_transformer_list(t_init,
                                                t_skip,
                                                t_body_star,
                                                t_body,
                                                t_inc,
                                                t_exit);
 
  ltf = transformer_list_to_transformer(ltl);
 
  gen_free_list(ltl);
 
  return ltf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_any_loop_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:

1. The loop is always entered and exited (usual case for scientific code: t_skip = transformer_empty).
2. The loop is always entered and never exited (real-time code situation, t_exit = transformer_empty)
3. The loop is never entered (in its current context, t_bodystar = transformer_empty because t_enter = transformer_empty).
4. The loop may be entered and exited (usual case for general purpose computing, think of list handling).
5. The loop may be entered but is then never exited (real-time code again).

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

Parameters

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.

{
  /* 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:
   *
   * 1. The loop is always entered and exited (usual case for
   * scientific code: t_skip = transformer_empty).
   *
   * 2. The loop is always entered and never exited (real-time code
   * situation, t_exit = transformer_empty)
   *
   * 3. The loop is never entered (in its current context, t_bodystar
   * = transformer_empty because t_enter = transformer_empty).
   *
   * 4. The loop may be entered and exited (usual case for general
   * purpose computing, think of list handling).
   *
   * 5. The loop may be entered but is then never exited (real-time
   * code again).
   *
   * These cases are checked with complete01.c,
   * complete02.c,... complete05.c
   */
  list ltl = NIL;
  // transformer ct = transformer_undefined;
  /* loop skipped transformer */
  transformer lst = transformer_combine(copy_transformer(t_init), t_skip);
  /* add loop entered transformer/condition: should already be in t_body_star */
  //transformer post_enter = transformer_range(t_enter);
  //transformer post_continue = transformer_range(t_continue);
  //transformer pre_body = transformer_convex_hull(post_enter, post_continue);
  //transformer let = transformer_combine(copy_transformer(t_body_star), pre_body);
  transformer let = copy_transformer(t_body_star);
 
  ifdebug(8) {
    fprintf(stderr, "t_init:\n");
    print_transformer(t_init);
    fprintf(stderr, "t_skip:\n");
    print_transformer(t_skip);
    fprintf(stderr, "t_body_star:\n");
    print_transformer(t_body_star);
    fprintf(stderr, "t_body:inc\n");
    print_transformer(t_body);
    fprintf(stderr, "t_inc:\n");
    print_transformer(t_inc);
    fprintf(stderr, "t_exit:\n");
    print_transformer(t_exit);
  }
 
  let = transformer_combine(let, t_body);
  let = transformer_combine(let, t_inc);
  let = transformer_combine(let, t_exit);
  let = transformer_normalize(let, 2);
 
  /* combine both cases in a transformer list */
  //ct = transformer_convex_hull(lst, let);
  ltl = two_transformers_to_list(lst, let);
 
  //free_transformer(post_enter);
  //free_transformer(post_continue);
  //free_transformer(pre_body);
 
  ifdebug(8) {
    fprintf(stderr, "ltl:\n");
    print_transformers(ltl);
  }
 
  return ltl;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_forloop_transformer()

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.

Parameters

t_body_star	_body_star
pre	re
fl	l

Definition at line 1686 of file loop.c.

{
  transformer ct = transformer_undefined;
  statement body_s = forloop_body(fl);
  transformer t_body = load_statement_transformer(body_s);
  transformer ct_body = transformer_undefined;
  transformer pre_body = transformer_undefined;
  expression init_e = forloop_initialization(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. */
  transformer t_init = safe_expression_to_transformer(init_e, pre);
  transformer post_init = transformer_apply(t_init, pre);
  expression cond_e = forloop_condition(fl);
  expression inc_e = forloop_increment(fl);
  transformer t_skip = condition_to_transformer(cond_e, post_init, false);
  transformer t_enter = condition_to_transformer(cond_e, post_init, true);
/* An effort could be made to compute the precondition for t_exit,
     especially if the precondition to t_inc is available. */
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  /* An effort could be made to compute the precondition for t_inc */
  transformer t_inc = safe_expression_to_transformer(inc_e, transformer_undefined);
 
  /* Make sure you have the effective statement transformer: it is not
     stored for loops and this is key for nested loops. */
  pre_body = transformer_apply(t_body_star, pre);
  ct_body = complete_statement_transformer(t_body, pre_body, body_s);
 
  ct = complete_any_loop_transformer(t_init, t_enter, t_skip, t_body_star, ct_body, t_continue, t_inc, t_exit);
 
  free_transformer(ct_body);
  free_transformer(pre_body);
  free_transformer(t_init);
  free_transformer(post_init);
  free_transformer(t_skip);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(t_exit);
  free_transformer(t_inc);
 
  return ct;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_forloop_transformer_list()

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.

Parameters

t_body_star	_body_star
pre	re
fl	l

Definition at line 1732 of file loop.c.

{
  list tfl = list_undefined;
  statement body_s = forloop_body(fl);
  transformer t_body = load_statement_transformer(body_s);
  transformer ct_body = transformer_undefined;
  transformer pre_body = transformer_undefined;
  expression init_e = forloop_initialization(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. */
  transformer t_init = safe_expression_to_transformer(init_e, pre);
  transformer post_init = transformer_apply(t_init, pre);
  expression cond_e = forloop_condition(fl);
  expression inc_e = forloop_increment(fl);
  transformer t_skip = condition_to_transformer(cond_e, post_init, false);
  transformer t_enter = condition_to_transformer(cond_e, post_init, true);
/* An effort could be made to compute the precondition for t_exit,
     especially if the precondition to t_inc is available. */
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  /* An effort could be made to compute the precondition for t_inc */
  transformer t_inc = safe_expression_to_transformer(inc_e, transformer_undefined);
 
  pips_internal_error("function is not implemented");
 
  /* Make sure you have the effective statement transformer: it is not
     stored for loops and this is key for nested loops. */
  pre_body = transformer_apply(t_body_star, pre);
  ct_body = complete_statement_transformer(t_body, pre_body, body_s);
 
  (void)complete_any_loop_transformer(t_init, t_enter, t_skip, t_body_star, ct_body, t_continue, t_inc, t_exit);
 
  free_transformer(ct_body);
  free_transformer(pre_body);
  free_transformer(t_init);
  free_transformer(post_init);
  free_transformer(t_skip);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(t_exit);
  free_transformer(t_inc);
 
  return tfl;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_loop_transformer()

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.

Parameters

ltf	tf
pre	re

Definition at line 1927 of file loop.c.

{
  transformer tf = transformer_undefined;
  transformer t_enter = transformer_undefined;
  transformer t_skip = transformer_undefined;
  /* loop body transformer */
  transformer btf = transformer_undefined;
  range r = loop_range(l);
  statement s = loop_body(l);
 
  pips_debug(8,"begin with loop precondition\n");
  ifdebug(8) {
    (void) print_transformer(pre);
    pips_debug(8,"and loop transformer:\n");
    (void) print_transformer(ltf);
  }
 
  /* compute the loop body transformer */
  if(statement_loop_p(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! */
    loop il = instruction_loop(statement_instruction(s));
    /* compute the loop body precondition */
    transformer raw_ipre = transformer_apply(ltf, pre);
    transformer ipre = transformer_range(raw_ipre);
    ipre = transformer_normalize(ipre, 2);
    /* 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 */
    transformer st = load_statement_transformer(s);
    btf = complete_loop_transformer(st, ipre, il);
    btf = transformer_normalize(btf, 2);
    free_transformer(ipre);
    free_transformer(raw_ipre);
  }
  else {
    btf = transformer_dup(load_statement_transformer(s));
  }
  /* 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. */
  t_enter = transformer_combine(transformer_dup(ltf), btf);
 
  ifdebug(8) {
    pips_debug(8, "entered loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* 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. */
  /*
  transformer t_inc = transformer_identity();
  t_inc = transformer_add_loop_index_incrementation(t_inc, l, pre);
  t_enter = transformer_combine(t_enter, t_inc);
  */
 
  /* add the exit condition, without any information pre to estimate the
     increment */
  transformer tmp = t_enter;
  /* FI: oops, pre is used in spite of previous comment */
  t_enter = add_loop_index_exit_value(t_enter, l, pre);
  transformer_free(tmp);
 
  ifdebug(8) {
    pips_debug(8, "entered and exited loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* add initialization for the unconditional initialization of the loop
     index variable */
  tmp = transformer_undefined_p(pre)?
    transformer_identity() :
    transformer_dup(pre);
  t_skip = add_loop_index_initialization(tmp, l, pre);
  //transformer ipre = transformer_apply(t_skip, pre);
  //transformer ripre = transformer_range(ipre);
  transformer_free(tmp);
  t_skip = add_loop_skip_condition(t_skip, l, pre);
  t_skip = transformer_normalize(t_skip, 2);
 
  ifdebug(8) {
    pips_debug(8, "skipped loop transformer t_skip=\n");
    fprint_transformer(stderr, t_skip, (get_variable_name_t) external_value_name);
  }
 
  /* 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. */
  // if(empty_range_wrt_precondition_p(r, ripre)) {
  if(empty_range_wrt_precondition_p(r, pre)) {
    tf = t_skip;
    free_transformer(t_enter);
  }
  // else if(non_empty_range_wrt_precondition_p(r, ripre)) {
  else if(non_empty_range_wrt_precondition_p(r, pre)) {
    tf = t_enter;
    free_transformer(t_skip);
  }
  else {
    tf = transformer_convex_hull(t_enter, t_skip);
    free_transformer(t_enter);
    free_transformer(t_skip);
  }
  //free_transformer(ipre);
  //free_transformer(ripre);
 
  tf = transformer_normalize(tf, 2);
 
  ifdebug(8) {
    pips_debug(8, "full refined loop transformer tf=\n");
    fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
    pips_debug(8, "end\n");
  }
 
  return tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_loop_transformer_list()

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.

Parameters

ltf	tf
pre	re

Definition at line 2061 of file loop.c.

{
  list tfl = list_undefined;
  transformer tf = transformer_undefined;
  transformer t_enter = transformer_undefined;
  transformer t_skip = transformer_undefined;
  /* loop body transformer */
  transformer btf = transformer_undefined;
  range r = loop_range(l);
  statement s = loop_body(l);
 
  pips_internal_error("Function not implemented.");
 
  pips_debug(8,"begin with loop precondition\n");
  ifdebug(8) {
    (void) print_transformer(pre);
    pips_debug(8,"and loop transformer:\n");
    (void) print_transformer(ltf);
  }
 
  /* compute the loop body transformer */
  if(statement_loop_p(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! */
    loop il = instruction_loop(statement_instruction(s));
    /* compute the loop body precondition */
    transformer raw_ipre = transformer_apply(ltf, pre);
    //transformer ipre = transformer_range(raw_ipre);
    //ipre = transformer_normalize(ipre, 2);
    /* You do not need a range to recurse. A full precondition with
       arguments is expected by complete_loop_transformer(). */
    btf = complete_loop_transformer(load_statement_transformer(s), raw_ipre, il);
    btf = transformer_normalize(btf, 2);
    //free_transformer(ipre);
    free_transformer(raw_ipre);
  }
  else {
    btf = transformer_dup(load_statement_transformer(s));
  }
  /* 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* */
  t_enter = transformer_combine(transformer_dup(ltf), btf);
 
  ifdebug(8) {
    pips_debug(8, "entered loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* 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. */
  /*
  transformer t_inc = transformer_identity();
  t_inc = transformer_add_loop_index_incrementation(t_inc, l, pre);
  t_enter = transformer_combine(t_enter, t_inc);
  */
 
  /* add the exit condition, without any information pre to estimate the
     increment */
  transformer tmp = t_enter;
  /* FI: oops, pre is used in spite of previous comment */
  t_enter = add_loop_index_exit_value(t_enter, l, pre);
  transformer_free(tmp);
 
  ifdebug(8) {
    pips_debug(8, "entered and exited loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* add initialization for the unconditional initialization of the loop
     index variable */
  tmp = transformer_undefined_p(pre)?
    transformer_identity() :
    transformer_dup(pre);
  t_skip = add_loop_index_initialization(tmp, l, pre);
  transformer_free(tmp);
  t_skip = add_loop_skip_condition(t_skip, l, pre);
  t_skip = transformer_normalize(t_skip, 2);
 
  ifdebug(8) {
    pips_debug(8, "skipped loop transformer t_skip=\n");
    fprint_transformer(stderr, t_skip, (get_variable_name_t) external_value_name);
  }
 
  /* 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. */
  if(empty_range_wrt_precondition_p(r, pre)) {
    tf = t_skip;
    free_transformer(t_enter);
  }
  else if(non_empty_range_wrt_precondition_p(r, pre)) {
    tf = t_enter;
    free_transformer(t_skip);
  }
  else {
    tf = transformer_convex_hull(t_enter, t_skip);
    free_transformer(t_enter);
    free_transformer(t_skip);
  }
 
  tf = transformer_normalize(tf, 2);
 
  ifdebug(8) {
    pips_debug(8, "full refined loop transformer tf=\n");
    fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
    pips_debug(8, "end\n");
  }
 
  return tfl;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_repeatloop_transformer()

transformer complete_repeatloop_transformer	(	transformer	t_body_star,
		transformer	pre,
		whileloop	wl
	)

Parameters

t_body_star	_body_star
pre	re
wl	l

Definition at line 1910 of file loop.c.

{
  list tl = complete_repeatloop_transformer_list(t_body_star, pre, wl);
  transformer ct = transformer_list_to_transformer(tl);
  return ct;
}

References complete_repeatloop_transformer_list(), and transformer_list_to_transformer().

Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_repeatloop_transformer_list()

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.

{
  list tfl = NIL;
  statement body_s = whileloop_body(wl);
  transformer pt_body = load_statement_transformer(body_s);
  transformer t_body = transformer_undefined;
  transformer pre_body = transformer_undefined;
  transformer t_init = transformer_identity();
  expression cond_e = whileloop_condition(wl);
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  transformer t_enter = transformer_identity();
  transformer t_skip = transformer_empty();
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  /* An effort could be made to compute the precondition for t_exit */
  transformer t_inc = transformer_identity();
  transformer t_loop_1 = transformer_undefined;
  transformer t_loop_2 = transformer_undefined;;
 
  /* Make sure you have the effective statement transformer: it is not
     stored for loops and this is key for nested loops. */
  pre_body = transformer_apply(t_body_star, pre);
  t_body = complete_statement_transformer(pt_body, pre_body, body_s);
 
  t_loop_1 = copy_transformer(t_body);
  t_loop_2 = copy_transformer(t_body);
 
  /* 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.
   */
 
  //  ct = complete_any_loop_transformer(t_init, t_enter, t_skip, t_body_star, t_body, t_continue, t_inc, t_exit);
 
  t_loop_1 = transformer_combine(t_loop_1, t_exit);
 
  t_loop_2 = transformer_combine(t_loop_2, t_continue);
  t_loop_2 = transformer_combine(t_loop_2, t_body_star);
  t_loop_2 = transformer_combine(t_loop_2, t_body);
  t_loop_2 = transformer_combine(t_loop_2, t_exit);
 
  //ct = transformer_convex_hull(t_loop_1, t_loop_2);
  tfl = two_transformers_to_list(t_loop_1, t_loop_2);
 
  free_transformer(t_body);
  free_transformer(pre_body);
  free_transformer(t_init);
  free_transformer(t_enter);
  free_transformer(t_skip);
  free_transformer(t_exit);
  free_transformer(t_inc);
 
  //free_transformer(t_loop_1);
  //free_transformer(t_loop_2);
 
  return tfl;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_whileloop_transformer()

transformer complete_whileloop_transformer	(	transformer	ltf,
		transformer	pre,
		whileloop	wl
	)

FI: I'm not sure this function is useful.

Parameters

ltf	tf
pre	re
wl	l

Definition at line 2183 of file loop.c.

{
  transformer t = transformer_undefined;
  evaluation lt = whileloop_evaluation(wl);
 
  if(evaluation_before_p(lt))
    t = new_complete_whileloop_transformer(ltf, pre, wl, false);
  else
    t = complete_repeatloop_transformer(ltf, pre, wl);
 
  return t;
}

References complete_repeatloop_transformer(), evaluation_before_p, new_complete_whileloop_transformer(), transformer_undefined, and whileloop_evaluation.

Referenced by old_complete_whileloop_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

complete_whileloop_transformer_list()

list complete_whileloop_transformer_list	(	transformer	ltf,
		transformer	pre,
		whileloop	wl
	)

Parameters

ltf	tf
pre	re
wl	l

Definition at line 2198 of file loop.c.

{
  list tfl = NIL;
  evaluation lt = whileloop_evaluation(wl);
 
  if(evaluation_before_p(lt))
    tfl = new_complete_whileloop_transformer_list(ltf, pre, wl, false);
  else
    tfl = complete_repeatloop_transformer_list(ltf, pre, wl);
 
  return tfl;
}

References complete_repeatloop_transformer_list(), evaluation_before_p, new_complete_whileloop_transformer_list(), NIL, and whileloop_evaluation.

Referenced by instruction_to_transformer_list().

Here is the call graph for this function:

Here is the caller graph for this function:

forloop_to_postcondition()

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

Parameters

pre	re
fl	l
t_body_star	_body_star

Definition at line 2707 of file loop.c.

{
  transformer post = transformer_undefined;
 
  statement body_s = forloop_body(fl);
  transformer t_body = load_statement_transformer(body_s);
 
  expression init_e = forloop_initialization(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. */
  transformer t_init = safe_expression_to_transformer(init_e, pre);
  transformer post_init = transformer_apply(t_init, pre);
 
  expression cond_e = forloop_condition(fl);
  transformer t_skip = condition_to_transformer(cond_e, post_init, false);
  transformer t_enter = condition_to_transformer(cond_e, post_init, true);
/* An effort could be made to compute the precondition for t_exit,
     especially if the precondition to t_inc is available. */
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
 
  expression inc_e = forloop_increment(fl);
  /* An effort could be made to compute the precondition for t_inc */
  transformer t_inc = safe_expression_to_transformer(inc_e, transformer_undefined);
 
  transformer t_next = transformer_combine(transformer_dup(t_inc), t_continue);
 
  post = any_loop_to_postcondition(body_s,
                                   t_init,
                                   t_enter,
                                   t_skip,
                                   t_body_star,
                                   t_body,
                                   t_next,
                                   t_inc,
                                   t_exit,
                                   pre);
 
  /* Clean up memory */
 
  free_transformer(t_init);
  free_transformer(post_init);
  free_transformer(t_skip);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(t_exit);
  free_transformer(t_inc);
  free_transformer(t_next);
 
    return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

forloop_to_transformer()

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

Parameters

fl	l
pre	re
flel	lel

Definition at line 326 of file loop.c.

{
  /* t_body_star =  t_init ; t_enter ;(t_body ; t_next)* */
  transformer t_body_star = transformer_undefined;
  statement body_s = forloop_body(fl);
 
  /* Deal with initialization expression */
  expression init_e = forloop_initialization(fl);
  transformer t_init = safe_expression_to_transformer(init_e, pre);
  transformer post_init = transformer_apply(t_init, pre);
 
  /* Deal with condition expression */
  expression cond_e = forloop_condition(fl);
  transformer t_enter = condition_to_transformer(cond_e, post_init, true);
  /* An effort could be made to compute the precondition for t_continue,
     especially if the precondition to t_inc is available. */
  transformer p_continue = transformer_identity();
  transformer t_continue = condition_to_transformer(cond_e, p_continue, true);
 
  /* Deal with increment expression */
  expression inc_e = forloop_increment(fl);
  /* An effort could be made to compute the precondition for t_inc */
  transformer t_inc = safe_expression_to_transformer(inc_e, transformer_undefined);
  transformer t_next = transformer_combine(t_inc, t_continue);
 
  t_body_star = any_loop_to_transformer(t_init, t_enter, t_next, body_s, flel, post_init);
 
  /* Let's clean up the memory */
 
  free_transformer(p_continue);
 
  free_transformer(t_init);
  free_transformer(post_init);
 
  free_transformer(t_enter);
  free_transformer(t_continue);
 
  // free_transformer(t_inc); it is absorbed by t_next
  free_transformer(t_next);
 
  return t_body_star;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

forloop_to_transformer_list()

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.

{
  list tfl = NIL;
  pips_internal_error("Not implemented yet.");
  return tfl;
}

References NIL, and pips_internal_error.

loop_body_transformer_add_entry_and_iteration_information()

static transformer loop_body_transformer_add_entry_and_iteration_information ( transformer  tfb, transformer  pre  )

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.

{
  /* 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] */
  transformer initial = transformer_range(pre);
  transformer next = transformer_range(tfb);
  transformer pre_body = transformer_convex_hull(initial, next);
 
 
  ifdebug(8) {
    pips_debug(5, "Begin with body transformer:\n");
    print_transformer(tfb);
    pips_debug(5, "initial precondition:\n");
    print_transformer(initial);
    pips_debug(5, "next precondition:\n");
    print_transformer(next);
    pips_debug(5, "body precondition:\n");
    print_transformer(pre_body);
  }
 
 
  tfb = transformer_domain_intersection(tfb, pre_body);
 
  free_transformer(initial);
  free_transformer(next);
  free_transformer(pre_body);
 
  ifdebug(8) {
    pips_debug(5, "End with new body transformer:\n");
    print_transformer(tfb);
  }
 
  return tfb;
}

References free_transformer(), ifdebug, pips_debug, print_transformer, transformer_convex_hull(), transformer_domain_intersection(), and transformer_range().

Referenced by standard_whileloop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_bound_evaluation_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.

Parameters

pre

re

Definition at line 1203 of file loop.c.

{
  transformer r = transformer_undefined;
  entity i = loop_index(l);
 
  //pips_assert("No temporary variables are allocated",
  //      number_of_temporary_values()==0);
 
  if(entity_has_values_p(i)) {
    expression lbe = range_lower(loop_range(l));
    transformer iit = loop_initialization_to_transformer(l, pre);
    entity lbv = make_local_temporary_value_entity(entity_type(i));
    transformer lbt = any_expression_to_transformer(lbv, lbe, pre, true);
 
    transformer preub = transformer_safe_apply(iit, pre);
    expression ube = range_upper(loop_range(l));
    entity ubv = make_local_temporary_value_entity(entity_type(i));
    transformer ubt = any_expression_to_transformer(ubv, ube, preub, true);
 
    transformer prei = transformer_safe_apply(ubt, preub);
    expression ie = range_increment(loop_range(l));
    entity iv = make_local_temporary_value_entity(entity_type(i));
    transformer it = any_expression_to_transformer(iv, ie, prei, true);
    transformer pre_inc = transformer_safe_intersection(prei, it);
    entity ni = entity_to_new_value(i);
    int inc_lb = 0;
    int inc_ub = 0;
    expression eiv = entity_to_expression(iv);
 
    expression_and_precondition_to_integer_interval(eiv, pre_inc, &inc_lb, &inc_ub);
    free_expression(eiv);
 
    if(inc_lb>0 || inc_ub<0) {
      Pvecteur lb_ineq = vect_new((Variable) ni, VALUE_MONE);
      Pvecteur ub_ineq = vect_new((Variable) ni, VALUE_ONE);
 
      vect_add_elem(&lb_ineq, (Variable) lbv, VALUE_ONE);
      vect_add_elem(&ub_ineq, (Variable) ubv, VALUE_MONE);
 
      if(inc_ub<0) {
        lb_ineq = vect_multiply(lb_ineq, VALUE_MONE);
        ub_ineq = vect_multiply(ub_ineq, VALUE_MONE);
      }
      r = transformer_safe_apply(it, prei);
      r = transformer_safe_image_intersection(r, lbt);
      r = transformer_safe_image_intersection(r, ubt);
      r = transformer_inequality_add(r, lb_ineq);
      r = transformer_inequality_add(r, ub_ineq);
      r = transformer_temporary_value_projection(r);
    }
    reset_temporary_value_counter();
  }
  return r;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_initialization_to_transformer()

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

Parameters

pre

re

Definition at line 1266 of file loop.c.

{
  effect init_e = make_effect(make_cell(is_cell_preference,
                                        make_preference(make_reference(loop_index(l), NIL))),
                              make_action_write_memory(),
                              make_approximation_exact(),
                              make_descriptor_none());
  list l_init_e = CONS(EFFECT, init_e, NIL);
  //list l_expr_e = expression_to_proper_effects(range_lower(loop_range(l)));
  expression lbe = range_lower(loop_range(l));
  list l_expr_e = expression_to_proper_constant_path_effects(lbe);
  list el = list_undefined;
 
  transformer r_pre = transformer_safe_range(pre);
  transformer t_init = transformer_undefined;
 
  ifdebug(9) {
    print_effects(l_init_e);
    print_effects(l_expr_e);
  }
 
  el = gen_nconc(l_init_e, l_expr_e);
 
  ifdebug(9) {
    print_effects(el);
  }
 
  t_init =
    any_scalar_assign_to_transformer(loop_index(l),
                                     range_lower(loop_range(l)),
                                     el, /* over-approximation of effects */
                                     r_pre);
 
  ifdebug(9) {
    print_effects(el);
  }
 
  gen_free_list(el);
  /* free_effects() is not enough, because it is a persistant reference */
  free_reference(preference_reference(cell_preference(effect_cell(init_e))));
  free_effect(init_e);
  free_transformer(r_pre);
 
  return t_init;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_continue_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.

Parameters

pre

re

Definition at line 1501 of file loop.c.

{
  transformer t = transformer_identity();
  /* FI: the function transformer_add_loop_index_incrementation should
     be rewritten to exploit preconditions better. */
  t = transformer_add_loop_index_incrementation(t, l, pre);
  transformer et = loop_to_enter_transformer(l, pre);
  t = transformer_combine(t, et);
  free_transformer(et);
  return t;
}

References free_transformer(), loop_to_enter_transformer(), transformer_add_loop_index_incrementation(), transformer_combine(), and transformer_identity().

Referenced by new_loop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_enter_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.

Parameters

pre

re

Definition at line 1442 of file loop.c.

{
  entity i = loop_index(l);
  range r = loop_range(l);
  expression low = range_lower(r);
  expression up = range_upper(r);
  expression inc = range_increment(r);
  int il, iu;
  transformer t = transformer_identity();
 
  if(scalar_integer_type_p(entity_type(i))) {
 
    integer_expression_and_precondition_to_integer_interval(inc, pre, &il, &iu);
 
    if(il==iu && il==0) {
      /* A zero increment is not legal because the Fortran standard
         imposes a division by the increment. */
      /* Only the loop bopy statement number is available... */
      pips_user_error("Null increment for DO loop detected.\n");
    }
    else if(il>0||iu<0) {
      /* Assumption: no side effect in loop bound expressions */
      entity lv = make_local_temporary_value_entity(entity_type(i));
      transformer lt = safe_integer_expression_to_transformer(lv, low, pre, true);
      entity uv = make_local_temporary_value_entity(entity_type(i));
      transformer ut = safe_integer_expression_to_transformer(uv, up, pre, true);
 
      if(il>0) {
        /* The increment is strictly positive */
        t = transformer_add_inequality_with_linear_term(t, lv, i, 1, true);
        t = transformer_add_inequality_with_linear_term(t, i, uv, 1, true);
      }
      else if(iu<0) {
        /* The increment is strictly negative */
        t = transformer_add_inequality_with_linear_term(t, uv, i, 1, true);
        t = transformer_add_inequality_with_linear_term(t, i, lv, 1, true);
      }
      t = transformer_intersection(t, lt);
      t = transformer_intersection(t, ut);
      t = transformer_temporary_value_projection(t);
      //t = transformer_normalize(t, 0);
      t = transformer_normalize(t, 1);
      free_transformers(lt, ut, NULL);
    }
    else {
      /* The sign of the increment is unknown, no information is available */
      ;
    }
  }
  else {
    /* No information is available for loop indices that are not integer */
    /* This could be improved, but floating point indices should never
       be used. */
    ;
  }
 
  return t;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_initialization_transformer()

transformer loop_to_initialization_transformer	(	loop	l,
		transformer	pre
	)

Transformer expression the loop initialization.

Parameters

pre

re

Definition at line 1430 of file loop.c.

{
  entity i = loop_index(l);
  range r = loop_range(l);
  expression low = range_lower(r);
  transformer t = assigned_expression_to_transformer(i, low, pre);
  return t;
}

References assigned_expression_to_transformer(), loop_index, loop_range, and range_lower.

Referenced by new_loop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_postcondition()

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:

• it almost never happens in user code
• it's time consuming
• when it happens in automatically generated code, dead code elimination is performed.

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?

Parameters

pre	re
tf	f

Definition at line 2841 of file loop.c.

{
  transformer post = transformer_undefined;
  statement s = loop_body(l);
  range r = loop_range(l);
 
  pips_debug(8,"begin\n");
 
  if(pips_flag_p(SEMANTICS_FIX_POINT) && pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
    pips_internal_error("Halbwachs not implemented");
  }
  else {
    /* 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 */
    transformer preb = transformer_dup(pre);
 
    /* 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!
     */
    preb = transformer_combine(preb, tf);
 
    /* Triolet's good loop algorithm */
    preb = add_good_loop_conditions(preb, l);
 
    /* It might be useful to normalize preb and to detect unfeasibility.
     * I choose not to do it because:
     *  - it almost never happens in user code
     *  - it's time consuming
     *  - when it happens in automatically generated code,
     *    dead code elimination is performed.
     *
     * 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. */
    if(get_bool_property("SEMANTICS_RECOMPUTE_FIX_POINTS_WITH_PRECONDITIONS")) {
      transformer new_tf = recompute_loop_transformer(l, preb);
 
      free_transformer(preb);
      preb = transformer_dup(pre);
      preb = transformer_combine(preb, new_tf);
      preb = add_good_loop_conditions(preb, l);
    }
 
 
    /* 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.
     */
    if(empty_range_wrt_precondition_p(r, pre)) {
      pips_debug(8, "The loop is never executed\n");
 
      /* propagate an impossible precondition in the loop body */
      (void) statement_to_postcondition(transformer_empty(), s);
      /* The loop body precondition is not useful any longer */
      free_transformer(preb);
 
      transformer tmp = transformer_dup(pre);
      post = add_loop_index_initialization(tmp, l, pre);
      transformer_free(tmp);
    }
    else if(non_empty_range_wrt_precondition_p(r, pre)) {
      debug(8, "loop_to_postcondition", "The loop certainly is executed\n");
 
      /* propagate preconditions in the loop body and compute its postcondition... */
      post = statement_to_postcondition(preb, s);
 
      /* ... 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()!
       */
      transformer tmp = post;
      post = add_loop_index_exit_value(post, l, pre);
      transformer_free(tmp);
    }
    else {
      /* 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
       */
      /*
        transformer preloop = transformer_dup(pre);
        debug(8, "loop_to_postcondition", "The loop may be executed or not\n");
 
        post = transformer_convex_hull(postloop, preloop);
        transformer_free(postloop);
        transformer_free(preloop);
      */
 
      /* Second version: assume it is empty or non-empty and perform
       * the convex hull of both
       * (should be checked on Validation/Semantics/induc1.f)
       */
      transformer t_init = loop_initialization_to_transformer(l, pre);
      transformer post_ne = transformer_apply(t_init, pre);
      transformer post_al = transformer_undefined;
      transformer lpre = transformer_range(post_ne);
 
      pips_debug(8, "The loop may be executed or not\n");
 
      /* propagate preconditions in the loop body */
      post_al =  statement_to_postcondition(preb, s);
      /* 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
       */
      post_ne = add_loop_skip_condition(post_ne, l, lpre);
      // FI: already done with t_init
      //post_ne = add_loop_index_initialization(post_ne, l, lpre);
      free_transformer(lpre);
 
      transformer tmp = post_al;
      post_al = add_loop_index_exit_value(post_al, l, post_al);
      transformer_free(tmp);
 
      ifdebug(8) {
        (void) fprintf(stderr,"%s: %s\n","[loop_to_postcondition]",
                       "Never executed: post_ne %p =");
        (void) print_transformer(post_ne);
        (void) fprintf(stderr,"%s: %s\n","[loop_to_postcondition]",
                       "Always executed: post_al %p = ");
        (void) print_transformer(post_al);
      }
      post = transformer_convex_hull(post_ne, post_al);
      transformer_free(post_ne);
      transformer_free(post_al);
    }
 
    /* 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?
    */
  }
 
  ifdebug(8) {
    (void) fprintf(stderr,"%s: %s\n","[loop_to_postcondition]",
                   "resultat post =");
    (void) print_transformer(post);
  }
  pips_debug(8,"end\n");
  return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_total_precondition()

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

Parameters

t_post	_post
tf	f
context	ontext

Definition at line 3023 of file loop.c.

{
  transformer t_pre = transformer_undefined;
  statement b = loop_body(l);
  range r = loop_range(l);
 
  pips_debug(8,"begin\n");
 
  if(get_bool_property("SEMANTICS_RECOMPUTE_FIX_POINTS_WITH_PRECONDITIONS")) {
    transformer new_tf = transformer_undefined;
    transformer preb  = transformer_dup(context);
 
    preb = transformer_combine(preb, tf);
 
    /* Triolet's good loop algorithm */
    preb = add_good_loop_conditions(preb, l);
 
    new_tf = recompute_loop_transformer(l, preb);
 
    free_transformer(preb);
    /* preb = transformer_dup(pre); */
    preb = transformer_combine(preb, new_tf);
    preb = add_good_loop_conditions(preb, l);
  }
 
  if(empty_range_wrt_precondition_p(r, context)) { /* The loop is never executed */
    transformer tf_init = loop_initialization_to_transformer(l, context);
    transformer tf_empty = transformer_empty();
    transformer b_t_pre = transformer_undefined;
 
    pips_debug(8, "The loop is never executed\n");
 
    b_t_pre = statement_to_total_precondition(tf_empty, b);
    pips_assert("The body total precondition is consistent",
                transformer_consistency_p(b_t_pre));
 
    /* impact of loop index initialization, i.e. I = IT(J),.. or I = K/L,.. */
    t_pre = transformer_inverse_apply(tf_init, t_post);
    t_pre = transformer_to_domain(t_pre);
 
    free_transformer(tf_empty);
    free_transformer(tf_init);
  }
  else /* the loop may be entered for sure, or entered or not */ {
 
    transformer t_pre_ne = transformer_undefined;
    transformer t_pre_al = transformer_undefined;
    /* We need a fix_point without the initial condition but with the exit
       condition */
    transformer btf = transformer_dup(load_statement_transformer(b));
    transformer ltf = transformer_undefined;
    transformer b_t_post = transformer_undefined;
    transformer b_t_pre = transformer_undefined;
    transformer tf_init = loop_initialization_to_transformer(l, context);
 
    btf = transformer_add_loop_index_incrementation(btf, l, context);
    ltf =  (* transformer_fix_point_operator)(btf);
    ltf = add_loop_index_exit_value(ltf, l, context); /* Also performs
                                                         last
                                                         incrementation */
    b_t_post = transformer_inverse_apply(ltf, t_post);
    b_t_post = transformer_to_domain(b_t_post);
    b_t_pre = statement_to_total_precondition(b_t_post, b);
    pips_assert("The body total precondition is consistent",
                transformer_consistency_p(b_t_pre));
    t_pre_al = transformer_inverse_apply(tf_init, b_t_pre);
    t_pre_al = transformer_to_domain(t_pre_al);
 
    /* free_transformer(b_t_pre); it is associated to the loop body!*/
    free_transformer(b_t_post);
    free_transformer(btf);
    free_transformer(ltf);
 
    if(non_empty_range_wrt_precondition_p(r, context)) {
      /* The loop is always entered */
      t_pre = t_pre_al;
 
      pips_debug(8, "The loop certainly is executed\n");
    }
    else /* The loop may be skipped or entered */ {
 
      pips_debug(8, "The loop may be executed or not\n");
 
      /* skipped case computed here too */
      t_pre_ne = transformer_inverse_apply(tf_init, t_post);
      t_pre_ne = transformer_to_domain(t_pre_ne);
      t_pre_ne = add_loop_skip_condition(t_pre_ne, l, context);
 
 
      ifdebug(8) {
        (void) fprintf(stderr,"%s: %s\n","[loop_to_postcondition]",
                       "Never executed: t_pre_ne =");
        (void) print_transformer(t_pre_ne);
        (void) fprintf(stderr,"%s: %s\n","[loop_to_postcondition]",
                       "Always executed: post_al =");
        (void) print_transformer(t_pre_al);
      }
 
      t_pre = transformer_convex_hull(t_pre_ne, t_pre_al);
      transformer_free(t_pre_ne);
      transformer_free(t_pre_al);
    }
    free_transformer(tf_init);
  }
 
  ifdebug(8) {
    pips_debug(8, "resultat t_pre =%p", t_pre);
    (void) print_transformer(t_pre);
    pips_debug(8,"end\n");
  }
  return t_pre;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_transformer()

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

Parameters

pre

re

Definition at line 1319 of file loop.c.

{
  /* loop transformer tf = tfb* or tf = tfb+ or ... */
  transformer tf = transformer_undefined;
  /* loop body transformer */
  transformer tfb = transformer_undefined;
  /* approximate loop transformer, including loop index updates */
  transformer abtf = effects_to_transformer(e);
  /* loop body precondition */
  transformer preb = invariant_wrt_transformer(pre, abtf);
  /* Information about loop local variables is lost */
  list lv = loop_locals(l);
  /* range r = loop_range(l); */
  statement b = loop_body(l);
  transformer t_init = transformer_undefined;
  transformer old_tf = transformer_undefined;
 
  pips_debug(8,"begin with precondition pre=%p\n", pre);
  ifdebug(8) {
    (void) print_transformer(pre);
  }
 
  /* 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.
   */
  preb = safe_transformer_projection(preb, lv);
 
  /* compute the loop body transformer under loop body precondition preb */
  if(!transformer_undefined_p(preb))
    preb = add_good_loop_conditions(preb, l);
 
  pips_debug(8,"body precondition preb=%p\n", preb);
  ifdebug(8) {
    (void) print_transformer(preb);
  }
 
  tfb = statement_to_transformer(b, preb);
  /* add indexation step under loop precondition pre */
  tfb = transformer_add_loop_index_incrementation(tfb, l, pre);
 
  pips_debug(8,"body transformer tfb=%p\n", tfb);
  ifdebug(8) {
    (void) print_transformer(tfb);
  }
 
  /* compute tfb's fix point according to pips flags */
  tf = (* transformer_fix_point_operator)(tfb);
 
  free_transformer(tfb);
 
  ifdebug(8) {
    pips_debug(8, "intermediate fix-point tf=\n");
    fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
  }
 
  /* restrict the domain of tf by the range of pre, except for the loop
     index which is assigned in between */
  if(!transformer_undefined_p(pre)
     && get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT")) {
    list li = CONS(ENTITY, loop_index(l), NIL);
    transformer preb = transformer_filter(transformer_dup(pre), li);
    transformer r_pre = transformer_range(preb);
 
    tf = transformer_domain_intersection(tf, r_pre);
    free_transformer(r_pre);
    free_transformer(preb);
    gen_free_list(li);
  }
 
  /* add initialization for the unconditional initialization of the loop
     index variable */
  t_init = loop_initialization_to_transformer(l, pre);
  old_tf = tf;
  tf = transformer_combine(t_init, tf);
  tf = add_index_range_conditions(tf, loop_index(l), loop_range(l),
                                  load_statement_transformer(b));
  free_transformer(old_tf);
 
  /* 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 */
 
  ifdebug(8) {
    (void) fprintf(stderr,"%s: %s\n","loop_to_transformer",
                   "resultat tf =");
    (void) (void) print_transformer(tf);
    pips_debug(8,"end\n");
  }
 
  return tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

loop_to_transformer_list()

list loop_to_transformer_list	(	loop l	__attribute__(unused),
		transformer pre	__attribute__(unused),
		list e	__attribute__(unused)
	)

Definition at line 1420 of file loop.c.

{
  list tfl = NIL;
  pips_internal_error("Not implemented yet.");
  return tfl;
}

References NIL, and pips_internal_error.

new_complete_whileloop_transformer()

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

Parameters

t_body_star	_body_star
pre	re
wl	l
entered_p	ntered_p

Definition at line 1833 of file loop.c.

{
  list tfl =
    new_complete_whileloop_transformer_list(t_body_star, pre, wl, entered_p);
  transformer ct = transformer_list_to_transformer(tfl);
  // tfl is destroyed by transformer_list_to_transformer()
  return ct;
}

References new_complete_whileloop_transformer_list(), and transformer_list_to_transformer().

Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

new_complete_whileloop_transformer_list()

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.

{
  list tfl = NIL;
  //transformer ct = transformer_undefined;
  statement body_s = whileloop_body(wl);
  transformer t_body = load_statement_transformer(body_s);
  transformer ct_body = transformer_undefined;
  transformer pre_body = transformer_undefined;
  transformer post_body = transformer_undefined;
  transformer t_init = transformer_identity();
  expression cond_e = whileloop_condition(wl);
  //transformer t_skip = entered_p?
  //  transformer_empty() : condition_to_transformer(cond_e, pre, false);
  transformer t_skip = condition_to_transformer(cond_e, pre, false);
  transformer t_enter = condition_to_transformer(cond_e, pre, true);
  /* An effort could be made to compute the preconditions for t_continue and t_exit: see while04.c. */
  //transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  //transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  transformer t_continue = transformer_undefined;
  transformer t_exit = transformer_undefined;
  transformer t_inc = transformer_identity();
 
  /* Make sure you have the effective statement transformer: it is not
     stored for loops and this is key for nested loops. */
  pre_body = transformer_apply(t_body_star, pre);
  /* Should we instead compute recursively a transformer list? */
  ct_body = complete_statement_transformer(t_body, pre_body, body_s);
 
  post_body = transformer_apply(ct_body, pre_body);
  t_continue = condition_to_transformer(cond_e, post_body, true);
  t_exit = condition_to_transformer(cond_e, post_body, false);
 
  tfl = complete_any_loop_transformer_list(t_init, t_skip, t_body_star,
                                           ct_body, t_inc, t_exit);
 
  free_transformer(ct_body);
  free_transformer(pre_body);
  free_transformer(post_body);
  free_transformer(t_init);
  free_transformer(t_skip);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(t_exit);
  free_transformer(t_inc);
 
  return tfl;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

new_loop_to_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

Parameters

pre	re
lel	el

Definition at line 1516 of file loop.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.
   */
  transformer t_body_star = transformer_undefined;
  statement body_s = loop_body(l);
 
  /* 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 */
  transformer t_init = loop_to_initialization_transformer(l, pre);
  // FI Memory leak
  transformer post_i = transformer_range(transformer_apply(t_init, pre));
 
  /* Deal with enter transformers */
  transformer t_enter = loop_to_enter_transformer(l, post_i);
  transformer pre_b = transformer_apply(t_enter, post_i);
 
  /* An effort could be made to compute the precondition for t_continue. 
   * Precondition pre and the loop effect list lel could be used.
   */
  //transformer p_continue = transformer_identity();
  /* approximate loop transformer, including loop index updates */
  transformer abtf = effects_to_transformer(lel);
  /* first approximation of the loop body precondition */
  // invariant_wrt_transformer() seems to add arguments to the
  // filtered precondition...
  // FI: memory leak
  transformer p_continue = transformer_range(invariant_wrt_transformer(pre_b, abtf));
  /* FI: could do better with body_transformer */
  transformer t_continue = loop_to_continue_transformer(l, p_continue);
 
  t_body_star = any_loop_to_transformer(t_init, t_enter, t_continue, body_s, lel, pre_b);
 
  /* Let's clean up the memory */
 
  free_transformer(p_continue);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(post_i);
  free_transformer(pre_b);
 
  return t_body_star;
}

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.

Here is the call graph for this function:

new_whileloop_to_k_transformer()

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

Parameters

wl	l
pre	re
wlel	lel
k	effects of whileloop wl

Definition at line 416 of file loop.c.

{
  /* t_body_star =  t_init ; t_enter ;(t_body ; t_next)* */
  transformer t_body_star = transformer_undefined;
  statement body_s = whileloop_body(wl);
 
  /* Deal with initialization expression */
  transformer t_init = transformer_identity();
 
  /* Deal with condition expression */
  expression cond_e = whileloop_condition(wl);
  transformer t_enter = condition_to_transformer(cond_e, pre, true);
  /* An effort could be made to compute the precondition for t_continue. */
  transformer p_continue = transformer_identity();
  transformer t_continue = condition_to_transformer(cond_e, p_continue, true);
 
  t_body_star = any_loop_to_k_transformer(t_init, t_enter, t_continue, body_s, wlel, pre, k);
 
  /* Let's clean up the memory */
 
  free_transformer(p_continue);
 
  free_transformer(t_enter);
  free_transformer(t_continue);
 
  return t_body_star;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

new_whileloop_to_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

Parameters

wl	l
pre	re
wlel	lel

Definition at line 380 of file loop.c.

{
  /* Equation:
   *
   * t_body_star =  t_init ; t_enter ;(t_body ; t_continue)*
   */
  transformer t_body_star = transformer_undefined;
  statement body_s = whileloop_body(wl);
 
  /* 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 */
  transformer t_init = transformer_identity();
 
  /* Deal with condition expression */
  expression cond_e = whileloop_condition(wl);
  transformer t_enter = condition_to_transformer(cond_e, pre, true);
  /* An effort could be made to compute the precondition for t_continue. */
  transformer p_continue = transformer_identity();
  transformer t_continue = condition_to_transformer(cond_e, p_continue, true);
 
  t_body_star = any_loop_to_transformer(t_init, t_enter, t_continue, body_s, wlel, pre);
 
  /* Let's clean up the memory */
 
  free_transformer(p_continue);
 
  free_transformer(t_enter);
  free_transformer(t_continue);
 
  return t_body_star;
}

References any_loop_to_transformer(), condition_to_transformer(), free_transformer(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.

Referenced by whileloop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

old_complete_whileloop_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.

Parameters

ltf	tf
pre	re

Definition at line 2213 of file loop.c.

{
  transformer tf = transformer_undefined;
  transformer t_enter = transformer_undefined;
  transformer t_skip = transformer_undefined;
  /* loop body transformer */
  transformer btf = transformer_undefined;
  expression cond = whileloop_condition(l);
  statement s = whileloop_body(l);
  transformer preb = invariant_wrt_transformer(pre, ltf);
 
  pips_debug(8,"begin with whileloop precondition\n");
  ifdebug(8) {
    (void) print_transformer(pre);
    pips_debug(8,"and whileloop transformer:\n");
    (void) print_transformer(ltf);
  }
 
  /* 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). */
  if(statement_loop_p(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! */
    loop il = instruction_loop(statement_instruction(s));
    btf = complete_loop_transformer(load_statement_transformer(s), pre, il);
  }
  else if(statement_whileloop_p(s)) {
    whileloop il = instruction_whileloop(statement_instruction(s));
    btf = complete_whileloop_transformer(load_statement_transformer(s), pre, il);
  }
  else { /* The proper transformer has been stored. */
    btf = transformer_dup(load_statement_transformer(s));
  }
 
  /* btf = transformer_add_condition_information(btf, cond, preb, true); */
  t_enter = transformer_combine(transformer_dup(ltf), btf);
 
  ifdebug(8) {
    pips_debug(8, "entered loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* add the exit condition */
  t_enter =  transformer_add_condition_information(t_enter, cond, preb, false);
 
  ifdebug(8) {
    pips_debug(8, "entered and exited loop transformer t_enter=\n");
    fprint_transformer(stderr, t_enter, (get_variable_name_t) external_value_name);
  }
 
  /* add initialization for the unconditional initialization of the loop
     index variable */
  t_skip = transformer_undefined_p(pre)?
    transformer_identity() :
    transformer_dup(pre);
  t_skip = transformer_add_condition_information(t_skip, cond, pre, false);
 
  ifdebug(8) {
    pips_debug(8, "skipped loop transformer t_skip=\n");
    fprint_transformer(stderr, t_skip, (get_variable_name_t) external_value_name);
  }
 
  /* 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. */
  if(!transformer_undefined_p(pre) && condition_false_wrt_precondition_p(cond, pre)) {
    tf = t_skip;
    free_transformer(t_enter);
  }
  else if(!transformer_undefined_p(pre) && condition_true_wrt_precondition_p(cond, pre)) {
    tf = t_enter;
    free_transformer(t_skip);
  }
  else {
    tf = transformer_convex_hull(t_enter, t_skip);
    free_transformer(t_enter);
    free_transformer(t_skip);
  }
 
  ifdebug(8) {
    pips_debug(8, "full refined loop transformer tf=\n");
    fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
    pips_debug(8, "end\n");
  }
 
  return tf;
}

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.

Here is the call graph for this function:

precondition_filter_old_values()

transformer precondition_filter_old_values

(

transformer

pre

)

Parameters

pre

re

Definition at line 1065 of file loop.c.

{
    Psysteme sc = predicate_system(transformer_relation(pre));
    Pbase b = BASE_UNDEFINED;
 
    for(b = sc_base(sc); !BASE_NULLE_P(b); b = vecteur_succ(b)) {
      entity old_v = (entity) vecteur_var(b);
 
      if(old_value_entity_p(old_v)) {
        pips_assert("No old values are left", false);
      }
    }
 
    return pre;
}

References BASE_NULLE_P, BASE_UNDEFINED, old_value_entity_p(), pips_assert, predicate_system, transformer_relation, vecteur_succ, and vecteur_var.

Here is the call graph for this function:

recompute_loop_transformer()

static transformer recompute_loop_transformer ( loop  l, transformer  pre  )

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.

{
  statement s = loop_body(l);
  entity i = loop_index(l);
  list list_mod = list_undefined;
  list list_old = list_undefined;
  list list_projectable = list_undefined;
  list list_val = list_undefined;
  transformer tf = load_statement_transformer(s);
  transformer tfb = transformer_add_loop_index_incrementation(transformer_dup(tf), l, pre);
  transformer new_tf = transformer_undefined;
  transformer preb = transformer_dup(pre);
  Psysteme sc_pre = SC_UNDEFINED;
  Psysteme sc = predicate_system(transformer_relation(tfb));
  
  ifdebug(5) {
    pips_debug(5, "Begin with precondition:\n");
    print_transformer(pre);
    pips_assert("Precondition pre is consistent", 
                transformer_internal_consistency_p(pre));
    pips_debug(5, "and transformer:\n");
    print_transformer(tf);
  }
 
  /* get rid of information modified by the loop body or the loop header */
  list_mod = dup_arguments(transformer_arguments(tf));
  arguments_add_entity(list_mod, i);
  gen_list_and(&list_mod, transformer_arguments(preb));
  ifdebug(5) {
    pips_debug(5, "Variables eliminated from the preconditions"
               " because they are modified by tf:");
    print_arguments(list_mod);
  }
  list_val = variables_to_values(list_mod);
  /* get rid of old values in preb which are meaning less in tf */
  list_old = arguments_difference(transformer_arguments(preb),
                                  transformer_arguments(tf));
  ifdebug(5) {
    pips_debug(5, "Variables eliminated from the preconditions"
               " because they are linked to the module entry point:");
    print_arguments(list_old);
  }
  /* do not try to eliminate the same variable twice */
  gen_list_and_not(&list_old, list_mod);
 
  list_val = gen_nconc(list_val, variables_to_old_values(list_old));
  ifdebug(5) {
    pips_debug(5, "Values which should be eliminated from the preconditions:");
    print_arguments(list_val);
  }
  /* Not all values can be projected in preb because some may appear in tf
     and not in preb */
  list_projectable = transformer_projectable_values(preb);
  gen_list_and(&list_val, list_projectable);
  ifdebug(5) {
    pips_debug(5, "Values which can be eliminated from the preconditions:");
    print_arguments(list_val);
  }
  preb = transformer_projection(preb, list_val);
 
  /* add the remaining conditional information to the loop transformer */
  sc_pre = predicate_system(transformer_relation(preb));
  sc = sc_append(sc, sc_pre);
  predicate_system(transformer_relation(tfb)) = sc;
  ifdebug(1) {
    if(!transformer_internal_consistency_p(tfb)) {
      print_transformer(tfb);
      sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
    }
    pips_assert("Conditional loop body transformer is consistent",
                transformer_internal_consistency_p(tfb));
  }
 
  tfb = transformer_add_loop_index_incrementation(tfb, l, pre);
 
  new_tf = (* transformer_fix_point_operator)(tfb);
  new_tf = transformer_add_loop_index_initialization(new_tf, l, pre);
 
  free_transformer(preb);
  gen_free_list(list_mod);
  gen_free_list(list_val);
 
  ifdebug(5) {
    pips_debug(5, "End with fixpoint:\n");
    print_transformer(new_tf);
  }
 
  return new_tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

repeatloop_to_postcondition()

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

Parameters

pre	re
wl	l
t_body_star	_body_star

Definition at line 2760 of file loop.c.

{
  transformer post = transformer_undefined;
 
  statement body_s = whileloop_body(wl);
  transformer t_body = load_statement_transformer(body_s);
  transformer t_body_c = complete_statement_transformer(t_body, pre, body_s);
  transformer t_init = transformer_identity();
  transformer post_init = copy_transformer(pre);
  expression cond_e = whileloop_condition(wl);
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  transformer t_skip = transformer_empty();
  //transformer t_skip = transformer_combine(copy_transformer(t_body), t_exit);
  transformer t_enter = transformer_identity();
  //transformer t_enter = transformer_combine(copy_transformer(t_body), t_continue);
  /* An effort could be made to compute the precondition for t_exit,
     especially if the precondition to t_inc is available. */
  transformer t_inc = transformer_identity();
  transformer post_1 = transformer_undefined;
  transformer post_2 = transformer_undefined;
  transformer post_3 = transformer_undefined;
  transformer post_4 = transformer_undefined;
  transformer post_5 = transformer_undefined;
  transformer post_6 = transformer_undefined;
 
  post = any_loop_to_postcondition(body_s,
                                   t_init,
                                   t_enter,
                                   t_skip,
                                   t_body_star,
                                   t_body_c,
                                   t_continue, //since t_inc is ineffective
                                   t_inc,
                                   t_exit,
                                   pre);
 
  /* 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. 
   */
 
  free_transformer(post);
 
  post_1 = transformer_apply(t_body_c, pre);
  post_2 = transformer_apply(t_exit, post_1);
 
  post_3 = transformer_apply(t_continue, post_1);
  post_4 = transformer_apply(t_body_star, post_3);
  post_5 = transformer_apply(t_body_c, post_4);
  post_6 = transformer_apply(t_exit, post_5);
 
  post = transformer_convex_hull(post_2, post_6);
 
  /* Clean up memory */
 
  free_transformer(t_init);
  free_transformer(post_init);
  free_transformer(t_skip);
  free_transformer(t_enter);
  free_transformer(t_continue);
  free_transformer(t_exit);
  free_transformer(t_inc);
  free_transformer(t_body_c);
 
  free_transformer(post_1);
  free_transformer(post_2);
  free_transformer(post_3);
  free_transformer(post_4);
  free_transformer(post_5);
  free_transformer(post_6);
 
    return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

repeatloop_to_transformer()

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

Parameters

wl	l
pre	re
wlel	lel

Definition at line 449 of file loop.c.

{
  /* t_body_star =  t_init ; t_enter ; (t_body ; t_next)+
   *
   * t_once = t_body; t_exit
   *
   * t_repeat = t_body_star + t_once
   */
  transformer t_body_star = transformer_undefined;
  statement body_s = whileloop_body(wl);
  transformer t_body = transformer_undefined; // load_statement_transformer(body_s);
  transformer t_init = transformer_identity();
  expression cond_e = whileloop_condition(wl);
  transformer t_enter = transformer_identity();
  /* An effort could be made to compute the precondition for t_continue,
     especially if the precondition to t_inc is available. */
  transformer t_continue = condition_to_transformer(cond_e, transformer_undefined, true);
  /* FI: it should be computed with the postcondition of the body */
  transformer t_exit = condition_to_transformer(cond_e, transformer_undefined, false);
  //transformer t_inc = transformer_identity();
  transformer t_next = t_continue;
 
  /* 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 */
  t_body_star = any_loop_to_transformer(t_init, t_enter, t_next, body_s, wlel, pre);
 
  /* The loop is executed only once */
  // any_loop_to_transformer() has computed the body transformer
  t_body = load_statement_transformer(body_s);
  transformer t_once = transformer_combine(copy_transformer(t_body), t_exit);
 
  /* global transformer */
  transformer t_repeat = transformer_convex_hull(t_once, t_body_star);
 
  // free_transformer(t_once), free_transformer(t_body_star), free_transformer(t_next), free_transformer(t_exit), free_transformer(t_enter);
 
  return t_repeat;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

simple_dead_loop_p()

bool simple_dead_loop_p	(	expression	lower,
		expression	upper
	)

Parameters

lower	ower
upper	pper

Definition at line 1028 of file loop.c.

{
  bool dead_loop_p = false;
  normalized n_lower = NORMALIZE_EXPRESSION(lower);
  normalized n_upper = NORMALIZE_EXPRESSION(upper);
 
  if(normalized_linear_p(n_upper) && normalized_linear_p(n_lower)) {
    Pvecteur v_lower = normalized_linear(n_lower);
    Pvecteur v_upper = normalized_linear(n_upper);
 
    if(VECTEUR_NUL_P(v_lower)) {
      if (!VECTEUR_NUL_P(v_upper)) {
        if(term_cst(v_upper)
           && VECTEUR_NUL_P(vecteur_succ(v_upper))) {
          dead_loop_p =  value_neg_p(vecteur_val(v_upper));
        }
      }
    }
    else if(VECTEUR_NUL_P(v_upper)) {
      if (!VECTEUR_NUL_P(v_lower)) {
        if(term_cst(v_lower)
           && VECTEUR_NUL_P(vecteur_succ(v_lower))) {
          dead_loop_p =  value_pos_p(vecteur_val(v_lower));
        }
      }
    }
    else if(term_cst(v_upper) && term_cst(v_lower)
            && VECTEUR_NUL_P(vecteur_succ(v_upper))
            && VECTEUR_NUL_P(vecteur_succ(v_lower))) {
      dead_loop_p =
        value_gt(vecteur_val(v_lower),vecteur_val(v_upper));
    }
  }
 
  return dead_loop_p;
}

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().

Here is the caller graph for this function:

standard_whileloop_to_transformer()

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?

Parameters

pre

re

Definition at line 2456 of file loop.c.

{
  /* loop transformer tf = tfb* or tf = tfb+ or ... */
  transformer tf;
  /* loop body transformer */
  transformer tfb;
  expression cond = whileloop_condition(l);
  statement s = whileloop_body(l);
 
  pips_debug(8,"begin\n");
 
  if(pips_flag_p(SEMANTICS_FIX_POINT)) {
    transformer pre_n = transformer_undefined;
 
    if(transformer_undefined_p(pre)) {
      pre_n = transformer_identity();
    }
    else {
      /* Make sure not to leave too much information in pre. Perform a very
         simplistic fix point based on effects. */
      transformer tf_star = effects_to_transformer(e);
 
      pre_n = invariant_wrt_transformer(pre, tf_star);
      free_transformer(tf_star);
    }
    /* 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! */
    pre_n = precondition_add_condition_information(pre_n, cond,
                                                   transformer_undefined, true);
 
    ifdebug(8) {
      pips_debug(8, "Precondition for loop body pre_n=\n");
      fprint_transformer(stderr, pre_n, (get_variable_name_t) external_value_name);
    }
 
    /* compute the whileloop body transformer, including the initial conditions */
    tfb = transformer_dup(statement_to_transformer(s, pre_n));
 
    /* 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 */
    if(!transformer_undefined_p(pre))
      tfb = loop_body_transformer_add_entry_and_iteration_information(tfb, pre);
 
    /* compute tfb's fix point according to pips flags */
    if(pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
      tf = transformer_halbwachs_fix_point(tfb);
    }
    else if ((!transformer_undefined_p(pre)
             && condition_false_wrt_precondition_p(cond, pre))
             /* The second clause is probably stronger than the first one */
             || transformer_empty_p(pre_n)) {
      /* The loop is never entered */
      /* Side effects of the condition evaluation should be taken into account */
      tf = transformer_identity();
      /* A temporary variable is expected as first argument. There is something to fix. */
      /* tf = any_expression_to_transformer(); */
    }
    else if(transformer_empty_p(tfb)) {
      /* The loop is never exited, e.g. because there is a STOP or an infinite loop inside */
      tf = transformer_empty();
    }
    else {
      transformer ftf = (* transformer_fix_point_operator)(tfb);
 
      if(*transformer_fix_point_operator==transformer_equality_fix_point) {
        Psysteme fsc = predicate_system(transformer_relation(ftf));
        Psysteme sc = SC_UNDEFINED;
 
        /* 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.
         */
        tf = effects_to_transformer(e);
        sc = (Psysteme) predicate_system(transformer_relation(tf));
 
        sc = sc_append(sc, fsc);
 
        free_transformer(ftf);
      }
      else {
        tf = ftf;
      }
 
      ifdebug(8) {
        pips_debug(8, "intermediate fix-point tf=\n");
        fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
      }
 
    }
 
    free_transformer(pre_n);
 
    /* 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 */
  }
  else {
    /* 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? */
    (void) statement_to_transformer(s, transformer_undefined);
    tf = effects_to_transformer(e);
  }
 
  ifdebug(8) {
    (void) fprintf(stderr,"%s: %s\n","standard_whileloop_to_transformer",
                   "resultat tf =");
    (void) print_transformer(tf);
  }
  pips_debug(8,"end\n");
  return tf;
}

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.

Here is the call graph for this function:

transformer_add_loop_index_incrementation()

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

Parameters

tf	f
pre	re

Definition at line 1136 of file loop.c.

{
  entity i = loop_index(l);
  range r = loop_range(l);
  expression incr = range_increment(r);
  Pvecteur v_incr = VECTEUR_UNDEFINED;
 
  /* SHOULD BE REWRITTEN WITH EXPRESSION_TO_TRANSFORMER */
 
  pips_assert("To please the compiler", pre==pre);
 
  pips_assert("Transformer tf is consistent before update",
              transformer_consistency_p(tf));
 
  /* it does not contain the loop index update the loop increment
     expression must be linear to find inductive variables related to
     the loop index */
  if(!VECTEUR_UNDEFINED_P(v_incr = expression_to_affine(incr))) {
    if(entity_has_values_p(i)) {
      if(value_mappings_compatible_vector_p(v_incr)) {
        tf = transformer_add_variable_incrementation(tf, i, v_incr);
      }
      else {
        entity i_old = entity_to_old_value(i);
        entity i_new = entity_to_new_value(i);
        Psysteme sc = predicate_system(transformer_relation(tf));
        Pbase b = sc_base(sc);
 
        transformer_arguments(tf) = arguments_add_entity(transformer_arguments(tf), i);
        b = base_add_variable(b, (Variable) i_old);
        b = base_add_variable(b, (Variable) i_new);
        sc_base(sc) = b;
        sc_dimension(sc) = base_dimension(sc_base(sc));
      }
    }
    else {
      pips_user_warning("non-integer or equivalenced loop index %s?\n",
                        entity_local_name(i));
    }
  }
  else {
    if(entity_has_values_p(i)) {
      entity i_old = entity_to_old_value(i);
      entity i_new = entity_to_new_value(i);
      Psysteme sc = predicate_system(transformer_relation(tf));
      Pbase b = sc_base(sc);
 
      transformer_arguments(tf) = arguments_add_entity(transformer_arguments(tf), i);
      b = base_add_variable(b, (Variable) i_old);
      b = base_add_variable(b, (Variable) i_new);
      sc_base(sc) = b;
      sc_dimension(sc) = base_dimension(sc_base(sc));
    }
  }
 
  pips_assert("Transformer tf is consistent after update",
              transformer_consistency_p(tf));
 
  return tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_add_loop_index_initialization()

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

Parameters

tf	f
pre	re

Definition at line 1082 of file loop.c.

{
  entity i = loop_index(l);
  range r = loop_range(l);
  normalized nlb = NORMALIZE_EXPRESSION(range_lower(r));
 
  /* EXPRESSION_TO_TRANSFORMER SHOULD BE USED */
  pips_assert("To please the compiler", pre==pre);
 
  if(entity_has_values_p(i) && normalized_linear_p(nlb)) {
    Psysteme sc = (Psysteme) predicate_system(transformer_relation(tf));
    Pcontrainte eq = CONTRAINTE_UNDEFINED;
    Pvecteur v_lb = vect_dup(normalized_linear(nlb));
    Pbase b_tmp, b_lb = make_base_from_vect(v_lb);
    entity i_init = entity_to_old_value(i);
 
    vect_add_elem(&v_lb, (Variable) i_init, VALUE_MONE);
    eq = contrainte_make(v_lb);
    /* 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 */
    sc = sc_projection_by_eq(sc, eq, (Variable) i_init);
    b_tmp = sc_base(sc);
    sc_base(sc) = base_union(b_tmp, b_lb);
    sc_dimension(sc) = base_dimension(sc_base(sc));
    base_rm(b_tmp);
    base_rm(b_lb);
    if(SC_RN_P(sc)) {
      /* FI: a NULL is not acceptable; I assume that we cannot
       * end up with a SC_EMPTY...
       */
      predicate_system_(transformer_relation(tf)) =
        newgen_Psysteme
        (sc_make(CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED));
    }
    else
      predicate_system_(transformer_relation(tf)) =
        newgen_Psysteme(sc);
  }
  else if(entity_has_values_p(i)) {
    /* Get rid of the initial value since it is unknowable */
    entity i_init = entity_to_old_value(i);
    list l_i_init = CONS(ENTITY, i_init, NIL);
 
    tf = transformer_projection(tf, l_i_init);
  }
 
return tf;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

whileloop_to_k_transformer()

transformer whileloop_to_k_transformer	(	whileloop	l,
		transformer	pre,
		list	e,
		int	k
	)

Parameters

pre	re
k	effects of whileloop l

Definition at line 2617 of file loop.c.

{
  transformer t = transformer_undefined;
  evaluation lt = whileloop_evaluation(l);
 
  if(evaluation_before_p(lt))
    t = new_whileloop_to_k_transformer(l, pre, e, k);
  else
    pips_internal_error("repeatloop_to_k_transformer() not implemented.");
    //t = repeatloop_to_k_transformer(l, pre, e);
  return t;
}

References evaluation_before_p, new_whileloop_to_k_transformer(), pips_internal_error, transformer_undefined, and whileloop_evaluation.

Referenced by whileloop_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

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:

• use the loop body postcondition and apply the loop exit condition transformer or precondition_add_condition_information;
• or use the loop precondition, the loop transformer, the loop entry condition, the loop body transformer and the loop exit transformer;

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

Parameters

pre	re
tf	f

Definition at line 3141 of file loop.c.

{
  transformer post = transformer_undefined;
  statement s = whileloop_body(l);
  expression c = whileloop_condition(l);
 
  pips_debug(8, "begin\n");
 
  if(pips_flag_p(SEMANTICS_FIX_POINT)
     && pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
    pips_internal_error("Halbwachs not implemented");
  }
 
  if(false_condition_wrt_precondition_p(c, pre)) {
    transformer c_t = condition_to_transformer(c, pre, false);
    pips_debug(8, "The loop is never executed\n");
 
    /* propagate an impossible precondition in the loop body */
    (void) statement_to_postcondition(transformer_empty(), s);
    /* 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 */
    post = transformer_combine(copy_transformer(pre), c_t);
    //post = transformer_apply(c_t, pre);
    free_transformer(c_t);
  }
  else { /* The loop may be entered at least once. */
    transformer pre_next = transformer_dup(pre);
    transformer pre_init =
      precondition_add_condition_information(transformer_dup(pre),
                                             c, pre, true);
    // FI: this should work but is not compatible with the following
    //code; by definition, tf also include the side effect of pre
    //transformer pre_init = transformer_apply(c_t, pre);
    transformer preb = transformer_undefined; // body precondition
    transformer postb = transformer_undefined; // body postcondition
    transformer tb = load_statement_transformer(s); // body transformer
    int k = get_int_property("SEMANTICS_K_FIX_POINT");
 
    /* 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.
    */
    transformer pre_fuzzy = transformer_apply(tf, pre);
    //tb = complete_non_identity_statement_transformer(tb, pre_fuzzy, s);
    list btl = list_undefined;
    int fbtll = 0;
 
    if(get_bool_property("SEMANTICS_USE_TRANSFORMER_LISTS")) {
      list fbtl = statement_to_transformer_list(s, pre_fuzzy);
      fbtll = (int) gen_length(fbtl);
      // filter out transformers that do not modify the state
      // FI: this is not a general approach since it depends on the
      // framework used and on the other variables, but it helps!
      btl = transformer_list_to_active_transformer_list(fbtl);
      gen_full_free_list(fbtl);
 
      if(gen_length(btl)==0) {
        tb = empty_transformer(transformer_identity());
      }
      else if(gen_length(btl)==1) {
        /* Nothing special in the loop body: no tests, no while,... */
        if(fbtll==1)
          tb = complete_statement_transformer(tb, pre_fuzzy, s);
        else
          // FI: not to sure about reuse and memory leaks...
          tb = copy_transformer(TRANSFORMER(CAR(btl)));
      }
      else {
        /* 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 */
        tb = active_transformer_list_to_transformer(gen_full_copy_list(btl));
      }
    }
    else {
      tb = complete_statement_transformer(tb, pre_fuzzy, s);
    }
 
    pips_debug(8, "The loop may be executed and preconditions must"
               " be propagated in the loop body\n");
 
    if(k==1) {
      if(!get_bool_property("SEMANTICS_USE_TRANSFORMER_LISTS")
         || gen_length(btl)==1) {
        /* 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.
         */
        // FI: I do not know why pre_next==pre is used instead of
        // pre_init==P_0 in the statement just below
        pre_next = transformer_combine(pre_next, tf);
        pre_next = precondition_add_condition_information(pre_next, c,
                                                          pre_next, true);
        pre_next = transformer_combine(pre_next, tb);
        pre_next = precondition_add_condition_information(pre_next, c,
                                                          pre_next, true);
        preb = transformer_convex_hull(pre_init, pre_next);
      }
      else { // transformer lists are used and at least two
             // transformers have been found
        transformer c_t = condition_to_transformer(c, pre_fuzzy, true);
        //transformer preb1 = transformer_list_closure_to_precondition(btl, c_t, pre_init);
        transformer preb1 = transformer_list_multiple_closure_to_precondition(btl, c_t, pre_init);
        //pre_next = transformer_combine(pre_next, tf);
        //pre_next = precondition_add_condition_information(pre_next, c,
        //                                                pre_next, true);
      //pre_next = transformer_combine(pre_next, tb);
      //pre_next = precondition_add_condition_information(pre_next, c,
        //                                        pre_next, true);
    //transformer preb2 = transformer_convex_hull(pre_init, pre_next);
    //pips_assert("The two preconditions have the same arguments",
    //              arguments_equal_p(transformer_arguments(preb1),
    //                        transformer_arguments(preb2)));
        // FI: the intersection generates overflows
        //preb = transformer_intersection(preb1, preb2);
        preb = preb1;
      }
    }
    else if (k==2) {
      /* 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.
      */
      list bel = load_cumulated_rw_effects_list(s); // Should be lel
      transformer tf2 = whileloop_to_k_transformer(l, pre, bel, 2);
      transformer pre_next2 = transformer_undefined;
      pre_next = transformer_combine(pre_next, tf2);
      pre_next = precondition_add_condition_information(pre_next, c,
                                                        pre_next, true);
      pre_next = transformer_combine(pre_next, tb);
      pre_next = precondition_add_condition_information(pre_next, c,
                                                        pre_next, true);
      preb = transformer_convex_hull(pre_init, pre_next);
 
      /* FI: since pre_next is no longer useful, pre_next2 could be
         avoided. It just makes debugging easier. */
      pre_next2 = copy_transformer(pre_next);
      pre_next2 = precondition_add_condition_information(pre_next2, c,
                                                         pre_next2, true);
      pre_next2 = transformer_combine(pre_next2, tb);
      pre_next2 = precondition_add_condition_information(pre_next2, c,
                                                         pre_next2, true);
      preb = transformer_convex_hull(preb, pre_next2);
      free_transformer(tf2);
      free_transformer(pre_next2);
    }
    else
      pips_user_error("Unexpected value %d for k.\n", k);
 
    free_transformer(pre_fuzzy);
 
    /* propagate preconditions in the loop body and get its postcondition */
 
    postb = statement_to_postcondition(preb, s);
 
    if(true_condition_wrt_precondition_p(c, pre)) {
      /* At least one iteration is executed. The postcondition can be
       * computed into three different ways:
       *
       *  - use the loop body postcondition and apply the loop exit
       * condition transformer or precondition_add_condition_information;
       *
       *  - or use the loop precondition, the loop transformer, the loop
       * entry condition, the loop body transformer and the loop exit
       * transformer;
       *
       * - 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.
       */
 
      pips_debug(8, "The loop certainly is executed.\n");
 
      if(false) {
        transformer ntl = transformer_undefined;
        transformer cpost = transformer_undefined; // combined postcondition
        ntl = transformer_apply(tf, pre);
        /* Let's execute the last iteration since it certainly exists */
        ntl = precondition_add_condition_information(ntl, c, ntl, true);
        post = transformer_apply(tb, ntl);
        free_transformer(ntl);
        post = precondition_add_condition_information(post, c, post, false);
 
        postb = precondition_add_condition_information(postb, c, postb, false);
 
        cpost = transformer_intersection(post, postb);
 
        free_transformer(post);
        free_transformer(postb);
 
        post = cpost;
      }
      else {
        // FI: does not work with side effects
        //post = precondition_add_condition_information(postb, c, postb, false);
        transformer pre_c = transformer_range(postb);
        transformer ctf = condition_to_transformer(c, pre_c, false);
        post = transformer_apply(ctf, postb);
        free_transformer(pre_c);
        free_transformer(ctf);
      }
    }
    else {
      /* Assume the loop is entered, post_al, or not, post_ne, and perform
       * the convex hull of both
       */
      transformer post_ne = transformer_dup(pre);
      transformer post_al = transformer_undefined;
      //transformer tb = load_statement_transformer(s);
 
      pips_debug(8, "The loop may be executed or not\n");
 
      /* The loop is executed at least once: let's execute the last iteration */
      //post_al = transformer_apply(tb, preb);
 
        // FI: does not work with side effects
        //post = precondition_add_condition_information(postb, c, postb, false);
        transformer pre_c = transformer_range(postb);
        transformer ctf = condition_to_transformer(c, pre_c, false);
        // Mmeory leak? Do we still need postb?
        post_al = transformer_apply(ctf, postb);
        free_transformer(pre_c);
        free_transformer(ctf);
        // post_al = precondition_add_condition_information(postb, c, postb, false);
 
      /* The loop is never executed */
        // FI: does not work with side effects
        // post_ne = precondition_add_condition_information(post_ne, c, post_ne, false);
        pre_c = transformer_range(post_ne);
        ctf = condition_to_transformer(c, pre_c, false);
        // Mmeory leak
        post_ne = transformer_apply(ctf, post_ne);
        free_transformer(pre_c);
        free_transformer(ctf);
 
      post = transformer_convex_hull(post_ne, post_al);
      // free for postb too? hidden within post_al?
      transformer_free(post_ne);
      transformer_free(post_al);
    }
  }
 
  ifdebug(8) {
    pips_debug(8, "resultat post =");
    (void) print_transformer(post);
  }
  pips_debug(8, "end\n");
  return post;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

whileloop_to_total_precondition()

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);

Parameters

t_post	_post
tf	f
context	ontext

Definition at line 3439 of file loop.c.

{
  transformer t_pre = transformer_undefined;
  statement s = whileloop_body(l);
  expression c = whileloop_condition(l);
 
  pips_assert("not implemented yet", false && t_post==t_post);
 
  pips_debug(8,"begin\n");
 
  if(pips_flag_p(SEMANTICS_FIX_POINT) && pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
    pips_internal_error("Halbwachs not implemented");
  }
  else {
    transformer preb = transformer_undefined /*= transformer_dup(pre)*/ ;
 
    /* Apply the loop fix point transformer T* to obtain the set of stores
     * for any number of iteration, including 0.
     */
    preb = transformer_combine(preb, tf);
 
    if(false_condition_wrt_precondition_p(c, context)) {
      pips_debug(8, "The loop is never executed\n");
 
      /* propagate an impossible precondition in the loop body */
      (void) statement_to_postcondition(transformer_empty(), s);
      /* The loop body precondition is not useful any longer */
      free_transformer(preb);
      /* do not add the exit condition since it is redundant with pre */
      /* post = transformer_dup(pre); */
    }
    else if(true_condition_wrt_precondition_p(c, context)) {
      /* At least one iteration is executed. The transformer of
       * the loop body is not useful!
       */
      /* transformer tb = load_statement_transformer(s); */
      transformer ntl = transformer_undefined;
 
      pips_debug(8, "The loop certainly is executed\n");
 
      /* propagate preconditions in the loop body */
      preb = precondition_add_condition_information(preb, c, preb, true);
      (void) statement_to_postcondition(preb, s);
 
      /* ntl = transformer_apply(tf, pre); */
      /* Let's execute the last iteration since it certainly exists */
      ntl = precondition_add_condition_information(ntl, c, ntl, true);
      /* post = transformer_apply(tb, ntl); */
      free_transformer(ntl);
      /* post = precondition_add_condition_information(post, c, post, false); */
    }
    else {
      /* Assume the loop is entered, post_al, or not, post_ne, and perform
       * the convex hull of both
       */
      transformer post_ne = transformer_undefined /* = transformer_dup(pre) */ ;
      transformer post_al = transformer_undefined;
      transformer tb = load_statement_transformer(s);
 
      pips_debug(8, "The loop may be executed or not\n");
 
      /* propagate preconditions in the loop body */
      precondition_add_condition_information(preb, c, preb, true);
      (void) statement_to_postcondition(preb, s);
 
      /* The loop is executed at least once: let's execute the last iteration */
      post_al = transformer_apply(tb, preb);
      post_al = precondition_add_condition_information(post_al, c, post_al, false);
 
      /* The loop is never executed */
      post_ne = precondition_add_condition_information(post_ne, c, post_ne, false);
 
      /* post = transformer_convex_hull(post_ne, post_al); */
      transformer_free(post_ne);
      transformer_free(post_al);
    }
  }
 
  ifdebug(8) {
    pips_debug(8, "resultat t_pre=%p\n", t_pre);
    (void) print_transformer(t_pre);
    pips_debug(8,"end\n");
  }
 
  return t_pre;
}

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().

Here is the call graph for this function:

Here is the caller graph for this function:

whileloop_to_transformer()

transformer whileloop_to_transformer	(	whileloop	l,
		transformer	pre,
		list	e
	)

effects of whileloop l

Parameters

pre

re

Definition at line 2583 of file loop.c.

{
  transformer t = transformer_undefined;
  evaluation lt = whileloop_evaluation(l);
 
  if(evaluation_before_p(lt))
    t = new_whileloop_to_transformer(l, pre, e);
  else
    t = repeatloop_to_transformer(l, pre, e);
  return t;
}

References evaluation_before_p, new_whileloop_to_transformer(), repeatloop_to_transformer(), transformer_undefined, and whileloop_evaluation.

Referenced by instruction_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function: