Merge pull request #1836 from goblint/halbwachs-phd-tests

Add tests from Halbwachs' PhD thesis

Author: sim642

src/analyses/loopTermination.ml

@@ -1,4 +1,6 @@
-(** Termination analysis for loops and [goto] statements ([termination]). *)
+(** Termination analysis for loops and [goto] statements ([termination]).
+
+    @see <https://theses.hal.science/tel-00288805> Halbwachs, N. Détermination automatique de relations linéaires vérifiées par les variables d’un programme. PhD thesis. Section 8.3. *)
 
 open Analyses
 open GoblintCil

tests/regression/89-apron3/01-halbwachs-phd-sec5.6.2.c

@@ -0,0 +1,30 @@
+// SKIP TERM PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra --set ana.activated[+] termination
+// fully works with --set ana.widen.delay.local 6
+// Somehow we prove termination even without and don't have good bounds on termination counter.
+// From Nicolas Halbwachs' PhD thesis, section 5.6.2.
+#include <goblint.h>
+
+int main() {
+  unsigned int i = 0;
+  unsigned int j = 0;
+  while (i <= 10) {
+    __goblint_check(j >= 0);
+    __goblint_check(i - 2 * j >= 0);
+    __goblint_check(i <= 10);
+
+    int r; // rand
+    if (r) {
+      i += 2;
+      j++;
+    }
+    else
+      i += 4;
+  }
+
+  __goblint_check(j >= 0);
+  __goblint_check(i - 2 * j >= 0);
+  __goblint_check(11 <= i);
+  __goblint_check(i <= 14); // TODO: needs one narrowing iteration
+  __goblint_check(i + 2 * j <= 24); // TODO: needs one narrowing iteration
+  return 0;
+}

tests/regression/89-apron3/02-halbwachs-phd-sec8.3.c

@@ -0,0 +1,43 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.apron.domain polyhedra
+// fully works with --set ana.widen.delay.local 6
+// From Nicolas Halbwachs' PhD thesis, section 8.3.
+// Same as 01-halbwachs-phd-sec5.6.2 annotated with an explicit termination counter.
+#include <goblint.h>
+
+int main() {
+  unsigned int i = 0;
+  unsigned int j = 0;
+  unsigned int k = 0; // explicit termination counter
+  while (k++, i <= 10) {
+    __goblint_check(j >= 0);
+    __goblint_check(i + 2 * j + 4 == 4 * k);
+    __goblint_check(i <= 10);
+    __goblint_check(2 * k <= i + 2);
+
+    int r; // rand
+    if (r) {
+      i += 2;
+      j++;
+    }
+    else
+      i += 4;
+
+    __goblint_check(j >= 0);
+    __goblint_check(i + 2 * j == 4 * k);
+    __goblint_check(i <= 14);
+    __goblint_check(1 <= k);
+    __goblint_check(k <= 6);
+    __goblint_check(2 * k <= i);
+  }
+
+  __goblint_check(j >= 0);
+  __goblint_check(i + 2 * j + 4 == 4 * k); // TODO: needs one narrowing iteration?
+  __goblint_check(11 <= i);
+  __goblint_check(i <= 14); // TODO: needs one narrowing iteration?
+  __goblint_check(2 * k <= i + 2); // TODO: needs one narrowing iteration?
+
+  // if i and j are projected out:
+  __goblint_check(4 <= k);
+  __goblint_check(k <= 7); // TODO: needs one narrowing iteration?
+  return 0;
+}

tests/regression/89-apron3/dune

@@ -0,0 +1,10 @@
+(rule
+ (aliases runtest runaprontest)
+ (enabled_if %{lib-available:apron})
+ (deps
+   (package goblint)
+   ../../../goblint ; update_suite calls local goblint
+   (:update_suite ../../../scripts/update_suite.rb)
+   (glob_files ??-*.c))
+ (locks /update_suite)
+ (action (chdir ../../.. (run %{update_suite} group apron3 -q))))