diff --git a/src/parser/parser.h b/src/parser/parser.h index 584019b99..f66369bd2 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -18,13 +18,46 @@ #include #include #include +#include #include #include "src/exceptions/file_IO_exception.h" +#include "src/exceptions/wrong_file_format.h" namespace mrmc { namespace parser { + /*! + * @brief Parses integer and checks, if something has been parsed. + * + * Calls strtol() internally and checks if the new pointer is different + * from the original one, i.e. if str != *end. If they are the same, a + * mrmc::exceptions::wrong_file_format will be thrown. + * @param str String to parse + * @param end New pointer will be written there + * @return Result of strtol() + */ + inline uint_fast64_t checked_strtol(const char* str, char** end) + { + uint_fast64_t res = strtol(str, end, 10); + if (str == *end) throw mrmc::exceptions::wrong_file_format(); + return res; + } + + /*! + * @brief Skips common whitespaces in a string. + * + * Skips spaces, tabs, newlines and carriage returns. Returns pointer + * to first char that is not a whitespace. + * @param buf String buffer + * @return pointer to first non-whitespace character + */ + inline char* skipWS(char* buf) + { + while ((*buf == ' ') || (*buf == '\t') || (*buf == '\n') || (*buf == '\r')) buf++; + return buf; + } + /*! * @brief Opens a file and maps it to memory providing a char* * containing the file content. @@ -79,7 +112,7 @@ namespace parser { * Will stat the given file, open it and map it to memory. * If anything of this fails, an appropriate exception is raised * and a log entry is written. - * @filename file to be opened + * @param filename file to be opened */ MappedFile(const char* filename) { diff --git a/src/parser/readLabFile.cpp b/src/parser/readLabFile.cpp index 01c44d420..c9e6f2f12 100644 --- a/src/parser/readLabFile.cpp +++ b/src/parser/readLabFile.cpp @@ -43,7 +43,7 @@ namespace parser { * @param filename input .lab file's name. * @return The pointer to the created labeling object. */ -mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename) +mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename) { /* * open file @@ -55,10 +55,14 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha * first run: obtain number of propositions */ char separator[] = " \n\t"; + bool foundDecl = false, foundEnd = false; uint_fast32_t proposition_count = 0; { size_t cnt = 0; - do + /* + * iterate over tokens while not at end of file + */ + while(buf[0] != '\0') { buf += cnt; cnt = strcspn(buf, separator); // position of next separator @@ -69,12 +73,25 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha * next token is #END: stop search * otherwise increase proposition_count */ - if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; - if (strncmp(buf, "#END", cnt) == 0) break; + if (strncmp(buf, "#DECLARATION", cnt) == 0) + { + foundDecl = true; + continue; + } + if (strncmp(buf, "#END", cnt) == 0) + { + foundEnd = true; + break; + } proposition_count++; } - else cnt = 1; // next char is separator, one step forward - } while (cnt > 0); + else buf++; // next char is separator, one step forward + } + + /* + * If #DECLARATION or #END were not found, the file format is wrong + */ + if (! (foundDecl && foundEnd)) throw mrmc::exceptions::wrong_file_format(); } /* @@ -91,6 +108,7 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha { /* * load propositions + * As we already checked the file format, we can be a bit sloppy here... */ char proposition[128]; // buffer for proposition names size_t cnt = 0; @@ -126,40 +144,43 @@ mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const cha */ uint_fast32_t node; char proposition[128]; + char* tmp; size_t cnt; - do + /* + * iterate over nodes + */ + while (buf[0] != '\0') { - node = strtol(buf, &buf, 10); // parse node number - while (*buf != '\0') // while not at end of file - { - cnt = strcspn(buf, separator); // position of next separator - if (cnt == 0) buf++; // next char is separator, one step forward - else break; - } /* - * if cnt > 0, buf points to the next proposition - * otherwise, we have reached the end of the file + * parse node number, then iterate over propositions */ - if (cnt > 0) - { - /* - * copy proposition to buffer, add assignment to labeling - */ - strncpy(proposition, buf, cnt); - proposition[cnt] = '\0'; - result->addAtomicPropositionToState(proposition, node); - } - else if (node == 0) + node = checked_strtol(buf, &buf); + while (buf[0] != '\n') { - /* - * If this is executed, we could read a number but there - * was no proposition after that. This strongly suggests a - * broken file, but it's not fatal... - */ - pantheios::log_WARNING("The label file ended on a node number. Is the file malformated?"); + cnt = strcspn(buf, separator); + if (cnt == 0) + { + /* + * next char is a separator + * if it's a newline, we continue with next node + * otherwise we skip it and try again + */ + if (buf[0] == '\n') break; + buf++; + } + else + { + /* + * copy proposition to buffer and add it to result + */ + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + result->addAtomicPropositionToState(proposition, node); + buf += cnt; + } } - buf += cnt; - } while (cnt > 0); + buf = skipWS(buf); + } } return result; diff --git a/src/parser/readLabFile.h b/src/parser/readLabFile.h index 31375ced8..625bd5685 100644 --- a/src/parser/readLabFile.h +++ b/src/parser/readLabFile.h @@ -10,7 +10,7 @@ namespace parser { /*! * @brief Load label file and return initialized AtomicPropositionsLabeling object. */ -mrmc::models::AtomicPropositionsLabeling * readLabFile(int node_count, const char * filename); +mrmc::models::AtomicPropositionsLabeling * readLabFile(uint_fast64_t node_count, const char * filename); } // namespace parser } // namespace mrmc diff --git a/src/parser/readTraFile.cpp b/src/parser/readTraFile.cpp index 7bb653da9..6130c9751 100644 --- a/src/parser/readTraFile.cpp +++ b/src/parser/readTraFile.cpp @@ -33,20 +33,6 @@ namespace mrmc { namespace parser{ -/*! - * Skips all whitespaces and returns new pointer. - * - * @todo should probably be replaced by strspn et.al. - */ -char* skipWS(char* buf) -{ - while(1) - { - if ((buf[0] != ' ') && (buf[0] != '\t') && (buf[0] != '\n') && (buf[0] != '\r')) return buf; - buf++; - } -} - /*! * @brief Perform first pass through the file and obtain number of * non-zero cells and maximum node id. @@ -83,13 +69,13 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) uint_fast32_t row, col; double val; maxnode = 0; - while (1) + while (buf[0] != '\0') { /* * read row and column */ - row = strtol(buf, &buf, 10); - col = strtol(buf, &buf, 10); + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); /* * check if one is larger than the current maximum id */ @@ -102,6 +88,7 @@ static uint_fast32_t makeFirstPass(char* buf, uint_fast32_t &maxnode) val = strtod(buf, &buf); if (val == 0.0) break; if (row == col) non_zero--; + buf = skipWS(buf); } return non_zero; @@ -150,10 +137,10 @@ sparse::StaticSparseMatrix * readTraFile(const char * filename) { * read file header, extract number of states */ buf += 7; // skip "STATES " - strtol(buf, &buf, 10); + checked_strtol(buf, &buf); buf = skipWS(buf); buf += 12; // skip "TRANSITIONS " - strtol(buf, &buf, 10); + checked_strtol(buf, &buf); pantheios::log_DEBUG("Creating matrix with ", pantheios::integer(maxnode + 1), " maxnodes and ", @@ -177,19 +164,16 @@ sparse::StaticSparseMatrix * readTraFile(const char * filename) { while (buf[0] != '\0') { /* - * read row, col and value. if value == 0.0, we have reached the - * end of the file. + * read row, col and value. */ - row = strtol(buf, &buf, 10); - if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format(); - - col = strtol(buf, &buf, 10); - if ((buf[0] != ' ') && (buf[0] != '\t')) throw mrmc::exceptions::wrong_file_format(); - + row = checked_strtol(buf, &buf); + col = checked_strtol(buf, &buf); val = strtod(buf, &buf); - if ((buf[0] != '\n') && (buf[0] != '\r')) throw mrmc::exceptions::wrong_file_format(); - if (val == 0.0) break; + /* + * only values in (0, 1] are meaningful + */ + if ((val <= 0.0) || (val > 1.0)) throw mrmc::exceptions::wrong_file_format(); pantheios::log_DEBUG("Write value ", pantheios::real(val), " to position ",