Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add python bindings for configurations #125

Open
wants to merge 15 commits into
base: vara-dev
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion bindings/python/vara-feature/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
pybind11_add_module(
vara_feature
pybind_Init.cpp
pybind_Configuration.cpp
pybind_Constraint.cpp
pybind_Feature.cpp
pybind_FeatureModel.cpp
Expand All @@ -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}
)
45 changes: 45 additions & 0 deletions bindings/python/vara-feature/pybind_Configuration.cpp
Original file line number Diff line number Diff line change
@@ -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 <filesystem>
#include <iostream>

namespace vf = vara::feature;
namespace vs = vara::solver;
namespace py = pybind11;

void init_configuration_module(py::module &M) {
py::class_<vf::ConfigurationOption>(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_<vf::Configuration>(M, "Configuration")
.def("__str__", [](vf::Configuration &C) { return C.dumpToString(); })
.def("getOptions", [](vf::Configuration &C) {
std::vector<vf::ConfigurationOption> 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");
}
3 changes: 3 additions & 0 deletions bindings/python/vara-feature/pybind_Init.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand All @@ -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);
}
4 changes: 4 additions & 0 deletions include/vara/Solver/Error.h
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ enum SolverErrorCode {
ALREADY_PRESENT,
NOT_ALL_CONSTRAINTS_PROCESSED,
PARENT_NOT_PRESENT,
ILLEGAL_STATE,
};

} // namespace solver
Expand Down Expand Up @@ -52,6 +53,9 @@ class Error<vara::solver::SolverErrorCode> {
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;
}
Expand Down
6 changes: 6 additions & 0 deletions include/vara/Solver/Z3Solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -95,6 +95,12 @@ class Z3Solver : public Solver {
/// The instance of the Z3 solver needed for caching the constraints and
/// variables.
std::unique_ptr<z3::solver> 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
Expand Down
54 changes: 29 additions & 25 deletions lib/Solver/Z3Solver.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -177,35 +177,47 @@ Result<SolverErrorCode, bool> Z3Solver::hasValidConfigurations() {

Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
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<SolverErrorCode, uint64_t> 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<SolverErrorCode,
std::vector<std::unique_ptr<vara::feature::Configuration>>>
Z3Solver::getAllValidConfigurations() {
if (Dirty) {
return Error(ILLEGAL_STATE);
}

Solver->push();
auto Vector = std::vector<std::unique_ptr<vara::feature::Configuration>>();
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;
}

Expand All @@ -227,23 +239,19 @@ Z3Solver::setBinaryFeatureConstraints(const feature::BinaryFeature &Feature,
}

Result<SolverErrorCode> 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);
Expand All @@ -252,17 +260,13 @@ Result<SolverErrorCode> Z3Solver::excludeCurrentConfiguration() {

Result<SolverErrorCode, std::unique_ptr<vara::feature::Configuration>>
Z3Solver::getCurrentConfiguration() {
if (Solver->check() == z3::unsat) {
return UNSAT;
}
const z3::model M = Solver->get_model();
auto Config = std::make_unique<vara::feature::Configuration>();

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;
Expand Down
4 changes: 3 additions & 1 deletion setup.py
Original file line number Diff line number Diff line change
Expand Up @@ -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')
Comment on lines +50 to +51
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure if this is a good way to determine if we should build the solver.

  1. the path is a system specific
  2. we might want to build the solver from scratch even for those system, as we depend on a very specific version of z3. (The debian 11 can cause problems)

Maybe we should keep building the solver as the default and give the user a option to disable that? Or, if it works for you, only you use the local one.


cfg = 'Debug' if self.debug else 'Release'
build_args = ['--config', cfg]
Expand All @@ -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(
Expand Down
40 changes: 40 additions & 0 deletions unittests/Solver/ConfigurationFactory.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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<string>();
for (auto &config : Configs) {
ConfigsStrings.push_back(config.get()->dumpToString());
}

auto UniqueConfigs =
std::set<string>(ConfigsStrings.begin(), ConfigsStrings.end());
EXPECT_EQ(Configs.size(), UniqueConfigs.size());
}

TEST(ConfigurationFactory, GetAllConfigurations3) {
auto FM = feature::loadFeatureModel(
getTestResource("test_msmr.xml"));
Comment on lines +76 to +77

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[clang-format] reported by reviewdog 🐶

Suggested change
auto FM = feature::loadFeatureModel(
getTestResource("test_msmr.xml"));
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<string>();
for (auto &config : Configs) {
ConfigsStrings.push_back(config.get()->dumpToString());
}

auto UniqueConfigs =
std::set<string>(ConfigsStrings.begin(), ConfigsStrings.end());
EXPECT_EQ(Configs.size(), UniqueConfigs.size());
}

TEST(ConfigurationFactory, GetNConfigurations) {
auto FM = getFeatureModel();
auto ConfigResult = ConfigurationFactory::getNConfigs(*FM, 100);
Expand Down
2 changes: 1 addition & 1 deletion unittests/Solver/Z3Tests.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down
2 changes: 2 additions & 0 deletions unittests/resources/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -32,13 +32,15 @@ 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
xml/test_out_of_order.xml
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
)
Expand Down
48 changes: 48 additions & 0 deletions unittests/resources/xml/test_msmr.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE vm SYSTEM "vm.dtd">
<vm name="SingleLocalSingle" root="root">
<binaryOptions>
<configurationOption>
<name>root</name>
<parent></parent>
<optional>False</optional>
</configurationOption>
<configurationOption>
<name>Slow</name>
<outputString>--slow</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
<configurationOption>
<name>Header</name>
<outputString>--header</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
<configurationOption>
<name>Extern</name>
<outputString>--extern</outputString>
<parent>root</parent>
<optional>True</optional>
<locations>
<sourceRange category="necessary">
<path>src/MultiSharedMultipleRegions/FeatureHeader.cpp</path>
<start>
<line>3</line>
<column>6</column>
</start>
<end>
<line>3</line>
<column>18</column>
</end>
</sourceRange>
</locations>
</configurationOption>
<configurationOption>
<name>Cpp</name>
<outputString>--cpp</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
</binaryOptions>
</vm>
29 changes: 29 additions & 0 deletions unittests/resources/xml/test_three_optional_features.xml
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE vm SYSTEM "vm.dtd">
<vm name="SingleLocalSingle" root="root">
<binaryOptions>
<configurationOption>
<name>root</name>
<parent></parent>
<optional>False</optional>
</configurationOption>
<configurationOption>
<name>A</name>
<outputString>A</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
<configurationOption>
<name>B</name>
<outputString>B</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
<configurationOption>
<name>C</name>
<outputString>C</outputString>
<parent>root</parent>
<optional>True</optional>
</configurationOption>
</binaryOptions>
</vm>
Loading