PIPS
|
Go to the source code of this file.
Macros | |
#define | SEMANTICS_MODULE_NAME "*SEMANTICS*" |
Warning! Do not modify this file that is automatically generated! More... | |
#define | SEMANTICS_SEPARATOR '#' |
Must be used in suffixes and prefixes below. More... | |
#define | OLD_VALUE_PREFIX "o#" |
internal entity names (FI: I should have used suffixes to be consistent with external suffixes More... | |
#define | INTERMEDIATE_VALUE_PREFIX "i#" |
#define | TEMPORARY_VALUE_PREFIX "t#" |
#define | NEW_VALUE_SUFFIX "#new" |
external suffixes (NEW_VALUE_SUFFIX is not used, new values are represented by the variable itself, i.e. More... | |
#define | OLD_VALUE_SUFFIX "#init" |
#define | INTERMEDIATE_VALUE_SUFFIX "#int" |
#define | ADDRESS_OF_SUFFIX "#addressof" |
#define | SIZEOF_SUFFIX "#sizeof" |
Functions | |
transformer | transformer_dup (transformer) |
cproto-generated files More... | |
void | transformer_free (transformer) |
void | free_transformers (transformer,...) |
void | old_transformer_free (transformer) |
transformer | transformer_identity (void) |
Allocate an identity transformer. More... | |
transformer | transformer_empty (void) |
Allocate an empty transformer. More... | |
transformer | empty_transformer (transformer) |
Do not allocate an empty transformer, but transform an allocated transformer into an empty_transformer. More... | |
bool | transformer_identity_p (transformer) |
Check that t is an identity function. More... | |
bool | transformer_is_empty_p (transformer) |
Check that transformer t is the canonical representation of an empty transformer. More... | |
bool | transformer_is_rn_p (transformer) |
Check that transformer t is the canonical representation of the whole afine space defined by its basis. More... | |
transformer | transformer_add_sign_information (transformer, entity, int) |
CHANGE THIS NAME: no loop index please, it's not directly linked to loops!!! More... | |
transformer | transformer_add_variable_incrementation (transformer, entity, Pvecteur) |
transformer transformer_add_loop_index(transformer t, entity i, Pvecteur incr): add the index incrementation expression incr for loop index i to transformer t. More... | |
transformer | transformer_add_variable_update (transformer, entity) |
Add an update of variable v into t. More... | |
transformer | transformer_add_value_update (transformer, entity) |
Add an update of variable v to t (a value cannot be updated) More... | |
transformer | transformer_add_variables_update (transformer, list) |
transformer | transformer_constraint_add (transformer, Pvecteur, bool) |
transformer | transformer_inequality_add (transformer, Pvecteur) |
transformer | transformer_equality_add (transformer, Pvecteur) |
transformer | transformer_equalities_add (transformer, Pcontrainte) |
transformer | transformer_inequalities_add (transformer, Pcontrainte) |
Warning: More... | |
transformer | transformer_add_identity (transformer, entity) |
transformer | transformer_add_equality (transformer, entity, entity) |
Add an equality between two values (two variables?) More... | |
transformer | transformer_add_equality_with_integer_constant (transformer, entity, long long int) |
Add an equality between a value and an integer constant: v==cst. More... | |
transformer | transformer_add_inequality (transformer, entity, entity, bool) |
Add the equality v1 <= v2 or v1 < v2. More... | |
transformer | transformer_add_inequality_with_integer_constraint (transformer, entity, long long int, bool) |
Add the inequality v <= cst or v >= cst. More... | |
transformer | transformer_add_inequality_with_affine_term (transformer, entity, entity, int, int, bool) |
Add the inequality v <= a x + cst or v >= a x + cst. More... | |
transformer | transformer_add_equality_with_affine_term (transformer, entity, entity, int, int) |
Add the equality v = a x + cst. More... | |
transformer | transformer_add_inequality_with_linear_term (transformer, entity, entity, int, bool) |
Add the inequality v <= a x or v >= a x. More... | |
transformer | transformer_add_3d_affine_constraint (transformer, int, entity, int, entity, int, entity, int, bool) |
Add the constraint a1 v1 + a2 v2 + a3 v3 + cst <= or == 0. More... | |
bool | transformer_argument_consistency_p (transformer) |
bool | transformer_argument_weak_consistency_p (transformer) |
bool | transformer_argument_general_consistency_p (transformer, bool) |
bool | transformer_consistency_p (transformer) |
FI: I do not know if this procedure should always return or fail when an inconsistency is found. More... | |
bool | transformers_consistency_p (list) |
bool | transformer_weak_consistency_p (transformer) |
Interprocedural transformers do not meet all conditions. More... | |
bool | transformer_general_consistency_p (transformer, bool) |
bool | transformer_internal_consistency_p (transformer) |
Same as above but equivalenced variables should not appear in the argument list or in the predicate basis. More... | |
list | transformer_projectable_values (transformer) |
bool | value_belongs_to_transformer_space (entity, transformer) |
void | add_value_to_transformer_space (entity, transformer) |
transformer | precondition_to_abstract_store (transformer) |
Get rid of all old values and arguments. More... | |
transformer | transformer_add_modified_variable (transformer, entity) |
FI: this function does not end up with a consistent transformer because the old value is not added to the basis of sc. More... | |
transformer | transformer_add_modified_variable_entity (transformer, entity) |
FI: like the previous function, but supposed to end up with a consistent transformer. More... | |
transformer | move_transformer (transformer, transformer) |
Move arguments and predicate of t2 into t1, free old arguments and predicate of t1, free what's left of t2. More... | |
bool | transformer_equations_constrain_variable_p (const transformer, const entity) |
Is value v used with a non-zero coefficient by the equations of transformer t? More... | |
bool | transformer_inequalities_constrain_variable_p (const transformer, const entity) |
Is value v used with a non-zero coefficient by the inequalities of transformer t? More... | |
transformer | transformer_convex_hull (transformer, transformer) |
convex_hull.c More... | |
transformer | transformer_halbwachs_fix_point (transformer) |
transformer | transformer_equality_fix_point (transformer) |
Let A be the affine loop transfert function. More... | |
void | build_transfer_equations (Pcontrainte, Pcontrainte *, Pbase *) |
bool | transfer_equation_p (Pvecteur) |
A transfer equation is an explicit equation giving one new value as a function of old values and a constant term. More... | |
entity | new_value_in_transfer_equation (Pvecteur) |
bool | sub_basis_p (Pbase, Pbase) |
FI: should be moved in base.c. More... | |
void | equations_to_bases (Pcontrainte, Pbase *, Pbase *) |
transformer | transformer_pattern_fix_point (transformer) |
This fixpoint function was developped to present a talk at FORMA. More... | |
Pvecteur | look_for_the_best_counter (Pcontrainte) |
Try to identify a loop counter among the equation egs. More... | |
Psysteme | sc_eliminate_constant_terms (Psysteme, Pvecteur) |
Eliminate all constant terms in sc using v. More... | |
Pcontrainte | constraints_eliminate_constant_terms (Pcontrainte, Pvecteur) |
Psysteme | sc_keep_invariants_only (Psysteme) |
This function cannot be moved into the Linear library. More... | |
Pcontrainte | constraints_keep_invariants_only (Pcontrainte) |
bool | invariant_vector_p (Pvecteur) |
A vector (in fact, a constraint) represents an invariant if it is a sum of delta for each variable. More... | |
Psysteme | sc_multiply_constant_terms (Psysteme, Variable, bool) |
Specific for the derivative fix point: each constant term in the constraints is multiplied by ik which is not in sc's basis, and ik is added to the basis is necessary. More... | |
transformer | transformer_derivative_fix_point (transformer) |
Computation of a transitive closure using constraints on the discrete derivative. More... | |
list | transformers_derivative_fix_point (list) |
transformer | transformer_basic_fix_point (transformer) |
Computation of a fix point: drop all constraints, remember which variables are changed. More... | |
transformer | any_transformer_to_k_closure (transformer, transformer, transformer, transformer, transformer, int, bool) |
Derived from any_loop_to_k_transformer() More... | |
transformer | print_transformer (transformer) |
io.c More... | |
transformer | print_any_transformer (transformer) |
For debugging without problem from temporary values. More... | |
list | print_transformers (list) |
transformer | fprint_transformer (FILE *, transformer, get_variable_name_t) |
list | fprint_transformers (FILE *, list, get_variable_name_t) |
char * | dump_value_name (entity) |
char * dump_value_name(e): used as functional argument because entity_name is a macro More... | |
void | dump_transformer (transformer) |
transformer | simple_equality_to_transformer (entity, entity, bool) |
transformer.c More... | |
transformer | simple_unary_minus_to_transformer (entity, entity) |
transformer | generic_equality_to_transformer (entity, entity, bool, bool) |
transformer | simple_addition_to_transformer (entity, entity, entity, bool) |
e and e1 and e2 are assumed to be values. More... | |
transformer | relation_to_transformer (entity, entity, entity, bool) |
e and f are assumed to be values. More... | |
transformer | transformer_combine (volatile transformer, transformer) |
transformer transformer_combine(transformer t1, transformer t2): compute the composition of transformers t1 and t2 (t1 then t2) More... | |
list | transformers_combine (list, transformer) |
Combine each transformer of transformer list tl1 with t2. More... | |
list | one_to_one_transformers_combine (list, list) |
Combine each transformer of transformer list tl1 with the corresponding transformer in transformer list tl2. More... | |
transformer | transformer_safe_combine_with_warnings (transformer, transformer) |
Transformer tf1 and tf2 are supposed to be independent but they may interfere, for instance because subexpressions have non-standard conformant side effects. More... | |
transformer | transformer_intersection (transformer, transformer) |
tf is a new transformer that receives the constraints in t1 and t2. More... | |
transformer | transformer_image_intersection (transformer, transformer) |
allocate a new transformer based on transformer t1 and postcondition t2 More... | |
transformer | transformer_safe_intersection (transformer, transformer) |
Allocate a new transformer. More... | |
transformer | transformer_safe_image_intersection (transformer, transformer) |
Allocate a new transformer. More... | |
transformer | transformer_domain_intersection (transformer, transformer) |
Restrict the domain of the relation tf with pre. More... | |
transformer | transformer_safe_domain_intersection (transformer, transformer) |
If tf and pre are defined, update tf. More... | |
transformer | transformer_range (transformer) |
Return the range of relation tf in a newly allocated transformer. More... | |
transformer | transformer_safe_range (transformer) |
list | transformers_range (list) |
Substitute each transformer in list tfl by its range. More... | |
transformer | transformer_to_domain (transformer) |
Return the domain of relation tf in a newly allocated transformer. More... | |
transformer | transformer_safe_domain (transformer) |
transformer | transformer_range_intersection (transformer, transformer) |
Allocate a new transformer rtf that is tf with its range restricted by the range r. More... | |
transformer | transformer_intersect_range_with_domain (transformer) |
When tf is used repeatedly in a loop, the range is part of the domain from iteration 2 to the end. More... | |
transformer | transformer_normalize (transformer, int) |
Eliminate (some) rational or integer redundancy. More... | |
transformer | transformer_safe_normalize (transformer, int) |
list | transformers_safe_normalize (list, int) |
bool | transformer_with_temporary_values_p (transformer) |
Does transformer tf use temporary values? More... | |
transformer | transformer_temporary_value_projection (transformer) |
transformer | safe_transformer_projection (transformer, list) |
t may be undefined, args may contain values unrelated to t More... | |
transformer | transformer_return_value_projection (entity, transformer) |
Project return values that are not linked to function f. More... | |
transformer | transformer_projection (transformer, list) |
values in args must be in t's base More... | |
transformer | transformer_arguments_projection (transformer) |
transformer transformer_projection(transformer t); projection of t along the hyperplane defined by values of variables in arguments; this generate a projection and not a cylinder based on the projection More... | |
Psysteme | no_elim (Psysteme) |
transformer | transformer_projection_with_redundancy_elimination (transformer, list, Psysteme(*)(Psysteme)) |
It is not clear if this function projects values or variables. More... | |
transformer | transformer_projection_without_check (transformer, list, Psysteme(*)(Psysteme)) |
In some cases, you know the projection will result in a non-consistent transformer that will be fixed later. More... | |
transformer | transformer_projection_with_redundancy_elimination_and_check (volatile transformer, list, Psysteme(*)(Psysteme), bool) |
transformer | transformer_apply (transformer, transformer) |
transformer transformer_apply(transformer tf, transformer pre): apply transformer tf on precondition pre to obtain postcondition post More... | |
list | transformer_apply_generic (list, transformer, bool) |
Generates a new list of postconditions, one for each transformer in tl, unless the postcondition is empty and keep_p is FALSE. More... | |
list | transformer_apply_map (list, transformer) |
Generates a new list of postconditions, one for each transformer in tl, unless the postcondition is empty. More... | |
list | transformers_apply (list, transformer) |
Same as previous one, but with a more normalized name. More... | |
list | transformers_apply_and_keep_all (list, transformer) |
Same as previous one, but with a more normalized name. More... | |
transformer | transformer_safe_apply (transformer, transformer) |
list | transformers_safe_apply (list, transformer) |
returns a list of postconditions, one for each transformer in tl More... | |
transformer | transformer_inverse_apply (transformer, transformer) |
transformer transformer_inverse_apply(transformer tf, transformer post): apply transformer tf on precondition pre to obtain postcondition post More... | |
transformer | transformer_safe_inverse_apply (transformer, transformer) |
transformer | transformer_filter (transformer, list) |
transformer transformer_filter(transformer t, cons * args): projection of t along the hyperplane defined by entities in args; this generate a projection and not a cylinder based on the projection; More... | |
transformer | transformer_variables_filter (transformer, list) |
Transformers are dealing with variables and/or variable values. More... | |
bool | transformer_affect_linear_p (transformer, Pvecteur) |
bool transformer_affect_linear_p(transformer tf, Pvecteur l): returns TRUE if there is a state s such that eval(l, s) != eval(l, tf(s)); returns false if l is invariant w.r.t. More... | |
bool | transformer_affect_transformer_p (transformer, transformer) |
Transformer tf1 affects transformer tf2 if values modified by tf1 appear in any constraint of tf2. More... | |
bool | transformer_safe_affect_transformer_p (transformer, transformer) |
transformer | args_to_transformer (list) |
Generates a transformer abstracting a totally unknown modification of the values associated to variables in list le. More... | |
transformer | invariant_wrt_transformer (transformer, transformer) |
transformer invariant_wrt_transformer(transformer p, transformer tf): Assume that tf is a fix-point operator. More... | |
transformer | transformer_value_substitute (transformer, entity, entity) |
transformer transformer_value_substitute(transformer t, entity e1, entity e2): if e2 does not appear in t initially: replaces occurences of value e1 by value e2 in transformer t's arguments and relation fields; else error fi More... | |
bool | transformer_value_substitutable_p (transformer, entity, entity) |
If e1 does not appear in t, it is substitutable. More... | |
transformer | transformer_safe_value_substitute (transformer, entity, entity) |
Pvecteur | simplify_float_constraint (Pvecteur, bool) |
If v is a not a float constraint, retun v. More... | |
Psysteme | simplify_float_constraint_system (Psysteme) |
Simplify float constraints and possibly detect. More... | |
bool | transformer_empty_p (transformer) |
If true is returned, the transformer certainly is empty. More... | |
bool | transformer_strongly_empty_p (transformer) |
If true is returned, the transformer certainly is empty. More... | |
bool | transformer_to_1D_lattice (entity, transformer, Value *, Value *) |
See if the equations in transformer "pre" constraint variable "v" by v = gcd x + c, where x is a free variable. More... | |
transformer | formal_and_actual_parameters_association (call, transformer) |
formal_and_actual_parameters_association(call c, transformer pre): Add equalities between actual and formal parameters binding by call c to pre pre := pre U {f = expr } i i for all i such that formal fi is an integer scalar variable and expression expr-i is affine More... | |
bool | same_dimension_p (entity, entity, list, size_t, transformer) |
This function returns true if the actual array and the dummy array have the same dimension number i, with respect to the current context (precondition + association) In case if the actual argument is an array element, we have to add the following condition: the i-th subscript of the array element is equal to its correspond lower bound. More... | |
list | transformer_to_potential_stub_translation (transformer, entity) |
list | transformer_to_analyzed_array_locations (transformer) |
list | transformer_to_analyzed_locations (transformer) |
The list of location entities that appear in the basis of the transformer predicate. More... | |
list | transformer_to_analyzed_arrays (transformer) |
The list of array entities that appear in the basis of the transformer predicate as array element locations. More... | |
list | transformer_to_local_values (transformer, list) |
Build a list of values appearing in tf that are linked to a variable in dl. More... | |
bool | hash_entity_to_values_undefined_p (void) |
value.c More... | |
void | reset_value_counters (void) |
void | reset_temporary_value_counter (void) |
int | number_of_temporary_values (void) |
void | set_analyzed_types (void) |
void | reset_analyzed_types (void) |
bool | integer_analyzed_p (void) |
bool | boolean_analyzed_p (void) |
bool | string_analyzed_p (void) |
bool | float_analyzed_p (void) |
bool | complex_analyzed_p (void) |
bool | pointer_analyzed_p (void) |
bool | constant_path_analyzed_p (void) |
bool | analyzed_basic_p (basic) |
The basic corresponds to one of the analyzed types. More... | |
bool | analyzed_type_p (type) |
The type t is one of the analyzed types. More... | |
bool | analyzed_struct_p (entity) |
Does struct s contain directly or indirectly a field that may be analyzable? More... | |
bool | analyzed_struct_type_p (type) |
bool | analyzed_array_p (entity) |
Does array a contain directly or indirectly a field that may be analyzable? More... | |
bool | analyzed_array_type_p (type) |
bool | analyzed_entity_p (entity) |
bool | analyzable_scalar_entity_p (entity) |
The entity type is one of the analyzed types. More... | |
bool | analyzed_constant_p (entity) |
The constant may appear as a variable in the linear systems. More... | |
bool | analyzed_reference_p (reference) |
FI: Nelson explains the motivation for can_be_constant_path_p() but I do not understand them. More... | |
entity | make_local_temporary_value_entity (type) |
entity | make_local_temporary_value_entity_with_basic (basic) |
entity | make_local_temporary_integer_value_entity (void) |
bool | local_old_value_entity_p (entity) |
Return true if an entity is a local old value (such as "o#0" for a global value "i#init"...). More... | |
bool | local_intermediate_value_entity_p (entity) |
bool | local_temporary_value_entity_p (entity) |
bool | global_new_value_p (entity) |
GLOBAL VALUES. More... | |
bool | global_old_value_p (entity) |
Return true if an entity is a global old value (such as "i#init"...). More... | |
bool | global_intermediate_value_p (entity) |
entity | global_new_value_to_global_old_value (entity) |
const char * | global_value_name_to_user_name (const char *) |
HASH TABLE USE. More... | |
const char * | external_value_name (entity) |
const char * | pips_user_value_name (entity) |
This function is called many times when the constraints and the system of constraints are sorted using lexicographic information based on this particular value name. More... | |
entity | entity_to_new_value (entity) |
entity | entity_to_old_value (entity) |
entity | entity_to_intermediate_value (entity) |
entity | reference_to_address_of_value (reference) |
entity | type_to_sizeof_value (type) |
bool | entity_has_values_p (entity) |
This function could be made more robust by checking the storage of e. More... | |
bool | new_value_entity_p (entity) |
the following three functions are directly or indirectly relative to the current module and its value hash tables. More... | |
bool | old_value_entity_p (entity) |
bool | intermediate_value_entity_p (entity) |
bool | address_of_value_entity_p (entity) |
bool | sizeof_value_entity_p (entity) |
bool | value_entity_p (entity) |
void | print_value_mappings (void) |
list | modified_variables_with_values (void) |
Return the list of all analyzed variables which are modified in the current module. More... | |
void | test_mapping_entry_consistency (void) |
int | number_of_analyzed_values (void) |
int | aproximate_number_of_analyzed_variables (void) |
int | number_of_analyzed_variables (void) |
FI: looks more like the number of values used. More... | |
void | allocate_value_mappings (int, int, int) |
bool | hash_value_to_name_undefined_p (void) |
void | error_reset_value_mappings (void) |
To be called by error handler only. More... | |
void | free_value_mappings (void) |
Normal call to free the mappings. More... | |
void | error_free_value_mappings (void) |
To be called by an error handler. More... | |
entity | reference_to_address_entity (reference) |
The address is the address of a variable or of a reference such as &a[5], not a of a value. More... | |
void | add_address_of_value (reference, type) |
void | add_sizeof_value (type) |
For a given architecture, sizeof(t) is a constant. More... | |
void | add_new_value (entity) |
void | add_new_alias_value (entity, entity) |
entity | external_entity_to_new_value (entity) |
entity | external_entity_to_old_value (entity) |
void | add_old_value (entity) |
void | add_old_alias_value (entity, entity) |
void | add_intermediate_value (entity) |
void | add_intermediate_alias_value (entity, entity) |
void | add_local_old_value (entity) |
void | add_local_intermediate_value (entity) |
void | remove_entity_values (entity, bool) |
void | add_synonym_values (entity, entity, bool) |
entity | value_to_variable (entity) |
Get the primitive variable associated to any value involved in a transformer. More... | |
entity | old_value_to_new_value (entity) |
entity | new_value_to_old_value (entity) |
entity | value_alias (entity) |
Static aliasing. More... | |
Pvecteur | vect_variables_to_values (Pvecteur) |
FI: not used, not debugged. More... | |
string | value_full_name (entity) |
for debugging purposes More... | |
const char * | readable_value_name (entity) |
For debugging purposes, we might have to print system with temporary values. More... | |
string | transformer_to_string (transformer) |
prettyprint.c More... | |
string | precondition_to_string (transformer) |
string | arguments_to_string (string, list) |
string | relation_to_string (string, Psysteme, char *(*)(entity)) |
const char * | generic_value_name (entity) |
list | merge_transformer_lists (list, list) |
transformer_list.c More... | |
bool | check_transformer_list (list) |
What do we want to impose? More... | |
list | combine_transformer_lists (list, list) |
each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer. More... | |
list | apply_transformer_lists_generic (list, list, bool) |
each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer. More... | |
list | apply_transformer_lists (list, list) |
list | apply_transformer_lists_with_exclusion (list, list) |
list | clean_up_transformer_list (list) |
Eliminate empty transformers and keep at most one identity transformer, placed as first list element. More... | |
list | two_transformers_to_list (transformer, transformer) |
Transformer two transformers into a correct transformer list. More... | |
transformer | generic_transformer_list_to_transformer (list, bool) |
Reduce the transformer list with the convex hull operator. More... | |
transformer | transformer_list_to_transformer (list) |
Reduce the transformer list ltl to one transformer using the convex hull operator. More... | |
transformer | active_transformer_list_to_transformer (list) |
Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator. More... | |
list | transformer_list_to_active_transformer_list (list) |
transformer | transformer_list_closure_to_precondition (list, transformer, transformer) |
Relay to select a heuristic. More... | |
list | transformer_list_safe_variables_projection (list, list) |
Returns a new list of newly allocated projected transformers. More... | |
list | transformer_list_to_argument (list) |
Returns the list of variables modified by at least one transformer in tl. More... | |
list | transformer_list_with_effect (list, entity) |
build a sublist sl of the transformer list tl with transformers that modify the value of variable v More... | |
list | transformer_list_preserved_variables (list, list, list) |
returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v. More... | |
transformer | transformer_list_multiple_closure_to_precondition (list, transformer, transformer) |
When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition. More... | |
Psysteme | transformer_derivative_constraints (transformer) |
Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x') More... | |
transformer | transformer_list_generic_transitive_closure (list, bool) |
Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers. More... | |
transformer | transformer_list_transitive_closure (list) |
Compute (U tfl)*. More... | |
transformer | transformer_list_transitive_closure_plus (list) |
Compute (U tfl)+. More... | |
Variables | |
transformer(* | transformer_fix_point_operator )(transformer) |
fix_point.c More... | |
#define ADDRESS_OF_SUFFIX "#addressof" |
Definition at line 56 of file transformer.h.
#define INTERMEDIATE_VALUE_PREFIX "i#" |
Definition at line 46 of file transformer.h.
#define INTERMEDIATE_VALUE_SUFFIX "#int" |
Definition at line 54 of file transformer.h.
#define NEW_VALUE_SUFFIX "#new" |
external suffixes (NEW_VALUE_SUFFIX is not used, new values are represented by the variable itself, i.e.
new value suffix is the empty string "")
Definition at line 52 of file transformer.h.
#define OLD_VALUE_PREFIX "o#" |
internal entity names (FI: I should have used suffixes to be consistent with external suffixes
Definition at line 45 of file transformer.h.
#define OLD_VALUE_SUFFIX "#init" |
Definition at line 53 of file transformer.h.
#define SEMANTICS_MODULE_NAME "*SEMANTICS*" |
Warning! Do not modify this file that is automatically generated!
Modify src/Libs/transformer/transformer-local.h instead, to add your own modifications. header file built by cproto transformer-local.h include file for transformer library prefix used for value entity names; no conflict should occur with user function names as long as they are restricted to 6 characters
Definition at line 38 of file transformer.h.
#define SEMANTICS_SEPARATOR '#' |
Must be used in suffixes and prefixes below.
Definition at line 41 of file transformer.h.
#define SIZEOF_SUFFIX "#sizeof" |
Definition at line 58 of file transformer.h.
#define TEMPORARY_VALUE_PREFIX "t#" |
Definition at line 47 of file transformer.h.
transformer active_transformer_list_to_transformer | ( | list | ltl | ) |
Reduce the sublist of active transformers in the transformer list ltl to one transformer using the convex hull operator.
An active transformer is a transformer with argument(s): at least one value is changed.
Note: a hidden identity transformer such as T(i) {i==i::init} is not detected.
ltl | tl |
Definition at line 447 of file transformer_list.c.
References generic_transformer_list_to_transformer().
Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and whileloop_to_postcondition().
add the couple (e, address_of_value)
add its name
Definition at line 1309 of file value.c.
References ADDRESS_OF_SUFFIX, concatenate(), copy_type(), entity_domain, entity_name, entity_undefined, entity_user_name(), gen_find_tabulated(), hash_entity_to_user_value_name, hash_get(), hash_put(), hash_reference_to_address_of_value, HASH_UNDEFINED_VALUE, hash_value_to_name, is_storage_rom, make_entity, make_storage(), pips_internal_error, reference_to_string(), reference_variable, strdup(), UU, value_to_variable(), and value_undefined.
add_new_value_name(e);
Definition at line 1495 of file value.c.
References entity_to_intermediate_value(), entity_undefined, hash_entity_to_intermediate_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, and pips_assert.
Referenced by add_interprocedural_value_entities().
void add_intermediate_value | ( | entity | e | ) |
get a new intermediate value, if necessary
add its (external) name
Definition at line 1476 of file value.c.
References concatenate(), entity_name, entity_type, hash_entity_to_intermediate_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_value_to_name, INTERMEDIATE_VALUE_SUFFIX, make_local_intermediate_value_entity(), and strdup().
Referenced by add_interprocedural_value_entities(), add_or_kill_equivalenced_variables(), convex_in_effect_loop_range_fix(), and interlaced_basic_workchunk_regions_p().
void add_local_intermediate_value | ( | entity | e | ) |
get a new intermediate value, if necessary
add its (external) name
Definition at line 1526 of file value.c.
References concatenate(), entity_name, entity_type, hash_entity_to_intermediate_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_value_to_name, INTERMEDIATE_VALUE_SUFFIX, make_local_intermediate_value_entity(), and strdup().
Referenced by add_intraprocedural_value_entities_unconditionally().
void add_local_old_value | ( | entity | e | ) |
get a new old value, if necessary
add its (external) name
Definition at line 1509 of file value.c.
References concatenate(), entity_name, entity_type, hash_entity_to_old_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_value_to_name, make_local_old_value_entity(), OLD_VALUE_SUFFIX, and strdup().
Referenced by add_intraprocedural_value_entities_unconditionally().
add_new_value_name(e);
Definition at line 1396 of file value.c.
References entity_name, entity_to_new_value(), entity_undefined, hash_entity_to_new_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, pips_assert, and pips_debug.
Referenced by add_interprocedural_new_value_entity(), and add_interprocedural_value_entities().
void add_new_value | ( | entity | e | ) |
Definition at line 1386 of file value.c.
References add_new_value_name(), entity_name, hash_entity_to_new_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, and pips_debug.
Referenced by add_interprocedural_new_value_entity(), add_interprocedural_value_entities(), add_intraprocedural_value_entities_unconditionally(), and add_or_kill_equivalenced_variables().
add_new_value_name(e);
Definition at line 1463 of file value.c.
References entity_to_old_value(), entity_undefined, hash_entity_to_old_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, and pips_assert.
Referenced by add_interprocedural_value_entities().
void add_old_value | ( | entity | e | ) |
find the old value entity if possible, else, generate it
add the couple (e, old_value)
add its name
Definition at line 1440 of file value.c.
References concatenate(), copy_type(), entity_domain, entity_name, entity_type, entity_undefined, gen_find_tabulated(), hash_entity_to_old_value, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_value_to_name, is_storage_rom, make_entity, make_storage(), OLD_VALUE_SUFFIX, strdup(), UU, and value_undefined.
Referenced by add_interprocedural_value_entities(), add_or_kill_equivalenced_variables(), and add_synonym_values().
void add_sizeof_value | ( | type | t | ) |
For a given architecture, sizeof(t) is a constant.
It has no old value, no new value, it is a value.
Constants are encoded as 0-ary functions, not as values.
find the sizeof entity if possible, else, generate it
add the couple (e, old_value)
add its name
Definition at line 1352 of file value.c.
References concatenate(), copy_type(), entity_domain, entity_name, entity_undefined, gen_find_tabulated(), hash_entity_to_new_value, hash_entity_to_user_value_name, hash_get(), hash_put(), hash_type_to_sizeof_value, HASH_UNDEFINED_VALUE, hash_value_to_name, is_storage_rom, make_entity, make_storage(), MODULE_SEP_STRING, SIZEOF_SUFFIX, strdup(), TOP_LEVEL_MODULE_NAME, type_to_full_string_definition(), UU, and value_undefined.
Referenced by expression_multiply_sizeof_to_transformer().
e and eq are entities whose values are always equal because they share the exact same memory location (i.e. they are alias). Values for e have already been declared. Values for eq have to be declared.
hash_put(hash_value_to_name, (char *) old_value_eq, entity_name(old_value_eq));
The name does not change. It is not used until the equivalence equations are added
eq | q |
readonly | eadonly |
Definition at line 1578 of file value.c.
References add_old_value(), concatenate(), entity_local_name(), entity_name, entity_to_intermediate_value(), entity_to_new_value(), entity_to_old_value(), eq, hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_put(), hash_update(), hash_value_to_name, NEW_VALUE_SUFFIX, pips_debug, and strdup().
Referenced by add_equivalenced_values().
void add_value_to_transformer_space | ( | entity | v, |
transformer | tf | ||
) |
tf | f |
Definition at line 859 of file basic.c.
References predicate_system, sc_base_add_variable(), and transformer_relation.
Referenced by transformer_add_variable_type_information().
Definition at line 962 of file value.c.
References ADDRESS_OF_SUFFIX, and entity_local_name().
Referenced by pips_user_value_name(), and value_to_variable().
Definition at line 1165 of file value.c.
References hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_entity_to_user_value_name, hash_pointer, hash_reference_to_address_of_value, hash_table_make(), hash_table_undefined_p, hash_type_to_sizeof_value, hash_value_to_name, and pips_assert.
Referenced by allocate_module_value_mappings().
The entity type is one of the analyzed types.
Definition at line 471 of file value.c.
References abstract_state_variable_p(), analyzed_type_p(), entity_basic_concrete_type(), entity_heap_location_p(), entity_typed_anywhere_locations_p(), place_holder_variable_p(), and typedef_entity_p().
Referenced by add_implicit_interprocedural_write_effects(), add_or_kill_equivalenced_variables(), any_user_call_site_to_transformer(), c_return_to_transformer(), external_entity_to_new_value(), generic_reference_to_transformer(), module_to_formal_analyzable_parameters(), module_to_value_mappings(), precondition_intra_to_inter(), and same_analyzable_type_scalar_entity_list_p().
Does array a contain directly or indirectly a field that may be analyzable?
Definition at line 434 of file value.c.
References analyzed_struct_type_p(), analyzed_type_p(), array_type_to_element_type(), entity_basic_concrete_type(), and struct_type_p().
at | t |
Definition at line 446 of file value.c.
References analyzed_struct_type_p(), analyzed_type_p(), array_type_to_element_type(), and struct_type_p().
Referenced by analyzed_entity_p(), and analyzed_struct_type_p().
The basic corresponds to one of the analyzed types.
Definition at line 337 of file value.c.
References analyze_boolean_scalar_entities, analyze_complex_scalar_entities, analyze_float_scalar_entities, analyze_integer_scalar_entities, analyze_pointer_scalar_entities, analyze_string_scalar_entities, basic_complex_p, basic_derived, basic_derived_p, basic_float_p, basic_int_p, basic_logical_p, basic_pointer, basic_pointer_p, basic_string_p, entity_basic_concrete_type(), pips_debug, type_enum_p, and type_to_string().
Referenced by analyzed_type_p(), and condition_to_transformer().
The constant may appear as a variable in the linear systems.
is f a 0-ary function, i.e. a constant of proper type?
integer and logical constants are handled explicitly
Definition at line 487 of file value.c.
References analyze_complex_scalar_entities, analyze_float_scalar_entities, analyze_pointer_scalar_entities, analyze_string_scalar_entities, basic_complex_p, basic_float_p, basic_pointer_p, basic_string_p, entity_constant_p, entity_type, f(), functional_result, type_functional, type_variable, and variable_basic.
Referenced by value_mappings_compatible_vector_p().
Definition at line 457 of file value.c.
References analyzed_array_type_p(), analyzed_struct_type_p(), analyzed_type_p(), array_type_p(), entity_basic_concrete_type(), and struct_type_p().
Referenced by generic_substitute_formal_array_elements_in_transformer().
FI: Nelson explains the motivation for can_be_constant_path_p() but I do not understand them.
He also explains the motivation for strict_constant_path_p() and I do not understand them either.
Stricly speaking, this funtion should be called analyzed_points_to_reference_p()
Definition at line 518 of file value.c.
References analyzed_type_p(), effects_package_entity_p(), generic_atomic_points_to_reference_p(), pips_debug, points_to_reference_to_concrete_type(), reference_to_string(), reference_variable, and store_independent_points_to_reference_p().
Referenced by any_assign_to_transformer(), any_basic_update_to_transformer(), any_update_to_transformer(), assign_rhs_to_reflhs_to_transformer(), generic_apply_effect_to_transformer(), lhs_expression_to_transformer(), module_to_value_mappings(), points_to_unary_operation_to_transformer(), and substitute_stubs_in_transformer().
Does struct s contain directly or indirectly a field that may be analyzable?
Definition at line 387 of file value.c.
References analyzed_struct_p(), analyzed_type_p(), ENTITY, entity_basic_concrete_type(), f(), FOREACH, struct_type_p(), and struct_variable_to_fields().
Referenced by analyzed_struct_p().
st | t |
Definition at line 406 of file value.c.
References analyzed_array_type_p(), analyzed_struct_type_p(), analyzed_type_p(), array_type_p(), ENTITY, entity_basic_concrete_type(), f(), FOREACH, struct_type_p(), and struct_type_to_fields().
Referenced by analyzed_array_p(), analyzed_array_type_p(), analyzed_entity_p(), and analyzed_struct_type_p().
The type t is one of the analyzed types.
Definition at line 367 of file value.c.
References analyzed_basic_p(), compute_basic_concrete_type(), ENDP, type_variable, type_variable_p, variable_basic, variable_dimensions, and volatile_variable_p().
Referenced by add_inter_or_intraprocedural_field_entities(), analyzable_scalar_entity_p(), analyzed_array_p(), analyzed_array_type_p(), analyzed_entity_p(), analyzed_reference_p(), analyzed_struct_p(), analyzed_struct_type_p(), assign_rhs_to_reflhs_to_transformer(), call_to_transformer(), create_values_for_simple_effect(), expression_to_transformer(), generic_reference_to_transformer(), generic_substitute_formal_array_elements_in_transformer(), make_local_temporary_value_entity(), module_to_value_mappings(), perform_array_element_substitutions_in_transformer(), semantics_usable_points_to_reference_p(), substitute_struct_stub_in_transformer(), and transformer_apply_field_assignments_or_equalities().
transformer any_transformer_to_k_closure | ( | transformer | t_init, |
transformer | t_enter, | ||
transformer | t_next, | ||
transformer | t_body, | ||
transformer | post_init, | ||
int | k, | ||
bool | assume_previous_iteration_p | ||
) |
Derived from any_loop_to_k_transformer()
The recursive computation of the loop transformer is not performed here.
Complete the body transformer with t_next (t_body is modified by side effects into t_fbody)
Compute the fix point
Compute t_body_star = t_init ; t_enter
and add the continuation condition, pre_iteration improved with knowledge about the body, npre_iteration. Note that pre_iteration would also provide correct results, although less accurate.
FI: this is a very strong normalization
obvious redundancy like 0<=x, x<=y, 0<=y is detected
Integer redundancy elimination is aso used and leads potentially to larger coefficients and ultimately to an accuracy reduction when a convex hull is performed.
Any transformer or other data structure to free?
t_init | _init |
t_enter | _enter |
t_next | _next |
t_body | _body |
post_init | ost_init |
assume_previous_iteration_p | ssume_previous_iteration_p |
Definition at line 1304 of file fix_point.c.
References copy_transformer(), fprintf(), free_transformer(), ifdebug, print_transformer, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_intersect_range_with_domain(), transformer_range(), and transformer_undefined.
Referenced by any_loop_to_k_transformer().
tl1 | l1 |
tl2 | l2 |
Definition at line 269 of file transformer_list.c.
References apply_transformer_lists_generic().
each transformer of tl1 must be applied to each precondition of tl2, including the identity transformer.
If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list. Empty preconditions are not preserved in the returned list. An empty list is unfeasible.
if exclude_p==false, return U_i1 U_i2 apply(t_i1, p_i2); else return U_i1 U_i2!=i1 apply(t_i1, p_i2);
tl1 | l1 |
tl2 | l2 |
exclude_p | xclude_p |
Definition at line 223 of file transformer_list.c.
References check_transformer_list(), CONS, FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_apply(), and transformer_empty_p().
Referenced by apply_transformer_lists(), and apply_transformer_lists_with_exclusion().
tl1 | l1 |
tl2 | l2 |
Definition at line 274 of file transformer_list.c.
References apply_transformer_lists_generic().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
int aproximate_number_of_analyzed_variables | ( | void | ) |
FI: I do not know if equivalenced variables are well taken into account
Definition at line 1153 of file value.c.
References hash_entity_to_new_value, and hash_table_entry_count().
Referenced by module_to_value_mappings().
transformer args_to_transformer | ( | list | le | ) |
Generates a transformer abstracting a totally unknown modification of the values associated to variables in list le.
list of entities
le | e |
Definition at line 1907 of file transformer.c.
References arguments_add_entity(), Ssysteme::base, CAR, Ssysteme::dimension, ENTITY, entity_to_new_value(), MAPL, predicate_system_, sc_new(), transformer_arguments, transformer_identity(), transformer_relation, vect_add_variable(), vect_size(), and VECTEUR_NUL.
Referenced by add_loop_index_exit_value(), and invariant_wrt_transformer().
args | rgs |
Definition at line 65 of file prettyprint.c.
References pips_internal_error, and string_undefined.
bool boolean_analyzed_p | ( | void | ) |
Definition at line 305 of file value.c.
References analyze_boolean_scalar_entities.
Referenced by any_expression_to_transformer(), and fortran_data_to_prec_for_variables().
void build_transfer_equations | ( | Pcontrainte | leq, |
Pcontrainte * | plteq, | ||
Pbase * | pb_new | ||
) |
FI: this is the simplest version; It would be possible to build a larger set of transfer equations by adding indirect transfer equations using a new basis till the set is stable, and then by removing equations containing old values which are not defined, again till the result is stable
I guess that these new equations would not change the fix-point and/or the preconditions.
derive the new basis and the old basis
check that the old basis is included in the new basis (else no fix-point!)
Remove equations as long b_old is not included in b_new
could be avoided by using only lteq...
leq | eq |
plteq | lteq |
pb_new | b_new |
Definition at line 433 of file fix_point.c.
References base_contains_variable_p(), base_difference(), base_fprint(), BASE_NULLE, BASE_NULLE_P, base_rm, BASE_UNDEFINED, contrainte_dup(), contrainte_rm, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, egalites_fprint(), eq, equations_to_bases(), external_value_name(), ifdebug, pips_debug, pips_internal_error, sub_basis_p(), Scontrainte::succ, Svecteur::succ, transfer_equation_p(), VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by transformer_equality_fix_point().
What do we want to impose?
The empty transformer list is used to represent the empty transformer...
It must be the first one
tl | l |
Definition at line 140 of file transformer_list.c.
References CAR, ENDP, FOREACH, pips_internal_error, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().
Referenced by apply_transformer_lists_generic(), combine_transformer_lists(), and merge_transformer_lists().
Eliminate empty transformers and keep at most one identity transformer, placed as first list element.
check_transformer_list(ntfl) should be TRUE.
tfl is fully destroyed (to avoid memory leaks and nightmares); to be more efficient, the transformers moved from the input list into the output list should be detached from the input list and then the input list could be fully destroyed without having to copy any transformers; but FOREACH operates at too high a level for this.
tfl | fl |
Definition at line 290 of file transformer_list.c.
References CONS, copy_transformer(), FOREACH, gen_full_free_list(), gen_nreverse(), NIL, TRANSFORMER, transformer_empty_p(), transformer_identity(), and transformer_identity_p().
Referenced by block_to_transformer_list().
each transformer of tl1 must be combined with a transformer of tl2, including the identity transformer.
If an identity transformer is generated and if identity transformers are always first in the list, it will again be first in the returned list.
tl1 | l1 |
tl2 | l2 |
Definition at line 180 of file transformer_list.c.
References check_transformer_list(), CONS, copy_transformer(), FOREACH, gen_length(), gen_nreverse(), NIL, pips_assert, TRANSFORMER, transformer_combine(), transformer_empty_p(), and transformer_normalize().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
bool complex_analyzed_p | ( | void | ) |
Definition at line 320 of file value.c.
References analyze_complex_scalar_entities.
bool constant_path_analyzed_p | ( | void | ) |
Definition at line 330 of file value.c.
References analyze_constant_path.
Referenced by any_assign_to_transformer(), assign_rhs_to_reflhs_to_transformer(), basic_update_reflhs_with_rhs_to_transformer(), generic_apply_effect_to_transformer(), integer_call_expression_to_transformer(), lhs_expression_to_transformer(), module_to_value_mappings(), process_call_for_summary_precondition(), and update_reflhs_with_rhs_to_transformer().
Pcontrainte constraints_eliminate_constant_terms | ( | Pcontrainte | lc, |
Pvecteur | v | ||
) |
cv may now be the null vector
lc | c |
Definition at line 865 of file fix_point.c.
References abort, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, TCST, vect_cl(), vect_coeff(), and vect_multiply().
Referenced by sc_eliminate_constant_terms().
Pcontrainte constraints_keep_invariants_only | ( | Pcontrainte | lc | ) |
lc | c |
Definition at line 910 of file fix_point.c.
References contrainte_succ, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, invariant_vector_p(), vect_rm(), and VECTEUR_NUL.
Referenced by sc_keep_invariants_only().
void dump_transformer | ( | transformer | tf | ) |
tf | f |
Definition at line 134 of file io.c.
References dump_value_name(), and fprint_transformer().
char* dump_value_name | ( | entity | e | ) |
char * dump_value_name(e): used as functional argument because entity_name is a macro
FI: should be moved in ri-util/entity.c
Definition at line 128 of file io.c.
References entity_name.
Referenced by check_range_wrt_precondition(), dump_transformer(), fortran_user_call_to_transformer(), print_value_mappings(), transformer_combine(), and translate_global_values().
transformer empty_transformer | ( | transformer | t | ) |
Do not allocate an empty transformer, but transform an allocated transformer into an empty_transformer.
Pretty dangerous because the predicate contained in t may have been deleted before empty_transformer is called. It is not clear that the predicate of t can be freed or not: it is up to the caller to be aware of the problem.
This function is risky to use. It can cause either a memory leak if the predicate is not freed, or a double free if the pointer in the transformer is already dangling. If the predicate has already been freed during some processing at the linear level, the caller must update the pointer transformer_relation(t) with:
transformer_relation(t) = relation_undefined;
before the call.
Definition at line 144 of file basic.c.
References BASE_NULLE, free_predicate(), gen_free_list(), make_predicate(), NIL, sc_empty(), transformer_arguments, and transformer_relation.
Referenced by modulo_by_a_constant_to_transformer(), statement_to_postcondition(), transformer_combine(), transformer_convex_hulls(), transformer_projection_with_redundancy_elimination_and_check(), and whileloop_to_postcondition().
This function could be made more robust by checking the storage of e.
Formal parameters of analyzed type always have values.
is e a variable whose value(s) (already) are analyzed?
Definition at line 911 of file value.c.
References hash_defined_p(), hash_entity_to_new_value, hash_table_undefined_p, and pips_assert.
Referenced by add_index_range_conditions(), add_inter_or_intraprocedural_field_entities(), add_interprocedural_new_value_entity(), add_interprocedural_value_entities(), add_intraprocedural_value_entities(), add_loop_index_exit_value(), add_or_kill_equivalenced_variables(), any_assign_operation_to_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), apply_abstract_effect_to_transformer(), assign_operation_to_transformer(), assigned_expression_to_transformer(), assigned_expression_to_transformer_list(), c_data_to_prec_for_variables(), declaration_to_transformer(), declaration_to_transformer_list(), dynamic_variables_to_values(), effects_to_arguments(), filter_transformer(), fortran_data_to_prec_for_variables(), fortran_user_call_to_transformer(), generic_apply_effect_to_transformer(), generic_reference_to_transformer(), generic_unary_operation_to_transformer(), integer_assign_to_transformer(), integer_assign_to_transformer_list(), logical_reference_to_transformer(), loop_bound_evaluation_to_transformer(), module_to_value_mappings(), noms_var(), pips_user_value_name(), pointer_unary_operation_to_transformer(), safe_assigned_expression_to_transformer(), safe_assigned_expression_to_transformer_list(), string_expression_to_transformer(), substitute_scalar_stub_in_transformer(), substitute_stubs_in_transformer(), transformer_add_condition_information_updown(), transformer_add_loop_index_incrementation(), transformer_add_loop_index_initialization(), transformer_add_modified_variable_entity(), transformer_add_variable_type_information(), transformer_filter_subsumed_variables(), transformer_general_consistency_p(), transformer_projection_with_redundancy_elimination_and_check(), transformer_variables_filter(), value_mappings_compatible_vector_p(), variable_to_values(), and variables_to_values().
Definition at line 879 of file value.c.
References entity_name, entity_undefined, hash_entity_to_intermediate_value, hash_get(), and pips_internal_error.
Referenced by add_intermediate_alias_value(), add_synonym_values(), convex_in_effect_loop_range_fix(), external_value_name(), interlaced_basic_workchunk_regions_p(), remove_entity_values(), transformer_combine(), transformer_derivative_constraints(), transformer_derivative_fix_point(), and transformer_list_generic_transitive_closure().
Definition at line 859 of file value.c.
References entity_name, entity_undefined, hash_entity_to_new_value, hash_get(), and pips_internal_error.
Referenced by add_affine_bound_conditions(), add_loop_index_exit_value(), add_new_alias_value(), add_synonym_values(), affine_to_transformer(), any_assign_operation_to_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), args_to_transformer(), assign_operation_to_transformer(), assigned_expression_to_transformer(), assigned_expression_to_transformer_list(), comp_regions_of_implied_do(), dynamic_variables_to_values(), external_value_name(), filter_transformer(), fortran_user_call_to_transformer(), generic_reference_to_transformer(), logical_reference_to_transformer(), loop_bound_evaluation_to_transformer(), old_value_to_new_value(), remove_entity_values(), string_expression_to_transformer(), substitute_scalar_stub_in_transformer(), substitute_stubs_in_transformer_with_translation_binding(), transformer_add_condition_information_updown(), transformer_add_identity(), transformer_add_loop_index_incrementation(), transformer_add_modified_variable_entity(), transformer_add_value_update(), transformer_add_variable_incrementation(), transformer_add_variable_type_information(), transformer_add_variable_update(), transformer_argument_general_consistency_p(), transformer_arguments_projection(), transformer_convex_hulls(), transformer_derivative_constraints(), transformer_derivative_fix_point(), transformer_domain_intersection(), transformer_internal_consistency_p(), transformer_list_generic_transitive_closure(), transformer_to_domain(), transformer_variables_filter(), update_cp_with_rhs_to_transformer(), value_mappings_compatible_vector_p(), value_passing_summary_transformer(), variable_to_values(), variables_to_new_values(), variables_to_values(), and vect_variables_to_values().
Definition at line 869 of file value.c.
References entity_name, entity_undefined, hash_entity_to_old_value, hash_get(), and pips_internal_error.
Referenced by add_old_alias_value(), add_synonym_values(), add_type_information(), affine_to_transformer(), any_assign_operation_to_transformer(), any_basic_update_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(), dynamic_variables_to_values(), external_value_name(), fortran_user_call_to_transformer(), new_value_to_old_value(), perform_array_element_substitutions_in_transformer(), precondition_intra_to_inter(), remove_entity_values(), safe_transformer_projection(), statement_to_postcondition(), statement_to_total_precondition(), substitute_scalar_stub_in_transformer(), substitute_stubs_in_transformer_with_translation_binding(), transformer_add_identity(), transformer_add_loop_index_incrementation(), transformer_add_loop_index_initialization(), transformer_add_modified_variable_entity(), transformer_add_value_update(), transformer_add_variable_incrementation(), transformer_add_variable_update(), transformer_arguments_projection(), transformer_combine(), transformer_convex_hulls(), transformer_domain_intersection(), transformer_intersect_range_with_domain(), transformer_list_safe_variables_projection(), transformer_projection_with_redundancy_elimination_and_check(), transformer_range(), transformer_to_domain(), transformer_variables_filter(), update_cp_with_rhs_to_transformer(), value_passing_summary_transformer(), variable_to_values(), variables_to_old_values(), and variables_to_values().
void equations_to_bases | ( | Pcontrainte | lteq, |
Pbase * | pb_new, | ||
Pbase * | pb_old | ||
) |
lteq | teq |
pb_new | b_new |
pb_old | b_old |
Definition at line 660 of file fix_point.c.
References BASE_UNDEFINED, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, eq, new_value_entity_p(), old_value_to_new_value(), Scontrainte::succ, Svecteur::succ, TCST, vect_add_variable(), VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by build_transfer_equations().
void error_free_value_mappings | ( | void | ) |
To be called by an error handler.
free previous hash tables, desallocate names; this implies ALL value names were malloced and were not pointer to a ri part
the three tables are assumed to be allocated all together
free names in hash_value_to_name; the other two hash tables contain pointers to the entity tabulated domain and thus need no value freeing
k is discovered unused by lint; it is syntaxically necessary
free the three tables themselves
Definition at line 1222 of file value.c.
References free(), hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_entity_to_user_value_name, HASH_MAP, hash_reference_to_address_of_value, hash_table_free(), hash_type_to_sizeof_value, hash_value_to_name, reset_analyzed_types(), reset_temporary_value_counter(), and reset_value_mappings().
Referenced by free_value_mappings().
void error_reset_value_mappings | ( | void | ) |
To be called by error handler only.
Potential memory leak.
Definition at line 1205 of file value.c.
References reset_value_mappings().
Referenced by free_value_mappings(), and module_to_value_mappings().
there is no decisive test here; a necessary condition is used instead
Definition at line 1411 of file value.c.
References analyzable_scalar_entity_p(), and pips_assert.
Referenced by add_formal_to_actual_bindings(), formal_and_actual_parameters_association(), fortran_user_call_to_transformer(), generic_reference_to_transformer(), logical_reference_to_transformer(), and substitute_stubs_in_transformer_with_translation_binding().
find the old value entity if possible or abort I should never have to call this function on an local entity (local entities include static local variables)
Definition at line 1422 of file value.c.
References concatenate(), entity_domain, entity_name, entity_undefined, gen_find_tabulated(), OLD_VALUE_SUFFIX, and pips_assert.
Referenced by fortran_user_call_to_transformer(), perform_array_element_substitutions_in_transformer(), and substitute_stubs_in_transformer_with_translation_binding().
const char* external_value_name | ( | entity | e | ) |
This should never occur. Please core dump!
Definition at line 753 of file value.c.
References entity_constant_p, entity_local_name(), entity_name, entity_symbolic_p, entity_to_intermediate_value(), entity_to_new_value(), entity_to_old_value(), get_current_module_entity(), global_intermediate_value_p(), global_new_value_p(), global_old_value_p(), global_value_name_to_user_name(), hash_get(), HASH_UNDEFINED_VALUE, hash_value_to_name, module_local_name(), module_name(), null_pointer_value_entity_p(), pips_assert, pips_internal_error, string_undefined, TOP_LEVEL_MODULE_NAME, and variable_in_module_p().
Referenced by __attribute__(), add_loop_skip_condition(), build_transfer_equations(), complete_loop_transformer(), complete_loop_transformer_list(), intermediate_value_entity_p(), invariant_vector_p(), loop_to_transformer(), noms_var(), old_complete_whileloop_transformer(), pips_user_value_name(), print_transformer(), print_transformers(), print_value_mappings(), readable_value_name(), recompute_loop_transformer(), remove_entity_values(), standard_whileloop_to_transformer(), transformer_derivative_constraints(), transformer_derivative_fix_point(), transformer_equality_fix_point(), transformer_list_generic_transitive_closure(), transformer_normalize(), and transformer_pattern_fix_point().
bool float_analyzed_p | ( | void | ) |
Definition at line 315 of file value.c.
References analyze_float_scalar_entities.
Referenced by any_expression_to_transformer(), fortran_data_to_prec_for_variables(), parametric_transformer_empty_p(), and transformer_normalize().
transformer formal_and_actual_parameters_association | ( | call | c, |
transformer | pre | ||
) |
formal_and_actual_parameters_association(call c, transformer pre): Add equalities between actual and formal parameters binding by call c to pre pre := pre U {f = expr } i i for all i such that formal fi is an integer scalar variable and expression expr-i is affine
let's start a long, long, long MAPL, so long that MAPL is a pain
pre | re |
Definition at line 2542 of file transformer.c.
References call_arguments, call_function, CAR, debug(), dump_transformer, ENDP, ENTITY, entity_module_p(), entity_storage, entity_to_formal_integer_parameters(), expression_undefined, external_entity_to_new_value(), f(), find_ith_argument(), formal_offset, free_arguments(), ifdebug, module_local_name(), NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, pips_assert, POP, storage_formal, transformer_equality_add(), transformer_undefined, user_error, vect_add_elem(), and vect_dup().
Referenced by interprocedural_abc_arrays(), and translate_to_module_frame().
transformer fprint_transformer | ( | FILE * | fd, |
transformer | tf, | ||
get_variable_name_t | value_name | ||
) |
print_transformer returns an int to be compatible with the debug() function; however, debug being a function and not a macro, its arguments are ALWAYS evaluated regardless of the debug level; so a call to print_transformer passed as an argument to debug is ALWAYS effective
print argument list
print relation
fd | d |
tf | f |
value_name | alue_name |
Definition at line 69 of file io.c.
References fprintf(), pips_internal_error, predicate_system, print_homogeneous_arguments(), sc_fprint(), transformer_arguments, transformer_domain, transformer_domain_number, transformer_relation, and transformer_undefined.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), dump_transformer(), expression_equal_in_context_p(), expression_less_than_in_context(), fprint_transformers(), loop_to_transformer(), old_complete_whileloop_transformer(), print_any_transformer(), print_transformer(), standard_whileloop_to_transformer(), transformer_derivative_fix_point(), transformer_equality_fix_point(), transformer_filter(), transformer_list_generic_transitive_closure(), transformer_normalize(), transformer_pattern_fix_point(), and transformer_projection_with_redundancy_elimination_and_check().
list fprint_transformers | ( | FILE * | fd, |
list | tl, | ||
get_variable_name_t | value_name | ||
) |
fd | d |
tl | l |
value_name | alue_name |
Definition at line 105 of file io.c.
References ENDP, FOREACH, fprint_transformer(), fprintf(), and TRANSFORMER.
Referenced by print_transformers().
void free_transformers | ( | transformer | t, |
... | |||
) |
Analyze in args the variadic arguments that may be after t:
Since a variadic function in C must have at least 1 non variadic argument (here the s), just skew the varargs analysis:
Get the next argument:
Release the variadic analyzis:
Definition at line 73 of file basic.c.
References free_transformer().
Referenced by loop_to_enter_transformer().
void free_value_mappings | ( | void | ) |
Normal call to free the mappings.
Definition at line 1212 of file value.c.
References error_free_value_mappings(), error_reset_value_mappings(), hash_entity_to_old_value, hash_table_undefined_p, pips_assert, and reset_hooks_unregister().
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(), continuation_conditions(), dsc_code_parallelization(), generic_module_name_to_transformers(), generic_print_xml_application(), get_continuation_condition_text(), get_semantic_text(), hbdsc_parallelization(), 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(), reset_convex_in_out_regions(), reset_convex_rw_regions(), reset_convex_summary_in_out_regions(), reset_convex_summary_rw_regions(), 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 generic_equality_to_transformer | ( | entity | e, |
entity | f, | ||
bool | assignment, | ||
bool | unary_minus_p | ||
) |
assignment | ssignment |
unary_minus_p | nary_minus_p |
Definition at line 72 of file transformer.c.
References CONS, contrainte_make(), CONTRAINTE_UNDEFINED, dump_transformer, ENTITY, entity_local_name(), eq, f(), ifdebug, make_predicate(), make_transformer(), NIL, pips_debug, sc_make(), transformer_undefined, VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by simple_equality_to_transformer(), and simple_unary_minus_to_transformer().
transformer generic_transformer_list_to_transformer | ( | list | ltl, |
bool | active_p | ||
) |
Reduce the transformer list with the convex hull operator.
If active_p is true, skip transformers that do not update the state. Beyond the identity transformer, any transformer without arguments does not really update the state, although it may restrict it.
A new transformer is always allocated. The transformers in the transformer list ltl are freed.
Look for the first useful transformer in the list
Only range conditions have been found: the store is restricted but not changed.
Take care of the following useful transformers
Look for the next useful transformer in the list
ltl | tl |
active_p | ctive_p |
Definition at line 384 of file transformer_list.c.
References copy_transformer(), ENDP, FOREACH, free_transformer(), POP, TRANSFORMER, transformer_arguments, transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_undefined, and transformer_undefined_p.
Referenced by active_transformer_list_to_transformer(), and transformer_list_to_transformer().
const char* generic_value_name | ( | entity | e | ) |
else if (entity_has_values_p(e)){
n = external_value_name(e);
Definition at line 81 of file prettyprint.c.
References entity_domain, entity_minimal_name(), gen_check(), hash_value_to_name_undefined_p(), local_temporary_value_entity_p(), pips_user_value_name(), string_undefined, TCST, and value_entity_p().
Referenced by varval_value_name_is_inferior_p().
this is not a general test; it will only work for GLOBAL values
Definition at line 703 of file value.c.
References entity_local_name(), entity_module_name(), INTERMEDIATE_VALUE_SUFFIX, SEMANTICS_MODULE_NAME, and SEMANTICS_SEPARATOR.
Referenced by external_value_name().
GLOBAL VALUES.
this is not a general test; it will only work for GLOBAL values
this function should always return false because new value = variable (FI)
=> suf == NULL string suf = strchr(entity_local_name(e), SEMANTICS_SEPARATOR);
pips_assert("global_new_value", suf != NULL);
new = strcmp(entity_module_name(e), SEMANTICS_MODULE_NAME) != 0 && strcmp(suf, NEW_VALUE_SUFFIX) == 0;
Definition at line 667 of file value.c.
References pips_assert.
Referenced by external_value_name().
There is no real test for global new values
v_new | _new |
Definition at line 716 of file value.c.
References concatenate(), entity_domain, entity_module_name(), entity_name, entity_undefined, gen_find_tabulated(), OLD_VALUE_SUFFIX, pips_assert, and SEMANTICS_MODULE_NAME.
Referenced by c_user_function_call_to_transformer(), fortran_user_function_call_to_transformer(), substitute_scalar_stub_in_transformer(), transformer_projection_with_redundancy_elimination_and_check(), and translate_global_value().
Return true if an entity is a global old value (such as "i#init"...).
this is not a general test; it will only work for GLOBAL values
Definition at line 690 of file value.c.
References entity_local_name(), entity_module_name(), OLD_VALUE_SUFFIX, SEMANTICS_MODULE_NAME, and SEMANTICS_SEPARATOR.
Referenced by external_value_name(), and translate_global_value().
const char* global_value_name_to_user_name | ( | const char * | gn | ) |
HASH TABLE USE.
Return a variable value name or map a variable to its different variable values. the '#' character used in value naming conflicts with the reserved character for struct naming
gn | n |
Definition at line 741 of file value.c.
References BLOCK_SEP_CHAR, and local_name().
Referenced by external_value_name().
bool hash_entity_to_values_undefined_p | ( | void | ) |
value.c
Definition at line 229 of file value.c.
References hash_entity_to_new_value, and hash_table_undefined_p.
bool hash_value_to_name_undefined_p | ( | void | ) |
Definition at line 1199 of file value.c.
References hash_table_undefined_p, and hash_value_to_name.
Referenced by generic_value_name().
bool integer_analyzed_p | ( | void | ) |
Definition at line 300 of file value.c.
References analyze_integer_scalar_entities.
Referenced by any_expression_to_transformer().
Definition at line 955 of file value.c.
References external_value_name(), and INTERMEDIATE_VALUE_SUFFIX.
Referenced by transformer_internal_consistency_p(), and value_to_variable().
A vector (in fact, a constraint) represents an invariant if it is a sum of delta for each variable.
Let di = i::new - i::old. If v = sigma (di) = 0, v can be used to build a loop invariant.
It is assumed that constant terms have been substituted earlier using a loop counter.
OK, you could argue for invariant = false, but this would not help my debugging!
if v_sum is non zero, you might try to bound it wrt the loop precondition?
Definition at line 934 of file fix_point.c.
References bool_to_string(), entity_name, external_value_name(), ifdebug, new_value_entity_p(), old_value_entity_p(), pips_debug, pips_internal_error, TCST, value_to_variable(), vect_add(), vect_add_elem(), vect_fprint(), vect_rm(), VECTEUR_NUL, VECTEUR_NUL_P, vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by constraints_keep_invariants_only().
transformer invariant_wrt_transformer | ( | transformer | p, |
transformer | tf | ||
) |
transformer invariant_wrt_transformer(transformer p, transformer tf): Assume that tf is a fix-point operator.
Old version: keep the invariant part of predicat p wrt tf in a VERY crude way; old and new values related to an entity modified by tf are discarded by projection, regardless of the way they are modified; information that they are modified is preserved; in fact, this is not a projection but a cylinder based on the projection. inf A real fix-point a la Halbwachs should be used p' = UNION(tf^k(p)) k=0 or simply one of PIPS loop fix-points.
Be careful if tf is not feasible because the result is p itself which may not be what you expect.
p is not modified.
if it is expensive, maybe it should not be computed over and over...
tf? fptf?
must be freed, otherwise it is leaked.
tf | f |
Definition at line 1948 of file transformer.c.
References args_to_transformer(), transformer_apply(), transformer_arguments, transformer_derivative_fix_point(), transformer_free(), transformer_undefined, and transformer_undefined_p.
Referenced by loop_to_transformer(), new_loop_to_transformer(), old_complete_whileloop_transformer(), process_ready_node(), standard_whileloop_to_transformer(), unstructured_to_postcondition(), and unstructured_to_total_precondition().
this is not a general test; it will only work for LOCAL values
Definition at line 648 of file value.c.
References entity_local_name(), and INTERMEDIATE_VALUE_PREFIX.
Return true if an entity is a local old value (such as "o#0" for a global value "i#init"...).
This is not a general test; it will only work for LOCAL values
Definition at line 642 of file value.c.
References entity_local_name(), and OLD_VALUE_PREFIX.
Referenced by add_type_information(), and regions_transformer_apply().
this is not a general test; it will only work for LOCAL values
Definition at line 654 of file value.c.
References entity_local_name(), and TEMPORARY_VALUE_PREFIX.
Referenced by generic_transformer_to_analyzed_locations(), generic_value_name(), non_local_temporary_value_entity_p(), old_value_entity_p(), readable_value_name(), transformer_add_sign_information(), transformer_projection_with_redundancy_elimination_and_check(), transformer_temporary_value_projection(), transformer_to_potential_stub_translation(), transformer_with_temporary_values_p(), and value_mappings_compatible_vector_p().
Pvecteur look_for_the_best_counter | ( | Pcontrainte | egs | ) |
Try to identify a loop counter among the equation egs.
If the transformer has been build naively, a loop counter should have a transformer equation like i::new = i::old + K_i where K_i is a numerical constant.
Since the loop counter is later used to eliminate constant terms in other constraints, variable i with the minimal absolute value K_i shuold be chosen.
egs | gs |
Definition at line 797 of file fix_point.c.
References ABS, contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, entity_local_name(), entity_undefined, entity_undefined_p, int, new_value_entity_p(), old_value_entity_p(), pips_internal_error, TCST, value_to_variable(), vect_size(), vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by transformer_pattern_fix_point().
entity make_local_temporary_integer_value_entity | ( | void | ) |
Definition at line 629 of file value.c.
References free_type(), is_basic_int, is_type_variable, local_temporary_value_counter, make_basic(), make_local_value_entity(), make_type(), make_variable(), and NIL.
Referenced by add_type_information(), bitwise_xor_to_transformer(), logical_not_to_transformer(), modulo_to_transformer(), transformer_add_condition_information_updown(), transformer_derivative_fix_point(), and transformer_list_generic_transitive_closure().
FI: is it easier to admit value of type void than to make a special case? Let see if it works... No, it's not a good idea because value are assumed of type variable in many places.
Definition at line 605 of file value.c.
References analyzed_type_p(), entity_undefined, local_temporary_value_counter, make_local_value_entity(), and pips_internal_error.
Referenced by add_formal_to_actual_bindings(), add_index_bound_conditions(), add_type_information(), addition_operation_to_transformer(), 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(), call_to_transformer(), expression_multiply_sizeof_to_transformer(), expression_to_transformer(), generic_abs_to_transformer(), generic_minmax_to_transformer(), iabs_to_transformer(), integer_binary_operation_to_transformer(), integer_expression_and_precondition_to_integer_interval(), integer_left_shift_to_transformer(), integer_minmax_to_transformer(), integer_multiply_to_transformer(), logical_binary_operation_to_transformer(), logical_unary_operation_to_transformer(), loop_bound_evaluation_to_transformer(), loop_to_enter_transformer(), unary_minus_operation_to_transformer(), update_cp_with_rhs_to_transformer(), update_operation_to_transformer(), and value_passing_summary_transformer().
Definition at line 620 of file value.c.
References copy_basic(), free_type(), is_type_variable, local_temporary_value_counter, make_local_value_entity(), make_type(), make_variable(), and NIL.
Referenced by condition_to_transformer(), precondition_minmax_of_expression(), and transformer_add_any_relation_information().
Tansformer lists are used to delay convex hulls and to refine the precondition computation of loops by putting aside the identity transformer.
If there is an identity transformer in the list, it is supposed to be the first one in the list.
However, some control paths are almost identity transformers because the store is apparently unchanged. However, they contain predicates on the possible values. Although they have no arguments, and hence, the store is left unchanged, they are different from the identity transformer bebcause the relation is smaller.
So it should be up to the function using the transformer list to decide how to cope with transformers that restrict the identity transition. Must not be used, beware of library cycles: include "semantics.h" Union of two lists
If the list includes the identity transformer, it must be the first in the list and be nowehere else
It is not clear if transformer lists will be stored in hash tables... Hence I do not know if the input list should be freed, reused or left unshared. To be conservative, no alias is created.
Do we have to worry about different bases in transformers?
Too much information is sometimes lost with this simplification
tl1 | l1 |
tl2 | l2 |
Definition at line 74 of file transformer_list.c.
References CAR, CDR, check_transformer_list(), CONS, ENDP, gen_full_copy_list(), gen_length(), gen_nconc(), ifdebug, NIL, pips_assert, TRANSFORMER, transformer_identity(), and transformer_identity_p().
Referenced by test_to_transformer_list().
list modified_variables_with_values | ( | void | ) |
Return the list of all analyzed variables which are modified in the current module.
If they are modified, they must have old values.
The intermediate values could be used as well
Definition at line 1094 of file value.c.
References hash_entity_to_old_value, and mapping_to_domain_list().
Referenced by apply_abstract_effect_to_transformer(), generic_reference_to_transformer(), and transformer_combine().
transformer move_transformer | ( | transformer | t1, |
transformer | t2 | ||
) |
Move arguments and predicate of t2 into t1, free old arguments and predicate of t1, free what's left of t2.
This is used to perform a side effect on an argument when a function allocates a new transformer to return a result. t2 should not be used after a call to move_transformer()
t1 | 1 |
t2 | 2 |
Definition at line 939 of file basic.c.
References free_arguments(), free_transformer(), NIL, pips_assert, predicate_system, sc_rm(), transformer_arguments, transformer_consistency_p(), and transformer_relation.
Referenced by transformer_domain_intersection().
the following three functions are directly or indirectly relative to the current module and its value hash tables.
since new values are always variable entities, hash_entity_to_new_value can be used for this test
Definition at line 925 of file value.c.
References entity_undefined, hash_entity_to_new_value, hash_get(), and pips_assert.
Referenced by build_transfer_matrix(), equations_to_bases(), invariant_vector_p(), look_for_the_best_counter(), new_value_in_transfer_equation(), transfer_equation_p(), transformer_internal_consistency_p(), and value_to_variable().
for gcc
eq | q |
Definition at line 570 of file fix_point.c.
References entity_undefined, eq, new_value_entity_p(), pips_assert, Svecteur::succ, TCST, value_mone_p, value_one_p, value_oppose, VALUE_ZERO, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by build_transfer_matrix().
FI: correct code entity var = entity_undefined;
var = value_to_variable(n_val); o_val = entity_to_old_value(var);
FI: faster code
n_val | _val |
Definition at line 1710 of file value.c.
References entity_to_old_value(), and entity_undefined.
Referenced by transformer_equality_fix_point(), and upwards_vect_rename().
int number_of_analyzed_values | ( | void | ) |
Definition at line 1148 of file value.c.
References hash_table_entry_count(), and hash_value_to_name.
Referenced by module_to_value_mappings().
int number_of_analyzed_variables | ( | void | ) |
FI: looks more like the number of values used.
Definition at line 1160 of file value.c.
References hash_table_entry_count(), and hash_value_to_name.
int number_of_temporary_values | ( | void | ) |
Definition at line 255 of file value.c.
References local_temporary_value_counter.
Referenced by transformer_temporary_value_projection(), and transformer_with_temporary_values_p().
void old_transformer_free | ( | transformer | t | ) |
I should use gen_free directly but Psysteme is not yet properly interfaced with NewGen
gen_free should stop before trying to free a Psysteme and won't free entities in arguments because they are tabulated
commented out for DRET demo
end of DRET demo
Definition at line 89 of file basic.c.
References pips_assert, predicate_system, predicate_system_, sc_rm(), transformer_relation, and transformer_undefined.
Temporary values do not have an external name.
OLD_VALUE_PREFIX is not used for global old values
string s = strstr(external_value_name(e), OLD_VALUE_SUFFIX);
string s = strstr(entity_local_name(e), OLD_VALUE_PREFIX);
Definition at line 936 of file value.c.
References entity_local_name(), local_temporary_value_entity_p(), OLD_VALUE_PREFIX, OLD_VALUE_SUFFIX, and s1.
Referenced by expression_less_than_in_context(), invariant_vector_p(), look_for_the_best_counter(), my_system_remove_variables(), precondition_filter_old_values(), print_call_precondition(), remove_temporal_variables_from_system(), transformer_derivative_constraints(), transformer_derivative_fix_point(), transformer_general_consistency_p(), transformer_internal_consistency_p(), transformer_list_generic_transitive_closure(), and value_to_variable().
o_val = variable_to_old_value(var);
o_val | _val |
Definition at line 1698 of file value.c.
References entity_to_new_value(), entity_undefined, and value_to_variable().
Referenced by build_transfer_matrix(), and equations_to_bases().
Combine each transformer of transformer list tl1 with the corresponding transformer in transformer list tl2.
Side-effect on tl1. See comments for transformer_combine().
See combine_transformer_lists() to combine each element of t1 with each element of t2.
tl1 | l1 |
tl2 | l2 |
Definition at line 476 of file transformer.c.
References CAR, FOREACH, gen_length(), pips_assert, POP, TRANSFORMER, and transformer_combine().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
const char* pips_user_value_name | ( | entity | e | ) |
This function is called many times when the constraints and the system of constraints are sorted using lexicographic information based on this particular value name.
See for instance Semantics-New/freia_52.c. Hence it is memorized.
Definition at line 815 of file value.c.
References ADDRESS_OF_SUFFIX, address_of_value_entity_p(), concatenate(), entity_domain, entity_has_values_p(), entity_minimal_name(), entity_name, entity_type, entity_user_name(), external_value_name(), free(), gen_check(), hash_entity_to_user_value_name, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, null_pointer_value_entity_p(), pips_debug, sizeof_value_entity_p(), strdup(), string_undefined, TCST, type_to_full_string_definition(), and value_to_variable().
Referenced by generic_value_name(), is_inferior_pvarval(), semantics_is_inferior_pvarval(), text_continuation(), and text_transformer().
bool pointer_analyzed_p | ( | void | ) |
Definition at line 325 of file value.c.
References analyze_pointer_scalar_entities.
Referenced by any_expression_to_transformer().
transformer precondition_to_abstract_store | ( | transformer | pre | ) |
Get rid of all old values and arguments.
Argument pre is unchanged and result as is allocated. Should be a call to transformer_range(). Should not be in basic.c.
Project all old values
Redefine the arguments
pre | re |
Definition at line 871 of file basic.c.
References gen_free_list(), NIL, transformer_arguments, transformer_dup(), and transformer_projection().
Referenced by test_to_transformer(), and test_to_transformer_list().
string precondition_to_string | ( | transformer | pre | ) |
pre | re |
Definition at line 58 of file prettyprint.c.
References pips_internal_error, and string_undefined.
Referenced by comp_regions_of_implied_do(), and evaluate_var_to_complexity().
transformer print_any_transformer | ( | transformer | tf | ) |
For debugging without problem from temporary values.
tf | f |
Definition at line 56 of file io.c.
References entity_local_name(), and fprint_transformer().
transformer print_transformer | ( | transformer | tf | ) |
io.c
io.c
Francois Irigoin, 21 April 1990 print_transformer(tf): not a macro because of dbx and gdb
tf | f |
Definition at line 48 of file io.c.
References external_value_name(), and fprint_transformer().
tl | l |
Definition at line 62 of file io.c.
References external_value_name(), and fprint_transformers().
Referenced by any_assign_to_transformer_list(), any_basic_update_to_transformer_list(), any_update_to_transformer_list(), block_to_transformer_list(), complete_any_loop_transformer_list(), declaration_to_transformer_list(), instruction_to_transformer_list(), integer_assign_to_transformer_list(), statement_to_transformer_list(), test_to_transformer_list(), and transformer_list_generic_transitive_closure().
void print_value_mappings | ( | void | ) |
Definition at line 993 of file value.c.
References dump_value_name(), entity_minimal_name(), external_value_name(), fprintf(), hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_reference_to_address_of_value, hash_table_fprintf(), hash_type_to_sizeof_value, hash_value_to_name, reference_to_string(), string_identity(), and type_to_full_string_definition().
Referenced by module_to_value_mappings().
const char* readable_value_name | ( | entity | v | ) |
For debugging purposes, we might have to print system with temporary values.
Definition at line 1769 of file value.c.
References entity_local_name(), external_value_name(), and local_temporary_value_entity_p().
Referenced by generic_module_name_to_transformers(), module_name_to_preconditions(), and module_name_to_total_preconditions().
The address is the address of a variable or of a reference such as &a[5], not a of a value.
The reference must be a constant memory access path. It does not have to be atomic, as struct are not considered atomic, following Pierre Jouvelot's view point since partial updates are possible.
An address is a constant within a C user function.
As a constant, it must be encoded as a 0-ary function, just like 1.0 or true.
We use the user representation as entity name, namey &a[5].
We do not use array names as constant pointers because they alreay are entities with types and storage. So the address of array a is &a[0].
References can be points-to references, i.e. fields can be encoded as indices.
trict_constant_path_p(r)
Should this local constant be added to the module declarations ?
Definition at line 1285 of file value.c.
References ADDRESS_OF_OPERATOR_NAME, concatenate(), copy_reference(), copy_type(), DEFAULT_ENTITY_KIND, entity_initial, entity_kind, entity_module_name(), entity_storage, entity_type, entity_undefined, FindOrCreateEntity(), make_constant_unknown(), make_functional(), make_storage_rom(), make_symbolic(), make_type_functional(), make_value_symbolic(), NIL, points_to_reference_to_concrete_type(), reference_to_expression(), reference_to_string(), reference_variable, store_independent_points_to_reference_p(), strdup(), and unary_intrinsic_expression.
Definition at line 889 of file value.c.
References entity_undefined, hash_get(), hash_reference_to_address_of_value, pips_internal_error, and reference_to_string().
transformer relation_to_transformer | ( | entity | op, |
entity | e1, | ||
entity | e2, | ||
bool | veracity | ||
) |
e and f are assumed to be values.
Operator op is overloaded and the result is operator and type dependent
Beware of type coercion... Fabien conjectures that values with incompatible types won't get mixed up...
type independent
Non convex information
op | p |
e1 | 1 |
e2 | 2 |
veracity | eracity |
Definition at line 139 of file transformer.c.
References b1, b2, basic_int_p, basic_logical_p, basic_pointer_p, basic_to_string(), contrainte_make(), CONTRAINTE_UNDEFINED, dump_transformer, 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_name, ENTITY_NON_EQUAL_P, entity_type, eq, ifdebug, make_predicate(), make_transformer(), module_local_name(), NIL, pips_debug, pips_internal_error, sc_make(), TCST, transformer_undefined, type_variable, VALUE_MONE, VALUE_ONE, variable_basic, vect_add_elem(), vect_new(), VECTEUR_NUL, and VECTEUR_NUL_P.
Referenced by transformer_add_any_relation_information().
pips_assert("remove_entity_values", e != entity_undefined);
readonly | eadonly |
Definition at line 1545 of file value.c.
References entity_to_intermediate_value(), entity_to_new_value(), entity_to_old_value(), entity_undefined, external_value_name(), hash_del(), hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_value_to_name, and pips_assert.
Referenced by add_or_kill_equivalenced_variables().
void reset_analyzed_types | ( | void | ) |
Definition at line 289 of file value.c.
References analyze_boolean_scalar_entities, analyze_complex_scalar_entities, analyze_constant_path, analyze_float_scalar_entities, analyze_integer_scalar_entities, analyze_pointer_scalar_entities, and analyze_string_scalar_entities.
Referenced by error_free_value_mappings(), and eval_linear_expression().
void reset_temporary_value_counter | ( | void | ) |
Definition at line 250 of file value.c.
References local_temporary_value_counter.
Referenced by add_index_bound_conditions(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), call_to_transformer(), error_free_value_mappings(), loop_bound_evaluation_to_transformer(), module_to_value_mappings(), precondition_add_condition_information(), test_to_transformer(), test_to_transformer_list(), and transformer_add_condition_information().
void reset_value_counters | ( | void | ) |
Definition at line 244 of file value.c.
References local_intermediate_value_counter, and local_old_value_counter.
Referenced by module_to_value_mappings().
transformer safe_transformer_projection | ( | transformer | t, |
list | args | ||
) |
t may be undefined, args may contain values unrelated to t
keep only values of args related to the transformer t
Make sure v is in the basis
Make sure the old value is projected too
args | rgs |
Definition at line 1187 of file transformer.c.
References arguments_add_entity(), base_contains_variable_p(), ENTITY, entity_is_argument_p(), entity_to_old_value(), FOREACH, gen_free_list(), NIL, predicate_system, transformer_arguments, transformer_projection(), transformer_relation, transformer_undefined, and transformer_undefined_p.
Referenced by add_index_bound_conditions(), add_type_information(), loop_to_transformer(), statement_to_postcondition(), statement_to_transformer(), statement_to_transformer_list(), substitute_stubs_in_transformer(), transformer_list_multiple_closure_to_precondition(), and transformer_list_safe_variables_projection().
bool same_dimension_p | ( | entity | actual_array, |
entity | dummy_array, | ||
list | l_actual_ref, | ||
size_t | i, | ||
transformer | context | ||
) |
This function returns true if the actual array and the dummy array have the same dimension number i, with respect to the current context (precondition + association) In case if the actual argument is an array element, we have to add the following condition: the i-th subscript of the array element is equal to its correspond lower bound.
The following test is necessary in case of array reshaping
actual_array | ctual_array |
dummy_array | ummy_array |
l_actual_ref | _actual_ref |
context | ontext |
Definition at line 2665 of file transformer.c.
References binary_intrinsic_expression, copy_expression(), dimension_lower, dimension_upper, entity_type, expression_equal_in_context_p(), expression_equal_integer_p(), find_ith_argument(), find_ith_dimension(), gen_length(), MINUS_OPERATOR_NAME, NIL, same_expression_p(), type_variable, and variable_dimensions.
Referenced by interprocedural_abc_arrays().
Eliminate all constant terms in sc using v.
No sharing between sc and v is assumed as sc is updated!
This function should be located in Linear/sc
sc | c |
Definition at line 853 of file fix_point.c.
References assert, constraints_eliminate_constant_terms(), TCST, and vect_coeff().
Referenced by transformer_pattern_fix_point().
This function cannot be moved into the Linear library.
It relies on the concepts of old and new values.
It could be improved by using an approximate initial fix-point to evaluate v_sum (see invariant_vector_p) and to degrade equations into inequalities or to relax inequalities.
For instance, p = p + a won't generate an invariant. However, if the lousy fix-point is sufficient to prove a >= 0, it is possible to derive p::new >= p::old. Or even better if a's value turns out to be known.
sc | c |
Definition at line 902 of file fix_point.c.
References constraints_keep_invariants_only().
Referenced by transformer_pattern_fix_point().
Specific for the derivative fix point: each constant term in the constraints is multiplied by ik which is not in sc's basis, and ik is added to the basis is necessary.
This possible only if ik is positive. Constraint ik>=0 is added if star_p is true because the function is used to compute T*. Else, contraint ik>=1 is added because the function is used to compute T+.
Also used in transformer_list.c
add constraint ik >= 0 to compute T*. Would be ik>=1 if T+ were sought.
sc | c |
ik | k |
star_p | tar_p |
Definition at line 1013 of file fix_point.c.
References Ssysteme::base, base_add_dimension, base_contains_variable_p(), contrainte_make(), CONTRAINTE_UNDEFINED_P, Ssysteme::dimension, Ssysteme::egalites, Ssysteme::inegalites, pips_assert, sc_add_inegalite(), Scontrainte::succ, Svecteur::succ, TCST, VALUE_MONE, VALUE_ONE, var_of, vect_add_elem(), vect_new(), Scontrainte::vecteur, and VECTEUR_NUL_P.
Referenced by transformer_derivative_fix_point(), and transformer_list_generic_transitive_closure().
void set_analyzed_types | ( | void | ) |
Definition at line 271 of file value.c.
References analyze_boolean_scalar_entities, analyze_complex_scalar_entities, analyze_constant_path, analyze_float_scalar_entities, analyze_integer_scalar_entities, analyze_pointer_scalar_entities, analyze_string_scalar_entities, and get_bool_property().
Referenced by eval_linear_expression(), and module_to_value_mappings().
transformer simple_addition_to_transformer | ( | entity | e, |
entity | e1, | ||
entity | e2, | ||
bool | addition_p | ||
) |
e and e1 and e2 are assumed to be values.
State e=e1+e2 or e=e1-e2. Type independent.
e1 | 1 |
e2 | 2 |
addition_p | ddition_p |
Definition at line 106 of file transformer.c.
References contrainte_make(), CONTRAINTE_UNDEFINED, dump_transformer, entity_local_name(), eq, ifdebug, make_predicate(), make_transformer(), NIL, pips_debug, sc_make(), transformer_undefined, VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by addition_operation_to_transformer().
transformer simple_equality_to_transformer | ( | entity | e, |
entity | f, | ||
bool | assignment | ||
) |
assignment | ssignment |
Definition at line 58 of file transformer.c.
References f(), and generic_equality_to_transformer().
Referenced by 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_user_function_call_to_transformer(), constant_to_transformer(), generic_reference_to_transformer(), logical_reference_to_transformer(), pointer_expression_to_transformer(), pointer_unary_operation_to_transformer(), and string_expression_to_transformer().
transformer simple_unary_minus_to_transformer | ( | entity | e, |
entity | f | ||
) |
Definition at line 65 of file transformer.c.
References f(), and generic_equality_to_transformer().
Referenced by unary_minus_operation_to_transformer().
If v is a not a float constraint, retun v.
If v is a float constraint, merge all float constants. If the constraint is trivially satisfied, return a NULL vector.
An integer constant cannot be mixed with floating point values
x!=0.
FI: do we want to represent 0. by 0?
Check that v is a feasible constraint
The new term must be the only one since vx is a new entity whose term cannot be cancelled by vect_add()
Unfeasible constraint
is_equation_p | s_equation_p |
Definition at line 2061 of file transformer.c.
References entity_constant_p, entity_type, float_constant_p(), float_constant_to_double(), float_to_entity(), float_type_p(), TCST, VALUE_MONE, VALUE_ONE, vect_add(), vect_add_elem(), vect_new(), vect_rm(), vect_size(), VECTEUR_NUL, vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, vecteur_var, and x.
Referenced by simplify_float_constraint_system().
Simplify float constraints and possibly detect.
Recompute the base, most of the time useless, but you cannot guess what happened in simplify_float_constraint()
Do not discard old values due to arguments... Just in case, keep too many floating point constants in the base. But add the new ones.
ps | s |
Definition at line 2146 of file transformer.c.
References base_dimension, base_union(), Ssysteme::egalites, eq, ifdebug, Ssysteme::inegalites, pips_assert, sc_consistent_p(), sc_to_minimal_basis(), simplify_float_constraint(), Scontrainte::succ, vect_rm(), and Scontrainte::vecteur.
Referenced by transformer_normalize().
Definition at line 969 of file value.c.
References entity_local_name(), and SIZEOF_SUFFIX.
Referenced by have_sizeof_value_in_multiply_pointer_expression_p(), pips_user_value_name(), and value_to_variable().
bool string_analyzed_p | ( | void | ) |
Definition at line 310 of file value.c.
References analyze_string_scalar_entities.
Referenced by any_expression_to_transformer(), fortran_data_to_prec_for_variables(), and parametric_transformer_empty_p().
FI: should be moved in base.c.
sub_basis_p(Pbase b1, Pbase b2): check if b1 is included in b2
b1 | 1 |
b2 | 2 |
Definition at line 648 of file fix_point.c.
References b1, b2, base_contains_variable_p(), Svecteur::succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by build_transfer_equations().
void test_mapping_entry_consistency | ( | void | ) |
This second assert is too strong when some analyzable variables are equivalenced together. The number of values required is smaller since two (or more) different variables share the same value: the number of entries in the tables is greater than the number of values. We must compute the number of values in each table.
Why greater instead of equal? Because the equivalence variable appears in the equivalence equations although it should never appear in regular constraints, except under its canonical name.
Definition at line 1113 of file value.c.
References hash_entity_to_intermediate_value, hash_entity_to_new_value, hash_entity_to_old_value, hash_table_entry_count(), hash_value_to_name, mapping_to_value_number(), and pips_assert.
Referenced by module_to_value_mappings().
A transfer equation is an explicit equation giving one new value as a function of old values and a constant term.
Because we are using diophantine equations, the coefficient of the new value must one or minus one. We assume that the equation is reduced (i.e. gcd(coeffs) == 1).
FI: Non-unary coefficients may appear because equations were combined, for instance by a previous internal fix-point as in KINETI of mdg-fi.f (Perfect Club). Maybe, something could be done for these nested fix-points.
eq | q |
Definition at line 552 of file fix_point.c.
References eq, new_value_entity_p(), Svecteur::succ, TCST, value_mone_p, value_one_p, VALUE_ZERO, VECTEUR_UNDEFINED_P, vecteur_val, and vecteur_var.
Referenced by build_transfer_equations().
transformer transformer_add_3d_affine_constraint | ( | transformer | tf, |
int | a1, | ||
entity | v1, | ||
int | a2, | ||
entity | v2, | ||
int | a3, | ||
entity | v3, | ||
int | cst, | ||
bool | equation_p | ||
) |
Add the constraint a1 v1 + a2 v2 + a3 v3 + cst <= or == 0.
tf | f |
a1 | 1 |
v1 | 1 |
a2 | 2 |
v2 | 2 |
a3 | 3 |
v3 | 3 |
cst | st |
equation_p | quation_p |
Definition at line 536 of file basic.c.
References eq, TCST, transformer_equality_add(), transformer_inequality_add(), vect_add_elem(), and vect_new().
Referenced by process_bounds_for_divide(), and update_cp_with_rhs_to_transformer().
transformer transformer_add_equality | ( | transformer | tf, |
entity | v1, | ||
entity | v2 | ||
) |
Add an equality between two values (two variables?)
tf | f |
v1 | 1 |
v2 | 2 |
Definition at line 436 of file basic.c.
References eq, transformer_equality_add(), VALUE_MONE, vect_add_elem(), and vect_new().
Referenced by any_basic_update_operation_to_transformer(), assign_operation_to_transformer(), generic_abs_to_transformer(), generic_reference_to_transformer(), generic_unary_operation_to_transformer(), lhs_expression_to_transformer(), transformer_apply_field_assignments_or_equalities(), and update_operation_to_transformer().
transformer transformer_add_equality_with_affine_term | ( | transformer | tf, |
entity | v, | ||
entity | x, | ||
int | a, | ||
int | cst | ||
) |
Add the equality v = a x + cst.
tf | f |
cst | st |
Definition at line 517 of file basic.c.
References eq, TCST, transformer_equality_add(), VALUE_ONE, vect_add_elem(), vect_new(), and x.
Referenced by generic_abs_to_transformer().
transformer transformer_add_equality_with_integer_constant | ( | transformer | tf, |
entity | v, | ||
long long int | cst | ||
) |
Add an equality between a value and an integer constant: v==cst.
tf | f |
cst | st |
Definition at line 450 of file basic.c.
References eq, TCST, transformer_equality_add(), VALUE_MONE, vect_add_elem(), and vect_new().
Referenced by add_type_information(), bitwise_xor_to_transformer(), constant_to_transformer(), generic_abs_to_transformer(), integer_expression_to_transformer(), integer_left_shift_to_transformer(), integer_power_to_transformer(), logical_binary_function_to_transformer(), logical_expression_to_transformer(), logical_not_to_transformer(), modulo_by_a_constant_to_transformer(), modulo_of_a_constant_to_transformer(), and transformer_add_condition_information_updown().
transformer transformer_add_identity | ( | transformer | tf, |
entity | v | ||
) |
tf | f |
Definition at line 421 of file basic.c.
References arguments_add_entity(), entity_to_new_value(), entity_to_old_value(), eq, transformer_arguments, transformer_equality_add(), vect_add_elem(), and vect_new().
transformer transformer_add_inequality | ( | transformer | tf, |
entity | v1, | ||
entity | v2, | ||
bool | strict_p | ||
) |
Add the equality v1 <= v2 or v1 < v2.
tf | f |
v1 | 1 |
v2 | 2 |
strict_p | trict_p |
Definition at line 464 of file basic.c.
References eq, TCST, transformer_inequality_add(), VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by add_index_bound_conditions(), integer_left_shift_to_transformer(), and integer_multiply_to_transformer().
transformer transformer_add_inequality_with_affine_term | ( | transformer | tf, |
entity | v, | ||
entity | x, | ||
int | a, | ||
int | cst, | ||
bool | less_than_p | ||
) |
Add the inequality v <= a x + cst or v >= a x + cst.
tf | f |
cst | st |
less_than_p | ess_than_p |
Definition at line 496 of file basic.c.
References eq, TCST, transformer_inequality_add(), VALUE_MONE, VALUE_ONE, vect_add_elem(), vect_new(), VECTEUR_NUL, and x.
Referenced by integer_left_shift_to_transformer(), integer_multiply_to_transformer(), and transformer_add_inequality_with_linear_term().
transformer transformer_add_inequality_with_integer_constraint | ( | transformer | tf, |
entity | v, | ||
long long int | cst, | ||
bool | less_than_p | ||
) |
Add the inequality v <= cst or v >= cst.
tf | f |
cst | st |
less_than_p | ess_than_p |
Definition at line 477 of file basic.c.
References eq, TCST, transformer_inequality_add(), VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by add_type_information(), integer_call_expression_to_transformer(), integer_left_shift_to_transformer(), integer_minmax_to_transformer(), integer_power_to_transformer(), logical_binary_function_to_transformer(), logical_not_to_transformer(), modulo_by_a_constant_to_transformer(), modulo_of_a_constant_to_transformer(), modulo_of_a_negative_value_to_transformer(), modulo_of_a_positive_value_to_transformer(), and modulo_to_transformer().
transformer transformer_add_inequality_with_linear_term | ( | transformer | tf, |
entity | v, | ||
entity | x, | ||
int | a, | ||
bool | less_than_p | ||
) |
Add the inequality v <= a x or v >= a x.
tf | f |
less_than_p | ess_than_p |
Definition at line 530 of file basic.c.
References transformer_add_inequality_with_affine_term(), VALUE_ZERO, and x.
Referenced by expression_multiply_sizeof_to_transformer(), integer_multiply_to_transformer(), and loop_to_enter_transformer().
transformer transformer_add_modified_variable | ( | transformer | tf, |
entity | var | ||
) |
FI: this function does not end up with a consistent transformer because the old value is not added to the basis of sc.
Also, the variable should be transformed into a new value... See next function.
Should we check that var has values?
tf | f |
var | ar |
Definition at line 889 of file basic.c.
References arguments_add_entity(), base_dimension, predicate_system, transformer_arguments, transformer_relation, and vect_add_variable().
Referenced by any_assign_operation_to_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), transformer_apply_field_assignments_or_equalities(), and transformer_apply_unknown_field_assignments_or_equalities().
transformer transformer_add_modified_variable_entity | ( | transformer | tf, |
entity | var | ||
) |
FI: like the previous function, but supposed to end up with a consistent transformer.
When the transformer is empty/unfeasible, the variable is not added to conform to rules about standard empty transformer: how could a variable be updated by a non-existing transition?
FI: it is not well specifived if the argument should be made of new values or of progtram variables because up to now the two are the same, except when printed out.
tf | f |
var | ar |
Definition at line 909 of file basic.c.
References arguments_add_entity(), base_dimension, entity_has_values_p(), entity_name, entity_to_new_value(), entity_to_old_value(), pips_internal_error, predicate_system, transformer_arguments, transformer_empty_p(), transformer_relation, and vect_add_variable().
Referenced by safe_assigned_expression_to_transformer(), and safe_assigned_expression_to_transformer_list().
transformer transformer_add_sign_information | ( | transformer | tf, |
entity | v, | ||
int | v_sign | ||
) |
CHANGE THIS NAME: no loop index please, it's not directly linked to loops!!!
Add in tf the information that v is striclty positive, strictly negative or zero.
Assume that v is a value and tf is defined.
v_sign<0
v_sign==0
tf | f |
v_sign | _sign |
Definition at line 200 of file basic.c.
References Ssysteme::base, base_add_variable(), base_dimension, contrainte_make(), Ssysteme::dimension, eq, ifdebug, local_temporary_value_entity_p(), pips_assert, predicate_system, sc_add_egalite(), sc_add_inegalite(), TCST, transformer_consistency_p(), transformer_relation, value_entity_p(), VALUE_MONE, VALUE_ONE, vect_add_elem(), and vect_new().
Referenced by condition_to_transformer().
transformer transformer_add_value_update | ( | transformer | t, |
entity | v | ||
) |
Add an update of variable v to t (a value cannot be updated)
Definition at line 321 of file basic.c.
References arguments_add_entity(), Ssysteme::base, base_add_variable(), base_contains_variable_p(), Ssysteme::dimension, entity_to_new_value(), entity_to_old_value(), predicate_system, transformer_arguments, transformer_empty_p(), transformer_relation, and vect_size().
Referenced by assigned_expression_to_transformer(), assigned_expression_to_transformer_list(), c_return_to_transformer(), and transformer_add_variables_update().
transformer transformer_add_variable_incrementation | ( | transformer | t, |
entity | i, | ||
Pvecteur | incr | ||
) |
transformer transformer_add_loop_index(transformer t, entity i, Pvecteur incr): add the index incrementation expression incr for loop index i to transformer t.
t = intersection(t, i::new = i::old + incr)
incr is supposed to be compatible with the value mappings
Pvecteur incr should not be used after a call to transformer_add_index because it is shared by t and modified
Psysteme * ps = &((Psysteme) predicate_system(transformer_relation(t)));
incr | ncr |
Definition at line 260 of file basic.c.
References arguments_add_entity(), Ssysteme::base, contrainte_make(), Ssysteme::dimension, entity_to_new_value(), entity_to_old_value(), predicate_system, sc_equation_add(), transformer_arguments, transformer_relation, value_to_variable(), vect_add_variable(), vect_chg_coeff(), and vect_size().
Referenced by transformer_add_loop_index_incrementation().
transformer transformer_add_variable_update | ( | transformer | t, |
entity | v | ||
) |
Add an update of variable v into t.
NL : this function is not finish do the same thing than transformer_add_value_update for the moment TODO
Definition at line 289 of file basic.c.
References arguments_add_entity(), Ssysteme::base, base_add_variable(), base_contains_variable_p(), Ssysteme::dimension, entity_to_new_value(), entity_to_old_value(), predicate_system, transformer_arguments, transformer_relation, value_to_variable(), and vect_size().
Referenced by apply_abstract_effect_to_transformer(), apply_array_effect_to_transformer(), apply_concrete_effect_to_transformer(), generic_apply_effect_to_transformer(), and generic_reference_to_transformer().
transformer transformer_add_variables_update | ( | transformer | t, |
list | vl | ||
) |
vl | l |
Definition at line 340 of file basic.c.
References ENTITY, FOREACH, and transformer_add_value_update().
Referenced by c_user_call_to_transformer().
bool transformer_affect_linear_p | ( | transformer | tf, |
Pvecteur | l | ||
) |
bool transformer_affect_linear_p(transformer tf, Pvecteur l): returns TRUE if there is a state s such that eval(l, s) != eval(l, tf(s)); returns false if l is invariant w.r.t.
tf, i.e. for all state s, eval(l, s) == eval(l, tf(s))
tf | f |
Definition at line 1850 of file transformer.c.
References ENTITY, MAP, transformer_arguments, transformer_undefined_p, value_notzero_p, and vect_coeff().
Referenced by add_affine_bound_conditions(), add_loop_index_exit_value(), and transformer_affect_transformer_p().
bool transformer_affect_transformer_p | ( | transformer | tf1, |
transformer | tf2 | ||
) |
Transformer tf1 affects transformer tf2 if values modified by tf1 appear in any constraint of tf2.
The two transformer do not commute and tf1 o tf2 does not equal tf2 o tf1.
No need to check anything if tf1 does not change the memory state
tf1 | f1 |
tf2 | f2 |
Definition at line 1870 of file transformer.c.
References contrainte_succ, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, ENDP, predicate_system, transformer_affect_linear_p(), transformer_arguments, and transformer_relation.
Referenced by transformer_safe_affect_transformer_p().
transformer transformer_apply | ( | transformer | tf, |
transformer | pre | ||
) |
transformer transformer_apply(transformer tf, transformer pre): apply transformer tf on precondition pre to obtain postcondition post
post = tf(pre) = pre o tf
There is (should be!) no sharing between pre and tf. No sharing is introduced between pre or tf and post. Neither pre nor tf are modified.
post = tf o pre ; pre would be modified by transformer_combine
tf | f |
pre | re |
Definition at line 1559 of file transformer.c.
References dump_transformer, ifdebug, pips_assert, pips_debug, transformer_combine(), transformer_dup(), and transformer_undefined.
Referenced by add_good_loop_conditions(), add_loop_index_exit_value(), add_loop_index_initialization(), addition_operation_to_transformer(), any_assign_to_transformer(), any_conditional_to_transformer(), any_expressions_to_transformer(), any_loop_to_k_transformer(), any_loop_to_postcondition(), any_transformer_to_k_closure(), any_user_call_site_to_transformer(), apply_transformer_lists_generic(), assign_rhs_to_reflhs_to_transformer(), bitwise_xor_to_transformer(), call_to_postcondition(), complete_forloop_transformer(), complete_forloop_transformer_list(), complete_loop_transformer(), complete_loop_transformer_list(), complete_repeatloop_transformer_list(), condition_to_transformer(), conditional_to_transformer(), cycle_to_flow_sensitive_preconditions(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), dag_to_flow_sensitive_preconditions(), declaration_to_transformer(), declaration_to_transformer_list(), dimensions_to_transformer(), expression_multiply_sizeof_to_transformer(), expression_to_postcondition(), expressions_to_transformer(), forloop_to_postcondition(), forloop_to_transformer(), integer_binary_operation_to_transformer(), integer_left_shift_to_transformer(), integer_multiply_to_transformer(), invariant_wrt_transformer(), loop_to_postcondition(), modulo_to_transformer(), new_add_formal_to_actual_bindings(), new_complete_whileloop_transformer_list(), new_loop_to_transformer(), precondition_minmax_of_expression(), process_ready_node(), repeatloop_to_postcondition(), statement_to_postcondition(), statement_to_transformer(), test_to_postcondition(), test_to_total_precondition(), test_to_transformer(), test_to_transformer_list(), transformer_add_any_relation_information(), transformer_add_condition_information_updown(), transformer_apply_generic(), transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), transformer_safe_apply(), unstructured_to_postcondition(), unstructured_to_total_precondition(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
list transformer_apply_generic | ( | list | tl, |
transformer | pre, | ||
bool | keep_p | ||
) |
Generates a new list of postconditions, one for each transformer in tl, unless the postcondition is empty and keep_p is FALSE.
keep_p is used to preserve the list lengths: the output list is exactly as long as the input list.
If keep_p is true, the output list is not "normalized"
tl | l |
pre | re |
keep_p | eep_p |
Definition at line 1593 of file transformer.c.
References CONS, FOREACH, gen_nreverse(), NIL, TRANSFORMER, transformer_apply(), and transformer_empty_p().
Referenced by transformer_apply_map(), transformers_apply(), and transformers_apply_and_keep_all().
list transformer_apply_map | ( | list | tl, |
transformer | pre | ||
) |
Generates a new list of postconditions, one for each transformer in tl, unless the postcondition is empty.
tl | l |
pre | re |
Definition at line 1610 of file transformer.c.
References transformer_apply_generic().
Referenced by test_to_transformer_list().
bool transformer_argument_consistency_p | ( | transformer | t | ) |
Definition at line 551 of file basic.c.
References transformer_argument_general_consistency_p().
Referenced by transformer_add_any_relation_information(), and transformer_general_consistency_p().
bool transformer_argument_general_consistency_p | ( | transformer | t, |
bool | is_weak | ||
) |
If no final state can be reached, no variable can be changed in between
If a variable appears as argument, its new value must be in the basis See for instance, effects_to_transformer()
pips_user_warning("No value for argument %s in relation basis\n", entity_name(e));
is_weak | s_weak |
Definition at line 561 of file basic.c.
References base_contains_variable_p(), ENDP, ENTITY, entity_name, entity_to_new_value(), MAP, pips_assert, pips_internal_error, predicate_system, sc_empty_p(), transformer_arguments, and transformer_relation.
Referenced by transformer_argument_consistency_p(), and transformer_argument_weak_consistency_p().
bool transformer_argument_weak_consistency_p | ( | transformer | t | ) |
Definition at line 556 of file basic.c.
References transformer_argument_general_consistency_p().
transformer transformer_arguments_projection | ( | transformer | t | ) |
transformer transformer_projection(transformer t); projection of t along the hyperplane defined by values of variables in arguments; this generate a projection and not a cylinder based on the projection
use the most complex/complete redundancy elimination in Linear
args is not modified. t is modified by side effects.
Definition at line 1285 of file transformer.c.
References base_contains_variable_p(), CONS, ENTITY, entity_to_new_value(), entity_to_old_value(), gen_free_list(), MAP, NIL, predicate_system, transformer_arguments, transformer_projection(), and transformer_relation.
transformer transformer_basic_fix_point | ( | transformer | tf | ) |
Computation of a fix point: drop all constraints, remember which variables are changed.
Except if the transformer is syntactically empty since its fix point is easy to compute. Without normalization, mathematically empty transformers are lost.
get rid of equalities and inequalities but keep the basis
tf | f |
Definition at line 1280 of file fix_point.c.
References CONTRAINTE_UNDEFINED, contraintes_free(), copy_transformer(), eq, predicate_system, transformer_empty_p(), and transformer_relation.
Referenced by select_fix_point_operator().
transformer transformer_combine | ( | volatile transformer | t1, |
transformer | t2 | ||
) |
transformer transformer_combine(transformer t1, transformer t2): compute the composition of transformers t1 and t2 (t1 then t2)
t1 := t2 o t1 return t1
t1 is updated, but t2 is preserved
general algorithm: let a1 be t1 arguments, a2 be t2 arguments, let ints be the intersection of a1 and a2 let r1 be t1 relation and r2 be a copy of t2 relation let a be a1 union a2 rename entities in ints in r1 (new->int) and r2 (old->int) rename entities in a2-ints in r1 (new->old) build a system b with r1 and r2 project b along ints build t1 with a and b
Handling of four special cases because abstract effects are likely to generate rn transformers, which lead to lots of variable projections if handled as a usual transformer. Not sufficient to solve Ticket 644. But sufficient to introduce lots of bugs...
not much to do since t1 is going to destroy all information in t2, except its range
not much to do since t2 is going to destroy all information in t1, except its domain
Standard case
Newgen does not generate the proper castings
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
ints: list of intermediate value entities
The consistencies of transformers t1 and t2 cannot be checked with respect to the current environment because t1 or t2 may be relative to a callee as in user_function_call_to_transformer(). Hence a debug level of 10.
both t1 and t2 are not obviously unfeasible
build new argument list and rename old and intermediate values, as well as new (i.e. unmodified) variables in t1
renaming of intermediate values in r1 and r2
if ever e2 is used as e2::new in r1 it must now be replaced by e2::old
e2 must be appended to a1 as new t1's arguments; hopefully we are not iterating on a1; but entity_is_argument_p() receives a longer argument each time; possible improvements?
build global linear system: r1 is destroyed, r2 is preserved
??? The base returned may be empty... FC... boumbadaboum in the projection later on.
get rid of intermediate values, if any. ??? guard added to avoid an obscure bug, but I guess it should never get here with en nil base... FC
CA
IER: problem with e_temp that should be volatile because of the catch structure. Not easy make it volatile because of the MAP MACRO
get rid of ints
update t1
No old values should be left in r1's basis.
t1 | 1 |
t2 | 2 |
Definition at line 238 of file transformer.c.
References arguments_add_entity(), arguments_set_equal_p(), Ssysteme::base, base_contains_variable_p(), BASE_NULLE, CAR, CATCH, CONS, copy_transformer(), dump_transformer, dump_value_name(), empty_transformer(), ENDP, ENTITY, entity_is_argument_p(), entity_local_name(), entity_name, entity_to_intermediate_value(), entity_to_old_value(), free_arguments(), free_transformer(), gen_free_list(), gen_nconc(), ifdebug, MAP, modified_variables_with_values(), NIL, NO_OFL_CTRL, overflow_error, pips_assert, pips_debug, pips_user_warning, POP, predicate_system, sc_append(), sc_base_remove_variable(), sc_dump(), sc_dup(), sc_elim_var(), sc_empty(), sc_empty_p(), sc_fprint(), sc_normalize2(), sc_rm(), sc_variable_rename(), transformer_arguments, transformer_consistency_p(), transformer_domain_intersection(), transformer_is_empty_p(), transformer_is_rn_p(), transformer_range(), transformer_range_intersection(), transformer_relation, transformer_to_domain(), TRY, UNCATCH, and VOLATILE_FOREACH.
Referenced by any_assign_operation_to_transformer(), any_assign_to_transformer(), any_conditional_to_transformer(), any_expression_side_effects_to_transformer(), any_expressions_side_effects_to_transformer(), any_expressions_to_transformer(), any_loop_to_k_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), any_transformer_to_k_closure(), any_user_call_site_to_transformer(), assign_rhs_to_reflhs_to_transformer(), assigned_expression_to_transformer(), assigned_expression_to_transformer_list(), block_to_transformer(), block_to_transformer_list(), c_data_to_prec_for_variables(), c_user_call_to_transformer(), c_user_function_call_to_transformer(), combine_transformer_lists(), complete_any_loop_transformer_list(), complete_loop_transformer(), complete_loop_transformer_list(), complete_repeatloop_transformer_list(), condition_to_transformer(), conditional_to_transformer(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), declaration_to_transformer(), declaration_to_transformer_list(), declarations_to_transformer(), declarations_to_transformer_list(), dimensions_to_transformer(), expression_to_transformer(), expressions_to_transformer(), forloop_to_postcondition(), forloop_to_transformer(), fortran_data_to_prec_for_variables(), fortran_user_function_call_to_transformer(), generic_unary_operation_to_transformer(), integer_binary_operation_to_transformer(), integer_expression_to_transformer(), integer_multiply_to_transformer(), loop_to_continue_transformer(), loop_to_postcondition(), loop_to_total_precondition(), loop_to_transformer(), module_name_to_total_preconditions(), modulo_to_transformer(), old_complete_whileloop_transformer(), one_to_one_transformers_combine(), pointer_unary_operation_to_transformer(), propagate_preconditions_in_declarations(), repeatloop_to_transformer(), safe_assigned_expression_to_transformer(), struct_reference_assignment_or_equality_to_transformer(), transformer_add_any_relation_information(), transformer_add_call_condition_information_updown(), transformer_apply(), transformer_apply_field_assignments_or_equalities(), transformer_apply_unknown_field_assignments_or_equalities(), transformer_halbwachs_fix_point(), transformer_inverse_apply(), transformer_list_add_combination(), transformer_safe_combine_with_warnings(), transformers_combine(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
bool transformer_consistency_p | ( | transformer | t | ) |
FI: I do not know if this procedure should always return or fail when an inconsistency is found.
For instance, summary transformers for callees are inconsistent with respect to the current module. FC/CA: help...
I do not understand why errors are reported only if the debug level is greater than 1. A demo effect? No, this routine is coded that way to save time on regular runs.
Also, since no precise information about the inconsistency is displayed, a core dump would be welcome to retrieve pieces of information with gdb. The returned value should always be tested and a call to pips_internal_error() should always be performed if an inconsistency is detected.
But, see final comment... In spite of it, I do not always return any longer.
Definition at line 612 of file basic.c.
References transformer_general_consistency_p().
Referenced by block_to_transformer(), block_to_transformer_list(), call_to_transformer(), declarations_to_transformer(), declarations_to_transformer_list(), generic_module_name_to_transformers(), initial_precondition(), loop_to_total_precondition(), module_name_to_total_preconditions(), move_transformer(), node_to_path_transformer_or_postcondition(), print_cycle_head_to_fixpoint(), program_postcondition(), program_precondition(), propagate_preconditions_in_declarations(), safe_assigned_expression_to_transformer(), statement_to_postcondition(), statement_to_total_precondition(), statement_to_transformer(), statement_to_transformer_list(), store_control_fix_point(), store_control_postcondition(), transformer_add_loop_index_incrementation(), transformer_add_sign_information(), transformer_combine(), transformer_derivative_fix_point(), transformer_internal_consistency_p(), transformer_inverse_apply(), transformer_list_closure_to_precondition(), transformer_list_closure_to_precondition_depth_two(), transformer_list_generic_transitive_closure(), transformer_list_multiple_closure_to_precondition(), transformer_normalize(), unstructured_to_flow_sensitive_postconditions(), and unstructured_to_flow_sensitive_total_preconditions().
transformer transformer_constraint_add | ( | transformer | tf, |
Pvecteur | i, | ||
bool | equality | ||
) |
tf | f |
equality | quality |
Definition at line 348 of file basic.c.
References contrainte_make(), pips_assert, predicate_system, sc_constraint_add(), transformer_relation, transformer_undefined, user_warning, and VECTEUR_NUL_P.
Referenced by transformer_equalities_add(), transformer_equality_add(), transformer_inequalities_add(), and transformer_inequality_add().
transformer transformer_convex_hull | ( | transformer | t1, |
transformer | t2 | ||
) |
convex_hull.c
convex_hull.c
return transformer_convex_hulls(t1, t2, sc_enveloppe);
return transformer_convex_hulls(t1, t2, sc_enveloppe_chernikova);
return transformer_convex_hulls(t1, t2, sc_common_projection_convex_hull);
t1 = transformer_normalize(t1, 4);
t2 = transformer_normalize(t2, 4);
t1 | 1 |
t2 | 2 |
Definition at line 216 of file convex_hull.c.
References cute_convex_union(), transformer_convex_hulls(), and transformer_normalize().
Referenced by add_module_call_site_precondition(), any_assign_to_transformer(), any_basic_update_to_transformer(), any_conditional_to_transformer(), any_loop_to_k_transformer(), any_loop_to_postcondition(), any_transformer_to_k_closure(), any_update_to_transformer(), complete_loop_transformer(), complete_loop_transformer_list(), condition_to_transformer(), conditional_to_transformer(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), dag_to_flow_sensitive_preconditions(), generic_transformer_list_to_transformer(), generic_unary_operation_to_transformer(), get_control_precondition(), lhs_expression_to_transformer(), loop_body_transformer_add_entry_and_iteration_information(), loop_to_postcondition(), loop_to_total_precondition(), main(), new_array_elements_backward_substitution_in_transformer(), new_array_elements_forward_substitution_in_transformer(), old_complete_whileloop_transformer(), points_to_unary_operation_to_transformer(), process_call_for_summary_precondition(), process_ready_node(), repeatloop_to_postcondition(), repeatloop_to_transformer(), statement_to_transformer(), statement_to_transformer_list(), struct_reference_assignment_or_equality_to_transformer(), test_to_postcondition(), test_to_total_precondition(), test_to_transformer(), transformer_add_anded_conditions_updown(), transformer_add_any_relation_information(), transformer_add_integer_relation_information(), transformer_add_ored_conditions_updown(), transformer_halbwachs_fix_point(), transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), unstructured_to_flow_insensitive_transformer(), update_summary_precondition(), update_temporary_precondition(), and whileloop_to_postcondition().
Psysteme transformer_derivative_constraints | ( | transformer | t | ) |
Allocate a new constraint system sc(dx) with dx=x'-x and t(x,x')
FI: this function should/might be located in fix_point.c
sc is going to be modified and returned
Do not handle variable which do not appear explicitly in constraints!
basis vector
Compute constraints with difference equations
Only generate difference equations if the old value is used
Project all variables but differences to get T'
Definition at line 891 of file transformer_list.c.
References BASE_NULLE, BASE_NULLE_P, contrainte_make(), CONTRAINTE_UNDEFINED, entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), ifdebug, old_value_entity_p(), pips_debug, predicate_system, sc_copy(), sc_equation_add(), sc_fprint(), sc_to_minimal_basis(), Svecteur::succ, TCST, transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), VECTEUR_NUL, and vecteur_var.
Referenced by transformer_list_generic_transitive_closure().
transformer transformer_derivative_fix_point | ( | transformer | tf | ) |
Computation of a transitive closure using constraints on the discrete derivative.
See http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Implicit equations, n::new - n::old = 0, are not added. Instead, invariant constraints in tf are obtained by projection and added.
Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old
I tried to use the standard procedure but arguments are not removed when the transformer tf is not feasible. Since we compute the * fix point and not the + fix point, the fix point is the identity.
sc is going to be modified and destroyed and eventually replaced in fix_tf
Do not handle variable which do not appear explicitly in constraints!
initial and final basis
basis vector
basis of difference vectors
Compute constraints with difference equations
Only generate difference equations if the old value is used
Project all variables but differences to get T'
Multiply the constant terms by the iteration number ik and add a positivity constraint for the iteration number ik and then eliminate the iteration number ik to get T*(dx).
Difference variables must substituted back to differences between old and new values.
Only generate difference equations if the old value is used
Project all difference variables
The full basis must be used again
Plug sc back into fix_tf
Add constraints about invariant variables. This could be avoided if implicit equalities were added before the derivative are processed: each invariant variable would generate an implicit null difference.
Such invariant constraints do not exist in general. We have them when array references are trusted.
This is wrong because we compute f* and not f+ and this is not true for the initial store.
What can be done instead is to refine fix_tf as :
dom(tf) U tf(fix_tf(dom(tf)))
But this fails because tf loops back to the beginning of the next iteration. Hence, the domain of tf implies two iterations instead of one. For instance, "i<n" becomes "i<=n-2" for a while loop such as "while(i<n) i++;".
So this refinement should be performed at a higher level where t_init and t_enter are know... so as to have:
dom_tf = transformer_range(t_enter(t_init)).
That's all!
tf | f |
Definition at line 1067 of file fix_point.c.
Referenced by transformers_derivative_fix_point().
transformer transformer_domain_intersection | ( | transformer | tf, |
transformer | pre | ||
) |
Restrict the domain of the relation tf with pre.
pre is assumed to be restricted to a store predicate: its argument list must be empty.
For a restriction on the image of tf, see transformer_image_intersection
tf is updated by side effect although transformer_image_intersection() allocates a fresh new transformer.
if a value in pre is modified by tf, it must be renamed as an old value
transformer dom is not consistent since it references old values but has no arguments
tf | f |
pre | re |
Definition at line 661 of file transformer.c.
References ENDP, ENTITY, entity_to_new_value(), entity_to_old_value(), free_transformer(), MAP, move_transformer(), pips_assert, pips_debug, predicate_system, sc_variable_rename(), transformer_arguments, transformer_dup(), transformer_image_intersection(), transformer_relation, and transformer_undefined.
Referenced by loop_body_transformer_add_entry_and_iteration_information(), loop_to_transformer(), statement_to_transformer(), statement_to_transformer_list(), transformer_combine(), and transformer_safe_domain_intersection().
transformer transformer_dup | ( | transformer | t_in | ) |
cproto-generated files
cproto-generated files
Francois Irigoin
FI: I do not reduce transformer_dup() to a macro calling copy_transformer() because I do not want to create problems with the link edit and because I want to keep the assertion
t_in | _in |
Definition at line 49 of file basic.c.
References copy_transformer(), pips_assert, predicate_system, transformer_relation, and transformer_undefined.
Referenced by add_index_bound_conditions(), add_loop_index_exit_value(), any_transformer_to_k_closure(), block_to_postcondition(), block_to_total_precondition(), block_to_transformer(), call_site_to_module_precondition_text(), call_to_summary_precondition(), check_condition_wrt_precondition(), comp_regions_of_implied_do(), complete_loop_transformer(), complete_loop_transformer_list(), cycle_to_flow_sensitive_preconditions(), dag_to_flow_sensitive_preconditions(), declarations_to_transformer(), declarations_to_transformer_list(), eval_condition_wrt_precondition_p(), forloop_to_postcondition(), fortran_user_call_to_transformer(), generic_module_name_to_transformers(), generic_transformer_intra_to_inter(), integer_expression_and_precondition_to_integer_interval(), interprocedural_abc_arrays(), load_arc_precondition(), loop_to_postcondition(), loop_to_total_precondition(), loop_to_transformer(), module_name_to_total_preconditions(), old_complete_whileloop_transformer(), precondition_to_abstract_store(), process_call_for_summary_precondition(), process_ready_node(), program_precondition(), propagate_preconditions_in_declarations(), recompute_loop_transformer(), standard_whileloop_to_transformer(), test_to_postcondition(), test_to_transformer(), test_to_transformer_list(), transformer_add_anded_conditions_updown(), transformer_add_any_relation_information(), transformer_add_integer_relation_information(), transformer_add_ored_conditions_updown(), transformer_apply(), transformer_convex_hulls(), transformer_derivative_fix_point(), transformer_domain_intersection(), transformer_equality_fix_point(), transformer_halbwachs_fix_point(), transformer_inverse_apply(), transformer_pattern_fix_point(), transformer_range(), transformer_to_domain(), unstructured_continuation_conditions(), unstructured_to_postcondition(), unstructured_to_postconditions(), unstructured_to_total_precondition(), unstructured_to_transformer(), update_summary_precondition(), update_temporary_precondition(), and whileloop_to_postcondition().
transformer transformer_empty | ( | void | ) |
Allocate an empty transformer.
Definition at line 120 of file basic.c.
References BASE_NULLE, make_predicate(), make_transformer(), NIL, and sc_empty().
Referenced by add_index_range_conditions(), block_continuation_conditions(), call_continuation_conditions(), complete_repeatloop_transformer_list(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), expression_multiply_sizeof_to_transformer(), generic_transformer_list_to_transformer(), get_control_precondition(), integer_binary_operation_to_transformer(), intrinsic_to_transformer(), intrinsic_to_transformer_list(), load_arc_precondition(), loop_continuation_conditions(), loop_to_postcondition(), loop_to_total_precondition(), module_summary_continuation_conditions(), modulo_of_a_constant_to_transformer(), modulo_to_transformer(), new_array_elements_backward_substitution_in_transformer(), new_array_elements_forward_substitution_in_transformer(), new_substitute_stubs_in_transformer(), ordinary_summary_precondition(), pointer_binary_operation_to_transformer(), points_to_unary_operation_to_transformer(), precondition_intra_to_inter(), process_bounds_for_divide(), process_unreachable_node(), ready_to_be_processed_p(), repeatloop_to_postcondition(), standard_whileloop_to_transformer(), statement_to_total_precondition(), summary_total_postcondition(), test_continuation_conditions(), transformer_add_call_condition_information_updown(), transformer_add_condition_information_updown(), transformer_general_intersection(), transformer_list_generic_transitive_closure(), unstructured_continuation_conditions(), unstructured_to_flow_insensitive_transformer(), unstructured_to_postconditions(), unstructured_to_transformer(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
bool transformer_empty_p | ( | transformer | t | ) |
If true is returned, the transformer certainly is empty.
If false is returned, the transformer still might be empty, but it's not too likely...
Well, k <= 2 and k >= 3 does not return empty in spite of sc_strong_normalize()... sc_bounded_normalization() should be used at a cost of O(n)
See also transformer_is_empty_p() for a simple quick syntactic check
Definition at line 2455 of file transformer.c.
References parametric_transformer_empty_p(), and sc_strong_normalize4().
Referenced by apply_transformer_lists_generic(), block_to_transformer_list(), check_condition_wrt_precondition(), check_transformer_list(), clean_up_transformer_list(), combine_transformer_lists(), eval_condition_wrt_precondition_p(), fortran_user_call_to_transformer(), generic_module_name_to_transformers(), instruction_to_transformer_list(), integer_binary_operation_to_transformer(), integer_multiply_to_transformer(), logical_binary_function_to_transformer(), main_summary_precondition(), precondition_intra_to_inter(), process_unreachable_node(), ready_to_be_processed_p(), simplify_boolean_expression_with_precondition(), standard_whileloop_to_transformer(), statement_feasible_p(), transformer_add_modified_variable_entity(), transformer_add_value_update(), transformer_apply_generic(), transformer_basic_fix_point(), transformer_convex_hulls(), transformer_derivative_fix_point(), transformer_equality_fix_point(), transformer_general_intersection(), transformer_list_add_combination(), transformer_projection_with_redundancy_elimination_and_check(), transformers_combine(), two_transformers_to_list(), unstructured_to_postcondition(), unstructured_to_total_precondition(), and unstructured_to_transformer().
transformer transformer_equalities_add | ( | transformer | tf, |
Pcontrainte | eqs | ||
) |
please, do not introduce any sharing at the Pcontrainte level you do not know how they have to be chained in diferent transformers; do not introduce any sharing at the Pvecteur level; I'm not sure it's so useful, but think of what would happen if one transformer is renamed...
tf | f |
eqs | qs |
Definition at line 391 of file basic.c.
References CONTRAINTE_UNDEFINED, contrainte_vecteur, Scontrainte::succ, transformer_constraint_add(), and vect_dup().
Referenced by tf_equivalence_equalities_add().
transformer transformer_equality_add | ( | transformer | tf, |
Pvecteur | i | ||
) |
tf | f |
Definition at line 383 of file basic.c.
References transformer_constraint_add().
Referenced by add_loop_index_exit_value(), add_type_information(), bitwise_xor_to_transformer(), expression_multiply_sizeof_to_transformer(), formal_and_actual_parameters_association(), fortran_data_to_prec_for_variables(), integer_left_shift_to_transformer(), integer_multiply_to_transformer(), logical_unary_operation_to_transformer(), transformer_add_3d_affine_constraint(), transformer_add_condition_information_updown(), transformer_add_equality(), transformer_add_equality_with_affine_term(), transformer_add_equality_with_integer_constant(), transformer_add_identity(), and transformer_add_integer_relation_information().
transformer transformer_equality_fix_point | ( | transformer | tf | ) |
Let A be the affine loop transfert function.
The affine transfer fix-point T is such that T(A-I) = 0
T A = 0 also gives a fix-point when merged with the initial state. It can only be used to compute preconditions.
Algorithm (let H be A's Smith normal form):
A = A - I (if necessary) H = P A Q A = P^-1 H Q^-1 T A = T P^-1 H Q^-1 = 0 T P^-1 H = 0 (by multipliying by Q)
Soit X t.q. X H = 0 A basis for all solutions is given by X chosen such that X is a rectangular matrix (0 I) selecting the zero submatrix of H
Note: I (FI) believe this functions is wrong because it does not return the appropriate arguments. The fix point transformer should modify as many variables as the input tf. A new basis should not be recomputed according to the transition matrix. This problem seems to be fixed in the callers, see loop_to_transformer() and whileloop_to_transformer().
result
do not modify an input argument
number of transfer equalities plus the homogeneous constraint which states that 1 == 1
use a matrix a to store these equalities in a dense form
Pbase t = BASE_UNDEFINED;
If the input transformer is not feasible, so is not its fixpoint because the number of iterations may be zero which implies identity.
fix_tf = transformer_identity();
find or build explicit transfer equations: v::new = f(v1::old, v2::old,...) and the corresponding sub-basis
FI: for each constant variable, whose constance is implictly implied by not having it in the argument field, an equation should be added...
lieq = build_implicit_equalities(tf); lieq->succ = leq; leq = lieq;
build matrix a from lteq and b_new: this should be moved in a function
Subtract the identity matrix
Compute the Smith normal form: H = P A Q
Find out the number of invariants n_inv
Convert p's last n_inv rows into constraints
FI: maybe I should retrieve fix_tf system...
is it a non-trivial invariant?
Set fix_tf's argument list
Fix the basis and the dimension
get rid of dense matrices
tf | f |
Definition at line 266 of file fix_point.c.
bool transformer_equations_constrain_variable_p | ( | const | transformer, |
const | entity | ||
) |
Is value v used with a non-zero coefficient by the equations of transformer t?
Definition at line 963 of file basic.c.
References predicate_system, sc_equations_constrain_variable_p(), and transformer_relation.
transformer transformer_filter | ( | transformer | t, |
list | args | ||
) |
transformer transformer_filter(transformer t, cons * args): projection of t along the hyperplane defined by entities in args; this generate a projection and not a cylinder based on the projection;
if the relation associated to t is empty, t is not modified although it should have a basis and this basis should be cleaned up. Since no basis is carried in the current implementation of an empty system, this cannot be performed (FI, 7/12/92).
formal argument args is not modified. t is updated by side effect.
Note: this function is almost equal to transformer_projection(); however, entities of args do not all have to appear in t's relation; thus transformer_filter has a larger definition domain than transformer_projection; on transformer_projection's domain, both functions are equal
transformer_projection is useful to get cores when you know all entities in args should appear in the relation.
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
sc_fprint(stderr, r, exernal_value_name);
sc_fprint(stderr, r, (char * (*)(Variable)) entity_local_name);
get rid of unwanted values in the relation r and in the basis
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
r = sc_projection(r, (Variable) e);
CA
sc_projection_along_variable_ofl_ctrl_timeout_ctrl
sc_projection_along_variable_ofl_ctrl(&r, (Variable) e, OFL_CTRL);
compute new_args
use functions on arguments instead of in-lining ! MAPL(ce, { entity e = ENTITY(CAR(ce)); if((entity) gen_find_eq(e, args)== (entity) chunk_undefined) { – e must be kept if it is not in args – new_args = arguments_add_entity(new_args, e); }}, transformer_arguments(t));
update the relation and the arguments field for t
Is the relation updated by side effect? Yes, in general. No if the system is non feasible
replace the old arguments by the new one
sc_fprint(stderr, r, exernal_value_name);
args | rgs |
Definition at line 1716 of file transformer.c.
References arguments_difference(), Ssysteme::base, base_contains_variable_p(), CAR, CATCH, Ssysteme::dimension, dump_arguments(), ENDP, ENTITY, entity_global_name(), entity_name, fprint_transformer(), free_arguments(), gen_free_list(), ifdebug, list_undefined, newgen_Psysteme, NIL, NO_OFL_CTRL, overflow_error, pips_assert, pips_debug, pips_user_warning, POP, predicate_system, predicate_system_, sc_base_remove_variable(), sc_elim_var(), sc_empty_p(), transformer_arguments, transformer_relation, transformer_weak_consistency_p(), TRY, UNCATCH, and vect_size().
Referenced by c_user_function_call_to_transformer(), fortran_user_call_to_transformer(), fortran_user_function_call_to_transformer(), loop_to_transformer(), statement_to_postcondition(), statement_to_total_precondition(), transformer_variables_filter(), and translate_global_value().
void transformer_free | ( | transformer | t | ) |
Definition at line 68 of file basic.c.
References free_transformer().
Referenced by add_loop_index_exit_value(), add_loop_index_initialization(), add_module_call_site_precondition(), comp_regions_of_implied_do(), complete_loop_transformer(), complete_loop_transformer_list(), do_array_expansion(), invariant_wrt_transformer(), loop_to_postcondition(), loop_to_total_precondition(), process_call_for_summary_precondition(), statement_to_transformer(), statement_to_transformer_list(), test_to_transformer(), test_to_transformer_list(), transformer_add_any_relation_information(), transformer_halbwachs_fix_point(), unstructured_to_postcondition(), unstructured_to_postconditions(), unstructured_to_total_precondition(), update_summary_precondition(), whileloop_to_postcondition(), and whileloop_to_total_precondition().
bool transformer_general_consistency_p | ( | transformer | tf, |
bool | is_weak | ||
) |
the relation should be consistent and any variable corresponding to an old value should appear in the argument list since an old value cannot (should not) be introduced unless the variable is changed and since every changed variable is in the argument list.
Apparently, a variable may appear as an argument but its old value does not have to appear in the basis if it is not required by the constraints. This does not seem very safe to me (FI, 13 Nov. 95)
The NewGen data structure must be fully defined
The predicate must be weakly consistent. Every variable in the constraints must be in the basis (but not the other way round).
If an old value appears in the predicate, the corresponding variable should be an argument of the transformer
test aliasing between arguments and relations high cost testing
FI: the next test is not safe because val can be a global value not recognized in the current context. old_value_entity_p() returns true or FALSE or pips_error.
A general version of this routine is needed... The return value of a function is not recognized as a global value by old_value_entity_p
old_value_entity_p() is likely to core dump on interprocedural transformers and preconditions.
The constant term should not appear in the basis
The constant term should not be an argument
Check that the transformer is compatible with the current value mappings.
This is not always true as you may need to import the summary transformer of a callee. Before translation, this check will most likely fail.
Debugging step which does not return if an incompatibility is found.
Check that every argument has a value. This is not redundant with the printout procedure which uses entity_minimal_name() and not the value mappings.
Values returned by callees may appear in interprocedural transformers
FI: let the user react and print info before core dumping
pips_assert("transformer_consistency_p", consistent);
tf | f |
is_weak | s_weak |
Definition at line 632 of file basic.c.
References BASE_UNDEFINED, BASE_UNDEFINED_P, CAR, debug(), dump_transformer, entities_may_conflict_p(), ENTITY, entity_has_values_p(), entity_in_formal_area_p(), entity_is_argument_p(), entity_local_name(), entity_module_name(), entity_name, entity_storage, entity_stub_sink_p(), FOREACH, ifdebug, MAP, old_value_entity_p(), pips_debug, pips_internal_error, pips_user_warning, POP, predicate_system, same_string_p, sc_weak_consistent_p(), storage_return_p, Svecteur::succ, TCST, term_cst, transformer_argument_consistency_p(), transformer_arguments, TRANSFORMER_CONSISTENCY_P_DEBUG_LEVEL, transformer_defined_p(), transformer_relation, value_to_variable(), and vecteur_var.
Referenced by transformer_consistency_p(), transformer_weak_consistency_p(), and transformers_consistency_p().
transformer transformer_halbwachs_fix_point | ( | transformer | tf | ) |
THIS FUNCTION WAS NEVER CORRECT AND HAS NOT BEEN REWRITTEN FOR THE NEW VALUE PACKAGE
simple fix-point for inductive variables: loop bounds are ignored
cons * args = effects_to_arguments(e);
tf1: transformer for one loop iteration
tf2: transformer for two loop iterations
tf12: transformer for one or two loop iterations
tf23: transformer for two or three loop iterations
tf_star: transformer for one, two, three,... loop iterations should be called tf_plus by I do not use the one_trip flag
preserve transformer of loop body s
temporarily commented out
duplicate tf1 because transformer_combine might not be able to use twice the same argument
input/output relation for one or two iteration of the loop
apply one iteration on tf12
fix-point
should be done again based on Chenikova
tf_star = transformer_fix_point(tf12, tf23);
free useless transformers
tf | f |
Definition at line 143 of file fix_point.c.
References fprintf(), ifdebug, pips_internal_error, print_transformer, transformer_combine(), transformer_convex_hull(), transformer_dup(), transformer_free(), and transformer_undefined.
Referenced by standard_whileloop_to_transformer().
transformer transformer_identity | ( | void | ) |
Allocate an identity transformer.
return make_transformer(NIL, make_predicate(SC_RN));
en fait, on voudrait initialiser a "liste de contraintes vide"
Definition at line 110 of file basic.c.
References CONTRAINTE_UNDEFINED, make_predicate(), make_transformer(), NIL, and sc_make().
Referenced by __attribute__(), addition_operation_to_transformer(), any_expression_to_transformer(), any_expressions_to_transformer(), any_user_call_site_to_transformer(), args_to_transformer(), bitwise_xor_to_transformer(), block_continuation_conditions(), block_to_transformer(), c_data_to_prec_for_variables(), c_return_to_transformer(), call_continuation_conditions(), call_to_transformer(), clean_up_transformer_list(), complete_loop_transformer(), complete_loop_transformer_list(), complete_repeatloop_transformer_list(), compute_postcondition(), condition_to_transformer(), constant_to_transformer(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), declaration_to_transformer(), declaration_to_transformer_list(), declarations_to_transformer(), declarations_to_transformer_list(), dimensions_to_transformer(), effects_to_transformer(), expression_multiply_sizeof_to_transformer(), expressions_to_transformer(), forloop_to_transformer(), fortran_data_to_prec_for_variables(), generic_abs_to_transformer(), generic_module_name_to_transformers(), generic_transformer_list_to_transformer(), iabs_to_transformer(), instruction_to_transformer(), integer_binary_operation_to_transformer(), integer_call_expression_to_transformer(), integer_expression_to_transformer(), integer_left_shift_to_transformer(), integer_minmax_to_transformer(), integer_multiply_to_transformer(), integer_power_to_transformer(), interprocedural_abc_arrays(), intrinsic_to_transformer(), load_completed_statement_transformer(), logical_binary_function_to_transformer(), logical_expression_to_transformer(), loop_continuation_conditions(), loop_to_continue_transformer(), loop_to_enter_transformer(), merge_transformer_lists(), module_name_to_total_preconditions(), module_summary_continuation_conditions(), modulo_by_a_constant_to_transformer(), modulo_of_a_constant_to_transformer(), modulo_of_a_negative_value_to_transformer(), modulo_of_a_positive_value_to_transformer(), modulo_to_transformer(), new_complete_whileloop_transformer_list(), new_whileloop_to_k_transformer(), new_whileloop_to_transformer(), old_complete_whileloop_transformer(), old_summary_precondition(), ordinary_summary_precondition(), pointer_unary_operation_to_transformer(), precondition_intra_to_inter(), program_postcondition(), program_precondition(), repeatloop_to_postcondition(), repeatloop_to_transformer(), safe_any_assign_operation_to_transformer(), safe_any_expression_to_transformer(), safe_assigned_expression_to_transformer(), safe_assigned_expression_to_transformer_list(), safe_expression_to_transformer(), sequence_dg(), standard_whileloop_to_transformer(), statement_continuation_conditions(), statement_to_transformer(), statement_to_transformer_list(), summary_total_postcondition(), test_continuation_conditions(), test_to_transformer(), test_to_transformer_list(), transformer_add_any_relation_information(), transformer_apply_field_assignments_or_equalities(), transformer_apply_unknown_field_assignments_or_equalities(), transformer_convex_hulls(), transformer_derivative_fix_point(), transformer_equality_fix_point(), transformer_general_intersection(), transformer_list_generic_transitive_closure(), transformer_safe_domain_intersection(), translate_to_module_frame(), unstructured_continuation_conditions(), unstructured_to_transformer(), and whileloop_to_postcondition().
bool transformer_identity_p | ( | transformer | t | ) |
Check that t is an identity function.
no variables are modified; no constraints exist on their values
Definition at line 154 of file basic.c.
References NIL, pips_assert, predicate_system, transformer_arguments, transformer_relation, and transformer_undefined.
Referenced by add_module_call_site_precondition(), check_transformer_list(), clean_up_transformer_list(), merge_transformer_lists(), modulo_to_transformer(), process_call_for_summary_precondition(), and two_transformers_to_list().
transformer transformer_image_intersection | ( | transformer | t1, |
transformer | t2 | ||
) |
allocate a new transformer based on transformer t1 and postcondition t2
t1 | 1 |
t2 | 2 |
Definition at line 608 of file transformer.c.
References pips_debug, transformer_general_intersection(), and transformer_undefined.
Referenced by statement_to_transformer(), transformer_domain_intersection(), and transformer_range_intersection().
transformer transformer_inequalities_add | ( | transformer | tf, |
Pcontrainte | ineqs | ||
) |
Warning:
tf | f |
ineqs | neqs |
Definition at line 409 of file basic.c.
References contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, and transformer_constraint_add().
Referenced by generic_minmax_to_transformer().
bool transformer_inequalities_constrain_variable_p | ( | const | transformer, |
const | entity | ||
) |
Is value v used with a non-zero coefficient by the inequalities of transformer t?
Definition at line 972 of file basic.c.
References predicate_system, sc_inequalities_constrain_variable_p(), and transformer_relation.
transformer transformer_inequality_add | ( | transformer | tf, |
Pvecteur | i | ||
) |
tf | f |
Definition at line 375 of file basic.c.
References transformer_constraint_add().
Referenced by add_affine_bound_conditions(), add_declaration_list_information(), add_loop_index_exit_value(), add_loop_skip_condition(), add_reference_information(), bitwise_xor_to_transformer(), expression_multiply_sizeof_to_transformer(), generic_abs_to_transformer(), iabs_to_transformer(), integer_left_shift_to_transformer(), integer_minmax_to_transformer(), integer_multiply_to_transformer(), integer_power_to_transformer(), logical_binary_operation_to_transformer(), loop_bound_evaluation_to_transformer(), transformer_add_3d_affine_constraint(), transformer_add_condition_information_updown(), transformer_add_inequality(), transformer_add_inequality_with_affine_term(), transformer_add_inequality_with_integer_constraint(), transformer_add_integer_relation_information(), and transformer_logical_inequalities_add().
bool transformer_internal_consistency_p | ( | transformer | t | ) |
Same as above but equivalenced variables should not appear in the argument list or in the predicate basis.
Definition at line 790 of file basic.c.
References BASE_NULLE_P, BASE_UNDEFINED, ENTITY, entity_constant_p, entity_local_name(), entity_null_locations_p(), entity_symbolic_p, entity_to_new_value(), FOREACH, intermediate_value_entity_p(), new_value_entity_p(), old_value_entity_p(), pips_assert, pips_user_warning, predicate_system, transformer_arguments, transformer_consistency_p(), transformer_relation, vecteur_succ, and vecteur_var.
Referenced by recompute_loop_transformer(), statement_to_transformer(), statement_to_transformer_list(), transformer_add_integer_relation_information(), and unstructured_to_flow_insensitive_transformer().
transformer transformer_intersect_range_with_domain | ( | transformer | tf | ) |
When tf is used repeatedly in a loop, the range is part of the domain from iteration 2 to the end.
This improves the derivative of tf when tf is involutive on a subspace. A new transformer is allocated. Of course, it cannot be used without caution. note that tf must be a range, i.e. no arguments, no old values in the basis.
tf | f |
Definition at line 845 of file transformer.c.
References base_to_entities(), copy_transformer(), ENTITY, entity_to_old_value(), FOREACH, gen_free_list(), predicate_system, sc_append(), transformer_range(), transformer_relation, and transformer_value_substitute().
Referenced by any_transformer_to_k_closure().
transformer transformer_intersection | ( | transformer | t1, |
transformer | t2 | ||
) |
tf is a new transformer that receives the constraints in t1 and t2.
For implicit equalities carried by args, this implies that the args for tf is the intersection of the args. And that the resulting transformer may be empty: for instance, a variable may be untouched in t1 and incremented in t2, which is impossible.
t1 | 1 |
t2 | 2 |
Definition at line 600 of file transformer.c.
References transformer_general_intersection().
Referenced by bitwise_xor_to_transformer(), expression_multiply_sizeof_to_transformer(), generic_reference_to_transformer(), integer_multiply_to_transformer(), logical_expression_to_transformer(), loop_to_enter_transformer(), pointer_expression_to_transformer(), pointer_unary_operation_to_transformer(), transformer_list_multiple_closure_to_precondition(), and whileloop_to_postcondition().
transformer transformer_inverse_apply | ( | transformer | tf, |
transformer | post | ||
) |
transformer transformer_inverse_apply(transformer tf, transformer post): apply transformer tf on precondition pre to obtain postcondition post
pre = post(tf) = tf o post
There is (should be!) no sharing between post and tf. No sharing is introduced between post or tf and pre. Neither post nor tf are modified.
pre = post o tf ; tf would be modified by transformer_combine
tf | f |
post | ost |
Definition at line 1657 of file transformer.c.
References dump_transformer, ifdebug, pips_assert, pips_debug, transformer_combine(), transformer_consistency_p(), transformer_dup(), and transformer_undefined.
Referenced by call_to_total_precondition(), loop_to_total_precondition(), and transformer_safe_inverse_apply().
bool transformer_is_empty_p | ( | transformer | t | ) |
Check that transformer t is the canonical representation of an empty transformer.
See transformer_empty_p(), transformer_strongly_empty_p() if you need to check that a set of affine constraints is not feasible.
Definition at line 172 of file basic.c.
References ENDP, pips_assert, predicate_system, sc_empty_p(), transformer_arguments, transformer_relation, and transformer_undefined.
Referenced by generic_apply_effects_to_transformer(), transformer_combine(), and transformer_normalize().
bool transformer_is_rn_p | ( | transformer | t | ) |
Check that transformer t is the canonical representation of the whole afine space defined by its basis.
Definition at line 183 of file basic.c.
References pips_assert, predicate_system, transformer_relation, and transformer_undefined.
Referenced by eval_linear_expression(), and transformer_combine().
transformer transformer_list_closure_to_precondition | ( | list | tl, |
transformer | c_t, | ||
transformer | p_0 | ||
) |
Relay to select a heuristic.
tl | l |
c_t | _t |
p_0 | _0 |
Definition at line 705 of file transformer_list.c.
References get_string_property(), pips_assert, pips_user_error, transformer_consistency_p(), transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and transformer_undefined.
Referenced by transformer_list_multiple_closure_to_precondition().
transformer transformer_list_generic_transitive_closure | ( | list | tfl, |
bool | star_p | ||
) |
Computation of an upper approximation of a transitive closure using constraints on the discrete derivative for a list of transformers.
Each transformer is used to compute its derivative and the derivatives are unioned by convex hull.
The reason for doing this is D(T1) U D(T2) == D(T1 U T2) but the complexity is lower
See http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Implicit equations, n::new - n::old = 0, are added because they are necessary for the convex hull.
Intermediate values are used to encode the differences. For instance, i::int = i::new - i::old This code was cut-and-pasted from transformer_derivative_fix_point() but is more general and subsume it transformer transformer_derivative_fix_point(transformer tf)
Since we compute the * transitive closure and not the + transitive closure, the fix point is the identity.
basis of difference vectors
Compute the global argument list and the global base b
Cannot use arguments_union() because a new list is allocated
For each transformer t in list tl
compute its derivative constraint system
add the equations for the unchanged variables
compute its convex hull with the current value of sc if sc is already defined
Add corresponding equation
This could be optimized by using the convex hull of a Psystemes list and by keeping the dual representation of the result instead of converting it several time back and forth.
Multiply the constant terms by the iteration number ik and add a positivity constraint for the iteration number ik and then eliminate the iteration number ik to get T*(dx).
Difference variables must substituted back to differences between old and new values.
Only generate difference equations if the old value is used
Project all difference variables
The full basis must be used again
Plug sc back into tc_tf
That's all!
tfl | fl |
star_p | tar_p |
Definition at line 960 of file transformer_list.c.
References arguments_add_entity(), Ssysteme::base, base_add_variable(), BASE_NULLE, BASE_NULLE_P, base_remove_variable(), base_rm, base_union(), contrainte_make(), CONTRAINTE_UNDEFINED, cute_convex_union(), Ssysteme::dimension, ENDP, ENTITY, entity_is_argument_p(), entity_to_intermediate_value(), entity_to_new_value(), eq, external_value_name(), FOREACH, fprint_transformer(), ifdebug, make_local_temporary_integer_value_entity(), NIL, old_value_entity_p(), pips_debug, predicate_system, print_transformers(), sc_copy(), sc_empty(), sc_equation_add(), sc_fprint(), sc_free(), sc_multiply_constant_terms(), sc_to_minimal_basis(), Svecteur::succ, TCST, TRANSFORMER, transformer_arguments, transformer_consistency_p(), transformer_derivative_constraints(), transformer_empty(), transformer_identity(), transformer_relation, VALUE_MONE, VALUE_ONE, value_to_variable(), VALUE_ZERO, vect_make(), vect_size(), VECTEUR_NUL, and vecteur_var.
Referenced by transformer_list_transitive_closure(), and transformer_list_transitive_closure_plus().
transformer transformer_list_multiple_closure_to_precondition | ( | list | tl, |
transformer | c_t, | ||
transformer | p_0 | ||
) |
When some variables are not modified by some transformers, use projections on subsets to increase the number of identity transformers and to increase the accuracy of the loop precondition.
The preconditions obtained with the different projections are intersected.
FI: this may be useless when derivatives are computed before the convex union. No. This was due to a bug in the computation of list of derivatives.
FI: this should be mathematically useless but it useful when a heuristic is used to compute the invariant. The number of transitions is reduced and hence a limited number of combinations is more likely to end up with a precise result.
tl | l |
c_t | _t |
p_0 | _0 |
Definition at line 826 of file transformer_list.c.
References arguments_difference(), arguments_subset_p(), copy_transformer(), ENTITY, FOREACH, free_transformer(), gen_copy_seq(), gen_free_list(), gen_full_free_list(), gen_length(), get_bool_property(), pips_assert, safe_transformer_projection(), transformer_arguments, transformer_consistency_p(), transformer_consistent_p(), transformer_intersection(), transformer_list_closure_to_precondition(), transformer_list_preserved_variables(), transformer_list_safe_variables_projection(), transformer_list_to_argument(), transformer_list_with_effect(), and transformer_range().
Referenced by whileloop_to_postcondition().
returns the list of variables in vl which are not modified by transformers belonging to tl-tl_v.
tl_v is assumed to be a subset of tl.
vl | l |
tl | l |
tl_v | l_v |
Definition at line 786 of file transformer_list.c.
References CONS, ENTITY, entity_is_argument_p(), FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
Returns a new list of newly allocated projected transformers.
If a value of a variable in list proj appears in t of tl, it is projected. New transformers are allocated to build the projection list.
tl | l |
proj | roj |
Definition at line 730 of file transformer_list.c.
References CONS, copy_transformer(), ENTITY, entity_is_argument_p(), entity_to_old_value(), FOREACH, gen_free_list(), gen_nreverse(), NIL, safe_transformer_projection(), TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
tl | l |
Definition at line 454 of file transformer_list.c.
References CONS, copy_transformer(), ENDP, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by whileloop_to_postcondition().
Returns the list of variables modified by at least one transformer in tl.
tl | l |
Definition at line 753 of file transformer_list.c.
References CONS, ENTITY, FOREACH, gen_in_list_p(), gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
transformer transformer_list_to_transformer | ( | list | ltl | ) |
Reduce the transformer list ltl to one transformer using the convex hull operator.
ltl | tl |
Definition at line 434 of file transformer_list.c.
References generic_transformer_list_to_transformer().
Referenced by complete_any_loop_transformer(), complete_repeatloop_transformer(), new_complete_whileloop_transformer(), transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
transformer transformer_list_transitive_closure | ( | list | tfl | ) |
Compute (U tfl)*.
tfl | fl |
Definition at line 1141 of file transformer_list.c.
References transformer_list_generic_transitive_closure().
Referenced by transformer_list_closure_to_precondition_depth_two(), transformer_list_closure_to_precondition_max_depth(), and unstructured_to_flow_insensitive_transformer().
transformer transformer_list_transitive_closure_plus | ( | list | tfl | ) |
Compute (U tfl)+.
tfl | fl |
Definition at line 1147 of file transformer_list.c.
References transformer_list_generic_transitive_closure().
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().
build a sublist sl of the transformer list tl with transformers that modify the value of variable v
tl | l |
Definition at line 771 of file transformer_list.c.
References CONS, entity_is_argument_p(), FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_arguments.
Referenced by transformer_list_multiple_closure_to_precondition().
transformer transformer_normalize | ( | transformer | t, |
int | level | ||
) |
Eliminate (some) rational or integer redundancy.
Remember that integer redundancy elimination may degrade results because some transformer operator such as convex hull use a rational interpretation of the constraints. Unfortunately, no information is given here about the properties used by the different functions of the C3 linear library which are used.
Does not take into account value types. So s=="hello" and s=="world" do not result into an empty transformer. But floating point values are taken into account.
Start with sc_bounded_normalization and then according to level:
0 -> sc_safe_elim_redund(), sc_elim_redund(), sc_inequations_elim_redund(), sc_rational_feasibility_ofl_ctrl()
1 -> sc_nredund(), build_sc_nredund_2pass(), build_sc_nredund_2pass_ofl_ctrl(), sc_normalize(), build_sc_nredund_1pass_ofl_ctrl(), build_sc_nredund_1pass_ofl_ctrl()
sc_normalize() is well documented (in French)
2 -> sc_strong_normalize(), sc_normalize() sc_strong_normalize_and_check_feasibility(), sc_check_inequality_redundancy(),
3 -> sc_strong_normalize2(): resolve the equations first, then deal with inequalities
4 -> sc_normalize2(): well documented; does not detect redundancy in a<=b, b<=c, a<=c
5 -> sc_strong_normalize3(), sc_strong_normalize_and_check_feasibility (ps, sc_rational_feasibility);
6 -> sc_strong_normalize4() sc_strong_normalize_and_check_feasibility2(ps, sc_normalize, variable_name, 2): well documented, deterministic
7 -> sc_strong_normalize5() sc_strong_normalize_and_check_feasibility2(ps, sc_rational_feasibility, variable_name, 2);
8 -> sc_safe_build_sc_nredund_1pass(): not documented build_sc_nredund_1pass(): do not take equations into consideration
See timing information in the comments below.
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
Select one tradeoff between speed and accuracy: enumerated by increasing speeds according to Beatrice
CA
Let start with an easy O(n) phase, unlikely to generate an overflow. It should be placed in another try-cath in order to return a better r2 in case of a later overflow.
This is not sufficient: it is more efficient to put this call directly in sc_normalize().
Our best choice for accuracy, but damned slow on ocean
Beatrice's best choice: does not deal with minmax2 (only) but still requires 74 minutes of real time (55 minutes of CPU time) for ocean preconditions, when applied to each precondition stored.
Only 64 s for ocean, if preconditions are not normalized. But andne, callabsval, dead2, hind, negand, negand2, or, validation_dead_code are not validated any more. Redundancy could always be detected in a trivial way after propagating values from equations into inequalities.
Francois' own: does most of the easy stuff. Fails on mimax2 and sum_prec, but it is somehow more user-friendly because trivial preconditions are not destroyed as redundant. It makes you feel safer.
Result for full precondition normalization on ocean: 114 s for preconditions, 4 minutes between split ocean.f and OCEAN.prec
Same plus a good feasibility test
Similar, but variable are actually substituted which is sometimes painful when a complex equations is used to replace a simple variable in a simple inequality.
Similar, but variables are substituted if they belong to a more or less simple equation, and simpler equations are processed first and a lexicographically minimal variable is chosen when equivalent variables are available.
Same plus a good feasibility test, plus variable selection for elimination, plus equation selection for elimination
Too expensive according to measurements by Beatrice Creusillet to be used anywhere but before storing transformers or preconditions or before printing them. Lots of calls to string operations when C is the analyzed language because variable names used for sorting are easy to extract due to scope information. It is not clear from the information mailed by Beatrice if sc_normalize2 is also too computational but it should be as only the basis of the constraint system is sorted out to normalize r more effectively.
Very expensive: the system is rebuilt by adding constraints one by one
end of TRY
level | evel |
Definition at line 932 of file transformer.c.
References Ssysteme::base, base_dup(), BASE_NULLE, base_rm, CATCH, Ssysteme::dimension, entity_local_name(), external_value_name(), float_analyzed_p(), fprint_transformer(), fprintf(), free_arguments(), ifdebug, level, NIL, overflow_error, pips_assert, pips_internal_error, pips_user_warning, predicate_system, sc_bounded_normalization(), sc_dup(), sc_empty(), sc_empty_p(), sc_normalize2(), sc_rm(), sc_safe_build_sc_nredund_1pass(), sc_safe_elim_redund(), sc_strong_normalize(), sc_strong_normalize2(), sc_strong_normalize3(), sc_strong_normalize4(), sc_strong_normalize5(), simplify_float_constraint_system(), transformer_arguments, transformer_consistency_p(), transformer_consistent_p(), transformer_is_empty_p(), transformer_relation, TRY, UNCATCH, varval_value_name_is_inferior_p(), vect_size(), and vect_sort_in_place().
Referenced by any_expressions_to_transformer(), any_user_call_site_to_transformer(), block_to_postcondition(), block_to_transformer(), block_to_transformer_list(), call_site_to_module_precondition_text(), call_to_transformer(), combine_transformer_lists(), complete_any_loop_transformer_list(), complete_loop_transformer(), complete_loop_transformer_list(), condition_to_transformer(), declarations_to_transformer(), declarations_to_transformer_list(), expression_multiply_sizeof_to_transformer(), expressions_to_transformer(), generic_module_name_to_transformers(), integer_multiply_to_transformer(), logical_binary_function_to_transformer(), loop_to_enter_transformer(), module_name_to_total_preconditions(), ordinary_summary_precondition(), propagate_preconditions_in_declarations(), statement_to_postcondition(), statement_to_total_precondition(), statement_to_transformer(), statement_to_transformer_list(), summary_precondition(), summary_total_postcondition(), test_to_postcondition(), test_to_total_precondition(), transformer_add_any_relation_information(), transformer_convex_hull(), transformer_list_add_combination(), transformer_safe_normalize(), and update_precondition_with_call_site_preconditions().
transformer transformer_pattern_fix_point | ( | transformer | tf | ) |
This fixpoint function was developped to present a talk at FORMA.
I used examples published by Pugh and I realized that the fixpoint constraints were obvious in the loop body transformer. You just had to identify them. This is not a clever algorithm. It certainly would not resist any messing up with the constraints, i.e. a change of basis. But it provides very good result for a class of applications.
Algorithm:
Let d_i = i::new - i::old. An invariant constraint is a sum of d_i which is equal to zero or greater than zero. Such a constraint is its own fixpoint: if you combine it with itself after renaming i::new as i::int on one hand and i::old as i::int on the other, the global sum for and equation or its sign for an inequality is unchanged.
result
Look for the best loop counter: the smallest increment is chosen
eliminate sharing between v_inc and fix_sc
Replace constant terms in equalities and inequalities by loop counter differences
Remove all constraints to build the invariant transformer
tf | f |
Definition at line 709 of file fix_point.c.
list transformer_projectable_values | ( | transformer | tf | ) |
tf | f |
Definition at line 827 of file basic.c.
References BASE_NULLE_P, BASE_UNDEFINED, CONS, ENTITY, NIL, predicate_system, transformer_relation, vecteur_succ, and vecteur_var.
Referenced by recompute_loop_transformer().
transformer transformer_projection | ( | transformer | t, |
list | args | ||
) |
values in args must be in t's base
transformer transformer_projection(transformer t, cons * args): projection of t along the hyperplane defined by values in args; this generate a projection and not a cylinder based on the projection
use the most complex/complete redundancy elimination in Linear
args is not modified. t is modified by side effects.
sc_safe_elim_redund() may increase the rational generating system
t = transformer_projection_with_redundancy_elimination(t, args, sc_safe_elim_redund);
args | rgs |
Definition at line 1267 of file transformer.c.
References sc_safe_normalize(), and transformer_projection_with_redundancy_elimination().
Referenced by generic_transformer_intra_to_inter(), new_array_element_backward_substitution_in_transformer(), precondition_to_abstract_store(), recompute_loop_transformer(), safe_transformer_projection(), transformer_add_loop_index_initialization(), transformer_arguments_projection(), transformer_filter_subsumed_variables(), transformer_formal_parameter_projection(), transformer_return_value_projection(), translate_global_value(), and value_passing_summary_transformer().
transformer transformer_projection_with_redundancy_elimination | ( | transformer | t, |
list | args, | ||
Psysteme(*)(Psysteme) | elim | ||
) |
It is not clear if this function projects values or variables.
If variables were projected, all values associated to a variable should also be projected. If values are projected and the transformer argument updated using args, old values should not be left in the basis when a new value is projected and its associated variable removed from tthe argument.
New values are identical to variables which makes it confusing.
The implementation, and the signature, are aware of the nature of the underlying predicate.
args | rgs |
Definition at line 1322 of file transformer.c.
References transformer_projection_with_redundancy_elimination_and_check().
Referenced by precondition_intra_to_inter(), transformer_projection(), transformer_range(), and transformer_temporary_value_projection().
transformer transformer_projection_with_redundancy_elimination_and_check | ( | volatile | transformer, |
list | args, | ||
Psysteme(*)(Psysteme) | elim, | ||
bool | check_consistency_p | ||
) |
Library Linear/sc contains several reundancy elimination functions: sc_elim_redund() build_sc_nredund_2pass_ofl_ctrl() — if it had the same profile... ... no_elim() is provided here to obtain the fastest possible projection
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
sc_fprint(stderr, r, exernal_value_name);
sc_fprint(stderr, r, (char * (*)(Variable)) entity_local_name);
A side effect of transformer_empty_p() is to normalize the transformer.
This is very expensive before a projection. empty_transformer_p()
Step 1: get rid of unwanted values in the relation r and in the basis
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
FC
sc_projection_along_variable_ofl_ctrl_timeout_ctrl
could eliminate redundancy at each projection stage to avoid explosion of the constraint number... however it is pretty expensive to do so. But we explode with NPRIO in FPPP (Spec CFP'95 benchmark). A heuristic could apply redundacy elimination from time to time?
Eliminate trivial redundant constraints generated by the projection
Probably redundant with what happens in elim()
if (SC_EMPTY_P(r)) { r = sc_empty(BASE_NULLE); sc_base_remove_variable(r,(Variable) e); } else base_rm(b); }
sc_fprint(stderr, r, exernal_value_name);
Step 2: eliminate redundancy only/again once projections have all been performed because redundancy elimination is expensive and because most variables are exactly projected because they appear in at least one equation
Should we use b or not? It does make some mathematical sense but it is not compatible with the argument list which should not be empty if old values appear in the basis. And the basis should not be used, even in convex hulls if the emptiness is detected first.
get rid of a useless basis
sc_fprint(stderr, r, exernal_value_name);
Step 3: compute new_args, but beware of left over old values!
e must be kept if it is not in args
The variable is going to be dropped from the argument list
Must be a variable from a module which is not the current module
Step 4: update the relation and the arguments field for t
the relation is updated by side effect FI ? Maybe not if SC_EMPTY(r) 1 Feb. 94
replace the old arguments by the new one, except if the constraint system is not feasible
sc_fprint(stderr, r, exernal_value_name);
Weak, because return value may still be present for functions.
args | rgs |
check_consistency_p | heck_consistency_p |
Definition at line 1343 of file transformer.c.
References arguments_add_entity(), Ssysteme::base, base_contains_variable_p(), base_dup(), BASE_NULLE, base_rm, CAR, CATCH, chunk_undefined, Ssysteme::dimension, empty_transformer(), ENDP, ENTITY, entity_global_name(), entity_has_values_p(), entity_name, entity_to_old_value(), entity_undefined, FOREACH, fprint_transformer(), fprintf(), gen_find_eq(), gen_free_list(), global_new_value_to_global_old_value(), ifdebug, local_temporary_value_entity_p(), newgen_Psysteme, NIL, NO_OFL_CTRL, overflow_error, pips_assert, pips_debug, pips_internal_error, pips_user_warning, POP, predicate_system, predicate_system_, print_entities(), sc_base_remove_variable(), sc_bounded_normalization(), sc_elim_var(), sc_empty(), sc_empty_p(), sc_fprint(), sc_to_minimal_basis(), transformer_arguments, transformer_empty_p(), transformer_relation, transformer_weak_consistency_p(), TRY, UNCATCH, value_to_variable(), vect_rm(), and vect_size().
Referenced by transformer_projection_with_redundancy_elimination(), and transformer_projection_without_check().
transformer transformer_projection_without_check | ( | transformer | t, |
list | args, | ||
Psysteme(*)(Psysteme) | elim | ||
) |
In some cases, you know the projection will result in a non-consistent transformer that will be fixed later.
The input transformer is nevertheless expected weakly consistent.
args | rgs |
Definition at line 1334 of file transformer.c.
References transformer_projection_with_redundancy_elimination_and_check().
Referenced by transformer_to_domain().
transformer transformer_range | ( | transformer | tf | ) |
Return the range of relation tf in a newly allocated transformer.
Projection of all old values.
A variable may be modified but its old value does not have to appear in the basis. Although the opposite is wrong.
rtf = transformer_projection(rtf, args);
tf | f |
Definition at line 714 of file transformer.c.
References base_contains_variable_p(), CONS, ENTITY, entity_to_old_value(), FOREACH, gen_free_list(), NIL, predicate_system, sc_identity(), transformer_arguments, transformer_dup(), transformer_projection_with_redundancy_elimination(), and transformer_relation.
Referenced by add_index_bound_conditions(), add_loop_index_initialization(), addition_operation_to_transformer(), any_conditional_to_transformer(), any_expressions_to_transformer(), any_loop_to_k_transformer(), any_transformer_to_k_closure(), assign_rhs_to_reflhs_to_transformer(), bitwise_xor_to_transformer(), block_to_transformer_list(), c_data_to_prec_for_variables(), call_to_postcondition(), complete_loop_transformer(), condition_to_transformer(), conditional_to_transformer(), declaration_to_transformer(), declaration_to_transformer_list(), declarations_to_transformer(), declarations_to_transformer_list(), dimensions_to_transformer(), do_array_expansion(), do_solve_hardware_constraints_on_nb_proc(), do_solve_hardware_constraints_on_volume(), effects_to_dma(), eval_linear_expression(), expression_multiply_sizeof_to_transformer(), expressions_to_transformer(), fortran_data_to_prec_for_variables(), generic_unary_operation_to_transformer(), integer_binary_operation_to_transformer(), integer_left_shift_to_transformer(), integer_multiply_to_transformer(), integer_power_to_transformer(), logical_not_to_transformer(), loop_body_transformer_add_entry_and_iteration_information(), loop_to_postcondition(), loop_to_transformer(), memorize_precondition_for_summary_precondition(), modulo_to_transformer(), new_loop_to_transformer(), partial_eval_min_or_max_operator(), pointer_unary_operation_to_transformer(), precondition_add_condition_information(), process_ready_node(), safe_assigned_expression_to_transformer(), safe_assigned_expression_to_transformer_list(), statement_to_total_precondition(), statement_to_transformer(), statement_to_transformer_list(), transformer_add_any_relation_information(), transformer_combine(), transformer_intersect_range_with_domain(), transformer_list_multiple_closure_to_precondition(), transformer_safe_range(), transformers_range(), unstructured_to_flow_sensitive_postconditions_or_transformers(), unstructured_to_postconditions(), and whileloop_to_postcondition().
transformer transformer_range_intersection | ( | transformer | tf, |
transformer | r | ||
) |
Allocate a new transformer rtf that is tf with its range restricted by the range r.
As a range, r is assumed to have no arguments.
tf | f |
Definition at line 830 of file transformer.c.
References ENDP, pips_assert, transformer_arguments, and transformer_image_intersection().
Referenced by add_index_bound_conditions(), integer_expression_and_precondition_to_integer_interval(), process_ready_node(), and transformer_combine().
transformer transformer_return_value_projection | ( | entity | f, |
transformer | t | ||
) |
Project return values that are not linked to function f.
Almost identical to transformer_formal_parameter_projection(). A lambda expression should be passed for the filtering.
Dealing with an interprocedural transformer, weak consistency is not true
pips_assert("t is weakly consistent", transformer_weak_consistency_p(t));
Definition at line 1220 of file transformer.c.
References BASE_NULLE_P, BASE_UNDEFINED, CONS, dump_transformer, ENTITY, entity_storage, f(), fprintf(), gen_free_list(), ifdebug, NIL, pips_assert, pips_debug, predicate_system, print_entities(), sc_weak_consistent_p(), storage_return, storage_return_p, transformer_projection(), transformer_relation, transformer_weak_consistency_p(), value_to_variable(), vecteur_succ, and vecteur_var.
Referenced by struct_reference_assignment_or_equality_to_transformer().
bool transformer_safe_affect_transformer_p | ( | transformer | tf1, |
transformer | tf2 | ||
) |
tf1 | f1 |
tf2 | f2 |
Definition at line 1894 of file transformer.c.
References transformer_affect_transformer_p(), and transformer_undefined_p.
Referenced by transformer_safe_combine_with_warnings().
transformer transformer_safe_apply | ( | transformer | tf, |
transformer | pre | ||
) |
tf | f |
pre | re |
Definition at line 1627 of file transformer.c.
References transformer_apply(), transformer_undefined, and transformer_undefined_p.
Referenced by block_to_transformer(), block_to_transformer_list(), declarations_to_transformer(), declarations_to_transformer_list(), expression_multiply_sizeof_to_transformer(), integer_binary_operation_to_transformer(), integer_left_shift_to_transformer(), integer_multiply_to_transformer(), loop_bound_evaluation_to_transformer(), propagate_preconditions_in_declarations(), transformers_safe_apply(), and unstructured_to_transformer().
transformer transformer_safe_combine_with_warnings | ( | transformer | tf1, |
transformer | tf2 | ||
) |
Transformer tf1 and tf2 are supposed to be independent but they may interfere, for instance because subexpressions have non-standard conformant side effects.
tf12 is a newly allocated transformer with no sharing with tf1 or tf2 (theoretically).
Intersection is not powerful enough to cope with side effects. But side effects can be dealt with only if the operation order is known when the standard is violated. We assume here a right to left evaluation.
No side effects at all
tf1 | f1 |
tf2 | f2 |
Definition at line 493 of file transformer.c.
References ENDP, free_transformer(), pips_debug, pips_user_warning, transformer_arguments, transformer_combine(), transformer_safe_affect_transformer_p(), transformer_safe_intersection(), transformer_undefined, and transformer_undefined_p.
Referenced by addition_operation_to_transformer(), and transformer_add_any_relation_information().
transformer transformer_safe_domain | ( | transformer | tf | ) |
tf | f |
Definition at line 815 of file transformer.c.
References transformer_to_domain(), transformer_undefined, and transformer_undefined_p.
transformer transformer_safe_domain_intersection | ( | transformer | tf, |
transformer | pre | ||
) |
If tf and pre are defined, update tf.
If tf is defined and pre is undefined, return tf unchanged. If tf and pre are undefined, return tf unchanged. If tf is undefined and pre is defined, we could exploit pre or return undefined.
tf | f |
pre | re |
Definition at line 696 of file transformer.c.
References transformer_domain_intersection(), transformer_identity(), and transformer_undefined_p.
Referenced by call_to_transformer().
transformer transformer_safe_image_intersection | ( | transformer | t1, |
transformer | t2 | ||
) |
Allocate a new transformer.
t1 | 1 |
t2 | 2 |
Definition at line 647 of file transformer.c.
References transformer_safe_general_intersection().
Referenced by add_formal_to_actual_bindings(), addition_operation_to_transformer(), fortran_user_call_to_transformer(), generic_abs_to_transformer(), generic_minmax_to_transformer(), iabs_to_transformer(), integer_minmax_to_transformer(), loop_bound_evaluation_to_transformer(), and transformer_add_any_relation_information().
transformer transformer_safe_intersection | ( | transformer | t1, |
transformer | t2 | ||
) |
Allocate a new transformer.
t1 | 1 |
t2 | 2 |
Definition at line 639 of file transformer.c.
References transformer_safe_general_intersection().
Referenced by logical_binary_operation_to_transformer(), loop_bound_evaluation_to_transformer(), transformer_safe_combine_with_warnings(), and unary_minus_operation_to_transformer().
transformer transformer_safe_inverse_apply | ( | transformer | tf, |
transformer | post | ||
) |
tf | f |
post | ost |
Definition at line 1686 of file transformer.c.
References transformer_inverse_apply(), transformer_undefined, and transformer_undefined_p.
transformer transformer_safe_normalize | ( | transformer | t, |
int | level | ||
) |
level | evel |
Definition at line 1111 of file transformer.c.
References level, transformer_normalize(), and transformer_undefined_p.
Referenced by block_to_transformer(), block_to_transformer_list(), c_data_to_prec_for_variables(), declarations_to_transformer(), declarations_to_transformer_list(), fortran_data_to_prec_for_variables(), propagate_preconditions_in_declarations(), and transformers_safe_normalize().
transformer transformer_safe_range | ( | transformer | tf | ) |
tf | f |
Definition at line 743 of file transformer.c.
References transformer_range(), transformer_undefined, and transformer_undefined_p.
Referenced by loop_initialization_to_transformer().
transformer transformer_safe_value_substitute | ( | transformer | t, |
entity | e1, | ||
entity | e2 | ||
) |
e1 | 1 |
e2 | 2 |
Definition at line 2048 of file transformer.c.
References transformer_undefined_p, and transformer_value_substitute().
Referenced by add_formal_to_actual_bindings().
bool transformer_strongly_empty_p | ( | transformer | t | ) |
If true is returned, the transformer certainly is empty.
If false is returned, the transformer still might be empty, but it's not likely at all...
Definition at line 2465 of file transformer.c.
References parametric_transformer_empty_p(), and sc_strong_normalize5().
Referenced by statement_strongly_feasible_p().
transformer transformer_temporary_value_projection | ( | transformer | tf | ) |
tf = transformer_projection(tf, tv);
tf = transformer_projection_with_redundancy_elimination(tf, tv, sc_identity);
tf | f |
Definition at line 1149 of file transformer.c.
References BASE_NULLE, BASE_NULLE_P, CONS, ENDP, ENTITY, gen_free_list(), ifdebug, local_temporary_value_entity_p(), NIL, number_of_temporary_values(), pips_assert, predicate_system, sc_safe_normalize(), transformer_projection_with_redundancy_elimination(), transformer_relation, vecteur_succ, and vecteur_var.
Referenced by add_index_bound_conditions(), 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(), c_user_call_to_transformer(), call_to_transformer(), condition_to_transformer(), expression_to_transformer(), fortran_data_to_prec_for_variables(), fortran_user_call_to_transformer(), loop_bound_evaluation_to_transformer(), loop_to_enter_transformer(), precondition_add_condition_information(), test_to_postcondition(), test_to_transformer(), test_to_transformer_list(), transformer_add_condition_information(), and update_cp_with_rhs_to_transformer().
bool transformer_to_1D_lattice | ( | entity | v, |
transformer | pre, | ||
Value * | gcd_p, | ||
Value * | c_p | ||
) |
See if the equations in transformer "pre" constraint variable "v" by v = gcd x + c, where x is a free variable.
If "v" is free, gcd==1 and c==0
Entity "v" is supposed to represent a value
Returns true unless the equations in "pre" have no integer solutions.
pre | re |
gcd_p | cd_p |
c_p | _p |
Definition at line 2480 of file transformer.c.
References A, B, base_contains_variable_p(), base_dimension, constraints_to_matrices(), free(), matrices_to_1D_lattice(), MATRIX_ELEM, matrix_new(), predicate_system, rank, rank_of_variable(), and transformer_relation.
Referenced by modulo_by_a_constant_to_transformer().
list transformer_to_analyzed_array_locations | ( | transformer | tf | ) |
tf | f |
Definition at line 2776 of file transformer.c.
References generic_transformer_to_analyzed_locations().
Referenced by generic_substitute_formal_array_elements_in_transformer(), new_array_elements_backward_substitution_in_transformer(), and new_array_elements_forward_substitution_in_transformer().
list transformer_to_analyzed_arrays | ( | transformer | tf | ) |
The list of array entities that appear in the basis of the transformer predicate as array element locations.
tf | f |
Definition at line 2793 of file transformer.c.
References CONS, ENTITY, entity_initial, gen_in_list_p(), NIL, predicate_system, reference_variable, transformer_relation, value_reference, value_reference_p, value_to_variable(), vecteur_succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by generic_substitute_formal_array_elements_in_transformer().
list transformer_to_analyzed_locations | ( | transformer | tf | ) |
The list of location entities that appear in the basis of the transformer predicate.
tf | f |
Definition at line 2785 of file transformer.c.
References generic_transformer_to_analyzed_locations().
Referenced by substitute_stubs_in_transformer(), and substitute_stubs_in_transformer_with_translation_binding().
transformer transformer_to_domain | ( | transformer | tf | ) |
Return the domain of relation tf in a newly allocated transformer.
Projection of all new values of modified variables. Renaming of old values as new values. The transformer returned is a predicate on the input state (i.e. not really a transformer).
dtf = transformer_projection(dtf, args);
dtf = transformer_projection_with_redundancy_elimination(dtf, new_args, sc_identity);
The resulting transformer is going to be inconsistent because old values appear although the argument list is empty.
Careful, sc and b have been updated by the projections
A variable may be modified but its old value does not have to appear in the basis. Although the opposite is wrong.
tf | f |
Definition at line 772 of file transformer.c.
References base_contains_variable_p(), CONS, ENTITY, entity_to_new_value(), entity_to_old_value(), FOREACH, gen_free_list(), NIL, predicate_system, sc_identity(), transformer_arguments, transformer_dup(), transformer_projection_without_check(), transformer_relation, and transformer_value_substitute().
Referenced by call_to_total_precondition(), loop_to_total_precondition(), transformer_combine(), and transformer_safe_domain().
list transformer_to_local_values | ( | transformer | tf, |
list | dl | ||
) |
Build a list of values appearing in tf that are linked to a variable in dl.
These values must be projected if the variables in dl are no longer in the scope, e.g. because they were declared in a block.
FI: I am not sure about what shuold be done for stubs
tf | f |
dl | l |
Definition at line 2821 of file transformer.c.
References CONS, ENTITY, entity_initial, gen_in_list_p(), NIL, predicate_system, reference_variable, transformer_relation, value_reference, value_reference_p, value_to_variable(), vecteur_succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by statement_to_transformer().
list transformer_to_potential_stub_translation | ( | transformer | , |
entity | |||
) |
string transformer_to_string | ( | transformer | tf | ) |
prettyprint.c
tf | f |
Definition at line 52 of file prettyprint.c.
References pips_internal_error, and string_undefined.
bool transformer_value_substitutable_p | ( | transformer | t, |
entity | e1, | ||
entity | e2 | ||
) |
If e1 does not appear in t, it is substitutable.
If e1 does appear in t but not e2, again it is substitutable. Else, it if not.
e1 | 1 |
e2 | 2 |
Definition at line 2033 of file transformer.c.
References Ssysteme::base, base_contains_variable_p(), entity_undefined, pips_assert, predicate_system, and transformer_relation.
Referenced by translate_global_value().
transformer transformer_value_substitute | ( | transformer | t, |
entity | e1, | ||
entity | e2 | ||
) |
transformer transformer_value_substitute(transformer t, entity e1, entity e2): if e2 does not appear in t initially: replaces occurences of value e1 by value e2 in transformer t's arguments and relation fields; else error fi
"e2 must not appear in t initially": this is the general case; the second case may occur when procedure A calls B and C and when B and C share a global variable X which is not seen from A. A may contain relations between B:X and C:X... See hidden.f in Bugs or Validation...
updates are performed by side effects
update only if necessary
rename value e1 in argument a; e1 does not necessarily appear in a because it's not necessarily the new value of a modified variable
e1 | 1 |
e2 | 2 |
Definition at line 1993 of file transformer.c.
References Ssysteme::base, base_contains_variable_p(), CAR, ENTITY, ENTITY_, entity_name, entity_undefined, MAPL, pips_assert, pips_internal_error, predicate_system, sc_variable_rename(), transformer_arguments, and transformer_relation.
Referenced by add_type_information(), 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(), fortran_user_call_to_transformer(), perform_array_element_substitutions_in_transformer(), precondition_intra_to_inter(), substitute_scalar_stub_in_transformer(), substitute_stubs_in_transformer_with_translation_binding(), transformer_intersect_range_with_domain(), transformer_safe_value_substitute(), transformer_to_domain(), translate_global_value(), and value_passing_summary_transformer().
transformer transformer_variables_filter | ( | transformer | t, |
list | vl | ||
) |
Transformers are dealing with variables and/or variable values.
The confusion is magnified because the new value of a variable is often identified to the variable. Also, it is not 100% clear if the argument list of a transformer is a list of variables or a list of new values. In principle, it is a list of variables or locations. To make thisn worse, both value and variable start with a v...
Here, it is assumed that list vl is a list of variables or locations.
Transformer t is modified by side effect. All values linked to any variable in ist vl are projected, when possible. It is assumed that the projected variables are removed from the transformer argument.
vl | l |
Definition at line 1827 of file transformer.c.
References CONS, ENTITY, entity_has_values_p(), entity_to_new_value(), entity_to_old_value(), entity_undefined_p, FOREACH, gen_free_list(), NIL, and transformer_filter().
bool transformer_weak_consistency_p | ( | transformer | t | ) |
Interprocedural transformers do not meet all conditions.
Definition at line 626 of file basic.c.
References transformer_general_consistency_p().
Referenced by c_user_call_to_transformer(), fortran_user_call_to_transformer(), transformer_filter(), transformer_formal_parameter_projection(), transformer_projection_with_redundancy_elimination_and_check(), and transformer_return_value_projection().
bool transformer_with_temporary_values_p | ( | transformer | tf | ) |
Does transformer tf use temporary values?
tf | f |
Definition at line 1131 of file transformer.c.
References BASE_NULLE, BASE_NULLE_P, count, local_temporary_value_entity_p(), number_of_temporary_values(), predicate_system, transformer_relation, vecteur_succ, and vecteur_var.
list transformers_apply | ( | list | tl, |
transformer | pre | ||
) |
Same as previous one, but with a more normalized name.
tl | l |
pre | re |
Definition at line 1616 of file transformer.c.
References transformer_apply_generic().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
list transformers_apply_and_keep_all | ( | list | tl, |
transformer | pre | ||
) |
Same as previous one, but with a more normalized name.
tl | l |
pre | re |
Definition at line 1622 of file transformer.c.
References transformer_apply_generic().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
list transformers_combine | ( | list | tl1, |
transformer | t2 | ||
) |
Combine each transformer of transformer list tl1 with t2.
Side-effect on tl1 or new list etl. See comments for transformer_combine()
FI: I'm not too sure about the best way to remove the resulting empty transformers. gen_remove() on tl1 or creation of new list...
tl1 | l1 |
t2 | 2 |
Definition at line 454 of file transformer.c.
References CONS, FOREACH, gen_free_list(), gen_nconc(), NIL, TRANSFORMER, transformer_combine(), and transformer_empty_p().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
tl | l |
Definition at line 616 of file basic.c.
References FOREACH, TRANSFORMER, and transformer_general_consistency_p().
Referenced by safe_assigned_expression_to_transformer_list().
tl | l |
Definition at line 1262 of file fix_point.c.
References CONS, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_derivative_fix_point().
Referenced by transformer_list_closure_to_precondition_depth_two(), and transformer_list_closure_to_precondition_max_depth().
Substitute each transformer in list tfl by its range.
tfl | fl |
Definition at line 754 of file transformer.c.
References CAR, free_transformer(), MAPL, TRANSFORMER, TRANSFORMER_, and transformer_range().
Referenced by block_to_transformer_list().
list transformers_safe_apply | ( | list | tl, |
transformer | pre | ||
) |
returns a list of postconditions, one for each transformer in tl
tl | l |
pre | re |
Definition at line 1638 of file transformer.c.
References CONS, FOREACH, gen_nreverse(), NIL, TRANSFORMER, and transformer_safe_apply().
Referenced by block_to_transformer_list().
tl | l |
level | evel |
Definition at line 1119 of file transformer.c.
References CONS, FOREACH, gen_nreverse(), level, NIL, TRANSFORMER, and transformer_safe_normalize().
Referenced by block_to_transformer_list().
list two_transformers_to_list | ( | transformer | t1, |
transformer | t2 | ||
) |
Transformer two transformers into a correct transformer list.
Could be generalized to any number of transformers using a varargs... and more thinking.
Two transformers are obtained for loops that may be skipped or entered and for tests whose condition is not statically decidable.
This is a very dangerous step that should not always be taken. It is useful to ease the detection of identity paths, but it looses a lot of information. So almost identity path might simply be better identified elsewhere
t1 | 1 |
t2 | 2 |
Definition at line 316 of file transformer_list.c.
References CONS, free_transformer(), NIL, TRANSFORMER, transformer_empty_p(), and transformer_identity_p().
Referenced by complete_any_loop_transformer_list(), and complete_repeatloop_transformer_list().
Definition at line 899 of file value.c.
References entity_undefined, hash_get(), hash_type_to_sizeof_value, pips_internal_error, type_to_full_string_definition(), and type_to_string().
Referenced by expression_multiply_sizeof_to_transformer().
Static aliasing.
useful for Fortran, useless for C. When no alias is found, an undefined entity must be returned.
lookup the current value name mapping and return an arbitrary "representant" of the interprocedural alias set of e; the equivalence relation is "has same location"
Definition at line 1729 of file value.c.
References entities_may_conflict_p(), entity_name, entity_undefined, HASH_FOREACH, hash_value_to_name, pips_debug, and variable_entity_p().
Referenced by add_interprocedural_new_value_entity(), add_interprocedural_value_entities(), and translate_global_value().
bool value_belongs_to_transformer_space | ( | entity | v, |
transformer | tf | ||
) |
tf | f |
Definition at line 842 of file basic.c.
References BASE_NULLE_P, BASE_UNDEFINED, predicate_system, transformer_relation, vecteur_succ, and vecteur_var.
Referenced by transformer_add_variable_type_information().
tells if e is seen as a variable value in the current module
Definition at line 976 of file value.c.
References hash_get(), HASH_UNDEFINED_VALUE, and hash_value_to_name.
Referenced by generic_value_name(), transformer_add_sign_information(), transformer_filter_subsumed_variables(), and translate_global_value().
for debugging purposes
Definition at line 1762 of file value.c.
References entity_name.
Referenced by parametric_transformer_empty_p().
Get the primitive variable associated to any value involved in a transformer.
For example can associate values such as "o#0" to "i" (via "i#init").
This function used to be restricted to values seen by the current module. It was extended to values in general to cope with translation issues.
for gcc only!
pips_assert("value_to_variable", s != HASH_UNDEFINED_VALUE);
pips_assert("value_to_variable", strchr(entity_name(val), (int) SEMANTICS_SEPARATOR) != NULL);
this may be a value, but it is unknown in the current module
new values in fact have no suffixes...
It can be an equivalenced variable... Additional testing should be performed!
val | al |
Definition at line 1624 of file value.c.
References ADDRESS_OF_SUFFIX, address_of_value_entity_p(), entity_domain, entity_name, entity_undefined, free(), gen_find_tabulated(), hash_get(), HASH_UNDEFINED_VALUE, hash_value_to_name, intermediate_value_entity_p(), INTERMEDIATE_VALUE_SUFFIX, new_value_entity_p(), NEW_VALUE_SUFFIX, old_value_entity_p(), OLD_VALUE_SUFFIX, pips_internal_error, SEMANTICS_SEPARATOR, SIZEOF_SUFFIX, sizeof_value_entity_p(), and strdup().
Referenced by add_address_of_value(), add_loop_index_exit_value(), add_type_information(), any_assign_operation_to_transformer(), any_scalar_assign_to_transformer_list(), any_scalar_assign_to_transformer_without_effect(), fortran_user_call_to_transformer(), generic_transformer_intra_to_inter(), generic_transformer_to_analyzed_locations(), invariant_vector_p(), look_for_the_best_counter(), old_value_to_new_value(), pips_user_value_name(), print_call_precondition(), transformer_add_variable_incrementation(), transformer_add_variable_update(), transformer_derivative_constraints(), transformer_derivative_fix_point(), transformer_formal_parameter_projection(), transformer_general_consistency_p(), transformer_list_generic_transitive_closure(), transformer_projection_with_redundancy_elimination_and_check(), transformer_return_value_projection(), transformer_to_analyzed_arrays(), transformer_to_local_values(), transformer_to_potential_stub_translation(), and value_passing_summary_transformer().
FI: not used, not debugged.
Definition at line 1755 of file value.c.
References entity_to_new_value(), non_local_temporary_value_entity_p(), and vect_rename_variables().
|
extern |
Interface between the untyped database manager and clean code and between pipsmake and clean code.
Several algorithms are available:
a fix point algorithm combining the last two algorithms above. This algorithm adds difference variables d_i = i::new - i::old for each variable i. All non d_i variables are thn projected. If the projection algorithm is sophisticated enough, the projection ordering will be "good". Left over inequalities are invariant or useless. Let N be the strictly positive iteration count:
sum ai di <= -k implies N sum ai di <= -Nk <= -k (OK)
sum ai di <= k implies N sum ai di <= Nk <= infinity (useless unless k == 0)
Left over equations can stay equations if the constant term is 0, or be degraded into an inequation if not. The nw inequation depends on the sign of the constant:
sum ai di == -k implies N sum ai di == -Nk <= -k
sum ai di == k implies N sum ai di == Nk >= k
sum ai di == 0 implies N sum ai di == 0
In a second step, the constant terms are eliminated to obtain new constraints leading to new invariants, using the same rules as above.
This algorithm was designed for while loops such as:
WHILE( I > 0 ) J = J + I I = I - 1
to find as loop transformer T(I,J) {I::new <= I::old - 1, J::new >= J::old + 1, I::new+J::new >= I::old + J::old}
Note that the second constraint is redundant with the other two, but the last one cannot be found before the constant terms are eliminated.
The current algorithm, the derivative version, is published and describes in NSAD 2010, A/426/CRI. See also A/429/CRI: http://www.cri.ensmp.fr/classement/doc/A-429.pdf
Francois Irigoin, 21 April 1990 The fixpoint operator is selected according to properties
Definition at line 114 of file fix_point.c.