transformer_list.c File Reference

#include <stdio.h>
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "ri-util.h"
#include "properties.h"
#include "misc.h"
#include "transformer.h"

Include dependency graph for transformer_list.c:

Go to the source code of this file.

Functions
list	merge_transformer_lists (list tl1, list tl2)
	Functions to deal with transformer lists. More...
bool	check_transformer_list (list tl)
	What do we want to impose? More...
list	combine_transformer_lists (list tl1, list tl2)
	each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer. More...
list	apply_transformer_lists_generic (list tl1, list tl2, bool exclude_p)
	each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer. More...
list	apply_transformer_lists (list tl1, list tl2)
list	apply_transformer_lists_with_exclusion (list tl1, list tl2)
list	clean_up_transformer_list (list tfl)
	Eliminate empty transformers and keep at most one identity transformer, placed as first list element. More...
list	two_transformers_to_list (transformer t1, transformer t2)
	Transformer two transformers into a correct transformer list. More...
transformer	generic_transformer_list_to_transformer (list ltl, bool active_p)
	Reduce the transformer list with the convex hull operator. More...
transformer	transformer_list_to_transformer (list ltl)
	Reduce the transformer list ltl to one transformer using the convex hull operator. More...
transformer	active_transformer_list_to_transformer (list ltl)
	Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator. More...
list	transformer_list_to_active_transformer_list (list tl)
static transformer	transformer_list_closure_to_precondition_depth_two (list tl, transformer c_t, transformer p_0)
	Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t. More...
static transformer	transformer_list_closure_to_precondition_max_depth (list tl, transformer c_t, transformer p_0)
	Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t. More...
transformer	transformer_list_closure_to_precondition (list tl, transformer c_t, transformer p_0)
	Relay to select a heuristic. More...
list	transformer_list_safe_variables_projection (list tl, list proj)
	Returns a new list of newly allocated projected transformers. More...
list	transformer_list_to_argument (list tl)
	Returns the list of variables modified by at least one transformer in tl. More...
list	transformer_list_with_effect (list tl, entity v)
	build a sublist sl of the transformer list tl with transformers that modify the value of variable v More...
list	transformer_list_preserved_variables (list vl, list tl, list tl_v)
	returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v. More...
transformer	transformer_list_multiple_closure_to_precondition (list tl, transformer c_t, transformer p_0)
	When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition. More...
Psysteme	transformer_derivative_constraints (transformer t)
	Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x') More...
transformer	transformer_list_generic_transitive_closure (list tfl, bool star_p)
	Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers. More...
transformer	transformer_list_transitive_closure (list tfl)
	Compute (U tfl)*. More...
transformer	transformer_list_transitive_closure_plus (list tfl)
	Compute (U tfl)+. More...
static list	transformer_list_add_combination (int tn, transformer ta[tn], int n, transformer ct, int past)
	Internal recursive function. More...
static list	__attribute__ ((unused))
	compute all combinations of n different transformers t from transformer list tl. More...

Function Documentation

__attribute__()

static list __attribute__ ( (unused)  )

static

compute all combinations of n different transformers t from transformer list tl.

No check is performed on the content of list tl. Empty transformers and identity transformers should have been removed before this call.

Parameters

tl	a non-empty list of transformers

int n: a strictly positive integer, smaller than the length of tl

Definition at line 1226 of file transformer_list.c.

{
  list cl = NIL;
  int tn = gen_length(tl);
 
  pips_assert("n is smaller than the number of transformers",
              n <= tn && n>=1 && n<=31);
 
  transformer ta[tn]; // build a transformer array
  int r = 0;
 
  FOREACH(TRANSFORMER, t, tl) {
    ta[r++] = t;
  }
 
  // Initialize recurrence
  transformer ct = transformer_identity();
  cl = transformer_list_add_combination(tn, ta, n, ct, -1);
  free_transformer(ct);
 
  return cl;
}

References FOREACH, free_transformer(), gen_length(), NIL, pips_assert, TRANSFORMER, transformer_identity(), and transformer_list_add_combination().

Here is the call graph for this function:

active_transformer_list_to_transformer()

transformer active_transformer_list_to_transformer

(

list

ltl

)

Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator.

An active transformer is a transformer with argument(s): at least one value is changed.

Note: a hidden identity transformer such as T(i) {i==i::init} is not detected.

Parameters

ltl

tl

Definition at line 447 of file transformer_list.c.

{
  return generic_transformer_list_to_transformer(ltl, true);
}

References generic_transformer_list_to_transformer().

Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and whileloop_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

apply_transformer_lists()

list apply_transformer_lists	(	list	tl1,
		list	tl2
	)

Parameters

tl1	l1
tl2	l2

Definition at line 269 of file transformer_list.c.

{
  return apply_transformer_lists_generic(tl1, tl2, false);
}

References apply_transformer_lists_generic().

Here is the call graph for this function:

apply_transformer_lists_generic()

list apply_transformer_lists_generic	(	list	tl1,
		list	tl2,
		bool	exclude_p
	)

each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer.

If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list. Empty preconditions are not preserved in the returned list. An empty list is unfeasible.

if exclude_p==false, return U_i1 U_i2 apply(t_i1, p_i2); else return U_i1 U_i2!=i1 apply(t_i1, p_i2);

Parameters

tl1	l1
tl2	l2
exclude_p	xclude_p

Definition at line 223 of file transformer_list.c.

{
  list ntl = NIL;
  int n1 = gen_length(tl1);
  int n2 = gen_length(tl2);
  int en = 0; // number of empty preconditions generated
  int sn = 0; // number of excluded/skipped preconditions
  int nn = -1; // number of preconditions in the result
  int i1 = 0;
 
  // FI: not true is option keep_p has been used to maintain
  //|tl_1|==|tl_2| which is useful when exclude_p is TRUE
  if(!exclude_p) {
    pips_assert("tl1 is OK\n", check_transformer_list(tl1));
    pips_assert("tl2 is OK\n", check_transformer_list(tl2));
  }
 
  FOREACH(TRANSFORMER, t1, tl1) {
    int i2 = 0;
    i1++;
    FOREACH(TRANSFORMER, t2, tl2) {
      i2++;
      if(i1!=i2 && exclude_p) {
        transformer nt = transformer_apply(t1, t2);
 
        if(!transformer_empty_p(nt))
          ntl = CONS(TRANSFORMER, nt, ntl);
        else
          en++;
      }
      else if(exclude_p)
        sn++;
    }
  }
  ntl = gen_nreverse(ntl);
 
  nn = gen_length(ntl);
  pips_assert("nn is n1*n2-en", nn==n1*n2-en-sn);
  //FI: there is no guarantee here that the identity transformer is
  //not returned multiple times... although it would make sense if the
  //input lists are properly sorted.
  pips_assert("ntl is OK\n", check_transformer_list(ntl));
 
  return ntl;
}

References check_transformer_list(), CONS, FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_apply(), and transformer_empty_p().

Referenced by apply_transformer_lists(), and apply_transformer_lists_with_exclusion().

Here is the call graph for this function:

Here is the caller graph for this function:

apply_transformer_lists_with_exclusion()

list apply_transformer_lists_with_exclusion	(	list	tl1,
		list	tl2
	)

Parameters

tl1	l1
tl2	l2

Definition at line 274 of file transformer_list.c.

{
  return apply_transformer_lists_generic(tl1, tl2, true);
}

References apply_transformer_lists_generic().

Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().

Here is the call graph for this function:

Here is the caller graph for this function:

check_transformer_list()

bool check_transformer_list

(

list

tl

)

What do we want to impose?

1. Only one identity transformer
2. Common basis?
3. No empty transformer

The empty transformer list is used to represent the empty transformer...

It must be the first one

Parameters

tl

l

Definition at line 140 of file transformer_list.c.

{
  bool identity_p = false;
  // unused: bool one_p = false; // useless for the time being
 
  if(ENDP(tl)) {
    /* The empty transformer list is used to represent the empty
       transformer... */
    ;
  }
  else {
    FOREACH(TRANSFORMER, tf, tl) {
      if(transformer_identity_p(tf)) {
        if(identity_p) {
          pips_internal_error("Two identity transformers in one list.");
        }
        else {
          identity_p = true;
        }
      }
    }
    if(identity_p) {
      /* It must be the first one */
      if(!transformer_identity_p(TRANSFORMER(CAR(tl))))
        pips_internal_error("The identity transformer is not the list header.");
    }
 
    FOREACH(TRANSFORMER, tf, tl) {
      if(transformer_empty_p(tf))
        pips_internal_error("An empty transformer has been found.");
    }
  }
 
  return true;
}

References CAR, ENDP, FOREACH, pips_internal_error, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().

Referenced by apply_transformer_lists_generic(), combine_transformer_lists(), and merge_transformer_lists().

Here is the call graph for this function:

Here is the caller graph for this function:

clean_up_transformer_list()

list clean_up_transformer_list

(

list

tfl

)

Eliminate empty transformers and keep at most one identity transformer, placed as first list element.

check_transformer_list(ntfl) should be TRUE.

tfl is fully destroyed (to avoid memory leaks and nightmares); to be more efficient, the transformers moved from the input list into the output list should be detached from the input list and then the input list could be fully destroyed without having to copy any transformers; but FOREACH operates at too high a level for this.

Parameters

tfl

fl

Definition at line 290 of file transformer_list.c.

{
  list ntfl = NIL;
  bool identity_p = false;
 
  FOREACH(TRANSFORMER, tf, tfl) {
    bool tf_identity_p = transformer_identity_p(tf);
    if(!tf_identity_p && !transformer_empty_p(tf))
      ntfl = CONS(TRANSFORMER, copy_transformer(tf), ntfl);
    identity_p = identity_p || tf_identity_p;
  }
  gen_full_free_list(tfl);
  ntfl = gen_nreverse(ntfl);
  if(identity_p)
    ntfl = CONS(TRANSFORMER, transformer_identity(), ntfl);
  return ntfl;
}

References CONS, copy_transformer(), FOREACH, gen_full_free_list(), gen_nreverse(), NIL, TRANSFORMER, transformer_empty_p(), transformer_identity(), and transformer_identity_p().

Referenced by block_to_transformer_list().

Here is the call graph for this function:

Here is the caller graph for this function:

combine_transformer_lists()

list combine_transformer_lists	(	list	tl1,
		list	tl2
	)

each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer.

If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list.

Parameters

tl1	l1
tl2	l2

Definition at line 180 of file transformer_list.c.

{
  list ntl = NIL;
  int n1 = gen_length(tl1);
  int n2 = gen_length(tl2);
  int en = 0;
  int nn = -1;
 
  pips_assert("tl1 is OK\n", check_transformer_list(tl1));
  pips_assert("tl2 is OK\n", check_transformer_list(tl2));
 
  FOREACH(TRANSFORMER, t1, tl1) {
    FOREACH(TRANSFORMER, t2, tl2) {
      transformer nt = transformer_combine(copy_transformer(t1), t2);
 
      // transformer_empty_p() is not strong enough currently
      // It does not detect that k<= 2 && k>=3 is empty...
      nt = transformer_normalize(nt, 2);
      if(!transformer_empty_p(nt))
        ntl = CONS(TRANSFORMER, nt, ntl);
      else
        en++;
    }
  }
  ntl = gen_nreverse(ntl);
 
  nn = gen_length(ntl);
  pips_assert("ntl is OK\n", check_transformer_list(ntl));
  pips_assert("nn is n1*n2-en", nn==n1*n2-en);
 
  return ntl;
}

References check_transformer_list(), CONS, copy_transformer(), FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_combine(), transformer_empty_p(), and transformer_normalize().

Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().

Here is the call graph for this function:

Here is the caller graph for this function:

generic_transformer_list_to_transformer()

transformer generic_transformer_list_to_transformer	(	list	ltl,
		bool	active_p
	)

Reduce the transformer list with the convex hull operator.

If active_p is true, skip transformers that do not update the state. Beyond the identity transformer, any transformer without arguments does not really update the state, although it may restrict it.

A new transformer is always allocated. The transformers in the transformer list ltl are freed.

Look for the first useful transformer in the list

Only range conditions have been found: the store is restricted but not changed.

Take care of the following useful transformers

Look for the next useful transformer in the list

Parameters

ltl	tl
active_p	ctive_p

Definition at line 384 of file transformer_list.c.

{
  transformer ltf = transformer_undefined; // list transformer
 
  if(ENDP(ltl))
    ltf = transformer_empty();
  else {
    list ctl = ltl;
    /* Look for the first useful transformer in the list */
    FOREACH(TRANSFORMER, tf, ltl) {
      if(!active_p || !ENDP(transformer_arguments(tf))) {
        ltf = copy_transformer(tf);
        free_transformer(tf);
        POP(ctl);
        break;
      }
      POP(ctl);
    }
    if(ENDP(ctl)) {
      if(transformer_undefined_p(ltf))
        /* Only range conditions have been found: the store is
           restricted but not changed. */
        ltf = transformer_identity();
    }
    else {
      /* Take care of the following useful transformers */
      while(!ENDP(ctl)) {
        /* Look for the next useful transformer in the list */
        FOREACH(TRANSFORMER, tf, ctl) {
          if(!active_p || !ENDP(transformer_arguments(tf))) {
            transformer ntf = copy_transformer(tf);
            transformer ptf = ltf;
            ltf = transformer_convex_hull(ptf, ntf);
            free_transformer(ntf);
            free_transformer(ptf);
            POP(ctl);
            break;
          }
          POP(ctl);
        }
      }
    }
  }
 
  return ltf;
}

References copy_transformer(), ENDP, FOREACH, free_transformer(), POP, TRANSFORMER, transformer_arguments, transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_undefined, and transformer_undefined_p.

Referenced by active_transformer_list_to_transformer(), and transformer_list_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

merge_transformer_lists()

list merge_transformer_lists	(	list	tl1,
		list	tl2
	)

Functions to deal with transformer lists.

transformer_list.c

Tansformer lists are used to delay convex hulls and to refine the precondition computation of loops by putting aside the identity transformer.

If there is an identity transformer in the list, it is supposed to be the first one in the list.

However, some control paths are almost identity transformers because the store is apparently unchanged. However, they contain predicates on the possible values. Although they have no arguments, and hence, the store is left unchanged, they are different from the identity transformer bebcause the relation is smaller.

So it should be up to the function using the transformer list to decide how to cope with transformers that restrict the identity transition. Must not be used, beware of library cycles: include "semantics.h" Union of two lists

If the list includes the identity transformer, it must be the first in the list and be nowehere else

It is not clear if transformer lists will be stored in hash tables... Hence I do not know if the input list should be freed, reused or left unshared. To be conservative, no alias is created.

Do we have to worry about different bases in transformers?

Too much information is sometimes lost with this simplification

Parameters

tl1	l1
tl2	l2

Definition at line 74 of file transformer_list.c.

{
  list ntl = NIL;
  list ntl1 = NIL;
  list ntl2 = NIL;
 
  if(ENDP(tl1))
    ntl = gen_full_copy_list(tl2);
  else if(ENDP(tl2))
    ntl = gen_full_copy_list(tl1);
  else {
    /* Do we have to worry about different bases in transformers? */
    transformer t1 = TRANSFORMER(CAR(tl1));
    transformer t2 = TRANSFORMER(CAR(tl2));
 
    /* Too much information is sometimes lost with this
       simplification */
    /*
    if(ENDP(transformer_arguments(t1))) {
      free_transformer(t1);
      t1 = transformer_identity();
    }
 
    if(ENDP(transformer_arguments(t2))) {
      free_transformer(t2);
      t2 = transformer_identity();
    }
    */
 
    if(transformer_identity_p(t1) || transformer_identity_p(t2)) {
      ntl = CONS(TRANSFORMER, transformer_identity(), NIL);
    }
    if(transformer_identity_p(t1))
      ntl1 = gen_full_copy_list(CDR(tl1));
    else
      ntl1 = gen_full_copy_list(tl1);
    if(transformer_identity_p(t2))
      ntl2 = gen_full_copy_list(CDR(tl2));
    else
      ntl2 = gen_full_copy_list(tl2);
    ntl1 = gen_nconc(ntl1, ntl2);
    ntl = gen_nconc(ntl, ntl1);
  }
 
  ifdebug(1) {
    int ntll = gen_length(ntl);
    int tl1l = gen_length(tl1);
    int tl2l = gen_length(tl2);
    pips_assert("The new list is about the sum of the input lists.\n",
                ntll>=tl1l+tl2l-1 && ntll<=tl1l+tl2l);
    pips_assert("The new transformer list is legal",
                check_transformer_list(ntl));
  }
  return ntl;
}

References CAR, CDR, check_transformer_list(), CONS, ENDP, gen_full_copy_list(), gen_length(), gen_nconc(), ifdebug, NIL, pips_assert, TRANSFORMER, transformer_identity(), and transformer_identity_p().

Referenced by test_to_transformer_list().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_derivative_constraints()

Psysteme transformer_derivative_constraints

(

transformer

t

)

Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x')

FI: this function should/might be located in fix_point.c

sc is going to be modified and returned

Do not handle variable which do not appear explicitly in constraints!

basis vector

Compute constraints with difference equations

Only generate difference equations if the old value is used

Project all variables but differences to get T'

Definition at line 891 of file transformer_list.c.

{
  Psysteme sc = sc_copy(predicate_system(transformer_relation(t)));
  /* sc is going to be modified and returned */
  /* Do not handle variable which do not appear explicitly in constraints! */
  Pbase b = sc_to_minimal_basis(sc);
  Pbase bv = BASE_NULLE; /* basis vector */
 
  /* Compute constraints with difference equations */
 
  for(bv = b; !BASE_NULLE_P(bv); bv = bv->succ) {
    entity oldv = (entity) vecteur_var(bv);
 
    /* Only generate difference equations if the old value is used */
    if(old_value_entity_p(oldv)) {
      entity var = value_to_variable(oldv);
      entity newv = entity_to_new_value(var);
      entity diffv = entity_to_intermediate_value(var);
      Pvecteur diff = VECTEUR_NUL;
      Pcontrainte eq = CONTRAINTE_UNDEFINED;
 
      diff = vect_make(diff,
                       (Variable) diffv, VALUE_ONE,
                       (Variable) newv,  VALUE_MONE,
                       (Variable) oldv, VALUE_ONE,
                       TCST, VALUE_ZERO);
 
      eq = contrainte_make(diff);
      sc = sc_equation_add(sc, eq);
    }
  }
 
  ifdebug(8) {
    pips_debug(8, "with difference equations=\n");
    sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
  }
 
  /* Project all variables but differences to get T' */
 
  sc = sc_projection_ofl_along_variables(sc, b);
 
  ifdebug(8) {
    pips_debug(8, "Non-homogeneous constraints on derivatives=\n");
    sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
  }
 
  return sc;
}

References BASE_NULLE, BASE_NULLE_P, contrainte_make(), CONTRAINTE_UNDEFINED, entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), ifdebug, old_value_entity_p(), pips_debug, predicate_system, sc_copy(), sc_equation_add(), sc_fprint(), sc_to_minimal_basis(), Svecteur::succ, TCST, transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), VECTEUR_NUL, and vecteur_var.

Referenced by transformer_list_generic_transitive_closure().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_add_combination()

static list transformer_list_add_combination ( int  tn, transformer  ta[tn], int  n, transformer  ct, int  past  )

static

Internal recursive function.

Should be used as transformer_list_combination(). As long as n is not zero, choose all unused transformation numbers in past and call yourself recursively after updating past and ct. past is a bit field. Each bit of past is set to 1 initially because no transformer has been used yet. It is reset to 0 when the transformation has been used. The selected transformer is combined to ct.

Parameters

tn	is the number of transformers that can be chosen to be combined
ta[tn]	is an array containing the tn transformers to combine
n	is the number of combinations to perform. It is less than tn.
ct	is the current combination of past transformers
past	is a bit field used to keep track of transformers alreasy used to build ct

Returns

the list of all non-empty combinations of n transformers

Definition at line 1175 of file transformer_list.c.

{
  list cl = NIL;
 
  if(n>0) {
    int k = 1; // to select a non-zero bit in past
    int ti; // transformation index
    bool found_p = false;
    for(ti=0; ti<n;ti++) {
      if(k&past) {
        // this transformation is selectable, because it has not been
        // selected yet
        int npast = past ^ k; // mark it as selected
        transformer t = ta[ti]; // to ease debugging
        transformer nct = transformer_combine(copy_transformer(ct), t);
        // Necessary before checking emptiness
        nct = transformer_normalize(nct, 2);
        // Check the sequence feasability
        if(!transformer_empty_p(nct)) {
          list nl = transformer_list_add_combination(tn, ta, n-1, nct, npast);
          cl = gen_nconc(cl, nl);
        }
        found_p = true;
        free_transformer(nct);
      }
      k <<= 1;
    }
    pips_assert("At least one transformation has been found", found_p);
  }
  else {
    // The recursion is over, ct contains the right number of
    // transformer combinations
    cl = CONS(TRANSFORMER, ct, NIL);
  }
  return cl;
}

References CONS, copy_transformer(), free_transformer(), gen_nconc(), NIL, pips_assert, TRANSFORMER, transformer_combine(), transformer_empty_p(), and transformer_normalize().

Referenced by __attribute__().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_closure_to_precondition()

transformer transformer_list_closure_to_precondition	(	list	tl,
		transformer	c_t,
		transformer	p_0
	)

Relay to select a heuristic.

Parameters

tl	l
c_t	_t
p_0	_0

Definition at line 705 of file transformer_list.c.

{
  transformer p_star = transformer_undefined;
  const char* h = get_string_property("SEMANTICS_LIST_FIX_POINT_OPERATOR");
 
  if(strcmp(h, "depth_two")) {
    p_star = transformer_list_closure_to_precondition_depth_two(tl, c_t, p_0);
  }
    else if(strcmp(h, "max_depth")) {
    p_star = transformer_list_closure_to_precondition_max_depth(tl, c_t, p_0);
  }
  else
    pips_user_error("Unknown value \"%s\" for property "
                    "\"SEMANTICS_LIST_FIX_POINT_OPERATOR\"", h);
  pips_assert("prec is consistent", transformer_consistency_p(p_star));
  return p_star;
}

References get_string_property(), pips_assert, pips_user_error, transformer_consistency_p(), transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and transformer_undefined.

Referenced by transformer_list_multiple_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_closure_to_precondition_depth_two()

static transformer transformer_list_closure_to_precondition_depth_two ( list  tl, transformer  c_t, transformer  p_0  )

static

Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t.

The precondition of iteration 0 is p_0.

We need a developped formulae for P*=(U_i T_i)^*P_0... to postpone the convex hulls as much as possible

For instance, and this is a heuristics:

P_0 is known as pre_init

P_1 = U_i T_i(P_0)

P_2 = U_i U_j T_i(T_j(P_0))

P_3^s = U_i T_i^+(P_0) — only one path is used

P_3^+ = U_i U_j!=i T^+_i(T_j(T^*(P_1))) — at least two paths are used

which would make more sense when i and j are in [0..1]. Note that in P_3, T_j and T^+_i could be recomputed wrt P_1 instead of pre_fuzzy... which is not provided

Maybe T^*=(U_i T_i)^* could/should be computed as (U_i T_i*)* but it is not clear how all the useful conditions could be taken into account.

A more accurate approach would use several developped formulae for P* and an intersection of their results.

Definition at line 501 of file transformer_list.c.

{
  list ntl = transformers_combine(gen_full_copy_list(tl), c_t);
 
  list p_1_l = transformers_apply(ntl, p_0);
  transformer p_1 = transformer_list_to_transformer(p_1_l);
 
  list t_2_l = combine_transformer_lists(ntl, ntl);
  list p_2_l = transformers_apply(t_2_l, p_0);
  transformer p_2 = transformer_list_to_transformer(p_2_l);
 
  list itcl = transformers_derivative_fix_point(ntl); // individual
                                                      // transformer closures
  itcl = transformers_combine(itcl, c_t);
  list itcl_plus = gen_full_copy_list(itcl); // to preserve ictl
  itcl_plus = one_to_one_transformers_combine(itcl_plus, ntl);
  list p_3_l = transformers_apply(itcl_plus, p_0);
  transformer p_3 = transformer_list_to_transformer(gen_full_copy_list(p_3_l));
 
  transformer t_star = transformer_undefined;
  if(!get_bool_property("SEMANTICS_USE_DERIVATIVE_LIST")) {
  // Not satisfying: works only for the whole space, not for subpaces
  // left untouched
    t_star = active_transformer_list_to_transformer(itcl);
  }
  else
    t_star = transformer_list_transitive_closure(itcl);
  transformer p_4_1 = transformer_apply(t_star, p_1); // one + * iteration
  list p_4_2_l = transformers_apply_and_keep_all(ntl, p_4_1); // another iteration
  pips_assert("itcl_plus and p_4_2_l have the same numer of elements",
              gen_length(itcl_plus)==gen_length(p_4_2_l));
  list p_4_3_l = apply_transformer_lists_with_exclusion(itcl_plus, p_4_2_l);
  transformer p_4 = transformer_list_to_transformer(p_4_3_l);
 
  transformer p_star = transformer_undefined;
 
  ifdebug(8) {
    pips_debug(8, "p_0:\n");
    print_transformer(p_0);
    pips_debug(8, "p_1:\n");
    print_transformer(p_1);
    pips_debug(8, "p_2:\n");
    print_transformer(p_2);
    pips_debug(8, "p_3:\n");
    print_transformer(p_3);
    pips_debug(8, "p_4:\n");
    print_transformer(p_4);
  }
 
  // reduce p_0, p_1, p_2, p_3 and p_4 to p_star
  transformer p_01 = transformer_convex_hull(p_0, p_1);
  transformer p_012 = transformer_convex_hull(p_01, p_2);
  transformer p_0123 = transformer_convex_hull(p_012, p_3);
  p_star = transformer_convex_hull(p_0123, p_4);
 
  ifdebug(8) {
    pips_debug(8, "p_star:\n");
    print_transformer(p_star);
  }
 
  // Clean up all intermediate variables
  gen_full_free_list(ntl);
  //gen_full_free_list(p_1_l);
  free_transformer(p_1);
  //gen_full_free_list(t_2_l);
  //gen_full_free_list(p_2_l);
  free_transformer(p_2);
  //gen_full_free_list(itcl);
  gen_full_free_list(itcl_plus);
  //gen_full_free_list(p_3_l);
  free_transformer(p_3);
  free_transformer(t_star);
  free_transformer(p_4_1);
  gen_full_free_list(p_4_2_l);
  //gen_full_free_list(p_4_3_l);
  free_transformer(p_4);
  free_transformer(p_01);
  free_transformer(p_012);
  free_transformer(p_0123);
  pips_assert("p_star is consistent", transformer_consistency_p(p_star));
  return p_star;
}

References active_transformer_list_to_transformer(), apply_transformer_lists_with_exclusion(), combine_transformer_lists(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), ifdebug, one_to_one_transformers_combine(), pips_assert, pips_debug, print_transformer, transformer_apply(), transformer_consistency_p(), transformer_convex_hull(), transformer_list_to_transformer(), transformer_list_transitive_closure(), transformer_undefined, transformers_apply(), transformers_apply_and_keep_all(), transformers_combine(), and transformers_derivative_fix_point().

Referenced by transformer_list_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_closure_to_precondition_max_depth()

static transformer transformer_list_closure_to_precondition_max_depth ( list  tl, transformer  c_t, transformer  p_0  )

static

Compute the precondition of a loop whose body transformers T_i are in transformer list tl and whose condition is modelized by transformer c_t.

The precondition of iteration 0 is p_0.

We need a developped formulae for P*=(U_i T_i)^*P_0... to postpone the convex hulls as much as possible

For instance, and this is a heuristics:

P_0 is known as pre_init

P_l = U_i T_i(P_0)

P_2 = U_i U_j T_i(T_j(P_0))

P_3^s = U_i T_i^+(P_0) — only one path is used

P_3^+ = U_i U_j!=i T^+_i(T_j(T^*(P_1))) — at least two paths are used

which would make more sense when i and j are in [0..1]. Note that in P_3, T_j and T^+_i could be recomputed wrt P_1 instead of pre_fuzzy... which is not provided

Maybe T^*=(U_i T_i)^* could/should be computed as (U_i T_i*)* but it is not clear how all the useful conditions could be taken into account.

A more accurate approach would use several developped formulae for P* and an intersection of their results.

Definition at line 618 of file transformer_list.c.

{
  list ntl = transformers_combine(gen_full_copy_list(tl), c_t);
  //pips_assert("ntl is OK", check_transformer_list(ntl));
 
  list p_1_l = transformers_apply(ntl, p_0);
  transformer p_1 = transformer_list_to_transformer(p_1_l);
 
  list t_2_l = combine_transformer_lists(ntl, ntl);
  list p_2_l = transformers_apply(t_2_l, p_0);
  transformer p_2 = transformer_list_to_transformer(p_2_l);
 
  list itcl = transformers_derivative_fix_point(ntl); // individual
                                                      // transformer closures
  itcl = transformers_combine(itcl, c_t);
  list itcl_plus = gen_full_copy_list(itcl); // to preserve ictl
  itcl_plus = one_to_one_transformers_combine(itcl_plus, ntl);
  list p_3_l = transformers_apply(itcl_plus, p_0);
  transformer p_3 = transformer_list_to_transformer(gen_full_copy_list(p_3_l));
 
  transformer t_star = transformer_undefined;
  if(!get_bool_property("SEMANTICS_USE_DERIVATIVE_LIST")) {
  // Not satisfying: works only for the whole space, not for subpaces
  // left untouched
    t_star = active_transformer_list_to_transformer(itcl);
  }
  else
    t_star = transformer_list_transitive_closure(itcl);
  transformer p_4_1 = transformer_apply(t_star, p_1); // one + * iteration
  list p_4_2_l = transformers_apply_and_keep_all(ntl, p_4_1); // another iteration
  pips_assert("itcl_plus and p_4_2_l have the same numer of elements",
              gen_length(itcl_plus)==gen_length(p_4_2_l));
  list p_4_3_l = apply_transformer_lists_with_exclusion(itcl_plus, p_4_2_l);
  transformer p_4 = transformer_list_to_transformer(p_4_3_l);
 
  transformer p_star = transformer_undefined;
 
  ifdebug(8) {
    pips_debug(8, "p_0:\n");
    print_transformer(p_0);
    pips_debug(8, "p_1:\n");
    print_transformer(p_1);
    pips_debug(8, "p_2:\n");
    print_transformer(p_2);
    pips_debug(8, "p_3:\n");
    print_transformer(p_3);
    pips_debug(8, "p_4:\n");
    print_transformer(p_4);
  }
 
  // reduce p_0, p_1, p_2, p_3 and p_4 to p_star
  transformer p_01 = transformer_convex_hull(p_0, p_1);
  transformer p_012 = transformer_convex_hull(p_01, p_2);
  transformer p_0123 = transformer_convex_hull(p_012, p_3);
  p_star = transformer_convex_hull(p_0123, p_4);
 
  ifdebug(8) {
    pips_debug(8, "p_star:\n");
    print_transformer(p_star);
  }
 
  // Clean up all intermediate variables
  gen_full_free_list(ntl);
  //gen_full_free_list(p_1_l);
  free_transformer(p_1);
  //gen_full_free_list(t_2_l);
  //gen_full_free_list(p_2_l);
  free_transformer(p_2);
  //gen_full_free_list(itcl);
  gen_full_free_list(itcl_plus);
  //gen_full_free_list(p_3_l);
  free_transformer(p_3);
  free_transformer(t_star);
  free_transformer(p_4_1);
  gen_full_free_list(p_4_2_l);
  //gen_full_free_list(p_4_3_l);
  free_transformer(p_4);
  free_transformer(p_01);
  free_transformer(p_012);
  free_transformer(p_0123);
 
  return p_star;
}

References active_transformer_list_to_transformer(), apply_transformer_lists_with_exclusion(), combine_transformer_lists(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), ifdebug, one_to_one_transformers_combine(), pips_assert, pips_debug, print_transformer, transformer_apply(), transformer_convex_hull(), transformer_list_to_transformer(), transformer_list_transitive_closure(), transformer_undefined, transformers_apply(), transformers_apply_and_keep_all(), transformers_combine(), and transformers_derivative_fix_point().

Referenced by transformer_list_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_generic_transitive_closure()

transformer transformer_list_generic_transitive_closure	(	list	tfl,
		bool	star_p
	)

Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers.

Each transformer is used to compute its derivative and the derivatives are unioned by convex hull.

The reason for doing this is D(T1) U D(T2) == D(T1 U T2) but the complexity is lower

See http://www.cri.ensmp.fr/classement/doc/A-429.pdf

Implicit equations, n::new - n::old = 0, are added because they are necessary for the convex hull.

Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old This code was cut-and-pasted from transformer_derivative_fix_point() but is more general and subsume it transformer transformer_derivative_fix_point(transformer tf)

Since we compute the * transitive closure and not the + transitive closure, the fix point is the identity.

basis of difference vectors

Compute the global argument list and the global base b

Cannot use arguments_union() because a new list is allocated

For each transformer t in list tl

compute its derivative constraint system

add the equations for the unchanged variables

compute its convex hull with the current value of sc if sc is already defined

Add corresponding equation

This could be optimized by using the convex hull of a Psystemes list and by keeping the dual representation of the result instead of converting it several time back and forth.

Multiply the constant terms by the iteration number ik and add a positivity constraint for the iteration number ik and then eliminate the iteration number ik to get T*(dx).

Difference variables must substituted back to differences between old and new values.

Only generate difference equations if the old value is used

Project all difference variables

The full basis must be used again

Plug sc back into tc_tf

That's all!

Parameters

tfl	fl
star_p	tar_p

Definition at line 960 of file transformer_list.c.

{
  transformer tc_tf = transformer_identity();
 
  ifdebug(8) {
    pips_debug(8, "Begin for transformer list %p:\n", tfl);
    print_transformers(tfl);
  }
 
  if(ENDP(tfl)) {
    if(star_p) {
    /* Since we compute the * transitive closure and not the +
       transitive closure, the fix point is the identity. */
      tc_tf = transformer_identity();
    }
    else {
      tc_tf = transformer_empty();
    }
  }
  else {
    // Pbase ib = base_dup(sc_base(sc)); /* initial and final basis */
    Pbase ib = BASE_NULLE;
    Pbase diffb = BASE_NULLE; /* basis of difference vectors */
    Pbase bv = BASE_NULLE;
    Pbase b = BASE_NULLE;
 
    /* Compute the global argument list and the global base b */
    list gal = NIL;
    FOREACH(TRANSFORMER, t, tfl) {
      list al = transformer_arguments(t);
      /* Cannot use arguments_union() because a new list is allocated */
      FOREACH(ENTITY, e, al)
        gal = arguments_add_entity(gal, e);
 
      // FI: this copy is almost entirely memory leaked
      Psysteme sc = sc_copy(predicate_system(transformer_relation(t)));
      // redundant with call to transformer_derivative_constraints(t)
      Pbase tb = sc_to_minimal_basis(sc);
      Pbase nb = base_union(b, tb);
      base_rm(b); // base_union() allocates a new base
      b = nb;
    }
 
    /* For each transformer t in list tl
     *
     *   compute its derivative constraint system
     *
     *   add the equations for the unchanged variables
     *
     *   compute its convex hull with the current value of sc if sc is
     *   already defined
     */
    Psysteme sc = SC_UNDEFINED;
    FOREACH(TRANSFORMER, t, tfl) {
      Psysteme tsc = transformer_derivative_constraints(t);
      FOREACH(ENTITY,e,gal) {
        if(!entity_is_argument_p(e, transformer_arguments(t))) {
          /* Add corresponding equation */
          entity diffv = entity_to_intermediate_value(e);
          Pvecteur diff = VECTEUR_NUL;
          Pcontrainte eq = CONTRAINTE_UNDEFINED;
 
          diff = vect_make(diff,
                           (Variable) diffv, VALUE_ONE,
                           TCST, VALUE_ZERO);
 
          eq = contrainte_make(diff);
          tsc = sc_equation_add(tsc, eq);
        }
      }
      if(SC_UNDEFINED_P(sc))
        sc = tsc;
      else {
        /* This could be optimized by using the convex hull of a
           Psystemes list and by keeping the dual representation of
           the result instead of converting it several time back
           and forth. */
        Psysteme nsc = cute_convex_union(sc, tsc);
        sc_free(sc);
        sc = nsc;
      }
    }
 
    /* Multiply the constant terms by the iteration number ik and add a
       positivity constraint for the iteration number ik and then
       eliminate the iteration number ik to get T*(dx). */
    entity ik = make_local_temporary_integer_value_entity();
    //Psysteme sc_t_prime_k = sc_dup(sc);
    //sc_t_prime_k = sc_multiply_constant_terms(sc_t_prime_k, (Variable) ik);
    sc = sc_multiply_constant_terms(sc, (Variable) ik, star_p);
    //Psysteme sc_t_prime_star = sc_projection_ofl(sc_t_prime_k, (Variable) ik);
    sc = sc_projection_ofl(sc, (Variable) ik);
    if(SC_EMPTY_P(sc)) {
      sc = sc_empty(BASE_NULLE);
    }
    else {
      sc->base = base_remove_variable(sc->base, (Variable) ik);
      sc->dimension--;
      // FI: I do not remember nor find how to get rid of local values...
      //sc_rm(sc);
      //sc = sc_t_prime_star;
    }
 
    ifdebug(8) {
      pips_debug(8, "All invariants on derivatives=\n");
      sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
    }
 
    /* Difference variables must substituted back to differences
     * between old and new values.
     */
 
    for(bv = b; !BASE_NULLE_P(bv); bv = bv->succ) {
      entity oldv = (entity) vecteur_var(bv);
 
      /* Only generate difference equations if the old value is used */
      if(old_value_entity_p(oldv)) {
        entity var = value_to_variable(oldv);
        entity newv = entity_to_new_value(var);
        entity diffv = entity_to_intermediate_value(var);
        Pvecteur diff = VECTEUR_NUL;
        Pcontrainte eq = CONTRAINTE_UNDEFINED;
 
        diff = vect_make(diff,
                         (Variable) diffv, VALUE_ONE,
                         (Variable) newv,  VALUE_MONE,
                         (Variable) oldv, VALUE_ONE,
                         TCST, VALUE_ZERO);
 
        eq = contrainte_make(diff);
        sc = sc_equation_add(sc, eq);
        diffb = base_add_variable(diffb, (Variable) diffv);
        ib = base_add_variable(ib, (Variable) oldv);
        ib = base_add_variable(ib, (Variable) newv);
      }
    }
 
    ifdebug(8) {
      pips_debug(8,
                 "All invariants on derivatives with difference variables=\n");
      sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
    }
 
    /* Project all difference variables */
 
    sc = sc_projection_ofl_along_variables(sc, diffb);
 
    ifdebug(8) {
      pips_debug(8, "All invariants on differences=\n");
      sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
    }
 
    /* The full basis must be used again */
    base_rm(sc_base(sc)), sc_base(sc) = BASE_NULLE;
    sc_base(sc) = ib;
    sc_dimension(sc) = vect_size(ib);
    base_rm(b), b = BASE_NULLE;
 
    ifdebug(8) {
      pips_debug(8, "All invariants with proper basis =\n");
      sc_fprint(stderr, sc, (char * (*)(Variable)) external_value_name);
    }
 
    /* Plug sc back into tc_tf */
    predicate_system(transformer_relation(tc_tf)) = sc;
    transformer_arguments(tc_tf) = gal;
 
  }
  /* That's all! */
 
  ifdebug(8) {
    pips_debug(8, "Transitive closure tc_tf=\n");
    fprint_transformer(stderr, tc_tf, (get_variable_name_t) external_value_name);
    transformer_consistency_p(tc_tf);
    pips_debug(8, "end\n");
  }
 
  return tc_tf;
}

References arguments_add_entity(), Ssysteme::base, base_add_variable(), BASE_NULLE, BASE_NULLE_P, base_remove_variable(), base_rm, base_union(), contrainte_make(), CONTRAINTE_UNDEFINED, cute_convex_union(), Ssysteme::dimension, ENDP, ENTITY, entity_is_argument_p(), entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), FOREACH, fprint_transformer(), ifdebug, make_local_temporary_integer_value_entity(), NIL, old_value_entity_p(), pips_debug, predicate_system, print_transformers(), sc_copy(), sc_empty(), sc_equation_add(), sc_fprint(), sc_free(), sc_multiply_constant_terms(), sc_to_minimal_basis(), Svecteur::succ, TCST, TRANSFORMER, transformer_arguments, transformer_consistency_p(), transformer_derivative_constraints(), transformer_empty(), transformer_identity(), transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), vect_size(), VECTEUR_NUL, and vecteur_var.

Referenced by transformer_list_transitive_closure(), and transformer_list_transitive_closure_plus().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_multiple_closure_to_precondition()

transformer transformer_list_multiple_closure_to_precondition	(	list	tl,
		transformer	c_t,
		transformer	p_0
	)

When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition.

The preconditions obtained with the different projections are intersected.

FI: this may be useless when derivatives are computed before the convex union. No. This was due to a bug in the computation of list of derivatives.

FI: this should be mathematically useless but it useful when a heuristic is used to compute the invariant. The number of transitions is reduced and hence a limited number of combinations is more likely to end up with a precise result.

Parameters

tl	l
c_t	_t
p_0	_0

Definition at line 826 of file transformer_list.c.

{
  transformer prec = transformer_list_closure_to_precondition(tl, c_t, p_0);
 
  if(get_bool_property("SEMANTICS_USE_LIST_PROJECTION")) {
    list al = transformer_arguments(prec);
    list vl = transformer_list_to_argument(tl); // list of modified
    // variables
    // FI: this is too strong vl must only be included in transformer_arguments(prec)
    //pips_assert("all modified variables are argument of the global precondition",
    //arguments_equal_p(vl, transformer_arguments(prec)));
    FOREACH(ENTITY, v, vl) {
      // FI: the same projection could be obtained for different
      // variables v and the computation should not be performed again
      // but I choose not to memoize past lists tl_v
      list tl_v = transformer_list_with_effect(tl, v);
 
      if(gen_length(tl_v)<gen_length(tl)) {
        list keep_v = transformer_list_preserved_variables(vl, tl, tl_v);
        list proj_v = arguments_difference(vl, keep_v);
        list ptl_v = transformer_list_safe_variables_projection(tl_v, proj_v);
        transformer p_0_v
          = safe_transformer_projection(copy_transformer(p_0), proj_v);
        transformer c_t_v
          = safe_transformer_projection(copy_transformer(c_t), proj_v);
        transformer prec_v
          = transformer_list_closure_to_precondition(ptl_v, c_t_v, p_0_v);
        if(arguments_subset_p(transformer_arguments(prec_v), al)) {
          // FI: this generates an inconsistent transformer if
          // transformer_arguments(prec_v) is not a subset of al...
          transformer_arguments(prec_v) = gen_copy_seq(al); // memory leak
        }
        else {
          transformer n_prec_v = transformer_range(prec_v);
          free_transformer(prec_v);
          prec_v = n_prec_v;
          transformer_arguments(prec_v) = gen_copy_seq(al);
        }
        prec = transformer_intersection(prec, prec_v); // memory leak
        // transformer_intersection() returns an inconsistent transformer
        // The argument list is empty but an old value is used in the conditions
        // prec = transformer_range(prec); // memory leak
        pips_assert("prec is consistent", transformer_consistent_p(prec));
 
        free_transformer(prec_v);
        free_transformer(c_t_v);
        free_transformer(p_0_v);
        gen_full_free_list(ptl_v);
        gen_free_list(keep_v);
      }
      gen_free_list(tl_v);
    }
 
    gen_free_list(vl);
  }
  pips_assert("prec is consistent", transformer_consistency_p(prec));
  return prec;
}

References arguments_difference(), arguments_subset_p(), copy_transformer(), ENTITY, FOREACH, free_transformer(), gen_copy_seq(), gen_free_list(), gen_full_free_list(), gen_length(), get_bool_property(), pips_assert, safe_transformer_projection(), transformer_arguments, transformer_consistency_p(), transformer_consistent_p(), transformer_intersection(), transformer_list_closure_to_precondition(), transformer_list_preserved_variables(), transformer_list_safe_variables_projection(), transformer_list_to_argument(), transformer_list_with_effect(), and transformer_range().

Referenced by whileloop_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_preserved_variables()

list transformer_list_preserved_variables	(	list	vl,
		list	tl,
		list	tl_v
	)

returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v.

tl_v is assumed to be a subset of tl.

Parameters

vl	l
tl	l
tl_v	l_v

Definition at line 786 of file transformer_list.c.

{
  list pvl = NIL;
 
  FOREACH(ENTITY, v, vl) {
    bool found_p = false;
    FOREACH(TRANSFORMER, t, tl) {
      if(!gen_in_list_p(t, tl_v)) {
        if(entity_is_argument_p(v, transformer_arguments(t))) {
          found_p = true;
          break;
        }
      }
    }
    if(!found_p) {
      pvl = CONS(ENTITY, v, pvl);
    }
  }
 
  pvl = gen_nreverse(pvl);
 
  return pvl;
}

References CONS, ENTITY, entity_is_argument_p(), FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.

Referenced by transformer_list_multiple_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_safe_variables_projection()

list transformer_list_safe_variables_projection	(	list	tl,
		list	proj
	)

Returns a new list of newly allocated projected transformers.

If a value of a variable in list proj appears in t of tl, it is projected. New transformers are allocated to build the projection list.

Parameters

tl	l
proj	roj

Definition at line 730 of file transformer_list.c.

{
  list ptl = NIL;
  FOREACH(TRANSFORMER, t, tl) {
    list apl = NIL; // actual projection list
    transformer nt = copy_transformer(t);
    FOREACH(ENTITY, v, proj) {
      if(entity_is_argument_p(v, transformer_arguments(t))) {
        entity ov = entity_to_old_value(v);
        apl = CONS(ENTITY, ov, apl);
      }
      apl = CONS(ENTITY, v, apl);
    }
    nt = safe_transformer_projection(nt, apl);
    ptl = CONS(TRANSFORMER, nt, ptl);
    gen_free_list(apl);
  }
  ptl = gen_nreverse(ptl);
  return ptl;
}

References CONS, copy_transformer(), ENTITY, entity_is_argument_p(), entity_to_old_value(), FOREACH, gen_free_list(), gen_nreverse(), NIL, safe_transformer_projection(), TRANSFORMER, and transformer_arguments.

Referenced by transformer_list_multiple_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_to_active_transformer_list()

list transformer_list_to_active_transformer_list

(

list

tl

)

Parameters

tl

l

Definition at line 454 of file transformer_list.c.

{
  list atl = NIL;
 
  FOREACH(TRANSFORMER, tf, tl) {
    if(!ENDP(transformer_arguments(tf)))
      atl = CONS(TRANSFORMER, copy_transformer(tf), atl);
  }
 
  atl = gen_nreverse(atl);
 
  return atl;
}

References CONS, copy_transformer(), ENDP, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.

Referenced by whileloop_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_to_argument()

list transformer_list_to_argument

(

list

tl

)

Returns the list of variables modified by at least one transformer in tl.

Parameters

tl

l

Definition at line 753 of file transformer_list.c.

{
  list vl = NIL;
 
  FOREACH(TRANSFORMER, t, tl) {
    FOREACH(ENTITY, v, transformer_arguments(t)) {
      if(!gen_in_list_p(v, vl))
        vl = CONS(ENTITY, v, vl);
    }
  }
 
  vl = gen_nreverse(vl);
 
  return vl;
}

References CONS, ENTITY, FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.

Referenced by transformer_list_multiple_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_to_transformer()

transformer transformer_list_to_transformer

(

list

ltl

)

Reduce the transformer list ltl to one transformer using the convex hull operator.

Parameters

ltl

tl

Definition at line 434 of file transformer_list.c.

{
  return generic_transformer_list_to_transformer(ltl, false);
}

References generic_transformer_list_to_transformer().

Referenced by complete_any_loop_transformer(), complete_repeatloop_transformer(), new_complete_whileloop_transformer(), transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_transitive_closure()

transformer transformer_list_transitive_closure

(

list

tfl

)

Compute (U tfl)*.

Parameters

tfl

fl

Definition at line 1141 of file transformer_list.c.

{
  return transformer_list_generic_transitive_closure(tfl, true);
}

References transformer_list_generic_transitive_closure().

Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and unstructured_to_flow_insensitive_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_transitive_closure_plus()

transformer transformer_list_transitive_closure_plus

(

list

tfl

)

Compute (U tfl)+.

Parameters

tfl

fl

Definition at line 1147 of file transformer_list.c.

{
  return transformer_list_generic_transitive_closure(tfl, false);
}

References transformer_list_generic_transitive_closure().

Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_list_with_effect()

list transformer_list_with_effect	(	list	tl,
		entity	v
	)

build a sublist sl of the transformer list tl with transformers that modify the value of variable v

Parameters

tl

l

Definition at line 771 of file transformer_list.c.

{
  list sl = NIL;
 
  FOREACH(TRANSFORMER, t, tl){
    if(entity_is_argument_p(v, transformer_arguments(t)))
      sl = CONS(TRANSFORMER, t, sl);
  }
  sl = gen_nreverse(sl);
  return sl;
}

References CONS, entity_is_argument_p(), FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.

Referenced by transformer_list_multiple_closure_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

two_transformers_to_list()

list two_transformers_to_list	(	transformer	t1,
		transformer	t2
	)

Transformer two transformers into a correct transformer list.

Could be generalized to any number of transformers using a varargs... and more thinking.

Two transformers are obtained for loops that may be skipped or entered and for tests whose condition is not statically decidable.

This is a very dangerous step that should not always be taken. It is useful to ease the detection of identity paths, but it looses a lot of information. So almost identity path might simply be better identified elsewhere

Parameters

t1	1
t2	2

Definition at line 316 of file transformer_list.c.

{
  list tl = NIL;
  if(transformer_empty_p(t1)) {
    if(transformer_empty_p(t2)) {
      tl = NIL;
    }
    else {
      tl = CONS(TRANSFORMER, t2, NIL);
    }
  }
  else {
    if(transformer_empty_p(t2)) {
      tl = CONS(TRANSFORMER, t1, NIL);
    }
    else {
 
      /* This is a very dangerous step that should not always be
         taken. It is useful to ease the detection of identity
         paths, but it looses a lot of information. So almost
         identity path might simply be better identified elsewhere */
      /*
      if(ENDP(transformer_arguments(t1))) {
        free_transformer(t1);
        t1 = transformer_identity();
      }
 
      if(ENDP(transformer_arguments(t2))) {
        free_transformer(t2);
        t2 = transformer_identity();
      }
      */
 
      if(transformer_identity_p(t1)) {
        if(transformer_identity_p(t2)) {
          tl = CONS(TRANSFORMER, t1, NIL);
          free_transformer(t2);
        }
        else {
          tl = CONS(TRANSFORMER, t1,
                    CONS(TRANSFORMER, t2, NIL));
        }
      }
      else {
        if(transformer_identity_p(t2)) {
          tl = CONS(TRANSFORMER, t2,
                    CONS(TRANSFORMER, t1, NIL));
        }
        else {
          tl = CONS(TRANSFORMER, t1,
                    CONS(TRANSFORMER, t2, NIL));
        }
      }
    }
  }
  return tl;
}

References CONS, free_transformer(), NIL, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().

Referenced by complete_any_loop_transformer_list(), and complete_repeatloop_transformer_list().

Here is the call graph for this function:

Here is the caller graph for this function: