PIPS
|
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include "genC.h"
#include "linear.h"
#include "ri.h"
#include "effects.h"
#include "ri-util.h"
#include "prettyprint.h"
#include "effects-util.h"
#include "misc.h"
#include "text-util.h"
#include "newgen_set.h"
#include "points_to_private.h"
#include "pointer_values.h"
#include "effects-generic.h"
#include "effects-convex.h"
Go to the source code of this file.
Functions | |
bool | convex_cell_reference_preceding_p (reference r1, descriptor d1, reference r2, descriptor d2, transformer current_precondition, bool strict_p, bool *exact_p) |
eval.c More... | |
bool | convex_cell_preceding_p (cell c1, descriptor d1, cell c2, descriptor d2, transformer current_precondition, bool strict_p, bool *exact_p) |
void | simple_reference_to_convex_reference_conversion (reference ref, reference *output_ref, descriptor *output_desc) |
void | simple_cell_to_convex_cell_conversion (cell input_cell, cell *output_cell, descriptor *output_desc) |
list | eval_convex_cell_with_points_to (cell c, descriptor d, list ptl, bool *exact_p, transformer current_precondition) |
list | convex_effect_to_constant_path_effects_with_points_to (effect eff) |
list | convex_effect_find_aliased_paths_with_pointer_values (effect eff, statement s) |
list | convex_effect_to_constant_path_effects_with_pointer_values (effect __attribute__((unused)) eff) |
bool convex_cell_preceding_p | ( | cell | c1, |
descriptor | d1, | ||
cell | c2, | ||
descriptor | d2, | ||
transformer | current_precondition, | ||
bool | strict_p, | ||
bool * | exact_p | ||
) |
c1 | 1 |
d1 | 1 |
c2 | 2 |
d2 | 2 |
current_precondition | urrent_precondition |
strict_p | trict_p |
exact_p | xact_p |
Definition at line 191 of file eval.c.
References cell_any_reference(), convex_cell_reference_preceding_p(), and current_precondition.
Referenced by convex_effect_find_aliased_paths_with_pointer_values().
bool convex_cell_reference_preceding_p | ( | reference | r1, |
descriptor | d1, | ||
reference | r2, | ||
descriptor | d2, | ||
transformer | current_precondition, | ||
bool | strict_p, | ||
bool * | exact_p | ||
) |
eval.c
same entity and the path length of r1 is shorter than the path length of r2.
we now have to check that each common index matches
only matching reference indices have been found (phi variables or struct field entities).
we must now check the descriptors.
r1 | 1 |
d1 | 1 |
r2 | 2 |
d2 | 2 |
current_precondition | urrent_precondition |
strict_p | trict_p |
exact_p | xact_p |
Definition at line 67 of file eval.c.
References CAR, cell_reference, CONS, copy_effect(), current_precondition, descriptor_undefined, EFFECT, effect_cell, effect_descriptor, ENDP, EXPRESSION, expression_equal_p(), free_effect(), gen_free_list(), gen_full_free_list(), gen_length(), is_cell_reference, make_action_write_memory(), make_approximation_exact(), make_cell(), make_effect(), NIL, phi_entities_list(), pips_debug, pips_debug_effect, POP, predicate_system, project_regions_along_variables(), reference_indices, reference_to_string(), reference_undefined, reference_variable, region, region_intersection(), region_sc_append(), region_sup_difference(), same_entity_p(), transformer_relation, and transformer_undefined_p.
Referenced by convex_cell_preceding_p(), and eval_convex_cell_with_points_to().
eff | ff |
Definition at line 326 of file eval.c.
References cell_relations_list, convex_cell_preceding_p(), convex_cell_with_address_of_cell_translation(), convex_cell_with_value_of_cell_translation(), convex_cells_inclusion_p(), convex_cells_intersection_p(), generic_effect_find_aliases_with_simple_pointer_values(), load_pv(), make_simple_pv_context(), reset_pv_context(), simple_cell_to_convex_cell_conversion(), and transformer_undefined.
Referenced by convex_effect_to_constant_path_effects_with_pointer_values().
list convex_effect_to_constant_path_effects_with_pointer_values | ( | effect __attribute__((unused)) | eff | ) |
it should be a union here. However, we expect the caller to perform the contraction afterwards.
Definition at line 346 of file eval.c.
References CONS, convex_effect_find_aliased_paths_with_pointer_values(), copy_action(), EFFECT, effect_action, effect_any_reference, effect_dup_func, effect_entity(), effect_reference_dereferencing_p(), effects_private_current_stmt_head(), entity_abstract_location_p(), FOREACH, free_effect(), gen_free_list(), make_anywhere_effect(), NIL, null_pointer_value_entity_p(), pips_debug, pips_debug_effects, ref, and undefined_pointer_value_entity_p().
We have not found any equivalent constant path : it may point anywhere
We should maybe contract these effects later. Is it done by the callers ?
change the resulting effects action to the current effect action
eff | ff |
Definition at line 285 of file eval.c.
References CONS, copy_action(), copy_effect(), EFFECT, effect_action, effect_any_reference, effect_cell, effect_descriptor, effect_read_p, effect_reference_dereferencing_p(), effects_private_current_context_empty_p(), effects_private_current_context_head(), effects_private_current_stmt_head(), effects_to_read_effects(), ENDP, eval_convex_cell_with_points_to(), gen_nconc(), load_pt_to_list(), make_anywhere_effect(), NIL, pips_debug, points_to_list_list, ref, and transformer_undefined.
Referenced by set_methods_for_convex_effects().
list eval_convex_cell_with_points_to | ( | cell | c, |
descriptor | d, | ||
list | ptl, | ||
bool * | exact_p, | ||
transformer | current_precondition | ||
) |
ptl | tl |
exact_p | xact_p |
current_precondition | urrent_precondition |
Definition at line 275 of file eval.c.
References convex_cell_reference_preceding_p(), convex_cell_reference_with_address_of_cell_reference_translation(), current_precondition, generic_eval_cell_with_points_to(), and simple_reference_to_convex_reference_conversion().
Referenced by convex_effect_to_constant_path_effects_with_points_to(), and set_methods_for_convex_effects().
void simple_cell_to_convex_cell_conversion | ( | cell | input_cell, |
cell * | output_cell, | ||
descriptor * | output_desc | ||
) |
input_cell | nput_cell |
output_cell | utput_cell |
output_desc | utput_desc |
Definition at line 234 of file eval.c.
References cell_any_reference(), make_cell_reference(), reference_undefined, and simple_reference_to_convex_reference_conversion().
Referenced by convex_effect_find_aliased_paths_with_pointer_values().
void simple_reference_to_convex_reference_conversion | ( | reference | ref, |
reference * | output_ref, | ||
descriptor * | output_desc | ||
) |
ref | ef |
output_ref | utput_ref |
output_desc | utput_desc |
Definition at line 205 of file eval.c.
References cell_reference, convex_region_add_expression_dimension(), descriptor_undefined, effect_add_field_dimension(), effect_any_reference, effect_cell, effect_descriptor, entity_field_p(), exp, EXPRESSION, expression_reference(), expression_reference_p(), FOREACH, free_effect(), make_action_write_memory(), make_approximation_exact(), make_cell_reference(), make_descriptor_convex(), make_effect(), make_reference(), NIL, pips_debug_effect, ref, reference_indices, reference_undefined, reference_variable, and sc_new().
Referenced by eval_convex_cell_with_points_to(), and simple_cell_to_convex_cell_conversion().