Fix wrapped pointer arithmetic and comparisons

[shaobo-he]

Fixes #804.

This also covers the GEP false alarm originally reported in #682.

Problem

Wrapped integers are represented as unbounded Boogie integers and normalized when their machine-width value is observed. Pointer operations did not consistently follow that rule:

• $add.ref, $sub.ref, and $mul.ref returned unbounded arithmetic results, so a constrained 64-bit index could address a different memory cell through a noncanonical representative.
• Pointer ordering used raw integer comparisons, making signed and unsigned pointer predicates equivalent.
• Equal-width integer-to-pointer conversion left noncanonical integer representatives unchanged.

Approach

• Canonicalize non-bitvector pointer arithmetic results to the signed pointer-width range with $tos.
• Canonicalize integer-to-pointer conversions the same way, giving pointer-producing operations one representative per machine pointer value.
• Keep equality and signed ordering linear over canonical pointers.
• Route unsigned pointer ordering through the existing signedness-aware integer predicates, which reinterpret canonical pointers with $tou.
• Leave bitvector-pointer arithmetic and predicates unchanged because bitvectors already wrap.

Keeping signed predicates linear is intentional. SMACK's allocation models use them to bound pointer values. Wrapping every pointer predicate, as attempted in the old fixed-pa-wrapped branch, admits noncanonical allocator values and made Corral's no-reuse contracts time out.

For integral pointers with the module's default pointer width, the conversion formulas follow LLVM's required truncation and zero-extension rules. Choosing $tos as the representative preserves values modulo 2^N; pointer-to-integer-to-pointer round trips preserve canonical pointer values. Alternate-width and non-integral address spaces remain outside SMACK's existing single-pointer-width model and are not addressed here.

This change is confined to pointer translation. It does not modify SeaDsa region construction or SMACK's memory-splitting policy.

Tests

• Added the exact False alarm when the integer encoding is wrapped integer #682/Incorrect modeling of pointer arithmetic/comparison when --integer-encoding=wrapped-integer #804 C regression with an unsigned 64-bit GEP index.
• Added an LLVM regression covering pointer arithmetic wraparound from INT64_MAX to INT64_MIN, distinct signed/unsigned pointer ordering, and pointer/integer roundtrip equality.
• LLVM exhaustive matrix: 30/30 passed.
• c/basic exhaustive matrix: 510/510 passed.
• c/data exhaustive matrix: 498/498 passed.
• LLVM 14 debug build and clang-format check passed.

[shaobo-he]

Why this PR no longer changes memory regions

While auditing pointer-to-integer conversions, I found a separate, pre-existing memory-splitting soundness issue. It is not caused by wrapped-pointer arithmetic and $tos does not fix it.

The problematic shape is:

%p = malloc(...)
%i = ptrtoint ptr %p to i64
%q = inttoptr i64 %i to ptr
store 0, ptr %q
store 1, ptr %p
%v = load ptr %q
assert(%v == 0) ; must fail

With ptrtoint and inttoptr hidden behind no-inline functions, SeaDsa can assign %p and %q different nodes. SMACK then chooses different Boogie memory maps for the two accesses. The translated pointer values can be equal, but a store through %p does not update the map read through %q, so SMACK can incorrectly prove the stale-value assertion. On the concrete regression, default memory splitting produced the false proof; --no-memory-splitting correctly found the error.

The cast canonicalization in this PR only ensures that equal machine pointer values have the same numerical Boogie ref representation. Region/map selection happens statically from SeaDsa nodes before that expression is used, so numerical canonicalization cannot make two separately selected maps alias.

My initial attempted fix changed Region::overlaps so one cast-marked node forced overlap with every other region. That is a global memory-splitting policy change across all integer encodings, not an issue-804 translation fix. It also exposed that Region::isComplicated groups nodes with different intended behavior: cast/unknown nodes, incomplete nodes, and external nodes. Applying one universal rule collapsed unrelated maps and broke the existing extern_mem.c expectations.

A proper follow-up should distinguish at least:

• provenance-preserving pointer/integer round trips, whose source and destination should share an alias class;
• arbitrary integer-derived pointers, which may require a universal alias fallback;
• external and incomplete SeaDsa nodes, whose existing behavior and precision requirements differ.

That work needs dedicated regressions for false proofs, external pointers, map counts, and performance. PR 836 therefore stays confined to wrapped pointer value semantics, and Regions.cpp remains unchanged from develop.