Skip to content

Commit a2ebb33

Browse files
tautschnigtautschnig
authored
Merge pull request diffblue#1713 from karkhaz/kk-debug-timestamps
Emit timestamps on each line of output
2 parents 7b5dd17 + 82549de commit a2ebb33

24 files changed

+242
-345
lines changed

‎src/cbmc/all_properties.cpp

+9-8
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "all_properties_class.h"
1313

14-
#include <util/time_stopping.h>
14+
#include <chrono>
15+
1516
#include <util/xml.h>
1617
#include <util/json.h>
1718

@@ -56,8 +57,8 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
5657

5758
solver.set_message_handler(get_message_handler());
5859

59-
// stop the time
60-
absolute_timet sat_start=current_time();
60+
auto now = std::chrono::steady_clock::now();
61+
auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
6162

6263
bmc.do_conversion();
6364

@@ -131,12 +132,12 @@ safety_checkert::resultt bmc_all_propertiest::operator()()
131132
g.second.status=goalt::statust::SUCCESS;
132133
}
133134

134-
// output runtime
135-
136135
{
137-
absolute_timet sat_stop=current_time();
138-
status() << "Runtime decision procedure: "
139-
<< (sat_stop-sat_start) << "s" << eom;
136+
now = std::chrono::steady_clock::now();
137+
auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
138+
139+
status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
140+
<< "s" << eom;
140141
}
141142

142143
// report

‎src/cbmc/bmc.cpp

+7-7
Original file line numberDiff line numberDiff line change
@@ -11,14 +11,14 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "bmc.h"
1313

14+
#include <chrono>
1415
#include <fstream>
1516
#include <iostream>
1617
#include <memory>
1718

1819
#include <util/string2int.h>
1920
#include <util/source_location.h>
2021
#include <util/string_utils.h>
21-
#include <util/time_stopping.h>
2222
#include <util/message.h>
2323
#include <util/json.h>
2424
#include <util/cprover_prefix.h>
@@ -154,20 +154,20 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
154154

155155
prop_conv.set_message_handler(get_message_handler());
156156

157-
// stop the time
158-
absolute_timet sat_start=current_time();
157+
auto now = std::chrono::steady_clock::now();
158+
auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
159159

160160
do_conversion();
161161

162162
status() << "Running " << prop_conv.decision_procedure_text() << eom;
163163

164164
decision_proceduret::resultt dec_result=prop_conv.dec_solve();
165-
// output runtime
166165

167166
{
168-
absolute_timet sat_stop=current_time();
169-
status() << "Runtime decision procedure: "
170-
<< (sat_stop-sat_start) << "s" << eom;
167+
now = std::chrono::steady_clock::now();
168+
auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
169+
status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
170+
<< "s" << eom;
171171
}
172172

173173
return dec_result;

‎src/cbmc/bmc_cover.cpp

+8-8
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,8 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "bmc.h"
1313

14-
#include <util/time_stopping.h>
14+
#include <chrono>
15+
1516
#include <util/xml.h>
1617
#include <util/xml_expr.h>
1718
#include <util/json.h>
@@ -191,8 +192,8 @@ bool bmc_covert::operator()()
191192

192193
solver.set_message_handler(get_message_handler());
193194

194-
// stop the time
195-
absolute_timet sat_start=current_time();
195+
auto now = std::chrono::steady_clock::now();
196+
auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
196197

197198
// Collect _all_ goals in `goal_map'.
198199
// This maps property IDs to 'goalt'
@@ -251,12 +252,11 @@ bool bmc_covert::operator()()
251252

252253
cover_goals();
253254

254-
// output runtime
255-
256255
{
257-
absolute_timet sat_stop=current_time();
258-
status() << "Runtime decision procedure: "
259-
<< (sat_stop-sat_start) << "s" << eom;
256+
now = std::chrono::steady_clock::now();
257+
auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
258+
status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
259+
<< "s" << eom;
260260
}
261261

262262
// report

‎src/cbmc/cbmc_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -1029,6 +1029,7 @@ void cbmc_parse_optionst::help()
10291029
" --json-ui use JSON-formatted output\n"
10301030
HELP_GOTO_TRACE
10311031
" --verbosity # verbosity level\n"
1032+
HELP_TIMESTAMP
10321033
"\n";
10331034
// clang-format on
10341035
}

‎src/cbmc/cbmc_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
17+
#include <util/timestamper.h>
1718

1819
#include <langapi/language.h>
1920

@@ -62,6 +63,7 @@ class optionst;
6263
"(version)" \
6364
"(cover):(symex-coverage-report):" \
6465
"(mm):" \
66+
OPT_TIMESTAMP \
6567
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \
6668
"(ppc-macos)(unsigned-char)" \
6769
"(arrays-uf-always)(arrays-uf-never)" \

‎src/cbmc/fault_localization.cpp

+8-6
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,13 @@ Author: Peter Schrammel
1111

1212
#include "fault_localization.h"
1313

14+
#include <chrono>
15+
1416
#include <util/threeval.h>
1517
#include <util/arith_tools.h>
1618
#include <util/symbol.h>
1719
#include <util/std_expr.h>
1820
#include <util/message.h>
19-
#include <util/time_stopping.h>
2021
#include <util/xml_expr.h>
2122

2223
#include <solvers/prop/minimize.h>
@@ -245,8 +246,8 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
245246

246247
prop_conv.set_message_handler(bmc.get_message_handler());
247248

248-
// stop the time
249-
absolute_timet sat_start=current_time();
249+
auto now = std::chrono::steady_clock::now();
250+
auto sat_start = std::chrono::time_point_cast<std::chrono::seconds>(now);
250251

251252
bmc.do_conversion();
252253

@@ -259,9 +260,10 @@ fault_localizationt::run_decision_procedure(prop_convt &prop_conv)
259260
// output runtime
260261

261262
{
262-
absolute_timet sat_stop=current_time();
263-
status() << "Runtime decision procedure: "
264-
<< (sat_stop-sat_start) << "s" << eom;
263+
now = std::chrono::steady_clock::now();
264+
auto sat_stop = std::chrono::time_point_cast<std::chrono::seconds>(now);
265+
status() << "Runtime decision procedure: " << (sat_stop - sat_start).count()
266+
<< "s" << eom;
265267
}
266268

267269
return dec_result;

‎src/cbmc/symex_coverage.cpp

+6-2
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ Date: March 2016
1313

1414
#include "symex_coverage.h"
1515

16+
#include <chrono>
1617
#include <iostream>
1718
#include <fstream>
1819
#include <sstream>
1920

20-
#include <util/time_stopping.h>
2121
#include <util/xml.h>
2222
#include <util/string2int.h>
2323
#include <util/cprover_prefix.h>
@@ -387,6 +387,10 @@ void symex_coveraget::build_cobertura(
387387
std::string overall_branch_rate_str=
388388
rate(overall_cov.branches_covered, overall_cov.branches_total);
389389

390+
auto now = std::chrono::system_clock::now();
391+
auto current_time = std::chrono::time_point_cast<std::chrono::seconds>(now);
392+
std::time_t tt = std::chrono::system_clock::to_time_t(current_time);
393+
390394
// <coverage line-rate="0.0" branch-rate="0.0" lines-covered="1"
391395
// lines-valid="1" branches-covered="1"
392396
// branches-valid="1" complexity="0.0"
@@ -404,7 +408,7 @@ void symex_coveraget::build_cobertura(
404408
xml_coverage.set_attribute("complexity", "0.0");
405409
xml_coverage.set_attribute("version", "2.1.1");
406410
xml_coverage.set_attribute("timestamp",
407-
std::to_string(current_time().get_t()));
411+
std::to_string(tt));
408412

409413
xmlt &packages=xml_coverage.new_element("packages");
410414

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -906,5 +906,6 @@ void goto_analyzer_parse_optionst::help()
906906
"\n"
907907
"Other options:\n"
908908
" --version show version and exit\n"
909+
HELP_TIMESTAMP
909910
"\n";
910911
}

‎src/goto-analyzer/goto_analyzer_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -103,6 +103,7 @@ Author: Daniel Kroening, [email protected]
103103

104104
#include <util/ui_message.h>
105105
#include <util/parse_options.h>
106+
#include <util/timestamper.h>
106107

107108
#include <langapi/language.h>
108109

@@ -135,6 +136,7 @@ class optionst;
135136
"(show-local-may-alias)" \
136137
"(json):(xml):" \
137138
"(text):(dot):" \
139+
OPT_TIMESTAMP \
138140
"(unreachable-instructions)(unreachable-functions)" \
139141
"(reachable-functions)" \
140142
"(intervals)(show-intervals)" \

‎src/goto-diff/goto_diff_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -501,5 +501,6 @@ void goto_diff_parse_optionst::help()
501501
"Other options:\n"
502502
" --version show version and exit\n"
503503
" --json-ui use JSON-formatted output\n"
504+
HELP_TIMESTAMP
504505
"\n";
505506
}

‎src/goto-diff/goto_diff_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Peter Schrammel
1414

1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
17+
#include <util/timestamper.h>
1718

1819
#include <goto-programs/goto_model.h>
1920
#include <goto-programs/show_goto_functions.h>
@@ -27,6 +28,7 @@ class optionst;
2728
"(json-ui)" \
2829
OPT_SHOW_GOTO_FUNCTIONS \
2930
"(verbosity):(version)" \
31+
OPT_TIMESTAMP \
3032
"u(unified)(change-impact)(forward-impact)(backward-impact)" \
3133
"(compact-output)"
3234

‎src/goto-instrument/goto_instrument_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -1568,5 +1568,6 @@ void goto_instrument_parse_optionst::help()
15681568
" --version show version and exit\n"
15691569
" --xml-ui use XML-formatted output\n"
15701570
" --json-ui use JSON-formatted output\n"
1571+
HELP_TIMESTAMP
15711572
"\n";
15721573
}

‎src/goto-instrument/goto_instrument_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
17+
#include <util/timestamper.h>
1718

1819
#include <goto-programs/goto_functions.h>
1920
#include <goto-programs/show_goto_functions.h>
@@ -66,6 +67,7 @@ Author: Daniel Kroening, [email protected]
6667
"(show-claims)(show-properties)(property):" \
6768
"(show-symbol-table)(show-points-to)(show-rw-set)" \
6869
"(cav11)" \
70+
OPT_TIMESTAMP \
6971
"(show-natural-loops)(accelerate)(havoc-loops)" \
7072
"(error-label):(string-abstraction)" \
7173
"(verbosity):(version)(xml-ui)(json-ui)(show-loops)" \

‎src/jbmc/jbmc_parse_options.cpp

+1
Original file line numberDiff line numberDiff line change
@@ -956,5 +956,6 @@ void jbmc_parse_optionst::help()
956956
" --json-ui use JSON-formatted output\n"
957957
HELP_GOTO_TRACE
958958
" --verbosity # verbosity level\n"
959+
HELP_TIMESTAMP
959960
"\n";
960961
}

‎src/jbmc/jbmc_parse_options.h

+2
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414

1515
#include <util/ui_message.h>
1616
#include <util/parse_options.h>
17+
#include <util/timestamper.h>
1718

1819
#include <langapi/language.h>
1920

@@ -60,6 +61,7 @@ class optionst;
6061
"(verbosity):" \
6162
"(version)" \
6263
"(cover):(symex-coverage-report):" \
64+
OPT_TIMESTAMP \
6365
"(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)" \
6466
"(ppc-macos)" \
6567
"(arrays-uf-always)(arrays-uf-never)" \

‎src/util/Makefile

+1-2
Original file line numberDiff line numberDiff line change
@@ -84,8 +84,7 @@ SRC = arith_tools.cpp \
8484
tempdir.cpp \
8585
tempfile.cpp \
8686
threeval.cpp \
87-
time_stopping.cpp \
88-
timer.cpp \
87+
timestamper.cpp \
8988
type.cpp \
9089
type_eq.cpp \
9190
typecheck.cpp \

‎src/util/time_stopping.cpp

-69
This file was deleted.

0 commit comments

Comments
 (0)