src/language/tests/datasheet-check.c

   1 /* PSPP - a program for statistical analysis.
   2    Copyright (C) 2007, 2009 Free Software Foundation, Inc.
   3
   4    This program is free software: you can redistribute it and/or modify
   5    it under the terms of the GNU General Public License as published by
   6    the Free Software Foundation, either version 3 of the License, or
   7    (at your option) any later version.
   8
   9    This program is distributed in the hope that it will be useful,
  10    but WITHOUT ANY WARRANTY; without even the implied warranty of
  11    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12    GNU General Public License for more details.
  13
  14    You should have received a copy of the GNU General Public License
  15    along with this program.  If not, see <http://www.gnu.org/licenses/>. */
  16
  17 #include <config.h>
  18
  19 #include <data/datasheet.h>
  20 #include "datasheet-check.h"
  21 #include "model-checker.h"
  22
  23 #include <stdlib.h>
  24 #include <string.h>
  25
  26 #include <data/casereader-provider.h>
  27 #include <data/casereader.h>
  28 #include <data/casewriter.h>
  29 #include <data/lazy-casereader.h>
  30 #include <data/sparse-cases.h>
  31 #include <libpspp/array.h>
  32 #include <libpspp/assertion.h>
  33 #include <libpspp/range-map.h>
  34 #include <libpspp/range-set.h>
  35 #include <libpspp/taint.h>
  36 #include <libpspp/tower.h>
  37
  38 #include "minmax.h"
  39 #include "md4.h"
  40 #include "xalloc.h"
  41
  42
  43 /* lazy_casereader callback function to instantiate a casereader
  44    from the datasheet. */
  45 static struct casereader *
  46 lazy_callback (void *ds_)
  47 {
  48   struct datasheet *ds = ds_;
  49   return datasheet_make_reader (ds);
  50 }
  51
  52
  53 /* Maximum size of datasheet supported for model checking
  54    purposes. */
  55 #define MAX_ROWS 5
  56 #define MAX_COLS 5
  57
  58
  59 /* Checks that READER contains the ROW_CNT rows and COLUMN_CNT
  60    columns of data in ARRAY, reporting any errors via MC. */
  61 static void
  62 check_datasheet_casereader (struct mc *mc, struct casereader *reader,
  63                             double array[MAX_ROWS][MAX_COLS],
  64                             size_t row_cnt, size_t column_cnt)
  65 {
  66   if (casereader_get_case_cnt (reader) != row_cnt)
  67     {
  68       if (casereader_get_case_cnt (reader) == CASENUMBER_MAX
  69           && casereader_count_cases (reader) == row_cnt)
  70         mc_error (mc, "datasheet casereader has unknown case count");
  71       else
  72         mc_error (mc, "casereader row count (%lu) does not match "
  73                   "expected (%zu)",
  74                   (unsigned long int) casereader_get_case_cnt (reader),
  75                   row_cnt);
  76     }
  77   else if (casereader_get_value_cnt (reader) != column_cnt)
  78     mc_error (mc, "casereader column count (%zu) does not match "
  79               "expected (%zu)",
  80               casereader_get_value_cnt (reader), column_cnt);
  81   else
  82     {
  83       struct ccase *c;
  84       size_t row;
  85
  86       for (row = 0; row < row_cnt; row++)
  87         {
  88           size_t col;
  89
  90           c = casereader_read (reader);
  91           if (c == NULL)
  92             {
  93               mc_error (mc, "casereader_read failed reading row %zu of %zu "
  94                         "(%zu columns)", row, row_cnt, column_cnt);
  95               return;
  96             }
  97
  98           for (col = 0; col < column_cnt; col++)
  99             if (case_num_idx (c, col) != array[row][col])
 100               mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: "
 101                         "%g != %g",
 102                         row, col, row_cnt, column_cnt,
 103                         case_num_idx (c, col), array[row][col]);
 104
 105           case_unref (c);
 106         }
 107
 108       c = casereader_read (reader);
 109       if (c != NULL)
 110         mc_error (mc, "casereader has extra cases (expected %zu)", row_cnt);
 111     }
 112 }
 113
 114 /* Checks that datasheet DS contains has ROW_CNT rows, COLUMN_CNT
 115    columns, and the same contents as ARRAY, reporting any
 116    mismatches via mc_error.  Then, adds DS to MC as a new state. */
 117 static void
 118 check_datasheet (struct mc *mc, struct datasheet *ds,
 119                  double array[MAX_ROWS][MAX_COLS],
 120                  size_t row_cnt, size_t column_cnt)
 121 {
 122   struct datasheet *ds2;
 123   struct casereader *reader;
 124   unsigned long int serial = 0;
 125
 126   assert (row_cnt < MAX_ROWS);
 127   assert (column_cnt < MAX_COLS);
 128
 129   /* If it is a duplicate hash, discard the state before checking
 130      its consistency, to save time. */
 131   if (mc_discard_dup_state (mc, hash_datasheet (ds)))
 132     {
 133       datasheet_destroy (ds);
 134       return;
 135     }
 136
 137   /* Check contents of datasheet via datasheet functions. */
 138   if (row_cnt != datasheet_get_row_cnt (ds))
 139     mc_error (mc, "row count (%lu) does not match expected (%zu)",
 140               (unsigned long int) datasheet_get_row_cnt (ds), row_cnt);
 141   else if (column_cnt != datasheet_get_column_cnt (ds))
 142     mc_error (mc, "column count (%zu) does not match expected (%zu)",
 143               datasheet_get_column_cnt (ds), column_cnt);
 144   else
 145     {
 146       size_t row, col;
 147
 148       for (row = 0; row < row_cnt; row++)
 149         for (col = 0; col < column_cnt; col++)
 150           {
 151             union value v;
 152             if (!datasheet_get_value (ds, row, col, &v, 1))
 153               NOT_REACHED ();
 154             if (v.f != array[row][col])
 155               mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: %g != %g",
 156                         row, col, row_cnt, column_cnt, v.f, array[row][col]);
 157           }
 158     }
 159
 160   /* Check that datasheet contents are correct when read through
 161      casereader. */
 162   ds2 = clone_datasheet (ds);
 163   reader = datasheet_make_reader (ds2);
 164   check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
 165   casereader_destroy (reader);
 166
 167   /* Check that datasheet contents are correct when read through
 168      casereader with lazy_casereader wrapped around it.  This is
 169      valuable because otherwise there is no non-GUI code that
 170      uses the lazy_casereader. */
 171   ds2 = clone_datasheet (ds);
 172   reader = lazy_casereader_create (column_cnt, row_cnt,
 173                                    lazy_callback, ds2, &serial);
 174   check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
 175   if (lazy_casereader_destroy (reader, serial))
 176     {
 177       /* Lazy casereader was never instantiated.  This will
 178          only happen if there are no rows (because in that case
 179          casereader_read never gets called). */
 180       datasheet_destroy (ds2);
 181       if (row_cnt != 0)
 182         mc_error (mc, "lazy casereader not instantiated, but should "
 183                   "have been (size %zu,%zu)", row_cnt, column_cnt);
 184     }
 185   else
 186     {
 187       /* Lazy casereader was instantiated.  This is the common
 188          case, in which some casereader operation
 189          (casereader_read in this case) was performed on the
 190          lazy casereader. */
 191       casereader_destroy (reader);
 192       if (row_cnt == 0)
 193         mc_error (mc, "lazy casereader instantiated, but should not "
 194                   "have been (size %zu,%zu)", row_cnt, column_cnt);
 195     }
 196
 197   mc_add_state (mc, ds);
 198 }
 199
 200 /* Extracts the contents of DS into DATA. */
 201 static void
 202 extract_data (const struct datasheet *ds, double data[MAX_ROWS][MAX_COLS])
 203 {
 204   size_t column_cnt = datasheet_get_column_cnt (ds);
 205   size_t row_cnt = datasheet_get_row_cnt (ds);
 206   size_t row, col;
 207
 208   assert (row_cnt < MAX_ROWS);
 209   assert (column_cnt < MAX_COLS);
 210   for (row = 0; row < row_cnt; row++)
 211     for (col = 0; col < column_cnt; col++)
 212       {
 213         union value v;
 214         if (!datasheet_get_value (ds, row, col, &v, 1))
 215           NOT_REACHED ();
 216         data[row][col] = v.f;
 217       }
 218 }
 219
 220 /* Clones the structure and contents of ODS into *DS,
 221    and the contents of ODATA into DATA. */
 222 static void
 223 clone_model (const struct datasheet *ods, double odata[MAX_ROWS][MAX_COLS],
 224              struct datasheet **ds, double data[MAX_ROWS][MAX_COLS])
 225 {
 226   *ds = clone_datasheet (ods);
 227   memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
 228 }
 229
 230 /* "init" function for struct mc_class. */
 231 static void
 232 datasheet_mc_init (struct mc *mc)
 233 {
 234   struct datasheet_test_params *params = mc_get_aux (mc);
 235   struct datasheet *ds;
 236
 237   if (params->backing_rows == 0 && params->backing_cols == 0)
 238     {
 239       /* Create unbacked datasheet. */
 240       ds = datasheet_create (NULL);
 241       mc_name_operation (mc, "empty datasheet");
 242       check_datasheet (mc, ds, NULL, 0, 0);
 243     }
 244   else
 245     {
 246       /* Create datasheet with backing. */
 247       struct casewriter *writer;
 248       struct casereader *reader;
 249       double data[MAX_ROWS][MAX_COLS];
 250       int row;
 251
 252       assert (params->backing_rows > 0 && params->backing_rows <= MAX_ROWS);
 253       assert (params->backing_cols > 0 && params->backing_cols <= MAX_COLS);
 254
 255       writer = mem_writer_create (params->backing_cols);
 256       for (row = 0; row < params->backing_rows; row++)
 257         {
 258           struct ccase *c;
 259           int col;
 260
 261           c = case_create (params->backing_cols);
 262           for (col = 0; col < params->backing_cols; col++)
 263             {
 264               double value = params->next_value++;
 265               data[row][col] = value;
 266               case_data_rw_idx (c, col)->f = value;
 267             }
 268           casewriter_write (writer, c);
 269         }
 270       reader = casewriter_make_reader (writer);
 271       assert (reader != NULL);
 272
 273       ds = datasheet_create (reader);
 274       mc_name_operation (mc, "datasheet with (%d,%d) backing",
 275                          params->backing_rows, params->backing_cols);
 276       check_datasheet (mc, ds, data,
 277                        params->backing_rows, params->backing_cols);
 278     }
 279 }
 280
 281 /* "mutate" function for struct mc_class. */
 282 static void
 283 datasheet_mc_mutate (struct mc *mc, const void *ods_)
 284 {
 285   struct datasheet_test_params *params = mc_get_aux (mc);
 286
 287   const struct datasheet *ods = ods_;
 288   double odata[MAX_ROWS][MAX_COLS];
 289   double data[MAX_ROWS][MAX_COLS];
 290   size_t column_cnt = datasheet_get_column_cnt (ods);
 291   size_t row_cnt = datasheet_get_row_cnt (ods);
 292   size_t pos, new_pos, cnt;
 293
 294   extract_data (ods, odata);
 295
 296   /* Insert all possible numbers of columns in all possible
 297      positions. */
 298   for (pos = 0; pos <= column_cnt; pos++)
 299     for (cnt = 0; cnt <= params->max_cols - column_cnt; cnt++)
 300       if (mc_include_state (mc))
 301         {
 302           struct datasheet *ds;
 303           union value new[MAX_COLS];
 304           size_t i, j;
 305
 306           mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
 307           clone_model (ods, odata, &ds, data);
 308
 309           for (i = 0; i < cnt; i++)
 310             new[i].f = params->next_value++;
 311
 312           if (!datasheet_insert_columns (ds, new, cnt, pos))
 313             mc_error (mc, "datasheet_insert_columns failed");
 314
 315           for (i = 0; i < row_cnt; i++)
 316             {
 317               insert_range (&data[i][0], column_cnt, sizeof data[i][0],
 318                             pos, cnt);
 319               for (j = 0; j < cnt; j++)
 320                 data[i][pos + j] = new[j].f;
 321             }
 322
 323           check_datasheet (mc, ds, data, row_cnt, column_cnt + cnt);
 324         }
 325
 326   /* Delete all possible numbers of columns from all possible
 327      positions. */
 328   for (pos = 0; pos < column_cnt; pos++)
 329     for (cnt = 0; cnt < column_cnt - pos; cnt++)
 330       if (mc_include_state (mc))
 331         {
 332           struct datasheet *ds;
 333           size_t i;
 334
 335           mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
 336           clone_model (ods, odata, &ds, data);
 337
 338           datasheet_delete_columns (ds, pos, cnt);
 339
 340           for (i = 0; i < row_cnt; i++)
 341             remove_range (&data[i], column_cnt, sizeof *data[i], pos, cnt);
 342
 343           check_datasheet (mc, ds, data, row_cnt, column_cnt - cnt);
 344         }
 345
 346   /* Move all possible numbers of columns from all possible
 347      existing positions to all possible new positions. */
 348   for (pos = 0; pos < column_cnt; pos++)
 349     for (cnt = 0; cnt < column_cnt - pos; cnt++)
 350       for (new_pos = 0; new_pos < column_cnt - cnt; new_pos++)
 351         if (mc_include_state (mc))
 352           {
 353             struct datasheet *ds;
 354             size_t i;
 355
 356             clone_model (ods, odata, &ds, data);
 357             mc_name_operation (mc, "move %zu columns from %zu to %zu",
 358                                cnt, pos, new_pos);
 359
 360             datasheet_move_columns (ds, pos, new_pos, cnt);
 361
 362             for (i = 0; i < row_cnt; i++)
 363               move_range (&data[i], column_cnt, sizeof data[i][0],
 364                           pos, new_pos, cnt);
 365
 366             check_datasheet (mc, ds, data, row_cnt, column_cnt);
 367           }
 368
 369   /* Insert all possible numbers of rows in all possible
 370      positions. */
 371   for (pos = 0; pos <= row_cnt; pos++)
 372     for (cnt = 0; cnt <= params->max_rows - row_cnt; cnt++)
 373       if (mc_include_state (mc))
 374         {
 375           struct datasheet *ds;
 376           struct ccase *c[MAX_ROWS];
 377           size_t i, j;
 378
 379           clone_model (ods, odata, &ds, data);
 380           mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
 381
 382           for (i = 0; i < cnt; i++)
 383             {
 384               c[i] = case_create (column_cnt);
 385               for (j = 0; j < column_cnt; j++)
 386                 case_data_rw_idx (c[i], j)->f = params->next_value++;
 387             }
 388
 389           insert_range (data, row_cnt, sizeof data[pos], pos, cnt);
 390           for (i = 0; i < cnt; i++)
 391             for (j = 0; j < column_cnt; j++)
 392               data[i + pos][j] = case_num_idx (c[i], j);
 393
 394           if (!datasheet_insert_rows (ds, pos, c, cnt))
 395             mc_error (mc, "datasheet_insert_rows failed");
 396
 397           check_datasheet (mc, ds, data, row_cnt + cnt, column_cnt);
 398         }
 399
 400   /* Delete all possible numbers of rows from all possible
 401      positions. */
 402   for (pos = 0; pos < row_cnt; pos++)
 403     for (cnt = 0; cnt < row_cnt - pos; cnt++)
 404       if (mc_include_state (mc))
 405         {
 406           struct datasheet *ds;
 407
 408           clone_model (ods, odata, &ds, data);
 409           mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
 410
 411           datasheet_delete_rows (ds, pos, cnt);
 412
 413           remove_range (&data[0], row_cnt, sizeof data[0], pos, cnt);
 414
 415           check_datasheet (mc, ds, data, row_cnt - cnt, column_cnt);
 416         }
 417
 418   /* Move all possible numbers of rows from all possible existing
 419      positions to all possible new positions. */
 420   for (pos = 0; pos < row_cnt; pos++)
 421     for (cnt = 0; cnt < row_cnt - pos; cnt++)
 422       for (new_pos = 0; new_pos < row_cnt - cnt; new_pos++)
 423         if (mc_include_state (mc))
 424           {
 425             struct datasheet *ds;
 426
 427             clone_model (ods, odata, &ds, data);
 428             mc_name_operation (mc, "move %zu rows from %zu to %zu",
 429                                cnt, pos, new_pos);
 430
 431             datasheet_move_rows (ds, pos, new_pos, cnt);
 432
 433             move_range (&data[0], row_cnt, sizeof data[0],
 434                         pos, new_pos, cnt);
 435
 436             check_datasheet (mc, ds, data, row_cnt, column_cnt);
 437           }
 438 }
 439
 440 /* "destroy" function for struct mc_class. */
 441 static void
 442 datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
 443 {
 444   struct datasheet *ds = ds_;
 445   datasheet_destroy (ds);
 446 }
 447
 448 /* Executes the model checker on the datasheet test driver with
 449    the given OPTIONS and passing in the given PARAMS, which must
 450    point to a modifiable "struct datasheet_test_params".  If any
 451    value in PARAMS is out of range, it will be adjusted into the
 452    valid range before running the test.
 453
 454    Returns the results of the model checking run. */
 455 struct mc_results *
 456 datasheet_test (struct mc_options *options, void *params_)
 457 {
 458   struct datasheet_test_params *params = params_;
 459   static const struct mc_class datasheet_mc_class =
 460     {
 461       datasheet_mc_init,
 462       datasheet_mc_mutate,
 463       datasheet_mc_destroy,
 464     };
 465
 466   params->next_value = 1;
 467   params->max_rows = MIN (params->max_rows, MAX_ROWS);
 468   params->max_cols = MIN (params->max_cols, MAX_COLS);
 469   params->backing_rows = MIN (params->backing_rows, params->max_rows);
 470   params->backing_cols = MIN (params->backing_cols, params->max_cols);
 471
 472   mc_options_set_aux (options, params);
 473   return mc_run (&datasheet_mc_class, options);
 474 }