Reviewed By: mbouaziz Differential Revision: D8024669 fbshipit-source-id: 479517emaster
parent
dde2000e75
commit
1263bfa899
@ -0,0 +1,66 @@
|
|||||||
|
/*
|
||||||
|
* Copyright (c) 2018 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*/
|
||||||
|
|
||||||
|
/* while loop that contains && in the guard. It gives the correct bound */
|
||||||
|
int compound_while(int m) {
|
||||||
|
int i = 0;
|
||||||
|
int j = 3 * i;
|
||||||
|
while (j == 0 && i < m) {
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
return j;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* B will be in the loop and executed ~100 times-- we get infinity due to
|
||||||
|
* control variable problem with gotos */
|
||||||
|
int simulated_while_with_and(int p) {
|
||||||
|
int k = 0;
|
||||||
|
int j = 0;
|
||||||
|
B:
|
||||||
|
j++;
|
||||||
|
if (k == 0 && j < 100) {
|
||||||
|
goto B; // continue;
|
||||||
|
}
|
||||||
|
return k;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* shortcut in the conditional, hence we won't loop, and get constant cost */
|
||||||
|
int simulated_while_shortcut(int p) {
|
||||||
|
int k = 0;
|
||||||
|
int j = 0;
|
||||||
|
B:
|
||||||
|
j++;
|
||||||
|
if (k == 1 && j < 100) {
|
||||||
|
goto B; // continue;
|
||||||
|
}
|
||||||
|
return k;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* p should be in control vars */
|
||||||
|
void while_and_or(int p) {
|
||||||
|
int i = 0;
|
||||||
|
while (p == 1 || (i < 30 && i > 0)) {
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
// should be constant cost, but due to p occuring in control vars, we would get
|
||||||
|
// +oo for p
|
||||||
|
int nested_while_and_or(int p) {
|
||||||
|
int i = 0;
|
||||||
|
int j = 3 * i;
|
||||||
|
while (p == 1 || (i < 30 && i > 0)) {
|
||||||
|
while (p == 1 || (j < 5 && j > 0)) {
|
||||||
|
|
||||||
|
return j;
|
||||||
|
}
|
||||||
|
i++;
|
||||||
|
}
|
||||||
|
return j;
|
||||||
|
}
|
@ -0,0 +1,36 @@
|
|||||||
|
/*
|
||||||
|
* Copyright (c) 2018 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*/
|
||||||
|
void nop() { int k = 0; }
|
||||||
|
|
||||||
|
/* we report infinity after the first loop, due to the problem in prune node.
|
||||||
|
* Instead, we should obtain the appropriate bounds for the two loops */
|
||||||
|
int two_loops_symb(int m) {
|
||||||
|
int p = 10;
|
||||||
|
|
||||||
|
for (int i = 0; i < m; i++) {
|
||||||
|
nop();
|
||||||
|
}
|
||||||
|
for (int j = 0; j < m; j++) {
|
||||||
|
nop();
|
||||||
|
}
|
||||||
|
return p;
|
||||||
|
}
|
||||||
|
|
||||||
|
/* we report the appropriate bounds for the two loops if the loops are over two
|
||||||
|
* different arguments */
|
||||||
|
int two_loops_symb_diff(int m, int k) {
|
||||||
|
int p = 10;
|
||||||
|
for (int i = 0; i < m; i++) {
|
||||||
|
nop();
|
||||||
|
}
|
||||||
|
for (int j = 0; j < k; j++) {
|
||||||
|
nop();
|
||||||
|
}
|
||||||
|
return p;
|
||||||
|
}
|
Loading…
Reference in new issue