| Age | Commit message (Collapse) | Author | Files | Lines |
|---|
|
Some instruction simplifications can be quite tricky and thus easy to
get wrong. Often, they also are hard to test (for example, you can
test it with a few input values but of course not all combinations).
I'm used to validate some of these with an independent tool
(Alive cfr. [1], [2]) which is quite neat but has some issues:
1) This tool doesn't work with Sparse's IR or C source but it needs to
have the tests written in its own language (very close to LLVM's IR).
So it can be used to test if the logic of a simplification but
not if implemented correctly.
2) This tool isn't maintained anymore (has some bugs too) and it's
successor (Alive2 [3]) is not quite as handy to me (I miss the
pre-conditions a lot).
So, this patch implement the same idea but fully integrated with
Sparse. This mean that you can write a test in C, let Sparse process
and simplify it and then directly validate it and not only for
a few values but symbolically, for all possible values.
Note: Of course, this is not totally stand-alone and depends on
an external library for the solver (Boolector, see [4], [5]).
Note: Currently, it's just a proof of concept and, except the
included tests, it's only very slightly tested (and untested
with anything more complex than a few instructions).
[1] https://blog.regehr.org/archives/1170
[2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf
[3] https://blog.regehr.org/archives/1722
[4] https://boolector.github.io/
[5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
The current .gitignore specifies that the generated programs
must be ignored. Good.
However, this is done by just specifying the name of the program
which has the effect of having any files or directories with the
same name to be ignored too. This is not intended.
Fix this using the pattern '/<name>' instead so that they match
in the root folder.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
The name 'sindex' is already used by another package (biosquid).
So it was decided to rename it to 'semind'.
Signed-off-by: Alexey Gladkov <gladkov.alexey@gmail.com>
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
sindex is the simple to use cscope-like tool based on sparse/dissect.
Unlike cscope it runs after pre-processor and thus it can't index the
code filtered out by ifdef's, but otoh it understands how the symbol
is used and it can track the usage of struct members.
To create an index for your linux kernel configuration:
$ make C=2 CHECK="sindex add --"
Now, to find where a definition of the pid field from the task_struct
structure:
$ sindex search -m def task_struct.pid
(def) include/linux/sched.h 793 11 pid_t pid;
default output format:
SOURCE-FILE \t LINE-NUMBER \t COLUMN \t IN FUNCTION NAME \t CODE LINE
To find where this field changes:
$ sindex search -m w task_struct.pid
(-w-) fs/exec.c 1154 6 de_thread tsk->pid = leader->pid;
(-w-) kernel/fork.c 2155 3 copy_process p->pid = pid_nr(pid);
To get only filenames and line number you can change output format:
$ sindex search -f '%f:%l' -m w task_struct.pid
fs/exec.c:1154
kernel/fork.c:2155
Current limitations:
* inline functions are ignored;
* enums are ignored;
* unknown #include leads to a fatal error.
Suggested-by: Oleg Nesterov <oleg@redhat.com>
Signed-off-by: Oleg Nesterov <oleg@redhat.com>
Signed-off-by: Alexey Gladkov <gladkov.alexey@gmail.com>
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
* clarify lazy evaluation & conversion of SYM_TYPEOF
|
|
Add another small client doing nothing but display the type
of the toplevel symbols.
This will help to test further changes in do_show_type().
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
The patterns have most probably been added in a queue-like way
but it makes harder to see what's in and what's not.
So, alphasort them.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Ignore any ~ files left in the repository.
Signed-off-by: Ben Dooks <ben.dooks@codethink.co.uk>
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Add a tool which parse comment from source files and
extract kerneldoc-like documentation from them.
Note: this is rather quite crude, support only generic 'blocs'
and doc for functions; it has no support for anything else.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
So people who like this file to be a hidden one or to be an
out-of-tree file or simply who don't like the name, can choose
whatever suits them the best.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Sparse being a library was installed as such and with support for
pkgconfig.
However, it seems that sparse is only used for its tools and not
as a library (at least not as an external one) and currently
doesn't offer a stable interface.
For now, remove the support for this, it will be easy enough to
restore it if there is a new need.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
|
|
Signed-off-by: Tony Camuso <tcamuso@redhat.com>
Signed-off-by: Christopher Li <sparse@chrisli.org>
|
|
Signed-off-by: Emilio G. Cota <cota@braap.org>
Signed-off-by: Christopher Li <sparse@chrisli.org>
|
|
This is the first commit to implementing a LLVM backend for sparse using the
LLVM C bindings.
Signed-off-by: Pekka Enberg <penberg@kernel.org>
|
|
Signed-off-by: Dan Carpenter <error27@gmail.com>
Signed-off-by: Christopher Li <sparse@chrisli.org>
|
|
This will allow users to override build settings without dirtying their
trees, making life with `git stash' a bit easier.
Signed-off-by: Samuel Bronson <naesten@gmail.com>
Signed-off-by: Christopher Li <sparse@chrisli.org>
|
|
Signed-off-by: Martin Nagy <nagy.martin@gmail.com>
Signed-off-by: Christopher Li <sparse@chrisli.org>
|
|
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
.gitignore contained an entry for .*, ignoring all dotfiles. Among other
things, that ignores .gitignore, requiring git add -f. Remove that entry.
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
This avoids ignoring .diff outside of the validation directory.
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
This patch introduces test-suite, a simple script that makes test cases
verification easier. Test cases in the validation directory are annotated
and this script parses them to check if the actual result is the one
expected by the test writer.
Signed-off-by: Damien Lespiau <damien.lespiau@gmail.com>
|
|
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
The Makefile now generates and installs a pkg-config file, sparse.pc, to
provide information about the installed Sparse library and header files. Use
`pkg-config --cflags sparse` to get the include path, and `pkg-config --libs
sparse` to get the library path and library.
To help packagers of Sparse, also add support for the DESTDIR variable to the
Makefile. DESTDIR allows you to target a particular prefix (such as /usr),
but install to another directory (such as debian/tmp), usually for the
purposes of subsequently constructing a package from that directory.
Previously, just setting PREFIX would work for that, but with the new
pkg-config file, the Makefile needs to know the real prefix.
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
Signed-off-by: Josh Triplett <josh@freedesktop.org>
|
|
Ignore tags and git frontends' files.
Signed-off-by: Damien Lespiau <damien.lespiau@gmail.com>
|
|
Add a new backend program which parses the input files, processes them through
the linearization pass, and outputs a graphviz graph of the resulting basic
blocks. Each entrypoint gets labelled by name, but for now the basic blocks
just get labelled with the address of the basic_block structure.
Signed-off-by: Josh Triplett <josh@freedesktop.org>
Signed-off-by: Linus Torvalds <torvalds@osdl.org>
|
|
Signed-off-by: Josh Triplett <josh@freedesktop.org>
Signed-off-by: Linus Torvalds <torvalds@osdl.org>
|
|
For now, it use a simple method but which introduces a lot more copies
than necessary. Can be fixed later.
Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@looxix.net>
Signed-off-by: Linus Torvalds <torvalds@osdl.org>
|
|
|
