1 /* PSPP - a program for statistical analysis.
2 Copyright (C) 2007 Free Software Foundation, Inc.
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.
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.
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/>. */
19 #include <data/datasheet.h>
24 #include <data/casereader-provider.h>
25 #include <data/casereader.h>
26 #include <data/casewriter.h>
27 #include <data/lazy-casereader.h>
28 #include <data/sparse-cases.h>
29 #include <libpspp/array.h>
30 #include <libpspp/assertion.h>
31 #include <libpspp/model-checker.h>
32 #include <libpspp/range-map.h>
33 #include <libpspp/range-set.h>
34 #include <libpspp/taint.h>
35 #include <libpspp/tower.h>
41 static struct axis *axis_create (void);
42 static struct axis *axis_clone (const struct axis *);
43 static void axis_destroy (struct axis *);
45 static void axis_hash (const struct axis *, struct md4_ctx *);
47 static bool axis_allocate (struct axis *, unsigned long int request,
48 unsigned long int *start,
49 unsigned long int *width);
50 static void axis_make_available (struct axis *,
51 unsigned long int start,
52 unsigned long int width);
53 static unsigned long int axis_extend (struct axis *, unsigned long int width);
55 static unsigned long int axis_map (const struct axis *, unsigned long log_pos);
57 static unsigned long axis_get_size (const struct axis *);
58 static void axis_insert (struct axis *,
59 unsigned long int log_start,
60 unsigned long int phy_start,
61 unsigned long int cnt);
62 static void axis_remove (struct axis *,
63 unsigned long int start, unsigned long int cnt);
64 static void axis_move (struct axis *,
65 unsigned long int old_start,
66 unsigned long int new_start,
67 unsigned long int cnt);
69 static struct source *source_create_empty (size_t column_cnt);
70 static struct source *source_create_casereader (struct casereader *);
71 static struct source *source_clone (const struct source *);
72 static void source_destroy (struct source *);
74 static casenumber source_get_backing_row_cnt (const struct source *);
75 static size_t source_get_column_cnt (const struct source *);
77 static bool source_read (const struct source *,
78 casenumber row, size_t column,
79 union value[], size_t value_cnt);
80 static bool source_write (struct source *,
81 casenumber row, size_t column,
82 const union value[], size_t value_cnt);
83 static bool source_write_columns (struct source *, size_t start_column,
84 const union value[], size_t value_cnt);
85 static bool source_has_backing (const struct source *);
86 static void source_increase_use (struct source *, size_t delta);
87 static void source_decrease_use (struct source *, size_t delta);
88 static bool source_in_use (const struct source *);
90 /* A datasheet is internally composed from a set of data files,
91 called "sources". The sources that make up a datasheet must
92 have the same number of rows (cases), but their numbers of
93 columns (variables) may vary.
95 A datasheet's external view is produced by mapping (permuting
96 and selecting) its internal data. Thus, we can rearrange or
97 delete rows or columns simply by modifying the mapping. We
98 add rows by adding rows to each source and to the row mapping.
99 We add columns by adding a new source, then adding that source
100 to the column mapping.
102 Each source in a datasheet can be a casereader or a
103 sparse_cases. Casereaders are read-only, so when sources made
104 from casereaders need to be modified, it is done "virtually"
105 through being overlaid by a sparse_cases. */
110 /* Mappings from logical to physical columns/rows. */
111 struct axis *columns;
114 /* Mapping from physical columns to "source_info"s. */
115 struct range_map sources;
117 /* Minimum number of columns to put in a new source when we
118 need new columns and none are free. We double it whenever
119 we add a new source to keep the number of file descriptors
120 needed by the datasheet to a minimum, reducing the
121 likelihood of running out. */
122 unsigned column_min_alloc;
124 /* Indicates corrupted data in the datasheet. */
128 /* Maps from a range of physical columns to a source. */
131 struct range_map_node column_range;
132 struct source *source;
135 /* Is this operation a read or a write? */
142 static void free_source_info (struct datasheet *, struct source_info *);
143 static struct source_info *source_info_from_range_map (
144 struct range_map_node *);
145 static bool rw_case (struct datasheet *ds, enum rw_op op,
146 casenumber lrow, size_t start_column, size_t column_cnt,
149 /* Creates and returns a new datasheet.
151 If READER is nonnull, then the datasheet initially contains
152 the contents of READER. */
154 datasheet_create (struct casereader *reader)
156 /* Create datasheet. */
157 struct datasheet *ds = xmalloc (sizeof *ds);
158 ds->columns = axis_create ();
159 ds->rows = axis_create ();
160 range_map_init (&ds->sources);
161 ds->column_min_alloc = 1;
162 ds->taint = taint_create ();
169 struct source_info *si;
171 si = xmalloc (sizeof *si);
172 si->source = source_create_casereader (reader);
173 column_cnt = source_get_column_cnt (si->source);
174 row_cnt = source_get_backing_row_cnt (si->source);
175 source_increase_use (si->source, column_cnt);
177 if ( column_cnt > 0 )
179 unsigned long int column_start;
180 column_start = axis_extend (ds->columns, column_cnt);
181 axis_insert (ds->columns, 0, column_start, column_cnt);
182 range_map_insert (&ds->sources, column_start, column_cnt,
188 unsigned long int row_start;
189 row_start = axis_extend (ds->rows, row_cnt);
190 axis_insert (ds->rows, 0, row_start, row_cnt);
197 /* Destroys datasheet DS. */
199 datasheet_destroy (struct datasheet *ds)
204 axis_destroy (ds->columns);
205 axis_destroy (ds->rows);
206 while (!range_map_is_empty (&ds->sources))
208 struct range_map_node *r = range_map_first (&ds->sources);
209 struct source_info *si = source_info_from_range_map (r);
210 free_source_info (ds, si);
212 taint_destroy (ds->taint);
216 /* Moves datasheet DS to a new location in memory, and returns
217 the new location. Afterward, the datasheet must not be
218 accessed at its former location.
220 This function is useful for ensuring that all references to a
221 datasheet have been dropped, especially in conjunction with
222 tools like Valgrind. */
224 datasheet_rename (struct datasheet *ds)
226 struct datasheet *new = xmemdup (ds, sizeof *ds);
231 /* Returns true if datasheet DS is tainted.
232 A datasheet is tainted by an I/O error or by taint
233 propagation to the datasheet. */
235 datasheet_error (const struct datasheet *ds)
237 return taint_is_tainted (ds->taint);
240 /* Marks datasheet DS tainted. */
242 datasheet_force_error (struct datasheet *ds)
244 taint_set_taint (ds->taint);
247 /* Returns datasheet DS's taint object. */
249 datasheet_get_taint (const struct datasheet *ds)
254 /* Returns the number of rows in DS. */
256 datasheet_get_row_cnt (const struct datasheet *ds)
258 return axis_get_size (ds->rows);
261 /* Returns the number of columns in DS. */
263 datasheet_get_column_cnt (const struct datasheet *ds)
265 return axis_get_size (ds->columns);
268 /* Inserts CNT columns into datasheet DS just before column
269 BEFORE. Initializes the contents of each row in the inserted
270 columns to the CNT values in INIT_VALUES.
272 Returns true if successful, false on failure. In case of
273 failure, the datasheet is unchanged. */
275 datasheet_insert_columns (struct datasheet *ds,
276 const union value init_values[], size_t cnt,
282 unsigned long first_phy; /* First allocated physical column. */
283 unsigned long phy_cnt; /* Number of allocated physical columns. */
285 /* Allocate physical columns from the pool of available
287 if (!axis_allocate (ds->columns, cnt, &first_phy, &phy_cnt))
289 /* No columns were available. Create a new source and
290 extend the axis to make some new ones available. */
291 struct source_info *si;
293 phy_cnt = MAX (cnt, ds->column_min_alloc);
294 first_phy = axis_extend (ds->columns, phy_cnt);
295 ds->column_min_alloc = MIN (65536, ds->column_min_alloc * 2);
297 si = xmalloc (sizeof *si);
298 si->source = source_create_empty (phy_cnt);
299 range_map_insert (&ds->sources, first_phy, phy_cnt,
303 axis_make_available (ds->columns, first_phy + cnt,
309 /* Initialize the columns and insert them into the columns
313 struct range_map_node *r; /* Range map holding FIRST_PHY column. */
314 struct source_info *s; /* Source containing FIRST_PHY column. */
315 size_t source_avail; /* Number of phys columns available. */
316 size_t source_cnt; /* Number of phys columns to use. */
318 /* Figure out how many columns we can and want to take
319 starting at FIRST_PHY, and then insert them into the
321 r = range_map_lookup (&ds->sources, first_phy);
322 s = source_info_from_range_map (r);
323 source_avail = range_map_node_get_end (r) - first_phy;
324 source_cnt = MIN (phy_cnt, source_avail);
325 axis_insert (ds->columns, before, first_phy, source_cnt);
327 /* Initialize the data for those columns in the
329 if (!source_write_columns (s->source,
330 first_phy - range_map_node_get_start (r),
331 init_values, source_cnt))
333 datasheet_delete_columns (ds, before - added,
335 taint_set_taint (ds->taint);
338 source_increase_use (s->source, source_cnt);
341 phy_cnt -= source_cnt;
342 first_phy += source_cnt;
343 init_values += source_cnt;
345 before += source_cnt;
352 /* Deletes the CNT columns in DS starting from column START. */
354 datasheet_delete_columns (struct datasheet *ds, size_t start, size_t cnt)
358 assert ( start + cnt <= axis_get_size (ds->columns) );
360 /* Free up columns for reuse. */
361 for (lcol = start; lcol < start + cnt; lcol++)
363 size_t pcol = axis_map (ds->columns, lcol);
364 struct range_map_node *r = range_map_lookup (&ds->sources, pcol);
365 struct source_info *si = source_info_from_range_map (r);
367 source_decrease_use (si->source, 1);
368 if (source_has_backing (si->source))
370 if (!source_in_use (si->source))
371 free_source_info (ds, si);
374 axis_make_available (ds->columns, pcol, 1);
377 /* Remove columns from logical-to-physical mapping. */
378 axis_remove (ds->columns, start, cnt);
381 /* Moves the CNT columns in DS starting at position OLD_START so
382 that they then start at position NEW_START. Equivalent to
383 deleting the column rows, then inserting them at what becomes
384 position NEW_START after the deletion.*/
386 datasheet_move_columns (struct datasheet *ds,
387 size_t old_start, size_t new_start,
390 axis_move (ds->columns, old_start, new_start, cnt);
393 /* Retrieves the contents of the given ROW in datasheet DS into
394 newly created case C. Returns true if successful, false on
397 datasheet_get_row (const struct datasheet *ds, casenumber row, struct ccase *c)
399 size_t column_cnt = datasheet_get_column_cnt (ds);
400 case_create (c, column_cnt);
401 if (rw_case ((struct datasheet *) ds, OP_READ,
402 row, 0, column_cnt, case_data_all_rw (c)))
411 /* Stores the contents of case C, which is destroyed, into the
412 given ROW in DS. Returns true on success, false on I/O error.
413 On failure, the given ROW might be partially modified or
416 datasheet_put_row (struct datasheet *ds, casenumber row, struct ccase *c)
418 size_t column_cnt = datasheet_get_column_cnt (ds);
419 bool ok = rw_case (ds, OP_WRITE, row, 0, column_cnt,
420 (union value *) case_data_all (c));
425 /* Stores the values of the WIDTH columns in DS in the given ROW
426 starting at COLUMN in DS into VALUES. Returns true if
427 successful, false on I/O error. */
429 datasheet_get_value (const struct datasheet *ds, casenumber row, size_t column,
430 union value *value, int width)
433 return rw_case ((struct datasheet *) ds,
434 OP_READ, row, column, value_cnt_from_width (width), value);
437 /* Stores the WIDTH given VALUES into the given ROW in DS
438 starting at COLUMN. Returns true if successful, false on I/O
439 error. On failure, the given ROW might be partially modified
442 datasheet_put_value (struct datasheet *ds, casenumber row, size_t column,
443 const union value *value, int width)
445 return rw_case (ds, OP_WRITE, row, column, value_cnt_from_width (width),
446 (union value *) value);
449 /* Inserts the CNT cases at C, which are destroyed, into
450 datasheet DS just before row BEFORE. Returns true if
451 successful, false on I/O error. On failure, datasheet DS is
454 datasheet_insert_rows (struct datasheet *ds,
455 casenumber before, struct ccase c[],
458 casenumber added = 0;
461 unsigned long first_phy;
462 unsigned long phy_cnt;
465 /* Allocate physical rows from the pool of available
467 if (!axis_allocate (ds->rows, cnt, &first_phy, &phy_cnt))
469 /* No rows were available. Extend the row axis to make
470 some new ones available. */
472 first_phy = axis_extend (ds->rows, cnt);
475 /* Insert the new rows into the row mapping. */
476 axis_insert (ds->rows, before, first_phy, phy_cnt);
478 /* Initialize the new rows. */
479 for (i = 0; i < phy_cnt; i++)
480 if (!datasheet_put_row (ds, before + i, &c[i]))
483 case_destroy (&c[i]);
484 datasheet_delete_rows (ds, before - added, phy_cnt + added);
497 /* Deletes the CNT rows in DS starting from row FIRST. */
499 datasheet_delete_rows (struct datasheet *ds,
500 casenumber first, casenumber cnt)
504 /* Free up rows for reuse.
506 for (lrow = first; lrow < first + cnt; lrow++)
507 axis_make_available (ds->rows, axis_map (ds->rows, lrow), 1);
509 /* Remove rows from logical-to-physical mapping. */
510 axis_remove (ds->rows, first, cnt);
513 /* Moves the CNT rows in DS starting at position OLD_START so
514 that they then start at position NEW_START. Equivalent to
515 deleting the given rows, then inserting them at what becomes
516 position NEW_START after the deletion. */
518 datasheet_move_rows (struct datasheet *ds,
519 size_t old_start, size_t new_start,
522 axis_move (ds->rows, old_start, new_start, cnt);
525 static const struct casereader_random_class datasheet_reader_class;
527 /* Creates and returns a casereader whose input cases are the
528 rows in datasheet DS. From the caller's perspective, DS is
529 effectively destroyed by this operation, such that the caller
530 must not reference it again. */
532 datasheet_make_reader (struct datasheet *ds)
534 struct casereader *reader;
535 ds = datasheet_rename (ds);
536 reader = casereader_create_random (datasheet_get_column_cnt (ds),
537 datasheet_get_row_cnt (ds),
538 &datasheet_reader_class, ds);
539 taint_propagate (datasheet_get_taint (ds), casereader_get_taint (reader));
543 /* "read" function for the datasheet random casereader. */
545 datasheet_reader_read (struct casereader *reader UNUSED, void *ds_,
546 casenumber case_idx, struct ccase *c)
548 struct datasheet *ds = ds_;
549 if (case_idx >= datasheet_get_row_cnt (ds))
551 else if (datasheet_get_row (ds, case_idx, c))
555 taint_set_taint (ds->taint);
560 /* "destroy" function for the datasheet random casereader. */
562 datasheet_reader_destroy (struct casereader *reader UNUSED, void *ds_)
564 struct datasheet *ds = ds_;
565 datasheet_destroy (ds);
568 /* "advance" function for the datasheet random casereader. */
570 datasheet_reader_advance (struct casereader *reader UNUSED, void *ds_,
573 struct datasheet *ds = ds_;
574 datasheet_delete_rows (ds, 0, case_cnt);
577 /* Random casereader class for a datasheet. */
578 static const struct casereader_random_class datasheet_reader_class =
580 datasheet_reader_read,
581 datasheet_reader_destroy,
582 datasheet_reader_advance,
585 /* Removes SI from DS's set of sources and destroys its
588 free_source_info (struct datasheet *ds, struct source_info *si)
590 range_map_delete (&ds->sources, &si->column_range);
591 source_destroy (si->source);
595 static struct source_info *
596 source_info_from_range_map (struct range_map_node *node)
598 return range_map_data (node, struct source_info, column_range);
601 /* Reads (if OP is OP_READ) or writes (if op is OP_WRITE) the
602 COLUMN_CNT columns starting from column START_COLUMN in row
603 LROW to/from the COLUMN_CNT values in DATA. */
605 rw_case (struct datasheet *ds, enum rw_op op,
606 casenumber lrow, size_t start_column, size_t column_cnt,
612 assert (lrow < datasheet_get_row_cnt (ds));
613 assert (column_cnt <= datasheet_get_column_cnt (ds));
614 assert (start_column + column_cnt <= datasheet_get_column_cnt (ds));
616 prow = axis_map (ds->rows, lrow);
617 for (lcol = start_column; lcol < start_column + column_cnt; lcol++, data++)
619 size_t pcol = axis_map (ds->columns, lcol);
620 struct range_map_node *r = range_map_lookup (&ds->sources, pcol);
621 struct source_info *s = source_info_from_range_map (r);
622 size_t pcol_ofs = pcol - range_map_node_get_start (r);
624 ? source_read (s->source, prow, pcol_ofs, data, 1)
625 : source_write (s->source, prow, pcol_ofs, data, 1)))
627 taint_set_taint (ds->taint);
636 An axis has two functions. First, it maintains a mapping from
637 logical (client-visible) to physical (storage) ordinates. The
638 axis_map and axis_get_size functions inspect this mapping, and
639 the axis_insert, axis_remove, and axis_move functions modify
640 it. Second, it tracks the set of ordinates that are unused
641 and available for reuse. (Not all unused ordinates are
642 available for reuse: in particular, unused columns that are
643 backed by a casereader are never reused.) The axis_allocate,
644 axis_make_available, and axis_extend functions affect the set
645 of available ordinates. */
648 struct tower log_to_phy; /* Map from logical to physical ordinates;
649 contains "struct axis_group"s. */
650 struct range_set *available; /* Set of unused, available ordinates. */
651 unsigned long int phy_size; /* Current physical length of axis. */
654 /* A mapping from logical to physical ordinates. */
657 struct tower_node logical; /* Range of logical ordinates. */
658 unsigned long phy_start; /* First corresponding physical ordinate. */
661 static struct axis_group *axis_group_from_tower_node (struct tower_node *);
662 static struct tower_node *make_axis_group (unsigned long int phy_start);
663 static struct tower_node *split_axis (struct axis *, unsigned long int where);
664 static void merge_axis_nodes (struct axis *, struct tower_node *,
665 struct tower_node **other_node);
666 static void check_axis_merged (const struct axis *axis UNUSED);
668 /* Creates and returns a new, initially empty axis. */
672 struct axis *axis = xmalloc (sizeof *axis);
673 tower_init (&axis->log_to_phy);
674 axis->available = range_set_create ();
679 /* Returns a clone of existing axis OLD.
681 Currently this is used only by the datasheet model checker
682 driver, but it could be otherwise useful. */
684 axis_clone (const struct axis *old)
686 const struct tower_node *node;
689 new = xmalloc (sizeof *new);
690 tower_init (&new->log_to_phy);
691 new->available = range_set_clone (old->available, NULL);
692 new->phy_size = old->phy_size;
694 for (node = tower_first (&old->log_to_phy); node != NULL;
695 node = tower_next (&old->log_to_phy, node))
697 unsigned long int size = tower_node_get_height (node);
698 struct axis_group *group = tower_data (node, struct axis_group, logical);
699 tower_insert (&new->log_to_phy, size, make_axis_group (group->phy_start),
706 /* Adds the state of AXIS to the MD4 hash context CTX.
708 This is only used by the datasheet model checker driver. It
709 is unlikely to be otherwise useful. */
711 axis_hash (const struct axis *axis, struct md4_ctx *ctx)
713 const struct tower_node *tn;
714 const struct range_set_node *rsn;
716 for (tn = tower_first (&axis->log_to_phy); tn != NULL;
717 tn = tower_next (&axis->log_to_phy, tn))
719 struct axis_group *group = tower_data (tn, struct axis_group, logical);
720 unsigned long int phy_start = group->phy_start;
721 unsigned long int size = tower_node_get_height (tn);
723 md4_process_bytes (&phy_start, sizeof phy_start, ctx);
724 md4_process_bytes (&size, sizeof size, ctx);
727 for (rsn = range_set_first (axis->available); rsn != NULL;
728 rsn = range_set_next (axis->available, rsn))
730 unsigned long int start = range_set_node_get_start (rsn);
731 unsigned long int end = range_set_node_get_end (rsn);
733 md4_process_bytes (&start, sizeof start, ctx);
734 md4_process_bytes (&end, sizeof end, ctx);
737 md4_process_bytes (&axis->phy_size, sizeof axis->phy_size, ctx);
742 axis_destroy (struct axis *axis)
747 while (!tower_is_empty (&axis->log_to_phy))
749 struct tower_node *node = tower_first (&axis->log_to_phy);
750 struct axis_group *group = tower_data (node, struct axis_group,
752 tower_delete (&axis->log_to_phy, node);
756 range_set_destroy (axis->available);
760 /* Allocates up to REQUEST contiguous unused and available
761 ordinates from AXIS. If successful, stores the number
762 obtained into *WIDTH and the ordinate of the first into
763 *START, marks the ordinates as now unavailable return true.
764 On failure, which occurs only if AXIS has no unused and
765 available ordinates, returns false without modifying AXIS. */
767 axis_allocate (struct axis *axis, unsigned long int request,
768 unsigned long int *start, unsigned long int *width)
770 return range_set_allocate (axis->available, request, start, width);
773 /* Marks the WIDTH contiguous ordinates in AXIS, starting from
774 START, as unused and available. */
776 axis_make_available (struct axis *axis,
777 unsigned long int start, unsigned long int width)
779 range_set_insert (axis->available, start, width);
782 /* Extends the total physical length of AXIS by WIDTH and returns
783 the first ordinate in the new physical region. */
784 static unsigned long int
785 axis_extend (struct axis *axis, unsigned long int width)
787 unsigned long int start = axis->phy_size;
788 axis->phy_size += width;
792 /* Returns the physical ordinate in AXIS corresponding to logical
793 ordinate LOG_POS. LOG_POS must be less than the logical
795 static unsigned long int
796 axis_map (const struct axis *axis, unsigned long log_pos)
798 struct tower_node *node;
799 struct axis_group *group;
800 unsigned long int group_start;
802 node = tower_lookup (&axis->log_to_phy, log_pos, &group_start);
803 group = tower_data (node, struct axis_group, logical);
804 return group->phy_start + (log_pos - group_start);
807 /* Returns the logical length of AXIS. */
809 axis_get_size (const struct axis *axis)
811 return tower_height (&axis->log_to_phy);
814 /* Inserts the CNT contiguous physical ordinates starting at
815 PHY_START into AXIS's logical-to-physical mapping, starting at
816 logical position LOG_START. */
818 axis_insert (struct axis *axis,
819 unsigned long int log_start, unsigned long int phy_start,
820 unsigned long int cnt)
822 struct tower_node *before = split_axis (axis, log_start);
823 struct tower_node *new = make_axis_group (phy_start);
824 tower_insert (&axis->log_to_phy, cnt, new, before);
825 merge_axis_nodes (axis, new, NULL);
826 check_axis_merged (axis);
829 /* Removes CNT ordinates from AXIS's logical-to-physical mapping
830 starting at logical position START. */
832 axis_remove (struct axis *axis,
833 unsigned long int start, unsigned long int cnt)
837 struct tower_node *last = split_axis (axis, start + cnt);
838 struct tower_node *cur, *next;
839 for (cur = split_axis (axis, start); cur != last; cur = next)
841 next = tower_delete (&axis->log_to_phy, cur);
842 free (axis_group_from_tower_node (cur));
844 merge_axis_nodes (axis, last, NULL);
845 check_axis_merged (axis);
849 /* Moves the CNT ordinates in AXIS's logical-to-mapping starting
850 at logical position OLD_START so that they then start at
851 position NEW_START. */
853 axis_move (struct axis *axis,
854 unsigned long int old_start, unsigned long int new_start,
855 unsigned long int cnt)
857 if (cnt > 0 && old_start != new_start)
859 struct tower_node *old_first, *old_last, *new_first;
860 struct tower_node *merge1, *merge2;
861 struct tower tmp_array;
863 /* Move ordinates OLD_START...(OLD_START + CNT) into new,
864 separate TMP_ARRAY. */
865 old_first = split_axis (axis, old_start);
866 old_last = split_axis (axis, old_start + cnt);
867 tower_init (&tmp_array);
868 tower_splice (&tmp_array, NULL,
869 &axis->log_to_phy, old_first, old_last);
870 merge_axis_nodes (axis, old_last, NULL);
871 check_axis_merged (axis);
873 /* Move TMP_ARRAY to position NEW_START. */
874 new_first = split_axis (axis, new_start);
875 merge1 = tower_first (&tmp_array);
876 merge2 = tower_last (&tmp_array);
877 if (merge2 == merge1)
879 tower_splice (&axis->log_to_phy, new_first, &tmp_array, old_first, NULL);
880 merge_axis_nodes (axis, merge1, &merge2);
881 merge_axis_nodes (axis, merge2, NULL);
882 check_axis_merged (axis);
886 /* Returns the axis_group in which NODE is embedded. */
887 static struct axis_group *
888 axis_group_from_tower_node (struct tower_node *node)
890 return tower_data (node, struct axis_group, logical);
893 /* Creates and returns a new axis_group at physical position
895 static struct tower_node *
896 make_axis_group (unsigned long phy_start)
898 struct axis_group *group = xmalloc (sizeof *group);
899 group->phy_start = phy_start;
900 return &group->logical;
903 /* Returns the tower_node in AXIS's logical-to-physical map whose
904 bottom edge is at exact level WHERE. If there is no such
905 tower_node in AXIS's logical-to-physical map, then split_axis
906 creates one by breaking an existing tower_node into two
907 separate ones, unless WHERE is equal to the tower height, in
908 which case it simply returns a null pointer. */
909 static struct tower_node *
910 split_axis (struct axis *axis, unsigned long int where)
912 unsigned long int group_start;
913 struct tower_node *group_node;
914 struct axis_group *group;
916 assert (where <= tower_height (&axis->log_to_phy));
917 if (where >= tower_height (&axis->log_to_phy))
920 group_node = tower_lookup (&axis->log_to_phy, where, &group_start);
921 group = axis_group_from_tower_node (group_node);
922 if (where > group_start)
924 unsigned long int size_1 = where - group_start;
925 unsigned long int size_2 = tower_node_get_height (group_node) - size_1;
926 struct tower_node *next = tower_next (&axis->log_to_phy, group_node);
927 struct tower_node *new = make_axis_group (group->phy_start + size_1);
928 tower_resize (&axis->log_to_phy, group_node, size_1);
929 tower_insert (&axis->log_to_phy, size_2, new, next);
933 return &group->logical;
936 /* Within AXIS, attempts to merge NODE (or the last node in AXIS,
937 if NODE is null) with its neighbor nodes. This is possible
938 when logically adjacent nodes are also adjacent physically (in
941 When a merge occurs, and OTHER_NODE is non-null and points to
942 the node to be deleted, this function also updates
943 *OTHER_NODE, if necessary, to ensure that it remains a valid
946 merge_axis_nodes (struct axis *axis, struct tower_node *node,
947 struct tower_node **other_node)
949 struct tower *t = &axis->log_to_phy;
950 struct axis_group *group;
951 struct tower_node *next, *prev;
953 /* Find node to potentially merge with neighbors. */
955 node = tower_last (t);
958 group = axis_group_from_tower_node (node);
960 /* Try to merge NODE with successor. */
961 next = tower_next (t, node);
964 struct axis_group *next_group = axis_group_from_tower_node (next);
965 unsigned long this_height = tower_node_get_height (node);
967 if (group->phy_start + this_height == next_group->phy_start)
969 unsigned long next_height = tower_node_get_height (next);
970 tower_resize (t, node, this_height + next_height);
971 if (other_node != NULL && *other_node == next)
972 *other_node = tower_next (t, *other_node);
973 tower_delete (t, next);
978 /* Try to merge NODE with predecessor. */
979 prev = tower_prev (t, node);
982 struct axis_group *prev_group = axis_group_from_tower_node (prev);
983 unsigned long prev_height = tower_node_get_height (prev);
985 if (prev_group->phy_start + prev_height == group->phy_start)
987 unsigned long this_height = tower_node_get_height (node);
988 group->phy_start = prev_group->phy_start;
989 tower_resize (t, node, this_height + prev_height);
990 if (other_node != NULL && *other_node == prev)
991 *other_node = tower_next (t, *other_node);
992 tower_delete (t, prev);
998 /* Verify that all potentially merge-able nodes in AXIS are
1001 check_axis_merged (const struct axis *axis UNUSED)
1003 #if ASSERT_LEVEL >= 10
1004 struct tower_node *prev, *node;
1006 for (prev = NULL, node = tower_first (&axis->log_to_phy); node != NULL;
1007 prev = node, node = tower_next (&axis->log_to_phy, node))
1010 struct axis_group *prev_group = axis_group_from_tower_node (prev);
1011 unsigned long prev_height = tower_node_get_height (prev);
1012 struct axis_group *node_group = axis_group_from_tower_node (node);
1013 assert (prev_group->phy_start + prev_height != node_group->phy_start);
1021 size_t columns_used; /* Number of columns in use by client. */
1022 struct sparse_cases *data; /* Data at top level, atop the backing. */
1023 struct casereader *backing; /* Backing casereader (or null). */
1024 casenumber backing_rows; /* Number of rows in backing (if nonnull). */
1027 /* Creates and returns an empty, unbacked source with COLUMN_CNT
1028 columns and an initial "columns_used" of 0. */
1029 static struct source *
1030 source_create_empty (size_t column_cnt)
1032 struct source *source = xmalloc (sizeof *source);
1033 source->columns_used = 0;
1034 source->data = sparse_cases_create (column_cnt);
1035 source->backing = NULL;
1036 source->backing_rows = 0;
1040 /* Creates and returns a new source backed by READER and with the
1041 same initial dimensions and content. */
1042 static struct source *
1043 source_create_casereader (struct casereader *reader)
1045 struct source *source
1046 = source_create_empty (casereader_get_value_cnt (reader));
1047 source->backing = reader;
1048 source->backing_rows = casereader_count_cases (reader);
1052 /* Returns a clone of source OLD with the same data and backing
1055 Currently this is used only by the datasheet model checker
1056 driver, but it could be otherwise useful. */
1057 static struct source *
1058 source_clone (const struct source *old)
1060 struct source *new = xmalloc (sizeof *new);
1061 new->columns_used = old->columns_used;
1062 new->data = sparse_cases_clone (old->data);
1063 new->backing = old->backing != NULL ? casereader_clone (old->backing) : NULL;
1064 new->backing_rows = old->backing_rows;
1065 if (new->data == NULL)
1067 source_destroy (new);
1073 /* Increases the columns_used count of SOURCE by DELTA.
1074 The new value must not exceed SOURCE's number of columns. */
1076 source_increase_use (struct source *source, size_t delta)
1078 source->columns_used += delta;
1079 assert (source->columns_used <= sparse_cases_get_value_cnt (source->data));
1082 /* Decreases the columns_used count of SOURCE by DELTA.
1083 This must not attempt to decrease the columns_used count below
1086 source_decrease_use (struct source *source, size_t delta)
1088 assert (delta <= source->columns_used);
1089 source->columns_used -= delta;
1092 /* Returns true if SOURCE has any columns in use,
1095 source_in_use (const struct source *source)
1097 return source->columns_used > 0;
1100 /* Destroys SOURCE and its data and backing, if any. */
1102 source_destroy (struct source *source)
1106 sparse_cases_destroy (source->data);
1107 casereader_destroy (source->backing);
1112 /* Returns the number of rows in SOURCE's backing casereader
1113 (SOURCE must have a backing casereader). */
1115 source_get_backing_row_cnt (const struct source *source)
1117 assert (source_has_backing (source));
1118 return source->backing_rows;
1121 /* Returns the number of columns in SOURCE. */
1123 source_get_column_cnt (const struct source *source)
1125 return sparse_cases_get_value_cnt (source->data);
1128 /* Reads VALUE_CNT columns from SOURCE in the given ROW, starting
1129 from COLUMN, into VALUES. Returns true if successful, false
1132 source_read (const struct source *source,
1133 casenumber row, size_t column,
1134 union value values[], size_t value_cnt)
1136 if (source->backing == NULL || sparse_cases_contains_row (source->data, row))
1137 return sparse_cases_read (source->data, row, column, values, value_cnt);
1143 assert (source->backing != NULL);
1144 ok = casereader_peek (source->backing, row, &c);
1147 case_copy_out (&c, column, values, value_cnt);
1154 /* Writes the VALUE_CNT values in VALUES to SOURCE in the given
1155 ROW, starting at ROW. Returns true if successful, false on
1156 I/O error. On error, the row's data may be completely or
1157 partially corrupted, both inside and outside the region to be
1160 source_write (struct source *source,
1161 casenumber row, size_t column,
1162 const union value values[], size_t value_cnt)
1164 size_t column_cnt = sparse_cases_get_value_cnt (source->data);
1167 if (source->backing == NULL
1168 || (column == 0 && value_cnt == column_cnt)
1169 || sparse_cases_contains_row (source->data, row))
1170 ok = sparse_cases_write (source->data, row, column, values, value_cnt);
1174 if (row < source->backing_rows)
1175 ok = casereader_peek (source->backing, row, &c);
1178 /* It's not one of the backed rows. Ideally, this
1179 should never happen: we'd always be writing the full
1180 contents of new, unbacked rows in a single call to
1181 this function, so that the first case above would
1182 trigger. But that's a little difficult at higher
1183 levels, so that we in fact usually write the full
1184 contents of new, unbacked rows in multiple calls to
1185 this function. Make this work. */
1186 case_create (&c, column_cnt);
1191 case_copy_in (&c, column, values, value_cnt);
1192 ok = sparse_cases_write (source->data, row, 0,
1193 case_data_all (&c), column_cnt);
1200 /* Within SOURCE, which must not have a backing casereader,
1201 writes the VALUE_CNT values in VALUES_CNT to the VALUE_CNT
1202 columns starting from START_COLUMN, in every row, even in rows
1203 not yet otherwise initialized. Returns true if successful,
1204 false if an I/O error occurs.
1206 We don't support backing != NULL because (1) it's harder and
1207 (2) source_write_columns is only called by
1208 datasheet_insert_columns, which doesn't reuse columns from
1209 sources that are backed by casereaders. */
1211 source_write_columns (struct source *source, size_t start_column,
1212 const union value values[], size_t value_cnt)
1214 assert (source->backing == NULL);
1216 return sparse_cases_write_columns (source->data, start_column,
1220 /* Returns true if SOURCE has a backing casereader, false
1223 source_has_backing (const struct source *source)
1225 return source->backing != NULL;
1228 /* Datasheet model checker test driver. */
1230 /* Maximum size of datasheet supported for model checking
1235 /* Hashes the structure of datasheet DS and returns the hash.
1236 We use MD4 because it is much faster than MD5 or SHA-1 but its
1237 collision resistance is just as good. */
1239 hash_datasheet (const struct datasheet *ds)
1241 unsigned int hash[DIV_RND_UP (20, sizeof (unsigned int))];
1243 struct range_map_node *r;
1245 md4_init_ctx (&ctx);
1246 axis_hash (ds->columns, &ctx);
1247 axis_hash (ds->rows, &ctx);
1248 for (r = range_map_first (&ds->sources); r != NULL;
1249 r = range_map_next (&ds->sources, r))
1251 unsigned long int start = range_map_node_get_start (r);
1252 unsigned long int end = range_map_node_get_end (r);
1253 md4_process_bytes (&start, sizeof start, &ctx);
1254 md4_process_bytes (&end, sizeof end, &ctx);
1256 md4_process_bytes (&ds->column_min_alloc, sizeof ds->column_min_alloc,
1258 md4_finish_ctx (&ctx, hash);
1262 /* Clones the structure and contents of ODS into a new datasheet,
1263 and returns the new datasheet. */
1264 static struct datasheet *
1265 clone_datasheet (const struct datasheet *ods)
1267 struct datasheet *ds;
1268 struct range_map_node *r;
1270 ds = xmalloc (sizeof *ds);
1271 ds->columns = axis_clone (ods->columns);
1272 ds->rows = axis_clone (ods->rows);
1273 range_map_init (&ds->sources);
1274 for (r = range_map_first (&ods->sources); r != NULL;
1275 r = range_map_next (&ods->sources, r))
1277 const struct source_info *osi = source_info_from_range_map (r);
1278 struct source_info *si = xmalloc (sizeof *si);
1279 si->source = source_clone (osi->source);
1280 range_map_insert (&ds->sources, range_map_node_get_start (r),
1281 range_map_node_get_width (r), &si->column_range);
1283 ds->column_min_alloc = ods->column_min_alloc;
1284 ds->taint = taint_create ();
1289 /* lazy_casereader callback function to instantiate a casereader
1290 from the datasheet. */
1291 static struct casereader *
1292 lazy_callback (void *ds_)
1294 struct datasheet *ds = ds_;
1295 return datasheet_make_reader (ds);
1298 /* Checks that READER contains the ROW_CNT rows and COLUMN_CNT
1299 columns of data in ARRAY, reporting any errors via MC. */
1301 check_datasheet_casereader (struct mc *mc, struct casereader *reader,
1302 double array[MAX_ROWS][MAX_COLS],
1303 size_t row_cnt, size_t column_cnt)
1305 if (casereader_get_case_cnt (reader) != row_cnt)
1307 if (casereader_get_case_cnt (reader) == CASENUMBER_MAX
1308 && casereader_count_cases (reader) == row_cnt)
1309 mc_error (mc, "datasheet casereader has unknown case count");
1311 mc_error (mc, "casereader row count (%lu) does not match "
1313 (unsigned long int) casereader_get_case_cnt (reader),
1316 else if (casereader_get_value_cnt (reader) != column_cnt)
1317 mc_error (mc, "casereader column count (%zu) does not match "
1319 casereader_get_value_cnt (reader), column_cnt);
1325 for (row = 0; row < row_cnt; row++)
1329 if (!casereader_read (reader, &c))
1331 mc_error (mc, "casereader_read failed reading row %zu of %zu "
1332 "(%zu columns)", row, row_cnt, column_cnt);
1336 for (col = 0; col < column_cnt; col++)
1337 if (case_num_idx (&c, col) != array[row][col])
1338 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: "
1340 row, col, row_cnt, column_cnt,
1341 case_num_idx (&c, col), array[row][col]);
1344 if (casereader_read (reader, &c))
1345 mc_error (mc, "casereader has extra cases (expected %zu)", row_cnt);
1349 /* Checks that datasheet DS contains has ROW_CNT rows, COLUMN_CNT
1350 columns, and the same contents as ARRAY, reporting any
1351 mismatches via mc_error. Then, adds DS to MC as a new state. */
1353 check_datasheet (struct mc *mc, struct datasheet *ds,
1354 double array[MAX_ROWS][MAX_COLS],
1355 size_t row_cnt, size_t column_cnt)
1357 struct datasheet *ds2;
1358 struct casereader *reader;
1359 unsigned long int serial = 0;
1361 assert (row_cnt < MAX_ROWS);
1362 assert (column_cnt < MAX_COLS);
1364 /* If it is a duplicate hash, discard the state before checking
1365 its consistency, to save time. */
1366 if (mc_discard_dup_state (mc, hash_datasheet (ds)))
1368 datasheet_destroy (ds);
1372 /* Check contents of datasheet via datasheet functions. */
1373 if (row_cnt != datasheet_get_row_cnt (ds))
1374 mc_error (mc, "row count (%lu) does not match expected (%zu)",
1375 (unsigned long int) datasheet_get_row_cnt (ds), row_cnt);
1376 else if (column_cnt != datasheet_get_column_cnt (ds))
1377 mc_error (mc, "column count (%zu) does not match expected (%zu)",
1378 datasheet_get_column_cnt (ds), column_cnt);
1383 for (row = 0; row < row_cnt; row++)
1384 for (col = 0; col < column_cnt; col++)
1387 if (!datasheet_get_value (ds, row, col, &v, 1))
1389 if (v.f != array[row][col])
1390 mc_error (mc, "element %zu,%zu (of %zu,%zu) differs: %g != %g",
1391 row, col, row_cnt, column_cnt, v.f, array[row][col]);
1395 /* Check that datasheet contents are correct when read through
1397 ds2 = clone_datasheet (ds);
1398 reader = datasheet_make_reader (ds2);
1399 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
1400 casereader_destroy (reader);
1402 /* Check that datasheet contents are correct when read through
1403 casereader with lazy_casereader wrapped around it. This is
1404 valuable because otherwise there is no non-GUI code that
1405 uses the lazy_casereader. */
1406 ds2 = clone_datasheet (ds);
1407 reader = lazy_casereader_create (column_cnt, row_cnt,
1408 lazy_callback, ds2, &serial);
1409 check_datasheet_casereader (mc, reader, array, row_cnt, column_cnt);
1410 if (lazy_casereader_destroy (reader, serial))
1412 /* Lazy casereader was never instantiated. This will
1413 only happen if there are no rows (because in that case
1414 casereader_read never gets called). */
1415 datasheet_destroy (ds2);
1417 mc_error (mc, "lazy casereader not instantiated, but should "
1418 "have been (size %zu,%zu)", row_cnt, column_cnt);
1422 /* Lazy casereader was instantiated. This is the common
1423 case, in which some casereader operation
1424 (casereader_read in this case) was performed on the
1426 casereader_destroy (reader);
1428 mc_error (mc, "lazy casereader instantiated, but should not "
1429 "have been (size %zu,%zu)", row_cnt, column_cnt);
1432 mc_add_state (mc, ds);
1435 /* Extracts the contents of DS into DATA. */
1437 extract_data (const struct datasheet *ds, double data[MAX_ROWS][MAX_COLS])
1439 size_t column_cnt = datasheet_get_column_cnt (ds);
1440 size_t row_cnt = datasheet_get_row_cnt (ds);
1443 assert (row_cnt < MAX_ROWS);
1444 assert (column_cnt < MAX_COLS);
1445 for (row = 0; row < row_cnt; row++)
1446 for (col = 0; col < column_cnt; col++)
1449 if (!datasheet_get_value (ds, row, col, &v, 1))
1451 data[row][col] = v.f;
1455 /* Clones the structure and contents of ODS into *DS,
1456 and the contents of ODATA into DATA. */
1458 clone_model (const struct datasheet *ods, double odata[MAX_ROWS][MAX_COLS],
1459 struct datasheet **ds, double data[MAX_ROWS][MAX_COLS])
1461 *ds = clone_datasheet (ods);
1462 memcpy (data, odata, MAX_ROWS * MAX_COLS * sizeof **data);
1465 /* "init" function for struct mc_class. */
1467 datasheet_mc_init (struct mc *mc)
1469 struct datasheet_test_params *params = mc_get_aux (mc);
1470 struct datasheet *ds;
1472 if (params->backing_rows == 0 && params->backing_cols == 0)
1474 /* Create unbacked datasheet. */
1475 ds = datasheet_create (NULL);
1476 mc_name_operation (mc, "empty datasheet");
1477 check_datasheet (mc, ds, NULL, 0, 0);
1481 /* Create datasheet with backing. */
1482 struct casewriter *writer;
1483 struct casereader *reader;
1484 double data[MAX_ROWS][MAX_COLS];
1487 assert (params->backing_rows > 0 && params->backing_rows <= MAX_ROWS);
1488 assert (params->backing_cols > 0 && params->backing_cols <= MAX_COLS);
1490 writer = mem_writer_create (params->backing_cols);
1491 for (row = 0; row < params->backing_rows; row++)
1496 case_create (&c, params->backing_cols);
1497 for (col = 0; col < params->backing_cols; col++)
1499 double value = params->next_value++;
1500 data[row][col] = value;
1501 case_data_rw_idx (&c, col)->f = value;
1503 casewriter_write (writer, &c);
1505 reader = casewriter_make_reader (writer);
1506 assert (reader != NULL);
1508 ds = datasheet_create (reader);
1509 mc_name_operation (mc, "datasheet with (%d,%d) backing",
1510 params->backing_rows, params->backing_cols);
1511 check_datasheet (mc, ds, data,
1512 params->backing_rows, params->backing_cols);
1516 /* "mutate" function for struct mc_class. */
1518 datasheet_mc_mutate (struct mc *mc, const void *ods_)
1520 struct datasheet_test_params *params = mc_get_aux (mc);
1522 const struct datasheet *ods = ods_;
1523 double odata[MAX_ROWS][MAX_COLS];
1524 double data[MAX_ROWS][MAX_COLS];
1525 size_t column_cnt = datasheet_get_column_cnt (ods);
1526 size_t row_cnt = datasheet_get_row_cnt (ods);
1527 size_t pos, new_pos, cnt;
1529 extract_data (ods, odata);
1531 /* Insert all possible numbers of columns in all possible
1533 for (pos = 0; pos <= column_cnt; pos++)
1534 for (cnt = 0; cnt <= params->max_cols - column_cnt; cnt++)
1535 if (mc_include_state (mc))
1537 struct datasheet *ds;
1538 union value new[MAX_COLS];
1541 mc_name_operation (mc, "insert %zu columns at %zu", cnt, pos);
1542 clone_model (ods, odata, &ds, data);
1544 for (i = 0; i < cnt; i++)
1545 new[i].f = params->next_value++;
1547 if (!datasheet_insert_columns (ds, new, cnt, pos))
1548 mc_error (mc, "datasheet_insert_columns failed");
1550 for (i = 0; i < row_cnt; i++)
1552 insert_range (&data[i][0], column_cnt, sizeof data[i][0],
1554 for (j = 0; j < cnt; j++)
1555 data[i][pos + j] = new[j].f;
1558 check_datasheet (mc, ds, data, row_cnt, column_cnt + cnt);
1561 /* Delete all possible numbers of columns from all possible
1563 for (pos = 0; pos < column_cnt; pos++)
1564 for (cnt = 0; cnt < column_cnt - pos; cnt++)
1565 if (mc_include_state (mc))
1567 struct datasheet *ds;
1570 mc_name_operation (mc, "delete %zu columns at %zu", cnt, pos);
1571 clone_model (ods, odata, &ds, data);
1573 datasheet_delete_columns (ds, pos, cnt);
1575 for (i = 0; i < row_cnt; i++)
1576 remove_range (&data[i], column_cnt, sizeof *data[i], pos, cnt);
1578 check_datasheet (mc, ds, data, row_cnt, column_cnt - cnt);
1581 /* Move all possible numbers of columns from all possible
1582 existing positions to all possible new positions. */
1583 for (pos = 0; pos < column_cnt; pos++)
1584 for (cnt = 0; cnt < column_cnt - pos; cnt++)
1585 for (new_pos = 0; new_pos < column_cnt - cnt; new_pos++)
1586 if (mc_include_state (mc))
1588 struct datasheet *ds;
1591 clone_model (ods, odata, &ds, data);
1592 mc_name_operation (mc, "move %zu columns from %zu to %zu",
1595 datasheet_move_columns (ds, pos, new_pos, cnt);
1597 for (i = 0; i < row_cnt; i++)
1598 move_range (&data[i], column_cnt, sizeof data[i][0],
1601 check_datasheet (mc, ds, data, row_cnt, column_cnt);
1604 /* Insert all possible numbers of rows in all possible
1606 for (pos = 0; pos <= row_cnt; pos++)
1607 for (cnt = 0; cnt <= params->max_rows - row_cnt; cnt++)
1608 if (mc_include_state (mc))
1610 struct datasheet *ds;
1611 struct ccase c[MAX_ROWS];
1614 clone_model (ods, odata, &ds, data);
1615 mc_name_operation (mc, "insert %zu rows at %zu", cnt, pos);
1617 for (i = 0; i < cnt; i++)
1619 case_create (&c[i], column_cnt);
1620 for (j = 0; j < column_cnt; j++)
1621 case_data_rw_idx (&c[i], j)->f = params->next_value++;
1624 insert_range (data, row_cnt, sizeof data[pos], pos, cnt);
1625 for (i = 0; i < cnt; i++)
1626 for (j = 0; j < column_cnt; j++)
1627 data[i + pos][j] = case_num_idx (&c[i], j);
1629 if (!datasheet_insert_rows (ds, pos, c, cnt))
1630 mc_error (mc, "datasheet_insert_rows failed");
1632 check_datasheet (mc, ds, data, row_cnt + cnt, column_cnt);
1635 /* Delete all possible numbers of rows from all possible
1637 for (pos = 0; pos < row_cnt; pos++)
1638 for (cnt = 0; cnt < row_cnt - pos; cnt++)
1639 if (mc_include_state (mc))
1641 struct datasheet *ds;
1643 clone_model (ods, odata, &ds, data);
1644 mc_name_operation (mc, "delete %zu rows at %zu", cnt, pos);
1646 datasheet_delete_rows (ds, pos, cnt);
1648 remove_range (&data[0], row_cnt, sizeof data[0], pos, cnt);
1650 check_datasheet (mc, ds, data, row_cnt - cnt, column_cnt);
1653 /* Move all possible numbers of rows from all possible existing
1654 positions to all possible new positions. */
1655 for (pos = 0; pos < row_cnt; pos++)
1656 for (cnt = 0; cnt < row_cnt - pos; cnt++)
1657 for (new_pos = 0; new_pos < row_cnt - cnt; new_pos++)
1658 if (mc_include_state (mc))
1660 struct datasheet *ds;
1662 clone_model (ods, odata, &ds, data);
1663 mc_name_operation (mc, "move %zu rows from %zu to %zu",
1666 datasheet_move_rows (ds, pos, new_pos, cnt);
1668 move_range (&data[0], row_cnt, sizeof data[0],
1671 check_datasheet (mc, ds, data, row_cnt, column_cnt);
1675 /* "destroy" function for struct mc_class. */
1677 datasheet_mc_destroy (const struct mc *mc UNUSED, void *ds_)
1679 struct datasheet *ds = ds_;
1680 datasheet_destroy (ds);
1683 /* Executes the model checker on the datasheet test driver with
1684 the given OPTIONS and passing in the given PARAMS, which must
1685 point to a modifiable "struct datasheet_test_params". If any
1686 value in PARAMS is out of range, it will be adjusted into the
1687 valid range before running the test.
1689 Returns the results of the model checking run. */
1691 datasheet_test (struct mc_options *options, void *params_)
1693 struct datasheet_test_params *params = params_;
1694 static const struct mc_class datasheet_mc_class =
1697 datasheet_mc_mutate,
1698 datasheet_mc_destroy,
1701 params->next_value = 1;
1702 params->max_rows = MIN (params->max_rows, MAX_ROWS);
1703 params->max_cols = MIN (params->max_cols, MAX_COLS);
1704 params->backing_rows = MIN (params->backing_rows, params->max_rows);
1705 params->backing_cols = MIN (params->backing_cols, params->max_cols);
1707 mc_options_set_aux (options, params);
1708 return mc_run (&datasheet_mc_class, options);