dbm_interface.c File Reference

#include <stdio.h>
#include <string.h>
#include "genC.h"
#include "database.h"
#include "resources.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "workspace-util.h"
#include "effects-util.h"
#include "pipsdbm.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "control.h"
#include "misc.h"
#include "transformer.h"
#include "semantics.h"
#include "properties.h"
#include "preprocessor.h"

Include dependency graph for dbm_interface.c:

Go to the source code of this file.

Functions
transformer	transformer_equality_fix_point (transformer)
	Let A be the affine loop transfert function. More...
transformer	transformer_pattern_fix_point (transformer)
	This fixpoint function was developped to present a talk at FORMA. More...
transformer	transformer_derivative_fix_point (transformer)
	Computation of a transitive closure using constraints on the discrete derivative. More...
transformer	load_completed_statement_transformer (statement s)
	three mappings used throughout semantics analysis: More...
static void	select_fix_point_operator ()
void	add_declaration_list_information (transformer pre, list dl, bool precondition_p)
static void	add_declaration_information (transformer pre, entity m, bool precondition_p)
static void	transformer_add_declaration_information (transformer pre, entity m)
static void	precondition_add_declaration_information (transformer pre, entity m)
bool	transformers_intra_fast (char *module_name)
	Functions to make transformers. More...
bool	transformers_intra_full (char *module_name)
bool	transformers_inter_fast (char *module_name)
bool	transformers_inter_full (char *module_name)
bool	transformers_inter_full_with_points_to (char *module_name)
bool	refine_transformers (char *module_name)
bool	refine_transformers_with_points_to (char *module_name)
bool	summary_transformer (char *module_name)
bool	preconditions_intra (char *module_name)
bool	preconditions_intra_fast (char *module_name)
bool	preconditions_inter_fast (char *module_name)
bool	preconditions_inter_full (char *module_name)
bool	preconditions_inter_full_with_points_to (char *module_name)
bool	total_preconditions_intra (char *module_name)
bool	total_preconditions_inter (char *module_name)
bool	old_summary_precondition (char *module_name)
bool	intraprocedural_summary_precondition (char *module_name)
bool	interprocedural_summary_precondition (char *module_name)
static void	set_use_points_to ()
static void	reset_use_points_to ()
bool	use_points_to_p ()
bool	interprocedural_summary_precondition_with_points_to (char *module_name)
static transformer	main_summary_precondition (entity callee)
	Special case: main module. More...
static transformer	ordinary_summary_precondition (const char *module_name, entity callee)
	Standard cases: called modules. More...
bool	summary_precondition (char *module_name)
bool	summary_total_postcondition (char *module_name)
bool	summary_total_precondition (char *module_name)
void	set_warning_counters (void)
bool	test_warning_counters (void)
bool	generic_module_name_to_transformers (const char *module_name, bool in_context)
	bool generic_module_name_to_transformers(char * module_name, bool in_context): compute a transformer for each statement of a module with a given name; compute also the global transformer for the module More...
bool	module_name_to_transformers_in_context (const char *module_name)
bool	module_name_to_transformers (const char *module_name)
bool	module_name_to_preconditions (const char *module_name)
	resource module_name_to_preconditions(char * module_name): compute a transformer for each statement of a module with a given name; compute also the global transformer for the module More...
bool	module_name_to_total_preconditions (const char *module_name)
transformer	load_summary_transformer (entity e)
void	update_summary_precondition (entity e, transformer t)
	void update_summary_precondition(e, t): t is supposed to be a precondition related to one of e's call sites and translated into e's basis; More...
transformer	load_summary_precondition (entity e)
	summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure that used/produced it More...
transformer	load_summary_total_postcondition (entity e)
	summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure that used/produced it More...
list	load_summary_effects (entity e)
	FI->FI, FI->BC: these two functions should be moved into effects-util or effects-simple. More...
list	load_body_effects (entity e)
list	load_module_intraprocedural_effects (entity e)
void	cumulated_effects_map_print (void)
	ca n'a rien a` faire ici, et en plus, il serait plus inte'ressant d'avoir une fonction void statement_map_print(statement_mapping htp) More...

Variables
transformer(*	transformer_fix_point_operator )(transformer)
	Interface between the untyped database manager and clean code and between pipsmake and clean code. More...
bool	refine_transformers_p = false
	Transformer recomputation cannot be of real use unless an interprocedural analysis is performed. More...
static bool	use_points_to_information_p = false
static int	wc = 0
	FI: Provisional management of warnings. More...

Function Documentation

add_declaration_information()

static void add_declaration_information ( transformer  pre, entity  m, bool  precondition_p  )

static

Definition at line 223 of file dbm_interface.c.

{
  //list decls = code_declarations(value_code(entity_initial(m)));
  list decls = current_module_declarations();
 
  ifdebug(8) {
      pips_debug(8, "Begin for module %s with precondition\n", module_local_name(m));
      print_transformer(pre);
  }
 
  add_declaration_list_information(pre, decls, precondition_p);
 
  ifdebug(8) {
      pips_debug(8, "End for module %s with precondition\n", module_local_name(m));
      print_transformer(pre);
  }
 
}

References add_declaration_list_information(), current_module_declarations(), ifdebug, module_local_name(), pips_debug, and print_transformer.

Referenced by precondition_add_declaration_information(), and transformer_add_declaration_information().

Here is the call graph for this function:

Here is the caller graph for this function:

add_declaration_list_information()

void add_declaration_list_information	(	transformer	pre,
		list	dl,
		bool	precondition_p
	)

Parameters

pre	re
dl	l
precondition_p	recondition_p

Definition at line 179 of file dbm_interface.c.

{
  entity m = get_current_module_entity();
  code c = value_code(entity_initial(m));
  language l = code_language(c);
 
  FOREACH(ENTITY, v, dl) {
    type t = entity_type(v);
 
    if(type_variable_p(t)) {
      variable tv = type_variable(t);
 
      FOREACH(DIMENSION, d, variable_dimensions(tv)) {
        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(vl) &&
             value_mappings_compatible_vector_p(vu)) {
            Pvecteur cv = vect_substract(vl, vu);
 
            if(language_c_p(l))
              vect_add_elem(&cv, TCST, VALUE_MONE);
 
            if(!precondition_p) {
              upwards_vect_rename(cv, pre);
            }
 
            if(!vect_constant_p(cv) || vect_coeff(TCST, cv) > 0) {
              transformer_inequality_add(pre, cv);
            }
          }
        }
      }
 
    }
  }
}

References code_language, DIMENSION, dimension_lower, dimension_upper, ENTITY, entity_initial, entity_type, FOREACH, get_current_module_entity(), language_c_p, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, TCST, transformer_inequality_add(), type_variable, type_variable_p, upwards_vect_rename(), value_code, value_mappings_compatible_vector_p(), VALUE_MONE, variable_dimensions, vect_add_elem(), vect_coeff(), vect_constant_p(), and vect_substract().

Referenced by add_declaration_information().

Here is the call graph for this function:

Here is the caller graph for this function:

cumulated_effects_map_print()

void cumulated_effects_map_print

(

void

)

ca n'a rien a` faire ici, et en plus, il serait plus inte'ressant d'avoir une fonction void statement_map_print(statement_mapping htp)

hash_table_print_header (htp,f);

Definition at line 1549 of file dbm_interface.c.

{
    FILE * f =stderr;
    statement_effects htp = get_cumulated_rw_effects();
 
    /* hash_table_print_header (htp,f); */
 
    STATEMENT_EFFECTS_MAP(k, v, {
        fprintf(f, "\n\n%td", statement_ordering((statement) k));
        print_effects( effects_effects(v));
    },
      htp);
}

References effects_effects, f(), fprintf(), get_cumulated_rw_effects(), print_effects, STATEMENT_EFFECTS_MAP, and statement_ordering.

Here is the call graph for this function:

generic_module_name_to_transformers()

bool generic_module_name_to_transformers	(	const char *	module_name,
		bool	in_context
	)

bool generic_module_name_to_transformers(char * module_name, bool in_context): compute a transformer for each statement of a module with a given name; compute also the global transformer for the module

intraprocedural preconditions: proper declarations

This stack is useful to document warnings and to retrieve points-to information.

could be a gen_find_tabulated as well...

cumulated_effects_map_print();

compute the basis related to module m

In the main module, transformers can be computed in context of the initial values

Add declaration information: arrays cannot be empty (Fortran standard, Section 5.1.2)

Get the preconditions: they might prove useful within loops where transformers cannot propagate enough information.

compute intraprocedural transformer

FI: side effect; compute and store the summary transformer, because every needed piece of data is available...

filter out local variables from the global intraprocedural effect

Two auxiliary hash tables allocated by effectsmap_to_listmap()

Parameters

module_name	odule_name
in_context	n_context

Definition at line 918 of file dbm_interface.c.

{
    transformer t_intra = transformer_undefined;
    transformer t_inter = transformer_undefined;
    /* intraprocedural preconditions: proper declarations */
    transformer mod_pre = transformer_undefined;
    list e_inter;
 
    debug_on(SEMANTICS_DEBUG_LEVEL);
    sc_variable_name_push((char* (*)(Variable)) readable_value_name);
 
    /* This stack is useful to document warnings and to retrieve
       points-to information. */
    make_statement_global_stack();
    set_warning_counters();
    set_current_module_entity(module_name_to_entity(module_name));
    /* could be a gen_find_tabulated as well... */
    set_current_module_statement(
        (statement) db_get_memory_resource(DBR_CODE, module_name, true));
    if( get_current_module_statement() == (statement) database_undefined )
        pips_internal_error("no statement for module %s", module_name);
 
    set_proper_rw_effects((statement_effects)
        db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
 
    set_cumulated_rw_effects((statement_effects)
        db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
 
    set_methods_for_simple_effects();
 
    /* cumulated_effects_map_print();*/
 
    e_inter = effects_to_list( (effects)
        db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true));
 
    set_transformer_map( MAKE_STATEMENT_MAPPING() );
 
    /* compute the basis related to module m */
    module_to_value_mappings( get_current_module_entity() );
 
    /* In the main module, transformers can be computed in context of the
       initial values */
    if(entity_main_module_p(get_current_module_entity())
       && get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT"))
    {
      if (get_bool_property(SEMANTICS_INTERPROCEDURAL))
      {
        mod_pre = (transformer)
          db_get_memory_resource(DBR_PROGRAM_PRECONDITION, "", false);
        if(transformer_empty_p(mod_pre)) {
          pips_user_warning(
             "Initial preconditions are not consistent.\n"
             " The Fortran standard rules about variable initialization"
             " with DATA statements are likely to be violated.\n"
             "set property PARSER_ACCEPT_ANSI_EXTENSIONS to false\n"
             "and CHECK_FORTRAN_SYNTAX_BEFORE_PIPS to true.\n");
        }
      }
      else
        mod_pre = data_to_precondition(get_current_module_entity());
    }
    else if(in_context) {
      mod_pre =
        transformer_dup(load_summary_precondition(get_current_module_entity()));
    }
    else
      mod_pre = transformer_identity();
 
    /* Add declaration information: arrays cannot be empty (Fortran
       standard, Section 5.1.2) */
    if(get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
      transformer_add_declaration_information(mod_pre,
                                              get_current_module_entity());
    }
 
    /* Get the preconditions: they might prove useful within loops where
       transformers cannot propagate enough information. */
    if(in_context) {
     set_precondition_map( (statement_mapping)
        db_get_memory_resource(DBR_PRECONDITIONS, module_name, true));
   }
 
    /* compute intraprocedural transformer */
    statement ms = get_current_module_statement();
    t_intra = statement_to_transformer(ms, mod_pre);
    free_transformer(mod_pre);
 
    DB_PUT_MEMORY_RESOURCE(DBR_TRANSFORMERS, module_name,
                           (char*) get_transformer_map() );
 
    /* FI: side effect; compute and store the summary transformer, because
       every needed piece of data is available... */
 
    /* filter out local variables from the global intraprocedural effect */
    t_inter = transformer_intra_to_inter(t_intra, e_inter);
    t_inter = transformer_normalize(t_inter, 2);
    if(c_module_p(get_current_module_entity())) {
      t_inter = value_passing_summary_transformer(get_current_module_entity(), t_inter);
    }
    if(!transformer_consistency_p(t_inter)) {
        (void) print_transformer(t_inter);
        pips_internal_error("Non-consistent summary transformer");
    }
    DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TRANSFORMER,
                           module_local_name(get_current_module_entity()),
                           (char*) t_inter);
    pips_debug(8, "t_inter=%p\n", t_inter);
 
    reset_current_module_entity();
    reset_current_module_statement();
    /* Two auxiliary hash tables allocated by effectsmap_to_listmap() */
    reset_proper_rw_effects();
    reset_cumulated_rw_effects();
    generic_effects_reset_all_methods();
    reset_transformer_map();
    if(in_context) reset_precondition_map();
 
    free_value_mappings();
    free_statement_global_stack();
 
    sc_variable_name_pop();
    debug_off();
 
    return true;
}

References c_module_p(), data_to_precondition(), database_undefined, db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, effects_to_list(), entity_main_module_p(), free_statement_global_stack(), free_transformer(), free_value_mappings(), generic_effects_reset_all_methods(), get_bool_property(), get_current_module_entity(), get_current_module_statement(), get_transformer_map(), load_summary_precondition(), make_statement_global_stack(), MAKE_STATEMENT_MAPPING, module_local_name(), module_name(), module_name_to_entity(), module_to_value_mappings(), pips_debug, pips_internal_error, pips_user_warning, print_transformer, readable_value_name(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_precondition_map(), reset_proper_rw_effects(), reset_transformer_map(), sc_variable_name_pop(), sc_variable_name_push(), SEMANTICS_DEBUG_LEVEL, SEMANTICS_INTERPROCEDURAL, set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_methods_for_simple_effects(), set_precondition_map(), set_proper_rw_effects(), set_transformer_map(), set_warning_counters(), statement_to_transformer(), transformer_add_declaration_information(), transformer_consistency_p(), transformer_dup(), transformer_empty_p(), transformer_identity(), transformer_intra_to_inter(), transformer_normalize(), transformer_undefined, and value_passing_summary_transformer().

Referenced by module_name_to_transformers(), and module_name_to_transformers_in_context().

Here is the call graph for this function:

Here is the caller graph for this function:

interprocedural_summary_precondition()

bool interprocedural_summary_precondition

(

char *

module_name

)

The DATA statement from all modules, called or not called, are used, as well as the preconditions at all call sites.

Parameters

module_name

odule_name

Definition at line 545 of file dbm_interface.c.

{
  /* The DATA statement from all modules, called or not called, are used,
     as well as the preconditions at all call sites. */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  return summary_precondition(module_name);
}

References module_name(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), and summary_precondition().

Here is the call graph for this function:

interprocedural_summary_precondition_with_points_to()

bool interprocedural_summary_precondition_with_points_to

(

char *

module_name

)

The DATA statement from all modules, called or not called, are used, as well as the preconditions at all call sites. Points_to information is required to perform a more accurate translation between callesr and callees.

Parameters

module_name

odule_name

Definition at line 571 of file dbm_interface.c.

{
  /* The DATA statement from all modules, called or not called, are
   * used, as well as the preconditions at all call sites. Points_to
   * information is required to perform a more accurate translation
   * between callesr and callees.
   */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_use_points_to();
  bool result_p = summary_precondition(module_name);
  reset_use_points_to();
  return result_p;
}

References module_name(), reset_use_points_to(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), set_use_points_to(), and summary_precondition().

Here is the call graph for this function:

intraprocedural_summary_precondition()

bool intraprocedural_summary_precondition

(

char *

module_name

)

The current module is sufficient to derive it.

Parameters

module_name

odule_name

Definition at line 538 of file dbm_interface.c.

{
  /* The current module is sufficient to derive it. */
  set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
  return summary_precondition(module_name);
}

References module_name(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), and summary_precondition().

Here is the call graph for this function:

load_body_effects()

list load_body_effects

(

entity

e

)

Definition at line 1508 of file dbm_interface.c.

{
  string module_name = (string) module_local_name(e);
 
    pips_assert("load_summary_effects", entity_module_p(e));
 
    statement b = (statement) db_get_memory_resource(DBR_CODE, module_name, true);
    statement_effects se = (statement_effects)
      db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true);
    effects be = (effects) (intptr_t)HASH_GET(p, p, statement_effects_hash_table(se), (void *) b);
    list bel = effects_effects(be);
 
    pips_assert("bel is defined", bel != list_undefined);
 
    return bel;
}

References db_get_memory_resource(), effects_effects, entity_module_p(), HASH_GET, intptr_t, list_undefined, module_local_name(), module_name(), pips_assert, and statement_effects_hash_table.

Referenced by user_call_to_points_to_interprocedural().

Here is the call graph for this function:

Here is the caller graph for this function:

load_completed_statement_transformer()

transformer load_completed_statement_transformer

(

statement

s

)

three mappings used throughout semantics analysis:

• transformer_map is computed in a first phase
• precondition_map is computed in a second phase
• cumulated_effects is used and assumed computed before (defined in effects.c)
• proper_effects might be useless... only DO loop analysis could use it (idem) declaration of the previously described mappings with their access functions :

(DEFINE_CURRENT_MAPPING is a macro defined in ~pips/Newgen/mapping.h)

BA, August 26, 1993 Returns the entry to exit transformer associated to a statement, since all statements in PIPS internal representation have a unique exit.

The transformers associated to loops are the transformers linking the loop precondition to the loop body precondition. When dealing with sequences or test or... the transformer linking the loop precondition to its postcondition, i.e. the precondition hodling at the loop exit, is needed.

To complete the statement transformer, a precondition is required. Different preconditions can be used:

• transformer_identity(): provides no information
• load_statement_precondition(): provides as much information as possible
• the transformer domain: provides information available when the transformers are computed, i.e. preconditions do not have to be available; this is unsafe as the loop entrance transition domain may be a subset of the precocndition, unless the loop is always entered.

Unlike load_statement_transformer(), this function allocates a new transformer. See comments associated to:

generic_complete_statement_transformer()

Definition at line 131 of file dbm_interface.c.

{
  transformer t = load_statement_transformer(s);
 
  // Unsafe if s is a loop, unless you check that the loop is always
  //entered
  //transformer pre = transformer_to_domain(t);
  transformer pre = transformer_identity();
 
  transformer te = complete_statement_transformer(t, pre, s);
 
  //pips_assert("te is defined", !transformer_undefined_p(te));
 
  free_transformer(pre);
 
  return te;
}

References complete_statement_transformer(), free_transformer(), load_statement_transformer(), and transformer_identity().

Referenced by set_methods_for_convex_effects(), and set_methods_for_convex_rw_pointer_effects().

Here is the call graph for this function:

Here is the caller graph for this function:

load_module_intraprocedural_effects()

list load_module_intraprocedural_effects

(

entity

e

)

memoization could be used to improve efficiency

Definition at line 1526 of file dbm_interface.c.

{
    /* memoization could be used to improve efficiency */
    list t;
    statement s;
 
    pips_assert("is a module", entity_module_p(e));
    pips_assert("is the current module", e == get_current_module_entity());
    s = get_current_module_statement();
    pips_assert("some statement", s!=statement_undefined);
 
    t = load_cumulated_rw_effects_list(s);
 
    pips_assert("some list", t != list_undefined);
 
    return t;
}

References entity_module_p(), get_current_module_entity(), get_current_module_statement(), list_undefined, load_cumulated_rw_effects_list(), pips_assert, and statement_undefined.

Referenced by allocate_module_value_mappings(), data_to_precondition(), and module_to_value_mappings().

Here is the call graph for this function:

Here is the caller graph for this function:

load_summary_effects()

list load_summary_effects

(

entity

e

)

FI->FI, FI->BC: these two functions should be moved into effects-util or effects-simple.

memorization could be used to improve efficiency

Definition at line 1492 of file dbm_interface.c.

{
    /* memorization could be used to improve efficiency */
    list t;
 
    pips_assert("load_summary_effects", entity_module_p(e));
 
    t = effects_to_list( (effects)
        db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_local_name(e),
                               true));
 
    pips_assert("t is defined", t != list_undefined);
 
    return t;
}

References db_get_memory_resource(), effects_to_list(), entity_module_p(), list_undefined, module_local_name(), and pips_assert.

Referenced by add_module_call_site_precondition(), call_site_to_module_precondition_text(), compute_summary_reductions(), module_to_value_mappings(), pure_function_p(), update_precondition_with_call_site_preconditions(), and user_call_to_points_to_fast_interprocedural().

Here is the call graph for this function:

Here is the caller graph for this function:

load_summary_precondition()

transformer load_summary_precondition

(

entity

e

)

summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure that used/produced it

memoization could be used to improve efficiency

Not done earlier, because the value mappings were not available. On the other hand, htis assumes that the value mappings have been initialized before a call to load_summary_precondition(0 is performed.

Definition at line 1431 of file dbm_interface.c.

{
  /* memoization could be used to improve efficiency */
  transformer t;
 
  pips_assert("e is a module", entity_module_p(e));
 
  pips_debug(8, "begin\n for %s\n",
             module_local_name(e));
 
  t = (transformer)
    db_get_memory_resource(DBR_SUMMARY_PRECONDITION, module_local_name(e),
                           true);
  /* Not done earlier, because the value mappings were not available. On
     the other hand, htis assumes that the value mappings have been
     initialized before a call to load_summary_precondition(0 is
     performed.*/
  translate_global_values(e, t);
 
  pips_assert("the summary precondition t is defined", t != transformer_undefined);
 
  ifdebug(8) {
    pips_debug(8, " precondition for %s:\n",
               module_local_name(e));
    dump_transformer(t);
    pips_debug(8, " end\n");
  }
 
  return t;
}

References db_get_memory_resource(), dump_transformer, entity_module_p(), ifdebug, module_local_name(), pips_assert, pips_debug, transformer_undefined, and translate_global_values().

Referenced by generic_module_name_to_transformers(), and module_name_to_preconditions().

Here is the call graph for this function:

Here is the caller graph for this function:

load_summary_total_postcondition()

transformer load_summary_total_postcondition

(

entity

e

)

summary_preconditions are expressed in any possible frame, in fact the frame of the last procedure that used/produced it

Definition at line 1465 of file dbm_interface.c.

{
    transformer t_post = transformer_undefined;;
 
    pips_assert("e is a module", entity_module_p(e));
 
    pips_debug(8, "begin\n for %s\n",
          module_local_name(e));
 
    t_post = (transformer)
        db_get_memory_resource(DBR_SUMMARY_TOTAL_POSTCONDITION, module_local_name(e),
                               true);
 
    pips_assert("t is defined", t_post != transformer_undefined);
 
    ifdebug(8) {
        pips_debug(8, " total postcondition for %s:\n",
              module_local_name(e));
        dump_transformer(t_post);
        pips_debug(8, " end\n");
    }
 
    return t_post;
}

References db_get_memory_resource(), dump_transformer, entity_module_p(), ifdebug, module_local_name(), pips_assert, pips_debug, and transformer_undefined.

Referenced by module_name_to_total_preconditions().

Here is the call graph for this function:

Here is the caller graph for this function:

load_summary_transformer()

transformer load_summary_transformer

(

entity

e

)

FI: I had to add a guard db_resource_p() on Nov. 14, 1995. I do not understand why the problem never occured before, although it should each time the intra-procedural option is selected.

This may partially be explained because summary transformers are implicitly computed with transformers instead of using an explicit call to summary_transformer (I guess I'm going to change that).

I think it would be better not to call load_summary_transformer() at all when no interprocedural options are selected. I should change that too.

memoization could be used to improve efficiency

db_get_memory_resource never returns database_undefined or resource_undefined

Let's be careful with people using an intraprocedural analysis of the transformers and requesting an interprocedural analysis of the preconditions...

Definition at line 1327 of file dbm_interface.c.

{
    /* FI: I had to add a guard db_resource_p() on Nov. 14, 1995.
     * I do not understand why the problem never occured before,
     * although it should each time the intra-procedural option
     * is selected.
     *
     * This may partially be explained because summary transformers
     * are implicitly computed with transformers instead of using
     * an explicit call to summary_transformer (I guess I'm going
     * to change that).
     *
     * I think it would be better not to call load_summary_transformer()
     * at all when no interprocedural options are selected. I should
     * change that too.
     */
 
    /* memoization could be used to improve efficiency */
    transformer t = transformer_undefined;
 
    pips_assert("e is a module", entity_module_p(e));
 
    if(db_resource_p(DBR_SUMMARY_TRANSFORMER, module_local_name(e))) {
        t = (transformer)
            db_get_memory_resource(DBR_SUMMARY_TRANSFORMER,
                                   entity_local_name(e),
                                   true);
 
        /* db_get_memory_resource never returns database_undefined or
           resource_undefined */
        pips_assert("load_summary_transformer", t != transformer_undefined);
    }
    else {
        t = transformer_undefined;
    }
 
    /* Let's be careful with people using an intraprocedural analysis
       of the transformers and requesting an interprocedural analysis
       of the preconditions... */
    if(transformer_undefined_p(t)) {
      if(db_resource_p(DBR_SUMMARY_EFFECTS, module_local_name(e))) {
        list el = effects_effects((effects)
                                  db_get_memory_resource(DBR_SUMMARY_EFFECTS,
                                                         entity_local_name(e),
                                                         true));
        t = effects_to_transformer(el);
      }
    }
 
    return t;
}

References db_get_memory_resource(), db_resource_p(), effects_effects, effects_to_transformer(), entity_local_name(), entity_module_p(), module_local_name(), pips_assert, transformer_undefined, and transformer_undefined_p.

Referenced by c_user_call_to_transformer(), and fortran_user_call_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

main_summary_precondition()

static transformer main_summary_precondition ( entity  callee )

static

Special case: main module.

Intraprocedural case: use the local DATA statement to define the initial store.

Interprocedural case: use the program precondition

Do we need to initialize the mappings before calling this subroutine?

Why not use a DB_GET of DBR_INITIAL_PRECONDITION?

t = data_to_precondition(callee);

Definition at line 593 of file dbm_interface.c.

{
  transformer t = transformer_undefined;
 
  if (get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    t = copy_transformer((transformer)
      db_get_memory_resource(DBR_PROGRAM_PRECONDITION, "", false));
    if(transformer_empty_p(t)) {
      pips_user_warning(
                        "Initial preconditions are not consistent.\n"
                        " The Fortran standard rules about variable initialization"
                        " with DATA statements are likely to be violated.\n"
                        "set property PARSER_ACCEPT_ANSI_EXTENSIONS to false\n"
                        "and CHECK_FORTRAN_SYNTAX_BEFORE_PIPS to true.\n");
    }
  }
  else {
    /* Do we need to initialize the mappings before calling this subroutine? */
    /* Why not use a DB_GET of DBR_INITIAL_PRECONDITION? */
    /* t = data_to_precondition(callee); */
    t = copy_transformer
      ((transformer) db_get_memory_resource(DBR_INITIAL_PRECONDITION,
                                            module_local_name(callee),
                                            false));
  }
 
  return t;
}

References callee, copy_transformer(), db_get_memory_resource(), get_bool_property(), module_local_name(), pips_user_warning, SEMANTICS_INTERPROCEDURAL, transformer_empty_p(), and transformer_undefined.

Referenced by summary_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

module_name_to_preconditions()

bool module_name_to_preconditions

(

const char *

module_name

)

resource module_name_to_preconditions(char * module_name): compute a transformer for each statement of a module with a given name; compute also the global transformer for the module

set_debug_level(get_int_property(SEMANTICS_DEBUG_LEVEL));

To provide information for warnings

could be a gen_find_tabulated as well...

Used to add reference information when it is trusted... which should always be, at least for automatic parallelization.

cumulated effects are used to compute the value mappings

p_inter is not used!!! FI, 9 February 1994

debug_on(SEMANTICS_DEBUG_LEVEL);

compute the mappings related to module m, that is likely to be unavailable during interprocedural analysis; a module reference should be kept with the mappings to avoid useless recomputation, allocation and frees, including those due to the prettyprinter

set the list of global values. This is a bit too restrictive in C as the formal arguments, even modified in the procedure body, will not appear in the transformer_arguments. Should we add missing formal arguments to this list? See for instance "character01.c".

debug_on(SEMANTICS_DEBUG_LEVEL);

Add declaration information: arrays cannot be empty (Fortran standard, Section 5.1.2). But according to summary_precondition(), this is now supposed to be performed by the transformer phase?

If the module is never called, its precondition is identity and by default no values are listed in its basis. Function add_type_information() has no effect.

if(transformer_identity_p(pre)) {

list el = effects_to_list(

(effects) db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true));

free_transformer(pre);

// FI: memory leak

pre = transformer_range(effects_to_transformer(el));

}

debug_on(SEMANTICS_DEBUG_LEVEL);

propagate the module precondition

post could be stored in the ri for later interprocedural uses but the ri cannot be modified so early before the DRET demo; also our current interprocedural algorithm does not propagate postconditions upwards in the call tree

Parameters

module_name

odule_name

Definition at line 1073 of file dbm_interface.c.

{
    transformer t_inter;
    transformer pre;
    transformer post;
 
    /* set_debug_level(get_int_property(SEMANTICS_DEBUG_LEVEL)); */
    debug_on(SEMANTICS_DEBUG_LEVEL);
    /* To provide information for warnings */
    make_statement_global_stack();
    sc_variable_name_push((char* (*)(Variable)) readable_value_name);
 
    set_current_module_entity(module_name_to_entity(module_name) );
    /* could be a gen_find_tabulated as well... */
    set_current_module_statement(
        (statement) db_get_memory_resource(DBR_CODE, module_name, true));
    if(get_current_module_statement() == (statement) database_undefined)
        pips_internal_error("no statement for module %s", module_name);
 
    /* Used to add reference information when it is trusted... which
       should always be, at least for automatic parallelization. */
    set_proper_rw_effects((statement_effects)
        db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
 
    /* cumulated effects are used to compute the value mappings */
    set_cumulated_rw_effects((statement_effects)
        db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
 
    set_methods_for_simple_effects();
 
    set_transformer_map( (statement_mapping)
        db_get_memory_resource(DBR_TRANSFORMERS, module_name, true));
 
 
    /* p_inter is not used!!! FI, 9 February 1994 */
    /*
    if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
        p_inter = (transformer)
            db_get_memory_resource(DBR_SUMMARY_PRECONDITION,
                                   module_name, true);
    }
    */
 
    t_inter = (transformer)
        db_get_memory_resource(DBR_SUMMARY_TRANSFORMER, module_name, true);
 
    /* debug_on(SEMANTICS_DEBUG_LEVEL); */
 
    set_precondition_map( MAKE_STATEMENT_MAPPING() );
 
    /* compute the mappings related to module m, that is likely to be
       unavailable during interprocedural analysis; a module reference
       should be kept with the mappings to avoid useless recomputation,
       allocation and frees, including those due to the prettyprinter */
 
    module_to_value_mappings( get_current_module_entity() );
 
    /* set the list of global values. This is a bit too restrictive in
       C as the formal arguments, even modified in the procedure body,
       will not appear in the transformer_arguments. Should we add
       missing formal arguments to this list? See for instance
       "character01.c". */
    set_module_global_arguments(transformer_arguments(t_inter));
 
    /* debug_on(SEMANTICS_DEBUG_LEVEL); */
 
    pre = copy_transformer(load_summary_precondition(get_current_module_entity()));
 
    /* Add declaration information: arrays cannot be empty (Fortran
       standard, Section 5.1.2). But according to summary_precondition(),
       this is now supposed to be performed by the transformer phase? */
    if(get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
        precondition_add_declaration_information(pre, get_current_module_entity());
    }
    if(get_bool_property("SEMANTICS_USE_TYPE_INFORMATION")
       || get_bool_property("SEMANTICS_USE_TYPE_INFORMATION_IN_PRECONDITIONS")) {
 
      /* If the module is never called, its precondition is identity
         and by default no values are listed in its basis. Function
         add_type_information() has no effect. */
 
      /* if(transformer_identity_p(pre)) { */
      /*        list el = effects_to_list( */
      /*                               (effects) db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true)); */
      /*        free_transformer(pre); */
      /*        // FI: memory leak  */
      /*        pre = transformer_range(effects_to_transformer(el)); */
      /* } */
 
      transformer_add_type_information(pre);
    }
 
    /* debug_on(SEMANTICS_DEBUG_LEVEL); */
 
    /* propagate the module precondition */
    init_reachable(get_current_module_statement());
    post = statement_to_postcondition(pre, get_current_module_statement() );
    close_reachable();
 
    /* post could be stored in the ri for later interprocedural uses
       but the ri cannot be modified so early before the DRET demo;
       also our current interprocedural algorithm does not propagate
       postconditions upwards in the call tree */
 
    DB_PUT_MEMORY_RESOURCE(DBR_PRECONDITIONS,
                           module_name,
                           (char*) get_precondition_map() );
 
    pips_debug(8, "postcondition computed for %s\n",
          entity_local_name( get_current_module_entity() ));
    ifdebug(8) (void) print_transformer(post);
    debug(1, "module_name_to_preconditions", "end\n");
 
    reset_current_module_entity();
    reset_current_module_statement();
    reset_transformer_map();
    reset_precondition_map();
    reset_proper_rw_effects();
    reset_cumulated_rw_effects();
    generic_effects_reset_all_methods();
 
    free_value_mappings();
 
    sc_variable_name_pop();
    free_statement_global_stack();
    debug_off();
 
    return true;
}

References close_reachable(), copy_transformer(), database_undefined, db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug(), debug_off, debug_on, entity_local_name(), free_statement_global_stack(), free_value_mappings(), generic_effects_reset_all_methods(), get_bool_property(), get_current_module_entity(), get_current_module_statement(), get_precondition_map(), ifdebug, init_reachable(), load_summary_precondition(), make_statement_global_stack(), MAKE_STATEMENT_MAPPING, module_name(), module_name_to_entity(), module_to_value_mappings(), pips_debug, pips_internal_error, precondition_add_declaration_information(), print_transformer, readable_value_name(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_precondition_map(), reset_proper_rw_effects(), reset_transformer_map(), sc_variable_name_pop(), sc_variable_name_push(), SEMANTICS_DEBUG_LEVEL, set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_methods_for_simple_effects(), set_module_global_arguments(), set_precondition_map(), set_proper_rw_effects(), set_transformer_map(), statement_to_postcondition(), transformer_add_type_information(), and transformer_arguments.

Referenced by preconditions_inter_fast(), preconditions_inter_full(), preconditions_inter_full_with_points_to(), preconditions_intra(), and preconditions_intra_fast().

Here is the call graph for this function:

Here is the caller graph for this function:

module_name_to_total_preconditions()

bool module_name_to_total_preconditions

(

const char *

module_name

)

set the list of global values

The program postcondition should be used DBR_PROGRAM_POSTCONDITION

that might be because we are at the call tree root or because no information is available; maybe, every module precondition should be initialized to a neutral value?

intra-procedural case, not a main module

propagate the module total postcondition

filter out local variables from the global intraprocedural effect

Parameters

module_name

odule_name

Definition at line 1203 of file dbm_interface.c.

{
  transformer t_inter = transformer_undefined;
  transformer t_pre = transformer_undefined;
  transformer t_pre_inter = transformer_undefined;
  transformer t_post = transformer_undefined;
  list e_inter = list_undefined;
 
  debug_on(SEMANTICS_DEBUG_LEVEL);
  sc_variable_name_push((char* (*)(Variable)) readable_value_name);
 
  set_current_module_entity(module_name_to_entity(module_name) );
  set_current_module_statement(
                               (statement) db_get_memory_resource(DBR_CODE, module_name, true));
  if(get_current_module_statement() == (statement) database_undefined)
    pips_internal_error("no statement for module %s", module_name);
 
  set_proper_rw_effects((statement_effects)
                        db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
 
  set_cumulated_rw_effects((statement_effects)
                           db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
 
  e_inter = effects_to_list((effects)
                            db_get_memory_resource(DBR_SUMMARY_EFFECTS, module_name, true));
 
  set_transformer_map( (statement_mapping)
                       db_get_memory_resource(DBR_TRANSFORMERS, module_name, true));
 
  set_precondition_map( (statement_mapping)
                       db_get_memory_resource(DBR_PRECONDITIONS, module_name, true));
 
 
  t_inter = (transformer)
    db_get_memory_resource(DBR_SUMMARY_TRANSFORMER, module_name, true);
 
  set_total_precondition_map( MAKE_STATEMENT_MAPPING() );
 
  module_to_value_mappings( get_current_module_entity() );
 
  /* set the list of global values */
  set_module_global_arguments(transformer_arguments(t_inter));
 
  if(entity_main_module_p(get_current_module_entity())) {
    /* The program postcondition should be used DBR_PROGRAM_POSTCONDITION */
    t_post = transformer_identity();
  }
 
  ifdebug(3) {
    pips_debug(1, "considering final total postcondition for %s\n", module_name);
    print_transformer(t_post);
  }
 
  if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    transformer ip =
      load_summary_total_postcondition(get_current_module_entity());
    if( ip == transformer_undefined) {
      /* that might be because we are at the call tree root
         or because no information is available;
         maybe, every module precondition should be initialized
         to a neutral value? */
      pips_user_warning("no interprocedural module total postcondition for %s\n",
                        entity_local_name(get_current_module_entity() ));
      ;
    }
    else {
      translate_global_values(get_current_module_entity(), ip);
      ifdebug(8) {
        pips_debug(8, "\t summary_total_postcondition %p after translation:\n",
                   ip);
        print_transformer(ip);
        pips_assert("The summary total postcondition is consistent",
                    transformer_consistency_p(ip));
      }
      t_post = transformer_combine(transformer_dup(ip), t_post);
    }
  }
  else if(transformer_undefined_p(t_post)) {
    /* intra-procedural case, not a main module */
    t_post = transformer_identity();
  }
 
  /* propagate the module total postcondition */
  init_reachable(get_current_module_statement());
  t_pre = statement_to_total_precondition(t_post, get_current_module_statement() );
  close_reachable();
 
  DB_PUT_MEMORY_RESOURCE(DBR_TOTAL_PRECONDITIONS,
                         module_name,
                         (char*) get_total_precondition_map() );
 
  /* filter out local variables from the global intraprocedural effect */
  t_pre_inter = transformer_intra_to_inter(t_pre, e_inter);
  t_pre_inter = transformer_normalize(t_pre_inter, 2);
  if(!transformer_consistency_p(t_pre_inter)) {
    (void) print_transformer(t_pre_inter);
    pips_internal_error("Non-consistent summary transformer");
  }
  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TOTAL_PRECONDITION,
                         module_local_name(get_current_module_entity()),
                         (char*) t_pre_inter);
 
  pips_debug(8, "total precondition computed for %s\n",
             entity_local_name( get_current_module_entity() ));
  ifdebug(8) (void) print_transformer(t_pre);
  pips_debug(1, "end\n");
 
  reset_current_module_entity();
  reset_current_module_statement();
  reset_transformer_map();
  reset_precondition_map();
  reset_total_precondition_map();
  reset_proper_rw_effects();
  reset_cumulated_rw_effects();
 
  free_value_mappings();
 
  sc_variable_name_pop();
  debug_off();
 
  return true;
}

References close_reachable(), database_undefined, db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, effects_to_list(), entity_local_name(), entity_main_module_p(), free_value_mappings(), get_bool_property(), get_current_module_entity(), get_current_module_statement(), get_total_precondition_map(), ifdebug, init_reachable(), list_undefined, load_summary_total_postcondition(), MAKE_STATEMENT_MAPPING, module_local_name(), module_name(), module_name_to_entity(), module_to_value_mappings(), pips_assert, pips_debug, pips_internal_error, pips_user_warning, print_transformer, readable_value_name(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_precondition_map(), reset_proper_rw_effects(), reset_total_precondition_map(), reset_transformer_map(), sc_variable_name_pop(), sc_variable_name_push(), SEMANTICS_DEBUG_LEVEL, SEMANTICS_INTERPROCEDURAL, set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_module_global_arguments(), set_precondition_map(), set_proper_rw_effects(), set_total_precondition_map(), set_transformer_map(), statement_to_total_precondition(), transformer_arguments, transformer_combine(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_intra_to_inter(), transformer_normalize(), transformer_undefined, transformer_undefined_p, and translate_global_values().

Referenced by total_preconditions_inter(), and total_preconditions_intra().

Here is the call graph for this function:

Here is the caller graph for this function:

module_name_to_transformers()

bool module_name_to_transformers

(

const char *

module_name

)

Parameters

module_name

odule_name

Definition at line 1062 of file dbm_interface.c.

{
  bool rc = false;
  rc = generic_module_name_to_transformers(module_name, false);
  return rc;
}

References generic_module_name_to_transformers(), and module_name().

Referenced by transformers_inter_fast(), transformers_inter_full(), transformers_inter_full_with_points_to(), transformers_intra_fast(), and transformers_intra_full().

Here is the call graph for this function:

Here is the caller graph for this function:

module_name_to_transformers_in_context()

bool module_name_to_transformers_in_context

(

const char *

module_name

)

Parameters

module_name

odule_name

Definition at line 1044 of file dbm_interface.c.

{
  bool rc = false;
  bool save_prop = get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT");
 
  if(!save_prop) {
    pips_user_warning("Although property SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT"
                      " is not set, it is used because it is necessary for this "
                      "recomputation to be useful\n");
    set_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT", true);
  }
 
  rc = generic_module_name_to_transformers(module_name, true);
 
  set_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT", save_prop);
  return rc;
}

References generic_module_name_to_transformers(), get_bool_property(), module_name(), pips_user_warning, and set_bool_property().

Referenced by refine_transformers(), and refine_transformers_with_points_to().

Here is the call graph for this function:

Here is the caller graph for this function:

old_summary_precondition()

bool old_summary_precondition

(

char *

module_name

)

do not nothing because it has been computed by side effects; or provide an empty precondition for root modules; maybe a touch to look nicer?

touch it

Parameters

module_name

odule_name

Definition at line 500 of file dbm_interface.c.

{
  /* do not nothing because it has been computed by side effects;
   * or provide an empty precondition for root modules;
   * maybe a touch to look nicer?
   */
 
  transformer t;
 
  debug_on(SEMANTICS_DEBUG_LEVEL);
 
  debug(8, "summary_precondition", "begin\n");
 
  if(db_resource_p(DBR_SUMMARY_PRECONDITION, module_name)) {
    /* touch it */
    t = (transformer) db_get_memory_resource(DBR_SUMMARY_PRECONDITION,
                                             module_name,
                                             true);
  }
  else {
    t = transformer_identity();
  }
 
  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
                         module_name, (char * )t);
 
  ifdebug(8) {
    pips_debug(8, "initial summary precondition %p for %s:\n",
               t, module_name);
    dump_transformer(t);
    pips_debug(8, "end\n");
  }
 
  debug_off();
 
  return true;
}

References db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, db_resource_p(), debug(), debug_off, debug_on, dump_transformer, ifdebug, module_name(), pips_debug, SEMANTICS_DEBUG_LEVEL, and transformer_identity().

Here is the call graph for this function:

ordinary_summary_precondition()

static transformer ordinary_summary_precondition ( const char *  module_name, entity  callee  )

static

Standard cases: called modules.

If a main is present, modules which are never called receive an unfeasible summary_precondition.

If no main is present in the current workspace, modules which are never called receive an identity summary precondition, i.e. no information.

If an interprocedural analysis is required, the preconditions of all call sites are translated and then unioned.

Look for all call sites in the callers

no callers => empty precondition if a main is being analyzed FC. 08/01/1999.

No main in the application? Do declare every module executed.

Try to eliminate (some) redundancy at a reasonnable cost.

What is a reasonnable cost?

Level 7 core dumps with Semantics-New/summary_precondition04.c unless formal parameter "_c" is renamed... external_value_name is called when the value mapping hash-tables are not available. Validations of Semantics and Semantics-new are not improved by level 7 wrt level 2.

t = transformer_normalize(t, 7);

Corinne's best one... for YPENT2 in ARC2D, but be ready to pay the price! And in case an overflow occurs, you may loose a lot of accuracy without any control.

t = transformer_normalize(t, 8);

No consistency check possible here because value_mappings are not available

pips_assert("The summary precondition is consistent", transformer_consistency_p(t));

Intraprocedural case

Definition at line 636 of file dbm_interface.c.

{
  transformer t = transformer_undefined;
 
  if(get_bool_property(SEMANTICS_INTERPROCEDURAL)) {
    /* Look for all call sites in the callers
     */
    callees callers = (callees) db_get_memory_resource(DBR_CALLERS,
                                                       module_name,
                                                       true);
    list lc = callees_callees(callers);
 
    ifdebug(1) {
      pips_debug(1, "begin for %s with %zd callers\n",
                 module_name,
                 gen_length(lc));
      FOREACH(STRING, caller_name, lc) {
        (void) fprintf(stderr, "%s, ", caller_name);
      }
      (void) fprintf(stderr, "\n");
    }
 
    reset_call_site_number();
    // FI: it might be safer to make and free this stack in the loop
    // body, once for each caller. The initialization is located in
    // summary_preconditions()
 
    // make_statement_global_stack();
 
    FOREACH(STRING, caller_name, callees_callees(callers)) {
      entity caller = module_name_to_entity(caller_name);
      t = update_precondition_with_call_site_preconditions(t, caller, callee);
    }
 
    // free_statement_global_stack();
 
    if (ENDP(callees_callees(callers)) &&
        some_main_entity_p()) {
      /* no callers => empty precondition if a main is being analyzed
         FC. 08/01/1999.
      */
      pips_user_warning("empty precondition to %s "
                        "because not in call tree from main.\n", module_name);
      t = transformer_empty();
    }
    else if (transformer_undefined_p(t)) {
      /* No main in the application? Do declare every module executed. */
      t = transformer_identity();
    }
    else {
      /* Try to eliminate (some) redundancy at a reasonnable cost. */
      /* What is a reasonnable cost? */
 
      t = transformer_normalize(t, 2);
      /* Level 7 core dumps with
       * Semantics-New/summary_precondition04.c unless formal
       * parameter "_c" is renamed... external_value_name is called
       * when the value mapping hash-tables are not
       * available. Validations of Semantics and Semantics-new are not
       * improved by level 7 wrt level 2.
       */
      /* t = transformer_normalize(t, 7); */
 
      /* Corinne's best one... for YPENT2 in ARC2D, but be ready to pay
         the price! And in case an overflow occurs, you may loose a lot of
         accuracy without any control. */
      /* t = transformer_normalize(t, 8); */
 
      /* No consistency check possible here because value_mappings are
         not available */
      /* pips_assert("The summary precondition is consistent",
         transformer_consistency_p(t));*/
    }
  }
  else {
    /* Intraprocedural case */
    t = transformer_identity();
  }
 
  return t;
}

References callee, callees_callees, caller_name, db_get_memory_resource(), ENDP, FOREACH, fprintf(), gen_length(), get_bool_property(), ifdebug, module_name(), module_name_to_entity(), pips_debug, pips_user_warning, reset_call_site_number(), SEMANTICS_INTERPROCEDURAL, some_main_entity_p(), STRING, transformer_empty(), transformer_identity(), transformer_normalize(), transformer_undefined, transformer_undefined_p, and update_precondition_with_call_site_preconditions().

Referenced by summary_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

precondition_add_declaration_information()

static void precondition_add_declaration_information ( transformer  pre, entity  m  )

static

Definition at line 247 of file dbm_interface.c.

{
  add_declaration_information(pre, m, true);
}

References add_declaration_information().

Referenced by module_name_to_preconditions().

Here is the call graph for this function:

Here is the caller graph for this function:

preconditions_inter_fast()

bool preconditions_inter_fast

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 435 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, false);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

References module_name(), module_name_to_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

preconditions_inter_full()

bool preconditions_inter_full

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 447 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

References module_name(), module_name_to_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

preconditions_inter_full_with_points_to()

bool preconditions_inter_full_with_points_to

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 459 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    set_pt_to_list( (statement_points_to)
                    db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
    bool result_p = module_name_to_preconditions(module_name);
    reset_pt_to_list();
    return result_p;
}

References db_get_memory_resource(), module_name(), module_name_to_preconditions(), reset_pt_to_list(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, set_bool_property(), and set_pt_to_list().

Here is the call graph for this function:

preconditions_intra()

bool preconditions_intra

(

char *

module_name

)

nothing to do: transformers are preconditions for this intraprocedural option

Maybe we should have an intra fast and an intra full as with other semantics entries

set_bool_property(SEMANTICS_FIX_POINT, false);

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 399 of file dbm_interface.c.

{
    /* nothing to do: transformers are preconditions for this
       intraprocedural option */
 
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    /* Maybe we should have an intra fast and an intra full as with other
       semantics entries */
    /* set_bool_property(SEMANTICS_FIX_POINT, false); */
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

References module_name(), module_name_to_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

preconditions_intra_fast()

bool preconditions_intra_fast

(

char *

module_name

)

nothing to do: transformers are preconditions for this intraprocedural option

Maybe we should have an intra fast and an intra full as with other semantics entries

set_bool_property(SEMANTICS_FIX_POINT, false);

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 417 of file dbm_interface.c.

{
    /* nothing to do: transformers are preconditions for this
       intraprocedural option */
 
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    /* Maybe we should have an intra fast and an intra full as with other
       semantics entries */
    /* set_bool_property(SEMANTICS_FIX_POINT, false); */
    set_bool_property(SEMANTICS_FIX_POINT, false);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_preconditions(module_name);
}

References module_name(), module_name_to_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

refine_transformers()

bool refine_transformers

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 354 of file dbm_interface.c.

{
  bool res;
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  set_bool_property(SEMANTICS_FIX_POINT, true);
  select_fix_point_operator();
  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
  refine_transformers_p = true;
  res = module_name_to_transformers_in_context(module_name);
  refine_transformers_p = false;
  return res;
}

References module_name(), module_name_to_transformers_in_context(), refine_transformers_p, select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

refine_transformers_with_points_to()

bool refine_transformers_with_points_to

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 369 of file dbm_interface.c.

{
  bool res;
  set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  set_bool_property(SEMANTICS_FIX_POINT, true);
  select_fix_point_operator();
  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
  set_pt_to_list( (statement_points_to)
                  db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
  refine_transformers_p = true;
  res = module_name_to_transformers_in_context(module_name);
  refine_transformers_p = false;
  reset_pt_to_list();
  return res;
}

References db_get_memory_resource(), module_name(), module_name_to_transformers_in_context(), refine_transformers_p, reset_pt_to_list(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, set_bool_property(), and set_pt_to_list().

Here is the call graph for this function:

reset_use_points_to()

static void reset_use_points_to ( )

static

Definition at line 560 of file dbm_interface.c.

{
  use_points_to_information_p = false;
}

References use_points_to_information_p.

Referenced by interprocedural_summary_precondition_with_points_to().

Here is the caller graph for this function:

select_fix_point_operator()

static void select_fix_point_operator ( )

static

This fix-point is not debugged nor used

Definition at line 150 of file dbm_interface.c.

{
    if(get_bool_property(SEMANTICS_FIX_POINT)) {
        const char* fp_name = get_string_property("SEMANTICS_FIX_POINT_OPERATOR");
        if(strcmp(fp_name, "transfer")==0) {
            transformer_fix_point_operator = transformer_equality_fix_point;
        }
        else if(strcmp(fp_name, "pattern")==0) {
            transformer_fix_point_operator = transformer_pattern_fix_point;
        }
        else if(strcmp(fp_name, "derivative")==0) {
            transformer_fix_point_operator = transformer_derivative_fix_point;
        }
        else {
            user_error("select_fix_point_operator", "Unknown value %s for property %s\n",
                       fp_name, "SEMANTICS_FIX_POINT_OPERATOR");
        }
    }
    else {
        transformer_fix_point_operator = transformer_basic_fix_point;
    }
    /* This fix-point is not debugged nor used */
    /*
    if(pips_flag_p(SEMANTICS_INEQUALITY_INVARIANT)) {
      tf = transformer_halbwachs_fix_point(tfb);
    }
    */
}

References get_bool_property(), get_string_property(), SEMANTICS_FIX_POINT, transformer_basic_fix_point(), transformer_derivative_fix_point(), transformer_equality_fix_point(), transformer_fix_point_operator, transformer_pattern_fix_point(), and user_error.

Referenced by preconditions_inter_fast(), preconditions_inter_full(), preconditions_inter_full_with_points_to(), preconditions_intra(), preconditions_intra_fast(), refine_transformers(), refine_transformers_with_points_to(), total_preconditions_inter(), total_preconditions_intra(), transformers_inter_fast(), transformers_inter_full(), transformers_inter_full_with_points_to(), transformers_intra_fast(), and transformers_intra_full().

Here is the call graph for this function:

Here is the caller graph for this function:

set_use_points_to()

static void set_use_points_to ( )

static

Definition at line 555 of file dbm_interface.c.

{
  use_points_to_information_p = true;
}

References use_points_to_information_p.

Referenced by interprocedural_summary_precondition_with_points_to().

Here is the caller graph for this function:

set_warning_counters()

void set_warning_counters

(

void

)

Definition at line 903 of file dbm_interface.c.

{
  wc = 0;
}

References wc.

Referenced by generic_module_name_to_transformers().

Here is the caller graph for this function:

summary_precondition()

bool summary_precondition

(

char *

module_name

)

transformer t = transformer_identity();

Add declaration information: arrays cannot be empty (Fortran standard, Section 5.1.2)

It does not seem to be a good idea for the semantics of SUMMARY_PRECONDITION. It seems better to have this information in the summary transformer as an input validity condition.

Try to put the summary precondition in a (partially) canonical form.

Parameters

module_name

odule_name

Definition at line 719 of file dbm_interface.c.

{
  /* transformer t = transformer_identity(); */
  transformer t = transformer_undefined;
  entity callee = module_name_to_entity(module_name);
 
  debug_on(SEMANTICS_DEBUG_LEVEL);
 
  make_statement_global_stack();
  set_current_module_entity(callee);
  set_current_module_statement((statement) db_get_memory_resource(DBR_CODE, module_name, true));
 
  if(entity_main_module_p(callee)) {
    t = main_summary_precondition(callee);
  }
  else {
    t = ordinary_summary_precondition(module_name, callee);
  }
 
  /* Add declaration information: arrays cannot be empty (Fortran
   * standard, Section 5.1.2)
   *
   * It does not seem to be a good idea for the semantics of
   * SUMMARY_PRECONDITION. It seems better to have this information in the
   * summary transformer as an input validity condition.
   *
   */
  if(false && get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
    set_cumulated_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
    set_proper_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
    module_to_value_mappings( get_current_module_entity() );
    transformer_add_declaration_information(t,
                                            get_current_module_entity());
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
    free_value_mappings();
  }
 
  pips_assert("t is defined", !transformer_undefined_p(t));
 
  /* Try to put the summary precondition in a (partially) canonical form. */
  t = transformer_normalize(t, 4);
  t = transformer_normalize(t, 4);
 
  ifdebug(3) {
    pips_debug(1, "considering summary precondition for %s\n", module_name);
    dump_transformer(t);
  }
 
  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
                         module_name, (char * )t);
 
  ifdebug(1) {
    pips_debug(1,
               "initial summary precondition %p for %s (%d call sites):\n",
               t, module_name, get_call_site_number());
    dump_transformer(t);
    pips_debug(1, "end for module %s\n", module_name);
  }
 
  reset_current_module_statement();
  reset_current_module_entity();
  free_statement_global_stack();
  debug_off();
 
  return true;
}

References callee, db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, dump_transformer, entity_main_module_p(), free_statement_global_stack(), free_value_mappings(), get_bool_property(), get_call_site_number(), get_current_module_entity(), ifdebug, main_summary_precondition(), make_statement_global_stack(), module_name(), module_name_to_entity(), module_to_value_mappings(), ordinary_summary_precondition(), pips_assert, pips_debug, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), SEMANTICS_DEBUG_LEVEL, set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), transformer_add_declaration_information(), transformer_normalize(), transformer_undefined, and transformer_undefined_p.

Referenced by interprocedural_summary_precondition(), interprocedural_summary_precondition_with_points_to(), and intraprocedural_summary_precondition().

Here is the call graph for this function:

Here is the caller graph for this function:

summary_total_postcondition()

bool summary_total_postcondition

(

char *

module_name

)

Look for all call sites in the callers

transformer t = transformer_identity();

no callers => empty precondition (but the main). FC. 08/01/1999.

try to eliminate (some) redundancy at a reasonnable cost

t = transformer_normalize(t, 2);

what cost?

Add declaration information: arrays cannot be empty (Fortran standard, Section 5.1.2)

It does not seem to be a good idea for the semantics of SUMMARY_PRECONDITION. It seems better to have this information in the summary transformer as an input validity condition.

Parameters

module_name

odule_name

Definition at line 789 of file dbm_interface.c.

{
  /* Look for all call sites in the callers
   */
  callees callers = (callees) db_get_memory_resource(DBR_CALLERS,
                                                     module_name,
                                                     true);
  entity callee = module_name_to_entity(module_name);
  /* transformer t = transformer_identity(); */
  transformer t = transformer_undefined;
 
  debug_on(SEMANTICS_DEBUG_LEVEL);
 
  pips_assert("Not implemented yet", false);
 
  set_current_module_entity(callee);
 
  ifdebug(1) {
    debug(1, "summary_precondition", "begin for %s with %d callers\n",
          module_name,
          gen_length(callees_callees(callers)));
    MAP(STRING, caller_name, {
      (void) fprintf(stderr, "%s, ", caller_name);
    }, callees_callees(callers));
    (void) fprintf(stderr, "\n");
  }
 
  reset_call_site_number();
 
  MAP(STRING, caller_name,
  {
    entity caller = module_name_to_entity(caller_name);
    t = update_precondition_with_call_site_preconditions(t, caller, callee);
  }, callees_callees(callers));
 
  if (!callees_callees(callers) &&
      !entity_main_module_p(callee) &&
      some_main_entity_p())
    {
      /* no callers => empty precondition (but the main).
         FC. 08/01/1999.
      */
      pips_user_warning("empty precondition to %s "
                        "because not in call tree from main.\n", module_name);
      t = transformer_empty();
    } else if (transformer_undefined_p(t)) {
      t = transformer_identity();
    } else {
      /* try to eliminate (some) redundancy at a reasonnable cost */
      /* t = transformer_normalize(t, 2); */
 
      /* what cost? */
      t = transformer_normalize(t, 7);
    }
 
  /* Add declaration information: arrays cannot be empty (Fortran
   * standard, Section 5.1.2)
   *
   * It does not seem to be a good idea for the semantics of
   * SUMMARY_PRECONDITION. It seems better to have this information in the
   * summary transformer as an input validity condition.
   *
   */
  if(false && get_bool_property("SEMANTICS_TRUST_ARRAY_DECLARATIONS")) {
    set_current_module_statement(
                                 (statement) db_get_memory_resource(DBR_CODE, module_name, true));
    set_cumulated_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_CUMULATED_EFFECTS, module_name, true));
    set_proper_rw_effects((statement_effects)
                             db_get_memory_resource(DBR_PROPER_EFFECTS, module_name, true));
    module_to_value_mappings( get_current_module_entity() );
    transformer_add_declaration_information(t,
                                            get_current_module_entity());
    reset_cumulated_rw_effects();
    reset_proper_rw_effects();
    reset_current_module_statement();
    free_value_mappings();
  }
 
  DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_TOTAL_POSTCONDITION,
                         module_name, (char * )t);
 
  ifdebug(1) {
    pips_debug(1,
               "summary total postcondition %p for %s (%d call sites):\n",
               t, module_name, get_call_site_number());
    dump_transformer(t);
    pips_debug(1, "end for module %s\n", module_name);
  }
 
  reset_current_module_entity();
  debug_off();
 
  return true;
}

References callee, callees_callees, caller_name, db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug(), debug_off, debug_on, dump_transformer, entity_main_module_p(), fprintf(), free_value_mappings(), gen_length(), get_bool_property(), get_call_site_number(), get_current_module_entity(), ifdebug, MAP, module_name(), module_name_to_entity(), module_to_value_mappings(), pips_assert, pips_debug, pips_user_warning, reset_call_site_number(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), SEMANTICS_DEBUG_LEVEL, set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), some_main_entity_p(), STRING, transformer_add_declaration_information(), transformer_empty(), transformer_identity(), transformer_normalize(), transformer_undefined, transformer_undefined_p, and update_precondition_with_call_site_preconditions().

Here is the call graph for this function:

summary_total_precondition()

bool summary_total_precondition

(

char *

module_name

)

there is a choice: do nothing and leave the effective computation in module_name_to_total_preconditions or move it here

Parameters

module_name

odule_name

Definition at line 885 of file dbm_interface.c.

{
    /* there is a choice: do nothing and leave the effective computation
       in module_name_to_total_preconditions or move it here */
  pips_debug(1, "considering module %s\n", module_name);
  return true;
}

References module_name(), and pips_debug.

Here is the call graph for this function:

summary_transformer()

bool summary_transformer

(

char *

module_name

)

There is a choice: do nothing and leave the effective computation in module_name_to_transformers, or move it here

There is another choice: distinguish between inter- and intra-procedural analyses at the summary level or in module_name_to_transformers(). The choice does not have to be consistent with the similar choice made for summary_precondition.

Parameters

module_name

odule_name

Definition at line 387 of file dbm_interface.c.

{
  /* There is a choice: do nothing and leave the effective computation
     in module_name_to_transformers, or move it here */
  /* There is another choice: distinguish between inter- and
     intra-procedural analyses at the summary level or in
     module_name_to_transformers(). The choice does not have to be
     consistent with the similar choice made for summary_precondition. */
  pips_debug(1, "considering module %s\n", module_name);
  return true;
}

References module_name(), and pips_debug.

Here is the call graph for this function:

test_warning_counters()

bool test_warning_counters

(

void

)

Definition at line 908 of file dbm_interface.c.

{
  return wc++==0;
}

References wc.

Referenced by points_to_unary_operation_to_transformer().

Here is the caller graph for this function:

total_preconditions_inter()

bool total_preconditions_inter

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 487 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_total_preconditions(module_name);
}

References module_name(), module_name_to_total_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

total_preconditions_intra()

bool total_preconditions_intra

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 475 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    set_bool_property(SEMANTICS_INEQUALITY_INVARIANT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_total_preconditions(module_name);
}

References module_name(), module_name_to_total_preconditions(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INEQUALITY_INVARIANT, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

transformer_add_declaration_information()

static void transformer_add_declaration_information ( transformer  pre, entity  m  )

static

Definition at line 242 of file dbm_interface.c.

{
  add_declaration_information(pre, m, false);
}

References add_declaration_information().

Referenced by generic_module_name_to_transformers(), summary_precondition(), and summary_total_postcondition().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_derivative_fix_point()

transformer transformer_derivative_fix_point

(

transformer

tf

)

Computation of a transitive closure using constraints on the discrete derivative.

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

Implicit equations, n::new - n::old = 0, are not added. Instead, invariant constraints in tf are obtained by projection and added.

Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old

I tried to use the standard procedure but arguments are not removed when the transformer tf is not feasible. Since we compute the * fix point and not the + fix point, the fix point is the identity.

sc is going to be modified and destroyed and eventually replaced in fix_tf

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

initial and final basis

basis vector

basis of difference vectors

Compute constraints with difference equations

Only generate difference equations if the old value is used

Project all variables but differences to get T'

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

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

Only generate difference equations if the old value is used

Project all difference variables

The full basis must be used again

Plug sc back into fix_tf

Add constraints about invariant variables. This could be avoided if implicit equalities were added before the derivative are processed: each invariant variable would generate an implicit null difference.

Such invariant constraints do not exist in general. We have them when array references are trusted.

This is wrong because we compute f* and not f+ and this is not true for the initial store.

What can be done instead is to refine fix_tf as :

dom(tf) U tf(fix_tf(dom(tf)))

But this fails because tf loops back to the beginning of the next iteration. Hence, the domain of tf implies two iterations instead of one. For instance, "i<n" becomes "i<=n-2" for a while loop such as "while(i<n) i++;".

So this refinement should be performed at a higher level where t_init and t_enter are know... so as to have:

dom_tf = transformer_range(t_enter(t_init)).

That's all!

Definition at line 1067 of file fix_point.c.

{
  transformer fix_tf = transformer_dup(tf);
 
  ifdebug(8) {
    pips_debug(8, "Begin for transformer %p:\n", tf);
    fprint_transformer(stderr, tf, (get_variable_name_t) external_value_name);
  }
 
  if(transformer_empty_p(tf)) {
    /* I tried to use the standard procedure but arguments are not removed
       when the transformer tf is not feasible. Since we compute the * fix
       point and not the + fix point, the fix point is the identity. */
    free_transformer(fix_tf);
    fix_tf = transformer_identity();
  }
  else {
    //transformer inv_tf = transformer_undefined; /* invariant constraints of tf */
    /* sc is going to be modified and destroyed and eventually
       replaced in fix_tf */
    Psysteme sc = predicate_system(transformer_relation(fix_tf));
    /* Do not handle variable which do not appear explicitly in constraints! */
    Pbase b = sc_to_minimal_basis(sc);
    Pbase ib = base_dup(sc_base(sc)); /* initial and final basis */
    Pbase bv = BASE_NULLE; /* basis vector */
    Pbase diffb = BASE_NULLE; /* basis of difference vectors */
 
    /* 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);
    }
 
    /* 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, true);
    //Psysteme sc_t_prime_star = sc_projection_ofl(sc_t_prime_k, (Variable) ik);
    sc = sc_projection_ofl(sc, (Variable) ik);
    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);
      }
    }
 
    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 fix_tf */
    predicate_system(transformer_relation(fix_tf)) = sc;
 
    /* Add constraints about invariant variables. This could be avoided if
       implicit equalities were added before the derivative are processed:
       each invariant variable would generate an implicit null
       difference.
 
       Such invariant constraints do not exist in general. We have them when
       array references are trusted.
 
       This is wrong because we compute f* and not f+ and this is not true
       for the initial store.
 
    */
    /*
       inv_tf = transformer_arguments_projection(transformer_dup(tf));
       fix_tf = transformer_image_intersection(fix_tf, inv_tf);
       free_transformer(inv_tf);
    */
 
    /* What can be done instead is to refine fix_tf as :
     *
     * dom(tf) U tf(fix_tf(dom(tf)))
     *
     * But this fails because tf loops back to the beginning of the
     * next iteration. Hence, the domain of tf implies *two*
     * iterations instead of one. For instance, "i<n" becomes "i<=n-2"
     * for a while loop such as "while(i<n) i++;".
     *
     * So this refinement should be performed at a higher level where
     * t_init and t_enter are know... so as to have:
     *
     * dom_tf = transformer_range(t_enter(t_init)).
     */
    /*
    transformer dom_tf = transformer_to_domain(tf);
    transformer tf_plus = transformer_combine(copy_transformer(dom_tf), fix_tf);
    tf_plus = transformer_combine(tf_plus, tf);
    free_transformer(fix_tf);
    fix_tf = transformer_convex_hull(dom_tf, tf_plus);
    free_transformer(dom_tf);
    free_transformer(tf_plus);
    */
  }
  /* That's all! */
 
  ifdebug(8) {
    pips_debug(8, "fix-point fix_tf=\n");
    fprint_transformer(stderr, fix_tf, (get_variable_name_t) external_value_name);
    transformer_consistency_p(fix_tf);
    pips_debug(8, "end\n");
  }
 
  return fix_tf;
}

References Ssysteme::base, base_add_variable(), base_dup(), BASE_NULLE, BASE_NULLE_P, base_remove_variable(), base_rm, contrainte_make(), CONTRAINTE_UNDEFINED, Ssysteme::dimension, entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), fprint_transformer(), free_transformer(), ifdebug, make_local_temporary_integer_value_entity(), old_value_entity_p(), pips_debug, predicate_system, sc_equation_add(), sc_fprint(), sc_multiply_constant_terms(), sc_to_minimal_basis(), Svecteur::succ, TCST, transformer_consistency_p(), transformer_dup(), transformer_empty_p(), transformer_identity(), transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), vect_size(), VECTEUR_NUL, and vecteur_var.

Referenced by invariant_wrt_transformer(), and select_fix_point_operator().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_equality_fix_point()

transformer transformer_equality_fix_point

(

transformer

tf

)

Let A be the affine loop transfert function.

The affine transfer fix-point T is such that T(A-I) = 0

T A = 0 also gives a fix-point when merged with the initial state. It can only be used to compute preconditions.

Algorithm (let H be A's Smith normal form):

A = A - I (if necessary) H = P A Q A = P^-1 H Q^-1 T A = T P^-1 H Q^-1 = 0 T P^-1 H = 0 (by multipliying by Q)

Soit X t.q. X H = 0 A basis for all solutions is given by X chosen such that X is a rectangular matrix (0 I) selecting the zero submatrix of H

T P^-1 = X T = X P

Note: I (FI) believe this functions is wrong because it does not return the appropriate arguments. The fix point transformer should modify as many variables as the input tf. A new basis should not be recomputed according to the transition matrix. This problem seems to be fixed in the callers, see loop_to_transformer() and whileloop_to_transformer().

result

do not modify an input argument

number of transfer equalities plus the homogeneous constraint which states that 1 == 1

use a matrix a to store these equalities in a dense form

Pbase t = BASE_UNDEFINED;

If the input transformer is not feasible, so is not its fixpoint because the number of iterations may be zero which implies identity.

fix_tf = transformer_identity();

find or build explicit transfer equations: v::new = f(v1::old, v2::old,...) and the corresponding sub-basis

FI: for each constant variable, whose constance is implictly implied by not having it in the argument field, an equation should be added...

lieq = build_implicit_equalities(tf); lieq->succ = leq; leq = lieq;

build matrix a from lteq and b_new: this should be moved in a function

Subtract the identity matrix

Compute the Smith normal form: H = P A Q

Find out the number of invariants n_inv

Convert p's last n_inv rows into constraints

FI: maybe I should retrieve fix_tf system...

is it a non-trivial invariant?

Set fix_tf's argument list

Fix the basis and the dimension

get rid of dense matrices

Definition at line 266 of file fix_point.c.

{
    /* result */
    transformer fix_tf = transformer_identity();
 
    /* do not modify an input argument */
    transformer tf_copy = transformer_dup(tf);
 
    /* number of transfer equalities plus the homogeneous constraint which
       states that 1 == 1 */
    int n_eq = 1;
    /* use a matrix a to store these equalities in a dense form */
    matrice a = MATRICE_UNDEFINED;
    matrice h = MATRICE_UNDEFINED;
    matrice p = MATRICE_UNDEFINED;
    matrice q = MATRICE_UNDEFINED;
    Pbase b_new = BASE_NULLE;
    Pcontrainte lteq = CONTRAINTE_UNDEFINED;
    Pcontrainte leq = sc_egalites((Psysteme) predicate_system(transformer_relation(tf_copy)));
 
    Psysteme sc_inv = SC_UNDEFINED;
    int n_inv = 0;
 
    int i = 0;
    /* Pbase t = BASE_UNDEFINED; */
 
    ifdebug(8) {
        pips_debug(8, "begin for transformer %p\n", tf);
        fprint_transformer(stderr, tf,
                           (get_variable_name_t) external_value_name);
    }
 
    /* If the input transformer is not feasible, so is not its fixpoint
     * because the number of iterations may be zero which implies identity.
     */
    if(transformer_empty_p(tf)) {
      /* fix_tf = transformer_identity(); */
        ifdebug(8) {
            pips_debug(8, "fix-point fix_tf=\n");
            fprint_transformer(stderr, fix_tf,
                               (get_variable_name_t) external_value_name);
            pips_debug(8, "end\n");
        }
        return fix_tf;
    }
 
    /* find or build explicit transfer equations: v#new = f(v1#old, v2#old,...)
     * and the corresponding sub-basis
     *
     * FI: for each constant variable, whose constance is implictly
     * implied by not having it in the argument field, an equation
     * should be added...
     *
     * lieq = build_implicit_equalities(tf);
     * lieq->succ = leq;
     * leq = lieq;
     */
    build_transfer_equations(leq, &lteq, &b_new);
 
    /* build matrix a from lteq and b_new: this should be moved in a function */
    n_eq = base_dimension(b_new)+1;
    build_transfer_matrix(&a , lteq, n_eq, b_new);
    ifdebug(8) {
        pips_debug(8, "transfer matrix:\n");
        matrice_fprint(stderr, a, n_eq, n_eq);
    }
 
    /* Subtract the identity matrix */
    for(i=1; i<= n_eq; i++) {
        value_substract(ACCESS(a, n_eq, i, i),VALUE_ONE);
    }
 
    /* Compute the Smith normal form: H = P A Q */
    h = matrice_new(n_eq, n_eq);
    p = matrice_new(n_eq, n_eq);
    q = matrice_new(n_eq, n_eq);
    DENOMINATOR(h) = VALUE_ONE;
    DENOMINATOR(p) = VALUE_ONE;
    DENOMINATOR(q) = VALUE_ONE;
    matrice_smith(a, n_eq, n_eq, p, h, q);
 
    ifdebug(8) {
        pips_debug(8, "smith matrix h=p.a.q:\n");
        matrice_fprint(stderr, h, n_eq, n_eq);
        pips_debug(8, "p  matrix:\n");
        matrice_fprint(stderr, p, n_eq, n_eq);
        pips_debug(8, "q  matrix:\n");
        matrice_fprint(stderr, q, n_eq, n_eq);
    }
 
    /* Find out the number of invariants n_inv */
    for(i=1; i <= n_eq &&
            value_notzero_p(ACCESS(h, n_eq, i, i)) ; i++)
        ;
    n_inv = n_eq - i + 1;
    pips_debug(8, "number of useful invariants: %d\n", n_inv-1);
    pips_assert("n_inv>=1", n_inv >= 1);
 
    /* Convert p's last n_inv rows into constraints */
    /* FI: maybe I should retrieve fix_tf system... */
    sc_inv = sc_new();
 
    for(i = n_eq - n_inv + 1 ; i <= n_eq; i++) {
        int j;
        /* is it a non-trivial invariant? */
        for(j=1; j<= n_eq-1 && value_zero_p(ACCESS(p, n_eq, i, j)); j++)
            ;
        if( j != n_eq) {
            Pvecteur v_inv = VECTEUR_NUL;
            Pcontrainte c_inv = CONTRAINTE_UNDEFINED;
 
            for(j = 1; j<= n_eq; j++) {
                Value coeff = ACCESS(p, n_eq, i, j);
 
                if(value_notzero_p(coeff)) {
                    entity n_eb = (entity) variable_of_rank(b_new, j);
                    entity o_eb = new_value_to_old_value(n_eb);
 
                    vect_add_elem(&v_inv, (Variable)n_eb, coeff);
                    vect_add_elem(&v_inv, (Variable)o_eb, value_uminus(coeff));
                }
            }
            c_inv = contrainte_make(v_inv);
            sc_add_egalite(sc_inv, c_inv);
        }
    }
 
    sc_creer_base(sc_inv);
 
    ifdebug(8) {
        pips_debug(8, "fix-point sc_inv=\n");
        sc_fprint(stderr, sc_inv, (char * (*)(Variable)) external_value_name);
        pips_debug(8, "end\n");
    }
 
    /* Set fix_tf's argument list */
    /*
    for(t = b_new; !BASE_NULLE_P(t); t = t->succ) {
        I should use a conversion function from value_to_variable()
        entity arg = (entity) vecteur_var(t);
 
        transformer_arguments(fix_tf) = arguments_add_entity(transformer_arguments(fix_tf), arg);
    }
    */
    transformer_arguments(fix_tf) = dup_arguments(transformer_arguments(tf));
    /* Fix the basis and the dimension */
    sc_base(sc_inv) = base_dup(sc_base(predicate_system(transformer_relation(tf))));
    sc_dimension(sc_inv) = sc_dimension(predicate_system(transformer_relation(tf)));
    transformer_relation(fix_tf) = make_predicate(sc_inv);
 
    /* get rid of dense matrices */
    matrice_free(a);
    matrice_free(h);
    matrice_free(p);
    matrice_free(q);
 
    free_transformer(tf_copy);
 
    ifdebug(8) {
        pips_debug(8, "fix-point fix_tf=\n");
        fprint_transformer(stderr, fix_tf, (get_variable_name_t) external_value_name);
        pips_debug(8, "end\n");
    }
 
    return fix_tf;
}

References ACCESS, base_dimension, base_dup(), BASE_NULLE, build_transfer_equations(), build_transfer_matrix(), contrainte_make(), CONTRAINTE_UNDEFINED, DENOMINATOR, dup_arguments(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, make_predicate(), matrice_fprint(), matrice_free, matrice_new, matrice_smith(), MATRICE_UNDEFINED, new_value_to_old_value(), pips_assert, pips_debug, predicate_system, sc_add_egalite(), sc_creer_base(), sc_fprint(), sc_new(), transformer_arguments, transformer_dup(), transformer_empty_p(), transformer_identity(), transformer_relation, value_notzero_p, VALUE_ONE, value_substract, value_uminus, value_zero_p, variable_of_rank(), vect_add_elem(), and VECTEUR_NUL.

Referenced by select_fix_point_operator(), and standard_whileloop_to_transformer().

Here is the call graph for this function:

Here is the caller graph for this function:

transformer_pattern_fix_point()

transformer transformer_pattern_fix_point

(

transformer

tf

)

This fixpoint function was developped to present a talk at FORMA.

I used examples published by Pugh and I realized that the fixpoint constraints were obvious in the loop body transformer. You just had to identify them. This is not a clever algorithm. It certainly would not resist any messing up with the constraints, i.e. a change of basis. But it provides very good result for a class of applications.

Algorithm:

1. Find a loop counter
2. Use it to eliminate all constant terms
3. Look for invariant constraints

Let d_i = i::new - i::old. An invariant constraint is a sum of d_i which is equal to zero or greater than zero. Such a constraint is its own fixpoint: if you combine it with itself after renaming i::new as i::int on one hand and i::old as i::int on the other, the global sum for and equation or its sign for an inequality is unchanged.

result

Look for the best loop counter: the smallest increment is chosen

eliminate sharing between v_inc and fix_sc

Replace constant terms in equalities and inequalities by loop counter differences

Remove all constraints to build the invariant transformer

Definition at line 709 of file fix_point.c.

{
    /* result */
    transformer fix_tf =  transformer_dup(tf);
    Psysteme fix_sc = (Psysteme) predicate_system(transformer_relation(fix_tf));
    Pvecteur v_inc = VECTEUR_UNDEFINED;
 
    ifdebug(8) {
        pips_debug(8, "Begin for transformer %p:\n", tf);
        fprint_transformer(stderr, tf,
                           (get_variable_name_t) external_value_name);
    }
 
    /* Look for the best loop counter: the smallest increment is chosen */
    v_inc = look_for_the_best_counter(sc_egalites(fix_sc));
 
    if(!VECTEUR_UNDEFINED_P(v_inc)) {
 
        ifdebug(8) {
            pips_debug(8, "incrementation vector=\n");
            vect_fprint(stderr, v_inc, (char * (*)(Variable)) external_value_name);
        }
 
        /* eliminate sharing between v_inc and fix_sc */
        v_inc = vect_dup(v_inc);
 
        /* Replace constant terms in equalities and inequalities by
         * loop counter differences
         */
        fix_sc = sc_eliminate_constant_terms(fix_sc, v_inc);
 
        ifdebug(8) {
            pips_debug(8, "after constant term elimination=\n");
            sc_fprint(stderr, fix_sc, (char * (*)(Variable)) external_value_name);
        }
 
        fix_sc = sc_elim_redund(fix_sc);
 
        ifdebug(8) {
            pips_debug(8, "after normalization=\n");
            sc_fprint(stderr, fix_sc, (char * (*)(Variable)) external_value_name);
        }
 
        fix_sc = sc_keep_invariants_only(fix_sc);
 
        ifdebug(8) {
            pips_debug(8, "after non-invariant elimination=\n");
            sc_fprint(stderr, fix_sc, (char * (*)(Variable)) external_value_name);
        }
 
        fix_sc = sc_elim_redund(fix_sc);
 
        ifdebug(8) {
            pips_debug(8, "after 2nd normalization=\n");
            sc_fprint(stderr, fix_sc, (char * (*)(Variable)) external_value_name);
        }
    }
    else {
        pips_debug(8, "No counter found\n");
        /* Remove all constraints to build the invariant transformer */
        contraintes_free(sc_egalites(fix_sc));
        sc_egalites(fix_sc) = CONTRAINTE_UNDEFINED;
        sc_nbre_egalites(fix_sc) = 0;
        contraintes_free(sc_inegalites(fix_sc));
        sc_inegalites(fix_sc) = CONTRAINTE_UNDEFINED;
        sc_nbre_inegalites(fix_sc) = 0;
    }
 
    ifdebug(8) {
        pips_debug(8, "fix-point fix_tf=\n");
        fprint_transformer(stderr, fix_tf, (get_variable_name_t) external_value_name);
        pips_debug(8, "end\n");
    }
 
    return fix_tf;
}

References CONTRAINTE_UNDEFINED, contraintes_free(), external_value_name(), fprint_transformer(), ifdebug, look_for_the_best_counter(), pips_debug, predicate_system, sc_elim_redund(), sc_eliminate_constant_terms(), sc_fprint(), sc_keep_invariants_only(), transformer_dup(), transformer_relation, vect_dup(), vect_fprint(), VECTEUR_UNDEFINED, and VECTEUR_UNDEFINED_P.

Referenced by select_fix_point_operator().

Here is the call graph for this function:

Here is the caller graph for this function:

transformers_inter_fast()

bool transformers_inter_fast

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 310 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, false);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

References module_name(), module_name_to_transformers(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

transformers_inter_full()

bool transformers_inter_full

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 321 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

References module_name(), module_name_to_transformers(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

transformers_inter_full_with_points_to()

bool transformers_inter_full_with_points_to

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 332 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    set_pt_to_list( (statement_points_to)
                    db_get_memory_resource(DBR_POINTS_TO, module_name, true) );
    bool result = module_name_to_transformers(module_name);
    reset_pt_to_list();
 
    return result;
}

References db_get_memory_resource(), module_name(), module_name_to_transformers(), reset_pt_to_list(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, set_bool_property(), and set_pt_to_list().

Here is the call graph for this function:

transformers_intra_fast()

bool transformers_intra_fast

(

char *

module_name

)

Functions to make transformers.

Set properties as required for a very fast semantics analysis

No need to select a fix point operator given the above property, but just in case...

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Restaure initial values of modified properties

Parameters

module_name

odule_name

Definition at line 254 of file dbm_interface.c.

{
  bool si = get_bool_property(SEMANTICS_INTERPROCEDURAL);
  bool sfs = get_bool_property(SEMANTICS_FLOW_SENSITIVE);
  bool sfp = get_bool_property(SEMANTICS_FIX_POINT);
  bool result = true;
 
  /* Set properties as required for a very fast semantics analysis */
  if(si) {
    pips_user_warning("Property SEMANTICS_INTERPROCEDURAL is ignored\n");
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
  }
  if(!sfs) {
    pips_user_warning("Property SEMANTICS_FLOW_SENSITIVE is ignored\n");
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
  }
  if(sfp) {
    pips_user_warning("Property SEMANTICS_FIX_POINT is ignored\n");
    set_bool_property(SEMANTICS_FIX_POINT, false);
  }
  /* No need to select a fix point operator given the above property, but just in case... */
  select_fix_point_operator();
 
  set_bool_property(SEMANTICS_STDOUT, false);
  /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
 
  if(get_bool_property("SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT")) {
    pips_user_warning("If you really want to set property "
                      "SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT, "
                      "you should activate TRANSFORMERS_INTER_FULL\n");
  }
 
  result =  module_name_to_transformers(module_name);
 
  /* Restaure initial values of modified properties */
  if(si)
    set_bool_property(SEMANTICS_INTERPROCEDURAL, true);
  if(!sfs)
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, false);
  if(sfp)
    set_bool_property(SEMANTICS_FIX_POINT, true);
 
  return result;
}

References get_bool_property(), module_name(), module_name_to_transformers(), pips_user_warning, select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

transformers_intra_full()

bool transformers_intra_full

(

char *

module_name

)

set_int_property(SEMANTICS_DEBUG_LEVEL, 0);

Parameters

module_name

odule_name

Definition at line 299 of file dbm_interface.c.

{
    set_bool_property(SEMANTICS_INTERPROCEDURAL, false);
    set_bool_property(SEMANTICS_FLOW_SENSITIVE, true);
    set_bool_property(SEMANTICS_FIX_POINT, true);
    select_fix_point_operator();
    set_bool_property(SEMANTICS_STDOUT, false);
    /* set_int_property(SEMANTICS_DEBUG_LEVEL, 0); */
    return module_name_to_transformers(module_name);
}

References module_name(), module_name_to_transformers(), select_fix_point_operator(), SEMANTICS_FIX_POINT, SEMANTICS_FLOW_SENSITIVE, SEMANTICS_INTERPROCEDURAL, SEMANTICS_STDOUT, and set_bool_property().

Here is the call graph for this function:

update_summary_precondition()

void update_summary_precondition	(	entity	e,
		transformer	t
	)

void update_summary_precondition(e, t): t is supposed to be a precondition related to one of e's call sites and translated into e's basis;

the current global precondition for e is replaced by its convex hull with t;

t may be slightly modified by transformer_convex_hull because of bad design (FI)

Definition at line 1390 of file dbm_interface.c.

{
    transformer t_old = transformer_undefined;
    transformer t_new = transformer_undefined;
 
    pips_assert("update_summary_precondition", entity_module_p(e));
 
    debug(8, "update_summary_precondition", "begin\n");
 
    t_old = (transformer)
        db_get_memory_resource(DBR_SUMMARY_PRECONDITION, module_local_name(e),
                               true);
 
    ifdebug(8) {
        debug(8, "update_summary_precondition", " old precondition for %s:\n",
              entity_local_name(e));
        print_transformer(t_old);
    }
 
    if(t_old == transformer_undefined)
        t_new = transformer_dup(t);
    else {
        t_new = transformer_convex_hull(t_old, t);
        transformer_free(t_old);
    }
 
    DB_PUT_MEMORY_RESOURCE(DBR_SUMMARY_PRECONDITION,
                           module_local_name(e),
                           (char*) t_new );
 
    ifdebug(8) {
        debug(8, "update_summary_precondition", "new precondition for %s:\n",
              entity_local_name(e));
        print_transformer(t_new);
        debug(8, "update_summary_precondition", "end\n");
    }
}

References db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug(), entity_local_name(), entity_module_p(), ifdebug, module_local_name(), pips_assert, print_transformer, transformer_convex_hull(), transformer_dup(), transformer_free(), and transformer_undefined.

Here is the call graph for this function:

use_points_to_p()

bool use_points_to_p

(

void

)

Definition at line 565 of file dbm_interface.c.

{
  return use_points_to_information_p;
}

References use_points_to_information_p.

Referenced by update_precondition_with_call_site_preconditions().

Here is the caller graph for this function:

Variable Documentation

refine_transformers_p

bool refine_transformers_p = false

Transformer recomputation cannot be of real use unless an interprocedural analysis is performed.

For intraprocedural analyses, using property SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT is sufficient.

Definition at line 352 of file dbm_interface.c.

Referenced by process_ready_node(), refine_transformers(), refine_transformers_with_points_to(), statement_to_transformer(), and statement_to_transformer_list().

transformer_fix_point_operator

transformer(* transformer_fix_point_operator) (transformer) ( transformer  )

extern

Interface between the untyped database manager and clean code and between pipsmake and clean code.

There are other interface routines in prettyprint.c

The top routines should be called by the PIPS make utility. They might eventually be integrated into it.

The lower level routines are dealing with "statement_mapping"s. They might have to be updated when mappings are integrated into NewGen. At that time, the whole file should disappear in a typed pipsmake.

Francois Irigoin, August 1990 the lowest level routines dealing with "statement_mapping"s are now generated by a macro defined in mapping.h : DEFINE_CURRENT_MAPPING. see this file for more details.

Be'atrice Apvrille, August 1993 FC 2015-07-21: redundant declarations to help with include cycle issues there are expected in "transformer.h"

Interface between the untyped database manager and clean code and between pipsmake and clean code.

Several algorithms are available:

• two untested versions using Halwachs approach; sc_elarg() was found to be very slow in an earlier implementation by Malik; experimentally, we did not find scientific Frotran programs that required such an algorithm.
• a fix point algorithm based on the transfer matrix linking the new values to the old values; this is sufficient for induction variables but only equations can be found.
• a fix point algorithm based on pattern matching which was developped experimentally for examples presented at FORMA; once the constant terms are eliminated using a loop counter, the constraints which are their own fixpoints are easy to pattern match; equations and inequalities can both be found.

• a fix point algorithm combining the last two algorithms above. This algorithm adds difference variables d_i = i::new - i::old for each variable i. All non d_i variables are thn projected. If the projection algorithm is sophisticated enough, the projection ordering will be "good". Left over inequalities are invariant or useless. Let N be the strictly positive iteration count:

  sum ai di <= -k implies N sum ai di <= -Nk <= -k (OK)

  sum ai di <= k implies N sum ai di <= Nk <= infinity (useless unless k == 0)

  Left over equations can stay equations if the constant term is 0, or be degraded into an inequation if not. The nw inequation depends on the sign of the constant:

  sum ai di == -k implies N sum ai di == -Nk <= -k

  sum ai di == k implies N sum ai di == Nk >= k

  sum ai di == 0 implies N sum ai di == 0

  In a second step, the constant terms are eliminated to obtain new constraints leading to new invariants, using the same rules as above.

  This algorithm was designed for while loops such as:

  WHILE( I > 0 ) J = J + I I = I - 1

  to find as loop transformer T(I,J) {I::new <= I::old - 1, J::new >= J::old + 1, I::new+J::new >= I::old + J::old}

  Note that the second constraint is redundant with the other two, but the last one cannot be found before the constant terms are eliminated.

The current algorithm, the derivative version, is published and describes in NSAD 2010, A/426/CRI. See also A/429/CRI: http://www.cri.ensmp.fr/classement/doc/A-429.pdf

Francois Irigoin, 21 April 1990 The fixpoint operator is selected according to properties

Definition at line 114 of file fix_point.c.

Referenced by select_fix_point_operator(), and standard_whileloop_to_transformer().

use_points_to_information_p

bool use_points_to_information_p = false

static

Definition at line 553 of file dbm_interface.c.

Referenced by reset_use_points_to(), set_use_points_to(), and use_points_to_p().

wc

int wc = 0

static

FI: Provisional management of warnings.

To avoid repetitive warnings.

A hash table could be used to count warnings according to the function and line number in the C file.

Definition at line 901 of file dbm_interface.c.

Referenced by set_warning_counters(), test_warning_counters(), and VASNPRINTF().