Support kconfirm-smt

README.md

@@ -284,6 +284,7 @@ There are also some general known limitations of torte. [^1]
 | [FeatureIDE/FeatJAR](https://github.com/FeatureIDE/FeatJAR) | 3fc8d66 | 2025-10-10 | [^12] [^15] [^6] |
 | [FeatureIDE/FeatureIDE](https://github.com/FeatureIDE/FeatureIDE) | 3.9.1 | 2022-12-06 | [^13] [^14] [^15] |
 | [isselab/configfix](https://github.com/ekuiter/torte-ConfigFix) | 0312ab7 | 2025-11-28 | [^33] [^39] [^40] [^42] |
+| [julianbraha/kconfirm](https://github.com/julianbraha/kconfirm) ([kconfirm-smt](https://github.com/julianbraha/kconfirm/tree/smt/kconfirm-smt)) | 176c549 | 2026-08-02 | [^43] |
 | [paulgazz/kmax](https://github.com/paulgazz/kmax) ([KClause](https://github.com/paulgazz/kmax/blob/master/kmax/kclause)) | 4.9 | 2025-10-27 | [^4] [^5] [^7] [^8] [^24] [^22] [^42] |
 | [Z3Prover/z3](https://github.com/Z3Prover/z3) | 4.11.2 | 2022-09-04 | [^10] |
 | [zephyrproject-rtos/Kconfiglib](https://github.com/zephyrproject-rtos/Kconfiglib) | 601f63d | 2025-11-04 | [^2] |
@@ -353,8 +354,11 @@ We did not succeed with the following systems: Buildroot, Freetz-NG, L4Re.
 [^39]: ConfigFix does not offer a feature extraction mechanism, so the computations for (un-)constrained features cannot be applied for this extractor.
 
 [^40]: ConfigFix has a [known bug](https://github.com/isselab/configfix/issues/1) that causes formulas of recent Linux versions (>= 6.16) to be unsatisfiable.
+
 While this issue is being resolved, we recommend to only extract formulas for Linux <= 6.15.
 
+[^43]: kconfirm-smt currently supports Linux only. Enable it explicitly with `extract-kconfig-models --with-kconfirm-smt y`. It emits SMT-LIB2 (`.smt2`) directly, and represents Kconfig's int / hex and string options as SMT integers and strings, respectively. Imply semantics are supported. Select's overreach of dependencies is also supported. Not compatible with transformations that expect Torte's legacy `.model` syntax.
+
 [^2]: UVL hierarchy extraction using Kconfiglib is currently experimental.
 In particular, this extraction is not available for all systems and revisions because it heavily relies on the parsing behavior of Kconfiglib.
 Also, this hierarchy extraction introduces implications due to parent-child relationships.

src/docker/kconfirm-smt/Dockerfile

@@ -0,0 +1,31 @@
+FROM rust:1.85-bookworm
+
+# kconfirm-smt builds its Z3 binding against the system library and evaluates
+# Linux Kconfig preprocessor macros with the host compiler.
+RUN apt-get update && apt-get install -y \
+    bc \
+    bison \
+    build-essential \
+    flex \
+    git \
+    libelf-dev \
+    libssl-dev \
+    libz3-dev \
+    parallel \
+    perl \
+    pkg-config \
+    python3 \
+    && rm -rf /var/lib/apt/lists/*
+
+WORKDIR /home
+RUN git clone https://github.com/julianbraha/kconfirm.git \
+    && cd kconfirm \
+    && git checkout 176c5495234e48c3907d78f955f09d76e310dd90 \
+    && cargo build --release -p kconfirm-smt
+
+RUN git config --global --add safe.directory '*' \
+    && git config --global user.email "anon@example.com" \
+    && git config --global user.name "anon" \
+    && git config --global init.defaultBranch main
+
+WORKDIR /home

src/lib/extraction.sh

@@ -159,6 +159,27 @@ extract-kconfig-model-with-kclause(system, revision, kconfig_file, lkc_binding_f
     MEASURED_TIME=$((MEASURED_TIME+$(grep -oP "^measure_time=\K.*" < "$output_log")))
 }
 
+# runs kconfirm-smt to extract a complete Linux Kconfig model as SMT-LIB2
+# sets the global MEASURED_TIME variable
+extract-kconfig-model-with-kconfirm-smt(system, revision, kconfig_model, features_file, output_log, options=, timeout=0) {
+    if [[ $system != linux ]]; then
+        echo "kconfirm-smt currently supports Linux only."
+        return
+    fi
+
+    # shellcheck disable=SC2086
+    measure "$timeout" /home/kconfirm/target/release/kconfirm-smt \
+        --linux . \
+        --output-smt-lib "$kconfig_model" \
+        $options \
+        | tee "$output_log"
+    MEASURED_TIME=$(grep -oP "^measure_time=\K.*" < "$output_log")
+
+    # Config option names precede the SMT encoding suffixes (>=m, >=y, and
+    # :vis). This list also lets downstream feature-set stages work normally.
+    sed -nE 's/^\(declare-fun \|?([^|:>= ]+).*/\1/p' "$kconfig_model" | sort -u > "$features_file"
+}
+
 # runs ConfigFix to extract a feature-model formula from Kconfig files
 # sets the global MEASURED_TIME variable
 extract-kconfig-model-with-configfix(system, revision, kconfig_file, kconfig_model, features_file, output_log, lkc_directory, lkc_target=config, lkc_output_directory=, options=, timeout=0, date_prefix=) {
@@ -264,20 +285,23 @@ extract-kconfig-model(extractor, lkc_binding, system, revision, kconfig_file, lk
         date_prefix="[$(date -d "@$(git -C "$(input-directory)/$system" log -1 --format="%ct" "$revision_without_context")" +"$date_prefix")]"
     fi
     local file_extension="model"
-    if [[ $extractor == configfix ]]; then
-        file_extension="model"
+    if [[ $extractor == kconfirm-smt ]]; then
+        file_extension="smt2"
     fi
     log "" "$(echo-progress extract)"
     trap 'ec=$?; (( ec != 0 )) && rm-safe '"$(output-path "$system" "${date_prefix}$revision")"'*' EXIT
     push "$(input-directory)/$system"
     local kconfig_model
-    kconfig_model=$(output-path "$system" "${date_prefix}$revision.model")
+    kconfig_model=$(output-path "$system" "${date_prefix}$revision.$file_extension")
     local features_file
     features_file=$(output-path "$system" "${date_prefix}$revision.features")
     local output_log
     output_log=$(mktemp)
     set-environment "$environment"
-    if [[ $extractor != configfix ]]; then
+    if [[ $extractor == kconfirm-smt ]]; then
+        extract-kconfig-model-with-kconfirm-smt \
+            "$system" "$revision" "$kconfig_model" "$features_file" "$output_log" "$options" "$timeout"
+    elif [[ $extractor != configfix ]]; then
         # at this point, the KConfig file should already have been generated by the makefiles during binding compilation
         if [[ -f $kconfig_file ]]; then
             if [[ -f $lkc_binding_file ]]; then
@@ -313,8 +337,13 @@ extract-kconfig-model(extractor, lkc_binding, system, revision, kconfig_file, lk
         if [[ $extractor != configfix ]]; then
             features=$(wc -l < "$features_file")
         fi
-        variables=$(sed "s/)/)\n/g" < "$kconfig_model" | grep "def(" | sed "s/.*def(\(.*\)).*/\1/g" | sort | uniq | wc -l)
-        literals=$(sed "s/)/)\n/g" < "$kconfig_model" | grep -c "def(")
+        if [[ $extractor == kconfirm-smt ]]; then
+            variables=$(grep -Ec '^\(declare-(const|fun) ' "$kconfig_model")
+            literals=$(grep -c '^[(]assert ' "$kconfig_model")
+        else
+            variables=$(sed "s/)/)\n/g" < "$kconfig_model" | grep "def(" | sed "s/.*def(\(.*\)).*/\1/g" | sort | uniq | wc -l)
+            literals=$(sed "s/)/)\n/g" < "$kconfig_model" | grep -c "def(")
+        fi
         kconfig_model=${kconfig_model#"$(output-directory)/"}
     fi
     echo "$system,$revision_without_context,$context,$lkc_binding_file,$kconfig_file,${environment//,/|},$options,$kconfig_model,$features,$variables,$literals,$MEASURED_TIME" >> "$(output-csv)"
@@ -399,6 +428,12 @@ extract-kconfig-models-with-configfix(options=, timeout=0, date_prefix=) {
     experiment-systems
 }
 
+# extracts complete Linux Kconfig models as SMT-LIB2 using kconfirm-smt
+extract-kconfig-models-with-kconfirm-smt(options=, timeout=0, date_prefix=) {
+    register-kconfig-extractor kconfirm-smt "$(none)" "$options" "$timeout" "$date_prefix"
+    experiment-systems
+}
+
 # extracts a non-flat UVL feature hierarchy from KConfig files by leveraging their menu structure
 # relies on KConfiglib for parsing the KConfig files, which may not succeed for all systems and revisions
 # so this is an optional step that can be used to enrich a flat UVL feature model with a hierarchy
@@ -479,4 +514,4 @@ extract-kconfig-hierarchies-with-kconfiglib(timeout=0) {
 mount-for-hierarchy-extraction(input=, uvl_input=transform-to-uvl-with-featureide, unconstrained_features_input=compute-unconstrained-features) {
     input=${input:-$ROOT_STAGE}
     echo "$MAIN_INPUT_KEY=$input,$UVL_INPUT_KEY=$uvl_input,$UNCONSTRAINED_FEATURES_INPUT_KEY=$unconstrained_features_input"
-}
+}

src/lib/stages.sh

@@ -40,10 +40,10 @@ define-stages() {
             --date-prefix "$date_prefix"
     }
 
-    # extracts kconfig models with kconfigreader, kclause, and/or configfix
-    # configfix is disabled by default, because it is experimental
-    extract-kconfig-models(input=, output=extract-kconfig-models, iteration_field=, options=, timeout=0, with_kconfigreader=, with_kclause=, with_configfix=, date_prefix=) {
-        if [[ -z $with_kconfigreader ]] && [[ -z $with_kclause ]] && [[ -z $with_configfix ]]; then
+    # extracts kconfig models with kconfigreader, kclause, configfix, and/or kconfirm-smt
+    # configfix and kconfirm-smt are disabled by default, because they are experimental and Linux-only, respectively
+    extract-kconfig-models(input=, output=extract-kconfig-models, iteration_field=, options=, timeout=0, with_kconfigreader=, with_kclause=, with_configfix=, with_kconfirm_smt=, date_prefix=) {
+        if [[ -z $with_kconfigreader ]] && [[ -z $with_kclause ]] && [[ -z $with_configfix ]] && [[ -z $with_kconfirm_smt ]]; then
             with_kconfigreader=y
             with_kclause=y
             with_configfix=n
@@ -54,6 +54,8 @@ define-stages() {
         [[ $with_kclause == y ]] && with_kclause=1
         [[ $with_configfix == n ]] && with_configfix=
         [[ $with_configfix == y ]] && with_configfix=1
+        [[ $with_kconfirm_smt == n ]] && with_kconfirm_smt=
+        [[ $with_kconfirm_smt == y ]] && with_kconfirm_smt=1
         local inputs=()
 
         if [[ -n $with_kconfigreader ]]; then
@@ -92,6 +94,18 @@ define-stages() {
             inputs+=("extract-kconfig-models-with-configfix")
         fi
 
+        if [[ -n $with_kconfirm_smt ]]; then
+            extract-kconfig-models-with \
+                --extractor kconfirm-smt \
+                --input "$input" \
+                --iterations "$with_kconfirm_smt" \
+                --iteration-field "$iteration_field" \
+                --options "$options" \
+                --timeout "$timeout" \
+                --date-prefix "$date_prefix"
+            inputs+=("extract-kconfig-models-with-kconfirm-smt")
+        fi
+
         # aggregate all extracted models in one stage
         aggregate \
             --output "$output" \

src/systems/linux.sh

@@ -105,7 +105,9 @@ tag-old-releases-linux-helper(base_uri, start_inclusive=, end_exclusive=) {
 }
 
 kconfig-post-checkout-hook-linux(system, revision) {
-    if [[ $system == linux ]]; then
+    # kconfirm-smt evaluates Kconfig macros itself, so preserve the original
+    # source instead of applying the LKC compatibility rewrites below.
+    if [[ $system == linux ]] && [[ $EXTRACTOR != kconfirm-smt ]]; then
         replace-linux(regex, replacement=) { find ./ -type f -name "*Kconfig*" -exec sed -i "s/$regex/$replacement/g" {} \;; }
         # ignore all constraints that use the newer $(success,...) syntax
         replace-linux "\s*default \$(.*" # default values are not translated into the formula anyway, so we can ignore them