Elazar Gershuni
Elazar Gershuni
This PR serves as a demonsration, and is unlikely to be merged, since it's far too large and not really automatable. ## Summary by CodeRabbit - **New Features** - Added...
Move numerical operations that deal with signedness and overflow from ebpf_domain_t to FiniteDomain, with its own cpp and hpp. Also: always allow `rx -= rx`.
This seems to happen on numbers that are close to the bound of the extension. The test `ebpf-samples/cilium/bpf_netdev.o from-netdev` should be marked as failing: ``` $ ./check --no-simplify ebpf-samples/cilium/bpf_netdev.o from-netdev...
Maybe we need a bulk-rename operation within the numerical domain: "rename this set of variables to this set of variables". The domain should handle correlations and default values. _Originally posted...
The variable `is64` is written to but not read afterwards. This is likely a bug. https://github.com/vbpf/prevail/blob/2a44d21f04737ecc5ee036fd7408cc15b1788202/src/crab/finite_domain.cpp#L127 https://github.com/vbpf/prevail/blob/2a44d21f04737ecc5ee036fd7408cc15b1788202/src/crab/finite_domain.cpp#L173
The variable `'lb` is written to but not read. This is likely a bug. https://github.com/vbpf/prevail/blob/2a44d21f04737ecc5ee036fd7408cc15b1788202/src/crab/finite_domain.cpp#L95
EbpfDomain tracks stack_numeric_size for each stack variable, but its semantic is a "must" analysis: everything inside the interval must be numerical. But the join operation treats it as "may" analysis:...
## Summary - add helpers in the transformer test fixture to construct program info for alternate platforms and to scope map descriptor mutations - extend the transformer Catch2 suite with...
## Summary - add a friend accessor so the tests can inspect EbpfDomain internals - create a dedicated Catch2 suite that covers lattice operations, helper lookups, and environment setup for...