Programs with Nonlinear Properties

[nguyenthanhvuh]

Added programs with nonlinear polynomial invariants in c/nla-digbench.

• [x ] programs added to new and appropriately named directory

• [x ] license present and acceptable (either in separate file or as comment at beginning of program)

• [x ] contributed-by present (either in README file or as comment at beginning of program)

• programs added to a .set file of an existing category, or new sub-category established (if justified)

• intended property matches the corresponding .prp file

• expected answer in file names according to convention

• architecture (32 bit vs. 64 bit) matches the corresponding .cfg file
• original sources present
• preprocessed files present
• preprocessed files generated with correct architecture
• Makefile added with correct content and without overly broad suppression of warnings

[dbeyer]

The CI check complains that there is no license file.
Could you please rename LICSENSE.txt to LICENSE.txt?

[dbeyer]

The task definitions are missing: Please have a look at Section Task Definitions
https://github.com/sosy-lab/sv-benchmarks/blob/master/README.md#task-definitions

[PhilippWendler]

For task-definition files, I guess most of them would look like this (foo.yml for foo.c):

format_version: '1.0'
input_files: 'foo.c'
properties:
  - property_file: ../properties/unreach-call.prp
    expected_verdict: ...

Leave out expected_verdict if you don't know it.
You can also consider adding other properties like termination, no-overflows, etc. if you consider them interesting for your programs.

[nguyenthanhvuh]

On Jun 7, 2019, at 2:02 AM, Philipp Wendler ***@***.***> wrote: @PhilippWendler commented on this pull request. For task-definition files, I guess most of them would look like this (foo.yml for foo.c): format_version: '1.0' input_files: 'foo.c' properties: - property_file: ../properties/unreach-call.prp expected_verdict: …

If the assertion is true then I should use expected_verdict: true, right ? I believe I can prove most of these by hand, but I don’t think there are existing tools to automatically prove them yet. Should I still put in expected verdicts then ? Also, should I add these programs to an existing or a new a new category (.set and .cfg files) ? When I am done making and committing the changes, do I create a new pull request ? Thanks,

…

Leave out expected_verdict if you don't know it. You can also consider adding other properties like termination, no-overflows, etc. if you consider them interesting for your programs. In c/nla-digbench/LICSENSE.txt: > @@ -0,0 +1,202 @@ + The license file could be replaced by a symlink to the Apache license in the root directory. In c/nla-digbench/Makefile: > @@ -0,0 +1,3 @@ +LEVEL := ../ +IGNORE_DIRS := ./cannotverify ./done What is cannotverify and done? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[nguyenthanhvuh]

Hi Dirk and Phillip, I've fixed the License and Task definition issues. I've also added a comment to the pull request for additional questions. Please take a look when you have time. Thanks ! On Fri, Jun 7, 2019 at 10:37 AM ThanhVu (Vu) Nguyen <nguyenthanhvuh@gmail.com> wrote:

…

> On Jun 7, 2019, at 2:02 AM, Philipp Wendler ***@***.***> wrote: > > @PhilippWendler commented on this pull request. > > For task-definition files, I guess most of them would look like this (foo.yml for foo.c): > > format_version: '1.0' > input_files: 'foo.c' > properties: > - property_file: ../properties/unreach-call.prp > expected_verdict: … If the assertion is true then I should use expected_verdict: true, right ? I believe I can prove most of these by hand, but I don’t think there are existing tools to automatically prove them yet. Should I still put in expected verdicts then ? When I am done making and committing the changes, do I create a new pull request ? Thanks, > > Leave out expected_verdict if you don't know it. > You can also consider adding other properties like termination, no-overflows, etc. if you consider them interesting for your programs. > > In c/nla-digbench/LICSENSE.txt: > > > @@ -0,0 +1,202 @@ > + > > The license file could be replaced by a symlink to the Apache license in the root directory. > > In c/nla-digbench/Makefile: > > > @@ -0,0 +1,3 @@ > +LEVEL := ../ > +IGNORE_DIRS := ./cannotverify ./done > > What is cannotverify and done? > > — > You are receiving this because you authored the thread. > Reply to this email directly, view it on GitHub, or mute the thread. >

[PhilippWendler]

If the assertion is true then I should use expected_verdict: true, right ? I believe I can prove most of these by hand, but I don’t think there are existing tools to automatically prove them yet. Should I still put in expected verdicts then ?

I would say yes.

Also, should I add these programs to an existing or a new a new category (.set and .cfg files) ?

Usually it is better to use an existing category, if there is one that fits. I guess ReachSafety-Loops.set would be a good category?

When I am done making and committing the changes, do I create a new pull request ?

No, please just update this pull request (as you have already done).

[nguyenthanhvuh]

Update branch with expected properties and add files to ReachSafety-Loops.set

[nguyenthanhvuh]

Looks like the latest update passes all the checks. Ready for review now.

[PhilippWendler]

Looks good.

I suggest to do a "Squash and Merge" because this PR contains a lot of individual commits.

[nguyenthanhvuh]

There's a message above saying that I "dismissed PhilippWendler’s stale review via 2815e06 10 hours ago". Not sure what that means. I did make some small edits to the README.md.

[nguyenthanhvuh]

Hi, anything that might block this from being pulled ?

[PhilippWendler]

Squash merge suggested.

[nguyenthanhvuh]

Hi, just want to check the status of this PR.

[PhilippWendler]

The file knuth.c includes math.h, this needs to be removed.

[nguyenthanhvuh]

Thanks Phillipp. 'knuth.c' requires the sqrt function from math.h. Any suggestion on how to replace sqrt with? If not I can remove knuth.c from the directory.

[PhilippWendler]

Just provide an extern declaration of the sqrt function as declared in the header. You could also preprocess the file (which leads to inlining the complete header), but in this case I guess adding the single declaration is easier.

[nguyenthanhvuh]

done, and push the changes to my github repo. can you reuse the old PR (which was already merged) or should I create a new PR?

…

On Aug 21, 2019, at 10:42 AM, Philipp Wendler ***@***.***> wrote: Just provide an extern declaration of the sqrt function as declared in the header. You could also preprocess the file (which leads to inlining the complete header), but in this case I guess adding the single declaration is easier. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub, or mute the thread.

[PhilippWendler]

One cannot merge a PR twice, you need a new PR.

[MartinSpiessl]

There seem to be overflows in the tasks, e.g. divbin.c in line 30.

[dbeyer]

@nguyenthanhvuh Could you please submit a new pull request?
Best is two:

• one for fixing the preprocessing
• one fixing the overflows (and leave the originals: they are perhaps good tests for overflow checking)

[dbeyer]

I wonder if this should become a new sub category.
The tasks require a certain powerful technology.
For the other tasks that require non-linear arithmetic, we had created a new sub-category "bitvectors".
The tasks here are also non-linear, but of a special type: polynomial.

[dbeyer]

@nguyenthanhvuh Could you please add to the README a small paragraph that briefly describes the kind of non-linearity? I.e., they invariants are polynomials. This would be good to know in order to understand that these tasks are very different from the other tasks with non-linear arithmetic.
I would even suggest to rename the directory from "nla" to "polynomial" or so.

[nguyenthanhvuh]

Hi, thanks. I will work on it this weekend.

• Regarding to the overflows, could you provide some suggestions on how to fix them ? Thanks.

• For the README, I've added something like this :
  These programs contain nonlinear polynomial properties (mostly equalities) that are challenging for program analysis. For example, program cohendiv.c has the loop invariants such as b == ya and x == qy + r where x,q,y,r,a are int variables. Let me know if that looks ok.

• About becoming new sub category: that might be a good idea to have a polynomial nonlinear pros category. But It's up to you. I'll do what you think is best.

[dbeyer]

(Just for the book-keeping: This PR addresses issue #796, which can now get closed.)

[dbeyer]

@nguyenthanhvuh Could you please start a new pull request (or two of them), such that we can track the discussion there, instead of under this already closed PR?

Yes, what you plan to write to the README sound nice!

I can take care of the new sub-category later.

[nguyenthanhvuh]

done, create new PR here #815.

…

On Sep 23, 2019, at 12:14 PM, Dirk Beyer ***@***.***> wrote: @nguyenthanhvuh Could you please start a new pull request (or two of them), such that we can track the discussion there, instead of under this already closed PR? Yes, what you plan to write to the README sound nice! I can take care of the new sub-category later. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.