From 3f9026e98182b1da90e3203f8525416fc8bf56df Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 11 Jun 2020 19:26:38 +0100 Subject: [PATCH 1/4] Fix format of nondet volatile command line help --- src/goto-instrument/nondet_volatile.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h index dc12bf83551..bb8d6a2b7d2 100644 --- a/src/goto-instrument/nondet_volatile.h +++ b/src/goto-instrument/nondet_volatile.h @@ -33,9 +33,9 @@ class optionst; " --" NONDET_VOLATILE_VARIABLE_OPT " \n" \ " makes reads from given volatile variable " \ "non-deterministic\n" \ - " --" NONDET_VOLATILE_MODEL_OPT ":\n" \ + " --" NONDET_VOLATILE_MODEL_OPT " :\n" \ " models reads from given volatile variable " \ - "by a call to the given model" + "by a call to the given model\n" // clang-format on void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options); From e7aacf249f91e1857f80074da24af55fa8170ef0 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 15 Jun 2020 11:34:06 +0100 Subject: [PATCH 2/4] Add function wrap_line() to wrap strings at given width --- src/util/string_utils.cpp | 72 ++++++++++++++++++++++++++++ src/util/string_utils.h | 40 ++++++++++++++++ unit/Makefile | 1 + unit/util/string_utils/wrap_line.cpp | 32 +++++++++++++ 4 files changed, 145 insertions(+) create mode 100644 unit/util/string_utils/wrap_line.cpp diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index aab98943475..9763c657b5a 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -174,3 +174,75 @@ std::string capitalize(const std::string &str) capitalized[0] = toupper(capitalized[0]); return capitalized; } + +std::string wrap_line( + const std::string &line, + const std::size_t left_margin, + const std::size_t width) +{ + return wrap_line(line.cbegin(), line.cend(), left_margin, width); +} + +std::string wrap_line( + std::string::const_iterator left, + std::string::const_iterator right, + const std::size_t left_margin, + const std::size_t width) +{ + PRECONDITION(left_margin < width); + + const std::size_t column_width = width - left_margin; + const std::string margin(left_margin, ' '); + + auto distance = std::distance(left, right); + CHECK_RETURN(distance > 0); + + std::string result; + + if(static_cast(distance) <= column_width) + { + result.append(margin); + result.append(left, right); + + return result; + } + + auto it_line_begin = left; + + do + { + // points to the first character past the current column + auto it = it_line_begin + column_width; + + auto rit_r = std::reverse_iterator(it) - 1; + auto rit_l = rit_r + column_width; + + auto rit_space = std::find(rit_r, rit_l, ' '); + + if(rit_space != rit_l) + { + auto it_space = rit_space.base() - 1; + CHECK_RETURN(*it_space == ' '); + + result.append(margin); + result.append(it_line_begin, it_space); + result.append("\n"); + + it_line_begin = it_space + 1; + } + else + { + // we have not found a space, thus cannot wrap this line + result.clear(); + result.append(left, right); + + return result; + } + } while(static_cast(std::distance(it_line_begin, right)) > + column_width); + + result.append(margin); + result.append(it_line_begin, right); + + return result; +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index a73bd8bd9cd..d6e06f21d3f 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -108,4 +108,44 @@ std::string escape(const std::string &); /// \return string with non-alphanumeric characters escaped std::string escape_non_alnum(const std::string &to_escape); +/// Wrap line at spaces to not extend past the right margin, and include given +/// padding with spaces to the left +/// +/// The given string should not contain any newlines. +/// +/// \param line: line to wrap, should not contain newlines +/// \param left_margin: each line will be padded to the left with `left_margin` +/// spaces +/// \param width: width of the resulting text, i.e., right margin +/// \return resulting string such that each line has length less or equal to +/// `width`, and each line includes `left_margin` spaces to the left; if the +/// given line cannot be wrapped (i.e., it cannot be broken up at spaces such +/// that every resulting line fits within the margin), the given line is +/// returned unchanged +std::string wrap_line( + const std::string &line, + const std::size_t left_margin = 0, + const std::size_t width = 80); + +/// Wrap line at spaces to not extend past the right margin, and include given +/// padding with spaces to the left +/// +/// The given string should not contain any newlines. +/// +/// \param left: iterator to beginning of string +/// \param right: iterator to end of string +/// \param left_margin: each line will be padded to the left with `left_margin` +/// spaces +/// \param width: width of the resulting text, i.e., right margin +/// \return resulting string such that each line has length less or equal to +/// `width`, and each line includes `left_margin` spaces to the left; if the +/// given line cannot be wrapped (i.e., it cannot be broken up at spaces such +/// that every resulting line fits within the margin), the given line is +/// returned unchanged +std::string wrap_line( + const std::string::const_iterator left, + const std::string::const_iterator right, + const std::size_t left_margin = 0, + const std::size_t width = 80); + #endif diff --git a/unit/Makefile b/unit/Makefile index f581bb010bf..e30aaf506f9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -117,6 +117,7 @@ SRC += analyses/ai/ai.cpp \ util/string_utils/join_string.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ + util/string_utils/wrap_line.cpp \ util/symbol_table.cpp \ util/symbol.cpp \ util/unicode.cpp \ diff --git a/unit/util/string_utils/wrap_line.cpp b/unit/util/string_utils/wrap_line.cpp new file mode 100644 index 00000000000..0c27996f341 --- /dev/null +++ b/unit/util/string_utils/wrap_line.cpp @@ -0,0 +1,32 @@ +/// Author: Daniel Poetzl + +/// \file Tests for wrap_line() + +#include +#include + +TEST_CASE("Wrap line", "[core][util]") +{ + SECTION("Wrap without margin") + { + REQUIRE(wrap_line("x", 0, 1) == "x"); + REQUIRE(wrap_line("x x", 0, 1) == "x\nx"); + REQUIRE(wrap_line("x x x", 0, 1) == "x\nx\nx"); + + REQUIRE(wrap_line("x x", 0, 2) == "x\nx"); + REQUIRE(wrap_line("xx xx xx", 0, 4) == "xx\nxx\nxx"); + + REQUIRE(wrap_line("xx", 0, 1) == "xx"); + } + + SECTION("Wrap with margin") + { + REQUIRE(wrap_line("x", 1, 2) == " x"); + REQUIRE(wrap_line("x x", 1, 2) == " x\n x"); + REQUIRE(wrap_line("x x x", 1, 2) == " x\n x\n x"); + + REQUIRE(wrap_line("x", 2, 3) == " x"); + + REQUIRE(wrap_line("xx", 1, 2) == "xx"); + } +} From 8ef633fc198309dc8e070ccaf6027ea3049f6909 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 16 Jun 2020 11:48:32 +0100 Subject: [PATCH 3/4] Add function help_entry() to format command line help entries --- src/util/parse_options.cpp | 53 +++++++++++++++++++++++++++++++++++++ src/util/parse_options.h | 6 +++++ unit/util/parse_options.cpp | 9 +++++++ 3 files changed, 68 insertions(+) diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index d9dbdac6e48..4e083e59bb5 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "parse_options.h" #include +#include #include #include @@ -23,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "exception_utils.h" #include "exit_codes.h" #include "signal_catcher.h" +#include "string_utils.h" parse_options_baset::parse_options_baset( const std::string &_optstring, @@ -151,3 +153,54 @@ banner_string(const std::string &front_end, const std::string &version) return align_center_with_border(version_str); } + +std::string help_entry( + const std::string &option, + const std::string &description, + const std::size_t left_margin, + const std::size_t width) +{ + PRECONDITION(!option.empty()); + PRECONDITION(!std::isspace(option.front())); + PRECONDITION(!std::isspace(option.back())); + PRECONDITION(option.length() <= width); + + PRECONDITION(!description.empty()); + PRECONDITION(!std::isspace(description.front())); + PRECONDITION(!std::isspace(description.back())); + + PRECONDITION(left_margin < width); + + std::string result; + + if(option.length() >= left_margin - 1) + { + result = " " + option + "\n"; + result += wrap_line(description, left_margin, width) + "\n"; + + return result; + } + + std::string padding(left_margin - option.length() - 1, ' '); + result = " " + option + padding; + + if(description.length() <= (width - left_margin)) + { + return result + description + "\n"; + } + + auto it = description.cbegin() + (width - left_margin); + auto rit = std::reverse_iterator(it) - 1; + + auto rit_space = std::find(rit, description.crend(), ' '); + auto it_space = rit_space.base() - 1; + CHECK_RETURN(*it_space == ' '); + + result.append(description.cbegin(), it_space); + result.append("\n"); + + result += + wrap_line(it_space + 1, description.cend(), left_margin, width) + "\n"; + + return result; +} diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 6cfdbcf9ad9..b4ea02d720c 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -58,4 +58,10 @@ banner_string(const std::string &front_end, const std::string &version); /// ``` std::string align_center_with_border(const std::string &text); +std::string help_entry( + const std::string &option, + const std::string &description, + const std::size_t left_margin = 30, + const std::size_t width = 80); + #endif // CPROVER_UTIL_PARSE_OPTIONS_H diff --git a/unit/util/parse_options.cpp b/unit/util/parse_options.cpp index 697cbe885fc..603671fdf3f 100644 --- a/unit/util/parse_options.cpp +++ b/unit/util/parse_options.cpp @@ -15,3 +15,12 @@ TEST_CASE("align_center_with_border", "[core][util]") align_center_with_border("test-text") == "* * test-text * *"); } + +TEST_CASE("help_entry", "[core][util]") +{ + REQUIRE(help_entry("--abc", "xyz", 8, 12) == " --abc xyz\n"); + REQUIRE(help_entry("--abc", "xxxx x", 8, 12) == " --abc xxxx\n x\n"); + REQUIRE(help_entry("--abc", "xx xx", 8, 12) == " --abc xx\n xx\n"); + REQUIRE(help_entry("--abcdef", "xyz", 8, 12) == " --abcdef\n xyz\n"); + REQUIRE(help_entry("--abcdefg", "xyz", 8, 12) == " --abcdefg\n xyz\n"); +} From 8307fab265840232b9781606c4c7ac140faf2829 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 16 Jun 2020 12:45:18 +0100 Subject: [PATCH 4/4] Use help_entry() in help text of nondet volatile feature --- .../goto_instrument_parse_options.cpp | 2 +- src/goto-instrument/nondet_volatile.h | 17 +++++++++-------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6f780755c7b..9a3d00a69b4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1799,7 +1799,7 @@ void goto_instrument_parse_optionst::help() " --race-check add floating-point data race checks\n" "\n" "Semantic transformations:\n" - HELP_NONDET_VOLATILE + << HELP_NONDET_VOLATILE << " --unwind unwinds the loops times\n" " --unwindset L:B,... unwind loop L with a bound of B\n" " --unwindset-file read unwindset from file\n" diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h index bb8d6a2b7d2..e0045a418bf 100644 --- a/src/goto-instrument/nondet_volatile.h +++ b/src/goto-instrument/nondet_volatile.h @@ -28,14 +28,15 @@ class optionst; "(" NONDET_VOLATILE_MODEL_OPT "):" #define HELP_NONDET_VOLATILE \ - " --" NONDET_VOLATILE_OPT " makes reads from volatile variables " \ - "non-deterministic\n" \ - " --" NONDET_VOLATILE_VARIABLE_OPT " \n" \ - " makes reads from given volatile variable " \ - "non-deterministic\n" \ - " --" NONDET_VOLATILE_MODEL_OPT " :\n" \ - " models reads from given volatile variable " \ - "by a call to the given model\n" + help_entry( \ + "--" NONDET_VOLATILE_OPT, \ + "makes reads from volatile variables non-deterministic") << \ + help_entry( \ + "--" NONDET_VOLATILE_VARIABLE_OPT " ", \ + "makes reads from given volatile variable non-deterministic") << \ + help_entry( \ + "--" NONDET_VOLATILE_MODEL_OPT " :", \ + "models reads from given volatile variable by a call to the given model") // clang-format on void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);