From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 2 Sep 2021 18:50:18 +0000 (-0700)
Subject: Add API check whether option in getOptionInfo() exists (#7093)
X-Git-Tag: cvc5-1.0.0~1287
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=67e6694f10919292ecc23b7ced60818ee13025e8;p=cvc5.git

Add API check whether option in getOptionInfo() exists (#7093)

This PR adds a missing check in the API for getOptionInfo().
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index d6c0a58ee..d41af938a 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7178,6 +7178,8 @@ OptionInfo Solver::getOptionInfo(const std::string& option) const
   CVC5_API_TRY_CATCH_BEGIN;
   //////// all checks before this line
   auto info = options::getInfo(d_smtEngine->getOptions(), option);
+  CVC5_API_CHECK(info.name != "")
+      << "Querying invalid or unknown option " << option;
   return std::visit(
       overloaded{
           [&info](const options::OptionInfo::VoidInfo& vi) {
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 62e70214d..d2881cc94 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -769,6 +769,10 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                     ['name == "{}"'.format(x) for x in sorted(names)])
 
                 # Generate code for getOptionInfo
+                if option.alias:
+                    alias = ', '.join(map(lambda s: '"{}"'.format(s), option.alias))
+                else:
+                    alias = ''
                 if option.name:
                     constr = None
                     fmt = {
@@ -788,11 +792,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
                         constr = 'OptionInfo::ModeInfo{{"{default}", {value}, {{ {modes} }}}}'.format(**fmt, modes=values)
                     else:
                         constr = 'OptionInfo::VoidInfo{}'
-                    if option.alias:
-                        alias = ', '.join(map(lambda s: '"{}"'.format(s), option.alias))
-                    else:
-                        alias = ''
                     options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, opts.{}.{}WasSetByUser, {}}};'.format(cond, long_get_option(option.long), module.id, option.name, constr, alias=alias))
+                else:
+                    options_get_info.append('if ({}) return OptionInfo{{"{}", {{{alias}}}, false, OptionInfo::VoidInfo{{}}}};'.format(cond, long_get_option(option.long), alias=alias))
 
                 if setoption_handlers:
                     setoption_handlers.append('  }} else if ({}) {{'.format(cond))
diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp
index 4beb47e0f..9c44dacba 100644
--- a/src/options/options_public_template.cpp
+++ b/src/options/options_public_template.cpp
@@ -277,7 +277,7 @@ OptionInfo getInfo(const Options& opts, const std::string& name)
   // clang-format off
   ${options_get_info}$
   // clang-format on
-  return OptionInfo{name, {}, false, OptionInfo::VoidInfo{}};
+  return OptionInfo{"", {}, false, OptionInfo::VoidInfo{}};
 }
 
 #undef DO_SEMANTIC_CHECKS_BY_DEFAULT
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 5ca96f035..e7d7c0bb4 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1332,10 +1332,13 @@ TEST_F(TestApiBlackSolver, getOptionNames)
 TEST_F(TestApiBlackSolver, getOptionInfo)
 {
   {
-    auto info = d_solver.getOptionInfo("verbose");
-    ASSERT_EQ(info.name, "verbose");
-    ASSERT_EQ(info.aliases, std::vector<std::string>{});
-    ASSERT_TRUE(std::holds_alternative<api::OptionInfo::VoidInfo>(info.valueInfo));
+    EXPECT_THROW(d_solver.getOptionInfo("asdf-invalid"), CVC5ApiException);
+  }
+  {
+    api::OptionInfo info = d_solver.getOptionInfo("verbose");
+    EXPECT_EQ("verbose", info.name);
+    EXPECT_EQ(std::vector<std::string>{}, info.aliases);
+    EXPECT_TRUE(std::holds_alternative<OptionInfo::VoidInfo>(info.valueInfo));
   }
   {
     // int64 type with default