PIPS
|
Go to the source code of this file.
Data Structures | |
struct | path |
Macros | |
#define | SEMANTICS_OPTIONS "?Otcfieod-D:" |
Warning! Do not modify this file that is automatically generated! More... | |
#define | SEQUENTIAL_TRANSFORMER_SUFFIX ".tran" |
#define | USER_TRANSFORMER_SUFFIX ".utran" |
#define | SEQUENTIAL_PRECONDITION_SUFFIX ".prec" |
#define | USER_PRECONDITION_SUFFIX ".uprec" |
#define | SEQUENTIAL_TOTAL_PRECONDITION_SUFFIX ".tprec" |
#define | USER_TOTAL_PRECONDITION_SUFFIX ".utprec" |
#define | semantics_user_warning semantics_user_warning_func2 |
Variables | |
bool | refine_transformers_p |
Transformer recomputation cannot be of real use unless an interprocedural analysis is performed. More... | |
#define SEMANTICS_OPTIONS "?Otcfieod-D:" |
Warning! Do not modify this file that is automatically generated!
Modify src/Libs/semantics/semantics-local.h instead, to add your own modifications. header file built by cproto semantics-local.h include file for semantic analysis
Definition at line 34 of file semantics.h.
#define semantics_user_warning semantics_user_warning_func2 |
Definition at line 54 of file semantics.h.
#define SEQUENTIAL_PRECONDITION_SUFFIX ".prec" |
Definition at line 38 of file semantics.h.
#define SEQUENTIAL_TOTAL_PRECONDITION_SUFFIX ".tprec" |
Definition at line 40 of file semantics.h.
#define SEQUENTIAL_TRANSFORMER_SUFFIX ".tran" |
Definition at line 36 of file semantics.h.
#define USER_PRECONDITION_SUFFIX ".uprec" |
Definition at line 39 of file semantics.h.
#define USER_TOTAL_PRECONDITION_SUFFIX ".utprec" |
Definition at line 41 of file semantics.h.
#define USER_TRANSFORMER_SUFFIX ".utran" |
Definition at line 37 of file semantics.h.
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().
e and eq are assumed to be different scalar variables of the same analyzed type
eq will be seen as e, as far as values are concerned, but for printing
new equalities e::new == eq::new and e::old == eq::old have to be added to the preconditions just before they are stored; since eq should never be written no eq::old should appear; thus the first equation is enough
By definition, all variables are conflicting with themselves but this is assumed filtered out above.
add the equivalence equations
eq | q |
readonly | eadonly |
Definition at line 107 of file mappings.c.
References add_equivalence_equality(), add_synonym_values(), eq, and pips_assert.
Referenced by add_or_kill_equivalenced_variables().
transformer add_formal_to_actual_bindings | ( | call | c, |
transformer | pre, | ||
entity | caller | ||
) |
add_formal_to_actual_bindings(call c, transformer pre, entity caller):
pre := pre U {f = expr } i i for all i such that formal f_i is an analyzable scalar variable and as far as expression expr_i is analyzable and of the same type
let's start a long, long, long MAPL, so long that MAPL is a pain
type checking. You already know that fp is a scalar variable
Do not care about side effects on expressions: this is used to map a caller precondition towards a callee summary precondition.
tmp must be used instead of fp_new because fp_new does not exist in the caller frame
Likely memory leak for the initial pre
ignore assocation
pre | re |
caller | aller |
Definition at line 283 of file interprocedural.c.
References any_expression_to_transformer(), basic_of_expression(), basic_tag, basic_to_string(), call_arguments, call_function, CAR, dump_transformer, ENDP, ENTITY, entity_local_name(), entity_module_p(), entity_storage, entity_type, expression_undefined, external_entity_to_new_value(), f(), find_ith_argument(), formal_offset, free_arguments(), free_transformer(), ifdebug, make_local_temporary_value_entity(), module_local_name(), module_to_formal_analyzable_parameters(), pips_assert, pips_debug, pips_user_error, pips_user_warning, POP, same_basic_p(), storage_formal, transformer_safe_image_intersection(), transformer_safe_value_substitute(), transformer_undefined, type_variable, and variable_basic.
Referenced by call_site_to_module_precondition_text(), and call_to_summary_precondition().
It is assumed that al is an abstract location that is written and which may conflict with effects in effect list el.
If there is a conflict, than the variable associated to this effect is written.
It should be generalized to non-interprocedural cases.
al | l |
el | l |
Definition at line 382 of file mappings.c.
References add_interprocedural_value_entities(), analyzable_scalar_entity_p(), dummy_parameter_entity_p(), EFFECT, effect_any_reference, entities_may_conflict_p(), entity_abstract_location_p(), entity_type, FOREACH, get_bool_property(), overloaded_type_p(), pips_internal_error, reference_variable, type_area_p, type_equal_p(), type_unknown_p, and ultimate_type().
Referenced by module_to_value_mappings().
transformer add_index_range_conditions | ( | transformer | pre, |
entity | i, | ||
range | r, | ||
transformer | tfb | ||
) |
if tfb is not undefined, then it is a loop; loop bounds can be kept as preconditions for the loop body if the loop increment is numerically known and if they are linear and if they are loop body invariant, i.e. indices are accepted
is the loop increment numerically known? Is its sign known?
incr == 0 is used below as a give-up condition
When lost, try to exploit type information thanks to unsigned variables
find the real upper and lower bounds
try to add the lower bound
try to add the upper bound
pre | re |
tfb | fb |
Definition at line 711 of file loop.c.
References add_index_bound_conditions(), entity_has_values_p(), expression_and_precondition_to_integer_interval(), free_transformer(), IS_LOWER_BOUND, IS_UPPER_BOUND, negative_expression_p(), pips_debug, pips_user_error, positive_expression_p(), range_increment, range_lower, range_upper, simple_dead_loop_p(), and transformer_empty().
Referenced by add_good_loop_conditions(), comp_regions_of_implied_do(), and loop_to_transformer().
void add_intraprocedural_value_entities | ( | entity | e | ) |
Use to be static, but may be called from ri_to_transformer.
void add_intraprocedural_value_entities(entity e)
Definition at line 181 of file mappings.c.
References add_intraprocedural_value_entities_unconditionally(), entity_basic_concrete_type(), entity_has_values_p(), entity_name, pips_debug, and type_variable_p.
Referenced by add_inter_or_intraprocedural_field_entities(), add_reference_values(), and module_to_value_mappings().
transformer add_loop_index_exit_value | ( | transformer | post, |
loop | l, | ||
transformer | pre | ||
) |
The exit value is known if.
Affine increments can be handled when their signs only are known.
For instance, for increment==k: i >= ub i-k <= ub-1
Note the simplification when k==1.
But, first of all, the value of the loop index in post must be incremented. This changes its relationship with induction variables.
Most tests here are redundant because this function is only called if it has been proved that the loop was executed which implies that the upper and lower bounds are affine, that the increment is affine and that the increment sign is known.
Always returns a newly allocated value precondition on loop entrance
This part should be useless because post really is a loop postcondition. There should be no need for an index incrementation or anything. It is used to recover some of the fix-point failures:-(
In fact, it may be useful. The loop transformer and its invariant are computed without knowledge about the number of iteration, which may be zero. By adding one execution of the loop body and the index incrementation, we change b* into b+ which should add effective information.
Do not apply an extra iteration!
post = transformer_apply(t_body, post);
v_i - v_incr == v_ub, regardless of the sign
v_i - v_incr <= v_ub < v_i or: v_i - v_incr - v_ub <= 0, v_ub - v_i + 1 <= 0
v_i - v_incr >= v_ub > v_i
or:
should never happen!
post | ost |
l | postcondition of the last iteration |
pre | loop to process |
Definition at line 878 of file loop.c.
References ABS, affine_increment_to_transformer(), args_to_transformer(), CONS, ENTITY, entity_has_values_p(), entity_local_name(), entity_to_new_value(), expression_and_precondition_to_integer_interval(), ifdebug, load_statement_transformer(), loop_body, loop_index, loop_range, NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, pips_debug, print_transformer, range_increment, range_upper, TCST, transformer_affect_linear_p(), transformer_apply(), transformer_dup(), transformer_equality_add(), transformer_free(), transformer_inequality_add(), transformer_undefined, value_mappings_compatible_vector_p(), value_to_variable(), vect_add_elem(), vect_cl(), vect_new(), vect_substract(), and VECTEUR_UNDEFINED.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
transformer add_loop_skip_condition | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
tf and pre are a unique data structure when preconditions are computed
It is assumed that loop l is not entered
EXPRESSION_TO_TRANSFORMER() should be used
is the loop increment numerically known? Is its sign known?
incr == 0 is used below as a give-up condition
find the real upper and lower bounds
exchange bounds
ub < lb, i.e. ub + lb + 1 <= 0
tf | f |
pre | re |
Definition at line 495 of file loop.c.
References debug(), expression_and_precondition_to_integer_interval(), external_value_name(), ifdebug, loop_range, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_debug, print_transformer, range_increment, range_lower, range_upper, TCST, transformer_inequality_add(), user_error, value_mappings_compatible_vector_p(), vect_add_elem(), vect_fprint(), and vect_substract().
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
void add_module_call_site_precondition | ( | entity | m, |
transformer | p | ||
) |
module precondition
cons * ef = code_effects(value_code(entity_initial(m)));
p might not be printable; it may (should!) contain formal parameters of module m
keep only the interprocedural part of p that can be easily used by m; this is non optimal because symbolic constants will be lost; this is due to value mappings; new and old values should be added to the mapping using the module precondition
convert global variables in the summary precondition in the local frame as defined by value mappings (FI, 1 February 1994)
p is returned in the callee's frame; there is no need for a translation; the caller's frame should always contain the callee's frame by definition of effects;unfortunately, I do not remember why I added this translation; it was linked to a problem encountered with transformer and "invisible" variables, i.e. global variables which are indirectly changed by a procedure which does not see them; such variables receive an arbitrary existing global name; they may receive different names in different context, because there is no canonical name; each time, summary_precondition and summary_transformer are used, they must be converted in a unique frame, which can only be the frame of the current module.
FI, 9 February 1994
the former precondition represents the entire space : the new precondition must also represent the entire space BC, november 1994.
the former precondition is undefined. The new precondition is defined by the current call site precondition BC, november 1994.
Definition at line 123 of file interprocedural.c.
References DB_PUT_MEMORY_RESOURCE, dump_transformer, entity_module_p(), get_current_module_entity(), get_module_precondition(), ifdebug, load_summary_effects(), module_local_name(), pips_assert, pips_debug, precondition_intra_to_inter(), strdup(), transformer_convex_hull(), transformer_free(), transformer_identity_p(), transformer_undefined, transformer_undefined_p, and translate_global_values().
Referenced by call_to_summary_precondition().
Look for variables equivalenced with e.
e already has values associated although it may not be a canonical representative of its equivalence class...
Forget dynamic aliasing between formal parameters.
Handle intraprocedural aliasing only.
Do not handle interprocedural aliasing: this does not seem to be the right place because too many synonyms, not visible from the current procedure, are introduced (global_shared = area_layout(type_area(t));
potential canonical representative for all variables equivalenced with e
Is e intraprocedurally equivalenced/aliased with an array or a non-analyzable variable which would make e and all its aliased variables unanalyzable?
Since the equivalence is reflexive, no need to process e==eq again.
Since the equivalence is symetrical, eq may have been processed already.
this approximate test by Pierre Jouvelot should be replaced by an exact test but it does not really matter; an exact test could only be useful in presence of arrays; and in presence of arrays we do nothing here
if it's not, go ahead: it exists at least one eq such that e and eq are different, are scalars and have the same analyzable type. All eq conflicting with e meets these conditions.
Declare values for the canonical representative re
Give values to re which should have none and remove values of e. Assume that e and re are local variables.
If it is intra-procedurally equivalenced, set the synonyms as read-only variables
if eq is an integer scalar variable it does not only have a destructive effect
Variable e is equivalenced with an array or a non-integer variable and cannot be analyzed; it must be removed from the hash tables.
semantics analysis should be performed on this kind of variable but it has probably been eliminated earlier; no equivalence possible anyway!
to be dealt with later if we assume non-standard dynamic aliasing between formal parameters
readonly | eadonly |
Definition at line 204 of file mappings.c.
References add_equivalenced_values(), add_intermediate_value(), add_new_value(), add_old_value(), analyzable_scalar_entity_p(), CAR, ENDP, entities_may_conflict_p(), ENTITY, entity_has_values_p(), entity_local_name(), entity_name, entity_storage, entity_type, eq, list_undefined, pips_assert, pips_debug, pips_internal_error, pips_user_warning, POP, ram_section, ram_shared, remove_entity_values(), storage_formal_p, storage_ram, storage_ram_p, storage_return_p, storage_tag, storage_to_string(), type_area_p, type_equal_p(), and type_to_string().
Referenced by add_interprocedural_new_value_entity(), add_interprocedural_value_entities(), and add_intraprocedural_value_entities_unconditionally().
transformer affine_increment_to_transformer | ( | entity | e, |
Pvecteur | a | ||
) |
Definition at line 1269 of file expression.c.
References affine_to_transformer(), and transformer_undefined.
Referenced by add_loop_index_exit_value().
transformer affine_to_transformer | ( | entity | e, |
Pvecteur | a, | ||
bool | assignment | ||
) |
must be duplicated right now because it will be renamed and checked at the same time by value_mappings_compatible_vector_p()
assignment | ssignment |
Definition at line 1212 of file expression.c.
References CONS, contrainte_make(), CONTRAINTE_UNDEFINED, ENTITY, entity_to_new_value(), entity_to_old_value(), eq, ifdebug, make_predicate(), make_transformer(), NIL, pips_debug, sc_make(), transformer_undefined, value_mappings_compatible_vector_p(), VALUE_ONE, vect_add_elem(), vect_dump(), vect_dup(), vect_new(), vect_rm(), vect_substract(), vect_variable_rename(), and VECTEUR_NUL.
Referenced by affine_increment_to_transformer().
transformer all_data_to_precondition | ( | entity | m | ) |
any variable is included.
FI: it would be nice, if only for debugging, to pass a more restricted list...
This assumes the all variables declared in a statement is also declared at the module level.
Definition at line 536 of file ri_to_preconditions.c.
References data_to_prec_for_variables(), gen_free_list(), and module_to_all_declarations().
Referenced by initial_precondition().
transformer any_assign_operation_to_transformer | ( | entity | , |
list | , | ||
transformer | , | ||
bool | |||
) |
transformer any_assign_to_transformer | ( | list | args, |
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis in Fortran. In C, the condition can be relaxed to take into account side effects in sub-expressions.
f ou NIL ??
if some condition was not met and transformer derivation failed
args | rgs |
ef | f |
pre | re |
Definition at line 3177 of file ri_to_transformers.c.
References analyzed_reference_p(), anywhere_reference_p(), apply_additional_effects_to_transformer(), assign_rhs_to_reflhs_to_transformer(), CAR, CDR, CELL, cell_any_reference(), constant_path_analyzed_p(), cp, EXPRESSION, expression_syntax, expression_undefined, FOREACH, free_transformer(), gen_length(), ifdebug, int, NIL, pips_assert, pips_debug, print_transformer, pt_to_list_undefined_p(), reference_to_string(), reference_typed_anywhere_locations_p(), safe_expression_to_transformer(), semantics_expression_to_points_to_sources(), semantics_usable_points_to_reference_p(), syntax_call_p, syntax_reference, syntax_reference_p, syntax_subscript_p, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_undefined, and transformer_undefined_p.
Referenced by intrinsic_to_transformer(), and intrinsic_to_transformer_list().
list any_assign_to_transformer_list | ( | list | args, |
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis
if some condition was not met and transformer derivation failed
args | rgs |
ef | f |
pre | re |
Definition at line 777 of file ri_to_transformer_lists.c.
References any_scalar_assign_to_transformer(), CAR, CDR, effects_to_transformer(), ENDP, EXPRESSION, expression_syntax, ifdebug, NIL, pips_assert, pips_debug, pips_internal_error, print_transformers(), reference_indices, reference_variable, syntax_reference, syntax_reference_p, and transformer_undefined.
transformer any_basic_update_operation_to_transformer | ( | entity | tmp, |
entity | v, | ||
entity | op | ||
) |
See also any_basic_update_to_transformer(), which should be based on this function.
FI: why
tmp | mp |
op | p |
Definition at line 317 of file expression.c.
References any_assign_operation_to_transformer(), CONS, dump_transformer, entity_intrinsic(), ENTITY_POST_DECREMENT_P, ENTITY_POST_INCREMENT_P, ENTITY_PRE_INCREMENT_P, entity_to_expression(), entity_to_old_value(), EXPRESSION, expression_undefined, gen_full_free_list(), ifdebug, int_to_expression(), list_undefined, MakeBinaryCall(), NIL, pips_debug, PLUS_C_OPERATOR_NAME, transformer_add_equality(), and transformer_undefined.
Referenced by generic_unary_operation_to_transformer(), and pointer_unary_operation_to_transformer().
transformer any_basic_update_to_transformer | ( | entity | op, |
list | args, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis No more, lhs can also be dereferencing
f ou NIL ??
if some condition was not met and transformer derivation failed
op | p |
args | rgs |
ef | f |
pre | re |
Definition at line 3525 of file ri_to_transformers.c.
References analyzed_reference_p(), basic_update_reflhs_with_rhs_to_transformer(), CAR, CDR, CELL, cell_preference, cell_preference_p, cell_reference, cp, effects_to_transformer(), entity_null_locations_p(), entity_typed_nowhere_locations_p(), EXPRESSION, expression_syntax, expression_to_string(), FOREACH, free_transformer(), gen_length(), ifdebug, NIL, pips_assert, pips_debug, pips_user_error, preference_reference, print_expression(), print_transformer, pt_to_list_undefined_p(), reference_to_string(), reference_variable, semantics_expression_to_points_to_sources(), semantics_user_warning, syntax_call_p, syntax_reference, syntax_reference_p, transformer_convex_hull(), transformer_undefined, and transformer_undefined_p.
Referenced by intrinsic_to_transformer(), and intrinsic_to_transformer_list().
list any_basic_update_to_transformer_list | ( | entity | op, |
list | args, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis
if some condition was not met and transformer derivation failed
op | p |
args | rgs |
ef | f |
pre | re |
Definition at line 849 of file ri_to_transformer_lists.c.
References any_scalar_assign_to_transformer(), CAR, CDR, copy_expression(), effects_to_transformer(), ENDP, entity_intrinsic(), ENTITY_POST_INCREMENT_P, ENTITY_PRE_INCREMENT_P, EXPRESSION, expression_syntax, expression_undefined, free_expression(), ifdebug, int_to_expression(), MakeBinaryCall(), NIL, pips_assert, pips_debug, pips_internal_error, PLUS_C_OPERATOR_NAME, print_transformers(), reference_indices, reference_variable, syntax_reference, syntax_reference_p, and transformer_undefined.
transformer any_conditional_to_transformer | ( | entity | v, |
list | args, | ||
transformer | pre | ||
) |
Take care of the returned value.
About a cut-and-paste of previous function, conditional_to_transformer().
args | rgs |
pre | re |
Definition at line 5524 of file expression.c.
References CAR, CDR, condition_to_transformer(), EXPRESSION, free_transformer(), safe_any_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_range(), and transformer_undefined.
Referenced by integer_call_expression_to_transformer(), and pointer_call_expression_to_transformer().
transformer any_expression_side_effects_to_transformer | ( | expression | , |
transformer | , | ||
bool | |||
) |
transformer any_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
A set of functions to compute the transformer associated to an expression evaluated in a given context.
The choices are:
Keyword: "any" implies that the expression value is needed
Keyword: "safe" implies that effects are used and that no undefined transformer is returned.
Suggested keyword: "light"
Should basic of expression take care of this?
Assume v is a value
If we are here, it should be an enum type...
Constants, at least, could be typed coerced
Redundant with explicit type coercion also available in PIPS
To be done later
PIPS does not represent negative constants: call to unary_minus
PIPS does not represent complex constants: call to CMPLX
Only constant string are processed
The overloading is supposed to have been lifted by basic_of_expression()
enum type are analyzed like int
This function is called from the region analysis, with extended expressions such as "*", the unbounded expression.
It might be interesting to go further in case the comma operator is used
No need to link the returned value as it must be cast to the proper type.
tf may be transformer_undefined when no information is derived
expr | xpr |
pre | re |
is_internal | s_internal |
Definition at line 4993 of file expression.c.
References basic_derived, basic_derived_p, basic_float_p, basic_int_p, basic_logical_p, basic_of_expression(), basic_overloaded_p, basic_pointer_p, basic_tag, basic_to_string(), basic_typedef, basic_typedef_p, boolean_analyzed_p(), call_arguments, call_function, comma_expression_p(), copy_basic(), ENTITY_CONTINUE_P, entity_local_name(), entity_type, entity_user_name(), expression_call(), expression_call_p(), expression_syntax, expression_to_string(), expressions_to_transformer(), float_analyzed_p(), float_expression_to_transformer(), free_basic(), ifdebug, integer_analyzed_p(), integer_expression_to_transformer(), is_basic_complex, is_basic_derived, is_basic_float, is_basic_int, is_basic_logical, is_basic_overloaded, is_basic_pointer, is_basic_string, is_basic_typedef, logical_expression_to_transformer(), pips_assert, pips_debug, pips_internal_error, pointer_analyzed_p(), pointer_expression_to_transformer(), print_expression(), semantics_user_warning, string_analyzed_p(), string_expression_to_transformer(), syntax_call, transformer_identity(), transformer_undefined, transformer_undefined_p, type_enum_p, type_variable, type_variable_p, ultimate_type(), unbounded_expression_p(), and variable_basic.
Referenced by add_formal_to_actual_bindings(), any_assign_operation_to_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), assigned_expression_to_transformer(), assigned_expression_to_transformer_list(), c_data_to_prec_for_variables(), c_return_to_transformer(), expression_to_transformer(), fortran_user_call_to_transformer(), generic_abs_to_transformer(), generic_minmax_to_transformer(), loop_bound_evaluation_to_transformer(), safe_any_expression_to_transformer(), and unary_minus_operation_to_transformer().
transformer any_expressions_side_effects_to_transformer | ( | list | el, |
transformer | p, | ||
bool | is_internal | ||
) |
same as any_expression_side_effects_to_transformer() but for a list of expressions
el | l |
is_internal | s_internal |
Definition at line 4921 of file expression.c.
References any_expression_side_effects_to_transformer(), EXPRESSION, FOREACH, free_transformer(), transformer_combine(), transformer_undefined, and transformer_undefined_p.
Referenced by any_expression_side_effects_to_transformer().
transformer any_expressions_to_transformer | ( | entity | v, |
list | expl, | ||
transformer | pre | ||
) |
Compute the transformer associated to a list of expressions such as "i=0, j = 1;".
The value returned is linked to v.
To be merged with the previous function.
el is an over-appoximation; should be replaced by a safe_expression_to_transformer() taking care of computing the precise effects of exp instead of using the effects of expl.
expl | xpl |
pre | re |
Definition at line 5754 of file expression.c.
References CAR, exp, EXPRESSION, FOREACH, free_transformer(), gen_last(), safe_any_expression_to_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by integer_call_expression_to_transformer(), and pointer_call_expression_to_transformer().
transformer any_loop_to_k_transformer | ( | transformer | , |
transformer | , | ||
transformer | , | ||
statement | , | ||
list | , | ||
transformer | , | ||
int | |||
) |
loop.c
transformer any_loop_to_postcondition | ( | statement | body, |
transformer | t_init, | ||
transformer | t_enter, | ||
transformer | t_skip, | ||
transformer | t_body_star, | ||
transformer | t_body, | ||
transformer | t_next, | ||
transformer | t_inc, | ||
transformer | t_exit, | ||
transformer | pre | ||
) |
The precondition to propagate in the body is:
p_body = (t_init ; t_enter)(pre) + (t_body_star ; t_body ; t_next) (pre)
The loop postcondition to return is:
post = (t_init ; t_skip)(pre) + (t_body_star ; t_body ; t_inc ; t_exit) (pre)
To restrict the state at the beginning of the last iteration: should be part of t_body_star
Decompose the computation of p_body
Decompose the computation of post
a_post should be used because it is more accurate than direct recomputation, but we chose for the time being to recompute post entirely
Get rid of now useless transformers
body | ody |
t_init | _init |
t_enter | _enter |
t_skip | _skip |
t_body_star | _body_star |
t_body | _body |
t_next | _next |
t_inc | _inc |
t_exit | _exit |
pre | re |
Definition at line 2634 of file loop.c.
References free_transformer(), statement_to_postcondition(), transformer_apply(), transformer_convex_hull(), and transformer_undefined.
Referenced by forloop_to_postcondition(), and repeatloop_to_postcondition().
transformer any_loop_to_transformer | ( | transformer | , |
transformer | , | ||
transformer | , | ||
statement | , | ||
list | , | ||
transformer | |||
) |
transformer any_scalar_assign_to_transformer | ( | entity | v, |
expression | rhs, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
rhs | hs |
ef | f |
pre | re |
Definition at line 2832 of file ri_to_transformers.c.
References any_scalar_assign_to_transformer_without_effect(), effects_to_transformer(), and transformer_undefined_p.
Referenced by add_loop_index_initialization(), any_assign_to_transformer_list(), any_basic_update_to_transformer_list(), any_update_to_transformer_list(), assign_rhs_to_cp_to_transformer(), assign_rhs_to_reflhs_to_transformer(), basic_update_reflhs_with_rhs_to_transformer(), loop_initialization_to_transformer(), and update_reflhs_with_rhs_to_transformer().
list any_scalar_assign_to_transformer_list | ( | entity | v, |
expression | rhs, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
Is it standard compliant? The assigned variable is modified by the rhs.
Take care of aliasing
tf = transformer_value_substitute(tf, v_new, v_old);
rhs | hs |
ef | f |
pre | re |
Definition at line 709 of file ri_to_transformer_lists.c.
References any_expression_to_transformer(), dump_transformer, effects_to_transformer(), entity_has_values_p(), entity_is_argument_p(), entity_local_name(), entity_to_new_value(), entity_to_old_value(), entity_type, entity_user_name(), expression_to_string(), free(), free_transformer(), ifdebug, make_local_temporary_value_entity(), NIL, pips_debug, pips_internal_error, reset_temporary_value_counter(), semantics_user_warning, simple_equality_to_transformer(), transformer_add_modified_variable(), transformer_arguments, transformer_combine(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, transformer_value_substitute(), ultimate_type(), and value_to_variable().
transformer any_scalar_assign_to_transformer_without_effect | ( | entity | v, |
expression | rhs, | ||
transformer | pre | ||
) |
assign to the scalar variable v the expression rhs (a scalar variable has a basic type; it cannot be an array, a struct or a union; it can be an enum) WARNING : this function can return transformer_undefined
v | entity/variable to be assign |
rhs | expression/value to assign |
pre | precondition, transformer already present |
Is it standard compliant? The assigned variable is modified by the rhs.
Take care of aliasing
tf = transformer_value_substitute(tf, v_new, v_old);
rhs | hs |
pre | re |
Definition at line 2766 of file ri_to_transformers.c.
References any_expression_to_transformer(), dump_transformer, entity_has_values_p(), entity_is_argument_p(), entity_local_name(), entity_to_new_value(), entity_to_old_value(), entity_type, entity_user_name(), expression_to_string(), free(), free_transformer(), ifdebug, make_local_temporary_value_entity(), pips_debug, reset_temporary_value_counter(), semantics_user_warning, simple_equality_to_transformer(), transformer_add_modified_variable(), transformer_arguments, transformer_combine(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, transformer_value_substitute(), ultimate_type(), and value_to_variable().
Referenced by any_scalar_assign_to_transformer().
transformer any_update_to_transformer | ( | entity | op, |
list | args, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis No more, lhs can also be dereferencing
f ou NIL ??
if some condition was not met and transformer derivation failed
op | p |
args | rgs |
ef | f |
pre | re |
Definition at line 3401 of file ri_to_transformers.c.
References analyzed_reference_p(), CAR, CDR, CELL, cell_preference, cell_preference_p, cell_reference, cp, effects_to_transformer(), entity_null_locations_p(), entity_typed_nowhere_locations_p(), EXPRESSION, expression_syntax, expression_to_string(), FOREACH, free_transformer(), gen_length(), ifdebug, NIL, pips_assert, pips_debug, pips_user_error, preference_reference, print_transformer, pt_to_list_undefined_p(), reference_to_string(), reference_variable, semantics_expression_to_points_to_sources(), semantics_user_warning, syntax_call_p, syntax_reference, syntax_reference_p, transformer_convex_hull(), transformer_undefined, transformer_undefined_p, and update_reflhs_with_rhs_to_transformer().
Referenced by intrinsic_to_transformer(), and intrinsic_to_transformer_list().
list any_update_to_transformer_list | ( | entity | op, |
list | args, | ||
list | ef, | ||
transformer | pre | ||
) |
precondition
The lhs must be a scalar reference to perform an interesting analysis
if some condition was not met and transformer derivation failed
op | p |
args | rgs |
ef | f |
pre | re |
Definition at line 810 of file ri_to_transformer_lists.c.
References any_scalar_assign_to_transformer(), CAR, CDR, copy_expression(), effects_to_transformer(), ENDP, entity_to_expression(), EXPRESSION, expression_syntax, free_expression(), ifdebug, MakeBinaryCall(), NIL, pips_assert, pips_debug, pips_internal_error, print_transformers(), reference_indices, reference_variable, syntax_reference, syntax_reference_p, transformer_undefined, and update_operator_to_regular_operator().
transformer any_user_call_site_to_transformer | ( | entity | , |
list | , | ||
transformer | , | ||
list | |||
) |
transformer apply_array_effect_to_transformer | ( | transformer | , |
effect | , | ||
bool | |||
) |
transformer array_elements_substitution_in_transformer | ( | transformer | , |
entity | , | ||
type | , | ||
expression | , | ||
transformer | , | ||
list | , | ||
bool | |||
) |
transformer assign_operation_to_transformer | ( | entity | val, |
expression | lhs, | ||
expression | rhs, | ||
transformer | pre | ||
) |
Returns an undefined transformer in case of failure.
&& integer_scalar_entity_p(e)
val | al |
lhs | hs |
rhs | hs |
pre | re |
Definition at line 2737 of file expression.c.
References assigned_expression_to_transformer(), dump_transformer, entity_has_values_p(), entity_to_new_value(), expression_reference_p(), expression_syntax, ifdebug, pips_debug, reference_variable, syntax_reference, transformer_add_equality(), transformer_undefined, and transformer_undefined_p.
Referenced by float_binary_operation_to_transformer(), integer_binary_operation_to_transformer(), logical_binary_function_to_transformer(), and pointer_binary_operation_to_transformer().
transformer assigned_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre | ||
) |
transformer assigned_expression_to_transformer(entity e, expression expr, list ef): returns a transformer abstracting the effect of assignment "e = expr" when possible, transformer_undefined otherwise.
Note: it might be better to distinguish further between e and expr and to return a transformer stating that e is modified when e is accepted for semantics analysis.
if the assigned variable is also assigned by the expression as in i = (i = 2) + 1, transformer_value_substitute() cannot be used right away. The previous store must be projected out.
v must be assigned
subcase of previous aternative
vect_rm(ve);
expr | xpr |
pre | re |
Definition at line 2595 of file ri_to_transformers.c.
References any_expression_to_transformer(), entity_has_values_p(), entity_is_argument_p(), entity_to_new_value(), entity_to_old_value(), entity_type, free_transformer(), make_local_temporary_value_entity(), pips_debug, simple_equality_to_transformer(), transformer_add_value_update(), transformer_arguments, transformer_combine(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, and transformer_value_substitute().
Referenced by assign_operation_to_transformer(), integer_assign_to_transformer(), integer_assign_to_transformer_list(), loop_to_initialization_transformer(), safe_assigned_expression_to_transformer(), and safe_assigned_expression_to_transformer_list().
list assigned_expression_to_transformer_list | ( | entity | v, |
expression | expr, | ||
transformer | pre | ||
) |
transformer assigned_expression_to_transformer(entity e, expression expr, list ef): returns a transformer abstracting the effect of assignment "e = expr" when possible, transformer_undefined otherwise.
Note: it might be better to distinguish further between e and expr and to return a transformer stating that e is modified when e is accepted for semantics analysis.
if the assigned variable is also assigned by the expression as in i = (i = 2) + 1, transformer_value_substitute() cannot be used right away. The previous store must be projected out.
v must be assigned
subcase of previous aternative
vect_rm(ve);
expr | xpr |
pre | re |
Definition at line 551 of file ri_to_transformer_lists.c.
References any_expression_to_transformer(), entity_has_values_p(), entity_is_argument_p(), entity_to_new_value(), entity_to_old_value(), entity_type, free_transformer(), make_local_temporary_value_entity(), NIL, pips_debug, pips_internal_error, simple_equality_to_transformer(), transformer_add_value_update(), transformer_arguments, transformer_combine(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, and transformer_value_substitute().
transformer bitwise_xor_to_transformer | ( | entity | v, |
list | args, | ||
transformer | pre | ||
) |
returns the transformer associated to a C bitwise xor, ^, applied to two integer argument, when meaningful, and transformer_undefined otherwise.
Effects must be used at a higher level to fall back on a legal transformer.
v | is the value associated to the expression |
args | is assumed to have only one expression element of type int negated by ! |
pre | is the current precondition |
Something can be done when both arguments have values in [0,1], when both arguments have known numerical values, when both arguments have the same value,... However, all this tests imply lots time consuming projections for a limited result... Unless somebody uses XOR to flip-flop between arrays... for instance to bother Sven Verdoolaege:-). A logical not might be more useful for this:-).
The two values are know at compile time
The two values can be interpreted as booleans
Code about cut-and-pasted from logical_binary_operation_to_transformer()
The two arguments may be equal because they are the same expression and the xor is used to generate a zero or because they have the same value.
Since the difference is zero the two values are equal
args | rgs |
pre | re |
Definition at line 5619 of file expression.c.
References CAR, CDR, eq, EXPRESSION, expression_equal_p(), free_transformer(), intptr_t, make_local_temporary_integer_value_entity(), precondition_minmax_of_value(), safe_any_expression_to_transformer(), TCST, transformer_add_equality_with_integer_constant(), transformer_apply(), transformer_equality_add(), transformer_identity(), transformer_inequality_add(), transformer_intersection(), transformer_range(), transformer_undefined, transformer_undefined_p, VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by integer_call_expression_to_transformer().
transformer c_return_to_transformer | ( | entity | , |
list | , | ||
list | , | ||
transformer | |||
) |
transformer c_user_call_to_transformer | ( | entity | f, |
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
Compute the call site transformer, the bindings between formal entities and actual argments
substitute stubs and formal array elements which are passed directly or indirectly by reference if requested
Combine tf with the summary transformer
Project the former parameters and the temporary values.
Check the consistency of the transformer with the constant effects
pc | c |
pre | re |
ef | f |
Definition at line 2196 of file ri_to_transformers.c.
References any_user_call_site_to_transformer(), call_arguments, copy_transformer(), EFFECT, effect_to_constant_path_effects_with_points_to(), effects_to_constant_path_effects_with_no_pointer_information(), effects_to_transformer(), f(), FOREACH, free_call(), free_transformer(), gen_nconc(), get_bool_property(), get_current_statement_from_statement_global_stack(), list_undefined, load_summary_transformer(), make_call(), new_substitute_stubs_in_transformer(), NIL, pips_assert, pt_to_list_undefined_p(), substitute_formal_array_elements_in_transformer(), transformer_add_variables_update(), transformer_arguments, transformer_combine(), transformer_filter_subsumed_variables(), transformer_formal_parameter_projection(), transformer_temporary_value_projection(), transformer_undefined, and transformer_weak_consistency_p().
Referenced by c_user_function_call_to_transformer(), and user_call_to_transformer().
cproto-generated files
misc.c
cproto-generated files
Francois Irigoin, April 1990
Modifications:
number of "call to m" sites within the current program; they are all in m's CALLERS
I do not know yet; let's return 1 to please the semantic analysis
Definition at line 51 of file misc.c.
References entity_initial, pips_assert, user_warning, and value_code_p.
This function does everything needed.
Called by ICFG with many different contexts.
summary effects for the callee
caller preconditions
callee preconditions
load caller preconditions
first, we deal with the caller
create htable for old_values ...
add to preconditions the links to the callee formal params
transform the preconditions to make sense for the callee
translate_global_values(e_caller, call_site_prec);
Now deal with the callee
Set the htable with its variables because now we work in this frame
caller | aller |
callee | allee |
Definition at line 1051 of file interprocedural.c.
References add_formal_to_actual_bindings(), callee, db_get_memory_resource(), free_value_mappings(), load_statement_semantic(), load_summary_effects(), module_local_name(), module_to_value_mappings(), precondition_intra_to_inter(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_semantic_map(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_semantic_map(), text_for_a_transformer(), transformer_dup(), transformer_normalize(), and transformer_undefined.
void call_to_summary_precondition | ( | transformer | pre, |
call | c | ||
) |
propagate precondition pre as summary precondition of user functions
propagate precondition pre as summary precondition of user functions
user_warning("call_to_summary_precondition", "call to symbolic %s\n", entity_name(e));
pre | re |
Definition at line 989 of file interprocedural.c.
References add_formal_to_actual_bindings(), add_module_call_site_precondition(), call_arguments, call_function, entity_initial, entity_name, expressions_to_summary_precondition(), get_current_module_entity(), is_value_code, is_value_constant, is_value_intrinsic, is_value_symbolic, is_value_unknown, pips_debug, pips_internal_error, transformer_dup(), transformer_undefined, user_warning, and value_tag.
Referenced by expression_to_summary_precondition().
transformer call_to_transformer | ( | call | c, |
transformer | pre, | ||
list | ef | ||
) |
Use to be static, but may be called from expressions in C.
effects of call c
call to an external function; preliminary version: rely on effects
A temporary variable should be allocated and user_function_call_to_transformer() be used. The variable should then be projected to keep only the side effects of the call.
Add information from pre. Invariant information is easy to use. Information about initial values, that is final values in pre, can also be used.
tf = transformer_normalize(tf, 4);
pre | re |
ef | f |
Definition at line 1044 of file ri_to_transformers.c.
References analyzed_type_p(), call_arguments, call_function, call_to_expression(), effects_to_transformer(), entity_initial, entity_name, entity_type, entity_user_name(), functional_result, get_bool_property(), get_current_statement_from_statement_global_stack(), ifdebug, intrinsic_to_transformer(), is_value_code, is_value_constant, is_value_intrinsic, is_value_symbolic, is_value_unknown, make_local_temporary_value_entity(), pips_assert, pips_debug, pips_internal_error, print_entity_variable(), print_statement(), print_transformer, reset_temporary_value_counter(), SEMANTICS_INTERPROCEDURAL, semantics_user_warning, statement_global_stack_defined_p(), statement_undefined, statement_undefined_p, transformer_consistency_p(), transformer_filter_subsumed_variables(), transformer_identity(), transformer_normalize(), transformer_safe_domain_intersection(), transformer_temporary_value_projection(), transformer_undefined, type_functional, type_void_p, ultimate_type(), user_call_to_transformer(), user_function_call_to_transformer(), and value_tag.
Referenced by expression_to_transformer(), instruction_to_transformer(), and instruction_to_transformer_list().
number of modules calling m within the current program; i.e. number of modules containing at least one call site to m
I do not know yet; let's return 1 to please the semantic analysis
Definition at line 63 of file misc.c.
References entity_initial, pips_assert, user_warning, and value_code_p.
bool check_condition_wrt_precondition | ( | expression | c, |
transformer | pre, | ||
bool | check_true | ||
) |
Check that is is always false in a store s such that p(s)
pre | re |
check_true | heck_true |
Definition at line 294 of file utils.c.
References bool_to_string(), pips_debug, transformer_add_condition_information(), transformer_dup(), and transformer_empty_p().
Referenced by condition_false_wrt_precondition_p(), and condition_true_wrt_precondition_p().
bool check_range_wrt_precondition | ( | range | r, |
transformer | p, | ||
bool | check_empty | ||
) |
FI: this function is outdated because it does not compute the transformers for the range expressions, because it does not take side effects into account and ...
We might need a range_to_transformer() or loop_range_to_transformer() instead and check that its range is empty.
gather information about the increment sign
Try to prove that no iterations are performed
Without information about the increment sign, you cannot make a decision. Should we accept increments greater or equal to zero? Lesser or equal to zero?
Try to prove that at least one iteration is performed
Without information about the increment sign, you cannot make a decision. Should we accept increments greater or equal to zero? Lesser or equal to zero?
No decision has been made yet
a numerical range may be empty although no information is available
s = sc_strong_normalize4(s, (char * (*)(Variable)) entity_local_name);
= sc_elim_redund(s);
check_empty | heck_empty |
Definition at line 135 of file utils.c.
References bool_to_string(), contrainte_make(), CONTRAINTE_UNDEFINED, debug(), dump_value_name(), entity_local_name(), expression_and_precondition_to_integer_interval(), ifdebug, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, normalized_undefined_p, pips_debug, predicate_system, range_increment, range_lower, range_upper, sc_dup(), sc_fprint(), sc_inequality_add(), sc_make(), sc_rm(), sc_strong_normalize5(), TCST, transformer_relation, transformer_undefined_p, user_error, vect_add_elem(), vect_dup(), and vect_substract().
Referenced by empty_range_wrt_precondition_p(), and non_empty_range_wrt_precondition_p().
transformer complete_any_loop_transformer | ( | transformer | , |
transformer | , | ||
transformer | , | ||
transformer | , | ||
transformer | , | ||
transformer | , | ||
transformer | , | ||
transformer | |||
) |
list complete_any_loop_transformer_list | ( | transformer | t_init, |
transformer | t_skip, | ||
transformer | t_body_star, | ||
transformer | t_body, | ||
transformer | t_inc, | ||
transformer | t_exit | ||
) |
FI: used to be complete_any_loop_transformer() with a direct reduction by convex hull.
t_loop = t_init ; t_skip + t_bodystar ; t_body ; t_inc; t_exit
Before entering t_body, t_enter or t_next have been applied which let us restrict the set of state modified by t_body. But this information should already been included in t_body_star.
Several cases must be tested:
These cases are checked with complete01.c, complete02.c,... complete05.c
loop skipped transformer
add loop entered transformer/condition: should already be in t_body_star
combine both cases in a transformer list
t_init | _init |
t_skip | _skip |
t_body_star | _body_star |
t_body | _body |
t_inc | _inc |
t_exit | _exit |
Definition at line 1578 of file loop.c.
References copy_transformer(), fprintf(), ifdebug, NIL, print_transformer, print_transformers(), transformer_combine(), transformer_normalize(), and two_transformers_to_list().
Referenced by complete_any_loop_transformer(), and new_complete_whileloop_transformer_list().
transformer complete_forloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
forloop | fl | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
t_body_star | _body_star |
pre | re |
fl | l |
Definition at line 1686 of file loop.c.
References complete_any_loop_transformer(), complete_statement_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), load_statement_transformer(), safe_expression_to_transformer(), transformer_apply(), and transformer_undefined.
Referenced by generic_complete_statement_transformer().
list complete_forloop_transformer_list | ( | transformer | t_body_star, |
transformer | pre, | ||
forloop | fl | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Make sure you have the effective statement transformer: it is not stored for loops and this is key for nested loops.
t_body_star | _body_star |
pre | re |
fl | l |
Definition at line 1732 of file loop.c.
References complete_any_loop_transformer(), complete_statement_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), list_undefined, load_statement_transformer(), pips_internal_error, safe_expression_to_transformer(), transformer_apply(), and transformer_undefined.
Referenced by instruction_to_transformer_list().
transformer complete_loop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
loop | l | ||
) |
The transformer computed and stored for a loop is useful to compute the loop body precondition, but it is not useful to analyze a higher level construct, which need the loop transformer with the exit condition.
Only Fortran DO loops are handled here. The need for nested WHILE loops has not been identified yet. The index variable is always initialized and then the loop is either entered and exited or not entered
loop body transformer
compute the loop body transformer
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
compute the loop body precondition
You do not need a range to recurse. A full precondition with arguments is expected by complete_loop_transformer(). Maybe, but it's much easier to debug with ranges as they only carry the useful information. And the result is correct for Semantics-New/for03.c and 04.c
The final index incrementation is performed later by add_loop_index_exit_value()
btf = transformer_add_loop_index_incrementation(btf, l, pre);
compute the transformer when the loop is entered: T o T*
Semantics-New/for04.c: this leads to t_enter == empty_transformer because the same conditions on the initial values of cpi and cpj are preserved in both ltf, which is OK, and btf, which is not OK.
add the entry condition
but it seems to be in t already
t_enter = transformer_add_loop_index_initialization(t_enter, l);
It would make sense to apply the incrementation, but this is performed as a side effect by add_loop_index_exit_value(), which avoids unfeasability wrt the final loop bound.
add the exit condition, without any information pre to estimate the increment
FI: oops, pre is used in spite of previous comment
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
pre cannot be used as such. the loop initialization must be applied first: the previous comment seems to be correct.
ltf | tf |
pre | re |
Definition at line 1927 of file loop.c.
References add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), empty_range_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, load_statement_transformer(), loop_body, loop_range, non_empty_range_wrt_precondition_p(), pips_debug, print_transformer, statement_instruction, statement_loop_p(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by complete_loop_transformer_list(), generic_complete_statement_transformer(), and old_complete_whileloop_transformer().
list complete_loop_transformer_list | ( | transformer | ltf, |
transformer | pre, | ||
loop | l | ||
) |
loop body transformer
compute the loop body transformer
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
compute the loop body precondition
You do not need a range to recurse. A full precondition with arguments is expected by complete_loop_transformer().
The final index incrementation is performed later by add_loop_index_exit_value()
btf = transformer_add_loop_index_incrementation(btf, l, pre);
compute the transformer when the loop is entered: T o T*
add the entry condition
but it seems to be in t already
t_enter = transformer_add_loop_index_initialization(t_enter, l);
It would make sense to apply the incrementation, but this is performed as a side effect by add_loop_index_exit_value(), which avoids unfeasability wrt the final loop bound.
add the exit condition, without any information pre to estimate the increment
FI: oops, pre is used in spite of previous comment
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
ltf | tf |
pre | re |
Definition at line 2061 of file loop.c.
References add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), complete_loop_transformer(), empty_range_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, list_undefined, load_statement_transformer(), loop_body, loop_range, non_empty_range_wrt_precondition_p(), pips_debug, pips_internal_error, print_transformer, statement_instruction, statement_loop_p(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), transformer_identity(), transformer_normalize(), transformer_undefined, and transformer_undefined_p.
Referenced by instruction_to_transformer_list().
transformer complete_non_identity_statement_transformer | ( | transformer | t, |
transformer | pre, | ||
statement | s | ||
) |
FI: only implemented for while loops.
pre | re |
Definition at line 3685 of file ri_to_transformers.c.
References generic_complete_statement_transformer().
transformer complete_repeatloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
whileloop | wl | ||
) |
t_body_star | _body_star |
pre | re |
wl | l |
Definition at line 1910 of file loop.c.
References complete_repeatloop_transformer_list(), and transformer_list_to_transformer().
Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().
list complete_repeatloop_transformer_list | ( | transformer | , |
transformer | , | ||
whileloop | |||
) |
transformer complete_statement_transformer | ( | transformer | t, |
transformer | pre, | ||
statement | s | ||
) |
Returns the effective transformer ct for a given statement s.
t is the stored transformer. For loops, t is useful to compute the body preconditions but not to compute the loop postcondition. ct can be used to compute the statement s postcondition, no matter what kind of statement s is, and to compute the transformer of a higher-level statement enclosing s.
In other words, load_statement_transformer(s) does not always return a transformer which can be composed with another transformer or applied to a precondition. But statement_to_transformer() always returns such a transformer.
Always allocates a new transformer. This probably creates a memory leak when going up the internal representation because it was originally assumed that the transformer returned recursively was also the transformer stored at a lower level. This is changed because this function calls itself recursively. So now statement_to_transformer() returns a transformer which is not the transformer stored for the statement.
pre | re |
Definition at line 3677 of file ri_to_transformers.c.
References generic_complete_statement_transformer().
Referenced by complete_forloop_transformer(), complete_forloop_transformer_list(), complete_repeatloop_transformer_list(), load_completed_statement_transformer(), new_complete_whileloop_transformer_list(), repeatloop_to_postcondition(), statement_to_transformer(), and whileloop_to_postcondition().
transformer complete_whileloop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | wl | ||
) |
FI: I'm not sure this function is useful.
ltf | tf |
pre | re |
wl | l |
Definition at line 2183 of file loop.c.
References complete_repeatloop_transformer(), evaluation_before_p, new_complete_whileloop_transformer(), transformer_undefined, and whileloop_evaluation.
Referenced by old_complete_whileloop_transformer().
list complete_whileloop_transformer_list | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | wl | ||
) |
ltf | tf |
pre | re |
wl | l |
Definition at line 2198 of file loop.c.
References complete_repeatloop_transformer_list(), evaluation_before_p, new_complete_whileloop_transformer_list(), NIL, and whileloop_evaluation.
Referenced by instruction_to_transformer_list().
transformer compute_path_transformer | ( | statement | , |
path | , | ||
path | |||
) |
statement_mapping compute_postcondition | ( | statement | stat, |
statement_mapping | post_map, | ||
statement_mapping | pre_map | ||
) |
statement_mapping compute_postcondition(stat, post_map, pre_map) statement stat; statement_mapping post_map, pre_map;
computes the postcondition mapping post_map from the precondition mapping pre_map and the related statement tree starting from stat. The rule applied is that the postcondition of one statement is the precondition of the following one. The last postcondition is arbitrary set to transformer_identity, what is not enough. (??? should I take the stat transformer?)
the initial postcondition is empty ???
Top-down definition
stat | tat |
post_map | ost_map |
pre_map | re_map |
Definition at line 186 of file postcondition.c.
References current_postcondition_map, current_precondition_map, debug_off, debug_on, gen_null(), gen_recurse, hash_table_undefined, pips_debug, postcondition_filter(), statement_domain, StorePost, and transformer_identity().
Referenced by set_resources_for_module().
bool condition_false_wrt_precondition_p | ( | expression | c, |
transformer | p | ||
) |
Definition at line 285 of file utils.c.
References check_condition_wrt_precondition().
Referenced by old_complete_whileloop_transformer(), and standard_whileloop_to_transformer().
transformer condition_to_transformer | ( | expression | cond, |
transformer | pre, | ||
bool | veracity | ||
) |
To capture side effects and to add C twist for numerical conditions.
Argument pre may be undefined.
Beware of tricky conditions using the comma or the conditional operator, although they should be handled as the default case, using effects.
upwards should be set to false when computing preconditions (but we have no way to know) or when computing tramsformers in context. And set to true in other cases. upwards is a way to gain execution time at the expense of precision. This speed/accuracy tradeoff has evolved with CPU technology.
If a comma operator is used, the test is the last expression
FI: quid of a conditional operator? e.g. "x>0?1<m:1<n"
FI: quid of assignment operator? e.g. "i = j = k = 1"
FI: we probably need a function tcond = expression_to_condition(cond)
C comparison operators return an integer value
FI: not good when side effects in cond
In case, there are side-effects in the condition. This is very unlikely for standard code and should be simplified with a test to transformer_identity_p(tf)
Make sure you can handle this kind of variable.
This test is added for Semantics-New/transformer01.c which tests a pointer. The underlying bug may still be there when pointers are analyzed by PIPS.
tmpv != 0
tmpv==0
Not yet? We may be in a = c? x : y; or in e1, e2,...; Does it matter?
May be dangerous if this routine is called internally to another routine using temporary variables...
reset_temporary_value_counter();
cond | ond |
pre | re |
veracity | eracity |
Definition at line 5348 of file expression.c.
References analyzed_basic_p(), basic_logical_p, basic_of_expression(), call_arguments, call_function, CAR, cast_expression, copy_transformer(), dump_transformer, effects_to_transformer(), ENTITY_COMMA_P, ENTITY_LOGICAL_OPERATOR_P, EXPRESSION, expression_call_p(), expression_cast(), expression_cast_p(), expression_syntax, expression_to_proper_constant_path_effects(), fprintf(), free_basic(), free_transformer(), gen_full_free_list(), gen_last(), ifdebug, make_local_temporary_value_entity_with_basic(), safe_any_expression_to_transformer(), safe_expression_to_transformer(), syntax_call, transformer_add_condition_information_updown(), transformer_add_sign_information(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_temporary_value_projection(), transformer_undefined, and transformer_undefined_p.
Referenced by any_conditional_to_transformer(), complete_forloop_transformer(), complete_forloop_transformer_list(), complete_repeatloop_transformer_list(), conditional_to_transformer(), forloop_to_postcondition(), forloop_to_transformer(), intrinsic_to_transformer(), intrinsic_to_transformer_list(), new_complete_whileloop_transformer_list(), new_whileloop_to_k_transformer(), new_whileloop_to_transformer(), repeatloop_to_postcondition(), repeatloop_to_transformer(), simplify_boolean_expression_with_precondition(), test_to_postcondition(), test_to_transformer(), test_to_transformer_list(), and whileloop_to_postcondition().
bool condition_true_wrt_precondition_p | ( | expression | c, |
transformer | p | ||
) |
A condition cannot be tested exactly wrt a precondition You can try to prove that it is always true (because it is never false) or you can try to prove that it is always false (because it is never true).
In both case, you may fail and be unable to decide emptiness or non-emptiness.
Definition at line 276 of file utils.c.
References check_condition_wrt_precondition(), and empty.
Referenced by old_complete_whileloop_transformer().
transformer conditional_to_transformer | ( | expression | cond, |
expression | te, | ||
expression | fe, | ||
transformer | pre, | ||
list | ef | ||
) |
FI: not too smart to start with the special case with no value returned, just side-effects...
cond | ond |
te | e |
fe | e |
pre | re |
ef | f |
Definition at line 5488 of file expression.c.
References condition_to_transformer(), effects_to_transformer(), free_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by intrinsic_to_transformer(), and intrinsic_to_transformer_list().
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.
transformer cycle_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p | ||
) |
Compute transformers or preconditions.
partition | artition |
ndu | du |
ancestor_map | ncestor_map |
scc_map | cc_map |
fix_point_map | ix_point_map |
e_pre | _pre |
n_pre | _pre |
control_postcondition_map | ontrol_postcondition_map |
postcondition_p | ostcondition_p |
Definition at line 1744 of file unstructured.c.
References dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), and transformer_undefined.
Referenced by process_ready_node().
transformer dag_or_cycle_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p, | ||
bool | is_dag | ||
) |
Should ndu be a dag or a cycle?
forward reachable nodes in u
The whole business could be simplified by using a larger definition of "to_be_processed".
wide_forward_control_map_get_blocs(unstructured_control(u), &to_be_processed);
Take care of unreachable nodes
FI: Wouldn't it be better to clean up the unstructured? Aren't they supposed to be clean? This piece of code contradict get_control_precondition() where the problem could be fixed at a lower cost. Another place where the problem is handled is ready_to_be_processed_p(), but it is called on still_to_be_processed, which does not take into account unreachable nodes. To make things worse, the daVinci printouts only include, most of the time, only reachable nodes.
Take care of the entry node
The entry node must be handled in a specific way... but not in the specific way implemented in process_ready_node() which only deals with DAG's. The entry node cannot be a meaningless control node.
Since control nodes have been replicated, it is difficult to predict if es has already been processed or not.
make_control_postcondition_map();
Take care of the forward reachable control nodes
process forward
right away because c's cdr might be modified
Compute fix point transformer for cycle
Compute the convex hull of the paths associated to each predecessor of the entry. Since this is a cycle, preds cannot be empty.
transformer fp_tf_plus = transformer_undefined;
If an entry range is known, do not use it as there may be more than one occurence of the cycle and more than one entry range. Keep this refinement to the precondition computation phase? It might be too late. The the data structure should be change to store more than one fix point per cycle.
Not convincing anyway: you should apply fp_tf_plus to e_pre for the next two lines to make sense.
Use the + fix point to preserve more information about the output and do not forget to perform a convex hull when you need a * fix point in process_ready_node()
Instead of computing the convex hull over all paths before computing the fix point, compute the fix point of a list of transformers.
e may have many synonyms
fix point are unique for all replication of a cycle
each cycle replication has its own fix-point
We might want to return the corresponding fix point?
partition | artition |
ndu | du |
ancestor_map | ncestor_map |
scc_map | cc_map |
fix_point_map | ix_point_map |
e_pre | _pre |
n_pre | _pre |
control_postcondition_map | ontrol_postcondition_map |
postcondition_p | ostcondition_p |
is_dag | s_dag |
Definition at line 1509 of file unstructured.c.
References CAR, CONS, CONTROL, control_map_get_blocs(), control_predecessors, control_statement, control_to_ancestor(), control_undefined, count, ENDP, FOREACH, forward_control_map_get_blocs(), free_transformer(), gen_append(), gen_copy_seq(), gen_free_list(), gen_list_and_not(), gen_remove(), get_bool_property(), ifdebug, init, list_undefined, list_undefined_p, load_arc_precondition(), load_statement_transformer(), MAP, meaningless_control_p(), NIL, pips_assert, pips_debug, POP, print_control_node_unss_sem(), print_transformer, process_ready_node(), ready_to_be_processed_p(), statement_identification(), statement_to_transformer(), store_control_fix_point(), store_control_postcondition(), TRANSFORMER, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_list_transitive_closure_plus(), transformer_undefined, transformer_undefined_p, and unstructured_control.
Referenced by cycle_to_flow_sensitive_postconditions_or_transformers(), and dag_to_flow_sensitive_postconditions_or_transformers().
transformer dag_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p | ||
) |
Compute transformers or preconditions.
partition | artition |
ndu | du |
ancestor_map | ncestor_map |
scc_map | cc_map |
fix_point_map | ix_point_map |
e_pre | _pre |
n_pre | _pre |
control_postcondition_map | ontrol_postcondition_map |
postcondition_p | ostcondition_p |
Definition at line 1724 of file unstructured.c.
References dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), and transformer_undefined.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
transformer data_to_precondition | ( | entity | m | ) |
restricted to variables with effects.
Definition at line 526 of file ri_to_preconditions.c.
References data_to_prec_for_variables(), effects_to_entity_list(), gen_free_list(), and load_module_intraprocedural_effects().
Referenced by generic_module_name_to_transformers().
transformer declaration_to_transformer | ( | entity | v, |
transformer | pre | ||
) |
Note: initializations of static variables are not used as transformers but to initialize the program precondition.
It is not assumed that entity_has_values_p(v)==TRUE A write effect on the declared variable is assumed as required by Beatrice Creusillet for region computation.
if(place_holder_variable_p(v)) {
tf = transformer_identity();
}
FI: the initialization expression might have relevant side-effects? This could ba handled by generalizing variable_to_initial_expression() and by returning expression_undefined incase of failure instead of aborting.
Use the dimension expressions and the initial value
add type information because it will not be done later since declarations with no initialization lead to an identity transformer
pre | re |
Definition at line 580 of file ri_to_transformers.c.
References dimensions_to_transformer(), entity_has_values_p(), entity_name, expression_undefined_p, free_expression(), free_transformer(), get_bool_property(), ifdebug, pips_assert, pips_debug, print_transformer, safe_assigned_expression_to_transformer(), transformer_add_variable_type_information(), transformer_apply(), transformer_combine(), transformer_identity(), transformer_range(), transformer_undefined, transformer_undefined_p, variable_initial_expression(), and variable_static_p().
Referenced by declarations_to_transformer(), declarations_to_transformer_list(), and propagate_preconditions_in_declarations().
list declaration_to_transformer_list | ( | entity | v, |
transformer | pre | ||
) |
This development was prompted by the last example found in the paper by Schrammel and Jeannet at NSAD 2010. See test cases schrammel04, 05 and 06. The minimal goal is to avoid the indentity transformer when performing the convex hull of several transformers.
This could also be useful to automatize the handling of tests within a loop using the technique presented at NSAD 2010 by Ancourt & al. The control structure
"while(c) if(t) T; else F;"
is replaced by
"while(c) {while(c&&t) T; while(c&& !t) F;}".
This replacement could be performed on the equations instead of requiring a program transformation. semantical analysis
phasis 3: compute transformer lists from statements and statement transformers
For refined precondition analysis. Keep track of all control paths within sequences
Francois Irigoin, September 2010 include <stdlib.h> Note: initializations of static variables are not used as transformers but to initialize the program precondition. It is not assumed that entity_has_values_p(v)==true A write effect on the declared variable is assumed as required by Beatrice Creusillet for region computation.
FI: the initialization expression might have relevant side-effects? This could ba handled by generalizing variable_to_initial_expression() and by returning expression_undefined incase of failure instead of aborting.
Use the dimension expressions and the initial value
FI: I preserve the code below in case I have problems with integer typing in the future
pre | re |
Definition at line 100 of file ri_to_transformer_lists.c.
References dimensions_to_transformer(), entity_has_values_p(), entity_name, free_expression(), get_bool_property(), ifdebug, NIL, pips_assert, pips_debug, pips_internal_error, print_transformers(), safe_assigned_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), transformer_range(), transformer_undefined, transformer_undefined_p, variable_initial_expression(), and variable_static_p().
transformer declarations_to_transformer | ( | list | dl, |
transformer | pre | ||
) |
For C declarations.
Very close to a block_to_transformer() as declarations can be seen as a sequence of assignments.
Note: initialization of static variables are not taken into account. They must be used for summary preconditions.
post = transformer_safe_normalize(post, 4);
post = transformer_safe_normalize(post, 4);
btf = transformer_normalize(btf, 4);
dl | l |
pre | re |
Definition at line 649 of file ri_to_transformers.c.
References CAR, declaration_to_transformer(), ENDP, ENTITY, entity_undefined, free_transformer(), ifdebug, pips_assert, pips_debug, POP, stf(), transformer_combine(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_safe_apply(), transformer_safe_normalize(), transformer_undefined, and transformer_undefined_p.
Referenced by statement_to_postcondition(), statement_to_transformer(), and statement_to_transformer_list().
list declarations_to_transformer_list | ( | list | dl, |
transformer | pre | ||
) |
For C declarations.
Very close to a block_to_transformer() as declarations can be seen as a sequence of assignments.
Note: initialization of static variables are not taken into account. They must be used for summary preconditions.
post = transformer_safe_normalize(post, 4);
post = transformer_safe_normalize(post, 4);
btf = transformer_normalize(btf, 4);
dl | l |
pre | re |
Definition at line 212 of file ri_to_transformer_lists.c.
References CAR, declaration_to_transformer(), ENDP, ENTITY, entity_undefined, free_transformer(), ifdebug, list_undefined, pips_assert, pips_debug, pips_internal_error, POP, stf(), transformer_combine(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_safe_apply(), transformer_safe_normalize(), transformer_undefined, and transformer_undefined_p.
void delete_statement_postcondition | ( | statement | ) |
void delete_statement_precondition | ( | statement | ) |
void delete_statement_semantic | ( | statement | ) |
void delete_statement_total_precondition | ( | statement | ) |
void delete_statement_transformer | ( | statement | ) |
transformer dimensions_to_transformer | ( | entity | v, |
transformer | pre | ||
) |
Assumes that entity_has_values_p(v) holds.
FI: this should be done for all variables, regardless of their types.
pre | re |
Definition at line 535 of file ri_to_transformers.c.
References copy_transformer(), DIMENSION, dimension_lower, dimension_upper, ENDP, entity_basic_concrete_type(), FOREACH, free_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), transformer_range(), type_variable, type_variable_p, and variable_dimensions.
Referenced by declaration_to_transformer(), and declaration_to_transformer_list().
number of call to m during the current program execution; return 0 if m is never called, either because it's a call graph root or because it was linked by mistake; return -1 if the dynamic call count is unknow, for instance because one of m's call site is located in a loop of unknown bounds; return k when it can be evaluated
I do not know yet; let's return 1 to please the semantic analysis
Definition at line 75 of file misc.c.
References entity_initial, pips_assert, pips_internal_error, and value_code_p.
Build the list of values to be projected when the declaration list list_mod is no longer valid because a block is closed/left.
Values for static variables are preserved. Values for heap variables also, in case their values are computed in the future...
This may not be the best algorithm when locations are used because the list of locations may be much longer, especially for arrays, than the list of values appearing in the transformer.
list_mod | ist_mod |
Definition at line 1007 of file mappings.c.
References CONS, ENTITY, entity_has_values_p(), entity_to_new_value(), entity_to_old_value(), FOREACH, NIL, variable_dynamic_p(), and variable_stack_p().
Referenced by statement_to_transformer(), and statement_to_transformer_list().
list of effects
algorithm: keep only write effects on scalar variable with values
fx | x |
Definition at line 798 of file ri_to_transformers.c.
References action_write_p, arguments_add_entity(), EFFECT, effect_action, effect_any_reference, entity_has_values_p(), FOREACH, NIL, and reference_variable.
returns an allocated list of entities that appear in lef.
an entity may appear several times.
lef | ef |
Definition at line 516 of file ri_to_preconditions.c.
References CONS, EFFECT, effect_any_reference, ENTITY, gen_nreverse(), MAP, NIL, and reference_variable.
Referenced by data_to_precondition().
transformer effects_to_transformer | ( | list | e | ) |
list of effects
Definition at line 474 of file ri_to_transformers.c.
References apply_effects_to_transformer(), expression_undefined, and transformer_identity().
Referenced by add_good_loop_conditions(), add_loop_index_initialization(), any_assign_to_transformer_list(), any_basic_update_to_transformer(), any_basic_update_to_transformer_list(), any_loop_to_k_transformer(), any_scalar_assign_to_transformer(), any_scalar_assign_to_transformer_list(), any_update_to_transformer(), any_update_to_transformer_list(), any_user_call_site_to_transformer(), c_return_to_transformer(), c_user_call_to_transformer(), c_user_function_call_to_transformer(), call_to_transformer(), condition_to_transformer(), conditional_to_transformer(), expression_effects_to_transformer(), expression_to_transformer(), fortran_user_call_to_transformer(), integer_assign_to_transformer(), integer_assign_to_transformer_list(), intrinsic_to_transformer(), intrinsic_to_transformer_list(), load_summary_transformer(), loop_to_transformer(), new_loop_to_transformer(), process_ready_node(), safe_any_expression_to_transformer(), standard_whileloop_to_transformer(), test_to_transformer(), test_to_transformer_list(), unstructured_to_transformer(), and user_call_to_transformer().
bool empty_range_wrt_precondition_p | ( | range | r, |
transformer | p | ||
) |
A range cannot be tested exactly wrt a precondition You can try to prove that it is empty or you can try to prove that it is not empty.
In both case, you may fail and be unable to decide emptiness or non-emptiness.
Definition at line 112 of file utils.c.
References check_range_wrt_precondition(), and empty.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
bool eval_condition_wrt_precondition_p | ( | expression | c, |
transformer | pre, | ||
bool | veracity | ||
) |
pre | re |
veracity | eracity |
Definition at line 5909 of file expression.c.
References f(), precondition_add_condition_information(), transformer_dup(), and transformer_empty_p().
Referenced by false_condition_wrt_precondition_p(), and true_condition_wrt_precondition_p().
void expression_and_precondition_to_integer_interval | ( | expression | e, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Evaluate expression e in context p, assuming that e is an integer expression.
If p is empty, return an empty interval.
Could be more general, I'm lazy (FI).
precondition p is not feasible
OK, we could do something: add a pseudo-variable equal to expression e and check its min abd max values
we are not handling an affine integer expression
plb | lb |
pub | ub |
Definition at line 325 of file utils.c.
References CONTRAINTE_UNDEFINED, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), TCST, transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, VALUE_ZERO, vect_coeff(), vect_constant_p(), vect_size(), VECTEUR_NUL_P, and vecteur_var.
Referenced by add_index_range_conditions(), add_loop_index_exit_value(), add_loop_skip_condition(), check_range_wrt_precondition(), loop_basic_workchunk_to_workchunk(), loop_bound_evaluation_to_transformer(), and modulo_to_transformer().
transformer expression_effects_to_transformer | ( | expression | expr | ) |
expr | xpr |
Definition at line 3465 of file expression.c.
References effects_to_transformer(), expression_to_proper_constant_path_effects(), and gen_full_free_list().
Referenced by integer_expression_to_transformer(), safe_any_expression_side_effects_to_transformer(), safe_assigned_expression_to_transformer(), safe_integer_expression_to_transformer(), transformer_add_call_condition_information_updown(), and transformer_add_condition_information_updown().
void expression_to_summary_precondition | ( | transformer | pre, |
expression | e | ||
) |
pre | re |
Definition at line 977 of file interprocedural.c.
References call_to_summary_precondition(), expression_syntax, syntax_call, and syntax_call_p.
Referenced by expressions_to_summary_precondition().
transformer expression_to_transformer | ( | expression | exp, |
transformer | pre, | ||
list | el | ||
) |
Just to capture side effects as the returned value is ignored.
Example: "(void) inc(&i);".
Or to capture the return of a struct, which cannot be expressed with an atomic return value.
FI: I assume this implies a cast to (void) but I'm wrong for any call to a void function.
FI: I do not remember the meaning of the last parameter
Must be a call to a void function
Wait till it happpens...
FI: is_internal_p has an impact on renaming in simple_affine_to_transformer().
FI: there may be (many) other exceptions with intrinsics...
Fortran intrinsics, such as IOs, are not taken into account because these code should not be executed for Fortran code.
If everything else has failed.
exp | xp |
pre | re |
el | l |
Definition at line 5190 of file expression.c.
References analyzed_type_p(), any_expression_to_transformer(), application_arguments, application_function, base, call_arguments, call_function, call_to_transformer(), CAR, cast_expression, compute_basic_concrete_type(), effects_to_transformer(), ENTITY_FIELD_P, entity_module_p(), ENTITY_POINT_TO_P, entity_undefined, exp, EXPRESSION, expression_application(), expression_application_p(), expression_call(), expression_call_p(), expression_cast(), expression_cast_p(), expression_reference(), expression_reference_p(), expression_sizeofexpression(), expression_sizeofexpression_p(), expression_subscript(), expression_subscript_p(), expression_syntax, expression_to_proper_constant_path_effects(), expression_to_type(), expressions_to_transformer(), f(), free_transformer(), free_type(), generic_reference_to_transformer(), make_local_temporary_value_entity(), pips_internal_error, safe_expression_to_transformer(), sizeofexpression_expression, sizeofexpression_expression_p, subscript_array, subscript_indices, syntax_call, syntax_call_p, syntax_cast, syntax_cast_p, transformer_combine(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, type_void_p, and user_call_to_transformer().
Referenced by expression_to_postcondition(), instruction_to_transformer(), and safe_expression_to_transformer().
void expressions_to_summary_precondition | ( | transformer | pre, |
list | le | ||
) |
pre | re |
le | e |
Definition at line 966 of file interprocedural.c.
References CAR, EXPRESSION, expression_to_summary_precondition(), and MAPL.
Referenced by call_to_summary_precondition().
transformer expressions_to_transformer | ( | list | expl, |
transformer | pre | ||
) |
Compute the transformer associated to a list of expressions such as "i=0, j = 1;".
The value returned is ignored.
el is an over-appoximation; should be replaced by a safe_expression_to_transformer() taking care of computing the precise effects of exp instead of using the effects of expl.
expl | xpl |
pre | re |
Definition at line 5722 of file expression.c.
References copy_transformer(), exp, EXPRESSION, FOREACH, free_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by any_expression_side_effects_to_transformer(), any_expression_to_transformer(), expression_to_transformer(), generic_reference_to_transformer(), intrinsic_to_transformer(), and intrinsic_to_transformer_list().
bool false_condition_wrt_precondition_p | ( | expression | c, |
transformer | pre | ||
) |
pre | re |
Definition at line 5891 of file expression.c.
References eval_condition_wrt_precondition_p().
Referenced by whileloop_to_postcondition(), and whileloop_to_total_precondition().
transformer filter_transformer | ( | transformer | t, |
list | e | ||
) |
Previous version of effects_to_transformer() transformer effects_to_transformer(list e) { list args = NIL; Pbase b = VECTEUR_NUL; Psysteme s = sc_new();.
s->base = b; s->dimension = vect_size(b);
return make_transformer(args, make_predicate(s)); }
algorithm: keep only information about scalar variables with values appearing in effects e and store it into a newly allocated transformer
action a = effect_action(ef);
I do not know yet if I should keep old values...
FI: I should check if sc is sc_empty but I haven't (yet) found a cheap syntactic test
Definition at line 495 of file ri_to_transformers.c.
References arguments_add_entity(), EFFECT, effect_any_reference, entity_has_values_p(), entity_is_argument_p(), entity_to_new_value(), FOREACH, make_predicate(), make_transformer(), NIL, predicate_system, reference_variable, sc_restricted_to_variables_transitive_closure(), transformer_arguments, transformer_relation, vect_add_variable(), and VECTEUR_NUL.
Referenced by semantic_to_text().
transformer float_expression_to_transformer | ( | entity | v, |
expression | rhs, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
pre can be used if some integer variables with constant values have to be promoted to float.
pips_assert("Precondition is undefined", transformer_undefined_p(pre));
rhs | hs |
pre | re |
is_internal | s_internal |
Definition at line 4153 of file expression.c.
References expression_syntax, float_call_expression_to_transformer(), generic_reference_to_transformer(), is_syntax_call, is_syntax_range, is_syntax_reference, pips_internal_error, syntax_reference, syntax_tag, and transformer_undefined.
Referenced by any_expression_to_transformer().
transformer forloop_to_postcondition | ( | transformer | pre, |
forloop | fl, | ||
transformer | t_body_star | ||
) |
This function does not seem to exist because we only used statement effects in the past and because those are stored in the database.
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
An effort could be made to compute the precondition for t_inc
Clean up memory
pre | re |
fl | l |
t_body_star | _body_star |
Definition at line 2707 of file loop.c.
References any_loop_to_postcondition(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), load_statement_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_dup(), and transformer_undefined.
Referenced by instruction_to_postcondition().
transformer forloop_to_transformer | ( | forloop | fl, |
transformer | pre, | ||
list | flel | ||
) |
effects of forloop fl
t_body_star = t_init ; t_enter ;(t_body ; t_next)*
Deal with initialization expression
Deal with condition expression
An effort could be made to compute the precondition for t_continue, especially if the precondition to t_inc is available.
Deal with increment expression
An effort could be made to compute the precondition for t_inc
Let's clean up the memory
fl | l |
pre | re |
flel | lel |
Definition at line 326 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), forloop_body, forloop_condition, forloop_increment, forloop_initialization, free_transformer(), safe_expression_to_transformer(), transformer_apply(), transformer_combine(), transformer_identity(), and transformer_undefined.
Referenced by instruction_to_transformer().
list forloop_to_transformer_list | ( | forloop | , |
transformer | , | ||
list | |||
) |
transformer fortran_user_call_to_transformer | ( | entity | f, |
list | pc, | ||
list | ef | ||
) |
Effects are necessary to clean up the transformer t_caller.
For instance, an effect on variable X may not be taken into account in t_callee but it may be equivalenced thru a common to a variable i which is analyzed in the caller. If X is written, I value is lost. See Validation/equiv02.f.
add equations linking formal parameters to argument expressions to transformer t_callee and project along the formal parameters
for performance, it would be better to avoid building formals and to inline entity_to_formal_parameters
it wouls also be useful to distinguish between in and out parameters; I'm not sure the information is really available in a field ???
take care of analyzable formal parameters
type checking. You already know that fp is a scalar variable
formal parameter e is modified. expr must be a reference
normal case: ap_new==fp_new, ap_old==fp_old
Variable ap is not analyzed. The information about fp will be lost.
Attemps at modifying a value: expr is call, fp is modified
Actual argument is not a reference: it might be a user error! Transformers do not carry the may/must information. A check with effect list ef should be performed...
FI: does effect computation emit a MUST/MAYwarning?
Formal parameter fp is not modified. Add fp == expr, if possible.
We should evaluate expr under a precondition pre... which has not been passed down. We set pre==tf_undefined.
temporary value counter cannot be reset because other temporary values may be in use in a case the user call is a user function call
reset_temporary_value_counter();
formal new and old values left over are eliminated
test to insure that entity_to_old_value exists
take care of global variables
FI: are invisible variables taken care of by translate_global_values()? Yes, now... A variable may be invisible because its location is reached thru an array or thru a non-integer scalar variable in the current module, for instance because a COMMON is defined differently. A variable whose location is not reachable in the current module environment is considered visible.
Callee f may have read/write effects on caller's scalar integer variables thru an array and/or non-integer variables.
The relation basis must be updated too
The return value of a function is not yet projected.
pc | c |
ef | f |
Definition at line 2269 of file ri_to_transformers.c.
References any_expression_to_transformer(), arguments_add_entity(), arguments_union(), Ssysteme::base, base_contains_variable_p(), basic_equal_p(), basic_of_expression(), basic_to_string(), CONS, dump_transformer, dump_value_name(), effects_to_transformer(), effects_write_at_least_once_p(), ENTITY, entity_has_values_p(), entity_is_argument_p(), entity_local_name(), entity_name, entity_storage, entity_to_new_value(), entity_to_old_value(), entity_type, entity_undefined, expression_syntax, expression_to_proper_constant_path_effects(), expression_undefined, external_entity_to_new_value(), external_entity_to_old_value(), f(), find_ith_argument(), FOREACH, formal_offset, free_arguments(), free_transformer(), gen_free_list(), get_current_module_entity(), get_current_module_name(), ifdebug, list_undefined, load_summary_transformer(), module_local_name(), module_to_formal_analyzable_parameters(), NIL, pips_assert, pips_debug, pips_user_error, predicate_system, reference_variable, sc_base_add_variable(), sc_fprint(), semantics_user_warning, storage_formal, syntax_reference, syntax_reference_p, transformer_arguments, transformer_dup(), transformer_empty_p(), transformer_filter(), transformer_relation, transformer_safe_image_intersection(), transformer_temporary_value_projection(), transformer_undefined, transformer_undefined_p, transformer_value_substitute(), transformer_weak_consistency_p(), translate_global_values(), type_variable, value_to_variable(), and variable_basic.
Referenced by fortran_user_function_call_to_transformer(), and user_call_to_transformer().
void free_postcondition_map | ( | void | ) |
void free_precondition_map | ( | void | ) |
void free_semantic_map | ( | void | ) |
void free_total_precondition_map | ( | void | ) |
void free_transformer_map | ( | void | ) |
transformer generic_complete_statement_transformer | ( | transformer | t, |
transformer | pre, | ||
statement | s, | ||
bool | identity_p | ||
) |
Loops, do, for, while or repeat, have transformers linked to their body preconditions so as to compute those.
But the real loop transformer includes also the possible loop skip and the possible loop exit. This function completes transformer t, which is linked to the loop body precondition, and use additional information carried by statement s, analyzed with precondition pre to return the global loop transformer. If statement s is not a loop, a copy of t is returned.
Parameter identity_p is likely to be useless. It was added to track identity transformers before they were dealt with by transformer lists.
If i is a loop, the expected transformer can be more complex (see nga06) because the stores transformer is later used to compute the loop body precondition. It cannot take into account the exit condition. So the exit condition is added by the complete_xxx functions.
likely memory leak:-(. ct should be allocated in both test branches and freed at call site but I program everything under the opposite assumption
The refined transformer may be lost or stored as a block transformer is the loop is directly surrounded by a bloc or used to compute the transformer of the surroundings blokcs
No need to complete it
The search for an non identity execution path must be propagated downwards
Each component may or not update the state...
pre | re |
identity_p | dentity_p |
Definition at line 3706 of file ri_to_transformers.c.
References complete_forloop_transformer(), complete_loop_transformer(), complete_repeatloop_transformer(), copy_transformer(), evaluation_before_p, instruction_forloop, instruction_forloop_p, instruction_loop, instruction_loop_p, instruction_sequence_p, instruction_whileloop, instruction_whileloop_p, new_complete_whileloop_transformer(), statement_instruction, transformer_undefined, and whileloop_evaluation.
Referenced by complete_non_identity_statement_transformer(), and complete_statement_transformer().
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().
transformer generic_reference_to_transformer | ( | entity | v, |
reference | r, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
expression.c
expression.c
May return an undefined transformer
If you are dealing with a C array reference, find transformers for each subscript expression in case of side effects.
pre | re |
is_internal | s_internal |
Definition at line 126 of file expression.c.
References analyzable_scalar_entity_p(), analyzed_type_p(), array_type_p(), c_language_module_p(), CONS, constant_memory_access_path_to_location_entity(), ENDP, ENTITY, entity_basic_concrete_type(), entity_has_values_p(), entity_initial, entity_to_new_value(), entity_undefined_p, EXPRESSION, expressions_to_transformer(), external_entity_to_new_value(), FOREACH, free_transformer(), get_bool_property(), get_current_module_entity(), location_entity_p(), make_reference(), make_zero_expression(), modified_variables_with_values(), NIL, points_to_reference_to_concrete_type(), reference_indices, reference_variable, references_may_conflict_p(), simple_equality_to_transformer(), store_independent_reference_p(), transformer_add_equality(), transformer_add_variable_update(), transformer_intersection(), transformer_undefined, transformer_undefined_p, and value_reference.
Referenced by assign_rhs_to_reflhs_to_transformer(), expression_to_transformer(), float_expression_to_transformer(), integer_expression_to_transformer(), pointer_expression_to_transformer(), and points_to_unary_operation_to_transformer().
transformer generic_substitute_formal_array_elements_in_transformer | ( | transformer | , |
entity | , | ||
list | , | ||
transformer | , | ||
list | , | ||
bool | |||
) |
transformer generic_transformer_intra_to_inter | ( | transformer | tf, |
list | le, | ||
bool | preserve_rv_p | ||
) |
transformer translation from the module intraprocedural transformer to the module interprocedural transformer.
Values related to variables local to the module must be eliminated. Note that in C they should be eliminated earlier when the effect of the local declaration is taken into account or when the corresponding scope block is closed.
Filtered TransFormer ftf
cons * old_args = transformer_arguments(ftf);
get rid of tf's arguments that do not appear in effects le
build a list of arguments to suppress
FI: I do not understand anymore why corresponding old values do not have to be suppressed too (6 July 1993)
FI: because only read arguments are eliminated, non? (12 November 1995)
FI: the resulting intermediate transformer is not consistent (18 July 2003)
get rid of them
ftf = transformer_projection(ftf, lost_args);
free the temporary list of entities
get rid of local read variables
FI: why not use this loop to get rid of all local variables, read or written?
Variables with no impact on the caller world are eliminated. However, the return value associated to a function is conditionnally preserved.
get rid of them
free the temporary list of entities
tf | f |
le | e |
preserve_rv_p | reserve_rv_p |
Definition at line 1398 of file ri_to_transformers.c.
References arguments_add_entity(), BASE_UNDEFINED, BASE_UNDEFINED_P, concrete_effects_may_read_or_write_scalar_entity_p(), dump_transformer, effects_may_read_or_write_scalar_entity_p(), entity_constant_p, entity_storage, f(), formal_parameter_p(), gen_free_list(), get_current_module_entity(), global_variable_p(), ifdebug, NIL, pips_debug, predicate_system, storage_return, storage_return_p, Svecteur::succ, TCST, transformer_dup(), transformer_projection(), transformer_relation, value_to_variable(), and vecteur_var.
Referenced by c_return_to_transformer(), and transformer_intra_to_inter().
int get_call_site_number | ( | void | ) |
Definition at line 1131 of file interprocedural.c.
References number_of_call_sites.
Referenced by summary_precondition(), and summary_total_postcondition().
list get_module_global_arguments | ( | void | ) |
Definition at line 98 of file ri_to_preconditions.c.
References module_global_arguments.
Referenced by statement_to_postcondition(), and statement_to_total_precondition().
transformer get_module_precondition | ( | entity | m | ) |
interprocedural.c
interprocedural.c
include <stdlib.h> What follows has to be updated!!!
The SUMMARY_PRECONDITION of a module m is built incrementally when the preconditions of its CALLERS are computed. Each time a call site cs to m is encountered, the precondition for cs is augmented with equations between formal and actual integer arguments. The new precondition so obtained is chained to the other preconditions for m.
In other word, SUMMARY_PRECONDITION is a list of preconditions containing each a relation between formal and actual parameter. Should it be called SUMMARY_PRECONDITIONS?
Before using the list of preconditions for m, each precondition has to:
These steps cannot be performed in the caller because the callee's value mappings are unknown.
Memory management:
Note: illegal request are made to pipsdbm()
FI: this does not work because the summary preconditions is reset each time it should be accumulated
Definition at line 92 of file interprocedural.c.
References db_get_memory_resource(), db_resource_p(), entity_module_p(), module_local_name(), pips_assert, and transformer_undefined.
Referenced by add_module_call_site_precondition().
statement_mapping get_postcondition_map | ( | void | ) |
statement_mapping get_precondition_map | ( | void | ) |
Referenced by init_use_preconditions(), module_name_to_preconditions(), set_resources_for_module(), and transformer_map_print().
statement_mapping get_semantic_map | ( | void | ) |
text get_text_preconditions | ( | const | string | ) |
string | odule_name |
Definition at line 193 of file prettyprint.c.
References get_bool_property(), get_semantic_text(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, and module_name().
Referenced by print_call_graph_with_preconditions().
text get_text_total_preconditions | ( | const | string | ) |
string | odule_name |
Definition at line 203 of file prettyprint.c.
References get_bool_property(), get_semantic_text(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, and module_name().
Referenced by print_call_graph_with_total_preconditions().
text get_text_transformers | ( | const | string | ) |
string | odule_name |
Definition at line 184 of file prettyprint.c.
References get_semantic_text(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, and module_name().
Referenced by print_call_graph_with_transformers().
statement_mapping get_total_precondition_map | ( | void | ) |
statement_mapping get_transformer_map | ( | void | ) |
Filter out local and unused variables from the local precondition? No, because it is not possible to guess what is used or unused at the program level. Filtering is postponed to program_precondition().
name | ame |
Definition at line 75 of file initial.c.
References all_data_to_precondition(), db_get_memory_resource(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free_statement_global_stack(), free_value_mappings(), ifdebug, make_statement_global_stack(), module, module_name_to_entity(), module_to_value_mappings(), pips_assert, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), strdup(), and transformer_consistency_p().
transformer integer_assign_to_transformer | ( | expression | lhs, |
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
This function never returns an undefined transformer.
It is used for an assignment statement, not for an assignment operation. effects of assign
algorithm: if lhs and rhs are linear expressions on scalar integer variables, build the corresponding equation; else, use effects ef
should be extended to cope with constant integer division as in N2 = N/2 because it is used in real program; inequalities should be generated in that case 2*N2 <= N <= 2*N2+1
same remark for MOD operator
implementation: part of this function should be moved into transformer.c
&& integer_scalar_entity_p(e)
FI: the initial version was conservative because only affine scalar integer assignments were processed precisely. But non-affine operators and calls to user defined functions can also bring some information as soon as some integer read or write effect exists
check that all read effects are on integer scalar entities
Check that some read or write effects are on integer scalar entities. This is almost always true... Let's hope assigned_expression_to_transformer() returns quickly for array expressions used to initialize a scalar integer entity.
if some condition was not met and transformer derivation failed
lhs | hs |
rhs | hs |
pre | re |
ef | f |
Definition at line 2693 of file ri_to_transformers.c.
References assigned_expression_to_transformer(), effects_to_transformer(), entity_has_values_p(), ifdebug, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_debug, print_transformer, some_integer_scalar_read_or_write_effects_p(), transformer_undefined, and vecteur_var.
list integer_assign_to_transformer_list | ( | expression | lhs, |
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
This function never returns an undefined transformer.
It is used for an assignment statement, not for an assignment operation. effects of assign
algorithm: if lhs and rhs are linear expressions on scalar integer variables, build the corresponding equation; else, use effects ef
should be extended to cope with constant integer division as in N2 = N/2 because it is used in real program; inequalities should be generated in that case 2*N2 <= N <= 2*N2+1
same remark for MOD operator
implementation: part of this function should be moved into transformer.c
&& integer_scalar_entity_p(e)
FI: the initial version was conservative because only affine scalar integer assignments were processed precisely. But non-affine operators and calls to user defined functions can also bring some information as soon as some integer read or write effect exists
check that all read effects are on integer scalar entities
Check that some read or write effects are on integer scalar entities. This is almost always true... Let's hope assigned_expression_to_transformer() returns quickly for array expressions used to initialize a scalar integer entity.
if some condition was not met and transformer derivation failed
lhs | hs |
rhs | hs |
pre | re |
ef | f |
Definition at line 645 of file ri_to_transformer_lists.c.
References assigned_expression_to_transformer(), effects_to_transformer(), entity_has_values_p(), ifdebug, NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_debug, pips_internal_error, print_transformers(), some_integer_scalar_read_or_write_effects_p(), transformer_undefined, and vecteur_var.
void integer_expression_and_precondition_to_integer_interval | ( | expression | e, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Could be used for bool expressions too? Extended to any kind of expression?
p is assumed to be a real precondition, i.e. a transformer_range().
This function is used by semantics as well as exported to other passes. To take care of debug_on()/debug_off(), set and reset_analyzed_types(), a different wrapper is needed.
If expression e is transformer-wise side-effect free (i.e. the ABSTRACT store is not modified)
precondition p is not feasible
plb | lb |
pub | ub |
Definition at line 386 of file utils.c.
References CONTRAINTE_UNDEFINED, debug_off, debug_on, ENDP, expression_to_type(), integer_expression_to_transformer(), make_local_temporary_value_entity(), predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), transformer_arguments, transformer_dup(), transformer_range_intersection(), transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, and VALUE_ZERO.
Referenced by eval_linear_expression(), expression_multiply_sizeof_to_transformer(), generic_abs_to_transformer(), and loop_to_enter_transformer().
transformer integer_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
Do check wrt to value mappings...
if you are not dealing with interprocedural issues
Assume: e is a value
Is it really useful to keep using this function which does not take the precondition into acount?
vect_rm(ve);
expr | xpr |
pre | re |
is_internal | s_internal |
Definition at line 3476 of file expression.c.
References cast_expression, cast_type, constant_int, constant_int_p, copy_transformer(), EvalSizeofexpression(), expression_effects_to_transformer(), expression_syntax, expression_to_type(), free_transformer(), free_type(), generic_reference_to_transformer(), get_bool_property(), ifdebug, integer_call_expression_to_transformer(), NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_debug, print_expression(), simple_affine_to_transformer(), syntax_call_p, syntax_cast, syntax_cast_p, syntax_reference, syntax_reference_p, syntax_sizeofexpression, syntax_sizeofexpression_p, transformer_add_equality_with_integer_constant(), transformer_combine(), transformer_identity(), transformer_undefined, transformer_undefined_p, type_equal_p(), value_constant, and value_constant_p.
Referenced by any_expression_to_transformer(), iabs_to_transformer(), integer_expression_and_precondition_to_integer_interval(), integer_minmax_to_transformer(), and safe_integer_expression_to_transformer().
void integer_value_and_precondition_to_integer_interval | ( | entity | v, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Should be used by previous function, integer_expression_and_precondition_to_integer_interval()
precondition p is not feasible
plb | lb |
pub | ub |
Definition at line 427 of file utils.c.
References CONTRAINTE_UNDEFINED, predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, and VALUE_ZERO.
Referenced by integer_binary_operation_to_transformer(), and integer_multiply_to_transformer().
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().
transformer intrinsic_to_transformer | ( | entity | e, |
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
effects of intrinsic call
FI: this may happen, for instance with the macro definition of assert() or because the programmer writes "i>1? (i = 2): (i = 3);" instead of "i = i>1? 2 : 3;"
FI: the condition should be evaluated and considered true on exit, but this is sometimes captured by a macro definition and the code below is then useless
The result is positive and less than RAND_MAX, but it is ignored by the semantics anaysis
pc | c |
pre | re |
ef | f |
Definition at line 911 of file ri_to_transformers.c.
References any_assign_to_transformer(), any_basic_update_to_transformer(), any_update_to_transformer(), c_return_to_transformer(), CAR, CDR, condition_to_transformer(), conditional_to_transformer(), effects_to_transformer(), ENTITY_ABORT_SYSTEM_P, ENTITY_ASSERT_FAIL_SYSTEM_P, ENTITY_ASSERT_SYSTEM_P, ENTITY_ASSIGN_P, ENTITY_BITWISE_AND_UPDATE_P, ENTITY_BITWISE_OR_UPDATE_P, ENTITY_BITWISE_XOR_UPDATE_P, ENTITY_C_RETURN_P, ENTITY_COMMA_P, ENTITY_CONDITIONAL_P, ENTITY_DIVIDE_UPDATE_P, ENTITY_EXIT_SYSTEM_P, ENTITY_LEFT_SHIFT_UPDATE_P, ENTITY_MINUS_UPDATE_P, ENTITY_MODULO_UPDATE_P, ENTITY_MULTIPLY_UPDATE_P, ENTITY_PLUS_UPDATE_P, ENTITY_POST_DECREMENT_P, ENTITY_POST_INCREMENT_P, ENTITY_PRE_DECREMENT_P, ENTITY_PRE_INCREMENT_P, ENTITY_RAND_P, ENTITY_RIGHT_SHIFT_UPDATE_P, ENTITY_STOP_P, EXPRESSION, expressions_to_transformer(), pips_debug, semantics_user_warning, transformer_empty(), transformer_identity(), and transformer_undefined.
Referenced by call_to_postcondition(), and call_to_transformer().
list intrinsic_to_transformer_list | ( | entity | e, |
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
because of the conditional and the comma C intrinsics at least
effects of intrinsic call
FI: this may happen, for instance with the macro definition of assert() or because the programmer writes "i>1? (i = 2): (i = 3);" instead of "i = i>1? 2 : 3;"
FI: the condition should be evaluated and considered true on exit, but this is sometimes captured by a macro definition and the code below is then useless
pc | c |
pre | re |
ef | f |
Definition at line 480 of file ri_to_transformer_lists.c.
References any_assign_to_transformer(), any_basic_update_to_transformer(), any_update_to_transformer(), c_return_to_transformer(), CAR, CDR, condition_to_transformer(), conditional_to_transformer(), CONS, effects_to_transformer(), ENTITY_ABORT_SYSTEM_P, ENTITY_ASSERT_FAIL_SYSTEM_P, ENTITY_ASSERT_SYSTEM_P, ENTITY_ASSIGN_P, ENTITY_BITWISE_AND_UPDATE_P, ENTITY_BITWISE_OR_UPDATE_P, ENTITY_BITWISE_XOR_UPDATE_P, ENTITY_C_RETURN_P, ENTITY_COMMA_P, ENTITY_CONDITIONAL_P, ENTITY_DIVIDE_UPDATE_P, ENTITY_EXIT_SYSTEM_P, ENTITY_LEFT_SHIFT_UPDATE_P, ENTITY_MINUS_UPDATE_P, ENTITY_MODULO_UPDATE_P, ENTITY_MULTIPLY_UPDATE_P, ENTITY_PLUS_UPDATE_P, ENTITY_POST_DECREMENT_P, ENTITY_POST_INCREMENT_P, ENTITY_PRE_DECREMENT_P, ENTITY_PRE_INCREMENT_P, ENTITY_RIGHT_SHIFT_UPDATE_P, ENTITY_STOP_P, EXPRESSION, expressions_to_transformer(), NIL, pips_debug, pips_internal_error, TRANSFORMER, transformer_empty(), and transformer_undefined.
transformer lhs_expression_to_transformer | ( | entity | e, |
expression | lhs, | ||
transformer | pre | ||
) |
This function deals with e1.e2 and e1->e2, not with simple references such as x or a[i].
This piece of code has mainly been retrieved from any_assign_to_transformer().
FI: I am not sure how to factorize it out because entity e corresponds to some memory location and is modified in an assignement environment. Here, e is likely to be a temporary value. It is not updated. It should not appear among the transformer arguments
lhs | hs |
pre | re |
Definition at line 6262 of file expression.c.
References analyzed_reference_p(), CELL, cell_any_reference(), constant_memory_access_path_to_location_entity(), constant_path_analyzed_p(), copy_transformer(), cp, entity_undefined_p, expression_syntax, FOREACH, free_transformer(), gen_length(), int, pips_internal_error, pt_to_list_undefined_p(), semantics_expression_to_points_to_sources(), semantics_usable_points_to_reference_p(), syntax_call_p, transformer_add_equality(), transformer_convex_hull(), transformer_undefined, and transformer_undefined_p.
Referenced by integer_call_expression_to_transformer().
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().
transformer load_cycle_fix_point | ( | control | c, |
hash_table | fix_point_map | ||
) |
fix_point_map | ix_point_map |
Definition at line 544 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, pips_assert, and transformer_undefined.
transformer load_cycle_temporary_precondition | ( | control | , |
control_mapping | , | ||
hash_table | , | ||
hash_table | |||
) |
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().
transformer load_statement_postcondition | ( | statement | ) |
transformer load_statement_precondition | ( | statement | ) |
Referenced by __attribute__(), add_alias_pairs_for_this_call_site(), any_complexities(), block_to_complexity(), comp_regions_of_statement(), create_step_regions(), do_array_expansion(), do_solve_hardware_constraints_on_nb_proc(), do_solve_hardware_constraints_on_volume(), effects_to_dma(), first_precondition_of_module(), formal_array_resizing_bottom_up(), interprocedural_abc_arrays(), loop_executed_approximation(), new_block_to_complexity(), out_regions_from_call_site_to_callee(), parametric_statement_feasible_p(), partial_eval_min_or_max_operator(), process_ready_node(), process_unreachable_node(), set_methods_for_convex_effects(), set_methods_for_convex_rw_pointer_effects(), statement_context(), statement_to_complexity(), statement_to_postcondition(), statement_to_total_precondition(), statement_to_transformer(), statement_to_transformer_list(), statement_weakly_feasible_p(), step_translate_and_map(), stmt_prec(), TestCoupleOfEffects(), xml_Call(), and xml_Loop().
transformer load_statement_semantic | ( | statement | ) |
Referenced by call_site_to_module_precondition_text(), memorize_precondition_for_summary_precondition(), and semantic_to_text().
transformer load_statement_temporary_precondition | ( | statement | s, |
statement_mapping | statement_temporary_precondition_map | ||
) |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 1069 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, and pips_assert.
Referenced by cycle_to_flow_sensitive_preconditions().
transformer load_statement_total_precondition | ( | statement | ) |
transformer load_statement_transformer | ( | statement | ) |
Referenced by add_loop_index_exit_value(), any_loop_to_k_transformer(), comp_regions_of_statement(), complete_forloop_transformer(), complete_forloop_transformer_list(), complete_loop_transformer(), complete_loop_transformer_list(), complete_repeatloop_transformer_list(), cycle_to_flow_sensitive_preconditions(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), forloop_to_postcondition(), load_completed_statement_transformer(), loop_to_total_precondition(), loop_to_transformer(), new_complete_whileloop_transformer_list(), old_complete_whileloop_transformer(), process_ready_node(), process_unreachable_node(), recompute_loop_transformer(), repeatloop_to_postcondition(), repeatloop_to_transformer(), set_methods_for_convex_effects(), set_methods_for_convex_rw_pointer_effects(), statement_to_postcondition(), statement_to_total_precondition(), statement_to_transformer(), statement_to_transformer_list(), unreachable_node_to_transformer(), unstructured_to_flow_insensitive_transformer(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
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().
transformer logical_expression_to_transformer | ( | entity | v, |
expression | rhs, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
Could be used to compute preconditions too.
v is assumed to be a new value or a temporary value.
Is likely to be handled as a nullary intrinsics
rhs | hs |
pre | re |
is_internal | s_internal |
Definition at line 3938 of file expression.c.
References call_constant_p(), call_function, expression_syntax, f(), integer_constant_p(), intrinsic_entity_p(), is_syntax_call, is_syntax_range, is_syntax_reference, logical_constant_p(), logical_intrinsic_to_transformer(), logical_reference_to_transformer(), pips_internal_error, reference_variable, syntax_call, syntax_reference, syntax_tag, transformer_add_equality_with_integer_constant(), transformer_identity(), transformer_intersection(), transformer_undefined, transformer_undefined_p, and user_function_call_to_transformer().
Referenced by any_expression_to_transformer(), logical_binary_operation_to_transformer(), and logical_unary_operation_to_transformer().
transformer logical_intrinsic_to_transformer | ( | entity | v, |
call | c, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
pre | re |
is_internal | s_internal |
Definition at line 3911 of file expression.c.
References call_arguments, call_function, entity_name, gen_length(), logical_binary_function_to_transformer(), logical_constant_to_transformer(), logical_unary_operation_to_transformer(), pips_internal_error, and transformer_undefined.
Referenced by logical_expression_to_transformer().
transformer logical_not_to_transformer | ( | entity | v, |
list | args, | ||
transformer | pre | ||
) |
returns the transformer associated to a C logical not, !, applied to an integer argument, when meaningful, and transformer_undefined otherwise.
Effects must be used at a higher level to fall back on a legal transformer.
v | is the value associated to the expression |
args | is assumed to have only one expression element of type int or enum negated by ! |
pre | is the current precondition |
args | rgs |
pre | re |
Definition at line 5571 of file expression.c.
References CAR, EXPRESSION, free_transformer(), intptr_t, make_local_temporary_integer_value_entity(), precondition_minmax_of_value(), safe_any_expression_to_transformer(), transformer_add_equality_with_integer_constant(), transformer_add_inequality_with_integer_constraint(), transformer_range(), and transformer_undefined.
Referenced by integer_call_expression_to_transformer().
transformer loop_bound_evaluation_to_transformer | ( | loop | l, |
transformer | pre | ||
) |
Side effects in loop bounds and increment are taken into account.
The conditions on the loop index are given by the range of this transformer.
pre | re |
Definition at line 1203 of file loop.c.
References any_expression_to_transformer(), entity_has_values_p(), entity_to_expression(), entity_to_new_value(), entity_type, expression_and_precondition_to_integer_interval(), free_expression(), loop_index, loop_initialization_to_transformer(), loop_range, make_local_temporary_value_entity(), range_increment, range_lower, range_upper, reset_temporary_value_counter(), transformer_inequality_add(), transformer_safe_apply(), transformer_safe_image_intersection(), transformer_safe_intersection(), transformer_temporary_value_projection(), transformer_undefined, VALUE_MONE, VALUE_ONE, vect_add_elem(), vect_multiply(), and vect_new().
Referenced by add_good_loop_conditions().
transformer loop_initialization_to_transformer | ( | loop | l, |
transformer | pre | ||
) |
Note: It used to be implemented by computing the effect list of the lower bound expression and and new allocated effect for the loop index definition.
It turns out to be very heavy, because cells must be of kind preference to be usable by several functions because macro effect_reference() expects so without testing it.
However, it is also difficult to add a variable to the transformer t_init because of aliasing. So let's stick to the initial implementation.
over-approximation of effects
free_effects() is not enough, because it is a persistant reference
pre | re |
Definition at line 1266 of file loop.c.
References any_scalar_assign_to_transformer(), cell_preference, CONS, EFFECT, effect_cell, expression_to_proper_constant_path_effects(), free_effect(), free_reference(), free_transformer(), gen_free_list(), gen_nconc(), ifdebug, is_cell_preference, list_undefined, loop_index, loop_range, make_action_write_memory(), make_approximation_exact(), make_cell(), make_descriptor_none(), make_effect(), make_preference(), make_reference(), NIL, preference_reference, print_effects, range_lower, transformer_safe_range(), and transformer_undefined.
Referenced by loop_bound_evaluation_to_transformer(), loop_to_postcondition(), loop_to_total_precondition(), and loop_to_transformer().
transformer loop_to_continue_transformer | ( | loop | l, |
transformer | pre | ||
) |
FI: the function transformer_add_loop_index_incrementation should be rewritten to exploit preconditions better.
pre | re |
Definition at line 1501 of file loop.c.
References free_transformer(), loop_to_enter_transformer(), transformer_add_loop_index_incrementation(), transformer_combine(), and transformer_identity().
Referenced by new_loop_to_transformer().
transformer loop_to_enter_transformer | ( | loop | l, |
transformer | pre | ||
) |
Transformer expressiong the conditions between the index and the loop bounds according to the sign of the increment.
A zero increment is not legal because the Fortran standard imposes a division by the increment.
Only the loop bopy statement number is available...
Assumption: no side effect in loop bound expressions
The increment is strictly positive
The increment is strictly negative
The sign of the increment is unknown, no information is available
No information is available for loop indices that are not integer
This could be improved, but floating point indices should never be used.
pre | re |
Definition at line 1442 of file loop.c.
References entity_type, free_transformers(), integer_expression_and_precondition_to_integer_interval(), loop_index, loop_range, make_local_temporary_value_entity(), pips_user_error, range_increment, range_lower, range_upper, safe_integer_expression_to_transformer(), scalar_integer_type_p(), transformer_add_inequality_with_linear_term(), transformer_identity(), transformer_intersection(), transformer_normalize(), and transformer_temporary_value_projection().
Referenced by loop_to_continue_transformer(), and new_loop_to_transformer().
transformer loop_to_initialization_transformer | ( | loop | l, |
transformer | pre | ||
) |
Transformer expression the loop initialization.
pre | re |
Definition at line 1430 of file loop.c.
References assigned_expression_to_transformer(), loop_index, loop_range, and range_lower.
Referenced by new_loop_to_transformer().
transformer loop_to_postcondition | ( | transformer | pre, |
loop | l, | ||
transformer | tf | ||
) |
pips_internal_error("Equality option not implemented");
the standard version should be OK for SEMANTICS_EQUALITY_INVARIANTS...
basic cheap version: add information on loop index in pre and propagate preb downwards in the loop body; compute the loop postcondition independently using the loop transformer
preb = precondition for loop body; includes a lousy fix-point
Get rid of information related to variables modified in iterations of the loop body (including loop indices).
Apparently, the loop index incrementation is not in tf... according to a test with DO I = I, N although it should be... according to the caller of this function and the display of loop transformers!
Triolet's good loop algorithm
It might be useful to normalize preb and to detect unfeasibility. I choose not to do it because:
So basically, I shift the burden from precondition computation to dead code elimination. Dead loop testing must use a strong feasibility test.
If this decision is reversed, dead code elimination can be speeded-up.
Note that add_good_loop_conditions() can test trivial cases automatically generated.
Decision reverted: Francois Irigoin, 4 June 1997
preb can now be used to obtain a refined tf, for instance to show that a variable is monotonically increasing.
FI: this is not correct when an invariant is found; we should add one more incrementation of I (to modify the output of the invariant and express the fact that the loop bound is no more true, at least when the increment is one. 6 July 1993
Note 1: this comments was wrong! See Validation/Semantics/induc1.f Note 2: but the result was wrong anyway because it assumed that at least one iteration always was performed. Note 3: This is fixed by reverting the above decision.
propagate an impossible precondition in the loop body
The loop body precondition is not useful any longer
propagate preconditions in the loop body and compute its postcondition...
... or compute directly the postcondition using the loop body transformer. This second approach is slightly less precise because the transformer cannot use preconditions to avoid some convex approximations.
post = transformer_apply(tf, pre);
The loop body effects should be passed as fourth argument to check that the value of the upper bound expression is not modified when the body is executed. But it is not available and it is not yet used by ad_loop_index_exit_value()!
First version: OK, but could be better!
transformer postloop = transformer_apply(tf, pre);
pre must be copied because sc_convex_hull updates is arguments and may make them inconsistent when the two bases are merged to perform the convex hull in a common vector space
Second version: assume it is empty or non-empty and perform the convex hull of both (should be checked on Validation/Semantics/induc1.f)
propagate preconditions in the loop body
post_al = transformer_apply(tf, pre);
We should add (when possible) the non-entry condition in post_ne! For instance, DO I = 1, N leads to N <= 0
FI: Cannot be freed because it was stored for statement s: transformer_free(preb); did I mean to free pre, which is useless since it was changed into preb?
pre | re |
tf | f |
Definition at line 2841 of file loop.c.
References add_good_loop_conditions(), add_loop_index_exit_value(), add_loop_index_initialization(), add_loop_skip_condition(), debug(), empty_range_wrt_precondition_p(), fprintf(), free_transformer(), get_bool_property(), ifdebug, loop_body, loop_initialization_to_transformer(), loop_range, non_empty_range_wrt_precondition_p(), pips_debug, pips_flag_p, pips_internal_error, print_transformer, recompute_loop_transformer(), SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_range(), and transformer_undefined.
Referenced by instruction_to_postcondition().
transformer loop_to_total_precondition | ( | transformer | t_post, |
loop | l, | ||
transformer | tf, | ||
transformer | context | ||
) |
Triolet's good loop algorithm
preb = transformer_dup(pre);
The loop is never executed
impact of loop index initialization, i.e. I = IT(J),.. or I = K/L,..
the loop may be entered for sure, or entered or not
We need a fix_point without the initial condition but with the exit condition
Also performs last incrementation
free_transformer(b_t_pre); it is associated to the loop body!
The loop is always entered
The loop may be skipped or entered
skipped case computed here too
t_post | _post |
tf | f |
context | ontext |
Definition at line 3023 of file loop.c.
References add_good_loop_conditions(), add_loop_index_exit_value(), add_loop_skip_condition(), empty_range_wrt_precondition_p(), fprintf(), free_transformer(), get_bool_property(), ifdebug, load_statement_transformer(), loop_body, loop_initialization_to_transformer(), loop_range, non_empty_range_wrt_precondition_p(), pips_assert, pips_debug, print_transformer, recompute_loop_transformer(), statement_to_total_precondition(), transformer_add_loop_index_incrementation(), transformer_combine(), transformer_consistency_p(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_inverse_apply(), transformer_to_domain(), and transformer_undefined.
Referenced by instruction_to_total_precondition().
transformer loop_to_transformer | ( | loop | l, |
transformer | pre, | ||
list | e | ||
) |
The transformer associated to a DO loop does not include the exit condition because it is used to compute the precondition for any loop iteration.
There is only one attachment for the unbounded transformer and for the bounded one.
loop transformer tf = tfb* or tf = tfb+ or ...
loop body transformer
approximate loop transformer, including loop index updates
loop body precondition
Information about loop local variables is lost
range r = loop_range(l);
eliminate all information about local variables
Mostly useful for Fortran code.
In C, variables declared in the loop body do not exist before the loop is entered and so do not have to be projected. But local variables may have been introduced by a privatization phase.
compute the loop body transformer under loop body precondition preb
add indexation step under loop precondition pre
compute tfb's fix point according to pips flags
restrict the domain of tf by the range of pre, except for the loop index which is assigned in between
add initialization for the unconditional initialization of the loop index variable
we have a problem here: to compute preconditions within the loop body we need a tf using private variables; to return the loop transformer, we need a filtered out tf; only one hook is available in the ri..; let'a assume there are no private variables and that if they are privatizable they are not going to get in our way
pre | re |
Definition at line 1319 of file loop.c.
References add_good_loop_conditions(), add_index_range_conditions(), CONS, effects_to_transformer(), ENTITY, external_value_name(), fprint_transformer(), fprintf(), free_transformer(), gen_free_list(), get_bool_property(), ifdebug, invariant_wrt_transformer(), load_statement_transformer(), loop_body, loop_index, loop_initialization_to_transformer(), loop_locals, loop_range, NIL, pips_debug, print_transformer, safe_transformer_projection(), statement_to_transformer(), transformer_add_loop_index_incrementation(), transformer_combine(), transformer_domain_intersection(), transformer_dup(), transformer_filter(), transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by instruction_to_transformer().
list loop_to_transformer_list | ( | loop | , |
transformer | , | ||
list | |||
) |
void make_postcondition_map | ( | void | ) |
void make_precondition_map | ( | void | ) |
sentence make_pred_commentary_sentence(string str_pred, string comment_prefix) input : a substring formatted to be a commentary output : a sentence, containing the commentary form of this string, beginning with the comment_prefix.
modifies : nothing
str_pred | tr_pred |
comment_prefix | omment_prefix |
Definition at line 678 of file prettyprint.c.
References concatenate(), make_sentence_formatted(), sentence_undefined, and strdup().
Referenced by string_predicate_to_commentary(), and text_comp_region().
void make_semantic_map | ( | void | ) |
void make_total_precondition_map | ( | void | ) |
void make_transformer_map | ( | void | ) |
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().
returns a module's parameter's list
get unsorted list of formal analyzable parameters for f by declaration filtering; these parameters may not be used by the callee's semantics analysis, but we have no way to know it because value mappings are not available
Definition at line 232 of file interprocedural.c.
References analyzable_scalar_entity_p(), CAR, code_declarations, CONS, ENTITY, entity_code(), entity_module_p(), entity_storage, f(), list_undefined, MAPL, NIL, pips_assert, and storage_formal_p.
Referenced by add_formal_to_actual_bindings(), and fortran_user_call_to_transformer().
void module_to_value_mappings | ( | entity | m | ) |
void module_to_value_mappings(entity m): build hash tables between variables and values (old, new and intermediate), and between values and names for module m, as well as equivalence equalities
NW: before calling "module_to_value_mappings" to set up the hash table to translate value into value names for module with name (string) module_name do:
set_current_module_entity( local_name_to_top_level_entity(module_name) );
(the following call is only necessary if a variable of type entity such as "module" is not already set) module = get_current_module_entity();
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));
(that's it, but we musn't forget to reset everything after the call to "module_to_value_mappings", as below)
reset_current_module_statement(); reset_cumulated_rw_effects(); reset_current_module_entity(); free_value_mappings();
reset local intermediate value counter for make_local_intermediate_value_entity and make_local_old_value_entity
module_inter_effects = code_effects(value_code(entity_initial(m)));
look for interprocedural write effects on scalar analyzable variables and generate proper entries into hash tables
In C, write effects on scalar formal parameter are masked by the value passing mode but the copy may nevertheless be written inside the function.
To keep the summary transformer consistent although the return value has no old value
look for interprocedural read effects on scalar analyzable variables and generate proper entries into hash tables
static variables have an old value too
look for intraprocedural write effects on scalar analyzable variables and generate proper entries into hash tables
look for intraprocedural read effects on scalar analyzable variables and generate proper entry into value name hash table if it has not been entered before; interprocedural read effects are implicitly dealed with since they are included; most entities are likely to have been encountered before; however in parameters and uninitialized variables have to be dealt with
FI: although it may only be read within this procedure, e might be written in another one thru a COMMON; this write is not visible from OUT, but only from a caller of out; because we have only a local intraprocedural or a global interprocedural view of aliasing, we have to create useless values:-(
add_new_value(e);
Note: this makes the control structure of this procedure obsolete!
This call is useless because it only is effective if entity_has_values_p() is true: add_intraprocedural_value_entities(e);
A stronger call to the same subroutine is included in the previous call: add_or_kill_equivalenced_variables(e, true);
scan declarations to make sure that private variables are taken into account; assume a read and write effects on these variables, although they may not even be used.
Only intraprocedural variables can be privatized (1 Aug. 92)
This should be useless if return variables are taken into account by effect analysis. No problem with Fortran because the return variable really is assigned a value. Not obvious in C because the assignment is implicit in the return statement. In C the return variable is more like a value: it cannot be re-assigned.
FI: Only return variables are forgotten by effects
FI: no, this is wrong in C; local variables are dropped from effect when their declaration statements are processed. They cannot be found in the effects of the module statement.
We need references to all fields, direct or indirect when a field is itself a struct
scan other referenced variables to make sure everyone has an entry in the symbol table
We need references to all fields, direct or indirect when a field is itself a struct
Beware of struct return values which may generate additional locations and location values
To be sure to retrieve all relevant locations, including array elements
for debug, print hash tables
Definition at line 624 of file mappings.c.
References action_read_p, action_write_p, add_implicit_interprocedural_write_effects(), add_interprocedural_field_entities(), add_interprocedural_new_value_entity(), add_interprocedural_value_entities(), add_intraprocedural_field_entities(), add_intraprocedural_value_entities(), add_intraprocedural_value_entities_unconditionally(), allocate_module_value_mappings(), analyzable_scalar_entity_p(), analyzed_reference_p(), analyzed_type_p(), aproximate_number_of_analyzed_variables(), c_module_p(), callees_callees, cell_any_reference(), compute_basic_concrete_type(), constant_path_analyzed_p(), current_module_declarations(), db_get_memory_resource(), EFFECT, effect_action, effect_any_reference, effect_cell, effects_package_entity_p(), ENTITY, entity_abstract_location_p(), entity_anywhere_locations_p(), entity_basic_concrete_type(), entity_for_value_mapping_p(), entity_formal_p(), entity_has_values_p(), entity_heap_location_p(), entity_local_name(), entity_module_p(), entity_static_variable_p(), entity_storage, entity_typed_anywhere_locations_p(), entity_variable_p, error_reset_value_mappings(), f(), FOREACH, free_reference(), free_type(), function_to_return_value(), functional_result, gen_true(), get_current_module_statement(), get_referenced_entities_filtered(), ifdebug, load_module_intraprocedural_effects(), load_summary_effects(), location_entity_p(), make_location_entity(), make_reference(), module_local_name(), module_name(), module_name_to_entity(), NIL, number_of_analyzed_values(), pips_assert, pips_debug, place_holder_variable_p(), points_to_reference_to_concrete_type(), print_value_mappings(), reference_variable, reset_equivalence_equalities(), reset_hooks_register(), reset_temporary_value_counter(), reset_value_counters(), set_analyzed_types(), SET_FOREACH, set_free(), storage_ram_p, storage_return_p, store_effect_p(), STRING, struct_type_p(), struct_type_to_fields(), test_mapping_entry_consistency(), type_functional, and values_for_current_module_intraprocedural_simple_effects().
Referenced by add_alias_pairs_for_this_caller(), alias_classes(), alias_lists(), alias_pairs(), aliases_text(), any_complexities(), array_expansion(), bdsc_code_instrumentation(), call_site_to_module_precondition_text(), comp_regions(), continuation_conditions(), dsc_code_parallelization(), generic_module_name_to_transformers(), generic_print_xml_application(), get_any_comp_regions_text(), get_continuation_condition_text(), get_semantic_text(), hbdsc_parallelization(), init_convex_in_out_regions(), init_convex_rw_regions(), init_convex_summary_in_out_regions(), init_convex_summary_rw_regions(), initial_precondition(), isolate_statement(), kernel_data_mapping(), kernel_load_store_engine(), module_name_to_preconditions(), module_name_to_total_preconditions(), out_regions_from_caller_to_callee(), partial_eval(), phrase_comEngine_distributor(), phrase_distributor(), phrase_distributor_control_code(), pragma_outliner(), print_initial_precondition(), print_program_precondition(), program_precondition(), safescale_distributor(), safescale_module_analysis(), sequence_dependence_graph(), solve_hardware_constraints(), spire_distributed_unstructured_to_structured(), summary_precondition(), summary_total_postcondition(), and update_precondition_with_call_site_preconditions().
transformer modulo_by_a_constant_to_transformer | ( | entity | v1, |
transformer | prec, | ||
entity | v2, | ||
int | k | ||
) |
Analyze v2 % k, with v2 constrainted by tf, assuming tf is a precondition.
See if exist a set v_i such that v2 = sum_i a_i v_i + c. Then v2 can be rewritten as v2 = gcd_i(a_i) lambda + c.
if k divides gcd(a_i) then v2>0 ? v1 = v2 % k = c % k : v1 = v2 % k = ck-k
If the sign of v2 is unknown, ck-k<=v1<=ck
v1 | 1 |
prec | rec |
v2 | 2 |
Definition at line 1481 of file expression.c.
References empty_transformer(), intptr_t, precondition_minmax_of_value(), transformer_add_equality_with_integer_constant(), transformer_add_inequality_with_integer_constraint(), transformer_identity(), and transformer_to_1D_lattice().
Referenced by modulo_to_transformer().
transformer new_add_formal_to_actual_bindings | ( | call | c, |
transformer | pre, | ||
entity | caller | ||
) |
Take side effects into account:
pre := (t(expr )...(t_expr ))(pre) U {f = expr } n 1 i i for all i such that formal f_i is an analyzable scalar variable and as far as expression expr_i is analyzable and of the same type.
The algorithmic structure has to be different from the previous one.
pre is modified by side effects.
pre | re |
caller | aller |
Definition at line 375 of file interprocedural.c.
References any_user_call_site_to_transformer(), call_arguments, call_function, dump_transformer, f(), free_transformer(), ifdebug, module_local_name(), NIL, pips_debug, and transformer_apply().
Referenced by process_call_for_summary_precondition().
transformer new_array_element_backward_substitution_in_transformer | ( | transformer | tf, |
entity | l, | ||
reference | fr, | ||
reference | ar | ||
) |
Substitute formal location entity l by a location entity corresponding to ar, if it is possible.
tf | f |
fr | r |
ar | r |
Definition at line 1723 of file ri_to_transformers.c.
References CONS, constant_memory_access_path_to_location_entity(), copy_reference(), ENDP, ENTITY, entity_undefined_p, entity_user_name(), free_reference(), gen_free_list(), gen_full_copy_list(), gen_nconc(), NIL, pl, reference_indices, reference_to_string(), semantics_user_warning, substitute_scalar_stub_in_transformer(), and transformer_projection().
Referenced by new_array_elements_backward_substitution_in_transformer().
transformer new_array_elements_backward_substitution_in_transformer | ( | transformer | , |
entity | , | ||
type | , | ||
expression | , | ||
transformer | , | ||
list | |||
) |
transformer new_array_elements_forward_substitution_in_transformer | ( | transformer | , |
entity | , | ||
type | , | ||
expression | , | ||
transformer | , | ||
list | |||
) |
transformer new_array_elements_substitution_in_transformer | ( | transformer | , |
entity | , | ||
type | , | ||
expression | , | ||
transformer | , | ||
list | , | ||
bool | |||
) |
transformer new_complete_whileloop_transformer | ( | transformer | t_body_star, |
transformer | pre, | ||
whileloop | wl, | ||
bool | entered_p | ||
) |
entered_p is used to for the execution of at least one iteration
t_body_star | _body_star |
pre | re |
wl | l |
entered_p | ntered_p |
Definition at line 1833 of file loop.c.
References new_complete_whileloop_transformer_list(), and transformer_list_to_transformer().
Referenced by complete_whileloop_transformer(), and generic_complete_statement_transformer().
list new_complete_whileloop_transformer_list | ( | transformer | , |
transformer | , | ||
whileloop | , | ||
bool | |||
) |
transformer new_loop_to_transformer | ( | loop | l, |
transformer | pre, | ||
list | lel | ||
) |
loop_to_transformer() was developed first but is not as powerful as the new algorithm used for all kinds of loops.
See flip-flop01.c.
Equation:
t_body_star = t_init ; t_enter ;(t_body ; t_inc; t_continue)*
t_init, t_enter and t_continue, which includes t_inc, must be computed from the loop and its precondition, pre, and extended body effects, lel. In case the loop index appears in the bound or increment expressions, the Fortran standard should be used to determine the precondition to use. The same is true in case of side-effects in the loop expressions.
t_body must be computed from the loop body and a preliminary loop invariant.
Deal with initialization expression, which may be included in the condition as in while(i++, j=0, i<m)? No because the expression is going to be evaluated at each cycle. The ised effects must be part of the condition transformer, tcond
Deal with enter transformers
An effort could be made to compute the precondition for t_continue. Precondition pre and the loop effect list lel could be used.
approximate loop transformer, including loop index updates
first approximation of the loop body precondition
FI: could do better with body_transformer
Let's clean up the memory
pre | re |
lel | el |
Definition at line 1516 of file loop.c.
References any_loop_to_transformer(), effects_to_transformer(), free_transformer(), invariant_wrt_transformer(), loop_body, loop_to_continue_transformer(), loop_to_enter_transformer(), loop_to_initialization_transformer(), transformer_apply(), transformer_range(), and transformer_undefined.
transformer new_substitute_stubs_in_transformer | ( | transformer | tf, |
call | c, | ||
statement | s, | ||
bool | backward_p | ||
) |
This leads to an empty transformer because the statement is unreachable. Some kind of dereferencement error has occured earlier in the execution
tf | f |
backward_p | ackward_p |
Definition at line 417 of file points_to.c.
References free_points_to_graph(), free_transformer(), get_points_to_graph_from_statement(), make_points_to_graph(), points_to_graph_bottom, pt_to_list_undefined_p(), substitute_stubs_in_transformer_with_translation_binding(), transformer_empty(), and user_call_to_points_to_interprocedural_binding_set().
Referenced by c_user_call_to_transformer().
transformer new_whileloop_to_k_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel, | ||
int | k | ||
) |
t_body_star = t_init ; t_enter ;(t_body ; t_next)*
Deal with initialization expression
Deal with condition expression
An effort could be made to compute the precondition for t_continue.
Let's clean up the memory
wl | l |
pre | re |
wlel | lel |
k | effects of whileloop wl |
Definition at line 416 of file loop.c.
References any_loop_to_k_transformer(), condition_to_transformer(), free_transformer(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_k_transformer().
transformer new_whileloop_to_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel | ||
) |
effects of whileloop wl
Equation:
t_body_star = t_init ; t_enter ;(t_body ; t_continue)*
Deal with initialization expression, which may be included in the condition as in while(i++, j=0, i<m)? No because the expression is going to be evaluated at each cycle. The ised effects must be part of the condition transformer, tcond
Deal with condition expression
An effort could be made to compute the precondition for t_continue.
Let's clean up the memory
wl | l |
pre | re |
wlel | lel |
Definition at line 380 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), free_transformer(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_transformer().
bool non_empty_range_wrt_precondition_p | ( | range | r, |
transformer | p | ||
) |
Definition at line 121 of file utils.c.
References check_range_wrt_precondition().
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
Number of formal parameters in pl before a vararg is reached.
The varargs are not analyzed.
pl | l |
Definition at line 1518 of file ri_to_transformers.c.
References FOREACH, PARAMETER, parameter_type, pips_internal_error, pl, type_varargs_p, type_void_p, and ultimate_type().
Referenced by any_user_call_site_to_transformer().
transformer old_complete_whileloop_transformer | ( | transformer | ltf, |
transformer | pre, | ||
whileloop | l | ||
) |
loop body transformer
Recompute the exact loop body transformer. This is weird: it should have already been done by statement_to_transformer and propagated bask. However, we need to recompute it because it has not been stored and cannot be retrieved. It might be better to use complete_statement_transformer(retrieved t, preb, s).
Since it is not stored, we need to go down recursively. A way to avoid this would be to always have sequences as loop bodies... Let's hope that perfectly nested loops are neither frequent nor deep!
The proper transformer has been stored.
btf = transformer_add_condition_information(btf, cond, preb, true);
add the exit condition
add initialization for the unconditional initialization of the loop index variable
It might be better not to compute useless transformer, but it's more readable that way. Since pre is information free, only loops with constant lower and upper bound and constant increment can benefit from this.
ltf | tf |
pre | re |
Definition at line 2213 of file loop.c.
References complete_loop_transformer(), complete_whileloop_transformer(), condition_false_wrt_precondition_p(), condition_true_wrt_precondition_p(), external_value_name(), fprint_transformer(), free_transformer(), ifdebug, instruction_loop, instruction_whileloop, invariant_wrt_transformer(), load_statement_transformer(), pips_debug, print_transformer, statement_instruction, statement_loop_p(), statement_whileloop_p(), transformer_add_condition_information(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_identity(), transformer_undefined, transformer_undefined_p, whileloop_body, and whileloop_condition.
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().
bool path_transformer | ( | const | string | ) |
string | odule_name |
transformer path_transformer_on | ( | statement | , |
path | , | ||
path | , | ||
int | |||
) |
transformer pointer_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
This function may return an undefined transformers if it fails to capture the semantics of expr in the polyhedral framework. cf any_expression_to_transformer which call it
v | value of the expression |
expr | pointer expression |
pre | transformer, no side effect |
is_internal | ?? use in generic_reference_to_transformer |
Assume: v is a value
expr | xpr |
pre | re |
is_internal | s_internal |
Definition at line 4582 of file expression.c.
References basic_pointer_p, cast_expression, cast_type, compute_basic_concrete_type(), ENDP, entity_type, expression_multiply_sizeof_to_transformer(), expression_null_p(), expression_syntax, expression_to_type(), free_transformer(), free_type(), generic_reference_to_transformer(), ifdebug, is_syntax_call, is_syntax_cast, is_syntax_reference, null_pointer_value_entity(), pips_debug, pointer_call_expression_to_transformer(), print_expression(), reference_variable, semantics_user_warning, simple_equality_to_transformer(), syntax_cast, syntax_reference, syntax_tag, transformer_intersection(), transformer_undefined, transformer_undefined_p, type_equal_p(), type_variable, type_variable_p, variable_basic, variable_dimensions, and volatile_variable_p().
Referenced by any_expression_to_transformer().
transformer points_to_unary_operation_to_transformer | ( | entity | e, |
entity | op, | ||
expression | e1, | ||
transformer | pre, | ||
bool | is_internal, | ||
bool | is_pointer | ||
) |
This function is redundant with generic_unary_operation_to_transformer() except for its use of parameter is_pointer.
op | p |
e1 | 1 |
pre | re |
is_internal | s_internal |
is_pointer | s_pointer |
Definition at line 2770 of file expression.c.
References active_phase_p(), analyzed_reference_p(), CELL, cell_preference, cell_preference_p, cell_reference, cp, dump_transformer, ENTITY_DEREFERENCING_P, ENTITY_FIELD_P, entity_null_locations_p(), ENTITY_POINT_TO_P, entity_typed_nowhere_locations_p(), expression_to_string(), FOREACH, free_transformer(), gen_length(), generic_reference_to_transformer(), get_bool_property(), ifdebug, pips_debug, pips_user_error, preference_reference, pt_to_list_undefined_p(), reference_to_string(), reference_variable, semantics_expression_to_points_to_sinks(), semantics_user_warning, test_warning_counters(), transformer_convex_hull(), transformer_empty(), transformer_undefined, and transformer_undefined_p.
bool postcondition_map_undefined_p | ( | void | ) |
transformer precondition_add_condition_information | ( | transformer | pre, |
expression | c, | ||
transformer | context, | ||
bool | veracity | ||
) |
context might be derivable from pre as transformer_range(pre) but this is sometimes very computationally intensive, e.g.
in ocean.
pre | re |
context | ontext |
veracity | eracity |
Definition at line 1111 of file expression.c.
References ENDP, free_transformer(), reset_temporary_value_counter(), transformer_add_condition_information_updown(), transformer_arguments, transformer_range(), transformer_temporary_value_projection(), transformer_undefined, and transformer_undefined_p.
Referenced by dag_to_flow_sensitive_preconditions(), eval_condition_wrt_precondition_p(), load_arc_precondition(), process_ready_node(), standard_whileloop_to_transformer(), transformer_add_range_condition(), unstructured_to_postconditions(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
void precondition_add_reference_information | ( | transformer | pre, |
statement | s | ||
) |
pre | re |
Definition at line 695 of file ri_to_preconditions.c.
References add_reference_information().
Referenced by statement_to_postcondition().
void precondition_add_type_information | ( | transformer | pre | ) |
pre | re |
Definition at line 705 of file ri_to_preconditions.c.
References transformer_add_type_information().
transformer precondition_filter_old_values | ( | transformer | pre | ) |
pre | re |
Definition at line 1065 of file loop.c.
References BASE_NULLE_P, BASE_UNDEFINED, old_value_entity_p(), pips_assert, predicate_system, transformer_relation, vecteur_succ, and vecteur_var.
transformer precondition_intra_to_inter | ( | entity | callee, |
transformer | pre, | ||
list | le | ||
) |
precondition cannot be printed because equations linking formal parameters have been added to the real precondition
make sure you do not export a (potentially) meaningless old value
Thru DATA statements, old values of other modules may appear
get rid of old_values
sc_elim_redund
no_elim
get rid of pre's variables that do not appear in effects le
we should not have to know about these internal objects, Psysteme and Pvecteur!
build a list of values to suppress
get rid of variables that are not referenced, directly or indirectly, by the callee; translate what you can
For clarity, all cases are presented
No need to substitute or eliminate this value
This is a short term improvement for partial_eval01-02 that works only for values local to the callee not for values updated indirectedly by callees of "callee".
It resulted in many core dumps in array privatization
no conflicts
list of conflicting entities
case 1: only one entity
case 1.1: one conflicting integer entity
Type mismatch
case 1.22: one conflicting non analyzable scalar entity
case 2: at least 2 conflicting entities
case 2.1: all entities have the same type, according to mapping_values the subtitution is made with the first list element e_callee
case 2.2: all entities do not have the same type
Get rid of variables local to the caller
Get rid of unused or untouched variables, even though they may appear as global variables or formal parameters
This happens with automatically generated modules and for routine XERCLT in KIVA (Renault) because it has been emptied.
No information but feasibility can be preserved
Get rid of the basis and arguments to define the empty set
No information: the all value space is OK
sc_elim_redund
no_elim
free the temporary list of entities
get rid of arguments because they are meaningless for a module precondition: v_new == v_old by definition
callee | allee |
pre | re |
le | e |
Definition at line 395 of file interprocedural.c.
References analyzable_scalar_entity_p(), arguments_add_entity(), arguments_difference(), Ssysteme::base, base_contains_variable_p(), c_language_module_p(), callee, CAR, concrete_effects_entities_which_may_conflict_with_scalar_entity(), DEBUG_PRECONDITION_INTRA_TO_INTER, dump_arguments(), dump_transformer, ENDP, ENTITY, entity_constant_p, entity_module_name(), entity_name, entity_to_old_value(), entity_type, fortran_language_module_p(), free_transformer(), gen_free_list(), gen_length(), get_current_module_entity(), ifdebug, local_entity_of_module_p(), module_local_name(), NIL, pips_debug, POP, predicate_system, print_effects, same_analyzable_type_scalar_entity_list_p(), same_string_p, sc_safe_normalize(), Svecteur::succ, transformer_arguments, transformer_empty(), transformer_empty_p(), transformer_identity(), transformer_projection_with_redundancy_elimination(), transformer_relation, transformer_value_substitute(), translate_global_values(), type_equal_p(), and vecteur_var.
Referenced by add_module_call_site_precondition(), call_site_to_module_precondition_text(), and process_call_for_summary_precondition().
bool precondition_map_undefined_p | ( | void | ) |
bool precondition_minmax_of_expression | ( | expression | exp, |
transformer | tr, | ||
intptr_t * | pmin, | ||
intptr_t * | pmax | ||
) |
compute integer bounds pmax
, pmin
of expression exp
under preconditions tr
require value mappings set !
create a temporary value
compute its preconditions
tidy & return
exp | xp |
tr | r |
pmin | min |
pmax | max |
Definition at line 5818 of file expression.c.
References basic_of_expression(), exp, free_basic(), free_entity(), free_transformer(), make_local_temporary_value_entity_with_basic(), precondition_minmax_of_value(), predicate_system, safe_any_expression_to_transformer(), transformer_apply(), and transformer_relation.
Referenced by bounds_of_expression(), integer_minmax_to_transformer(), integer_power_to_transformer(), partial_eval_min_or_max_operator(), and simplify_minmax_expression().
bool precondition_minmax_of_value | ( | entity | val, |
transformer | tr, | ||
intptr_t * | pmin, | ||
intptr_t * | pmax | ||
) |
compute integer bounds pmax
, pmin
of value val
under preconditions tr
require value mappings set !
retrieve the associated psysteme
compute min / max bounds
special case to handle VMIN and VMAX in 32 bits
val | al |
tr | r |
pmin | min |
pmax | max |
Definition at line 5790 of file expression.c.
References intptr_t, pips_assert, predicate_system, sc_dup(), sc_minmax_of_variable(), transformer_relation, VALUE_MAX, and VALUE_MIN.
Referenced by add_type_information(), bitwise_xor_to_transformer(), integer_left_shift_to_transformer(), logical_binary_function_to_transformer(), logical_not_to_transformer(), modulo_by_a_constant_to_transformer(), and precondition_minmax_of_expression().
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 print_call_graph_with_preconditions | ( | const | string | ) |
string | odule_name |
Definition at line 712 of file prettyprint.c.
References get_text_preconditions(), module_name(), and print_decorated_call_graph().
bool print_call_graph_with_total_preconditions | ( | const | string | ) |
string | odule_name |
Definition at line 722 of file prettyprint.c.
References get_text_total_preconditions(), module_name(), and print_decorated_call_graph().
bool print_call_graph_with_transformers | ( | const | string | ) |
string | odule_name |
Definition at line 702 of file prettyprint.c.
References get_text_transformers(), module_name(), and print_decorated_call_graph().
bool print_code_as_a_graph_preconditions | ( | const | string | ) |
string | od_name |
Definition at line 120 of file prettyprint.c.
References print_code_preconditions(), and set_bool_property().
bool print_code_as_a_graph_total_preconditions | ( | const | string | ) |
string | od_name |
Definition at line 144 of file prettyprint.c.
References print_code_total_preconditions(), and set_bool_property().
bool print_code_as_a_graph_transformers | ( | const | string | ) |
string | od_name |
Definition at line 99 of file prettyprint.c.
References print_code_transformers(), and set_bool_property().
bool print_code_preconditions | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 110 of file prettyprint.c.
References get_bool_property(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
Referenced by print_code_as_a_graph_preconditions().
bool print_code_total_preconditions | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 131 of file prettyprint.c.
References get_bool_property(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
Referenced by print_code_as_a_graph_total_preconditions().
bool print_code_transformers | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 90 of file prettyprint.c.
References is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
Referenced by print_code_as_a_graph_transformers().
void print_control_postcondition_map | ( | control_mapping | control_postcondition_map | ) |
unstructured.c
control_postcondition_map | ontrol_postcondition_map |
Definition at line 294 of file unstructured.c.
References control_statement, fprintf(), HASH_MAP, hash_table_entry_count(), pips_assert, print_transformer, and statement_identification().
Referenced by dag_to_flow_sensitive_preconditions().
bool print_icfg_with_control_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_control_total_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_control_transformers | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_loops_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_loops_total_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_loops_transformers | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_total_preconditions | ( | const | string | ) |
string | odule_name |
bool print_icfg_with_transformers | ( | const | string | ) |
string | odule_name |
bool print_initial_precondition | ( | const | string | ) |
string | ame |
Definition at line 261 of file initial.c.
References db_get_memory_resource(), debug_off, debug_on, free_value_mappings(), make_text_resource_and_free(), module, module_name_to_entity(), module_to_value_mappings(), ok, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().
bool print_program_precondition | ( | const | string | ) |
A small function that would require pipsdbm and ri-util
string | ame |
Definition at line 293 of file initial.c.
References db_get_memory_resource(), debug_off, debug_on, free(), free_value_mappings(), get_main_entity_name(), make_text_resource_and_free(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), ok, pips_debug, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), and text_transformer().
bool print_source_preconditions | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 164 of file prettyprint.c.
References get_bool_property(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
bool print_source_total_preconditions | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 174 of file prettyprint.c.
References get_bool_property(), is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
bool print_source_transformers | ( | const char * | module_name | ) |
module_name | odule_name |
Definition at line 155 of file prettyprint.c.
References is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, module_name(), and print_code_semantics().
void print_statement_temporary_precondition | ( | statement_mapping | statement_temporary_precondition_map | ) |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 1006 of file unstructured.c.
References fprintf(), HASH_MAP, hash_table_entry_count(), pips_assert, print_transformer, and statement_identification().
Referenced by dag_to_flow_sensitive_preconditions().
The program correctness postcondition cannot be infered.
It should be provided by the user.
A small function that would require pipsdbm and ri-util
name | ame |
Definition at line 233 of file initial.c.
References DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, free(), get_main_entity_name(), ifdebug, module_local_name(), module_name_to_entity(), pips_assert, pips_debug, pred_debug, transformer_consistency_p(), and transformer_identity().
bool program_precondition | ( | const | string | ) |
Compute the union of all initial preconditions.
A small function that would require pipsdbm and ri-util
e_inter = effects_to_list(get_cumulated_rw_effects(get_current_module_statement()));
Unavoidable pitfall: initializations in uncalled modules may be taken into account. It all depends on the "create" command.
no dup & false => core
modifies tm!
tm = transformer_normalize(tm, 2);
string | ame |
Definition at line 134 of file initial.c.
References db_get_memory_resource(), db_get_module_list(), DB_PUT_MEMORY_RESOURCE, debug_off, debug_on, effects_to_list(), entity_undefined, free(), free_statement_global_stack(), free_transformer(), free_value_mappings(), gen_array_full_free(), gen_array_item(), gen_array_nitems(), get_main_entity_name(), ifdebug, intersect(), make_statement_global_stack(), module_local_name(), module_name_to_entity(), module_to_value_mappings(), NIL, pips_assert, pips_debug, pips_internal_error, pred_debug, print_transformer, reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), transformer_consistency_p(), transformer_dup(), transformer_identity(), transformer_intra_to_inter(), and translate_global_values().
transformer propagate_preconditions_in_declarations | ( | list | dl, |
transformer | pre, | ||
void(*)(expression, transformer) | process_initial_expression | ||
) |
This function is mostly copied from declarations_to_transformer().
It is used to recompute intermediate preconditions and to process the initialization expressions with the proper precondition. For instance, in:
int i = 10, j = i+1, a[i], k = foo(i);
you need to collect information about i's value to initialize j, dimension a and compute the summary precondition of function foo().
We assume that the precondition does not change within the expression as in:
int k = i++ + foo(i);
I do not remember if the standard prohibits this or not, but it may well forbid such expressions or state that the result is undefined.
But you can also have:
int a[i++][foo(i)];
or
int a[i++][j=foo(i)];
and the intermediate steps are overlooked by declaration_to_transformer() but can be checked with a proper process_dimensions() function.
This function can be called from ri_to_preconditions.c to propagate preconditions or from interprocedural.c to compute summary preconditions. In the second case, the necessary side effects are provided by the two functional parameters.
post = transformer_safe_normalize(post, 4);
post = transformer_safe_normalize(post, 4);
btf = transformer_normalize(btf, 4);
dl | l |
pre | re |
Definition at line 977 of file ri_to_preconditions.c.
References CAR, copy_transformer(), declaration_to_transformer(), ENDP, ENTITY, expression_undefined_p, free_expression(), free_transformer(), ifdebug, pips_assert, pips_debug, POP, stf(), transformer_combine(), transformer_consistency_p(), transformer_dup(), transformer_normalize(), transformer_safe_apply(), transformer_safe_normalize(), transformer_undefined, transformer_undefined_p, and variable_initial_expression().
Referenced by memorize_precondition_for_summary_precondition().
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().
transformer repeatloop_to_postcondition | ( | transformer | pre, |
whileloop | wl, | ||
transformer | t_body_star | ||
) |
An effort could be made to compute the precondition for t_exit, especially if the precondition to t_inc is available.
The repeat loop does not fit well in the current generic approach. Most of the basic transformers such as t_init, t_skip, t_enter,... are meaningless. Instead of dealing with zero or at least one iteration, we have to deal with one or at least two.
post = (t_body_c ; t_exit)(pre) + (t_body_c ; t_continue ; t_body_star ; t_body_c ; t_exit)(pre)
where we assume that t_body_star includes the continuation condition.
Clean up memory
pre | re |
wl | l |
t_body_star | _body_star |
Definition at line 2760 of file loop.c.
References any_loop_to_postcondition(), complete_statement_transformer(), condition_to_transformer(), copy_transformer(), free_transformer(), load_statement_transformer(), transformer_apply(), transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by instruction_to_postcondition().
transformer repeatloop_to_transformer | ( | whileloop | wl, |
transformer | pre, | ||
list | wlel | ||
) |
effects of whileloop wl
t_body_star = t_init ; t_enter ; (t_body ; t_next)+
t_once = t_body; t_exit
t_repeat = t_body_star + t_once
An effort could be made to compute the precondition for t_continue, especially if the precondition to t_inc is available.
FI: it should be computed with the postcondition of the body
The loop is executed at least twice; FI: I'm note sure the twice is captured
FI: example dowhile02 seems to show this is wrong with t_next empty, in spite of the star
The loop is executed only once
global transformer
wl | l |
pre | re |
wlel | lel |
Definition at line 449 of file loop.c.
References any_loop_to_transformer(), condition_to_transformer(), copy_transformer(), load_statement_transformer(), transformer_combine(), transformer_convex_hull(), transformer_identity(), transformer_undefined, whileloop_body, and whileloop_condition.
Referenced by whileloop_to_transformer().
void reset_call_site_number | ( | void | ) |
Definition at line 1126 of file interprocedural.c.
References number_of_call_sites.
Referenced by ordinary_summary_precondition(), and summary_total_postcondition().
void reset_postcondition_map | ( | void | ) |
void reset_precondition_map | ( | void | ) |
Referenced by add_alias_pairs_for_this_caller(), any_complexities(), array_bound_check_interprocedural(), array_expansion(), bdsc_code_instrumentation(), comp_regions(), dsc_code_parallelization(), formal_array_resizing_bottom_up(), generic_module_name_to_transformers(), generic_print_xml_application(), hbdsc_parallelization(), ikernel_load_store(), isolate_statement(), kernel_data_mapping(), kernel_load_store_engine(), module_name_to_preconditions(), module_name_to_total_preconditions(), out_regions_from_caller_to_callee(), partial_eval(), pragma_outliner(), reset_convex_in_out_regions(), reset_convex_rw_regions(), reset_resources_for_module(), reset_static_phase_variables(), rice_dependence_graph(), sequence_dependence_graph(), solve_hardware_constraints(), and spire_distributed_unstructured_to_structured().
void reset_semantic_map | ( | void | ) |
Referenced by call_site_to_module_precondition_text(), get_semantic_text(), and update_precondition_with_call_site_preconditions().
void reset_total_precondition_map | ( | void | ) |
Referenced by module_name_to_total_preconditions(), and reset_static_phase_variables().
void reset_transformer_map | ( | void | ) |
Referenced by bdsc_code_instrumentation(), comp_regions(), continuation_conditions(), dsc_code_parallelization(), generic_module_name_to_transformers(), hbdsc_parallelization(), module_name_to_preconditions(), module_name_to_total_preconditions(), pragma_outliner(), reset_convex_in_out_regions(), reset_convex_rw_regions(), reset_static_phase_variables(), sequence_dependence_graph(), and spire_distributed_unstructured_to_structured().
transformer safe_any_assign_operation_to_transformer | ( | entity | tmp, |
list | args, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
tmp | mp |
args | rgs |
pre | re |
is_internal | s_internal |
Definition at line 575 of file expression.c.
References any_assign_operation_to_transformer(), transformer_identity(), and transformer_undefined_p.
transformer safe_any_expression_side_effects_to_transformer | ( | expression | e, |
transformer | p, | ||
bool | is_internal | ||
) |
Same as any_expression_side_effects_to_transformer() but effects are used to always generate a transformer.
FI: I do not know how effects should be used. It might be useful to allow special transformers using location abstraction to simplify the recurrence. Currently, effects are used or not. It might be necessary to use only some of them at a given time in the evaluation process as variables can be assigned almost anywhere in C.
is_internal | s_internal |
Definition at line 4947 of file expression.c.
References any_expression_side_effects_to_transformer(), expression_effects_to_transformer(), and transformer_undefined_p.
transformer safe_any_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
Always return a usable transformer.
Use effects if no better transformer can be found
expr | xpr |
pre | re |
is_internal | s_internal |
Definition at line 5156 of file expression.c.
References any_expression_to_transformer(), copy_transformer(), effect_list_can_be_safely_full_freed_p(), effects_to_transformer(), expression_to_proper_constant_path_effects(), free_transformer(), gen_full_free_list(), transformer_identity(), and transformer_undefined_p.
Referenced by add_index_bound_conditions(), addition_operation_to_transformer(), any_conditional_to_transformer(), any_expressions_to_transformer(), any_user_call_site_to_transformer(), bitwise_xor_to_transformer(), condition_to_transformer(), fortran_data_to_prec_for_variables(), logical_not_to_transformer(), modulo_to_transformer(), precondition_minmax_of_expression(), transformer_add_any_relation_information(), and update_cp_with_rhs_to_transformer().
transformer safe_assigned_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre | ||
) |
Always returns a fully defined transformer.
FI: The property to compute transformers in context is not taken into account to add information from pre within tf. pre is used to evaluate expr, but is not made part of tf.
Side effects in expression ?
expr | xpr |
pre | re |
Definition at line 2651 of file ri_to_transformers.c.
References assigned_expression_to_transformer(), entity_has_values_p(), entity_type, expression_effects_to_transformer(), expression_undefined_p, free_transformer(), get_bool_property(), pips_assert, transformer_add_modified_variable_entity(), transformer_combine(), transformer_consistency_p(), transformer_identity(), transformer_range(), transformer_undefined, transformer_undefined_p, and type_with_const_qualifier_p().
Referenced by declaration_to_transformer(), and declaration_to_transformer_list().
list safe_assigned_expression_to_transformer_list | ( | entity | v, |
expression | expr, | ||
transformer | pre | ||
) |
Always returns a fully defined transformer.
FI: The property to compute transformers in context is not taken into account to add information from pre within tf. pre is used to evaluate expr, but is not made part of tf.
expr | xpr |
pre | re |
Definition at line 610 of file ri_to_transformer_lists.c.
References assigned_expression_to_transformer(), entity_has_values_p(), expression_undefined_p, get_bool_property(), NIL, pips_assert, pips_internal_error, transformer_add_modified_variable_entity(), transformer_identity(), transformer_range(), transformer_undefined, transformer_undefined_p, and transformers_consistency_p().
transformer safe_expression_to_transformer | ( | expression | exp, |
transformer | pre | ||
) |
This simple function does not take points-to information into account. Furthermore, precise points-to information is not available when side effects occur as in comma expressions.
FI: I do not see a simple way out. I can try to fix partly the problem in statement_to_transformer where the effects are known... Or I can play safer and use an effect function that replaces dereferencements by anywhere effects.
See anywhere03.c as an example of the issue.
exp | xp |
pre | re |
Definition at line 5307 of file expression.c.
References entity_field_p(), exp, expression_reference(), expression_reference_p(), expression_to_proper_constant_path_effects(), expression_to_transformer(), gen_full_free_list(), reference_variable, transformer_identity(), transformer_undefined, and transformer_undefined_p.
Referenced by any_assign_to_transformer(), any_expressions_to_transformer(), assign_rhs_to_reflhs_to_transformer(), complete_forloop_transformer(), complete_forloop_transformer_list(), condition_to_transformer(), conditional_to_transformer(), dimensions_to_transformer(), expression_to_transformer(), expressions_to_transformer(), forloop_to_postcondition(), forloop_to_transformer(), and struct_reference_assignment_or_equality_to_transformer().
transformer safe_integer_expression_to_transformer | ( | entity | v, |
expression | expr, | ||
transformer | pre, | ||
bool | is_internal | ||
) |
Always return a defined transformer, using effects in case a more precise analysis fails.
Do check wrt to value mappings... if you are not dealing with interprocedural issues
expr | xpr |
pre | re |
is_internal | s_internal |
Definition at line 3552 of file expression.c.
References expression_effects_to_transformer(), integer_expression_to_transformer(), and transformer_undefined_p.
Referenced by expression_multiply_sizeof_to_transformer(), integer_binary_operation_to_transformer(), integer_left_shift_to_transformer(), integer_multiply_to_transformer(), loop_to_enter_transformer(), and transformer_add_condition_information_updown().
Definition at line 255 of file interprocedural.c.
References analyzable_scalar_entity_p(), CAR, CDR, ENDP, ENTITY, entity_type, MAP, and type_equal_p().
Referenced by precondition_intra_to_inter().
bool semantic_map_undefined_p | ( | void | ) |
prettyprint.c
this function name is VERY misleading - it should be changed, sometime FI
module | odule |
margin | argin |
stmt | tmt |
Definition at line 354 of file prettyprint.c.
References apply_number_to_statement(), attach_preconditions_decoration_to_text(), attach_total_preconditions_decoration_to_text(), attach_transformers_decoration_to_text(), filter_transformer(), HASH_UNDEFINED_VALUE, is_total_precondition, is_transformer, is_transformer_filtered, is_user_view, load_cumulated_rw_effects_list(), load_statement_semantic(), module, nts, pips_assert, statement_number, statement_undefined_p, text_transformer(), and transformer_undefined_p.
Referenced by get_semantic_text().
list semantics_expression_to_points_to_sinks | ( | expression | e | ) |
Returns a list of cells.
Definition at line 112 of file points_to.c.
References CELL, CONS, expression_to_points_to_sinks(), get_current_statement_from_statement_global_stack(), get_points_to_graph_from_statement(), list_undefined, make_anywhere_points_to_cell(), NIL, points_to_expression_to_concrete_type(), and pt_to_list_undefined_p().
Referenced by generic_unary_operation_to_transformer(), and points_to_unary_operation_to_transformer().
list semantics_expression_to_points_to_sources | ( | expression | e | ) |
points_to.c
points_to.c
FI: check if new cells are allocated to build the returned location list ll...
Definition at line 94 of file points_to.c.
References expression_to_points_to_sources(), get_current_statement_from_statement_global_stack(), get_points_to_graph_from_statement(), points_to_graph_undefined, pt_to_list_undefined_p(), and statement_undefined_p.
Referenced by any_assign_to_transformer(), any_basic_update_to_transformer(), any_update_to_transformer(), lhs_expression_to_transformer(), new_array_elements_backward_substitution_in_transformer(), new_array_elements_forward_substitution_in_transformer(), and struct_reference_assignment_or_equality_to_transformer().
bool semantics_usable_points_to_reference_p | ( | reference | rlhs, |
expression | lhs, | ||
int | n | ||
) |
See if references rlhs is usable and process null, undefined and anywhere locations defined by rlhs.
Expression lhs is passed to clarify the error and warning messages.
n is the number of alternative references. It is used to check the severity of unusable references. If n=1, a NULL rlhs implies a bug. If n>1, the points-to analysis could not determine precisely the target location.
This function is designed to check constant references in a loop over a list of references returned by the points-to analysis.
A heap location may represent several locations. p==heap ^ q==heap does not imply p==q
An anywhere location may represent several locations. p==heap ^ q==heap does not imply p==q
rlhs | lhs |
lhs | hs |
Definition at line 6194 of file expression.c.
References analyzed_type_p(), entity_anywhere_locations_p(), entity_heap_location_p(), entity_null_locations_p(), entity_typed_anywhere_locations_p(), entity_typed_nowhere_locations_p(), expression_to_string(), expression_undefined_p, ifdebug, pips_debug, pips_user_error, points_to_reference_to_concrete_type(), reference_to_string(), reference_variable, semantics_user_warning, type_struct_variable_p(), and type_variable_p.
Referenced by any_assign_to_transformer(), generic_unary_operation_to_transformer(), lhs_expression_to_transformer(), new_array_elements_backward_substitution_in_transformer(), new_array_elements_forward_substitution_in_transformer(), and struct_reference_assignment_or_equality_to_transformer().
void semantics_user_warning_func | ( | const char * | func_name, |
const char * | format, | ||
... | |||
) |
func_name | unc_name |
format | ormat |
Definition at line 118 of file misc.c.
References semantics_user_warning_alist().
void semantics_user_warning_func2 | ( | const char * | format, |
... | |||
) |
format | ormat |
Definition at line 129 of file misc.c.
References pips_unknown_function, and semantics_user_warning_alist().
void set_module_global_arguments | ( | list | args | ) |
args | rgs |
Definition at line 103 of file ri_to_preconditions.c.
References module_global_arguments.
Referenced by module_name_to_preconditions(), and module_name_to_total_preconditions().
void set_postcondition_map | ( | statement_mapping | ) |
void set_precondition_map | ( | statement_mapping | ) |
Referenced by add_alias_pairs_for_this_caller(), any_complexities(), array_bound_check_interprocedural(), array_expansion(), bdsc_code_instrumentation(), comp_regions(), dsc_code_parallelization(), formal_array_resizing_bottom_up(), generic_module_name_to_transformers(), generic_print_xml_application(), hbdsc_parallelization(), ikernel_load_store(), init_convex_in_out_regions(), init_convex_rw_regions(), init_use_preconditions(), isolate_statement(), kernel_data_mapping(), kernel_load_store_engine(), module_name_to_preconditions(), module_name_to_total_preconditions(), out_regions_from_caller_to_callee(), pragma_outliner(), rice_dependence_graph(), sequence_dependence_graph(), set_resources_for_module(), solve_hardware_constraints(), and spire_distributed_unstructured_to_structured().
void set_prettyprint_transformer | ( | void | ) |
Definition at line 77 of file prettyprint.c.
References is_total_precondition, is_transformer, and is_transformer_filtered.
void set_semantic_map | ( | statement_mapping | ) |
Referenced by call_site_to_module_precondition_text(), get_semantic_text(), and update_precondition_with_call_site_preconditions().
void set_total_precondition_map | ( | statement_mapping | ) |
void set_transformer_map | ( | statement_mapping | ) |
Referenced by bdsc_code_instrumentation(), comp_regions(), continuation_conditions(), dsc_code_parallelization(), generic_module_name_to_transformers(), hbdsc_parallelization(), init_convex_in_out_regions(), init_convex_rw_regions(), module_name_to_preconditions(), module_name_to_total_preconditions(), pragma_outliner(), sequence_dependence_graph(), and spire_distributed_unstructured_to_structured().
void set_warning_counters | ( | void | ) |
Definition at line 903 of file dbm_interface.c.
References wc.
Referenced by generic_module_name_to_transformers().
transformer simple_affine_to_transformer | ( | entity | e, |
Pvecteur | a, | ||
bool | is_internal | ||
) |
INTEGER EXPRESSIONS.
FI: I do no longer understand the semantics of "is_internal"... although I designed it. The intent was probably to manage temporary values: they should be preserved as long as the analysis is internal and else projected.
Furthermore, this function is no longer very useful as normalization can be performed dynamically again and again at a low cost.
The renaming from variables in a to new values in ve and vexpr is performed as a side-effect by value_mappings_compatible_vector_p() which fails when a renaming fails.
This is very dangerous when is_internal==false
is_internal | s_internal |
Definition at line 1167 of file expression.c.
References bool_to_string(), contrainte_make(), CONTRAINTE_UNDEFINED, dump_transformer, eq, ifdebug, make_predicate(), make_transformer(), NIL, pips_debug, sc_make(), transformer_undefined, value_mappings_compatible_vector_p(), VALUE_ONE, vect_dump(), vect_dup(), vect_new(), vect_rm(), vect_substract(), and VECTEUR_NUL.
Referenced by integer_expression_to_transformer().
bool simple_dead_loop_p | ( | expression | lower, |
expression | upper | ||
) |
lower | ower |
upper | pper |
Definition at line 1028 of file loop.c.
References NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, term_cst, value_gt, value_neg_p, value_pos_p, VECTEUR_NUL_P, vecteur_succ, and vecteur_val.
Referenced by add_index_range_conditions().
int simplify_boolean_expression_with_precondition | ( | expression | e, |
transformer | p | ||
) |
Simplification of bool expressions with precondition.
Expression e is modified, if necessary, by side effect.
The value returned is 1 if the expression e is always true (never false) under condition p, 0 if is the expression is always false (never true), and -1 otherwise.
This function is not used within the semantics library. It is exported for partial_eval and suppress_dead_code or similar passes.
Because of C flexibility, all kinds of "boolean" expressions may arise. Think of the conditional and comma operators, think of all kinds of side effects, think of integer expressions,...
FI: In the short term, I only need to deal with bool operators and, or and not.
Definition at line 6080 of file expression.c.
References call_arguments, call_function, CAR, CDR, condition_to_transformer(), copy_expression(), ENTITY_AND_P, ENTITY_NOT_P, ENTITY_OR_P, EXPRESSION, expression_syntax, logical_operator_expression_p(), make_false_expression(), make_true_expression(), replace_expression_content(), syntax_call, and transformer_empty_p().
void simplify_minmax_expression | ( | expression | e, |
transformer | tr | ||
) |
tries hard to simplify expression e
if it is a min or a max operator, by evaluating it under preconditions tr
.
Two approaches are tested: check bounds of lhs-rhs, or compare bounds of lhs and rhs
tr | r |
Definition at line 5849 of file expression.c.
References binary_call_lhs, binary_call_rhs, call_function, copy_expression(), ENTITY_MAX_P, expression_call(), expression_minmax_p(), intptr_t, is_max, local_assign_expression(), make_op_exp(), MINUS_OPERATOR_NAME, and precondition_minmax_of_expression().
Referenced by do_array_expansion(), do_solve_hardware_constraints_on_nb_proc(), and region_to_minimal_dimensions().
transformer standard_whileloop_to_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e | ||
) |
This function computes the effect of K loop iteration, with K positive.
This function does not take the loop exit into account because its result is used to compute the precondition of the loop body. Hence the loop exit condition only is added when preconditions are computed. This is confusing when transformers are prettyprinted with the source code.
loop transformer tf = tfb* or tf = tfb+ or ...
loop body transformer
Make sure not to leave too much information in pre. Perform a very simplistic fix point based on effects.
If the while entry condition is usable, it must be added on the old values
I'd like to use pre_n as context to evaluate the condition cond, but I'm not sure it's safe (Francois Irigoin)
Side effects in cond are ignored!
compute the whileloop body transformer, including the initial conditions
The convex hull of the image of pre and of the image of tfb can be added as conditions on tfb's domain, if some information is available in pre
compute tfb's fix point according to pips flags
The second clause is probably stronger than the first one
The loop is never entered
Side effects of the condition evaluation should be taken into account
A temporary variable is expected as first argument. There is something to fix.
tf = any_expression_to_transformer();
The loop is never exited, e.g. because there is a STOP or an infinite loop inside
Dirty looking fix for a fix point computation error: sometimes, the basis is restricted to a subset of the integer scalar variables. Should be useless with proper fixpoint opertors.
we have a problem here: to compute preconditions within the whileloop body we need a tf using private variables; to return the loop transformer, we need a filtered out tf; only one hook is available in the ri..; let'a assume there are no private variables and that if they are privatizable they are not going to get in our way
basic cheap version: do not use the whileloop body transformer and avoid fix-points; local variables do not have to be filtered out because this was already done while computing effects
The loop body transformers could benefit from pre_n instead of transformer_undefined, but who would think of combining these two options?
pre | re |
Definition at line 2456 of file loop.c.
References condition_false_wrt_precondition_p(), effects_to_transformer(), external_value_name(), fprint_transformer(), fprintf(), free_transformer(), ifdebug, invariant_wrt_transformer(), loop_body_transformer_add_entry_and_iteration_information(), pips_debug, pips_flag_p, precondition_add_condition_information(), predicate_system, print_transformer, sc_append(), SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_transformer(), transformer_dup(), transformer_empty(), transformer_empty_p(), transformer_equality_fix_point(), transformer_fix_point_operator, transformer_halbwachs_fix_point(), transformer_identity(), transformer_relation, transformer_undefined, transformer_undefined_p, whileloop_body, and whileloop_condition.
Return true if statement s is reachable according to its precondition.
Definition at line 92 of file utils.c.
References parametric_statement_feasible_p(), and transformer_empty_p().
Return true if statement s is reachable according to its precondition.
Definition at line 99 of file utils.c.
References parametric_statement_feasible_p(), and transformer_strongly_empty_p().
Referenced by set_methods_for_convex_effects(), and set_methods_for_convex_rw_pointer_effects().
transformer statement_to_postcondition | ( | transformer | pre, |
statement | s | ||
) |
end of the non recursive section
Refine the precondition pre of s using side effects and compute its postcondition post.
Postcondition post is returned.
FI: if the statement s is a loop, the transformer tf is not the statement transformer but the transformer T* which maps the precondition pre onto the loop body precondition. The real statement transformer is obtained by executing the loop till it is exited. See complete_any_loop_transformer()
ACHTUNG! "pre" is likely to be misused! FI, Sept. 3, 1990
To provide information for warnings
FC: if the code is not reachable (thanks to STOP or GOTO), which is a structural information, the precondition is just empty.
keep only global initial scalar integer values; else, you might end up giving the same xxx::old name to two different local values
FI: OK, to be fixed when the declaration representation is frozen.
add array references information
add type information
Add information from declarations when useful
FI: it might be better to have another function, declarations_to_postconditions(), which might be slightly more accurate? Note that declarations_to_transformer() does compute the postcondition, but free it before returning the transformer
Remove information when leaving a block
add equivalence equalities
eliminate redundancy, rational redundancy but not integer redundancy.
FI: nice... but time consuming!
Version 3 is OK. Equations are over-used and make inequalities uselessly conplex
pre = transformer_normalize(pre, 3);
pre = transformer_normalize(pre, 6);
pre = transformer_normalize(pre, 7);
The double normalization could be avoided with a non-heuristics approach. For ocean, its overhead is 34s out of 782.97 to give 816.62s: 5 %. The double normalization is also useful for some exit conditions of WHILE loops (w05, w06, w07). It is not powerful enough for preconditions containing equations with three or more variables such as fraer01,...
BC: pre = transformer_normalize(pre, 4);
FI->BC: why keep a first normalization before the next one? FI: Because a level 2 normalization does things that a level 4 does not perform! Although level 2 is much faster...
pre = transformer_normalize(pre, 2);
Do not keep too many initial variables in the preconditions: not so smart? invariance01.c: information is lost... Since C passes values, it is usually useless to keep track of the initial values of arguments because programmers usually do not modify them. However, when they do modify the formal parameter, information is lost.
See character01.c, but other counter examples above about non_initial_values.
FI: redundancy possibly added. See asopt02. Maybe this should be moved up before the normalization step.
store the precondition in the ri
pre = statement_precondition(s);
post = instruction_to_postcondition(pre, i, tf);
pre | re |
s | postcondition of predecessor |
Definition at line 712 of file ri_to_preconditions.c.
References arguments_difference(), CAR, declaration_statement_p(), declarations_to_transformer(), empty_transformer(), ENDP, ENTITY, ENTITY_, entity_to_old_value(), fprintf(), gen_free_list(), get_bool_property(), get_int_property(), get_module_global_arguments(), ifdebug, instruction_identification(), instruction_to_postcondition(), load_statement_precondition(), load_statement_transformer(), loop_index, MAPL, NIL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, pips_user_warning, pop_statement_global_stack(), precondition_add_reference_information(), print_transformer, push_statement_on_statement_global_stack(), safe_transformer_projection(), statement_block_p, statement_declarations, statement_instruction, statement_loop(), statement_loop_p(), statement_number, statement_ordering, statement_reachable_p(), store_statement_precondition(), tf_equivalence_equalities_add(), transformer_add_type_information(), transformer_apply(), transformer_arguments, transformer_consistency_p(), transformer_filter(), transformer_normalize(), transformer_undefined, variable_to_values(), and variables_to_values().
Referenced by any_loop_to_postcondition(), block_to_postcondition(), dag_to_flow_sensitive_preconditions(), loop_to_postcondition(), module_name_to_preconditions(), process_unreachable_node(), test_to_postcondition(), unstructured_to_postcondition(), unstructured_to_postconditions(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
transformer statement_to_total_precondition | ( | transformer | t_post, |
statement | s | ||
) |
phasis 3: propagate total preconditions from statement to sub-statement, starting from the module unique return statement. Total preconditions are over-approximation of the theoretical total preconditions, i.e. the conditions that must be met by the store before a statement is executed to reach the end of the module (intra-procedural) or the end of the program (interprocedural). Since over-approximations are computed, the end of the module or of the program cannot be reached if it is not met.
For (simple) interprocedural analysis, this phasis should be performed top-down on the call tree.
Most functions are called xxx_to_total_precondition. They receive a total postcondition as input and use a transformer to convert it into a total precondition.
Total preconditions are NEVER shared. Sharing would introduce desastrous side effects when they are updated as for equivalenced variables and would make freeing them impossible. Thus on a recursive path from statement_to_total_precondition() to itself the precondition must have been reallocated even when its value is not changed as between a block precondition and the first statement of the block precondition. In the same way statement_to_total_precondition() should never returned a total_precondition aliased with its precondition argument. Somewhere in the recursive call down the data structures towards call_to_total_precondition() some allocation must take place even if the statement as no effect on preconditions.
Ambiguity: the type "transformer" is used to abstract statement effects as well as effects combined from the beginning of the module to just before the current statement (precondition) to just after the current statement (total_precondition). This is because it was not realized that preconditions could advantageously be seen as transformers of the initial state when designing the ri. include <stdlib.h>
Preconditions may be useful to deal with tests and loops and to find out if some control paths do not exist
transformer context = transformer_undefined;
If the code is not reachable, thanks to STOP or GOTO, which is a structural information, the total precondition is just empty.
keep only global initial scalar integer values; else, you might end up giving the same xxx::old name to two different local values (?)
add equivalence equalities
t_pre = transformer_normalize(t_pre, 4);
store the total precondition in the ri
t_post | _post |
Definition at line 355 of file ri_to_total_preconditions.c.
References arguments_difference(), CAR, ENTITY, ENTITY_, entity_to_old_value(), fprintf(), free_transformer(), gen_free_list(), get_module_global_arguments(), ifdebug, instruction_to_total_precondition(), list_undefined, load_statement_precondition(), load_statement_total_precondition(), load_statement_transformer(), MAPL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, print_transformer, statement_instruction, statement_number, statement_ordering, statement_reachable_p(), store_statement_total_precondition(), tf_equivalence_equalities_add(), transformer_arguments, transformer_consistency_p(), transformer_empty(), transformer_filter(), transformer_normalize(), transformer_range(), and transformer_undefined.
Referenced by block_to_total_precondition(), loop_to_total_precondition(), module_name_to_total_preconditions(), test_to_total_precondition(), and unstructured_to_total_precondition().
transformer statement_to_transformer | ( | statement | s, |
transformer | spre | ||
) |
stmt precondition
old transformer for s
new transformer for s under spre
nt updated with loop exit information
Transformation REFINE_TRANSFORMERS is being executed: add information available from the statement precondition
it would be nicer to control warning_on_redefinition
FI: OK, we will have to switch to the new declaration representation some day, but the old representation is still fine.
not very smart because declarations_to_transformer() computes post and free it...
add type information
FI: how do we want to handle declarations:
int i = 1; => T() {i==1}
or
int i = 1; => T(i) {i==1}
What is the impact of this choice? BC prefers the second one because it it consistent for convex effect computation.
Note: this issue could be dealt with earlier in declarations_to_transformer()
FI: the code below might be useful again when declarations are carried by any kind of statement
Option 1
Option 2, currently bugged
Currently, the preconditions is useless as only the effects will be used to compute the CONTINUE transformer.
Remove information cancelled by abstract effects
This correction should be moved down in test_to_transformer(), loop_to_transformer() and call_to_transformer() to reduce its impact. See Ticket 792.
add array references information using proper effects
nt = transformer_normalize(nt, 0);
add type information
nt = transformer_normalize(nt, 0);
When we leave a block the local stack allocated variables disappear
Get rid of the dynamic and stack variables declared in this block statement. No stack variable should be analyzed as the stack area is used only for dependent types.
nt = transformer_normalize(nt, 7);
nt = transformer_normalize(nt, 4);
(void) print_transformer(load_statement_transformer(s));
When the statement is virtually replicated via control nodes, the statement transformer is the convex hull of all its replicate transformers.
This implies that transformers are computed in context and that we are dealing with a non-deterministic unstructured with several nodes for a unique statement.
Written abstract locations may require some information destruction
The current implementation is too crude. A new function is needed, abstract_effects_to_transformer(). The current implementation is OK for anywhere effects.
Also, abstract effects should not be applied several times. For instance, a block statement cannot add new effects that have not already been taken into account. A test or a loop only add abstract effects linked to the condition or the loop control. Which leaves us mostly with call statements. Which means that abstract effects should be taken into account at a lower level.
This is mathematically correct but very inefficient (see ticket 644) and useless as long anymodule:anywhere is the only abstract effect we have to deal with.
Not a sufficient solution: free_transformer(t); t = etf;
store or update the statement transformer
delete_statement_transformer(s);
store_statement_transformer(s, t);
The transformer returned for the statement is not always the transformer stored for the statement. This happens for loops and for context sensitive transformers for replicated statements in CFG/unstructured. See comments in loop.c
spre | pre |
Definition at line 3759 of file ri_to_transformers.c.
References all_statements_defined_p(), apply_abstract_effects_to_transformer(), complete_statement_transformer(), copy_transformer(), declaration_statement_p(), declarations_to_transformer(), dump_transformer, dynamic_variables_to_values(), effects_abstract_location_p(), ENDP, fprintf(), free_transformer(), get_bool_property(), get_int_property(), ifdebug, instruction_to_transformer(), load_cumulated_rw_effects_list(), load_statement_precondition(), load_statement_transformer(), NIL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, pop_statement_global_stack(), print_transformer, push_statement_on_statement_global_stack(), refine_transformers_p, safe_transformer_projection(), semantics_user_warning, statement_block_p, statement_declarations, statement_global_stack_defined_p(), statement_instruction, statement_number, statement_ordering, stf(), store_statement_transformer(), transformer_add_reference_information(), transformer_add_type_information(), transformer_apply(), transformer_consistency_p(), transformer_consistent_p(), transformer_convex_hull(), transformer_domain_intersection(), transformer_free(), transformer_identity(), transformer_image_intersection(), transformer_internal_consistency_p(), transformer_normalize(), transformer_range(), transformer_to_local_values(), transformer_undefined, transformer_undefined_p, and update_statement_transformer().
Referenced by any_loop_to_k_transformer(), block_to_transformer(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), generic_module_name_to_transformers(), loop_to_transformer(), process_ready_node(), process_unreachable_node(), standard_whileloop_to_transformer(), test_to_transformer(), test_to_transformer_list(), unreachable_node_to_transformer(), and unstructured_to_transformers().
list statement_to_transformer_list | ( | statement | s, |
transformer | spre | ||
) |
A transformer is already available for statement s, but it is going to be refined into a list of transformers to isolate at least the identity transformer from effective transformers.
stmt precondition
Transformation REFINE_TRANSFORMERS is being executed: add information available from the statement precondition
it would be nicer to control warning_on_redefinition
FI: an empty tl means that s does not return. An undefined tl means that instruction_to_transformer() is not implemented in a satisfactory way. So the existing transformer is used by default.
add array references information using proper effects
nt = transformer_normalize(nt, 0);
When we leave a block the local stack allocated variables disappear
Get rid of the dynamic and stack variables declared in this block statement. No stack variable should be analyzed as the stack area is used only for dependent types.
nt = transformer_normalize(nt, 7);
nt = transformer_normalize(nt, 4);
(void) print_transformer(load_statement_transformer(s));
The transformer returned for the statement is not always the transformer stored for the statement. This happens for loops and for context sensitive transformers for replicated statements in CFG/unstructured. See comments in loop.c
spre | pre |
Definition at line 978 of file ri_to_transformer_lists.c.
References all_statements_defined_p(), CONS, copy_transformer(), declaration_statement_p(), declarations_to_transformer(), dump_transformer, dynamic_variables_to_values(), ENDP, FOREACH, fprintf(), free_transformer(), gen_length(), get_bool_property(), get_int_property(), ifdebug, instruction_to_transformer_list(), list_undefined_p, load_cumulated_rw_effects_list(), load_statement_precondition(), load_statement_transformer(), NIL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, print_transformer, print_transformers(), refine_transformers_p, safe_transformer_projection(), semantics_user_warning, statement_block_p, statement_declarations, statement_instruction, statement_number, statement_ordering, store_statement_transformer(), TRANSFORMER, transformer_add_reference_information(), transformer_consistency_p(), transformer_consistent_p(), transformer_convex_hull(), transformer_domain_intersection(), transformer_free(), transformer_identity(), transformer_internal_consistency_p(), transformer_normalize(), transformer_range(), transformer_undefined, transformer_undefined_p, and update_statement_transformer().
Referenced by block_to_transformer_list(), test_to_transformer_list(), and whileloop_to_postcondition().
utils.c
utils.c
bool feasible_p = !transformer_empty_p(pre);
FI: this test is much stronger than I intended. I just wanted to check that the predicate of pre was exactly sc_empty()!
Now I'm afraid to change it. suppress_dead_code isn't that slow on ocean. I'm not sure that I could validate Transformations.
Definition at line 72 of file utils.c.
References load_statement_precondition(), predicate_system, sc_empty_p(), and transformer_relation.
Referenced by interprocedural_abc_arrays().
void store_statement_postcondition | ( | statement | , |
transformer | |||
) |
void store_statement_precondition | ( | statement | , |
transformer | |||
) |
void store_statement_semantic | ( | statement | , |
transformer | |||
) |
void store_statement_total_precondition | ( | statement | , |
transformer | |||
) |
void store_statement_transformer | ( | statement | , |
transformer | |||
) |
Referenced by statement_to_transformer(), and statement_to_transformer_list().
transformer string_expression_to_transformer | ( | entity | v, |
expression | rhs | ||
) |
tf = constant_to_transformer(v, call_function(syntax_call(srhs)));
rhs | hs |
Definition at line 3994 of file expression.c.
References basic_string_p, basic_to_string(), call_arguments, call_function, constant_to_transformer(), entity_has_values_p(), entity_name, entity_to_new_value(), entity_type, expression_syntax, gen_length(), is_syntax_call, is_syntax_range, is_syntax_reference, pips_internal_error, pips_user_error, reference_variable, simple_equality_to_transformer(), string_type_size(), syntax_call, syntax_reference, syntax_tag, transformer_undefined, type_variable, and variable_basic.
Referenced by any_expression_to_transformer().
text string_predicate_to_commentary(string str_pred, string comment_prefix) input : a string, part of which represents a predicate.
output : a text consisting of several lines of commentaries, containing the string str_pred, and beginning with comment_prefix. modifies : str_pred;
if str_pred is too long, it must be splitted in several lines; the hyphenation must be done only between the constraints of the predicate, when there is a "," or a ")". A space is added at the beginning of extra lines, for indentation.
search the maximal substring which length is less than longueur_max
add it to the text
if the remaining string fits in one line
str_pred | tr_pred |
comment_prefix | omment_prefix |
Definition at line 570 of file prettyprint.c.
References ADD_SENTENCE_TO_TEXT, FORESYS_CONTINUATION_PREFIX, get_bool_property(), make_pred_commentary_sentence(), make_text(), MAX_PRED_COMMENTARY_STRLEN, NIL, and strdup().
Referenced by words_predicate_to_commentary().
transformer struct_reference_assignment_to_transformer | ( | reference | r, |
type | t, | ||
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
rhs | hs |
pre | re |
ef | f |
Definition at line 3078 of file ri_to_transformers.c.
References struct_reference_assignment_or_equality_to_transformer().
Referenced by assign_rhs_to_reflhs_to_transformer(), and struct_variable_assignment_to_transformer().
transformer struct_reference_equality_to_transformer | ( | reference | r, |
type | t, | ||
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
rhs | hs |
pre | re |
ef | f |
Definition at line 3083 of file ri_to_transformers.c.
References struct_reference_assignment_or_equality_to_transformer().
Referenced by struct_variable_equality_to_transformer().
transformer struct_variable_assignment_to_transformer | ( | entity | v, |
type | t, | ||
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
v | assigned struct variable (does not handle the general case, "e1==e2;" where e1 and e2 are lhs expressions |
t | type of v, which much be matched by rhs expression type and which must not contain any named type |
rhs | right-hand side expression |
ef | list of effects |
pre | precondition of the assignment |
rhs | hs |
pre | re |
ef | f |
Definition at line 3100 of file ri_to_transformers.c.
References free_reference(), make_reference(), NIL, and struct_reference_assignment_to_transformer().
Referenced by assign_rhs_to_reflhs_to_transformer(), and c_return_to_transformer().
transformer struct_variable_equality_to_transformer | ( | entity | v, |
type | t, | ||
expression | rhs, | ||
transformer | pre, | ||
list | ef | ||
) |
rhs | hs |
pre | re |
ef | f |
Definition at line 3108 of file ri_to_transformers.c.
References free_reference(), make_reference(), NIL, and struct_reference_equality_to_transformer().
Referenced by any_user_call_site_to_transformer().
transformer substitute_formal_array_elements_in_precondition | ( | transformer | tf, |
entity | f, | ||
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
tf | f |
pc | c |
pre | re |
ef | f |
Definition at line 2014 of file ri_to_transformers.c.
References f(), and generic_substitute_formal_array_elements_in_transformer().
Referenced by process_call_for_summary_precondition().
transformer substitute_formal_array_elements_in_transformer | ( | transformer | tf, |
entity | f, | ||
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
tf | f |
pc | c |
pre | re |
ef | f |
Definition at line 2009 of file ri_to_transformers.c.
References f(), and generic_substitute_formal_array_elements_in_transformer().
Referenced by c_user_call_to_transformer().
transformer substitute_scalar_stub_in_transformer | ( | transformer | tf, |
entity | se, | ||
entity | de, | ||
bool | backward_p, | ||
list * | ppl | ||
) |
If both "se", source entity, and "de", destination entity, are defined, substitute the values of "se" by the values of "de" in "backward_p" mode, when translating a callee transformer at a call site of a caller.
If the "se" entity cannot be substituted, its value must be project.
tf | f |
se | e |
de | e |
backward_p | ackward_p |
ppl | pl |
Definition at line 136 of file points_to.c.
References CONS, ENTITY, entity_has_values_p(), entity_is_argument_p(), entity_to_new_value(), entity_to_old_value(), entity_undefined_p, entity_user_name(), global_new_value_to_global_old_value(), pips_user_warning, transformer_arguments, and transformer_value_substitute().
Referenced by forward_substitute_array_location_in_transformer(), new_array_element_backward_substitution_in_transformer(), substitute_struct_stub_in_transformer(), and substitute_stubs_in_transformer().
transformer substitute_struct_stub_in_transformer | ( | transformer | , |
reference | , | ||
type | , | ||
reference | , | ||
type | , | ||
bool | , | ||
list * | |||
) |
transformer substitute_stubs_in_transformer | ( | transformer | tf, |
call | c, | ||
statement | s, | ||
bool | backward_p | ||
) |
Exploit the binding map to substitute calles's stubs by actual arguments, which may be stubs of the callers,.
backward_p request a substitution from the callees' frame into the caller's frame, which is useful for transformers. Flag backward_p is set to false to compute summary preconditions.
FI: this function is now only used for preconditions. It has been rewritten for transformers to speed up the process when array elements are involved. It is better to start from the needs, the stubs used in the transformer, than from all possible stubs, but it is much easier for a backward translation. With a forward translation, regular variables may have to be translated into stubs.
FI: A quick improvement would to return when no translation is needed... but you do not always know it when backward_p is set to false.
tf | f |
backward_p | ackward_p |
Definition at line 256 of file points_to.c.
References analyzed_reference_p(), approximation_exact_p, approximation_must_p, atomic_points_to_reference_p(), cell_any_reference(), compute_basic_concrete_type(), CONS, constant_memory_access_path_to_location_entity(), ENDP, ENTITY, entity_basic_concrete_type(), entity_has_values_p(), entity_undefined_p, gen_free_list(), get_current_module_entity(), get_points_to_graph_from_statement(), NIL, pips_internal_error, pl, points_to_approximation, points_to_graph_bottom, points_to_sink, points_to_source, pt_to_list_undefined_p(), reference_indices, reference_to_type(), reference_variable, relevant_translation_pair_p(), safe_transformer_projection(), SET_FOREACH, substitute_scalar_stub_in_transformer(), substitute_struct_stub_in_transformer(), transformer_to_analyzed_locations(), transformer_to_potential_stub_translation(), type_struct_variable_p(), and user_call_to_points_to_interprocedural_binding_set().
Referenced by process_call_for_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.
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().
text text_for_a_transformer | ( | transformer | tran, |
bool | is_a_transformer | ||
) |
call this one from outside.
tran | ran |
is_a_transformer | s_a_transformer |
Definition at line 540 of file prettyprint.c.
References is_total_precondition, is_transformer, text_transformer(), and text_undefined.
Referenced by call_site_to_module_precondition_text().
text text_transformer | ( | transformer | tran | ) |
text text_transformer(transformer tran) input : a transformer representing a transformer or a precondition output : a text containing commentaries representing the transformer modifies : nothing.
Modification: AP, Nov 10th, 1995. Instead of building a (very long) string, I directly use the transformer to build the prettyprint in text format. This is to avoid the problem occuring when the buffer used in transformer[precondition]_to_string() is too small. I also use a static buffer to build each constraint; we are restricted to constraints of lengths smaller than the line length.
If in EMACS mode, does not add any separator line:
tran | ran |
Definition at line 464 of file prettyprint.c.
References ADD_SENTENCE_TO_TEXT, append, close_current_line(), dump_text(), entity_list_text_format(), entity_minimal_name(), FORESYS_CONTINUATION_PREFIX, get_bool_property(), get_comment_continuation(), get_comment_sentinel(), HASH_UNDEFINED_VALUE, ifdebug, is_sentence_formatted, is_total_precondition, is_transformer, list_undefined, make_sentence(), make_text(), MAX_LINE_LENGTH, NIL, pips_debug, pips_user_value_name(), PREC_FORESYS_PREFIX, predicate_system, sc_copy(), sc_lexicographic_sort(), sc_rm(), sc_syst_debug(), semantics_is_inferior_pvarval(), strdup(), system_text_format(), TRAN_FORESYS_PREFIX, transformer_arguments, transformer_relation, and transformer_undefined.
Referenced by get_semantic_text(), print_initial_precondition(), print_program_precondition(), semantic_to_text(), and text_for_a_transformer().
transformer tf_equivalence_equalities_add | ( | transformer | tf | ) |
mappings.c
I need here a contraintes_dup() that is not yet available in Linear and I cannot change Linear just before the DRET meeting; I've got to modify transformer_equalities_add() and to give it a behavior different from transformer_equality_add()
tf | f |
Definition at line 83 of file mappings.c.
References equivalence_equalities, and transformer_equalities_add().
Referenced by statement_to_postcondition(), and statement_to_total_precondition().
bool total_precondition_map_undefined_p | ( | void | ) |
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().
transformer transformer_add_any_relation_information | ( | transformer | pre, |
entity | op, | ||
expression | e1, | ||
expression | e2, | ||
transformer | context, | ||
bool | veracity, | ||
bool | upwards | ||
) |
compute transformer or precondition
This is not satisfactory: when going upwards you might nevertheless benefit from some precondition information. But you would then need to pass two transformers as argument: a context transformer and a to-be-modified transformer
context = upwards? transformer_undefined : pre;
context = transformer_range(pre);
Logical are represented by integer values
PIPS does not represent negative constants: call to unary_minus
PIPS does not represent complex constants: call to CMPLX
Only constant string are processed
Pointer analysis
This is not correct if side effects occur in e1 or e2
This is very complicated to add constraints from tf1, tf2 and rel in pre!
tf1 may modify the initial context. See w10.f
tf1 disappears into cond
try to break rel it into two convex components
pre disappears into newpre2
pre disappears into newpre
newpre stays undefined or newpre is pre
free_transformer(tf1); already gone
Nothing to be done with struct and union
pre may be unchanged when no information is derived
pre | re |
op | p |
e1 | 1 |
e2 | 2 |
context | ontext |
veracity | eracity |
upwards | pwards |
Definition at line 4686 of file expression.c.
References b1, b2, basic_of_expression(), basic_tag, ENTITY_EQUAL_P, entity_name, ENTITY_NON_EQUAL_P, free_basic(), free_transformer(), GREATER_THAN_OPERATOR_NAME, is_basic_bit, is_basic_complex, is_basic_derived, is_basic_float, is_basic_int, is_basic_logical, is_basic_overloaded, is_basic_pointer, is_basic_string, is_basic_typedef, LESS_THAN_OPERATOR_NAME, local_name_to_top_level_entity(), make_local_temporary_value_entity_with_basic(), pips_assert, pips_debug, pips_internal_error, relation_to_transformer(), safe_any_expression_to_transformer(), semantics_basic_tag(), semantics_user_warning, transformer_apply(), transformer_argument_consistency_p(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), transformer_identity(), transformer_normalize(), transformer_range(), transformer_safe_combine_with_warnings(), transformer_safe_image_intersection(), transformer_undefined, and transformer_undefined_p.
Referenced by logical_binary_function_to_transformer(), and transformer_add_call_condition_information_updown().
transformer transformer_add_condition_information | ( | transformer | pre, |
expression | c, | ||
transformer | context, | ||
bool | veracity | ||
) |
pre | re |
context | ontext |
veracity | eracity |
Definition at line 1092 of file expression.c.
References reset_temporary_value_counter(), transformer_add_condition_information_updown(), and transformer_temporary_value_projection().
Referenced by check_condition_wrt_precondition(), old_complete_whileloop_transformer(), and transformer_add_domain_condition().
transformer transformer_add_domain_condition | ( | transformer | tf, |
expression | c, | ||
transformer | context, | ||
bool | veracity | ||
) |
tf | f |
context | ontext |
veracity | eracity |
Definition at line 1138 of file expression.c.
References transformer_add_condition_information().
Referenced by test_to_total_precondition().
transformer transformer_add_integer_relation_information | ( | transformer | pre, |
entity | relop, | ||
expression | e1, | ||
expression | e2, | ||
bool | veracity, | ||
bool | upwards | ||
) |
It is supposed to be obsolete but is still called.
Maybe, it's only partly obsolete... If upwards is false, it is worth performing more convex hulls because the precondition on entry may restrain the space. upwards = transformer, !upwards = precondition
default: no change
both expressions e1 and e2 must be affine
Make sure that new values only are used in v1 and v2
v1 - v2 == 0
v2 - v1 + 1 <= 0 ou v1 - v2 + 1 <= 0
FI: I do not know if this is valid when your are moving upwards variables in v2 and v1 may have to be renamed as init values (i.e. old values)
FI: I think that this should be programmed (see comment above) but I'm waiting for a bug to occur... (6 July 1993)
FI: Well, the bug was eventually seen:-) (8 November 1995)
free_transformer(prea);
free_transformer(preb);
v2 - v1 + 1 <= 0
v1 - v2 <= 0
v2 - v1 <= 0
v1 - v2 + 1 <= 0
do nothing... although Malik may have tried harder!
do nothing, although MODULO and INTEGER DIVIDE could be handled
pre | re |
relop | elop |
e1 | 1 |
e2 | 2 |
veracity | eracity |
upwards | pwards |
Definition at line 5929 of file expression.c.
References bool_to_string(), DEBUG_TRANSFORMER_ADD_RELATION_INFORMATION, ENTITY_EQUAL_P, ENTITY_GREATER_OR_EQUAL_P, ENTITY_GREATER_THAN_P, ENTITY_LESS_OR_EQUAL_P, ENTITY_LESS_THAN_P, entity_local_name(), ENTITY_NON_EQUAL_P, fprintf(), ifdebug, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, pips_debug, print_expression(), print_transformer, TCST, transformer_convex_hull(), transformer_dup(), transformer_equality_add(), transformer_inequality_add(), transformer_internal_consistency_p(), upwards_vect_rename(), value_mappings_compatible_vector_p(), VALUE_ONE, variables_to_new_values(), vect_add_elem(), vect_dup(), vect_rm(), and vect_substract().
transformer transformer_add_loop_index_incrementation | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
SHOULD BE REWRITTEN WITH EXPRESSION_TO_TRANSFORMER
it does not contain the loop index update the loop increment expression must be linear to find inductive variables related to the loop index
tf | f |
pre | re |
Definition at line 1136 of file loop.c.
References arguments_add_entity(), base_add_variable(), base_dimension, entity_has_values_p(), entity_local_name(), entity_to_new_value(), entity_to_old_value(), expression_to_affine(), loop_index, loop_range, pips_assert, pips_user_warning, predicate_system, range_increment, transformer_add_variable_incrementation(), transformer_arguments, transformer_consistency_p(), transformer_relation, value_mappings_compatible_vector_p(), VECTEUR_UNDEFINED, and VECTEUR_UNDEFINED_P.
Referenced by loop_to_continue_transformer(), loop_to_total_precondition(), loop_to_transformer(), and recompute_loop_transformer().
transformer transformer_add_loop_index_initialization | ( | transformer | tf, |
loop | l, | ||
transformer | pre | ||
) |
The loop initialization is performed before tf.
EXPRESSION_TO_TRANSFORMER SHOULD BE USED
The new variables in eq must be added to sc; otherwise, further consistency checks core dump. bc.
sc_add_egalite(sc, eq);
The call to sc_projection_with_eq frees eq
FI: a NULL is not acceptable; I assume that we cannot end up with a SC_EMPTY...
Get rid of the initial value since it is unknowable
tf | f |
pre | re |
Definition at line 1082 of file loop.c.
References base_dimension, base_rm, base_union(), CONS, contrainte_make(), CONTRAINTE_UNDEFINED, ENTITY, entity_has_values_p(), entity_to_old_value(), eq, loop_index, loop_range, make_base_from_vect(), newgen_Psysteme, NIL, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, predicate_system, predicate_system_, range_lower, sc_make(), transformer_projection(), transformer_relation, VALUE_MONE, vect_add_elem(), and vect_dup().
Referenced by recompute_loop_transformer().
transformer transformer_add_range_condition | ( | transformer | tf, |
expression | c, | ||
transformer | context, | ||
bool | veracity | ||
) |
tf | f |
context | ontext |
veracity | eracity |
Definition at line 1147 of file expression.c.
References precondition_add_condition_information().
void transformer_add_reference_information | ( | transformer | tf, |
statement | s | ||
) |
tf | f |
Definition at line 700 of file ri_to_preconditions.c.
References add_reference_information().
Referenced by statement_to_transformer(), and statement_to_transformer_list().
void transformer_add_type_information | ( | transformer | tf | ) |
type.c
tf | f |
Definition at line 162 of file type.c.
References add_type_information().
Referenced by module_name_to_preconditions(), precondition_add_type_information(), statement_to_postcondition(), statement_to_transformer(), and transformer_add_variable_type_information().
void transformer_add_variable_type_information | ( | transformer | tf, |
entity | v | ||
) |
tf | f |
Definition at line 168 of file type.c.
References add_value_to_transformer_space(), entity_has_values_p(), entity_to_new_value(), pips_assert, transformer_add_type_information(), and value_belongs_to_transformer_space().
Referenced by declaration_to_transformer().
transformer transformer_apply_field_assignments | ( | transformer | t, |
reference | l, | ||
reference | r, | ||
type | st | ||
) |
st | t |
Definition at line 2925 of file ri_to_transformers.c.
References transformer_apply_field_assignments_or_equalities().
Referenced by struct_reference_assignment_or_equality_to_transformer(), and transformer_apply_field_assignments_or_equalities().
transformer transformer_apply_field_assignments_or_equalities | ( | transformer | t, |
reference | l, | ||
reference | r, | ||
type | st, | ||
bool | assign_p | ||
) |
For all analyzable fields f, apply the assignment "le.f = re.f;" to transformer t.
If s1.f is a struct, go down recursively.
It is assumed that s1 and s2 have the exact same concrete struct type, st.
Transformer t is updated. It is assumed to contain the current precondition.
st | t |
assign_p | ssign_p |
Definition at line 2876 of file ri_to_transformers.c.
References add_subscript_to_reference(), analyzed_type_p(), constant_memory_access_path_to_location_entity(), copy_reference(), ENTITY, entity_basic_concrete_type(), entity_to_expression(), entity_undefined_p, f(), FOREACH, free_reference(), free_transformer(), pips_internal_error, struct_type_to_fields(), transformer_add_equality(), transformer_add_modified_variable(), transformer_apply_field_assignments(), transformer_combine(), transformer_identity(), transformer_undefined_p, and type_struct_p.
Referenced by transformer_apply_field_assignments(), and transformer_apply_field_equalities().
transformer transformer_apply_field_equalities | ( | transformer | t, |
reference | l, | ||
reference | r, | ||
type | st | ||
) |
st | t |
Definition at line 2930 of file ri_to_transformers.c.
References transformer_apply_field_assignments_or_equalities().
Referenced by struct_reference_assignment_or_equality_to_transformer().
transformer transformer_apply_unknown_field_assignments | ( | transformer | t, |
reference | l, | ||
type | st | ||
) |
st | t |
Definition at line 2976 of file ri_to_transformers.c.
References transformer_apply_unknown_field_assignments_or_equalities().
Referenced by struct_reference_assignment_or_equality_to_transformer().
transformer transformer_apply_unknown_field_equalities | ( | transformer | t, |
reference | l, | ||
type | st | ||
) |
st | t |
Definition at line 2981 of file ri_to_transformers.c.
References transformer_apply_unknown_field_assignments_or_equalities().
Referenced by struct_reference_assignment_or_equality_to_transformer().
transformer transformer_formal_parameter_projection | ( | entity | f, |
transformer | t | ||
) |
Dealing with an interprocedural transformer, weak consistency is not true
pips_assert("t is weakly consistent", transformer_weak_consistency_p(t));
Definition at line 1537 of file ri_to_transformers.c.
References BASE_NULLE_P, BASE_UNDEFINED, CONS, dump_transformer, ENTITY, entity_storage, f(), formal_function, fprintf(), gen_free_list(), ifdebug, location_entity_p(), NIL, pips_assert, pips_debug, predicate_system, print_entities(), sc_weak_consistent_p(), storage_formal, storage_formal_p, transformer_projection(), transformer_relation, transformer_weak_consistency_p(), value_to_variable(), vecteur_succ, and vecteur_var.
Referenced by c_user_call_to_transformer().
transformer transformer_intra_to_inter | ( | transformer | tf, |
list | le | ||
) |
tf | f |
le | e |
Definition at line 1510 of file ri_to_transformers.c.
References generic_transformer_intra_to_inter().
Referenced by generic_module_name_to_transformers(), module_name_to_total_preconditions(), and program_precondition().
transformer transformer_logical_inequalities_add | ( | transformer | tf, |
entity | v | ||
) |
PROCESSING OF LOGICAL EXPRESSIONS.
the values of v are between 0 and 1
tf | f |
Definition at line 3569 of file expression.c.
References TCST, transformer_inequality_add(), VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by logical_binary_operation_to_transformer(), logical_reference_to_transformer(), and logical_unary_operation_to_transformer().
bool transformer_map_undefined_p | ( | void | ) |
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 translate_global_value | ( | entity | m, |
transformer | tf, | ||
entity | v | ||
) |
Try to convert an value on a non-local variable into an value on a local variable using a guessed name (instead of a location identity: M and N declared as COMMON/FOO/M and COMMON/FOO/N are not identified as a unique variable/location).
Mo more true: It might also fail to translate variable C:M into A:M if C is indirectly called from A thru B and if M is not defined in B.
This routine is not too safe. It accepts non-translatable variable as input and does not refuse them, most of the time.
Filter out constant and values local to the current module
FI: to be modified to account for global values that have a name but that should nevertheless be translated on their canonical representant; this occurs for non-visible global variables
FI: to be completed later... 3 December 1993 entity var = value_to_variable(v);
pips_debug(7, "%s is translated into %s\n", entity_name(v), entity_name(e)); transformer_value_substitute(tf, v, e);
Filter out old values: they are translated when the new value is encountered, and the new value has to appear if the old value does appear.
Instead, old values could be translated into new values and processing could go on...
FI, 26 October 1994
Should it be projected? No, this should occur later for xxxx::init variables when the xxxx is translated. Or before if xxxx has been translated
must be a common; dynamic and static area must have been filtered out before
try to find an equivalent entity by its name (whereas we should use locations)
no equivalent name found, get rid of v
transformer_projection(tf, CONS(ENTITY, v_old, NIL));
no equivalent location found, get rid of v
no equivalent location found, get rid of v
e has already been introduced and v eliminated; this happens when a COMMON variable is also passed as real argument
FI: v may still appear in the constraints as in spice.f (Perfect Club) and spice01.f (Validation)
this cannot happen when the summary transformer of a called procedure is translated because the write effect in the callee that is implied by v_init existence must have been passed upwards and must have led to the creation of e_init
this should not happen when a caller precondition at a call site is transformed into a piece of a summary precondition for the callee because v_init becomes meaningless; at the callee's entry point, by definition, e == e_init; v_init should have been projected before
forget e_init: there is no v_init in tf
there is no v_init to worry about; v is not changed in the caller (or its subtree of callees)
this value does not need to be translated
tf | f |
Definition at line 657 of file interprocedural.c.
References arguments_add_entity(), base_contains_variable_p(), BASE_UNDEFINED, concatenate(), CONS, contrainte_make(), CONTRAINTE_UNDEFINED, dump_transformer, ENTITY, entity_constant_p, entity_domain, entity_is_argument_p(), entity_local_name(), entity_module_name(), entity_name, entity_storage, entity_type, entity_undefined, eq, gen_find_tabulated(), gen_free_list(), global_new_value_to_global_old_value(), global_old_value_p(), ifdebug, language_c_p, module_language, module_local_name(), MODULE_SEP_STRING, NIL, OLD_VALUE_SUFFIX, pips_debug, pips_internal_error, pips_user_error, predicate_system, ram_function, ram_section, ram_undefined, same_scalar_location_p(), sc_add_egalite(), sc_equation_add(), storage_formal_p, storage_ram, storage_ram_p, storage_return_p, storage_rom_p, storage_tag, storage_undefined, strdup(), top_level_entity_p(), transformer_arguments, transformer_filter(), transformer_projection(), transformer_relation, transformer_value_substitutable_p(), transformer_value_substitute(), type_equal_p(), type_to_string(), user_warning, value_alias(), value_entity_p(), vect_add_elem(), and vect_new().
Referenced by translate_global_values().
void translate_global_values | ( | entity | m, |
transformer | tf | ||
) |
a copy of sc_base(s) is needed because translate_global_value() modifies it at the same time
tf | f |
Definition at line 625 of file interprocedural.c.
References base_rm, dump_value_name(), ifdebug, pips_debug, predicate_system, sc_fprint(), Svecteur::succ, transformer_relation, translate_global_value(), vect_dup(), and vecteur_var.
Referenced by add_module_call_site_precondition(), fortran_user_call_to_transformer(), get_semantic_text(), load_summary_precondition(), module_name_to_total_preconditions(), precondition_intra_to_inter(), process_call_for_summary_precondition(), and program_precondition().
bool true_condition_wrt_precondition_p | ( | expression | c, |
transformer | pre | ||
) |
pre | re |
Definition at line 5900 of file expression.c.
References eval_condition_wrt_precondition_p().
Referenced by whileloop_to_postcondition(), and whileloop_to_total_precondition().
transformer unstructured_to_flow_insensitive_transformer | ( | unstructured | u | ) |
This simple fix-point over-approximates the CFG by a fully connected graph.
Each vertex can be executed at any time any number of times.
The fix point is easy to compute because it is the fix point of the convex hull all each node transformers.
The result is sometimes surprising as users see the real paths and cannot understand why a variable is declared modified when it obviously is not. This mostly choses in node preconditions since the overall unstructured transformer is not displayed usually and since it is globally correct.
But it is a perfectly valid over-approximation usable by automatic analyses.
Using the effects of the unstructured to derive a fix point leads to the same surprise although it is as correct, using the same over approximation of the control flow graph but a cruder version of the transformers.
This function is also used when computing preconditions if the exit node is not reached (?). It assumes that transformers for all statements in the unstructured have already been computed.
Two modes are possible: the transitive closure of the convex hull of all elementary transformers, or the transitive closure of the transformer list.
Assume any reachable node is executed at each iteration. A fix-point of the result can be used to approximate the node preconditions. Some nodes can be discarded because they do not modify the store such as IF statements (always) and CONTINUE statements (if they do not link the entry and the exit nodes).
Entry node
transformer_convex_hull has side effects on its arguments:-(
Should be fixed now, 29 June 2000
transformer tf_st = copy_transformer(load_statement_transformer(st));
Any side effect?
test
continue
other
Definition at line 2206 of file unstructured.c.
References chunk_undefined, CONS, continue_statement_p(), control_predecessors, control_statement, control_successors, ENDP, FORWARD_CONTROL_MAP, free_transformer(), gen_find_eq(), gen_free_list(), get_bool_property(), ifdebug, load_statement_transformer(), NIL, pips_assert, pips_debug, print_transformer, statement_test_p(), TRANSFORMER, transformer_arguments, transformer_convex_hull(), transformer_empty(), transformer_internal_consistency_p(), transformer_list_transitive_closure(), transformer_undefined, unstructured_control, and unstructured_exit.
Referenced by unstructured_to_postcondition(), unstructured_to_total_precondition(), and unstructured_to_transformer().
transformer unstructured_to_flow_sensitive_postconditions | ( | transformer | pre_u, |
transformer | pre, | ||
unstructured | u | ||
) |
compute pre- and post-conditions in an unstructured from the entry precondition pre and return the exit postcondition.
pre_u is pre filtered by the u's transformer and can be used for any node.
control tail = unstructured_exit(u);
pre_u | re_u |
pre | re |
Definition at line 2040 of file unstructured.c.
References forward_control_map_get_blocs(), gen_free_list(), gen_length(), get_bool_property(), get_int_property(), NIL, pips_assert, semantics_user_warning, transformer_consistency_p(), transformer_undefined, unstructured_control, unstructured_to_flow_sensitive_postconditions_or_transformers(), and unstructured_to_postconditions().
Referenced by unstructured_to_postcondition().
transformer unstructured_to_flow_sensitive_postconditions_or_transformers | ( | transformer | pre_u, |
transformer | pre, | ||
unstructured | u, | ||
bool | postcondition_p | ||
) |
compute either the postconditions in an unstructured or the transformer of this unstructured.
In both cases, transformers for all nodes used to be supposed to be available.
Do not go down into nested unstructured
Propagate the precondition in the DAG and recompute the cycle transformers or compute the path transformers and the cycle fix point transformers.
Compute the real precondition for each statement and propagate postconditions in it.
Take care of unreachable nodes
Get rid of the auxiliary data structures
pre_u | re_u |
pre | precondition at entry: e_pre |
u | precondition true for every node: n_pre |
postcondition_p | ostcondition_p |
Definition at line 1821 of file unstructured.c.
References bourdoncle_free(), bourdoncle_partition(), control_domain, control_statement, copy_transformer(), dag_to_flow_sensitive_postconditions_or_transformers(), dag_to_flow_sensitive_preconditions(), fprintf(), free_control_fix_point_map(), free_control_postcondition_map(), gen_context_multi_recurse(), gen_false(), gen_multi_recurse(), gen_null(), gen_true(), HASH_MAP, hash_table_entry_count(), hash_table_undefined, ifdebug, load_control_postcondition(), local_process_unreachable_node(), make_control_fix_point_map(), make_control_postcondition_map(), node_to_path_transformer_or_postcondition(), pips_assert, pips_debug, print_control_node_uns(), print_cycle_head_to_fixpoint(), print_transformer, statement_domain, statement_identification(), transformer_range(), transformer_undefined, transformer_undefined_p, unstructured_control, unstructured_exit, and unstructured_undefined.
Referenced by unstructured_to_flow_sensitive_postconditions(), and unstructured_to_transformer().
transformer unstructured_to_flow_sensitive_total_preconditions | ( | transformer | t_post_u, |
transformer | pre, | ||
unstructured | u | ||
) |
control tail = unstructured_exit(u);
t_post_u | _post_u |
pre | re |
Definition at line 2473 of file unstructured.c.
References pips_assert, transformer_consistency_p(), and transformer_undefined.
Referenced by unstructured_to_total_precondition().
transformer unstructured_to_postcondition | ( | transformer | pre, |
unstructured | u, | ||
transformer | tf | ||
) |
there is only one statement and no arcs in u; no need for a fix-point
FI: pre should not be duplicated because statement_to_postcondition() means that pre is not going to be changed, just post produced.
Do not try anything clever! God knows what may happen in unstructured code. Postcondition post is not computed recursively from its components but directly derived from u's transformer. Preconditions associated to its components are then computed independently, hence the name unstructured_to_postconditionS instead of unstructured_to_postcondition
propagate as precondition an invariant for the whole unstructured u assuming that all nodes in the CFG are fully connected, unless tf is not feasible because the unstructured is never exited or exited thru a call to STOP which invalidates the previous assumption.
FI: I do not know if I should duplicate pre or not.
FI: well, dumdum, you should have duplicated tf!
FI: euh... why? According to comments about transformer_apply() neither arguments are modified...
post = unstructured_to_postconditions(pre_n, pre, u);
pre | re |
tf | f |
Definition at line 2075 of file unstructured.c.
References control_predecessors, control_statement, control_successors, ifdebug, invariant_wrt_transformer(), NIL, pips_assert, pips_debug, print_transformer, statement_to_postcondition(), transformer_apply(), transformer_dup(), transformer_empty_p(), transformer_free(), transformer_undefined, transformer_undefined_p, unstructured_control, unstructured_to_flow_insensitive_transformer(), unstructured_to_flow_sensitive_postconditions(), and unstructured_undefined.
Referenced by instruction_to_postcondition().
transformer unstructured_to_transformer | ( | unstructured | u, |
transformer | e_pre, | ||
list | e | ||
) |
effects of u
approximate store condition for all control nodes: simple context for improved transformer derivation; it is not a precondition and should have no arguments.
Same as previous one for the store on entry in the unstructured. This the entry node usually has predecessors in the CFG, this is not the context for the entry node. It is not a precondition.
No information available on entrance
Cheapest fix point transformer. The flow insensitive fix point could be used instead.
pre is replaced by its range condition later when needed
Transformers should be computed precisely whether the unstructured is left by the exit node or by an explicit or implicit call to STOP.
computing the transformer for u is like computing the postcondition with no information on entry: no, the input context may be used to refine the transformer.
pre_u is restricted to its range later when needed.
These tests should be performed at the scc level
Not really linked to fix point issue, but a way to know we are using a FAST option.
Do something for nodes unreachable from the entry but linked to the exit
The control flow graph is never exited... by the exit node
The unstructured is never exited, but all nodes are supposed to have transformers. This would never occur if the control restructuration were clean unless an infinite loop is stopped within a called procedure. Control effects are not reported.
FI: pre should be used!
Might be useless because it's now performed just above and more generally by a gen_multi_recurse()
e_pre | _pre |
e | precondition on entrance |
Definition at line 2332 of file unstructured.c.
References control_domain, effects_to_transformer(), forward_control_map_get_blocs(), free_transformer(), gen_false(), gen_free_list(), gen_in_list_p(), gen_length(), gen_multi_recurse(), gen_null(), gen_true(), get_bool_property(), get_int_property(), NIL, pips_assert, pips_debug, semantics_user_warning, statement_domain, transformer_dup(), transformer_empty(), transformer_empty_p(), transformer_identity(), transformer_safe_apply(), transformer_undefined, transformer_undefined_p, unreachable_node_to_transformer(), unstructured_control, unstructured_exit, unstructured_to_flow_insensitive_transformer(), unstructured_to_flow_sensitive_postconditions_or_transformers(), and unstructured_to_transformers().
Referenced by instruction_to_transformer().
void update_cycle_temporary_precondition | ( | control | c, |
transformer | pre, | ||
control_mapping | cycle_temporary_precondition_map | ||
) |
pre | re |
cycle_temporary_precondition_map | ycle_temporary_precondition_map |
Definition at line 1021 of file unstructured.c.
References control_statement, ifdebug, pips_debug, print_transformer, statement_identification(), and update_temporary_precondition().
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_to_flow_sensitive_preconditions().
transformer update_precondition_with_call_site_preconditions | ( | transformer | t, |
entity | caller, | ||
entity | callee | ||
) |
Update precondition t for callee with preconditions of call sites to callee in caller.
Call sites are found in the statement of caller, but also in its declarations. Return the updated precondition t.
summary effects for the callee
calls hidden in dimension declarations are not caught because entities are not traversed by gen_recurse().
This normalization seems pretty uneffective for fraer01.tpips
caller | aller |
callee | allee |
Definition at line 1371 of file interprocedural.c.
References call_domain, callee, current_callee, current_caller, current_precondition, current_summary_precondition, db_get_memory_resource(), entity_name, entity_undefined, free_value_mappings(), gen_multi_recurse(), gen_null(), get_current_module_entity(), get_current_module_statement(), list_undefined, load_summary_effects(), memorize_precondition_for_summary_precondition(), module_local_name(), module_to_value_mappings(), pips_assert, pips_user_error, pop_statement_global_stack(), process_call_for_summary_precondition(), reset_cumulated_rw_effects(), reset_current_module_entity(), reset_current_module_statement(), reset_proper_rw_effects(), reset_pt_to_list(), reset_semantic_map(), set_cumulated_rw_effects(), set_current_module_entity(), set_current_module_statement(), set_proper_rw_effects(), set_pt_to_list(), set_semantic_map(), statement_domain, summary_effects_of_callee, transformer_defined_p(), transformer_normalize(), transformer_undefined, and use_points_to_p().
Referenced by ordinary_summary_precondition(), and summary_total_postcondition().
void update_statement_postcondition | ( | statement | , |
transformer | |||
) |
void update_statement_precondition | ( | statement | , |
transformer | |||
) |
void update_statement_semantic | ( | statement | , |
transformer | |||
) |
void update_statement_temporary_precondition | ( | statement | s, |
transformer | pre, | ||
statement_mapping | statement_temporary_precondition_map | ||
) |
pre | re |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 997 of file unstructured.c.
References pips_debug, statement_identification(), and update_temporary_precondition().
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_to_flow_sensitive_preconditions().
void update_statement_total_precondition | ( | statement | , |
transformer | |||
) |
void update_statement_transformer | ( | statement | , |
transformer | |||
) |
Referenced by statement_to_transformer(), and statement_to_transformer_list().
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.
void update_summary_precondition_in_declaration | ( | expression | e, |
transformer | pre | ||
) |
This function is called to deal with call sites located in initialization expressions carried by declarations.
pre | re |
Definition at line 1356 of file interprocedural.c.
References call_domain, current_precondition, gen_null(), gen_recurse, and process_call_for_summary_precondition().
Referenced by memorize_precondition_for_summary_precondition().
void update_temporary_precondition | ( | void * | k, |
transformer | pre, | ||
hash_table | precondition_map | ||
) |
pre | re |
precondition_map | recondition_map |
Definition at line 975 of file unstructured.c.
References free_transformer(), hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_update(), ifdebug, pips_debug, print_transformer, transformer_convex_hull(), and transformer_dup().
Referenced by update_cycle_temporary_precondition(), and update_statement_temporary_precondition().
void upwards_vect_rename | ( | Pvecteur | v, |
transformer | post | ||
) |
Renaming of variables in v according to transformations occuring later.
If a variable is modified by post, its old value must be used in v
FI: it would probably ne more efficient to scan va and vb than the argument list...
post | ost |
Definition at line 1062 of file mappings.c.
References ENTITY, FOREACH, new_value_to_old_value(), transformer_arguments, and vect_variable_rename().
Referenced by add_declaration_list_information(), add_reference_information(), and transformer_add_integer_relation_information().
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 user_call_to_transformer | ( | entity | f, |
list | pc, | ||
transformer | pre, | ||
list | ef | ||
) |
pc | c |
pre | re |
ef | f |
Definition at line 2506 of file ri_to_transformers.c.
References c_module_p(), c_user_call_to_transformer(), effects_to_transformer(), entity_module_p(), f(), fortran_user_call_to_transformer(), get_bool_property(), pips_assert, pips_debug, SEMANTICS_INTERPROCEDURAL, and transformer_undefined.
Referenced by call_to_transformer(), and expression_to_transformer().
transformer user_function_call_to_transformer | ( | entity | e, |
expression | expr, | ||
transformer | pre | ||
) |
a function call is a call to a non void function in C and to a FUNCTION in Fortran
its precondition
expr | a value |
pre | a call to a function |
Definition at line 1373 of file ri_to_transformers.c.
References c_module_p(), c_user_function_call_to_transformer(), call_function, expression_call(), f(), fortran_user_function_call_to_transformer(), and transformer_undefined.
Referenced by call_to_transformer(), float_call_expression_to_transformer(), integer_call_expression_to_transformer(), logical_expression_to_transformer(), and pointer_call_expression_to_transformer().
transform a vector based on variable entities into a vector based on new value entities when possible; does nothing most of the time; does a little in the presence of equivalenced variables
Ugly because it has a hidden side effect on v to handle Fortran equivalences and because its implementation is dependent on type Pvecteur.
Assume that the value mappings are available (as implied by the function's name!), which may not be true when dealing with call sites.
The variable may denote a constant with compatible type
or a temporary variable
Or a variable value
Or a phi variable, when transformers are computed by the region analysis
Or the vector cannot be used in the semantics analysis
iv | v |
Definition at line 924 of file mappings.c.
References analyzed_constant_p(), entity_constant_p, entity_has_values_p(), entity_to_new_value(), entity_undefined, local_temporary_value_entity_p(), Svecteur::succ, TCST, variable_phi_p, VECTEUR_NUL_P, and vecteur_var.
Referenced by add_affine_bound_conditions(), add_declaration_list_information(), add_loop_index_exit_value(), add_loop_skip_condition(), add_reference_information(), affine_to_transformer(), integer_divide_to_transformer(), integer_right_shift_to_transformer(), simple_affine_to_transformer(), transformer_add_integer_relation_information(), and transformer_add_loop_index_incrementation().
transformer value_passing_summary_transformer | ( | entity | f, |
transformer | tf | ||
) |
With value passing, writes on formal parameters are not effective interprocedurally unless an array is passed as parameter.
All new values corresponding to formal arguments of f must be projected out and removed from the arguments list.
Performed by side-effect on tf.
The old values cannot be renamed directly after projection, because the transformer projection opearator detects an inconsistency.
Rename old values as temporary values in the caller frame.
Updates the argument list after the projections
Rename tmp values as new values in the caller frame.
oav renamed oav1 because of FOREACH macro implementation
tf | f |
Definition at line 1471 of file interprocedural.c.
References CAR, CONS, ENTITY, entity_storage, entity_to_new_value(), entity_to_old_value(), entity_type, f(), FOREACH, formal_function, gen_free_list(), gen_nreverse(), location_entity_p(), make_local_temporary_value_entity(), NIL, POP, storage_formal, storage_formal_p, transformer_arguments, transformer_projection(), transformer_value_substitute(), ultimate_type(), and value_to_variable().
Referenced by generic_module_name_to_transformers().
Definition at line 982 of file mappings.c.
References CONS, ENTITY, entity_has_values_p(), entity_to_new_value(), entity_to_old_value(), and NIL.
Referenced by statement_to_postcondition().
void variables_to_new_values | ( | Pvecteur | v | ) |
replace variables by new values which is necessary for equivalenced variables
Definition at line 1038 of file mappings.c.
References entity_to_new_value(), TCST, vect_variable_rename(), VECTEUR_NUL_P, vecteur_succ, VECTEUR_UNDEFINED, and vecteur_var.
Referenced by transformer_add_integer_relation_information().
list_mod | ist_mod |
Definition at line 1024 of file mappings.c.
References CONS, ENTITY, entity_to_old_value(), MAP, and NIL.
Referenced by recompute_loop_transformer().
list_mod | ist_mod |
Definition at line 966 of file mappings.c.
References CONS, ENTITY, entity_has_values_p(), entity_to_new_value(), entity_to_old_value(), FOREACH, and NIL.
Referenced by recompute_loop_transformer(), and statement_to_postcondition().
transformer whileloop_to_k_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e, | ||
int | k | ||
) |
pre | re |
k | effects of whileloop l |
Definition at line 2617 of file loop.c.
References evaluation_before_p, new_whileloop_to_k_transformer(), pips_internal_error, transformer_undefined, and whileloop_evaluation.
Referenced by whileloop_to_postcondition().
transformer whileloop_to_postcondition | ( | transformer | pre, |
whileloop | l, | ||
transformer | tf | ||
) |
propagate an impossible precondition in the loop body
do not add the exit condition since it is redundant with pre, but take care of side effects in the condition c
transformer_apply() generates a lot of warnings
The loop may be entered at least once.
The standard transformer tb is not enough, especially if the loop body s is a loop since then it is not even the statement transformer, but more generally we do not want the identity to be taken into account in tb since it is already added with P0. So we would like to guarantee that at least one state change occurs: we are not interested in identity iterations. For instance, if s is a loop, this means that the loop is entered, except if the loop condition has side effects.
To recompute this transformer, we use a pre_fuzzy=T*(P0) because we have nothing better.
complete_statement_transformer() is not really useful here because we usually do not have tighly nested while loops.
Nothing special in the loop body: no tests, no while,...
Recompute the body transformer without taking identity transformers into account. This is not enough because the decision about "activity" should be made dimension by dimension. We cannot get good result in general with a convex hull performed here: only specific cases are handled. We need instead a complex formulae to compute the loop precondition as a function of p_0 and all t_i
btl is copied because the function below frees at least its components
The loop fix point transformer T* could be used to obtain the set of stores for any number of iterations, including 0. Instead, use T+ and a convex hull with the precondition for the first iteration, which preserves more information when the fixpoint is not precise:
P^* = P_0 U cond(c)(tb(cond(c)(tb^*(P_0))))
Bertrand Jeannet suggests that we compute P0 U T(P0) U T^2(P0) U T_3(P0) where T_3 is the transitive closure obtained for iterations 3 to infinity by setting the initial iteration number k to 3 before projection. NSAD 2010. No test case has been forwarded to show that this would be useful.
We need the loop effects to recompute the unrolled transformer. Let's use NIL to start with... disaster. Let's use the body effects and hope for no side effects in loop condition.
FI: since pre_next is no longer useful, pre_next2 could be avoided. It just makes debugging easier.
propagate preconditions in the loop body and get its postcondition
At least one iteration is executed. The postcondition can be computed into three different ways:
or use both and use their intersection as unique postcondition (the added redundant information seems to result in less information after a projection for w09.f, Halbwachs car example).
The second way is more likely to suffer from non-convexity as it uses many more steps.
Also, note that precondition_add_condition_information() is more geared towards Fortran as it assumes no side effects in the condition evaluation. However, it is better at handling non-convex condition than condition_to_transformer(), but condition_to_transformer(), which is built on top of precondition_add_condition_information() could be improved/might be improvable... In case the condition is not convex, there is no single transformer which fits it. But the postcondition can be updated with different convex components and then different results united in a unique postcondition by a convex hull.
Let's execute the last iteration since it certainly exists
Assume the loop is entered, post_al, or not, post_ne, and perform the convex hull of both
The loop is executed at least once: let's execute the last iteration
The loop is never executed
pre | re |
tf | f |
Definition at line 3141 of file loop.c.
References active_transformer_list_to_transformer(), CAR, complete_statement_transformer(), condition_to_transformer(), copy_transformer(), empty_transformer(), false_condition_wrt_precondition_p(), free_transformer(), gen_full_copy_list(), gen_full_free_list(), gen_length(), get_bool_property(), get_int_property(), ifdebug, int, list_undefined, load_cumulated_rw_effects_list(), load_statement_transformer(), pips_debug, pips_flag_p, pips_internal_error, pips_user_error, precondition_add_condition_information(), print_transformer, SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), statement_to_transformer_list(), TRANSFORMER, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_empty(), transformer_free(), transformer_identity(), transformer_intersection(), transformer_list_multiple_closure_to_precondition(), transformer_list_to_active_transformer_list(), transformer_range(), transformer_undefined, true_condition_wrt_precondition_p(), whileloop_body, whileloop_condition, and whileloop_to_k_transformer().
Referenced by instruction_to_postcondition().
transformer whileloop_to_total_precondition | ( | transformer | t_post, |
whileloop | l, | ||
transformer | tf, | ||
transformer | context | ||
) |
transformer_dup(pre)
Apply the loop fix point transformer T* to obtain the set of stores for any number of iteration, including 0.
propagate an impossible precondition in the loop body
The loop body precondition is not useful any longer
do not add the exit condition since it is redundant with pre
post = transformer_dup(pre);
At least one iteration is executed. The transformer of the loop body is not useful!
transformer tb = load_statement_transformer(s);
propagate preconditions in the loop body
ntl = transformer_apply(tf, pre);
Let's execute the last iteration since it certainly exists
post = transformer_apply(tb, ntl);
post = precondition_add_condition_information(post, c, post, false);
Assume the loop is entered, post_al, or not, post_ne, and perform the convex hull of both
= transformer_dup(pre)
propagate preconditions in the loop body
The loop is executed at least once: let's execute the last iteration
The loop is never executed
post = transformer_convex_hull(post_ne, post_al);
t_post | _post |
tf | f |
context | ontext |
Definition at line 3439 of file loop.c.
References false_condition_wrt_precondition_p(), free_transformer(), ifdebug, load_statement_transformer(), pips_assert, pips_debug, pips_flag_p, pips_internal_error, precondition_add_condition_information(), print_transformer, SEMANTICS_FIX_POINT, SEMANTICS_INEQUALITY_INVARIANT, statement_to_postcondition(), transformer_apply(), transformer_combine(), transformer_empty(), transformer_free(), transformer_undefined, true_condition_wrt_precondition_p(), whileloop_body, and whileloop_condition.
Referenced by instruction_to_total_precondition().
transformer whileloop_to_transformer | ( | whileloop | l, |
transformer | pre, | ||
list | e | ||
) |
effects of whileloop l
pre | re |
Definition at line 2583 of file loop.c.
References evaluation_before_p, new_whileloop_to_transformer(), repeatloop_to_transformer(), transformer_undefined, and whileloop_evaluation.
Referenced by instruction_to_transformer().
text words_predicate_to_commentary(list w_pred, string comment_prefix) input : a list of strings, one of them representing a predicate.
output : a text of several lines of commentaries containing this list of strings, and beginning with comment_prefix. modifies : nothing.
str_pred is the string corresponding to the concatenation of the strings in w_pred
w_pred | _pred |
comment_prefix | omment_prefix |
Definition at line 653 of file prettyprint.c.
References string_predicate_to_commentary(), and words_to_string().
Referenced by print_any_reductions(), text_comp_region(), text_points_to(), and text_reductions().
|
extern |
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 198 of file semantics.h.
Referenced by process_ready_node(), refine_transformers(), refine_transformers_with_points_to(), statement_to_transformer(), and statement_to_transformer_list().