PIPS
|
#include <stdio.h>
#include "arithmetique.h"
#include "boolean.h"
#include "vecteur.h"
#include "contrainte.h"
#include "sc.h"
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "effects-util.h"
#include "misc.h"
#include "transformer.h"
#include "semantics.h"
Go to the source code of this file.
Functions | |
static bool | parametric_statement_feasible_p (statement s, bool empty_p(transformer)) |
Return true if statement s is reachable according to its precondition. More... | |
bool | statement_weakly_feasible_p (statement s) |
Return false if precondition of statement s is transformer_empty() More... | |
bool | statement_feasible_p (statement s) |
Return true if statement s is reachable according to its precondition. More... | |
bool | statement_strongly_feasible_p (statement s) |
Return true if statement s is reachable according to its precondition. More... | |
bool | empty_range_wrt_precondition_p (range r, transformer p) |
A range cannot be tested exactly wrt a precondition You can try to prove that it is empty or you can try to prove that it is not empty. More... | |
bool | non_empty_range_wrt_precondition_p (range r, transformer p) |
bool | check_range_wrt_precondition (range r, transformer p, bool check_empty) |
FI: this function is outdated because it does not compute the transformers for the range expressions, because it does not take side effects into account and ... More... | |
bool | condition_true_wrt_precondition_p (expression c, transformer p) |
A condition cannot be tested exactly wrt a precondition You can try to prove that it is always true (because it is never false) or you can try to prove that it is always false (because it is never true). More... | |
bool | condition_false_wrt_precondition_p (expression c, transformer p) |
bool | check_condition_wrt_precondition (expression c, transformer pre, bool check_true) |
void | expression_and_precondition_to_integer_interval (expression e, transformer p, int *plb, int *pub) |
Evaluate expression e in context p, assuming that e is an integer expression. More... | |
void | integer_expression_and_precondition_to_integer_interval (expression e, transformer p, int *plb, int *pub) |
Could be used for bool expressions too? Extended to any kind of expression? More... | |
void | integer_value_and_precondition_to_integer_interval (entity v, transformer p, int *plb, int *pub) |
Should be used by previous function, integer_expression_and_precondition_to_integer_interval() More... | |
bool check_condition_wrt_precondition | ( | expression | c, |
transformer | pre, | ||
bool | check_true | ||
) |
Check that is is always false in a store s such that p(s)
pre | re |
check_true | heck_true |
Definition at line 294 of file utils.c.
References bool_to_string(), pips_debug, transformer_add_condition_information(), transformer_dup(), and transformer_empty_p().
Referenced by condition_false_wrt_precondition_p(), and condition_true_wrt_precondition_p().
bool check_range_wrt_precondition | ( | range | r, |
transformer | p, | ||
bool | check_empty | ||
) |
FI: this function is outdated because it does not compute the transformers for the range expressions, because it does not take side effects into account and ...
We might need a range_to_transformer() or loop_range_to_transformer() instead and check that its range is empty.
gather information about the increment sign
Try to prove that no iterations are performed
Without information about the increment sign, you cannot make a decision. Should we accept increments greater or equal to zero? Lesser or equal to zero?
Try to prove that at least one iteration is performed
Without information about the increment sign, you cannot make a decision. Should we accept increments greater or equal to zero? Lesser or equal to zero?
No decision has been made yet
a numerical range may be empty although no information is available
s = sc_strong_normalize4(s, (char * (*)(Variable)) entity_local_name);
= sc_elim_redund(s);
check_empty | heck_empty |
Definition at line 135 of file utils.c.
References bool_to_string(), contrainte_make(), CONTRAINTE_UNDEFINED, debug(), dump_value_name(), entity_local_name(), expression_and_precondition_to_integer_interval(), ifdebug, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, normalized_undefined_p, pips_debug, predicate_system, range_increment, range_lower, range_upper, sc_dup(), sc_fprint(), sc_inequality_add(), sc_make(), sc_rm(), sc_strong_normalize5(), TCST, transformer_relation, transformer_undefined_p, user_error, vect_add_elem(), vect_dup(), and vect_substract().
Referenced by empty_range_wrt_precondition_p(), and non_empty_range_wrt_precondition_p().
bool condition_false_wrt_precondition_p | ( | expression | c, |
transformer | p | ||
) |
Definition at line 285 of file utils.c.
References check_condition_wrt_precondition().
Referenced by old_complete_whileloop_transformer(), and standard_whileloop_to_transformer().
bool condition_true_wrt_precondition_p | ( | expression | c, |
transformer | p | ||
) |
A condition cannot be tested exactly wrt a precondition You can try to prove that it is always true (because it is never false) or you can try to prove that it is always false (because it is never true).
In both case, you may fail and be unable to decide emptiness or non-emptiness.
Definition at line 276 of file utils.c.
References check_condition_wrt_precondition(), and empty.
Referenced by old_complete_whileloop_transformer().
bool empty_range_wrt_precondition_p | ( | range | r, |
transformer | p | ||
) |
A range cannot be tested exactly wrt a precondition You can try to prove that it is empty or you can try to prove that it is not empty.
In both case, you may fail and be unable to decide emptiness or non-emptiness.
Definition at line 112 of file utils.c.
References check_range_wrt_precondition(), and empty.
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
void expression_and_precondition_to_integer_interval | ( | expression | e, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Evaluate expression e in context p, assuming that e is an integer expression.
If p is empty, return an empty interval.
Could be more general, I'm lazy (FI).
precondition p is not feasible
OK, we could do something: add a pseudo-variable equal to expression e and check its min abd max values
we are not handling an affine integer expression
plb | lb |
pub | ub |
Definition at line 325 of file utils.c.
References CONTRAINTE_UNDEFINED, NORMALIZE_EXPRESSION, normalized_linear, normalized_linear_p, predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), TCST, transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, VALUE_ZERO, vect_coeff(), vect_constant_p(), vect_size(), VECTEUR_NUL_P, and vecteur_var.
Referenced by add_index_range_conditions(), add_loop_index_exit_value(), add_loop_skip_condition(), check_range_wrt_precondition(), loop_basic_workchunk_to_workchunk(), loop_bound_evaluation_to_transformer(), and modulo_to_transformer().
void integer_expression_and_precondition_to_integer_interval | ( | expression | e, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Could be used for bool expressions too? Extended to any kind of expression?
p is assumed to be a real precondition, i.e. a transformer_range().
This function is used by semantics as well as exported to other passes. To take care of debug_on()/debug_off(), set and reset_analyzed_types(), a different wrapper is needed.
If expression e is transformer-wise side-effect free (i.e. the ABSTRACT store is not modified)
precondition p is not feasible
plb | lb |
pub | ub |
Definition at line 386 of file utils.c.
References CONTRAINTE_UNDEFINED, debug_off, debug_on, ENDP, expression_to_type(), integer_expression_to_transformer(), make_local_temporary_value_entity(), predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), transformer_arguments, transformer_dup(), transformer_range_intersection(), transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, and VALUE_ZERO.
Referenced by eval_linear_expression(), expression_multiply_sizeof_to_transformer(), generic_abs_to_transformer(), and loop_to_enter_transformer().
void integer_value_and_precondition_to_integer_interval | ( | entity | v, |
transformer | p, | ||
int * | plb, | ||
int * | pub | ||
) |
Should be used by previous function, integer_expression_and_precondition_to_integer_interval()
precondition p is not feasible
plb | lb |
pub | ub |
Definition at line 427 of file utils.c.
References CONTRAINTE_UNDEFINED, predicate_system, sc_dup(), sc_make(), sc_minmax_of_variable(), transformer_relation, transformer_undefined_p, value_max_p, value_min_p, VALUE_TO_INT, and VALUE_ZERO.
Referenced by integer_binary_operation_to_transformer(), and integer_multiply_to_transformer().
bool non_empty_range_wrt_precondition_p | ( | range | r, |
transformer | p | ||
) |
Definition at line 121 of file utils.c.
References check_range_wrt_precondition().
Referenced by complete_loop_transformer(), complete_loop_transformer_list(), loop_to_postcondition(), and loop_to_total_precondition().
Return true if statement s is reachable according to its precondition.
Definition at line 47 of file utils.c.
References debug(), ifdebug, load_statement_precondition(), ORDERING_NUMBER, ORDERING_STATEMENT, statement_number, and statement_ordering.
Referenced by statement_feasible_p(), and statement_strongly_feasible_p().
Return true if statement s is reachable according to its precondition.
Definition at line 92 of file utils.c.
References parametric_statement_feasible_p(), and transformer_empty_p().
Return true if statement s is reachable according to its precondition.
Definition at line 99 of file utils.c.
References parametric_statement_feasible_p(), and transformer_strongly_empty_p().
Referenced by set_methods_for_convex_effects(), and set_methods_for_convex_rw_pointer_effects().
Return false if precondition of statement s is transformer_empty()
utils.c
bool feasible_p = !transformer_empty_p(pre);
FI: this test is much stronger than I intended. I just wanted to check that the predicate of pre was exactly sc_empty()!
Now I'm afraid to change it. suppress_dead_code isn't that slow on ocean. I'm not sure that I could validate Transformations.
Definition at line 72 of file utils.c.
References load_statement_precondition(), predicate_system, sc_empty_p(), and transformer_relation.
Referenced by interprocedural_abc_arrays().