Improve compilation checks

[PhilippWendler]

It would be good to improve the compilation checks that are executed for all benchmarks:

• Read architecture of files from official Category.cfg task-definition files instead of Makefile to avoid the need to specify it twice.
• New files and directories should be picked up automatically, without need to explicitly list them in another file.
• Do not abort on first error, but show all errors.
• Enable all warnings and treat them as errors by default, but allow to silence certain warnings per directory.

I keep wondering whether the existing Makefile-based system is a good fit for this. The Makefile syntax is very hard to read (especially Makefile.rules) and I would have no idea how to implement these features. @delcypher how could this be done?

[delcypher]

@PhilippWendler

The Category.cfg files did not exist when the build system was written. If they did I may have tried using them. I don't consider the current build system to be particularly good however everything you list is probably possible.

Repository meta-data organisation

However I feel compelled to point out I'm not happy with the Category.cfg file (or any of the other files that describe the verification tasks for that matter). When organising benchmarks you have a choice, have a single file describe everything about a benchmark (which is what I went for when I made the sv-comp mock up) or distribute this information across multiple files (what the repository currently does). Both choices have their advantages/disadvantages.

The single file describing everything about a benchmark (the spec.yml file in my mock up) has the following advantages:

• Easy for the build system to build the benchmark because it does not need to traverse and process lots of files to work out what to do. This not only faster but also much simpler.
• The same (as above) applies to verifiers wanting to verify the benchmark.
• It makes it very easy to specify multiple properties and their correctness for a benchmark.
• It makes the repository more modular (i.e. you can take any sub-directory and that on its own is a valid benchmark repository that can be built and verified).

It has the following disadvantages:

• It introduces some wasted space. For example is my mock-up every spec.yml file has to specify what categories a benchmark belongs to. This uses up more disk space than the *.set files do.
• It is harder to gain aggregate statistics (e.g. "How many benchmarks are in category X?", "How many benchmarks as expected to be correct?") because every spec.yml file has to be loaded into to memory.

The multiple file approach has the following advantages:

• Easier to gain aggregate statistics because there are less files to parse
• This representation of benchmark information is more compact.

it has the following disadvantages:

• Harder for the build system to work out how to build the benchmarks because multiple files need to be traversed and loaded and parsed.
• The same (as above) applies to verifiers.
• Not modular.

There is a trade off here but I consider the single file (per benchmark) approach to be better. The weakness of gathering statistics can be solved by having additional scripts to traverse the repository and gather the needed information. The modular nature of this organisation is also quite nice because you can pass the script a sub directory of the repository and it will gather statistics only for that sub directory.

Whatever choice is made it is important that metadata be machine readable. Although the Category.cfg file kind of looks like YAML, there's no schema that documents the format and allows it to be easily read by a machine.

This is why the mock up I had provided a versioned (for doing upgrades) schema for the spec.yml files.

Given the current organisation I wouldn't want to hook the build system up to it.

Other issues

New files and directories should be picked up automatically, without need to explicitly list them in another file.

That is a fairly straight forward change to make. It requires changing how directory traversal works in Makefile.rules. Right now source files are found implicitly but directories must be listed explicitly. The change would be to make directory traversal behave similarly to source file traversal.

Do not abort on first error, but show all errors.

I think just doing make --ignore-errors might do that. I'm not sure if it would finally exit with a non-zero exit code if there was a problem though.

Enable all warnings and treat them as errors by default, but allow to silence certain warnings per directory.

This is do-able today by modifying the relevant Makefile in a directory where you want to change which warnings are used. Here's an example

LEVEL := ../

include $(LEVEL)/Makefile.config

# Filter out a warning. It's important that this come after the include $(LEVEL)/Makefile.config
CC.Warnings := $(filter-out -Wsome-warning,$(CC.Warnings))
CC.WarningsAsErrors := $(filter-out -Wsome-warning,$(CC.WarningsAsErrors))

# Note doing this below has the same effect although it is more error prone as you might accidently
# filter out non warning flags if the arguments to the `filter-out` function are wrong.
CC.Flags := $(filter-out -Wsome-warning,$(CC.Flags))

[PhilippWendler]

@delcypher Many thanks for your response!

However I feel compelled to point out I'm not happy with the Category.cfg file (or any of the other files that describe the verification tasks for that matter). When organising benchmarks you have a choice, have a single file describe everything about a benchmark (which is what I went for when I made the sv-comp mock up) or distribute this information across multiple files (what the repository currently does). Both choices have their advantages/disadvantages.

This is probably a topic for a different issue, I just want to give a single comment:

The single file describing everything about a benchmark (the spec.yml file in my mock up) has the following advantages:

• Easy for the build system to build the benchmark because it does not need to traverse and process lots of files to work out what to do. This not only faster but also much simpler.
• The same (as above) applies to verifiers wanting to verify the benchmark.

The build system is the least important consumer of these metadata. Other people that want to use these tasks for benchmarking are the ones for who we should make it as easy as possible.
Verifiers that want to verify a task are no direct consumers at all, they won't see these files anyway but will be only passed the pieces they need to know (e.g., architecture and property but not expected verdict obviously).

The current structure is mostly motivated by the fact that it is trivial to use in all sorts of scripts.

This does not mean that it cannot and should not be improved, but we need to take into account what the important goals are, and we should discuss this in another issue.

Whatever choice is made it is important that metadata be machine readable. Although the Category.cfg file kind of looks like YAML, there's no schema that documents the format and allows it to be easily read by a machine.

Yes it intended to be YAML. A schema would be good to have and will probably be written when the format is more stable, but machines can already read it as it is (check.py already uses it).

New files and directories should be picked up automatically, without need to explicitly list them in another file.

That is a fairly straight forward change to make. It requires changing how directory traversal works in Makefile.rules. Right now source files are found implicitly but directories must be listed explicitly. The change would be to make directory traversal behave similarly to source file traversal.

That would be great. I have no idea how to do this with the current set of Makefiles, though. It would be great if you could create a PR?

Do not abort on first error, but show all errors.

I think just doing make --ignore-errors might do that. I'm not sure if it would finally exit with a non-zero exit code if there was a problem though.

Ok, I will experiment with this.

Enable all warnings and treat them as errors by default, but allow to silence certain warnings per directory.

This is do-able today by modifying the relevant Makefile in a directory where you want to change which warnings are used. Here's an example

LEVEL := ../

include $(LEVEL)/Makefile.config

# Filter out a warning. It's important that this come after the include $(LEVEL)/Makefile.config
CC.Warnings := $(filter-out -Wsome-warning,$(CC.Warnings))
CC.WarningsAsErrors := $(filter-out -Wsome-warning,$(CC.WarningsAsErrors))

The example would be great, but you mentioned recently that WARNINGS_AS_ERRORS is not compatible with SUPPRESS_WARNINGS, which is required by the Travis build. So I fear enabling it would break the Travis build?

[dbeyer]

@PhilippWendler Thanks for the detailed answers and explanations, which fully match my intentions.

@delcypher When I introduced the new structure with the .prp and .cfg files, I had two goals in mind:

• keep it as simple as possible for users of the repository of verification tasks
• focus on the current set of requirements

I do not work according to Waterfall process model, more like Scrum.
The current format implements everything I need for the current sprint.
The current setup is flexible to allow future extensions, but I should not worry about more right now.

More will be added to those files when I start setting up the demo category on no-preprocessing, i.e., the next "sprint"
(most likely not this year, perhaps in January).

Best,
Dirk

On 2016-11-07 09:13 PM, Philipp Wendler wrote:

@delcypher https://github.com/delcypher Many thanks for your response!

However I feel compelled to point out I'm not happy with the Category.cfg file (or any of the other files that describe the verification
tasks for that matter). When organising benchmarks you have a choice, have a single file describe everything about a benchmark (which is
what I went for when I made the sv-comp mock up) or distribute this information across multiple files (what the repository currently does).
Both choices have their advantages/disadvantages.

This is probably a topic for a different issue, I just want to give a single comment:

The single file describing everything about a benchmark (the spec.yml file in my mock up) has the following advantages:

  * Easy for the build system to build the benchmark because it does not need to traverse and process lots of files to work out what to do.
    This not only faster but also much simpler.
  * The same (as above) applies to verifiers wanting to verify the benchmark.

The build system is the least important consumer of these metadata. Other people that want to use these tasks for benchmarking are the ones for
who we should make it as easy as possible.
Verifiers that want to verify a task are /no/ direct consumers at all, they won't see these files anyway but will be only passed the pieces they
need to know (e.g., architecture and property but not expected verdict obviously).

The current structure is mostly motivated by the fact that it is trivial to use in all sorts of scripts.

This does not mean that it cannot and should not be improved, but we need to take into account what the important goals are, and we should
discuss this in another issue.

Whatever choice is made it is important that metadata be machine readable. Although the Category.cfg file kind of looks like YAML, there's
no schema that documents the format and allows it to be easily read by a machine.

Yes it intended to be YAML. A schema would be good to have and will probably be written when the format is more stable, but machines can already
read it as it is (|check.py| already uses it).

    New files and directories should be picked up automatically, without need to explicitly list them in another file.

That is a fairly straight forward change to make. It requires changing how directory traversal works in Makefile.rules. Right now source
files are found implicitly but directories must be listed explicitly. The change would be to make directory traversal behave similarly to
source file traversal.

That would be great. I have no idea how to do this with the current set of Makefiles, though. It would be great if you could create a PR?

    Do not abort on first error, but show all errors.

I think just doing make --ignore-errors might do that. I'm not sure if it would finally exit with a non-zero exit code if there was a
problem though.

Ok, I will experiment with this.

    Enable all warnings and treat them as errors by default, but allow to silence certain warnings per directory.

This is do-able today by modifying the relevant Makefile in a directory where you want to change which warnings are used. Here's an example

|LEVEL := ../ include $(LEVEL)/Makefile.config # Filter out a warning. It's important that this come after the include
$(LEVEL)/Makefile.config CC.Warnings := $(filter-out -Wsome-warning,$(CC.Warnings)) CC.WarningsAsErrors := $(filter-out
-Wsome-warning,$(CC.WarningsAsErrors)) |

The example would be great, but you mentioned recently that |WARNINGS_AS_ERRORS| is not compatible with |SUPPRESS_WARNINGS|, which is required
by the Travis build. So I fear enabling it would break the Travis build?

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub #194 (comment), or mute the
thread https://github.com/notifications/unsubscribe-auth/ACzgUDcq9cBdEGg4JFvW39t5mVjhCOeOks5q74ZMgaJpZM4Kq6uz.

[delcypher]

@PhilippWendler

The build system is the least important consumer of these metadata. Other people that want to use these tasks for benchmarking are the ones for who we should make it as easy as possible.
Verifiers that want to verify a task are no direct consumers at all, they won't see these files anyway but will be only passed the pieces they need to know (e.g., architecture and property but not expected verdict obviously).

I've create #213 for this. But I don't agree with "Verifiers that want to verify a task are no direct consumers at all". If you want the benchmark suite to be useful outside of SV-COMP (which I think you or @dbeyer mentioned as a goal at some point) then focusing only what the SV-COMP verifiers will see is the wrong approach. The repository meta-data as it is right now is not very convenient to work with directly.

New files and directories should be picked up automatically, without need to explicitly list them in another file.
That is a fairly straight forward change to make. It requires changing how directory traversal works in Makefile.rules. Right now source files are found implicitly but directories must be listed explicitly. The change would be to make directory traversal behave similarly to source file traversal.

That would be great. I have no idea how to do this with the current set of Makefiles, though. It would be great if you could create a PR?

I've made a PR (#212).