Skip to content

Commit 5b05f18

Browse files
FrNecasFrNecas
committed
Workaround removed property_checkert
Signed-off-by: František Nečas <[email protected]>
1 parent b11501d commit 5b05f18

13 files changed

+143
-94
lines changed

‎src/2ls/2ls_parse_options.cpp

Lines changed: 40 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ Author: Daniel Kroening, Peter Schrammel
6969
#define FILTER_ASSERTIONS 1
7070

7171
twols_parse_optionst::twols_parse_optionst(int argc, const char **argv):
72-
parse_options_baset(TWOLS_OPTIONS, argc, argv),
72+
parse_options_baset(TWOLS_OPTIONS, argc, argv, "2LS " TWOLS_VERSION),
7373
messaget(ui_message_handler),
7474
ui_message_handler(cmdline, "2LS " TWOLS_VERSION),
7575
recursion_detected(false),
@@ -630,34 +630,43 @@ int twols_parse_optionst::doit()
630630
// do actual analysis
631631
switch((*checker)(goto_model))
632632
{
633-
case property_checkert::resultt::PASS:
633+
case resultt::PASS:
634634
if(report_assertions)
635-
report_properties(options, goto_model, checker->property_map);
635+
report_properties(
636+
options,
637+
goto_model,
638+
checker->property_map,
639+
checker->traces);
636640
report_success();
637641
if(cmdline.isset("graphml-witness"))
638642
output_graphml_proof(options, goto_model, *checker);
639643
retval=0;
640644
break;
641645

642-
case property_checkert::resultt::FAIL:
646+
case resultt::FAIL:
643647
{
644648
if(report_assertions)
645-
report_properties(options, goto_model, checker->property_map);
649+
report_properties(
650+
options,
651+
goto_model,
652+
checker->property_map,
653+
checker->traces);
646654

647655
// validate trace
648656
bool trace_valid=false;
649657
for(const auto &p : checker->property_map)
650658
{
651-
if(p.second.result!=property_checkert::resultt::FAIL)
659+
if(p.second.status!=property_statust::FAIL)
652660
continue;
653661

662+
goto_tracet trace=checker->traces[p.first];
654663
if(options.get_bool_option("trace"))
655-
show_counterexample(goto_model, p.second.error_trace);
664+
show_counterexample(goto_model, trace);
656665

657666
trace_valid=
658-
!p.second.error_trace.steps.empty() &&
667+
!trace.steps.empty() &&
659668
(options.get_bool_option("nontermination") ||
660-
p.second.error_trace.steps.back().is_assert());
669+
trace.steps.back().is_assert());
661670
break;
662671
}
663672

@@ -678,9 +687,13 @@ int twols_parse_optionst::doit()
678687
retval=10;
679688
break;
680689
}
681-
case property_checkert::resultt::UNKNOWN:
690+
case resultt::UNKNOWN:
682691
if(report_assertions)
683-
report_properties(options, goto_model, checker->property_map);
692+
report_properties(
693+
options,
694+
goto_model,
695+
checker->property_map,
696+
checker->traces);
684697
retval=5;
685698
report_unknown();
686699
break;
@@ -1179,9 +1192,10 @@ bool twols_parse_optionst::process_goto_program(
11791192
void twols_parse_optionst::report_properties(
11801193
const optionst &options,
11811194
const goto_modelt &goto_model,
1182-
const property_checkert::property_mapt &property_map)
1195+
const propertiest &property_map,
1196+
const tracest &traces)
11831197
{
1184-
for(property_checkert::property_mapt::const_iterator
1198+
for(propertiest::const_iterator
11851199
it=property_map.begin();
11861200
it!=property_map.end();
11871201
it++)
@@ -1193,7 +1207,7 @@ void twols_parse_optionst::report_properties(
11931207
#endif
11941208

11951209
if(!options.get_bool_option("all-properties") &&
1196-
it->second.result!=property_checkert::resultt::FAIL)
1210+
it->second.status!=property_statust::FAIL)
11971211
continue;
11981212

11991213
if(ui_message_handler.get_ui()==ui_message_handlert::uit::XML_UI)
@@ -1202,27 +1216,27 @@ void twols_parse_optionst::report_properties(
12021216
xml_result.set_attribute("property", id2string(it->first));
12031217
xml_result.set_attribute(
12041218
"status",
1205-
property_checkert::as_string(it->second.result));
1219+
as_string(it->second.status));
12061220
std::cout << xml_result << "\n";
12071221
}
12081222
else
12091223
{
12101224
status() << "[" << it->first << "] "
1211-
<< it->second.location->source_location.get_comment()
1225+
<< it->second.pc->source_location.get_comment()
12121226
<< ": "
1213-
<< property_checkert::as_string(it->second.result)
1227+
<< as_string(it->second.status)
12141228
<< eom;
12151229
}
12161230

12171231
if(options.get_bool_option("trace") &&
1218-
it->second.result==property_checkert::resultt::FAIL)
1219-
show_counterexample(goto_model, it->second.error_trace);
1232+
it->second.status==property_statust::FAIL)
1233+
show_counterexample(goto_model, traces.at(it->first));
12201234
if(cmdline.isset("json-cex") &&
1221-
it->second.result==property_checkert::resultt::FAIL)
1235+
it->second.status==property_statust::FAIL)
12221236
output_json_cex(
12231237
options,
12241238
goto_model,
1225-
it->second.error_trace,
1239+
traces.at(it->first),
12261240
id2string(it->first));
12271241
}
12281242

@@ -1233,14 +1247,14 @@ void twols_parse_optionst::report_properties(
12331247
unsigned failed=0;
12341248
unsigned unknown=0;
12351249

1236-
for(property_checkert::property_mapt::const_iterator
1250+
for(propertiest::const_iterator
12371251
it=property_map.begin();
12381252
it!=property_map.end();
12391253
it++)
12401254
{
1241-
if(it->second.result==property_checkert::resultt::UNKNOWN)
1255+
if(it->second.status==property_statust::UNKNOWN)
12421256
unknown++;
1243-
if(it->second.result==property_checkert::resultt::FAIL)
1257+
if(it->second.status==property_statust::FAIL)
12441258
failed++;
12451259
}
12461260

@@ -1309,15 +1323,15 @@ void twols_parse_optionst::output_graphml_cex(
13091323
{
13101324
for(const auto &p : summary_checker.property_map)
13111325
{
1312-
if(p.second.result!=property_checkert::resultt::FAIL)
1326+
if(p.second.status!=property_statust::FAIL)
13131327
continue;
13141328

13151329
const namespacet ns(goto_model.symbol_table);
13161330
const std::string graphml=options.get_option("graphml-witness");
13171331
if(!graphml.empty())
13181332
{
13191333
graphml_witnesst graphml_witness(ns);
1320-
graphml_witness(p.second.error_trace);
1334+
graphml_witness(summary_checker.traces.at(p.first));
13211335

13221336
if(graphml=="-")
13231337
write_graphml(graphml_witness.graph(), std::cout);

‎src/2ls/2ls_parse_options.h

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,8 @@ class twols_parse_optionst:
102102
void report_properties(
103103
const optionst &options,
104104
const goto_modelt &,
105-
const summary_checker_baset::property_mapt &);
105+
const propertiest &,
106+
const tracest &traces);
106107

107108
void show_counterexample(
108109
const goto_modelt &,

‎src/2ls/cover_goals_ext.cpp

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -130,14 +130,14 @@ void cover_goals_extt::assignment()
130130
for(goal_mapt::const_iterator it=goal_map.begin();
131131
it!=goal_map.end(); it++, g_it++)
132132
{
133-
if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
133+
if(property_map.at(it->first).status==property_statust::UNKNOWN &&
134134
solver.l_get(g_it->condition).is_true())
135135
{
136-
property_map[it->first].result=property_checkert::resultt::FAIL;
136+
property_map.at(it->first).status=property_statust::FAIL;
137137
if(build_error_trace)
138138
{
139139
ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
140-
build_goto_trace(property_map[it->first].error_trace);
140+
build_goto_trace(traces[it->first]);
141141
if(!all_properties)
142142
break;
143143
}
@@ -159,14 +159,14 @@ void cover_goals_extt::assignment()
159159
for(goal_mapt::const_iterator it=goal_map.begin();
160160
it!=goal_map.end(); it++, g_it++)
161161
{
162-
if(property_map[it->first].result==property_checkert::resultt::UNKNOWN &&
162+
if(property_map.at(it->first).status==property_statust::UNKNOWN &&
163163
solver.l_get(g_it->condition).is_true())
164164
{
165-
property_map[it->first].result=property_checkert::resultt::FAIL;
165+
property_map.at(it->first).status=property_statust::FAIL;
166166
if(build_error_trace)
167167
{
168168
ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver());
169-
build_goto_trace(property_map[it->first].error_trace);
169+
build_goto_trace(traces[it->first]);
170170

171171
#if 0
172172
show_raw_countermodel(

‎src/2ls/cover_goals_ext.h

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,12 @@ Author: Daniel Kroening, [email protected]
1313
#define CPROVER_2LS_2LS_COVER_GOALS_EXT_H
1414

1515
#include <util/message.h>
16-
#include <goto-programs/property_checker.h>
16+
#include <goto-checker/properties.h>
1717

1818
#include "../ssa/local_ssa.h"
1919
#include "../ssa/unwindable_local_ssa.h"
2020
#include "../domains/incremental_solver.h"
21+
#include "types.h"
2122

2223
/// Try to cover some given set of goals incrementally. This can be seen as a
2324
/// heuristic variant of SAT-based set-cover. No minimality guarantee.
@@ -46,13 +47,15 @@ class cover_goals_extt:public messaget
4647
unwindable_local_SSAt &_SSA,
4748
incremental_solvert &_solver,
4849
const exprt::operandst& _loophead_selects,
49-
property_checkert::property_mapt &_property_map,
50+
propertiest &_property_map,
51+
tracest &_traces,
5052
bool _spurious_check,
5153
bool _all_properties,
5254
bool _build_error_trace):
5355
SSA(_SSA),
5456
solver(_solver),
5557
property_map(_property_map),
58+
traces(_traces),
5659
spurious_check(_spurious_check),
5760
all_properties(_all_properties),
5861
build_error_trace(_build_error_trace),
@@ -111,7 +114,8 @@ class cover_goals_extt:public messaget
111114
unwindable_local_SSAt &SSA;
112115
unsigned _number_covered, _iterations;
113116
incremental_solvert &solver;
114-
property_checkert::property_mapt &property_map;
117+
propertiest &property_map;
118+
tracest &traces;
115119
bool spurious_check, all_properties, build_error_trace;
116120
exprt::operandst loophead_selects;
117121

‎src/2ls/summary_checker_ai.cpp

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Author: Peter Schrammel
1212
#include "summary_checker_ai.h"
1313
#include <ssa/ssa_build_goto_trace.h>
1414

15-
property_checkert::resultt summary_checker_ait::operator()(
15+
resultt summary_checker_ait::operator()(
1616
const goto_modelt &goto_model)
1717
{
1818
SSA_functions(goto_model, goto_model.symbol_table);
@@ -30,9 +30,9 @@ property_checkert::resultt summary_checker_ait::operator()(
3030
}
3131

3232
// properties
33-
initialize_property_map(goto_model.goto_functions);
33+
property_map=initialize_properties(goto_model);
3434

35-
property_checkert::resultt result=property_checkert::resultt::UNKNOWN;
35+
resultt result=resultt::UNKNOWN;
3636
bool finished=false;
3737
while(!finished)
3838
{
@@ -54,7 +54,7 @@ property_checkert::resultt summary_checker_ait::operator()(
5454
{
5555
report_statistics();
5656
report_preconditions();
57-
return property_checkert::resultt::UNKNOWN;
57+
return resultt::UNKNOWN;
5858
}
5959

6060
if(termination)
@@ -65,13 +65,13 @@ property_checkert::resultt summary_checker_ait::operator()(
6565

6666
#ifdef SHOW_CALLINGCONTEXTS
6767
if(options.get_bool_option("show-calling-contexts"))
68-
return property_checkert::resultt::UNKNOWN;
68+
return resultt::UNKNOWN;
6969
#endif
7070

7171
result=check_properties();
7272
report_statistics();
7373

74-
if(result==property_checkert::resultt::UNKNOWN &&
74+
if(result==resultt::UNKNOWN &&
7575
options.get_bool_option("values-refine") &&
7676
options.get_bool_option("intervals"))
7777
{
@@ -110,7 +110,7 @@ void summary_checker_ait::report_preconditions()
110110
}
111111
}
112112

113-
property_checkert::resultt summary_checker_ait::report_termination()
113+
resultt summary_checker_ait::report_termination()
114114
{
115115
result() << eom;
116116
result() << "** Termination: " << eom;
@@ -134,17 +134,17 @@ property_checkert::resultt summary_checker_ait::report_termination()
134134
<< (!computed ? "not computed" : threeval2string(terminates)) << eom;
135135
}
136136
if(not_computed)
137-
return property_checkert::resultt::UNKNOWN;
137+
return resultt::UNKNOWN;
138138
if(all_terminate)
139-
return property_checkert::resultt::PASS;
139+
return resultt::PASS;
140140
if(one_nonterminate)
141141
{
142142
#if 0
143-
return property_checkert::resultt::FAIL;
143+
return resultt::FAIL;
144144
#else
145145
// rely on nontermination checker to find counterexample
146-
return property_checkert::resultt::UNKNOWN;
146+
return resultt::UNKNOWN;
147147
#endif
148148
}
149-
return property_checkert::resultt::UNKNOWN;
149+
return resultt::UNKNOWN;
150150
}

‎src/2ls/summary_checker_ai.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ class summary_checker_ait:public summary_checker_baset
2424

2525
protected:
2626
void report_preconditions();
27-
property_checkert::resultt report_termination();
27+
resultt report_termination();
2828
};
2929

3030
#endif

0 commit comments

Comments
 (0)