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);
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.
A codet representing an assignment in the program.
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
variable_sensitivity_dependence_domain_factoryt(variable_sensitivity_dependence_grapht &_dg, variable_sensitivity_object_factory_ptrt _object_factory, const vsd_configt &_configuration)
std::unique_ptr< statet > make(locationt l) const override
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.
post_dominators_mapt & cfg_post_dominators()
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)
const goto_functionst & goto_functions
void add_dep(vs_dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
virtual statet & get_state(locationt l)
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.