diff --git a/bindings/python/vara-feature/CMakeLists.txt b/bindings/python/vara-feature/CMakeLists.txt index b8a4ac4aa..67a5df1c4 100644 --- a/bindings/python/vara-feature/CMakeLists.txt +++ b/bindings/python/vara-feature/CMakeLists.txt @@ -1,6 +1,7 @@ pybind11_add_module( vara_feature pybind_Init.cpp + pybind_Configuration.cpp pybind_Constraint.cpp pybind_Feature.cpp pybind_FeatureModel.cpp @@ -12,4 +13,10 @@ pybind11_add_module( set(LLVM_LINK_COMPONENTS Core Support) -target_link_libraries(vara_feature LINK_PUBLIC VaRAFeature ${STD_FS_LIB}) +target_link_libraries( + vara_feature + LINK_PUBLIC + VaRAFeature + VaRASolver + ${STD_FS_LIB} +) diff --git a/bindings/python/vara-feature/pybind_Configuration.cpp b/bindings/python/vara-feature/pybind_Configuration.cpp new file mode 100644 index 000000000..f77430f39 --- /dev/null +++ b/bindings/python/vara-feature/pybind_Configuration.cpp @@ -0,0 +1,45 @@ +#include "pybind_common.h" +#include "vara/Configuration/Configuration.h" +#include "vara/Solver/ConfigurationFactory.h" + +#include "pybind11/detail/common.h" +#include "pybind11/pybind11.h" + +#include +#include + +namespace vf = vara::feature; +namespace vs = vara::solver; +namespace py = pybind11; + +void init_configuration_module(py::module &M) { + py::class_(M, "ConfigurationOption") + .def_property_readonly( + "name", [](vf::ConfigurationOption &CO) { return CO.name().str(); }, + R"pbdoc(Returns the name of the ConfigurationOption.)pbdoc") + .def_property_readonly( + "value", &vf::ConfigurationOption::asString, + R"pbdoc(Returns the value of the ConfigurationOption as str.)pbdoc"); + py::class_(M, "Configuration") + .def("__str__", [](vf::Configuration &C) { return C.dumpToString(); }) + .def("getOptions", [](vf::Configuration &C) { + std::vector V; + for (auto &O : C) { + V.push_back(*O.getValue()); + } + + return V; + }); + M.def( + "getAllConfigs", + [](vf::FeatureModel &FM) { + return vs::ConfigurationFactory::getAllConfigs(FM).extractValue(); + }, + R"pbdoc(Get all configurations of FeatureModel. + +Args: + fm (FeatureModel): the FeatureModel + +Returns: list of all configurations. +)pbdoc"); +} diff --git a/bindings/python/vara-feature/pybind_Init.cpp b/bindings/python/vara-feature/pybind_Init.cpp index 50e00f5f8..141da5f0e 100644 --- a/bindings/python/vara-feature/pybind_Init.cpp +++ b/bindings/python/vara-feature/pybind_Init.cpp @@ -12,6 +12,7 @@ void init_feature_location_module(py::module &M); void init_feature_model_module(py::module &M); void init_feature_model_builder_module(py::module &M); void init_xml_writer(py::module &M); +void init_configuration_module(py::module &M); PYBIND11_MODULE(vara_feature, M) { auto LLVMModule = M.def_submodule("llvm_util"); @@ -27,4 +28,6 @@ PYBIND11_MODULE(vara_feature, M) { init_xml_writer(FMWriterModule); auto FeatureModelBuilderModule = M.def_submodule("feature_model_builder"); init_feature_model_builder_module(FeatureModelBuilderModule); + auto ConfigurationModule = M.def_submodule("configuration"); + init_configuration_module(ConfigurationModule); } diff --git a/include/vara/Solver/Error.h b/include/vara/Solver/Error.h index 895f4ca52..60f78aad8 100644 --- a/include/vara/Solver/Error.h +++ b/include/vara/Solver/Error.h @@ -14,6 +14,7 @@ enum SolverErrorCode { ALREADY_PRESENT, NOT_ALL_CONSTRAINTS_PROCESSED, PARENT_NOT_PRESENT, + ILLEGAL_STATE, }; } // namespace solver @@ -52,6 +53,9 @@ class Error { case vara::solver::PARENT_NOT_PRESENT: OS << "Parent feature of a feature is not present."; break; + case vara::solver::ILLEGAL_STATE: + OS << "The solver is in an illegal state for this operation."; + break; } return OS; } diff --git a/include/vara/Solver/Z3Solver.h b/include/vara/Solver/Z3Solver.h index cd43e3a8b..0c29826ad 100644 --- a/include/vara/Solver/Z3Solver.h +++ b/include/vara/Solver/Z3Solver.h @@ -95,6 +95,12 @@ class Z3Solver : public Solver { /// The instance of the Z3 solver needed for caching the constraints and /// variables. std::unique_ptr Solver; + + /// Flag that indicates whether the solver state has been modified by calling + /// \c getNextConfiguration. + /// This is important for functions that want to enumerate all configurations, + /// like \c getAllValidConfigurations or \c getNumberValidConfigurations. + bool Dirty = false; }; /// \brief This class is a visitor to convert the constraints from the diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index f28c9d4de..43128aa0d 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -177,35 +177,47 @@ Result Z3Solver::hasValidConfigurations() { Result> Z3Solver::getNextConfiguration() { - // Add previous configuration as a constraint - excludeCurrentConfiguration(); + if (Dirty) { + excludeCurrentConfiguration(); + } else { + Dirty = true; + } - // Retrieve the next configuration + if (Solver->check() == z3::unsat) { + return UNSAT; + } return getCurrentConfiguration(); } Result Z3Solver::getNumberValidConfigurations() { + if (Dirty) { + return Error(ILLEGAL_STATE); + } + Solver->push(); uint64_t Count = 0; - while (Solver->check() == z3::sat) { - excludeCurrentConfiguration(); + while (getNextConfiguration()) { Count++; } Solver->pop(); + Dirty = false; return Count; } Result>> Z3Solver::getAllValidConfigurations() { + if (Dirty) { + return Error(ILLEGAL_STATE); + } + Solver->push(); auto Vector = std::vector>(); - while (Solver->check() == z3::sat) { - auto Config = getCurrentConfiguration().extractValue(); - Vector.insert(Vector.begin(), std::move(Config)); - excludeCurrentConfiguration(); + while (auto Config = getNextConfiguration()) { + Vector.insert(Vector.begin(), Config.extractValue()); } Solver->pop(); + Dirty = false; return Vector; } @@ -227,23 +239,19 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature, } Result Z3Solver::excludeCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); z3::expr Expr = Context.bool_val(false); - for (auto Iterator = OptionToVariableMapping.begin(); - Iterator != OptionToVariableMapping.end(); Iterator++) { - const z3::expr OptionExpr = *Iterator->getValue(); + for (const auto &Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); if (Value.is_bool()) { if (Value.is_true()) { - Expr = Expr || !*Iterator->getValue(); + Expr = Expr || !OptionExpr; } else { - Expr = Expr || *Iterator->getValue(); + Expr = Expr || OptionExpr; } } else { - Expr = Expr || (*Iterator->getValue() != Value); + Expr = Expr || (OptionExpr != Value); } } Solver->add(Expr); @@ -252,17 +260,13 @@ Result Z3Solver::excludeCurrentConfiguration() { Result> Z3Solver::getCurrentConfiguration() { - if (Solver->check() == z3::unsat) { - return UNSAT; - } const z3::model M = Solver->get_model(); auto Config = std::make_unique(); - for (auto Iterator = OptionToVariableMapping.begin(); - Iterator != OptionToVariableMapping.end(); Iterator++) { - const z3::expr OptionExpr = *Iterator->getValue(); + for (const auto &Entry : OptionToVariableMapping) { + const z3::expr OptionExpr = *Entry.getValue(); const z3::expr Value = M.eval(OptionExpr, true); - Config->setConfigurationOption(Iterator->getKey(), + Config->setConfigurationOption(Entry.getKey(), llvm::StringRef(Value.to_string())); } return Config; diff --git a/setup.py b/setup.py index 805810a6d..63af382ec 100644 --- a/setup.py +++ b/setup.py @@ -47,6 +47,8 @@ def build_extension(self, ext): '-DPYTHON_EXECUTABLE=' + sys.executable, '-DVARA_FEATURE_USE_Z3_SOLVER=True' ] + if os.path.exists('/lib/x86_64-linux-gnu/libz3.so'): + cmake_args.append('-DVARA_FEATURE_BUILD_Z3_SOLVER=False') cfg = 'Debug' if self.debug else 'Release' build_args = ['--config', cfg] @@ -61,7 +63,7 @@ def build_extension(self, ext): build_args += ['--', '/m'] else: cmake_args += ['-DCMAKE_BUILD_TYPE=' + cfg] - build_args += ['--', '-j2'] + build_args += ['--', f'-j{os.cpu_count()}'] env = os.environ.copy() env['CXXFLAGS'] = '{} -DVERSION_INFO=\\"{}\\"'.format( diff --git a/unittests/Solver/ConfigurationFactory.cpp b/unittests/Solver/ConfigurationFactory.cpp index 5170271fa..84988998f 100644 --- a/unittests/Solver/ConfigurationFactory.cpp +++ b/unittests/Solver/ConfigurationFactory.cpp @@ -2,6 +2,8 @@ #include "vara/Feature/ConstraintBuilder.h" #include "vara/Feature/FeatureModelBuilder.h" + +#include "Utils/UnittestHelper.h" #include "gtest/gtest.h" namespace vara::solver { @@ -51,6 +53,44 @@ TEST(ConfigurationFactory, GetAllConfigurations) { EXPECT_EQ(ConfigResult.extractValue().size(), 6 * 63); } +TEST(ConfigurationFactory, GetAllConfigurations2) { + auto FM = feature::loadFeatureModel( + getTestResource("test_three_optional_features.xml")); + auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM); + EXPECT_TRUE(ConfigResult); + auto Configs = ConfigResult.extractValue(); + + EXPECT_EQ(Configs.size(), 8); + + auto ConfigsStrings = std::vector(); + for (auto &config : Configs) { + ConfigsStrings.push_back(config.get()->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + EXPECT_EQ(Configs.size(), UniqueConfigs.size()); +} + +TEST(ConfigurationFactory, GetAllConfigurations3) { + auto FM = feature::loadFeatureModel( + getTestResource("test_msmr.xml")); + auto ConfigResult = ConfigurationFactory::getAllConfigs(*FM); + EXPECT_TRUE(ConfigResult); + auto Configs = ConfigResult.extractValue(); + + EXPECT_EQ(Configs.size(), 16); + + auto ConfigsStrings = std::vector(); + for (auto &config : Configs) { + ConfigsStrings.push_back(config.get()->dumpToString()); + } + + auto UniqueConfigs = + std::set(ConfigsStrings.begin(), ConfigsStrings.end()); + EXPECT_EQ(Configs.size(), UniqueConfigs.size()); +} + TEST(ConfigurationFactory, GetNConfigurations) { auto FM = getFeatureModel(); auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100); diff --git a/unittests/Solver/Z3Tests.cpp b/unittests/Solver/Z3Tests.cpp index bd36af3b0..6848f746f 100644 --- a/unittests/Solver/Z3Tests.cpp +++ b/unittests/Solver/Z3Tests.cpp @@ -115,7 +115,7 @@ TEST(Z3Solver, TestGetNextConfiguration) { S->addFeature(*FM->getFeature("Foo")); S->addFeature(*FM->getFeature("Num1")); - for (int Count = 0; Count < 3; Count++) { + for (int Count = 0; Count < 4; Count++) { auto C = S->getNextConfiguration(); EXPECT_TRUE(C); auto Config = C.extractValue(); diff --git a/unittests/resources/CMakeLists.txt b/unittests/resources/CMakeLists.txt index a243fcb77..dbf71e528 100644 --- a/unittests/resources/CMakeLists.txt +++ b/unittests/resources/CMakeLists.txt @@ -32,6 +32,7 @@ set(FEATURE_LIB_TEST_FILES xml/test_hsqldb_num.xml xml/test_member_offset.xml xml/test_mixed_constraints.xml + xml/test_msmr.xml xml/test_numbers.xml xml/test_only_children.xml xml/test_only_parents.xml @@ -39,6 +40,7 @@ set(FEATURE_LIB_TEST_FILES xml/test_output_string.xml xml/test_revision_range.xml xml/test_step_function.xml + xml/test_three_optional_features.xml xml/test_with_whitespaces.xml yml/dune_configs.yml ) diff --git a/unittests/resources/xml/test_msmr.xml b/unittests/resources/xml/test_msmr.xml new file mode 100644 index 000000000..20f41419e --- /dev/null +++ b/unittests/resources/xml/test_msmr.xml @@ -0,0 +1,48 @@ + + + + + + root + + False + + + Slow + --slow + root + True + + + Header + --header + root + True + + + Extern + --extern + root + True + + + src/MultiSharedMultipleRegions/FeatureHeader.cpp + + 3 + 6 + + + 3 + 18 + + + + + + Cpp + --cpp + root + True + + + \ No newline at end of file diff --git a/unittests/resources/xml/test_three_optional_features.xml b/unittests/resources/xml/test_three_optional_features.xml new file mode 100644 index 000000000..d18ea984f --- /dev/null +++ b/unittests/resources/xml/test_three_optional_features.xml @@ -0,0 +1,29 @@ + + + + + + root + + False + + + A + A + root + True + + + B + B + root + True + + + C + C + root + True + + +