PIPS
|
#include <stdio.h>
#include <string.h>
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "effects-util.h"
#include "control.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "misc.h"
#include "properties.h"
#include "ray_dte.h"
#include "sommet.h"
#include "sg.h"
#include "polyedre.h"
#include "transformer.h"
#include "semantics.h"
Go to the source code of this file.
Macros | |
#define | DEBUG_TEST_TO_TOTAL_PRECONDITION 7 |
Functions | |
transformer | statement_to_total_precondition (transformer, statement) |
semantical analysis More... | |
static transformer | block_to_total_precondition (transformer t_post, list b) |
static transformer | unstructured_to_total_precondition (transformer pre, unstructured u, transformer tf) |
static transformer | test_to_total_precondition (transformer t_post, test t, transformer tf, transformer context) |
static transformer | call_to_total_precondition (transformer t_post, call c, transformer tf) |
static transformer | instruction_to_total_precondition (transformer t_post, instruction i, transformer tf, transformer context) |
#define DEBUG_TEST_TO_TOTAL_PRECONDITION 7 |
|
static |
t_pre is already associated with a statement
Definition at line 95 of file ri_to_total_preconditions.c.
References CAR, ENDP, gen_nreverse(), pips_debug, POP, STATEMENT, statement_to_total_precondition(), transformer_dup(), and transformer_undefined.
Referenced by instruction_to_total_precondition().
|
static |
memory leak
Definition at line 250 of file ri_to_total_preconditions.c.
References call_function, entity_initial, entity_name, is_value_code, is_value_constant, is_value_intrinsic, is_value_symbolic, is_value_unknown, pips_debug, pips_internal_error, transformer_inverse_apply(), transformer_to_domain(), transformer_undefined, and value_tag.
Referenced by instruction_to_total_precondition().
|
static |
never reached: post = pre;
Definition at line 288 of file ri_to_total_preconditions.c.
References block_to_total_precondition(), call_to_total_precondition(), call_undefined, evaluation_before_p, ifdebug, instruction_block, instruction_call, instruction_loop, instruction_tag, instruction_test, instruction_unstructured, instruction_whileloop, is_instruction_block, is_instruction_call, is_instruction_forloop, is_instruction_goto, is_instruction_loop, is_instruction_test, is_instruction_unstructured, is_instruction_whileloop, loop_to_total_precondition(), loop_undefined, pips_debug, pips_internal_error, pips_user_error, print_transformer, test_to_total_precondition(), test_undefined, transformer_undefined, unstructured_to_total_precondition(), whileloop_evaluation, and whileloop_to_total_precondition().
Referenced by statement_to_total_precondition().
transformer statement_to_total_precondition | ( | transformer | t_post, |
statement | s | ||
) |
semantical analysis
phasis 3: propagate total preconditions from statement to sub-statement, starting from the module unique return statement. Total preconditions are over-approximation of the theoretical total preconditions, i.e. the conditions that must be met by the store before a statement is executed to reach the end of the module (intra-procedural) or the end of the program (interprocedural). Since over-approximations are computed, the end of the module or of the program cannot be reached if it is not met.
For (simple) interprocedural analysis, this phasis should be performed top-down on the call tree.
Most functions are called xxx_to_total_precondition. They receive a total postcondition as input and use a transformer to convert it into a total precondition.
Total preconditions are NEVER shared. Sharing would introduce desastrous side effects when they are updated as for equivalenced variables and would make freeing them impossible. Thus on a recursive path from statement_to_total_precondition() to itself the precondition must have been reallocated even when its value is not changed as between a block precondition and the first statement of the block precondition. In the same way statement_to_total_precondition() should never returned a total_precondition aliased with its precondition argument. Somewhere in the recursive call down the data structures towards call_to_total_precondition() some allocation must take place even if the statement as no effect on preconditions.
Ambiguity: the type "transformer" is used to abstract statement effects as well as effects combined from the beginning of the module to just before the current statement (precondition) to just after the current statement (total_precondition). This is because it was not realized that preconditions could advantageously be seen as transformers of the initial state when designing the ri. include <stdlib.h>
Preconditions may be useful to deal with tests and loops and to find out if some control paths do not exist
transformer context = transformer_undefined;
If the code is not reachable, thanks to STOP or GOTO, which is a structural information, the total precondition is just empty.
keep only global initial scalar integer values; else, you might end up giving the same xxx::old name to two different local values (?)
add equivalence equalities
t_pre = transformer_normalize(t_pre, 4);
store the total precondition in the ri
t_post | _post |
Definition at line 355 of file ri_to_total_preconditions.c.
References arguments_difference(), CAR, ENTITY, ENTITY_, entity_to_old_value(), fprintf(), free_transformer(), gen_free_list(), get_module_global_arguments(), ifdebug, instruction_to_total_precondition(), list_undefined, load_statement_precondition(), load_statement_total_precondition(), load_statement_transformer(), MAPL, ORDERING_NUMBER, ORDERING_STATEMENT, pips_assert, pips_debug, pips_internal_error, print_transformer, statement_instruction, statement_number, statement_ordering, statement_reachable_p(), store_statement_total_precondition(), tf_equivalence_equalities_add(), transformer_arguments, transformer_consistency_p(), transformer_empty(), transformer_filter(), transformer_normalize(), transformer_range(), and transformer_undefined.
Referenced by block_to_total_precondition(), loop_to_total_precondition(), module_name_to_total_preconditions(), test_to_total_precondition(), and unstructured_to_total_precondition().
|
static |
t_pret = transformer_normalize(t_pret, 4);
transformer_normalize(t_pref, 4);
Definition at line 198 of file ri_to_total_preconditions.c.
References DEBUG_TEST_TO_TOTAL_PRECONDITION, ifdebug, pips_debug, pips_flag_p, print_transformer, SEMANTICS_FLOW_SENSITIVE, statement_to_total_precondition(), test_condition, test_false, test_true, transformer_add_domain_condition(), transformer_apply(), transformer_convex_hull(), and transformer_normalize().
Referenced by instruction_to_total_precondition().
|
static |
there is only one statement in u; no need for a fix-point
FI: pre should not be duplicated because statement_to_total_precondition() means that pre is not going to be changed, just post produced.
Do not try anything clever! God knows what may happen in unstructured code. Total_Precondition post is not computed recursively from its components but directly derived from u's transformer. Preconditions associated to its components are then computed independently, hence the name unstructured_to_total_preconditionS instead of unstructured_to_total_precondition
propagate as precondition an invariant for the whole unstructured u assuming that all nodes in the CFG are fully connected, unless tf is not feasible because the unstructured is never exited or exited thru a direct or indirect call to STOP which invalidates the previous assumption.
Definition at line 130 of file ri_to_total_preconditions.c.
References control_predecessors, control_statement, control_successors, debug(), ifdebug, invariant_wrt_transformer(), NIL, pips_assert, pips_debug, print_transformer, statement_to_total_precondition(), transformer_apply(), transformer_dup(), transformer_empty_p(), transformer_free(), transformer_undefined, transformer_undefined_p, unstructured_control, unstructured_to_flow_insensitive_transformer(), unstructured_to_flow_sensitive_total_preconditions(), and unstructured_undefined.
Referenced by instruction_to_total_precondition().