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 goto_programt &goto_program)
23 {
24  baset::initialize(goto_program);
25 }
26 
28  const goto_functionst &goto_functions)
29 {
30  baset::initialize(goto_functions);
31 }
32 
34  const goto_programt &goto_program,
35  const irep_idt &identifier,
36  xmlt &dest) const
37 {
38  source_locationt previous_location;
39 
40  forall_goto_program_instructions(i_it, goto_program)
41  {
42  const source_locationt &location=i_it->source_location;
43 
44  if(location==previous_location)
45  continue;
46 
47  if(location.is_nil() || location.get_file().empty())
48  continue;
49 
50  // find value set
51  const value_sett &value_set=(*this)[i_it].value_set;
52 
53  xmlt &i=dest.new_element("instruction");
54  i.new_element()=::xml(location);
55 
56  for(value_sett::valuest::const_iterator
57  v_it=value_set.values.begin();
58  v_it!=value_set.values.end();
59  v_it++)
60  {
61  xmlt &var=i.new_element("variable");
62  var.new_element("identifier").data=
63  id2string(v_it->first);
64 
65  #if 0
66  const value_sett::expr_sett &expr_set=
67  v_it->second.expr_set();
68 
69  for(value_sett::expr_sett::const_iterator
70  e_it=expr_set.begin();
71  e_it!=expr_set.end();
72  e_it++)
73  {
74  std::string value_str=
75  from_expr(ns, identifier, *e_it);
76 
77  var.new_element("value").data=
78  xmlt::escape(value_str);
79  }
80  #endif
81  }
82  }
83 }
84 void convert(
85  const goto_functionst &goto_functions,
86  const value_set_analysist &value_set_analysis,
87  xmlt &dest)
88 {
89  dest=xmlt("value_set_analysis");
90 
91  for(goto_functionst::function_mapt::const_iterator
92  f_it=goto_functions.function_map.begin();
93  f_it!=goto_functions.function_map.end();
94  f_it++)
95  {
96  xmlt &f=dest.new_element("function");
97  f.new_element("identifier").data=id2string(f_it->first);
98  value_set_analysis.convert(f_it->second.body, f_it->first, f);
99  }
100 }
101 
102 void convert(
103  const goto_programt &goto_program,
104  const value_set_analysist &value_set_analysis,
105  xmlt &dest)
106 {
107  dest=xmlt("value_set_analysis");
108 
109  value_set_analysis.convert(
110  goto_program,
111  "",
112  dest.new_element("program"));
113 }
const namespacet & ns
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
Value Set Propagation.
std::set< exprt > expr_sett
Definition: value_set.h:119
Definition: xml.h:18
void convert(const goto_programt &goto_program, const irep_idt &identifier, xmlt &dest) const
virtual void initialize(const goto_programt &goto_program)
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 specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
const irep_idt & get_file() const
virtual void initialize(const goto_programt &goto_program)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
bool empty() const
Definition: dstring.h:61
valuest values
Definition: value_set.h:156