Finish decls.h and make them the documented function signatures

[sosy-lab]

Finish decls.h and make them the documented function signatures

[PhilippWendler]

I disagree, I think each benchmark file should be a complete C file, including declarations for all used functions. This makes them much easier to use, here and in other contexts.

Also, why can't we allow both signatures of __VERIFIER_assume? Each benchmark could declare and use the one it needs, as long as it does not contradict the written rules.

I am not sure what you mean by "function signatures need implementing". The benchmarks should certainly not provide their own implementations of these functions, these are expected to be defined in the verifier.

[delcypher]

I disagree, I think each benchmark file should be a complete C file, including declarations for all used functions. This makes them much easier to use, here and in other contexts.

But this is massively redundant and a maintenance nightmare. It is good engineering practice to put the declarations of external functions in a header file. It is also very easy to use the decls.h file.

If you are using a compiler as part of your verifier you can just pass -include decls.h or alternatively the verifier just needs to do something like.

$ cat decls.h benchmark.c > benchmark_to_verify.c
$ your_awesome_verifier benchmark_to_verify.c

I think the benefits of having the declarations is one place massively outweigh the minor inconvenience to the verifier.

Also, why can't we allow both signatures of __VERIFIER_assume? Each benchmark could declare and use the one it needs, as long as it does not contradict the written rules.

Because doing so is a compiler error for both gcc and clang

void __VERIFIER_assume(int);
void __VERIFIER_assume(_Bool);

int main() {
    int x;
    __VERIFIER_assume(x > 0);
    return 0;
}

$ gcc -Wall -std=c99 svcomp_decl_test.c 
svcomp_decl_test.c:2:6: error: conflicting types for ‘__VERIFIER_assume’
 void __VERIFIER_assume(_Bool);
      ^
svcomp_decl_test.c:1:6: note: previous declaration of ‘__VERIFIER_assume’ was here
 void __VERIFIER_assume(int);
      ^

$ clang -Wall -std=c99 svcomp_decl_test.c 
svcomp_decl_test.c:2:6: error: conflicting types for '__VERIFIER_assume'
void __VERIFIER_assume(_Bool);
     ^
svcomp_decl_test.c:1:6: note: previous declaration is here
void __VERIFIER_assume(int);
     ^
1 error generated.

In my opinion verifying benchmarks that could never be run (because they can't be compiled) is completely pointless, therefore it must be possible to actually compile the benchmarks.

I am not sure what you mean by "function signatures need implementing". The benchmarks should certainly not provide their own implementations of these functions, these are expected to be defined in the verifier.

Sorry I wasn't being very precise there. What I meant was that every __VERIFIER_* function that is the existing documentation for SV-COMP should be declared in decls.h.

[PhilippWendler]

I disagree, I think each benchmark file should be a complete C file, including declarations for all used functions. This makes them much easier to use, here and in other contexts.

But this is massively redundant and a maintenance nightmare. It is good engineering practice to put the declarations of external functions in a header file. It is also very easy to use the decls.h file.

I think the benefit of having each benchmark as a single compilable self-contained file outweighs this. You have worked a lot into this direction (thanks!), so why stop here and change the current SV-Comp rules and remove code from the files such that currently-compiling benchmarks will no longer compile without an explicitly given additional file? Imagine people finding this benchmark repository and taking source files for their own project, won't the first thing the complain about that all of our files are invalid C because they reference undeclared functions?

Regarding the "massively redundant": Much more redundant is that we have all files pre-processed, which means than many of them contain massive amounts of code from the standard header files, much more than the few lines we are talking about here. And yet this is necessary because content of header files may be different depending on the system and we want to have benchmarks without specific external dependencies.

I also think this won't be a maintenance nightmare. Once we have added all relevant function declarations, why should the benchmark need to be changed again in that regard? On the contrary, I would think that having the declarations in a separate file would create maintenance problems, because as soon as you change decls.h you need to make sure not to introduce anything that would be incompatible to existing benchmarks.

It is not clear to me whether you think that every verifier should contain decls.h and automatically add it to the source code, or whether it would be given as separate file on the command line. Both would be problematic.
On one hand, if the verifier includes decls.h and concats it to the source code this might make the verifier incompatible with non-SV-Comp benchmarks. Worse, now there will be a big maintenance nightmare because every verifier will need to include and update this file. If there is a change (e.g., a newly added function), we won't be able to verify next year's benchmarks with this year's verifiers for comparison, just because the verifier lacks the new decls.h.
On the other hand, if we decide to pass both the real source file and decls.h on the command line, every verifier needs to be changed to allow multiple source files to be given at once (I believe the number of verifiers supporting this already is minimal). We would also need to define that multiple source files passed on the command line need to be concatenated, which differs from the usual semantics of tools that can be passed multiple files at the same time (e.g., a compiler). Concatenating arbitrary C source files may produce invalid source code, so adding this feature to a verifier might be unwanted by some teams (for example CPAchecker already accepts multiple C files but treats them as separate translation units that are linked together like a compiler would do).

Also, why can't we allow both signatures of __VERIFIER_assume? Each benchmark could declare and use the one it needs, as long as it does not contradict the written rules.

Because doing so is a compiler error for both gcc and clang

Please do not assume I am proposing to have non-compilable benchmarks.
Allowing both signatures of __VERIFIER_assume is only a problem because you want to have these definitions in decls.h. If we continue the current style to have the necessary declarations in each source file, one source file could without problems use the int version whereas another source file can use the _Bool version.

[dbeyer]

Hello,

A C program file for an SV-COMP verification task must be a readily pre-processed, complete, single-file piece of C program code.

I apologize for having merged the decls.h into the repository. I unfortunately did not understand the plan about this.

decls.h must not be used for the competition; each verification task must be self-contained.

Best regards and sorry for the confusion that my misunderstanding and my merge has caused,
Dirk

On 15-10-15 01:21 PM, Philipp Wendler wrote:

    I disagree, I think each benchmark file should be a complete C file, including declarations for all used functions. This makes them much easier to use, here and in other contexts.

But this is massively redundant and a maintenance nightmare. It is good engineering practice to put the declarations of external functions in a header file. It is also very easy to use the decls.h file.

I think the benefit of having each benchmark as a single compilable self-contained file outweighs this. You have worked a lot into this direction (thanks!), so why stop here and change the current SV-Comp rules and remove code from the files such that currently-compiling benchmarks will no longer compile without an explicitly given additional file? Imagine people finding this benchmark repository and taking source files for their own project, won't the first thing the complain about that all of our files are invalid C because they reference undeclared functions?

Regarding the "massively redundant": Much more redundant is that we have all files pre-processed, which means than many of them contain massive amounts of code from the standard header files, much more than the few lines we are talking about here. And yet this is necessary because content of header files may be different depending on the system and we want to have benchmarks without specific external dependencies.

I also think this won't be a maintenance nightmare. Once we have added all relevant function declarations, why should the benchmark need to be changed again in that regard? On the contrary, I would think that having the declarations in a separate file would create maintenance problems, because as soon as you change decls.h you need to make sure not to introduce anything that would be incompatible to existing benchmarks.

It is not clear to me whether you think that every verifier should contain |decls.h| and automatically add it to the source code, or whether it would be given as separate file on the command line. Both would be problematic.
On one hand, if the verifier includes |decls.h| and concats it to the source code this might make the verifier incompatible with non-SV-Comp benchmarks. Worse, now there will be a big maintenance nightmare because every verifier will need to include and update this file. If there is a change (e.g., a newly added function), we won't be able to verify next year's benchmarks with this year's verifiers for comparison, just because the verifier lacks the new |decls.h|.
On the other hand, if we decide to pass both the real source file and |decls.h| on the command line, every verifier needs to be changed to allow multiple source files to be given at once (I believe the number of verifiers supporting this already is minimal). We would also need to define that multiple source files passed on the command line need to be concatenated, which differs from the usual semantics of tools that can be passed multiple files at the same time (e.g., a compiler). Concatenating arbitrary C source files may produce invalid source code, so adding this feature to a verifier might be unwanted by some teams (for example CPAchecker already accepts multiple C files but treats them as separate translation units that are linked together like a compiler would do).

    Also, why can't we allow both signatures of __VERIFIER_assume? Each benchmark could declare and use the one it needs, as long as it does not contradict the written rules.

Because doing so is a compiler error for both gcc and clang

Please do not assume I am proposing to have non-compilable benchmarks.
Allowing both signatures of |__VERIFIER_assume| is only a problem because you want to have these definitions in |decls.h|. If we continue the current style to have the necessary declarations in each source file, one source file could without problems use the |int| version whereas another source file can use the |_Bool| version.

—
Reply to this email directly or view it on GitHub #55 (comment).

[delcypher]

I think the benefit of having each benchmark as a single compilable self-contained file outweighs this. You have worked a lot into this direction (thanks!), so why stop here and change the current SV-Comp rules and remove code from the files such that currently-compiling benchmarks will no longer compile without an explicitly given additional file? Imagine people finding this benchmark repository and taking source files for their own project, won't the first thing the complain about that all of our files are invalid C because they reference undeclared functions?

Oh, actually the current build system passes -include $(ROOT_DIR)/decls.h to the compiler. I'm not sure if compilation will succeed without it. I haven't tried. I did this because @tautschnig 's check script was doing this.

I also think this won't be a maintenance nightmare. Once we have added all relevant function declarations, why should the benchmark need to be changed again in that regard? On the contrary, I would think that having the declarations in a separate file would create maintenance problems, because as soon as you change decls.h you need to make sure not to introduce anything that would be incompatible to existing benchmarks.

I suppose if you never plan to change the signatures then I guess this is fine. I personally don't like it but I'm not in charge so I don't get to decide.
@dbeyer has made it clear the the *.c or *.i files must be standalone.

On one hand, if the verifier includes decls.h and concats it to the source code this might make the verifier incompatible with non-SV-Comp benchmarks. I should have been more precise. I meant something like

$ cat decls.h <(echo "#line 1") benchmark.c > benchmark_to_verify.c
$ your_awesome_verifier benchmark_to_verify.c

i.e. it emulates what the -include option does in gcc and clang.

Worse, now there will be a big maintenance nightmare because every verifier will need to include and update this file. If there is a change (e.g., a newly added function), we won't be able to verify next year's benchmarks with this year's verifiers for comparison, just because the verifier lacks the new decls.h.

I actually expected that the verifier not keep a copy of this file and instead have it provided to it when it receives the benchmark to verify. I guess this would be a change to the current behaviour.

Looks like I'm not going to be allowed to remove the __VERIFIER_* declarations from the source but there are still some points to address.

• I think the type of the argument passed to __VERIFIER_assume() should be _Bool not int. Although we could have two I think it's a bad idea that just makes things confusing.
• What do you want to do with decls.h?

On a related note it just occurred to me... When you give a verifier an anonymized benchmark do they also get given the set compiler flags that would be needed compile it? If not this seems rather unfair because it seems that different flags are needed for different benchmarks

• Some require -std=gnu99 rather than -std=c99
• Some require -m32, some others do not
• Some require defines (e.g. -DNR=1 -DITERATIONS=2)

[PhilippWendler]

Oh, actually the current build system passes -include $(ROOT_DIR)/decls.h to the compiler. I'm not sure if compilation will succeed without it. I haven't tried.

Well, this should be easy to try and easy to fix. I already fixed these issues in many benchmarks in the past.

• I think the type of the argument passed to __VERIFIER_assume() should be _Bool not int. Although we could have two I think it's a bad idea that just makes things confusing.

I would consider that orthogonal to the current issue and discuss it separately.

• What do you want to do with decls.h?

I guess as soon as the build system is fixed and the check script is removed we can delete it.

On a related note it just occurred to me... When you give a verifier an anonymized benchmark do they also get given the set compiler flags that would be needed compile it? If not this seems rather unfair because it seems that different flags are needed for different benchmarks

• Some require -std=gnu99 rather than -std=c99
• Some require -m32, some others do not

This is defined in the rules. You can get a parameter passed for the machine model and the memory model, but not for anything else.

So far, this never seemed a problem. Shouldn't all benchmarks compile with -std=gnu99? Is there really something that is legal in c99 that is illegal in gnu99? Our tool works fine with parsing everything as GNU C code.

• Some require defines (e.g. -DNR=1 -DITERATIONS=2)

I would consider this a bug and ask the author for a fix (declare these as global variables, either constant or non-deterministically initialized).

[PhilippWendler]

I am closing this because -include decls.h is gone and so the main problem does not exist anymore. Separate issues should be created for other problems if they still exist.