Skip to content

Commit e9e3659

Browse files
tautschnigtautschnig
authored
Merge pull request #6475 from martin-cs/tidy/goto-instrument-options
Tidying up the options for goto-instrument
2 parents 7eceeb5 + b71a830 commit e9e3659

File tree

18 files changed

+192
-54
lines changed

18 files changed

+192
-54
lines changed

‎regression/cbmc-cpp/Overloading_Operators16/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
main.cpp
3-
--no-pointer-check
3+
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-cpp/virtual11/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
main.cpp
3-
--unwind 1 --no-pointer-check
3+
--unwind 1
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-cpp/virtual12/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
main.cpp
3-
--unwind 1 --no-pointer-check
3+
--unwind 1
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/cbmc-cpp/virtual3/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
KNOWNBUG
22
main.cpp
3-
--no-pointer-check
3+
44
^EXIT=0$
55
^SIGNAL=0$
66
^VERIFICATION SUCCESSFUL$

‎regression/goto-instrument/document-properties-basic/html.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--document-properties-html
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^<em> assert\(1 == 1\);<\/em>$
7+
--
8+
^warning: ignoring
9+
--
10+
Tests whether this option works at all.

‎regression/goto-instrument/document-properties-basic/latex.desc

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--document-properties-latex
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\\claim\{assertion 1 == 1\}$
7+
--
8+
^warning: ignoring
9+
--
10+
Tests whether this option works at all.

‎regression/goto-instrument/document-properties-basic/main.c

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
#include <assert.h>
2+
3+
int main(int argc, char **argv)
4+
{
5+
assert(1 == 1);
6+
7+
return 0;
8+
}

‎regression/goto-instrument/uninitialized-check/main.c

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
#include <stdlib.h>
2+
3+
int globals_are_actually_initialized; // See ISO-9899!
4+
5+
int main(int argc, char **argv)
6+
{
7+
int definitely_uninitialized;
8+
int maybe_uninitialized;
9+
int actually_initialized;
10+
11+
if(argc > 1)
12+
{
13+
maybe_uninitialized = 1;
14+
}
15+
16+
if(argc <= 3)
17+
{
18+
actually_initialized = 0;
19+
}
20+
if(argc >= 4)
21+
{
22+
actually_initialized = 1;
23+
}
24+
25+
int *heap_variables_uninitialized = malloc(sizeof(int));
26+
27+
return definitely_uninitialized + maybe_uninitialized + actually_initialized +
28+
globals_are_actually_initialized + *heap_variables_uninitialized;
29+
}

‎regression/goto-instrument/uninitialized-check/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--uninitialized-check
4+
^\[main.uninitialized_local.1\] line \d+ use of uninitialized local variable main::1::definitely_uninitialized: FAILURE$
5+
^\[main.uninitialized_local.2\] line \d+ use of uninitialized local variable main::1::maybe_uninitialized: FAILURE$
6+
^\[main.uninitialized_local.3\] line \d+ use of uninitialized local variable main::1::actually_initialized: SUCCESS$
7+
^VERIFICATION FAILED$
8+
^EXIT=10$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--
13+
A basic test of the uninitialized variable check.
14+
In an ideal world there would be a check for heap_variables_uninitialized
15+
that would fail however this is beyond the current scope of the analysis.
16+

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
7070
if(cmdline.isset("cover"))
7171
parse_cover_options(cmdline, options);
7272

73-
if(cmdline.isset("mm"))
74-
options.set_option("mm", cmdline.get_value("mm"));
75-
7673
// all checks supported by goto_check
7774
PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
7875

‎src/goto-instrument/document_properties.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,15 @@ void document_properties_html(
2424
const goto_modelt &,
2525
std::ostream &out);
2626

27+
#define OPT_DOCUMENT_PROPERTIES \
28+
"(document-claims-latex)(document-claims-html)" \
29+
"(document-properties-latex)(document-properties-html)"
30+
31+
// clang-format off
32+
#define HELP_DOCUMENT_PROPERTIES \
33+
" --document-properties-html generate HTML property documentation\n" \
34+
" --document-properties-latex generate Latex property documentation\n"
35+
36+
// clang-format on
37+
2738
#endif // CPROVER_GOTO_INSTRUMENT_DOCUMENT_PROPERTIES_H

‎src/goto-instrument/dump_c.h

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,4 +43,20 @@ void dump_cpp(
4343
const namespacet &ns,
4444
std::ostream &out);
4545

46+
#define OPT_DUMP_C \
47+
"(dump-c)(dump-cpp)" \
48+
"(dump-c-type-header):" \
49+
"(no-system-headers)(use-all-headers)(harness)"
50+
51+
// clang-format off
52+
#define HELP_DUMP_C \
53+
" --dump-c generate C source\n" \
54+
" --dump-c-type-header m generate a C header for types local in m\n" \
55+
" --dump-cpp generate C++ source\n" \
56+
" --no-system-headers generate C source expanding libc includes\n"\
57+
" --use-all-headers generate C source with all includes\n" \
58+
" --harness include input generator in output\n"
59+
60+
// clang-format on
61+
4662
#endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_H

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 8 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,6 @@ Author: Daniel Kroening, [email protected]
5252
#include <goto-programs/write_goto_binary.h>
5353

5454
#include <pointer-analysis/add_failed_symbols.h>
55-
#include <pointer-analysis/goto_program_dereference.h>
5655
#include <pointer-analysis/show_value_sets.h>
5756
#include <pointer-analysis/value_set_analysis.h>
5857

@@ -85,9 +84,7 @@ Author: Daniel Kroening, [email protected]
8584
#include "branch.h"
8685
#include "call_sequences.h"
8786
#include "concurrency.h"
88-
#include "document_properties.h"
8987
#include "dot.h"
90-
#include "dump_c.h"
9188
#include "full_slicer.h"
9289
#include "function.h"
9390
#include "havoc_loops.h"
@@ -110,11 +107,9 @@ Author: Daniel Kroening, [email protected]
110107
#include "stack_depth.h"
111108
#include "thread_instrumentation.h"
112109
#include "undefined_functions.h"
113-
#include "uninitialized.h"
114110
#include "unwind.h"
115111
#include "unwindset.h"
116112
#include "value_set_fi_fp_removal.h"
117-
#include "wmm/weak_memory.h"
118113

119114
/// invoke main modules
120115
int goto_instrument_parse_optionst::doit()
@@ -1723,14 +1718,13 @@ void goto_instrument_parse_optionst::help()
17231718
" goto-instrument in out perform instrumentation\n"
17241719
"\n"
17251720
"Main options:\n"
1726-
" --document-properties-html generate HTML property documentation\n"
1727-
" --document-properties-latex generate Latex property documentation\n"
1728-
" --dump-c generate C source\n"
1729-
" --dump-c-type-header m generate a C header for types local in m\n"
1730-
" --dump-cpp generate C++ source\n"
1721+
HELP_DOCUMENT_PROPERTIES
17311722
" --dot generate CFG graph in DOT format\n"
17321723
" --interpreter do concrete execution\n"
17331724
"\n"
1725+
"Dump Source:\n"
1726+
HELP_DUMP_C
1727+
"\n"
17341728
"Diagnosis:\n"
17351729
" --show-loops show the loops in the program\n"
17361730
HELP_SHOW_PROPERTIES
@@ -1763,7 +1757,7 @@ void goto_instrument_parse_optionst::help()
17631757
"Safety checks:\n"
17641758
" --no-assertions ignore user assertions\n"
17651759
HELP_GOTO_CHECK
1766-
" --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*)
1760+
HELP_UNINITIALIZED_CHECK
17671761
" --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
17681762
" --race-check add floating-point data race checks\n"
17691763
"\n"
@@ -1781,7 +1775,7 @@ void goto_instrument_parse_optionst::help()
17811775
" --nondet-static-exclude e same as nondet-static except for the variable e\n" //NOLINT(*)
17821776
" (use multiple times if required)\n"
17831777
" --check-invariant function instruments invariant checking function\n"
1784-
" --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
1778+
HELP_REMOVE_POINTERS
17851779
" --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*)
17861780
" --undefined-function-is-assume-false\n"
17871781
// NOLINTNEXTLINE(whitespace/line_length)
@@ -1799,17 +1793,7 @@ void goto_instrument_parse_optionst::help()
17991793
" --skip-loops <loop-ids> add gotos to skip selected loops during execution\n" // NOLINT(*)
18001794
"\n"
18011795
"Memory model instrumentations:\n"
1802-
" --mm <tso,pso,rmo,power> instruments a weak memory model\n"
1803-
" --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
1804-
" --one-event-per-cycle only instruments one event per cycle\n"
1805-
" --minimum-interference instruments an optimal number of events\n"
1806-
" --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
1807-
" --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
1808-
" --no-dependencies no dependency analysis\n"
1809-
// NOLINTNEXTLINE(whitespace/line_length)
1810-
" --no-po-rendering no representation of the threads in the dot\n"
1811-
" --render-cluster-file clusterises the dot by files\n"
1812-
" --render-cluster-function clusterises the dot by functions\n"
1796+
HELP_WMM_FULL
18131797
"\n"
18141798
"Slicing:\n"
18151799
HELP_REACHABILITY_SLICER
@@ -1854,11 +1838,9 @@ void goto_instrument_parse_optionst::help()
18541838
HELP_ENFORCE_CONTRACT
18551839
"\n"
18561840
"Other options:\n"
1857-
" --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
1858-
" --use-all-headers with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
1859-
" --harness with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
18601841
" --version show version and exit\n"
18611842
HELP_FLUSH
1843+
" --xml output files in XML where supported\n"
18621844
" --xml-ui use XML-formatted output\n"
18631845
" --json-ui use JSON-formatted output\n"
18641846
HELP_TIMESTAMP

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 14 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -28,42 +28,37 @@ Author: Daniel Kroening, [email protected]
2828

2929
#include <analyses/goto_check.h>
3030

31+
#include <pointer-analysis/goto_program_dereference.h>
32+
3133
#include "aggressive_slicer.h"
3234
#include "contracts/contracts.h"
35+
#include "count_eloc.h"
36+
#include "document_properties.h"
37+
#include "dump_c.h"
3338
#include "generate_function_bodies.h"
3439
#include "insert_final_assert_false.h"
3540
#include "nondet_volatile.h"
3641
#include "replace_calls.h"
37-
38-
#include "count_eloc.h"
42+
#include "uninitialized.h"
43+
#include "wmm/weak_memory.h"
3944

4045
// clang-format off
4146
#define GOTO_INSTRUMENT_OPTIONS \
42-
"(all)" \
43-
"(document-claims-latex)(document-claims-html)" \
44-
"(document-properties-latex)(document-properties-html)" \
45-
"(dump-c-type-header):" \
46-
"(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
47-
"(harness)" \
47+
OPT_DOCUMENT_PROPERTIES \
48+
OPT_DUMP_C \
49+
"(dot)(xml)" \
4850
OPT_GOTO_CHECK \
49-
/* no-X-check are deprecated and ignored */ \
50-
"(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
51-
"(no-nan-check)" \
52-
"(remove-pointers)" \
51+
OPT_REMOVE_POINTERS \
5352
"(no-simplify)" \
54-
"(uninitialized-check)" \
55-
"(race-check)(scc)(one-event-per-cycle)" \
56-
"(minimum-interference)" \
57-
"(mm):(my-events)" \
53+
OPT_UNINITIALIZED_CHECK \
54+
OPT_WMM \
55+
"(race-check)" \
5856
"(unwind):(unwindset):(unwindset-file):" \
5957
"(unwinding-assertions)(partial-loops)(continue-as-loops)" \
6058
"(log):" \
61-
"(max-var):(max-po-trans):(ignore-arrays)" \
62-
"(cfg-kill)(no-dependencies)(force-loop-duplication)" \
6359
"(call-graph)(reachable-call-graph)" \
6460
OPT_INSERT_FINAL_ASSERT_FALSE \
6561
OPT_SHOW_CLASS_HIERARCHY \
66-
"(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
6762
"(isr):" \
6863
"(stack-depth):(nondet-static)" \
6964
"(nondet-static-exclude):" \
@@ -87,7 +82,6 @@ Author: Daniel Kroening, [email protected]
8782
"(remove-function-pointers)" \
8883
"(show-claims)(property):" \
8984
"(show-symbol-table)(show-points-to)(show-rw-set)" \
90-
"(cav11)" \
9185
OPT_TIMESTAMP \
9286
"(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
9387
"(string-abstraction)" \

‎src/goto-instrument/uninitialized.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -158,7 +158,7 @@ void uninitializedt::add_assertions(
158158
symbol_exprt(new_identifier, bool_typet()),
159159
instruction.source_location());
160160
assertion.source_location_nonconst().set_comment(
161-
"use of uninitialized local variable");
161+
"use of uninitialized local variable " + id2string(identifier));
162162
assertion.source_location_nonconst().set_property_class(
163163
"uninitialized local");
164164

‎src/goto-instrument/uninitialized.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,4 +24,10 @@ void show_uninitialized(
2424
const goto_modelt &,
2525
std::ostream &out);
2626

27+
#define OPT_UNINITIALIZED_CHECK "(uninitialized-check)"
28+
29+
#define HELP_UNINITIALIZED_CHECK \
30+
" --uninitialized-check add checks for uninitialized locals " \
31+
"(experimental)\n" // NOLINT(whitespace/line_length)
32+
2733
#endif // CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H

‎src/goto-instrument/wmm/weak_memory.h

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,4 +54,55 @@ void introduce_temporaries(
5454
#endif
5555
messaget &message);
5656

57+
// clang-format off
58+
#define OPT_WMM_MEMORY_MODEL "(mm):"
59+
60+
#define OPT_WMM_INSTRUMENTATION_STRATEGIES \
61+
"(one-event-per-cycle)" \
62+
"(minimum-interference)" \
63+
"(read-first)" \
64+
"(write-first)" \
65+
"(my-events)" \
66+
67+
#define OPT_WMM_LIMITS \
68+
"(max-var):" \
69+
"(max-po-trans):" \
70+
71+
#define OPT_WMM_LOOPS \
72+
"(force-loop-duplication)" \
73+
"(no-loop-duplication)" \
74+
75+
#define OPT_WMM_MISC \
76+
"(scc)" \
77+
"(cfg-kill)" \
78+
"(no-dependencies)" \
79+
"(no-po-rendering)" \
80+
"(render-cluster-file)" \
81+
"(render-cluster-function)" \
82+
"(cav11)" \
83+
"(hide-internals)" \
84+
"(ignore-arrays)" \
85+
86+
#define OPT_WMM \
87+
OPT_WMM_MEMORY_MODEL \
88+
OPT_WMM_INSTRUMENTATION_STRATEGIES \
89+
OPT_WMM_LIMITS \
90+
OPT_WMM_LOOPS \
91+
OPT_WMM_MISC \
92+
93+
94+
#define HELP_WMM_FULL \
95+
" --mm <tso,pso,rmo,power> instruments a weak memory model\n" \
96+
" --scc detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \
97+
" --one-event-per-cycle only instruments one event per cycle\n" \
98+
" --minimum-interference instruments an optimal number of events\n" \
99+
" --my-events only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \
100+
" --cfg-kill enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \
101+
" --no-dependencies no dependency analysis\n" \
102+
" --no-po-rendering no representation of the threads in the dot\n"\
103+
" --render-cluster-file clusterises the dot by files\n" \
104+
" --render-cluster-function clusterises the dot by functions\n"
105+
106+
// clang-format on
107+
57108
#endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H

0 commit comments

Comments
 (0)