cmathcombinationsmodel-checkingcbmc

How to get all permutations in CBMC?


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?


Solution

  • 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).