Add benchmarks from zilu paper

These are some simple benchmarks with loops where
linear/disjunctive/conjunctive/polynomial invariants
are needed to prove the programs to be correct.

Author: MartinSpiessl

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,37 @@
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+      unsigned int __line, __const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+
+void reach_error(void) {__assert_fail ("0", "benchmark01_polynomial.c", 11, __PRETTY_FUNCTION__);}
+
+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 (1) {
+    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.c'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/loop-zilu/benchmark02_linear.c

@@ -0,0 +1,37 @@
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+      unsigned int __line, __const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+
+void reach_error(void) {__assert_fail ("0", "benchmark02_conjunctive.c", 11, __PRETTY_FUNCTION__);}
+
+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;
+}

c/loop-zilu/benchmark02_linear.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+
+input_files: 'benchmark02_linear.c'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32

c/loop-zilu/benchmark03_linear.c

@@ -0,0 +1,45 @@
+extern void __assert_fail (__const char *__assertion, __const char *__file,
+      unsigned int __line, __const char *__function)
+     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern _Bool __VERIFIER_nondet_bool(void);
+
+void reach_error(void) {__assert_fail ("0", "benchmark03_linear.c", 11, __PRETTY_FUNCTION__);}
+
+void __VERIFIER_assert(int cond) {
+  if (!cond) {
+    reach_error();
+  }
+}
+
+/* 03.cfg:
+names=i j
+beforeloop=int x, y;
+beforeloopinit=x = 0; y = 0;
+symbolic=flag
+precondition=i==0 && j==0
+loopcondition=
+loop=x++; y++; i+=x; j+=y; if (flag) j+=1;
+postcondition=j>=i
+afterloop=
+learners= linear
+*/
+int main() {
+  int x = __VERIFIER_nondet_int();
+  int y = __VERIFIER_nondet_int();
+  int i = __VERIFIER_nondet_int();
+  int j = __VERIFIER_nondet_int();
+  
+  _Bool flag = __VERIFIER_nondet_bool();
+  x = 0; y = 0;
+  if (!(i==0 && j==0)) return 0;
+  while (1) {
+    x++;
+    y++;
+    i+=x;
+    j+=y;
+    if (flag) j+=1;
+  }
+  __VERIFIER_assert(j>=i);
+  return 0;
+}

c/loop-zilu/benchmark03_linear.yml

@@ -0,0 +1,11 @@
+format_version: '2.0'
+
+input_files: 'benchmark03_linear.c'
+
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32