umount-test-opts - README.md

 1# umount-test-opts
 2
 3This repository contains files to perform equivalence testing of the `-O` option implementation for `umount(8)` shipped with [BusyBox](https://busybox.net/) and [util-linux](https://git.kernel.org/cgit/utils/util-linux/util-linux.git).
 4
 5## Background
 6
 7The `-O` option provided by `umount(8)` unmounts file systems by mount options.
 8This is implemented by checking the mount options of a file system against a provided pattern.
 9The function that performs this comparison is called [`mnt_match_options()`](https://cdn.kernel.org/pub/linux/utils/util-linux/v2.37/libmount-docs/libmount-Options-string.html#mnt-match-options) in util-linux.
10Vanilla BusyBox does not provide this feature, but I have written a patch that [adds this feature to BusyBox](http://lists.busybox.net/pipermail/busybox/2022-June/089769.html).
11The corresponding function is called `fsopts_matches` in my patch.
12This is an attempt to check if my BusyBox implementation of this feature is "correct".
13This setup has found one [undefined behavior bug in util-linux](https://git.kernel.org/pub/scm/utils/util-linux/util-linux.git/commit/?id=06ee5267516761721ebfbdfa313980cef8e54c66) and two functional errors in [my BusyBox patch](http://lists.busybox.net/pipermail/busybox/2023-March/090193.html).
14
15## Setup
16
17The setup provided here uses [symbolic execution](https://en.wikipedia.org/wiki/Symbolic_execution) with [KLEE](https://klee.github.io) to ensure that both implementations always return the same value for the same input strings via an assertion in the test harness:
18
19    assert(mnt_match_options(options, pattern) == fsopts_matches(options, pattern));
20
21This is a well-known idea that is already mentioned in the [original KLEE paper](https://www.usenix.org/legacy/events/osdi08/tech/full_papers/cadar/cadar.pdf) (Section 5.5).
22For two 7 byte inputs, KLEE finds 70119 execution paths for this assertion under the constraints mentioned below.
23On all of these execution paths, the assertion holds.
24On an AMD Ryzen 5700, this takes around 4 minutes.
25
26## Usage
27
28Ideally, use this repository with [Guix](https://guix.gnu.org):
29
30    $ guix time-machine -C channels.scm -- shell
31
32Within the Guix shell run the following commands:
33
34    $ make sim
35
36Alternatively, you can also try to use KLEE's [Docker](https://www.docker.io/) image:
37
38    $ docker run --rm -it klee/klee -v "$(pwd):/code"
39
40Within the container run:
41
42    $ cd /code
43    $ make sim
44
45## Limitations
46
47* The equivalence checked is only performed for fixed-size strings of length `N`.
48* Support for `key=value` mount options is not implemented in BusyBox, hence the input is constrained to `[-,+A-Za-z]`.
49* The inputs always have a length of `INPUT_SIZE` since the aforementioned constraint does not include null terminators.