Improvements to dependency tracking (#69)

So far dependency tracking in bpfvv relied only on interpretation of
individual instructions. For example, `r1 = r6` is parsed as ALU
instruction that *reads* r6 and *writes* to r1.

BPF verifier often prints relevant values for instructions, and bpfvv
of course parses them to build an array of BpfState objects.

This change expands the dependency tracking to include information
about value changes, as reported by the verifier.

For example:

    26: (bf) r6 = r0 ; R0_w=map_value_or_null(id=1,map=bpfj_pod_map,ks=4,vs=1040) R6_w=map_value_or_null(id=1,map=bpfj_pod_map,ks=4,vs=1040)
    ...
    29: (15) if r6 == 0x0 goto pc+27 ; R6=map_value(map=bpfj_pod_map,ks=4,vs=1040)

Note that the value of r6 has changed from `map_value_or_null` to
`map_value`, even though there was no actual writes to r6 in the
instruction stream. It is correct however, because in this trace
verifier is exploring a branch where r6 is not equal to 0, and so it's
value (as interpreted by the verifier) did actually change.

In bpfvv, we can notice such value changes and take them into account
when calculating dependencies. This also has an additional benefit of
indirect stack access tracking, at least in simple cases, such as:

    525: (bf) r1 = r10                    ; frame2: R1_w=fp0 R10=fp0
    526: (07) r1 += -24                   ; frame2: R1_w=fp-24
    ...
    529: (7b) *(u64 *)(r1 +0) = r8        ; frame2: R1_w=fp-24 R8=scalar(id=102) fp-24_w=scalar(id=102)
    ...
    999: (79) r6 = *(u64 *)(r10 -24) ;

With this change, the user can now see the dependency of instruction
at 999 on 529, even though stack access is indirect.

Author: theihor

src/__snapshots__/App.test.tsx.snap

@@ -276,13 +276,17 @@ exports[`App renders the log visualizer when text is pasted 1`] = `
                   </td>
                 </tr>
                 <tr
-                  class="effect-read"
+                  class="effect-write"
                 >
                   <td>
                     r1
                   </td>
                   <td>
                     <span>
+                      ctx()
+                       
+                      -&gt;
+                       
                       0
                     </span>
                   </td>
@@ -338,13 +342,16 @@ exports[`App renders the log visualizer when text is pasted 1`] = `
                   </td>
                 </tr>
                 <tr
-                  class="effect-read"
+                  class="effect-write"
                 >
                   <td>
                     r7
                   </td>
                   <td>
                     <span>
+                       
+                      -&gt;
+                       
                       map_value(off=0,ks=4,vs=2808,imm=0)
                     </span>
                   </td>

src/analyzer.test.ts

@@ -185,6 +185,41 @@ ERROR: Loading BPF object(s) failed.
     });
   });
 
+  describe("processes indirect stack access correctly", () => {
+    const sampleLog = `
+525: (bf) r1 = r10                    ; R1_w=fp0 R10=fp0
+526: (07) r1 += -24                   ; R1_w=fp-24
+527: (79) r2 = *(u64 *)(r10 -56)      ; R2_w=0 R10=fp0 fp-56=0
+528: (0f) r1 += r2
+529: (7b) *(u64 *)(r1 +0) = r8        ; R1_w=fp-24 R8=scalar(id=102) fp-24_w=scalar(id=102)
+900: (bf) r2 = r10                    ; R2_w=fp0 R10=fp0
+901: (07) r2 += -24                   ; R2_w=fp-24
+902: (79) r6 = *(u64 *)(r2 +0)        ; R2=fp-24 R6_w=scalar(id=102) fp-24=scalar(id=102)
+`;
+    const bpfStates = bpfStatesFromLog(sampleLog);
+    it("*(u64 *)(r1 +0) = r8", () => {
+      const s = bpfStates[4];
+      expect(s.frame).toBe(0);
+      expect(s.idx).toBe(4);
+      expect(s.pc).toBe(529);
+      expect(s.values.get("fp-24")).toMatchObject({
+        value: "scalar(id=102)",
+        effect: Effect.WRITE,
+      });
+    });
+
+    it("r6 = *(u64 *)(r2 +0)", () => {
+      const s = bpfStates[7];
+      expect(s.frame).toBe(0);
+      expect(s.idx).toBe(7);
+      expect(s.pc).toBe(902);
+      expect(s.values.get("fp-24")).toMatchObject({
+        value: "scalar(id=102)",
+      });
+      expect(s.lastKnownWrites.get("fp-24")).toBe(4);
+    });
+  });
+
   const verifierLogFragmentWithASubprogramCall = `
 702: (bf) r1 = r7                     ; frame0: R1_w=map_value(off=0,ks=4,vs=2808,imm=0) R7=map_value(off=0,ks=4,vs=2808,imm=0)
 703: (bf) r2 = r6                     ; frame0: R2_w=rcu_ptr_task_struct(off=0,imm=0) R6=rcu_ptr_task_struct(off=0,imm=0)
@@ -215,10 +250,7 @@ to caller at 705:
       expect(s.frame).toBe(0);
       expect(s.idx).toBe(0);
       expect(s.pc).toBe(702);
-      expect(s.values.get("r7")).toMatchObject({
-        value: r1Value,
-        effect: Effect.READ,
-      });
+      expect(s.values.get("r7")?.value).toBe(r1Value);
       expect(s.values.get("r1")).toMatchObject({
         value: r1Value,
         effect: Effect.WRITE,
@@ -230,10 +262,7 @@ to caller at 705:
       expect(s.frame).toBe(0);
       expect(s.idx).toBe(1);
       expect(s.pc).toBe(703);
-      expect(s.values.get("r6")).toMatchObject({
-        value: r2Value,
-        effect: Effect.READ,
-      });
+      expect(s.values.get("r6")?.value).toBe(r2Value);
       expect(s.values.get("r2")).toMatchObject({
         value: r2Value,
         effect: Effect.WRITE,

src/analyzer.ts

@@ -85,8 +85,6 @@ export function makeValue(
   prevValue: string = "",
 ): BpfValue {
   const ret: BpfValue = { value, effect };
-  // @Hack display fp0 as fp-0
-  if (ret.value === "fp0") ret.value = "fp-0";
   if (prevValue) ret.prevValue = prevValue;
   return ret;
 }
@@ -97,7 +95,7 @@ export function initialBpfState(): BpfState {
     values.set(`r${i}`, { value: "", effect: Effect.NONE });
   }
   values.set("r1", makeValue("ctx()"));
-  values.set("r10", makeValue("fp0"));
+  values.set("r10", makeValue("fp-0"));
   let lastKnownWrites = new Map<string, number>();
   lastKnownWrites.set("r1", 0);
   lastKnownWrites.set("r10", 0);
@@ -156,7 +154,7 @@ function pushStackFrame(
   for (const r of ["r0", ...BPF_CALLEE_SAVED_REGS]) {
     values.set(r, { value: "", effect: Effect.WRITE });
   }
-  values.set("r10", makeValue("fp0"));
+  values.set("r10", makeValue("fp-0"));
 
   let lastKnownWrites = new Map<string, number>();
   for (const r of BPF_SCRATCH_REGS) {
@@ -245,10 +243,18 @@ function nextBpfState(
     newState.lastKnownWrites.set(id, line.idx);
   }
 
-  // verifier reported values
+  // If verifier reported a particular expr, it overrides any values we may have computed so far
+  // This means, for example, that conditions can be UPDATEs
   for (const expr of line.bpfStateExprs) {
-    const effect = effects.get(expr.id) || Effect.NONE;
     const val: BpfValue | undefined = newState.values.get(expr.id);
+    let effect = effects.get(expr.id) || Effect.NONE;
+    if (!val) {
+      effect = Effect.WRITE;
+      newState.lastKnownWrites.set(expr.id, line.idx);
+    } else if (expr.value !== val.value && effect !== Effect.WRITE) {
+      effect = Effect.UPDATE;
+      newState.lastKnownWrites.set(expr.id, line.idx);
+    }
     newState.values.set(
       expr.id,
       makeValue(expr.value, effect, val?.prevValue || ""),
@@ -409,7 +415,7 @@ export function getMemSlotDependencies(
 
       deps = getMemSlotDependencies(verifierLogState, prevDepIdx, memSlotId);
     }
-  } else if (nReads === 1) {
+  } else if (nReads === 1 && depIdx !== bpfState.idx) {
     deps = getMemSlotDependencies(verifierLogState, depIdx, depIns.reads[0]);
   }
 

src/parser.ts

@@ -275,11 +275,9 @@ const parseBpfStateExpr = (
     }
     i++;
   }
-  const expr = {
-    id,
-    value: str.substring(equalsIndex + 1, i),
-    rawKey: key,
-  };
+  let value = str.substring(equalsIndex + 1, i);
+  if (value === "fp0") value = "fp-0"; // normalize fp0 to fp-0
+  const expr = { id, value, rawKey: key };
   return { expr, rest: str.substring(i) };
 };
 
@@ -645,6 +643,14 @@ function parseConditionalJmp(
   const target = jmpTarget.match[2];
   rest = consumeSpaces(jmpTarget.rest);
 
+  const reads = [];
+  if (leftOp.op.type !== OperandType.IMM) {
+    reads.push(leftOp.op.id);
+  }
+  if (rightOp.op.type !== OperandType.IMM) {
+    reads.push(rightOp.op.id);
+  }
+
   const ins: BpfConditionalJmpInstruction = {
     kind: BpfInstructionKind.JMP,
     jmpKind: BpfJmpKind.CONDITIONAL_GOTO,
@@ -655,7 +661,7 @@ function parseConditionalJmp(
       op: operator,
       right: rightOp.op,
     },
-    reads: [leftOp.op.id, rightOp.op.id],
+    reads,
     writes: [], // technically goto writes pc, but we don't care about it (?)
   };
   return { ins, rest };