Date: Mon, 27 Jun 2016 12:38:02 +0200 From: Hans Petter Selasky <hps@selasky.org> To: Slawa Olhovchenkov <slw@zxy.spb.ru>, Baptiste Daroussin <bapt@FreeBSD.org> Cc: ports@FreeBSD.org, FreeBSD Current <freebsd-current@freebsd.org> Subject: pkg SAT_SOLVER bugs Message-ID: <416359ce-1dcd-1160-5c56-f120a0f6358f@selasky.org> In-Reply-To: <5593D0AE.2010205@selasky.org> References: <20150414200459.GE39658@ivaldir.etoilebsd.net> <20150421103454.GR1394@zxy.spb.ru> <5593D0AE.2010205@selasky.org>
next in thread | previous in thread | raw e-mail | index | archive | help
This is a multi-part message in MIME format.
--------------AA5E85B16E334BA99B677397
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Hi,
I found some bugs in PKG with regard to the SAT_SOLVER environment
variable. Please find patch attached :-)
Issues fixed:
1) No need to use hash table when generating SAT rules for external
solver. Variables are already in a linear array. Fix encoding and
decoding of SAT data.
2) Endless variable loop caused pkg to crash.
3) it->inverse was checked for non-zero, while it should actually be
checked for -1 only. SAT rules produces were all negative.
How to verify:
make -C /usr/ports/math/picosat all install clean
env SAT_SOLVER=picosat pkg upgrade
--HPS
--------------AA5E85B16E334BA99B677397
Content-Type: text/x-patch;
name="pkg.diff"
Content-Transfer-Encoding: 7bit
Content-Disposition: attachment;
filename="pkg.diff"
--- ./work/pkg-1.8.99.6/libpkg/pkg_solve.c.orig 2016-06-27 10:32:46.119810000 +0200
+++ ./work/pkg-1.8.99.6/libpkg/pkg_solve.c 2016-06-27 12:28:07.901757000 +0200
@@ -118,8 +118,6 @@
#define PKG_SOLVE_CHECK_ITEM(item) \
((item)->var->to_install ^ (item)->inverse)
-#define PKG_SOLVE_VAR_NEXT(a, e) ((e) == NULL ? &a[0] : (e + 1))
-
/*
* Utilities to convert jobs to SAT rule
*/
@@ -1302,45 +1300,23 @@
fprintf(file, "}\n");
}
-struct pkg_solve_ordered_variable {
- struct pkg_solve_variable *var;
- int order;
- UT_hash_handle hh;
-};
-
int
pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f)
{
- struct pkg_solve_ordered_variable *ordered_variables = NULL, *nord;
- struct pkg_solve_variable *var;
struct pkg_solve_rule *rule;
struct pkg_solve_item *it;
- int cur_ord = 1;
-
- /* Order variables */
- var = NULL;
- while ((var = PKG_SOLVE_VAR_NEXT(problem->variables, var))) {
- nord = calloc(1, sizeof(struct pkg_solve_ordered_variable));
- nord->order = cur_ord ++;
- nord->var = var;
- HASH_ADD_PTR(ordered_variables, var, nord);
- }
fprintf(f, "p cnf %d %zu\n", (int)problem->nvars, kv_size(problem->rules));
for (unsigned int i = 0; i < kv_size(problem->rules); i++) {
rule = kv_A(problem->rules, i);
LL_FOREACH(rule->items, it) {
- HASH_FIND_PTR(ordered_variables, &it->var, nord);
- if (nord != NULL) {
- fprintf(f, "%s%d ", (it->inverse ? "-" : ""), nord->order);
- }
+ size_t order = it->var - problem->variables;
+ if (order < problem->nvars)
+ fprintf(f, "%ld ", (long)((order + 1) * it->inverse));
}
fprintf(f, "0\n");
}
-
- HASH_FREE(ordered_variables, free);
-
return (EPKG_OK);
}
@@ -1443,26 +1419,42 @@
return (EPKG_OK);
}
+static bool
+pkg_solve_parse_sat_output_store(struct pkg_solve_problem *problem, const char *var_str)
+{
+ struct pkg_solve_variable *var;
+ ssize_t order;
+
+ order = strtol(var_str, NULL, 10);
+ if (order == 0)
+ return (true);
+ if (order < 0) {
+ /* negative value means false */
+ order = - order - 1;
+ if ((size_t)order < problem->nvars) {
+ var = problem->variables + order;
+ var->flags &= ~PKG_VAR_INSTALL;
+ }
+ } else {
+ /* positive value means true */
+ order = order - 1;
+ if ((size_t)order < problem->nvars) {
+ var = problem->variables + order;
+ var->flags |= PKG_VAR_INSTALL;
+ }
+ }
+ return (false);
+}
+
int
pkg_solve_parse_sat_output(FILE *f, struct pkg_solve_problem *problem)
{
- struct pkg_solve_ordered_variable *ordered_variables = NULL, *nord;
- struct pkg_solve_variable *var;
- int cur_ord = 1, ret = EPKG_OK;
+ int ret = EPKG_OK;
char *line = NULL, *var_str, *begin;
size_t linecap = 0;
ssize_t linelen;
bool got_sat = false, done = false;
- /* Order variables */
- var = NULL;
- while ((var = PKG_SOLVE_VAR_NEXT(problem->variables, var))) {
- nord = calloc(1, sizeof(struct pkg_solve_ordered_variable));
- nord->order = cur_ord ++;
- nord->var = var;
- HASH_ADD_INT(ordered_variables, order, nord);
- }
-
while ((linelen = getline(&line, &linecap, f)) > 0) {
if (strncmp(line, "SAT", 3) == 0) {
got_sat = true;
@@ -1474,22 +1466,8 @@
/* Skip unexpected lines */
if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
continue;
- cur_ord = 0;
- cur_ord = abs((int)strtol(var_str, NULL, 10));
- if (cur_ord == 0) {
+ if (pkg_solve_parse_sat_output_store(problem, var_str))
done = true;
- break;
- }
-
- HASH_FIND_INT(ordered_variables, &cur_ord, nord);
- if (nord != NULL) {
- if (*var_str == '-') {
- nord->var->flags &= ~PKG_VAR_INSTALL;
- }
- else {
- nord->var->flags |= PKG_VAR_INSTALL;
- }
- }
} while (begin != NULL);
}
else if (strncmp(line, "v ", 2) == 0) {
@@ -1499,23 +1477,8 @@
/* Skip unexpected lines */
if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
continue;
- cur_ord = 0;
- cur_ord = abs((int)strtol(var_str, NULL, 10));
- if (cur_ord == 0) {
+ if (pkg_solve_parse_sat_output_store(problem, var_str))
done = true;
- break;
- }
-
- HASH_FIND_INT(ordered_variables, &cur_ord, nord);
-
- if (nord != NULL) {
- if (*var_str == '-') {
- nord->var->flags &= ~PKG_VAR_INSTALL;
- }
- else {
- nord->var->flags |= PKG_VAR_INSTALL;
- }
- }
} while (begin != NULL);
}
else {
@@ -1531,7 +1494,6 @@
ret = EPKG_FATAL;
}
- HASH_FREE(ordered_variables, free);
free(line);
return (ret);
--------------AA5E85B16E334BA99B677397--
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?416359ce-1dcd-1160-5c56-f120a0f6358f>