-#define NB_REGIONS 3 /* binary data (data + BSS) (type = 2), libsimgrid data (data + BSS) (type = 1), std_heap (type = 0)*/
-
-typedef struct s_mc_mem_region{
- // Real address:
- void *start_addr;
- // Copy of the datra:
- void *data;
- // Size of the data region:
- size_t size;
- // For per-page snapshots, this is an array to the number of
- size_t* page_numbers;
-} s_mc_mem_region_t, *mc_mem_region_t;
-
-static inline __attribute__ ((always_inline))
-bool mc_region_contain(mc_mem_region_t region, void* p)
-{
- return p >= region->start_addr &&
- p < (void*)((char*) region->start_addr + region->size);
-}
-
-/** Ignored data
- *
- * Some parts of the snapshot are ignored by zeroing them out: the real
- * values is stored here.
- * */
-typedef struct s_mc_snapshot_ignored_data {
- void* start;
- size_t size;
- void* data;
-} s_mc_snapshot_ignored_data_t, *mc_snapshot_ignored_data_t;
-
-typedef struct s_mc_snapshot{
- size_t heap_bytes_used;
- mc_mem_region_t regions[NB_REGIONS];
- xbt_dynar_t enabled_processes;
- mc_mem_region_t* privatization_regions;
- int privatization_index;
- size_t *stack_sizes;
- xbt_dynar_t stacks;
- xbt_dynar_t to_ignore;
- uint64_t hash;
- xbt_dynar_t ignored_data;
-} s_mc_snapshot_t, *mc_snapshot_t;
-
-mc_mem_region_t mc_get_snapshot_region(void* addr, mc_snapshot_t snapshot);
-
-static inline __attribute__ ((always_inline))
-mc_mem_region_t mc_get_region_hinted(void* addr, mc_snapshot_t snapshot, mc_mem_region_t region)
-{
- if (mc_region_contain(region, addr))
- return region;
- else
- return mc_get_snapshot_region(addr, snapshot);
-}
-
-/** Information about a given stack frame
- *
- */
-typedef struct s_mc_stack_frame {
- /** Instruction pointer */
- unw_word_t ip;
- /** Stack pointer */
- unw_word_t sp;
- unw_word_t frame_base;
- dw_frame_t frame;
- char* frame_name;
- unw_cursor_t unw_cursor;
-} s_mc_stack_frame_t, *mc_stack_frame_t;
-
-typedef struct s_mc_snapshot_stack{
- xbt_dynar_t local_variables;
- xbt_dynar_t stack_frames; // mc_stack_frame_t
-}s_mc_snapshot_stack_t, *mc_snapshot_stack_t;
-
-typedef struct s_mc_global_t{
- mc_snapshot_t snapshot;
- int raw_mem_set;
- int prev_pair;
- char *prev_req;
- int initial_communications_pattern_done;
- int comm_deterministic;
- int send_deterministic;
-}s_mc_global_t, *mc_global_t;
-
-typedef struct s_mc_checkpoint_ignore_region{
- void *addr;
- size_t size;
-}s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
-
-static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot);
-
-mc_snapshot_t SIMIX_pre_mc_snapshot(smx_simcall_t simcall);
-mc_snapshot_t MC_take_snapshot(int num_state);
-void MC_restore_snapshot(mc_snapshot_t);
-void MC_free_snapshot(mc_snapshot_t);
-
-int mc_important_snapshot(mc_snapshot_t snapshot);
-
-size_t* mc_take_page_snapshot_region(void* data, size_t page_count, uint64_t* pagemap, size_t* reference_pages);
-void mc_free_page_snapshot_region(size_t* pagenos, size_t page_count);
-void mc_restore_page_snapshot_region(mc_mem_region_t region, size_t page_count, uint64_t* pagemap, mc_mem_region_t reference_region);
-
-mc_mem_region_t mc_region_new_sparse(int type, void *start_addr, size_t size, mc_mem_region_t ref_reg);
-void mc_region_restore_sparse(mc_mem_region_t reg, mc_mem_region_t ref_reg);
-void mc_softdirty_reset();
-
-static inline __attribute__((always_inline))
-bool mc_snapshot_region_linear(mc_mem_region_t region) {
- return !region || !region->data;
-}
-
-void* mc_snapshot_read_fragmented(void* addr, mc_mem_region_t region, void* target, size_t size);
-
-void* mc_snapshot_read(void* addr, mc_snapshot_t snapshot, void* target, size_t size);
-int mc_snapshot_region_memcmp(
- void* addr1, mc_mem_region_t region1,
- void* addr2, mc_mem_region_t region2, size_t size);
-int mc_snapshot_memcp(
- void* addr1, mc_snapshot_t snapshot1,
- void* addr2, mc_snapshot_t snapshot2, size_t size);
-
-static void* mc_snapshot_read_pointer(void* addr, mc_snapshot_t snapshot);
-
-/** @brief State of the model-checker (global variables for the model checker)
- *
- * Each part of the state of the model chercker represented as a global
- * variable prevents some sharing between snapshots and must be ignored.
- * By moving as much state as possible in this structure allocated
- * on the model-chercker heap, we avoid those issues.
- */
-typedef struct s_mc_model_checker {
- // This is the parent snapshot of the current state:
- mc_snapshot_t parent_snapshot;
- mc_pages_store_t pages;
- int fd_clear_refs;
- int fd_pagemap;
-} s_mc_model_checker_t, *mc_model_checker_t;
-
-extern mc_model_checker_t mc_model_checker;
-