Merge pull request #1191 from MartinSpiessl/zilu-fix

Zilu fix

Author: dbeyer

.reuse/dep5

@@ -92,6 +92,7 @@ Files:
  c/loop-lit
  c/loop-new
  c/loop-simple
+ c/loop-zilu
  c/loops-crafted-1
  c/memory-alloca
  c/memsafety

c/NoOverflows-Other.set

@@ -3,3 +3,4 @@ recursive/*.yml
 recursive-simple/*.yml
 bitvector/*.yml
 psyco/*.yml
+loop-zilu/*.yml

c/ReachSafety-Loops.set

@@ -9,6 +9,7 @@ loop-industry-pattern/*.yml
 loops-crafted-1/*.yml
 loop-invariants/*.yml
 loop-simple/*.yml
+loop-zilu/*.yml
 verifythis/duplets.yml
 verifythis/elimination_max.yml
 verifythis/lcp.yml

c/loop-zilu/LICENSE.GPLv2.txt

@@ -0,0 +1 @@
+../../LICENSE.GPLv2.txt

c/loop-zilu/Makefile

@@ -0,0 +1,3 @@
+LEVEL := ../
+
+include $(LEVEL)/Makefile.config

c/loop-zilu/README.txt

@@ -0,0 +1,39 @@
+These tasks were generated by Martin Spiessl
+from information in the tool repository of zilu,
+a tool for invariant generation throug selective sampling,
+which is described in the following publication:
+
+Li, J., Sun, J., Li, L., Le, Q. L., & Lin, S. W. (2017, October).
+Automatic loop-invariant generation anc refinement through selective sampling.
+In 2017 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE) (pp. 782-792). IEEE.
+
+These tasks represent the 53 benchmarks
+that are listed in table 1 in this publication.
+
+The original repository for zilu was at (according to the paper):
+https://github.com/lijiaying/zilu
+
+It seems this repository was deleted or set to private.
+The original repository was published unter GPL-2.0,
+a copy I made can be found at:
+https://github.com/MartinSpiessl/zilu
+
+So I supply these tasks unter GPL-2.0 as well.
+
+The paper mentions that the tasks were collected
+from various papers/sources, one of them being SV-COMP.
+It is not easy to identify which tasks were taken from which source,
+and the authors state many of the SV-COMP tasks had to be excluded anyway
+because they were too complicated/ out of scope.
+Also the tasks are written down in a simplified format
+in the zilu repository in special files with the extension "cfg".
+
+I did the translation into SV-COMP compliant tasks
+myself with a small python script.
+Due to these 2 transformations,
+I do not believe that the tasks contain
+any copyrightable material anymore
+from the publications they were originally taken from.
+Also the tasks are very simple,
+so they will probably fall below the
+threshold of originality anyway.

c/loop-zilu/benchmark01_conjunctive.c

@@ -0,0 +1,35 @@
+#include <assert.h>
+void reach_error(void) {assert(0);}
+
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    reach_error();
+  }
+}
+
+/* 01.cfg:
+names=x y
+beforeloop=
+beforeloopinit=
+precondition=x==1 && y==1
+loopcondition=
+loop=x=x+y; y=x;
+postcondition=y>=1
+afterloop=
+learners= conj
+*/
+int main() {
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
+  
+  if (!(x==1 && y==1)) return 0;
+  while (__VERIFIER_nondet_bool()) {
+    x=x+y;
+    y=x;
+  }
+  __VERIFIER_assert(y>=1);
+  return 0;
+}

c/loop-zilu/benchmark01_conjunctive.i

@@ -0,0 +1,29 @@
+
+extern void __assert_fail (const char *__assertion, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert_perror_fail (int __errnum, const char *__file,
+      unsigned int __line, const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern void __assert (const char *__assertion, const char *__file, int __line)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+
+void reach_error(void) {((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "benchmark01_conjunctive.c", 2, __extension__ __PRETTY_FUNCTION__); }));}
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    reach_error();
+  }
+}
+int main() {
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
+  if (!(x==1 && y==1)) return 0;
+  while (__VERIFIER_nondet_bool()) {
+    x=x+y;
+    y=x;
+  }
+  __VERIFIER_assert(y>=1);
+  return 0;
+}

c/loop-zilu/benchmark01_conjunctive.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+
+input_files: 'benchmark01_conjunctive.i'
+
+properties:
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
+
+options:
+  language: C
+  data_model: ILP32

c/loop-zilu/benchmark02_linear.c

@@ -0,0 +1,35 @@
+#include <assert.h>
+void reach_error(void) {assert(0);}
+
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    reach_error();
+  }
+}
+
+/* 02.cfg:
+names=l
+beforeloop= int n; int i;
+beforeloopinit= i = l;
+precondition= l>0
+loopcondition= i < n
+loop=i++;
+postcondition=l>=1
+afterloop=
+learners= linear
+*/
+int main() {
+  int n = __VERIFIER_nondet_int();
+  int i = __VERIFIER_nondet_int();
+  int l = __VERIFIER_nondet_int();
+  i = l;
+  if (!(l>0)) return 0;
+  while (i < n) {
+    i++;
+  }
+  __VERIFIER_assert(l>=1);
+  return 0;
+}