Skip to content

Commit 67f679a

Browse files
tautschnigtautschnig
authored
Merge pull request #1485 from diffblue/show-module-class
factor out module list output
2 parents 1d95a6e + 4ab1e1b commit 67f679a

File tree

13 files changed

+182
-174
lines changed

13 files changed

+182
-174
lines changed

‎regression/ebmc/CLI/show-modules-smv.desc‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,16 +4,19 @@ show-modules-smv.smv
44
activate-multi-line-match
55
Module 1:
66
Location: file show-modules-smv\.smv line 3
7+
Mode: SMV
78
Identifier: smv::main
89
Name: main
910

1011
Module 2:
1112
Location: file show-modules-smv\.smv line 8
13+
Mode: SMV
1214
Identifier: smv::bar
1315
Name: bar
1416

1517
Module 3:
1618
Location: file show-modules-smv\.smv line 13
19+
Mode: SMV
1720
Identifier: smv::foo
1821
Name: foo
1922
^EXIT=0$

‎src/Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ ifneq ($(BUILD_ENV),MSVC)
2121
ebmc.dir: ic3.dir
2222
endif
2323

24-
hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \
24+
hw-cbmc.dir: ebmc.dir trans-word-level.dir trans-netlist.dir verilog.dir \
2525
vhdl.dir smvlang.dir cprover.dir temporal-logic.dir
2626

2727
vlindex.dir: ebmc.dir cprover.dir verilog.dir

‎src/ebmc/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ SRC = \
3636
ranking_function.cpp \
3737
report_results.cpp \
3838
show_formula_solver.cpp \
39+
show_modules.cpp \
3940
show_properties.cpp \
4041
show_trans.cpp \
4142
tautology_check.cpp \

‎src/ebmc/build_transition_system.cpp‎

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,12 @@ Author: Daniel Kroening, [email protected]
2020
#include <langapi/mode.h>
2121
#include <smvlang/smv_ebmc_language.h>
2222
#include <trans-word-level/show_module_hierarchy.h>
23-
#include <trans-word-level/show_modules.h>
2423

2524
#include "ebmc_error.h"
2625
#include "ebmc_language_file.h"
2726
#include "ebmc_version.h"
2827
#include "output_file.h"
28+
#include "show_modules.h"
2929
#include "transition_system.h"
3030

3131
#include <fstream>
@@ -228,22 +228,25 @@ int get_transition_system(
228228

229229
if(cmdline.isset("show-modules"))
230230
{
231-
show_modules(transition_system.symbol_table, std::cout);
231+
show_modulest::from_symbol_table(transition_system.symbol_table)
232+
.plain_text(std::cout);
232233
return 0;
233234
}
234235

235236
if(cmdline.isset("modules-xml"))
236237
{
237238
auto filename = cmdline.get_value("modules-xml");
238-
auto outfile = output_filet{filename};
239-
show_modules_xml(transition_system.symbol_table, outfile.stream());
239+
auto out_file = output_filet{filename};
240+
show_modulest::from_symbol_table(transition_system.symbol_table)
241+
.xml(out_file.stream());
240242
return 0;
241243
}
242244

243245
if(cmdline.isset("json-modules"))
244246
{
245247
auto out_file = output_filet{cmdline.get_value("json-modules")};
246-
json_modules(transition_system.symbol_table, out_file.stream());
248+
show_modulest::from_symbol_table(transition_system.symbol_table)
249+
.json(out_file.stream());
247250
return 0;
248251
}
249252

‎src/ebmc/show_modules.cpp‎

Lines changed: 97 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,97 @@
1+
/*******************************************************************\
2+
3+
Module: Show Modules
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "show_modules.h"
10+
11+
#include <util/json_irep.h>
12+
#include <util/symbol_table_base.h>
13+
#include <util/xml_irep.h>
14+
15+
void show_modulest::xml(std::ostream &out) const
16+
{
17+
std::size_t count = 0;
18+
19+
for(const auto &module : modules)
20+
{
21+
count++;
22+
23+
xmlt xml("module");
24+
xml.new_element("number").data = std::to_string(count); // will go away
25+
xml.set_attribute("number", std::to_string(count));
26+
27+
xmlt &l = xml.new_element();
28+
convert(module.source_location, l);
29+
l.name = "location";
30+
31+
// these go away
32+
xml.new_element("identifier").data = id2string(module.identifier);
33+
xml.new_element("mode").data = id2string(module.mode);
34+
xml.new_element("name").data = id2string(module.display_name);
35+
36+
// these stay
37+
xml.set_attribute("identifier", id2string(module.identifier));
38+
xml.set_attribute("mode", id2string(module.mode));
39+
xml.set_attribute("name", id2string(module.display_name));
40+
41+
out << xml;
42+
}
43+
}
44+
45+
void show_modulest::plain_text(std::ostream &out) const
46+
{
47+
std::size_t count = 0;
48+
49+
for(const auto &module : modules)
50+
{
51+
count++;
52+
53+
out << "Module " << count << ":" << '\n';
54+
55+
out << " Location: " << module.source_location << '\n';
56+
out << " Mode: " << module.mode << '\n';
57+
out << " Identifier: " << module.identifier << '\n';
58+
out << " Name: " << module.display_name << '\n' << '\n';
59+
}
60+
}
61+
62+
void show_modulest::json(std::ostream &out) const
63+
{
64+
json_arrayt json_modules;
65+
66+
for(const auto &module : modules)
67+
{
68+
json_objectt json_module;
69+
json_module["location"] = ::json(module.source_location);
70+
json_module["identifier"] = json_stringt{id2string(module.identifier)};
71+
json_module["mode"] = json_stringt{id2string(module.mode)};
72+
json_module["name"] = json_stringt{id2string(module.display_name)};
73+
74+
json_modules.push_back(std::move(json_module));
75+
}
76+
77+
out << json_modules;
78+
}
79+
80+
show_modulest
81+
show_modulest::from_symbol_table(const symbol_table_baset &symbol_table)
82+
{
83+
show_modulest show_modules;
84+
85+
for(const auto &s : symbol_table.symbols)
86+
{
87+
const symbolt &symbol = s.second;
88+
89+
if(symbol.type.id() == ID_module)
90+
{
91+
show_modules.modules.emplace_back(
92+
symbol.name, symbol.display_name(), symbol.mode, symbol.location);
93+
}
94+
}
95+
96+
return show_modules;
97+
}

‎src/ebmc/show_modules.h‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
/*******************************************************************\
2+
3+
Module: Show Modules
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_EBMC_SHOW_MODULES_H
10+
#define CPROVER_EBMC_SHOW_MODULES_H
11+
12+
#include <util/source_location.h>
13+
14+
#include <iosfwd>
15+
#include <list>
16+
#include <string>
17+
18+
class symbol_table_baset;
19+
20+
class show_modulest
21+
{
22+
public:
23+
struct modulet
24+
{
25+
modulet(
26+
irep_idt _identifier,
27+
irep_idt _display_name,
28+
irep_idt _mode,
29+
source_locationt _source_location)
30+
: identifier(_identifier),
31+
display_name(_display_name),
32+
mode(_mode),
33+
source_location(std::move(_source_location))
34+
{
35+
}
36+
37+
irep_idt identifier, display_name, mode;
38+
source_locationt source_location;
39+
};
40+
41+
using modulest = std::list<modulet>;
42+
modulest modules;
43+
44+
void plain_text(std::ostream &) const;
45+
void xml(std::ostream &) const;
46+
void json(std::ostream &) const;
47+
48+
static show_modulest from_symbol_table(const symbol_table_baset &);
49+
};
50+
51+
#endif

‎src/ebmc/transition_system.cpp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected]
2020
#include <langapi/language_util.h>
2121
#include <langapi/mode.h>
2222
#include <trans-word-level/show_module_hierarchy.h>
23-
#include <trans-word-level/show_modules.h>
2423
#include <verilog/verilog_types.h>
2524

2625
#include "ebmc_error.h"

‎src/hw-cbmc/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \
3434
$(CPROVER_DIR)/solvers/solvers$(LIBEXT) \
3535
$(CPROVER_DIR)/util/util$(LIBEXT) \
3636
$(CPROVER_DIR)/json/json$(LIBEXT) \
37+
../ebmc/show_modules$(OBJEXT) \
3738
../temporal-logic/temporal-logic$(LIBEXT) \
3839
../trans-netlist/trans_trace$(OBJEXT) \
3940
../trans-word-level/trans-word-level$(LIBEXT)

‎src/hw-cbmc/hw_cbmc_parse_options.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,12 +19,12 @@ Author: Daniel Kroening, [email protected]
1919
#include <goto-programs/show_properties.h>
2020

2121
#include <ansi-c/goto-conversion/goto_convert_functions.h>
22+
#include <ebmc/show_modules.h>
2223
#include <goto-checker/all_properties_verifier_with_trace_storage.h>
2324
#include <goto-checker/goto_verifier.h>
2425
#include <goto-checker/multi_path_symex_checker.h>
2526
#include <goto-checker/solver_factory.h>
2627
#include <langapi/mode.h>
27-
#include <trans-word-level/show_modules.h>
2828
#include <trans-word-level/trans_trace_word_level.h>
2929
#include <trans-word-level/unwind.h>
3030

@@ -246,7 +246,8 @@ int hw_cbmc_parse_optionst::get_modules(std::list<exprt> &bmc_constraints) {
246246
}
247247
else if(cmdline.isset("show-modules"))
248248
{
249-
show_modules(goto_model.symbol_table, std::cout);
249+
show_modulest::from_symbol_table(goto_model.symbol_table)
250+
.plain_text(std::cout);
250251
return 0; // done
251252
}
252253

‎src/smvlang/smv_ebmc_language.cpp‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ Author: Daniel Kroening, [email protected]
1616
#include <util/unicode.h>
1717

1818
#include <ebmc/ebmc_error.h>
19+
#include <ebmc/output_file.h>
20+
#include <ebmc/show_modules.h>
1921
#include <ebmc/transition_system.h>
2022

2123
#include "smv_parser.h"
@@ -70,31 +72,30 @@ std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
7072
return {};
7173
}
7274

73-
if(cmdline.isset("show-modules"))
75+
if(
76+
cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
77+
cmdline.isset("json-modules"))
7478
{
75-
std::size_t count = 0;
76-
auto &out = std::cout;
79+
show_modulest show_modules;
7780

7881
for(const auto &module : parse_tree.module_list)
79-
{
80-
count++;
82+
show_modules.modules.emplace_back(
83+
module.name, module.base_name, "SMV", module.source_location);
8184

82-
out << "Module " << count << ":" << '\n';
85+
auto filename = cmdline.value_opt("outfile").value_or("-");
86+
output_filet output_file{filename};
87+
auto &out = output_file.stream();
8388

84-
out << " Location: " << module.source_location << '\n';
85-
out << " Identifier: " << module.name << '\n';
86-
out << " Name: " << module.base_name << '\n' << '\n';
87-
}
89+
if(cmdline.isset("show-modules"))
90+
show_modules.plain_text(out);
91+
else if(cmdline.isset("modules-xml"))
92+
show_modules.xml(out);
93+
else if(cmdline.isset("json-modules"))
94+
show_modules.json(out);
8895

8996
return {};
9097
}
9198

92-
if(cmdline.isset("modules-xml") || cmdline.isset("json-modules"))
93-
{
94-
//show_modules(cmdline, message_handler);
95-
return {};
96-
}
97-
9899
if(cmdline.isset("show-module-hierarchy"))
99100
{
100101
//show_module_hierarchy(cmdline, message_handler);

0 commit comments

Comments
 (0)