How to get all permutations in CBMC?

Question

I am trying to get all permutations of an array in CBMC. For small cases, e.g., [1,2,3], I suppose I can write

i1 = nondet()
i2 = nondet()
i3 = nondet()
assume (i > 0 && i < 4); ...
assume (i1 != i2 && i2 != i3 && i1 != i3);
// do stuffs with i1,i2,i3

But with larger elements, the code will be very messy. So my question is that is there a better/general way to express this?

What about using an array? (e.g.) `#define COUNT 1000 int array[COUNT]; for (int i = 0; i < COUNT; ++i) array[i] = nondet();` — Craig Estey, Apr 15 '20 at 14:36
@CraigEstey the problem with this is it won't be a permutation - the same value could appear multiple times in the array. I am working on an answer whereby you set a nondet value in the array to i, but for some reason it isn't working as I expected. — T. Kiley, May 07 '20 at 08:41
Steinhaus–Johnson–Trotter algorithm can be used to cycle over all permutations. You can check if it is applicable to your problem. Maybe with some tricks as explained in https://stackoverflow.com/questions/46919309/steinhaus-johnson-trotter-algorithm-with-an-arbitrary-initial-state — meolic, May 22 '20 at 18:50
Thank you all for comments and suggestions. In the end, I approached the requirement a bit differently, and coded up an alternative which is presumably slow (due to the use of additional arrays and defensive code - loops) but it does what I think it does. — user2579326, May 24 '20 at 06:33

T. Kiley · Accepted Answer · 2020-05-07T12:08:17.503

Building on Craig's suggestion of using an array, you could loop over the values you want to permute, and nodeterministically select a location that has not been taken. For example, a loop like this (where sequence is pre-initalized with -1 for all values).

for(int i = 1; i <= count; ++i) {
  int nondet;
  assume(nondet >= 0 && nondet < count);
  // ensure we don't pick a spot already picked
  assume(sequence[nondet] == -1); 
  sequence[nondet] = i;
}

So a full program would look something like this:

#include <assert.h>
#include <memory.h>

int sum(int *array, int count) {
    int total = 0;
    for(int i = 0; i < count; ++i) {
        total += array[i];
    }
    return total;
}

int main(){

    int count = 5; // 1, ..., 6
    int *sequence = malloc(sizeof(int) * count);

    // this isn't working - not sure why, but constant propagator should
    // unroll the loop anyway
    // memset(sequence, -1, count);
    for(int i = 0; i < count; ++i) {
        sequence[i] = -1;
    }

    assert(sum(sequence, count) == -1 * count);

    for(int i = 1; i <= count; ++i) {
      int nondet;
      __CPROVER_assume(nondet >= 0);
      __CPROVER_assume(nondet < count);
      __CPROVER_assume(sequence[nondet] == -1); // ensure we don't pick a spot already picked
      sequence[nondet] = i;
    }

    int total = (count * (count + 1)) / 2;
    // verify this is a permuation
    assert(sum(sequence, count) == total);
}

However, this is pretty slow for values >6 (though I haven't compared it against your approach - it doesn't get stuck unwinding, it gets stuck solving).

How to get all permutations in CBMC?

1 Answers1