ekuiter / torte Goto Github PK

The following issues show the general roadmap for the future development of torte.

Bugs

• weird exit code when solving linux,v2.6.36,1,kclause,z3
• implement proper locking with flock on CSV files to avoid race conditions for long model counts
• starting with Linux kernel 6.9, kextractor does not work due to for_all_symbols being moved https://elixir.bootlin.com/linux/latest/source/scripts/kconfig/expr.h#L134, https://elixir.bootlin.com/linux/v6.9-rc1/source/scripts/kconfig/internal.h#L11
• Illegal instruction error (on arm platform for some #SAT solvers)

Minor improvements

• upgrade Z3 to 4.12.1, see Z3Prover/z3#6577
• test and improve error handling for missing values (NA), e.g., that failed extractions/transformations propagate appropriately to the other stages (or are ignored)
• combine iterate with run, deduce file fields automatically based on suffix -file
• add a filter stage (maybe transient) that removes some input files before executing another stage
• Z3: for DIMACS, some solvers require that "c " lines occur before "p cnf", Z3 does not do that correctly
• make transformer and analyzer names consistent with each other
• make names of columns follow a consistent scheme
• find out license for each committed blob/binary and document in readme
• remove CONFIG_ prefix from all files to save space
• treat Killed (due to OOM killer) as a failure

New Features

• new algorithms:
  • hybrid CNF transformation
  • FeatJAR's Tseitin transformation
  • allow configurable thresholds for KConfigReader, Z3, and FeatJAR
  • neg-kc-CNF (e.g., new KC artifact)
  • neg-enc-CNF (e.g., truth inversion)
  • semantic structural properties (e.g., community structure)
  • more CNF transformations (FLOTTER, https://github.com/vprover/vampire/search?q=clausify, http://fmv.jku.at/limboole/)
  • ddnnife
  • export ddnnfs with d4
• support evaluation beyond the creation of CSV files (e.g., by integrating more tools)
• separate the binding and model stages of the extraction (this would require some architectural changes to be able to combine the input directory with the bindings' output directory, but it would make the additional dependencies make and binutils for KConfigReader unnecessary)
• parallelize extraction
• auto-calculate the worst possible duration of each stage by taking timeouts into account and estimating evaluation runtime
• megamodel by introducing an arch choice or applying neg-kc-CNF
• revise input system so one stage can take multiple input stages and so that aggregate stages do not need to copy all their inputs (e.g., symlinks instead)
• create "near-correct" feature models (e.g., in UVL) that already omit dead features and also include all unconstrained features to improve the accuracy of extracted models (or, in DIMACS, add number of unconstrained variables to p cnf ...)
• integrate ConfigFix (which is the spiritual successor to KConfigReader, can export CNF with make cfoutconfig)
• add continuous integration where a virtue machine automatically installs and runs the default experiment

Improving External Validity

• add more systems (i.e., systematically search GitHub for compatible Kconfig projects, some ideas are listed in the experiment files, e.g., u-boot)
• add feature-model hierarchies (e.g., act as consumer and supplier to https://github.com/SoftVarE-Group/feature-model-benchmark)
• add more solvers (e.g., a portfolio solver, more solvers can be found in competitions)
• reproduce ASE'22 evaluation (e.g., add core/dead feature calculation) - currently, at least axTLS and freetz-ng seem buggy
• for each subject system, determine the best Linux KConfig binding version and possibly update them
• find a more elegant way to work around the Kconfig helper macros
• reproduce the results of existing evaluations (e.g., TypeChef) with other CNF transformations and/or KConfig extractors
• implement SAT format, which is used by some tools as input, as an addition to .model and .smt
• find a good way to store/upload Docker images and extracted models (really large files, Zenodo? Git LFS? university?)
• add virtualbox/vagrant image for easier reproduction

Building the kmax image currently fails. The reason seems to be that Python 3.6 is used, but the dd dependency (resolved to version 0.6.0) requires Python >= 3.11.

Full build log: build-log.txt