From 62d87e063318cc4c842b1b2d8c184f48aeaf6659 Mon Sep 17 00:00:00 2001 From: Sebastiano Tronto Date: Mon, 19 May 2025 17:45:14 +0200 Subject: Refactored checkdata Relevant changes include: - Changed the signature of nissy_checkdata(). - Removed expected_distribution.h from tools; this data is now included in each solver's src/ code. - Removed distribution check for cocsep; may add back later. --- src/solvers/h48/checkdata.h | 234 +++++++++++++++++++++++++++++++++++++++ src/solvers/h48/gendata_eoesep.h | 4 +- src/solvers/h48/gendata_h48.h | 90 --------------- src/solvers/h48/h48.h | 1 + 4 files changed, 237 insertions(+), 92 deletions(-) create mode 100644 src/solvers/h48/checkdata.h (limited to 'src/solvers/h48') diff --git a/src/solvers/h48/checkdata.h b/src/solvers/h48/checkdata.h new file mode 100644 index 0000000..53e616b --- /dev/null +++ b/src/solvers/h48/checkdata.h @@ -0,0 +1,234 @@ +STATIC long long checkdata_h48( + const char *, unsigned long long n, const unsigned char [n]); + +/* +Currently unused. +TODO: re-introduce check on cocsep table +*/ +uint64_t expected_cocsep[21] = { + [0] = 1, + [1] = 6, + [2] = 63, + [3] = 468, + [4] = 3068, + [5] = 15438, + [6] = 53814, + [7] = 71352, + [8] = 8784, + [9] = 96 +}; + +struct { + uint8_t max; + uint64_t table[21]; +} expected_h48[12][9] = { + [0] = { + [2] = { + .max = 3, + .table = { + [0] = 5473562, + [1] = 34776317, + [2] = 68566704, + [3] = 8750867, + }, + }, + [4] = { + .max = 12, + .table = { + [0] = 1, + [1] = 1, + [2] = 4, + [3] = 34, + [4] = 331, + [5] = 3612, + [6] = 41605, + [7] = 474128, + [8] = 4953846, + [9] = 34776317, + [10] = 68566704, + [11] = 8749194, + [12] = 1673, + }, + }, + }, + [1] = { + [2] = { + .max = 3, + .table = { + [0] = 6012079, + [1] = 45822302, + [2] = 142018732, + [3] = 41281787, + }, + }, + }, + [2] = { + [2] = { + .max = 3, + .table = { + [0] = 6391286, + [1] = 55494785, + [2] = 252389935, + [3] = 155993794, + }, + }, + }, + [3] = { + [2] = { + .max = 3, + .table = { + [0] = 6686828, + [1] = 63867852, + [2] = 392789689, + [3] = 477195231, + }, + }, + }, + [4] = { + [2] = { + .max = 3, + .table = { + [0] = 77147213, + [1] = 543379415, + [2] = 1139570251, + [3] = 120982321, + }, + }, + }, + [5] = { + [2] = { + .max = 3, + .table = { + [0] = 82471284, + [1] = 687850732, + [2] = 2345840746, + [3] = 645995638, + }, + }, + }, + [6] = { + [2] = { + .max = 3, + .table = { + [0] = 85941099, + [1] = 804752968, + [2] = 4077248182, + [3] = 2556374551, + }, + }, + }, + [7] = { + [2] = { + .max = 3, + .table = { + [0] = 88529761, + [1] = 897323475, + [2] = 6126260791, + [3] = 7936519573, + }, + }, + }, + [8] = { + [2] = { + .max = 3, + .table = { + [0] = 1051579940, + [1] = 8136021316, + [2] = 19024479822, + [3] = 18851861220, + }, + }, + }, + [9] = { + [2] = { + .max = 3, + .table = { + [0] = 1102038189, + [1] = 9888265242, + [2] = 38299375805, + [3] = 10904855164, + }, + }, + }, + [10] = { + [2] = { + .max = 3, + .table = { + [0] = 1133240039, + [1] = 11196285614, + [2] = 64164702961, + [3] = 43894840186, + }, + }, + }, + [11] = { + [2] = { + .max = 3, + .table = { + [0] = 1150763161, + [1] = 12045845660, + [2] = 91163433330, + [3] = 136418095449, + }, + }, + }, +}; + +STATIC long long +checkdata_h48( + const char *solver, + unsigned long long data_size, + const unsigned char data[data_size] +) +{ + const unsigned char *table; + tableinfo_t info; + int64_t err; + uint64_t actual_distribution[INFO_DISTRIBUTION_LEN]; + uint8_t em; + uint64_t *ed; + + if ((size_t)data % 8 != 0) { + LOG("[checkdata] Error: buffer is not 8-byte aligned\n"); + return NISSY_ERROR_DATA; + } + + do { + err = readtableinfo(data_size, data, &info); + if (err != NISSY_OK) { + LOG("[checkdata] Data is corrupt\n"); + return NISSY_ERROR_DATA; + } + + table = data + INFOSIZE; + data += info.next; + data_size -= info.next; + + if (info.type != TABLETYPE_PRUNING) { + LOG("[checkdata] Skipping '%s'\n", info.solver); + continue; + } + + ed = expected_h48[info.h48h][info.bits].table; + em = expected_h48[info.h48h][info.bits].max; + + LOG("[checkdata] Checking distribution for '%s' from " + "table preamble\n", info.solver); + if (!distribution_equal(ed, info.distribution, em)) { + LOG("[checkdata] Distribution from the table preamble " + "does not matche the expected one\n"); + return NISSY_ERROR_DATA; + } + + LOG("[checkdata] Checking distribution for '%s' from " + "actual table\n", info.solver); + getdistribution(table, actual_distribution, &info); + if (!distribution_equal(ed, actual_distribution, em)) { + LOG("[checkdata] Distribution from the actual table " + "does not match the expected one\n"); + return NISSY_ERROR_DATA; + } + } while (info.next != 0); + + return NISSY_OK; +} diff --git a/src/solvers/h48/gendata_eoesep.h b/src/solvers/h48/gendata_eoesep.h index f1e3d4c..52e2b8b 100644 --- a/src/solvers/h48/gendata_eoesep.h +++ b/src/solvers/h48/gendata_eoesep.h @@ -79,7 +79,7 @@ gendata_eoesep(unsigned char *buf, uint8_t maxdepth) if (buf == NULL) goto gendata_eoesep_return_size; - LOG("Computing eoesep data\n"); + LOG("[H48 gendata] Computing eoesep data\n"); memset(buf, 0xFF, EOESEP_FULLSIZE); esep_classes = (uint32_t *)(buf + INFOSIZE); buf8 = buf + INFOSIZE + 4*ESEP_MAX; @@ -111,7 +111,7 @@ gendata_eoesep(unsigned char *buf, uint8_t maxdepth) writetableinfo(&info, EOESEP_FULLSIZE, buf); - LOG("eoesep data computed\n"); + LOG("[H48 gendata] eoesep data computed\n"); gendata_eoesep_return_size: return EOESEP_FULLSIZE; diff --git a/src/solvers/h48/gendata_h48.h b/src/solvers/h48/gendata_h48.h index 644ddc2..d1ab3bd 100644 --- a/src/solvers/h48/gendata_h48.h +++ b/src/solvers/h48/gendata_h48.h @@ -25,8 +25,6 @@ STATIC_INLINE uint8_t get_h48_pval_atomic( STATIC_INLINE void set_h48_pval_atomic( _Atomic unsigned char *, int64_t, uint8_t, uint8_t); -size_t gendata_h48_derive(uint8_t, const unsigned char *, unsigned char *); - STATIC long long gendata_h48_dispatch( const char *solver, @@ -711,91 +709,3 @@ set_h48_pval_atomic( table[H48_INDEX(i, k)] = (table[H48_INDEX(i, k)] & (~H48_MASK(i, k))) | (val << H48_SHIFT(i, k)); } - -size_t -gendata_h48_derive(uint8_t h, const unsigned char *fulltable, unsigned char *buf) -{ - size_t cocsepsize, h48size; - uint8_t val_full, val_derive; - const unsigned char *h48full; - unsigned char *h48derive; - int64_t i, j, h48max; - uint64_t bufsize; - gendata_h48_arg_t arg; - tableinfo_t cocsepinfo, fulltableinfo; - - /* Initializing values in case of error */ - /* TODO cleanup this */ - fulltableinfo.h48h = 11; - fulltableinfo.bits = 2; - fulltableinfo.base = 8; - - int64_t TODOlarge = 999999999999; /* TODO: cleanup here */ - - readtableinfo_n(TODOlarge, fulltable, 2, &fulltableinfo); - arg.h = h; - arg.k = fulltableinfo.bits; - arg.maxdepth = 20; - arg.buf = buf; - arg.cocsepdata = (uint32_t *)(buf + INFOSIZE); - arg.base = fulltableinfo.base; - arg.info = makeinfo_h48k2(&arg); - - /* Technically this step is redundant, except that we - need selfsim and crep */ - cocsepsize = gendata_cocsep(buf, arg.selfsim, arg.crep); - arg.h48buf = (_Atomic unsigned char *)buf + cocsepsize; - h48size = H48_TABLESIZE(h, arg.k) + INFOSIZE; - - if (buf == NULL) - goto gendata_h48_derive_return_size; - - bufsize = COCSEP_FULLSIZE + INFOSIZE; - if (readtableinfo(bufsize, buf, &cocsepinfo) != NISSY_OK) { - LOG("[H48 derive gendata] Error: could not read info for " - "cocsep table\n"); - goto gendata_h48_derive_error; - } - - cocsepinfo.next = cocsepsize; - bufsize = COCSEP_FULLSIZE + INFOSIZE; - if (writetableinfo(&cocsepinfo, bufsize, buf) != NISSY_OK) { - LOG("[H48 derive gendata] Error: could not write info for " - "cocsep table with updated 'next' value\n"); - goto gendata_h48_derive_error; - } - - h48full = fulltable + cocsepsize + INFOSIZE; - h48derive = (unsigned char *)arg.h48buf + INFOSIZE; - memset(h48derive, 0xFF, H48_TABLESIZE(h, arg.k)); - memset(arg.info.distribution, 0, - INFO_DISTRIBUTION_LEN * sizeof(uint64_t)); - - h48max = H48_COORDMAX(fulltableinfo.h48h); - for (i = 0; i < h48max; i++) { - if (i % INT64_C(1000000000) == 0 && i > 0) - LOG("[H48 derive gendata] Processing %" PRId64 - "th coordinate\n", i); - j = i >> (int64_t)(fulltableinfo.h48h - h); - val_full = get_h48_pval(h48full, i, arg.k); - val_derive = get_h48_pval(h48derive, j, arg.k); - set_h48_pval( - h48derive, j, arg.k, MIN(val_full, val_derive)); - } - - getdistribution(h48derive, arg.info.distribution, &arg.info); - - bufsize = arg.buf_size - COCSEP_FULLSIZE - INFOSIZE; - if (writetableinfo(&arg.info, bufsize, (unsigned char *)arg.h48buf) - != NISSY_OK) { - LOG("H48 derive gendata] Error: could not write info " - "for table\n"); - goto gendata_h48_derive_error; - } - -gendata_h48_derive_return_size: - return cocsepsize + h48size; - -gendata_h48_derive_error: - return 0; -} diff --git a/src/solvers/h48/h48.h b/src/solvers/h48/h48.h index 79d2583..44fdb59 100644 --- a/src/solvers/h48/h48.h +++ b/src/solvers/h48/h48.h @@ -7,4 +7,5 @@ #include "gendata_cocsep.h" #include "gendata_eoesep.h" #include "gendata_h48.h" +#include "checkdata.h" #include "solve.h" -- cgit v1.3