Benchmarks C: non linear

Here, we list all benchmarks from Complexity_C_Non_Linear and provide sources and context for all 20 programs. The benchmarks can be downloaded here. To test our benchmarks, we suggest to use our web interface for C programs. For more precise bounds, please refer to the “All Bounds” section at the end of the generated proof.

non_linear01.c

This benchmark is the simple, non-linear prs-loop which has logarithmic runtime from the introduction of our paper.

int non_linear01(int x1, int x2, int x3, int x4, int x5) {
  while(x4*x4 - x3*x3*x3*x3*x3 < x5 && x4 != 0) {
    int x1_ = x1;
    int x2_ = x2;
    x1 = 3*x1_ + 2*x2_;
    x2 = -5*x1_ -3*x2_;
    x4 = -2*x4;
    x5 = 3*x5 + x3*x3;
  }
  return 0;
}

non_linear02.c

This program corresponds to the chained version of the introductory loop from our paper, i.e., we chained the loop of non_linear01.c once.

int non_linear02(int x1, int x2, int x3, int x4, int x5) {
  while(x4*x4 - x3*x3*x3*x3*x3 < x5 && x4 != 0) {
    x1 = -1*x1;
    x2 = -1*x2;
    x4 = 4*x4;
    x5 = 9*x5 + x3*x3;
  }
  return 0;
}

non_linear03.c

This benchmark is also a simple, non-linear prs-loop which has logarithmic runtime. In contrast to non_linear02.koat, we consider the product of two different variables x1 and x2.

int non_linear03(int x1, int x2, int x3) {
  while(x3*x3 < x1*x2 && x3 != 0) {
    x1 = 2*x1;
    x2 = 3*x2;
    x3 = 4*x3;
  }
  return 0;
}

non_linear04.c

This benchmark is prs-loop which has a disjunction in its guard.

int non_linear04(int x1, int x2, int x3) {
  while((x3 < x1 || x3 < x2) && x3 > 0) {
    x1 = 2*x1;
    x2 = 3*x2;
    x3 = 4*x3;
  }
  return 0;
}

non_linear05.c

This benchmark is a prs-loop which can be transformed into the twn-loop while(x2 < x1 ∧ 0 < x2) do x1 = 2*x1; x2 = 3*x2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)) by the automorphism ϑ(x1) = x2 - x1 and ϑ(x2) = 2*x1 - x2, and its inverse ϑ⁻¹(x1) = x1 + x2 and ϑ⁻¹(x1) = 2*x1 + x2.

int non_linear05(int x1, int x2) {
  while(3*x1 < 2*x2 && x2 < 2*x1) {
    int x1_ = x1;
    int x2_ = x2;
    x1 = 4*x1_ - x2_;
    x2 = 2*x1_ + x2_;
  }
  return 0;
}

non_linear06.c

This benchmark corresponds to the unsolvable loop (3) which is transformed into non_linear01.c by using the polynomial 2*y1 - y2.

int non_linear06(int x1, int x2, int x3, int x4, int y1, int y2) {
  while(x4*x4 - x3*x3*x3*x3*x3 < 2*y1 - y2 && x4 != 0) {
    int x1_ = x1;
    int x2_ = x2;
    x1 = 3*x1_ + 2*x2_;
    x2 = -5*x1_ -3*x2_;
    x4 = -2*x4;
    int y1_ = y1;
    int y2_ = y2;
    y1 = y1_ + y1_*y1_ + x3*x3;
    y2 = -4*y1_ + 2*y1_*y1_ + 3*y2_ + x3*x3;
  }
  return 0;
}

non_linear07.c

This benchmark is an unsolvable loop which has a disjunction in its guard and which is transformed into non_linear03.koat by using the polynomial y1 + 2*y2.

int non_linear07(int y1, int y2, int x2, int x3) {
  while((x3 < y1 + 2*y2 || x3 < x2) && x3 > 0) {
    int y1_ = y1;
    int y2_ = y2;
    y1 = 2*y1_*y1_ + 2*y1_;
    y2 = 2*y2_ - y1_*y1_;
    x2 = 3*x2;
    x3 = 4*x3;
  }
  return 0;
}

non_linear08.c

This benchmark is an unsolvable loop which has a disjunction in its guard and which is transformed into non_linear03.koat by using the polynomials y1 + 2*y2 and z1 - z2.

int non_linear08(int y1, int y2, int z1, int z2, int x3) {
  while((x3 < y1 + 2*y2 || x3 < z1 - z2) && x3 > 0) {
    int y1_ = y1;
    int y2_ = y2;
    int z1_ = z1;
    int z2_ = z2;
    y1 = 2*y1_*y1_ + 2*y1_;
    y2 = 2*y2_ - y1_*y1_;
    z1 = z1_*z1_+z1_ - 3*z2_;
    z2 = z1_*z1_+z1_ - 3*z1_;
    x3 = 4*x3;
  }
  return 0;
}

non_linear09.c

This ITS is the leading example of our paper. Here, the loop at location l2 corresponds to the loop non_linear01.c.

extern int __VERIFIER_nondet_int(void);

int non_linear09(int x1, int x2, int x3, int x4, int x5, int x6) {
  int y = 1;

  while(0 < y && y <= x6) {
    x1 = x6;
    x2 = x6;
    x3 = 2;
    x4 = x3;
    x5 = x6;
    x6 = x6 - 1;
    int y = __VERIFIER_nondet_int();
    while(x4*x4 - x3*x3*x3*x3*x3 < x5 && x4 != 0) {
      int x1_ = x1;
      int x2_ = x2;
      x1 = 3*x1_ + 2*x2_;
      x2 = -5*x1_ -3*x2_;
      x4 = -2*x4;
      x5 = 3*x5 + x3*x3;
    }
  }
  x6 = x1;
  while(x6 > 0) {
    x6 = x6 - 1;
  }
  return 0;
}

non_linear10.c

This benchmark is similar to non_linear09.c. However, instead of using the loop non_linear01.c at location l2, this example uses the unsolvable loop from non_linear06.c.

extern int __VERIFIER_nondet_int(void);

int non_linear10(int x1, int x2, int x3, int x4, int y1, int y2, int x6) {
  int y = 1;

  while(0 < y && y <= x6) {
    x1 = x6;
    x2 = x6;
    x3 = 2;
    x4 = x3;
    y1 = x6;
    y2 = x6;
    x6 = x6 - y;
    int y = __VERIFIER_nondet_int();
    while(x4*x4 - x3*x3*x3*x3*x3 < 2*y1 - y2 && x4 != 0) {
      int x1_ = x1;
      int x2_ = x2;
      x1 = 3*x1_ + 2*x2_;
      x2 = -5*x1_ -3*x2_;
      x4 = -2*x4;
      int y1_ = y1;
      int y2_ = y2;
      y1 = y1_ + y1_*y1_ + x3*x3;
      y2 = -4*y1_ + 2*y1_*y1_ + 3*y2_ + x3*x3;
    }
  }
  x6 = x1;
  while(x6 > 0) {
    x6 = x6 - 1;
  }
  return 0;
}

non_linear11.c

This benchmark corresponds to the commuting program of Fig. 5 in the paper.

extern int __VERIFIER_nondet_int(void);

int non_linear11(int x1, int x2, int x3) {
  while(x1 > 0) {
    if(__VERIFIER_nondet_int()) {
        x1 = x1 - 1;
        x3 = x3 + x2*x2;
    } else {
        x1 = x1 - 1;
        x3 = x3 + x2*x2 + 1;
    }
  }
  while(x3 > 0) {
    x3 = x3 - 1;
  }
  return 0;
}

non_linear12.c

This benchmark is an advanced version of the previous example. Here, the update of x1 and x2 is not twn.

extern int __VERIFIER_nondet_int(void);

int non_linear12(int x1, int x2, int x3, int x4) {
  while(x4 > 0) {
    if(__VERIFIER_nondet_int()) {
        int x1_ = x1;
        int x2_ = x2;
        x1 = 3*x1_ + 2*x2_ + x3*x3;
        x2 = -5*x1_ -3*x2_;
        x4 = x4 - 1;
    } else {
        int x1_ = x1;
        int x2_ = x2;
        x1 = 3*x1_ + 2*x2_ + x3*x3;
        x2 = -5*x1_ -3*x2_;
        x4 = x4 - 1;
    }
  }
  x4 = x1;
  while(x4 > 0) {
    x4 = x4 - 1;
  }
  return 0;
}

non_linear13.c

This benchmark consists of two consecutive loops. In the first loop, we double x2 in every iteration. Hence, the value of x2 is exponential after the first loop. However, the program still has linear runtime as the second loop is only executed a logarithmic number of times.

int non_linear13(int x1, int x2, int x3) {
  while(x1 > 0) {
    x1 = x1 - 1;
    x2 = 2*x2;
  }
  while(x3 < x2 && x3 > 0) {
    x2 = 2*x2;
    x3 = 3*x3;
  }
  return 0;
}

non_linear14.c

This example combines an integer program which needs control-flow refinement (see Giesl et al. here, Fig.7) to be analyzed successfully and the unsolvable loop non_linear03.c.

extern int __VERIFIER_nondet_int(void);

void non_linear14(int x1, int x2, int x3, int x4, int y1, int y2) {
  int u = __VERIFIER_nondet_int();
  int v = __VERIFIER_nondet_int();

  x1 = u;
  while (1) {
    if (1 <= x1 && x1 <= 3 && v == 0) {
      x1 = x1 + 1;
      v = __VERIFIER_nondet_int();
    } else if (x2 > 1 && v == 1) {
      x2 = x2 - 1;
      v = __VERIFIER_nondet_int();
    } else {
      while(x4*x4 - x3*x3*x3*x3*x3 < 2*y1 - y2 && x4 != 0) {
        x4 = -2*x4;
        int y1_ = y1;
        int y2_ = y2;
        y1 = y1_ + y1_*y1_ + x3*x3;
        y2 = -4*y1_ + 2*y1_*y1_ + 3*y2_ + x3*x3;
      }
      break;
    }
  }
}

non_linear15.c

This benchmark consists of two commuting twn-loops which both do not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5) but can be handled individually by our twn-technique. However, this combination of two twn-loops needs more advanced techniques.

extern int __VERIFIER_nondet_int(void);

int non_linear15(int x1, int x2) {
  while(x2 < x1 && x2 > 0) {
    if(__VERIFIER_nondet_int()) {
      x1 = 2*x1;
      x2 = 3*x2;
    } else {
      x1 = 2*x1;
      x2 = 4*x2;
    }
  }
  return 0;
}

non_linear16.c

This benchmark consists of a twn-loop and a second loop which cannot be handled by our techniques for loops as it contains temporary variables. Furthermore, this second loop needs a MPRF of depth at least two.

extern int __VERIFIER_nondet_int(void);

int non_linear16(int x1, int x2, int y1, int y2) {
  while(x2 < x1 && x2 > 0) {
    x1 = 2*x1;
    x2 = 3*x2;
  }
  int t = __VERIFIER_nondet_int();
  while(y1 > 0 && t > 0) {
    y1 = y1 + y2;
    y2 = y2 - t;
    t = __VERIFIER_nondet_int();
  }
  return 0;
}

non_linear17.c

Here, we have extended the example from our earlier paper here, Fig.7 by a twn-loop which has a logarithmic runtime and thus yields linear size bounds. These linear size bounds are important for a third loop which decrements y1 iteratively by one.

extern int __VERIFIER_nondet_int(void);

void f(int x1, int x2, int x3, int x4, int y1, int y2) {
  int u = __VERIFIER_nondet_int();
  int v = __VERIFIER_nondet_int();

  x1 = u;

  int f = v;
  while (1) {
    if (1 <= x1 && x1 <= 3 && f == 0) {
      x1 = x1 + 1;
      v = __VERIFIER_nondet_int();
      f = v;
    } else if (x2 > 1 && f == 1) {
      x2 = x2 - 1;
      v = __VERIFIER_nondet_int();
      f = v;
    } else {
      break;
    }
  }
  while(y2 < y1 && y2 > 0) {
    y1 = 2*y1;
    y2 = 3*y2;
  }
  while(y2 > 0) {
    y2 = y2 - 1;
  }
}

non_linear18.c

This benchmarks contains a non-unit, solvable loop. The eigenvalues of this loop have absolute value 1/2 * (5 + sqrt(33)). Hence, the value of x1 is exponential before the second loop and thus also the runtime of the complete program is exponential.

int non_linear18(int x1, int x2, int x3) {
  while(x3 > 0) {
    int x1_ = x1;
    int x2_ = x2;
    x1 = x1_ + 2*x2_;
    x2 = 3*x1_ + 4*x2_;
    x3 = x3 - 1;
  }
  while(x1 > 0) {
    x1 = x1 - 1;
  }
  return 0;
}

non_linear19.c

This benchmark is a more advanced version of the twn-loop while(x2 < x1 ∧ 0 < x2) do x1 = 2*x1; x2 = 3*x2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)). Here, we extended this loop by the update of x3. The first loop is not a solvable loop. However, the update still admits a (super-exponential) closed form for x3. As the first loop has a logarithmic runtime complexity, the overall size of x3 is still polynomial and thus the runtime of the complete program is also polynomial.

int non_linear19(int x1, int x2, int x3) {
  while(x2 < x1 && x2 > 0) {
    x1 = 2*x1;
    x2 = 3*x2;
    x3 = x3*x3;
  }
  while(0 < x3) {
    x3 = x3 - 1;
  }
  return 0;
}

non_linear20.c

This benchmark is a more advanced version of the twn-loop while(x2 < x1 ∧ 0 < x2) do x1 = 2*x1; x2 = 3*x2; (which does not admit a linear ranking function over the reals (see Leike & Heizmann here, Thm. 4.5)). Here, we introduced a temporary variable and consider the following loop while(X2 < X1 ∧ 0 < X2) do X1 = 2*X1; X2 >= 3*X2;. Our current technique is not able to succeed on this benchmark.

extern int __VERIFIER_nondet_int(void);

int non_linear20(int x1, int x2) {
  int t = __VERIFIER_nondet_int();
  while(x2 < x1 && x2 > 0 && t >= 3) {
    x1 = 2*x1;
    x2 = t*x2;
    int t = __VERIFIER_nondet_int();
  }
  return 0;
}