"""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"}
# v1 adds owned-collection arg types, passed to the function by reference (`&a`): `bytes`=Vec<u8>, `u32s`=Vec<u32>, `usizes`=Vec<usize>,
# and `opt_usize`=Option<usize> (passed by value). Kani handles scalars only (vec/option properties are reported `unsupported` for Kani).
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