[Heapster] Another improvement to widening offsets

[m-yac]

Building off #1467, this PR makes widening work for offsets which differ by a constant amount > 1 or by a common factor. For example:

uint64_t sum(const uint64_t *arr, size_t len) {
  uint64_t sum = 0;
  while (len--) {
    sum += arr[0];
    arr += 8;
  }
  return sum;
}

(Compared to the example in #1467, arr is now a pointer to a uint64_t and gets incremented by 8 instead of 1.)

Note that this PR also:

• Fixes the translation of SImpl_LLVMArrayFromBlock
• Adds a few FIXME comments in Permissions.hs (@eddywestbrook check these out)
• Adds a few FIXME comments in SAWCoreBitvectors.hs (see Extend the library of Coq rewrite rules for bitvector operations #1236)
• Adds an example of a for loop with an increment > 1 to arrays.c (no-errors proof is only partially complete)

[eddywestbrook]

I suggested two small changes, that are mostly about cleanup. Overall this looks good, though! Great job figuring out the semantics we want for widening!