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/prefix.h>
15 #include <util/cprover_prefix.h>
16 #include <util/xml_expr.h>
17 #include <util/xml.h>
18 
19 #include <langapi/language_util.h>
20 
22  const std::function<const value_sett &(goto_programt::const_targett)>
23  &get_value_set,
24  const goto_programt &goto_program,
25  xmlt &dest)
26 {
27  source_locationt previous_location;
28 
29  forall_goto_program_instructions(i_it, goto_program)
30  {
31  const source_locationt &location=i_it->source_location;
32 
33  if(location==previous_location)
34  continue;
35 
36  if(location.is_nil() || location.get_file().empty())
37  continue;
38 
39  // find value set
40  const value_sett &value_set=get_value_set(i_it);
41 
42  xmlt &i=dest.new_element("instruction");
43  i.new_element()=::xml(location);
44 
45  for(value_sett::valuest::const_iterator
46  v_it=value_set.values.begin();
47  v_it!=value_set.values.end();
48  v_it++)
49  {
50  xmlt &var=i.new_element("variable");
51  var.new_element("identifier").data=
52  id2string(v_it->first);
53 
54  #if 0
55  const value_sett::expr_sett &expr_set=
56  v_it->second.expr_set();
57 
58  for(value_sett::expr_sett::const_iterator
59  e_it=expr_set.begin();
60  e_it!=expr_set.end();
61  e_it++)
62  {
63  std::string value_str=
64  from_expr(ns, identifier, *e_it);
65 
66  var.new_element("value").data=
67  xmlt::escape(value_str);
68  }
69  #endif
70  }
71  }
72 }
73 
74 void convert(
75  const goto_functionst &goto_functions,
76  const value_set_analysist &value_set_analysis,
77  xmlt &dest)
78 {
79  dest=xmlt("value_set_analysis");
80 
81  for(goto_functionst::function_mapt::const_iterator
82  f_it=goto_functions.function_map.begin();
83  f_it!=goto_functions.function_map.end();
84  f_it++)
85  {
86  xmlt &f=dest.new_element("function");
87  f.new_element("identifier").data=id2string(f_it->first);
88  value_set_analysis.convert(f_it->second.body, f);
89  }
90 }
91 
92 void convert(
93  const goto_programt &goto_program,
94  const value_set_analysist &value_set_analysis,
95  xmlt &dest)
96 {
97  dest=xmlt("value_set_analysis");
98 
99  value_set_analysis.convert(
100  goto_program,
101  dest.new_element("program"));
102 }
value_set_analysis_templatet::convert
void convert(const goto_programt &goto_program, xmlt &dest) const
Definition: value_set_analysis.h:48
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
prefix.h
value_set_analysis_templatet
Definition: value_set_analysis.h:30
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:41
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:74
xml.h
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:21
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:268
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
language_util.h
irept::is_nil
bool is_nil() const
Definition: irep.h:172
dstringt::empty
bool empty() const
Definition: dstring.h:75
cprover_prefix.h
xmlt
Definition: xml.h:18
source_locationt
Definition: source_location.h:20
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
value_set_analysis.h
xmlt::data
std::string data
Definition: xml.h:30
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:804
xml_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
value_sett::values
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:346