1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * TEST THE TIMEOUT MODULE
21 */
22
23 #include <stdint.h>
24 #include <stdio.h>
25 #include <stdbool.h>
26 #include <inttypes.h>
27 #include <assert.h>
28
29 #include "utils/cputime.h"
30 #include "utils/timeout.h"
31
32
33 /*
34 * Timeout handler: set the interrupt flag
35 */
36 typedef struct wrapper_s {
37 volatile bool interrupted;
38 } wrapper_t;
39
40 static wrapper_t wrapper;
41
handler(void * ptr)42 static void handler(void *ptr) {
43 assert(ptr == &wrapper);
44 printf(" timeout received\n");
45 fflush(stdout);
46 ((wrapper_t *) ptr)->interrupted = true;
47 }
48
49
50 /*
51 * Busy computation: increment a binary counter
52 * - c = array of bits (0 or 1) in little-endian
53 * - n = number of bits
54 */
55 // increment c and return the carry out
increment(uint32_t * c,uint32_t n)56 static uint32_t increment(uint32_t *c, uint32_t n) {
57 uint32_t i, c0, b;
58
59 c0 = 1; // carry
60 for (i=0; i<n; i++) {
61 b = c0 + c[i];
62 c[i] = b % 2;
63 c0 = b/2;
64 }
65
66 return c0;
67 }
68
69 // increment until we get a carry out or an interrupt
loop(uint32_t * c,uint32_t n)70 static void loop(uint32_t *c, uint32_t n) {
71 uint32_t i;
72
73 for (i=0; i<n; i++) {
74 c[i] = 0;
75 }
76
77 do {
78 i = increment(c, n);
79 } while (i == 0 && !wrapper.interrupted);
80 }
81
82 // print the counter value
show_counter(uint32_t * c,uint32_t n)83 static void show_counter(uint32_t *c, uint32_t n) {
84 while (n > 0) {
85 n --;
86 assert(c[n] == 0 || c[n] == 1);
87 fputc('0' + c[n], stdout);
88 }
89 }
90
91
92 /*
93 * Test: n = size of the counter, t = timeout value
94 */
test_timeout(uint32_t * c,uint32_t n,uint32_t timeout)95 static void test_timeout(uint32_t *c, uint32_t n, uint32_t timeout) {
96 double start, end;
97
98 printf("---> test: size = %"PRIu32", timeout = %"PRIu32" s\n", n, timeout);
99 fflush(stdout);
100 wrapper.interrupted = false;
101 start_timeout(timeout, handler, &wrapper);
102 start = get_cpu_time();
103 loop(c, n);
104 clear_timeout();
105 end = get_cpu_time();
106 printf(" cpu time = %.2f s\n", end - start);
107 fflush(stdout);
108 if (wrapper.interrupted) {
109 printf(" interrupted at: ");
110 show_counter(c, n);
111 printf("\n");
112 fflush(stdout);
113 } else {
114 printf(" completed: ");
115 show_counter(c, n);
116 printf("\n");
117 fflush(stdout);
118 }
119 }
120
121
122 /*
123 * Global array used as counter
124 */
125 static uint32_t counter[64];
126
main(void)127 int main(void) {
128 uint32_t n;
129 uint32_t time;
130
131 init_timeout();
132
133 time = 20;
134 for (n=5; n<40; n++) {
135 test_timeout(counter, n, time);
136 }
137
138 delete_timeout();
139
140 return 0;
141 }
142