OPT_ and HELP_ macros for the weak memory model flags

This also adds:
 --read-first
 --write-first
 --no-loop-duplication
 --hide-internals
which are handled by goto-instrument but were not options so couldn't be
used.

Author: martin

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -110,7 +110,6 @@ Author: Daniel Kroening, [email protected]
 #include "unwind.h"
 #include "unwindset.h"
 #include "value_set_fi_fp_removal.h"
-#include "wmm/weak_memory.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
@@ -1793,17 +1792,7 @@ void goto_instrument_parse_optionst::help()
     " --skip-loops <loop-ids>      add gotos to skip selected loops during execution\n" // NOLINT(*)
     "\n"
     "Memory model instrumentations:\n"
-    " --mm <tso,pso,rmo,power>     instruments a weak memory model\n"
-    " --scc                        detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
-    " --one-event-per-cycle        only instruments one event per cycle\n"
-    " --minimum-interference       instruments an optimal number of events\n"
-    " --my-events                  only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
-    " --cfg-kill                   enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
-    " --no-dependencies            no dependency analysis\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --no-po-rendering            no representation of the threads in the dot\n"
-    " --render-cluster-file        clusterises the dot by files\n"
-    " --render-cluster-function    clusterises the dot by functions\n"
+    HELP_WMM_FULL
     "\n"
     "Slicing:\n"
     HELP_REACHABILITY_SLICER

src/goto-instrument/goto_instrument_parse_options.h

@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
 #include "nondet_volatile.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
+#include "wmm/weak_memory.h"
 
 // clang-format off
 #define GOTO_INSTRUMENT_OPTIONS \
@@ -50,18 +51,14 @@ Author: Daniel Kroening, [email protected]
   OPT_REMOVE_POINTERS \
   "(no-simplify)" \
   OPT_UNINITIALIZED_CHECK \
-  "(race-check)(scc)(one-event-per-cycle)" \
-  "(minimum-interference)" \
-  "(mm):(my-events)" \
+  OPT_WMM \
+  "(race-check)" \
   "(unwind):(unwindset):(unwindset-file):" \
   "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
   "(log):" \
-  "(max-var):(max-po-trans):(ignore-arrays)" \
-  "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)(reachable-call-graph)" \
   OPT_INSERT_FINAL_ASSERT_FALSE \
   OPT_SHOW_CLASS_HIERARCHY \
-  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(isr):" \
   "(stack-depth):(nondet-static)" \
   "(nondet-static-exclude):" \
@@ -85,7 +82,6 @@ Author: Daniel Kroening, [email protected]
   "(remove-function-pointers)" \
   "(show-claims)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
-  "(cav11)" \
   OPT_TIMESTAMP \
   "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
   "(string-abstraction)" \

src/goto-instrument/wmm/weak_memory.h

@@ -54,4 +54,55 @@ void introduce_temporaries(
 #endif
   messaget &message);
 
+// clang-format off
+#define OPT_WMM_MEMORY_MODEL  "(mm):"
+
+#define OPT_WMM_INSTRUMENTATION_STRATEGIES                                     \
+  "(one-event-per-cycle)"                                                      \
+  "(minimum-interference)"                                                     \
+  "(read-first)"                                                               \
+  "(write-first)"                                                              \
+  "(my-events)"                                                                \
+
+#define OPT_WMM_LIMITS                                                         \
+  "(max-var):"                                                                 \
+  "(max-po-trans):"                                                            \
+
+#define OPT_WMM_LOOPS                                                          \
+  "(force-loop-duplication)"                                                   \
+  "(no-loop-duplication)"                                                      \
+
+#define OPT_WMM_MISC                                                           \
+  "(scc)"                                                                      \
+  "(cfg-kill)"                                                                 \
+  "(no-dependencies)"                                                          \
+  "(no-po-rendering)"                                                          \
+  "(render-cluster-file)"                                                      \
+  "(render-cluster-function)"                                                  \
+  "(cav11)"                                                                    \
+  "(hide-internals)"                                                           \
+  "(ignore-arrays)"                                                            \
+
+#define OPT_WMM                                                                \
+  OPT_WMM_MEMORY_MODEL                                                         \
+  OPT_WMM_INSTRUMENTATION_STRATEGIES                                           \
+  OPT_WMM_LIMITS                                                               \
+  OPT_WMM_LOOPS                                                                \
+  OPT_WMM_MISC                                                                 \
+
+
+#define HELP_WMM_FULL                                                          \
+  " --mm <tso,pso,rmo,power>     instruments a weak memory model\n"            \
+  " --scc                        detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \
+  " --one-event-per-cycle        only instruments one event per cycle\n"       \
+  " --minimum-interference       instruments an optimal number of events\n"    \
+  " --my-events                  only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \
+  " --cfg-kill                   enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \
+  " --no-dependencies            no dependency analysis\n"                     \
+  " --no-po-rendering            no representation of the threads in the dot\n"\
+  " --render-cluster-file        clusterises the dot by files\n"               \
+  " --render-cluster-function    clusterises the dot by functions\n"
+
+// clang-format on
+
 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H