How to say anything about an array of structs

[weaversa]

I'm really struggling to specify an array of arrays in saw

Consider the following example. How can I (for a given nNumElements and nLength) prove that clear zeroes out each pList?

#include <stdint.h>
#include <stdlib.h>
#include <stdio.h>

typedef struct mytype {
  uint32_t nLength;
  uint32_t *pList;
} mytype;

mytype *init(uint32_t nNumElements, uint32_t nLength) {
  mytype *ret = malloc(nNumElements * sizeof(mytype));
  uint32_t i;
  for(i = 0; i < nNumElements; i++) {
   ret[i].nLength = nLength;
    ret[i].pList = malloc(nLength * sizeof(uint32_t));
  }

  return ret;
}

void clear(mytype *x, uint32_t nNumElements) {
  uint32_t i, j;
  for(i = 0; i < nNumElements; i++) {
    for(j = 0; j < x[i].nLength; i++) {
      x[i].pList[j] = 0;
    }
  }
}

Using the generic function below, I am able to create a list of the structures, but I can't figure out how to transform this list to an array.

rec struct_list numElements init_function params =
  if (eval_bool {{ (`numElements : [32]) == 0 }}) then []
  else (concat [init_function params]
               (struct_list (eval_int {{ (`numElements : [32]) - 1 }}) init_function params));

I have tried running the result of this function through crucible_array, but get type mismatches between SetupValue and CrucibleSetup...so, I'm lost right now. Any help would be appreciated.

[weaversa]

Recursive saw-script functions are hard to write.

Here's what I have, which seems to work. It initializes numElements objects using init_function which takes the position of the current element being worked on as well as a set of constant parameters. Thank you to everyone who helped!

let error = do {
  crucible_precond {{ True }};
  crucible_postcond {{ True }};
  return {{ True }};
};

let noerror = do {
  return {{ True }};
};

let struct_list_empty = do {
  return {s=[], c={{ [] }}} : CrucibleSetup {s : [SetupValue], c : Term};
};

rec struct_list_rec (numElements : Int) (init_function : Int -> a -> CrucibleSetup {s : SetupValue, c : Term}) (params : a) = do {
  err <- if (eval_bool {{ (`numElements : [32]) == 0 }}) then error else noerror; //numElements must be greater than 0                                       
  element <- init_function (eval_int {{ (`numElements : [32]) - 1 }}) params;
  rest <- if (eval_bool {{ (`numElements : [32]) == 1 }}) then struct_list_empty
          else struct_list_rec (eval_int {{ (`numElements : [32]) - 1 }}) init_function params;

  let ret_s = (concat [element.s] rest.s);

  let element_c = element.c;
  let rest_c = rest.c;
  let ret_c = {{ [element_c] # rest_c : [numElements]_ }};

  return {s=ret_s, c=ret_c};
};