Repository: paulgazz/kmax (language: python)

Issue:
kismet: raise specific error when Kconfig files can't be opened
Catch exceptions of type `Arch.CantOpenKconfigFiles` and write a specific
error message to inform the issue with the input Kconfig specifications.

For example, when you run the following in a Linux git copy:
```
git checkout 012e3ca3cb4d7f
kismet -a x86_64
```

kismet will output (tail of the kismet logs) and terminate:

```
ERROR: Can't open Kconfig files:
  drivers/media/platform/Kconfig:69: can't open file "drivers/media/platform/am437x/Kconfig"
```

Fixes https://github.com/paulgazz/kmax/issues/164


Discussion / hints:

Fix patch:
diff --git a/README.md b/README.md
index 17ee2983..f4e6a59b 100644
--- a/README.md
+++ b/README.md
@@ -1,100 +1,97 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
-- [The Kmax Tool Suite](#the-kmax-tool-suite)
-  - [Getting Started](#getting-started)
-  - [Cross-Compiling](#cross-compiling)
-  - [Installing from Source](#installing-from-source)
-  - [Additional Documentation](#additional-documentation)
+- [The kmax tool suite](#the-kmax-tool-suite)
+  - [Getting started](#getting-started)
+    - [Installing the kmax tool suite](#installing-the-kmax-tool-suite)
+    - [Kicking the tires](#kicking-the-tires)
+  - [Using `klocalizer --repair` on patches](#using-klocalizer---repair-on-patches)
+  - [Using `kismet`](#using-kismet)
+  - [Additional documentation](#additional-documentation)
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
 
-# The Kmax Tool Suite
-
-## Getting Started
+# The kmax tool suite
 
-Kmax currently depends on python 3.8 or later.  Install kmax in one of two ways:
+## Getting started
 
-1. In a python virtual environment (_recommended_):
+### Installing the kmax tool suite
 
-        sudo apt install -y python3-pip python3-venv flex bison bc libssl-dev libelf-dev
-        python3 -m venv kmax_env  # create the environment
-        source kmax_env/bin/activate  # enter the environment
-        pip3 install kmax  # install kmax in the environment
-    
-2. System-wide:
+Install the requiste python tools (the kmax tool suite currently depends on python 3.8 or later), setup a python virtual environment (recommended), and finally install the tools from pip.
 
-        sudo apt install -y python3-pip flex bison bc libssl-dev libelf-dev
-        sudo pip3 install kmax
+    sudo apt install -y python3 python3-pip python3-venv
+    python3 -m venv ~/env_kmax/
+    source ~/env_kmax/bin/activate
+    pip3 install kmax
 
-Download and enter the Linux source:
+Instructions to install from source can be found in the [advanced documentation](docs/advanced.md).
 
-    wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.4.tar.xz
-    tar -xvf linux-5.4.tar.xz
-    cd linux-5.4/
 
-### `klocalizer`
+### Kicking the tires
 
-Run `klocalizer` to generate a `.config` file that builds a given compilation unit:
+Install dependencies for compiling Linux source, then download and enter the Linux source:
 
-    klocalizer drivers/usb/storage/alauda.o
+    sudo apt install -y flex bison bc libssl-dev libelf-dev
+    cd ~/
+    wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.16.tar.xz
+    tar -xvf linux-5.16.tar.xz
+    cd ~/linux-5.16/
 
-Build the `.config` file made by `klocalizer` to confirm inclusion of the compilation unit:
+Run `klocalizer --repair` to modify `allnoconfig` so that builds a given compilation unit:
 
-    make ARCH=x86_64 olddefconfig
-    make ARCH=x86_64 clean drivers/usb/storage/alauda.o
-    
-### `kismet`
+    make allnoconfig
+    klocalizer --repair .config -o allnoconfig_repaired --include drivers/usb/storage/alauda.o
+    KCONFIG_CONFIG=allnoconfig_repaired make ARCH=x86_64 olddefconfig clean drivers/usb/storage/alauda.o
     
-Run `kismet` to find unmet dependency bugs due to Kconfig's [reverse dependencies](https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html#menu-attributes):
+You should see `CC      drivers/usb/storage/alauda.o` at the end of the build.
 
-    kismet --linux-ksrc="./" -a=x86_64
 
-Once finished (it can take about an hour), kismet will produce three outputs:
-
-  1. A summary of the results in `kismet_summary_x86_64.txt`
-  2. A list of results for each `select` construct in `kismet_summary_x86_64.csv` (`UNMET_ALARM` denotes the buggy ones)
-  3. A list of `.config` files meant to exercise each bug in `kismet-test-cases/`
+## Using `klocalizer --repair` on patches
 
-Technical details can be found in the [paper](https://paulgazzillo.com/papers/esecfse21.pdf) on `kclause` and `kismet`.  The experiment [replication script](scripts/kismet_experiments_replication.sh) can be used to run kismet on all architectures' Kconfig specifications.
+First install [SuperC](https://github.com/appleseedlab/superc), which `klocalizer` depends on for per-line, `#ifdef` constraints:
 
+    sudo apt-get install -y libz3-java libjson-java sat4j unzip flex bison bc libssl-dev libelf-dev xz-utils lftp
+    wget -O - https://raw.githubusercontent.com/appleseedlab/superc/master/scripts/install.sh | bash
+    export CLASSPATH=${CLASSPATH}:/usr/share/java/org.sat4j.core.jar:/usr/share/java/json-lib.jar:${HOME}/.local/share/superc/z3-4.8.12-x64-glibc-2.31/bin/com.microsoft.z3.jar:${HOME}/.local/share/superc/JavaBDD/javabdd-1.0b2.jar:${HOME}/.local/share/superc/xtc.jar:${HOME}/.local/share/superc/superc.jar
+    export PATH=${PATH}:${HOME}/.local/bin/
 
-## Cross-Compiling Linux Compilation Units
+Start with a clone of the linux repository and get a patch file:
 
-Get `make.cross`:
-
-    sudo apt install -y xz-utils lftp
-    wget https://raw.githubusercontent.com/fengguang/lkp-tests/master/sbin/make.cross
+    cd ~/
+    git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
+    cd ~/linux/
+    git checkout 6fc88c354f3af
+    git show > 6fc88c354f3af.diff
+    
+Repair allnoconfig to include lines of the patch and test the build.  When using `--include-mutex` all configuration files needed to cover the patch are exported as `NUM-ARCH.config`:
 
-Run `klocalizer` with a different architecture:
+    make allnoconfig
+    klocalizer --repair .config -a x86_64 --include-mutex 6fc88c354f3af.diff
+    KCONFIG_CONFIG=0-x86_64.config make ARCH=x86_64 olddefconfig clean kernel/bpf/cgroup.o net/ipv4/af_inet.o net/ipv4/udp.o net/ipv6/af_inet6.o net/ipv6/udp.o
+    
 
-    klocalizer -a powerpc drivers/block/ps3disk.o
-    bash make.cross ARCH=powerpc olddefconfig; bash make.cross ARCH=powerpc clean drivers/block/ps3disk.o
+## Using `kismet`
 
+This tool will check for unmet dependency bugs in [Kconfig specifications](https://www.kernel.org/doc/html/latest/kbuild/kconfig-language.html#menu-attributes) due to reverse dependencies overriding direct dependencies.
 
-## Installing Kmax from Source
+Run `kismet` on the root of the Linux source tree.
 
-Install the prerequisites
+    kismet --linux-ksrc="${HOME}/linux-5.16/" -a=x86_64
 
-    sudo apt install -y python3-setuptools python3-dev
-    
-Clone and install kmax
+Once finished (it can take about an hour on a commodity desktop), kismet will produce three outputs:
 
-    git clone https://github.com/paulgazz/kmax.git
-    cd kmax
-    sudo python3 setup.py install
+  1. A summary of the results in `kismet_summary_x86_64.txt`
+  2. A list of results for each `select` construct in `kismet_summary_x86_64.csv` (`UNMET_ALARM` denotes the buggy ones)
+  3. A list of `.config` files meant to exercise each bug in `kismet-test-cases/`
 
-Alternatilvely, installing for development to obviate the need to
-rereun setup.py when making changes to the code
+Technical details can be found in in the [kismet documentation](docs/advanced.md#kismet) and the [publication](https://paulgazzillo.com/papers/esecfse21.pdf) on `kclause` and `kismet`.  The experiment [replication script](scripts/kismet_experiments_replication.sh) can be used to run kismet on all architectures' Kconfig specifications.
 
-    sudo python3 setup.py develop
 
-## Additional Documentation
+## Additional documentation
 
-[Overview](https://github.com/paulgazz/kmax/blob/master/docs/overview.md)
+[Overview](docs/overview.md)
 
-[Advanced Usage](https://github.com/paulgazz/kmax/blob/master/docs/advanced.md)
+[Advanced Usage](docs/advanced.md)
 
-[Bugs Found](https://github.com/paulgazz/kmax/blob/master/docs/bugs_found.md)
+[Bugs Found](docs/bugs_found.md)
diff --git a/docs/advanced.md b/docs/advanced.md
index a21be28b..a7b7f30a 100644
--- a/docs/advanced.md
+++ b/docs/advanced.md
@@ -1,8 +1,19 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Advanced Usage](#advanced-usage)
+  - [Installing from Source](#installing-from-source)
+  - [`klocalizer` and `krepair`](#klocalizer-and-krepair)
+    - [Example usage](#example-usage)
+    - [Coverage report](#coverage-report)
+    - [`ERROR: SuperC checks failed`](#error-superc-checks-failed)
+    - [Getting configuration files to build commit ranges](#getting-configuration-files-to-build-commit-ranges)
+  - [`kismet`](#kismet)
+    - [Analysis stages](#analysis-stages)
+      - [Syntactical optimization](#syntactical-optimization)
+      - [Optimized SAT check](#optimized-sat-check)
+      - [Precise SAT check](#precise-sat-check)
+    - [Summary format](#summary-format)
   - [Annotated Example](#annotated-example)
   - [Use Cases](#use-cases)
     - [A compilation unit not built by allyesconfig](#a-compilation-unit-not-built-by-allyesconfig)
@@ -22,17 +33,133 @@
     - [Example](#example)
     - [Other uses](#other-uses)
       - [Get a list of all visible configs](#get-a-list-of-all-visible-configs)
-  - [Kismet](#kismet)
-    - [Analysis stages](#analysis-stages)
-      - [Syntactical optimization](#syntactical-optimization)
-      - [Optimized SAT check](#optimized-sat-check)
-      - [Precise SAT check](#precise-sat-check)
-    - [Summary format](#summary-format)
 
 <!-- END doctoc generated TOC please keep comment here to allow auto update -->
 
 # Advanced Usage
 
+## Installing from Source
+
+Install the prerequisites
+
+    sudo apt install -y python3-setuptools python3-dev
+    
+Clone and install kmax
+
+    git clone https://github.com/paulgazz/kmax.git
+    cd kmax
+    python3 -m venv ~/kmax_env/
+    source ~/kmax_env/bin/activate
+    python3 setup.py install
+
+Alternatively, installing for development to obviate the need to
+rereun setup.py when making changes to the code
+
+    python3 setup.py develop
+
+
+## `klocalizer` and `krepair`
+
+### Example usage
+
+`klocalizer --repair` can repair existing configuration files to include given source code directories, files, and lines from Linux kernel source code.  For instance, let's use it to repair the minimal `allnoconfig` so that it includes specific lines of `kernel/bpf/cgroup.c`.  `allnoconfig` will not even include the source file,
+
+    cd ~/linux-5.16/
+    make allnoconfig
+    make kernel/bpf/cgroup.o
+    
+results in an error: `make[2]: *** No rule to make target 'kernel/bpf/cgroup.o'.  Stop.`  We can ensure that the relevant configuration options are modified in `allnoconfig` in order to include this file and any specified lines:
+
+    make allnoconfig  # configuration file stored in .config
+    klocalizer --repair .config --include-mutex kernel/bpf/cgroup.o:[1354,1357-1359]
+
+This produces a new version of the `.config` file in `0-x86_64.config`.  To build with it, install it with `olddefconfig` and attempt to build the source file:
+
+    cp 0-x86_64.config .config
+    make olddefconfig
+    make kernel/bpf/cgroup.o
+    
+This time, the source file is successfully built: `CC      kernel/bpf/cgroup.o`.  Any number of `--include-mutex` constraints may be added.  If there is mutual-exclusion among source files, `klocalizer` will as many configuration files needed to cover all constraints.  Always on or off constraints can be added with `--include` or `--exclude`.  See the documentation on [`klocalizer` and `krepair`](docs/advanced.md#klocalizer-and-krepair) for more usage information.
+
+
+### Coverage report
+
+- kmax failed, superc failed
+- unconstrained
+- headers not included
+
+### `ERROR: SuperC checks failed`
+
+Try running `java superc.SuperC -sourcelinePC /dev/null /dev/null`.  If the class is not found, double-check the SuperC installation and your CLASSPATH.
+
+If you get a `java.lang.NoSuchMethodError: 'com.microsoft.z3.BoolExpr com.microsoft.z3.Context.mkAnd(com.microsoft.z3.BoolExpr[])'` error, then there is a mismatch between the z3 java library.  Please be sure that your `superc.jar` and `z3-4.8.12-x64-glibc-2.31/bin/com.microsoft.z3.jar` jarfiles downloaded according to the SuperC installation directions.  Or try [building SuperC](https://github.com/appleseedlab/superc) from scratch.
+
+
+
+### Getting configuration files to build commit ranges
+
+To repair `allnoconfig` to include changed lines from a range of commits, first get the diff file, checkout the version having the patch(es) applied, then call repair:
+
+    cd ~/
+    git clone git://git.kernel.org/pub/scm/linux/kernel/git/torvalds/linux.git
+    cd linux
+    git diff commit1..commit2 > patch.diff
+    git checkout commit2
+    klocalizer --include{-mutex,} patchfile.diff
+    
+    
+    `klocalizer` will also take patches ending in `.patch`, e.g., from `git format-patch` in addition to `.diff` as long as the file is in the unified diff format.  Be sure to run `klocalizer` from the already-patched source tree, since this contains the constraints of the resulting code from the patch.
+
+
+<!-- - headers -->
+<!-- - difference between cosntraints for a directory vs. constraints for the files in the directory -->
+<!-- - doing patches -->
+<!-- - doing commit ranges, git diff HEAD~, git diff commit1..commitN -->
+<!-- - arch stuff, goes through one arch at a time -->
+
+
+<!-- - --include-mutex -->
+<!--   - generates N configs, each will have at least one of the include-mutex configs -->
+<!--   - if not possible to get any config with at least one, then unsat, no configs made -->
+  
+<!-- - --include -->
+<!--   - generates N configs, all will have all --include constraints  (all constraints are included) -->
+  
+<!-- - --exclude -->
+<!--   - generates N configs, none will have any of the --exclude constraints (all cosntraints are excluded) -->
+
+
+## `kismet`
+
+### Analysis stages
+
+`kismet`'s routine consists of a three step analyses pipeline, each at different precisions.
+
+After the identification of the select constructs, each construct is seen as a potential unmet direct dependency case, thus, marked to raise unmet dependency alarm. The subsequent stages works on the alarms of the previous stage, trying to rule out alarms as unmet dependency safe, thus, increasing the precision. While any stage is at least as precise as the stages before it, the earlier stages helps to increase the performance.
+
+#### Syntactical optimization
+Given the fact that a select construct is unmet dependency safe if the selectee has no direct dependency, this stage marks such constructs as unmet safe. This is very fast, and does not involve any SAT solvers but only syntactical analysis of the constructs.
+
+#### Optimized SAT check
+For a select construct to be unmet dependency free, the kclause constraints for the architecture together with the additional unmet dependency free constraints (which we call optimized constraints) must be satisfiable. We name this whole set of constraints as precise constraints. Given the observation that the optimized constraints are much smaller than the precise constraints, SAT solvers can decide the optimized constraints much faster. In this stage, `kismet` discharges the optimized constraints to a SAT solver to rule out more constructs as unmet dependency safe.
+
+#### Precise SAT check
+In this stage, `kismet` discharges the whole set of constraints (optimized and kclause architecture constraints, i.e., precise constraints) to a SAT solver to analyse remaining alarms and rule them as safe. This is the last stage of the static analysis pipeline, where any construct could not be ruled to be unmet safe raise unmet alarms.
+
+### Summary format
+Upon completing the analysis, `kismet` writes a detailed summary in CSV format to the standard output.
+
+This includes the following columns:  
+- `selectee`: The selectee of the select construct.  
+- `selector`: The selector of the select construct.  
+- `visib_id`: The visibility id of the select construct. One (selectee, selector) pair might appear multiple times on different visibility constraints (e.g., within `CONFIG_SELECTOR`, there might be two entries, such as: `select SELECTEE if VISIB1`, `select SELECTEE if VISIB2`). Such constructs are distinguished with this visibility id.  
+- `constraint_type`: There are possibly multiple ways to satisfy the optimized constraints. If exploring the whole unmet space is enabled (disabled by default, use `'--explore-whole-unmet-space` to enable), all expressions to satisfy the optimized constraints are explored individually, called as SAT options. On the other hand, some random solution to precise constraints is called generic option, which suffices to verify alarms. In the summary, generic option has `constraint_type` 0 while exhaustively explored SAT options have `constraint_type` ids starting from 1.  
+- `analysis_result`: one of: `UNMET_ALARM`, `UNMET_SAFE_SYNTACTIC_PASS`, `UNMET_SAFE_OPTIMIZED_PASS`, `UNMET_SAFE_PRECISE_PASS`.  
+- `verified`: If the analysis result is an alarm, includes whether the generated test case for the related construct verifies the alarm.  
+- `forced_target_udd_only`: If the analysis result is an alarm, includes whether forcing the target unmet dependency only was successful.  
+- `testcase`: The path to the generated test case, i.e., sample Kconfig config file.  
+
+
 ## Annotated Example
 
 Run klocalizer for a given compilation unit, e.g.,
@@ -462,33 +589,3 @@ Then, from the root of a Linux source tree, run the following:
     
     # the visibles should be a subset of the configs
     diff configs.txt visible.txt  | grep ">"
-
-## Kismet
-
-`kismet`'s routine consists of a three step analyses pipeline, each at different precisions.
-
-After the identification of the select constructs, each construct is seen as a potential unmet direct dependency case, thus, marked to raise unmet dependency alarm. The subsequent stages works on the alarms of the previous stage, trying to rule out alarms as unmet dependency safe, thus, increasing the precision. While any stage is at least as precise as the stages before it, the earlier stages helps to increase the performance.
-
-### Analysis stages
-
-#### Syntactical optimization
-Given the fact that a select construct is unmet dependency safe if the selectee has no direct dependency, this stage marks such constructs as unmet safe. This is very fast, and does not involve any SAT solvers but only syntactical analysis of the constructs.
-
-#### Optimized SAT check
-For a select construct to be unmet dependency free, the kclause constraints for the architecture together with the additional unmet dependency free constraints (which we call optimized constraints) must be satisfiable. We name this whole set of constraints as precise constraints. Given the observation that the optimized constraints are much smaller than the precise constraints, SAT solvers can decide the optimized constraints much faster. In this stage, `kismet` discharges the optimized constraints to a SAT solver to rule out more constructs as unmet dependency safe.
-
-#### Precise SAT check
-In this stage, `kismet` discharges the whole set of constraints (optimized and kclause architecture constraints, i.e., precise constraints) to a SAT solver to analyse remaining alarms and rule them as safe. This is the last stage of the static analysis pipeline, where any construct could not be ruled to be unmet safe raise unmet alarms.
-
-### Summary format
-Upon completing the analysis, `kismet` writes a detailed summary in CSV format to the standard output.
-
-This includes the following columns:  
-- `selectee`: The selectee of the select construct.  
-- `selector`: The selector of the select construct.  
-- `visib_id`: The visibility id of the select construct. One (selectee, selector) pair might appear multiple times on different visibility constraints (e.g., within `CONFIG_SELECTOR`, there might be two entries, such as: `select SELECTEE if VISIB1`, `select SELECTEE if VISIB2`). Such constructs are distinguished with this visibility id.  
-- `constraint_type`: There are possibly multiple ways to satisfy the optimized constraints. If exploring the whole unmet space is enabled (disabled by default, use `'--explore-whole-unmet-space` to enable), all expressions to satisfy the optimized constraints are explored individually, called as SAT options. On the other hand, some random solution to precise constraints is called generic option, which suffices to verify alarms. In the summary, generic option has `constraint_type` 0 while exhaustively explored SAT options have `constraint_type` ids starting from 1.  
-- `analysis_result`: one of: `UNMET_ALARM`, `UNMET_SAFE_SYNTACTIC_PASS`, `UNMET_SAFE_OPTIMIZED_PASS`, `UNMET_SAFE_PRECISE_PASS`.  
-- `verified`: If the analysis result is an alarm, includes whether the generated test case for the related construct verifies the alarm.  
-- `forced_target_udd_only`: If the analysis result is an alarm, includes whether forcing the target unmet dependency only was successful.  
-- `testcase`: The path to the generated test case, i.e., sample Kconfig config file.  
\ No newline at end of file
diff --git a/docs/bugs_found.md b/docs/bugs_found.md
index 774ac4f9..a19eba09 100644
--- a/docs/bugs_found.md
+++ b/docs/bugs_found.md
@@ -1,11 +1,29 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Bugs Found by Kmax Tools](#bugs-found-by-kmax-tools)
   - [Linux kernel](#linux-kernel)
+    - [crypto: fix unmet dependency on CRYPTO for CRYPTO_LIB_CHACHA_GENERIC](#crypto-fix-unmet-dependency-on-crypto-for-crypto_lib_chacha_generic)
+    - [pinctrl: bcm63xx: fix unmet dependency on REGMAP for GPIO_REGMAP](#pinctrl-bcm63xx-fix-unmet-dependency-on-regmap-for-gpio_regmap)
+    - [input: fix Kconfig dependency on IIO_BUFFER](#input-fix-kconfig-dependency-on-iio_buffer)
+    - [ASoC: au1x: fix unmet dependency on SND_SOC_I2C_AND_SPI for SND_SOC_WM8731](#asoc-au1x-fix-unmet-dependency-on-snd_soc_i2c_and_spi-for-snd_soc_wm8731)
+    - [ASoC: stm32: fix unmet dependency on GPIOLIB for SND_SOC_DMIC](#asoc-stm32-fix-unmet-dependency-on-gpiolib-for-snd_soc_dmic)
+    - [ASoC: mediatek: fix unmet dependency on GPIOLIB for SND_SOC_DMIC](#asoc-mediatek-fix-unmet-dependency-on-gpiolib-for-snd_soc_dmic)
+    - [ASoC: intel: fix unmet dependencies on GPIOLIB for SND_SOC_DMIC and SND_SOC_MAX98357A](#asoc-intel-fix-unmet-dependencies-on-gpiolib-for-snd_soc_dmic-and-snd_soc_max98357a)
+    - [ASoC: amd: fix unmet dependency on GPIOLIB for SND_SOC_DMIC](#asoc-amd-fix-unmet-dependency-on-gpiolib-for-snd_soc_dmic)
+    - [efi: fix unmet dependency on MFD_SYSCON for PINCTRL_ASPEED](#efi-fix-unmet-dependency-on-mfd_syscon-for-pinctrl_aspeed)
+    - [efi: fix unmet dependency on CRYPTO for CRYPTO_LIB_SHA256](#efi-fix-unmet-dependency-on-crypto-for-crypto_lib_sha256)
+    - [ARM: fix unmet dependency on BITREVERSE for HAVE_ARCH_BITREVERSE](#arm-fix-unmet-dependency-on-bitreverse-for-have_arch_bitreverse)
+    - [pinctrl: qcom: fix unmet dependencies on GPIOLIB for GPIOLIB_IRQCHIP](#pinctrl-qcom-fix-unmet-dependencies-on-gpiolib-for-gpiolib_irqchip)
+    - [ASoC: fix unmet dependencies on GPIOLIB for SND_SOC_RT1015P](#asoc-fix-unmet-dependencies-on-gpiolib-for-snd_soc_rt1015p)
+    - [drm/sun4i: fix unmet dependency on RESET_CONTROLLER for PHY_SUN6I_MIPI_DPHY](#drmsun4i-fix-unmet-dependency-on-reset_controller-for-phy_sun6i_mipi_dphy)
+    - [scsi: ufs: fix unmet dependency for RESET_TI_SYSCON when !RESET_CONTROLLER](#scsi-ufs-fix-unmet-dependency-for-reset_ti_syscon-when-reset_controller)
+    - [ASoC: fix unmet dependencies on GPIOLIB for SND_SOC_DMIC](#asoc-fix-unmet-dependencies-on-gpiolib-for-snd_soc_dmic)
+    - [drm: bridge: fix unmet dependency for DRM_PANEL_BRIDGE when !DRM_KMS_HELPER](#drm-bridge-fix-unmet-dependency-for-drm_panel_bridge-when-drm_kms_helper)
+    - [ASoC: fix unmet dependency when SND_SOC_INTEL_KBL_DA7219_MAX98357A_MACH && !GPIOLIB](#asoc-fix-unmet-dependency-when-snd_soc_intel_kbl_da7219_max98357a_mach--gpiolib)
+    - [ASoC: fix unmet dependency for SND_SOC_MAX98357A when !GPIOLIB](#asoc-fix-unmet-dependency-for-snd_soc_max98357a-when-gpiolib)
     - [drivers: pinctrl: qcom: fix unmet dependency for PINCTRL_MSM when !GPIOLIB](#drivers-pinctrl-qcom-fix-unmet-dependency-for-pinctrl_msm-when-gpiolib)
-    - [drivers: gpu: drm: bridge: fix unmet dependency for DRM_KMS_HELPER when !DRM_KMS_HELPER](#drivers-gpu-drm-bridge-fix-unmet-dependency-for-drm_kms_helper-when-drm_kms_helper)
+    - [drivers: gpu: drm: bridge: fix unmet dependency for DRM_PANEL_BRIDGE when !DRM_KMS_HELPER](#drivers-gpu-drm-bridge-fix-unmet-dependency-for-drm_panel_bridge-when-drm_kms_helper)
     - [mips: fix unmet dependency for FRAME_POINTER when !ARCH_WANT_FRAME_POINTERS](#mips-fix-unmet-dependency-for-frame_pointer-when-arch_want_frame_pointers)
     - [mips: fix unmet dependency for MTD_COMPLEX_MAPPINGS when !MTD](#mips-fix-unmet-dependency-for-mtd_complex_mappings-when-mtd)
     - [mips: fix unmet dependency for DEBUG_INFO when !DEBUG_KERNEL](#mips-fix-unmet-dependency-for-debug_info-when-debug_kernel)
diff --git a/docs/experiments/experiments.md b/docs/experiments/experiments.md
index 2e72067a..e0169b4a 100644
--- a/docs/experiments/experiments.md
+++ b/docs/experiments/experiments.md
@@ -1,7 +1,6 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Experiments](#experiments)
   - [Results](#results)
     - [Linux next-20191129 2019-12-02](#linux-next-20191129-2019-12-02)
diff --git a/docs/kextractor_format.md b/docs/kextractor_format.md
index aa6323f3..ad5d35b3 100644
--- a/docs/kextractor_format.md
+++ b/docs/kextractor_format.md
@@ -1,7 +1,6 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Generating a DIMACS version of a Kconfig feature model](#generating-a-dimacs-version-of-a-kconfig-feature-model)
 - [Proto-DIMACS output grammar](#proto-dimacs-output-grammar)
   - [Semantics](#semantics)
diff --git a/docs/kmax_format.md b/docs/kmax_format.md
index 7d758bb4..d8e1db12 100644
--- a/docs/kmax_format.md
+++ b/docs/kmax_format.md
@@ -1,7 +1,6 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Constraints for compilation units in the `full_pc` format](#constraints-for-compilation-units-in-the-full_pc-format)
 - [Constraints for compilation units in the `unit_pc` format](#constraints-for-compilation-units-in-the-unit_pc-format)
 
diff --git a/docs/overview.md b/docs/overview.md
index 4e0c81ce..438e4bc7 100644
--- a/docs/overview.md
+++ b/docs/overview.md
@@ -1,7 +1,6 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Overview](#overview)
   - [Tools](#tools)
   - [Contributors](#contributors)
diff --git a/kmax/arch.py b/kmax/arch.py
index e8d81852..474a440f 100644
--- a/kmax/arch.py
+++ b/kmax/arch.py
@@ -287,6 +287,7 @@ def __init__(self, name: str, linux_ksrc=None, arch_dir=None, is_kclause_composi
     self.__selects_file_delayed_dump = None
 
     # kextract summary cache
+    self.__kconfig_bool_tristate_options=None
     self.__kconfig_types=None
     self.__kconfig_visible=None
     self.__kconfig_has_def_nonbool=None
@@ -501,7 +502,8 @@ def __ensure_kextract_summary(self):
       - kconfig visible
       - kconfig has def nonbool
     """
-    if self.__kconfig_types != None and self.__kconfig_visible != None and self.__kconfig_has_def_nonbool != None:
+    if self.__kconfig_types is not None and self.__kconfig_visible is not None and \
+       self.__kconfig_has_def_nonbool is not None and self.__kconfig_bool_tristate_options is not None:
       # the formulas are already there
       return
 
@@ -511,10 +513,9 @@ def __ensure_kextract_summary(self):
     # generate kextract_summary
     self.__generate_kextract_summary()
 
-  # generates and caches kconfig_types, kconfig_visible, and kconfig_has_def_nonbool from kextract
   def __generate_kextract_summary(self):
-    """Generate and set kextract summary (kconfig_types, kconfig_visible, and
-    kconfig_has_def_nonbool) from kextract.
+    """Generate and set kextract summary (kconfig_types, kconfig_visible,
+    kconfig_has_def_nonbool, and kconfig_bool_tristate_options) from kextract.
     """
     kextract = self.get_kextract() # ensure kextract
     if kextract == None:
@@ -523,20 +524,30 @@ def __generate_kextract_summary(self):
     kconfig_types = {}
     kconfig_visible = set()
     kconfig_has_def_nonbool = set()
+    kconfig_bool_tristate_options = set()
     for kconfig_line in kextract.splitlines():
       kconfig_line = kconfig_line.split(" ")
       # see docs/kextract_format.md for more info
       if kconfig_line[0] == "config":
         kconfig_types[kconfig_line[1]] = kconfig_line[2]
+        if kconfig_line[2] in {'bool', 'tristate'}:
+          kconfig_bool_tristate_options.add(kconfig_line[1])
       if kconfig_line[0] == "prompt":
         kconfig_visible.add(kconfig_line[1])
       if kconfig_line[0] == "def_nonbool":
         kconfig_has_def_nonbool.add(kconfig_line[1])
     
+    self.__kconfig_bool_tristate_options = kconfig_bool_tristate_options
     self.__kconfig_types = kconfig_types
     self.__kconfig_visible = kconfig_visible
     self.__kconfig_has_def_nonbool = kconfig_has_def_nonbool
 
+  def get_bool_tristate_options(self):
+    """Get the set of all bool or tristate configuration options.
+    """
+    self.__ensure_kextract_summary()
+    return self.__kconfig_bool_tristate_options
+
   def get_kconfig_types(self):
     """Get the mapping of kconfig symbols to their types extracted from kextract.
     """
@@ -672,6 +683,7 @@ def get_selects(self):
     return self.__selects
 
   def __reset_kextract_summary(self):
+    self.__kconfig_bool_tristate_options=None
     self.__kconfig_types=None
     self.__kconfig_visible=None
     self.__kconfig_has_def_nonbool=None
diff --git a/kmax/common.py b/kmax/common.py
index a4acd20f..c8fec9a7 100644
--- a/kmax/common.py
+++ b/kmax/common.py
@@ -1,10 +1,51 @@
 import sys
 import pickle
 import z3
+import enum
 
 quiet = False
 verbose = False
 
+class VoidLogger:
+  """A quiet logger satisfying the attribute requirements."""
+  def info(self, msg):
+    pass
+  def warning(self, msg):
+    pass
+  def error(self, msg):
+    pass
+  def debug(self, msg):
+    pass
+
+class BasicLogger:
+  """A simple logger."""
+  def __init__(self, quiet=False, verbose=False, flush=True):
+    assert (not (quiet and verbose))
+    self.quiet = quiet
+    self.verbose = verbose
+    self.flush = flush
+  
+  def __flush(self):
+    if self.flush: sys.stderr.flush()
+
+  def info(self, msg):
+    if not self.quiet:
+      sys.stderr.write("INFO: %s" % msg)
+      self.__flush()
+    
+  def warning(self, msg):
+    sys.stderr.write("WARNING: %s" % msg)
+    self.__flush()
+    
+  def error(self, msg):
+    sys.stderr.write("ERROR: %s" % msg)
+    self.__flush()
+    
+  def debug(self, msg):
+    if self.verbose:
+      sys.stderr.write("DEBUG: %s" % msg)
+      self.__flush()
+
 def info(msg, ending="\n"):
   if not quiet: sys.stderr.write("INFO: %s%s" % (msg, ending))
 
@@ -41,3 +82,56 @@ def unpickle_kmax_file(kmax_file):
   with open(kmax_file, 'rb') as fp:
     kmax = pickle.load(fp)
     return kmax
+
+class SourceFileType(enum.Enum):
+  SOURCE = 1 # .c
+  HEADER = 2 # .h
+  MAKEFILE = 3 # Makefile/Kbuild
+  KCONFIG = 4 # Kconfig
+  OTHER = 5 # anything else
+
+  @classmethod
+  def get_file_type(cls, filename: str):
+    assert filename != None
+
+    if filename.endswith('.c'):
+      return SourceFileType.SOURCE
+    elif filename.endswith('.h'):
+      return SourceFileType.HEADER
+    elif filename.startswith("Makefile") or filename.startswith("Kbuild"):
+      return SourceFileType.MAKEFILE
+    elif filename.startswith("Kconfig"):
+      return SourceFileType.KCONFIG
+    else: 
+      return SourceFileType.OTHER
+
+class FileChangeType(enum.Enum):
+	CREATED = 1
+	REMOVED = 2
+	MOVED_ONLY = 3 # file was moved but the content didn't change
+	MOVED_MODIFIED = 4 # file was moved and the content was modified
+	MODIFIED_ONLY = 5 # content was modified but the file wasn't moved
+
+	@classmethod
+	def getType(cls, diff):
+		none_file="/dev/null"
+		assert not (diff.header.old_path == none_file and diff.header.new_path == none_file)
+		
+		if diff.header.old_path == none_file:
+			return FileChangeType.CREATED
+		elif diff.header.new_path == none_file:
+			return FileChangeType.REMOVED
+		elif diff.header.old_path != diff.header.new_path:
+			# filename changed
+			if diff.changes:
+				return FileChangeType.MOVED_MODIFIED
+			else:
+				return FileChangeType.MOVED_ONLY
+		elif diff.header.old_path == diff.header.new_path and diff.changes:
+			return FileChangeType.MODIFIED_ONLY
+		elif "deleted file" in diff.text:
+			# When deleted a file, some patches might have the same file path for
+			# both before and after instead of none_file name. See
+			# e8bf1f522aee3b3e1e7658e8f224dca1d88c3338 for the Linux kernel.
+			return FileChangeType.REMOVED
+		else: assert False # all cases are covered above
diff --git a/kmax/klocalizer b/kmax/klocalizer
index 948958bd..944313cc 100644
--- a/kmax/klocalizer
+++ b/kmax/klocalizer
@@ -3,6 +3,14 @@
 import kmax.kextractcommon
 from kmax.klocalizer import *
 import logging
+from kmax.superc import SuperC, SyntaxAnalysis
+from kmax.vcommon import get_build_system_id
+import json
+from collections import OrderedDict
+from kmax import patch
+import pathlib
+
+z3_true = z3.BoolVal(True)
 
 class BasicLogger:
   def __init__(self, quiet=False, verbose=False):
@@ -34,7 +42,9 @@ def klocalizerCLI():
                         help="""Path to the Linux kernel source directory.  Used to generate kmax, kextract, and kclause formulas as needed.  Also, the defaults for kmax, kextract, and kclause formulas directories/files are relative to this.  Defaults to \"./\"""")
   argparser.add_argument('--formulas',
                          type=str,
-                         help="""Path to the formulas which contain one kmax file for all compilation units and one directory for each architecture containing kclause files.  Defaults to \"LINUX_KSRC/.kmax/\"""")
+                         help="""Path to the formulas which contain one build system subdirectory per unique build systems named with an identifier hash code."""
+                              """  Each directory contains one kmax file for all compilation units, one directory for kclause files, and one directory for superc files."""
+                              """  Defaults to \"LINUX_KSRC/.kmax/\"""")
   argparser.add_argument('--kmax-formulas',
                          type=str,
                          default=None,
@@ -60,6 +70,34 @@ def klocalizerCLI():
                          type=str,
                          default=None,
                          help="""The kextract module version to use for generating kextract formulas.  the latest possible version suitable for the kernel version is detected and used.  Cannot be used with --kextract.  Current default: %s.  All available versions: %s""" % (kmax.kextractcommon.latest_module, ", ".join(kmax.kextractcommon.module_versions.keys())))
+  argparser.add_argument('--include',
+                        action="append",
+                        default=[],
+                        help="Paths to one or more compilation units (.o file) optionally with a list of lines, to include for compilation in ALL output .config files."
+                             "  Path is relative to the top of the source tree."
+                             "  The list of lines may include both single lines and line ranges (inclusive of start-end lines).  List must not contain whitespaces."
+                             "  Examples: kernel/fork.o (only the unit), kernel/fork.o:[5,70-72] (lines 5,70,71,72. No whitespaces in the list)."
+                             "  When a path to a patch file in unified diff format (\".patch\" or \".diff\" extension) is given, "
+                             "klocalizer computes and uses a set of (unit, line) pairs for patch coverage.  The target lines are also written to \"INPUT.kloc_targets\", "
+                             "where INPUT is the path to the diff file.  It is assumed that the patch is applied to the Linux source.")
+  argparser.add_argument('--include-mutex',
+                        action="append",
+                        default=[],
+                        help="Paths to one or more compilation units (.o file) optionally with a list of lines, to include for compilation in the output .config files."
+                             "  Path is relative to the top of the source tree."
+                             "  The option allows coverage to be split in multiple output .config files, accounting for mutual exclusion."
+                             "  For example, two (mutually exclusive) lines from the same unit might get covered in two output .config files, one compiling each line."
+                             "  Despite not guaranteed, the greedy search algorithm aims to cover all constraints with as few .config files as possible."
+                             "  klocalizer does not fail if some of --include-mutex constraints are not met."
+                             "  A coverage report will be generated (see --coverage-report)."
+                             "  Input format is the same with --include.")
+  argparser.add_argument('--exclude',
+                        action="append",
+                        default=[],
+                        help="Paths to one or more compilation units (.o file) optionally with the list of lines, or directories, to exclude from ALL output .config files."
+                             "  Path is relative to the top of the source tree."
+                             "  If a compilation unit is given with a list of lines, either the unit is excluded, or the unit is included and the list of specific lines are excluded."
+                             "  Input format for compilation units and lines is the same with --include.")
   argparser.add_argument('--constraints-file',
                          type=str,
                          help="""A text file containing ad-hoc constraints.  One configuration option name per line.  Prefix with ! to force it off; no prefix means force on.""")
@@ -82,13 +120,18 @@ def klocalizerCLI():
   argparser.add_argument('-o',
                          '--output',
                          type=str,
-                         default=".config",
-                         help="""Name of the output .config file.  Defaults to .config.""")
+                         help="""Name of the output .config file if mutex is disabled (no --include-mutex is specified).  Defaults to .config.  """
+                              """Path to the directory for output configs if mutex is enabled (--include-mutex is used).  Defaults to \"./\"""")
   argparser.add_argument('-m',
                          '--approximate',
                          '--match',
-                         type=str,
-                         help="""An existing .config file to use to try to match as closely as possible while still containing the desired objective.""")
+                         '--repair',
+                         action="append",
+                         default=[],
+                         help="""One or more existing .config file to use to try to match as closely as possible while still containing the desired objective.  """
+                              """Prefix with \"arch_name:\" to specify for a specific architecture.  """
+                              """For example, \"--repair x86_64:1.config --repair arm:2.config --repair others.config\" will use """
+                              """1.config for x86_64,  2.config for arm, and others.config for any other architecture.""")
   argparser.add_argument('--modules',
                          action="store_true",
                          help="""Set tristate options to 'm' instead of 'y' to build as modules instead of built-ins.""")
@@ -96,6 +139,10 @@ def klocalizerCLI():
                          '--show-unsat-core',
                          action="store_true",
                          help="""Show the unsatisfiable core if the formula is unsatisfiable.""")
+  argparser.add_argument('--coverage-report',
+                         type=str,
+                         default="coverage_report.json",
+                         help="""Path to output coverage report file.  Only created if --include-mutex is used.  Only reports the units in --include-mutex.  Defaults to \"coverage_report.json\"""")
   argparser.add_argument('-D',
                          '--define',
                          action="append",
@@ -127,9 +174,6 @@ def klocalizerCLI():
   argparser.add_argument("--save-dimacs",
                          type=str,
                          help="""Save the resulting formula in DIMACS format to the given file.  This option will not create a .config file.""")
-  argparser.add_argument("--exclude-compilation-units",
-                         action="store_true",
-                         help="""Invert the z3 formula of the compilation unit (.o file) when generating .config""")
   argparser.add_argument("--force-unmet-free",
                          action="store_true",
                          help="""Force unmet direct dependency free configuration.  This requires kclause direct depedency formulas file to exist in KMAX_FORMULAS/kclause/ARCH/kclause.normal_dep, which is a pickled dictionary from configuration options to direct dependency formulas.""")
@@ -138,6 +182,44 @@ def klocalizerCLI():
                          nargs="*",
                          default=[],
                          help="""The list of configuration symbols for which allow unmet direct dependency.  Can be used with --force-unmet-free only to relax the constraints for some symbols.""")
+  argparser.add_argument("--superc-linux-script", #< Needed for SuperC config creation
+                         type=str,
+                         help="""Path to the SuperC linux script, which is usually at """
+                              """superc/scripts/superc_linux.sh where superc/ is the """
+                              """top SuperC source directory. Searches \"superc_linux.sh\" in PATH by default.""")
+  argparser.add_argument("--cross-compiler", #< Needed for SuperC config creation
+                         type=str,
+                         default="make.cross",
+                         help="""Path to the executable make script for cross compilation.  """
+                              """It is only executed to create SuperC configuration files.  """
+                              """Otherwise, it appears in the suggested compilation command.  """
+                              """Defaults to \"make.cross\".""")
+  argparser.add_argument("--compile-jobs", #< Used for SuperC config creation
+                         type=int,
+                         default=1,
+                         help="""Number of jobs to allow while compiling units.  """
+                              """It is only used when creating SuperC configuration files.  """
+                              """Infinite if <1.  Defaults to 1.""")
+  argparser.add_argument("--build-targets", #< Needed for SuperC config creation
+                         type=str,
+                         help="""Path to the json file with source file to build target mappings.  """
+                              """Usual case (src/file.c -> src/file.o) is used for missing mappings.  """
+                              """It is only used while creating SuperC configuration files.""")
+  # TODO: allow using different timeouts values for units vs directories
+  argparser.add_argument("--build-timeout", #< Needed for SuperC config creation
+                         type=int,
+                         default=300,
+                         help="""Timeout in seconds for building a single build target.  """
+                              """It is only used while creating SuperC configuration files.  """
+                              """Defaults to 300 (5 minutes).""")
+  argparser.add_argument("--superc-timeout", #< Needed for SuperC config creation
+                         type=int,
+                         default=300,
+                         help="""Timeout in seconds for SuperC source line presence conditions analysis.  """
+                              """Defaults to 300 (5 minutes).""")
+  argparser.add_argument('--werror',
+                         action="store_true",
+                         help="""Make all warnings into errors.  Warnings include kmax and SuperC failures.""")
   argparser.add_argument('-q',
                          '--quiet',
                          action="store_true",
@@ -150,13 +232,10 @@ def klocalizerCLI():
                          action="version",
                          version="%s %s" % (kmax.about.__title__, kmax.about.__version__),
                          help="""Print the version number.""")
-  argparser.add_argument("compilation_units",
-                         nargs='*',
-                         help="The path of the compilation unit (.o file) to generate a .config for, relative to the top of the source tree.")
   args = argparser.parse_args()
   
   linux_ksrc = args.linux_ksrc
-  formulas = args.formulas
+  formulas_arg = args.formulas
   kmax_file = args.kmax_formulas
   kclause_file = args.kclause_formulas
   disable_downloading_formulas = args.disable_downloading_formulas
@@ -166,12 +245,18 @@ def klocalizerCLI():
   archs_arg = args.arch
   allarchs = args.all
   reportallarchs = args.report_all
+  include_arg = args.include
+  include_mutex_arg = args.include_mutex
+  exclude_arg = args.exclude
   constraints_file = args.constraints_file
   constraints_file_smt2 = args.constraints_file_smt2
-  output_file = args.output
+  # Both mutex and non-mutex use --output for output file or dir
+  output_file = args.output if args.output else ".config"
+  output_dir = args.output if args.output else "./"
   show_unsat_core = args.show_unsat_core
   approximate = args.approximate
   modules_arg = args.modules
+  coverage_report_file = args.coverage_report
   define = args.define
   undefine = args.undefine
   disable_config_broken = not args.allow_config_broken
@@ -182,79 +267,280 @@ def klocalizerCLI():
   sample_prefix = args.sample_prefix
   random_seed = args.random_seed
   save_dimacs = args.save_dimacs
-  compilation_units = args.compilation_units
-  dont_compile = args.exclude_compilation_units
   force_unmet_free = args.force_unmet_free
   allow_unmet_for = args.allow_unmet_for
+  superc_linux_script = args.superc_linux_script
+  cross_compiler = args.cross_compiler
+  build_targets_file = args.build_targets
+  compile_jobs = args.compile_jobs
+  build_timeout = args.build_timeout
+  superc_timeout = args.superc_timeout
+  werror = args.werror
   quiet = args.quiet
   verbose = args.verbose
 
   kmax.common.quiet = quiet
   kmax.common.verbose = verbose
   logger = BasicLogger(quiet=quiet, verbose=verbose)
+
+  def warn_or_err(warn_msg, err_msg, exit_code):
+    """Takes action on warnings.  Behavior is different based on whether
+    --werror or not.
+    
+    If werror, prints err_msg on error channel and terminates with
+    exit_code.  Otherwise, prints warn_msg on warning channel and returns.
+    """
+    if werror:
+      logger.error(err_msg)
+      exit(exit_code)
+    else:
+      logger.warning(warn_msg)
+  
+  exit_code_superc_config_creation_failed = 27
+  exit_code_superc_sourcelinepc_failed = 28
+    
+  sys.stderr.write("klocalizer, %s %s\n" % (kmax.about.__title__, kmax.about.__version__))
+
+  def unit2srcfile(unit):
+    assert unit.endswith('.o')
+    return unit[:-len('.o')] + '.c'
+  def srcfile2unit(srcfile):
+    assert srcfile.endswith('.c')
+    return srcfile[:-len('.c')] + '.o'
+  
+  def get_exclusion_constraints(unit_constraints, line_constraints):
+    # Exclusion means none of the lines are built
+    lines_not_built = z3.And([z3.Not(line_constraints)])
+    # Either the unit is not built, or the unit is built without any of the lines
+    unit_not_built = z3.Not(z3.And(unit_constraints))
+    return z3.Or([unit_not_built, lines_not_built])
+
+  # The extension for the json file that contain { file: [lines] }, which
+  # can be used as input to klocalizer.
+  kloc_targets_ext = ".kloc_targets"
+
+  def get_patch_target_lines(patch_file_path: str):
+    # Compute the klocalizer targets from patch file
+    logger.debug("Computing the target lines from the patch file \"%s\"\n" % patch_file_path)
+    with open(patch_file_path, 'r') as f:
+      patch_txt = f.read()
+    r = patch.get_target_c_lines(patch_txt)
+
+    # Turn .c extensions into .o extensions and do additional checks on lines
+    for fpath in list(r.keys()):
+      newpath = srcfile2unit(fpath)
+      r[newpath] = sorted(list(set(r[fpath])))
+      for l in r[newpath]:
+        assert l > 0
+      del r[fpath]
+
+    # Write the klocalizer targets (for diagnostic purposes)
+    kloc_targets_filepath = patch_file_path + kloc_targets_ext
+    logger.debug("Writing the patch target c lines to \"%s\"\n" % kloc_targets_filepath)
+    with open(kloc_targets_filepath, 'w') as f:
+      json.dump(r, f)
+
+    # Return the kloc targets 
+    return r
+
+  def parse_lines_list(compilation_unit_arg : str):
+    """Given compilation unit arg, parse and return the compilation unit
+    and the list of lines, or the directory path. Returned list of lines
+    are unique and sorted.
+
+    Returned compilation unit names are guaranteed to end with '.o' extension.
+
+    Returned directory paths are guaranteed to end with '/' suffix.
+
+    Example input/outputs:
+    == Input ==                    == Output ==
+    "kernel/fork.o"                ("kernel/fork.o", [])
+    "kernel/fork.c"                ("kernel/fork.o", []) ('.c' -> '.o')
+    "kernel/fork.o:[]"             ("kernel/fork.o", [])
+    "kernel/fork.o:[5,7,10]"       ("kernel/fork.o", [5,7,10])
+    "kernel/fork.o:[10-10]"        ("kernel/fork.o", [10])
+    "kernel/fork.o:[5,7-10]"       ("kernel/fork.o", [5,7,8,9,10])
+    "kernel"                       ("kernel/", [])
+    "kernel/"                      ("kernel/", [])
+    "kernel/power/"                ("kernel/power/", [])
+    "kernel/power:[]"              Prints error and terminates
+    "kernel/fork.o:[10-7]"         Prints error and terminates
+    "kernel/fork.o:[10,"           Prints error and terminates
+    """
+    assert compilation_unit_arg
+    def arg_error(arg: str, problem: str):
+      argparser.print_help()
+      logger.error("Malformed compilation unit or directory argument (\"%s\"): %s\n" % (arg, problem))
+      exit(12)
+
+    #
+    # Split the unit path and the lines list
+    #
+    split_arg = compilation_unit_arg.split(':')
+    assert len(split_arg) > 0
+    if len(split_arg) == 1:
+      unit_str = split_arg[0]
+      lines_str = None
+    elif len(split_arg) == 2:
+      unit_str, lines_str = split_arg
+      if len(lines_str) < 2: # must at least have '[' and ']'
+        arg_error(compilation_unit_arg, "incorrect lines list format.")
+    elif len(split_arg) > 2:
+      arg_error(compilation_unit_arg, "\":\" must be used at most once to between the unit path and the lines list.")
+
+    #
+    # Check and parse if directory
+    #
+    ext = os.path.splitext(unit_str)[-1]
+    if not ext: # directory
+      if lines_str:
+        arg_error(compilation_unit_arg, "lines cannot be specified for directory paths.")
+      if unit_str.endswith('/'):
+        return unit_str, []
+      else: # Add the '/' suffix
+        return unit_str + '/', []
+
+    #
+    # Check and parse the unit path into unit_str
+    #
+    if not unit_str.endswith('.c') and not unit_str.endswith('.o'):
+      arg_error(compilation_unit_arg, "unit must have \".c\" or \".o\" extension.")
+
+    # Force extension to be .o
+    if not unit_str.endswith('.o'):
+      logger.warning("Forcing file extension to be .o, since lookup is by compilation unit: \"%s\"\n" % (unit_str))
+      unit_str = "%s.o" % unit_str[:-len('.c')]
+
+    #
+    # Check and parse the lines list into lines_list
+    #
+    lines_list = []
+    if lines_str:
+      # Check line list
+      if not lines_str.startswith('[') or not lines_str.endswith(']'):
+        arg_error(compilation_unit_arg, "incorrect lines list format.")
+      assert len(lines_str) > 1 #< Has '[' and ']'
+      lines_str = lines_str[1:-1]
+
+      def parse_pos_int(num_str : str) -> int:
+        if not num_str or not set(num_str).issubset([str(n) for n in range(10)]):
+          arg_error(compilation_unit_arg, "incorrect lines list format.")
+        else:
+          num = int(num_str)
+          if num <= 0:
+            arg_error(compilation_unit_arg, "lines are 1-indexed and must be greater than 0.")
+          else:
+            return num
+
+      # Parse the lines
+      if lines_str: #< Still has lines to parse after removing list brackets
+        for el in lines_str.split(','):
+          if not el or not set(el).issubset([str(n) for n in range(10)] + ['-']):
+            arg_error(compilation_unit_arg, "incorrect lines list format")
+          if el.count('-') > 1:
+            arg_error(compilation_unit_arg, "incorrect lines list format")
+          
+          if '-' in el: #< Range
+            start, end = el.split('-')
+            start, end = parse_pos_int(start), parse_pos_int(end)
+            if end < start:
+              arg_error(compilation_unit_arg, "end of line range cannot be smaller than the start")
+            lines_list.extend(range(start, end+1))
+          else:         #< Single line
+            lines_list.append(parse_pos_int(el))
+
+      # Sort and make sure each line is unique.
+      lines_list = sorted(list(set(lines_list)))
+
+    return unit_str, lines_list
+
+  def parse_units_args(args):
+    def is_patch_input(a):
+      return a.endswith(".patch") or a.endswith(".diff")    
+    parsed_list = []
+    for a in args:
+      if is_patch_input(a):
+        logger.info("Diff file was given as input (\"%s\"): assuming it was applied to the Linux source.\n" % a)
+        parsed_list.extend(list(get_patch_target_lines(a).items()))
+      else:
+        parsed_list.append(parse_lines_list(a))
+
+    # Have one entry per unique unit, all sorted.
+    uniq_compilation_units_lines = {}
+    for unit, lines in parsed_list:
+      if lines is None:
+        lines = []
+      existing_lines = uniq_compilation_units_lines.get(unit, [])
+      new_lines = sorted(list(set(existing_lines + lines)))
+      uniq_compilation_units_lines[unit] = new_lines
+    return sorted(list(uniq_compilation_units_lines.items()))
+
+  # Parse units/lines.
+  include_list = parse_units_args(include_arg)
+  include_mutex_list = parse_units_args(include_mutex_arg)
+  exclude_list = parse_units_args(exclude_arg)
+  # Make a copy of the original list since the lists will get simplified
+  # along the way, and we will need the original list for coverage reports.
+  original_include_mutex_list = include_mutex_list[:]
+
+  # Determines whether kmax will be run.
+  has_file_constraints = len(include_list + include_mutex_list + exclude_list) > 0
+  all_comp_units_list = include_list + include_mutex_list + exclude_list
+
   klocalizer.set_logger(logger)
 
   klocalizer.set_linux_krsc(linux_ksrc)
 
-  # set default value for formulas if not specified
-  if not formulas:
-    # try to determine the version of the linux source code
-    # first try git
-    command=["git", "describe", "--abbrev=0", "--tags"]
-    popen = subprocess.Popen(command, stdin=None, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
-    linux_tag_version, _ = popen.communicate()
-    linux_tag_version = linux_tag_version.strip().decode('utf-8')
-    if popen.returncode == 0:
-      # successfully found linux version git
-      pass
-    else:
-      # apparently not a git repository, so try with make kernelversion
-      command=["make", "kernelversion"]
-      popen = subprocess.Popen(command, stdin=None, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
-      linux_tag_version, _ = popen.communicate()
-      linux_tag_version = linux_tag_version.strip().decode('utf-8')
-      if popen.returncode == 0:
-        # successfully found linux version from make
-        pass
+  #
+  # Formulas directory
+  #
+  # Set default value for formulas if not specified
+  if not formulas_arg:
+    formulas_arg = os.path.join(linux_ksrc, ".kmax/")
+
+  # Get the build system id, which names the formulas cache subdirectory
+  logger.debug("Computing the build system id for the Linux source..\n")
+  build_system_id = get_build_system_id(linux_ksrc) # takes about 4sec on an SSD
+  logger.debug("Build system id: %s\n" % build_system_id)
+  formulas = os.path.join(formulas_arg, build_system_id)
+
+  # Try downloading a cached version if formulas are not available
+  if not disable_downloading_formulas:
+    # Is formulas empty: dir doesn't exist or dir is empty
+    is_formulas_empty = (not os.path.exists(formulas)) or (not os.listdir(formulas))
+    if is_formulas_empty:
+      # get cache index; if we can't, then fatal error
+      link = Klocalizer.get_kclause_cache_url(build_system_id)
+      # lookup version in the cache; if we can't, then tell user it's not available
+      import requests
+      req = requests.get(link)
+      logger.debug("Looking up cache index: %s\n" % (link))
+      if req.status_code == 200:
+        url_to_cached_formulas = (req.text if req.encoding is None else req.text.decode(req.encoding)).strip()
+        logger.info("Found cached formulas for %s.  Downloading...\n" % (build_system_id))
+        # download from the url; if we can't, then error
+        import shutil
+        local_filename = url_to_cached_formulas.split('/')[-1]
+        with requests.get(url_to_cached_formulas, stream=True) as r:
+            with open(local_filename, 'wb') as f:
+              shutil.copyfileobj(r.raw, f)
+        # untar; if we can't, then error
+        import tarfile
+        logger.info("Unpacking %s...\n" % (local_filename))
+        with tarfile.open(local_filename) as t:
+          t.extractall(formulas)
+          t.close()
+        logger.debug("Removing downloaded cache file %s\n" % (local_filename))
+        os.remove(local_filename)
       else:
-        # could not get any linux_tag_version
-        linux_tag_version = None
-    assert(type(linux_tag_version) == str or linux_tag_version is None)
-    if linux_tag_version is None:
-      # provide a hard-coded version name since we couldn't determine the version
-      formulas = os.path.join(linux_ksrc, ".kmax/", "_unknown_version")
+        logger.warning("No cached formulas for %s available for download :(\n" % (build_system_id))
     else:
-      # set the formula folder based on the linux version
-      formulas = os.path.join(linux_ksrc, ".kmax/", linux_tag_version)
-
-      # try downloading a cached version if user hasn't already started generating formulas
-      if not disable_downloading_formulas and not os.path.exists(formulas):
-        # get cache index; if we can't, then fatal error
-        link = Klocalizer.get_kclause_cache_url(linux_tag_version)
-        # lookup version in the cache; if we can't, then tell user it's not available
-        import requests
-        req = requests.get(link)
-        logger.debug("Looking up cache index: %s\n" % (link))
-        if req.status_code == 200:
-          url_to_cached_formulas = (req.text if req.encoding is None else req.text.decode(req.encoding)).strip()
-          logger.info("Found cached formulas for %s.  Downloading...\n" % (linux_tag_version))
-          # download from the url; if we can't, then error
-          import shutil
-          local_filename = url_to_cached_formulas.split('/')[-1]
-          with requests.get(url_to_cached_formulas, stream=True) as r:
-              with open(local_filename, 'wb') as f:
-                shutil.copyfileobj(r.raw, f)
-          # untar; if we can't, then error
-          import tarfile
-          logger.info("Unpacking %s...\n" % (local_filename))
-          with tarfile.open(local_filename) as t:
-            t.extractall(formulas)
-            t.close()
-          logger.debug("Removing downloaded cache file %s\n" % (local_filename))
-          os.remove(local_filename)
-        else:
-          logger.warning("No cached formulas for %s available for download :(\n" % (linux_tag_version))
-  
+      # formulas directory exists and not empty: no need to download
+      pass
+  else:
+    # user disabled downloading formulas: compute them as needed
+    pass
+
   # flatten allow_unmet_for list of lists
   allow_unmet_for = [ item for elem in allow_unmet_for for item in elem ]
 
@@ -294,6 +580,25 @@ def klocalizerCLI():
     logger.error("Cannot use --all-architectures when providing explicit --arch arguments.\n")
     exit(12)
 
+  mutual_exclusion_str = "--include-mutex"
+  mutex_enabled = len(include_mutex_arg) > 0
+  if mutex_enabled:
+    if allarchs:
+      logger.error("%s is incompatible with --all.\n" % mutual_exclusion_str)
+      exit(12)
+    if reportallarchs:
+      logger.error("%s is incompatible with --report-all.\n" % mutual_exclusion_str)
+      exit(12)
+    if show_unsat_core:
+      logger.error("%s is incompatible with --show-unsat-core.\n" % mutual_exclusion_str)
+      exit(12)
+    if view_kbuild:
+      logger.error("%s is incompatible with --view-kbuild.\n" % mutual_exclusion_str)
+      exit(12)
+    if save_dimacs:
+      logger.error("%s is incompatible with --save-dimacs.\n" % mutual_exclusion_str)
+      exit(12)
+    
   if save_dimacs:
     if os.path.exists(save_dimacs):
       logger.warning("Overwriting existing file with the DIMACS output: %s\n" % (save_dimacs))
@@ -306,7 +611,7 @@ def klocalizerCLI():
   if sample is not None:
     if sample_prefix is None:
       sample_prefix="config"
-    if approximate is not None:
+    if approximate:
       argparser.print_help()
       logger.error("--approximate and --sample cannot currently be used together\n")
       exit(12)
@@ -329,14 +634,69 @@ def klocalizerCLI():
     # or couldn't be downloaded
     os.makedirs(formulas)
 
-  if approximate and not os.path.isfile(approximate):
-    logger.error("Cannot find config file to approximate: %s\n" % approximate)
+  # Parse and check the config file paths to approximate
+  # {arch_name : config_file_path}. "default" is the special key, has value
+  # to default config file to approximate without arch specified.
+  approximate_configs = {} 
+  if approximate:
+    for s in approximate:
+      #
+      # Set apprx_arch_name and apprx_config_file_path
+      #
+      if len(s.split(":")) > 1: #< for a specific architecture.
+        apprx_arch_name = s.split(':')[0]
+        apprx_config_file_path = "".join(s.split(':')[1:])
+        if not apprx_arch_name:
+          logger.error("Empty architecture name for approximate config: %s\n" % s)
+          exit(6)
+        if apprx_arch_name in approximate_configs:
+          logger.error("Multiple .config files specified to approximate for an architecture: %s\n" % apprx_arch_name)
+          exit(12)
+      else: #< default
+        apprx_arch_name = "default"
+        apprx_config_file_path = s
+        if apprx_arch_name in approximate_configs:
+          logger.error("Multiple .config files as default .config to approximate.\n")
+          exit(12)
+
+      #
+      # Record the .config to approximate
+      #
+      if not os.path.isfile(apprx_config_file_path):
+        logger.error("Cannot find config file to approximate: %s\n" % apprx_config_file_path)
+        exit(6)
+      assert apprx_arch_name not in approximate_configs
+      approximate_configs[apprx_arch_name] = apprx_config_file_path
+    logger.debug("Approximate configs: %s\n" % approximate_configs)
+
+  if build_targets_file and not os.path.isfile(build_targets_file):
+    logger.error("Cannot find build targets file: %s\n" % build_targets_file)
     exit(6)
+  
+  if build_timeout <= 0:
+    logger.error("--build-timeout must be greater than 0.\n")
+    exit(12)
+
+  if superc_timeout <= 0:
+    logger.error("--superc-timeout must be greater than 0.\n")
+    exit(12)
+
+  if mutex_enabled and view_kbuild:
+    logger.error("%s cannot be used with --view-kbuild.\n" % mutual_exclusion_str)
+    exit(12)
+
+  #
+  # Load build targets
+  #
+  build_targets = {}
+  if build_targets_file:
+    with open(build_targets_file, 'r') as f:
+      build_targets = json.load(f)
 
   #
   # Set kmax file
   #
-  if len(compilation_units) > 0:
+  if has_file_constraints:
     # logger.info("Getting the compilation unit constraints via kmax\n")
     if not kmax_file:
       kmax_file = os.path.join(formulas, "kmax") # default kmax file
@@ -352,26 +712,157 @@ def klocalizerCLI():
       is_kmax_cache = False
 
   #
-  # Check compilation units' names
+  # Simplify line requirements through syntax analysis.
   #
-  for i, unit in enumerate(compilation_units):
-    if not unit.endswith(".o"):
-      logger.warning("Forcing file extension to be .o, since lookup is by compilation unit: %s\n" % (unit))
-      unit = os.path.splitext(unit)[0] + ".o"
-      compilation_units[i] = unit
+  # If a line is unconstrained by syntax (not under any conditional
+  # preprocessor directive, remove it from the list. Localizing for the unit
+  # will suffice to build the line. This may help avoid running SuperC for
+  # this file if no lines remain. Syntax analysis is faster and precise;
+  # therefore, this will improve performance.
+  global_scope_lines = {} # { unit : set(int) }, lines outside any ifdefs
+  for target_list in [include_list, include_mutex_list, exclude_list]:
+    for i, (unit, line_list) in enumerate(target_list):
+      if line_list:
+        srcfile = unit2srcfile(unit)
+        srcfile_fullpath = os.path.join(linux_ksrc, srcfile)
+        assert os.path.isfile(srcfile_fullpath)
+        logger.debug("Doing syntax analysis on \"%s\" to get constrained line ranges.\n" % srcfile)
+        
+        root_cb = SyntaxAnalysis.get_conditional_blocks_of_file(srcfile_fullpath)
+
+        # Check if given line list is valid for the file.
+        line_count = root_cb.end_line - 1 #< Root (dummy) ConditionalBlock has special end_line value.
+        for l in line_list:
+          if not 0 < l <= line_count:
+            logger.error("Requested line (%s) is invalid for the source file (\"%s\")\n" % (l, srcfile))
+            exit(12)
+
+        # Get the ConditionalBlock that cover the requested lines.
+        nodes = [root_cb.retrieve_deepest_block(l) for l in line_list]
+        assert len(nodes) == len(line_list)
+        # Get the constrained lines only (those that don't belong to dummy root)
+        # Unconstrained lines will already build with the file.
+        new_line_list = []
+        for l, n in zip(line_list, nodes):
+          if n == root_cb:
+            global_scope_lines[unit] = global_scope_lines.get(unit, set()).union([l])
+          else:
+            new_line_list.append(l)
+        removed_lines = len(line_list) - len(new_line_list)
+        assert removed_lines >= 0
+        logger.debug(
+          """Syntax analysis for \"%s\" found %s unconstrained lines, """
+          """%s lines are remaining for presence condition analysis.\n"""
+          """""" % (srcfile, removed_lines, len(new_line_list)))
+        target_list[i] = unit, new_line_list
+  
+  # Determines whether SuperC is needed. This is done after simplification
+  # through syntax analysis since the simplification can discard line
+  # requirements by reducing them to file inclusion.
+  has_line_constraints = len([u for u, l in include_list + include_mutex_list + exclude_list if l]) > 0
 
   #
-  # Add the compilation units
+  # SuperC: ensure configs and get presence conditions for a "srcfile" under an "arch"
   #
-  for unit in compilation_units:
-    if dont_compile:
-      klocalizer.exclude_compilation_unit(unit)
-    else:
-      klocalizer.include_compilation_unit(unit)
+  line_constraints = {} # { srcfile (.c): { arch_name: ConditionalBlock } }
+  for unit, lines in all_comp_units_list: # initialize
+    if not unit.endswith('/'):
+      line_constraints[unit2srcfile(unit)] = {}
+  # This function uses values from global scope (linux ksrc, formulas dir, etc.)
+  # but parametrizes the operation into srcfile and architecture.
+  def get_presence_conditions(srcfile, arch):
+    """Ensures SuperC configs for srcfile and computes the line presence
+    conditions.
+    
+    Returns an instance of ConditionalBlock on success.
+    Returns None on error.
+
+    Retrieves from or fills the cache (line_constraints).
+    """
+    assert srcfile.endswith('.c')
+    # Check the cache.
+    if srcfile in line_constraints and arch.name in line_constraints[srcfile]:
+      return line_constraints[srcfile][arch.name]
+    
+    if srcfile not in line_constraints:
+      line_constraints[srcfile] = {}
+
+    #
+    # Make sure SuperC configs exist.
+    #
+    logger.info("Computing line presence conditions for \"%s\"\n" % srcfile)
+    superc_formulas_dir = SuperC.get_superc_formulas_dir(formulas, arch.name)
+    config_exists = superc.ensure_superc_config(srcfile, superc_formulas_dir, linux_ksrc, arch, cross_compiler, build_targets, compile_jobs, build_timeout, logger)
+    if not config_exists:
+      logger.debug("Failed to find/create SuperC config file for \"%s\"\n" % srcfile)
+      error_msg = "Failed to compute line presence conditions for \"%s\": SuperC config generation error\n" % srcfile
+      line_constraints[srcfile][arch.name] = None # Special value, depicts failure.
+      warn_or_err(error_msg, error_msg, exit_code_superc_config_creation_failed)
+      return None
+    else: # config exists
+      logger.debug("SuperC config file was found for \"%s\"\n" % srcfile)
+      logger.debug("Computing the presence conditions for \"%s\"\n" % srcfile)
+
+      #
+      # Get presence conditions, thus, line constraints
+      #
+      # Map source files to presence conditions (ConditionalBlock instances)
+      logger.debug("Computing presence conditions for \"%s\".\n" % srcfile)
+      cb = superc.get_pc(srcfile, arch, linux_ksrc, superc_formulas_dir, superc_timeout, logger)
+      if not cb:
+        logger.debug("Computing presence conditions failed for \"%s\"\n" % srcfile)
+        error_msg = "Failed to compute line presence conditions for \"%s\": SuperC sourcelinePC error\n" % srcfile
+        line_constraints[srcfile][arch.name] = None # Special value, depicts failure.
+        warn_or_err(error_msg, error_msg, exit_code_superc_sourcelinepc_failed)
+        return None
+      else: # pc was successfully computed
+        logger.debug("Computed presence conditions for \"%s\"\n" % srcfile)
+        line_constraints[srcfile][arch.name] = cb
+        return cb
+
+  #
+  # Compute kmax constraints
+  #
+  kmax_constraints = {} # { unit: [kmax_constraints] }, None value means failed
+  def compute_kmax_constraints(unit):
+    try:
+      kmax_constraints[unit] = klocalizer.get_compilation_unit_constraints(unit)
+    except Klocalizer.NoFormulaFoundForCompilationUnit as e:
+      error_msg = "No formula from kmax was found for the compilation unit: %s\n" % (e.unit)
+      warn_or_err(error_msg, error_msg, 3)
+      kmax_constraints[unit] = None
+    except Klocalizer.MultipleCompilationUnitsMatch as e:
+      error_msg = "There are multiple compilation units that match %s.  Please provide one of the Kbuild paths from below:\n%s\n" % (e.unit, "\n".join(e.matching_units))
+      warn_or_err(error_msg, error_msg, 4)
+      kmax_constraints[unit] = None
+    return kmax_constraints[unit]
+
+  # Precompute all
+  for unit, lines in all_comp_units_list:
+    compute_kmax_constraints(unit)
+
+  #
+  # Include or exclude units
+  #
+  for unit, lines in include_list:
+    if kmax_constraints[unit] is not None: #< None is failure.
+      klocalizer.add_constraints(kmax_constraints[unit])
+
+  for unit, lines in exclude_list:
+    if not lines:
+      if kmax_constraints[unit] is not None: #< None is failure.
+        constraints = kmax_constraints[unit]
+        if not constraints:
+          logger.error("The unit/directory to exclude (\"%s\") is unconstrained: no satisfying configuration is possible.\n" % unit)
+          exit(11)
+        klocalizer.add_constraints([z3.Not(z3.And(constraints))])
+    else: # has lines
+      # This is handled when the line conditions are computed.
+      pass
   
   if view_kbuild:
-    if len(compilation_units) > 0:
-      for unit in compilation_units:
+    if len(all_comp_units_list) > 0:
+      for unit, _ in all_comp_units_list:
         logger.info("The Kbuild constraints for %s:\n" % (unit))
         get_kmax_constraints(klocalizer.get_kmax_formulas(), unit, view=True)
       exit(0)
@@ -382,7 +873,7 @@ def klocalizerCLI():
   #
   # Update the kmax cache (now that we are done with generating new kmax formulas)
   #
-  if len(compilation_units) > 0 and is_kmax_cache:
+  if len(all_comp_units_list) > 0 and is_kmax_cache:
     logger.debug("Updating Kmax formulas cache file: %s\n" % kmax_cache_file)
     klocalizer.update_kmax_cache_file(kmax_cache_file)
     logger.debug("Kmax formulas cache file was updated.\n")
@@ -418,8 +909,8 @@ def klocalizerCLI():
   #
   # Filter archs based on unit name
   #
-  if not kclause_file:
-    for unit in compilation_units:
+  if not kclause_file :
+    for unit, _ in include_list:
       if unit.startswith("arch/"):
         unit_archs = Arch.get_archs_from_subdir(unit)
         archs = [ arch for arch in archs if arch.name in unit_archs ]
@@ -487,19 +978,518 @@ def klocalizerCLI():
   #
   # Get the approximate constraints
   #
-  approximate_constraints=None
-  if approximate:
-    approximate_constraints=Klocalizer.get_config_file_constraints(approximate)
-  
+  approximate_constraints={}
+  for arch_name in approximate_configs:
+    apprx_config_file_path = approximate_configs[arch_name]
+    approximate_constraints[arch_name]=Klocalizer.get_config_file_constraints(apprx_config_file_path)
+
+  # Check if there are line constraints, which will require a SuperC instance.
+  if has_line_constraints:
+    try:
+      superc = SuperC(superc_linux_script_path=superc_linux_script, logger = logger)
+    except SuperC.SuperC_ChecksFailed as e:
+      # TODO: if superc checks fail and werror is disabled, let SuperC
+      # methods still return something for calls to superc
+
+      # Pass this to the main func to terminate until allowing klocalizer
+      # to work without SuperC
+      raise e 
+
+      # prefix  = "SuperC checks failed, reason: %s." % e.reason
+      # warn_msg = "%s.  Search will exclude line presence constraints.\n" % prefix
+      # err_msg = "%s.  Either fix the issue or omit the line requirements.\n" % prefix
+      # warn_or_err(warn_msg, err_msg, exit_code_superc_checks_failed)
+
   # Everything is set. Continue with SAT checking and config sample generation.
   seen_unsat = False # to prevent logging some info multiple times for unsat cases
   sat_archs = []
+
+  #
+  # Algo 1: mutex enabled
+  #
+  if mutex_enabled:
+    # Initialize the requirements, which will be consumed and updated.
+    requirements = include_mutex_list[:]
+    # Use 0 as the special line number, which depicts the global scope 
+    # (only the file itself). Always target to compile the file in case
+    # specific lines fail and no werror.
+    requirements = [(u, [0] + l) for u, l in requirements]
+    # Don't include units without kmax constraints (failures).
+    requirements = [(u, l) for u, l in requirements if kmax_constraints[u] is not None]
+
+    # TODO: if an arch only compiles the file, and another arch compiles
+    # both the file and the line, we keep both configs. However, we can
+    # later remove the arch that only compiles the file, since the other
+    # one outperforms it.
+
+    # Save the covering improving z3 models, from which config files will be sampled.
+    z3_models = [] # (arch, z3_model, [(unit:line)]) tuples
+
+    # The architecture is only updated if the coverage is no longer improved
+    # by the current architecture. This means, we can do several iterations
+    # on the same architecture to account for mutually exclusive configurations.
+    arch_idx = 0
+    printed_arch_info = False
+    got_first_improvement = False
+    while arch_idx < len(archs) and requirements:
+      # Assign the architecture to work with.
+      arch = archs[arch_idx]
+
+      if not printed_arch_info:
+        logger.info("Trying \"%s\"\n" % (arch.name))
+        printed_arch_info = True
+
+      # This will be only compiled later if a SAT check is necessary.
+      compiled_arch_constraints = None
+
+      #
+      # Compute presence conditions for the architecture.
+      #
+      # This will only happen in the first try of the architecture since
+      # we set values to line_constraints[unit] for every unit, even if
+      # it is failure (None depicts failure).
+      units_to_compute_pc = []
+      for unit, lines in requirements:
+        if lines == [0]:
+          # 0 is the special line number, depicting the global scope.
+          # If 0 is the only required line, it means no specific lines are
+          # required to be compiled but only the file. Therefore, presence
+          # conditions are not required.
+          pass
+        elif arch.name not in line_constraints[unit2srcfile(unit)]:
+          units_to_compute_pc.append(unit)
+      # Also for the units with always include/excludes
+      units_to_compute_pc.extend([unit for unit, lines in (include_list + exclude_list) if lines])
+      units_to_compute_pc = [u for u in units_to_compute_pc if not u.endswith('/')] # exclude directories
+      units_to_compute_pc = sorted(list(set(units_to_compute_pc)))
+      if units_to_compute_pc:
+        logger.info("Computing the line presence conditions under %s for the following units: %s\n" % (arch.name, " ".join(units_to_compute_pc)))
+      for unit in units_to_compute_pc:
+        get_presence_conditions(unit2srcfile(unit), arch)
+
+      # Presence conditions are computed.
+
+      # Accumulate constraints for the config file. This will hold file and
+      # line constraints. At the end, if there is an improvement to coverage
+      # with such satisfiable constraints, a config file will be sampled
+      # from these constraints.
+      accumulated_constraints = []
+
+      #
+      # Add the constraints for "include" lines
+      #
+      # This needs to be done here since line constraints may be specific
+      # to architecture in constrast to Makefile constraints.
+      logger.debug("Adding the constraints for \"include\" lines.\n")
+      for unit, lines in include_list:
+        if lines and lines != [0]:
+          srcfile = unit2srcfile(unit)
+          if line_constraints[srcfile][arch.name] is not None: # None is SuperC failure.
+            pc_blocks = line_constraints[srcfile][arch.name].get_deepest_blocks(lines)
+            for pcb in pc_blocks:
+              accumulated_constraints.extend(pcb.pc.assertions())
+      #
+      # Add the constraints for "exclude" lines
+      #
+      # This needs to be done here since line constraints may be specific
+      # to architecture in constrast to Makefile constraints.
+      logger.debug("Adding the constraints for \"exclude\" lines.\n")
+      for unit, lines in exclude_list:
+        if not lines:
+          pass # Already handled
+        else: # has lines
+          # Get the line constraints
+          unit_line_c = []
+          srcfile = unit2srcfile(unit)
+          if line_constraints[srcfile][arch.name] is not None: # None is SuperC failure.
+            pc_blocks = line_constraints[srcfile][arch.name].get_deepest_blocks(lines)
+            for pcb in pc_blocks:
+              unit_line_c.extend(pcb.pc.assertions())
+          # Get kmax constraints
+          unit_kmax_c = kmax_constraints[unit]
+          unit_kmax_c = unit_kmax_c if unit_kmax_c else []
+          # Get exclusion constraints
+          c = get_exclusion_constraints(unit_kmax_c, unit_line_c)
+          accumulated_constraints.extend(c)
+    
+      # Keep track of whether there is an improvement found to the coverage
+      # with the accumulated constraints. If not, loop will continue with
+      # the next architecture. Otherwise, the loop will give this arch
+      # another chance since there can be mutually exclusive lines to cover
+      # in the next iteration.
+      is_improved = False
+
+      # A dict of (file:[lines]) covered by the current model being
+      # built. This will be used for reporting purposes. This is empty if
+      # is_improved is False, otherwise non-empty.
+      current_coverage = {}
+
+      # This is the updated requirements, which excludes what is covered
+      # in this iteration. At the end of the iteration, this will replace
+      # the previous requirements.
+      new_requirements = []
+
+      # Visit requirements.
+      if not got_first_improvement:
+        logger.info("Searching for a constraints model that cover all or part of the constraints\n")
+      else:
+        logger.info("Searching for a constraints model that cover all or part of the remaining constraints\n")
+      for unit, lines in requirements:
+        remaining_lines = [] #< Remaining lines to cover for the unit.
+
+        # Check if arch is good for the unit
+        if unit.startswith("arch/") and not kclause_file:
+          unit_archs = Arch.get_archs_from_subdir(unit)
+          if arch.name not in unit_archs:
+            logger.debug("Skipping the unit (\"%s\") for this architecture (\"%s\") as the unit is architecture specific.\n" % (unit, arch.name))
+            new_requirements.append((unit, lines))
+            continue
+
+        # Add the Makefile constraints.
+        assert kmax_constraints[unit] is not None
+        constraints_with_file = accumulated_constraints + kmax_constraints[unit]
+
+        # Map lines into ConditionalBlocks.
+        line_to_cb = {} # key: int line number, value: ConditionalBlock instance.
+        # arch.name key exists if line_constraints were needed
+        # the value for line_constraints[unit][arch.name] is None if SuperC failed
+        if not unit.endswith('/'):
+          if arch.name in line_constraints[unit2srcfile(unit)] and line_constraints[unit2srcfile(unit)][arch.name] is not None:
+            root_cb = line_constraints[unit2srcfile(unit)][arch.name]
+            for line in lines:
+              line_to_cb[line] = root_cb.get_deepest_block(line)
+        
+        # Keep track of covered blocks. Different lines may point to the
+        # same block. This allows avoiding additional SAT checks for
+        # duplicate blocks.
+        covered_blocks = set()
+        cant_cover_blocks = set()
+
+        # Check for each line.
+        for line in lines:
+          logger.debug("Working on (%s:%s)\n" % (unit, line))
+          
+          #
+          # Get the line constraints
+          #
+          if line != 0 and line_constraints[unit2srcfile(unit)][arch.name] is None:
+            # A specific line is required, for which the pc does not exist.
+            # Therefore, nothing to do for this.
+            remaining_lines.append(line)
+            continue
+          elif line == 0: #< Special line number: compile file only.
+            line_const = [z3_true]
+            deepest_block = None
+          else: #< A line under ifdef is required, for which we have the pc.
+            assert line > 0
+            assert line_constraints[unit2srcfile(unit)][arch.name] is not None
+            cb = line_constraints[unit2srcfile(unit)][arch.name]
+            deepest_block = cb.get_deepest_block(line)
+            line_const = deepest_block.pc.assertions()
+          
+          #
+          # Attempt to build the line
+          #
+          line_covered = False
+
+          if deepest_block in cant_cover_blocks:
+            # The surrounding ConditionalBlock is already determined to be
+            # non coverable while checking for a different line.
+            logger.debug("%s was already determined to be not coverable\n" % line)
+            line_covered = False
+          elif deepest_block in covered_blocks:
+            # This line is already covered as it shares the constraints
+            # with a previously covered line.
+            logger.debug("Line %s was already covered\n" % line)
+            line_covered = True
+          else: #< No info on line's coverage so far -- need additional constraints.
+            constraints_with_line = constraints_with_file[:]
+            constraints_with_line.extend(line_const)
+
+            # SAT check.
+            if compiled_arch_constraints is None:
+              compiled_arch_constraints = klocalizer.compile_constraints(arch)
+            full_constraints = compiled_arch_constraints + constraints_with_line
+            logger.debug("Checking constraints: %s\n"% constraints_with_line)
+            model_sampler = Klocalizer.Z3ModelSampler(full_constraints, random_seed=random_seed, logger=logger)
+            is_sat, z3_model = model_sampler.sample_model()
+
+            # Constraints is SAT means line is covered.
+            line_covered = is_sat
+
+            if is_sat: # Line constraints are satisfiable
+              # The constraints are approved to be SAT and improving coverage,
+              # therefore, keep them in.
+              accumulated_constraints = constraints_with_line[:]
+              constraints_with_file = constraints_with_line[:]
+
+          # End of attempting to build the line: check if line is built and
+          # account for it.
+          if line_covered:
+            logger.debug("Covered: (%s:%s)\n" % (unit, line))
+            # Signal that the current constraints improved the coverage.
+            is_improved = True
+
+            # Report the coverage for this model being built.
+            current_coverage[unit] = sorted(current_coverage.get(unit, []) + [line])
+
+            # For optimization, keep track of all blocks covered with this.
+            covered_blocks.add(None) #< Global scope, special value.
+            # Self and all ancestor blocks.
+            while deepest_block is not None:
+              covered_blocks.add(deepest_block)
+              deepest_block = deepest_block.parent
+          else:
+            logger.debug("Failed to cover: (%s:%s)\n" % (unit, line))
+            # Line is not covered -- therefore, keep it as requirement.
+            remaining_lines.append(line)
+            
+            # For optimization, keep track of blocks that cannot be covered.
+            # Self and all descendants are not coverable.
+            cant_cover_blocks.add(deepest_block)
+            if deepest_block:
+              blocks = [deepest_block]
+              while blocks:
+                b = blocks.pop()
+                cant_cover_blocks.add(b)
+                for sub_b in b.sub_block_groups:
+                  blocks.extend(sub_b)
+
+        # TODO: in some cases, we know the line is never satisfiable by
+        # syntax analysis (condition is 0). Don't keep them as requirement?
+
+        # Keep the remaining lines in the requirements.
+        if remaining_lines:
+          new_requirements.append((unit, remaining_lines))
+        else: # If no more remaining lines, then no more requirements for the file.
+          pass
+      
+      # Done with an iteration over all required file:lines with the current arch.
+      
+      # Update the requirements, which is potentially smaller with the new coverage.
+      requirements = new_requirements
+      logger.debug("Remaining requirements: %s\n" % requirements)
+
+      # Save this accumulated model, which improves coverage.
+      if is_improved:
+        got_first_improvement = True
+        logger.info("A coverage improving constraints set found: sampling a model.\n")
+        assert compiled_arch_constraints
+        assert accumulated_constraints
+        full_constraints = compiled_arch_constraints + accumulated_constraints
+        # Repair is done here only since this is where the final model to
+        # get the config file is produced.
+        apprx_constraints = approximate_constraints.get(arch.name, approximate_constraints.get("default", None))
+        model_sampler = Klocalizer.Z3ModelSampler(full_constraints, approximate_constraints=apprx_constraints, random_seed=random_seed, logger=logger)
+        is_sat, z3_model = model_sampler.sample_model()
+        assert is_sat
+        assert current_coverage
+        z3_models.append((arch, z3_model, current_coverage))
+        logger.debug("Sampled a model\n")
+      else:
+        # Continue with the next arch as this could not improve coverage anymore.
+        # We don't change the architecture right away if there is improvement
+        # because something that could not be covered in this iteration
+        # might get covered in next iteration due to mutual exclusion.
+        arch_idx += 1
+        printed_arch_info = False
+
+    logger.debug("Localization search is done. Numbers of models created: %s\n" % len(z3_models))
+
+    # "original_include_mutex_list" has all the lines the user provided.
+    # "include_mutex_list" is the processed list, where the lines
+    # belonging to the global scope (not under any ifdefs) are filtered out.
+    # This filtering helped us to avoid calls to SuperC if all lines were
+    # global. We have the coverage results for the filtered lines. Now,
+    # translate back to user's original list of lines for the coverage report.
+    # Structure: { "path/to/unit": { "unit": [configs_list], 1: [configs_list], ...]  }  }
+    # "unit" is special value for all configs that compile the unit, even
+    # without any line targets.
+    coverage_report = OrderedDict()
+    for unit, lines in original_include_mutex_list:
+      coverage_report[unit] = OrderedDict()
+      # List of configs that compiles the unit, even without specific line targets.
+      # If there is some config file that does not compile any specific lines
+      # but the unit only, it will be here together with all other configs that
+      # compile the unit.
+      coverage_report[unit]["unit"] = [] 
+      for l in lines:
+        coverage_report[unit][l] = []
+      # Values will be updated before writing the report if they were covered.
+
+    #
+    # Sample configs (and create coverage report)
+    #
+    num_models = len(z3_models)
+    if num_models == 0 :
+      logger.error("No satisfying configuration found.\n")
+      exit(11)
+
+    assert z3_models # (arch, z3_model, current_coverage) tuples
+    logger.info("Sampling and writing %s configuration files from models.\n" % num_models)
+    for i, (arch, model, coverage) in enumerate(z3_models):
+      config_id = "%s-%s" % (i, arch.name)
+      config_basename = "%s.config" % config_id 
+      config_file_path = os.path.join(output_dir, config_basename)
+      pathlib.Path(os.path.dirname(config_file_path)).mkdir(parents=True, exist_ok=True)
+      
+      # Sample the config from the model
+      logger.info("[%s/%s] Sampling and writing the configuration file to %s\n" % (i+1, num_models, config_file_path))
+      config_content = Klocalizer.get_config_from_model(model, arch, set_tristate_m=modules_arg, allow_non_visibles=allow_non_visibles)
+      # Write the config file
+      with open(config_file_path, 'w') as f:
+        f.write(config_content)
+      
+      # Create the coverage report for the config
+      built_mutex_units = [] #< Use for logging the build command
+      for unit, lines in original_include_mutex_list:
+        if unit in coverage:
+          built_mutex_units.append(unit)
+          coverage_report[unit]["unit"].append(config_basename)
+        for l in lines:
+          if l in global_scope_lines.get(unit, []) and unit in coverage:
+            coverage_report[unit][l].append(config_basename)
+          elif unit in coverage and l in coverage[unit]:
+            coverage_report[unit][l].append(config_basename)
+
+      # Log the build command
+      build_cmd = "KCONFIG_CONFIG=%s %s ARCH=%s olddefconfig clean %s" % (config_file_path, cross_compiler, arch.name, " ".join([u for u, _ in include_list] + built_mutex_units))
+      logger.info("Build with \"%s\"\n" % build_cmd)
+
+    # Compute coverage report summary
+    num_target_files = 0
+    num_target_lines = 0
+    num_files_compiled = 0
+    num_lines_compiled = 0
+    for unit in coverage_report:
+      num_target_files += 1
+      if coverage_report[unit]["unit"]:
+        num_files_compiled += 1
+      # Count lines
+      for k in coverage_report[unit]:
+        if k == "unit":
+          continue
+        num_target_lines += 1
+        if coverage_report[unit][k]:
+          num_lines_compiled += 1
+    assert num_target_files >= num_files_compiled
+    assert num_target_lines >= num_lines_compiled
+    
+    # Log coverage summary
+    if num_target_files == num_files_compiled and num_target_lines == num_lines_compiled:
+      logger.info("Coverage summary: all mutex constraints were satisfied.\n")
+    elif num_files_compiled == 0: # No coverage
+      assert num_lines_compiled == 0
+      logger.info("Coverage summary: none of the mutex constraints were satisfied.\n")
+    else: # Some coverage
+      assert num_target_files > 0
+      logger.info("Coverage summary: some of the mutex constraints were satisfied: %s/%s files and %s/%s lines were covered.\n" % (num_files_compiled, num_target_files, num_lines_compiled, num_target_lines))
+      logger.warning("Despite the high accuracy, klocalizer cannot guarantee claimed coverage due to under approximations.\n")
+
+    # Write the coverage report
+    logger.info("Writing the coverage report to %s\n" % coverage_report_file)
+    logger.info("Note coverage report is attempted coverage.  Actual coverage may be reduced due to limitations of klocalizer's constraint collection.\n")
+    with open(coverage_report_file, 'w') as f:
+      json.dump(coverage_report, f, indent=2)
+    
+    #
+    # end of mutual exclusion algorithm
+    #
+    exit(0)
+
+  #
+  # Sampling algo 2: single config, no mutual exclusion
+  #
+  assert not mutex_enabled
+  assert not include_mutex_list
   for arch in archs:
     logger.info("Trying \"%s\"\n" % (arch.name))
+
+    #
+    # SAT check for units only (without line constraints)
+    #
+    # This will be final SAT check if there are no line constraints to add.
+    # Otherwise, this check will serve as architecture search, and the
+    # extended constraints with the line constraints will be checked again.
     constraints = klocalizer.compile_constraints(arch)
-    model_sampler = Klocalizer.Z3ModelSampler(constraints, approximate_constraints=approximate_constraints, random_seed=random_seed, logger=logger)
+    if has_line_constraints:
+       # Don't do approximation yet, this is only arch search, final model will come with the line constraints.
+      model_sampler = Klocalizer.Z3ModelSampler(constraints, random_seed=random_seed, logger=logger)
+    else:
+      # Do the approximation at the same time: this will be the final model.
+      apprx_constraints = approximate_constraints.get(arch.name, approximate_constraints.get("default", None))
+      model_sampler = Klocalizer.Z3ModelSampler(constraints, approximate_constraints=apprx_constraints, random_seed=random_seed, logger=logger)
     is_sat, payload = model_sampler.sample_model()
 
+    #
+    # Account for line constraints
+    #
+    if is_sat and has_line_constraints:
+      # We could have added the line constraints in the first place.
+      # However, if the line constraints are not cached, SuperC config
+      # creation takes a long time since it requires localizing a Linux
+      # configuration file to build the unit and building the unit.
+      # To avoid attempting the setup for already unsatisfiable
+      # architectures, we first find a building architecture, then request
+      # the line constraints. If, for example, we have 5 units, we avoid
+      # running SuperC setup for each of these files if the architecture
+      # does not compile some of these units. An optimization to SuperC
+      # configuration creation pipeline might solve this.
+      logger.info("The constraints are satisfiable for the units.  Trying with the line constraints.\n")
+
+      #
+      # Compute line presence conditions
+      #
+      srcfiles_with_line_requirements = ["%s.c" % u[:-len('.o')] for u, lines in all_comp_units_list if lines]
+      logger.info("Computing the line presence conditions under %s for the following units: %s\n" % (arch.name, " ".join(srcfiles_with_line_requirements)))
+      for unit in srcfiles_with_line_requirements:
+        get_presence_conditions(unit2srcfile(unit), arch)
+
+      logger.debug("Getting additional line constraints.\n")
+
+      # For "includes"
+      logger.debug("Adding the constraints for \"include\" lines.\n")
+      additional_line_constraints = []
+      for unit, lines in include_list:
+        if lines:
+          srcfile = unit2srcfile(unit)
+          if line_constraints[srcfile][arch.name] is not None: # None is SuperC failure.
+            pc_blocks = line_constraints[srcfile][arch.name].get_deepest_blocks(lines)
+            for pcb in pc_blocks:
+              additional_line_constraints.extend(pcb.pc.assertions())
+      
+      # For "excludes"
+      logger.debug("Adding the constraints for \"exclude\" lines.\n")
+      for unit, lines in exclude_list:
+        if not lines:
+          pass # Already handled
+        else: # has lines
+          # Get the line constraints
+          unit_line_c = []
+          srcfile = unit2srcfile(unit)
+          if line_constraints[srcfile][arch.name] is not None: # None is SuperC failure.
+            pc_blocks = line_constraints[srcfile][arch.name].get_deepest_blocks(lines)
+            for pcb in pc_blocks:
+              unit_line_c.extend(pcb.pc.assertions())
+          # Get kmax constraints
+          unit_kmax_c = kmax_constraints[unit]
+          unit_kmax_c = unit_kmax_c if unit_kmax_c else []
+          # Get exclusion constraints
+          c = get_exclusion_constraints(unit_kmax_c, unit_line_c)
+          additional_line_constraints.extend(c)
+
+
+      # Add line constraints to the overall constraints
+      logger.debug("Adding %s line constraints to the overall constraints.\n" % len(additional_line_constraints))
+      constraints.extend(additional_line_constraints)
+
+      # Do another SAT check to update is_sat and payload values with the
+      # overall constraints that include line constraints
+      logger.debug("Doing another SAT check with the complete set of constraints.\n")
+      apprx_constraints = approximate_constraints.get(arch.name, approximate_constraints.get("default", None))
+      model_sampler = Klocalizer.Z3ModelSampler(constraints, approximate_constraints=apprx_constraints, random_seed=random_seed, logger=logger)
+      is_sat, payload = model_sampler.sample_model()
+
     #
     # Constraints are UNSAT
     #
@@ -561,11 +1551,11 @@ def klocalizerCLI():
 
         # Print the command for building
         if sample_count == 1:
-          if not compilation_units:
-            build_cmd = "make.cross ARCH=%s clean; make.cross ARCH=%s" % (arch.name, arch.name)
+          if not include_list:
+            build_cmd = "%s ARCH=%s clean; %s ARCH=%s" % (cross_compiler, arch.name, cross_compiler, arch.name)
           else:
-            build_cmd = "make.cross ARCH=%s clean %s" % (arch.name, " ".join(compilation_units))
-          logger.info("Build with \"make.cross ARCH=%s olddefconfig; %s\".\n" % (arch.name, build_cmd))
+            build_cmd = "%s ARCH=%s clean %s" % (cross_compiler, arch.name, " ".join([u for u, _ in include_list]))
+          logger.info("Build with \"%s ARCH=%s olddefconfig; %s\".\n" % (cross_compiler, arch.name, build_cmd))
 
       # Stop the SAT search with the first SAT arch if not reporting for all archs
       if not reportallarchs:
@@ -596,5 +1586,8 @@ if __name__ == '__main__':
   except Arch.FormulaGenerationError as e:
     logger.error("Cannot generate %s formulas.\n" % (e.formula_type))
     exit(13)
+  except SuperC.SuperC_ChecksFailed as e:
+    logger.error("SuperC checks failed, reason: %s.  "
+                 "Either fix the issue or omit the line requirements.\n" % (e.reason))
   
   exit(0)
diff --git a/kmax/klocalizer.py b/kmax/klocalizer.py
index 01844eae..1159dbb7 100644
--- a/kmax/klocalizer.py
+++ b/kmax/klocalizer.py
@@ -2,6 +2,7 @@
 import os
 import argparse
 import z3
+import re
 import regex
 import pickle
 import random
@@ -11,12 +12,37 @@
 import pprint
 import enum
 import z3
+import time
 from kmax.arch import Arch
 from kmax.common import get_kmax_constraints, unpickle_kmax_file
-from kmax.vcommon import getLogLevel, getLogger
+from kmax.vcommon import getLogLevel, getLogger, run
 
 # TODO(necip): automated testing
 
+def __parse_cb(cb_string_rep: str):
+  """Parse and return a conditional block group.
+
+  Arguments:
+  cb_string_rep -- string representation of a conditional block.
+
+  Returns ConditionalBlock.
+  """
+  # TODO: change these
+  cb = Klocalizer.ConditionalBlock()
+  cb.start_line = int(cb_string_rep["StartLine"])
+  cb.end_line = int(cb_string_rep["EndLine"])
+  # Config options come as |(defined CONFIG_A)| from SuperC. Convert
+  # them to CONFIG_A format for compatibility with kclause.
+  pc_string = cb_string_rep["PC"]
+  pc_string = re.sub(r'\|\(defined (CONFIG_[a-zA-Z0-9_]*)\)\|', r'\1', pc_string)
+  z3_solver = z3.Solver()
+  z3_solver.from_string(pc_string) # TODO: make this an expression instead?
+  cb.pc = z3_solver
+  cb.sub_block_groups = Klocalizer.ConditionalBlock.__parse_sub(cb_string_rep["Sub"], cb)
+
+  return cb
+
+
 try:
   from subprocess import DEVNULL  # Python 3.
 except ImportError:
@@ -588,23 +614,34 @@ def compile_constraints(self, arch: Arch):
   class __CompUnitInclusionProp(enum.Enum):
     EXCLUDE=0
     INCLUDE=1
-
-  def __add_compilation_unit(self, unit: str, inclusion_prop: __CompUnitInclusionProp):
-    """Given a compilation unit, fetch the inclusion constraints using kmax,
-    and add these constraints to kmax constraints based on inclusion property.
+  
+  def get_compilation_unit_constraints(self, unit: str):
+    """Given a compilation unit, fetch and return the inclusion constraints
+    using kmax.
 
     May raise NoFormulaFoundForCompilationUnit or MultipleCompilationUnitsMatch exception.
 
     Arguments:
-    unit -- compilation unit.
-    inclusion_prop -- Inclusion property, i.e., include or exclude the unit.
+    unit -- compilation unit or directory.
     """
     #
     # Format the unit name
     #
-    if not unit.endswith(".o"):
-      self.__logger.warning("Forcing file extension to be .o, since lookup is by compilation unit: %s\n" % (unit))
-      unit = os.path.splitext(unit)[0] + ".o"
+    # There must be '.o' extension for units, '/' suffix for directories
+    if not unit.endswith(".o") and not unit.endswith('/'):
+      # Try to understand whether it was directory or unit
+      bname = unit.split('/')[-1]
+      assert bname
+      ext = os.path.splitext(bname)[-1]
+      if ext and ext.lower() in ['.c', '.s', '.o']:
+        # This must be a single unit rather than a directory
+        self.__logger.warning("Forcing file extension to be .o, since lookup is by compilation unit: %s\n" % (unit))
+        unit = os.path.splitext(unit)[0] + ".o"
+      else:
+        # This must be a directory
+        unit = unit + '/'
+      
+    is_top_level_dir = unit.endswith('/') and unit.count('/') == 1
     
     #
     # Process the unit name get all the paths for which to pull the kmax formulas
@@ -615,7 +652,14 @@ def __add_compilation_unit(self, unit: str, inclusion_prop: __CompUnitInclusionP
       # Maybe we should just do the same for all? Maybe that's the reason for the issue Jeho experienced.
       self.__fetch_kmax_constraints(unit)
       if unit not in self.__kmax_formulas:
-        raise Klocalizer.NoFormulaFoundForCompilationUnit(unit)
+        if is_top_level_dir:
+          # This is a top-level directory, which is controlled by a
+          # non-kbuild Makefile that kmax cannot work on. These are mostly
+          # unconstrained. The constrained top-level directories are
+          # handled through hard-coding of the constraints below.
+          pass
+        else:
+          raise Klocalizer.NoFormulaFoundForCompilationUnit(unit)
     else: # kmax_formulas is not cache but complete
       if unit not in self.__kmax_formulas:
         kbuild_paths = self.__resolve_kbuild_path(unit)
@@ -649,13 +693,33 @@ def __add_compilation_unit(self, unit: str, inclusion_prop: __CompUnitInclusionP
         if not kmax_constraints_for_unit: 
           kmax_constraints_for_unit = []
         kmax_constraints_for_unit.append(top_makefile_constraints[top_dir])
+    
+    if kmax_constraints_for_unit is None:
+      # "None" is allowed only for top level directories, which are outside
+      # kbuild makefiles.
+      assert is_top_level_dir
+      kmax_constraints_for_unit = []
+
+    return kmax_constraints_for_unit
+
+  def __add_compilation_unit(self, unit: str, inclusion_prop: __CompUnitInclusionProp):
+    """Given a compilation unit, fetch the inclusion constraints using kmax,
+    and add these constraints to kmax constraints based on inclusion property.
+
+    May raise NoFormulaFoundForCompilationUnit or MultipleCompilationUnitsMatch exception.
+
+    Arguments:
+    unit -- compilation unit.
+    inclusion_prop -- Inclusion property, i.e., include or exclude the unit.
+    """
+    kmax_constraints_for_unit = self.get_compilation_unit_constraints(unit)
 
     if inclusion_prop == Klocalizer.__CompUnitInclusionProp.INCLUDE:
       self.__include_compilation_units.append(unit)
       self.__kmax_constraints.extend(kmax_constraints_for_unit)
     elif inclusion_prop == Klocalizer.__CompUnitInclusionProp.EXCLUDE:
       self.__exclude_compilation_units.append(unit)
-      self.__kmax_constraints.extend([z3.Not(c) for c in kmax_constraints_for_unit])
+      self.__kmax_constraints.extend(z3.Not(z3.And(kmax_constraints_for_unit)))
     else:
       assert False
 
@@ -688,6 +752,615 @@ def reset_compilation_units(self):
     self.__include_compilation_units=[]
     self.__exclude_compilation_units=[]
 
+  class ConditionalBlock:
+    """A node of tree-like representation of source code for conditional blocks
+    defined by conditional preprocessor directives.
+    """
+    def __init__(self):
+      # Line number where the conditional block starts in the source code.
+      # A conditional block starts with a`#if` or `#elif` directive. Thus,
+      # the corresponding line in the source code contains one of these directives.
+      self.start_line = -1
+
+      # Line number where the conditional block ends in the source code. A
+      # conditional block ends with a `#elif` (the beginning of the next conditional
+      # block) or `#endif` directive. Thus, the corresponding line in the source
+      # code contains one of these directives.
+      self.end_line = -1
+
+      # List of sub conditional block groups contained. A conditional block
+      # group is a conditional ladder (#if [#elif]* #endif), which might contain
+      # one or more conditional blocks.
+      self.sub_block_groups = []
+
+      # Complete presence condition for the conditional block. A z3.Solver instance.
+      self.pc = None
+
+      # Parent conditional block.
+      self.parent = None
+    
+    def dumps(self) -> str:
+      """Return string representation of conditional block.
+      """
+      return self.__repr__()
+    
+    @staticmethod
+    def loads(cb_string: str):
+      """Parse conditional block from its string representation.
+
+      Arguments:
+      cb_string -- string representation of conditional block.
+
+      Returns an instance of ConditionalBlock.
+      """
+      from ast import literal_eval
+      return Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(literal_eval(cb_string))
+
+    def __repr__(self):
+      pc_repr = ""
+      if self.pc: pc_repr = self.pc.to_smt2().replace("\n", "\\n")
+      return "{\"StartLine\": %d, \"EndLine\": %d, \"PC\": \"%s\", \"Sub\": %s}" % (self.start_line, self.end_line, pc_repr, self.sub_block_groups)
+
+    def get_deepest_blocks(self, lines):
+      """Given a line number, returns the unique set of deepest conditional
+      blocks that contains these lines. The return value is equivalent to what
+      would be obtained by calling get_deepest_block() for each line and deduplicating.
+      However, this method is faster.
+
+      Arguments:
+      lines -- List of lines to query the deepest conditional blocks for.
+
+      Returns `None` if a block for some line can't be found."""
+      # TODO: optimize: do a single traversal on the tree.
+      # Use a list to preserve the order for replicability.
+      cbs = []
+      for line in lines:
+        cb = self.get_deepest_block(line)
+        if cb == None: return None
+        if cb not in cbs: cbs.append(cb)
+      start_line_cbs = [(cb.start_line, cb) for cb in cbs]
+      start_line_cbs.sort()
+      return [x[1] for x in start_line_cbs]
+      
+      return cbs
+
+    def get_deepest_block(self, line: int):
+      """Given a line number, returns the deepest conditional block that contains
+      the line.
+
+      Arguments:
+      line -- Line number to query the deepest conditional block for.
+
+      Returns `None` if line is not included within the block."""
+      if not (self.start_line <= line < self.end_line):
+        return None
+      
+      # visit children
+      for cbgroup in self.sub_block_groups:
+        for cb in cbgroup:
+          ret = cb.get_deepest_block(line)
+          if ret != None:
+            return ret
+      
+      # no children covers but the self does -- return self
+      return self
+
+    @staticmethod
+    def __parse_sub(sub_string_rep: str, parent):
+      """Parse and return conditional block groups This may be any intermediate
+      conditional block group as well.
+
+      Arguments:
+      sub_string_rep -- string representation of conditional block groups.
+      parent -- Parent ConditionalBlock instance. The parent of top-level conditional
+      block groups parsed by the method will be set to this.
+
+      Returns [[ConditionalBlock]], i.e., a list of conditional block groups.
+      """
+      groups = []
+      for cbgroup_str in sub_string_rep:
+        group = []
+        for cb_str in cbgroup_str:
+          cb = Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(cb_str)
+          cb.parent = parent
+          group.append(cb)
+        groups.append(group)
+      return groups
+
+    @staticmethod
+    def __parse_cb(cb_string_rep: str):
+      """Parse and return a conditional block group.
+
+      Arguments:
+      cb_string_rep -- string representation of a conditional block.
+
+      Returns ConditionalBlock.
+      """
+      # TODO: change these
+      cb = Klocalizer.ConditionalBlock()
+      cb.start_line = int(cb_string_rep["StartLine"])
+      cb.end_line = int(cb_string_rep["EndLine"])
+      # Config options come as |(defined CONFIG_A)| from SuperC. Convert
+      # them to CONFIG_A format for compatibility with kclause.
+      pc_string = cb_string_rep["PC"]
+      pc_string = re.sub(r'\|\(defined (CONFIG_[a-zA-Z0-9_]*)\)\|', r'\1', pc_string)
+      z3_solver = z3.Solver()
+      z3_solver.from_string(pc_string) # TODO: make this an expression instead?
+      cb.pc = z3_solver
+      cb.sub_block_groups = Klocalizer.ConditionalBlock.__parse_sub(cb_string_rep["Sub"], cb)
+
+      return cb
+
+    # TODO: impl method: given pc and line ranges, return configs
+
+  @staticmethod
+  def __check_args_get_sourceline_pc( \
+      srcfile: str, srcdir: str, is_linux: bool, \
+      archs, superc_linux_script, makecross_script, \
+      skip_kconfig_config_gen, skip_building_unit, skip_superc_config_gen):
+    """Check arguments of for sourceline presence condition localization methods
+    through assertions.
+    """
+    from shutil import which
+    def is_success(command_to_run: list):
+      return 0 == run(command_to_run, capture_stdout=True, capture_stderr=True)[2]
+    
+    def check_java():
+      return which("java") != None
+
+    def check_superc():
+      return is_success(["java", "superc.SuperC"])
+    
+    def check_superc_linux_script():
+      return which(superc_linux_script) != None
+    
+    def check_makecross_script():
+      return which(makecross_script) != None
+    
+    # TODO: raise specific exceptions instead of assertion failures
+    assert srcfile
+    if srcdir: assert os.path.isdir(srcdir) and os.path.isfile(os.path.join(srcdir, srcfile))
+    if not srcdir: os.path.isfile(srcfile)
+    assert check_java()
+    assert check_superc()
+    if is_linux:
+      assert srcdir # TODO: check if dir is linux ksrc
+      assert skip_building_unit or check_makecross_script()
+      assert check_superc_linux_script()
+      assert archs
+      for arch in archs:
+        assert type(arch) is Arch
+
+  class Ret_LocalizeConfig(enum.Enum):
+    SUCCESS=0       #< All success.
+    ERROR_UNSAT=1   #< Given archs do not compile the unit.
+    ERROR_KMAX_EXCEPTION=2       #< A Klocalizer.KmaxException was thrown for one of the units.
+    ERROR_KLOCALIZER_EXCEPTION=3 #< A Klocalizer.KlocalizerException was thrown.
+
+  @staticmethod
+  def localize_config(unit_paths: list, output_config_path: str,
+    linux_ksrc: str, archs: list, logger):
+    """Localize a linux configuration file that compiles the given units.
+
+    This is a simplified version of what klocalizer command line tool does:
+    it searches for an architecture one by one, and when found a SAT one,
+    creates a configuration file (takes a random solution).
+
+    Returns a tuple of 3 values:
+    * Ret_LocalizeConfig: An instance of Ret_LocalizeConfig, representing
+    success/error.
+    * Arch: The first Arch instance that compiles the units from the input
+    archs list. May be None on error.
+    * Exception: The exception thrown if the status is ERROR_KMAX_EXCEPTION
+    or ERROR_KLOCALIZER_EXCEPTION, which can be used for diagnostic.
+
+    Also, writes the output configuration file to output_config_path on
+    success. This is as obtained from klocalizer: may need olddefconfig.
+    A config file might be created even on error.
+
+    Arguments:
+    * unit_paths -- List of unit paths (e.g., ['kernel/fork.o', 'kernel/cpu.o'])
+    * output_config_path -- Path to non-existing output configuration file.
+    * linux_ksrc -- Path to top linux source directory.
+    * archs -- Architectures to try as a list of Arch instances.
+    * logger -- Logger that implements common.VoidLogger interface.
+    """
+    try:
+      return Klocalizer.__localize_config(unit_paths, output_config_path, linux_ksrc, archs, logger)
+    except Klocalizer.KmaxException as e:
+      logger.debug("Exception in localize_config(): \"%s\"\n" % e.message)
+      ret_status = Klocalizer.Ret_LocalizeConfig.ERROR_KMAX_EXCEPTION
+      ret_arch = None
+      ret_exception = e
+      return ret_status, ret_arch, ret_exception
+    except Klocalizer.KlocalizerException as e:
+      logger.debug("Exception in localize_config(): \"%s\"\n" % e.message)
+      ret_status = Klocalizer.Ret_LocalizeConfig.ERROR_KLOCALIZER_EXCEPTION
+      ret_arch = None
+      ret_exception = e
+      return ret_status, ret_arch, ret_exception
+
+
+  @staticmethod
+  def __localize_config(unit_paths: list, output_config_path: str,
+    linux_ksrc: str, archs: list, logger):
+    """Helper to Klocalizer.localize_config(). May throw exception to be
+    caught by Klocalizer.localize_config().
+    """
+    #
+    # Check arguments
+    #
+    assert unit_paths
+    for u in unit_paths:
+        assert u.endswith(".o")
+    assert os.path.isdir(linux_ksrc)
+    assert archs
+    assert logger
+
+    #
+    # Create a klocalizer instance
+    #
+    logger.debug("Creating the klocalizer instance.\n")
+    kloc = Klocalizer()
+    kloc.set_linux_krsc(linux_ksrc)
+    kloc.add_constraints([z3.Not(z3.Bool("CONFIG_BROKEN"))])
+    
+    #
+    # Add compilation units (also retrives kmax formulas)
+    #
+    logger.debug("Adding the compilation units to klocalizer.\n")
+    for u in unit_paths:
+      kloc.include_compilation_unit(u)
+
+    #
+    # Find an architecture that compiles the unit
+    #
+    logger.debug("Detecting the architecture.\n")
+    time_start = time.time()
+    for arch in archs:
+      logger.debug("Trying \"%s\"\n" % arch.name)
+      full_constraints = kloc.compile_constraints(arch)
+      model_sampler = Klocalizer.Z3ModelSampler(full_constraints)
+      is_sat, z3_model = model_sampler.sample_model()
+      if is_sat:
+        break
+    time_elapsed = time.time() - time_start
+    logger.debug("TIME: Time elapsed(sec) for architecture search: %.2f\n" % time_elapsed)
+    if not is_sat: #< Not possible to compile with the given set of archs
+      logger.debug("Could not find an architecture that compiles the unit.\n")
+      return Klocalizer.Ret_LocalizeConfig.ERROR_UNSAT, None, None
+    else:          #< Compiles for arch
+      assert arch
+      logger.debug("The unit compiles for the architecture: \"%s\"\n" % arch.name)
+
+    #
+    # Create a config file that compiles the unit
+    #
+    logger.debug("Creating config file to compile the unit.\n")
+    time_start = time.time()
+    assert is_sat and (z3_model is not None)
+    config_content = Klocalizer.get_config_from_model(z3_model, arch, set_tristate_m=False, allow_non_visibles=False)
+    assert config_content
+    with open(output_config_path, "w") as f:
+      f.write(config_content)
+    assert os.path.isfile(output_config_path)
+    time_elapsed = time.time() - time_start
+    logger.debug("TIME: Time elapsed(sec) for creating the config file: %.2f\n" % time_elapsed)
+
+    return Klocalizer.Ret_LocalizeConfig.SUCCESS, arch, None
+
+  @staticmethod
+  def get_sourceline_pc_standalone_file(srcfile: str):
+    """Get sourceline presence conditions for a stand-alone source file.
+
+    Requires SuperC.
+
+    Arguments:
+    srcfile -- Path to the source file.
+
+    Returns ConditionalBlock.
+    """
+    # TODO: let user choose whether to restrict to CONFIG_ prefixed options
+    Klocalizer.__check_args_get_sourceline_pc(srcfile=srcfile, srcdir=None, is_linux=False, \
+      superc_linux_script=None, makecross_script=None,
+      skip_kconfig_config_gen=True, skip_building_unit=True, skip_superc_config_gen=True)
+  
+    #
+    # Run SuperC
+    #
+    import tempfile
+    with tempfile.NamedTemporaryFile() as tmpfile:
+      tmpfilename = tmpfile.name
+      superc_cmd = ["java", "superc.SuperC", "-sourcelinePC", tmpfilename, srcfile]
+      _, _, ret, _ = run(superc_cmd, capture_stdout=True, capture_stderr=True)
+      assert ret == 0
+      from ast import literal_eval
+      return Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(literal_eval(tmpfile.read().decode()))
+
+  class SourcelinePcResult(enum.Enum):
+    SUCCESS=0       #< All success.
+    ERROR_UNSAT=1   #< Given archs do not compile the unit.
+    ERROR_MAKE=2    #< Make results in error while trying to compile the unit.
+    ERROR_SUPERC=3  #< SuperC fails to create sourceline presence conditions,
+                    #< or SuperC cannot be found. The returned architecture
+                    #< is still valid to compile the unit.
+    ERROR_MAKE_TIMEOUT=4   #< Make timed-out while trying to compile the unit.
+    ERROR_SUPERC_TIMEOUT=5 #< SuperC timed-out while creating sourceline
+                    #< presence conditions. The returned architecture is
+                    #< still valid to compile the unit.
+
+
+  @staticmethod
+  def get_sourceline_pc_linux_file(srcfile: str, linux_ksrc: str, archs, \
+      superc_linux_script: str, makecross_script: str, \
+      build_target: str,
+      restrict_to_config_prefix=True, \
+      superc_configs_dir="superc_configs/", \
+      skip_kconfig_config_gen=False, skip_building_unit=False, skip_superc_config_gen=False, \
+      make_out_path=None, make_err_path=None, \
+      superc_out_path=None, superc_err_path=None, \
+      make_timeout=None, superc_timeout=None,
+      logger=VoidLogger()):
+    """Get sourceline presence conditions for a source file within a Linux
+    kernel source.
+
+    Requires SuperC.
+
+    The routine is as follows:
+    1. Create a config file that compiles the unit using Klocalizer.
+    2. Compile the unit using the compiler script (makecross_script).
+    3. Create SuperC config file for the unit using SuperC Linux script (superc_linux_script).
+    4. Clear autoconf.h ($LINUX_KSRC/include/generated/autoconf.h)
+    5. Run SuperC using SuperC Linux script (superc_linux_script).
+    6. Parse SuperC's output and and return (arch, [[ConditionalBlock]]).
+
+    Arguments:
+    srcfile -- Path to the source file. This must be relative to the top directory
+    of the Linux kernel source, specified with linux_ksrc argument.
+    linux_ksrc -- Path to the Linux kernel source.
+    arch -- A list of Arch instances. The first arch that compiles the unit
+    will be used.
+    superc_linux_script -- Path to the superc_linux script to be used to obtain
+    SuperC configs for the source file and to run SuperC. This can be found
+    at $SUPERC_SRC/scripts/superc_linux.sh.
+    makecross_script -- Path to the make script for cross compilation. For
+    Linux source files, SuperC needs the source file to be built. If not
+    cross-compiling, having this set to `make` is enough if it is in PATH.
+    restrict_to_config_prefix -- If set, `-restrictConfigToPrefix` is set to 
+    `CONFIG_` for SuperC. This boosts the performance and results in focusing
+    on config macros, while setting the rest to their default values.
+    build_target -- Build target for the given source file (srcfile).
+    Usually, replacing the source file extension with .o (src/file.c -> src/file.o)
+    is enough, but there are cases where parent or different directories need
+    to be built.
+    superc_configs_dir -- Directory to read/write SuperC configs. See `skip_superc_config_gen`.
+    skip_kconfig_config_gen -- Set to skip Kconfig config generation for the unit.
+    skip_building_unit -- Set to skip building the unit.
+    skip_superc_config_gen -- Set to skip SuperC config generation for the
+    unit to reuse existing configs. If not set, a config is always generated.
+    make_out_path -- Path to the file where to write make's stdout while
+    compiling the unit. Created if the unit cannot be compiled, i.e., 
+    when status is ERROR_MAKE.
+    make_err_path -- Path to the file where to write make's stderr while
+    compiling the unit. Created if the unit cannot be compiled, i.e.,
+    when status is ERROR_MAKE.
+    superc_out_path -- Path to the file where to write superc's stdout
+    while computing sourceline pc. Created if it fails, i.e., when status
+    is ERROR_SUPERC.
+    superc_err_path -- Path to the file where to write superc's stderr
+    while computing sourceline pc. Created if it fails, i.e., when status
+    is ERROR_SUPERC.
+    make_timeout -- Timeout in seconds for make.
+    superc_timeout -- Timeout in seconds for SuperC.
+    logger -- Logger.
+
+    Returns a tuple of three values:
+      - An instance of SourcelinePcResult, representing the success/error.
+      - An Arch instance, representing the architecture that compiles the
+        unit. May be None in error cases, e.g., ERROR_UNSAT.
+      - A ConditionalBlock instance, representing the sourceline presence
+        conditions for the sourcefile. May be None in error cases.
+    """
+    # TODO: take additional flags to SuperC
+    # TODO: any existing .config file is overwritten. write new Kconfig configs to a path different than linux_ksrc/.config?
+    # TODO: don't create superc_configs if exists already? add a flag such as create_if_no_config
+    superc_configs_dir=os.path.realpath(superc_configs_dir)
+
+    # Check the arguments.
+    Klocalizer.__check_args_get_sourceline_pc(srcfile, linux_ksrc, True, \
+      archs, superc_linux_script, makecross_script, \
+      skip_kconfig_config_gen, skip_building_unit, skip_superc_config_gen)
+
+    def write_content_to_file(content : str, fpath : str):
+      if fpath is None:
+        return False
+      os.makedirs(os.path.dirname(fpath), exist_ok=True)
+      with open(fpath, 'w') as f:
+        f.write(content)
+      return True
+
+    #
+    # Detect the architecture
+    #
+    logger.info("Detecting the architecture.")
+    time_start = time.time()
+    kloc = Klocalizer()
+    kloc.set_linux_krsc(linux_ksrc)
+    kloc.add_constraints([z3.Not(z3.Bool("CONFIG_BROKEN"))])
+    kloc.include_compilation_unit(srcfile)
+
+    #
+    # Find an architecture that compiles the unit
+    #
+    for arch in archs:
+      logger.info("Trying \"%s\"" % arch.name)
+      full_constraints = kloc.compile_constraints(arch)
+      model_sampler = Klocalizer.Z3ModelSampler(full_constraints)
+      is_sat, z3_model = model_sampler.sample_model()
+      if is_sat:
+        break
+    time_elapsed = time.time() - time_start
+    logger.info("TIME: Time elapsed(sec) for architecture search: %.2f" % time_elapsed)
+    # Not possible to compile with the given set of architectures
+    if not is_sat:
+      logger.warning("Could not find an architecture that compiles the unit.")
+      return Klocalizer.SourcelinePcResult.ERROR_UNSAT, None, None
+    else:
+      assert arch
+      logger.info("The unit compiles for the architecture: \"%s\"" % arch.name)
+      
+
+    #
+    # Create a config file that compiles the unit
+    #
+    config_filepath = os.path.join(linux_ksrc, ".config")
+    if not skip_kconfig_config_gen:
+      logger.info("Creating config file to compile the unit.")
+      time_start = time.time()
+      assert is_sat and (z3_model != None)
+      config_content = Klocalizer.get_config_from_model(z3_model, arch, set_tristate_m=False, allow_non_visibles=False)
+      with open(config_filepath, "w") as f:
+        f.write(config_content)
+      assert os.path.isfile(config_filepath)
+      time_elapsed = time.time() - time_start
+      logger.info("TIME: Time elapsed(sec) for creating the config file: %.2f" % time_elapsed)
+
+    else:
+      logger.info("Skipped: creating config file to compile the unit.")
+
+    #
+    # Compile the unit
+    #
+    unit_name = srcfile[:-len(".c")] + ".o"
+    if not skip_building_unit:
+      logger.info("Compiling the unit.")
+      olddefconf_cmd = ["make", "ARCH=%s" % arch.name, "olddefconfig"]
+      assert srcfile.endswith(".c") # TODO: what if this is not a sourcefile but a header file?
+
+      compile_cmd = [makecross_script, "ARCH=%s" % arch.name, "clean", build_target]
+      compile_cmd_str = " ".join(compile_cmd)
+
+      _, _, _, time_elapsed = run(olddefconf_cmd, cwd=linux_ksrc)
+      logger.info("TIME: Time elapsed(sec) for running make olddefconfig: %.2f" % time_elapsed)
+      try:
+        make_out, make_err, ret, time_elapsed = run(compile_cmd, cwd=linux_ksrc, timeout=make_timeout)
+        logger.info("TIME: Time elapsed(sec) for running make: %0.2f" % time_elapsed)
+
+        # Write make's stdout and stderr
+        if ret != 0:
+          # Might happen with warnings like unmet dependency bug. Make is
+          # said to fail if the unit cannot be found compiled.
+          logger.warning("Make returned non-zero(%s)" % ret)
+        unit_path = os.path.join(linux_ksrc, unit_name)
+        if not os.path.isfile(unit_path):
+          logger.error("Cannot find a compiled unit at \"%s\"" % unit_path)
+          write_content_to_file(compile_cmd_str +"\n"+ make_out.decode('utf-8'), make_out_path)
+          write_content_to_file(compile_cmd_str +"\n"+ make_err.decode('utf-8'), make_err_path)
+          return Klocalizer.SourcelinePcResult.ERROR_MAKE, None, None
+      except subprocess.TimeoutExpired:
+        logger.error("Timeout expired for make, duration(sec): %.2f" % make_timeout)
+        write_content_to_file(compile_cmd_str +"\n"+ "Timeout expired, duration(sec): %.2f" % make_timeout, make_out_path)
+        write_content_to_file(compile_cmd_str +"\n"+ "Timeout expired, duration(sec): %.2f" % make_timeout, make_err_path)
+        return Klocalizer.SourcelinePcResult.ERROR_MAKE_TIMEOUT, None, None
+    else:
+      logger.info("Skipped: compiling the unit.")
+
+    #
+    # Create superc config for srcfile
+    #
+    superc_config_path = os.path.join(superc_configs_dir, srcfile+".configs_superc")
+    if not skip_superc_config_gen:
+      logger.info("Creating SuperC config file.")
+      # use superc_linux_script
+      # /usr/bin/time bash $superc_linux_script -S"$superc_args" -w -L configs/ ${source_file} < /dev/null
+      import pathlib
+      pathlib.Path(superc_configs_dir).mkdir(parents=True, exist_ok=True)
+      assert os.path.isdir(superc_configs_dir)
+      config_gen_cmd = [superc_linux_script, "-w", "-x", makecross_script, "-a", arch.name, "-L", superc_configs_dir, srcfile]
+      logger.info("SuperC config gen command: \"%s\"" % " ".join(config_gen_cmd))
+      _, _, _, time_elapsed = run(config_gen_cmd, cwd=linux_ksrc)
+      logger.info("TIME: Time elapsed(sec) for SuperC config generation: %.2f" % time_elapsed)
+      assert os.path.isfile(superc_config_path)
+    else:
+      logger.info("Skipped: creating SuperC config file.")
+    
+    #
+    # Clear autoconf.h
+    #
+    logger.info("Clearing autoconf.h.")
+    autoconf_path = os.path.join(linux_ksrc, "include/generated/autoconf.h")
+    with open(autoconf_path, "w") as f: pass
+    assert os.path.isfile(autoconf_path)
+    with open(autoconf_path, "r") as f: assert not f.readlines()
+
+    #
+    # Create header file to handle IS_ENABLED() with SuperC
+    #
+    options_header_file = os.path.join(linux_ksrc, "config_options.h")
+    logger.info("Creating a temporary header file of config options at \"%s\" to handle IS_ENABLED macro." % options_header_file)
+
+    def get_superc_header_content(config_options):
+      """Given a list of config options, create and return the header
+      content to handle IS_ENABLED macro for SuperC.
+      """
+      def get_for_option(option):
+        assert option.startswith("CONFIG_")
+        ret =     "#ifdef %s" % option
+        ret += "\n#define %s 1" % option
+        ret += "\n#else"
+        ret += "\n#undef %s" % option
+        ret += "\n#endif\n"
+        return ret
+      return "\n".join([get_for_option(option) for option in config_options])
+
+    config_options = arch.get_bool_tristate_options()
+    header_content = get_superc_header_content(config_options)
+    with open(options_header_file, 'w') as f:
+      f.write(header_content)
+    assert os.path.isfile(options_header_file)
+
+    #
+    # Run SuperC
+    #
+    logger.info("Running SuperC.")
+    import tempfile
+    with tempfile.NamedTemporaryFile() as tmpfile:
+      tmpfilename = tmpfile.name
+
+      restrict_flag = " -restrictConfigToPrefix CONFIG_ " if restrict_to_config_prefix else ""
+      superc_flags = "%s -sourcelinePC %s" % (restrict_flag, tmpfilename)
+      superc_flags += " -include %s" % options_header_file
+      superc_sourcelinepc_cmd = [superc_linux_script, "-S%s" % superc_flags, "-L%s" % superc_configs_dir, srcfile]
+      superc_sourcelinepc_cmd_str = " ".join(superc_sourcelinepc_cmd)
+      logger.info("SuperC command: \"%s\"" % " ".join(superc_sourcelinepc_cmd))
+      try:
+        superc_out, superc_err, ret, time_elapsed = run(superc_sourcelinepc_cmd, cwd=linux_ksrc, timeout=superc_timeout)
+        logger.info("TIME: Time elapsed(sec) for SuperC sourceline pc computation: %0.2f" % time_elapsed)
+
+        if ret != 0:
+          # Might happen with warnings/errors where we still get some results.
+          logger.warning("SuperC returned non-zero(%s)" % ret)
+
+        superc_pcfile_content = tmpfile.read().decode()
+        if not superc_pcfile_content:
+          logger.error("Empty SuperC output.")
+          write_content_to_file(superc_sourcelinepc_cmd_str +"\n"+ superc_out.decode('utf-8'), superc_out_path)
+          write_content_to_file(superc_sourcelinepc_cmd_str +"\n"+ superc_err.decode('utf-8'), superc_err_path)
+          return Klocalizer.SourcelinePcResult.ERROR_SUPERC, arch, None
+      except subprocess.TimeoutExpired:
+        logger.error("Timeout expired for SuperC, duration(sec): %.2f" % superc_timeout)
+        write_content_to_file(superc_sourcelinepc_cmd_str +"\n"+ "Timeout expired, duration(sec): %.2f" % superc_timeout, superc_out_path)
+        write_content_to_file(superc_sourcelinepc_cmd_str +"\n"+ "Timeout expired, duration(sec): %.2f" % superc_timeout, superc_err_path)
+        return Klocalizer.SourcelinePcResult.ERROR_SUPERC_TIMEOUT, arch, None
+
+    assert superc_pcfile_content
+    assert arch
+    from ast import literal_eval
+    # return __parse_cb(literal_eval(superc_pcfile_content))
+    ret_code = Klocalizer.SourcelinePcResult.SUCCESS
+    pc = Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(literal_eval(superc_pcfile_content))
+    return ret_code, arch, pc
+
   #
   # Exceptions
   #
diff --git a/kmax/patch.py b/kmax/patch.py
new file mode 100644
index 00000000..0b47880b
--- /dev/null
+++ b/kmax/patch.py
@@ -0,0 +1,217 @@
+from common import SourceFileType, FileChangeType
+import whatthepatch
+
+def is_maybe_kernel(filepath) -> bool:
+  """Check whether the file is a kernel file based on the directory it is
+  included.
+
+  If the return value is False, it is guaranteed to be non-kernel.
+  Otherwise, it may be kernel.
+  """
+  assert filepath
+  non_kernel_dirs = ["tools", "Documentation", "usr", "LICENSES", "scripts"]
+  for non_kernel_dir in non_kernel_dirs:
+    if filepath.startswith(non_kernel_dir):
+      return False
+  return True
+
+def is_interesting_diff(diff) -> bool:
+  """Check whether the diff is an interesting change based on:
+  * C source with .c extension
+  * Change type (created, modified_only, or moved_modified)
+  * Kernel file (based on directory, checked with is_maybe_kernel())
+  """
+  assert diff
+  file_type = diff['file_type']
+  if file_type != SourceFileType.SOURCE:
+    return False
+
+  change_type = diff['change_type']
+  if change_type != FileChangeType.CREATED        and \
+     change_type != FileChangeType.MODIFIED_ONLY  and \
+     change_type != FileChangeType.MOVED_MODIFIED:
+    # otherwise, it is REMOVED or MOVED_ONLY; for which we don't create configs
+    return False
+
+  return is_maybe_kernel(diff['new_path'])
+
+def summarize_patch(patch: str, str_change_type=False) -> list:
+  """Summarize a patch and return the summary as a list of diff summary dictionaries.
+  
+  Each summary is in the following format:
+  "change_type": an instance of FileChangeType enum describing how file was changed
+  "old_path": path to the old path of the changed file (unset if change_type is CREATED)
+  "new_path": path to the new path of the changed file (unset if change_type is REMOVED)
+  "added_lines": added lines as a list of integers (unset if none)
+  "removed_lines": removed lines as a list of integers (unset if none)
+
+  Removed lines are in terms of their position in the old file while added
+  lines are in terms of their position in the new file.
+
+  Arguments:
+  patch -- Patch string to parse and summarize.
+  """
+  diff = whatthepatch.parse_patch(patch)
+
+  diff_summaries = []
+  for d in diff:
+    old_path = d.header.old_path
+    new_path = d.header.new_path
+    change_type = FileChangeType.getType(d)
+
+    added_lines = []
+    removed_lines = []
+    if d.changes:
+      for c in d.changes:
+        if c.old == None:
+          assert c.new != None
+          added_lines.append(c.new)
+        elif c.new == None:
+          assert c.old != None
+          if change_type != FileChangeType.CREATED:
+            removed_lines.append(c.old)
+        else:
+          # no change in the line, just the mapping from old to new line number
+          assert c.new != None and c.old != None
+      
+    diff_summary = {}
+    diff_summary["change_type"] = change_type.name if str_change_type else change_type
+    none_file = "/dev/null"
+    # TODO: due to https://github.com/cscorley/whatthepatch/issues/43 we are
+    # stripping the a/ and b/ prefixes, which might cause inaccuracies if the
+    # file is really in such folder.
+    def try_remove_prefix(s, prefix):
+      if s == None or prefix == None:
+        return s
+      if s.startswith(prefix):
+        return s[len(prefix):]
+      else:
+        return s
+    # old path is none_file?
+    if old_path != none_file: 
+      diff_summary["old_path"] = try_remove_prefix(old_path, "a/")
+      old_path = diff_summary["old_path"]
+    else:
+      old_path = None
+
+    if new_path != none_file:
+      diff_summary["new_path"] = try_remove_prefix(new_path, "b/")
+      new_path = diff_summary["new_path"]
+    else:
+      new_path = None
+
+    if added_lines: diff_summary["added_lines"] = added_lines
+    if removed_lines: diff_summary["removed_lines"] = removed_lines
+
+    if old_path and new_path:
+      assert SourceFileType.get_file_type(old_path) == SourceFileType.get_file_type(new_path)
+
+    # set file type
+    if old_path:
+      diff_summary["file_type"] = SourceFileType.get_file_type(old_path)
+    elif new_path:
+      diff_summary["file_type"] = SourceFileType.get_file_type(new_path)
+    else:
+      assert False
+
+    diff_summaries.append(diff_summary)
+  
+  return diff_summaries
+
+def get_lines_to_build_for_removed(added_lines, removed_lines):
+  """Get the list of lines that need building due to removed lines.
+  
+  These are the unchanged lines that used to be just above the removed lines.
+
+  As in unified diff format, added lines is the line numbers after the patch
+  is applied, and removed lines is the line numbers before the patch is applied.
+  """
+  if not removed_lines:
+    return []
+  added_lines = sorted(list(set(added_lines)))
+  removed_lines = sorted(list(set(removed_lines)))
+
+  # First, map the removed lines to the unchanged lines that need building,
+  # but line numbers in the unpatched state.
+  lines2build_unpatched = []
+  for i, line_num in enumerate(removed_lines):
+    # If the line before line_num is also removed, then they require the
+    # same unchanged line to be built. In this case, no need to add any
+    # additional line.
+    if i > 0 and removed_lines[i-1] == (line_num - 1):
+      continue
+    else:
+      # Map to the unchanged line just before this line.
+      lines2build_unpatched.append(line_num - 1)
+  
+  # lines2build_unpatched includes the line numbers "before the patch is
+  # applied". However, removing/adding lines change their position in the
+  # new file. Map them to their position in the new file.
+  # To achieve this, traverse three lists at the same time: added_lines,
+  # removed_lines, and lines2build_unpatched. Added lines require to shift
+  # forwards while removed lines require to shift backwards.
+  lines2build = []
+  shift = 0
+  added_lines_idx = 0
+  removed_lines_idx = 0
+  for l in lines2build_unpatched:
+    # For each removed line above l, shift l backwards.
+    while removed_lines_idx < len(removed_lines) and removed_lines[removed_lines_idx] < l:
+      shift -= 1
+      removed_lines_idx += 1
+    # For each line added at this point on, shift l forwards.
+    while added_lines_idx < len(added_lines) and added_lines[added_lines_idx] <= (l + shift):
+      shift += 1
+      added_lines_idx += 1
+    # Add the line by applying the shift
+    lines2build.append(l + shift)
+  assert len(lines2build) > 0 and lines2build[0] >= 0
+
+  # Edge case: if the first line is removed, it maps to line 0, which does
+  # not exist. Map it to the first line in the new file.
+  if lines2build[0] == 0:
+    lines2build[0] = 1
+  
+  return lines2build
+
+def get_target_c_lines(patch_txt: str):
+  """Given a patch file content, compute and return the C lines that need
+  building for covering the patch.
+
+  These lines are based only on parse of the patch. They include the
+  added lines, and the lines with closest proximity to the removed lines.
+  
+  Filter out files if:
+  * The file is NOT a C file (source file with .c extension)
+  * The change removes the file completely or only moves it without line changes
+  * The file is non-kernel code (based on directory they are in)
+
+  Returned mapping has the following structure:
+  {
+    "path/to/sourcefile1": [line2build_1, line2build_2, ...],
+    ...
+  }
+
+  Notice that the header files are excluded.
+  """
+  # Summarize the patch
+  patch_summary = summarize_patch(patch_txt)
+  assert patch_summary
+
+  ret = {}
+
+  for diff in patch_summary:
+    if not is_interesting_diff(diff):
+      continue
+
+    added_lines = diff.get('added_lines', [])
+    removed_lines = diff.get('removed_lines', [])
+    lines_to_build_for_removed = get_lines_to_build_for_removed(added_lines, removed_lines)
+    lines_to_build = sorted(list(set(added_lines + lines_to_build_for_removed)))
+    assert len(lines_to_build) > 0
+
+    # Add the file:lines to the results
+    patched_path = diff['new_path']
+    ret[patched_path] = lines_to_build
+
+  return ret
diff --git a/kmax/superc.py b/kmax/superc.py
new file mode 100644
index 00000000..b24b9bf8
--- /dev/null
+++ b/kmax/superc.py
@@ -0,0 +1,764 @@
+from common import BasicLogger
+from vcommon import run, write_content_to_file, check_if_compiles
+from kmax.arch import Arch
+import os
+import pathlib
+from shutil import which
+from kmax.klocalizer import Klocalizer
+import subprocess
+import shutil
+
+class SuperC:
+  class SuperC_Exception(Exception):
+    pass
+  class SuperC_ChecksFailed(SuperC_Exception):
+    def __init__(self, reason):
+      self.reason = reason
+      super().__init__(self.reason)
+
+  def __init__(self, superc_linux_script_path = None, logger = BasicLogger()):
+    """Arguments:
+    * superc_linux_script_path -- SuperC linux script, which is found at
+    superc/scripts/superc_linux.sh, where superc/ is the top SuperC source
+    directory. Searches "superc_linux.sh" in PATH by default.
+    """
+    self.logger = logger
+
+    # Set SuperC linux script path
+    if superc_linux_script_path:
+      self.superc_linux_script_path = superc_linux_script_path
+    else: #< Searches in PATH by default.
+      self.superc_linux_script_path = "superc_linux.sh"
+    assert self.superc_linux_script_path
+
+    self.__check_superc() #< Check SuperC
+  
+  def __check_superc(self):
+    """Check and whether SuperC can be used for getting sourceline presence
+    conditions for Linux files.
+    
+    Returns on success.
+    Raises SuperC_ChecksFailed exception on error.
+
+    Followings checks are done:
+    * java exists
+    * java runs
+    * SuperC runs
+    * SuperC -sourcelinePC runs
+    * SuperC linux script exists
+    * SuperC linux script runs
+    """
+    def is_success(command_to_run: list):
+      return 0 == run(command_to_run, capture_stdout=True, capture_stderr=True)[2]
+    
+    self.logger.debug("Starting SuperC checks.\n")
+
+    #
+    # Check java
+    #
+    if not which("java"):
+      raise SuperC.SuperC_ChecksFailed("java could not be found")
+
+    cmd = ["java", "--help"]
+    if not is_success(cmd):
+      raise SuperC.SuperC_ChecksFailed("Running java (\"%s\") failed" % " ".join(cmd))
+
+    #
+    # Check SuperC
+    #
+    cmd = ["java", "superc.SuperC"]
+    if not is_success(cmd):
+      raise SuperC.SuperC_ChecksFailed("Running SuperC (\"%s\") failed" % " ".join(cmd))
+
+    cmd = ["java", "superc.SuperC", "-sourcelinePC", os.devnull, os.devnull]
+    if not is_success(cmd):
+      raise SuperC.SuperC_ChecksFailed("Running SuperC -sourcelinePC (\"%s\") failed" % " ".join(cmd))
+    
+    #
+    # Check SuperC linux script
+    #
+    if not which(self.superc_linux_script_path):
+      raise SuperC.SuperC_ChecksFailed(
+        """SuperC linux script executable cannot be found: either set """
+        """path to the script or have script in PATH.""")
+
+    cmd = [self.superc_linux_script_path]
+    if not is_success(cmd):
+      raise SuperC.SuperC_ChecksFailed("Executing SuperC linux script (\"%s\") failed" % cmd)
+    
+    # None failed: checks passed
+    self.logger.debug("SuperC checks passed.\n")
+    return True
+
+  @staticmethod
+  def get_superc_basepath_for_file(srcfile: str, superc_formulas_dir: str) -> str:
+    """The basepath, which is concat with extensions to create any kind
+    of files specific to the srcfile.
+    """
+    return os.path.join(superc_formulas_dir, srcfile)
+  
+  @staticmethod
+  def get_superc_logs_dir_for_file(srcfile: str, superc_formulas_dir: str) -> str:
+    """The directory, which is concat with log filenames to create any kind
+    of logs files specific to the given srcfile.
+    """
+    return os.path.join(superc_formulas_dir, "%s_superc_logs/" % srcfile)
+
+  @staticmethod
+  def get_superc_configs_for_file(srcfile: str, superc_formulas_dir: str) -> str:
+    """Compute and return the path to the SuperC config file for the given
+    source file.
+    """
+    return os.path.join(superc_formulas_dir, "%s.configs_superc" % srcfile)
+
+  @staticmethod
+  def get_superc_formulas_dir(formulas: str, arch_name: str) -> str:
+    """Given formulas directory and the architecture name, return the
+    path to SuperC formulas directory.
+
+    For example, formulas=".kmax/v5.13" and arch_name="x86_64" returns
+    ".kmax/v5.13/superc/x86_64/configs/".
+    
+    While this is a simple string concatenation, any changes to directory
+    structure will be maintained through this method.
+    """
+    assert arch_name
+    return os.path.join(formulas, "superc", arch_name, "configs")
+  
+  @staticmethod
+  def get_superc_pc_path(srcfile: str, superc_formulas_dir: str) -> str:
+    """Compute and return the path to the presence conditions file for the
+    given source file. Notice that we have no (efficient) way of checking
+    whether the given presence conditions file is up-to-date. Therefore,
+    this file is always recomputed/replaced as needed, and should be used
+    for diagnostic purposes only.
+
+    Otherwise, the path structure is maintained here.
+    """
+    return os.path.join(superc_formulas_dir, "%s.pc" % srcfile)
+  
+  @staticmethod
+  def get_superc_header_path(superc_formulas_dir: str) -> str:
+    """Get the path to the SuperC header file.
+    """
+    return os.path.join(superc_formulas_dir, "config_options.h")
+  
+  @staticmethod
+  def get_superc_header_content(config_options: list):
+    """Given a list of config options, create and return the header
+    content to handle IS_ENABLED macro for SuperC.
+    TODO: document more
+    """
+    def get_for_option(option):
+      assert option.startswith("CONFIG_")
+      ret =     "#ifdef %s" % option
+      ret += "\n#define %s 1" % option
+      ret += "\n#else"
+      ret += "\n#undef %s" % option
+      ret += "\n#endif\n"
+      return ret
+    return "\n".join([get_for_option(option) for option in config_options])
+
+  def get_pc(self,
+    srcfile_path: str, arch: Arch, linux_ksrc: str,
+    superc_formulas_dir: str, superc_timeout_sec: int,
+    logger) -> Klocalizer.ConditionalBlock:
+    """
+    Compute the presence conditions (pc) using SuperC, and return it as a
+    ConditionalBlock instance.
+
+    Arguments:
+    * srcfile_path -- Path to the source file to compute the pc for.
+    Relative to the top Linux source directory.
+    * arch -- Target architecture as an instance of kmax.Arch.
+    * linux_ksrc -- Top Linux source directory.
+    * superc_formulas_dir -- Path to the SuperC formulas directory. To use
+    the cache dir structure, get it using SuperC.get_superc_formulas_dir().
+    * superc_timeout_sec -- Timeout amount for running SuperC in seconds.
+    * logger -- Logger that implements common.VoidLogger interface.
+    
+    Returns:
+    * On success: A ConditionalBlock instance, which is a dummy root that
+    encapsulates the conditional blocks in the source file. The root has
+    special start/end line values (0 and line_count + 1).
+    * On error: None. Check the log messages for info. For advanced
+    diagnostics, check the diagnostic files created in the SuperC formulas
+    directory.
+
+    Creates the following files for diagnostics (for full path, prefix each
+    with "superc/formulas/dir///source/file/path"):
+    * Always:
+       * PREFIX.superc_sourcelinepc_cmd: SuperC command.
+    * On completion without timeout:
+       * PREFIX.superc_sourcelinepc_exit_code: SuperC exit code.
+       * PREFIX.superc_sourcelinepc_out: SuperC stdout.
+       * PREFIX.superc_sourcelinepc_err: SuperC stderr.
+       * PREFIX.superc_sourcelinepc_time_elapsed: SuperC time elapsed in sec.
+    * On time out:
+       * PREFIX.superc_sourcelinepc_timed_out: Timeout duration in sec.
+
+    Notes:
+    * SuperC config files must exist for the source file in the SuperC
+    formulas directory. Otherwise, it is error (returns None).
+    * Retrieves the config options header file (or creates it at if does
+    not exist) from the path produced by SuperC.get_superc_header_path().
+    * We have no (efficient) way of knowing whether an existing pc file
+    is up-to-date. Therefore, we don't keep a cache, and always replace
+    the pc file that may exists in the formulas directory, and keep the old
+    one with .old suffix. This file must be used for diagnostic purposes
+    only.
+    * "include/generated/autoconf.h" is cleared in the Linux source, and
+    not restored.
+    """
+    assert os.path.isfile(os.path.join(linux_ksrc, srcfile_path))
+    # Check that configs exist
+    configs_file = self.get_superc_configs_for_file(srcfile_path, superc_formulas_dir)
+    if not os.path.isfile(configs_file):
+      logger.error("Cannot find SuperC configs file at \"%s\"." % configs_file)
+      return None #< Error
+
+    assert os.path.isfile(configs_file)
+    logs_dir = SuperC.get_superc_logs_dir_for_file(srcfile_path, superc_formulas_dir)
+    def logpath(f: str):
+      return os.path.join(logs_dir, f)
+    pathlib.Path(logs_dir).mkdir(parents=True, exist_ok=True)
+
+    #
+    # Clear autoconf.h
+    #
+    logger.debug("Clearing autoconf.h.\n")
+    autoconf_path = os.path.join(linux_ksrc, "include/generated/autoconf.h")
+    with open(autoconf_path, "w") as f:
+      pass #< Remove the content but keep the file
+    assert os.path.isfile(autoconf_path)
+    with open(autoconf_path, "r") as f:
+      assert not f.readlines() #< Verify that file is empty.
+
+    #
+    # Retrieve or create header file to handle IS_ENABLED() with SuperC
+    #
+    options_header_file = SuperC.get_superc_header_path(linux_ksrc)
+    if os.path.isfile(options_header_file):
+      logger.debug("Options header file for handling IS_ENABLED macro is found at \"%s\"\n" % options_header_file)
+    else:
+      logger.debug("Computing options header file content to handle IS_ENABLED macro.\n")
+      config_options = arch.get_bool_tristate_options()
+      header_content = SuperC.get_superc_header_content(config_options)
+      assert header_content
+      logger.debug("Writing the options header file to \"%s\".\n" % options_header_file)
+      with open(options_header_file, 'w') as f:
+        f.write(header_content)
+      assert os.path.isfile(options_header_file)
+
+    #
+    # SuperC sourcelinePC
+    #
+    pc_file_path = SuperC.get_superc_pc_path(srcfile_path, superc_formulas_dir)
+    logger.debug("Presence conditions file will be created at \"%s\".\n" % pc_file_path)
+
+    # If a pc file already exists, rename it to have .old extension
+    if os.path.isfile(pc_file_path):
+      old_pc_file_path = pc_file_path + ".old"
+      logger.debug("Moving the existing presence conditions file to \"%s\".\n" % old_pc_file_path)
+      assert pathlib.Path(pc_file_path).rename(old_pc_file_path)
+      assert not os.path.isfile(pc_file_path)
+      assert os.path.isfile(old_pc_file_path)
+    
+    # Prepare the SuperC command
+    superc_flags = "-sourcelinePC %s" % pc_file_path
+    superc_flags += " -include %s" % options_header_file
+    # TODO: restrict to the list of config options instead of given prefix
+    restrict_flag = " -restrictConfigToPrefix CONFIG_ "
+    superc_flags += restrict_flag
+    superc_sourcelinepc_cmd = [self.superc_linux_script_path, "-S%s" % superc_flags, "-L%s" % superc_formulas_dir, srcfile_path]
+    superc_sourcelinepc_cmd_str = " ".join(superc_sourcelinepc_cmd)
+    logger.debug("SuperC command: \"%s\"\n" % " ".join(superc_sourcelinepc_cmd))
+    write_content_to_file(logpath("superc_sourcelinepc_cmd"), str(superc_sourcelinepc_cmd_str) + '\n')
+
+    # Run SuperC
+    try:
+      logger.debug("Running SuperC sourcelinePC.\n")
+      out, err, ret, time_elapsed = run(superc_sourcelinepc_cmd, cwd=linux_ksrc, timeout=superc_timeout_sec)
+      logger.debug("Finished running SuperC sourcelinePC.\n")
+
+      # Write diagnostic information
+      write_content_to_file(logpath("superc_sourcelinepc_exit_code"), str(ret) + '\n')
+      write_content_to_file(logpath("superc_sourcelinepc_out"), str(out.decode('UTF-8')) + '\n')
+      write_content_to_file(logpath("superc_sourcelinepc_err"), str(err.decode('UTF-8')) + '\n')
+      write_content_to_file(logpath("superc_sourcelinepc_time_elapsed"), str(time_elapsed) + '\n')
+      logger.debug("SuperC config creation diagnostic info was written to files.\n")
+
+      # Did SuperC create a presence conditions file?
+      if not os.path.isfile(pc_file_path):
+        logger.debug("SuperC failed to create presence conditions file at \"%s\".\n" % pc_file_path)
+        return None #< Error
+      
+      # Read the presence conditions file
+      with open(pc_file_path, 'r') as f:
+        superc_pcfile_content = f.read()
+      
+      # If file is empty, error
+      if not superc_pcfile_content:
+        logger.debug("Empty SuperC presence conditions file at \"%s\".\n")
+        return None #< Error
+      
+      # Parse the ConditionalBlock instance and return
+      from ast import literal_eval
+      pc = Klocalizer.ConditionalBlock._ConditionalBlock__parse_cb(literal_eval(superc_pcfile_content))
+      assert pc
+      return pc
+    except subprocess.TimeoutExpired: #< SuperC timed out
+      logger.debug("Timeout expired for SuperC, duration(sec): %.2f\n" % superc_timeout_sec)
+
+      # Write diagnostic information
+      write_content_to_file(logpath("superc_sourcelinepc_timed_out"), str(superc_timeout_sec) + '\n')
+
+      return None #< Error
+    
+    assert False #< Unreachable
+
+  def create_superc_config_on_built_unit(self,
+    srcfile_path: str, output_superc_configs_dir_path: str,
+    linux_ksrc: str, arch_name: str, cross_compiler: str) -> list:
+    """Create SuperC configs files for the given source file where the unit
+    is already built and building configuration is in the Linux source.
+
+    This method only runs the SuperC linux script for creating the SuperC
+    configuration files, and assumes the Linux source is already ready
+    for this operation. Here are the requirements:
+    * A compiled binary for the source file must exist in the same
+    directory as the source file.
+    * The linux configuration file that compiled the source file must exist
+    at linux_ksrc/.config.
+
+    The method Klocalizer.localize_config() can help setting up the Linux
+    source before running this method. Alternatively, use
+    SuperC.create_linux_superc_configs_from_scratch() that handles both the
+    setup and the SuperC configuration creation.
+
+    Arguments:
+    * srcfile_path -- A linux source file with '.c' extension. It must be
+    already compiled, i.e., corresponding binary with '.o' extension must
+    exist. Relative to linux_ksrc.
+    * output_superc_configs_dir_path -- Output SuperC configs directory
+    path. Convention is to use SuperC.get_superc_configs_dir() to obtain
+    this. Configs are created as src/file/path.configs_{all,superc}. Config
+    must not already exist.
+    * linux_ksrc -- Path to the top Linux source directory.
+    * arch_name -- Architecture name, e.g., "x86_64".
+    * cross_compiler -- Executable cross_compiler, e.g., "make.cross".
+
+    Returns a tuple of 5 values:
+    * bool: Whether SuperC config files were successfully created.
+    * int : SuperC linux script return code.
+    * str : SuperC linux script stdout.
+    * str : SuperC linux script stderr.
+    * int : Time elapsed (sec) to run SuperC linux script.
+    """
+    #
+    # Check arguments
+    #
+    assert srcfile_path
+    assert srcfile_path.endswith(".c")
+    assert os.path.isfile(os.path.join(linux_ksrc, srcfile_path))
+    assert os.path.isdir(output_superc_configs_dir_path)
+    assert os.path.isdir(linux_ksrc)
+    assert arch_name
+    assert isinstance(arch_name, str)
+    assert which(cross_compiler)
+    # The linux configuration file that compiled the source file must exist
+    # at linux_ksrc/.config
+    assert os.path.isfile(os.path.join(linux_ksrc, ".config"))
+    superc_config_path = os.path.join(output_superc_configs_dir_path, "%s.configs_superc" % srcfile_path)
+    assert not os.path.isfile(superc_config_path) #< SuperC config does not already exist.
+
+    # Check that unit is compiled
+    unit_path = "%s.o" % srcfile_path[:-len('.c')]
+    assert os.path.isfile(os.path.join(linux_ksrc, unit_path))
+
+    # Create the SuperC configs.
+    self.logger.debug("Creating SuperC configs for \"%s\"\n" % srcfile_path)
+    # use superc_linux_script
+    # /usr/bin/time bash $superc_linux_script -S"$superc_args" -w -L configs/ ${source_file} < /dev/null
+    config_gen_cmd = [self.superc_linux_script_path, "-w",
+      "-x", cross_compiler, "-a", arch_name,
+      "-L", output_superc_configs_dir_path, srcfile_path]
+    self.logger.debug("SuperC config generation command: \"%s\"\n" % " ".join(config_gen_cmd))
+    out, err, ret, time_elapsed = run(config_gen_cmd, cwd=linux_ksrc)
+    self.logger.debug("TIME: Time elapsed(sec) for SuperC config generation: %.2f\n" % time_elapsed)
+    config_created = os.path.isfile(superc_config_path)
+    if config_created:
+      self.logger.debug("SuperC configs creation was successful for \"%s\"\n" % srcfile_path)
+    else:
+      self.logger.debug("Failed to create SuperC configs for \"%s\"\n" % srcfile_path)
+
+    return config_created, ret, out.decode('UTF-8'), err.decode('UTF-8'), time_elapsed
+
+  def ensure_superc_config(self,
+    srcfile: str, output_superc_configs_dir_path: str, linux_ksrc: str,
+    arch: Arch, cross_compiler, build_targets, compile_jobs, build_timeout,
+    logger):
+    """
+    Ensure that SuperC configs exist for the input sourcefile.
+
+    First, check if it already exists.  Otherwise, attempt to create it by
+    following the below steps:
+    * Localize a .config file that builds the unit,
+    * Compile the unit,
+    * Create SuperC configuration for the unit.
+
+    If the config is found, or otherwise successfully created, returns True.
+    Otherwise, returns False.
+    """
+    assert os.path.exists(os.path.join(linux_ksrc, srcfile))
+    assert srcfile.endswith('.c')
+    unit = srcfile[:-len('.c')] + '.o'
+
+    logs_dir = SuperC.get_superc_logs_dir_for_file(srcfile, output_superc_configs_dir_path)
+    def logpath(f: str):
+      return os.path.join(logs_dir, f)
+    pathlib.Path(logs_dir).mkdir(parents=True, exist_ok=True)
+    superc_config_file = SuperC.get_superc_configs_for_file(srcfile, output_superc_configs_dir_path)
+    config_exists = os.path.isfile(superc_config_file)
+    if config_exists:
+      # All have their SuperC configuration files.
+      logger.debug("SuperC config exists for \"%s\".\n" % srcfile)
+      return True
+    else:
+      logger.debug("Creating SuperC config file for \"%s\".\n" % srcfile)
+
+      #
+      # Localize a building configuration file.
+      #
+      output_config_file = logpath("kloc_localized_config")
+      ret_status, ret_arch, ret_exception = Klocalizer.localize_config([unit], output_config_file, linux_ksrc, [arch], logger)
+      # Write diagnostic info
+      write_content_to_file(logpath("kloc_config_loc_status"), str(ret_status) + '\n')
+      # no need to write ret_arch: there is already a single architecture
+      write_content_to_file(logpath("kloc_config_loc_exception"), repr(ret_exception) + '\n')
+
+      is_config_created = ret_status == Klocalizer.Ret_LocalizeConfig.SUCCESS
+      if not is_config_created:
+        logger.debug("Failed to localize a building Linux .config file.\n")
+        return False
+      else:
+        assert os.path.isfile(output_config_file)
+        logger.debug("A building Linux .config file was localized.\n")
+      
+      # Check if the unit compiles (also build them to prep for SuperC config creation)
+      logger.debug("Attempting to build the unit.\n")
+      ret = check_if_compiles([unit], output_config_file, arch.name, linux_ksrc,
+        build_targets, cross_compiler, compile_jobs, build_timeout, True, logger)
+      is_unit_compiled, make_timed_out, make_ret, make_out, make_err, time_elapsed = ret
+      write_content_to_file(logpath("build_unit_status"), str(is_unit_compiled) + '\n')
+      write_content_to_file(logpath("build_unit_make_timed_out"), str(make_timed_out) + '\n')
+      write_content_to_file(logpath("build_unit_make_ret"), str(make_ret) + '\n')
+      write_content_to_file(logpath("build_unit_make_out"), str(make_out) + '\n')
+      write_content_to_file(logpath("build_unit_make_err"), str(make_err) + '\n')
+      write_content_to_file(logpath("build_unit_time_elapsed"), str(time_elapsed) + '\n')
+      if not is_unit_compiled:
+        logger.debug("Unit could not be compiled.\n")
+        return False
+      else:
+        logger.debug("Unit was successfully compiled.\n")
+
+      # Create missing SuperC config files
+      logger.debug("Creating the missing SuperC config file.\n")
+      pathlib.Path(output_superc_configs_dir_path).mkdir(parents=True, exist_ok=True)
+      assert shutil.copy(output_config_file, os.path.join(linux_ksrc, ".config"))
+      ret = self.create_superc_config_on_built_unit(srcfile, output_superc_configs_dir_path, linux_ksrc, arch.name, cross_compiler)
+      config_created, superc_ret, superc_out, superc_err, time_elapsed = ret
+      write_content_to_file(logpath("superc_config_gen_status"), str(config_created) + '\n')
+      write_content_to_file(logpath("superc_config_gen_ret"), str(superc_ret) + '\n')
+      write_content_to_file(logpath("superc_config_gen_out"), str(superc_out) + '\n')
+      write_content_to_file(logpath("superc_config_gen_err"), str(superc_err) + '\n')
+      write_content_to_file(logpath("superc_config_gen_time_elapsed"), str(time_elapsed) + '\n')
+      if not config_created:
+        logger.error("SuperC configuration generation failed\n")
+        return False
+
+      # All succeeded.
+      config_exists = os.path.isfile(superc_config_file)
+      assert config_exists
+      return True
+
+###########################################################################
+
+#
+# Static analysis of C source files without SuperC
+#
+class SyntaxAnalysis:
+    # taken from plocalizer/scripts/create_validation_conditions.py
+    # TODO: merge this ConditionalBlock implementation with Klocalizer.ConditionalBlock
+    class ConditionalBlock:
+      """For capturing the start/end of preprocessor conditional blocks."""
+      def __init__(self):
+        self.start_line = -1
+        self.end_line   = -1
+        self.sub_block_groups = []
+      
+      def getdict(self):
+        """Get a dictionary representation of the conditional block.
+        
+        May be used for debugging purposes."""
+        r = {}
+        r["StartLine"] = self.start_line
+        r["EndLine"] = self.end_line
+        r["Sub"] = []
+        for s in self.sub_block_groups:
+          r["Sub"].append([k.getdict() for k in s])
+        return r
+
+      def retrieve_deepest_block(self, line : int): # -> ConditionalBlock
+        """Retrieve the end line of the deepest encapsulating conditional block
+        for the given line.
+
+        If there is no such block (line is out of range of the conditional
+        blocks), return None.
+
+        This should always return valid values when called with a valid line
+        number on a conditional block tree with a dummy root for covering the
+        overall file.
+        """
+        # TODO: Search for multiple lines can be optimized by doing a
+        # traversal for all lines.
+        assert line >= 0
+
+        # For the given line, retrieve the end-of-block line that it belongs to.
+        if self.start_line <= line < self.end_line:
+          # Search within the sub blocks
+          ret_from_sub_blocks = []
+          for s in self.sub_block_groups:
+            for k in s:
+              r = k.retrieve_deepest_block(line)
+              if r is not None:
+                ret_from_sub_blocks.append(r)
+          # It may belong to at most one sub block
+          assert len(ret_from_sub_blocks) <= 1
+
+          if ret_from_sub_blocks:
+            # Belongs to a sub block
+            return ret_from_sub_blocks[0]
+          else:
+            # Belongs to self, not in any nested sub block
+            return self
+        else:
+          return None
+
+    # taken from plocalizer/scripts/eval_common.py
+    @staticmethod
+    def get_tokens(s):
+        """
+        TODO: document
+        takes a string, and returns a list of (token, line #)
+        """
+        buf = ""
+        token_list = []
+        line_num = 1
+        prev_char = ''
+        for c in s:
+            # append the existing buffered token when we reach a space or tab
+            if c == ' ' or c == '\t':
+                if buf != "":
+                    token_list.append((buf, line_num))
+                    buf = ""
+            else:
+                # append the existing token if we reach a newline character, and increment the line number counter.
+                if c == '\n':
+                    if buf != "":
+                        token_list.append((buf, line_num))
+                        buf = ""
+                    line_num += 1 # TODO: make this function return a list of tokens with their line numbers.
+                # logic for special characters (comments, strings, and preprocessor directives)
+                # appends the existing buffered token, then appends the special character(s) as new tokens.
+                elif c == '#' or c == '\'' or c == '"' or c == '\\' or (c == '/' and prev_char == '/') or (prev_char == '/' and c == '*') or (prev_char == '*' and c == '/'):
+                    if buf != '/' and buf != '*' and buf != "":
+                        token_list.append((buf, line_num))
+                        buf = ""
+                    buf += c
+                    token_list.append((buf, line_num))
+                    buf = ""
+                # the next character could be /, so we want to start a new token just for this.
+                elif c == '*' or c == '/':
+                    if buf != "":
+                        token_list.append((buf, line_num))
+                        buf = ""
+                    buf += c
+                # if the current character is not special in any way, then we just add it to the buffer.
+                else:
+                    buf += c
+            # keep track of the previous character, so we can determine when we have /*, */, or //
+            prev_char = c
+
+        # ensure that we catch the final string
+        if buf != "":
+            token_list.append((buf, line_num))
+        return token_list
+
+    @staticmethod
+    def analyze_c_tokens(tokens_w_line_nums):
+        """
+        TODO: document
+        determines what kind of code each token is (c, comment, or preprocessor).
+        returns a map between line number and a list of (token mapped to type of code)
+        """
+        analyzed_tokens = {}
+
+        in_quotes = False
+        in_single_line_comment = False
+        in_preprocessor = False
+        prev_line_num = 0
+        in_comment = False
+        continued_preprocessor = False
+        for token, line_num in tokens_w_line_nums:
+            if len(token) < 1:
+                continue
+            if line_num == prev_line_num:
+                pass
+            else:
+                if not continued_preprocessor:
+                    in_preprocessor = False
+                if in_single_line_comment:
+                    in_comment = False
+                    in_single_line_comment = False
+                analyzed_tokens[line_num] = []
+
+            # preprocessor check
+            if (not in_comment) and (not in_quotes) and token[0] == '#':
+                in_preprocessor = True
+
+            # NOTE: this gets tricky.
+            # 1. if we start quotes while already in a comment or preprocessor, then it's still a comment.
+            # 2. if we start a comment or preprocessor while already in quotes, then it's still quotes.
+
+            # invert the quote status whenever we reach a new quote
+            if (not in_preprocessor) and (not in_comment) and ("\"" in token):
+                in_quotes = not in_quotes
+
+            if (not in_quotes) and (not in_comment) and ("//" in token):
+                in_single_line_comment = True
+                in_comment = True
+
+            if (not in_quotes) and (not in_comment) and ("/*" in token):
+                in_comment = True
+
+            # add the token with code type
+            if in_comment:
+                analyzed_tokens[line_num].append({token: "comment"})
+            elif in_preprocessor:
+                analyzed_tokens[line_num].append({token: "preprocessor"})
+            else:
+                analyzed_tokens[line_num].append({token: "c"})
+
+            if in_comment and ("*/" in token):
+                in_comment = False
+
+            if token == '\\':
+                continued_preprocessor = True
+            else:
+                continued_preprocessor = False
+
+            prev_line_num = line_num
+        return analyzed_tokens
+
+    # taken from plocalizer/scripts/create_validation_conditions.py
+    @staticmethod
+    def get_conditional_blocks(src_content, line_count):
+        """Output conditional block is the dummy root with special start/end
+        values, which covers any conditional blocks in the file.
+        """
+        assert src_content
+
+        # Analyze the tokens to get preprocessor tokens
+        tokens = SyntaxAnalysis.get_tokens(src_content)
+        categorized_tokens = SyntaxAnalysis.analyze_c_tokens(tokens)
+
+        # Root is the one that is not due to any preprocessor directives, but the
+        # encapsulating block with condition 1. 
+        root_conditional_block = SyntaxAnalysis.ConditionalBlock()
+        root_conditional_block.start_line = 0 #< Special value
+        root_conditional_block.end_line = line_count + 1 #< Special value
+        stack = [root_conditional_block]
+
+        # Conditional blocks have a stack-like structure. The above stack helps
+        # us to keep track of the current context. For example, if a opening for
+        # a conditional block is seen, it is nested under the block at the
+        # top the stack.
+
+        for linenum in categorized_tokens:
+          for i, token_to_type in enumerate(categorized_tokens[linenum]):
+            # Get the token and its type
+            assert len(token_to_type) == 1 #< One token mapped to its type.
+            token = list(token_to_type.keys())[0]
+            token_type = token_to_type[token]
+
+            # Check if it is a conditional preprocessor directive
+            if token == '#' and token_type == 'preprocessor':
+              # Beginning of a new preprocessor directive, read the next token
+              # to see if it is a conditional preprocessor directive.
+              # Assumption: preprocessor directives like #if are not broken into
+              # two lines right after the # sign (# \ if).
+              next_token_to_type = categorized_tokens[linenum][i + 1]
+              assert len(next_token_to_type) == 1
+              next_token = list(next_token_to_type.keys())[0]
+              next_token_type = next_token_to_type[next_token]
+              assert next_token_type == "preprocessor"
+              if next_token not in ['if', 'ifdef', 'ifndef', 'elif', 'else', 'endif']:
+                # Not a conditional preprocessor directive
+                continue
+              
+              if next_token in ['if', 'ifdef', 'ifndef']:
+                # Open a new conditional block
+                new_cb = SyntaxAnalysis.ConditionalBlock()
+                new_cb.start_line = linenum
+                stack[-1].sub_block_groups.append([new_cb])
+                stack.append(new_cb)
+              elif next_token in ['elif', 'else']:
+                # Close the currently open conditional block.
+                last_cb = stack[-1]
+                last_cb.end_line = linenum
+                stack.pop()
+
+                # Open a new one in the same block group as the closed one.
+                new_cb = SyntaxAnalysis.ConditionalBlock()
+                new_cb.start_line = linenum
+                parent_cb = stack[-1]
+                parent_cb.sub_block_groups[-1].append(new_cb)
+                stack.append(new_cb)
+              elif next_token == 'endif':
+                # Close the currently open conditional block.
+                last_cb = stack[-1]
+                last_cb.end_line = linenum
+                stack.pop()
+              else:
+                assert False
+
+        # There must remain only one element, which is the dummy root
+        assert len(stack) == 1
+        return stack[0]
+    
+    @staticmethod
+    def get_conditional_blocks_of_file(srcfile_path: str) -> ConditionalBlock:
+      """Returns a ConditionalBlock instance with the dummy root. Anything
+      inside the root node is unconditional.  Children nodes depict blocks
+      under conditional preprocessor directives, but the actual conditions
+      are not set since this is only a syntax analysis.
+      """
+      assert os.path.isfile(srcfile_path)
+
+      # Read the source file.
+      with open(srcfile_path, 'r') as f:
+        content = f.read()
+      # Read the line count
+      # Old method was to count the '\n' in source content but this failed
+      # for a file (commit 88f8575bca5f, drivers/gpu/drm/amd/amdgpu/gfx_v9_4_2.c)
+      # probably because there was no newline at the end of the file. Use
+      # the file system to count the lines as below, which is safer.
+      with open(srcfile_path, 'r') as f:
+        line_count = len(f.readlines())
+
+      # Get the conditional blocks (start-end lines).
+      # Root has the special start/end values: 0 and line_count+1
+      cb = SyntaxAnalysis.get_conditional_blocks(content, line_count)
+
+      return cb
diff --git a/kmax/vcommon.py b/kmax/vcommon.py
index 9ccb454f..79b4791e 100644
--- a/kmax/vcommon.py
+++ b/kmax/vcommon.py
@@ -4,9 +4,183 @@
 import subprocess as sp
 import operator
 import inspect
+from shutil import which
 
 import logging
 
+def write_content_to_file(filepath: str, content: str):
+    with open(filepath, 'w') as f:
+        f.write(content)
+
+def get_build_system_id(linux_ksrc: str) -> str:
+    """Given path to the top Linux source directory, compute a 12 chars
+    build system identifier.
+
+    Following command is run in linux_ksrc:
+    find . -type f -regex '.*\(Makefile\|Kconfig\|Kbuild\).*' -exec md5sum {} \; | sort | md5sum | head -c 12
+    """
+    # Check arguments
+    assert os.path.isdir(linux_ksrc)
+    assert which("find")
+    assert which("sort")
+    assert which("md5sum")
+    assert which("head")
+
+    # Compute build system id
+    cmd = "find . -type f -regex '.*\(Makefile\|Kconfig\|Kbuild\).*' -exec md5sum {} \; | sort | md5sum | head -c 12"
+    out, _, ret, _ = run(cmd, cwd=linux_ksrc, shell=True)
+    assert ret == 0
+    id = out.decode('utf-8').lower()
+    assert len(id) == 12
+    assert id.isalnum()
+    return id
+
+def run(args, stdin=None, capture_stdout=True, capture_stderr=True, cwd=None, timeout=None, shell=False):
+  """Helper for running an external process.
+  Returns a tuple of (stdout, stderr, return_code, time_elapsed) for the process.
+  Arguments:
+  args -- args, a list to pass to subprocess.Popen.
+  stdin -- The content to be passed as stdin to the process.
+  capture_stdout -- If set, capture stdout to be returned by the method. Otherwise, keep it at stdout.
+  capture_stderr -- If set, capture stderr to be returned by the method. Otherwise, keep it at stdin.
+  cwd -- Current working directory for the process.
+  timeout -- timeout in seconds. If expires, raises an subprocess.TimeoutExpired exception.
+  """
+  import subprocess
+  import time
+  stdout_param = subprocess.PIPE if capture_stdout else None
+  stderr_param = subprocess.PIPE if capture_stderr else None
+  time_start = time.time()
+  popen = subprocess.Popen(args, stdin=subprocess.PIPE, stdout=stdout_param, stderr=stderr_param, cwd=cwd, shell=shell)
+  if stdin != None: popen.stdin.write(stdin)
+  captured_stdout, captured_stderr = popen.communicate(timeout=timeout)
+  time_elapsed = time.time() - time_start
+  popen.stdin.close()
+  
+  return captured_stdout, captured_stderr, popen.returncode, time_elapsed
+
+def is_linux_dir(linux_ksrc: str) -> bool:
+    """Return whether the given is a path to a top Linux source directory.
+
+    Checks are incomplete but good for sanity checks.
+    TODO: improve checks (check for certain files, attempt make kernelversion)
+    """
+    return os.path.isdir(linux_ksrc)
+
+# TODO: improvement idea: decouple everything about compilation checks including the line checker.
+def check_if_compiles(unit_paths: list, config_path: str, arch_name: str,
+    linux_ksrc: str, build_targets: dict, cross_compiler: str, jobs: int,
+    build_timeout_sec, use_olddefconfig_target: bool, logger) -> bool:
+    """Check whether the given units compile with the given configuration
+    file.
+
+    Arguments:
+    * unit_paths -- List of unit paths (e.g., ['kernel/fork.o', 'kernel/cpu.o']).
+    Paths are relative to the top Linux source directory.
+    * config_path -- Path to input Linux configuration file to use.
+    * arch_name -- Name of the architecture (e.g., x86_64)
+    * linux_ksrc -- Path to a top linux source directory.
+    * build_targets -- Unit path to build target mapping. Defaults to unit path.
+    * cross_compiler -- Executable cross compiler script (e.g., make.cross)
+    * jobs -- Num jobs for make (passed with -j). None or <=0 are infinite.
+    * build_timeout_sec -- Timeout in seconds for compilation. Pass None
+    for no timeout constraints.
+    * use_olddefconfig_target -- Whether to include olddefconfig in the
+    build targets.
+    * logger -- Logger that implements common.VoidLogger interface.
+
+    Returns: a tuple of 6 values:
+    1. List[bool] : Whether the units could be found at unit paths after
+    compilation. One bool value per unit path. If all are True, it means
+    compiled binaries can be found for all units.
+    2. bool : Whether make timed out.
+    3. int  : make return code. None if make timed out.
+    4. str  : make stdout. None if make timed out.
+    5. str  : make stderr. None if make timed out.
+    6. float: Time elapsed for running make. None if make timed out.
+
+    Whether the units could be compiled with the config file.
+    The signal for successful compilation is whether units exist at unit
+    path.  
+
+    Notes:
+    * The make target "clean" is included as the first target.
+    * The Linux source directory is NOT cleaned after the compilation,
+    i.e., the built binaries can still be found.
+    * olddefconfig is NOT run on the configuration file.
+    * -i is used on make to ignore errors thus to try all targets.
+    """
+    #
+    # Check arguments
+    #
+
+    # Check unit_paths
+    assert unit_paths
+    for u in unit_paths:
+        assert u.endswith(".o")
+
+    assert os.path.isfile(config_path) #< Check config file.
+    assert isinstance(arch_name, str) and len(arch_name) > 0 #< Check arch.
+    assert is_linux_dir(linux_ksrc)    #< Check linux source directory.
+    assert which(cross_compiler)       #< Check cross compiler.
+    assert jobs is None or isinstance(jobs, int) #< Check jobs.
+
+    # Prepare jobs parameter
+    if jobs is None or jobs <= 0:
+        jobs_param="-j" #< Infinite.
+    else:
+        jobs_param="-j%s" % jobs
+
+    #
+    # Prepare build targets
+    #
+    targets = ["clean"]  #< clean is the first target.
+    if use_olddefconfig_target:
+        targets.append("olddefconfig")
+    for u in unit_paths: #< Map units into build targets.
+        target = build_targets.get(u, u) #< Default is the unit path.
+        if target not in targets: #< Don't include duplicates.
+            targets.append(target)
+    assert len(targets) > 1 #< At least one target other than clean.
+    logger.debug("Build targets are: \"[%s]\"\n" % ", ".join(targets))
+
+    #
+    # Prepare compilation command
+    #
+    config_abspath = os.path.abspath(config_path) #< Command will run in linux as cwd.
+    assert os.path.isfile(config_abspath)
+    compile_cmd = [cross_compiler, jobs_param, "-i", "KCONFIG_CONFIG=%s" % config_abspath, "ARCH=%s" % arch_name]
+    compile_cmd.extend(targets)  #< Add the targets.
+    logger.debug("Compilation command: \"%s\"\n" % " ".join(compile_cmd))
+
+    # Function definition for preparing the first return value: whether
+    # units were found after compilation.
+    def are_units_compiled():
+        full_unit_paths = [os.path.join(linux_ksrc, u) for u in unit_paths]
+        ret = [os.path.isfile(fpath) for fpath in full_unit_paths]
+        assert len(ret) == len(unit_paths)
+        return ret
+
+    #
+    # Run the compilation command
+    #
+    logger.debug("Running the compilation command.\n")
+    from subprocess import TimeoutExpired
+    try:
+        make_out, make_err, ret, time_elapsed = run(
+            compile_cmd, cwd=linux_ksrc, timeout=build_timeout_sec)
+        logger.debug("Compilation finished in %.2f seconds, make exit code: %s\n" % (time_elapsed, ret))
+
+        # Check the method docs for what each return value mean.
+        make_out = make_out.decode('UTF-8')
+        make_err = make_err.decode('UTF-8')
+        return are_units_compiled(), False, ret, make_out, make_err, time_elapsed
+    except TimeoutExpired:
+        logger.debug("Timeout expired for compilation, duration(sec): %.2f\n" % build_timeout_sec)
+
+        # Check the method docs for what each return value mean.
+        return are_units_compiled(), True, None, None, None, None
+
 def pause(s=None):
     try: #python2
         raw_input("Press any key to continue ..." if s is None else s)
diff --git a/setup.py b/setup.py
index 7950de61..f35085f3 100644
--- a/setup.py
+++ b/setup.py
@@ -45,6 +45,7 @@ def read(fname):
         'dd',
         'networkx==2.2', # for dd to work on python2
         'requests',
+        'whatthepatch',
     ],
     use_2to3=True,
 )


Test patch:
diff --git a/docs/experiments/testmake.md b/docs/experiments/testmake.md
index c7ab3e58..8421a1f3 100644
--- a/docs/experiments/testmake.md
+++ b/docs/experiments/testmake.md
@@ -1,7 +1,6 @@
 <!-- START doctoc generated TOC please keep comment here to allow auto update -->
 <!-- DON'T EDIT THIS SECTION, INSTEAD RE-RUN doctoc TO UPDATE -->
 
-
 - [Klocalizer Tests](#klocalizer-tests)
   - [Setup](#setup)
   - [Results](#results)