Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history
commit ed141be
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:54:43 2019 -0500

    updated info on location of previous analysis scripts in older versions

commit b27c6a8
Merge: d35e1d8 827b6e8
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:53:09 2019 -0500

    Merge branch 'separate_out_kmax'

    This merge is from a branch that converts the kmax repository into a stand-alone python program.

commit 827b6e8
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:49:38 2019 -0500

    improve directions on running on linux

commit 67277ad
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:49:11 2019 -0500

    added the makefile that can retrieve all top-level linux directories

commit df39d68
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:47:17 2019 -0500

    add intro to readme

commit 817a3f4
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:35:08 2019 -0500

    move aggregation script into the driver

commit c9a068e
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:34:50 2019 -0500

    add python dependencies

commit 1e74fa6
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:34:40 2019 -0500

    dependencies are now setup.py

commit 5fc592e
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:22:43 2019 -0500

    Revert "partially removed pycudd"

    This reverts commit 55ac5c6.

commit 55ac5c6
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:17:55 2019 -0500

    partially removed pycudd

commit e638344
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:05:47 2019 -0500

    ignore generated stuff

commit 6b6f77d
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:05:36 2019 -0500

    setup scripts and add pymake package

commit ca630b8
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:04:58 2019 -0500

    get dependencies right

commit 45e38f3
Author: Paul <[email protected]>
Date:   Sat Nov 16 00:04:31 2019 -0500

    added pymake source code with its license

commit 8a40dad
Author: Paul <[email protected]>
Date:   Wed Nov 6 11:36:32 2019 -0500

    updated

commit f27f9bc
Author: Paul <[email protected]>
Date:   Wed Nov 6 11:36:02 2019 -0500

    updated version number

commit 660fd90
Author: Paul <[email protected]>
Date:   Wed Nov 6 11:35:57 2019 -0500

    updated readme

commit 50f8f7a
Author: Paul <[email protected]>
Date:   Wed Nov 6 11:35:43 2019 -0500

    added license text

commit a625bbc
Author: Paul <[email protected]>
Date:   Wed Nov 6 11:23:23 2019 -0500

    reorganizing and setting up via setuptools

commit 606a50a
Author: Paul <[email protected]>
Date:   Tue Nov 5 01:30:31 2019 -0500

    removed

commit 2cfb376
Author: Paul <[email protected]>
Date:   Tue Nov 5 01:28:55 2019 -0500

    removed

commit 1b1d5e3
Author: Paul <[email protected]>
Date:   Tue Nov 5 01:16:27 2019 -0500

    removed unneeded lib

commit 55e66e2
Author: Paul <[email protected]>
Date:   Mon Nov 4 14:24:55 2019 -0500

    separate out only kmax code

commit d35e1d8
Author: Paul Gazzillo <[email protected]>
Date:   Wed Sep 25 13:06:58 2019 -0400

    Update README.md

commit d5d4660
Merge: b7a7c59 818186f
Author: Paul Gazzillo <[email protected]>
Date:   Wed Sep 18 12:38:56 2019 -0400

    Merge pull request #78 from paulgazz/Sayma23-patch-1-1

    Update README.md

commit 818186f
Author: Sayma23 <[email protected]>
Date:   Wed Sep 18 11:08:05 2019 -0400

    Update README.md

commit b7a7c59
Merge: 0067a2b cac0b5c
Author: Paul <[email protected]>
Date:   Fri Aug 2 14:05:28 2019 -0400

    Merge branch 'master' of github.com:paulgazz/kmax into release

commit cac0b5c
Merge: 1ca7570 07cf43b
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:39:58 2019 -0400

    Merge branch 'update_kconfig_to_4.19.50'

    This includes the z3 branch as well.

commit 07cf43b
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:34:40 2019 -0400

    new kclause tests

commit 1b556a2
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:33:44 2019 -0400

    more tests

commit c3d2edd
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:32:37 2019 -0400

    add GPL from linux

commit 8c91f51
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:24:56 2019 -0400

    code from new version of kconfig

commit 629c4ff
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:24:06 2019 -0400

    introduce kclause

commit e300870
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:21:11 2019 -0400

    ignore pymake download

commit 9cad8de
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:20:46 2019 -0400

    add makefile to get pymake

commit 6631b2d
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:20:20 2019 -0400

    start unifying documentation into a single directory

commit 6275fc4
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:19:59 2019 -0400

    another table of build system stats

commit 1b195cf
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:19:16 2019 -0400

    move BDD version of Kmax instructions to kbuild/ directory

commit b9aec0f
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:17:34 2019 -0400

    code to emit all clauses for kconfig

commit 657c3d9
Author: Paul <[email protected]>
Date:   Fri Aug 2 13:17:06 2019 -0400

    updated documentation to describe z3 version only and for linux

commit 0d93482
Author: Paul <[email protected]>
Date:   Thu Jun 20 15:58:54 2019 -0400

    upgraded kconfig to linux version 4.19.50

commit 92ad6ec
Author: Paul <[email protected]>
Date:   Thu Jun 20 14:52:48 2019 -0400

    added script to run kmax's Kbuild Makefile interpreter recursively on each subdirectory of the source code

commit cf6f026
Author: Paul <[email protected]>
Date:   Thu Jun 20 14:49:46 2019 -0400

    added script to combine the compilation unit and directory presence conditions, i.e., converting the unit_pc format to the full_pc format.

commit ecaeeff
Author: Paul <[email protected]>
Date:   Thu Jun 20 14:41:22 2019 -0400

    add command-line flag for producing the kmax unit_pc format that maps filenames to boolean expressions representing the conditions under which they are included in the binary

commit ef0bfe9
Author: Paul <[email protected]>
Date:   Thu Jun 20 14:40:35 2019 -0400

    process one makefile at a time

commit 65ff3ea
Author: Paul <[email protected]>
Date:   Wed Jun 5 15:05:23 2019 -0400

    add simplification to z3 kconfig converter

commit ddd7be0
Author: Paul <[email protected]>
Date:   Wed Jun 5 15:05:06 2019 -0400

    report presence conditions in the original kbuild format

commit e7c166f
Author: Paul <[email protected]>
Date:   Fri Mar 8 02:18:57 2019 -0500

    use fancy ctx-solver-simplify in addition to the regular simplify for cleaner expressions

commit af2c27e
Author: Paul <[email protected]>
Date:   Fri Mar 8 02:18:13 2019 -0500

    need to have default definition for recursive variable assignment

commit 5f15a64
Author: Paul <[email protected]>
Date:   Fri Mar 8 02:10:52 2019 -0500

    added collection script for linux that uses the new kbuildplus

commit a32ebd7
Author: Paul <[email protected]>
Date:   Fri Mar 8 01:19:57 2019 -0500

    print presence conditions

commit 3e0eff4
Author: Paul <[email protected]>
Date:   Thu Mar 7 23:59:40 2019 -0500

    linux results are too large to process it all in one run of python at once (stack depth exceeded), so linux run takes a single makefile and pickles it for linux_case_study.py; add back support for subdirs

commit 679efb7
Author: Paul <[email protected]>
Date:   Thu Mar 7 23:58:35 2019 -0500

    add back support for tracking subdirs in results

commit c2a51df
Author: Paul <[email protected]>
Date:   Mon Feb 18 17:55:06 2019 -0500

    fix problem where set of presence conditions was reset for each makefile.  now all presence conditions will be collected for all makefiles.

commit b024b9b
Author: Paul <[email protected]>
Date:   Tue Jan 29 01:31:26 2019 -0500

    remove all uses of the old subdir_pc and token_pc

commit 88106af
Author: Paul <[email protected]>
Date:   Tue Jan 29 01:20:14 2019 -0500

    remove obsolete method for getting presence conditions

commit faef0d7
Author: Paul <[email protected]>
Date:   Wed Jan 23 13:49:41 2019 -0500

    fixed bug where nested conditionals conditions were not being conjoined in a certain case, i.e., when it was an ifdef that expanded only to a string and not a multiverse

commit 2753365
Author: Paul <[email protected]>
Date:   Wed Jan 23 13:48:17 2019 -0500

    typo in test case

commit 14b2074
Author: Paul <[email protected]>
Date:   Mon Jan 21 16:51:15 2019 -0500

    Support for presence conditions for composite compilation units.

commit 15b710d
Author: Paul <[email protected]>
Date:   Mon Jan 21 14:44:11 2019 -0500

    Fixed several issues with presence condition creation:

    - Use the resulting symbol table to construct presence conditions for each token, intead of the previous hack that computed them while processing the Makefile
    - Only use the default variable entry for BITS if the Makefile does not define it, e.g., for tests/kbuild/paper_example
    - Add output for the new presence condition computation.

commit 313b0fa
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Jan 5 09:04:20 2019 -0600

    add files

commit 7b39d3a
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Jan 5 09:01:37 2019 -0600

    latest

commit 703b0a5
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Dec 22 23:57:49 2018 -0600

    updates (using vscode)

commit faeed3d
Author: ThanhVu Nguyen <[email protected]>
Date:   Thu Dec 20 10:28:02 2018 -0600

    about to cleanup

commit 8080a03
Author: ThanhVu Nguyen <[email protected]>
Date:   Tue Dec 18 15:59:18 2018 -0600

    can parse linux usr

commit 465dda8
Author: ThanhVu Nguyen <[email protected]>
Date:   Tue Dec 18 15:06:09 2018 -0600

    begin Linux script

commit 2d2ab3f
Author: ThanhVu Nguyen <[email protected]>
Date:   Tue Dec 18 02:50:48 2018 -0600

    more cleanup

commit a58b8e3
Author: ThanhVu Nguyen <[email protected]>
Date:   Mon Dec 17 02:02:29 2018 -0600

    refactor

commit 56ef0db
Author: ThanhVu Nguyen <[email protected]>
Date:   Mon Dec 17 00:23:16 2018 -0600

    busybox cleanup

commit 61fe83f
Author: ThanhVu Nguyen <[email protected]>
Date:   Sat Dec 15 00:48:48 2018 -0600

    included_c_files

commit fd0a77f
Author: ThanhVu Nguyen <[email protected]>
Date:   Thu Dec 13 23:31:27 2018 -0600

    almost done with busybox scripts

commit 8879901
Author: ThanhVu Nguyen <[email protected]>
Date:   Tue Dec 11 14:50:35 2018 -0600

    cleanup code, similar to compilation units

commit d9ed473
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Dec 10 22:21:23 2018 -0600

    add files

commit a698402
Author: Paul <[email protected]>
Date:   Tue Dec 4 15:19:28 2018 -0500

    fixed typo

commit 1ca7570
Author: Paul <[email protected]>
Date:   Tue Dec 4 15:19:28 2018 -0500

    fixed typo

commit d906f2d
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sun Dec 2 09:54:45 2018 -0600

    clean up, settings, remove several do_

commit 6ff3a1a
Author: Paul <[email protected]>
Date:   Thu Nov 29 13:51:48 2018 -0500

    add -B flag for boolean

commit 0906a87
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Thu Nov 29 12:27:00 2018 -0600

    works with busybox

commit 76b1af6
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Nov 24 09:34:59 2018 -0600

    update

commit 366cb40
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Nov 19 14:26:00 2018 -0600

    more api, pass args as arguments

commit 8e7a29c
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Nov 19 12:43:32 2018 -0600

    API

commit d3d0a8c
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Nov 12 15:37:52 2018 -0600

    some cleanup

commit 04cec2e
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Nov 12 11:25:49 2018 -0600

    complete code for contains_unexpanded v1 and v2

commit 90fefca
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Nov 12 07:46:14 2018 -0600

    fix a bug in dedup

commit 62aefb9
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Nov 10 11:00:52 2018 -0600

    add support for boolean configs

commit 389c7b1
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Nov 10 08:53:02 2018 -0600

    add orig script

commit c0c1ff0
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Nov 10 08:52:51 2018 -0600

    remove unnecessary imports

commit 42859ed
Author: Paul <[email protected]>
Date:   Tue Oct 30 22:14:55 2018 -0400

    instructions for running on busybox

commit 8e54bdb
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 12:18:51 2018 -0500

    add additional files

commit 66934c2
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 12:11:28 2018 -0500

    fix pylint errors

commit f3c1e21
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 11:45:28 2018 -0500

    readd tests

commit b0989b5
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 11:43:53 2018 -0500

    fix a small bug first_branch_cond is not None

commit e5ad9f9
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 11:39:37 2018 -0500

    make dedup part of multiverse

commit 4e110f2
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 29 11:37:02 2018 -0500

    more z3 integration, simplify dedup

commit e5ae531
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Oct 27 11:33:45 2018 -0500

    subst_config_var

commit 4bcce99
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Oct 27 09:59:26 2018 -0500

    more print results

commit b6c6f6d
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Sat Oct 27 09:52:46 2018 -0500

    print results

commit 19c5910
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Wed Oct 24 15:57:04 2018 -0500

    presence cond for paper example

commit c7c9d4f
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Wed Oct 24 13:54:46 2018 -0500

    works with paper example

commit c956c2c
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Wed Oct 24 13:23:30 2018 -0500

    more z3 integration

commit c3b170f
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Tue Oct 23 10:52:36 2018 -0500

    more z3 integration

commit f04e1f6
Author: ThanhVu (Vu) Nguyen <[email protected]>
Date:   Mon Oct 22 16:27:52 2018 -0500

    begin to add z3 support

commit 494ed4c
Author: Paul <[email protected]>
Date:   Sun Sep 23 13:49:02 2018 -0400

    Improve installation directions for dependencies.

commit 402f280
Merge: 34de485 48b524b
Author: Paul Gazzillo <[email protected]>
Date:   Fri Sep 21 16:02:22 2018 -0400

    Merge pull request #73 from paulgazz/better_selects_and_nonvisibles

    Better selects and nonvisibles

commit 48b524b
Author: Paul <[email protected]>
Date:   Fri Sep 21 15:51:55 2018 -0400

    Revert "Preserve dimacs.py naming for backwards compatibility with existing scripts."

    This reverts commit 6c5db72.

commit a148598
Author: Paul <[email protected]>
Date:   Fri Sep 21 15:51:43 2018 -0400

    Revert "Create the dimacs.py which calls into the newly-named build_model.py."

    This reverts commit eff4a55.

commit eff4a55
Author: Paul <[email protected]>
Date:   Fri Sep 21 15:49:40 2018 -0400

    Create the dimacs.py which calls into the newly-named build_model.py.

commit 6c5db72
Author: Paul <[email protected]>
Date:   Fri Sep 21 15:47:46 2018 -0400

    Preserve dimacs.py naming for backwards compatibility with existing scripts.

commit e90a424
Author: Paul <[email protected]>
Date:   Fri Sep 21 15:45:53 2018 -0400

    Move z3 generation into existing dimacs generator.

commit 70a54b5
Merge: 3f5c613 10bbe37
Author: Paul <[email protected]>
Date:   Sun Sep 16 23:34:12 2018 -0400

    Merge branch 'kconfig_z3' into merge_improve_with_z3

commit 10bbe37
Author: Paul <[email protected]>
Date:   Sun Sep 16 23:28:03 2018 -0400

    Check for feasibility of expression.

commit e72c743
Author: Paul <[email protected]>
Date:   Sun Sep 16 23:27:37 2018 -0400

    Simplify clauses after conversion.

commit e7c7490
Author: Paul <[email protected]>
Date:   Fri Sep 14 13:15:30 2018 -0400

    Generate z3 clauses from the expression tree.

commit cc04ec2
Author: Paul <[email protected]>
Date:   Fri Sep 14 12:44:13 2018 -0400

    Prepare for z3 clauses generation, by duplicating dimacs code and making it switchable.

commit 43ff516
Author: Paul <[email protected]>
Date:   Fri Sep 14 12:36:56 2018 -0400

    Factor out dimacs clause generation.

commit d6b5425
Author: Paul <[email protected]>
Date:   Fri Sep 14 12:22:26 2018 -0400

    Make z3 test more complicated.

commit 464605e
Author: Paul <[email protected]>
Date:   Sat Sep 8 10:50:05 2018 -0400

    simple constraints

commit b0896b0
Author: Paul <[email protected]>
Date:   Sat Sep 8 10:21:35 2018 -0400

    Better naming.

commit dc147dc
Author: Paul <[email protected]>
Date:   Sat Sep 8 10:16:17 2018 -0400

    Started z3 version of the kconfig constraint generator.

commit 3f5c613
Author: Paul <[email protected]>
Date:   Sat Aug 11 13:57:59 2018 -0400

    Tests for large reverse dependencies.  This is to evaluate how to avoid massive blowup in negating these expressions.

commit 455d7b4
Author: Paul <[email protected]>
Date:   Sat Aug 11 13:56:36 2018 -0400

    First attempt at simplified clause implementation, but it is still broken.

commit 79cd583
Author: Paul <[email protected]>
Date:   Sat Aug 11 13:56:17 2018 -0400

    Support None in negation method.

commit 90f63b0
Author: Paul <[email protected]>
Date:   Fri Aug 10 15:50:41 2018 -0400

    New disjunction function that filters out None args.

commit 79ab757
Author: Paul <[email protected]>
Date:   Fri Aug 10 15:36:22 2018 -0400

    Make a switch for the old, unsimplified version of the expression formula and add a template for the unified version of simplified formula.

commit 4b85276
Author: Paul <[email protected]>
Date:   Fri Aug 10 15:22:08 2018 -0400

    Comment on why we have `if False:`

commit 4925aad
Author: Paul <[email protected]>
Date:   Fri Aug 10 15:21:36 2018 -0400

    Improved disjunction function that takes n args.

commit 4147a66
Author: Paul <[email protected]>
Date:   Fri Jul 27 15:49:40 2018 -0400

    Use simplified form of nonvisibles.

commit b26c2c6
Author: Paul <[email protected]>
Date:   Fri Jul 27 15:47:11 2018 -0400

    Remove some excess debugging output and pretty print some expressions.

commit 34de485
Author: Paul <[email protected]>
Date:   Mon Jul 23 13:05:45 2018 -0400

    Created a token-based replacement method that replaces the buggy pure string replacement.  This enables expressions to replace expressions; otherwise replacing just a string may replace part of a token.

commit 06bf1e0
Author: Paul <[email protected]>
Date:   Mon Jul 23 12:48:20 2018 -0400

    Use "not" instead of "!" to enable parsing of subexpressions.

commit 7280945
Merge: ab7ac0d 6ea3d48
Author: paulgazz <[email protected]>
Date:   Thu Jul 5 13:29:29 2018 -0400

    Merge pull request #62 from paulgazz/improve_clause_generation

    Reduce clause explosion for reverse dependencies

commit 6ea3d48
Author: Paul <[email protected]>
Date:   Thu Jul 5 13:22:55 2018 -0400

    Moved from kconfig_case_studies; (incomplete) description of kconfig semantics.

commit ab7ac0d
Merge: 5ab1cd0 3edf130
Author: paulgazz <[email protected]>
Date:   Tue Jul 3 16:10:26 2018 -0400

    Merge pull request #69 from paulgazz/presence_conditions_for_lib_objects

    Pass-through old naive append flag

commit 3edf130
Merge: 20068f0 5ab1cd0
Author: Paul <[email protected]>
Date:   Tue Jul 3 16:09:41 2018 -0400

    Merge branch 'master' into presence_conditions_for_lib_objects

commit 5ab1cd0
Merge: a091db9 f17161e
Author: paulgazz <[email protected]>
Date:   Tue Jul 3 15:37:41 2018 -0400

    Merge pull request #67 from paulgazz/new_kconfig_testcases

    Added new test cases for kconfig

commit a091db9
Merge: 8a82418 cd0793f
Author: paulgazz <[email protected]>
Date:   Tue Jul 3 15:37:31 2018 -0400

    Merge pull request #68 from paulgazz/minor_script_addition

    New script to count up configs per C file.

commit cd0793f
Author: Paul <[email protected]>
Date:   Tue Jul 3 15:33:56 2018 -0400

    New script to count up configs per C file.

commit f17161e
Author: Paul <[email protected]>
Date:   Tue Jul 3 15:29:44 2018 -0400

    Added new test cases for kconfig

commit 625f75d
Author: Paul <[email protected]>
Date:   Tue Jul 3 15:27:03 2018 -0400

    Make optimization for reverse dependencies controllable.

commit 6f88ce8
Author: Paul <[email protected]>
Date:   Mon Jul 2 18:37:18 2018 -0400

    Optimization to reduce CNF blowup when dealing with reverse dependencies.

    Combine factors by disjunction for top-level terms, i.e., A & D1 or A & D2 => A & (D1 or D2).

commit 2cd101b
Author: Paul <[email protected]>
Date:   Mon Jul 2 18:12:02 2018 -0400

    Restored use of rev_dep lines.

commit e509295
Author: Paul <[email protected]>
Date:   Mon Jul 2 18:11:25 2018 -0400

    Added support for debugging expressions in output.

commit 48f96fb
Author: Paul <[email protected]>
Date:   Mon Jul 2 15:37:16 2018 -0400

    Improve error handling for parsing errors while converting expressions to CNF.

    This also increasing the recursion depth for python to allow for parsing of deeply-nested expressions.

commit 5e965b3
Author: Paul <[email protected]>
Date:   Sat Jun 30 12:40:20 2018 -0400

    Uses the new select dependency emitted by `check_dep` to generate much
    smaller clauses for reverse dependencies.

    Fixes #66.

commit bf1debc
Author: Paul <[email protected]>
Date:   Sat Jun 30 12:39:58 2018 -0400

    clean up comments

commit c2dd984
Author: Paul <[email protected]>
Date:   Sat Jun 30 12:29:22 2018 -0400

    This fixes #66 by only emitting the expression found in the `select ... if expression` line.

    It works by creating a new field in the property struct that stores the original if expression before it gets processed by kconfig.  This expression is then emitted in the select line of the kmax output by `check_dep --dimacs`.

commit d1d816d
Author: Paul <[email protected]>
Date:   Wed Jun 27 18:19:19 2018 -0400

    reimplement the reverse dependency expression using the new select_line to limit clause blowup; fixes #64

commit b785ad3
Author: Paul <[email protected]>
Date:   Wed Jun 27 17:24:35 2018 -0400

    Use simplified formulas for visible variables.

    Improve debugging output and show progress of clause post-processing.

commit 4ba9e1a
Author: Paul <[email protected]>
Date:   Wed Jun 27 16:16:00 2018 -0400

    export the raw select lines instead of the pre-computed rev_dep expression; fixes #61

commit 8a82418
Merge: 21f475e f0e1b3f
Author: paulgazz <[email protected]>
Date:   Fri Jun 1 18:36:01 2018 -0400

    Merge pull request #59 from paulgazz/support_prompt_conditions

    Support prompt conditions

commit f0e1b3f
Author: Paul <[email protected]>
Date:   Fri Jun 1 18:19:44 2018 -0400

    corrected bool choice to allow for no choice to be selected if the choice's dependencies are not met

commit acf4d9c
Author: Paul <[email protected]>
Date:   Fri Jun 1 16:56:29 2018 -0400

    fixed expression for reverse dependencies for visible variables; turn on filtering by default

commit 5514a01
Author: Paul <[email protected]>
Date:   Fri May 25 16:14:58 2018 -0400

    examples of nonbool with prompt

commit 27d5abf
Author: Paul <[email protected]>
Date:   Fri May 25 09:26:40 2018 -0400

    fix support for prompt condition in nonbools; add support for comments in kmax files

commit 6ab2a21
Author: Paul <[email protected]>
Date:   Thu May 24 12:58:58 2018 -0400

    support env variables as selectable; fixes #60

commit d6d8b3d
Author: Paul <[email protected]>
Date:   Thu May 24 12:39:23 2018 -0400

    deduplicate clauses and remove true clauses; fixes #40

commit 0a4688d
Author: Paul <[email protected]>
Date:   Thu May 24 12:11:32 2018 -0400

    bugs in processing prompt expressions

commit 9706336
Author: Paul <[email protected]>
Date:   Thu May 24 12:03:50 2018 -0400

    refactored visible and nonvisible variable dependencies and included prompt conditions

commit 86ebe3f
Author: Paul <[email protected]>
Date:   Wed May 23 14:53:00 2018 -0400

    document ability to add raw expressions to the dimacs file

commit d6b7850
Author: Paul <[email protected]>
Date:   Wed May 23 14:52:36 2018 -0400

    collect new config and prompt lines; remove option for root variable

commit 220dcf2
Author: Paul <[email protected]>
Date:   Wed May 23 14:36:26 2018 -0400

    support prompt conditions and improve declarations and type names in pre-dimacs output

commit 21f475e
Merge: 6c9b904 fee95c4
Author: paulgazz <[email protected]>
Date:   Wed May 23 12:35:16 2018 -0400

    Merge pull request #39 from paulgazz/improve_select

    Improve select

commit fee95c4
Merge: 58f051b 6c9b904
Author: Paul <[email protected]>
Date:   Wed May 23 12:31:38 2018 -0400

    Merge branch 'master' into improve_select

commit 58f051b
Author: Paul <[email protected]>
Date:   Wed May 23 12:28:01 2018 -0400

    update to support environment var labeling

commit b9edac0
Author: Paul <[email protected]>
Date:   Mon May 21 14:55:08 2018 -0400

    escape backslashes in strings

commit 6c9b904
Merge: 4b9964b 84ed937
Author: Elias Kuiter <[email protected]>
Date:   Fri May 18 01:25:12 2018 +0200

    Merge pull request #47 from ekuiter/master

    Treat tristate configs as Boolean in Linux & Busybox analysis

commit 84ed937
Author: Elias Kuiter <[email protected]>
Date:   Thu May 17 20:02:16 2018 +0200

    Added "boolean configs" for Linux analysis as well

commit 872a614
Author: Elias Kuiter <[email protected]>
Date:   Thu May 17 18:33:32 2018 +0200

    Added "boolean variables" option to Busybox analysis

commit 4b9964b
Merge: 4c2040c 5106a45
Author: paulgazz <[email protected]>
Date:   Thu May 17 11:33:37 2018 -0400

    Merge pull request #46 from paulgazz/new_testcases

    New test cases for presence conditions

commit 5106a45
Author: Paul <[email protected]>
Date:   Thu May 17 11:31:52 2018 -0400

    option to treat configs as pure boolean variables; fixes #43

commit d171ea7
Author: Paul <[email protected]>
Date:   Thu May 17 09:43:06 2018 -0400

    new testcases.  thanks to @ekuiter!

commit fc398c8
Author: Paul <[email protected]>
Date:   Wed May 9 15:51:29 2018 -0400

    added dimacs output for test cases

commit 27c452b
Merge: 83aaa86 4c2040c
Author: Paul <[email protected]>
Date:   Wed May 9 15:35:54 2018 -0400

    Merge branch 'master' into improve_select

commit 4c2040c
Merge: 96df934 05a7471
Author: paulgazz <[email protected]>
Date:   Wed May 9 15:34:50 2018 -0400

    Merge pull request #45 from paulgazz/more_kconfig_testcases

    Reorganize and add testcases

commit 05a7471
Author: Paul <[email protected]>
Date:   Wed May 9 15:26:09 2018 -0400

    reorganize testcases

commit 83aaa86
Merge: b842dff 96df934
Author: Paul <[email protected]>
Date:   Fri May 4 14:03:49 2018 -0400

    Merge branch 'master' into improve_select

commit 96df934
Merge: 023e7cb 289ed70
Author: paulgazz <[email protected]>
Date:   Fri May 4 14:03:15 2018 -0400

    Merge pull request #44 from paulgazz/kconfig_analysis_testcases

    added semantics tests from analysis paper

commit 289ed70
Author: Paul <[email protected]>
Date:   Fri May 4 14:02:24 2018 -0400

    added semantics tests from analysis paper

commit b842dff
Author: Paul <[email protected]>
Date:   Fri May 4 13:35:26 2018 -0400

    nonvisible boolean default to off

commit ee52e40
Author: Paul <[email protected]>
Date:   Fri May 4 13:19:31 2018 -0400

    fix bug that was remove nonvisibles that were used in visibles' dependencies

commit d98f18b
Merge: 580e6a9 8118eb6
Author: Paul <[email protected]>
Date:   Tue May 1 10:40:50 2018 -0400

    Merge branch 'append_optimiation' into improve_select

    Minor updates to busybox test script

commit 580e6a9
Merge: 9daa521 023e7cb
Author: Paul <[email protected]>
Date:   Tue May 1 10:40:46 2018 -0400

    Merge branch 'master' into improve_select

commit 8118eb6
Author: Paul <[email protected]>
Date:   Tue May 1 10:39:45 2018 -0400

    added new directory for 1.28.1 busybox

commit 023e7cb
Merge: 179003b 944454c
Author: paulgazz <[email protected]>
Date:   Tue May 1 10:38:23 2018 -0400

    Merge pull request #28 from paulgazz/append_optimiation

    New optimization for append

commit 944454c
Merge: d7717bd 0a2ac80
Author: Paul <[email protected]>
Date:   Tue May 1 10:04:25 2018 -0400

    Merge branch 'presence_conditions_for_lib_objects_reduced' into append_optimiation

    This will add support for presence conditions for library objects and collect them when running kmax for busybox.

commit 9daa521
Author: Paul <[email protected]>
Date:   Mon Apr 30 16:11:40 2018 -0400

    bugfix: don't assume there exists a factor in the term

commit 60b4cb6
Author: Paul <[email protected]>
Date:   Mon Apr 30 16:01:17 2018 -0400

    remove the direct dependency expressions that are added to each term of the reverse dependency expression; fixes #41

commit 4e0eb22
Author: Paul <[email protected]>
Date:   Fri Apr 27 16:24:00 2018 -0400

    removed todos, which are done or can be found in github issues

commit 046c1d8
Author: Paul <[email protected]>
Date:   Fri Apr 27 16:23:11 2018 -0400

    identifier bools that are part of a choice block in the dimacs output

commit f5b714c
Author: Paul <[email protected]>
Date:   Wed Apr 25 18:01:31 2018 -0400

    remove undefined variables; fixes #38

commit 40e1a03
Author: Paul <[email protected]>
Date:   Wed Apr 25 17:44:52 2018 -0400

    readded support for nonbools ; fixes #37

commit d7717bd
Author: Paul <[email protected]>
Date:   Tue Apr 24 18:18:04 2018 -0400

    clean up temp files

commit e390dc0
Author: Paul <[email protected]>
Date:   Tue Apr 24 15:11:14 2018 -0400

    use variable equivalence set in other variable assignment operations and when collecting compilation units

commit 4fa08cb
Author: Paul <[email protected]>
Date:   Tue Apr 24 14:55:15 2018 -0400

    use equivalence set of variables in expansions as well; test case included

commit 3900309
Author: Paul <[email protected]>
Date:   Tue Apr 24 14:53:12 2018 -0400

    use equivalence set of variables in expansions as well

commit 33cb0e6
Author: Paul <[email protected]>
Date:   Tue Apr 24 11:41:58 2018 -0400

    create predicate abstracts for non-boolean expressions

commit 05aa42c
Author: Paul <[email protected]>
Date:   Tue Apr 24 11:15:03 2018 -0400

    implemented new dependency formula for visible variables; fixes #34

commit 53c5a07
Author: Paul <[email protected]>
Date:   Mon Apr 23 12:41:48 2018 -0400

    debugging output

commit 9bf1258
Author: Paul <[email protected]>
Date:   Mon Apr 23 12:18:18 2018 -0400

    integrate mandatory nonbool settings into new dependency computation

commit d64aae1
Author: Paul <[email protected]>
Date:   Mon Apr 23 12:02:41 2018 -0400

    remove debugging output

commit 53987ab
Author: Paul <[email protected]>
Date:   Mon Apr 23 12:00:31 2018 -0400

    minor refactoring, fixes, and warnings for new dependency implementation

commit 6f515cb
Author: Paul <[email protected]>
Date:   Mon Apr 23 11:45:09 2018 -0400

    clean up bugs in new dependency computation

commit 38f6862
Author: Paul <[email protected]>
Date:   Mon Apr 23 11:35:35 2018 -0400

    implement logic for nonvisible and visible clauses

commit 8ffe912
Author: Paul <[email protected]>
Date:   Mon Apr 23 10:56:29 2018 -0400

    templates for implication and biimplication

commit 8c87b0b
Author: Paul <[email protected]>
Date:   Mon Apr 23 10:52:23 2018 -0400

    factor out handling of default booleans

commit f7ff90c
Author: Paul <[email protected]>
Date:   Fri Apr 20 17:11:15 2018 -0400

    only need a nonvisible to not be in any other dependency to remove it

commit f43c2db
Author: Paul <[email protected]>
Date:   Fri Apr 20 15:42:46 2018 -0400

    consider variables set by environment variables as user selectable

commit eb1241b
Author: Paul <[email protected]>
Date:   Fri Apr 20 15:32:48 2018 -0400

    only remove boolean orphans

commit d7c199d
Author: Paul <[email protected]>
Date:   Fri Apr 20 15:20:58 2018 -0400

    bug in outputting bad selects

commit 9599d06
Author: Paul <[email protected]>
Date:   Fri Apr 20 15:18:32 2018 -0400

    generate dependency clauses after reading in all dependency lines first

commit 165592f
Author: Paul <[email protected]>
Date:   Fri Apr 20 14:49:35 2018 -0400

    handle strings in expressions by removing them

commit 5db099b
Author: Paul <[email protected]>
Date:   Thu Apr 19 17:24:56 2018 -0400

    option to output new comment format; fixes #32 and fixes #33

commit 7c045a5
Author: Paul <[email protected]>
Date:   Thu Apr 19 16:52:27 2018 -0400

    handle strings in boolean expressions

commit a79bb3e
Author: Paul <[email protected]>
Date:   Thu Apr 19 13:54:48 2018 -0400

    add support for removing nonvisibles that don't defaults or selects

commit 1acb3ab
Author: Paul <[email protected]>
Date:   Thu Apr 19 13:41:57 2018 -0400

    cleaner support for removing nonvisibles; better cli args

commit 0da766b
Author: Paul <[email protected]>
Date:   Thu Apr 19 13:00:38 2018 -0400

    report bad usage of select statements

commit e2d604f
Author: Paul <[email protected]>
Date:   Wed Apr 18 15:06:41 2018 -0400

    check for bad select statements and ignore their reverse dependencies

commit ba805f6
Author: Paul <[email protected]>
Date:   Wed Apr 18 14:32:21 2018 -0400

    update doc on format ordering assumptions

commit 7af2fa1
Author: Paul <[email protected]>
Date:   Wed Apr 18 14:32:04 2018 -0400

    fix args logic

commit 2e50ba2
Author: Paul <[email protected]>
Date:   Wed Apr 18 14:09:09 2018 -0400

    improved cli arguments

commit 3d27528
Author: Paul <[email protected]>
Date:   Wed Apr 18 13:57:04 2018 -0400

    support removing invisibles only if not in visible variables' dependencies

commit 179003b
Merge: 4381bff a68c0f8
Author: paulgazz <[email protected]>
Date:   Fri Apr 13 10:47:40 2018 -0400

    Merge pull request #30 from paulgazz/improve_select

    Improve how dimacs.py handles nonselectable variables and reverse dependencies

commit a68c0f8
Author: Paul <[email protected]>
Date:   Fri Apr 13 10:09:50 2018 -0400

    flag to ignore reverse dependencies

commit 20068f0
Author: Paul <[email protected]>
Date:   Fri Apr 13 09:56:42 2018 -0400

    pass-through naive-append parameter

commit 11f9581
Author: Paul <[email protected]>
Date:   Thu Apr 12 17:14:28 2018 -0400

    reimplement flag for inclusion of nonselectable vars

commit 7b8e0a1
Author: Paul <[email protected]>
Date:   Thu Apr 12 17:12:46 2018 -0400

    implement general-purpose dimacs clause filtering

commit 06d97fe
Author: Paul <[email protected]>
Date:   Thu Apr 12 16:08:24 2018 -0400

    abstract away dimacs printing

commit 4d33a3b
Author: Paul <[email protected]>
Date:   Thu Apr 12 13:48:11 2018 -0400

    add argparser

commit eab4bf7
Author: Paul <[email protected]>
Date:   Wed Apr 11 12:13:09 2018 -0400

    use rev_dep to identify reverse dependencies

commit 77357ec
Author: Paul <[email protected]>
Date:   Tue Apr 10 15:48:01 2018 -0400

    new optimization for append

commit 4381bff
Merge: 736644a 88d6f11
Author: paulgazz <[email protected]>
Date:   Mon Apr 9 17:36:12 2018 -0400

    Merge pull request #26 from paulgazz/check_dep_env

    Minor improvements to Kconfig processing

commit 88d6f11
Author: Paul <[email protected]>
Date:   Mon Apr 9 17:27:38 2018 -0400

    ensure empty values are quoted; strip quotes for nonstring nonbooleans

commit 5f7f1af
Author: Paul <[email protected]>
Date:   Mon Apr 9 16:35:50 2018 -0400

    support setting environment variables and a custom prefix

commit 736644a
Merge: eb45280 45f1b73
Author: paulgazz <[email protected]>
Date:   Mon Apr 9 15:49:11 2018 -0400

    Merge pull request #25 from paulgazz/incorporate_dimacs_changes

    Incorporate dimacs changes

commit 45f1b73
Author: Paul <[email protected]>
Date:   Fri Apr 6 15:53:57 2018 -0400

    improve error handling and debugging output

commit f5cba34
Author: Paul <[email protected]>
Date:   Tue Mar 27 09:27:32 2018 -0400

    support nonboolean expression predicates

commit 0a2ac80
Author: Paul <[email protected]>
Date:   Mon Apr 9 13:19:16 2018 -0400

    collect presence conditions for busybox

commit e24987b
Author: Paul <[email protected]>
Date:   Mon Apr 9 13:19:06 2018 -0400

    support getting presence conditions from library units as well

commit eb45280
Merge: a72a092 6857f77
Author: paulgazz <[email protected]>
Date:   Sat Apr 7 09:09:47 2018 -0400

    Merge pull request #22 from paulgazz/dimacs_fixes

    Add new options to dimacs output

commit 6857f77
Author: Paul <[email protected]>
Date:   Sat Apr 7 09:08:11 2018 -0400

    add option to force all nonbools on regardless of dependencies; this is off by default

commit a2187d5
Author: Paul <[email protected]>
Date:   Sat Apr 7 08:51:39 2018 -0400

    disable def_bools by default

commit ac86487
Author: Paul <[email protected]>
Date:   Sat Apr 7 08:41:16 2018 -0400

    improved duplicate removal; flag for supporting bool defaults or not

commit 7af98a1
Author: Paul <[email protected]>
Date:   Fri Apr 6 15:57:00 2018 -0400

    ensure no duplicates in clauses

commit a72a092
Merge: bfbf60c 793e4e5
Author: paulgazz <[email protected]>
Date:   Fri Mar 16 11:50:16 2018 -0400

    Merge pull request #14 from paulgazz/bugfixes

    Fixes bugs in processing configuration expressions

commit bfbf60c
Merge: f6440c3 fe03859
Author: paulgazz <[email protected]>
Date:   Fri Mar 16 11:49:26 2018 -0400

    Merge pull request #1 from paulgazz/dimacs

    Support for creating dimacs files from Kconfig feature models

commit 793e4e5
Author: Paul <[email protected]>
Date:   Fri Mar 16 11:16:03 2018 -0400

    this enhances the boolean expressions that represent tristate values; fixes #12

commit f3c0944
Author: Paul <[email protected]>
Date:   Thu Mar 15 13:46:01 2018 -0400

    bdd printing error; fixes #11

commit 7ea2149
Author: Paul <[email protected]>
Date:   Thu Mar 15 13:45:03 2018 -0400

    add debug levels

commit f6440c3
Merge: 0baf96d ee1d7f4
Author: paulgazz <[email protected]>
Date:   Wed Feb 28 17:11:34 2018 -0500

    Merge pull request #10 from paulgazz/doc_updates

    Doc updates

commit ee1d7f4
Author: Paul <[email protected]>
Date:   Wed Feb 28 17:03:12 2018 -0500

    added simple example run

commit 3bb553c
Author: Paul <[email protected]>
Date:   Wed Feb 28 16:57:10 2018 -0500

    example from the esecfse17 paper

commit fe03859
Author: Paul <[email protected]>
Date:   Mon Feb 5 16:05:05 2018 -0500

    add first available nonbool default value

commit e9fa4ed
Author: Paul <[email protected]>
Date:   Wed Jan 17 18:27:44 2018 -0500

    update kmax file format

commit 8cd5469
Author: Paul <[email protected]>
Date:   Wed Jan 17 18:27:23 2018 -0500

    support removing unselectable variables; support ghost bools for nonbool defaults

commit 6c940f2
Author: Paul <[email protected]>
Date:   Wed Jan 17 18:26:21 2018 -0500

    print out type of nonbools; depend on True for nonbools

commit 2b071e7
Author: Paul <[email protected]>
Date:   Tue Jan 9 12:15:59 2018 -0500

    updated description with selectability

commit 39e0353
Author: Paul <[email protected]>
Date:   Tue Jan 9 12:15:19 2018 -0500

    distinguish between user-selectable and non-user-selectable boolean variables; always emit defaults for non-user-selectable

commit 6d94083
Author: Paul <[email protected]>
Date:   Tue Jan 9 12:14:09 2018 -0500

    added flag to disable root var

commit fc2e33f
Author: Paul <[email protected]>
Date:   Fri Jan 5 18:20:57 2018 -0500

    remove from clauses any variables not declared with bool or nonbool

commit c890aa7
Author: Paul <[email protected]>
Date:   Fri Jan 5 18:20:30 2018 -0500

    reverse dependencies and nonselectable bools off by default;  there are new cli flags to turn them

commit 0baf96d
Author: Paul <[email protected]>
Date:   Wed Jan 3 09:59:05 2018 -0500

    support for busybox 1_22_stable in kmax script

commit 69733dd
Author: Paul <[email protected]>
Date:   Wed Jan 3 09:57:55 2018 -0500

    support for boolean default values that arent visible to the user

commit c69d0c4
Author: Paul <[email protected]>
Date:   Wed Jan 3 09:57:12 2018 -0500

    simple script to compare configs before and after make oldconfig

commit 44d1abe
Author: Paul <[email protected]>
Date:   Fri Dec 22 14:18:19 2017 -0500

    don't create the built-in config var

commit a49f641
Author: Paul <[email protected]>
Date:   Fri Dec 22 14:17:13 2017 -0500

    detailed description of the proto-dimacs format and usage instructions

commit feaeb76
Author: Paul <[email protected]>
Date:   Fri Dec 22 14:17:11 2017 -0500

    script to generated dimacs output from the .kmax output via --dimacs

commit 6cfc365
Author: Paul <[email protected]>
Date:   Fri Dec 22 14:16:06 2017 -0500

    the --dimacs action produces a special kmax format for postprocessing into dimacs

commit 1ff1511
Author: Paul <[email protected]>
Date:   Fri Dec 22 14:14:03 2017 -0500

    build v4.13
  • Loading branch information
paulgazz committed Nov 16, 2019
1 parent 0067a2b commit b61c55e
Show file tree
Hide file tree
Showing 583 changed files with 6,460 additions and 52,078 deletions.
4 changes: 4 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,2 +1,6 @@
*.pyc
*.pyo
*~
build/
kmax.egg-info/
dist/
File renamed without changes.
65 changes: 12 additions & 53 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,34 +1,14 @@
# Kmax

## Dependencies
Kmax collects configuration information from [Kbuild Makefiles](https://www.kernel.org/doc/html/latest/kbuild/makefiles.html). It determines, for each compilation unit, a symbolic Boolean expression that represents the conditions under which the file gets compiled and linked into the final program.

### lockfile
Kmax was created by [Paul Gazzillo](https://paulgazzillo.com). Its algorithm is described in this [publication](https://paulgazzillo.com/papers/esecfse17.pdf). The paper version of Kmax (v1.0) can be found [here](https://github.com/paulgazz/kmax/releases/tag/v1.0) along with other older [releases](https://github.com/paulgazz/kmax/releases) that have the Kconfig processing and other analysis scripts.

pip install lockfile
Special thanks to [ThanhVu Nguyen](https://cse.unl.edu/~tnguyen/) for helping to integrate z3 into Kmax.

Or
## pycudd

https://github.com/openstack/pylockfile

python setup.py install --user

### enum34

pip install lockfile

Or

https://pypi.python.org/packages/source/e/enum34/enum34-1.0.tar.gz#md5=9d57f5454c70c11707998ea26c1b0a7c

python setup.py install --user

### regex

Improved regular expression library

pip install regex

### pycudd
*pycudd usage is superseded by z3. this dependency will be removed in later versions.*

http://bears.ece.ucsb.edu/ftp/pub/pycudd2.0/pycudd2.0.2.tar.gz

Expand Down Expand Up @@ -59,47 +39,25 @@ Finally, go up to the parent directory, enter `pycudd/`, and build:

make FLAGS="-I /opt/python/include/python2.7/ -fPIC"

## Building Kmax

`check_dep` gathers constraints and other information from Kconfig files

# inside the kconfig/ directory
make

The Kbuild portion of Kmax is written in python, and needs no compilation. It depends on `pymake`, so install that with

# inside the kbuild/ directory
make

## Environment

Kmax expects several environment variables to be set:

KMAX_ROOT=/path/to/kmax/
PYCUDD_ROOT=/path/to/pycudd/
KMAX_SCRATCH=/path/to/kmax_scratch
KMAX_DATA=/path/to/kmax_data
export KMAX_ROOT PYCUDD_ROOT KMAX_SCRATCH KMAX_DATA

- set `KMAX_ROOT` to the path to the Kmax source directory
- set `PYCUDD_ROOT` to the path to the pycudd directory that
contains both pycudd itself and cudd-2.4.2
- set `KMAX_SCRATCH` to a new directory for storing downloaded source code
- set `KMAX_DATA` to a new directory to store kmax's output
export PYCUDD_ROOT=/path/to/pycudd/
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:${PYCUDD_ROOT}/cudd-2.4.2/lib

With those variables configured, modify the `PATH`, `PYTHONPATH`, and
`LD_LIBRARY_PATH` variables to point to kmax and pycudd like so:

export PATH=$PATH:${KMAX_ROOT}/kconfig:${KMAX_ROOT}/kbuild:$KMAX_ROOT/analysis
export PYTHONPATH=$PYTHONPATH:${PYCUDD_ROOT}/pycudd:${KMAX_ROOT}/lib
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:${PYCUDD_ROOT}/cudd-2.4.2/lib
export PATH=$PATH:${KMAX_ROOT}/kconfig:${KMAX_ROOT}/kbuild:${KMAX_ROOT}/kbuildplus:${KMAX_ROOT}/analysis
export PYTHONPATH=$PYTHONPATH:${KMAX_ROOT}/lib

## Simple example

This will run Kmax on the example from the
[paper](https://paulgazzillo.com/papers/esecfse17.pdf) on Kmax.

python kbuildplus/kbuildplus.py -B tests/kbuild/paper_example
python kmax/kbuildplus.py -B tests/kbuild/paper_example

This will output the list of configuration conditions for each compilation unit file in the example Kbuild file. The `-B` tells Kmax to treat configuration options as Boolean options (as opposed to Kconfig tristate options).

Expand All @@ -114,7 +72,8 @@ The `unit_pc` lines have the [format](docs/unit_pc.md) of compilation unit name
There is a script that will run Kmax on all Kbuild Makefiles from a project, e.g., the Linux kernel source code.

# from, e.g., the top-level directory of the linux-4.19.50 source code
python /path/to/kmax/kbuildplus/compilation_units.py -B -g $(make CC=cc ARCH=x86 -f /path/to/kmax/kbuild/makefile_override alldirs) | tee unit_pc
cd linux-source/
kmaxdriver.py -B -g $(make CC=cc ARCH=x86 -f /path/to/kmax/scripts/makefile_override alldirs) | tee unit_pc

The `-B` options means treat configuraion options as Boolean (as opposed to tristate) and `-g` means get the presence conditions in the `unit_pc` [format](docs/unit_pc.md). The `makefile_override` file will extract all the top-level source directories, e.g., drivers, kernel, etc, from the Linux build system. These are then each processed by Kmax, recursively entering any Kbuild subdirectories.

Expand Down
17 changes: 0 additions & 17 deletions analysis/Makefile

This file was deleted.

232 changes: 0 additions & 232 deletions analysis/collect_buildsystem.py

This file was deleted.

Loading

0 comments on commit b61c55e

Please sign in to comment.