llvm-to-smt: Kernel regression for BPF_ADD/SUB: `[handleCallInst]call instruction not supported`

[pchaigno]

Command to reproduce:

python3 generate_encodings.py --kernver 6.10 --commit 28a4411076b254c67842348e3b25c2fb41a94cad --kernbasedir ~/linux --outdir ../bpf-encodings/torvalds_linux --specific-op BPF_ADD --modular

Ends with:

-------------------
  %i16.i8.i = call { i32, i1 } @llvm.sadd.with.overflow.i32(i32 %i.i6.i, i32 %src_reg1.sroa.50.0.copyload) #2
-------------------
terminate called after throwing an instance of 'std::runtime_error'
  what():  [handleCallInst]call instruction not supported

Caught it with the new CI job (https://github.com/bpfverif/agni/actions/runs/10358960586) and bisected it to commit 28a4411076b2 upstream. I haven't checked it yet.

[harishankarv]

This seems to be because of check_add_overflow in scalar32_min_max_add and scalar_min_max_add. check_add_overflow is defined using a compiler builtin (__builtin_add_overflow) that causes clang to emit an llvm intrinsic @llvm.sadd.with.overflow.i32 when compiling verifier.c

llvm-to-smt doesn't know the semantics of this intrinsic (or any other intrinsic for that matter). It will fail on any calls to call @llvm.any.llvm.intrinsic() with the usual [handleCallInst]call instruction not supported.

This was also the case for fls() and fls64() functions in the kernel, the default definition for which also used compiler builtins; clang emitted a call i64 @llvm.ctlz.i64 intrinsic for that. We provided our own definition using the ones found in asm-generic/bitops.

We need to provide our own semantics (in C) for the sadd.with.overflow intrinsic. The easy method is to do this in C, similar to fls and fls64. However, I am unable to find a C definition for this intrinsic in the kernel source code. Please let me know if you are able to help with this @pchaigno @mshachnai

[pchaigno]

You can go back to v4.18, when check_add_overflow was introduced, to find the alternative definition: https://elixir.bootlin.com/linux/v4.18.20/source/include/linux/overflow.h#L187.

It relies on __builtin_choose_expr, which I'm guessing will have the same issue, but that's probably easier to replace.

[pchaigno]

Alternatively, could we detect the sadd.with.overflow intrinsic and replace it with a call to Z3's bvadd_no_overflow? IIUC, that would mean we trust the sadd.with.overflow intrinsic to be correct, but it's probably not worse than replacing it with something that doesn't correspond to the actual implementation.

[harishankarv]

Alternatively, could we detect the sadd.with.overflow intrinsic

I was thinking about this ... if it might be a better idea to handle/detect a certain set of intrinsics as "first-class" in llvm-to-smt, and encoding them in bitvector theory directly.

that would mean we trust the sadd.with.overflow intrinsic to be correct

Yes, but our whole llvm-to-smt process depends on the correctness of clang's C-to-llvm translation anyway and clang is indeed part of our trusted computing base. So like you say, this is indeed better that replacing it with something that doesn't correspond to the actual implementation.