16032530443

Committed 02 Jul 2025 06:08PM UTC coverage: 60.349% (-5.0%) from 65.357%

Build # 16032530443

Build Type

Pull #582

github

Committed by

web-flow

Commit Message

Merge b7e09d316 into b3af64ab1

Pull Request Pull Request #582: Update ci

Run Details

63716 of 105580 relevant lines covered (60.35%)

1127640.75 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

95.92

/src/utils/timeout.c

/*
 * This file is part of the Yices SMT Solver.
 * Copyright (C) 2017 SRI International.
 *
 * Yices is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * Yices is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
 */

/*
 * SUPPORT FOR A SINGLE TIMEOUT
 */

/*
 * Two implementations:
 * one for UNIX (Linux/Darwin/Cygwin)
 * one for Windows (MinGW).
 *
 * NOTES:
 * signal has different behavior on different Unix versions.
 * Here's what the manpage says (on Linux).
 *
 * The original Unix signal() would  reset the handler to SIG_DFL, and
 * System V (and the Linux kernel  and libc4,5) does the same.  On the
 * other  hand,  BSD  does  not  reset the  handler,  but  blocks  new
 * instances  of this  signal  from  occurring during  a  call of  the
 * handler.  The glibc2 library follows the BSD behavior.
 *
 * Testing results:
 * - on solaris 5.10, the signal handler is reset to SIG_DFL before
 *   the handler is called. So we must restore the handler every time.
 * - on Linux/Darwin/Cygwin: the signal handler is not changed.
 *
 */

#include <assert.h>
#ifdef MINGW
// Use the oldest version of the Windows API.
#ifndef _WIN32_WINNT
#define _WIN32_WINNT 0x0500
#endif

#include <windows.h>
#elif defined(THREAD_SAFE)
#include <pthread.h>
#include <sys/time.h>
#endif

#include "utils/error.h"
#include "utils/memalloc.h"
#include "utils/timeout.h"
#include "yices_exit_codes.h"

/*
 * Timeout state:
 * - NOT_READY: initial state and after call to delete_timeout
 * - READY: ready to be started (state after init_timeout
 *          and after clear_timeout)
 * - ACTIVE: after a call to start_timeout, before the timer fires
 *           or the timeout is canceled
 * - CANCELED: used by clear_timeout
 * - FIRED: after the handler has been called
 */
typedef enum timeout_state {
  TIMEOUT_NOT_READY, // 0
  TIMEOUT_READY,
  TIMEOUT_ACTIVE,
  TIMEOUT_CANCELED,
  TIMEOUT_FIRED,
} timeout_state_t;


typedef struct timeout_s {
  timeout_state_t state;
  timeout_handler_t handler;
  void *param;
#ifdef MINGW
  HANDLE timer_queue;
  HANDLE timer;
#elif defined(THREAD_SAFE)
  struct timespec ts;
  pthread_t thread;
  pthread_mutex_t mutex;
  pthread_cond_t cond;
#endif
} timeout_t;


#if !defined(MINGW) && !defined(THREAD_SAFE)

/*
 * Global structure for single-threaded case.
 */
static timeout_t the_timeout;

#endif

/* Initialize the timeout fields common to all implementations. */

static inline void init_base_timeout(timeout_t *timeout) {
  timeout->state = TIMEOUT_READY;
  timeout->handler = NULL;
  timeout->param = NULL;
}

#ifndef MINGW


/*****************************
 *  UNIX/C99 IMPLEMENTATION  *
 ****************************/

#include <unistd.h>
#include <signal.h>
#include <stdio.h>
#include <stdlib.h>
#include <sys/errno.h>

#ifdef THREAD_SAFE

#include "mt/threads.h"

timeout_t *init_timeout(void) {
  timeout_t *timeout;

  timeout = (timeout_t *) safe_malloc(sizeof(timeout_t));

  init_base_timeout(timeout);
  timeout->ts.tv_sec = 0;
  timeout->ts.tv_nsec = 0;

  check_thread_api(pthread_mutex_init(&timeout->mutex, /*attr=*/NULL),
                   "start_timeout: pthread_mutex_init");
  check_thread_api(pthread_cond_init(&timeout->cond, /*attr=*/NULL),
                   "start_timeout: pthread_cond_init");
  
  return timeout;
}

void delete_timeout(timeout_t *timeout) {
  check_thread_api(pthread_cond_destroy(&timeout->cond),
                   "delete_timeout: pthread_cond_destroy");
  check_thread_api(pthread_mutex_destroy(&timeout->mutex),
                   "delete_timeout: pthread_mutex_destroy");
    
  safe_free(timeout);
}

static void *timer_thread(void *arg) {
  timeout_t *timeout;
  
  timeout = (timeout_t *) arg;

  /* Get exclusive access to the state. */
  check_thread_api(pthread_mutex_lock(&timeout->mutex),
                   "timer_thread: pthread_mutex_lock");
  /* It is theoretically possible that the timeout has already been
     canceled by a quick call to clear_timeout. If so, we do not need
     to wait. */
  if (timeout->state != TIMEOUT_CANCELED) {
    int ret = pthread_cond_timedwait(&timeout->cond, &timeout->mutex,
                                     &timeout->ts);
    if (ret && ret != ETIMEDOUT)
      perror_fatal_code("timer_thread: pthread_cond_timedwait", ret);
  }

  /* If the timeout wasn't canceled, then the timeout expired. */
  if (timeout->state != TIMEOUT_CANCELED) {
    timeout->state = TIMEOUT_FIRED;
    timeout->handler(timeout->param);
  }

  check_thread_api(pthread_mutex_unlock(&timeout->mutex),
                   "timer_thread: pthread_mutex_unlock");
  
  return NULL;
}

void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
  struct timeval tv;
  
  assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL);

  timeout->state = TIMEOUT_ACTIVE;
  timeout->handler = handler;
  timeout->param = param;

  /* Compute the desired stop time. */
  if (gettimeofday(&tv, /*tzp=*/NULL) == -1)
    perror_fatal("start_timeout: gettimeofday");
  timeout->ts.tv_sec = tv.tv_sec + delay;
  timeout->ts.tv_nsec = 1000 * tv.tv_usec;

  check_thread_api(pthread_create(&timeout->thread, /*attr=*/NULL,
                                  timer_thread, timeout),
                   "start_timeout: pthread_create");
}

void clear_timeout(timeout_t *timeout) {
  void *value;
  
  /* Tell the thread to exit. */
  check_thread_api(pthread_mutex_lock(&timeout->mutex),
                   "clear_timeout: pthread_mutex_lock");
  timeout->state = TIMEOUT_CANCELED;
  check_thread_api(pthread_mutex_unlock(&timeout->mutex),
                   "clear_timeout: pthread_mutex_unlock");
  check_thread_api(pthread_cond_signal(&timeout->cond),
                   "clear_timeout: pthread_cond_signal");

  /* Wait for the thread to exit. */
  check_thread_api(pthread_join(timeout->thread, &value),
                   "clear_timeout: pthread_join");

  timeout->state = TIMEOUT_READY;
}

#else /* !defined(THREAD_SAFE) */

/*
 * To save the original SIG_ALRM handler
 */
static void (*saved_handler)(int);


/*
 * SIG_ALRM handler:
 * - do nothing if the timeout is not active
 * - otherwise, change the state to fired
 *   then call the handler
 */
static void alarm_handler(int signum) {
  if (the_timeout.state == TIMEOUT_ACTIVE) {
    the_timeout.state = TIMEOUT_FIRED;
    the_timeout.handler(the_timeout.param);
  }
}


/*
 * Initialization:
 * - install the alarm_handler (except on Solaris)
 * - initialize state to READY
 */
timeout_t *init_timeout(void) {
#ifndef SOLARIS
  saved_handler = signal(SIGALRM, alarm_handler);
  if (saved_handler == SIG_ERR) {
    perror("Yices: failed to install SIG_ALRM handler: ");
    exit(YICES_EXIT_INTERNAL_ERROR);
  }
#endif

  init_base_timeout(&the_timeout);

  return &the_timeout;
}



/*
 * Activate the timer
 * - delay = timeout in seconds (must be positive)
 * - handler = the handler to call
 * - param = data passed to the handler
 *
 * On Solaris: set the signal handler here.
 */
void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
  assert(timeout == &the_timeout);
  assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL);
  the_timeout.state = TIMEOUT_ACTIVE;
  the_timeout.handler = handler;
  the_timeout.param = param;

#ifdef SOLARIS
  saved_handler = signal(SIGALRM, alarm_handler);
  if (saved_handler == SIG_ERR) {
    perror("Yices: failed to install SIG_ALRM handler: ");
    exit(YICES_EXIT_INTERNAL_ERROR);
  }
#endif

  (void) alarm(delay);
}



/*
 * Clear timeout:
 * - cancel the timeout if it's not fired
 * - set state to READY
 */
void clear_timeout(timeout_t *timeout) {
  assert(timeout == &the_timeout);
  
  // TODO: Check whether we should block the signals here?
  if (the_timeout.state == TIMEOUT_ACTIVE) {
    // not fired;
    the_timeout.state = TIMEOUT_CANCELED;
    (void) alarm(0); // cancel the alarm
  }
  the_timeout.state = TIMEOUT_READY;
}


/*
 * Final cleanup:
 * - cancel the timeout if it's active
 * - restore the original handler
 */
void delete_timeout(timeout_t *timeout) {
  assert(timeout == &the_timeout);
  
  if (the_timeout.state == TIMEOUT_ACTIVE) {
    (void) alarm(0);
  }
  (void) signal(SIGALRM, saved_handler);
  the_timeout.state = TIMEOUT_NOT_READY;
}

#endif /* defined(THREAD_SAFE) */

#else


/************************************
 *   WINDOWS/MINGW IMPLEMENTATION   *
 ***********************************/

#include <inttypes.h>
#include <stdio.h>
#include <stdlib.h>

/*
 * Callback function for the timer
 * - do nothing if the timeout is not active
 * - otherwise change the state to fired and
 *   call the handler.
 */
static VOID CALLBACK timer_callback(PVOID param, BOOLEAN timer_or_wait_fired) {
  timeout_t *timeout = (timeout_t *) param;
  
  if (timeout->state == TIMEOUT_ACTIVE) {
    timeout->state = TIMEOUT_FIRED;
    timeout->handler(timeout->param);
  }
}


/*
 * Initialization:
 * - create the timer queue
 */
timeout_t *init_timeout(void) {
  timeout_t *timeout = (timeout_t *) safe_malloc(sizeof(timeout_t));

  init_base_timeout(timeout);

  timeout->timer_queue = CreateTimerQueue();
  if (timeout->timer_queue == NULL) {
    fprintf(stderr, "Yices: CreateTimerQueue failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
    fflush(stderr);
    exit(YICES_EXIT_INTERNAL_ERROR);
  }

  timeout->timer = NULL;

  return timeout;
}



/*
 * Activate:
 * - delay = timeout in seconds (must be positive)
 * - handler = handler to call if fired
 * - param = parameter for the handler
 */
void start_timeout(timeout_t *timeout, uint32_t delay, timeout_handler_t handler, void *param) {
  DWORD duetime;

  assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL);

  duetime = delay * 1000; // delay in milliseconds
  if (CreateTimerQueueTimer(&timeout->timer,
                            timeout->timer_queue,
                            (WAITORTIMERCALLBACK) timer_callback,
                            timeout, duetime,
                            /*Period=*/0,
                            /*Flags=*/WT_EXECUTEDEFAULT)) {
    // timer created
    timeout->state = TIMEOUT_ACTIVE;
    timeout->handler = handler;
    timeout->param = param;
  } else {
    fprintf(stderr, "Yices: CreateTimerQueueTimer failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
    fflush(stderr);
    exit(YICES_EXIT_INTERNAL_ERROR);
  }
}



/*
 * Delete the timer
 */
void clear_timeout(timeout_t *timeout) {
  // GetLastError returns DWORD, which is an unsigned 32bit integer
  uint32_t error_code;

  if (timeout->state == TIMEOUT_ACTIVE || timeout->state == TIMEOUT_FIRED) {
    if (timeout->state == TIMEOUT_ACTIVE) {
      // active and not fired yet
      timeout->state = TIMEOUT_CANCELED; // will prevent call to handle
    }

    /*
     * We give NULL as CompletionEvent so timer_callback will complete
     * if the timer has fired. That's fine as the timeout state is not
     * active anymore so the timer_callback does nothing.
     *
     * Second try: give INVALID_HANDLE_VALUE?
     * This causes SEG FAULT in ntdll.dll
     */
    if (! DeleteTimerQueueTimer(timeout->timer_queue, timeout->timer,
                                INVALID_HANDLE_VALUE)) {
      error_code = (uint32_t) GetLastError();
      // The Microsoft doc says we should try again
      // unless error code is ERROR_IO_PENDING??
      fprintf(stderr, "Yices: DeleteTimerQueueTimer failed with error code %"PRIu32"\n", error_code);
      fflush(stderr);
      exit(YICES_EXIT_INTERNAL_ERROR);
    }
  }

  timeout->state = TIMEOUT_READY;
}



/*
 * Final cleanup:
 * - delete the timer_queue
 */
void delete_timeout(timeout_t *timeout) {
  if (! DeleteTimerQueueEx(timeout->timer_queue, INVALID_HANDLE_VALUE)) {
    fprintf(stderr, "Yices: DeleteTimerQueueEx failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
    fflush(stderr);
    exit(YICES_EXIT_INTERNAL_ERROR);
  }

  safe_free(timeout);
}




#endif /* MINGW */

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	* SUPPORT FOR A SINGLE TIMEOUT
21	*/
22
23	/*
24	* Two implementations:
25	* one for UNIX (Linux/Darwin/Cygwin)
26	* one for Windows (MinGW).
27	*
28	* NOTES:
29	* signal has different behavior on different Unix versions.
30	* Here's what the manpage says (on Linux).
31	*
32	* The original Unix signal() would reset the handler to SIG_DFL, and
33	* System V (and the Linux kernel and libc4,5) does the same. On the
34	* other hand, BSD does not reset the handler, but blocks new
35	* instances of this signal from occurring during a call of the
36	* handler. The glibc2 library follows the BSD behavior.
37	*
38	* Testing results:
39	* - on solaris 5.10, the signal handler is reset to SIG_DFL before
40	* the handler is called. So we must restore the handler every time.
41	* - on Linux/Darwin/Cygwin: the signal handler is not changed.
42	*
43	*/
44
45	#include <assert.h>
46	#ifdef MINGW
47	// Use the oldest version of the Windows API.
48	#ifndef _WIN32_WINNT
49	#define _WIN32_WINNT 0x0500
50	#endif
51
52	#include <windows.h>
53	#elif defined(THREAD_SAFE)
54	#include <pthread.h>
55	#include <sys/time.h>
56	#endif
57
58	#include "utils/error.h"
59	#include "utils/memalloc.h"
60	#include "utils/timeout.h"
61	#include "yices_exit_codes.h"
62
63	/*
64	* Timeout state:
65	* - NOT_READY: initial state and after call to delete_timeout
66	* - READY: ready to be started (state after init_timeout
67	* and after clear_timeout)
68	* - ACTIVE: after a call to start_timeout, before the timer fires
69	* or the timeout is canceled
70	* - CANCELED: used by clear_timeout
71	* - FIRED: after the handler has been called
72	*/
73	typedef enum timeout_state {
74	TIMEOUT_NOT_READY, // 0
75	TIMEOUT_READY,
76	TIMEOUT_ACTIVE,
77	TIMEOUT_CANCELED,
78	TIMEOUT_FIRED,
79	} timeout_state_t;
80
81
82	typedef struct timeout_s {
83	timeout_state_t state;
84	timeout_handler_t handler;
85	void *param;
86	#ifdef MINGW
87	HANDLE timer_queue;
88	HANDLE timer;
89	#elif defined(THREAD_SAFE)
90	struct timespec ts;
91	pthread_t thread;
92	pthread_mutex_t mutex;
93	pthread_cond_t cond;
94	#endif
95	} timeout_t;
96
97
98	#if !defined(MINGW) && !defined(THREAD_SAFE)
99
100	/*
101	* Global structure for single-threaded case.
102	*/
103	static timeout_t the_timeout;
104
105	#endif
106
107	/* Initialize the timeout fields common to all implementations. */
108
109	static inline void init_base_timeout(timeout_t *timeout) {	3✔
110	timeout->state = TIMEOUT_READY;	3✔
111	timeout->handler = NULL;	3✔
112	timeout->param = NULL;	3✔
113	}	3✔
114
115	#ifndef MINGW
116
117
118	/*****************************
119	* UNIX/C99 IMPLEMENTATION *
120	****************************/
121
122	#include <unistd.h>
123	#include <signal.h>
124	#include <stdio.h>
125	#include <stdlib.h>
126	#include <sys/errno.h>
127
128	#ifdef THREAD_SAFE
129
130	#include "mt/threads.h"
131
132	timeout_t *init_timeout(void) {	3✔
133	timeout_t *timeout;
134
135	timeout = (timeout_t *) safe_malloc(sizeof(timeout_t));	3✔
136
137	init_base_timeout(timeout);	3✔
138	timeout->ts.tv_sec = 0;	3✔
139	timeout->ts.tv_nsec = 0;	3✔
140
141	check_thread_api(pthread_mutex_init(&timeout->mutex, /attr=/NULL),	3✔
142	"start_timeout: pthread_mutex_init");
143	check_thread_api(pthread_cond_init(&timeout->cond, /attr=/NULL),	3✔
144	"start_timeout: pthread_cond_init");
145
146	return timeout;	3✔
147	}
148
149	void delete_timeout(timeout_t *timeout) {	3✔
150	check_thread_api(pthread_cond_destroy(&timeout->cond),	3✔
151	"delete_timeout: pthread_cond_destroy");
152	check_thread_api(pthread_mutex_destroy(&timeout->mutex),	3✔
153	"delete_timeout: pthread_mutex_destroy");
154
155	safe_free(timeout);	3✔
156	}	3✔
157
158	static void timer_thread(void arg) {	3✔
159	timeout_t *timeout;
160
161	timeout = (timeout_t *) arg;	3✔
162
163	/* Get exclusive access to the state. */
164	check_thread_api(pthread_mutex_lock(&timeout->mutex),	3✔
165	"timer_thread: pthread_mutex_lock");
166	/* It is theoretically possible that the timeout has already been
167	canceled by a quick call to clear_timeout. If so, we do not need
168	to wait. */
169	if (timeout->state != TIMEOUT_CANCELED) {	3✔
170	int ret = pthread_cond_timedwait(&timeout->cond, &timeout->mutex,	3✔
171	&timeout->ts);	3✔
172	if (ret && ret != ETIMEDOUT)	3✔
173	perror_fatal_code("timer_thread: pthread_cond_timedwait", ret);	×
174	}
175
176	/* If the timeout wasn't canceled, then the timeout expired. */
177	if (timeout->state != TIMEOUT_CANCELED) {	3✔
178	timeout->state = TIMEOUT_FIRED;	3✔
179	timeout->handler(timeout->param);	3✔
180	}
181
182	check_thread_api(pthread_mutex_unlock(&timeout->mutex),	3✔
183	"timer_thread: pthread_mutex_unlock");
184
185	return NULL;	3✔
186	}
187
188	void start_timeout(timeout_t timeout, uint32_t delay, timeout_handler_t handler, void param) {	3✔
189	struct timeval tv;
190
191	assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL);
192
193	timeout->state = TIMEOUT_ACTIVE;	3✔
194	timeout->handler = handler;	3✔
195	timeout->param = param;	3✔
196
197	/* Compute the desired stop time. */
198	if (gettimeofday(&tv, /tzp=/NULL) == -1)	3✔
199	perror_fatal("start_timeout: gettimeofday");	×
200	timeout->ts.tv_sec = tv.tv_sec + delay;	3✔
201	timeout->ts.tv_nsec = 1000 * tv.tv_usec;	3✔
202
203	check_thread_api(pthread_create(&timeout->thread, /attr=/NULL,	3✔
204	timer_thread, timeout),
205	"start_timeout: pthread_create");
206	}	3✔
207
208	void clear_timeout(timeout_t *timeout) {	3✔
209	void *value;
210
211	/* Tell the thread to exit. */
212	check_thread_api(pthread_mutex_lock(&timeout->mutex),	3✔
213	"clear_timeout: pthread_mutex_lock");
214	timeout->state = TIMEOUT_CANCELED;	3✔
215	check_thread_api(pthread_mutex_unlock(&timeout->mutex),	3✔
216	"clear_timeout: pthread_mutex_unlock");
217	check_thread_api(pthread_cond_signal(&timeout->cond),	3✔
218	"clear_timeout: pthread_cond_signal");
219
220	/* Wait for the thread to exit. */
221	check_thread_api(pthread_join(timeout->thread, &value),	3✔
222	"clear_timeout: pthread_join");
223
224	timeout->state = TIMEOUT_READY;	3✔
225	}	3✔
226
227	#else /* !defined(THREAD_SAFE) */
228
229	/*
230	* To save the original SIG_ALRM handler
231	*/
232	static void (*saved_handler)(int);
233
234
235	/*
236	* SIG_ALRM handler:
237	* - do nothing if the timeout is not active
238	* - otherwise, change the state to fired
239	* then call the handler
240	*/
241	static void alarm_handler(int signum) {
242	if (the_timeout.state == TIMEOUT_ACTIVE) {
243	the_timeout.state = TIMEOUT_FIRED;
244	the_timeout.handler(the_timeout.param);
245	}
246	}
247
248
249	/*
250	* Initialization:
251	* - install the alarm_handler (except on Solaris)
252	* - initialize state to READY
253	*/
254	timeout_t *init_timeout(void) {
255	#ifndef SOLARIS
256	saved_handler = signal(SIGALRM, alarm_handler);
257	if (saved_handler == SIG_ERR) {
258	perror("Yices: failed to install SIG_ALRM handler: ");
259	exit(YICES_EXIT_INTERNAL_ERROR);
260	}
261	#endif
262
263	init_base_timeout(&the_timeout);
264
265	return &the_timeout;
266	}
267
268
269
270	/*
271	* Activate the timer
272	* - delay = timeout in seconds (must be positive)
273	* - handler = the handler to call
274	* - param = data passed to the handler
275	*
276	* On Solaris: set the signal handler here.
277	*/
278	void start_timeout(timeout_t timeout, uint32_t delay, timeout_handler_t handler, void param) {
279	assert(timeout == &the_timeout);
280	assert(delay > 0 && the_timeout.state == TIMEOUT_READY && handler != NULL);
281	the_timeout.state = TIMEOUT_ACTIVE;
282	the_timeout.handler = handler;
283	the_timeout.param = param;
284
285	#ifdef SOLARIS
286	saved_handler = signal(SIGALRM, alarm_handler);
287	if (saved_handler == SIG_ERR) {
288	perror("Yices: failed to install SIG_ALRM handler: ");
289	exit(YICES_EXIT_INTERNAL_ERROR);
290	}
291	#endif
292
293	(void) alarm(delay);
294	}
295
296
297
298	/*
299	* Clear timeout:
300	* - cancel the timeout if it's not fired
301	* - set state to READY
302	*/
303	void clear_timeout(timeout_t *timeout) {
304	assert(timeout == &the_timeout);
305
306	// TODO: Check whether we should block the signals here?
307	if (the_timeout.state == TIMEOUT_ACTIVE) {
308	// not fired;
309	the_timeout.state = TIMEOUT_CANCELED;
310	(void) alarm(0); // cancel the alarm
311	}
312	the_timeout.state = TIMEOUT_READY;
313	}
314
315
316	/*
317	* Final cleanup:
318	* - cancel the timeout if it's active
319	* - restore the original handler
320	*/
321	void delete_timeout(timeout_t *timeout) {
322	assert(timeout == &the_timeout);
323
324	if (the_timeout.state == TIMEOUT_ACTIVE) {
325	(void) alarm(0);
326	}
327	(void) signal(SIGALRM, saved_handler);
328	the_timeout.state = TIMEOUT_NOT_READY;
329	}
330
331	#endif /* defined(THREAD_SAFE) */
332
333	#else
334
335
336	/************************************
337	* WINDOWS/MINGW IMPLEMENTATION *
338	***********************************/
339
340	#include <inttypes.h>
341	#include <stdio.h>
342	#include <stdlib.h>
343
344	/*
345	* Callback function for the timer
346	* - do nothing if the timeout is not active
347	* - otherwise change the state to fired and
348	* call the handler.
349	*/
350	static VOID CALLBACK timer_callback(PVOID param, BOOLEAN timer_or_wait_fired) {
351	timeout_t timeout = (timeout_t ) param;
352
353	if (timeout->state == TIMEOUT_ACTIVE) {
354	timeout->state = TIMEOUT_FIRED;
355	timeout->handler(timeout->param);
356	}
357	}
358
359
360	/*
361	* Initialization:
362	* - create the timer queue
363	*/
364	timeout_t *init_timeout(void) {
365	timeout_t timeout = (timeout_t ) safe_malloc(sizeof(timeout_t));
366
367	init_base_timeout(timeout);
368
369	timeout->timer_queue = CreateTimerQueue();
370	if (timeout->timer_queue == NULL) {
371	fprintf(stderr, "Yices: CreateTimerQueue failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
372	fflush(stderr);
373	exit(YICES_EXIT_INTERNAL_ERROR);
374	}
375
376	timeout->timer = NULL;
377
378	return timeout;
379	}
380
381
382
383	/*
384	* Activate:
385	* - delay = timeout in seconds (must be positive)
386	* - handler = handler to call if fired
387	* - param = parameter for the handler
388	*/
389	void start_timeout(timeout_t timeout, uint32_t delay, timeout_handler_t handler, void param) {
390	DWORD duetime;
391
392	assert(delay > 0 && timeout->state == TIMEOUT_READY && handler != NULL);
393
394	duetime = delay * 1000; // delay in milliseconds
395	if (CreateTimerQueueTimer(&timeout->timer,
396	timeout->timer_queue,
397	(WAITORTIMERCALLBACK) timer_callback,
398	timeout, duetime,
399	/Period=/0,
400	/Flags=/WT_EXECUTEDEFAULT)) {
401	// timer created
402	timeout->state = TIMEOUT_ACTIVE;
403	timeout->handler = handler;
404	timeout->param = param;
405	} else {
406	fprintf(stderr, "Yices: CreateTimerQueueTimer failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
407	fflush(stderr);
408	exit(YICES_EXIT_INTERNAL_ERROR);
409	}
410	}
411
412
413
414	/*
415	* Delete the timer
416	*/
417	void clear_timeout(timeout_t *timeout) {
418	// GetLastError returns DWORD, which is an unsigned 32bit integer
419	uint32_t error_code;
420
421	if (timeout->state == TIMEOUT_ACTIVE \|\| timeout->state == TIMEOUT_FIRED) {
422	if (timeout->state == TIMEOUT_ACTIVE) {
423	// active and not fired yet
424	timeout->state = TIMEOUT_CANCELED; // will prevent call to handle
425	}
426
427	/*
428	* We give NULL as CompletionEvent so timer_callback will complete
429	* if the timer has fired. That's fine as the timeout state is not
430	* active anymore so the timer_callback does nothing.
431	*
432	* Second try: give INVALID_HANDLE_VALUE?
433	* This causes SEG FAULT in ntdll.dll
434	*/
435	if (! DeleteTimerQueueTimer(timeout->timer_queue, timeout->timer,
436	INVALID_HANDLE_VALUE)) {
437	error_code = (uint32_t) GetLastError();
438	// The Microsoft doc says we should try again
439	// unless error code is ERROR_IO_PENDING??
440	fprintf(stderr, "Yices: DeleteTimerQueueTimer failed with error code %"PRIu32"\n", error_code);
441	fflush(stderr);
442	exit(YICES_EXIT_INTERNAL_ERROR);
443	}
444	}
445
446	timeout->state = TIMEOUT_READY;
447	}
448
449
450
451	/*
452	* Final cleanup:
453	* - delete the timer_queue
454	*/
455	void delete_timeout(timeout_t *timeout) {
456	if (! DeleteTimerQueueEx(timeout->timer_queue, INVALID_HANDLE_VALUE)) {
457	fprintf(stderr, "Yices: DeleteTimerQueueEx failed with error code %"PRIu32"\n", (uint32_t) GetLastError());
458	fflush(stderr);
459	exit(YICES_EXIT_INTERNAL_ERROR);
460	}
461
462	safe_free(timeout);
463	}
464
465
466
467
468	#endif /* MINGW */

SRI-CSL / yices2 / 16032530443

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous