Skip to content

Commit 3574aa1

Browse files
kroeningkroening
committed
ebmc: replace ebmc_baset in main flow
This replaces the use of ebmc_baset in the main property checking flow by using a direct call to ebmc_propertiest::from_command_line.
1 parent c50315a commit 3574aa1

File tree

5 files changed

+120
-105
lines changed

5 files changed

+120
-105
lines changed

‎src/ebmc/ebmc_base.cpp‎

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -56,18 +56,6 @@ int ebmc_baset::get_properties()
5656
properties = ebmc_propertiest::from_command_line(
5757
cmdline, transition_system, message.get_message_handler());
5858

59-
if(cmdline.isset("show-properties"))
60-
{
61-
show_properties();
62-
return 0;
63-
}
64-
65-
if(cmdline.isset("json-properties"))
66-
{
67-
json_properties(cmdline.get_value("json-properties"));
68-
return 0;
69-
}
70-
7159
return -1; // done
7260
}
7361

‎src/ebmc/ebmc_base.h‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,6 @@ class ebmc_baset
4747

4848
bool parse_property(const std::string &property);
4949
bool get_model_properties();
50-
void show_properties();
51-
void json_properties(const std::string &file_name);
5250

5351
bool parse();
5452
bool parse(const std::string &filename);

‎src/ebmc/ebmc_parse_options.cpp‎

Lines changed: 87 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ Author: Daniel Kroening, [email protected]
2424
#include "property_checker.h"
2525
#include "random_traces.h"
2626
#include "ranking_function.h"
27+
#include "show_properties.h"
2728
#include "show_trans.h"
2829

2930
#include <iostream>
@@ -210,94 +211,97 @@ int ebmc_parse_optionst::doit()
210211
// get the transition system
211212
auto transition_system = get_transition_system(cmdline, ui_message_handler);
212213

214+
// get the properties
215+
auto properties = ebmc_propertiest::from_command_line(
216+
cmdline, transition_system, ui_message_handler);
217+
218+
if(cmdline.isset("show-properties"))
219+
{
220+
show_properties(properties, ui_message_handler);
221+
return 0;
222+
}
223+
224+
if(cmdline.isset("json-properties"))
225+
{
226+
json_properties(properties, cmdline.get_value("json-properties"));
227+
return 0;
228+
}
229+
230+
// possibly apply liveness-to-safety
231+
if(cmdline.isset("liveness-to-safety"))
232+
liveness_to_safety(transition_system, properties);
233+
234+
if(cmdline.isset("show-varmap"))
235+
{
236+
auto netlist =
237+
make_netlist(transition_system, properties, ui_message_handler);
238+
netlist.var_map.output(std::cout);
239+
return 0;
240+
}
241+
242+
if(cmdline.isset("show-ldg"))
213243
{
214244
ebmc_baset ebmc_base(cmdline, ui_message_handler);
215245
ebmc_base.transition_system = std::move(transition_system);
246+
ebmc_base.properties = std::move(properties);
247+
ebmc_base.show_ldg(std::cout);
248+
return 0;
249+
}
250+
251+
if(cmdline.isset("show-netlist"))
252+
{
253+
auto netlist =
254+
make_netlist(transition_system, properties, ui_message_handler);
255+
netlist.print(std::cout);
256+
return 0;
257+
}
258+
259+
if(cmdline.isset("dot-netlist"))
260+
{
261+
auto netlist =
262+
make_netlist(transition_system, properties, ui_message_handler);
263+
auto filename = cmdline.value_opt("outfile").value_or("-");
264+
output_filet outfile{filename};
265+
outfile.stream() << "digraph netlist {\n";
266+
netlist.output_dot(outfile.stream());
267+
outfile.stream() << "}\n";
268+
return 0;
269+
}
270+
271+
if(cmdline.isset("smv-netlist"))
272+
{
273+
auto netlist =
274+
make_netlist(transition_system, properties, ui_message_handler);
275+
auto filename = cmdline.value_opt("outfile").value_or("-");
276+
output_filet outfile{filename};
277+
outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
278+
outfile.stream() << "-- Generated from "
279+
<< transition_system.main_symbol->name << '\n';
280+
outfile.stream() << '\n';
281+
netlist.output_smv(outfile.stream());
282+
return 0;
283+
}
216284

217-
auto result = ebmc_base.get_properties();
218-
219-
if(result != -1)
220-
return result;
221-
222-
// possibly apply liveness-to-safety
223-
if(cmdline.isset("liveness-to-safety"))
224-
liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties);
225-
226-
if(cmdline.isset("show-varmap"))
227-
{
228-
netlistt netlist;
229-
if(ebmc_base.make_netlist(netlist))
230-
return 1;
231-
netlist.var_map.output(std::cout);
232-
return 0;
233-
}
234-
235-
if(cmdline.isset("show-ldg"))
236-
{
237-
ebmc_base.show_ldg(std::cout);
238-
return 0;
239-
}
240-
241-
if(cmdline.isset("show-netlist"))
242-
{
243-
netlistt netlist;
244-
if(ebmc_base.make_netlist(netlist))
245-
return 1;
246-
netlist.print(std::cout);
247-
return 0;
248-
}
249-
250-
if(cmdline.isset("dot-netlist"))
251-
{
252-
netlistt netlist;
253-
if(ebmc_base.make_netlist(netlist))
254-
return 1;
255-
auto filename = cmdline.value_opt("outfile").value_or("-");
256-
output_filet outfile{filename};
257-
outfile.stream() << "digraph netlist {\n";
258-
netlist.output_dot(outfile.stream());
259-
outfile.stream() << "}\n";
260-
return 0;
261-
}
262-
263-
if(cmdline.isset("smv-netlist"))
264-
{
265-
netlistt netlist;
266-
if(ebmc_base.make_netlist(netlist))
267-
return 1;
268-
auto filename = cmdline.value_opt("outfile").value_or("-");
269-
output_filet outfile{filename};
270-
outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n';
271-
outfile.stream() << "-- Generated from "
272-
<< ebmc_base.transition_system.main_symbol->name
273-
<< '\n';
274-
outfile.stream() << '\n';
275-
netlist.output_smv(outfile.stream());
276-
return 0;
277-
}
278-
279-
if(cmdline.isset("cegar"))
280-
{
281-
auto netlist = make_netlist(
282-
ebmc_base.transition_system,
283-
ebmc_base.properties,
284-
ui_message_handler);
285-
const namespacet ns(ebmc_base.transition_system.symbol_table);
286-
return do_bmc_cegar(
287-
netlist, ebmc_base.properties, ns, ui_message_handler);
288-
}
289-
290-
if(cmdline.isset("compute-ct"))
291-
return ebmc_base.do_compute_ct();
292-
293-
auto checker_result = property_checker(
294-
cmdline,
295-
ebmc_base.transition_system,
296-
ebmc_base.properties,
297-
ui_message_handler);
298-
299-
return checker_result.exit_code();
285+
if(cmdline.isset("cegar"))
286+
{
287+
auto netlist =
288+
make_netlist(transition_system, properties, ui_message_handler);
289+
const namespacet ns(transition_system.symbol_table);
290+
return do_bmc_cegar(netlist, properties, ns, ui_message_handler);
300291
}
292+
293+
if(cmdline.isset("compute-ct"))
294+
{
295+
ebmc_baset ebmc_base(cmdline, ui_message_handler);
296+
ebmc_base.transition_system = std::move(transition_system);
297+
ebmc_base.properties = std::move(properties);
298+
return ebmc_base.do_compute_ct();
299+
}
300+
301+
auto checker_result = property_checker(
302+
cmdline, transition_system, properties, ui_message_handler);
303+
304+
return checker_result.exit_code();
301305
}
302306
catch(const ebmc_errort &ebmc_error)
303307
{

‎src/ebmc/show_properties.cpp‎

Lines changed: 13 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,25 +1,27 @@
11
/*******************************************************************\
22
3-
Module: Base for Verification Modules
3+
Module: Show Properties
44
55
Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9+
#include "show_properties.h"
10+
911
#include <util/json.h>
1012
#include <util/json_irep.h>
1113
#include <util/xml.h>
1214
#include <util/xml_irep.h>
1315

14-
#include "ebmc_base.h"
1516
#include "ebmc_error.h"
17+
#include "ebmc_properties.h"
1618
#include "output_file.h"
1719

1820
#include <iostream>
1921

2022
/*******************************************************************\
2123
22-
Function: ebmc_baset::show_properties
24+
Function: show_properties
2325
2426
Inputs:
2527
@@ -29,7 +31,9 @@ Function: ebmc_baset::show_properties
2931
3032
\*******************************************************************/
3133

32-
void ebmc_baset::show_properties()
34+
void show_properties(
35+
const ebmc_propertiest &properties,
36+
ui_message_handlert &message_handler)
3337
{
3438
unsigned p_nr=1;
3539

@@ -49,8 +53,7 @@ void ebmc_baset::show_properties()
4953

5054
for(const auto &p : properties.properties)
5155
{
52-
switch(static_cast<ui_message_handlert &>(message.get_message_handler())
53-
.get_ui())
56+
switch(message_handler.get_ui())
5457
{
5558
case ui_message_handlert::uit::XML_UI:
5659
std::cout << make_xml(p, p_nr) << '\n';
@@ -70,7 +73,7 @@ void ebmc_baset::show_properties()
7073

7174
/*******************************************************************\
7275
73-
Function: ebmc_baset::json_properties
76+
Function: json_properties
7477
7578
Inputs:
7679
@@ -80,7 +83,9 @@ Function: ebmc_baset::json_properties
8083
8184
\*******************************************************************/
8285

83-
void ebmc_baset::json_properties(const std::string &file_name)
86+
void json_properties(
87+
const ebmc_propertiest &properties,
88+
const std::string &file_name)
8489
{
8590
json_arrayt json;
8691

‎src/ebmc/show_properties.h‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
/*******************************************************************\
2+
3+
Module: Show Properties
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_EBMC_SHOW_PROPERTIES_H
10+
#define CPROVER_EBMC_SHOW_PROPERTIES_H
11+
12+
#include <string>
13+
14+
class ebmc_propertiest;
15+
class ui_message_handlert;
16+
17+
void show_properties(const ebmc_propertiest &, ui_message_handlert &);
18+
void json_properties(const ebmc_propertiest &, const std::string &file_name);
19+
20+
#endif

0 commit comments

Comments
 (0)