Branch data Line data Source code
1 : : /*-
2 : : * Copyright (c) 2013-2017 Vsevolod Stakhov <vsevolod@FreeBSD.org>
3 : : * Copyright (c) 2024 Serenity Cyber Security, LLC <license@futurecrew.ru>
4 : : * Author: Gleb Popov <arrowd@FreeBSD.org>
5 : : * All rights reserved.
6 : : *
7 : : * Redistribution and use in source and binary forms, with or without
8 : : * modification, are permitted provided that the following conditions
9 : : * are met:
10 : : * 1. Redistributions of source code must retain the above copyright
11 : : * notice, this list of conditions and the following disclaimer
12 : : * in this position and unchanged.
13 : : * 2. Redistributions in binary form must reproduce the above copyright
14 : : * notice, this list of conditions and the following disclaimer in the
15 : : * documentation and/or other materials provided with the distribution.
16 : : *
17 : : * THIS SOFTWARE IS PROVIDED BY THE AUTHOR(S) ``AS IS'' AND ANY EXPRESS OR
18 : : * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES
19 : : * OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
20 : : * IN NO EVENT SHALL THE AUTHOR(S) BE LIABLE FOR ANY DIRECT, INDIRECT,
21 : : * INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT
22 : : * NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
23 : : * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
24 : : * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
25 : : * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF
26 : : * THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27 : : */
28 : :
29 : : #include <sys/param.h>
30 : : #include <sys/mount.h>
31 : :
32 : : #include <assert.h>
33 : : #include <errno.h>
34 : : #include <stdbool.h>
35 : : #include <stdlib.h>
36 : : #include <stdio.h>
37 : : #include <string.h>
38 : : #include <ctype.h>
39 : : #include <math.h>
40 : : #include <tllist.h>
41 : :
42 : : #include "pkg.h"
43 : : #include "pkghash.h"
44 : : #include "private/event.h"
45 : : #include "private/pkg.h"
46 : : #include "private/pkgdb.h"
47 : : #include "private/pkg_jobs.h"
48 : : #include "picosat.h"
49 : :
50 : : struct pkg_solve_item;
51 : :
52 : : #define dbg(x, ...) pkg_dbg(PKG_DBG_SOLVER, x, __VA_ARGS__)
53 : :
54 : : enum pkg_solve_rule_type {
55 : : PKG_RULE_DEPEND = 0,
56 : : PKG_RULE_UPGRADE_CONFLICT,
57 : : PKG_RULE_EXPLICIT_CONFLICT,
58 : : PKG_RULE_REQUEST_CONFLICT,
59 : : PKG_RULE_REQUEST,
60 : : PKG_RULE_REQUIRE,
61 : : PKG_RULE_MAX
62 : : };
63 : :
64 : : static const char *rule_reasons[] = {
65 : : [PKG_RULE_DEPEND] = "dependency",
66 : : [PKG_RULE_UPGRADE_CONFLICT] = "upgrade",
67 : : [PKG_RULE_REQUEST_CONFLICT] = "candidates",
68 : : [PKG_RULE_EXPLICIT_CONFLICT] = "conflict",
69 : : [PKG_RULE_REQUEST] = "request",
70 : : [PKG_RULE_REQUIRE] = "require",
71 : : [PKG_RULE_MAX] = NULL
72 : : };
73 : :
74 : : enum pkg_solve_variable_flags {
75 : : PKG_VAR_INSTALL = (1 << 0),
76 : : PKG_VAR_TOP = (1 << 1),
77 : : PKG_VAR_FAILED = (1 << 2),
78 : : PKG_VAR_ASSUMED = (1 << 3),
79 : : PKG_VAR_ASSUMED_TRUE = (1 << 4)
80 : : };
81 : : struct pkg_solve_variable {
82 : : struct pkg_job_universe_item *unit;
83 : : unsigned int flags;
84 : : int order;
85 : : const char *digest;
86 : : const char *uid;
87 : : const char *assumed_reponame;
88 : : struct pkg_solve_variable *next, *prev;
89 : : };
90 : :
91 : : struct pkg_solve_item {
92 : : int nitems;
93 : : int nresolved;
94 : : struct pkg_solve_variable *var;
95 : : int inverse;
96 : : struct pkg_solve_item *prev,*next;
97 : : };
98 : :
99 : : struct pkg_solve_rule {
100 : : enum pkg_solve_rule_type reason;
101 : : struct pkg_solve_item *items;
102 : : };
103 : :
104 : : struct pkg_solve_problem {
105 : : struct pkg_jobs *j;
106 : : tll(struct pkg_solve_rule *) rules;
107 : : pkghash *variables_by_uid;
108 : : struct pkg_solve_variable *variables;
109 : : PicoSAT *sat;
110 : : size_t nvars;
111 : : };
112 : :
113 : : struct pkg_solve_impl_graph {
114 : : struct pkg_solve_variable *var;
115 : : struct pkg_solve_impl_graph *prev, *next;
116 : : };
117 : :
118 : : /*
119 : : * Use XOR here to implement the following logic:
120 : : * atom is true if it is installed and not inverted or
121 : : * if it is not installed but inverted
122 : : */
123 : : #define PKG_SOLVE_CHECK_ITEM(item) \
124 : : ((item)->var->to_install ^ (item)->inverse)
125 : :
126 : : /*
127 : : * Utilities to convert jobs to SAT rule
128 : : */
129 : :
130 : : static void
131 : 970 : pkg_solve_item_new(struct pkg_solve_rule *rule, struct pkg_solve_variable *var,
132 : : int inverse)
133 : : {
134 : : struct pkg_solve_item *it;
135 : :
136 : 970 : it = xcalloc(1, sizeof(struct pkg_solve_item));
137 : 970 : it->var = var;
138 : 970 : it->inverse = inverse;
139 [ + + ]: 970 : it->nitems = rule->items ? rule->items->nitems + 1 : 1;
140 [ + + ]: 970 : DL_APPEND(rule->items, it);
141 : 970 : }
142 : :
143 : : static struct pkg_solve_rule *
144 : 550 : pkg_solve_rule_new(enum pkg_solve_rule_type reason)
145 : : {
146 : : struct pkg_solve_rule *result;
147 : :
148 : 550 : result = xcalloc(1, sizeof(struct pkg_solve_rule));
149 : 550 : result->reason = reason;
150 : :
151 : 550 : return (result);
152 : : }
153 : :
154 : : static void
155 : 377 : pkg_solve_variable_set(struct pkg_solve_variable *var,
156 : : struct pkg_job_universe_item *item)
157 : : {
158 : 377 : var->unit = item;
159 : : /* XXX: Is it safe to save a ptr here ? */
160 : 377 : var->digest = item->pkg->digest;
161 : 377 : var->uid = item->pkg->uid;
162 : 377 : var->prev = var;
163 : 377 : }
164 : :
165 : : static void
166 : 550 : pkg_solve_rule_free(struct pkg_solve_rule *rule)
167 : : {
168 : : struct pkg_solve_item *it, *tmp;
169 : :
170 [ + + - + : 1520 : LL_FOREACH_SAFE(rule->items, it, tmp) {
+ + ]
171 : 970 : free(it);
172 : 970 : }
173 : 550 : free(rule);
174 : 550 : }
175 : :
176 : :
177 : : void
178 : 176 : pkg_solve_problem_free(struct pkg_solve_problem *problem)
179 : : {
180 [ + + + + : 489 : tll_free_and_free(problem->rules, pkg_solve_rule_free);
+ + ]
181 : 176 : pkghash_destroy(problem->variables_by_uid);
182 : 176 : picosat_reset(problem->sat);
183 : 176 : free(problem->variables);
184 : 176 : free(problem);
185 : 176 : }
186 : :
187 : :
188 : : static void
189 : 0 : pkg_print_rule_buf(struct pkg_solve_rule *rule, xstring *sb)
190 : : {
191 : 0 : struct pkg_solve_item *it = rule->items, *key_elt = NULL;
192 : :
193 : 0 : fprintf(sb->fp, "%s rule: ", rule_reasons[rule->reason]);
194 [ # # # # : 0 : switch(rule->reason) {
# # ]
195 : : case PKG_RULE_DEPEND:
196 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
197 [ # # ]: 0 : if (it->inverse == -1) {
198 : 0 : key_elt = it;
199 : 0 : break;
200 : : }
201 : 0 : }
202 [ # # ]: 0 : if (key_elt) {
203 : 0 : fprintf(sb->fp, "package %s%s depends on: ", key_elt->var->uid,
204 : 0 : (key_elt->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
205 : 0 : }
206 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
207 [ # # ]: 0 : if (it != key_elt) {
208 : 0 : fprintf(sb->fp, "%s%s", it->var->uid,
209 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
210 : 0 : }
211 : 0 : }
212 : 0 : break;
213 : : case PKG_RULE_UPGRADE_CONFLICT:
214 : 0 : fprintf(sb->fp, "upgrade local %s-%s to remote %s-%s",
215 : 0 : it->var->uid, it->var->unit->pkg->version,
216 : 0 : it->next->var->uid, it->next->var->unit->pkg->version);
217 : 0 : break;
218 : : case PKG_RULE_EXPLICIT_CONFLICT:
219 : 0 : fprintf(sb->fp, "The following packages conflict with each other: ");
220 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
221 : 0 : fprintf(sb->fp, "%s-%s%s%s", it->var->unit->pkg->uid, it->var->unit->pkg->version,
222 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)",
223 : 0 : it->next ? ", " : "");
224 : 0 : }
225 : 0 : break;
226 : : case PKG_RULE_REQUIRE:
227 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
228 [ # # ]: 0 : if (it->inverse == -1) {
229 : 0 : key_elt = it;
230 : 0 : break;
231 : : }
232 : 0 : }
233 [ # # ]: 0 : if (key_elt) {
234 : 0 : fprintf(sb->fp, "package %s%s depends on a requirement provided by: ",
235 : 0 : key_elt->var->uid,
236 : 0 : (key_elt->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
237 : 0 : }
238 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
239 [ # # ]: 0 : if (it != key_elt) {
240 : 0 : fprintf(sb->fp, "%s%s", it->var->uid,
241 : 0 : (it->var->unit->pkg->type == PKG_INSTALLED) ? "(l)" : "(r)");
242 : 0 : }
243 : 0 : }
244 : 0 : break;
245 : : case PKG_RULE_REQUEST_CONFLICT:
246 : 0 : fprintf(sb->fp, "The following packages in request are candidates for installation: ");
247 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
248 : 0 : fprintf(sb->fp, "%s-%s%s", it->var->uid, it->var->unit->pkg->version,
249 : 0 : it->next ? ", " : "");
250 : 0 : }
251 : 0 : break;
252 : : default:
253 : 0 : break;
254 : : }
255 : 0 : }
256 : :
257 : : static void
258 : 313 : pkg_debug_print_rule(struct pkg_solve_rule *rule)
259 : : {
260 : : xstring *sb;
261 : :
262 [ + - ]: 313 : if (ctx.debug_level < 3)
263 : 313 : return;
264 : :
265 : 0 : sb = xstring_new();
266 : :
267 : 0 : pkg_print_rule_buf(rule, sb);
268 : :
269 : 0 : fflush(sb->fp);
270 : 0 : dbg(2, "rule: %s", sb->buf);
271 : 0 : xstring_free(sb);
272 : 313 : }
273 : :
274 : : static int
275 : 17 : pkg_solve_handle_provide (struct pkg_solve_problem *problem,
276 : : struct pkg_job_provide *pr, struct pkg_solve_rule *rule,
277 : : struct pkg *orig, const char *reponame, int *cnt)
278 : : {
279 : : struct pkg_solve_variable *var, *curvar;
280 : : struct pkg_job_universe_item *un;
281 : : struct pkg *pkg;
282 : : bool libfound, providefound;
283 : :
284 : : /* Find the first package in the universe list */
285 : 17 : un = pr->un;
286 [ + + ]: 22 : while (un->prev->next != NULL) {
287 : 5 : un = un->prev;
288 : : }
289 : :
290 : : /* Find the corresponding variables chain */
291 : :
292 : 17 : var = pkghash_get_value(problem->variables_by_uid, un->pkg->uid);
293 [ + + ]: 41 : LL_FOREACH(var, curvar) {
294 : : /*
295 : : * For each provide we need to check whether this package
296 : : * actually provides this require
297 : : */
298 : 24 : libfound = providefound = false;
299 : 24 : pkg = curvar->unit->pkg;
300 : :
301 [ + + ]: 24 : if (pr->is_shlib) {
302 : 4 : libfound = stringlist_contains(&pkg->shlibs_provided, pr->provide);
303 : : /* Skip incompatible ABI as well */
304 [ + - + - ]: 4 : if (libfound && !STREQ(pkg->abi, orig->abi)) {
305 : 0 : dbg(2, "require %s: package %s-%s(%c) provides wrong ABI %s, "
306 : : "wanted %s", pr->provide, pkg->name, pkg->version,
307 : : pkg->type == PKG_INSTALLED ? 'l' : 'r', pkg->abi, orig->abi);
308 : 0 : continue;
309 : : }
310 : 4 : }
311 : : else {
312 : 20 : providefound = stringlist_contains(&pkg->provides, pr->provide);
313 : : }
314 : :
315 [ + + + + ]: 24 : if (!providefound && !libfound) {
316 : 7 : dbg(4, "%s provide is not satisfied by %s-%s(%c)", pr->provide,
317 : : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ?
318 : : 'l' : 'r');
319 : 7 : continue;
320 : : }
321 : :
322 [ - + ]: 17 : if (curvar->assumed_reponame == NULL) {
323 : 17 : curvar->assumed_reponame = reponame;
324 : 17 : }
325 : :
326 : 17 : dbg(4, "%s provide is satisfied by %s-%s(%c)", pr->provide,
327 : : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ?
328 : : 'l' : 'r');
329 : :
330 : 17 : pkg_solve_item_new(rule, curvar, 1);
331 : 17 : (*cnt)++;
332 : 17 : }
333 : :
334 : 17 : return (EPKG_OK);
335 : : }
336 : :
337 : : static int
338 : 129 : pkg_solve_add_depend_rule(struct pkg_solve_problem *problem,
339 : : struct pkg_solve_variable *var,
340 : : struct pkg_dep *dep,
341 : : const char *reponame)
342 : : {
343 : : const char *uid;
344 : : struct pkg_solve_variable *depvar, *curvar;
345 : 129 : struct pkg_solve_rule *rule = NULL;
346 : 129 : int cnt = 0;
347 : : struct pkg_dep *cur;
348 : :
349 : : /* Dependency rule: (!A | B1 | B2 | B3...) must be true */
350 : 129 : rule = pkg_solve_rule_new(PKG_RULE_DEPEND);
351 : : /* !A */
352 : 129 : pkg_solve_item_new(rule, var, -1);
353 : :
354 [ + + ]: 258 : LL_FOREACH2(dep, cur, alt_next) {
355 : 129 : uid = cur->uid;
356 : 129 : depvar = NULL;
357 : 129 : depvar = pkghash_get_value(problem->variables_by_uid, uid);
358 [ + + ]: 129 : if (depvar == NULL) {
359 : 10 : dbg(2, "cannot find variable dependency %s", uid);
360 : 10 : continue;
361 : : }
362 : :
363 : : /* B1 | B2 | ... */
364 : 119 : cnt = 1;
365 [ + + ]: 291 : LL_FOREACH(depvar, curvar) {
366 : : /* Propagate reponame */
367 [ - + ]: 172 : if (curvar->assumed_reponame == NULL) {
368 : 172 : curvar->assumed_reponame = reponame;
369 : 172 : }
370 : :
371 : 172 : pkg_solve_item_new(rule, curvar, 1);
372 : 172 : cnt++;
373 : 172 : }
374 : 119 : }
375 : :
376 [ + + ]: 129 : if (cnt == 0) {
377 : 10 : dbg(2, "cannot find any suitable dependency for %s", var->uid);
378 : 10 : pkg_solve_rule_free(rule);
379 : :
380 : 10 : return (EPKG_FATAL);
381 : : }
382 : :
383 [ + + + + : 119 : tll_push_front(problem->rules, rule);
+ - - + +
+ ]
384 : :
385 : 119 : return (EPKG_OK);
386 : 129 : }
387 : :
388 : : static int
389 : 40 : pkg_solve_add_conflict_rule(struct pkg_solve_problem *problem,
390 : : struct pkg *pkg,
391 : : struct pkg_solve_variable *var,
392 : : struct pkg_conflict *conflict)
393 : : {
394 : : const char *uid;
395 : : struct pkg_solve_variable *confvar, *curvar;
396 : 40 : struct pkg_solve_rule *rule = NULL;
397 : : struct pkg *other;
398 : :
399 : 40 : uid = conflict->uid;
400 : 40 : confvar = pkghash_get_value(problem->variables_by_uid, uid);
401 [ + - ]: 40 : if (confvar == NULL) {
402 : 0 : dbg(2, "cannot find conflict %s", uid);
403 : 0 : return (EPKG_END);
404 : : }
405 : :
406 : : /* Add conflict rule from each of the alternative */
407 [ + + ]: 118 : LL_FOREACH(confvar, curvar) {
408 : 78 : other = curvar->unit->pkg;
409 [ + + ]: 78 : if (conflict->type == PKG_CONFLICT_REMOTE_LOCAL) {
410 : : /* Skip unappropriate packages */
411 [ + + ]: 59 : if (pkg->type == PKG_INSTALLED) {
412 [ + + ]: 32 : if (other->type == PKG_INSTALLED)
413 : 9 : continue;
414 : 23 : }
415 : : else {
416 [ + + ]: 27 : if (other->type != PKG_INSTALLED)
417 : 11 : continue;
418 : : }
419 : 39 : }
420 [ - + ]: 19 : else if (conflict->type == PKG_CONFLICT_REMOTE_REMOTE) {
421 [ - + ]: 19 : if (pkg->type == PKG_INSTALLED)
422 : 0 : continue;
423 : :
424 [ + + ]: 19 : if (other->type == PKG_INSTALLED)
425 : 6 : continue;
426 : 13 : }
427 : : /*
428 : : * Also if a conflict is digest specific then we skip
429 : : * variables with mismatched digests
430 : : */
431 [ - + ]: 52 : if (conflict->digest) {
432 [ + + ]: 52 : if (!STREQ(conflict->digest, other->digest))
433 : 12 : continue;
434 : 40 : }
435 : :
436 : : /* Conflict rule: (!A | !Bx) must be true */
437 : 40 : rule = pkg_solve_rule_new(PKG_RULE_EXPLICIT_CONFLICT);
438 : : /* !A */
439 : 40 : pkg_solve_item_new(rule, var, -1);
440 : : /* !Bx */
441 : 40 : pkg_solve_item_new(rule, curvar, -1);
442 : :
443 [ + + + + : 40 : tll_push_front(problem->rules, rule);
+ - - + +
+ ]
444 : 40 : }
445 : :
446 : 40 : return (EPKG_OK);
447 : 40 : }
448 : :
449 : : static int
450 : 29 : pkg_solve_add_require_rule(struct pkg_solve_problem *problem,
451 : : struct pkg_solve_variable *var,
452 : : const char *requirement,
453 : : const char *reponame)
454 : : {
455 : : struct pkg_solve_rule *rule;
456 : : struct pkg_job_provide *pr, *prhead;
457 : : struct pkg *pkg;
458 : : int cnt;
459 : :
460 : 29 : pkg = var->unit->pkg;
461 : :
462 : 29 : prhead = pkghash_get_value(problem->j->universe->provides, requirement);
463 [ + + ]: 29 : if (prhead != NULL) {
464 : 17 : dbg(4, "Add require rule: %s-%s(%c) wants %s",
465 : : pkg->name, pkg->version, pkg->type == PKG_INSTALLED ? 'l' : 'r',
466 : : requirement);
467 : : /* Require rule: ( !A | P1 | P2 | P3 ... ) must be true */
468 : 17 : rule = pkg_solve_rule_new(PKG_RULE_REQUIRE);
469 : : /* !A */
470 : 17 : pkg_solve_item_new(rule, var, -1);
471 : : /* P1 | P2 | ... */
472 : 17 : cnt = 1;
473 [ + + ]: 34 : LL_FOREACH(prhead, pr) {
474 [ - + - + ]: 34 : if (pkg_solve_handle_provide(problem, pr, rule, pkg, reponame, &cnt)
475 : 17 : != EPKG_OK) {
476 : 0 : free(rule);
477 : 0 : return (EPKG_FATAL);
478 : : }
479 : 17 : }
480 : :
481 [ + - ]: 17 : if (cnt > 1) {
482 [ + + + + : 17 : tll_push_front(problem->rules, rule);
+ - - + +
+ ]
483 : 17 : }
484 : : else {
485 : : /* Missing dependencies... */
486 : 0 : free(rule);
487 : : }
488 : 17 : }
489 : : else {
490 : : /*
491 : : * XXX:
492 : : * This is terribly broken now so ignore till provides/requires
493 : : * are really fixed.
494 : : */
495 : 12 : dbg(1, "for package: %s cannot find provide for requirement: %s",
496 : : pkg->name, requirement);
497 : : }
498 : :
499 : 29 : return (EPKG_OK);
500 : 29 : }
501 : :
502 : : static struct pkg_solve_variable *
503 : 508 : pkg_solve_find_var_in_chain(struct pkg_solve_variable *var,
504 : : struct pkg_job_universe_item *item)
505 : : {
506 : : struct pkg_solve_variable *cur;
507 : :
508 [ + - ]: 508 : assert(var != NULL);
509 [ + - ]: 607 : LL_FOREACH(var, cur) {
510 [ + + ]: 607 : if (cur->unit == item) {
511 : 508 : return (cur);
512 : : }
513 : 99 : }
514 : :
515 : 0 : return (NULL);
516 : 508 : }
517 : :
518 : : static int
519 : 227 : pkg_solve_add_request_rule(struct pkg_solve_problem *problem,
520 : : struct pkg_solve_variable *var, struct pkg_job_request *req, int inverse)
521 : : {
522 : : struct pkg_solve_rule *rule;
523 : : struct pkg_job_request_item *item, *confitem;
524 : : struct pkg_solve_variable *confvar, *curvar;
525 : : int cnt;
526 : :
527 : 227 : dbg(4, "add variable from %s request with uid %s-%s",
528 : : inverse < 0 ? "delete" : "install", var->uid, var->digest);
529 : :
530 : : /*
531 : : * Get the suggested item
532 : : */
533 : 227 : var = pkghash_get_value(problem->variables_by_uid, req->item->pkg->uid);
534 : 227 : var = pkg_solve_find_var_in_chain(var, req->item->unit);
535 [ + - ]: 227 : assert(var != NULL);
536 : : /* Assume the most significant variable */
537 : 227 : picosat_assume(problem->sat, var->order * inverse);
538 : :
539 : : /*
540 : : * Add clause for any of candidates:
541 : : * A1 | A2 | ... | An
542 : : */
543 : 227 : rule = pkg_solve_rule_new(PKG_RULE_REQUEST);
544 : :
545 : 227 : cnt = 0;
546 : :
547 [ + + ]: 508 : LL_FOREACH(req->item, item) {
548 : 281 : curvar = pkg_solve_find_var_in_chain(var, item->unit);
549 [ + - ]: 281 : assert(curvar != NULL);
550 : 281 : pkg_solve_item_new(rule, curvar, inverse);
551 : : /* All request variables are top level */
552 : 281 : curvar->flags |= PKG_VAR_TOP;
553 : :
554 [ + + ]: 281 : if (inverse > 0) {
555 : 250 : curvar->flags |= PKG_VAR_INSTALL;
556 : 250 : }
557 : :
558 : 281 : cnt++;
559 : 281 : }
560 : :
561 [ + + + - ]: 227 : if (cnt > 1 && var->unit->inhash != 0) {
562 [ # # # # : 0 : tll_push_front(problem->rules, rule);
# # # # #
# ]
563 : : /* Also need to add pairs of conflicts */
564 [ # # ]: 0 : LL_FOREACH(req->item, item) {
565 : 0 : curvar = pkg_solve_find_var_in_chain(var, item->unit);
566 [ # # ]: 0 : assert(curvar != NULL);
567 [ # # ]: 0 : if (item->next == NULL)
568 : 0 : continue;
569 [ # # ]: 0 : LL_FOREACH(item->next, confitem) {
570 : 0 : confvar = pkg_solve_find_var_in_chain(var, confitem->unit);
571 [ # # ]: 0 : assert(confvar != NULL && confvar != curvar && confvar != var);
572 : : /* Conflict rule: (!A | !Bx) must be true */
573 : 0 : rule = pkg_solve_rule_new(PKG_RULE_REQUEST_CONFLICT);
574 : : /* !A */
575 : 0 : pkg_solve_item_new(rule, curvar, -1);
576 : : /* !Bx */
577 : 0 : pkg_solve_item_new(rule, confvar, -1);
578 : :
579 [ # # # # : 0 : tll_push_front(problem->rules, rule);
# # # # #
# ]
580 : 0 : }
581 : 0 : }
582 : 0 : }
583 : : else {
584 : : /* No need to add unary rules as we added the assumption already */
585 : 227 : pkg_solve_rule_free(rule);
586 : : }
587 : :
588 : 227 : var->flags |= PKG_VAR_TOP;
589 [ + + ]: 227 : if (inverse > 0) {
590 : 196 : var->flags |= PKG_VAR_INSTALL;
591 : 196 : }
592 : :
593 : 227 : return (EPKG_OK);
594 : : }
595 : :
596 : : static int
597 : 81 : pkg_solve_add_chain_rule(struct pkg_solve_problem *problem,
598 : : struct pkg_solve_variable *var)
599 : : {
600 : : struct pkg_solve_variable *curvar, *confvar;
601 : : struct pkg_solve_rule *rule;
602 : :
603 : : /* Rewind to first */
604 [ - + ]: 81 : while (var->prev->next != NULL) {
605 : 0 : var = var->prev;
606 : : }
607 : :
608 [ - + ]: 190 : LL_FOREACH(var, curvar) {
609 : : /* Conflict rule: (!Ax | !Ay) must be true */
610 [ + + ]: 190 : if (curvar->next == NULL) {
611 : 81 : break;
612 : : }
613 : :
614 [ + + ]: 246 : LL_FOREACH(curvar->next, confvar) {
615 : 137 : rule = pkg_solve_rule_new(PKG_RULE_UPGRADE_CONFLICT);
616 : : /* !Ax */
617 : 137 : pkg_solve_item_new(rule, curvar, -1);
618 : : /* !Ay */
619 : 137 : pkg_solve_item_new(rule, confvar, -1);
620 : :
621 [ + + + + : 137 : tll_push_front(problem->rules, rule);
+ - - + +
+ ]
622 : 137 : }
623 : 109 : }
624 : :
625 : 81 : return (EPKG_OK);
626 : : }
627 : :
628 : : static int
629 : 268 : pkg_solve_process_universe_variable(struct pkg_solve_problem *problem,
630 : : struct pkg_solve_variable *var)
631 : : {
632 : : struct pkg_dep *dep;
633 : : struct pkg_conflict *conflict;
634 : : struct pkg *pkg;
635 : : struct pkg_solve_variable *cur_var;
636 : 268 : struct pkg_jobs *j = problem->j;
637 : 268 : struct pkg_job_request *jreq = NULL;
638 : 268 : bool chain_added = false;
639 : 268 : bool force = j->flags & PKG_FLAG_FORCE;
640 : :
641 [ + + ]: 645 : LL_FOREACH(var, cur_var) {
642 : 377 : pkg = cur_var->unit->pkg;
643 : :
644 : : /* Request */
645 [ + + ]: 377 : if (!(cur_var->flags & PKG_VAR_TOP)) {
646 : 305 : jreq = pkghash_get_value(j->request_add, cur_var->uid);
647 [ + + ]: 305 : if (jreq != NULL)
648 : 196 : pkg_solve_add_request_rule(problem, cur_var, jreq, 1);
649 : 305 : jreq = pkghash_get_value(j->request_delete, cur_var->uid);
650 [ + + ]: 305 : if (jreq != NULL)
651 : 31 : pkg_solve_add_request_rule(problem, cur_var, jreq, -1);
652 : 305 : }
653 : :
654 [ + + ]: 377 : if (jreq) {
655 : 31 : cur_var->assumed_reponame = pkg->reponame;
656 : 31 : }
657 : :
658 : : /* Depends */
659 [ + + ]: 506 : LL_FOREACH(pkg->depends, dep) {
660 [ + + + + : 387 : if (pkg_solve_add_depend_rule(problem, cur_var, dep,
+ + ]
661 : 258 : cur_var->assumed_reponame) != EPKG_OK) {
662 : 10 : continue;
663 : : }
664 : 119 : }
665 : :
666 : : /* Conflicts */
667 [ + + ]: 417 : LL_FOREACH(pkg->conflicts, conflict) {
668 [ - + ]: 40 : if (pkg_solve_add_conflict_rule(problem, pkg, cur_var, conflict) !=
669 : : EPKG_OK)
670 : 0 : continue;
671 : 40 : }
672 : :
673 : : /* Shlibs */
674 [ + + + + : 402 : tll_foreach(pkg->shlibs_required, s) {
+ + ]
675 [ + + ]: 25 : if (pkghash_get(j->system_shlibs, s->item) != NULL) {
676 : : /* The shlib is provided by the system */
677 : 12 : continue;
678 : : }
679 [ - + - + : 39 : if (pkg_solve_add_require_rule(problem, cur_var,
- + ]
680 : 26 : s->item, cur_var->assumed_reponame) != EPKG_OK) {
681 : 0 : continue;
682 : : }
683 : 13 : }
684 [ + + + + : 393 : tll_foreach(pkg->requires, r) {
- + ]
685 [ - + - + : 48 : if (pkg_solve_add_require_rule(problem, cur_var,
- + ]
686 : 32 : r->item, cur_var->assumed_reponame) != EPKG_OK) {
687 : 0 : continue;
688 : : }
689 : 16 : }
690 : :
691 : : /*
692 : : * If this var chain contains mutually conflicting vars
693 : : * we need to register conflicts with all following
694 : : * vars
695 : : */
696 [ + + + + : 377 : if (!chain_added && (cur_var->next != NULL || cur_var->prev != var)) {
- + ]
697 [ - + ]: 81 : if (pkg_solve_add_chain_rule(problem, cur_var) != EPKG_OK)
698 : 0 : continue;
699 : :
700 : 81 : chain_added = true;
701 : 81 : }
702 : 377 : }
703 : :
704 : 268 : return (EPKG_OK);
705 : : }
706 : :
707 : : static int
708 : 268 : pkg_solve_add_variable(struct pkg_job_universe_item *un,
709 : : struct pkg_solve_problem *problem, size_t *n)
710 : : {
711 : : struct pkg_job_universe_item *ucur;
712 : 268 : struct pkg_solve_variable *var = NULL, *tvar = NULL;
713 : :
714 [ + + ]: 645 : LL_FOREACH(un, ucur) {
715 [ + - ]: 377 : assert(*n < problem->nvars);
716 : :
717 : : /* Add new variable */
718 : 377 : var = &problem->variables[*n];
719 : 377 : pkg_solve_variable_set(var, ucur);
720 : :
721 [ + + ]: 377 : if (tvar == NULL) {
722 : 268 : dbg(4, "add variable from universe with uid %s", var->uid);
723 [ + + - + ]: 364 : pkghash_safe_add(problem->variables_by_uid, var->uid, var, NULL);
724 : 268 : tvar = var;
725 : 268 : }
726 : : else {
727 : : /* Insert a variable to a chain */
728 [ + - ]: 109 : DL_APPEND(tvar, var);
729 : : }
730 : 377 : (*n) ++;
731 : 377 : var->order = *n;
732 : 377 : }
733 : :
734 : 268 : return (EPKG_OK);
735 : : }
736 : :
737 : : struct pkg_solve_problem *
738 : 176 : pkg_solve_jobs_to_sat(struct pkg_jobs *j)
739 : : {
740 : : struct pkg_solve_problem *problem;
741 : : struct pkg_job_universe_item *un;
742 : 176 : size_t i = 0;
743 : : pkghash_it it;
744 : :
745 : 176 : problem = xcalloc(1, sizeof(struct pkg_solve_problem));
746 : :
747 : 176 : problem->j = j;
748 : 176 : problem->nvars = j->universe->nitems;
749 : 176 : problem->variables = xcalloc(problem->nvars, sizeof(struct pkg_solve_variable));
750 : 176 : problem->sat = picosat_init();
751 : :
752 [ + - ]: 176 : if (problem->sat == NULL) {
753 : 0 : pkg_emit_errno("picosat_init", "pkg_solve_sat_problem");
754 : 0 : return (NULL);
755 : : }
756 : :
757 : 176 : picosat_adjust(problem->sat, problem->nvars);
758 : :
759 : : /* Parse universe */
760 : 176 : it = pkghash_iterator(j->universe->items);
761 [ + + ]: 444 : while (pkghash_next(&it)) {
762 : 268 : un = (struct pkg_job_universe_item *)it.value;
763 : : /* Add corresponding variables */
764 [ - + ]: 268 : if (pkg_solve_add_variable(un, problem, &i) == EPKG_FATAL)
765 : 0 : return (NULL);
766 : : }
767 : :
768 : : /* Add rules for all conflict chains */
769 : 176 : it = pkghash_iterator(j->universe->items);
770 [ + + ]: 444 : while (pkghash_next(&it)) {
771 : : struct pkg_solve_variable *var;
772 : :
773 : 268 : un = (struct pkg_job_universe_item *)it.value;
774 : 268 : var = pkghash_get_value(problem->variables_by_uid, un->pkg->uid);
775 [ - + ]: 268 : if (var == NULL) {
776 : 0 : pkg_emit_error("internal solver error: variable %s is not found",
777 : 0 : un->pkg->uid);
778 : 0 : return (NULL);
779 : : }
780 [ - + ]: 268 : if (pkg_solve_process_universe_variable(problem, var) != EPKG_OK)
781 : 0 : return (NULL);
782 : : }
783 : :
784 [ + + ]: 176 : if (tll_length(problem->rules) == 0)
785 : 107 : dbg(1, "problem has no requests");
786 : :
787 : 176 : return (problem);
788 : 176 : }
789 : :
790 : : static int
791 : 186 : pkg_solve_picosat_iter(struct pkg_solve_problem *problem, int iter __unused)
792 : : {
793 : : int res, i;
794 : : struct pkg_solve_variable *var, *cur;
795 : 186 : bool is_installed = false;
796 : :
797 : 186 : picosat_reset_phases(problem->sat);
798 : 186 : picosat_reset_scores(problem->sat);
799 : : /* Set initial guess */
800 [ + + ]: 618 : for (i = 0; i < problem->nvars; i ++) {
801 : 432 : var = &problem->variables[i];
802 : 432 : is_installed = false;
803 : :
804 [ + + ]: 738 : LL_FOREACH(var, cur) {
805 [ + + ]: 467 : if (cur->unit->pkg->type == PKG_INSTALLED) {
806 : 161 : is_installed = true;
807 : 161 : break;
808 : : }
809 : 306 : }
810 : :
811 [ + + ]: 432 : if (var->flags & PKG_VAR_TOP)
812 : 212 : continue;
813 : :
814 [ + + ]: 220 : if (!(var->flags & (PKG_VAR_FAILED|PKG_VAR_ASSUMED))) {
815 [ + + ]: 143 : if (is_installed) {
816 : 95 : picosat_set_default_phase_lit(problem->sat, i + 1, 1);
817 : 95 : picosat_set_more_important_lit(problem->sat, i + 1);
818 : 95 : }
819 [ + + + + ]: 48 : else if (!var->next && var->prev == var) {
820 : : /* Prefer not to install if have no local version */
821 : 10 : picosat_set_default_phase_lit(problem->sat, i + 1, -1);
822 : 10 : picosat_set_less_important_lit(problem->sat, i + 1);
823 : 10 : }
824 : 143 : }
825 [ + + ]: 77 : else if (var->flags & PKG_VAR_FAILED) {
826 [ + + ]: 13 : if (var->unit->pkg->type == PKG_INSTALLED) {
827 : 11 : picosat_set_default_phase_lit(problem->sat, i + 1, -1);
828 : 11 : picosat_set_less_important_lit(problem->sat, i + 1);
829 : 11 : }
830 : : else {
831 : 2 : picosat_set_default_phase_lit(problem->sat, i + 1, 1);
832 : 2 : picosat_set_more_important_lit(problem->sat, i + 1);
833 : : }
834 : :
835 : 13 : var->flags &= ~PKG_VAR_FAILED;
836 : 13 : }
837 : 220 : }
838 : :
839 : 186 : res = picosat_sat(problem->sat, -1);
840 : :
841 : 186 : return (res);
842 : : }
843 : :
844 : : static void
845 : 313 : pkg_solve_set_initial_assumption(struct pkg_solve_problem *problem,
846 : : struct pkg_solve_rule *rule)
847 : : {
848 : : struct pkg_job_universe_item *selected, *cur, *local, *first;
849 : : struct pkg_solve_item *item;
850 : : struct pkg_solve_variable *var, *cvar;
851 : 313 : bool conservative = false, prefer_local = false;
852 : 313 : const char *assumed_reponame = NULL;
853 : :
854 [ + + ]: 313 : if (problem->j->type == PKG_JOBS_INSTALL) {
855 : : /* Avoid upgrades on INSTALL job */
856 : 71 : conservative = true;
857 : 71 : prefer_local = true;
858 : 71 : }
859 : : else {
860 : 242 : conservative = pkg_object_bool(pkg_config_get("CONSERVATIVE_UPGRADE"));
861 : : }
862 : :
863 [ + + + ]: 313 : switch (rule->reason) {
864 : : case PKG_RULE_DEPEND:
865 : : /*
866 : : * The first item is dependent item, the next items are
867 : : * dependencies. We assume that all deps belong to a single
868 : : * upgrade chain.
869 : : */
870 [ + - ]: 119 : assert (rule->items != NULL);
871 : 119 : item = rule->items;
872 : 119 : var = item->var;
873 : 119 : assumed_reponame = var->assumed_reponame;
874 : :
875 : : /* Check what we are depending on */
876 [ + + ]: 119 : if (!(var->flags & (PKG_VAR_TOP|PKG_VAR_ASSUMED_TRUE))) {
877 : : /*
878 : : * We are interested merely in dependencies of top variables
879 : : * or of previously assumed dependencies
880 : : */
881 : 50 : dbg(4, "not interested in dependencies for %s-%s",
882 : : var->unit->pkg->name, var->unit->pkg->version);
883 : 50 : return;
884 : : }
885 : : else {
886 : 69 : dbg(4, "examine dependencies for %s-%s",
887 : : var->unit->pkg->name, var->unit->pkg->version);
888 : : }
889 : :
890 : :
891 : 69 : item = rule->items->next;
892 [ + - ]: 69 : assert (item != NULL);
893 : 69 : var = item->var;
894 : 69 : first = var->unit;
895 : :
896 : : /* Rewind chains */
897 [ - + ]: 69 : while (first->prev->next != NULL) {
898 : 0 : first = first->prev;
899 : : }
900 [ - + ]: 69 : while (var->prev->next != NULL) {
901 : 0 : var = var->prev;
902 : : }
903 : :
904 [ + + ]: 134 : LL_FOREACH(var, cvar) {
905 [ + + ]: 84 : if (cvar->flags & PKG_VAR_ASSUMED) {
906 : : /* Do not reassume packages */
907 : 19 : return;
908 : : }
909 : 65 : }
910 : : /* Forward chain to find local package */
911 : 50 : local = NULL;
912 : :
913 [ + + ]: 81 : DL_FOREACH (first, cur) {
914 [ + + ]: 50 : if (cur->pkg->type == PKG_INSTALLED) {
915 : 19 : local = cur;
916 : 19 : break;
917 : : }
918 : 31 : }
919 : :
920 [ + + + + ]: 50 : if (prefer_local && local != NULL) {
921 : 1 : selected = local;
922 : 1 : }
923 : : else {
924 : 98 : selected = pkg_jobs_universe_select_candidate(first, local,
925 : 49 : conservative, assumed_reponame, true);
926 : :
927 [ + + + + : 49 : if (local && (STREQ(selected->pkg->digest, local->pkg->digest) ||
- + ]
928 : 2 : !pkg_jobs_need_upgrade(selected->pkg, local->pkg))) {
929 : 16 : selected = local;
930 : 16 : }
931 : : }
932 : :
933 : : /* Now we can find the according var */
934 [ - + ]: 50 : if (selected != NULL) {
935 : :
936 [ + + ]: 115 : LL_FOREACH(var, cvar) {
937 [ + + ]: 65 : if (cvar->unit == selected) {
938 : 50 : picosat_set_default_phase_lit(problem->sat, cvar->order, 1);
939 : 50 : dbg(4, "assumed %s-%s(%s) to be installed",
940 : : selected->pkg->name, selected->pkg->version,
941 : : selected->pkg->type == PKG_INSTALLED ? "l" : "r");
942 : 50 : cvar->flags |= PKG_VAR_ASSUMED_TRUE;
943 : 50 : }
944 : : else {
945 : 15 : dbg(4, "assumed %s-%s(%s) to be NOT installed",
946 : : cvar->unit->pkg->name, cvar->unit->pkg->version,
947 : : cvar->unit->pkg->type == PKG_INSTALLED ? "l" : "r");
948 : 15 : picosat_set_default_phase_lit(problem->sat, cvar->order, -1);
949 : : }
950 : :
951 : 65 : cvar->flags |= PKG_VAR_ASSUMED;
952 : 65 : }
953 : :
954 : 50 : }
955 : 50 : break;
956 : : case PKG_RULE_REQUIRE:
957 : : /* XXX: deal with require rules somehow */
958 : 17 : break;
959 : : default:
960 : : /* No nothing */
961 : 177 : return;
962 : : }
963 : 313 : }
964 : :
965 : : int
966 : 176 : pkg_solve_sat_problem(struct pkg_solve_problem *problem)
967 : : {
968 : : struct pkg_solve_rule *rule;
969 : : struct pkg_solve_item *item;
970 : 176 : int res, iter = 0;
971 : : size_t i;
972 : 176 : bool need_reiterate = false;
973 : 176 : const int *failed = NULL;
974 : 176 : int attempt = 0;
975 : : struct pkg_solve_variable *var;
976 : :
977 [ + + + + : 489 : tll_foreach(problem->rules, it) {
+ + ]
978 : 313 : rule = it->item;
979 : :
980 [ + + ]: 992 : LL_FOREACH(rule->items, item) {
981 : 679 : picosat_add(problem->sat, item->var->order * item->inverse);
982 : 679 : }
983 : :
984 : 313 : picosat_add(problem->sat, 0);
985 : 313 : pkg_debug_print_rule(rule);
986 : 313 : }
987 : :
988 [ + + + + : 489 : tll_foreach(problem->rules, it) {
+ + ]
989 : 313 : rule = it->item;
990 : 313 : pkg_solve_set_initial_assumption(problem, rule);
991 : 489 : }
992 : :
993 : : reiterate:
994 : :
995 : 186 : res = pkg_solve_picosat_iter(problem, iter);
996 : :
997 [ + + ]: 186 : if (res != PICOSAT_SATISFIABLE) {
998 : : /*
999 : : * in case we cannot satisfy the problem it appears by
1000 : : * experience that the culprit seems to always be the latest of
1001 : : * listed in the failed assumptions.
1002 : : * So try to remove them for the given problem.
1003 : : * To avoid endless loop allow a maximum of 10 iterations no
1004 : : * more
1005 : : */
1006 : 2 : failed = picosat_failed_assumptions(problem->sat);
1007 : 2 : attempt++;
1008 : :
1009 : : /* get the last failure */
1010 [ + + ]: 6 : while (*failed) {
1011 : 4 : failed++;
1012 : : }
1013 : 2 : failed--;
1014 : :
1015 [ - + ]: 2 : if (attempt >= 10) {
1016 : 0 : pkg_emit_error("Cannot solve problem using SAT solver");
1017 : 0 : xstring *sb = xstring_new();
1018 : :
1019 [ # # ]: 0 : while (*failed) {
1020 : 0 : var = &problem->variables[abs(*failed) - 1];
1021 [ # # # # : 0 : tll_foreach(problem->rules, it) {
# # ]
1022 : 0 : rule = it->item;
1023 : :
1024 [ # # ]: 0 : if (rule->reason != PKG_RULE_DEPEND) {
1025 [ # # ]: 0 : LL_FOREACH(rule->items, item) {
1026 [ # # ]: 0 : if (item->var == var) {
1027 : 0 : pkg_print_rule_buf(rule, sb);
1028 : 0 : fputc('\n', sb->fp);
1029 : 0 : break;
1030 : : }
1031 : 0 : }
1032 : 0 : }
1033 : 0 : }
1034 : :
1035 : 0 : fprintf(sb->fp, "cannot %s package %s, remove it from request? ",
1036 : 0 : var->flags & PKG_VAR_INSTALL ? "install" : "remove", var->uid);
1037 : :
1038 : 0 : fflush(sb->fp);
1039 [ # # ]: 0 : if (pkg_emit_query_yesno(true, sb->buf)) {
1040 : 0 : var->flags |= PKG_VAR_FAILED;
1041 : 0 : }
1042 : :
1043 : 0 : failed++;
1044 : 0 : need_reiterate = true;
1045 : : }
1046 : 0 : xstring_free(sb);
1047 : 0 : } else {
1048 : 2 : pkg_emit_notice("Cannot solve problem using SAT solver, trying another plan");
1049 : 2 : var = &problem->variables[abs(*failed) - 1];
1050 : :
1051 : 2 : var->flags |= PKG_VAR_FAILED;
1052 : :
1053 : 2 : need_reiterate = true;
1054 : : }
1055 : :
1056 : : #if 0
1057 : : failed = picosat_next_maximal_satisfiable_subset_of_assumptions(problem->sat);
1058 : :
1059 : : while (*failed) {
1060 : : struct pkg_solve_variable *var = &problem->variables[*failed - 1];
1061 : :
1062 : : pkg_emit_notice("var: %s", var->uid);
1063 : :
1064 : : failed ++;
1065 : : }
1066 : :
1067 : : return (EPKG_AGAIN);
1068 : : #endif
1069 : 2 : }
1070 : : else {
1071 : :
1072 : : /* Assign vars */
1073 [ + + ]: 607 : for (i = 0; i < problem->nvars; i ++) {
1074 : 423 : int val = picosat_deref(problem->sat, i + 1);
1075 : 423 : struct pkg_solve_variable *var = &problem->variables[i];
1076 : :
1077 [ + + ]: 423 : if (val > 0)
1078 : 245 : var->flags |= PKG_VAR_INSTALL;
1079 : : else
1080 : 178 : var->flags &= ~PKG_VAR_INSTALL;
1081 : :
1082 : 423 : dbg(2, "decided %s %s-%s to %s",
1083 : : var->unit->pkg->type == PKG_INSTALLED ? "local" : "remote",
1084 : : var->uid, var->digest,
1085 : : var->flags & PKG_VAR_INSTALL ? "install" : "delete");
1086 : 423 : }
1087 : :
1088 : : /* Check for reiterations */
1089 [ + + + + ]: 235 : if ((problem->j->type == PKG_JOBS_INSTALL ||
1090 [ + + ]: 184 : problem->j->type == PKG_JOBS_UPGRADE) && iter == 0) {
1091 [ + + ]: 474 : for (i = 0; i < problem->nvars; i ++) {
1092 : 334 : bool failed_var = false;
1093 : 334 : struct pkg_solve_variable *var = &problem->variables[i], *cur;
1094 : :
1095 [ + + ]: 334 : if (!(var->flags & PKG_VAR_INSTALL)) {
1096 [ + + ]: 241 : LL_FOREACH(var, cur) {
1097 [ + + ]: 194 : if (cur->flags & PKG_VAR_INSTALL) {
1098 : 72 : failed_var = false;
1099 : 72 : break;
1100 : : }
1101 [ + + ]: 122 : else if (cur->unit->pkg->type == PKG_INSTALLED) {
1102 : 83 : failed_var = true;
1103 : 83 : }
1104 : 122 : }
1105 : 119 : }
1106 : :
1107 : : /*
1108 : : * If we want to delete local packages on installation, do one more SAT
1109 : : * iteration to ensure that we have no other choices
1110 : : */
1111 [ + + ]: 334 : if (failed_var) {
1112 : 12 : dbg (1, "trying to delete local package %s-%s on install/upgrade,"
1113 : : " reiterate on SAT",
1114 : : var->unit->pkg->name, var->unit->pkg->version);
1115 : 12 : need_reiterate = true;
1116 : :
1117 [ + + ]: 26 : LL_FOREACH(var, cur) {
1118 : 14 : cur->flags |= PKG_VAR_FAILED;
1119 : 14 : }
1120 : 12 : }
1121 : 334 : }
1122 : 140 : }
1123 : : }
1124 : :
1125 [ + + ]: 186 : if (need_reiterate) {
1126 : 10 : iter ++;
1127 : :
1128 : : /* Restore top-level assumptions */
1129 [ + + ]: 65 : for (i = 0; i < problem->nvars; i ++) {
1130 : 55 : struct pkg_solve_variable *var = &problem->variables[i];
1131 : :
1132 [ + + + + ]: 55 : if (var->flags & PKG_VAR_TOP || var->unit->pkg->vital) {
1133 [ + + ]: 18 : if (var->flags & PKG_VAR_FAILED) {
1134 : 3 : var->flags ^= PKG_VAR_INSTALL | PKG_VAR_FAILED;
1135 : 3 : }
1136 : :
1137 : 36 : picosat_assume(problem->sat, var->order *
1138 : 18 : (var->flags & PKG_VAR_INSTALL ? 1 : -1));
1139 : 18 : }
1140 : 55 : }
1141 : :
1142 : 10 : need_reiterate = false;
1143 : :
1144 : 10 : goto reiterate;
1145 : : }
1146 : :
1147 : 176 : return (EPKG_OK);
1148 : : }
1149 : :
1150 : : void
1151 : 0 : pkg_solve_dot_export(struct pkg_solve_problem *problem, FILE *file)
1152 : : {
1153 : : struct pkg_solve_rule *rule;
1154 : : size_t i;
1155 : :
1156 : 0 : fprintf(file, "digraph {\n");
1157 : :
1158 [ # # ]: 0 : for (i = 0; i < problem->nvars; i ++) {
1159 : 0 : struct pkg_solve_variable *var = &problem->variables[i];
1160 : :
1161 : 0 : fprintf(file, "\tp%d [shape=%s label=\"%s-%s\"]\n", var->order,
1162 : 0 : var->unit->pkg->type == PKG_INSTALLED ? "ellipse" : "octagon",
1163 : 0 : var->uid, var->unit->pkg->version);
1164 : 0 : }
1165 : :
1166 : : /* Print all variables as nodes */
1167 : :
1168 [ # # # # : 0 : tll_foreach(problem->rules, rit) {
# # ]
1169 : 0 : rule = rit->item;
1170 : 0 : struct pkg_solve_item *it = rule->items, *key_elt = NULL;
1171 : :
1172 [ # # # # : 0 : switch(rule->reason) {
# # ]
1173 : : case PKG_RULE_DEPEND:
1174 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1175 [ # # ]: 0 : if (it->inverse == -1) {
1176 : 0 : key_elt = it;
1177 : 0 : break;
1178 : : }
1179 : 0 : }
1180 [ # # ]: 0 : assert (key_elt != NULL);
1181 : :
1182 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1183 [ # # ]: 0 : if (it != key_elt) {
1184 : 0 : fprintf(file, "\tp%d -> p%d;\n", key_elt->var->order,
1185 : 0 : it->var->order);
1186 : 0 : }
1187 : 0 : }
1188 : 0 : break;
1189 : : case PKG_RULE_UPGRADE_CONFLICT:
1190 : : case PKG_RULE_EXPLICIT_CONFLICT:
1191 : : case PKG_RULE_REQUEST_CONFLICT:
1192 : 0 : fprintf(file, "\tp%d -> p%d [arrowhead=none,color=red];\n",
1193 : 0 : it->var->order, it->next->var->order);
1194 : 0 : break;
1195 : : case PKG_RULE_REQUIRE:
1196 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1197 [ # # ]: 0 : if (it->inverse == -1) {
1198 : 0 : key_elt = it;
1199 : 0 : break;
1200 : : }
1201 : 0 : }
1202 [ # # ]: 0 : assert (key_elt != NULL);
1203 : :
1204 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1205 [ # # ]: 0 : if (it != key_elt) {
1206 : 0 : fprintf(file, "\tp%d -> p%d[arrowhead=diamond];\n", key_elt->var->order,
1207 : 0 : it->var->order);
1208 : 0 : }
1209 : 0 : }
1210 : 0 : break;
1211 : : default:
1212 : 0 : break;
1213 : : }
1214 : 0 : }
1215 : :
1216 : 0 : fprintf(file, "}\n");
1217 : 0 : }
1218 : :
1219 : : int
1220 : 0 : pkg_solve_dimacs_export(struct pkg_solve_problem *problem, FILE *f)
1221 : : {
1222 : : struct pkg_solve_rule *rule;
1223 : : struct pkg_solve_item *it;
1224 : :
1225 : 0 : fprintf(f, "p cnf %d %zu\n", (int)problem->nvars, tll_length(problem->rules));
1226 : :
1227 [ # # # # : 0 : tll_foreach(problem->rules, rit) {
# # ]
1228 : 0 : rule = rit->item;
1229 [ # # ]: 0 : LL_FOREACH(rule->items, it) {
1230 : 0 : size_t order = it->var - problem->variables;
1231 [ # # ]: 0 : if (order < problem->nvars)
1232 : 0 : fprintf(f, "%ld ", (long)((order + 1) * it->inverse));
1233 : 0 : }
1234 : 0 : fprintf(f, "0\n");
1235 : 0 : }
1236 : 0 : return (EPKG_OK);
1237 : : }
1238 : :
1239 : : static void
1240 : 268 : pkg_solve_insert_res_job (struct pkg_solve_variable *var,
1241 : : struct pkg_solve_problem *problem)
1242 : : {
1243 : : struct pkg_solved *res;
1244 : 268 : struct pkg_solve_variable *cur_var, *del_var = NULL, *add_var = NULL;
1245 : 268 : int seen_add = 0, seen_del = 0;
1246 : 268 : struct pkg_jobs *j = problem->j;
1247 : :
1248 [ + + ]: 645 : LL_FOREACH(var, cur_var) {
1249 [ + + + + ]: 377 : if ((cur_var->flags & PKG_VAR_INSTALL) &&
1250 : 226 : cur_var->unit->pkg->type != PKG_INSTALLED) {
1251 : 209 : add_var = cur_var;
1252 : 209 : seen_add ++;
1253 : 209 : }
1254 [ + + ]: 168 : else if (!(cur_var->flags & PKG_VAR_INSTALL)
1255 [ + + ]: 168 : && cur_var->unit->pkg->type == PKG_INSTALLED) {
1256 : 116 : del_var = cur_var;
1257 : 116 : seen_del ++;
1258 : 116 : }
1259 : 377 : }
1260 : :
1261 [ - + ]: 268 : if (seen_add > 1) {
1262 : 0 : pkg_emit_error("internal solver error: more than two packages to install(%d) "
1263 : 0 : "from the same uid: %s", seen_add, var->uid);
1264 : 0 : return;
1265 : : }
1266 [ + + + + ]: 268 : else if (seen_add != 0 || seen_del != 0) {
1267 [ + + ]: 251 : if (seen_add > 0) {
1268 : 209 : res = xcalloc(1, sizeof(struct pkg_solved));
1269 : : /* Pure install */
1270 [ + + ]: 209 : if (seen_del == 0) {
1271 : 135 : res->items[0] = add_var->unit;
1272 : 135 : res->type = (j->type == PKG_JOBS_FETCH) ?
1273 : : PKG_SOLVED_FETCH : PKG_SOLVED_INSTALL;
1274 [ + + + + : 135 : tll_push_back(j->jobs, res);
+ - - + +
+ ]
1275 : 135 : dbg(3, "pkg_solve: schedule installation of %s %s",
1276 : : add_var->uid, add_var->digest);
1277 : 135 : }
1278 : : else {
1279 : : /* Upgrade */
1280 : 74 : res->items[0] = add_var->unit;
1281 : 74 : res->items[1] = del_var->unit;
1282 : 74 : res->type = PKG_SOLVED_UPGRADE;
1283 [ + + + + : 74 : tll_push_back(j->jobs, res);
+ - - + +
+ ]
1284 : 74 : dbg(3, "pkg_solve: schedule upgrade of %s from %s to %s",
1285 : : del_var->uid, del_var->digest, add_var->digest);
1286 : : }
1287 : 209 : }
1288 : :
1289 : : /*
1290 : : * For delete requests there could be multiple delete requests per UID,
1291 : : * so we need to re-process vars and add all delete jobs required.
1292 : : */
1293 [ + + ]: 609 : LL_FOREACH(var, cur_var) {
1294 [ + + + + ]: 358 : if (!(cur_var->flags & PKG_VAR_INSTALL) &&
1295 : 149 : cur_var->unit->pkg->type == PKG_INSTALLED) {
1296 : : /* Skip already added items */
1297 [ + + - + ]: 116 : if (seen_add > 0 && cur_var == del_var)
1298 : 74 : continue;
1299 : :
1300 : 42 : res = xcalloc(1, sizeof(struct pkg_solved));
1301 : 42 : res->items[0] = cur_var->unit;
1302 : 42 : res->type = PKG_SOLVED_DELETE;
1303 [ + + + + : 42 : tll_push_back(j->jobs, res);
+ - - + +
+ ]
1304 : 42 : dbg(3, "schedule deletion of %s %s",
1305 : : cur_var->uid, cur_var->digest);
1306 : 42 : }
1307 : 284 : }
1308 : 251 : }
1309 : : else {
1310 : 17 : dbg(2, "ignoring package %s(%s) as its state has not been changed",
1311 : : var->uid, var->digest);
1312 : : }
1313 : 268 : }
1314 : :
1315 : : int
1316 : 176 : pkg_solve_sat_to_jobs(struct pkg_solve_problem *problem)
1317 : : {
1318 : : struct pkg_solve_variable *var;
1319 : 176 : pkghash_it it = pkghash_iterator(problem->variables_by_uid);
1320 : :
1321 [ + + ]: 444 : while (pkghash_next(&it)) {
1322 : 268 : var = (struct pkg_solve_variable *)it.value;
1323 : 268 : dbg(4, "check variable with uid %s", var->uid);
1324 : 268 : pkg_solve_insert_res_job(var, problem);
1325 : : }
1326 : :
1327 : 176 : return (EPKG_OK);
1328 : : }
1329 : :
1330 : : static bool
1331 : 0 : pkg_solve_parse_sat_output_store(struct pkg_solve_problem *problem, const char *var_str)
1332 : : {
1333 : : struct pkg_solve_variable *var;
1334 : : ssize_t order;
1335 : :
1336 : 0 : order = strtol(var_str, NULL, 10);
1337 [ # # ]: 0 : if (order == 0)
1338 : 0 : return (true);
1339 [ # # ]: 0 : if (order < 0) {
1340 : : /* negative value means false */
1341 : 0 : order = - order - 1;
1342 [ # # ]: 0 : if ((size_t)order < problem->nvars) {
1343 : 0 : var = problem->variables + order;
1344 : 0 : var->flags &= ~PKG_VAR_INSTALL;
1345 : 0 : }
1346 : 0 : } else {
1347 : : /* positive value means true */
1348 : 0 : order = order - 1;
1349 [ # # ]: 0 : if ((size_t)order < problem->nvars) {
1350 : 0 : var = problem->variables + order;
1351 : 0 : var->flags |= PKG_VAR_INSTALL;
1352 : 0 : }
1353 : : }
1354 : 0 : return (false);
1355 : 0 : }
1356 : :
1357 : : int
1358 : 0 : pkg_solve_parse_sat_output(FILE *f, struct pkg_solve_problem *problem)
1359 : : {
1360 : 0 : int ret = EPKG_OK;
1361 : 0 : char *line = NULL, *var_str, *begin;
1362 : 0 : size_t linecap = 0;
1363 : 0 : bool got_sat = false, done = false;
1364 : :
1365 [ # # ]: 0 : while (getline(&line, &linecap, f) > 0) {
1366 [ # # ]: 0 : if (strncmp(line, "SAT", 3) == 0) {
1367 : 0 : got_sat = true;
1368 : 0 : }
1369 [ # # ]: 0 : else if (got_sat) {
1370 : 0 : begin = line;
1371 : 0 : do {
1372 : 0 : var_str = strsep(&begin, " \t");
1373 : : /* Skip unexpected lines */
1374 [ # # # # : 0 : if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
# # ]
1375 : 0 : continue;
1376 [ # # ]: 0 : if (pkg_solve_parse_sat_output_store(problem, var_str))
1377 : 0 : done = true;
1378 [ # # ]: 0 : } while (begin != NULL);
1379 : 0 : }
1380 [ # # ]: 0 : else if (strncmp(line, "v ", 2) == 0) {
1381 : 0 : begin = line + 2;
1382 : 0 : do {
1383 : 0 : var_str = strsep(&begin, " \t");
1384 : : /* Skip unexpected lines */
1385 [ # # # # : 0 : if (var_str == NULL || (!isdigit(*var_str) && *var_str != '-'))
# # ]
1386 : 0 : continue;
1387 [ # # ]: 0 : if (pkg_solve_parse_sat_output_store(problem, var_str))
1388 : 0 : done = true;
1389 [ # # ]: 0 : } while (begin != NULL);
1390 : 0 : }
1391 : : else {
1392 : : /* Slightly ignore anything from solver */
1393 : 0 : continue;
1394 : : }
1395 : : }
1396 : :
1397 [ # # ]: 0 : if (done)
1398 : 0 : ret = pkg_solve_sat_to_jobs(problem);
1399 : : else {
1400 : 0 : pkg_emit_error("cannot parse sat solver output");
1401 : 0 : ret = EPKG_FATAL;
1402 : : }
1403 : :
1404 : 0 : free(line);
1405 : :
1406 : 0 : return (ret);
1407 : : }
|
