1 /* Copyright (c) 2008-2013. The SimGrid Team.
2 * All rights reserved. */
4 /* This program is free software; you can redistribute it and/or modify it
5 * under the terms of the license (GNU LGPL) which comes with this package. */
13 #include "simgrid/sg_config.h"
14 #include "../surf/surf_private.h"
15 #include "../simix/smx_private.h"
16 #include "../xbt/mmalloc/mmprivate.h"
18 #include "mc_private.h"
19 #include "xbt/automaton.h"
22 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
23 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
24 "Logging specific to MC (global)");
26 /* Configuration support */
27 e_mc_reduce_t mc_reduce_kind=e_mc_reduce_unset;
29 int _sg_do_model_check = 0;
30 int _sg_mc_checkpoint=0;
31 char* _sg_mc_property_file=NULL;
34 int _sg_mc_max_depth=1000;
36 char *_sg_mc_dot_output_file = NULL;
38 int user_max_depth_reached = 0;
40 void _mc_cfg_cb_reduce(const char *name, int pos) {
41 if (_sg_cfg_init_status && !_sg_do_model_check) {
42 xbt_die("You are specifying a reduction strategy after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
44 char *val= xbt_cfg_get_string(_sg_cfg_set, name);
45 if (!strcasecmp(val,"none")) {
46 mc_reduce_kind = e_mc_reduce_none;
47 } else if (!strcasecmp(val,"dpor")) {
48 mc_reduce_kind = e_mc_reduce_dpor;
50 xbt_die("configuration option %s can only take 'none' or 'dpor' as a value",name);
54 void _mc_cfg_cb_checkpoint(const char *name, int pos) {
55 if (_sg_cfg_init_status && !_sg_do_model_check) {
56 xbt_die("You are specifying a checkpointing value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
58 _sg_mc_checkpoint = xbt_cfg_get_int(_sg_cfg_set, name);
60 void _mc_cfg_cb_property(const char *name, int pos) {
61 if (_sg_cfg_init_status && !_sg_do_model_check) {
62 xbt_die("You are specifying a property after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
64 _sg_mc_property_file= xbt_cfg_get_string(_sg_cfg_set, name);
67 void _mc_cfg_cb_timeout(const char *name, int pos) {
68 if (_sg_cfg_init_status && !_sg_do_model_check) {
69 xbt_die("You are specifying a value to enable/disable timeout for wait requests after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
71 _sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
74 void _mc_cfg_cb_hash(const char *name, int pos) {
75 if (_sg_cfg_init_status && !_sg_do_model_check) {
76 xbt_die("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
78 _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name);
81 void _mc_cfg_cb_max_depth(const char *name, int pos) {
82 if (_sg_cfg_init_status && !_sg_do_model_check) {
83 xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
85 _sg_mc_max_depth= xbt_cfg_get_int(_sg_cfg_set, name);
88 void _mc_cfg_cb_visited(const char *name, int pos) {
89 if (_sg_cfg_init_status && !_sg_do_model_check) {
90 xbt_die("You are specifying a number of stored visited states after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
92 _sg_mc_visited= xbt_cfg_get_int(_sg_cfg_set, name);
95 void _mc_cfg_cb_dot_output(const char *name, int pos) {
96 if (_sg_cfg_init_status && !_sg_do_model_check) {
97 xbt_die("You are specifying a file name for a dot output of graph state after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
99 _sg_mc_dot_output_file= xbt_cfg_get_string(_sg_cfg_set, name);
102 /* MC global data structures */
103 mc_state_t mc_current_state = NULL;
104 char mc_replay_mode = FALSE;
105 double *mc_time = NULL;
106 __thread mc_comparison_times_t mc_comp_times = NULL;
107 __thread double mc_snapshot_comparison_time;
108 mc_stats_t mc_stats = NULL;
111 xbt_fifo_t mc_stack_safety = NULL;
112 mc_global_t initial_state_safety = NULL;
115 xbt_fifo_t mc_stack_liveness = NULL;
116 mc_global_t initial_state_liveness = NULL;
119 xbt_automaton_t _mc_property_automaton = NULL;
122 mc_object_info_t mc_libsimgrid_info = NULL;
123 mc_object_info_t mc_binary_info = NULL;
125 /* Ignore mechanism */
126 extern xbt_dynar_t mc_heap_comparison_ignore;
127 extern xbt_dynar_t stacks_areas;
130 FILE *dot_output = NULL;
131 const char* colors[13];
134 /******************************* DWARF Information *******************************/
135 /**********************************************************************************/
137 /************************** Free functions *************************/
139 static void dw_location_free(dw_location_t l){
141 if(l->type == e_dw_loclist)
142 xbt_dynar_free(&(l->location.loclist));
143 else if(l->type == e_dw_compose)
144 xbt_dynar_free(&(l->location.compose));
145 else if(l->type == e_dw_arithmetic)
146 xbt_free(l->location.arithmetic);
152 static void dw_location_entry_free(dw_location_entry_t e){
153 dw_location_free(e->location);
157 void dw_type_free(dw_type_t t){
159 xbt_free(t->dw_type_id);
160 xbt_dynar_free(&(t->members));
164 static void dw_type_free_voidp(void *t){
165 dw_type_free((dw_type_t) * (void **) t);
168 void dw_variable_free(dw_variable_t v){
171 xbt_free(v->type_origin);
173 dw_location_free(v->location);
178 void dw_variable_free_voidp(void *t){
179 dw_variable_free((dw_variable_t) * (void **) t);
184 mc_object_info_t MC_new_object_info(void) {
185 mc_object_info_t res = xbt_new0(s_mc_object_info_t, 1);
186 res->local_variables = xbt_dict_new_homogeneous(NULL);
187 res->global_variables = xbt_dynar_new(sizeof(dw_variable_t), dw_variable_free_voidp);
188 res->types = xbt_dict_new_homogeneous(NULL);
189 res->types_by_name = xbt_dict_new_homogeneous(NULL);
194 void MC_free_object_info(mc_object_info_t* info) {
195 xbt_free(&(*info)->file_name);
196 xbt_dict_free(&(*info)->local_variables);
197 xbt_dynar_free(&(*info)->global_variables);
198 xbt_dict_free(&(*info)->types);
199 xbt_dict_free(&(*info)->types_by_name);
201 xbt_dynar_free(&(*info)->functions_index);
207 void* MC_object_base_address(mc_object_info_t info) {
208 void* result = info->start_exec;
209 if(info->start_rw!=NULL && result > (void*) info->start_rw) result = info->start_rw;
210 if(info->start_ro!=NULL && result > (void*) info->start_ro) result = info->start_ro;
214 // ***** Functions index
216 static int MC_compare_frame_index_items(mc_function_index_item_t a, mc_function_index_item_t b) {
217 if(a->low_pc < b->low_pc)
219 else if(a->low_pc == b->low_pc)
225 static void MC_make_functions_index(mc_object_info_t info) {
226 xbt_dynar_t index = xbt_dynar_new(sizeof(s_mc_function_index_item_t), NULL);
228 // The base address of the function must be used to offset the addresses.
229 // This should be fixed this in the frame_t structure instead.
230 // Relocated addresses are offset for shared objets and constant for executables objects.
231 // See DWARF4 spec 7.5
232 void* offset = info->flags & MC_OBJECT_INFO_EXECUTABLE ? 0 : MC_object_base_address(info);
234 // Populate the array:
235 dw_frame_t frame = NULL;
236 xbt_dict_cursor_t cursor = NULL;
237 const char* name = NULL;
238 xbt_dict_foreach(info->local_variables, cursor, name, frame) {
239 if(frame->low_pc==NULL)
241 s_mc_function_index_item_t entry;
242 entry.low_pc = (char*) frame->low_pc + (unsigned long) offset;
243 entry.high_pc = (char*) frame->high_pc + (unsigned long) offset;
244 entry.function = frame;
245 xbt_dynar_push(index, &entry);
248 mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(index, 0);
250 // Sort the array by low_pc:
252 xbt_dynar_length(index),
253 sizeof(s_mc_function_index_item_t),
254 (int (*)(const void *, const void *))MC_compare_frame_index_items);
256 info->functions_index = index;
259 mc_object_info_t MC_ip_find_object_info(void* ip) {
260 mc_object_info_t infos[2] = { mc_binary_info, mc_libsimgrid_info };
263 for(i=0; i!=n; ++i) {
264 if(ip >= (void*)infos[i]->start_exec && ip <= (void*)infos[i]->end_exec) {
271 static dw_frame_t MC_find_function_by_ip_and_object(void* ip, mc_object_info_t info) {
272 xbt_dynar_t dynar = info->functions_index;
273 mc_function_index_item_t base = (mc_function_index_item_t) xbt_dynar_get_ptr(dynar, 0);
275 int j = xbt_dynar_length(dynar) - 1;
277 int k = i + ((j-i)/2);
278 if(ip < base[k].low_pc) {
280 } else if(ip > base[k].high_pc) {
283 return base[k].function;
289 dw_frame_t MC_find_function_by_ip(void* ip) {
290 mc_object_info_t info = MC_ip_find_object_info(ip);
294 return MC_find_function_by_ip_and_object(ip, info);
297 /** \brief Finds informations about a given shared object/executable */
298 mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable) {
299 mc_object_info_t result = MC_new_object_info();
301 result->flags |= MC_OBJECT_INFO_EXECUTABLE;
302 result->file_name = xbt_strdup(name);
303 MC_find_object_address(maps, result);
304 MC_dwarf_get_variables(result);
305 MC_post_process_types(result);
306 MC_make_functions_index(result);
310 /*************************************************************************/
312 static dw_location_t MC_dwarf_get_location(xbt_dict_t location_list, char *expr){
314 dw_location_t loc = xbt_new0(s_dw_location_t, 1);
316 if(location_list != NULL){
318 char *key = bprintf("%d", (int)strtoul(expr, NULL, 16));
319 loc->type = e_dw_loclist;
320 loc->location.loclist = (xbt_dynar_t)xbt_dict_get_or_null(location_list, key);
321 if(loc->location.loclist == NULL)
322 XBT_INFO("Key not found in loclist");
329 char *tok = NULL, *tok2 = NULL;
331 xbt_dynar_t tokens1 = xbt_str_split(expr, ";");
334 loc->type = e_dw_compose;
335 loc->location.compose = xbt_dynar_new(sizeof(dw_location_t), NULL);
337 while(cursor < xbt_dynar_length(tokens1)){
339 tok = xbt_dynar_get_as(tokens1, cursor, char*);
340 tokens2 = xbt_str_split(tok, " ");
341 tok2 = xbt_dynar_get_as(tokens2, 0, char*);
343 if(strncmp(tok2, "DW_OP_reg", 9) == 0){
344 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
345 new_element->type = e_dw_register;
346 new_element->location.reg = atoi(strtok(tok2, "DW_OP_reg"));
347 xbt_dynar_push(loc->location.compose, &new_element);
348 }else if(strcmp(tok2, "DW_OP_fbreg:") == 0){
349 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
350 new_element->type = e_dw_fbregister_op;
351 new_element->location.fbreg_op = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
352 xbt_dynar_push(loc->location.compose, &new_element);
353 }else if(strncmp(tok2, "DW_OP_breg", 10) == 0){
354 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
355 new_element->type = e_dw_bregister_op;
356 new_element->location.breg_op.reg = atoi(strtok(tok2, "DW_OP_breg"));
357 new_element->location.breg_op.offset = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
358 xbt_dynar_push(loc->location.compose, &new_element);
359 }else if(strncmp(tok2, "DW_OP_lit", 9) == 0){
360 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
361 new_element->type = e_dw_lit;
362 new_element->location.lit = atoi(strtok(tok2, "DW_OP_lit"));
363 xbt_dynar_push(loc->location.compose, &new_element);
364 }else if(strcmp(tok2, "DW_OP_piece:") == 0){
365 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
366 new_element->type = e_dw_piece;
367 new_element->location.piece = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
368 xbt_dynar_push(loc->location.compose, &new_element);
369 }else if(strcmp(tok2, "DW_OP_plus_uconst:") == 0){
370 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
371 new_element->type = e_dw_plus_uconst;
372 new_element->location.plus_uconst = atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char *));
373 xbt_dynar_push(loc->location.compose, &new_element);
374 }else if(strcmp(tok, "DW_OP_abs") == 0 ||
375 strcmp(tok, "DW_OP_and") == 0 ||
376 strcmp(tok, "DW_OP_div") == 0 ||
377 strcmp(tok, "DW_OP_minus") == 0 ||
378 strcmp(tok, "DW_OP_mod") == 0 ||
379 strcmp(tok, "DW_OP_mul") == 0 ||
380 strcmp(tok, "DW_OP_neg") == 0 ||
381 strcmp(tok, "DW_OP_not") == 0 ||
382 strcmp(tok, "DW_OP_or") == 0 ||
383 strcmp(tok, "DW_OP_plus") == 0){
384 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
385 new_element->type = e_dw_arithmetic;
386 new_element->location.arithmetic = strdup(strtok(tok2, "DW_OP_"));
387 xbt_dynar_push(loc->location.compose, &new_element);
388 }else if(strcmp(tok, "DW_OP_stack_value") == 0){
389 }else if(strcmp(tok2, "DW_OP_deref_size:") == 0){
390 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
391 new_element->type = e_dw_deref;
392 new_element->location.deref_size = (unsigned int short) atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*));
393 xbt_dynar_push(loc->location.compose, &new_element);
394 }else if(strcmp(tok, "DW_OP_deref") == 0){
395 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
396 new_element->type = e_dw_deref;
397 new_element->location.deref_size = sizeof(void *);
398 xbt_dynar_push(loc->location.compose, &new_element);
399 }else if(strcmp(tok2, "DW_OP_constu:") == 0){
400 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
401 new_element->type = e_dw_uconstant;
402 new_element->location.uconstant.bytes = 1;
403 new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
404 xbt_dynar_push(loc->location.compose, &new_element);
405 }else if(strcmp(tok2, "DW_OP_consts:") == 0){
406 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
407 new_element->type = e_dw_sconstant;
408 new_element->location.sconstant.bytes = 1;
409 new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
410 xbt_dynar_push(loc->location.compose, &new_element);
411 }else if(strcmp(tok2, "DW_OP_const1u:") == 0 ||
412 strcmp(tok2, "DW_OP_const2u:") == 0 ||
413 strcmp(tok2, "DW_OP_const4u:") == 0 ||
414 strcmp(tok2, "DW_OP_const8u:") == 0){
415 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
416 new_element->type = e_dw_uconstant;
417 new_element->location.uconstant.bytes = tok2[11] - '0';
418 new_element->location.uconstant.value = (unsigned long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
419 xbt_dynar_push(loc->location.compose, &new_element);
420 }else if(strcmp(tok, "DW_OP_const1s") == 0 ||
421 strcmp(tok, "DW_OP_const2s") == 0 ||
422 strcmp(tok, "DW_OP_const4s") == 0 ||
423 strcmp(tok, "DW_OP_const8s") == 0){
424 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
425 new_element->type = e_dw_sconstant;
426 new_element->location.sconstant.bytes = tok2[11] - '0';
427 new_element->location.sconstant.value = (long int)(atoi(xbt_dynar_get_as(tokens2, xbt_dynar_length(tokens2) - 1, char*)));
428 xbt_dynar_push(loc->location.compose, &new_element);
430 dw_location_t new_element = xbt_new0(s_dw_location_t, 1);
431 new_element->type = e_dw_unsupported;
432 xbt_dynar_push(loc->location.compose, &new_element);
436 xbt_dynar_free(&tokens2);
440 xbt_dynar_free(&tokens1);
449 /** \brief Finds a frame (DW_TAG_subprogram) from an DWARF offset in the rangd of this subprogram
451 * The offset can be an offset of a child DW_TAG_variable.
453 static dw_frame_t MC_dwarf_get_frame_by_offset(xbt_dict_t all_variables, unsigned long int offset){
455 xbt_dict_cursor_t cursor = NULL;
459 xbt_dict_foreach(all_variables, cursor, name, res) {
460 if(offset >= res->start && offset < res->end){
461 xbt_dict_cursor_free(&cursor);
466 xbt_dict_cursor_free(&cursor);
471 static dw_variable_t MC_dwarf_get_variable_by_name(dw_frame_t frame, char *var){
473 unsigned int cursor = 0;
474 dw_variable_t current_var;
476 xbt_dynar_foreach(frame->variables, cursor, current_var){
477 if(strcmp(var, current_var->name) == 0)
484 static int MC_dwarf_get_variable_index(xbt_dynar_t variables, char* var, void *address){
486 if(xbt_dynar_is_empty(variables))
489 unsigned int cursor = 0;
491 int end = xbt_dynar_length(variables) - 1;
492 dw_variable_t var_test = NULL;
495 cursor = (start + end) / 2;
496 var_test = (dw_variable_t)xbt_dynar_get_as(variables, cursor, dw_variable_t);
497 if(strcmp(var_test->name, var) < 0){
499 }else if(strcmp(var_test->name, var) > 0){
502 if(address){ /* global variable */
503 if(var_test->address == address)
505 if(var_test->address > address)
509 }else{ /* local variable */
515 if(strcmp(var_test->name, var) == 0){
516 if(address && var_test->address < address)
520 }else if(strcmp(var_test->name, var) < 0)
527 void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable) {
528 int index = MC_dwarf_get_variable_index(info->global_variables, variable->name, variable->address);
530 xbt_dynar_insert_at(info->global_variables, index, &variable);
534 void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
535 xbt_assert(frame, "Frame is NULL");
536 int index = MC_dwarf_get_variable_index(frame->variables, variable->name, NULL);
538 xbt_dynar_insert_at(frame->variables, index, &variable);
542 void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable) {
544 MC_dwarf_register_global_variable(info, variable);
546 xbt_die("No frame for this local variable");
548 MC_dwarf_register_non_global_variable(info, frame, variable);
552 /******************************* Ignore mechanism *******************************/
553 /*********************************************************************************/
555 xbt_dynar_t mc_checkpoint_ignore;
557 typedef struct s_mc_stack_ignore_variable{
560 }s_mc_stack_ignore_variable_t, *mc_stack_ignore_variable_t;
562 /**************************** Free functions ******************************/
564 static void stack_ignore_variable_free(mc_stack_ignore_variable_t v){
565 xbt_free(v->var_name);
570 static void stack_ignore_variable_free_voidp(void *v){
571 stack_ignore_variable_free((mc_stack_ignore_variable_t) * (void **) v);
574 void heap_ignore_region_free(mc_heap_ignore_region_t r){
578 void heap_ignore_region_free_voidp(void *r){
579 heap_ignore_region_free((mc_heap_ignore_region_t) * (void **) r);
582 static void checkpoint_ignore_region_free(mc_checkpoint_ignore_region_t r){
586 static void checkpoint_ignore_region_free_voidp(void *r){
587 checkpoint_ignore_region_free((mc_checkpoint_ignore_region_t) * (void **) r);
590 /***********************************************************************/
592 void MC_ignore_heap(void *address, size_t size){
594 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
598 mc_heap_ignore_region_t region = NULL;
599 region = xbt_new0(s_mc_heap_ignore_region_t, 1);
600 region->address = address;
603 region->block = ((char*)address - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
605 if(((xbt_mheap_t)std_heap)->heapinfo[region->block].type == 0){
606 region->fragment = -1;
607 ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_block.ignore++;
609 region->fragment = ((uintptr_t) (ADDR2UINT (address) % (BLOCKSIZE))) >> ((xbt_mheap_t)std_heap)->heapinfo[region->block].type;
610 ((xbt_mheap_t)std_heap)->heapinfo[region->block].busy_frag.ignore[region->fragment]++;
613 if(mc_heap_comparison_ignore == NULL){
614 mc_heap_comparison_ignore = xbt_dynar_new(sizeof(mc_heap_ignore_region_t), heap_ignore_region_free_voidp);
615 xbt_dynar_push(mc_heap_comparison_ignore, ®ion);
621 unsigned int cursor = 0;
622 mc_heap_ignore_region_t current_region = NULL;
624 int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
627 cursor = (start + end) / 2;
628 current_region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
629 if(current_region->address == address){
630 heap_ignore_region_free(region);
634 }else if(current_region->address < address){
641 if(current_region->address < address)
642 xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor + 1, ®ion);
644 xbt_dynar_insert_at(mc_heap_comparison_ignore, cursor, ®ion);
650 void MC_remove_ignore_heap(void *address, size_t size){
652 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
656 unsigned int cursor = 0;
658 int end = xbt_dynar_length(mc_heap_comparison_ignore) - 1;
659 mc_heap_ignore_region_t region;
660 int ignore_found = 0;
663 cursor = (start + end) / 2;
664 region = (mc_heap_ignore_region_t)xbt_dynar_get_as(mc_heap_comparison_ignore, cursor, mc_heap_ignore_region_t);
665 if(region->address == address){
668 }else if(region->address < address){
671 if((char * )region->address <= ((char *)address + size)){
680 if(ignore_found == 1){
681 xbt_dynar_remove_at(mc_heap_comparison_ignore, cursor, NULL);
682 MC_remove_ignore_heap(address, size);
690 void MC_ignore_global_variable(const char *name){
692 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
696 xbt_assert(mc_libsimgrid_info, "MC subsystem not initialized");
698 unsigned int cursor = 0;
699 dw_variable_t current_var;
701 int end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
704 cursor = (start + end) /2;
705 current_var = (dw_variable_t)xbt_dynar_get_as(mc_libsimgrid_info->global_variables, cursor, dw_variable_t);
706 if(strcmp(current_var->name, name) == 0){
707 xbt_dynar_remove_at(mc_libsimgrid_info->global_variables, cursor, NULL);
709 end = xbt_dynar_length(mc_libsimgrid_info->global_variables) - 1;
710 }else if(strcmp(current_var->name, name) < 0){
721 void MC_ignore_local_variable(const char *var_name, const char *frame_name){
723 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
727 unsigned int cursor = 0;
728 dw_variable_t current_var;
730 if(strcmp(frame_name, "*") == 0){ /* Remove variable in all frames */
731 xbt_dict_cursor_t dict_cursor;
732 char *current_frame_name;
734 xbt_dict_foreach(mc_libsimgrid_info->local_variables, dict_cursor, current_frame_name, frame){
736 end = xbt_dynar_length(frame->variables) - 1;
738 cursor = (start + end) / 2;
739 current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
740 if(strcmp(current_var->name, var_name) == 0){
741 xbt_dynar_remove_at(frame->variables, cursor, NULL);
743 end = xbt_dynar_length(frame->variables) - 1;
744 }else if(strcmp(current_var->name, var_name) < 0){
751 xbt_dict_foreach(mc_binary_info->local_variables, dict_cursor, current_frame_name, frame){
753 end = xbt_dynar_length(frame->variables) - 1;
755 cursor = (start + end) / 2;
756 current_var = (dw_variable_t)xbt_dynar_get_as(frame->variables, cursor, dw_variable_t);
757 if(strcmp(current_var->name, var_name) == 0){
758 xbt_dynar_remove_at(frame->variables, cursor, NULL);
760 end = xbt_dynar_length(frame->variables) - 1;
761 }else if(strcmp(current_var->name, var_name) < 0){
769 xbt_dynar_t variables_list = ((dw_frame_t)xbt_dict_get_or_null(
770 mc_libsimgrid_info->local_variables, frame_name))->variables;
772 end = xbt_dynar_length(variables_list) - 1;
774 cursor = (start + end) / 2;
775 current_var = (dw_variable_t)xbt_dynar_get_as(variables_list, cursor, dw_variable_t);
776 if(strcmp(current_var->name, var_name) == 0){
777 xbt_dynar_remove_at(variables_list, cursor, NULL);
779 end = xbt_dynar_length(variables_list) - 1;
780 }else if(strcmp(current_var->name, var_name) < 0){
793 void MC_new_stack_area(void *stack, char *name, void* context, size_t size){
795 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
799 if(stacks_areas == NULL)
800 stacks_areas = xbt_dynar_new(sizeof(stack_region_t), NULL);
802 stack_region_t region = NULL;
803 region = xbt_new0(s_stack_region_t, 1);
804 region->address = stack;
805 region->process_name = strdup(name);
806 region->context = context;
808 region->block = ((char*)stack - (char*)((xbt_mheap_t)std_heap)->heapbase) / BLOCKSIZE + 1;
809 xbt_dynar_push(stacks_areas, ®ion);
815 void MC_ignore(void *addr, size_t size){
817 int raw_mem_set= (mmalloc_get_current_heap() == raw_heap);
821 if(mc_checkpoint_ignore == NULL)
822 mc_checkpoint_ignore = xbt_dynar_new(sizeof(mc_checkpoint_ignore_region_t), checkpoint_ignore_region_free_voidp);
824 mc_checkpoint_ignore_region_t region = xbt_new0(s_mc_checkpoint_ignore_region_t, 1);
828 if(xbt_dynar_is_empty(mc_checkpoint_ignore)){
829 xbt_dynar_push(mc_checkpoint_ignore, ®ion);
832 unsigned int cursor = 0;
834 int end = xbt_dynar_length(mc_checkpoint_ignore) -1;
835 mc_checkpoint_ignore_region_t current_region = NULL;
838 cursor = (start + end) / 2;
839 current_region = (mc_checkpoint_ignore_region_t)xbt_dynar_get_as(mc_checkpoint_ignore, cursor, mc_checkpoint_ignore_region_t);
840 if(current_region->addr == addr){
841 if(current_region->size == size){
842 checkpoint_ignore_region_free(region);
846 }else if(current_region->size < size){
851 }else if(current_region->addr < addr){
858 if(current_region->addr == addr){
859 if(current_region->size < size){
860 xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion);
862 xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion);
864 }else if(current_region->addr < addr){
865 xbt_dynar_insert_at(mc_checkpoint_ignore, cursor + 1, ®ion);
867 xbt_dynar_insert_at(mc_checkpoint_ignore, cursor, ®ion);
875 /******************************* Initialisation of MC *******************************/
876 /*********************************************************************************/
878 static void MC_init_debug_info();
879 static void MC_init_debug_info() {
880 XBT_INFO("Get debug information ...");
882 memory_map_t maps = MC_get_memory_map();
884 /* Get local variables for state equality detection */
885 mc_binary_info = MC_find_object_info(maps, xbt_binary_name, 1);
886 mc_libsimgrid_info = MC_find_object_info(maps, libsimgrid_path, 0);
888 MC_free_memory_map(maps);
889 XBT_INFO("Get debug information done !");
894 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
898 /* Initialize the data structures that must be persistent across every
899 iteration of the model-checker (in RAW memory) */
903 MC_init_memory_map_info();
904 MC_init_debug_info();
907 parmap = xbt_parmap_mc_new(xbt_os_get_numcores(), XBT_PARMAP_DEFAULT);
911 /* Ignore some variables from xbt/ex.h used by exception e for stacks comparison */
912 MC_ignore_local_variable("e", "*");
913 MC_ignore_local_variable("__ex_cleanup", "*");
914 MC_ignore_local_variable("__ex_mctx_en", "*");
915 MC_ignore_local_variable("__ex_mctx_me", "*");
916 MC_ignore_local_variable("__xbt_ex_ctx_ptr", "*");
917 MC_ignore_local_variable("_log_ev", "*");
918 MC_ignore_local_variable("_throw_ctx", "*");
919 MC_ignore_local_variable("ctx", "*");
921 MC_ignore_local_variable("next_context", "smx_ctx_sysv_suspend_serial");
922 MC_ignore_local_variable("i", "smx_ctx_sysv_suspend_serial");
924 /* Ignore local variable about time used for tracing */
925 MC_ignore_local_variable("start_time", "*");
927 MC_ignore_global_variable("mc_comp_times");
928 MC_ignore_global_variable("mc_snapshot_comparison_time");
929 MC_ignore_global_variable("mc_time");
930 MC_ignore_global_variable("smpi_current_rank");
931 MC_ignore_global_variable("counter"); /* Static variable used for tracing */
932 MC_ignore_global_variable("maestro_stack_start");
933 MC_ignore_global_variable("maestro_stack_end");
934 MC_ignore_global_variable("smx_total_comms");
936 MC_ignore_heap(&(simix_global->process_to_run), sizeof(simix_global->process_to_run));
937 MC_ignore_heap(&(simix_global->process_that_ran), sizeof(simix_global->process_that_ran));
938 MC_ignore_heap(simix_global->process_to_run, sizeof(*(simix_global->process_to_run)));
939 MC_ignore_heap(simix_global->process_that_ran, sizeof(*(simix_global->process_that_ran)));
941 smx_process_t process;
942 xbt_swag_foreach(process, simix_global->process_list){
943 MC_ignore_heap(&(process->process_hookup), sizeof(process->process_hookup));
951 static void MC_init_dot_output(){ /* FIXME : more colors */
955 colors[2] = "green3";
956 colors[3] = "goldenrod";
958 colors[5] = "purple";
959 colors[6] = "magenta";
960 colors[7] = "turquoise4";
961 colors[8] = "gray25";
962 colors[9] = "forestgreen";
963 colors[10] = "hotpink";
964 colors[11] = "lightblue";
967 dot_output = fopen(_sg_mc_dot_output_file, "w");
969 if(dot_output == NULL){
970 perror("Error open dot output file");
974 fprintf(dot_output, "digraph graphname{\n fixedsize=true; rankdir=TB; ranksep=.25; edge [fontsize=12]; node [fontsize=10, shape=circle,width=.5 ]; graph [resolution=20, fontsize=10];\n");
978 /******************************* Core of MC *******************************/
979 /**************************************************************************/
981 void MC_do_the_modelcheck_for_real() {
984 mc_comp_times = xbt_new0(s_mc_comparison_times_t, 1);
987 if (!_sg_mc_property_file || _sg_mc_property_file[0]=='\0') {
988 if (mc_reduce_kind==e_mc_reduce_unset)
989 mc_reduce_kind=e_mc_reduce_dpor;
991 XBT_INFO("Check a safety property");
992 MC_modelcheck_safety();
996 if (mc_reduce_kind==e_mc_reduce_unset)
997 mc_reduce_kind=e_mc_reduce_none;
999 XBT_INFO("Check the liveness property %s",_sg_mc_property_file);
1000 MC_automaton_load(_sg_mc_property_file);
1001 MC_modelcheck_liveness();
1005 void MC_modelcheck_safety(void)
1007 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1009 /* Check if MC is already initialized */
1010 if (initial_state_safety)
1013 mc_time = xbt_new0(double, simix_process_maxpid);
1015 /* mc_time refers to clock for each process -> ignore it for heap comparison */
1016 MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1018 /* Initialize the data structures that must be persistent across every
1019 iteration of the model-checker (in RAW memory) */
1023 /* Initialize statistics */
1024 mc_stats = xbt_new0(s_mc_stats_t, 1);
1025 mc_stats->state_size = 1;
1027 /* Create exploration stack */
1028 mc_stack_safety = xbt_fifo_new();
1030 if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1031 MC_init_dot_output();
1035 if(_sg_mc_visited > 0){
1039 MC_init_memory_map_info();
1040 MC_init_debug_info();
1047 /* Save the initial state */
1048 initial_state_safety = xbt_new0(s_mc_global_t, 1);
1049 initial_state_safety->snapshot = MC_take_snapshot(0);
1050 initial_state_safety->initial_communications_pattern_done = 0;
1051 initial_state_safety->comm_deterministic = 1;
1052 initial_state_safety->send_deterministic = 1;
1064 void MC_modelcheck_liveness(){
1066 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1070 mc_time = xbt_new0(double, simix_process_maxpid);
1072 /* mc_time refers to clock for each process -> ignore it for heap comparison */
1073 MC_ignore_heap(mc_time, simix_process_maxpid * sizeof(double));
1077 /* Initialize statistics */
1078 mc_stats = xbt_new0(s_mc_stats_t, 1);
1079 mc_stats->state_size = 1;
1081 /* Create exploration stack */
1082 mc_stack_liveness = xbt_fifo_new();
1084 /* Create the initial state */
1085 initial_state_liveness = xbt_new0(s_mc_global_t, 1);
1087 if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0'))
1088 MC_init_dot_output();
1095 MC_print_statistics(mc_stats);
1112 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max){
1114 return simcall->mc_value;
1118 int MC_random(int min, int max)
1120 /*FIXME: return mc_current_state->executed_transition->random.value;*/
1121 return simcall_mc_random(min, max);
1125 * \brief Schedules all the process that are ready to run
1127 void MC_wait_for_requests(void)
1129 smx_process_t process;
1133 while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
1134 SIMIX_process_runall();
1135 xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
1136 req = &process->simcall;
1137 if (req->call != SIMCALL_NONE && !MC_request_is_visible(req))
1138 SIMIX_simcall_pre(req, 0);
1143 int MC_deadlock_check()
1145 int deadlock = FALSE;
1146 smx_process_t process;
1147 if(xbt_swag_size(simix_global->process_list)){
1149 xbt_swag_foreach(process, simix_global->process_list){
1150 if(process->simcall.call != SIMCALL_NONE
1151 && MC_request_is_enabled(&process->simcall)){
1161 * \brief Re-executes from the state at position start all the transitions indicated by
1162 * a given model-checker stack.
1163 * \param stack The stack with the transitions to execute.
1164 * \param start Start index to begin the re-execution.
1166 void MC_replay(xbt_fifo_t stack, int start)
1168 int raw_mem = (mmalloc_get_current_heap() == raw_heap);
1170 int value, i = 1, count = 1;
1172 smx_simcall_t req = NULL, saved_req = NULL;
1173 xbt_fifo_item_t item, start_item;
1175 smx_process_t process = NULL;
1176 int comm_pattern = 0;
1178 XBT_DEBUG("**** Begin Replay ****");
1181 /* Restore the initial state */
1182 MC_restore_snapshot(initial_state_safety->snapshot);
1183 /* At the moment of taking the snapshot the raw heap was set, so restoring
1184 * it will set it back again, we have to unset it to continue */
1188 start_item = xbt_fifo_get_last_item(stack);
1191 start_item = xbt_fifo_get_prev_item(start_item);
1197 xbt_dict_reset(first_enabled_state);
1198 xbt_swag_foreach(process, simix_global->process_list){
1199 if(MC_process_is_enabled(process)){
1200 char *key = bprintf("%lu", process->pid);
1201 char *data = bprintf("%d", count);
1202 xbt_dict_set(first_enabled_state, key, data, NULL);
1206 xbt_dynar_reset(communications_pattern);
1210 /* Traverse the stack from the state at position start and re-execute the transitions */
1211 for (item = start_item;
1212 item != xbt_fifo_get_first_item(stack);
1213 item = xbt_fifo_get_prev_item(item)) {
1215 state = (mc_state_t) xbt_fifo_get_item_content(item);
1216 saved_req = MC_state_get_executed_request(state, &value);
1219 char *key = bprintf("%lu", saved_req->issuer->pid);
1220 xbt_dict_remove(first_enabled_state, key);
1225 /* because we got a copy of the executed request, we have to fetch the
1226 real one, pointed by the request field of the issuer process */
1227 req = &saved_req->issuer->simcall;
1229 /* Debug information */
1230 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1231 req_str = MC_request_to_string(req, value);
1232 XBT_DEBUG("Replay: %s (%p)", req_str, state);
1237 if(req->call == SIMCALL_COMM_ISEND)
1239 else if(req->call == SIMCALL_COMM_IRECV)
1242 SIMIX_simcall_pre(req, value);
1245 if(comm_pattern != 0){
1246 get_comm_pattern(communications_pattern, req, comm_pattern);
1252 MC_wait_for_requests();
1257 /* Insert in dict all enabled processes */
1258 xbt_swag_foreach(process, simix_global->process_list){
1259 if(MC_process_is_enabled(process) /*&& !MC_state_process_is_done(state, process)*/){
1260 char *key = bprintf("%lu", process->pid);
1261 if(xbt_dict_get_or_null(first_enabled_state, key) == NULL){
1262 char *data = bprintf("%d", count);
1263 xbt_dict_set(first_enabled_state, key, data, NULL);
1270 /* Update statistics */
1271 mc_stats->visited_states++;
1272 mc_stats->executed_transitions++;
1276 XBT_DEBUG("**** End Replay ****");
1286 void MC_replay_liveness(xbt_fifo_t stack, int all_stack)
1289 initial_state_liveness->raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1293 smx_simcall_t req = NULL, saved_req = NULL;
1294 xbt_fifo_item_t item;
1299 XBT_DEBUG("**** Begin Replay ****");
1301 /* Restore the initial state */
1302 MC_restore_snapshot(initial_state_liveness->snapshot);
1304 /* At the moment of taking the snapshot the raw heap was set, so restoring
1305 * it will set it back again, we have to unset it to continue */
1306 if(!initial_state_liveness->raw_mem_set)
1311 item = xbt_fifo_get_last_item(stack);
1313 while(depth <= xbt_fifo_size(stack)){
1315 pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1316 state = (mc_state_t) pair->graph_state;
1318 if(pair->requests > 0){
1320 saved_req = MC_state_get_executed_request(state, &value);
1321 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1323 if(saved_req != NULL){
1324 /* because we got a copy of the executed request, we have to fetch the
1325 real one, pointed by the request field of the issuer process */
1326 req = &saved_req->issuer->simcall;
1327 //XBT_DEBUG("Req->call %u", req->call);
1329 /* Debug information */
1330 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1331 req_str = MC_request_to_string(req, value);
1332 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1338 SIMIX_simcall_pre(req, value);
1339 MC_wait_for_requests();
1344 /* Update statistics */
1345 mc_stats->visited_pairs++;
1346 mc_stats->executed_transitions++;
1348 item = xbt_fifo_get_prev_item(item);
1353 /* Traverse the stack from the initial state and re-execute the transitions */
1354 for (item = xbt_fifo_get_last_item(stack);
1355 item != xbt_fifo_get_first_item(stack);
1356 item = xbt_fifo_get_prev_item(item)) {
1358 pair = (mc_pair_t) xbt_fifo_get_item_content(item);
1359 state = (mc_state_t) pair->graph_state;
1361 if(pair->requests > 0){
1363 saved_req = MC_state_get_executed_request(state, &value);
1364 //XBT_DEBUG("SavedReq->call %u", saved_req->call);
1366 if(saved_req != NULL){
1367 /* because we got a copy of the executed request, we have to fetch the
1368 real one, pointed by the request field of the issuer process */
1369 req = &saved_req->issuer->simcall;
1370 //XBT_DEBUG("Req->call %u", req->call);
1372 /* Debug information */
1373 if(XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)){
1374 req_str = MC_request_to_string(req, value);
1375 XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
1381 SIMIX_simcall_pre(req, value);
1382 MC_wait_for_requests();
1387 /* Update statistics */
1388 mc_stats->visited_pairs++;
1389 mc_stats->executed_transitions++;
1393 XBT_DEBUG("**** End Replay ****");
1395 if(initial_state_liveness->raw_mem_set)
1403 * \brief Dumps the contents of a model-checker's stack and shows the actual
1405 * \param stack The stack to dump
1407 void MC_dump_stack_safety(xbt_fifo_t stack)
1410 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1412 MC_show_stack_safety(stack);
1414 if(!_sg_mc_checkpoint){
1419 while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
1420 MC_state_delete(state);
1433 void MC_show_stack_safety(xbt_fifo_t stack)
1436 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1442 xbt_fifo_item_t item;
1444 char *req_str = NULL;
1446 for (item = xbt_fifo_get_last_item(stack);
1447 (item ? (state = (mc_state_t) (xbt_fifo_get_item_content(item)))
1448 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1449 req = MC_state_get_executed_request(state, &value);
1451 req_str = MC_request_to_string(req, value);
1452 XBT_INFO("%s", req_str);
1461 void MC_show_deadlock(smx_simcall_t req)
1463 /*char *req_str = NULL;*/
1464 XBT_INFO("**************************");
1465 XBT_INFO("*** DEAD-LOCK DETECTED ***");
1466 XBT_INFO("**************************");
1467 XBT_INFO("Locked request:");
1468 /*req_str = MC_request_to_string(req);
1469 XBT_INFO("%s", req_str);
1470 xbt_free(req_str);*/
1471 XBT_INFO("Counter-example execution trace:");
1472 MC_dump_stack_safety(mc_stack_safety);
1473 MC_print_statistics(mc_stats);
1477 void MC_show_stack_liveness(xbt_fifo_t stack){
1480 xbt_fifo_item_t item;
1482 char *req_str = NULL;
1484 for (item = xbt_fifo_get_last_item(stack);
1485 (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
1486 : (NULL)); item = xbt_fifo_get_prev_item(item)) {
1487 req = MC_state_get_executed_request(pair->graph_state, &value);
1489 if(pair->requests>0){
1490 req_str = MC_request_to_string(req, value);
1491 XBT_INFO("%s", req_str);
1494 XBT_INFO("End of system requests but evolution in Büchi automaton");
1500 void MC_dump_stack_liveness(xbt_fifo_t stack){
1502 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1507 while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
1508 MC_pair_delete(pair);
1517 void MC_print_statistics(mc_stats_t stats)
1519 if(stats->expanded_pairs == 0){
1520 XBT_INFO("Expanded states = %lu", stats->expanded_states);
1521 XBT_INFO("Visited states = %lu", stats->visited_states);
1523 XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
1524 XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
1526 XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
1528 if((_sg_mc_dot_output_file != NULL) && (_sg_mc_dot_output_file[0]!='\0')){
1529 fprintf(dot_output, "}\n");
1532 if(initial_state_safety != NULL){
1533 // XBT_INFO("Communication-deterministic : %s", !initial_state_safety->comm_deterministic ? "No" : "Yes");
1534 // XBT_INFO("Send-deterministic : %s", !initial_state_safety->send_deterministic ? "No" : "Yes");
1539 void MC_assert(int prop)
1541 if (MC_is_active() && !prop){
1542 XBT_INFO("**************************");
1543 XBT_INFO("*** PROPERTY NOT VALID ***");
1544 XBT_INFO("**************************");
1545 XBT_INFO("Counter-example execution trace:");
1546 MC_dump_stack_safety(mc_stack_safety);
1547 MC_print_statistics(mc_stats);
1553 user_max_depth_reached = 1;
1556 void MC_process_clock_add(smx_process_t process, double amount)
1558 mc_time[process->pid] += amount;
1561 double MC_process_clock_get(smx_process_t process)
1565 return mc_time[process->pid];
1573 void MC_automaton_load(const char *file){
1575 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1579 if (_mc_property_automaton == NULL)
1580 _mc_property_automaton = xbt_automaton_new();
1582 xbt_automaton_load(_mc_property_automaton,file);
1591 void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
1593 int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
1597 if (_mc_property_automaton == NULL)
1598 _mc_property_automaton = xbt_automaton_new();
1600 xbt_automaton_propositional_symbol_new(_mc_property_automaton,id,fct);