name = "arrayvec"
description = """
ETNA workload for the Rust `arrayvec` crate. Each variant re-introduces
one historical bug-fix into a fresh patched branch and pairs it with a
framework-neutral property, four PBT adapters, and a deterministic
witness test.
"""
language = "rust"
strategies = ["proptest", "quickcheck", "crabcheck", "hegel"]
crate = "arrayvec"
base_commit = "2d005c25f655241206c340c5f2c74873051bcd5e"

[[tasks]]
mutations = ["extend_silent_truncate_a554ea2_1"]

[tasks.source]
repo = "https://github.com/bluss/arrayvec"
commits = ["a554ea219a181f74542c5aaaeccec97a52f51939"]
commit_subjects = ["API: Panic in .extend() and from_iter on capacity exceeded"]
summary = "`.extend()` and `from_iter` silently truncated the iterator once the `ArrayVec` hit capacity, contradicting the documented behaviour of panicking on overflow. The fix routes both paths through `extend_panic()` when the backing buffer is full."

[tasks.injection]
kind = "patch"
patch = "patches/extend_silent_truncate_a554ea2_1.patch"
files = ["src/arrayvec.rs"]
locations = [{ file = "src/arrayvec.rs", line = 1143, symbol = "extend_from_iter" }]

[tasks.bug]
short_name = "extend_silent_truncate"
invariant = """
`ArrayVec::extend` must panic when the iterator yields more items than the vector's remaining capacity; truncating silently is a data-loss bug visible to callers that rely on the documented "panic on overflow" behaviour.
"""
how_triggered = "replacing `if ptr == end_ptr && CHECK { extend_panic(); }` with `if ptr == end_ptr && CHECK { return; }` makes the extend loop bail out silently once the backing buffer is full. Witness `case_five_items_cap_four` drives this by extending a capacity-4 `ArrayVec` with a 5-element iterator: base build panics as expected; the buggy build truncates to 4 elements and returns normally, and the property reports `vec.len()=4` without a panic observation. The `case_exact_fit` witness guards against over-correction — 4 items must still succeed."

[[tasks.tasks]]
property = "ExtendPanicsOnOverflow"
witnesses = [
  { test_fn = "witness_extend_panics_on_overflow_case_five_items_cap_four" },
  { test_fn = "witness_extend_panics_on_overflow_case_exact_fit" },
]

[[tasks]]
mutations = ["insert_bound_off_by_one_2a1378d_1"]

[tasks.source]
repo = "https://github.com/bluss/arrayvec"
commits = ["2a1378d3eb073026468063fd354d90511b61def0"]
commit_subjects = ["Fix bounds checking in ArrayVec::insert(index, element)"]
summary = "`try_insert` rejected `index == len` (the valid append position) with an out-of-range panic instead of pushing to the tail, diverging from `Vec::insert`'s contract. The fix loosens the guard from `index >= len` to `index > len` while adding a separate capacity check."

[tasks.injection]
kind = "patch"
patch = "patches/insert_bound_off_by_one_2a1378d_1.patch"
files = ["src/arrayvec.rs"]
locations = [{ file = "src/arrayvec.rs", line = 310, symbol = "try_insert" }]

[tasks.bug]
short_name = "insert_bound_off_by_one"
invariant = "`ArrayVec::try_insert(len, v)` must behave as a push-to-tail — index `== len` is a valid append position per the docs, matching `Vec::insert`'s contract. The buggy boundary check rejects this call with a panic as if the index were out of range."
how_triggered = "the base code tests `if index > self.len() { panic_oob!(...) }`; the mutation restores the pre-2a1378d condition `if index >= self.len() { panic_oob!(...) }`, which treats the append position as out-of-bounds. `witness_case_empty` (insert at 0 into an empty vec) and `witness_case_three_elements` (insert at 3 into a 3-element vec) both hit the boundary and panic under the buggy code where the base succeeds."

[[tasks.tasks]]
property = "InsertAtLengthSucceeds"
witnesses = [
  { test_fn = "witness_insert_at_length_succeeds_case_empty" },
  { test_fn = "witness_insert_at_length_succeeds_case_three_elements" },
]

[[dropped]]
commit = "27401fbc"
subject = "Fix miri error in extend_zst"
reason = "detection requires miri"

[[dropped]]
commit = "c094906a"
subject = "Fix mutable reborrow in retain"
reason = "detection requires miri"

[[dropped]]
commit = "c9ff5794"
subject = "Fix stacked borrows violations"
reason = "detection requires miri"

[[dropped]]
commit = "9beb7534"
subject = "fix aliasing in drain_range"
reason = "detection requires miri"

[[dropped]]
commit = "f40e708f"
subject = "truncate: no raw pointer from self"
reason = "detection requires miri"

[[dropped]]
commit = "2a339799"
subject = ".extend() for ZST"
reason = "detection requires miri (ZST len)"

[[dropped]]
commit = "9f578790"
subject = "UB in DerefMut of ArrayString"
reason = "detection requires miri"

[[dropped]]
commit = "dc33f756"
subject = "track_caller"
reason = "observability-only, no behavior change"

[[dropped]]
commit = "812c83a2"
subject = "16-bit lengths on 16-bit targets"
reason = "not reachable on 64-bit host"

[[dropped]]
commit = "0fdf39f1"
subject = "debug-assert into_inner_unchecked"
reason = "unsafe API; no public invariant change"

[[dropped]]
commit = "b7f3aa9f"
subject = "new_const"
reason = "API addition, not a bug"

[[dropped]]
commit = "b82a6d49"
subject = "retain optimization const-generic switch"
reason = "no behavior change"

[[dropped]]
commit = "090a5c50"
subject = "encode_utf8 uninit pointer"
reason = "surface removed, const-generic rewrite"
