Go to the documentation of this file.
31 std::dynamic_pointer_cast<const data_dependency_contextt>(
eval(expr, ns));
33 if(res->get_data_dependencies().size() > 0)
37 for(
const auto &dep : res->get_data_dependencies())
38 deps[dep].insert(expr);
74 locationt from{trace_from->current_location()};
75 locationt to{trace_to->current_location()};
78 function_from, trace_from, function_to, trace_to, ai, ns);
83 dep_graph !=
nullptr,
"Domains should all be of the same type");
86 if(from->is_function_call())
88 if(function_from == function_to)
100 DATA_INVARIANT(s !=
nullptr,
"Domains should all be of the same type");
147 if(rhs.
id() == ID_side_effect)
152 if(from->is_function_call())
154 const exprt &call = from->call_function();
156 if(call.
id() == ID_symbol)
161 goto_functionst::function_mapt::const_iterator it =
166 if(!it->second.body_available())
189 else if(to->is_function_call())
192 for(
const auto &arg : args)
197 else if(to->is_goto())
223 if(from->is_goto() || from->is_assume())
225 else if(from->is_end_function())
241 goto_functionst::function_mapt::const_iterator f_it =
251 pd_tmp(goto_program);
262 bool post_dom_all = !cd->is_assume();
263 bool post_dom_one =
false;
270 for(
const auto &edge : m.out)
277 post_dom_all =
false;
280 if(post_dom_all || !post_dom_one)
288 if(cd->is_goto() && !cd->is_backwards_goto())
292 to->location_number >= t->location_number ?
tvt(
false) :
tvt(
true);
319 bool changed =
false;
325 for(
const auto &c_dep : other_control_deps)
328 while(it !=
control_deps.end() && it->first < c_dep.first)
340 it !=
control_deps.end(),
"Property of branch needed for safety");
342 !(it->first < c_dep.first),
"Property of loop needed for safety");
344 !(c_dep.first < it->first),
"Property of loop needed for safety");
346 tvt &branch1 = it->second;
347 const tvt &branch2 = c_dep.second;
349 if(branch1 != branch2 && !branch1.
is_unknown())
364 other_control_dep_candidates.begin(), other_control_dep_candidates.end());
373 other_control_dep_calls.begin(), other_control_dep_calls.end());
382 other_control_dep_call_candidates.begin(),
383 other_control_dep_call_candidates.end());
403 bool changed =
false;
413 for(
auto bdep : cast_b.domain_data_deps)
415 for(
exprt bexpr : bdep.second)
418 changed |= result.second;
424 cast_b.control_dep_candidates,
425 cast_b.control_dep_calls,
426 cast_b.control_dep_call_candidates);
459 function_call, function_start, function_end, ns);
476 out <<
"Control dependencies: ";
477 for(control_depst::const_iterator it =
control_deps.begin();
487 out << cd->location_number <<
" [" <<
branch <<
"]";
497 out << (*it)->location_number <<
" [UNCONDITIONAL]";
505 out <<
"Data dependencies: ";
512 out << dep.first->location_number;
514 bool first_expr =
true;
515 for(
auto &expr : dep.second)
552 link[
"locationNumber"] =
554 link[
"sourceLocation"] =
json(target->source_location);
562 link[
"locationNumber"] =
564 link[
"sourceLocation"] =
json(target->source_location);
572 link[
"locationNumber"] =
574 link[
"sourceLocation"] =
json(dep.first->source_location);
578 const std::set<exprt> &expr_set = dep.second;
581 for(
const exprt &e : expr_set)
589 return std::move(graph);
625 auto p = util_make_unique<variable_sensitivity_dependence_domaint>(
629 return std::unique_ptr<statet>(p.release());
652 goto_functions(goto_functions),
662 const node_indext n_from = (*this)[from].get_node_id();
664 const node_indext n_to = (*this)[to].get_node_id();
672 nodes[n_from].out[n_to].add(kind);
673 nodes[n_to].in[n_from].add(kind);
variable_sensitivity_object_factory_ptrt object_factory
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to) override
Computes the join between "this" and "b".
control_depst control_deps
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
The common case of history is to only care about where you are now, not how you got there!...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
std::set< goto_programt::const_targett > control_dep_callst
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
node_indext add_node(arguments &&... values)
data_depst domain_data_deps
Base class for all expressions.
const vsd_configt configuration
std::unique_ptr< statet > make(locationt l) const override
variable_sensitivity_dependence_grapht & dg
variable_sensitivity_dependence_domain_factoryt(variable_sensitivity_dependence_grapht &_dg, variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
side_effect_exprt & to_side_effect_expr(exprt &expr)
function_mapt function_map
json_objectt & make_object()
A forked and modified version of analyses/dependence_graph.
ai_history_baset::trace_ptrt trace_ptrt
const goto_functionst & goto_functions
nodet::node_indext node_indext
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
std::unique_ptr< T > util_make_unique(Ts &&... ts)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
An easy factory implementation for histories that don't need parameters.
void branch(goto_modelt &goto_model, const irep_idt &id)
variable_sensitivity_dependence_grapht(const goto_functionst &goto_functions, const namespacet &_ns, variable_sensitivity_object_factory_ptrt object_factory, const vsd_configt &_configuration, message_handlert &message_handler)
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
std::set< goto_programt::const_targett > control_dep_candidatest
virtual void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns)
Perform a context aware merge of the changes that have been applied between function_start and the cu...
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
void control_dependencies(const irep_idt &from_function, goto_programt::const_targett from, const irep_idt &to_function, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph)
void eval_data_deps(const exprt &expr, const namespacet &ns, data_depst &deps) const
Evaluate an expression and accumulate all the data dependencies involved in the evaluation.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
exprt::operandst argumentst
json_arrayt & make_array()
Maintain data dependencies as a context in the variable sensitivity domain.
The most conventional storage; one domain per location.
post_dominators_mapt & cfg_post_dominators()
std::map< goto_programt::const_targett, tvt > control_depst
const irep_idt & get_statement() const
bool merge_control_dependencies(const control_depst &other_control_deps, const control_dep_candidatest &other_control_dep_candidates, const control_dep_callst &other_control_dep_calls, const control_dep_callst &other_control_dep_call_candidates)
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
A collection of goto functions.
goto_programt::const_targett locationt
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
This is the basic interface of the abstract interpreter with default implementations of the core func...
A generic container class for the GOTO intermediate representation of one function.
ai_domain_baset::locationt locationt
instructionst::const_iterator const_targett
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A codet representing an assignment in the program.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
void merge_three_way_function_return(const ai_domain_baset &function_call, const ai_domain_baset &function_start, const ai_domain_baset &function_end, const namespacet &ns) override
Perform a context aware merge of the changes that have been applied between function_start and the cu...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) override
Compute the abstract transformer for a single instruction.
jsont & push_back(const jsont &json)
control_dep_callst control_dep_calls
An expression containing a side effect.
virtual statet & get_state(locationt l)
control_dep_candidatest control_dep_candidates
control_dep_callst control_dep_call_candidates