PIPS
|
#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"
Go to the source code of this file.
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... | |
|
static |
Definition at line 223 of file dbm_interface.c.
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().
void add_declaration_list_information | ( | transformer | pre, |
list | dl, | ||
bool | precondition_p | ||
) |
pre | re |
dl | l |
precondition_p | recondition_p |
Definition at line 179 of file dbm_interface.c.
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().
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.
References effects_effects, f(), fprintf(), get_cumulated_rw_effects(), print_effects, STATEMENT_EFFECTS_MAP, and statement_ordering.
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()
module_name | odule_name |
in_context | n_context |
Definition at line 918 of file dbm_interface.c.
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().
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.
module_name | odule_name |
Definition at line 545 of file dbm_interface.c.
References module_name(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), and summary_precondition().
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.
module_name | odule_name |
Definition at line 571 of file dbm_interface.c.
References module_name(), reset_use_points_to(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), set_use_points_to(), and summary_precondition().
bool intraprocedural_summary_precondition | ( | char * | module_name | ) |
The current module is sufficient to derive it.
module_name | odule_name |
Definition at line 538 of file dbm_interface.c.
References module_name(), SEMANTICS_INTERPROCEDURAL, set_bool_property(), and summary_precondition().
Definition at line 1508 of file dbm_interface.c.
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().
transformer load_completed_statement_transformer | ( | statement | s | ) |
three mappings used throughout semantics analysis:
(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:
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.
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().
memoization could be used to improve efficiency
Definition at line 1526 of file dbm_interface.c.
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().
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.
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().
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.
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().
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.
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().
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.
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().
|
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.
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().
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
module_name | odule_name |
Definition at line 1073 of file dbm_interface.c.
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().
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
module_name | odule_name |
Definition at line 1203 of file dbm_interface.c.
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().
bool module_name_to_transformers | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 1062 of file dbm_interface.c.
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().
bool module_name_to_transformers_in_context | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 1044 of file dbm_interface.c.
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().
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
module_name | odule_name |
Definition at line 500 of file dbm_interface.c.
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().
|
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.
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().
|
static |
Definition at line 247 of file dbm_interface.c.
References add_declaration_information().
Referenced by module_name_to_preconditions().
bool preconditions_inter_fast | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 435 of file dbm_interface.c.
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().
bool preconditions_inter_full | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 447 of file dbm_interface.c.
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().
bool preconditions_inter_full_with_points_to | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 459 of file dbm_interface.c.
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().
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);
module_name | odule_name |
Definition at line 399 of file dbm_interface.c.
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().
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);
module_name | odule_name |
Definition at line 417 of file dbm_interface.c.
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().
bool refine_transformers | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 354 of file dbm_interface.c.
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().
bool refine_transformers_with_points_to | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 369 of file dbm_interface.c.
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().
|
static |
Definition at line 560 of file dbm_interface.c.
References use_points_to_information_p.
Referenced by interprocedural_summary_precondition_with_points_to().
|
static |
This fix-point is not debugged nor used
Definition at line 150 of file dbm_interface.c.
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().
|
static |
Definition at line 555 of file dbm_interface.c.
References use_points_to_information_p.
Referenced by interprocedural_summary_precondition_with_points_to().
void set_warning_counters | ( | void | ) |
Definition at line 903 of file dbm_interface.c.
References wc.
Referenced by generic_module_name_to_transformers().
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.
module_name | odule_name |
Definition at line 719 of file dbm_interface.c.
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().
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.
module_name | odule_name |
Definition at line 789 of file dbm_interface.c.
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().
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
module_name | odule_name |
Definition at line 885 of file dbm_interface.c.
References module_name(), and pips_debug.
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.
module_name | odule_name |
Definition at line 387 of file dbm_interface.c.
References module_name(), and pips_debug.
bool test_warning_counters | ( | void | ) |
Definition at line 908 of file dbm_interface.c.
References wc.
Referenced by points_to_unary_operation_to_transformer().
bool total_preconditions_inter | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 487 of file dbm_interface.c.
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().
bool total_preconditions_intra | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 475 of file dbm_interface.c.
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().
|
static |
Definition at line 242 of file dbm_interface.c.
References add_declaration_information().
Referenced by generic_module_name_to_transformers(), summary_precondition(), and summary_total_postcondition().
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.
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().
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
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.
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().
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:
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.
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().
bool transformers_inter_fast | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 310 of file dbm_interface.c.
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().
bool transformers_inter_full | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 321 of file dbm_interface.c.
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().
bool transformers_inter_full_with_points_to | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 332 of file dbm_interface.c.
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().
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
module_name | odule_name |
Definition at line 254 of file dbm_interface.c.
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().
bool transformers_intra_full | ( | char * | module_name | ) |
set_int_property(SEMANTICS_DEBUG_LEVEL, 0);
module_name | odule_name |
Definition at line 299 of file dbm_interface.c.
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().
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.
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.
bool use_points_to_p | ( | void | ) |
Definition at line 565 of file dbm_interface.c.
References use_points_to_information_p.
Referenced by update_precondition_with_call_site_preconditions().
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().
|
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:
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().
Definition at line 553 of file dbm_interface.c.
Referenced by reset_use_points_to(), set_use_points_to(), and use_points_to_p().
|
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().