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,
25  xmlt &dest)
26 {
27  source_locationt previous_location;
28 
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(
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 }
void convert(const goto_functionst &goto_functions, const value_set_analysist &value_set_analysis, xmlt &dest)
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert(const goto_programt &goto_program, xmlt &dest) const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
function_mapt function_map
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
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)
Value Set Propagation.
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
Definition: value_set.h:268
instructionst::const_iterator const_targett
Definition: goto_program.h:398
Definition: xml.h:18
State type in value_set_domaint, used in value-set analysis and goto-symex.
Definition: value_set.h:41
std::string data
Definition: xml.h:30
static void escape(const std::string &s, std::ostream &out)
escaping for XML elements
Definition: xml.cpp:78
xmlt & new_element(const std::string &name)
Definition: xml.h:86
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
const irep_idt & get_file() const
goto_programt & goto_program
Definition: cover.cpp:63
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool empty() const
Definition: dstring.h:73
valuest values
Stores the LHS ID -> RHS expression set map.
Definition: value_set.h:343