If we run into our special BPF_PSEUDO_MAP_ORACLE instruction in the
interpreter, we need to run the oracle test to check for inconsistencies
between concrete values and verifier states. This patch implements that
check and throws a kernel warning if any inconsistency is found.

The kernel warning message looks as follows, if only R6 was found not to
match some states:

    oracle caught invalid states in oracle_map[id:21]: r6=0xffffffffffffffd4

Signed-off-by: Paul Chaignon <paul.chaignon@gmail.com>
---
 include/linux/bpf_verifier.h |  1 +
 include/linux/tnum.h         |  3 ++
 kernel/bpf/core.c            | 12 +++++--
 kernel/bpf/oracle.c          | 65 ++++++++++++++++++++++++++++++++++++
 kernel/bpf/tnum.c            |  5 +++
 5 files changed, 84 insertions(+), 2 deletions(-)

diff --git a/include/linux/bpf_verifier.h b/include/linux/bpf_verifier.h
index cffbd0552b43..6a53087cdd1d 100644
--- a/include/linux/bpf_verifier.h
+++ b/include/linux/bpf_verifier.h
@@ -1130,5 +1130,6 @@ int save_state_in_oracle(struct bpf_verifier_env *env, int insn_idx);
 struct bpf_prog *patch_oracle_check_insn(struct bpf_verifier_env *env, struct bpf_insn *insn,
 					 int i, int *cnt);
 int create_and_populate_oracle_map(struct bpf_verifier_env *env);
+void oracle_test(struct bpf_map *oracle_states, u64 *regs);
 
 #endif /* _LINUX_BPF_VERIFIER_H */
diff --git a/include/linux/tnum.h b/include/linux/tnum.h
index c52b862dad45..e028869371ca 100644
--- a/include/linux/tnum.h
+++ b/include/linux/tnum.h
@@ -54,6 +54,9 @@ 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 true if tnum a matches value b. */
+bool tnum_match(struct tnum a, u64 b);
+
 /* Return a tnum representing numbers satisfying both @a and @b */
 struct tnum tnum_intersect(struct tnum a, struct tnum b);
 
diff --git a/kernel/bpf/core.c b/kernel/bpf/core.c
index 67226145a4db..fe251f1ff703 100644
--- a/kernel/bpf/core.c
+++ b/kernel/bpf/core.c
@@ -1848,10 +1848,18 @@ static u64 ___bpf_prog_run(u64 *regs, const struct bpf_insn *insn)
 	ALU64_MOV_K:
 		DST = IMM;
 		CONT;
-	LD_IMM_DW:
-		DST = (u64) (u32) insn[0].imm | ((u64) (u32) insn[1].imm) << 32;
+	LD_IMM_DW: {
+		u64 address = (u64)(u32)insn[0].imm | ((u64)(u32)insn[1].imm) << 32;
+
+		if (insn[0].src_reg == BPF_PSEUDO_MAP_ORACLE) {
+			oracle_test((struct bpf_map *)address, regs);
+			insn++;
+			CONT;
+		}
+		DST = address;
 		insn++;
 		CONT;
+	}
 	ALU_ARSH_X:
 		DST = (u64) (u32) (((s32) DST) >> (SRC & 31));
 		CONT;
diff --git a/kernel/bpf/oracle.c b/kernel/bpf/oracle.c
index 44b86e6ef3b2..ce330853b53f 100644
--- a/kernel/bpf/oracle.c
+++ b/kernel/bpf/oracle.c
@@ -8,6 +8,8 @@
 
 #include <linux/bpf_verifier.h>
 
+#define REGS_FMT_BUF_LEN 221
+
 static void convert_oracle_state(struct bpf_verifier_state *istate, struct bpf_oracle_state *ostate)
 {
 	struct bpf_func_state *frame = istate->frame[istate->curframe];
@@ -320,3 +322,66 @@ int create_and_populate_oracle_map(struct bpf_verifier_env *env)
 
 	return populate_oracle_map(env, oracle_map);
 }
+
+static bool oracle_test_reg(struct bpf_reg_oracle_state *exp, u64 reg)
+{
+	if (exp->scalar) {
+		if (reg < exp->umin_value || reg > exp->umax_value ||
+		    (s64)reg < exp->smin_value || (s64)reg > exp->smax_value ||
+		    (u32)reg < exp->u32_min_value || (u32)reg > exp->u32_max_value ||
+		    (s32)reg < exp->s32_min_value || (s32)reg > exp->s32_max_value ||
+		    !tnum_match(exp->var_off, reg))
+			return true;
+	} else if (exp->ptr_not_null && !reg) {
+		return true;
+	}
+	return false;
+}
+
+static bool oracle_test_state(struct bpf_oracle_state *state, u64 *regs, u32 *non_match_regs)
+{
+	int i;
+
+	for (i = 0; i < MAX_BPF_REG - 1; i++) {
+		if (oracle_test_reg(&state->regs[i], regs[i])) {
+			*non_match_regs |= 1 << i;
+			return true;
+		}
+	}
+
+	return false;
+}
+
+static void format_non_match_regs(u32 non_match_regs, u64 *regs, char *buf)
+{
+	int i, delta = 0;
+
+	for (i = 0; i < MAX_BPF_REG - 1; i++) {
+		if (non_match_regs & (1 << i)) {
+			delta += snprintf(buf + delta, REGS_FMT_BUF_LEN - delta, "r%d=%#llx ",
+					  i, regs[i]);
+		}
+	}
+}
+
+void oracle_test(struct bpf_map *oracle_states, u64 *regs)
+{
+	struct bpf_oracle_state *state;
+	u32 non_match_regs = 0;
+	char regs_fmt[REGS_FMT_BUF_LEN];
+	bool expected = false;
+	int i;
+
+	for (i = 0; i < oracle_states->max_entries; i++) {
+		state = oracle_states->ops->map_lookup_elem(oracle_states, &i);
+		if (!oracle_test_state(state, regs, &non_match_regs)) {
+			expected = true;
+			break;
+		}
+	}
+	if (!expected) {
+		format_non_match_regs(non_match_regs, regs, regs_fmt);
+		BPF_WARN_ONCE(1, "oracle caught invalid states in oracle_map[id:%d]: %s\n",
+			      oracle_states->id, regs_fmt);
+	}
+}
diff --git a/kernel/bpf/tnum.c b/kernel/bpf/tnum.c
index f8e70e9c3998..afe7adf6a6f5 100644
--- a/kernel/bpf/tnum.c
+++ b/kernel/bpf/tnum.c
@@ -167,6 +167,11 @@ bool tnum_overlap(struct tnum a, struct tnum b)
 	return (a.value & mu) == (b.value & mu);
 }
 
+bool tnum_match(struct tnum a, u64 b)
+{
+	return (a.value & ~a.mask) == (b & ~a.mask);
+}
+
 /* Note that if a and b disagree - i.e. one has a 'known 1' where the other has
  * a 'known 0' - this will return a 'known 1' for that bit.
  */
-- 
2.43.0