CBMC
Loading...
Searching...
No Matches
count_eloc.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Count effective lines of code
4
5Author: Michael Tautschnig
6
7Date: December 2012
8
9\*******************************************************************/
10
13
14#include "count_eloc.h"
15
16#include <util/pointer_expr.h>
18#include <util/prefix.h>
19
20#include <goto-programs/cfg.h>
22
24
25#include <filesystem>
26#include <iostream>
27#include <unordered_set>
28
29typedef std::unordered_set<irep_idt> linest;
30typedef std::unordered_map<irep_idt, linest> filest;
31typedef std::unordered_map<irep_idt, filest> working_dirst;
32
33static 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
54void count_eloc(const goto_modelt &goto_model)
55{
56 std::size_t eloc=0;
57
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
68void list_eloc(const goto_modelt &goto_model)
69{
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 =
79 std::filesystem::path(id2string(files.first)).append(file).string();
80
81 for(const irep_idt &line : lines.second)
82 std::cout << file << ':' << line << '\n';
83 }
84}
85
86void print_path_lengths(const goto_modelt &goto_model)
87{
88 const irep_idt &entry_point=goto_model.goto_functions.entry_point();
89 goto_functionst::function_mapt::const_iterator start=
90 goto_model.goto_functions.function_map.find(entry_point);
91
92 if(start==goto_model.goto_functions.function_map.end() ||
93 !start->second.body_available())
94 {
95 std::cout << "No entry point found, path length undefined\n";
96 return;
97 }
98
100 {
101 bool visited;
102
103 visited_cfg_nodet():visited(false)
104 {
105 }
106 };
107
108 typedef cfg_baset<visited_cfg_nodet> cfgt;
109 cfgt cfg;
110 cfg(goto_model.goto_functions);
111
112 const goto_programt &start_program=start->second.body;
113
114 const cfgt::entryt &start_node =
115 cfg.get_node_index(start_program.instructions.begin());
116 const cfgt::entryt &last_node =
117 cfg.get_node_index(--start_program.instructions.end());
118
119 cfgt::patht shortest_path;
120 cfg.shortest_path(start_node, last_node, shortest_path);
121 std::cout << "Shortest control-flow path: " << shortest_path.size()
122 << " instructions\n";
123
124 std::size_t n_loops=0, loop_ins=0;
125 for(const auto &gf_entry : goto_model.goto_functions.function_map)
126 {
128 {
129 // loops or recursion
130 if(
131 i_it->is_backwards_goto() ||
132 i_it == gf_entry.second.body.instructions.begin())
133 {
134 const cfgt::entryt &node = cfg.get_node_index(i_it);
135 cfgt::patht loop;
136 cfg.shortest_loop(node, loop);
137
138 if(!loop.empty())
139 {
140 ++n_loops;
141 loop_ins+=loop.size()-1;
142 }
143 }
144 }
145 }
146
147 if(n_loops>0)
148 std::cout << "Loop information: " << n_loops << " loops, "
149 << loop_ins << " instructions in shortest paths of loop bodies\n";
150
151 std::size_t n_reachable=0;
152 cfg.visit_reachable(start_node);
153 for(std::size_t i=0; i<cfg.size(); ++i)
154 if(cfg[i].visited)
155 ++n_reachable;
156 std::cout << "Reachable instructions: " << n_reachable << "\n";
157}
158
160{
161 const namespacet ns(goto_model.symbol_table);
162
163 // if we have a linked object, only account for those that are used
164 // (slice-global-inits may have been used to avoid unnecessary initialization)
165 goto_functionst::function_mapt::const_iterator f_it =
167 const bool has_initialize =
168 f_it != goto_model.goto_functions.function_map.end();
169 std::unordered_set<irep_idt> initialized;
170
172 {
173 for(const auto &ins : f_it->second.body.instructions)
174 {
175 if(ins.is_assign())
176 {
178 ode.build(ins.assign_lhs(), ns);
179
180 if(ode.root_object().id() == ID_symbol)
181 {
182 const symbol_exprt &symbol_expr = to_symbol_expr(ode.root_object());
183 initialized.insert(symbol_expr.get_identifier());
184 }
185 }
186 }
187 }
188
190
191 for(const auto &symbol_entry : goto_model.symbol_table.symbols)
192 {
193 const symbolt &symbol = symbol_entry.second;
194 if(
195 symbol.is_type || symbol.is_macro || symbol.type.id() == ID_code ||
196 symbol.type.get_bool(ID_C_constant) ||
198 (has_initialize && initialized.find(symbol.name) == initialized.end()))
199 {
200 continue;
201 }
202
203 const auto bits = pointer_offset_bits(symbol.type, ns);
204 if(bits.has_value() && bits.value() > 0)
205 total_size += bits.value();
206 }
207
208 std::cout << "Total size of global objects: " << total_size << " bits\n";
209}
Control Flow Graph.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
Definition dstring.h:95
bool empty() const
Definition dstring.h:89
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
bool get_bool(const irep_idt &name) const
Definition irep.cpp:57
const irep_idt & id() const
Definition irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Split an expression into a base object and a (byte) offset.
Expression to hold a symbol (variable)
Definition std_expr.h:131
const irep_idt & get_identifier() const
Definition std_expr.h:160
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition symbol.h:28
bool is_macro
Definition symbol.h:62
bool is_type
Definition symbol.h:61
typet type
Type of symbol.
Definition symbol.h:31
irep_idt name
The unique identifier.
Definition symbol.h:40
std::unordered_set< irep_idt > linest
void count_eloc(const goto_modelt &goto_model)
void print_global_state_size(const goto_modelt &goto_model)
std::unordered_map< irep_idt, filest > working_dirst
static void collect_eloc(const goto_modelt &goto_model, working_dirst &dest)
void print_path_lengths(const goto_modelt &goto_model)
std::unordered_map< irep_idt, linest > filest
void list_eloc(const goto_modelt &goto_model)
Count effective lines of code.
#define CPROVER_PREFIX
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
API to expression classes for Pointers.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition smt_terms.h:17
#define INITIALIZE_FUNCTION
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:272