CBMC
count_eloc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Count effective lines of code
4 
5 Author: Michael Tautschnig
6 
7 Date: December 2012
8 
9 \*******************************************************************/
10 
13 
14 #include "count_eloc.h"
15 
16 #include <iostream>
17 #include <unordered_set>
18 
19 #include <util/file_util.h>
20 #include <util/pointer_expr.h>
22 #include <util/prefix.h>
23 
24 #include <goto-programs/cfg.h>
26 
28 
29 typedef std::unordered_set<irep_idt> linest;
30 typedef std::unordered_map<irep_idt, linest> filest;
31 typedef std::unordered_map<irep_idt, filest> working_dirst;
32 
33 static void collect_eloc(
34  const goto_modelt &goto_model,
35  working_dirst &dest)
36 {
37  for(const auto &gf_entry : goto_model.goto_functions.function_map)
38  {
39  for(const auto &instruction : gf_entry.second.body.instructions)
40  {
41  const auto &source_location = instruction.source_location();
42 
43  filest &files = dest[source_location.get_working_directory()];
44  const irep_idt &file = source_location.get_file();
45 
46  if(!file.empty() && !source_location.is_built_in())
47  {
48  files[file].insert(source_location.get_line());
49  }
50  }
51  }
52 }
53 
54 void count_eloc(const goto_modelt &goto_model)
55 {
56  std::size_t eloc=0;
57 
58  working_dirst eloc_map;
59  collect_eloc(goto_model, eloc_map);
60 
61  for(auto const &files : eloc_map)
62  for(auto const &lines : files.second)
63  eloc+=lines.second.size();
64 
65  std::cout << "Effective lines of code: " << eloc << '\n';
66 }
67 
68 void list_eloc(const goto_modelt &goto_model)
69 {
70  working_dirst eloc_map;
71  collect_eloc(goto_model, eloc_map);
72 
73  for(auto const &files : eloc_map)
74  for(auto const &lines : files.second)
75  {
76  std::string file=id2string(lines.first);
77  if(!files.first.empty())
78  file=concat_dir_file(id2string(files.first), file);
79 
80  for(const irep_idt &line : lines.second)
81  std::cout << file << ':' << line << '\n';
82  }
83 }
84 
85 void print_path_lengths(const goto_modelt &goto_model)
86 {
87  const irep_idt &entry_point=goto_model.goto_functions.entry_point();
88  goto_functionst::function_mapt::const_iterator start=
89  goto_model.goto_functions.function_map.find(entry_point);
90 
91  if(start==goto_model.goto_functions.function_map.end() ||
92  !start->second.body_available())
93  {
94  std::cout << "No entry point found, path length undefined\n";
95  return;
96  }
97 
98  struct visited_cfg_nodet
99  {
100  bool visited;
101 
102  visited_cfg_nodet():visited(false)
103  {
104  }
105  };
106 
107  typedef cfg_baset<visited_cfg_nodet> cfgt;
108  cfgt cfg;
109  cfg(goto_model.goto_functions);
110 
111  const goto_programt &start_program=start->second.body;
112 
113  const cfgt::entryt &start_node =
114  cfg.get_node_index(start_program.instructions.begin());
115  const cfgt::entryt &last_node =
116  cfg.get_node_index(--start_program.instructions.end());
117 
118  cfgt::patht shortest_path;
119  cfg.shortest_path(start_node, last_node, shortest_path);
120  std::cout << "Shortest control-flow path: " << shortest_path.size()
121  << " instructions\n";
122 
123  std::size_t n_loops=0, loop_ins=0;
124  for(const auto &gf_entry : goto_model.goto_functions.function_map)
125  {
126  forall_goto_program_instructions(i_it, gf_entry.second.body)
127  {
128  // loops or recursion
129  if(
130  i_it->is_backwards_goto() ||
131  i_it == gf_entry.second.body.instructions.begin())
132  {
133  const cfgt::entryt &node = cfg.get_node_index(i_it);
134  cfgt::patht loop;
135  cfg.shortest_loop(node, loop);
136 
137  if(!loop.empty())
138  {
139  ++n_loops;
140  loop_ins+=loop.size()-1;
141  }
142  }
143  }
144  }
145 
146  if(n_loops>0)
147  std::cout << "Loop information: " << n_loops << " loops, "
148  << loop_ins << " instructions in shortest paths of loop bodies\n";
149 
150  std::size_t n_reachable=0;
151  cfg.visit_reachable(start_node);
152  for(std::size_t i=0; i<cfg.size(); ++i)
153  if(cfg[i].visited)
154  ++n_reachable;
155  std::cout << "Reachable instructions: " << n_reachable << "\n";
156 }
157 
158 void print_global_state_size(const goto_modelt &goto_model)
159 {
160  const namespacet ns(goto_model.symbol_table);
161 
162  // if we have a linked object, only account for those that are used
163  // (slice-global-inits may have been used to avoid unnecessary initialization)
164  goto_functionst::function_mapt::const_iterator f_it =
166  const bool has_initialize =
167  f_it != goto_model.goto_functions.function_map.end();
168  std::unordered_set<irep_idt> initialized;
169 
170  if(has_initialize)
171  {
172  for(const auto &ins : f_it->second.body.instructions)
173  {
174  if(ins.is_assign())
175  {
177  ode.build(ins.assign_lhs(), ns);
178 
179  if(ode.root_object().id() == ID_symbol)
180  {
181  const symbol_exprt &symbol_expr = to_symbol_expr(ode.root_object());
182  initialized.insert(symbol_expr.get_identifier());
183  }
184  }
185  }
186  }
187 
188  mp_integer total_size = 0;
189 
190  for(const auto &symbol_entry : goto_model.symbol_table.symbols)
191  {
192  const symbolt &symbol = symbol_entry.second;
193  if(
194  symbol.is_type || symbol.is_macro || symbol.type.id() == ID_code ||
195  symbol.type.get_bool(ID_C_constant) ||
197  (has_initialize && initialized.find(symbol.name) == initialized.end()))
198  {
199  continue;
200  }
201 
202  const auto bits = pointer_offset_bits(symbol.type, ns);
203  if(bits.has_value() && bits.value() > 0)
204  total_size += bits.value();
205  }
206 
207  std::cout << "Total size of global objects: " << total_size << " bits\n";
208 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
pointer_offset_size.h
cfg.h
mp_integer
BigInt mp_integer
Definition: smt_terms.h:17
symbolt::is_macro
bool is_macro
Definition: symbol.h:61
object_descriptor_exprt::build
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
Definition: pointer_expr.cpp:107
print_global_state_size
void print_global_state_size(const goto_modelt &goto_model)
Definition: count_eloc.cpp:158
file_util.h
filest
std::unordered_map< irep_idt, linest > filest
Definition: count_eloc.cpp:30
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:166
prefix.h
count_eloc.h
goto_model.h
goto_modelt
Definition: goto_model.h:25
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
object_descriptor_exprt::root_object
static const exprt & root_object(const exprt &expr)
Definition: pointer_expr.cpp:168
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
concat_dir_file
std::string concat_dir_file(const std::string &directory, const std::string &file_name)
Definition: file_util.cpp:159
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:142
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
pointer_expr.h
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:222
count_eloc
void count_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:54
irept::id
const irep_idt & id() const
Definition: irep.h:396
dstringt::empty
bool empty() const
Definition: dstring.h:88
cfg_baset
A multi-procedural control flow graph (CFG) whose nodes store references to instructions in a GOTO pr...
Definition: cfg.h:86
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
patht
std::list< path_nodet > patht
Definition: path.h:44
symbolt
Symbol table entry.
Definition: symbol.h:27
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
symbolt::is_type
bool is_type
Definition: symbol.h:61
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
working_dirst
std::unordered_map< irep_idt, filest > working_dirst
Definition: count_eloc.cpp:31
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
linest
std::unordered_set< irep_idt > linest
Definition: count_eloc.cpp:29
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
static_lifetime_init.h
list_eloc
void list_eloc(const goto_modelt &goto_model)
Definition: count_eloc.cpp:68
collect_eloc
static void collect_eloc(const goto_modelt &goto_model, working_dirst &dest)
Definition: count_eloc.cpp:33
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
print_path_lengths
void print_path_lengths(const goto_modelt &goto_model)
Definition: count_eloc.cpp:85
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
irept::get_bool
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:58
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1229