| """Shared property bank. One JSON file per item: |
| { |
| "item_id": "...", "crate_dir": "path with Cargo.toml (lib name `target_crate`)", "lib_name": "tiny", |
| "properties": [ |
| {"id": "p1", "fn": "avg_buggy", "args": [["a","u32"],["b","u32"]], |
| "pre": "true", "post": "r == ((a as u64 + b as u64) / 2) as u32", "ret": "u32"} |
| ] |
| } |
| `pre` and `post` are Rust boolean expressions over the arg names and `r` (the return value). Every property also |
| carries the implicit check "the call does not panic / overflow", which each tool detects natively. |
| """ |
| import json |
|
|
| SCALARS = {"u8", "u16", "u32", "u64", "usize", "i8", "i16", "i32", "i64", "isize", "bool"} |
| |
| |
| RUST_TYPE = {"bytes": "Vec<u8>", "u32s": "Vec<u32>", "usizes": "Vec<usize>", "opt_usize": "Option<usize>"} |
| BY_REF = {"bytes", "u32s", "usizes"} |
| SUPPORTED = SCALARS | set(RUST_TYPE) |
|
|
|
|
| def rust_type(t): return RUST_TYPE.get(t, t) |
|
|
|
|
| def call_arg(n, t): return ("&" + n) if t in BY_REF else n |
|
|
|
|
| def revision(bank, rev): |
| """Return a copy of the bank pointed at the `pre` or `post` revision of a kernel (crate_dir .../pre -> .../post, lib k_x_pre -> k_x_post).""" |
| b = dict(bank) |
| if rev == "post": |
| b["crate_dir"] = bank["crate_dir"].rstrip("/").rsplit("/pre", 1)[0] + "/post" |
| b["lib_name"] = bank["lib_name"].rsplit("_pre", 1)[0] + "_post" |
| return b |
|
|
|
|
| def load(path): |
| b = json.load(open(path)) |
| for k in ("item_id", "crate_dir", "lib_name", "properties"): |
| if k not in b: raise ValueError(f"bank missing {k}") |
| ids = set() |
| for p in b["properties"]: |
| for k in ("id", "fn", "args", "pre", "post", "ret"): |
| if k not in p: raise ValueError(f"property missing {k}: {p}") |
| if p["id"] in ids: raise ValueError("duplicate property id " + p["id"]) |
| ids.add(p["id"]) |
| for _, t in p["args"]: |
| if t not in SUPPORTED: raise ValueError(f"unsupported arg type {t} ") |
| return b |
|
|
