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