33 std::dynamic_pointer_cast<const data_dependency_contextt>(
eval(expr, ns));
35 if(res->get_data_dependencies().size() > 0)
39 for(
const auto &dep : res->get_data_dependencies())
40 deps[dep].insert(expr);
76 locationt from{trace_from->current_location()};
77 locationt to{trace_to->current_location()};
80 function_from, trace_from, function_to, trace_to, ai, ns);
85 dep_graph !=
nullptr,
"Domains should all be of the same type");
88 if(from->is_function_call())
90 if(function_from == function_to)
102 DATA_INVARIANT(s !=
nullptr,
"Domains should all be of the same type");
145 const exprt &rhs = to->assign_rhs();
148 if(rhs.
id() == ID_side_effect)
153 if(from->is_function_call())
155 const exprt &call = from->call_function();
157 if(call.
id() == ID_symbol)
162 goto_functionst::function_mapt::const_iterator it =
167 if(!it->second.body_available())
190 else if(to->is_function_call())
193 for(
const auto &arg : args)
198 else if(to->is_goto())
224 if(from->is_goto() || from->is_assume())
226 else if(from->is_end_function())
242 goto_functionst::function_mapt::const_iterator f_it =
252 pd_tmp(goto_program);
263 bool post_dom_all = !cd->is_assume();
264 bool post_dom_one =
false;
271 for(
const auto &edge : m.out)
278 post_dom_all =
false;
281 if(post_dom_all || !post_dom_one)
289 if(cd->is_goto() && !cd->is_backwards_goto())
293 to->location_number >= t->location_number ?
tvt(
false) :
tvt(
true);
320 bool changed =
false;
326 for(
const auto &c_dep : other_control_deps)
329 while(it !=
control_deps.end() && it->first < c_dep.first)
341 it !=
control_deps.end(),
"Property of branch needed for safety");
343 !(it->first < c_dep.first),
"Property of loop needed for safety");
345 !(c_dep.first < it->first),
"Property of loop needed for safety");
347 tvt &branch1 = it->second;
348 const tvt &branch2 = c_dep.second;
350 if(branch1 != branch2 && !branch1.
is_unknown())
365 other_control_dep_candidates.begin(), other_control_dep_candidates.end());
374 other_control_dep_calls.begin(), other_control_dep_calls.end());
383 other_control_dep_call_candidates.begin(),
384 other_control_dep_call_candidates.end());
404 bool changed =
false;
414 for(
auto bdep : cast_b.domain_data_deps)
416 for(
exprt bexpr : bdep.second)
419 changed |= result.second;
425 cast_b.control_dep_candidates,
426 cast_b.control_dep_calls,
427 cast_b.control_dep_call_candidates);
460 function_call, function_start, function_end, ns);
477 out <<
"Control dependencies: ";
478 for(control_depst::const_iterator it =
control_deps.begin();
488 out << cd->location_number <<
" [" <<
branch <<
"]";
498 out << (*it)->location_number <<
" [UNCONDITIONAL]";
506 out <<
"Data dependencies: ";
513 out << dep.first->location_number;
515 bool first_expr =
true;
516 for(
auto &expr : dep.second)
553 link[
"locationNumber"] =
555 link[
"sourceLocation"] =
json(target->source_location());
563 link[
"locationNumber"] =
565 link[
"sourceLocation"] =
json(target->source_location());
573 link[
"locationNumber"] =
575 link[
"sourceLocation"] =
json(dep.first->source_location());
579 const std::set<exprt> &expr_set = dep.second;
582 for(
const exprt &e : expr_set)
590 return std::move(graph);
626 auto p = util_make_unique<variable_sensitivity_dependence_domaint>(
630 return std::unique_ptr<statet>(p.release());
653 goto_functions(goto_functions),
663 const node_indext n_from = (*this)[from].get_node_id();
665 const node_indext n_to = (*this)[to].get_node_id();
673 nodes[n_from].out[n_to].add(kind);
674 nodes[n_to].in[n_from].add(kind);
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
void branch(goto_modelt &goto_model, const irep_idt &id)
The common case of history is to only care about where you are now, not how you got there!...
This is the basic interface of the abstract interpreter with default implementations of the core func...
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
ai_history_baset::trace_ptrt trace_ptrt
goto_programt::const_targett locationt
ai_domain_baset::locationt locationt
An easy factory implementation for histories that don't need parameters.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
exprt::operandst argumentst
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
nodet::node_indext node_indext
node_indext add_node(arguments &&... values)
const irep_idt & id() const
jsont & push_back(const jsont &json)
json_arrayt & make_array()
json_objectt & make_object()
The most conventional storage; one domain per location.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
An expression containing a side effect.
const irep_idt & get_statement() const
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
variable_sensitivity_object_factory_ptrt object_factory
const vsd_configt configuration
variable_sensitivity_dependence_grapht & dg
std::unique_ptr< statet > make(locationt l) const override
variable_sensitivity_dependence_domain_factoryt(variable_sensitivity_dependence_grapht &_dg, variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
control_dep_candidatest control_dep_candidates
std::set< goto_programt::const_targett > control_dep_callst
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)
std::map< goto_programt::const_targett, tvt > control_depst
control_depst control_deps
void populate_dep_graph(variable_sensitivity_dependence_grapht &, goto_programt::const_targett) const
control_dep_callst control_dep_calls
std::map< goto_programt::const_targett, std::set< exprt >, dependency_ordert > data_depst
control_dep_callst control_dep_call_candidates
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.
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.
std::set< goto_programt::const_targett > control_dep_candidatest
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)
bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to) override
Computes the join between "this" and "b".
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...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
Basic text output of the abstract domain.
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, variable_sensitivity_dependence_grapht &dep_graph, const namespacet &ns)
data_depst domain_data_deps
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
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)
post_dominators_mapt & cfg_post_dominators()
virtual statet & get_state(locationt l)
const goto_functionst & goto_functions
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
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.
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
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...
virtual bool merge(const variable_sensitivity_domaint &b, trace_ptrt from, trace_ptrt to)
Computes the join between "this" and "b".
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
Maintain data dependencies as a context in the variable sensitivity domain.
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...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::unique_ptr< T > util_make_unique(Ts &&... ts)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
side_effect_exprt & to_side_effect_expr(exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
A forked and modified version of analyses/dependence_graph.