PIPS
|
#include <stdio.h>
#include <string.h>
#include "genC.h"
#include "database.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "text.h"
#include "text-util.h"
#include "ri-util.h"
#include "effects-util.h"
#include "constants.h"
#include "control.h"
#include "effects-generic.h"
#include "effects-simple.h"
#include "misc.h"
#include "properties.h"
#include "vecteur.h"
#include "contrainte.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.
Data Structures | |
struct | recursive_context |
Functions | |
static void | print_control_node_uns (control c) |
semantical analysis More... | |
static void | print_control_node_unss_sem (list l) |
static transformer | load_control_postcondition (control c, control_mapping control_postcondition_map) |
static transformer | load_arc_precondition (control, control, control_mapping) |
forward declaration More... | |
static transformer | get_control_precondition (control c, control_mapping control_postcondition_map, unstructured u, transformer pre_entry) |
static void | store_control_postcondition (control c, transformer post, control_mapping control_postcondition_map) |
static void | update_control_postcondition (control c, transformer post, control_mapping control_postcondition_map) |
void | print_control_postcondition_map (control_mapping control_postcondition_map) |
unstructured.c More... | |
static control_mapping | make_control_postcondition_map () |
static control_mapping | free_control_postcondition_map (control_mapping control_postcondition_map) |
static transformer | load_control_fix_point (control c, control_mapping control_fix_point_map, hash_table ancestor_map, hash_table scc_map) |
The fix point can be linked either to the entry node of the scc or to the ancestor node. More... | |
static void | store_control_fix_point (control c, transformer fptf, control_mapping control_fix_point_map) |
static control_mapping | make_control_fix_point_map () |
static control_mapping | free_control_fix_point_map (control_mapping control_fix_point_map) |
static bool | ready_to_be_processed_p (control c, list to_be_processed, list still_to_be_processed, list already_processed, control_mapping control_postcondition_map) |
a control is ready to be processed if all its predecessors have known postconditions or can receive a trivial empty postcondition More... | |
transformer | load_cycle_fix_point (control c, hash_table fix_point_map) |
static list | unstructured_to_effects (unstructured scc, hash_table ancestor_map, hash_table scc_map) |
In fact, non-deterministic unstructured to effects. More... | |
static list | non_deterministic_unstructured_to_effects (unstructured scc, hash_table ancestor_map, hash_table scc_map) |
static void | process_ready_node (control c, transformer pre_entry, transformer n_pre, unstructured u, control_mapping control_postcondition_map, hash_table ancestor_map, hash_table scc_map, list partition, control_mapping fix_point_map, bool postcondition_p) |
static bool | process_unreachable_node (control c, control_mapping control_postcondition_map, bool postcondition_p) |
static void | add_cycle_dependency (control d, control c, control_mapping cycle_dependencies_map) |
State that d depends on c: cycle c must be processed before cycle d can be processed. More... | |
static void | remove_cycle_dependencies (control c, control_mapping cycle_dependencies_map) |
c has been processed and no other cycle can depend on it More... | |
static list | get_cycle_dependencies (control d, control_mapping cycle_dependencies_map) |
Some cycle may appear nowhere but in the DAG and have no entries in the table. More... | |
void | update_temporary_precondition (void *k, transformer pre, hash_table precondition_map) |
void | update_statement_temporary_precondition (statement s, transformer pre, statement_mapping statement_temporary_precondition_map) |
void | print_statement_temporary_precondition (statement_mapping statement_temporary_precondition_map) |
void | update_cycle_temporary_precondition (control c, transformer pre, control_mapping cycle_temporary_precondition_map) |
transformer | load_cycle_temporary_precondition (control c, control_mapping cycle_temporary_precondition_map, hash_table ancestor_map, hash_table scc_map __attribute__((__unused__))) |
transformer | load_statement_temporary_precondition (statement s, statement_mapping statement_temporary_precondition_map) |
static void | cycle_to_flow_sensitive_preconditions (list partition, unstructured c_u, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, control_mapping cycle_temporary_precondition_map, statement_mapping statement_temporary_precondition_map, transformer c_pre, transformer pre, control_mapping control_postcondition_map) |
Very likely the transformer paths wrt the entry point and not really a postcondition. More... | |
static void | dag_to_flow_sensitive_preconditions (list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer pre_u, transformer pre, control_mapping control_postcondition_map) |
transformer | dag_or_cycle_to_flow_sensitive_postconditions_or_transformers (list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p, bool is_dag) |
Should ndu be a dag or a cycle? More... | |
transformer | dag_to_flow_sensitive_postconditions_or_transformers (list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p) |
Compute transformers or preconditions. More... | |
transformer | cycle_to_flow_sensitive_postconditions_or_transformers (list partition, unstructured ndu, hash_table ancestor_map, hash_table scc_map, control_mapping fix_point_map, transformer e_pre, transformer n_pre, hash_table control_postcondition_map, bool postcondition_p) |
Compute transformers or preconditions. More... | |
static void | local_process_unreachable_node (control c, recursive_context *pcontext) |
static void | node_to_path_transformer_or_postcondition (control c, recursive_context *pcontext) |
A debug function to prettyprint the result. More... | |
static void | print_cycle_head_to_fixpoint (control c, recursive_context *pcontext) |
A debug function to prettyprint the fix points. More... | |
transformer | unstructured_to_flow_sensitive_postconditions_or_transformers (transformer pre_u, transformer pre, unstructured u, bool postcondition_p) |
compute either the postconditions in an unstructured or the transformer of this unstructured. More... | |
static transformer | unstructured_to_postconditions (transformer pre, transformer pre_first, unstructured u) |
transformer | unstructured_to_flow_sensitive_postconditions (transformer pre_u, transformer pre, unstructured u) |
compute pre- and post-conditions in an unstructured from the entry precondition pre and return the exit postcondition. More... | |
transformer | unstructured_to_postcondition (transformer pre, unstructured u, transformer tf) |
static void | unreachable_node_to_transformer (control c) |
transformer | unstructured_to_flow_insensitive_transformer (unstructured u) |
This simple fix-point over-approximates the CFG by a fully connected graph. More... | |
static void | unstructured_to_transformers (unstructured u, transformer pre) |
Computation of transformers associated to each node of u and to each of its sub-statements. More... | |
transformer | unstructured_to_transformer (unstructured u, transformer e_pre, list e) |
effects of u More... | |
transformer | unstructured_to_flow_sensitive_total_preconditions (transformer t_post_u, transformer pre, unstructured u) |
|
static |
State that d depends on c: cycle c must be processed before cycle d can be processed.
Update the hash_table by side effect
Definition at line 934 of file unstructured.c.
References CONS, CONTROL, gen_nconc(), hash_get(), hash_put(), HASH_UNDEFINED_VALUE, and NIL.
Referenced by dag_to_flow_sensitive_preconditions().
transformer cycle_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p | ||
) |
Compute transformers or preconditions.
partition | artition |
ndu | Bourdoncle's processing ordering |
ancestor_map | A non-deterministic acyclic control flow graph |
scc_map | Mapping from non-deterministic nodes to deterministic nodes |
fix_point_map | mapping from deterministic nodes to non-deterministic cycles |
e_pre | mapping from cycle heads to fix point transformers |
n_pre | precondition on entry |
control_postcondition_map | precondition true for any node. |
postcondition_p | ostcondition_p |
Definition at line 1744 of file unstructured.c.
References dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), and transformer_undefined.
Referenced by process_ready_node().
|
static |
Very likely the transformer paths wrt the entry point and not really a postcondition.
Let's update it as a real postcondition.
Yet another forward DAG propagation with an exception for the cycle head: cut-and-paste and adapt
forward reachable nodes in u
FI: Please the compiler complaining about useless parameters (and remove them later!)
wide_forward_control_map_get_blocs(unstructured_control(u), &to_be_processed);
Take care of the entry node whose precondition does not rely on its predecessors
post = statement_to_postcondition(c_pre, es);
c_pre is USED
Propagate the postcondition downwards
process forward
right away because c's cdr might be modified
Already done earlier if(cycle_head_p(c, ancestor_map, scc_map)) { transformer fp_tf = load_control_fix_point(a, fix_point_map, ancestor_map, scc_map); e_pre = transformer_apply(fp_tf, pre); update_cycle_temporary_precondition (a, e_pre, cycle_temporary_precondition_map); } else { e_pre = transformer_dup(pre); }
fix point are unique for all replication of a cycle
(a, e_pre, cycle_temporary_precondition_map);
Go down the subcycle... when necessary... since there is a loop somewhere else and the cycles are called in the right order?
post = statement_to_postcondition(transformer_dup(e_pre), c_s);
FI: you should use the really current precondition using load_statement_temporary_precondition()
post = transformer_apply(load_statement_transformer(c_s), e_pre);
Hard to track memory leaks...
It is much too late to update the control postcondition!
update_control_postcondition(c, post, control_postcondition_map);
FI: just to see what happens, without any understanding of the process
FI: what is the point when control are replicated?
The precondition for the entry node may be improved by now using the precondition of its predecessors and the cycle entry. OK, but to what end?
c_u | Is it relevant? |
ancestor_map | The cycle unstructured |
statement_temporary_precondition_map | To be updated when a cycle head is encountered |
c_pre | To be updated each time a statement is encountered |
pre | precondition of cycle c_u, already processed with the fix point |
control_postcondition_map | aproximate precondition holding for all nodes |
Definition at line 1080 of file unstructured.c.
References ancestor_cycle_head_to_scc(), CAR, CONS, CONTROL, control_statement, control_to_ancestor(), control_undefined, count, cycle_head_p(), ENDP, forward_control_map_get_blocs(), free_transformer(), gen_append(), gen_copy_seq(), gen_remove(), get_bool_property(), get_control_precondition(), ifdebug, list_undefined, load_control_fix_point(), load_statement_temporary_precondition(), load_statement_transformer(), meaningless_control_p(), NIL, pips_assert, pips_debug, POP, print_control_node_unss_sem(), ready_to_be_processed_p(), transformer_apply(), transformer_dup(), transformer_undefined, unstructured_control, unstructured_undefined, update_control_postcondition(), update_cycle_temporary_precondition(), and update_statement_temporary_precondition().
Referenced by dag_to_flow_sensitive_preconditions().
transformer dag_or_cycle_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p, | ||
bool | is_dag | ||
) |
Should ndu be a dag or a cycle?
forward reachable nodes in u
The whole business could be simplified by using a larger definition of "to_be_processed".
wide_forward_control_map_get_blocs(unstructured_control(u), &to_be_processed);
Take care of unreachable nodes
FI: Wouldn't it be better to clean up the unstructured? Aren't they supposed to be clean? This piece of code contradict get_control_precondition() where the problem could be fixed at a lower cost. Another place where the problem is handled is ready_to_be_processed_p(), but it is called on still_to_be_processed, which does not take into account unreachable nodes. To make things worse, the daVinci printouts only include, most of the time, only reachable nodes.
Take care of the entry node
The entry node must be handled in a specific way... but not in the specific way implemented in process_ready_node() which only deals with DAG's. The entry node cannot be a meaningless control node.
Since control nodes have been replicated, it is difficult to predict if es has already been processed or not.
make_control_postcondition_map();
Take care of the forward reachable control nodes
process forward
right away because c's cdr might be modified
Compute fix point transformer for cycle
Compute the convex hull of the paths associated to each predecessor of the entry. Since this is a cycle, preds cannot be empty.
transformer fp_tf_plus = transformer_undefined;
If an entry range is known, do not use it as there may be more than one occurence of the cycle and more than one entry range. Keep this refinement to the precondition computation phase? It might be too late. The the data structure should be change to store more than one fix point per cycle.
Not convincing anyway: you should apply fp_tf_plus to e_pre for the next two lines to make sense.
Use the + fix point to preserve more information about the output and do not forget to perform a convex hull when you need a * fix point in process_ready_node()
Instead of computing the convex hull over all paths before computing the fix point, compute the fix point of a list of transformers.
e may have many synonyms
fix point are unique for all replication of a cycle
each cycle replication has its own fix-point
We might want to return the corresponding fix point?
partition | artition |
ndu | Bourdoncle's processing ordering |
ancestor_map | A non-deterministic acyclic control flow graph |
scc_map | Mapping from non-deterministic nodes to deterministic nodes |
fix_point_map | mapping from deterministic nodes to non-deterministic cycles |
e_pre | mapping from cycle heads to fix point transformers |
n_pre | precondition on entry |
control_postcondition_map | precondition true for any node. |
postcondition_p | ostcondition_p |
is_dag | Compute transformers or preconditions |
Definition at line 1509 of file unstructured.c.
References CAR, CONS, CONTROL, control_map_get_blocs(), control_predecessors, control_statement, control_to_ancestor(), control_undefined, count, ENDP, FOREACH, forward_control_map_get_blocs(), free_transformer(), gen_append(), gen_copy_seq(), gen_free_list(), gen_list_and_not(), gen_remove(), get_bool_property(), ifdebug, init, list_undefined, list_undefined_p, load_arc_precondition(), load_statement_transformer(), MAP, meaningless_control_p(), NIL, pips_assert, pips_debug, POP, print_control_node_unss_sem(), print_transformer, process_ready_node(), ready_to_be_processed_p(), statement_identification(), statement_to_transformer(), store_control_fix_point(), store_control_postcondition(), TRANSFORMER, transformer_apply(), transformer_combine(), transformer_convex_hull(), transformer_empty(), transformer_identity(), transformer_list_transitive_closure_plus(), transformer_undefined, transformer_undefined_p, and unstructured_control.
Referenced by cycle_to_flow_sensitive_postconditions_or_transformers(), and dag_to_flow_sensitive_postconditions_or_transformers().
transformer dag_to_flow_sensitive_postconditions_or_transformers | ( | list | partition, |
unstructured | ndu, | ||
hash_table | ancestor_map, | ||
hash_table | scc_map, | ||
control_mapping | fix_point_map, | ||
transformer | e_pre, | ||
transformer | n_pre, | ||
hash_table | control_postcondition_map, | ||
bool | postcondition_p | ||
) |
Compute transformers or preconditions.
partition | artition |
ndu | Bourdoncle's processing ordering |
ancestor_map | A non-deterministic acyclic control flow graph |
scc_map | Mapping from non-deterministic nodes to deterministic nodes |
fix_point_map | mapping from deterministic nodes to non-deterministic cycles |
e_pre | mapping from cycle heads to fix point transformers |
n_pre | precondition on entry |
control_postcondition_map | precondition true for any node. |
postcondition_p | ostcondition_p |
Definition at line 1724 of file unstructured.c.
References dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), and transformer_undefined.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
A statement may appear in several nodes, and the same is true for cycles.
DUPLICATED CODE
The cycle is entered
Or the cycle is not entered and the store is not in fptf's domain.
Have we followed a true or a false branch? We'll know later but it is better to add this information before the convex hull is performed.
FI: I do not know why an empty context is passed down.
free_transformer(pre);
END OF DUPLICATED CODE
e_pre = transformer_apply(fp_tf, pre);
fix point are unique for all replication of a cycle
update_cycle_temporary_precondition(a, e_pre, cycle_temporary_precondition_map);
FI: sharing between statement_temporary_precondition and statement_temporary_precondition; freeing the second one frees part of the first one
Build the cycle dependencies
control a = control_to_ancestor(c, ancestor_map);
unstructured scc_ u = cycle_head_to_scc(c, ancestor_map, scc_map);
build dependencies among ancestors, which are representative of scc's
then cc depends on c
build dependencies among heads, which are representative of scc's
No cycles with dependencies
While some cycles still have to be processed.
right away because c's cdr might be modified
The precondition of cycle c is complete
control a = control_to_ancestor(c, ancestor_map);
Definition at line 1234 of file unstructured.c.
References add_cycle_dependency(), ancestor_cycle_head_to_scc(), CAR, CONS, CONTROL, control_map_get_blocs(), control_statement, control_test_p(), control_to_ancestor(), control_undefined, count, cycle_head_p(), cycle_head_to_scc(), cycle_to_flow_sensitive_preconditions(), ENDP, false_successors_only_p(), free_transformer(), gen_append(), gen_free_list(), gen_remove(), get_bool_property(), get_control_precondition(), get_cycle_dependencies(), HASH_MAP, hash_table_entry_count(), ifdebug, list_undefined, load_control_fix_point(), load_cycle_temporary_precondition(), MAKE_CONTROL_MAPPING, MAKE_STATEMENT_MAPPING, meaningless_control_p(), NIL, pips_assert, pips_debug, POP, precondition_add_condition_information(), print_control_node_unss_sem(), print_control_postcondition_map(), print_statement_temporary_precondition(), proper_cycle_head_to_scc(), remove_cycle_dependencies(), statement_identification(), statement_test(), statement_to_postcondition(), test_condition, transformer_apply(), transformer_convex_hull(), transformer_dup(), transformer_undefined, true_successors_only_p(), unstructured_control, unstructured_undefined, update_cycle_temporary_precondition(), and update_statement_temporary_precondition().
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
all fix_points must be freed
return control_mapping_undefined;
Definition at line 412 of file unstructured.c.
References FREE_CONTROL_MAPPING, free_transformer(), and HASH_MAP.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
all postconditions must be freed
return control_mapping_undefined;
Definition at line 318 of file unstructured.c.
References FREE_CONTROL_MAPPING, free_transformer(), and HASH_MAP.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
Compute its precondition from the postconditions of its predecessor and from the entry precondition. Use arc pred->c information to deal with tests.
Do not forget the unstructured precondition for the entry node
FI: I do not know why it has to be replicated. Probably because the statement containing the unstructured and the statement of the entry node may share the same precondition.
This is not the entry node: without predecessors, it is unreachable
memory leak with lpre. pre_entry and postconditions cannot be freed: lpre cannot be freed during the first iteration
Definition at line 185 of file unstructured.c.
References CAR, CONTROL, control_predecessors, control_statement, copy_transformer(), ENDP, FOREACH, free_transformer(), ifdebug, load_arc_precondition(), meaningless_control_p(), pips_assert, pips_debug, POP, print_transformer, statement_identification(), transformer_convex_hull(), transformer_empty(), transformer_undefined, transformer_undefined_p, and unstructured_control.
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_to_flow_sensitive_preconditions().
|
static |
Some cycle may appear nowhere but in the DAG and have no entries in the table.
In that case, they have an empty dependency list.
Definition at line 963 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, and NIL.
Referenced by dag_to_flow_sensitive_preconditions().
|
static |
forward declaration
Returns the precondition of c associated to arc pred->c in a newly allocated transformer.
pred must be unreachable, left over by the controlizer...
It would be nice to be able to check that it is unreachable... and that we do not land here because of a bug...
This should never happen.
let's assume that Bourdoncle's restructuring does not clutter the successor list too much.
Assume that the same node is in the true and false successor lists.
Do not bother with the test condition... and FI loose the side effects.
If side effects can be detected, perform a convex hull of the true and false branches as nothing else is available.
add the test condition
One of the true successors
One of the false successors
Definition at line 468 of file unstructured.c.
References control_statement, control_successors, control_test_p(), gen_occurences(), gen_position(), ifdebug, load_control_postcondition(), pips_assert, pips_debug, precondition_add_condition_information(), print_transformer, statement_test(), statement_test_p(), test_condition, transformer_dup(), transformer_empty(), transformer_undefined, and transformer_undefined_p.
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), get_control_precondition(), and process_ready_node().
|
static |
The fix point can be linked either to the entry node of the scc or to the ancestor node.
The ancestor node is used by default, when transformer are not computed in context. So the argument is either the ancestor node (transformer out of context), or the call node (transformers computed in context) or the entry node (preconditions computed with transformers in context).
It is assumed that cycle_head_p(c) holds, but it is not assumed that its fixpoint is available..
Definition at line 342 of file unstructured.c.
References ancestor_cycle_head_to_scc(), control_to_ancestor(), control_undefined, control_undefined_p, get_bool_property(), hash_get(), HASH_UNDEFINED_VALUE, ifdebug, pips_assert, pips_debug, transformer_undefined, unstructured_control, and unstructured_undefined_p.
Referenced by cycle_to_flow_sensitive_preconditions(), dag_to_flow_sensitive_preconditions(), and process_ready_node().
|
static |
Definition at line 169 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, and transformer_undefined.
Referenced by load_arc_precondition(), node_to_path_transformer_or_postcondition(), print_cycle_head_to_fixpoint(), process_unreachable_node(), ready_to_be_processed_p(), and unstructured_to_flow_sensitive_postconditions_or_transformers().
transformer load_cycle_fix_point | ( | control | c, |
hash_table | fix_point_map | ||
) |
fix_point_map | ix_point_map |
Definition at line 544 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, pips_assert, and transformer_undefined.
transformer load_cycle_temporary_precondition | ( | control | c, |
control_mapping | cycle_temporary_precondition_map, | ||
hash_table | ancestor_map, | ||
hash_table scc_map | __attribute__(__unused__) | ||
) |
Definition at line 1037 of file unstructured.c.
References control_to_ancestor(), control_undefined, get_bool_property(), hash_get(), HASH_UNDEFINED_VALUE, ifdebug, pips_assert, pips_debug, print_transformer, and transformer_undefined.
Referenced by dag_to_flow_sensitive_preconditions().
transformer load_statement_temporary_precondition | ( | statement | s, |
statement_mapping | statement_temporary_precondition_map | ||
) |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 1069 of file unstructured.c.
References hash_get(), HASH_UNDEFINED_VALUE, and pips_assert.
Referenced by cycle_to_flow_sensitive_preconditions().
|
static |
Definition at line 1781 of file unstructured.c.
References recursive_context::pcond, process_unreachable_node(), and recursive_context::smap.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
Definition at line 405 of file unstructured.c.
References MAKE_CONTROL_MAPPING.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
Definition at line 311 of file unstructured.c.
References MAKE_CONTROL_MAPPING.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
A debug function to prettyprint the result.
Definition at line 1787 of file unstructured.c.
References control_statement, fprintf(), load_control_postcondition(), meaningless_control_p(), pips_assert, print_transformer, recursive_context::smap, statement_identification(), transformer_consistency_p(), and transformer_undefined_p.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
entry point
Definition at line 603 of file unstructured.c.
References ifdebug, pips_debug, print_effects, unstructured_control, and unstructured_to_effects().
Referenced by process_ready_node().
|
static |
semantical analysis
Computation of transformers and postconditions and total preconditions in unstructured (i.e. CFG).
Accurate results are obtained by restructuring CFG into a set of non-deterministic CFG's using Bourdoncle's partitioning as implemented in control/bourdoncle.c. The cycle heads are chosen using Bourdoncle's heuristics. Then the graph is augmented with new nodes in order that cycle heads are the only entry and exit node of the cycles in each scc. So the input CFG is transformed into a non-deterministic DAG. Some nodes of the DAG point to SCC's. Each SCC is represented by a DAG whose leaves point back to the cycle head. The SCC DAG may contain nodes pointing to sub-SCC's.
It is not clear if you want to store the node pre or postcondition. The postcondition may depend on the outgoing arc. But the precondition would have to be processed by the node transformer once for each arc. To avoid both problems the postconditions are stored without the control information. It is added later according to the outgoing arc considered. But it is not satisfactory to apply a reverse transformer to retrieve the precondition or to re-apply a convex hull on the input after having taken care of the potential cycle. All in all, it would be easier to store preconditions...
Transformers between the entry point and after the current node are very similar to postcondition between the module entry point and the current node. Transformers are obtained like precondition but without a precondition at the CFG entry point.
It is possible to store the star or the plus fix points. I first stored the star fix points. It is often needed. It is safe because it can be applied several times without impacting the result. However, it does not retain information about the cycle body transformer. Because the convex hull operator looses information, it is more accurate to use the plus fix point and to apply a convex hull to the direct precondition and to the cycle output. Thus, if the entry node is a test, its conditions can be added before the convex hull is performed.
It might be useful to add a pseudo-node as predecessor of the CFG entry node. This pseudo-node would simplify the algorithms and the function profiles. Its post-condition would be the precondition of the CFG or no information. Without it, each node must be checked to see if it is the entry node because, then, it has an extra-predecessor.
Francois Irigoin, July 2002 (First version: October 2000)
Note: Bourdoncle's heuristics minimizes the number of cycles under the assumption that most information is lost when performing a widening. We do not use widening but direct computation of an upper approximation of the transition closure. And sometimes, a lot of information is lost when performing convex hulls of transformers. So, using transformers, it would be better to maximize the number of cycles to minimize the number of paths in each cycle. include <stdlib.h>
Definition at line 122 of file unstructured.c.
References CONTROL, control_predecessors, control_statement, control_successors, fprintf(), gen_length(), MAP, and safe_statement_identification().
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
|
static |
Definition at line 143 of file unstructured.c.
References CONTROL, control_statement, ENDP, fprintf(), MAP, and safe_statement_identification().
Referenced by cycle_to_flow_sensitive_preconditions(), dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), and dag_to_flow_sensitive_preconditions().
void print_control_postcondition_map | ( | control_mapping | control_postcondition_map | ) |
unstructured.c
control_postcondition_map | ontrol_postcondition_map |
Definition at line 294 of file unstructured.c.
References control_statement, fprintf(), HASH_MAP, hash_table_entry_count(), pips_assert, print_transformer, and statement_identification().
Referenced by dag_to_flow_sensitive_preconditions().
|
static |
A debug function to prettyprint the fix points.
Most control nodes are not associated to a fix point
Definition at line 1803 of file unstructured.c.
References control_statement, fprintf(), load_control_postcondition(), pips_assert, print_transformer, recursive_context::smap, statement_identification(), transformer_consistency_p(), and transformer_undefined_p.
Referenced by unstructured_to_flow_sensitive_postconditions_or_transformers().
void print_statement_temporary_precondition | ( | statement_mapping | statement_temporary_precondition_map | ) |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 1006 of file unstructured.c.
References fprintf(), HASH_MAP, hash_table_entry_count(), pips_assert, print_transformer, and statement_identification().
Referenced by dag_to_flow_sensitive_preconditions().
|
static |
Compute its precondition pre from the postconditions of its predecessor and from the entry precondition. Use arc pred->c information to deal with tests.
Do not forget the unstructured precondition for the entry node
FI: I do not know why it has to be replicated. Probably because the statement containing the unstructured and the statement of the entry node may share the same precondition.
memory leak with lpre. pre_entry and postconditions cannot be freed: lpre cannot be freed during the first iteration
if(pred!=CONTROL(CAR(preds))) free_transformer(lpre);
Add the information from the current precondition.
If the control is a cycle head, find and apply its fix point tranformer to the precondition before proceeding into the node itself
unstructured_to_flow_insensitive_transformer(scc_u) cannot be used because it assumes that all transformers for statements in scc_u are defined, which is not true yet.
transformer tf_u = unstructured_to_flow_insensitive_transformer(scc_u);
n_pre_u is assumed more accurate than n_pre
Bourdoncle's processing ordering
A non-deterministic acyclic control flow graph
Mapping from non-deterministic nodes to deterministic nodes
mapping from deterministic nodes to non-deterministic cycles
precondition on entry
precondition true for any node of scc_u.
Compute transformers
The cycle is entered
Or the cycle is not entered and the store is not in fptf's domain.
Have we followed a true or a false branch? We'll know later but it is better to add this information before the convex hull is performed.
FI: I do not know why an empty context is passed down.
Propagate the precondition thru the node to obtain a postcondition which does not include arc information (FI: hard if side-effects?)
FI: The transformer might have to be recomputed before the call if the option is selected? It does not seem to be located in statement_to_postcondition()
FI: is this correct when the statement is a test since the node only exploits the condition? It might be because of the convex hull nullifying the condition and hence the arc information.
FI: statement_to_postcondition() cannot always be used because the statement may appear in different non-deterministic nodes; pre is only of of the many preconditions that can hold before stmt is executed; statement_to_postcondition() should be called later when the whole unstructured has been analyzed.
post = statement_to_postcondition(pre, stmt);
The statement transformer may have been computed earlier thru a fix point calculation, but the transformer may not be correct if it were computed in context (property SEMANTICS_COMPUTE_TRANSFORMERS_IN_CONTEXT true).
We are in trouble: the transformer attached to a statement should be the convex hull of its transformers computed in all its context. Our options:
Let's live very dangerously and try 1...
Definition at line 630 of file unstructured.c.
References CAR, CONTROL, control_predecessors, control_statement, control_test_p(), copy_transformer(), cycle_head_p(), cycle_head_to_scc(), cycle_to_flow_sensitive_postconditions_or_transformers(), effects_to_transformer(), false_successors_only_p(), free_transformer(), gen_free_list(), get_bool_property(), ifdebug, invariant_wrt_transformer(), load_arc_precondition(), load_control_fix_point(), load_statement_precondition(), load_statement_transformer(), MAP, meaningless_control_p(), non_deterministic_unstructured_to_effects(), pips_assert, pips_debug, POP, precondition_add_condition_information(), print_transformer, refine_transformers_p, statement_identification(), statement_test(), statement_to_transformer(), store_control_postcondition(), test_condition, transformer_apply(), transformer_convex_hull(), transformer_dup(), transformer_range(), transformer_range_intersection(), transformer_undefined, transformer_undefined_p, true_successors_only_p(), and unstructured_control.
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().
|
static |
Careful, this may have been done earlier by the CONTROL_MAP in unstructured_to_transformers()
FI: We should use the generic node precondition n_pre; it should be an additional component in the context.
Problem with ELSIP in ARC2D after partial redundancy elimination
pips_internal_error(statement_identification(s));
Problem with SHALLOW in SWIM
Definition at line 862 of file unstructured.c.
References control_statement, load_control_postcondition(), load_statement_precondition(), load_statement_transformer(), meaningless_control_p(), pips_assert, pips_debug, pips_internal_error, safe_statement_identification(), semantics_user_warning, statement_identification(), statement_ordering, STATEMENT_ORDERING_UNDEFINED, statement_to_postcondition(), statement_to_transformer(), store_control_postcondition(), transformer_empty(), transformer_empty_p(), transformer_undefined, and transformer_undefined_p.
Referenced by local_process_unreachable_node().
|
static |
a control is ready to be processed if all its predecessors have known postconditions or can receive a trivial empty postcondition
useless, except for debugging
postcondition must be empty because pred is not reachable
transformer pre = transformer_empty();
transformer post = statement_to_postcondition(pre, stmt);
Definition at line 427 of file unstructured.c.
References CONTROL, control_predecessors, control_statement, gen_in_list_p(), load_control_postcondition(), MAP, pips_assert, pips_internal_error, statement_identification(), store_control_postcondition(), transformer_empty(), transformer_empty_p(), and transformer_undefined_p.
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().
|
static |
c has been processed and no other cycle can depend on it
Oops... gen_remove() might change the pointer
Definition at line 951 of file unstructured.c.
References gen_remove(), HASH_MAP, and hash_update().
Referenced by dag_to_flow_sensitive_preconditions().
|
static |
Definition at line 382 of file unstructured.c.
References control_statement, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, ifdebug, meaningless_control_p(), pips_assert, pips_debug, print_transformer, statement_identification(), statement_undefined_p, and transformer_consistency_p().
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers().
|
static |
Definition at line 245 of file unstructured.c.
References control_statement, hash_get(), hash_put(), HASH_UNDEFINED_VALUE, ifdebug, meaningless_control_p(), pips_assert, pips_debug, print_transformer, statement_identification(), statement_undefined_p, and transformer_consistency_p().
Referenced by dag_or_cycle_to_flow_sensitive_postconditions_or_transformers(), process_ready_node(), process_unreachable_node(), and ready_to_be_processed_p().
|
static |
Definition at line 2158 of file unstructured.c.
References control_statement, load_statement_transformer(), pips_debug, semantics_user_warning, statement_identification(), statement_ordering, STATEMENT_ORDERING_UNDEFINED, statement_to_transformer(), transformer_undefined, and transformer_undefined_p.
Referenced by unstructured_to_transformer().
|
static |
In fact, non-deterministic unstructured to effects.
entry point
Definition at line 556 of file unstructured.c.
References control_statement, cycle_head_p(), cycle_head_to_scc(), effects_same_action_p(), EffectsMayUnion(), FORWARD_CONTROL_MAP, gen_free_list(), gen_full_copy_list(), ifdebug, list_undefined, load_cumulated_rw_effects_list(), meaningless_control_p(), NIL, pips_debug, print_effects, and unstructured_control.
Referenced by non_deterministic_unstructured_to_effects().
transformer unstructured_to_flow_insensitive_transformer | ( | unstructured | u | ) |
This simple fix-point over-approximates the CFG by a fully connected graph.
Each vertex can be executed at any time any number of times.
The fix point is easy to compute because it is the fix point of the convex hull all each node transformers.
The result is sometimes surprising as users see the real paths and cannot understand why a variable is declared modified when it obviously is not. This mostly choses in node preconditions since the overall unstructured transformer is not displayed usually and since it is globally correct.
But it is a perfectly valid over-approximation usable by automatic analyses.
Using the effects of the unstructured to derive a fix point leads to the same surprise although it is as correct, using the same over approximation of the control flow graph but a cruder version of the transformers.
This function is also used when computing preconditions if the exit node is not reached (?). It assumes that transformers for all statements in the unstructured have already been computed.
Two modes are possible: the transitive closure of the convex hull of all elementary transformers, or the transitive closure of the transformer list.
Assume any reachable node is executed at each iteration. A fix-point of the result can be used to approximate the node preconditions. Some nodes can be discarded because they do not modify the store such as IF statements (always) and CONTINUE statements (if they do not link the entry and the exit nodes).
Entry node
transformer_convex_hull has side effects on its arguments:-(
Should be fixed now, 29 June 2000
transformer tf_st = copy_transformer(load_statement_transformer(st));
Any side effect?
test
continue
other
Definition at line 2206 of file unstructured.c.
References chunk_undefined, CONS, continue_statement_p(), control_predecessors, control_statement, control_successors, ENDP, FORWARD_CONTROL_MAP, free_transformer(), gen_find_eq(), gen_free_list(), get_bool_property(), ifdebug, load_statement_transformer(), NIL, pips_assert, pips_debug, print_transformer, statement_test_p(), TRANSFORMER, transformer_arguments, transformer_convex_hull(), transformer_empty(), transformer_internal_consistency_p(), transformer_list_transitive_closure(), transformer_undefined, unstructured_control, and unstructured_exit.
Referenced by unstructured_to_postcondition(), unstructured_to_total_precondition(), and unstructured_to_transformer().
transformer unstructured_to_flow_sensitive_postconditions | ( | transformer | pre_u, |
transformer | pre, | ||
unstructured | u | ||
) |
compute pre- and post-conditions in an unstructured from the entry precondition pre and return the exit postcondition.
pre_u is pre filtered by the u's transformer and can be used for any node.
control tail = unstructured_exit(u);
pre_u | re_u |
pre | re |
Definition at line 2040 of file unstructured.c.
References forward_control_map_get_blocs(), gen_free_list(), gen_length(), get_bool_property(), get_int_property(), NIL, pips_assert, semantics_user_warning, transformer_consistency_p(), transformer_undefined, unstructured_control, unstructured_to_flow_sensitive_postconditions_or_transformers(), and unstructured_to_postconditions().
Referenced by unstructured_to_postcondition().
transformer unstructured_to_flow_sensitive_postconditions_or_transformers | ( | transformer | pre_u, |
transformer | pre, | ||
unstructured | u, | ||
bool | postcondition_p | ||
) |
compute either the postconditions in an unstructured or the transformer of this unstructured.
In both cases, transformers for all nodes used to be supposed to be available.
Do not go down into nested unstructured
Propagate the precondition in the DAG and recompute the cycle transformers or compute the path transformers and the cycle fix point transformers.
Compute the real precondition for each statement and propagate postconditions in it.
Take care of unreachable nodes
Get rid of the auxiliary data structures
pre_u | re_u |
pre | precondition at entry: e_pre |
u | precondition true for every node: n_pre |
postcondition_p | ostcondition_p |
Definition at line 1821 of file unstructured.c.
References bourdoncle_free(), bourdoncle_partition(), control_domain, control_statement, copy_transformer(), dag_to_flow_sensitive_postconditions_or_transformers(), dag_to_flow_sensitive_preconditions(), fprintf(), free_control_fix_point_map(), free_control_postcondition_map(), gen_context_multi_recurse(), gen_false(), gen_multi_recurse(), gen_null(), gen_true(), HASH_MAP, hash_table_entry_count(), hash_table_undefined, ifdebug, load_control_postcondition(), local_process_unreachable_node(), make_control_fix_point_map(), make_control_postcondition_map(), node_to_path_transformer_or_postcondition(), pips_assert, pips_debug, print_control_node_uns(), print_cycle_head_to_fixpoint(), print_transformer, statement_domain, statement_identification(), transformer_range(), transformer_undefined, transformer_undefined_p, unstructured_control, unstructured_exit, and unstructured_undefined.
Referenced by unstructured_to_flow_sensitive_postconditions(), and unstructured_to_transformer().
transformer unstructured_to_flow_sensitive_total_preconditions | ( | transformer | t_post_u, |
transformer | pre, | ||
unstructured | u | ||
) |
control tail = unstructured_exit(u);
t_post_u | _post_u |
pre | re |
Definition at line 2473 of file unstructured.c.
References pips_assert, transformer_consistency_p(), and transformer_undefined.
Referenced by unstructured_to_total_precondition().
transformer unstructured_to_postcondition | ( | transformer | pre, |
unstructured | u, | ||
transformer | tf | ||
) |
there is only one statement and no arcs in u; no need for a fix-point
FI: pre should not be duplicated because statement_to_postcondition() means that pre is not going to be changed, just post produced.
Do not try anything clever! God knows what may happen in unstructured code. Postcondition post is not computed recursively from its components but directly derived from u's transformer. Preconditions associated to its components are then computed independently, hence the name unstructured_to_postconditionS instead of unstructured_to_postcondition
propagate as precondition an invariant for the whole unstructured u assuming that all nodes in the CFG are fully connected, unless tf is not feasible because the unstructured is never exited or exited thru a call to STOP which invalidates the previous assumption.
FI: I do not know if I should duplicate pre or not.
FI: well, dumdum, you should have duplicated tf!
FI: euh... why? According to comments about transformer_apply() neither arguments are modified...
post = unstructured_to_postconditions(pre_n, pre, u);
pre | re |
tf | f |
Definition at line 2075 of file unstructured.c.
References control_predecessors, control_statement, control_successors, ifdebug, invariant_wrt_transformer(), NIL, pips_assert, pips_debug, print_transformer, statement_to_postcondition(), transformer_apply(), transformer_dup(), transformer_empty_p(), transformer_free(), transformer_undefined, transformer_undefined_p, unstructured_control, unstructured_to_flow_insensitive_transformer(), unstructured_to_flow_sensitive_postconditions(), and unstructured_undefined.
Referenced by instruction_to_postcondition().
|
static |
SHARING! Every statement gets a pointer to the same precondition! I do not know if it's good or not but beware the bugs!!!
FI: changed to make free_transformer_mapping possible without testing sharing.
pre and pre_first can or not be used depending on the unstructured structure. They are always duplicated and the caller has to take care of their de-allocation.
special case for the first node if it has no predecessor
and if it is a test, as it always should, at least if
unspaghettify has been applied...
this is pretty useless and should be generalized to the DAG part of the CFG
refine the precondition if the node has only one predecessor and if this predecessor is a test and if the test can be exploited
the condition is true if c is the first successor of prev_c
pre_first | precondition holding for any node |
u | precondition holding at entry |
Definition at line 1952 of file unstructured.c.
References CAR, CONTROL, CONTROL_MAP, control_predecessors, control_statement, control_successors, ENDP, free_transformer(), gen_free_list(), gen_length(), ifdebug, NIL, pips_debug, precondition_add_condition_information(), print_transformer, statement_test(), statement_test_p(), statement_to_postcondition(), test_condition, transformer_dup(), transformer_empty(), transformer_free(), transformer_range(), transformer_undefined, transformer_undefined_p, unstructured_control, and unstructured_exit.
Referenced by unstructured_to_flow_sensitive_postconditions().
transformer unstructured_to_transformer | ( | unstructured | u, |
transformer | e_pre, | ||
list | e | ||
) |
effects of u
approximate store condition for all control nodes: simple context for improved transformer derivation; it is not a precondition and should have no arguments.
Same as previous one for the store on entry in the unstructured. This the entry node usually has predecessors in the CFG, this is not the context for the entry node. It is not a precondition.
No information available on entrance
Cheapest fix point transformer. The flow insensitive fix point could be used instead.
pre is replaced by its range condition later when needed
Transformers should be computed precisely whether the unstructured is left by the exit node or by an explicit or implicit call to STOP.
computing the transformer for u is like computing the postcondition with no information on entry: no, the input context may be used to refine the transformer.
pre_u is restricted to its range later when needed.
These tests should be performed at the scc level
Not really linked to fix point issue, but a way to know we are using a FAST option.
Do something for nodes unreachable from the entry but linked to the exit
The control flow graph is never exited... by the exit node
The unstructured is never exited, but all nodes are supposed to have transformers. This would never occur if the control restructuration were clean unless an infinite loop is stopped within a called procedure. Control effects are not reported.
FI: pre should be used!
Might be useless because it's now performed just above and more generally by a gen_multi_recurse()
e_pre | _pre |
e | precondition on entrance |
Definition at line 2332 of file unstructured.c.
References control_domain, effects_to_transformer(), forward_control_map_get_blocs(), free_transformer(), gen_false(), gen_free_list(), gen_in_list_p(), gen_length(), gen_multi_recurse(), gen_null(), gen_true(), get_bool_property(), get_int_property(), NIL, pips_assert, pips_debug, semantics_user_warning, statement_domain, transformer_dup(), transformer_empty(), transformer_empty_p(), transformer_identity(), transformer_safe_apply(), transformer_undefined, transformer_undefined_p, unreachable_node_to_transformer(), unstructured_control, unstructured_exit, unstructured_to_flow_insensitive_transformer(), unstructured_to_flow_sensitive_postconditions_or_transformers(), and unstructured_to_transformers().
Referenced by instruction_to_transformer().
|
static |
Computation of transformers associated to each node of u and to each of its sub-statements.
pre is valid for any node of u
There is no need to compute transformers for unreachable code, using CONTROL_MAP, but this may create storage and prettyprinter problems because of the data structure inconsistency.
Definition at line 2309 of file unstructured.c.
References CONTROL_MAP, control_statement, gen_free_list(), NIL, pips_debug, statement_to_transformer(), and unstructured_control.
Referenced by unstructured_to_transformer().
|
static |
Definition at line 268 of file unstructured.c.
References control_statement, hash_get(), HASH_UNDEFINED_VALUE, hash_update(), ifdebug, meaningless_control_p(), pips_assert, pips_debug, print_transformer, statement_identification(), and statement_undefined_p.
Referenced by cycle_to_flow_sensitive_preconditions().
void update_cycle_temporary_precondition | ( | control | c, |
transformer | pre, | ||
control_mapping | cycle_temporary_precondition_map | ||
) |
pre | re |
cycle_temporary_precondition_map | ycle_temporary_precondition_map |
Definition at line 1021 of file unstructured.c.
References control_statement, ifdebug, pips_debug, print_transformer, statement_identification(), and update_temporary_precondition().
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_to_flow_sensitive_preconditions().
void update_statement_temporary_precondition | ( | statement | s, |
transformer | pre, | ||
statement_mapping | statement_temporary_precondition_map | ||
) |
pre | re |
statement_temporary_precondition_map | tatement_temporary_precondition_map |
Definition at line 997 of file unstructured.c.
References pips_debug, statement_identification(), and update_temporary_precondition().
Referenced by cycle_to_flow_sensitive_preconditions(), and dag_to_flow_sensitive_preconditions().
void update_temporary_precondition | ( | void * | k, |
transformer | pre, | ||
hash_table | precondition_map | ||
) |
pre | re |
precondition_map | recondition_map |
Definition at line 975 of file unstructured.c.
References free_transformer(), hash_get(), hash_put(), HASH_UNDEFINED_VALUE, hash_update(), ifdebug, pips_debug, print_transformer, transformer_convex_hull(), and transformer_dup().
Referenced by update_cycle_temporary_precondition(), and update_statement_temporary_precondition().