cprover
value_set_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "value_set_analysis.h"
13 
14 #include <util/cprover_prefix.h>
15 #include <util/prefix.h>
16 #include <util/xml_irep.h>
17 
18 #include <langapi/language_util.h>
19 
21  const std::function<const value_sett &(goto_programt::const_targett)>
22  &get_value_set,
23  const goto_programt &goto_program,
24  xmlt &dest)
25 {
26  source_locationt previous_location;
27 
28  forall_goto_program_instructions(i_it, goto_program)
29  {
30  const source_locationt &location=i_it->source_location;
31 
32  if(location==previous_location)
33  continue;
34 
35  if(location.is_nil() || location.get_file().empty())
36  continue;
37 
38  // find value set
39  const value_sett &value_set=get_value_set(i_it);
40 
41  xmlt &i=dest.new_element("instruction");
42  i.new_element()=::xml(location);
43 
45  value_set.values.get_view(view);
46 
47  for(const auto &values_entry : view)
48  {
49  xmlt &var=i.new_element("variable");
50  var.new_element("identifier").data = id2string(values_entry.first);
51 
52 #if 0
53  const value_sett::expr_sett &expr_set=
54  v_it->second.expr_set();
55 
56  for(value_sett::expr_sett::const_iterator
57  e_it=expr_set.begin();
58  e_it!=expr_set.end();
59  e_it++)
60  {
61  std::string value_str=
62  from_expr(ns, identifier, *e_it);
63 
64  var.new_element("value").data=
65  xmlt::escape(value_str);
66  }
67 #endif
68  }
69  }
70 }
71 
72 void convert(
73  const goto_functionst &goto_functions,
74  const value_set_analysist &value_set_analysis,
75  xmlt &dest)
76 {
77  dest=xmlt("value_set_analysis");
78 
79  for(goto_functionst::function_mapt::const_iterator
80  f_it=goto_functions.function_map.begin();
81  f_it!=goto_functions.function_map.end();
82  f_it++)
83  {
84  xmlt &f=dest.new_element("function");
85  f.new_element("identifier").data=id2string(f_it->first);
86  value_set_analysis.convert(f_it->second.body, f);
87  }
88 }
89 
90 void convert(
91  const goto_programt &goto_program,
92  const value_set_analysist &value_set_analysis,
93  xmlt &dest)
94 {
95  dest=xmlt("value_set_analysis");
96 
97  value_set_analysis.convert(
98  goto_program,
99  dest.new_element("program"));
100 }
value_set_analysis_templatet::convert
void convert(const goto_programt &goto_program, xmlt &dest) const
Definition: value_set_analysis.h:55
prefix.h
value_set_analysis_templatet
This template class implements a data-flow analysis which keeps track of what values different variab...
Definition: value_set_analysis.h:40
xmlt::escape
static void escape(const std::string &s, std::ostream &out)
escaping for XML elements
Definition: xml.cpp:79
value_sett
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:45
xml_irep.h
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
convert
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
Definition: value_set_analysis.cpp:72
value_sets_to_xml
void value_sets_to_xml(const std::function< const value_sett &(goto_programt::const_targett)> &get_value_set, const goto_programt &goto_program, xmlt &dest)
Definition: value_set_analysis.cpp:20
value_sett::expr_sett
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:241
sharing_mapt< irep_idt, entryt >::viewt
std::vector< view_itemt > viewt
View of the key-value pairs in the map.
Definition: sharing_map.h:365
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
language_util.h
irept::is_nil
bool is_nil() const
Definition: irep.h:398
dstringt::empty
bool empty() const
Definition: dstring.h:88
cprover_prefix.h
xmlt
Definition: xml.h:21
sharing_mapt::get_view
void get_view(viewt &view) const
Get a view of the elements in the map A view is a list of pairs with the components being const refer...
Definition: sharing_map.h:782
source_locationt
Definition: source_location.h:20
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
value_set_analysis.h
Value Set Propagation.
xmlt::data
std::string data
Definition: xml.h:39
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
value_sett::values
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:329