From patchwork Fri Sep 20 08:56:21 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Ole Schuerks X-Patchwork-Id: 13808361 Received: from mail-ej1-f46.google.com (mail-ej1-f46.google.com [209.85.218.46]) (using TLSv1.2 with cipher ECDHE-RSA-AES128-GCM-SHA256 (128/128 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 08FF113BC26; Fri, 20 Sep 2024 08:56:53 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; arc=none smtp.client-ip=209.85.218.46 ARC-Seal: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1726822617; cv=none; b=gvCAnMegDpkKljGUcmJZmEPUX8al+Hxb490l9mnimW6UdENCjREzasbqQFe9X5rF/DefMv/cGJPlJNf3GxiZBdjzkptWm48NXK8GxkvN/C2zrm70lyeGS2InjjsY2EDP8dTu5lOX1x70ppbLrSABjPV0gDKX0x+LGYsmC6UcREM= ARC-Message-Signature: i=1; a=rsa-sha256; d=subspace.kernel.org; s=arc-20240116; t=1726822617; c=relaxed/simple; bh=DppSDWkTADuYC8A8QtyR0WLPME8rqZb2I8wilkJ7OBs=; h=From:To:Cc:Subject:Date:Message-Id:In-Reply-To:References: MIME-Version; b=uJZMl3epINLxuKwsqSeYFCybRi6MjR9n5/PsHwHE52OIDRk9ySX2qR1J8Hw9yeMDdOGyWnSy6tvXZk1yTIzF/NhdWTYZ2YlxKORxrcv7B1ot/zIgfEKtV/VbgCiRVbzNYkOWvN46ES0N1SwECwlbno78M0PAMNiVyU0ceU/ASQc= ARC-Authentication-Results: i=1; smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com; spf=pass smtp.mailfrom=gmail.com; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b=dkgp0udP; arc=none smtp.client-ip=209.85.218.46 Authentication-Results: smtp.subspace.kernel.org; dmarc=pass (p=none dis=none) header.from=gmail.com Authentication-Results: smtp.subspace.kernel.org; spf=pass smtp.mailfrom=gmail.com Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="dkgp0udP" Received: by mail-ej1-f46.google.com with SMTP id a640c23a62f3a-a7aa086b077so238431166b.0; Fri, 20 Sep 2024 01:56:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1726822612; x=1727427412; darn=vger.kernel.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=w30kYie/I7kDYlUhxrK0Y05nk4BLpcF3m1+t/JjpMkA=; b=dkgp0udPUkjjW62WGaGC4uTWA+06ik8v+ZFMXdqYW41Z4/FqfWCnXMT/RaLaQTcqU6 xW0YhzR/4dfXe0NWVg42+qOBaKFnrQKc7Asf9+z1BSl+/PzPskfOC3NE2U8P9hT68RzR wDXFc/pucuFApO8uO2od2NHwwLV0MqeSNORZZ4qbMQjxg8bsa8V41kOCGFaecVb6cBLY KAzqN9DYf8s9WNIoCjCMGWl5JI9xaP/Jk4+1jEK8ss76xgBhr9RDVmuBXE9Gz7bmtXEB z5J299IPqQ8qsBePBdZ5JKS8aS14yjDPKP+p3U0UEZUyzMxLPwkwuP9BLAHGtDOR44F/ XGzA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1726822612; x=1727427412; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=w30kYie/I7kDYlUhxrK0Y05nk4BLpcF3m1+t/JjpMkA=; b=IcZAt3+aaRrkYid7NmrXlXGmUi06GiNvSX4vFuwaWEDx7aw+1HfA+qq+nloIQEMXzA r7/Fmzf2jAuJQLIOYH8zljhcLjzWgXHQjU1Eq0RHYH0XjRlETiIvAESW8jt6w63EYzyn 493U3K6NdHYqFv79UgeN4BY2FmQJfVfaiTla5RkJBGitseI4MgKez0aC9t963XiAzrij ax51yMRzD2T8YS6Fm7nZ0o8biUC9ytZZiO9QpFZEBXWzHdIekQMbHHwDPC1O8gZi3/Ya ypF5tf9Be0PajQTUu/sYVVRx8O06a1teOaH2pWR+fl53foBWnQ8ZpupZ+OwJhO7g5D1V jErQ== X-Forwarded-Encrypted: i=1; AJvYcCWpd+OqtC4DMLVIMK83pJIg8ksYCfQ9DyiTLfDs9LA7Yr/+7KcO049BD2d14+NLCyE4ssXRlgEmhd/kV8w=@vger.kernel.org X-Gm-Message-State: AOJu0Yw4v1w2upKw5BAWhGZpkej7WjSAUbp9VCq8KQh0R3rMQWh3Oz6I kRD8SUpybjsUdziWQ2BePDQ0IctyF/ctmcWIwbtCyaB75t9h5LMFTaDK6A== X-Google-Smtp-Source: AGHT+IG8tsvImSBOB1odJz/JAl7iElepOJ9K8zviMRM79l8m4CTgk7HhFZCN7FwYhsVQbXWZkofSmw== X-Received: by 2002:a17:907:3daa:b0:a86:7924:11bd with SMTP id a640c23a62f3a-a90d512700dmr195794466b.41.1726822611810; Fri, 20 Sep 2024 01:56:51 -0700 (PDT) Received: from localhost.localdomain ([2a02:908:e842:bf20:422c:48db:9094:2fa9]) by smtp.gmail.com with ESMTPSA id a640c23a62f3a-a906109637esm817861866b.40.2024.09.20.01.56.50 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 20 Sep 2024 01:56:51 -0700 (PDT) From: Ole Schuerks To: linux-kbuild@vger.kernel.org Cc: ole0811sch@gmail.com, jude.gyimah@rub.de, thorsten.berger@rub.de, deltaone@debian.org, jan.sollmann@rub.de, mcgrof@kernel.org, masahiroy@kernel.org, linux-kernel@vger.kernel.org, nathan@kernel.org, nicolas@fjasle.eu Subject: [PATCH v5 04/11] kconfig: Add files for building constraints Date: Fri, 20 Sep 2024 10:56:21 +0200 Message-Id: <20240920085628.51863-5-ole0811sch@gmail.com> X-Mailer: git-send-email 2.39.2 In-Reply-To: <20240920085628.51863-1-ole0811sch@gmail.com> References: <20240920085628.51863-1-ole0811sch@gmail.com> Precedence: bulk X-Mailing-List: linux-kbuild@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 These files translate the Kconfig-model into propositional logic and store the constraints for each symbol in the corresponding struct. Co-developed-by: Patrick Franz Signed-off-by: Patrick Franz Co-developed-by: Ibrahim Fayaz Signed-off-by: Ibrahim Fayaz Reviewed-by: Luis Chamberlain Tested-by: Evgeny Groshev Suggested-by: Sarah Nadi Suggested-by: Thorsten Berger Signed-off-by: Thorsten Berger Signed-off-by: Ole Schuerks --- scripts/kconfig/cf_constraints.c | 1789 ++++++++++++++++++++++++++++++ scripts/kconfig/cf_constraints.h | 24 + 2 files changed, 1813 insertions(+) create mode 100644 scripts/kconfig/cf_constraints.c create mode 100644 scripts/kconfig/cf_constraints.h diff --git a/scripts/kconfig/cf_constraints.c b/scripts/kconfig/cf_constraints.c new file mode 100644 index 000000000000..b84280ea5309 --- /dev/null +++ b/scripts/kconfig/cf_constraints.c @@ -0,0 +1,1789 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * Copyright (C) 2023 Patrick Franz + */ + +#include "cf_defs.h" +#include "expr.h" +#include "list.h" +#define _GNU_SOURCE +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "cf_utils.h" +#include "internal.h" +#include "cf_expr.h" +#include "cf_constraints.h" + +#define KCR_CMP false +#define NPC_OPTIMISATION true + +static void find_nonboolean_known_vals(struct cfdata *data); +static void build_constraints_bool(struct cfdata *data); +static void build_constraints_select(struct cfdata *data); +static void build_constraints_nonbool(struct cfdata *data); + +static void build_tristate_constraint_clause(struct symbol *sym, + struct cfdata *data); + +static void add_selects_kcr(struct symbol *sym, struct cfdata *data); +static void add_selects(struct symbol *sym, struct cfdata *data); + +static void add_dependencies_bool(struct symbol *sym, struct cfdata *data); +static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data); +static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data); + +static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data); +static void add_choice_dependencies(struct symbol *sym, struct cfdata *data); +static void add_choice_constraints(struct symbol *sym, struct cfdata *data); +static void add_invisible_constraints(struct symbol *sym, struct cfdata *data); +static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data); +static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data); +static void sym_add_nonbool_values_from_default_range(struct symbol *sym, + struct cfdata *data); +static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data); +static void sym_add_nonbool_prompt_constraint(struct symbol *sym, + struct cfdata *data); + +static struct default_map *create_default_map_entry(struct fexpr *val, + struct pexpr *e); +static struct defm_list *calc_default_conditions(struct symbol *sym, struct cfdata *data); +static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data); +static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data); +static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data); +static long sym_get_range_val(struct symbol *sym, int base); + +/* -------------------------------------- */ + +/* + * build the constraints for each symbol + */ +void build_constraints(struct cfdata *data) +{ + printd("Building constraints..."); + + find_nonboolean_known_vals(data); + build_constraints_bool(data); + build_constraints_select(data); + build_constraints_nonbool(data); +} + +/* + * need to go through the constraints once to find all "known values" + * for the non-Boolean symbols (and add them to sym->nb_vals for the given + * symbols). + * expr_calculate_pexpr_both and get_defaults have the side effect of creating + * known values. + */ +static void find_nonboolean_known_vals(struct cfdata *data) +{ + struct symbol *sym; + struct property *p; + + for_all_symbols(sym) { + struct property *prompt; + + if (sym->type == S_UNKNOWN) + continue; + + if (sym_is_boolean(sym)) { + for_all_properties(sym, p, P_SELECT) + pexpr_put(expr_calculate_pexpr_both( + p->visible.expr, data)); + + for_all_properties(sym, p, P_IMPLY) + pexpr_put(expr_calculate_pexpr_both( + p->visible.expr, data)); + } + + if (sym->dir_dep.expr) + pexpr_put(expr_calculate_pexpr_both(sym->dir_dep.expr, + data)); + + prompt = sym_get_prompt(sym); + if (prompt != NULL && prompt->visible.expr) { + pexpr_put(expr_calculate_pexpr_both( + prompt->visible.expr, data)); + defm_list_destruct(calc_default_conditions(sym, data)); + } + + if (sym_is_nonboolean(sym)) { + const char *curr; + + for_all_defaults(sym, p) { + if (p == NULL) + continue; + + sym_create_nonbool_fexpr( + sym, p->expr->left.sym->name, data); + } + for_all_properties(sym, p, P_RANGE) { + if (p == NULL) + continue; + + sym_create_nonbool_fexpr( + sym, p->expr->left.sym->name, data); + sym_create_nonbool_fexpr( + sym, p->expr->right.sym->name, data); + } + curr = sym_get_string_value(sym); + if (strcmp(curr, "") != 0) + sym_create_nonbool_fexpr(sym, (char *)curr, + data); + } + + if (sym->type == S_HEX || sym->type == S_INT) + sym_add_nonbool_values_from_default_range(sym, data); + } +} + +/* + * build constraints for boolean symbols + */ +static void build_constraints_bool(struct cfdata *data) +{ + struct symbol *sym; + + for_all_symbols(sym) { + if (!sym_is_boolean(sym)) + continue; + + /* build tristate constraints */ + if (sym->type == S_TRISTATE) + build_tristate_constraint_clause(sym, data); + + /* build constraints for select statements + * need to treat choice symbols separately + */ + if (!KCR_CMP) { + add_selects(sym, data); + } else { + if (sym->rev_dep.expr && !sym_is_choice(sym) && + !sym_is_choice_value(sym)) + add_selects_kcr(sym, data); + } + + /* build constraints for dependencies for booleans */ + if (sym->dir_dep.expr && !sym_is_choice(sym) && + !sym_is_choice_value(sym)) { + if (!KCR_CMP) + add_dependencies_bool(sym, data); + else + add_dependencies_bool_kcr(sym, data); + } + + /* build constraints for choice prompts */ + if (sym_is_choice(sym)) + add_choice_prompt_cond(sym, data); + + /* + * build constraints for dependencies (choice symbols and + * options) + */ + if (sym_is_choice(sym) || sym_is_choice_value(sym)) + add_choice_dependencies(sym, data); + + /* build constraints for the choice groups */ + if (sym_is_choice(sym)) + add_choice_constraints(sym, data); + + /* build invisible constraints */ + add_invisible_constraints(sym, data); + } +} + +/* + * build the constraints for select-variables + * skip non-Booleans, choice symbols/options och symbols without rev_dir + */ +static void build_constraints_select(struct cfdata *data) +{ + struct symbol *sym; + + for_all_symbols(sym) { + struct pexpr *sel_y, *sel_m; + struct pexpr *c1, *c2; + + if (KCR_CMP) + continue; + + if (!sym_is_boolean(sym)) + continue; + + if (sym_is_choice(sym) || sym_is_choice_value(sym)) + continue; + + if (!sym->rev_dep.expr) + continue; + + if (sym->list_sel_y == NULL) + continue; + + sel_y = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_sel_y), + pexpr_alloc_symbol(sym->fexpr_y), data, + PEXPR_ARGX); + sym_add_constraint(sym, sel_y, data); + + c1 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_sel_y), + sym->list_sel_y, data, PEXPR_ARG1); + sym_add_constraint(sym, c1, data); + + /* only continue for tristates */ + if (sym->type == S_BOOLEAN) + continue; + + sel_m = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_sel_m), + sym_get_fexpr_both(sym, data), data, + PEXPR_ARGX); + sym_add_constraint(sym, sel_m, data); + + c2 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_sel_m), + sym->list_sel_m, data, PEXPR_ARG1); + sym_add_constraint(sym, c2, data); + PEXPR_PUT(sel_y, sel_m, c1, c2); + } +} + +/* + * build constraints for non-booleans + */ +static void build_constraints_nonbool(struct cfdata *data) +{ + struct symbol *sym; + + for_all_symbols(sym) { + if (!sym_is_nonboolean(sym)) + continue; + + /* the symbol must have a value, if there is a prompt */ + if (sym_has_prompt(sym)) + sym_add_nonbool_prompt_constraint(sym, data); + + /* build the range constraints for int/hex */ + if (sym->type == S_HEX || sym->type == S_INT) + sym_add_range_constraints(sym, data); + + /* build constraints for dependencies for non-booleans */ + if (sym->dir_dep.expr) + add_dependencies_nonbool(sym, data); + + /* build invisible constraints */ + add_invisible_constraints(sym, data); + + /* exactly one of the symbols must be true */ + sym_nonbool_at_least_1(sym, data); + sym_nonbool_at_most_1(sym, data); + } +} + +/* + * enforce tristate constraints + */ +static void build_tristate_constraint_clause(struct symbol *sym, + struct cfdata *data) +{ + struct pexpr *X, *X_m, *modules, *c; + + if (sym->type != S_TRISTATE) + return; + + X = pexpr_alloc_symbol(sym->fexpr_y); + X_m = pexpr_alloc_symbol(sym->fexpr_m); + modules = pexpr_alloc_symbol(modules_sym->fexpr_y); + + /* -X v -X_m */ + c = pexpr_or(pexpr_not_share(X, data), pexpr_not_share(X_m, data), + data, PEXPR_ARGX); + sym_add_constraint(sym, c, data); + + /* X_m -> MODULES */ + if (modules_sym->fexpr_y != NULL) { + struct pexpr *c2 = pexpr_implies_share(X_m, modules, data); + + sym_add_constraint(sym, c2, data); + PEXPR_PUT(c2); + } + PEXPR_PUT(X, X_m, modules, c); +} + +/* + * build the select constraints + * - RDep(X) implies X + */ +static void add_selects_kcr(struct symbol *sym, struct cfdata *data) +{ + struct pexpr *rdep_y = expr_calculate_pexpr_y(sym->rev_dep.expr, data); + struct pexpr *c1 = pexpr_implies( + rdep_y, pexpr_alloc_symbol(sym->fexpr_y), data, PEXPR_ARG2); + + struct pexpr *rdep_both = + expr_calculate_pexpr_both(sym->rev_dep.expr, data); + struct pexpr *c2 = pexpr_implies( + rdep_both, sym_get_fexpr_both(sym, data), data, PEXPR_ARG2); + + sym_add_constraint(sym, c1, data); + sym_add_constraint(sym, c2, data); + PEXPR_PUT(rdep_y, c1, rdep_both, c2); +} + +/* + * build the select constraints simplified + * - RDep(X) implies X + */ +static void add_selects(struct symbol *sym, struct cfdata *data) +{ + struct property *p; + + if (!sym_is_boolean(sym)) + return; + + for_all_properties(sym, p, P_SELECT) { + struct symbol *selected = p->expr->left.sym; + struct pexpr *cond_y, *cond_both; + + if (selected->type == S_UNKNOWN) + continue; + + if (!selected->rev_dep.expr) + continue; + + if (p->visible.expr) { + cond_y = expr_calculate_pexpr_y(p->visible.expr, data); + cond_both = expr_calculate_pexpr_both(p->visible.expr, + data); + } else { + cond_y = + pexpr_alloc_symbol(data->constants->const_true); + cond_both = + pexpr_alloc_symbol(data->constants->const_true); + } + + if (selected->type == S_BOOLEAN) { + /* imply that symbol is selected to y */ + struct pexpr *e1 = pexpr_and( + cond_both, sym_get_fexpr_both(sym, data), data, + PEXPR_ARG2); + struct pexpr *c1 = pexpr_implies( + e1, pexpr_alloc_symbol(selected->fexpr_sel_y), + data, PEXPR_ARG2); + + sym_add_constraint(selected, c1, data); + + if (selected->list_sel_y == NULL) + selected->list_sel_y = pexpr_get(e1); + else + selected->list_sel_y = + pexpr_or(selected->list_sel_y, e1, data, + PEXPR_ARG1); + PEXPR_PUT(e1, c1); + } + + if (selected->type == S_TRISTATE) { + struct pexpr *e2, *e3, *c2, *c3; + + /* imply that symbol is selected to y */ + e2 = pexpr_and(cond_y, pexpr_alloc_symbol(sym->fexpr_y), + data, PEXPR_ARG2); + c2 = pexpr_implies( + e2, pexpr_alloc_symbol(selected->fexpr_sel_y), + data, PEXPR_ARG2); + sym_add_constraint(selected, c2, data); + + if (selected->list_sel_y == NULL) + selected->list_sel_y = pexpr_get(e2); + else + selected->list_sel_y = + pexpr_or(selected->list_sel_y, e2, + data, PEXPR_ARG1); + + /* imply that symbol is selected to m */ + e3 = pexpr_and(cond_both, sym_get_fexpr_both(sym, data), + data, PEXPR_ARG2); + c3 = pexpr_implies( + e3, pexpr_alloc_symbol(selected->fexpr_sel_m), + data, PEXPR_ARG2); + sym_add_constraint(selected, c3, data); + + if (selected->list_sel_m == NULL) + selected->list_sel_m = pexpr_get(e3); + else + selected->list_sel_m = + pexpr_or(selected->list_sel_m, e3, + data, PEXPR_ARG1); + PEXPR_PUT(e2, c2, e3, c3); + } + PEXPR_PUT(cond_y, cond_both); + } +} + +/* + * build the dependency constraints for booleans + * - X implies Dep(X) or RDep(X) + */ +static void add_dependencies_bool(struct symbol *sym, struct cfdata *data) +{ + struct pexpr *dep_both; + struct pexpr *visible_m; + struct pexpr *visible_y; + struct pexpr *visible_both; + struct property *prompt; + struct pexpr *has_prompt; + struct pexpr *sel_y; + + if (!sym_is_boolean(sym) || !sym->dir_dep.expr) + return; + + prompt = sym_get_prompt(sym); + if (!prompt) { + visible_m = pexpr_alloc_symbol(data->constants->const_false); + visible_y = pexpr_get(visible_m); + visible_both = pexpr_get(visible_m); + } else if (prompt->expr == NULL) { + visible_m = pexpr_alloc_symbol(data->constants->const_true); + visible_y = pexpr_get(visible_m); + visible_both = pexpr_get(visible_m); + } else { + visible_m = expr_calculate_pexpr_m(prompt->expr, data); + visible_y = expr_calculate_pexpr_y(prompt->expr, data); + visible_both = pexpr_or_share(visible_y, visible_m, data); + } + + dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data); + + sel_y = sym->rev_dep.expr ? + pexpr_alloc_symbol(sym->fexpr_sel_y) : + pexpr_alloc_symbol(data->constants->const_false); + has_prompt = pexpr_get(visible_both); + has_prompt = pexpr_and( + has_prompt, + pexpr_not(pexpr_and_share(sel_y, visible_m, data), + data), + data, PEXPR_ARGX); + + if (sym->type == S_TRISTATE) { + struct pexpr *c1; + struct pexpr *c2; + struct pexpr *dep_y = + expr_calculate_pexpr_y(sym->dir_dep.expr, data); + struct pexpr *sel_both = sym_get_fexpr_sel_both(sym, data); + struct pexpr *cond_y1; + struct pexpr *cond_y2; + struct pexpr *cond_y; + struct pexpr *cond_m1; + struct pexpr *cond_m2; + struct pexpr *cond_m; + + cond_y1 = pexpr_implies(pexpr_not_share(has_prompt, data), + pexpr_or_share(dep_y, sel_y, data), + data, PEXPR_ARGX); + cond_y2 = pexpr_implies_share(has_prompt, visible_y, data); + cond_y = pexpr_and_share(cond_y1, cond_y2, data); + cond_m1 = + pexpr_implies(pexpr_not_share(has_prompt, data), + pexpr_or_share(dep_both, sel_both, data), + data, PEXPR_ARGX); + cond_m2 = pexpr_implies(has_prompt, + pexpr_not_share(sel_y, data), data, + PEXPR_ARG2); + cond_m = pexpr_and_share(cond_m1, cond_m2, data); + c1 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), cond_y, + data, PEXPR_ARG1); + c2 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_m), cond_m, + data, PEXPR_ARG1); + + sym_add_constraint(sym, c1, data); + sym_add_constraint(sym, c2, data); + PEXPR_PUT(c1, c2, dep_y, sel_both, cond_y1, + cond_y2, cond_y, cond_m1, cond_m2, cond_m); + } else if (sym->type == S_BOOLEAN) { + struct pexpr *cond1; + struct pexpr *cond2; + struct pexpr *c; + + cond1 = pexpr_implies(pexpr_not_share(has_prompt, data), + pexpr_or(dep_both, + pexpr_alloc_symbol(sym->fexpr_m), + data, PEXPR_ARG2), + data, PEXPR_ARGX); + cond2 = pexpr_implies_share(has_prompt, visible_y, data); + c = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), + pexpr_and_share(cond1, cond2, data), data, + PEXPR_ARGX); + + sym_add_constraint(sym, c, data); + PEXPR_PUT(c, cond1, cond2); + } + PEXPR_PUT(dep_both, has_prompt, sel_y, visible_y, visible_m, + visible_both); +} + +/* + * build the dependency constraints for booleans (KCR) + * - X implies Dep(X) or RDep(X) + */ +static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data) +{ + struct pexpr *dep_both, *sel_both; + + if (!sym_is_boolean(sym) || !sym->dir_dep.expr) + return; + + dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data); + + sel_both = sym->rev_dep.expr ? + expr_calculate_pexpr_both(sym->rev_dep.expr, data) : + pexpr_alloc_symbol(data->constants->const_false); + + if (sym->type == S_TRISTATE) { + struct pexpr *c1; + struct pexpr *c2; + { + struct pexpr *dep_y = + expr_calculate_pexpr_y(sym->dir_dep.expr, data); + struct pexpr *sel_y = + sym->rev_dep.expr ? + expr_calculate_pexpr_y( + sym->rev_dep.expr, data) : + pexpr_alloc_symbol( + data->constants->const_false); + c1 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), + pexpr_or(dep_y, sel_y, + data, PEXPR_ARGX), + data, PEXPR_ARGX); + } + c2 = pexpr_implies(pexpr_alloc_symbol(sym->fexpr_m), + pexpr_or_share(dep_both, sel_both, + data), + data, PEXPR_ARGX); + + sym_add_constraint(sym, c1, data); + sym_add_constraint(sym, c2, data); + PEXPR_PUT(c1, c2); + } else if (sym->type == S_BOOLEAN) { + struct pexpr *c = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_y), + pexpr_or_share(dep_both, sel_both, data), data, + PEXPR_ARGX); + + sym_add_constraint(sym, c, data); + PEXPR_PUT(c); + } + + PEXPR_PUT(dep_both, sel_both); +} + +/* + * build the dependency constraints for non-booleans + * + * sym is not 'n' implies `sym->dir_dep` + */ +static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data) +{ + struct pexpr *dep_both; + struct pexpr *nb_vals; // "sym is set to some value" / "sym is not 'n'" + struct fexpr_node *node; + struct pexpr *c; + bool first = true; + + if (!sym_is_nonboolean(sym) || !sym->dir_dep.expr || sym->rev_dep.expr) + return; + + dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data); + + nb_vals = pexpr_alloc_symbol(data->constants->const_false); + /* can skip the first non-boolean value, since this is 'n' */ + CF_LIST_FOR_EACH(node, sym->nb_vals, fexpr) { + if (first) { + first = false; + continue; + } + + nb_vals = pexpr_or(nb_vals, pexpr_alloc_symbol(node->elem), + data, PEXPR_ARGX); + } + + c = pexpr_implies(nb_vals, dep_both, data, PEXPR_ARGX); + sym_add_constraint(sym, c, data); + pexpr_put(c); +} + +/* + * build the constraints for the choice prompt + */ +static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data) +{ + struct property *prompt; + struct pexpr *promptCondition; + struct pexpr *fe_both; + struct pexpr *pr_cond; + struct pexpr *req_cond; + + if (!sym_is_boolean(sym)) + return; + + prompt = sym_get_prompt(sym); + if (prompt == NULL) + return; + + promptCondition = + prompt->visible.expr ? + expr_calculate_pexpr_both(prompt->visible.expr, data) : + pexpr_alloc_symbol(data->constants->const_true); + fe_both = sym_get_fexpr_both(sym, data); + req_cond = pexpr_implies_share(promptCondition, fe_both, data); + sym_add_constraint(sym, req_cond, data); + pr_cond = pexpr_implies_share(fe_both, promptCondition, data); + sym_add_constraint(sym, pr_cond, data); + PEXPR_PUT(promptCondition, fe_both, req_cond, pr_cond); +} + +/* + * build constraints for dependencies (choice symbols and options) + */ +static void add_choice_dependencies(struct symbol *sym, struct cfdata *data) +{ + struct property *prompt; + struct expr *to_parse; + struct pexpr *dep_both; + + if (!sym_is_choice(sym) || !sym_is_choice_value(sym)) + return; + + prompt = sym_get_prompt(sym); + if (prompt == NULL) + return; + + if (sym_is_choice(sym)) { + if (!prompt->visible.expr) + return; + to_parse = prompt->visible.expr; + } else { + if (!sym->dir_dep.expr) + return; + to_parse = sym->dir_dep.expr; + } + + dep_both = expr_calculate_pexpr_both(to_parse, data); + + if (sym->type == S_TRISTATE) { + struct pexpr *dep_y = expr_calculate_pexpr_y(to_parse, data); + struct pexpr *c1 = + pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), dep_y, + data, PEXPR_ARG1); + struct pexpr *c2 = + pexpr_implies(pexpr_alloc_symbol(sym->fexpr_m), + dep_both, data, PEXPR_ARG1); + + sym_add_constraint_unique(sym, c1, data); + sym_add_constraint_unique(sym, c2, data); + PEXPR_PUT(dep_y, c1, c2); + } else if (sym->type == S_BOOLEAN) { + struct pexpr *c = + pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), + dep_both, data, PEXPR_ARG1); + + sym_add_constraint_unique(sym, c, data); + pexpr_put(c); + } + pexpr_put(dep_both); +} + +/* + * build constraints for the choice groups + */ +static void add_choice_constraints(struct symbol *sym, struct cfdata *data) +{ + struct property *prompt; + struct symbol *choice, *choice2; + struct sym_node *node; + struct sym_list *items, *promptItems; + struct pexpr *c1; + struct menu *menu_ptr, *choiceval_menu; + + if (!sym_is_boolean(sym)) + return; + + prompt = sym_get_prompt(sym); + if (prompt == NULL) + return; + + /* create list of all choice options */ + items = CF_LIST_INIT(sym); + /* create list of choice options with a prompt */ + promptItems = CF_LIST_INIT(sym); + + for_all_choices(sym, choiceval_menu, menu_ptr) { + choice = choiceval_menu->sym; + + CF_PUSH_BACK(items, choice, sym); + if (sym_get_prompt(choice) != NULL) + CF_PUSH_BACK(promptItems, choice, sym); + } + + /* if the choice is set to yes, at least one child must be set to yes */ + c1 = NULL; + CF_LIST_FOR_EACH(node, promptItems, sym) { + choice = node->elem; + c1 = list_is_head(node->node.prev, &promptItems->list) ? + pexpr_alloc_symbol(choice->fexpr_y) : + pexpr_or(c1, pexpr_alloc_symbol(choice->fexpr_y), + data, PEXPR_ARGX); + } + if (c1 != NULL) { + struct pexpr *c2 = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_y), c1, data, PEXPR_ARG1); + + sym_add_constraint(sym, c2, data); + PEXPR_PUT(c1, c2); + } + + /* + * every choice option (even those without a prompt) implies the choice + */ + CF_LIST_FOR_EACH(node, items, sym) { + choice = node->elem; + c1 = pexpr_implies(sym_get_fexpr_both(choice, data), + sym_get_fexpr_both(sym, data), data, + PEXPR_ARGX); + sym_add_constraint(sym, c1, data); + pexpr_put(c1); + } + + /* choice options can only select mod, if the entire choice is mod */ + if (sym->type == S_TRISTATE) { + CF_LIST_FOR_EACH(node, items, sym) { + choice = node->elem; + if (choice->type == S_TRISTATE) { + c1 = pexpr_implies( + pexpr_alloc_symbol(choice->fexpr_m), + pexpr_alloc_symbol(sym->fexpr_m), data, + PEXPR_ARGX); + sym_add_constraint(sym, c1, data); + pexpr_put(c1); + } + } + } + + /* tristate options cannot be m, if the choice symbol is boolean */ + if (sym->type == S_BOOLEAN) { + CF_LIST_FOR_EACH(node, items, sym) { + choice = node->elem; + if (choice->type == S_TRISTATE) { + struct pexpr *e = pexpr_not( + pexpr_alloc_symbol(choice->fexpr_m), + data); + sym_add_constraint(sym, e, data); + pexpr_put(e); + } + } + } + + /* all choice options are mutually exclusive for yes */ + CF_LIST_FOR_EACH(node, promptItems, sym) { + struct sym_node *node2; + + choice = node->elem; + list_for_each_entry_from(node2, + &list_next_entry(node, node)->node, + &promptItems->list, node) { + choice2 = node2->elem; + c1 = pexpr_or( + pexpr_not(pexpr_alloc_symbol(choice->fexpr_y), + data), + pexpr_not(pexpr_alloc_symbol(choice2->fexpr_y), + data), + data, PEXPR_ARGX); + sym_add_constraint(sym, c1, data); + pexpr_put(c1); + } + } + + /* if one choice option with a prompt is set to yes, + * then no other option may be set to mod + */ + if (sym->type == S_TRISTATE) { + CF_LIST_FOR_EACH(node, promptItems, sym) { + struct sym_list *tmp; + struct sym_node *node2; + + choice = node->elem; + + tmp = CF_LIST_INIT(sym); + list_for_each_entry_from( + node2, &list_next_entry(node, node)->node, + &promptItems->list, node) { + choice2 = node2->elem; + if (choice2->type == S_TRISTATE) + CF_PUSH_BACK(tmp, choice2, sym); + } + if (list_empty(&tmp->list)) + continue; + + CF_LIST_FOR_EACH(node2, tmp, sym) { + struct pexpr *choice2_mod = + pexpr_alloc_symbol(choice2->fexpr_m); + + choice2 = node2->elem; + if (list_is_first(&node2->node, &tmp->list)) + c1 = pexpr_not_share(choice2_mod, data); + else + c1 = pexpr_and( + c1, + pexpr_not_share(choice2_mod, + data), + data, PEXPR_ARGX); + + PEXPR_PUT(choice2_mod); + } + c1 = pexpr_implies(pexpr_alloc_symbol(choice->fexpr_y), + c1, data, PEXPR_ARGX); + sym_add_constraint(sym, c1, data); + pexpr_put(c1); + } + } + CF_LIST_FREE(promptItems, sym); + CF_LIST_FREE(items, sym); +} + +/* + * build the constraints for invisible options such as defaults + */ +static void add_invisible_constraints(struct symbol *sym, struct cfdata *data) +{ + struct property *prompt = sym_get_prompt(sym); + struct pexpr *promptCondition_both, *promptCondition_yes, *noPromptCond; + struct pexpr *npc; + struct defm_list *defaults; + struct pexpr *default_y, *default_m, *default_both; + + /* no constraints for the prompt, nothing to do here */ + if (prompt != NULL && !prompt->visible.expr) + return; + + if (prompt == NULL) { + promptCondition_both = + pexpr_alloc_symbol(data->constants->const_false); + promptCondition_yes = + pexpr_alloc_symbol(data->constants->const_false); + noPromptCond = pexpr_alloc_symbol(data->constants->const_true); + } else { + struct property *p; + + promptCondition_both = + pexpr_alloc_symbol(data->constants->const_false); + promptCondition_yes = + pexpr_alloc_symbol(data->constants->const_false); + + /* some symbols have multiple prompts */ + for_all_prompts(sym, p) { + promptCondition_both = + pexpr_or(promptCondition_both, + expr_calculate_pexpr_both( + p->visible.expr, data), + data, PEXPR_ARGX); + promptCondition_yes = pexpr_or( + promptCondition_yes, + expr_calculate_pexpr_y(p->visible.expr, data), + data, PEXPR_ARGX); + } + noPromptCond = pexpr_not_share(promptCondition_both, data); + } + + if (NPC_OPTIMISATION) { + struct fexpr *npc_fe = + fexpr_create(data->sat_variable_nr++, FE_NPC, ""); + + if (sym_is_choice(sym)) + str_append(&npc_fe->name, "Choice_"); + + str_append(&npc_fe->name, sym_get_name(sym)); + str_append(&npc_fe->name, "_NPC"); + sym->noPromptCond = npc_fe; + fexpr_add_to_satmap(npc_fe, data); + + npc = pexpr_alloc_symbol(npc_fe); + + if (!sym_is_choice_value(sym) && !sym_is_choice(sym)) { + struct pexpr *c = + pexpr_implies_share(noPromptCond, npc, data); + sym_add_constraint(sym, c, data); + pexpr_put(c); + } + } else { + npc = pexpr_get(noPromptCond); + } + + defaults = calc_default_conditions(sym, data); + default_y = get_default_y(defaults, data); + default_m = get_default_m(defaults, data); + default_both = pexpr_or_share(default_y, default_m, data); + + /* + * tristate elements are only selectable as yes, if they are visible as + * yes + */ + if (sym->type == S_TRISTATE) { + struct pexpr *e1 = pexpr_implies( + promptCondition_both, + pexpr_implies(pexpr_alloc_symbol(sym->fexpr_y), + promptCondition_yes, data, + PEXPR_ARG1), + data, PEXPR_ARG2); + + sym_add_constraint(sym, e1, data); + pexpr_put(e1); + } + + /* if invisible and off by default, then a symbol can only be + * deactivated by its reverse dependencies + */ + if (sym->type == S_TRISTATE) { + struct pexpr *sel_y, *sel_m, *sel_both; + struct pexpr *c1, *c2, *c3; + struct pexpr *d1, *d2, *d3; + struct pexpr *e1, *e2, *e3; + + if (sym->fexpr_sel_y != NULL) { + sel_y = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_y), + pexpr_alloc_symbol(sym->fexpr_sel_y), data, + PEXPR_ARGX); + sel_m = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_m), + pexpr_alloc_symbol(sym->fexpr_sel_m), data, + PEXPR_ARGX); + sel_both = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_y), + pexpr_or(pexpr_alloc_symbol(sym->fexpr_sel_m), + pexpr_alloc_symbol(sym->fexpr_sel_y), + data, PEXPR_ARGX), + data, PEXPR_ARGX); + } else { + sel_y = pexpr_not(pexpr_alloc_symbol(sym->fexpr_y), + data); + sel_m = pexpr_not(pexpr_alloc_symbol(sym->fexpr_m), + data); + sel_both = pexpr_get(sel_y); + } + + c1 = pexpr_implies(pexpr_not_share(default_y, data), sel_y, + data, PEXPR_ARG1); + c2 = pexpr_implies(pexpr_alloc_symbol(modules_sym->fexpr_y), c1, + data, PEXPR_ARG1); + c3 = pexpr_implies_share(npc, c2, data); + sym_add_constraint(sym, c3, data); + + d1 = pexpr_implies(pexpr_not_share(default_m, data), sel_m, + data, PEXPR_ARG1); + d2 = pexpr_implies(pexpr_alloc_symbol(modules_sym->fexpr_y), d1, + data, PEXPR_ARG1); + d3 = pexpr_implies_share(npc, d2, data); + sym_add_constraint(sym, d3, data); + + e1 = pexpr_implies(pexpr_not_share(default_both, data), + sel_both, data, PEXPR_ARG1); + e2 = pexpr_implies( + pexpr_not(pexpr_alloc_symbol(modules_sym->fexpr_y), + data), + e1, data, PEXPR_ARG1); + e3 = pexpr_implies_share(npc, e2, data); + sym_add_constraint(sym, e3, data); + PEXPR_PUT(sel_y, sel_m, sel_both, c1, c2, c3, d1, d2, d3, e1, + e2, e3); + } else if (sym->type == S_BOOLEAN) { + struct pexpr *sel_y; + struct pexpr *e1, *e2; + + if (sym->fexpr_sel_y != NULL) + sel_y = pexpr_implies( + pexpr_alloc_symbol(sym->fexpr_y), + pexpr_alloc_symbol(sym->fexpr_sel_y), data, + PEXPR_ARGX); + else + sel_y = pexpr_not(pexpr_alloc_symbol(sym->fexpr_y), + data); + + e1 = pexpr_implies(pexpr_not_share(default_both, data), + sel_y, data, PEXPR_ARG1); + e2 = pexpr_implies_share(npc, e1, data); + + sym_add_constraint_unique(sym, e2, data); + PEXPR_PUT(sel_y, e1, e2); + } else { + /* if non-boolean is invisible and no default's condition is + * fulfilled, then the symbol is not set + */ + struct pexpr *default_any = get_default_any(sym, data); + struct pexpr *e1 = + pexpr_alloc_symbol(data->constants->const_true); + struct pexpr *e2, *e3; + struct fexpr_node *node; + bool first = true; + + /* e1 = "sym is not set" */ + CF_LIST_FOR_EACH(node, sym->nb_vals, fexpr) { + if (first) { + first = false; + continue; + } + e1 = pexpr_and(e1, + pexpr_not(pexpr_alloc_symbol(node->elem), + data), + data, PEXPR_ARGX); + } + + e2 = pexpr_implies(pexpr_not_share(default_any, data), e1, + data, PEXPR_ARG1); + e3 = pexpr_implies_share(npc, e2, data); + + sym_add_constraint(sym, e3, data); + PEXPR_PUT(default_any, e1, e2, e3); + } + + /* if invisible and on by default, then a symbol can only be deactivated + * by its dependencies + */ + if (list_empty(&defaults->list)) { + // nothing to do + } else if (sym->type == S_TRISTATE) { + struct pexpr *e1; + struct pexpr *e2; + + e1 = pexpr_implies( + npc, + pexpr_implies(default_y, + pexpr_alloc_symbol(sym->fexpr_y), data, + PEXPR_ARG2), + data, PEXPR_ARG2); + sym_add_constraint(sym, e1, data); + + e2 = pexpr_implies( + npc, + pexpr_implies(default_m, + sym_get_fexpr_both(sym, data), + data, PEXPR_ARG2), + data, PEXPR_ARG2); + sym_add_constraint(sym, e2, data); + PEXPR_PUT(e1, e2); + } else if (sym->type == S_BOOLEAN) { + struct pexpr *c; + struct pexpr *c2; + + c = pexpr_implies(default_both, + pexpr_alloc_symbol(sym->fexpr_y), data, + PEXPR_ARG2); + + // TODO tristate choice hack + + c2 = pexpr_implies_share(npc, c, data); + sym_add_constraint(sym, c2, data); + PEXPR_PUT(c, c2); + } else { + /* if non-boolean invisible, then it assumes the correct + * default (if any). + */ + struct defm_node *node; + struct pexpr *cond, *c; + struct fexpr *f; + + CF_LIST_FOR_EACH(node, defaults, defm) { + f = node->elem->val; + cond = node->elem->e; + c = pexpr_implies(npc, + pexpr_implies(cond, + pexpr_alloc_symbol(f), + data, PEXPR_ARG2), + data, PEXPR_ARG2); + sym_add_constraint(sym, c, data); + pexpr_put(c); + } + } + + PEXPR_PUT(promptCondition_yes, promptCondition_both, noPromptCond, npc, + default_y, default_m, default_both); + defm_list_destruct(defaults); +} + +/* + * add the known values from the default and range properties + */ +static void sym_add_nonbool_values_from_default_range(struct symbol *sym, + struct cfdata *data) +{ + struct property *p; + + for_all_defaults(sym, p) { + if (p == NULL) + continue; + + /* add the value to known values, if it doesn't exist yet */ + sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data); + } + + for_all_properties(sym, p, P_RANGE) { + if (p == NULL) + continue; + + /* add the values to known values, if they don't exist yet */ + sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data); + sym_create_nonbool_fexpr(sym, p->expr->right.sym->name, data); + } +} + +/* + * build the range constraints for int/hex: + * For each range and each value in `sym->nb_vals` that's not in the range: + * If the range's condition is fulfilled, then sym can't have this value. + */ +static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data) +{ + struct property *prop; + struct pexpr *prevs; + struct pexpr *propCond; + struct pexpr_list *prevCond; // list of all conditions of the ranges + // from the previous iterations + + prevCond = CF_LIST_INIT(pexpr); + + for_all_properties(sym, prop, P_RANGE) { + int base; + long long range_min, range_max, tmp; + struct fexpr_node *node; + bool first; + + if (prop == NULL) + continue; + + prevs = pexpr_alloc_symbol(data->constants->const_true); + propCond = prop_get_condition(prop, data); + + // construct prevs as "none of the previous ranges' conditions + // were fulfilled but this range's condition is" + if (list_empty(&prevCond->list)) { + pexpr_put(prevs); + prevs = pexpr_get(propCond); +; + } else { + struct pexpr_node *node; + + CF_LIST_FOR_EACH(node, prevCond, pexpr) + prevs = pexpr_and(pexpr_not_share(node->elem, + data), + prevs, data, PEXPR_ARGX); + + prevs = pexpr_and(propCond, prevs, data, + PEXPR_ARG2); + } + CF_PUSH_BACK(prevCond, pexpr_get(propCond), pexpr); + + switch (sym->type) { + case S_INT: + base = 10; + break; + case S_HEX: + base = 16; + break; + default: + return; + } + + range_min = sym_get_range_val(prop->expr->left.sym, base); + range_max = sym_get_range_val(prop->expr->right.sym, base); + + first = true; + /* can skip the first non-boolean value, since this is 'n' */ + CF_LIST_FOR_EACH(node, sym->nb_vals, fexpr) { + struct pexpr *not_nb_val; + struct pexpr *c; + + if (first) { + first = false; + continue; + } + + tmp = strtoll(str_get(&node->elem->nb_val), NULL, base); + + /* known value is in range, nothing to do here */ + if (tmp >= range_min && tmp <= range_max) + continue; + + not_nb_val = + pexpr_not(pexpr_alloc_symbol(node->elem), data); + c = pexpr_implies_share(prevs, not_nb_val, data); + sym_add_constraint(sym, c, data); + PEXPR_PUT(not_nb_val, c); + } + PEXPR_PUT(prevs, propCond); + } + + pexpr_list_free_put(prevCond); + +} + +/* + * at least 1 of the known values for a non-boolean symbol must be true + */ +static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data) +{ + struct pexpr *e; + struct fexpr_node *node; + + if (!sym_is_nonboolean(sym)) + return; + + e = pexpr_alloc_symbol(data->constants->const_false); + CF_LIST_FOR_EACH(node, sym->nb_vals, fexpr) + e = pexpr_or(e, pexpr_alloc_symbol(node->elem), data, + PEXPR_ARGX); + + sym_add_constraint(sym, e, data); + pexpr_put(e); +} + +/* + * at most 1 of the known values for a non-boolean symbol can be true + */ +static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data) +{ + struct fexpr_node *node1; + + if (!sym_is_nonboolean(sym)) + return; + + /* iterate over all subsets of sym->nb_vals of size 2 */ + CF_LIST_FOR_EACH(node1, sym->nb_vals, fexpr) { + struct pexpr *e1 = pexpr_alloc_symbol(node1->elem); + struct fexpr_node *node2; + + list_for_each_entry_reverse(node2, &sym->nb_vals->list, node) { + struct pexpr *e2, *e; + + if (node2 == node1) + break; + e2 = pexpr_alloc_symbol(node2->elem); + e = pexpr_or(pexpr_not_share(e1, data), + pexpr_not_share(e2, data), + data, PEXPR_ARGX); + + sym_add_constraint(sym, e, data); + PEXPR_PUT(e, e2); + } + pexpr_put(e1); + } +} + +/* + * a visible prompt for a non-boolean implies a value for the symbol + */ +static void sym_add_nonbool_prompt_constraint(struct symbol *sym, + struct cfdata *data) +{ + struct property *prompt; + struct pexpr *promptCondition; + struct pexpr *n; + struct pexpr *c = NULL; + + prompt = sym_get_prompt(sym); + if (prompt == NULL) + return; + + promptCondition = prop_get_condition(prompt, data); + n = pexpr_alloc_symbol(sym_get_nonbool_fexpr(sym, "n")); + + if (n->type != PE_SYMBOL || n->left.fexpr == NULL) + goto cleanup; + + c = pexpr_implies(promptCondition, pexpr_not_share(n, data), data, + PEXPR_ARG2); + + sym_add_constraint(sym, c, data); + +cleanup: + PEXPR_PUT(n, promptCondition, c); +} + +static struct default_map *create_default_map_entry(struct fexpr *val, + struct pexpr *e) +{ + struct default_map *map = malloc(sizeof(struct default_map)); + + pexpr_get(e); + map->val = val; + map->e = e; + + return map; +} + +/** + * findDefaultEntry() + * @val: Value that the entry must have + * @defaults: List of defaults to search in + * @constants: To get ``constants->const_false`` from + * + * Finds an entry in @defaults whose &default_map.val attribute is the same + * pointer as the @val argument. + * + * Return: The condition &default_map.e of the found entry, or + * ``pexf(constants->const_false)`` if none was found. To be pexpr_put() by the + * caller. + */ +static struct pexpr *findDefaultEntry(struct fexpr *val, + struct defm_list *defaults, + struct constants *constants) +{ + struct defm_node *node; + + CF_LIST_FOR_EACH(node, defaults, defm) { + if (val == node->elem->val) { + pexpr_get(node->elem->e); + return node->elem->e; + } + } + + return pexpr_alloc_symbol(constants->const_false); +} + +/* + * accumulated during execution of add_defaults(), a disjunction of the + * conditions for all default props of a symbol + */ +static struct pexpr *covered; + +static bool is_tri_as_num(struct symbol *sym) +{ + if (!sym->name) + return false; + + return !strcmp(sym->name, "0") + || !strcmp(sym->name, "1") + || !strcmp(sym->name, "2"); +} + +/** + * add_to_default_map() - Add to or update an entry in a default list + * @entry: Will be consumed by this function, i.e. the caller should and need + * only access @entry via @defaults. + */ +static void add_to_default_map(struct defm_list *defaults, + struct default_map *entry, struct symbol *sym) +{ + /* as this is a map, the entry must be replaced if it already exists */ + if (sym_is_boolean(sym)) { + struct default_map *map; + struct defm_node *node; + + CF_LIST_FOR_EACH(node, defaults, defm) { + map = node->elem; + if (map->val->sym == entry->val->sym) { + pexpr_put(map->e); + map->e = entry->e; + free(entry); + return; + } + } + CF_PUSH_BACK(defaults, entry, defm); + } else { + struct default_map *map; + struct defm_node *node; + + CF_LIST_FOR_EACH(node, defaults, defm) { + map = node->elem; + if (map->val->satval == entry->val->satval) { + pexpr_put(map->e); + map->e = entry->e; + free(entry); + return; + } + } + CF_PUSH_BACK(defaults, entry, defm); + } +} + +/** + * updateDefaultList() - Update a default list with a new value-condition pair + * @val: The value whose condition will be updated + * @newCond: The condition of the default prop. Does not include the condition + * that the earlier default's conditions are not fulfilled. + * @result: the default list + * @sym: the symbol that the defaults belong to + * + * Update the condition that @val will be used for @sym by considering the next + * default property, whose condition is given by @newCond. + */ +static void updateDefaultList(struct fexpr *val, struct pexpr *newCond, + struct defm_list *result, struct symbol *sym, + struct cfdata *data) +{ + // The current condition of @val deduced from the previous default props + struct pexpr *prevCond = findDefaultEntry(val, result, data->constants); + // New combined condition for @val + struct pexpr *condUseVal = + pexpr_or(prevCond, + pexpr_and(newCond, pexpr_not_share(covered, data), + data, PEXPR_ARG2), + data, PEXPR_ARG2); + add_to_default_map(result, create_default_map_entry(val, condUseVal), + sym); + covered = pexpr_or(covered, newCond, data, PEXPR_ARG1); + PEXPR_PUT(prevCond, condUseVal); +} + +/** + * add_defaults() - Generate list of default values and their conditions + * @defaults: List of the default properties + * @ctx: Additional condition that needs to be fulfilled for any default. May be + * NULL. + * @result: List that will be filled + * @sym: Symbol that the defaults belong to + * + * Creates a map from values that @sym can assume to the conditions under which + * they will be assumed. Without @ctx, this will only consider the conditions + * directly associated with the defaults, e.g. sym->dir_dep would not be + * considered. + * + * As a side effect, the &symbol->nb_vals of @sym will be added for + * all default values (as well as the @symbol->nb_vals of other symbols @sym has + * as default (recursively)). + */ +static void add_defaults(struct prop_list *defaults, struct expr *ctx, + struct defm_list *result, struct symbol *sym, + struct cfdata *data) +{ + struct prop_node *node; + struct property *p; + struct expr *expr; + + CF_LIST_FOR_EACH(node, defaults, prop) { + p = node->elem; + /* calculate expr as whether the default's condition (and the + * one inherited from ctx) is fulfilled + */ + if (p->visible.expr) { + if (ctx == NULL) + expr = expr_copy(p->visible.expr); + else + expr = expr_alloc_and( + expr_copy(p->visible.expr), + expr_copy(ctx)); + } else { + if (ctx == NULL) + expr = expr_alloc_symbol(&symbol_yes); + else + expr = expr_alloc_and( + expr_alloc_symbol(&symbol_yes), + expr_copy(ctx)); + } + + /* if tristate and def.value = y */ + if (p->expr->type == E_SYMBOL && sym->type == S_TRISTATE && + p->expr->left.sym == &symbol_yes) { + struct pexpr *expr_y = + expr_calculate_pexpr_y(expr, data); + struct pexpr *expr_m = + expr_calculate_pexpr_m(expr, data); + + updateDefaultList(data->constants->symbol_yes_fexpr, + expr_y, result, sym, data); + updateDefaultList(data->constants->symbol_mod_fexpr, + expr_m, result, sym, data); + PEXPR_PUT(expr_y, expr_m); + } + /* if def.value = n/m/y */ + else if (p->expr->type == E_SYMBOL && + sym_is_tristate_constant(p->expr->left.sym) && + sym_is_boolean(sym)) { + struct fexpr *s; + struct pexpr *expr_both = + expr_calculate_pexpr_both(expr, data); + + if (p->expr->left.sym == &symbol_yes) + s = data->constants->symbol_yes_fexpr; + else if (p->expr->left.sym == &symbol_mod) + s = data->constants->symbol_mod_fexpr; + else + s = data->constants->symbol_no_fexpr; + + updateDefaultList(s, expr_both, result, sym, data); + pexpr_put(expr_both); + } + /* if def.value = n/m/y, but written as 0/1/2 for a boolean */ + else if (sym_is_boolean(sym) && p->expr->type == E_SYMBOL && + p->expr->left.sym->type == S_UNKNOWN && + is_tri_as_num(p->expr->left.sym)) { + struct fexpr *s; + struct pexpr *expr_both = + expr_calculate_pexpr_both(expr, data); + + if (!strcmp(p->expr->left.sym->name, "0")) + s = data->constants->symbol_no_fexpr; + else if (!strcmp(p->expr->left.sym->name, "1")) + s = data->constants->symbol_mod_fexpr; + else + s = data->constants->symbol_yes_fexpr; + + updateDefaultList(s, expr_both, result, sym, data); + pexpr_put(expr_both); + } + /* if def.value = non-boolean constant */ + else if (expr_is_nonbool_constant(p->expr)) { + struct fexpr *s = sym_get_or_create_nonbool_fexpr( + sym, p->expr->left.sym->name, data); + struct pexpr *expr_both = + expr_calculate_pexpr_both(expr, data); + + updateDefaultList(s, expr_both, result, sym, data); + pexpr_put(expr_both); + } + /* any expression which evaluates to n/m/y for a tristate */ + else if (sym->type == S_TRISTATE) { + struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr), + expr_copy(expr)); + struct pexpr *expr_y = + expr_calculate_pexpr_y(e_tmp, data); + struct pexpr *expr_m = + expr_calculate_pexpr_m(e_tmp, data); + + updateDefaultList(data->constants->symbol_yes_fexpr, + expr_y, result, sym, data); + updateDefaultList(data->constants->symbol_mod_fexpr, + expr_m, result, sym, data); + PEXPR_PUT(expr_y, expr_m); + expr_free(e_tmp); + } + /* if non-boolean && def.value = non-boolean symbol */ + else if (p->expr->type == E_SYMBOL && sym_is_nonboolean(sym) && + sym_is_nonboolean(p->expr->left.sym)) { + CF_DEF_LIST(nb_sym_defaults, prop); + struct property *p_tmp; + + /* Add defaults of other symbol as possible defaults for + * this symbol + */ + for_all_defaults(p->expr->left.sym, p_tmp) + CF_PUSH_BACK(nb_sym_defaults, p_tmp, prop); + + add_defaults(nb_sym_defaults, expr, result, sym, data); + CF_LIST_FREE(nb_sym_defaults, prop); + } + /* any expression which evaluates to n/m/y */ + else { + struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr), + expr_copy(expr)); + struct pexpr *expr_both = + expr_calculate_pexpr_both(e_tmp, data); + + updateDefaultList(data->constants->symbol_yes_fexpr, + expr_both, result, sym, data); + + pexpr_put(expr_both); + expr_free(e_tmp); + } + expr_free(expr); + } +} + +/** + * get_defaults() - Generate list of default values and their conditions + * @sym: Symbol whose defaults we want to look at + * + * Creates a map from values that @sym can assume to the conditions under which + * they will be assumed. This will only consider the conditions + * directly associated with the defaults, e.g. sym->dir_dep would not be + * considered. + * + * As a side effect, the &symbol->nb_vals of @sym will be added for + * all default values (as well as the @symbol->nb_vals of other symbols @sym has + * as default (recursively)). + */ +static struct defm_list *calc_default_conditions(struct symbol *sym, + struct cfdata *data) +{ + CF_DEF_LIST(result, defm); + struct prop_list *defaults; /* list of default props of sym */ + struct property *p; + + covered = pexpr_alloc_symbol(data->constants->const_false); + + defaults = CF_LIST_INIT(prop); + for_all_defaults(sym, p) + CF_PUSH_BACK(defaults, p, prop); + + add_defaults(defaults, NULL, result, sym, data); + CF_LIST_FREE(defaults, prop); + pexpr_put(covered); + + return result; +} + +/* + * return the condition for "y", False if it doesn't exist + */ +static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data) +{ + struct default_map *entry; + struct defm_node *node; + + CF_LIST_FOR_EACH(node, list, defm) { + entry = node->elem; + if (entry->val->type == FE_SYMBOL && + entry->val->sym == &symbol_yes) { + pexpr_get(entry->e); + return entry->e; + } + } + + return pexpr_alloc_symbol(data->constants->const_false); +} + +/* + * return the condition for "m", False if it doesn't exist + */ +static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data) +{ + struct default_map *entry; + struct defm_node *node; + + CF_LIST_FOR_EACH(node, list, defm) { + entry = node->elem; + if (entry->val->type == FE_SYMBOL && + entry->val->sym == &symbol_mod) { + pexpr_get(entry->e); + return entry->e; + } + } + + return pexpr_alloc_symbol(data->constants->const_false); +} + +/* + * return the constraint when _some_ default value will be applied + */ +static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data) +{ + struct property *prop; + struct expr *e; + struct pexpr *p; + + if (!sym_is_nonboolean(sym)) + return NULL; + + p = pexpr_alloc_symbol(data->constants->const_false); + for_all_defaults(sym, prop) { + if (prop->visible.expr) + e = expr_copy(prop->visible.expr); + else + e = expr_alloc_symbol(&symbol_yes); + + if (expr_can_evaluate_to_mod(e)) + p = pexpr_or(p, expr_calculate_pexpr_both(e, data), + data, PEXPR_ARGX); + + p = pexpr_or(p, expr_calculate_pexpr_y(e, data), data, + PEXPR_ARGX); + + expr_free(e); + } + + return p; +} + +/* + * get the value for the range + */ +static long sym_get_range_val(struct symbol *sym, int base) +{ + sym_calc_value(sym); + switch (sym->type) { + case S_INT: + base = 10; + break; + case S_HEX: + base = 16; + break; + default: + break; + } + return strtol(sym->curr.val, NULL, base); +} + +/* + * count the number of all constraints + */ +unsigned int count_constraints(void) +{ + unsigned int c = 0; + struct symbol *sym; + + for_all_symbols(sym) { + if (sym->type == S_UNKNOWN) + continue; + + c += list_size(&sym->constraints->list); + } + + return c; +} + +/* + * add a constraint for a symbol + */ +void sym_add_constraint(struct symbol *sym, struct pexpr *constraint, + struct cfdata *data) +{ + if (!constraint) + return; + + /* no need to add that */ + if (constraint->type == PE_SYMBOL && + constraint->left.fexpr == data->constants->const_true) + return; + + /* this should never happen */ + if (constraint->type == PE_SYMBOL && + constraint->left.fexpr == data->constants->const_false) + perror("Adding const_false."); + + CF_PUSH_BACK(sym->constraints, pexpr_get(constraint), pexpr); + + if (!pexpr_is_nnf(constraint)) + pexpr_print("Not NNF:", constraint, -1); +} + +/* + * add a constraint for a symbol, but check for duplicate constraints + */ +void sym_add_constraint_unique(struct symbol *sym, struct pexpr *constraint, + struct cfdata *data) +{ + struct pexpr_node *node; + + if (!constraint) + return; + + /* no need to add that */ + if (constraint->type == PE_SYMBOL && + constraint->left.fexpr == data->constants->const_true) + return; + + /* this should never happen */ + if (constraint->type == PE_SYMBOL && + constraint->left.fexpr == data->constants->const_false) + perror("Adding const_false."); + + /* check the constraints for the same symbol */ + CF_LIST_FOR_EACH(node, sym->constraints, pexpr) + if (pexpr_test_eq(constraint, node->elem, data)) + return; + + CF_PUSH_BACK(sym->constraints, pexpr_get(constraint), pexpr); + + if (!pexpr_is_nnf(constraint)) + pexpr_print("Not NNF:", constraint, -1); +} diff --git a/scripts/kconfig/cf_constraints.h b/scripts/kconfig/cf_constraints.h new file mode 100644 index 000000000000..a68dc9ba4f03 --- /dev/null +++ b/scripts/kconfig/cf_constraints.h @@ -0,0 +1,24 @@ +/* SPDX-License-Identifier: GPL-2.0 */ +/* + * Copyright (C) 2023 Patrick Franz + */ + +#ifndef CF_CONSTRAINTS_H +#define CF_CONSTRAINTS_H + +#include "cf_defs.h" +#include "expr.h" + +/* build the constraints for each symbol */ +void build_constraints(struct cfdata *data); + +/* count the number of all constraints */ +unsigned int count_constraints(void); + +/* add a constraint for a symbol */ +void sym_add_constraint(struct symbol *sym, struct pexpr *constraint, struct cfdata *data); + +/* add a constraint for a symbol, but check for duplicate constraints */ +void sym_add_constraint_unique(struct symbol *sym, struct pexpr *constraint, struct cfdata *data); + +#endif