From owner-freebsd-ports@freebsd.org Mon Jun 27 10:34:31 2016 Return-Path: Delivered-To: freebsd-ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id 0D96AB80366 for ; Mon, 27 Jun 2016 10:34:31 +0000 (UTC) (envelope-from hps@selasky.org) Received: from mailman.ysv.freebsd.org (mailman.ysv.freebsd.org [IPv6:2001:1900:2254:206a::50:5]) by mx1.freebsd.org (Postfix) with ESMTP id ED2A32222 for ; Mon, 27 Jun 2016 10:34:30 +0000 (UTC) (envelope-from hps@selasky.org) Received: by mailman.ysv.freebsd.org (Postfix) id EC832B80365; Mon, 27 Jun 2016 10:34:30 +0000 (UTC) Delivered-To: ports@mailman.ysv.freebsd.org Received: from mx1.freebsd.org (mx1.freebsd.org [IPv6:2001:1900:2254:206a::19:1]) by mailman.ysv.freebsd.org (Postfix) with ESMTP id EC079B80363; Mon, 27 Jun 2016 10:34:30 +0000 (UTC) (envelope-from hps@selasky.org) Received: from mail.turbocat.net (heidi.turbocat.net [88.198.202.214]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (Client did not present a certificate) by mx1.freebsd.org (Postfix) with ESMTPS id 459AC2221; Mon, 27 Jun 2016 10:34:30 +0000 (UTC) (envelope-from hps@selasky.org) Received: from laptop015.home.selasky.org (unknown [62.141.129.119]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by mail.turbocat.net (Postfix) with ESMTPSA id 5CE521FE022; Mon, 27 Jun 2016 12:34:21 +0200 (CEST) Subject: pkg SAT_SOLVER bugs To: Slawa Olhovchenkov , Baptiste Daroussin References: <20150414200459.GE39658@ivaldir.etoilebsd.net> <20150421103454.GR1394@zxy.spb.ru> <5593D0AE.2010205@selasky.org> Cc: ports@FreeBSD.org, FreeBSD Current From: Hans Petter Selasky Message-ID: <416359ce-1dcd-1160-5c56-f120a0f6358f@selasky.org> Date: Mon, 27 Jun 2016 12:38:02 +0200 User-Agent: Mozilla/5.0 (X11; FreeBSD amd64; rv:45.0) Gecko/20100101 Thunderbird/45.0 MIME-Version: 1.0 In-Reply-To: <5593D0AE.2010205@selasky.org> Content-Type: multipart/mixed; boundary="------------AA5E85B16E334BA99B677397" X-BeenThere: freebsd-ports@freebsd.org X-Mailman-Version: 2.1.22 Precedence: list List-Id: Porting software to FreeBSD List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 27 Jun 2016 10:34:31 -0000 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--