From e8c23600433674646c33e374d061a5db46f4d7a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Dec 2024 16:57:17 -0800 Subject: [PATCH] fix #7461 Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_seq_plugin.cpp | 36 +++++++++++++++++----------------- src/ast/sls/sls_seq_plugin.h | 10 +++++----- src/shell/main.cpp | 11 +++++++++++ 3 files changed, 34 insertions(+), 23 deletions(-) diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index 89118cae2..fd2b85a2a 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -697,18 +697,18 @@ namespace sls { u[i][j] = d[i - 1][j - 1]; } if (d[i - 1][j] == u[i][j] && !a_is_value[i - 1]) { - add_string_update(side::left, op::del, i - 1, 0); - add_string_update(side::left, op::add, j - 1, i - 1); + add_string_update(side_t::left, op_t::del, i - 1, 0); + add_string_update(side_t::left, op_t::add, j - 1, i - 1); } if (d[i][j - 1] == u[i][j] && !b_is_value[j - 1]) { - add_string_update(side::right, op::del, j - 1, 0); - add_string_update(side::right, op::add, i - 1, j - 1); + add_string_update(side_t::right, op_t::del, j - 1, 0); + add_string_update(side_t::right, op_t::add, i - 1, j - 1); } if (d[i - 1][j - 1] == u[i][j] && !a_is_value[i - 1]) - add_string_update(side::left, op::copy, j - 1, i - 1); + add_string_update(side_t::left, op_t::copy, j - 1, i - 1); if (d[i - 1][j - 1] == u[i][j] && !b_is_value[j - 1]) - add_string_update(side::right, op::copy, i - 1, j - 1); + add_string_update(side_t::right, op_t::copy, i - 1, j - 1); } } @@ -833,20 +833,20 @@ namespace sls { #if 1 for (auto const& [side, op, i, j] : m_string_updates) { switch (op) { - case op::del: - if (side == side::left) + case op_t::del: + if (side == side_t::left) verbose_stream() << "del " << a[i] << " @ " << i << " left\n"; else verbose_stream() << "del " << b[i] << " @ " << i << " right\n"; break; - case op::add: - if (side == side::left) + case op_t::add: + if (side == side_t::left) verbose_stream() << "add " << b[i] << " @ " << j << " left\n"; else verbose_stream() << "add " << a[i] << " @ " << j << " right\n"; break; - case op::copy: - if (side == side::left) + case op_t::copy: + if (side == side_t::left) verbose_stream() << "copy " << b[i] << " @ " << j << " left\n"; else verbose_stream() << "copy " << a[i] << " @ " << j << " right\n"; @@ -855,7 +855,7 @@ namespace sls { } #endif for (auto& [side, op, i, j] : m_string_updates) { - if (op == op::del && side == side::left) { + if (op == op_t::del && side == side_t::left) { for (auto x : L) { auto const& value = strval0(x); @@ -868,7 +868,7 @@ namespace sls { } } } - else if (op == op::del && side == side::right) { + else if (op == op_t::del && side == side_t::right) { for (auto x : R) { auto const& value = strval0(x); if (i >= value.length()) @@ -880,7 +880,7 @@ namespace sls { } } } - else if (op == op::add && side == side::left) { + else if (op == op_t::add && side == side_t::left) { for (auto x : L) { auto const& value = strval0(x); //verbose_stream() << "add " << j << " " << value << " " << value.length() << " " << is_value(x) << "\n"; @@ -894,7 +894,7 @@ namespace sls { break; } } - else if (op == op::add && side == side::right) { + else if (op == op_t::add && side == side_t::right) { for (auto x : R) { auto const& value = strval0(x); //verbose_stream() << "add " << j << " " << value << " " << value.length() << " " << is_value(x) << "\n"; @@ -908,7 +908,7 @@ namespace sls { break; } } - else if (op == op::copy && side == side::left) { + else if (op == op_t::copy && side == side_t::left) { for (auto x : L) { auto const& value = strval0(x); if (j >= value.length()) @@ -920,7 +920,7 @@ namespace sls { } } } - else if (op == op::copy && side == side::right) { + else if (op == op_t::copy && side == side_t::right) { for (auto x : R) { auto const& value = strval0(x); if (j >= value.length()) diff --git a/src/ast/sls/sls_seq_plugin.h b/src/ast/sls/sls_seq_plugin.h index 7de3e888a..ea9b3f0b9 100644 --- a/src/ast/sls/sls_seq_plugin.h +++ b/src/ast/sls/sls_seq_plugin.h @@ -92,19 +92,19 @@ namespace sls { void repair_up_str_itos(app* e); void repair_up_str_stoi(app* e); - enum op { + enum op_t { add, del, copy }; - enum side { + enum side_t { left, right }; struct string_update { - side side; - op op; + side_t side; + op_t op; unsigned i, j; }; svector m_string_updates; - void add_string_update(side side, op op, unsigned i, unsigned j) { m_string_updates.push_back({ side, op, i, j }); } + void add_string_update(side_t side, op_t op, unsigned i, unsigned j) { m_string_updates.push_back({ side, op, i, j }); } unsigned edit_distance_with_updates(zstring const& a, bool_vector const& a_is_value, zstring const& b, bool_vector const& b_is_value); unsigned edit_distance(zstring const& a, zstring const& b); void add_edit_updates(ptr_vector const& w, zstring const& val, zstring const& val_other, uint_set const& chars); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 1aada6c41..4bf0370d6 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -123,6 +123,13 @@ void display_usage() { std::cout << " module_name.param_name=value for setting module parameters.\n"; std::cout << "Use 'z3 -p' for the complete list of global and module parameters.\n"; } + +static bool validate_is_ulong(char const* s) { + for (; *s; ++s) + if (*s < '0' || *s > '9') + return false; + return true; +} static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) { long timeout = 0; @@ -220,6 +227,8 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) else if (strcmp(opt_name, "v") == 0) { if (!opt_arg) error("option argument (-v:level) is missing."); + if (!validate_is_ulong(opt_arg)) + error("invalid argument for -v option, it must be a non-negative integer."); long lvl = strtol(opt_arg, nullptr, 10); set_verbosity_level(lvl); } @@ -229,6 +238,8 @@ static void parse_cmd_line_args(std::string& input_file, int argc, char ** argv) else if (strcmp(opt_name, "T") == 0) { if (!opt_arg) error("option argument (-T:timeout) is missing."); + if (!validate_is_ulong(opt_arg)) + error("invalid argument for -T option, it must be a non-negative integer."); timeout = strtol(opt_arg, nullptr, 10); } else if (strcmp(opt_name, "t") == 0) {