mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git
synced 2026-03-08 18:26:12 +01:00
76e954155b
This commit introduces tnum_step(), a function that, when given t, and a
number z returns the smallest member of t larger than z. The number z
must be greater or equal to the smallest member of t and less than the
largest member of t.
The first step is to compute j, a number that keeps all of t's known
bits, and matches all unknown bits to z's bits. Since j is a member of
the t, it is already a candidate for result. However, we want our result
to be (minimally) greater than z.
There are only two possible cases:
(1) Case j <= z. In this case, we want to increase the value of j and
make it > z.
(2) Case j > z. In this case, we want to decrease the value of j while
keeping it > z.
(Case 1) j <= z
t = xx11x0x0
z = 10111101 (189)
j = 10111000 (184)
^
k
(Case 1.1) Let's first consider the case where j < z. We will address j
== z later.
Since z > j, there had to be a bit position that was 1 in z and a 0 in
j, beyond which all positions of higher significance are equal in j and
z. Further, this position could not have been unknown in a, because the
unknown positions of a match z. This position had to be a 1 in z and
known 0 in t.
Let k be position of the most significant 1-to-0 flip. In our example, k
= 3 (starting the count at 1 at the least significant bit). Setting (to
1) the unknown bits of t in positions of significance smaller than
k will not produce a result > z. Hence, we must set/unset the unknown
bits at positions of significance higher than k. Specifically, we look
for the next larger combination of 1s and 0s to place in those
positions, relative to the combination that exists in z. We can achieve
this by concatenating bits at unknown positions of t into an integer,
adding 1, and writing the bits of that result back into the
corresponding bit positions previously extracted from z.
>From our example, considering only positions of significance greater
than k:
t = xx..x
z = 10..1
+ 1
-----
11..0
This is the exact combination 1s and 0s we need at the unknown bits of t
in positions of significance greater than k. Further, our result must
only increase the value minimally above z. Hence, unknown bits in
positions of significance smaller than k should remain 0. We finally
have,
result = 11110000 (240)
(Case 1.2) Now consider the case when j = z, for example
t = 1x1x0xxx
z = 10110100 (180)
j = 10110100 (180)
Matching the unknown bits of the t to the bits of z yielded exactly z.
To produce a number greater than z, we must set/unset the unknown bits
in t, and *all* the unknown bits of t candidates for being set/unset. We
can do this similar to Case 1.1, by adding 1 to the bits extracted from
the masked bit positions of z. Essentially, this case is equivalent to
Case 1.1, with k = 0.
t = 1x1x0xxx
z = .0.1.100
+ 1
---------
.0.1.101
This is the exact combination of bits needed in the unknown positions of
t. After recalling the known positions of t, we get
result = 10110101 (181)
(Case 2) j > z
t = x00010x1
z = 10000010 (130)
j = 10001011 (139)
^
k
Since j > z, there had to be a bit position which was 0 in z, and a 1 in
j, beyond which all positions of higher significance are equal in j and
z. This position had to be a 0 in z and known 1 in t. Let k be the
position of the most significant 0-to-1 flip. In our example, k = 4.
Because of the 0-to-1 flip at position k, a member of t can become
greater than z if the bits in positions greater than k are themselves >=
to z. To make that member *minimally* greater than z, the bits in
positions greater than k must be exactly = z. Hence, we simply match all
of t's unknown bits in positions more significant than k to z's bits. In
positions less significant than k, we set all t's unknown bits to 0
to retain minimality.
In our example, in positions of greater significance than k (=4),
t=x000. These positions are matched with z (1000) to produce 1000. In
positions of lower significance than k, t=10x1. All unknown bits are set
to 0 to produce 1001. The final result is:
result = 10001001 (137)
This concludes the computation for a result > z that is a member of t.
The procedure for tnum_step() in this commit implements the idea
described above. As a proof of correctness, we verified the algorithm
against a logical specification of tnum_step. The specification asserts
the following about the inputs t, z and output res that:
1. res is a member of t, and
2. res is strictly greater than z, and
3. there does not exist another value res2 such that
3a. res2 is also a member of t, and
3b. res2 is greater than z
3c. res2 is smaller than res
We checked the implementation against this logical specification using
an SMT solver. The verification formula in SMTLIB format is available
at [1]. The verification returned an "unsat": indicating that no input
assignment exists for which the implementation and the specification
produce different outputs.
In addition, we also automatically generated the logical encoding of the
C implementation using Agni [2] and verified it against the same
specification. This verification also returned an "unsat", confirming
that the implementation is equivalent to the specification. The formula
for this check is also available at [3].
Link: https://pastebin.com/raw/2eRWbiit [1]
Link: https://github.com/bpfverif/agni [2]
Link: https://pastebin.com/raw/EztVbBJ2 [3]
Co-developed-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Signed-off-by: Srinivas Narayana <srinivas.narayana@rutgers.edu>
Co-developed-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Santosh Nagarakatte <santosh.nagarakatte@rutgers.edu>
Signed-off-by: Harishankar Vishwanathan <harishankar.vishwanathan@gmail.com>
Link: https://lore.kernel.org/r/93fdf71910411c0f19e282ba6d03b4c65f9c5d73.1772225741.git.paul.chaignon@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
138 lines
4.7 KiB
C
138 lines
4.7 KiB
C
/* tnum: tracked (or tristate) numbers
|
|
*
|
|
* A tnum tracks knowledge about the bits of a value. Each bit can be either
|
|
* known (0 or 1), or unknown (x). Arithmetic operations on tnums will
|
|
* propagate the unknown bits such that the tnum result represents all the
|
|
* possible results for possible values of the operands.
|
|
*/
|
|
|
|
#ifndef _LINUX_TNUM_H
|
|
#define _LINUX_TNUM_H
|
|
|
|
#include <linux/types.h>
|
|
|
|
struct tnum {
|
|
u64 value;
|
|
u64 mask;
|
|
};
|
|
|
|
/* Constructors */
|
|
/* Represent a known constant as a tnum. */
|
|
struct tnum tnum_const(u64 value);
|
|
/* A completely unknown value */
|
|
extern const struct tnum tnum_unknown;
|
|
/* An unknown value that is a superset of @min <= value <= @max.
|
|
*
|
|
* Could include values outside the range of [@min, @max].
|
|
* For example tnum_range(0, 2) is represented by {0, 1, 2, *3*},
|
|
* rather than the intended set of {0, 1, 2}.
|
|
*/
|
|
struct tnum tnum_range(u64 min, u64 max);
|
|
|
|
/* Arithmetic and logical ops */
|
|
/* Shift a tnum left (by a fixed shift) */
|
|
struct tnum tnum_lshift(struct tnum a, u8 shift);
|
|
/* Shift (rsh) a tnum right (by a fixed shift) */
|
|
struct tnum tnum_rshift(struct tnum a, u8 shift);
|
|
/* Shift (arsh) a tnum right (by a fixed min_shift) */
|
|
struct tnum tnum_arshift(struct tnum a, u8 min_shift, u8 insn_bitness);
|
|
/* Add two tnums, return @a + @b */
|
|
struct tnum tnum_add(struct tnum a, struct tnum b);
|
|
/* Subtract two tnums, return @a - @b */
|
|
struct tnum tnum_sub(struct tnum a, struct tnum b);
|
|
/* Neg of a tnum, return 0 - @a */
|
|
struct tnum tnum_neg(struct tnum a);
|
|
/* Bitwise-AND, return @a & @b */
|
|
struct tnum tnum_and(struct tnum a, struct tnum b);
|
|
/* Bitwise-OR, return @a | @b */
|
|
struct tnum tnum_or(struct tnum a, struct tnum b);
|
|
/* Bitwise-XOR, return @a ^ @b */
|
|
struct tnum tnum_xor(struct tnum a, struct tnum b);
|
|
/* Multiply two tnums, return @a * @b */
|
|
struct tnum tnum_mul(struct tnum a, struct tnum b);
|
|
|
|
/* Return true if the known bits of both tnums have the same value */
|
|
bool tnum_overlap(struct tnum a, struct tnum b);
|
|
|
|
/* Return a tnum representing numbers satisfying both @a and @b */
|
|
struct tnum tnum_intersect(struct tnum a, struct tnum b);
|
|
|
|
/* Returns a tnum representing numbers satisfying either @a or @b */
|
|
struct tnum tnum_union(struct tnum t1, struct tnum t2);
|
|
|
|
/* Return @a with all but the lowest @size bytes cleared */
|
|
struct tnum tnum_cast(struct tnum a, u8 size);
|
|
|
|
/* Swap the bytes of a tnum */
|
|
struct tnum tnum_bswap16(struct tnum a);
|
|
struct tnum tnum_bswap32(struct tnum a);
|
|
struct tnum tnum_bswap64(struct tnum a);
|
|
|
|
/* Returns true if @a is a known constant */
|
|
static inline bool tnum_is_const(struct tnum a)
|
|
{
|
|
return !a.mask;
|
|
}
|
|
|
|
/* Returns true if @a == tnum_const(@b) */
|
|
static inline bool tnum_equals_const(struct tnum a, u64 b)
|
|
{
|
|
return tnum_is_const(a) && a.value == b;
|
|
}
|
|
|
|
/* Returns true if @a is completely unknown */
|
|
static inline bool tnum_is_unknown(struct tnum a)
|
|
{
|
|
return !~a.mask;
|
|
}
|
|
|
|
/* Returns true if @a is known to be a multiple of @size.
|
|
* @size must be a power of two.
|
|
*/
|
|
bool tnum_is_aligned(struct tnum a, u64 size);
|
|
|
|
/* Returns true if @b represents a subset of @a.
|
|
*
|
|
* Note that using tnum_range() as @a requires extra cautions as tnum_in() may
|
|
* return true unexpectedly due to tnum limited ability to represent tight
|
|
* range, e.g.
|
|
*
|
|
* tnum_in(tnum_range(0, 2), tnum_const(3)) == true
|
|
*
|
|
* As a rule of thumb, if @a is explicitly coded rather than coming from
|
|
* reg->var_off, it should be in form of tnum_const(), tnum_range(0, 2**n - 1),
|
|
* or tnum_range(2**n, 2**(n+1) - 1).
|
|
*/
|
|
bool tnum_in(struct tnum a, struct tnum b);
|
|
|
|
/* Formatting functions. These have snprintf-like semantics: they will write
|
|
* up to @size bytes (including the terminating NUL byte), and return the number
|
|
* of bytes (excluding the terminating NUL) which would have been written had
|
|
* sufficient space been available. (Thus tnum_sbin always returns 64.)
|
|
*/
|
|
/* Format a tnum as a pair of hex numbers (value; mask) */
|
|
int tnum_strn(char *str, size_t size, struct tnum a);
|
|
/* Format a tnum as tristate binary expansion */
|
|
int tnum_sbin(char *str, size_t size, struct tnum a);
|
|
|
|
/* Returns the 32-bit subreg */
|
|
struct tnum tnum_subreg(struct tnum a);
|
|
/* Returns the tnum with the lower 32-bit subreg cleared */
|
|
struct tnum tnum_clear_subreg(struct tnum a);
|
|
/* Returns the tnum with the lower 32-bit subreg in *reg* set to the lower
|
|
* 32-bit subreg in *subreg*
|
|
*/
|
|
struct tnum tnum_with_subreg(struct tnum reg, struct tnum subreg);
|
|
/* Returns the tnum with the lower 32-bit subreg set to value */
|
|
struct tnum tnum_const_subreg(struct tnum a, u32 value);
|
|
/* Returns true if 32-bit subreg @a is a known constant*/
|
|
static inline bool tnum_subreg_is_const(struct tnum a)
|
|
{
|
|
return !(tnum_subreg(a)).mask;
|
|
}
|
|
|
|
/* Returns the smallest member of t larger than z */
|
|
u64 tnum_step(struct tnum t, u64 z);
|
|
|
|
#endif /* _LINUX_TNUM_H */
|