Array terms are blasted apart and reassembled inefficiently

[brianhuffman]

Proof goals are often seen in saw-script with subterms that look like [x@0, x@1, x@2, x@3, x@4, x@5, x@6, x@7]. These arise when we use overrides that have inputs and outputs of array types. When this expansion happens repeatedly the terms get rather large and slow.

Here is an example that shows the problem in crucible-llvm:

#include <stdint.h>

void next (int len, uint32_t *x) {
    for (int i = len-1; i > 0; i--) {
        x[i] += x[i-1];
    }
}

void nextn (int n, int len, uint32_t *x) {
    for (int i = 0; i < n; i++) {
        next(len, x);
    }
}

bc <- llvm_load_module "arrayoverride.bc";

let len = 20;
let i32 = llvm_int 32;
let arr = llvm_array len i32;
let l = crucible_term {{ `len:[32] }};

let {{
  next : [len][32] -> [len][32]
  next x = x + (x >> 1)
}};

next_ov <- crucible_llvm_verify bc "next" [] false
  do {
    x <- crucible_fresh_var "x" arr;
    px <- crucible_alloc arr;
    crucible_points_to px (crucible_term x);
    crucible_execute_func [l, px];
    crucible_points_to px (crucible_term {{ next x }});
  }
  z3;

let nextn_ov num =
  crucible_llvm_verify bc "nextn" [next_ov] false
  do {
    x <- crucible_fresh_var "x" arr;
    px <- crucible_alloc arr;
    crucible_points_to px (crucible_term x);
    let n = {{ `num:[32] }};
    crucible_execute_func [crucible_term n, l, px];
    crucible_points_to px (crucible_term {{ iterate next x @ n }});
  }
  do {
    print_goal;
    unint_z3 ["next"];
    //assume_unsat;
  };

time (nextn_ov 10);
time (nextn_ov 20);
time (nextn_ov 40);

The problem also shows up various subgoals (e.g. mul) in the crucible-jvm version of the ecdsa proof, whereas the old-style jss proof doesn't have this problem. (See also #399.)

[brianhuffman]

Issue #863 seems related to this.