Merge pull request #304 from paulgazz/dev/kextractlinux-llvm-support

Fix klocalizer's tristate modeling issues and enable support for clang/llvm configs

Author: paulgazz

kmax/arch.py

@@ -789,6 +789,7 @@ def get_missing_kconfig_file_messages(make_stderr: str) -> list:
       kextract_version=kextract_module_versions.pop() # pop the next version to try
       command = [ "kextractlinux", self.name, kextract_file, "--module-version", kextract_version]
       self.__logger.debug("Running kextract tool to generate kextract (module version: %s)." % kextract_version)
+      self.__logger.debug(f"{" ".join(command)}")
       _, ke_stderr_bytes, ret_code = self.__run_command(command, cwd=self.__linux_ksrc)
       if ret_code == 0:
         break
@@ -956,7 +957,6 @@ def generate_kclause(self):
 
     command = ["kclause", "--remove-orphaned-nonvisible" ]
     if self.__kclause_args != None: command = command + self.__kclause_args
-    # TODO: disable tristate handling when requested, i.e., for kismet
     self.__logger.debug("Running kclause tool to generate kclause formulas.")
     proc_stdout, _, ret_code = self.__run_command(command, self.__kextract.encode(), capture_stderr=False)
 

kmax/kclause

@@ -1128,6 +1128,7 @@ if __name__ == '__main__':
           sys.stderr.write("%s has no final expression\n" % (var))
 
       if not disable_tristate_support and var in need_tristate_values and var in bool_types.keys() and bool_types[var] == "tristate":
+      # if not disable_tristate_support and var in bool_types.keys() and bool_types[var] == "tristate":
         config_on_iff_y_xor_m = biimplication(var, xor(tristate_config_gen(var, "y"), tristate_config_gen(var, "m")))
         # print(config_on_iff_y_xor_m)
         convert_and_add_clause(var, config_on_iff_y_xor_m)

kmax/kextractlinux

@@ -75,9 +75,28 @@ if __name__ == '__main__':
   if not os.path.isdir(archdir):
     sys.stderr.write("Architecture directory not available \"%s\", so not attempting kextractlinux.\n" % (archdir))
     exit(2)
-  args.extend([ "-e", "ARCH=%s" % (arch), "-e", "SRCARCH=%s" % (srcarch), "-e", "KERNELVERSION=kcu", "-e", "srctree=./", "-e", "CC=cc", "-e", "LD=ld", "-e", "RUSTC=rustc" ])
+  args.extend([
+    "-e", "ARCH=%s" % (arch), 
+    "-e", "SRCARCH=%s" % (srcarch),
+    "-e", "KERNELVERSION=kcu",
+    "-e", "srctree=./",
+    "-e", "RUSTC=rustc"
+  ])
+  # let the user specify CC and LD, e.g., for clang support
+  cc_env = os.environ.get("CC", "cc")
+  ld_env = os.environ.get("LD", "ld")
+  args.extend([
+    "-e", f"CC={cc_env}",
+    "-e", f"LD={ld_env}",
+  ])
+  # optionally use the LLVM environment variable to support clang/llvm kernel builds
+  llvm = os.environ.get("LLVM")
+  if llvm != None:
+    args.extend([ "-e", f"LLVM={llvm}" ])
+    # example: LLVM=1 CC="clang -fintegrated-a" LD=ld.lld kextractlinux x86_64 kextract.out --module-version next-20251023
   # set arch-specific environment variables
   args.extend(arch_specific(arch))
   # set the kconfig filename
   args.extend([ kconfigfilename ])
+  sys.stderr.write(f'{" ".join(args)}\n')
   kmax.kextractcommon.kextract(module_version, args)

kmax/klocalizer

@@ -1022,15 +1022,15 @@ def klocalizerCLI():
 
   assert allarchs + (len(archs_arg) > 0) + (kclause_file != None) < 2 # at most one can be defined
   if len(archs_arg) > 0:
-    archs = [Arch(arch, linux_ksrc=linux_ksrc, arch_dir=get_arch_formulas_dir(formulas, arch), is_kclause_composite=use_composite_kclause_formulas_files, kextract_version=kextract_version, loggerLevel=arch_logger_level) for arch in archs_arg]
+    archs = [Arch(arch, linux_ksrc=linux_ksrc, arch_dir=get_arch_formulas_dir(formulas, arch), is_kclause_composite=use_composite_kclause_formulas_files, kextract_version=kextract_version, loggerLevel=arch_logger_level, kclause_args=["--disable-tristate-support"]) for arch in archs_arg]
   elif kclause_file != None:
     # A custom architecture
-    arch = Arch(Arch.CUSTOM_ARCH_NAME, kextract_version=kextract_version, loggerLevel=arch_logger_level)
+    arch = Arch(Arch.CUSTOM_ARCH_NAME, kextract_version=kextract_version, loggerLevel=arch_logger_level, kclause_args=["--disable-tristate-support"])
     if kextract_file != None: arch.load_kextract(kextract_file, delay_loading=True)
     arch.load_kclause(kclause_file, is_composite=use_composite_kclause_formulas_files, delay_loading=True)
     archs = [arch]
   else: # allarchs is enabled, or if the above are not defined behave as if allarchs
-    archs = [Arch(arch, linux_ksrc=linux_ksrc, arch_dir=get_arch_formulas_dir(formulas, arch), is_kclause_composite=use_composite_kclause_formulas_files, kextract_version=kextract_version, loggerLevel=arch_logger_level) for arch in Arch.ARCHS]
+    archs = [Arch(arch, linux_ksrc=linux_ksrc, arch_dir=get_arch_formulas_dir(formulas, arch), is_kclause_composite=use_composite_kclause_formulas_files, kextract_version=kextract_version, loggerLevel=arch_logger_level, kclause_args=["--disable-tristate-support"]) for arch in Arch.ARCHS]
 
   if kclause_file == None:
     logger.info("Trying the following architectures: %s\n" % " ".join(arch.name for arch in archs))

kmax/klocalizer.py

@@ -360,8 +360,11 @@ def get_config_file_constraints(config_file):
           on = on_pattern.match(line)
           if on:
             # TODO: use the boolean approximation of tristate if this is disabled by kclause.  currently the tristate modeling is kept on by klocalizer for kclause.  alternatively use biimplication between options, e.g., CONFIG_A <-> CONFIG_A=y, to support both kclause with and without tristate modeling simultaneously, though this will increase the number of clauses.
-            # var_name = on.group(1)
-            var_name = tristate_config_gen(on.group(1), on.group(2))
+            if False: # tristate_support:  # TODO: thread these options throughout kclause and klocalizer for tristate support
+              var_name = tristate_config_gen(on.group(1), on.group(2))
+            else: # has tristate support
+              # TODO: tristate is disabled, because this is not properly integrated with how kclause models tristate options.  We likely need to add both the CONFIG_A and CONFIG_A=y boolean predicates to the constraints, because kclause is using both models in parallel as an optimization to reduce the number of clauses.
+              var_name = on.group(1)
             # sys.stderr.write(f"{var_name}\n")
             constraint = z3.Bool(var_name)
             constraints.append(constraint)
@@ -463,6 +466,9 @@ def get_config_from_model(model: z3.Model, arch: Arch, set_tristate_m, allow_non
     tristate_settings = {}
     for entry in model:
       str_entry = str(entry)
+      # sys.stderr.write(f"{str(entry)} {str(model[entry])}\n")
+      # sys.stderr(f"{str(entry)}\n")
+      # print(f"{str(entry)}\n")
       matches = tristate_pattern.match(str_entry)
       if matches:
         if model[entry]:
@@ -639,6 +645,7 @@ def __approximate_model(self):
       solver.add(self.__constraints)
 
       is_sat = solver.check(assumptions) == z3.sat
+      # breakpoint()
       if is_sat:
         self.__logger.info("Already satisfiable when constraining with given config.  No approximatation needed.\n")
       else: