PIPS
|
#include <stdio.h>
#include "linear.h"
#include "matrice.h"
#include "sparse_sc.h"
#include "genC.h"
#include "ri.h"
#include "ri-util.h"
#include "effects-util.h"
#include "prettyprint.h"
#include "misc.h"
#include "transformer.h"
Go to the source code of this file.
Functions | |
static Psysteme | sc_identity (Psysteme sc) |
Predicate transformer package: sc complexity level. More... | |
transformer | simple_equality_to_transformer (entity e, entity f, bool assignment) |
e and f are assumed to be values, Type independent. More... | |
transformer | simple_unary_minus_to_transformer (entity e, entity f) |
transformer | generic_equality_to_transformer (entity e, entity f, bool assignment, bool unary_minus_p) |
transformer | simple_addition_to_transformer (entity e, entity e1, entity e2, bool addition_p) |
e and e1 and e2 are assumed to be values. More... | |
transformer | relation_to_transformer (entity op, entity e1, entity e2, bool veracity) |
e and f are assumed to be values. More... | |
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) More... | |
list | transformers_combine (list tl1, transformer t2) |
Combine each transformer of transformer list tl1 with t2. More... | |
list | one_to_one_transformers_combine (list tl1, list tl2) |
Combine each transformer of transformer list tl1 with the corresponding transformer in transformer list tl2. More... | |
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. More... | |
static transformer | transformer_general_intersection (transformer t1, transformer t2, bool image_only) |
Allocate a new transformer with constraints in t1 and t2. More... | |
transformer | transformer_intersection (transformer t1, transformer t2) |
tf is a new transformer that receives the constraints in t1 and t2. More... | |
transformer | transformer_image_intersection (transformer t1, transformer t2) |
allocate a new transformer based on transformer t1 and postcondition t2 More... | |
static transformer | transformer_safe_general_intersection (transformer t1, transformer t2, bool image_only) |
Allocate a new transformer. More... | |
transformer | transformer_safe_intersection (transformer t1, transformer t2) |
Allocate a new transformer. More... | |
transformer | transformer_safe_image_intersection (transformer t1, transformer t2) |
Allocate a new transformer. More... | |
transformer | transformer_domain_intersection (transformer tf, transformer pre) |
Restrict the domain of the relation tf with pre. More... | |
transformer | transformer_safe_domain_intersection (transformer tf, transformer pre) |
If tf and pre are defined, update tf. More... | |
transformer | transformer_range (transformer tf) |
Return the range of relation tf in a newly allocated transformer. More... | |
transformer | transformer_safe_range (transformer tf) |
list | transformers_range (list tfl) |
Substitute each transformer in list tfl by its range. More... | |
transformer | transformer_to_domain (transformer tf) |
Return the domain of relation tf in a newly allocated transformer. More... | |
transformer | transformer_safe_domain (transformer tf) |
transformer | transformer_range_intersection (transformer tf, transformer r) |
Allocate a new transformer rtf that is tf with its range restricted by the range r. More... | |
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. More... | |
static int | varval_value_name_is_inferior_p (Pvecteur *pvarval1, Pvecteur *pvarval2) |
transformer | transformer_normalize (transformer t, int level) |
Eliminate (some) rational or integer redundancy. More... | |
transformer | transformer_safe_normalize (transformer t, int level) |
list | transformers_safe_normalize (list tl, int level) |
bool | transformer_with_temporary_values_p (transformer tf) |
Does transformer tf use temporary values? More... | |
transformer | transformer_temporary_value_projection (transformer tf) |
transformer | safe_transformer_projection (transformer t, list args) |
t may be undefined, args may contain values unrelated to t More... | |
transformer | transformer_return_value_projection (entity f, transformer t) |
Project return values that are not linked to function f. More... | |
transformer | transformer_projection (transformer t, list args) |
values in args must be in t's base More... | |
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 More... | |
Psysteme | no_elim (Psysteme ps) |
transformer | transformer_projection_with_redundancy_elimination (transformer t, list args, Psysteme(*elim)(Psysteme)) |
It is not clear if this function projects values or variables. More... | |
transformer | transformer_projection_without_check (transformer t, list args, Psysteme(*elim)(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 t, list args, Psysteme(*elim)(Psysteme), bool check_consistency_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 More... | |
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. More... | |
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. More... | |
list | transformers_apply (list tl, transformer pre) |
Same as previous one, but with a more normalized name. More... | |
list | transformers_apply_and_keep_all (list tl, transformer pre) |
Same as previous one, but with a more normalized name. More... | |
transformer | transformer_safe_apply (transformer tf, transformer pre) |
list | transformers_safe_apply (list tl, transformer pre) |
returns a list of postconditions, one for each transformer in tl More... | |
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 More... | |
transformer | transformer_safe_inverse_apply (transformer tf, transformer post) |
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; More... | |
transformer | transformer_variables_filter (transformer t, list vl) |
Transformers are dealing with variables and/or variable values. More... | |
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. More... | |
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. More... | |
bool | transformer_safe_affect_transformer_p (transformer tf1, transformer tf2) |
transformer | args_to_transformer (list le) |
Generates a transformer abstracting a totally unknown modification of the values associated to variables in list le. More... | |
transformer | invariant_wrt_transformer (transformer p, transformer tf) |
transformer invariant_wrt_transformer(transformer p, transformer tf): Assume that tf is a fix-point operator. More... | |
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 More... | |
bool | transformer_value_substitutable_p (transformer t, entity e1, entity e2) |
If e1 does not appear in t, it is substitutable. More... | |
transformer | transformer_safe_value_substitute (transformer t, entity e1, entity e2) |
Pvecteur | simplify_float_constraint (Pvecteur v, bool is_equation_p) |
If v is a not a float constraint, retun v. More... | |
Psysteme | simplify_float_constraint_system (Psysteme ps) |
Simplify float constraints and possibly detect. More... | |
static bool | constant_constraint_check (Pvecteur v, bool is_equation_p) |
Check if a transformer is empty. More... | |
static bool | parametric_transformer_empty_p (transformer t, Psysteme(*normalize)(Psysteme, char *(*)(Variable))) |
If true is returned, the transformer certainly is empty. More... | |
bool | transformer_empty_p (transformer t) |
If true is returned, the transformer certainly is empty. More... | |
bool | transformer_strongly_empty_p (transformer t) |
If true is returned, the transformer certainly is empty. More... | |
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. More... | |
static list | entity_to_formal_integer_parameters (entity f) |
get unsorted list of formal integer parameters of module f by declaration filtering; these parameters may not be used by the callee's semantics analysis, but we have no way to know it because value mappings are not available. More... | |
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 More... | |
static bool | expression_equal_in_context_p (expression e1, expression e2, transformer context) |
Fast checks : More... | |
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. More... | |
list | transformer_to_potential_stub_translation (transformer tf, entity m __attribute__((unused))) |
Provide a list of variables that might be forward translated into a stub when preconditions are propagated in callees. More... | |
static list | generic_transformer_to_analyzed_locations (transformer tf, bool array_p) |
The list of location entities that appear in the basis of the transformer predicate. More... | |
list | transformer_to_analyzed_array_locations (transformer tf) |
list | transformer_to_analyzed_locations (transformer tf) |
The list of location entities that appear in the basis of the transformer predicate. More... | |
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. More... | |
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. More... | |
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().
Check if a transformer is empty.
Take into account, if necessary, constraints with floating point and string constraints. Simplify constraints build with float and string constants only
Logical are represented by integer values
PIPS does not represent negative constants: call to unary_minus
s1 = module_local_name(e);
s2 = module_local_name(e);
PIPS does not represent complex constants: call to CMPLX
Unfeasible equation or trivial inequality
Must be a trivial integer constraint. Already processed
Definition at line 2183 of file transformer.c.
References basic_tag, constant_basic(), entity_constant_p, entity_name, false, float_constant_to_double(), fortran_string_compare(), int, is_basic_complex, is_basic_float, is_basic_int, is_basic_logical, is_basic_overloaded, is_basic_string, pips_assert, pips_internal_error, s1, string_undefined, TCST, vect_size(), vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, vecteur_val, vecteur_var, and x.
Referenced by parametric_transformer_empty_p().
get unsorted list of formal integer parameters of module f by declaration filtering; these parameters may not be used by the callee's semantics analysis, but we have no way to know it because value mappings are not available.
Definition at line 2517 of file transformer.c.
References code_declarations, CONS, ENTITY, entity_code(), entity_integer_scalar_p(), entity_module_p(), entity_storage, f(), FOREACH, NIL, pips_assert, and storage_formal_p.
Referenced by formal_and_actual_parameters_association().
|
static |
Fast checks :
Definition at line 2600 of file transformer.c.
References clean_all_normalized(), efficient_sc_check_inequality_feasibility(), entity_local_name(), expression_reference(), expression_reference_p(), fprint_transformer(), fprintf(), ifdebug, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, predicate_system, print_expression(), reference_variable, same_expression_p(), same_scalar_location_p(), TCST, transformer_relation, val_of, value_notzero_p, value_zero_p, vect_add(), vect_constant_p(), vect_multiply(), vect_new(), vect_rm(), vect_substract(), and VECTEUR_NUL_P.
Referenced by same_dimension_p().
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 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().
|
static |
The list of location entities that appear in the basis of the transformer predicate.
Definition at line 2745 of file transformer.c.
References CONS, ENTITY, entity_initial, entity_stub_sink_p(), gen_in_list_p(), local_temporary_value_entity_p(), NIL, predicate_system, transformer_relation, value_reference_p, value_to_variable(), vecteur_succ, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by transformer_to_analyzed_array_locations(), and transformer_to_analyzed_locations().
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().
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().
|
static |
If true is returned, the transformer certainly is empty.
If false is returned, the transformer still might be empty, it all depends on the normalization procedure power. Beware of its execution time!
FI: the arguments seem to have no impact on the emptiness (i.e. falseness) of t
Automatic variables read in a CATCH block need to be declared volatile as specified by the documentation
empty_p = !sc_faisabilite(ps);
empty_p = !sc_rational_feasibility_ofl_ctrl(ps, OFL_CTRL, true);
Normalize the transformer, use all "reasonnable" equations to reduce the problem size, check feasibility on the projected system
new_ps = normalize(new_ps, (char * (*)(Variable)) external_value_name);
FI: when dealing with interprocedural preconditions, the value mappings are initialized for the caller but the convex hull, which calls this function, must be performed in the calle value space.
Depending on the instance of "normalize", might always be trapped by the previous test.
Inconsistent equalities or inequalities between constants may be present. Project variable and temporary values and analyze resulting system. No equations should be left over unless equal constants are encoded differently. Inequations should be interpreted and checked.
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
No redundancy elimination...
new_ps = elim(new_ps);
sc_fprint(stderr, r, exernal_value_name);
Check remaining equalities and inequalities
sc_fprint(stderr, r, exernal_value_name);
Definition at line 2319 of file transformer.c.
References base_rm, CATCH, constant_constraint_check(), contrainte_succ, CONTRAINTE_UNDEFINED, CONTRAINTE_UNDEFINED_P, contrainte_vecteur, entity_constant_p, entity_local_name(), entity_name, eq, float_analyzed_p(), ifdebug, NO_OFL_CTRL, overflow_error, pips_debug, pips_user_warning, predicate_system, sc_base_remove_variable(), sc_dup(), sc_elim_var(), sc_empty_p(), sc_fprint(), sc_rm(), sc_to_minimal_basis(), string_analyzed_p(), transformer_relation, TRY, UNCATCH, value_full_name(), vecteur_succ, VECTEUR_UNDEFINED, VECTEUR_UNDEFINED_P, and vecteur_var.
Referenced by transformer_empty_p(), and transformer_strongly_empty_p().
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().
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().
Predicate transformer package: sc complexity level.
include "boolean.h" include "vecteur.h" include "contrainte.h" include "sc.h" include "matrix.h"
Definition at line 52 of file transformer.c.
Referenced by transformer_range(), and transformer_to_domain().
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 | ||
) |
e and f are assumed to be values, Type independent.
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().
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().
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_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().
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().
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_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().
|
static |
Allocate a new transformer with constraints in t1 and t2.
If t2 has no arguments, it restrains the domain of t1. This is necessary if image_only is true.
If not, the two transformers are supposed to be two separate abstraction of the same transformation and an intersection of the relation graphs is performed.
no need to duplicate s2, it is done in sc_append. Psysteme s2 = sc_dup((Psysteme) predicate_system(transformer_relation(t2)));
Do not restrict the transition but the image of the relation t1 with constraints in t2.
intersect transition t1 and transition t2
Definition at line 539 of file transformer.c.
References arguments_intersection(), bool_to_string(), dump_transformer, dup_arguments(), ENDP, pips_assert, pips_debug, predicate_system, s1, sc_append(), sc_dup(), transformer_arguments, transformer_empty(), transformer_empty_p(), transformer_identity(), transformer_relation, and transformer_undefined.
Referenced by transformer_image_intersection(), transformer_intersection(), and transformer_safe_general_intersection().
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_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().
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_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 | t, |
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().
|
static |
Allocate a new transformer.
Definition at line 622 of file transformer.c.
References copy_transformer(), transformer_general_intersection(), transformer_undefined, and transformer_undefined_p.
Referenced by transformer_safe_image_intersection(), and transformer_safe_intersection().
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 | tf, |
entity m | __attribute__(unused) | ||
) |
Provide a list of variables that might be forward translated into a stub when preconditions are propagated in callees.
Basically, remove nothing from the transformer base ?
Definition at line 2720 of file transformer.c.
References CONS, ENTITY, entity_initial, gen_in_list_p(), local_temporary_value_entity_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 substitute_stubs_in_transformer().
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_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().
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().
Definition at line 870 of file transformer.c.
References generic_value_name(), s1, and vecteur_var.
Referenced by transformer_normalize().