Shung-Hsi Yu shunghsiyu
shunghsiyu
/ tnum_scast_check.py
Last active
October 4, 2024 06:37
z3-based model checking of tnum_scast() implementation from @dkanaliev
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/python3 | |
| from uuid import uuid4 | |
| from z3 import And, BitVec, BitVecRef, BitVecVal, Implies, prove, ULT, Extract, SignExt, ZeroExt | |
| SIZE = 64 # Working with 64-bit integers | |
| class Tnum: | |
| """A model of tristate number use in Linux kernel's BPF verifier. | |
| https://github.com/torvalds/linux/blob/v5.18/kernel/bpf/tnum.c | |
| """ |
shunghsiyu
/ vmtest.Containerfile
Created
December 18, 2024 05:13
Example container description for building and running BPF selftests of stable 6.6 kernel
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| FROM debian:11-slim | |
| ARG pahole_branch=master | |
| ENV PAHOLE_BRANCH=$pahole_branch | |
| ARG pahole_origin=https://git.kernel.org/pub/scm/devel/pahole/pahole.git | |
| ENV PAHOLE_ORIGIN=$pahole_origin | |
| ARG llvm_version=17 | |
| ENV LLVM_VERSION=$llvm_version | |
| ENV CLANG=clang-$llvm_version | |
| ENV LLVM_STRIP=llvm-strip-$llvm_version |
OlderNewer