ri_to_preconditions.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 "control.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "misc.h"
#include "properties.h"
#include "ray_dte.h"
#include "sommet.h"
#include "sg.h"
#include "polyedre.h"
#include "transformer.h"
#include "semantics.h"

Include dependency graph for ri_to_preconditions.c:

Go to the source code of this file.

Macros
#define	DEBUG_TEST_TO_POSTCONDITION   7

Functions
list	get_module_global_arguments ()
	ri_to_preconditions.c More...
void	set_module_global_arguments (list args)
transformer	statement_to_postcondition (transformer, statement)
	end of the non recursive section More...
static transformer	block_to_postcondition (transformer b_pre, list b)
static transformer	test_to_postcondition (transformer pre, test t, transformer tf)
static transformer	expression_to_postcondition (transformer pre, expression exp, transformer tf)
static transformer	call_to_postcondition (transformer pre, call c, transformer tf)
static transformer	fortran_data_to_prec_for_variables (entity m, list le)
	a remake that works in all cases. More...
static transformer	c_data_to_prec_for_variables (entity m, list le)
static transformer	data_to_prec_for_variables (entity m, list le)
list	effects_to_entity_list (list lef)
	returns an allocated list of entities that appear in lef. More...
transformer	data_to_precondition (entity m)
	restricted to variables with effects. More...
transformer	all_data_to_precondition (entity m)
	any variable is included. More...
static transformer	instruction_to_postcondition (transformer pre, instruction i, transformer tf)
static void	add_reference_information (transformer pre, statement s, bool renaming)
	Assume that all references are legal. More...
void	precondition_add_reference_information (transformer pre, statement s)
void	transformer_add_reference_information (transformer tf, statement s)
void	precondition_add_type_information (transformer pre)
transformer	propagate_preconditions_in_declarations (list dl, transformer pre, void(*process_initial_expression)(expression, transformer))
	This function is mostly copied from declarations_to_transformer(). More...

Variables
static list	module_global_arguments = NIL
	semantical analysis More...

Macro Definition Documentation

DEBUG_TEST_TO_POSTCONDITION

#define DEBUG_TEST_TO_POSTCONDITION   7

Function Documentation

add_reference_information()

static void add_reference_information ( transformer  pre, statement  s, bool  renaming  )

static

Assume that all references are legal.

Assume that variables used in array declarations are not modified in the module.

This assert is too strong in argument lists in Fortran and everywhere in C

Definition at line 623 of file ri_to_preconditions.c.

{
  list efs = load_proper_rw_effects_list(s);
 
  FOREACH(EFFECT, e, efs) {
    reference r = effect_any_reference(e);
    list li = reference_indices(r);
 
    if(!ENDP(li)){
      entity v = reference_variable(r);
      variable tv = type_variable(ultimate_type(entity_type(v)));
      basic b = variable_basic(tv);
      list ld = NIL;
 
      pips_assert("Variable must be of type 'variable'",
                  type_variable_p(entity_type(v)));
      if(!basic_pointer_p(b)) {
        ld = variable_dimensions(tv);
        /* This assert is too strong in argument lists in Fortran and
           everywhere in C */
        //pips_assert("Reference dimension = array dimension",
        //        gen_length(li)==gen_length(ld));
        pips_assert("Reference dimension = array dimension",
                    gen_length(li)<=gen_length(ld));
        FOREACH(EXPRESSION, i, li) {
          normalized ni = NORMALIZE_EXPRESSION(i);
          if(normalized_linear_p(ni)) {
            Pvecteur vi = normalized_linear(ni);
            dimension d = DIMENSION(CAR(ld));
            normalized nl = NORMALIZE_EXPRESSION(dimension_lower(d));
            normalized nu = NORMALIZE_EXPRESSION(dimension_upper(d));
            if(normalized_linear_p(nl) && normalized_linear_p(nu)) {
              Pvecteur vl = normalized_linear(nl);
              Pvecteur vu = normalized_linear(nu);
 
              if(value_mappings_compatible_vector_p(vi)) {
                if(value_mappings_compatible_vector_p(vl)) {
                  Pvecteur cv = vect_substract(vl, vi);
 
                  if(renaming)
                    upwards_vect_rename(cv, pre);
                  if(!vect_constant_p(cv) || vect_coeff(TCST, cv) > 0) {
                    transformer_inequality_add(pre, cv);
                  }
                  else {
                    vect_rm(cv);
                  }
                }
 
                if(value_mappings_compatible_vector_p(vu)) {
                  Pvecteur cv = vect_substract(vi, vu);
 
                  if(renaming)
                    upwards_vect_rename(cv, pre);
                  if(!vect_constant_p(cv) || vect_coeff(TCST, cv) > 0) {
                    transformer_inequality_add(pre, cv);
                  }
                  else {
                    vect_rm(cv);
                  }
                }
              }
 
            }
          }
          POP(ld);
        }
      }
    }
  }
}

References basic_pointer_p, CAR, DIMENSION, dimension_lower, dimension_upper, EFFECT, effect_any_reference, ENDP, entity_type, EXPRESSION, FOREACH, gen_length(), load_proper_rw_effects_list(), NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, POP, reference_indices, reference_variable, TCST, transformer_inequality_add(), type_variable, type_variable_p, ultimate_type(), upwards_vect_rename(), value_mappings_compatible_vector_p(), variable_basic, variable_dimensions, vect_coeff(), vect_constant_p(), vect_rm(), and vect_substract().

Referenced by precondition_add_reference_information(), and transformer_add_reference_information().

Here is the call graph for this function:

Here is the caller graph for this function:

all_data_to_precondition()

transformer all_data_to_precondition

(

entity

m

)

any variable is included.

FI: it would be nice, if only for debugging, to pass a more restricted list...

This assumes the all variables declared in a statement is also declared at the module level.

Definition at line 536 of file ri_to_preconditions.c.

{
  /* FI: it would be nice, if only for debugging, to pass a more
     restricted list...
 
     This assumes the all variables declared in a statement is also
     declared at the module level. */
  //  transformer pre =
  // data_to_prec_for_variables(m, code_declarations(entity_code(m)));
  list dl = module_to_all_declarations(m);
  transformer pre = data_to_prec_for_variables(m, dl);
 
  gen_free_list(dl);
 
  return pre;
}

References data_to_prec_for_variables(), gen_free_list(), and module_to_all_declarations().

Referenced by initial_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

block_to_postcondition()

static transformer block_to_postcondition ( transformer  b_pre, list  b  )

static

The first statement of the block must receive a copy of the block precondition to avoid data sharing

to avoid accumulating equivalence equalities

the precondition has been allocated as post

Definition at line 111 of file ri_to_preconditions.c.

{
    statement s;
    transformer post;
    transformer s_pre = transformer_undefined;
    list ls = b;
 
    debug(8,"block_to_postcondition","begin pre=%x\n", b_pre);
 
    /* The first statement of the block must receive a copy
     * of the block precondition to avoid data sharing
     */
 
    if(ENDP(ls))
        /* to avoid accumulating equivalence equalities */
        post = transformer_dup(b_pre);
    else {
        s = STATEMENT(CAR(ls));
        s_pre = transformer_dup(b_pre);
        post = statement_to_postcondition(s_pre, s);
        for (POP(ls) ; !ENDP(ls); POP(ls)) {
            s = STATEMENT(CAR(ls));
            /* the precondition has been allocated as post */
            s_pre = post;
            post = statement_to_postcondition(s_pre, s);
            // FI: within a long loop body, do not replicate the loop
            // bound constraints
            post = transformer_normalize(post, 2);
        }
    }
 
    pips_debug(8,"post=%p end\n", post);
    return post;
}

References CAR, debug(), ENDP, pips_debug, POP, STATEMENT, statement_to_postcondition(), transformer_dup(), transformer_normalize(), and transformer_undefined.

Referenced by instruction_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

c_data_to_prec_for_variables()

static transformer c_data_to_prec_for_variables ( entity  m, list  le  )

static

look for static entities with an initial value.

e may not have values but its initialization expression may refer other variables which have values, however they are not likely to be static initializations.

any_expression_to_transformer may end up with an undefined transformer ...

Parameters

le

of entity

Definition at line 453 of file ri_to_preconditions.c.

{
  transformer pre = transformer_identity();
  transformer pre_r = transformer_undefined; // range of pre
  //linear_hashtable_pt b = linear_hashtable_make(); /* already seen */
  //list ce = list_undefined;
 
  pips_debug(8, "begin for %s\n", module_local_name(m));
 
  /* look for static entities with an initial value. */
  FOREACH(ENTITY, e, le) {
    if(variable_static_p(e) && entity_has_values_p(e)) {
      /* e may not have values but its initialization expression may
         refer other variables which have values, however they are not
         likely to be static initializations. */
      expression ie = variable_initial_expression(e);
      transformer pre_r = transformer_range(pre);
      transformer npre = transformer_undefined;
      if( !expression_undefined_p(ie) )
          npre = any_expression_to_transformer(e, ie, pre_r, false);
      /* any_expression_to_transformer may end up with an undefined transformer ... */
      if(transformer_undefined_p(npre))
          npre=transformer_identity();
 
      pips_debug(8, "begin for variable %s\n", entity_name(e));
 
 
      pre = transformer_combine(pre, npre);
      pre = transformer_safe_normalize(pre, 2);
      free_transformer(npre);
      free_transformer(pre_r);
    }
  }
 
  pre = transformer_temporary_value_projection(pre);
  pre_r = transformer_range(pre);
  free_transformer(pre);
 
  ifdebug(8) {
    dump_transformer(pre_r);
    pips_debug(8, "end for %s\n", module_local_name(m));
  }
 
  return pre_r;
}

References any_expression_to_transformer(), dump_transformer, ENTITY, entity_has_values_p(), entity_name, expression_undefined_p, FOREACH, free_transformer(), ifdebug, module_local_name(), pips_debug, transformer_combine(), transformer_identity(), transformer_range(), transformer_safe_normalize(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, variable_initial_expression(), and variable_static_p().

Referenced by data_to_prec_for_variables().

Here is the call graph for this function:

Here is the caller graph for this function:

call_to_postcondition()

static transformer call_to_postcondition ( transformer  pre, call  c, transformer  tf  )

static

there is room for improvement because assign is now the only well handled intrinsic

impedance problem: build an expression from call c

propagate precondition pre as summary precondition of user functions

FI: don't! Summary preconditions are computed independently

Declared in preprocessor.h

This cannot occur in Fortran, but is possible in C.

Definition at line 281 of file ri_to_preconditions.c.

{
  transformer post = transformer_undefined;
  entity e = call_function(c);
  tag tt;
 
  pips_debug(8,"begin\n");
 
  switch (tt = value_tag(entity_initial(e))) {
  case is_value_intrinsic:
    /* there is room for improvement because assign is now the
       only well handled intrinsic */
    pips_debug(5, "intrinsic function %s\n",
               entity_name(e));
    if(get_bool_property("SEMANTICS_RECOMPUTE_EXPRESSION_TRANSFORMERS")
       && ENTITY_ASSIGN_P(call_function(c))) {
      entity f = call_function(c);
      list args = call_arguments(c);
      /* impedance problem: build an expression from call c */
      expression expr = make_expression(make_syntax(is_syntax_call, c),
                                        normalized_undefined);
      //list ef = expression_to_proper_effects(expr);
      list ef = expression_to_proper_constant_path_effects(expr);
      transformer pre_r = transformer_range(pre);
      transformer new_tf = intrinsic_to_transformer(f, args, pre_r, ef);
 
      post = transformer_apply(new_tf, pre);
      syntax_call(expression_syntax(expr)) = call_undefined;
      free_expression(expr);
      free_transformer(new_tf);
      free_transformer(pre_r);
    }
    else {
      post = transformer_apply(tf, pre);
    }
    /* propagate precondition pre as summary precondition
       of user functions */
    /* FI: don't! Summary preconditions are computed independently*/
    /*
      if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
      list args = call_arguments(c);
      expressions_to_summary_precondition(pre, args);
      }
    */
    break;
  case is_value_code:
    pips_debug(5, "external function %s\n", entity_name(e));
    if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
      /*
        list args = call_arguments(c);
 
        transformer pre_callee = transformer_dup(pre);
        pre_callee =
        add_formal_to_actual_bindings(c, pre_callee);
        add_module_call_site_precondition(e, pre_callee);
      */
      /*
        expressions_to_summary_precondition(pre, args);
      */
    }
    post = transformer_apply(tf, pre);
    break;
  case is_value_symbolic:
  case is_value_constant: {
    /* Declared in preprocessor.h */
    /* This cannot occur in Fortran, but is possible in C. */
    if(c_module_p(get_current_module_entity())) {
      post = transformer_apply(tf, pre);
    }
    else {
      pips_internal_error("call to symbolic or constant %s",
                          entity_name(e));
    }
    break;
  }
  case is_value_unknown:
    pips_internal_error("unknown function %s", entity_name(e));
    break;
  default:
    pips_internal_error("unknown tag %d", tt);
  }
 
  pips_debug(8,"end\n");
 
  return post;
}

References c_module_p(), call_arguments, call_function, call_undefined, ENTITY_ASSIGN_P, entity_initial, entity_name, expression_syntax, expression_to_proper_constant_path_effects(), f(), free_expression(), free_transformer(), get_bool_property(), get_current_module_entity(), intrinsic_to_transformer(), is_syntax_call, is_value_code, is_value_constant, is_value_intrinsic, is_value_symbolic, is_value_unknown, make_expression(), make_syntax(), normalized_undefined, pips_debug, pips_internal_error, SEMANTICS_INTERPROCEDURAL, syntax_call, transformer_apply(), transformer_range(), transformer_undefined, and value_tag.

Referenced by instruction_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

data_to_prec_for_variables()

static transformer data_to_prec_for_variables ( entity  m, list  le  )

static

Parameters

le

of entity

Definition at line 499 of file ri_to_preconditions.c.

{
  transformer tf = transformer_undefined;
 
  if(c_language_module_p(m))
    tf = c_data_to_prec_for_variables(m, le);
  else if(fortran_language_module_p(m) || fortran95_language_module_p(m))
    tf = fortran_data_to_prec_for_variables(m, le);
  else
    pips_internal_error("Unexpected language");
 
  return tf;
}

References c_data_to_prec_for_variables(), c_language_module_p(), fortran95_language_module_p(), fortran_data_to_prec_for_variables(), fortran_language_module_p(), pips_internal_error, and transformer_undefined.

Referenced by all_data_to_precondition(), and data_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

data_to_precondition()

transformer data_to_precondition

(

entity

m

)

restricted to variables with effects.

Definition at line 526 of file ri_to_preconditions.c.

{
  list lef = load_module_intraprocedural_effects(m);
  list le = effects_to_entity_list(lef);
  transformer pre = data_to_prec_for_variables(m, le);
  gen_free_list(le);
  return pre;
}

References data_to_prec_for_variables(), effects_to_entity_list(), gen_free_list(), and load_module_intraprocedural_effects().

Referenced by generic_module_name_to_transformers().

Here is the call graph for this function:

Here is the caller graph for this function:

effects_to_entity_list()

list effects_to_entity_list

(

list

lef

)

returns an allocated list of entities that appear in lef.

an entity may appear several times.

Parameters

lef

ef

Definition at line 516 of file ri_to_preconditions.c.

{
  list le = NIL;
  MAP(EFFECT, e,
      le = CONS(ENTITY, reference_variable(effect_any_reference(e)), le),
      lef);
  return gen_nreverse(le);
}

References CONS, EFFECT, effect_any_reference, ENTITY, gen_nreverse(), MAP, NIL, and reference_variable.

Referenced by data_to_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

expression_to_postcondition()

static transformer expression_to_postcondition ( transformer  pre, expression  exp, transformer  tf  )

static

Wild guess. See what should be done in call_to_postcondition()

Definition at line 260 of file ri_to_preconditions.c.

{
  transformer post = transformer_undefined;
 
  if(get_bool_property("SEMANTICS_RECOMPUTE_EXPRESSION_TRANSFORMERS")) {
    /* Wild guess. See what should be done in call_to_postcondition() */
    //list el = expression_to_proper_effects(exp);
    list el = expression_to_proper_constant_path_effects(exp);
    transformer new_tf = expression_to_transformer(exp, pre, el);
    post = transformer_apply(new_tf, pre);
    free_transformer(new_tf);
  }
  else
    post = transformer_apply(tf, pre);
 
  return post;
}

References exp, expression_to_proper_constant_path_effects(), expression_to_transformer(), free_transformer(), get_bool_property(), transformer_apply(), and transformer_undefined.

Referenced by instruction_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

fortran_data_to_prec_for_variables()

static transformer fortran_data_to_prec_for_variables ( entity  m, list  le  )

static

a remake that works in all cases.

FC. Isn'it a bit presumptuous? FI.

This function works for C as well as Fortran. Its name should be initial_value_to_preconditions.

FI: It remains to be enhanced to handle more cases for non-integer types. EvalExpression() should be extended to non-integer types. The new fields of data structure "constant" should be exploited.

already seen

look for entities with an initial value.

Parameters

le

of entity

Definition at line 383 of file ri_to_preconditions.c.

{
  transformer pre = transformer_identity();
  transformer pre_r = transformer_undefined; // range of pre
  linear_hashtable_pt b = linear_hashtable_make(); /* already seen */
  //list ce = list_undefined;
 
  pips_debug(8, "begin for %s\n", module_local_name(m));
 
  /* look for entities with an initial value. */
  FOREACH(ENTITY, e, le) {
    value val = entity_initial(e);
 
    pips_debug(8, "begin for variable %s\n", entity_name(e));
 
    if (entity_has_values_p(e) && !linear_hashtable_isin(b, e)) {
      if(value_constant_p(val)) {
        constant c = value_constant(val);
        if (constant_int_p(c)) {
          int int_val = constant_int(value_constant(val));
 
          Pvecteur v = vect_make(VECTEUR_NUL,
                                 (Variable) e, VALUE_ONE,
                                 TCST, int_to_value(-int_val));
          pre = transformer_equality_add(pre, v);
          linear_hashtable_put_once(b, e, e);
        }
        else if (constant_call_p(c)) {
          entity f = constant_call(c);
          basic bt = variable_basic(type_variable(functional_result
                                                  (type_functional(entity_type(f)))));
 
          if((basic_float_p(bt) && float_analyzed_p())
             || (basic_string_p(bt) && string_analyzed_p())
             || (basic_logical_p(bt) && boolean_analyzed_p()) ) {
            Pvecteur v = vect_make(VECTEUR_NUL,
                                   (Variable) e, VALUE_ONE,
                                   (Variable) constant_call(c), VALUE_MONE,
                                   TCST, VALUE_ZERO);
            pre = transformer_equality_add(pre, v);
            linear_hashtable_put_once(b, e, e);
          }
        }
      }
      else if(value_expression_p(val)) {
        expression expr = value_expression(val);
        transformer npre = safe_any_expression_to_transformer(e, expr, pre, false);
 
        pre = transformer_combine(pre, npre);
        pre = transformer_safe_normalize(pre, 2);
        free_transformer(npre);
      }
    }
  }
 
  pre = transformer_temporary_value_projection(pre);
  pre_r = transformer_range(pre);
  free_transformer(pre);
 
  linear_hashtable_free(b);
  pips_assert("some transformer", pre_r != transformer_undefined);
 
  ifdebug(8) {
    dump_transformer(pre_r);
    pips_debug(8, "end for %s\n", module_local_name(m));
  }
 
  return pre_r;
}

References basic_float_p, basic_logical_p, basic_string_p, boolean_analyzed_p(), constant_call, constant_call_p, constant_int, constant_int_p, dump_transformer, ENTITY, entity_has_values_p(), entity_initial, entity_name, entity_type, f(), float_analyzed_p(), FOREACH, free_transformer(), functional_result, ifdebug, int_to_value, linear_hashtable_free(), linear_hashtable_isin(), linear_hashtable_make(), linear_hashtable_put_once(), module_local_name(), pips_assert, pips_debug, safe_any_expression_to_transformer(), string_analyzed_p(), TCST, transformer_combine(), transformer_equality_add(), transformer_identity(), transformer_range(), transformer_safe_normalize(), transformer_temporary_value_projection(), transformer_undefined, type_functional, type_variable, value_constant, value_constant_p, value_expression, value_expression_p, VALUE_MONE, VALUE_ONE, VALUE_ZERO, variable_basic, vect_make(), and VECTEUR_NUL.

Referenced by data_to_prec_for_variables().

Here is the call graph for this function:

Here is the caller graph for this function:

get_module_global_arguments()

list get_module_global_arguments

(

void

)

ri_to_preconditions.c

Definition at line 98 of file ri_to_preconditions.c.

{
    return module_global_arguments;
}

References module_global_arguments.

Referenced by statement_to_postcondition(), and statement_to_total_precondition().

Here is the caller graph for this function:

instruction_to_postcondition()

static transformer instruction_to_postcondition ( transformer  pre, instruction  i, transformer  tf  )

static

never reached: post = pre;

Definition at line 554 of file ri_to_preconditions.c.

{
    transformer post = transformer_undefined;
    test t;
    loop l;
    whileloop wl;
    forloop fl;
    call c;
    expression exp;
 
    pips_debug(9,"begin pre=%p tf=%p\n", pre, tf);
 
    switch(instruction_tag(i)) {
      case is_instruction_block:
        post = block_to_postcondition(pre, instruction_block(i));
        break;
      case is_instruction_test:
        t = instruction_test(i);
        post = test_to_postcondition(pre, t, tf);
        break;
      case is_instruction_loop:
        l = instruction_loop(i);
        post = loop_to_postcondition(pre, l, tf);
        break;
    case is_instruction_whileloop: {
        wl = instruction_whileloop(i);
        if(evaluation_before_p(whileloop_evaluation(wl)))
          post = whileloop_to_postcondition(pre, wl, tf);
        else
          post = repeatloop_to_postcondition(pre, wl, tf);
        break;
    }
    case is_instruction_forloop: {
        fl = instruction_forloop(i);
        post = forloop_to_postcondition(pre, fl, tf);
        break;
    }
      case is_instruction_goto:
        pips_internal_error("unexpected goto in semantics analysis");
        /* never reached: post = pre; */
        break;
      case is_instruction_call:
        c = instruction_call(i);
        post = call_to_postcondition(pre, c, tf);
        break;
      case is_instruction_unstructured:
        post = unstructured_to_postcondition(pre, instruction_unstructured(i),
                                             tf);
        break ;
      case is_instruction_expression:
        exp = instruction_expression(i);
        post = expression_to_postcondition(pre, exp, tf);
        break ;
      case is_instruction_multitest:
        pips_internal_error("Should have been removed by the controlizer?");
        break ;
      default:
        pips_internal_error("unexpected tag %d", instruction_tag(i));
    }
    pips_debug(9,"resultat post, %p:\n", post);
    ifdebug(9) (void) print_transformer(post);
    return post;
}

References block_to_postcondition(), call_to_postcondition(), evaluation_before_p, exp, expression_to_postcondition(), forloop_to_postcondition(), ifdebug, instruction_block, instruction_call, instruction_expression, instruction_forloop, instruction_loop, instruction_tag, instruction_test, instruction_unstructured, instruction_whileloop, is_instruction_block, is_instruction_call, is_instruction_expression, is_instruction_forloop, is_instruction_goto, is_instruction_loop, is_instruction_multitest, is_instruction_test, is_instruction_unstructured, is_instruction_whileloop, loop_to_postcondition(), pips_debug, pips_internal_error, print_transformer, repeatloop_to_postcondition(), test_to_postcondition(), transformer_undefined, unstructured_to_postcondition(), whileloop_evaluation, and whileloop_to_postcondition().

Referenced by statement_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

precondition_add_reference_information()

void precondition_add_reference_information	(	transformer	pre,
		statement	s
	)

Parameters

pre

re

Definition at line 695 of file ri_to_preconditions.c.

{
  add_reference_information(pre, s, false);
}

References add_reference_information().

Referenced by statement_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

precondition_add_type_information()

void precondition_add_type_information

(

transformer

pre

)

Parameters

pre

re

Definition at line 705 of file ri_to_preconditions.c.

{
  transformer_add_type_information(pre);
}

References transformer_add_type_information().

Here is the call graph for this function:

propagate_preconditions_in_declarations()

transformer propagate_preconditions_in_declarations	(	list	dl,
		transformer	pre,
		void(*)(expression, transformer)	process_initial_expression
	)

This function is mostly copied from declarations_to_transformer().

It is used to recompute intermediate preconditions and to process the initialization expressions with the proper precondition. For instance, in:

int i = 10, j = i+1, a[i], k = foo(i);

you need to collect information about i's value to initialize j, dimension a and compute the summary precondition of function foo().

We assume that the precondition does not change within the expression as in:

int k = i++ + foo(i);

I do not remember if the standard prohibits this or not, but it may well forbid such expressions or state that the result is undefined.

But you can also have:

int a[i++][foo(i)];

or

int a[i++][j=foo(i)];

and the intermediate steps are overlooked by declaration_to_transformer() but can be checked with a proper process_dimensions() function.

This function can be called from ri_to_preconditions.c to propagate preconditions or from interprocedural.c to compute summary preconditions. In the second case, the necessary side effects are provided by the two functional parameters.

post = transformer_safe_normalize(post, 4);

post = transformer_safe_normalize(post, 4);

btf = transformer_normalize(btf, 4);

Parameters

dl	l
pre	re

Definition at line 977 of file ri_to_preconditions.c.

{
  //entity v = entity_undefined;
  //transformer btf = transformer_undefined;
  //transformer stf = transformer_undefined;
  transformer post = transformer_undefined;
  list l = dl;
 
  pips_debug(8,"begin\n");
 
  if(ENDP(l))
    post = copy_transformer(pre);
  else {
    entity v = ENTITY(CAR(l));
    expression ie = variable_initial_expression(v);
    transformer stf = declaration_to_transformer(v, pre);
    // FI: ongoing implementation
    //transformer stf = (*process_dimensions)(v, pre);
    transformer btf = transformer_dup(stf);
    transformer next_pre = transformer_undefined;
 
    if(!expression_undefined_p(ie)) {
      (*process_initial_expression)(ie, pre);
      free_expression(ie);
    }
 
    post = transformer_safe_apply(stf, pre);
/*     post = transformer_safe_normalize(post, 4); */
    post = transformer_safe_normalize(post, 2);
 
    for (POP(l) ; !ENDP(l); POP(l)) {
      v = ENTITY(CAR(l));
      ie = variable_initial_expression(v);
      if(!expression_undefined_p(ie)) {
        (*process_initial_expression)(ie, post);
        free_expression(ie);
      }
 
      if(!transformer_undefined_p(next_pre))
        free_transformer(next_pre);
      next_pre = post;
      stf = declaration_to_transformer(v, next_pre);
      post = transformer_safe_apply(stf, next_pre);
/*       post = transformer_safe_normalize(post, 4); */
      post = transformer_safe_normalize(post, 2);
      btf = transformer_combine(btf, stf);
/*       btf = transformer_normalize(btf, 4); */
      btf = transformer_normalize(btf, 2);
 
      ifdebug(1)
        pips_assert("btf is a consistent transformer", transformer_consistency_p(btf));
      pips_assert("post is a consistent transformer if pre is defined",
                    transformer_undefined_p(pre) || transformer_consistency_p(post));
    }
    free_transformer(btf);
  }
 
  pips_debug(8, "end\n");
  return post;
}

References CAR, copy_transformer(), declaration_to_transformer(), ENDP, ENTITY, expression_undefined_p, free_expression(), free_transformer(), ifdebug, pips_assert, pips_debug, POP, stf(), transformer_combine(), transformer_consistency_p(), transformer_dup(), transformer_normalize(), transformer_safe_apply(), transformer_safe_normalize(), transformer_undefined, transformer_undefined_p, and variable_initial_expression().

Referenced by memorize_precondition_for_summary_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

set_module_global_arguments()

void set_module_global_arguments

(

list

args

)

Parameters

args

rgs

Definition at line 103 of file ri_to_preconditions.c.

{
    module_global_arguments = args;
}

References module_global_arguments.

Referenced by module_name_to_preconditions(), and module_name_to_total_preconditions().

Here is the caller graph for this function:

statement_to_postcondition()

transformer statement_to_postcondition	(	transformer	pre,
		statement	s
	)

end of the non recursive section

Refine the precondition pre of s using side effects and compute its postcondition post.

Postcondition post is returned.

FI: if the statement s is a loop, the transformer tf is not the statement transformer but the transformer T* which maps the precondition pre onto the loop body precondition. The real statement transformer is obtained by executing the loop till it is exited. See complete_any_loop_transformer()

ACHTUNG! "pre" is likely to be misused! FI, Sept. 3, 1990

To provide information for warnings

FC: if the code is not reachable (thanks to STOP or GOTO), which is a structural information, the precondition is just empty.

keep only global initial scalar integer values; else, you might end up giving the same xxx::old name to two different local values

FI: OK, to be fixed when the declaration representation is frozen.

add array references information

add type information

Add information from declarations when useful

FI: it might be better to have another function, declarations_to_postconditions(), which might be slightly more accurate? Note that declarations_to_transformer() does compute the postcondition, but free it before returning the transformer

Remove information when leaving a block

add equivalence equalities

eliminate redundancy, rational redundancy but not integer redundancy.

FI: nice... but time consuming!

Version 3 is OK. Equations are over-used and make inequalities uselessly conplex

pre = transformer_normalize(pre, 3);

pre = transformer_normalize(pre, 6);

pre = transformer_normalize(pre, 7);

The double normalization could be avoided with a non-heuristics approach. For ocean, its overhead is 34s out of 782.97 to give 816.62s: 5 %. The double normalization is also useful for some exit conditions of WHILE loops (w05, w06, w07). It is not powerful enough for preconditions containing equations with three or more variables such as fraer01,...

BC: pre = transformer_normalize(pre, 4);

FI->BC: why keep a first normalization before the next one? FI: Because a level 2 normalization does things that a level 4 does not perform! Although level 2 is much faster...

pre = transformer_normalize(pre, 2);

Do not keep too many initial variables in the preconditions: not so smart? invariance01.c: information is lost... Since C passes values, it is usually useless to keep track of the initial values of arguments because programmers usually do not modify them. However, when they do modify the formal parameter, information is lost.

See character01.c, but other counter examples above about non_initial_values.

FI: redundancy possibly added. See asopt02. Maybe this should be moved up before the normalization step.

store the precondition in the ri

pre = statement_precondition(s);

post = instruction_to_postcondition(pre, i, tf);

Parameters

pre	re
s	postcondition of predecessor

Definition at line 712 of file ri_to_preconditions.c.

{
    transformer post = transformer_undefined;
    instruction i = statement_instruction(s);
    /* FI: if the statement s is a loop, the transformer tf is not the
       statement transformer but the transformer T* which maps the
       precondition pre onto the loop body precondition. The real
       statement transformer is obtained by executing the loop till
       it is exited. See complete_any_loop_transformer() */
    transformer tf = load_statement_transformer(s);
 
    /* ACHTUNG! "pre" is likely to be misused! FI, Sept. 3, 1990 */
 
    pips_debug(1,"begin\n");
 
    pips_assert("The statement precondition is defined",
                pre != transformer_undefined);
 
    ifdebug(1) {
        int so = statement_ordering(s);
        (void) fprintf(stderr, "statement %03td (%d,%d), precondition %p:\n",
                       statement_number(s), ORDERING_NUMBER(so),
                       ORDERING_STATEMENT(so), pre);
        (void) print_transformer(pre) ;
    }
 
    pips_assert("The statement transformer is defined",
                tf != transformer_undefined);
    ifdebug(1) {
        int so = statement_ordering(s);
        (void) fprintf(stderr, "statement %03td (%d,%d), transformer %p:\n",
                       statement_number(s), ORDERING_NUMBER(so),
                       ORDERING_STATEMENT(so), tf);
        (void) print_transformer(tf) ;
    }
 
    /* To provide information for warnings */
    push_statement_on_statement_global_stack(s);
 
    if (!statement_reachable_p(s))
    {
        /* FC: if the code is not reachable (thanks to STOP or GOTO), which
         * is a structural information, the precondition is just empty.
         */
      pre = empty_transformer(pre);
    }
 
    if (load_statement_precondition(s) == transformer_undefined) {
        /* keep only global initial scalar integer values;
           else, you might end up giving the same xxx#old name to
           two different local values */
        list non_initial_values =
            arguments_difference(transformer_arguments(pre),
                                 get_module_global_arguments());
        list dl = declaration_statement_p(s) ? statement_declarations(s) : NIL;
 
        /* FI: OK, to be fixed when the declaration representation is
           frozen. */
        if(!ENDP(statement_declarations(s)) && !statement_block_p(s)
           && !declaration_statement_p(s)) {
          // FI: Just to gain some time before dealing with controlizer and declarations updates
          //pips_internal_error("Statement %p carries declarations");
          pips_user_warning("Statement %p with instruction carries declarations\n",
                            instruction_identification(statement_instruction(s)));
        }
 
        MAPL(cv,
         {
           entity v = ENTITY(CAR(cv));
           ENTITY_(CAR(cv)) = entity_to_old_value(v);
         },
             non_initial_values);
 
        /* add array references information */
        if(get_bool_property("SEMANTICS_TRUST_ARRAY_REFERENCES")) {
            precondition_add_reference_information(pre, s);
        }
 
        /* add type information */
        if(get_bool_property("SEMANTICS_USE_TYPE_INFORMATION")
          || get_bool_property("SEMANTICS_USE_TYPE_INFORMATION_IN_PRECONDITIONS")) {
          transformer_add_type_information(pre);
        }
 
        /* Add information from declarations when useful */
        if(declaration_statement_p(s) && !ENDP(dl)) {
          /* FI: it might be better to have another function,
             declarations_to_postconditions(), which might be
             slightly more accurate? Note that
             declarations_to_transformer() does compute the
             postcondition, but free it before returning the transformer */
          transformer dt = declarations_to_transformer(dl, pre);
          transformer dpre = transformer_apply(dt, pre);
 
          //post = instruction_to_postcondition(dpre, i, tf);
          //free_transformer(dpre);
          // FI: Let's assume that declaration statement do not
          //require further analysis
          post = dpre;
        }
        else {
          post = instruction_to_postcondition(pre, i, tf);
        }
 
        /* Remove information when leaving a block */
        if(statement_block_p(s) && !ENDP(statement_declarations(s))) {
          list vl = variables_to_values(statement_declarations(s));
 
          if(!ENDP(vl))
            post = safe_transformer_projection(post, vl);
        }
        else if(statement_loop_p(s)
                && !get_bool_property("SEMANTICS_KEEP_DO_LOOP_EXIT_CONDITION")) {
          loop l = statement_loop(s);
          entity i = loop_index(l);
          list vl = variable_to_values(i);
          post = safe_transformer_projection(post, vl);
        }
 
        /* add equivalence equalities */
        pre = tf_equivalence_equalities_add(pre);
 
        /* eliminate redundancy, rational redundancy but not integer redundancy.  */
 
        /* FI: nice... but time consuming! */
        /* Version 3 is OK. Equations are over-used and make
         * inequalities uselessly conplex
         */
        /* pre = transformer_normalize(pre, 3); */
 
        /* pre = transformer_normalize(pre, 6); */
        /* pre = transformer_normalize(pre, 7); */
 
        /* The double normalization could be avoided with a non-heuristics
           approach. For ocean, its overhead is 34s out of 782.97 to give
           816.62s: 5 %. The double normalization is also useful for some
           exit conditions of WHILE loops (w05, w06, w07). It is not
           powerful enough for preconditions containing equations with
           three or more variables such as fraer01,...*/
 
        if(!transformer_consistency_p(pre)) {
          ;
        }
        /* BC: pre = transformer_normalize(pre, 4); */
        /* FI->BC: why keep a first normalization before the next
           one? FI: Because a level 2 normalization does things that
           a level 4 does not perform! Although level 2 is much
           faster... */
        pre = transformer_normalize(pre, 2);
 
        if(!transformer_consistency_p(pre)) {
          ;
        }
        /* pre = transformer_normalize(pre, 2); */
        if(get_int_property("SEMANTICS_NORMALIZATION_LEVEL_BEFORE_STORAGE")
           == 4)
          // FI HardwareAccelerator/freia_52: this level does not
          // handle the signs properly for simple equations like -i==0
          // and it does not sort constraints lexicographically!
          pre = transformer_normalize(pre, 4);
        else
          pre = transformer_normalize(pre, 2);
 
        if(!transformer_consistency_p(pre)) {
            int so = statement_ordering(s);
            fprintf(stderr, "statement %03td (%d,%d), precondition %p end:\n",
                           statement_number(s), ORDERING_NUMBER(so),
                           ORDERING_STATEMENT(so), pre);
            print_transformer(pre);
            pips_internal_error("Non-consistent precondition after update");
        }
 
        /* Do not keep too many initial variables in the
         * preconditions: not so smart? invariance01.c: information is
         * lost... Since C passes values, it is usually useless to
         * keep track of the initial values of arguments because
         * programmers usually do not modify them. However, when they
         * do modify the formal parameter, information is lost.
         *
         * See character01.c, but other counter examples above about
         * non_initial_values.
         *
         * FI: redundancy possibly added. See asopt02. Maybe this
         * should be moved up before the normalization step.
         */
        if(get_bool_property("SEMANTICS_FILTER_INITIAL_VALUES")) {
          pre = transformer_filter(pre, non_initial_values);
          pre = transformer_normalize(pre, 2);
        }
 
        /* store the precondition in the ri */
        store_statement_precondition(s, pre);
 
        gen_free_list(non_initial_values);
    }
    else {
        pips_debug(8,"precondition already available\n");
        /* pre = statement_precondition(s); */
        (void) print_transformer(pre);
        pips_internal_error("precondition already computed");
    }
 
    /* post = instruction_to_postcondition(pre, i, tf); */
 
    ifdebug(1) {
        int so = statement_ordering(s);
        fprintf(stderr, "statement %03td (%d,%d), precondition %p end:\n",
                statement_number(s), ORDERING_NUMBER(so),
                ORDERING_STATEMENT(so), load_statement_precondition(s));
        print_transformer(load_statement_precondition(s)) ;
    }
 
    ifdebug(1) {
        int so = statement_ordering(s);
        fprintf(stderr, "statement %03td (%d,%d), postcondition %p:\n",
                statement_number(s), ORDERING_NUMBER(so),
                ORDERING_STATEMENT(so), post);
        print_transformer(post) ;
    }
 
    pips_assert("no sharing",post!=pre);
    pop_statement_global_stack();
 
    pips_debug(1, "end\n");
 
    return post;
}

References arguments_difference(), CAR, declaration_statement_p(), declarations_to_transformer(), empty_transformer(), ENDP, ENTITY, ENTITY_, entity_to_old_value(), fprintf(), gen_free_list(), get_bool_property(), get_int_property(), get_module_global_arguments(), ifdebug, instruction_identification(), instruction_to_postcondition(), load_statement_precondition(), load_statement_transformer(), loop_index, MAPL, NIL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, pips_user_warning, pop_statement_global_stack(), precondition_add_reference_information(), print_transformer, push_statement_on_statement_global_stack(), safe_transformer_projection(), statement_block_p, statement_declarations, statement_instruction, statement_loop(), statement_loop_p(), statement_number, statement_ordering, statement_reachable_p(), store_statement_precondition(), tf_equivalence_equalities_add(), transformer_add_type_information(), transformer_apply(), transformer_arguments, transformer_consistency_p(), transformer_filter(), transformer_normalize(), transformer_undefined, variable_to_values(), and variables_to_values().

Referenced by any_loop_to_postcondition(), block_to_postcondition(), dag_to_flow_sensitive_preconditions(), loop_to_postcondition(), module_name_to_preconditions(), process_unreachable_node(), test_to_postcondition(), unstructured_to_postcondition(), unstructured_to_postconditions(), whileloop_to_postcondition(), and whileloop_to_total_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

test_to_postcondition()

static transformer test_to_postcondition ( transformer  pre, test  t, transformer  tf  )

static

there are three levels of flow sensitivity and we have only a bool flag! FI

test conditions are assumed to have no side effects; it might be somewhere in the standard since functions called in an expression e cannot (should not) modify any variable used in e

&& !transformer_identity_p(tf)

convex hull might avoided if it is not required or if it is certainly useless but test information should always be propagated

True and false condition transformers. The nest three variables should be freed.

To obtain the best results, transformer_normalize(x,7) should be applied to subtransformers generated by precondition_add_condition_information() in case of equality condition and in case of string or float analysis.

"strong" transformer normalization to detect dead code generated by the test condition

A normalization of degree 3 is fine

transformer_normalize(pret, 3);

Just to get a stronger normalization with sc_safe_normalize()... which is sc_normalize(), a weak normalization function. FI: I do not understand what's going on.

FI, CA: the following "optimization" was added to avoid a call to Chernikova convex hull that core dumps:-(. 8 September 1993

From a theoretical point of view, pref could always be computed.

FI: removed because it is mathematically wrong in many cases; the negation of the test condition is lost! I keep the structure just in case another core dump occurs (25 April 1997).

To obtain the best results, transformer_normalize(x,7) should be applied to subtransformers generated by precondition_add_condition_information() in case of equality condition and in case of string or float analysis.

transformer_normalize(pref, 3);

Just to get a stronger normalization with sc_safe_normalize()

do not try to compute a refined precondition for an empty block keep the current precondition to store in the precondition statement mapping

Be careful, pre is updated by statement_to_postcondition!

Definition at line 147 of file ri_to_preconditions.c.

{
#   define DEBUG_TEST_TO_POSTCONDITION 7
    expression e = test_condition(t);
    statement st = test_true(t);
    statement sf = test_false(t);
    transformer post;
 
    debug(DEBUG_TEST_TO_POSTCONDITION,"test_to_postcondition","begin\n");
 
    /* there are three levels of flow sensitivity and we have only a
       bool flag! FI */
 
    /* test conditions are assumed to have no side effects; it might
       be somewhere in the standard since functions called in an expression e
       cannot (should not) modify any variable used in e */
 
    if(pips_flag_p(SEMANTICS_FLOW_SENSITIVE) /* && !transformer_identity_p(tf) */) {
        /* convex hull might avoided if it is not required or if it is certainly useless 
         * but test information should always be propagated 
         */
      /* True and false condition transformers. The nest three variables should be freed. */
      transformer tct = condition_to_transformer(e, pre, true);
      transformer fct = condition_to_transformer(e, pre, false);
          /* To obtain the best results, transformer_normalize(x,7) should
             be applied to subtransformers generated by
             precondition_add_condition_information() in case of equality
             condition and in case of string or float analysis. */
      //        transformer pret =
      //  precondition_add_condition_information(transformer_dup(pre),e, pre,
      //                                          true);
      transformer pret = transformer_apply(tct, pre);
 
        transformer pref = transformer_undefined;
 
        transformer postt;
        transformer postf;
 
        /* "strong" transformer normalization to detect dead code generated by the
         * test condition
         */
        /* A normalization of degree 3 is fine */
        /* transformer_normalize(pret, 3); */
        transformer_normalize(pret, 7);
          /* Just to get a stronger normalization with
             sc_safe_normalize()... which is sc_normalize(), a weak
             normalization function. FI: I do not understand what's
             going on. */
          pret = transformer_temporary_value_projection(pret);  
 
        /* FI, CA: the following "optimization" was added to avoid a call
         * to Chernikova convex hull that core dumps:-(. 8  September 1993
         *
         * From a theoretical point of view, pref could always be computed.
         *
         * FI: removed because it is mathematically wrong in many cases;
         * the negation of the test condition is lost! I keep the structure
         * just in case another core dump occurs (25 April 1997).
         */
        if(!empty_statement_p(sf)||true) {
          /* To obtain the best results, transformer_normalize(x,7) should
             be applied to subtransformers generated by
             precondition_add_condition_information() in case of equality
             condition and in case of string or float analysis. */
          /*
            pref = precondition_add_condition_information(transformer_dup(pre),e,
                                                          pre, false);
          */
          pref = transformer_apply(fct, pre);
          /* transformer_normalize(pref, 3); */
          transformer_normalize(pref, 7);
          /* Just to get a stronger normalization with sc_safe_normalize() */
          pref = transformer_temporary_value_projection(pref);  
        }
        else {
            /* do not try to compute a refined precondition for an empty block
             * keep the current precondition to store in the precondition statement mapping
             */
            pref = transformer_dup(pre);
        }
 
        ifdebug(DEBUG_TEST_TO_POSTCONDITION) {
            pips_debug(DEBUG_TEST_TO_POSTCONDITION, "pret=%p\n", pret);
            (void) print_transformer(pret);
            pips_debug(DEBUG_TEST_TO_POSTCONDITION, "pref=%p\n", pref);
            (void) print_transformer(pref);
        }
 
        postt = statement_to_postcondition(pret, st);
        postf = statement_to_postcondition(pref, sf);
        post = transformer_convex_hull(postt, postf);
        free_transformer(postt);
        free_transformer(postf);
    }
    else {
      /* Be careful, pre is updated by statement_to_postcondition! */
        (void) statement_to_postcondition(pre, st);
        (void) statement_to_postcondition(pre, sf);
        post = transformer_apply(tf, pre);
    }
 
    ifdebug(DEBUG_TEST_TO_POSTCONDITION) {
        debug(DEBUG_TEST_TO_POSTCONDITION,"test_to_postcondition",
              "end post=\n");
        (void) print_transformer(post);
    }
 
    return post;
}

References condition_to_transformer(), debug(), DEBUG_TEST_TO_POSTCONDITION, empty_statement_p(), free_transformer(), ifdebug, pips_debug, pips_flag_p, print_transformer, SEMANTICS_FLOW_SENSITIVE, statement_to_postcondition(), test_condition, test_false, test_true, transformer_apply(), transformer_convex_hull(), transformer_dup(), transformer_normalize(), transformer_temporary_value_projection(), and transformer_undefined.

Referenced by instruction_to_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_add_reference_information()

void transformer_add_reference_information	(	transformer	tf,
		statement	s
	)

Parameters

tf

f

Definition at line 700 of file ri_to_preconditions.c.

{
  add_reference_information(tf, s, true);
}

References add_reference_information().

Referenced by statement_to_transformer(), and statement_to_transformer_list().

Here is the call graph for this function:

Here is the caller graph for this function:

Variable Documentation

module_global_arguments

list module_global_arguments = NIL

static

semantical analysis

phasis 2: propagate preconditions from statement to sub-statement, starting from the module 1st statement

For (simple) interprocedural analysis, this phasis should be performed top-down on the call tree.

Most functions are called xxx_to_postcondition although the purpose is to compute preconditions. However transformer are applied to preconditions to produce postconditions. Thus these modules store the preconditions and then compute an independent (i.e. no sharing) postcondition which is returned to be used by the caller.

Preconditions are NEVER shared. Sharing would introduce desastrous side effects when they are updated as for equivalenced variables and would make freeing them impossible. Thus on a recursive path from statement_to_postcondition() to itself the precondition must have been reallocated even when its value is not changed as between a block precondition and the first statement of the block precondition. In the same way statement_to_postcondition() should never returned a postcondition aliased with its precondition argument. Somewhere in the recursive call down the data structures towards call_to_postcondition() some allocation must take place even if the statement as no effect on preconditions.

Preconditions can be used to evaluate sub-expressions because Fortran standard prohibit side effects within an expression. For instance, in: J = I + F(I) function F cannot modify I.

Ambiguity: the type "transformer" is used to abstract statement effects as well as effects combined from the beginning of the module to just before the current statement (precondition) to just after the current statement (postcondition). This is because it was not realized that preconditions could advantageously be seen as transformers of the initial state when designing the ri. include <stdlib.h> another non recursive section used to filter out preconditions

Definition at line 95 of file ri_to_preconditions.c.

Referenced by get_module_global_arguments(), and set_module_global_arguments().