Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[issue1146] Validate SAS file #227

Draft
wants to merge 8 commits into
base: main
Choose a base branch
from

Conversation

tanjaschindler
Copy link

No description provided.

Copy link
Member

@FlorianPommerening FlorianPommerening left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had a look at the code. I don't know the list of things this should check so I didn't verify completeness.

void confirm_end_of_file();
// TODO: Should this be public at all? Or should we add a get_line method?
void error(const std::string &message) const;
private:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be together with the other private members at the top of the class (with an implicit private: rather than an explicit one).

bool may_start_line = true;
const std::regex only_whitespaces;
public:
explicit InputFileParser(std::istream &stream);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Since the parser takes a stream and not a file stream, would it make sense to drop File from the name? Maybe instead describe the functionality better, for example LineInputParser?

const std::regex only_whitespaces;
public:
explicit InputFileParser(std::istream &stream);
~InputFileParser();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We typically leave out default destructors.

/*
Set context for error reporting.
*/
void set_context(const std::string &context);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure if this is still relevant, but we have classes for the command line parsing that do something similar (for example SyntaxAnalyzerContext, DecorateContext, and ConstructContext, they are different private classes for different use cases but all parallel code). They have an advantage over setting the context manually because they leave the context once they go out of scope. This way you can produce error messages with a stack trace of contexts.

One suggestion would be to use a similar design here, another (more complicated) option would be to extract the common functionality.

void set_context(const std::string &context);
/*
Read a single token within a line. Tokens within a line are
separated by arbitrary whitespaces. Set curser to the end of the
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
separated by arbitrary whitespaces. Set curser to the end of the
separated by arbitrary whitespaces. Set cursor to the end of the

int num_facts = file_parser.read_line_int("number of facts in mutex group");
if (num_facts < 1) {
file_parser.error("Number of facts in mutex group is less than 1, should be at least 1.");
}
vector<FactPair> invariant_group;
invariant_group.reserve(num_facts);
for (int j = 0; j < num_facts; ++j) {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Don't we already have a function that reads a list of facts? And doesn't it also need the check that there are no duplicate facts?

const vector<ExplicitVariable> &variables) {
int count;
in >> count;
in.set_context(is_axiom ? "axiom section" : "operator section");
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You could use a single if ... else ... here instead of two ?-operators.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

that would be

int count;
if (is_axiom) {
    in.set_context("axiom section");
    count = in.read_line_int("number of axioms");
} else {
    in.set_context("operator section");
    count = in.read_line_int("number of operators");
} 

It is only personal preference but I like the variant with the ? operator more. In my opinion it emphasizes the idea of setting the context first and reading the number afterwards with slight changes of the string parameter if the is_axiom flag is true.
? also requires no declaration of count with later assignment.

read_and_verify_version(in);
bool use_metric = read_metric(in);
variables = read_variables(in);
utils::InputFileParser file(in);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't have to be a file. How about parser?


// TODO: Maybe we could move this into a separate function as well
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

sounds good

axioms = read_actions(in, true, use_metric, variables);
operators = read_actions(file, false, use_metric, variables);
axioms = read_actions(file, true, use_metric, variables);
file.confirm_end_of_file();
/* TODO: We should be stricter here and verify that we
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The TODO is fixed now.

ExplicitOperator(istream &in, bool is_an_axiom, bool use_metric);
void read_pre_post(utils::InputFileParser &in);
void read_axiom(utils::InputFileParser &in);
ExplicitOperator(utils::InputFileParser &in, bool is_an_axiom, bool use_metric);
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

InputFileParser is called file_parser at other places. I would prefer it to be called file_parser instead of in here (and at other places), too.

vector<FactPair> conditions = read_facts(in);
int var, value_pre, value_post;
in >> var >> value_pre >> value_post;
void ExplicitOperator::read_axiom(utils::InputFileParser &in) {
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you might want to add a flag to indicate axiom or pre_post as the read_axiom and read_pre_post are exactly the same besides the boolean flag in the read_facts call and the string in the assignment of var (and the order of the confirm_end_of_line, precondition.emplace_back which should be the same both ways).

in >> version;
check_magic(in, "end_version");
static void read_and_verify_version(utils::InputFileParser &in) {
in.set_context("version section");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

you sometimes use spaces and other times use _ in the context string.
this should be consistent.

const vector<ExplicitVariable> &variables) {
int count;
in >> count;
in.set_context(is_axiom ? "axiom section" : "operator section");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

that would be

int count;
if (is_axiom) {
    in.set_context("axiom section");
    count = in.read_line_int("number of axioms");
} else {
    in.set_context("operator section");
    count = in.read_line_int("number of operators");
} 

It is only personal preference but I like the variant with the ? operator more. In my opinion it emphasizes the idea of setting the context first and reading the number afterwards with slight changes of the string parameter if the is_axiom flag is true.
? also requires no declaration of count with later assignment.

separated by arbitrary whitespaces. Set curser to the end of the
read token.
*/
std::string read(const std::string &message); // TODO: templates
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

combining read and read_int into one templated function to call
read<string> and read<int> instead.

Read a complete line as a single string. Set cursor to the
beginning of the next line.
*/
std::string read_line(const std::string &message); // TODO: templates
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The docu comment should add a sentence like Requires cursor to be at the beginning of the current line.

std::string line;
std::vector<std::string> tokens;
bool may_start_line = true;
const std::regex only_whitespaces;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
const std::regex only_whitespaces;
constexpr std::regex only_whitespaces = "\\s*";

and remove it from the constructor.

getline(stream, next_line);
++line_number;
if (!regex_match(next_line, only_whitespaces)) {
return next_line;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

find_next_line changes line_number as side effect but returns a string that is used to change line every time (except in confirm_end_of_file but would fit to do it there, too)
You could make the change of the field line a side effect there, too. This would make it a void function where it is more clear that all effects are side effects.

if(next_line != "") {
error("Expected end of file, found non-empty line " + next_line);
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
}
void InputFileParser::confirm_end_of_file() {
assert(may_start_line);
if (!stream.eof()) {
line = find_next_line();
error("Expected end of file, found non-empty line " + line);
}

this would also remove the need of a bool flag in find_next_line.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants