-/********************************** Safety verification **************************************/
-
-typedef enum {
- e_mc_reduce_unset,
- e_mc_reduce_none,
- e_mc_reduce_dpor
-} e_mc_reduce_t;
-
-extern e_mc_reduce_t mc_reduce_kind;
-extern xbt_dict_t first_enabled_state;
-
-void MC_pre_modelcheck_safety(void);
-void MC_modelcheck_safety(void);
-
-typedef struct s_mc_visited_state{
- mc_snapshot_t system_state;
- size_t heap_bytes_used;
- int nb_processes;
- int num;
- int other_num; // dot_output for
-}s_mc_visited_state_t, *mc_visited_state_t;
-
-extern xbt_dynar_t visited_states;
-mc_visited_state_t is_visited_state(void);
-void visited_state_free(mc_visited_state_t state);
-void visited_state_free_voidp(void *s);
-
-/********************************** Liveness verification **************************************/
-
-extern xbt_automaton_t _mc_property_automaton;
-
-typedef struct s_mc_pair{
- int num;
- int search_cycle;
- mc_state_t graph_state; /* System state included */
- xbt_automaton_state_t automaton_state;
- xbt_dynar_t atomic_propositions;
- int requests;
-}s_mc_pair_t, *mc_pair_t;
-
-typedef struct s_mc_visited_pair{
- int num;
- int other_num; /* Dot output for */
- int acceptance_pair;
- mc_state_t graph_state; /* System state included */
- xbt_automaton_state_t automaton_state;
- xbt_dynar_t atomic_propositions;
- size_t heap_bytes_used;
- int nb_processes;
- int acceptance_removed;
- int visited_removed;
-}s_mc_visited_pair_t, *mc_visited_pair_t;
-
-mc_pair_t MC_pair_new(void);
-void MC_pair_delete(mc_pair_t);
-void mc_pair_free_voidp(void *p);
-mc_visited_pair_t MC_visited_pair_new(int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
-void MC_visited_pair_delete(mc_visited_pair_t p);
-
-void MC_pre_modelcheck_liveness(void);
-void MC_modelcheck_liveness(void);
-void MC_show_stack_liveness(xbt_fifo_t stack);
-void MC_dump_stack_liveness(xbt_fifo_t stack);
-
-extern xbt_dynar_t visited_pairs;
-int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions);
-
-
-/********************************** Variables with DWARF **********************************/
-
-#define MC_OBJECT_INFO_EXECUTABLE 1
-
-struct s_mc_object_info {
- size_t flags;
- char* file_name;
- char *start_exec, *end_exec; // Executable segment
- char *start_rw, *end_rw; // Read-write segment
- char *start_ro, *end_ro; // read-only segment
- xbt_dict_t subprograms; // xbt_dict_t<origin as hexadecimal string, dw_frame_t>
- xbt_dynar_t global_variables; // xbt_dynar_t<dw_variable_t>
- xbt_dict_t types; // xbt_dict_t<origin as hexadecimal string, dw_type_t>
- xbt_dict_t full_types_by_name; // xbt_dict_t<name, dw_type_t> (full defined type only)
-
- // Here we sort the minimal information for an efficient (and cache-efficient)
- // lookup of a function given an instruction pointer.
- // The entries are sorted by low_pc and a binary search can be used to look them up.
- xbt_dynar_t functions_index;
-};
-
-mc_object_info_t MC_new_object_info(void);
-mc_object_info_t MC_find_object_info(memory_map_t maps, char* name, int executable);
-void MC_free_object_info(mc_object_info_t* p);
-
-void MC_dwarf_get_variables(mc_object_info_t info);
-void MC_dwarf_get_variables_libdw(mc_object_info_t info);
-const char* MC_dwarf_attrname(int attr);
-const char* MC_dwarf_tagname(int tag);
-
-dw_frame_t MC_find_function_by_ip(void* ip);
-mc_object_info_t MC_ip_find_object_info(void* ip);
-
-extern mc_object_info_t mc_libsimgrid_info;
-extern mc_object_info_t mc_binary_info;
-extern mc_object_info_t mc_object_infos[2];
-extern size_t mc_object_infos_size;
-
-void MC_find_object_address(memory_map_t maps, mc_object_info_t result);
-void MC_post_process_types(mc_object_info_t info);
-void MC_post_process_object_info(mc_object_info_t info);
-
-// ***** Expressions
-
-/** \brief a DWARF expression with optional validity contraints */
-typedef struct s_mc_expression {
- size_t size;
- Dwarf_Op* ops;
- // Optional validity:
- void* lowpc, *highpc;
-} s_mc_expression_t, *mc_expression_t;
-
-/** A location list (list of location expressions) */
-typedef struct s_mc_location_list {
- size_t size;
- mc_expression_t locations;
-} s_mc_location_list_t, *mc_location_list_t;
-
-/** A location is either a location in memory of a register location
- *
- * Usage:
- *
- * * mc_dwarf_resolve_locations or mc_dwarf_resolve_location is used
- * to find the location of a given location expression or location list;
- *
- * * mc_get_location_type MUST be used to find the location type;
- *
- * * for MC_LOCATION_TYPE_ADDRESS, memory_address is the resulting address
- *
- * * for MC_LOCATION_TYPE_REGISTER, unw_get_reg(l.cursor, l.register_id, value)
- * and unw_get_reg(l.cursor, l.register_id, value) can be used to read/write
- * the value.
- * </ul>
- */
-typedef struct s_mc_location {
- void* memory_location;
- unw_cursor_t* cursor;
- int register_id;
-} s_mc_location_t, *mc_location_t;
-
-/** Type of a given location
- *
- * Use `mc_get_location_type(location)` to find the type.
- * */
-typedef enum mc_location_type {
- MC_LOCATION_TYPE_ADDRESS,
- MC_LOCATION_TYPE_REGISTER
-} mc_location_type;
-
-/** Find the type of a location */
-static inline __attribute__ ((always_inline))
-enum mc_location_type mc_get_location_type(mc_location_t location) {
- if (location->cursor) {
- return MC_LOCATION_TYPE_REGISTER;
- } else {
- return MC_LOCATION_TYPE_ADDRESS;
- }
-}
-
-void mc_dwarf_resolve_location(mc_location_t location, mc_expression_t expression, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_snapshot_t snapshot, int process_index);
-void mc_dwarf_resolve_locations(mc_location_t location, mc_location_list_t locations, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_snapshot_t snapshot, int process_index);
-
-void mc_dwarf_expression_clear(mc_expression_t expression);
-void mc_dwarf_expression_init(mc_expression_t expression, size_t len, Dwarf_Op* ops);
-
-void mc_dwarf_location_list_clear(mc_location_list_t list);
-
-void mc_dwarf_location_list_init_from_expression(mc_location_list_t target, size_t len, Dwarf_Op* ops);
-void mc_dwarf_location_list_init(mc_location_list_t target, mc_object_info_t info, Dwarf_Die* die, Dwarf_Attribute* attr);
-
-// ***** Variables and functions
-
-struct s_dw_type{
- e_dw_type_type type;
- Dwarf_Off id; /* Offset in the section (in hexadecimal form) */
- char *name; /* Name of the type */
- int byte_size; /* Size in bytes */
- int element_count; /* Number of elements for array type */
- char *dw_type_id; /* DW_AT_type id */
- xbt_dynar_t members; /* if DW_TAG_structure_type, DW_TAG_class_type, DW_TAG_union_type*/
- int is_pointer_type;
-
- // Location (for members) is either of:
- struct s_mc_expression location;
- int offset;
-
- dw_type_t subtype; // DW_AT_type
- dw_type_t full_type; // The same (but more complete) type
-};
-
-void* mc_member_resolve(const void* base, dw_type_t type, dw_type_t member, mc_snapshot_t snapshot, int process_index);
-
-typedef struct s_dw_variable{
- Dwarf_Off dwarf_offset; /* Global offset of the field. */
- int global;
- char *name;
- char *type_origin;
- dw_type_t type;
-
- // Use either of:
- s_mc_location_list_t locations;
- void* address;
-
- size_t start_scope;
- mc_object_info_t object_info;
-
-}s_dw_variable_t, *dw_variable_t;
-
-struct s_dw_frame{
- int tag;
- char *name;
- void *low_pc;
- void *high_pc;
- s_mc_location_list_t frame_base;
- xbt_dynar_t /* <dw_variable_t> */ variables; /* Cannot use dict, there may be several variables with the same name (in different lexical blocks)*/
- unsigned long int id; /* DWARF offset of the subprogram */
- xbt_dynar_t /* <dw_frame_t> */ scopes;
- Dwarf_Off abstract_origin_id;
- mc_object_info_t object_info;
-};
-
-struct s_mc_function_index_item {
- void* low_pc, *high_pc;
- dw_frame_t function;
-};
-
-void mc_frame_free(dw_frame_t freme);
-
-void dw_type_free(dw_type_t t);
-void dw_variable_free(dw_variable_t v);
-void dw_variable_free_voidp(void *t);
-
-void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t variable);
-void MC_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
-void MC_dwarf_register_non_global_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
-void MC_dwarf_register_variable(mc_object_info_t info, dw_frame_t frame, dw_variable_t variable);
-
-/** Find the DWARF offset for this ELF object
- *
- * An offset is applied to address found in DWARF:
- *
- * <ul>
- * <li>for an executable obejct, addresses are virtual address
- * (there is no offset) i.e. \f$\text{virtual address} = \{dwarf address}\f$;</li>
- * <li>for a shared object, the addreses are offset from the begining
- * of the shared object (the base address of the mapped shared
- * object must be used as offset
- * i.e. \f$\text{virtual address} = \text{shared object base address}
- * + \text{dwarf address}\f$.</li>
- *
- */
-void* MC_object_base_address(mc_object_info_t info);
-
-/********************************** DWARF **********************************/
-
-#define MC_EXPRESSION_STACK_SIZE 64
-
-#define MC_EXPRESSION_OK 0
-#define MC_EXPRESSION_E_UNSUPPORTED_OPERATION 1
-#define MC_EXPRESSION_E_STACK_OVERFLOW 2
-#define MC_EXPRESSION_E_STACK_UNDERFLOW 3
-#define MC_EXPRESSION_E_MISSING_STACK_CONTEXT 4
-#define MC_EXPRESSION_E_MISSING_FRAME_BASE 5
-#define MC_EXPRESSION_E_NO_BASE_ADDRESS 6
-
-typedef struct s_mc_expression_state {
- uintptr_t stack[MC_EXPRESSION_STACK_SIZE];
- size_t stack_size;
-
- unw_cursor_t* cursor;
- void* frame_base;
- mc_snapshot_t snapshot;
- mc_object_info_t object_info;
- int process_index;
-} s_mc_expression_state_t, *mc_expression_state_t;