X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/4eb93650a8d0e43ef85f23ac0ab014b175c020e3..a20e82ad79e5dbc42c6c02903740edece926bc3e:/src/mc/mc_private.h

diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 6f53d84483..e7a2703122 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -21,6 +21,7 @@
 #include "xbt/function_types.h"
 #include "xbt/mmalloc.h"
 #include "../simix/smx_private.h"
+#include "../xbt/mmalloc/mmprivate.h"
 #include "xbt/automaton.h"
 #include "xbt/hash.h"
 #include "msg/msg.h"
@@ -36,8 +37,11 @@ typedef struct s_mc_function_index_item s_mc_function_index_item_t, *mc_function
 #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;
 } s_mc_mem_region_t, *mc_mem_region_t;
 
@@ -45,6 +49,8 @@ typedef struct s_mc_snapshot{
   size_t heap_bytes_used;
   mc_mem_region_t regions[NB_REGIONS];
   int nb_processes;
+  mc_mem_region_t* privatization_regions;
+  int privatization_index;
   size_t *stack_sizes;
   xbt_dynar_t stacks;
   xbt_dynar_t to_ignore;
@@ -87,11 +93,43 @@ typedef struct s_mc_checkpoint_ignore_region{
   size_t size;
 }s_mc_checkpoint_ignore_region_t, *mc_checkpoint_ignore_region_t;
 
+inline static void* mc_snapshot_get_heap_end(mc_snapshot_t snapshot) {
+  if(snapshot==NULL)
+    xbt_die("snapshot is NULL");
+  xbt_mheap_t heap = (xbt_mheap_t)snapshot->regions[0]->data;
+  return heap->breakval;
+}
+
 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);
 
+/** \brief Translate a pointer from process address space to snapshot address space
+ *
+ *  The address space contains snapshot of the main/application memory:
+ *  this function finds the address in a given snaphot for a given
+ *  real/application address.
+ *
+ *  For read only memory regions and other regions which are not int the
+ *  snapshot, the address is not changed.
+ *
+ *  \param addr     Application address
+ *  \param snapshot The snapshot of interest (if NULL no translation is done)
+ *  \return         Translated address in the snapshot address space
+ * */
+void* mc_translate_address(uintptr_t addr, mc_snapshot_t snapshot);
+
+/** \brief Translate a pointer from the snapshot address space to the application address space
+ *
+ *  This is the inverse of mc_translate_address.
+ *
+ * \param addr    Address in the snapshot address space
+ * \param snapsot Snapshot of interest (if NULL no translation is done)
+ * \return        Translated address in the application address space
+ */
+uintptr_t mc_untranslate_address(void* addr, mc_snapshot_t snapshot);
+
 extern xbt_dynar_t mc_checkpoint_ignore;
 
 /********************************* MC Global **********************************/
@@ -110,9 +148,11 @@ void MC_wait_for_requests(void);
 void MC_show_deadlock(smx_simcall_t req);
 void MC_show_stack_safety(xbt_fifo_t stack);
 void MC_dump_stack_safety(xbt_fifo_t stack);
-void MC_init(void);
 int SIMIX_pre_mc_random(smx_simcall_t simcall, int min, int max);
 
+extern xbt_fifo_t mc_stack;
+int get_search_interval(xbt_dynar_t list, void *ref, int *min, int *max);
+
 
 /********************************* Requests ***********************************/
 
@@ -129,6 +169,8 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value);
 
 /******************************** States **************************************/
 
+extern mc_global_t initial_global_state;
+
 /* Possible exploration status of a process in a state */
 typedef enum {
   MC_NOT_INTERLEAVE=0,      /* Do not interleave (do not execute) */
@@ -191,7 +233,7 @@ void MC_print_statistics(mc_stats_t);
 /* you must wrap the code between MC_SET_RAW_MODE and MC_UNSET_RAW_MODE */
 
 extern void *std_heap;
-extern void *raw_heap;
+extern void *mc_heap;
 
 
 /* FIXME: Horrible hack! because the mmalloc library doesn't provide yet of */
@@ -206,8 +248,8 @@ extern void *raw_heap;
 /*   size_t bytes_free;            /\* Byte total of chunks in the free list. *\/ */
 /* }; */
 
-#define MC_SET_RAW_MEM    mmalloc_set_current_heap(raw_heap)
-#define MC_UNSET_RAW_MEM  mmalloc_set_current_heap(std_heap)
+#define MC_SET_MC_HEAP    mmalloc_set_current_heap(mc_heap)
+#define MC_SET_STD_HEAP  mmalloc_set_current_heap(std_heap)
 
 
 /******************************* MEMORY MAPPINGS ***************************/
@@ -265,7 +307,7 @@ void print_comparison_times(void);
 //#define MC_DEBUG 1
 #define MC_VERBOSE 1
 
-/********************************** DPOR for safety property **************************************/
+/********************************** Safety verification **************************************/
 
 typedef enum {
   e_mc_reduce_unset,
@@ -274,12 +316,10 @@ typedef enum {
 } e_mc_reduce_t;
 
 extern e_mc_reduce_t mc_reduce_kind;
-extern mc_global_t initial_state_safety;
-extern xbt_fifo_t mc_stack_safety;
 extern xbt_dict_t first_enabled_state;
 
-void MC_dpor_init(void);
-void MC_dpor(void);
+void MC_pre_modelcheck_safety(void);
+void MC_modelcheck_safety(void);
 
 typedef struct s_mc_visited_state{
   mc_snapshot_t system_state;
@@ -289,13 +329,14 @@ typedef struct s_mc_visited_state{
   int other_num; // dot_output for
 }s_mc_visited_state_t, *mc_visited_state_t;
 
+extern xbt_dynar_t visited_states;
+int is_visited_state(void);
+void visited_state_free(mc_visited_state_t state);
+void visited_state_free_voidp(void *s);
 
-/********************************** Double-DFS for liveness property **************************************/
+/********************************** Liveness verification **************************************/
 
-extern xbt_fifo_t mc_stack_liveness;
-extern mc_global_t initial_state_liveness;
 extern xbt_automaton_t _mc_property_automaton;
-extern int compare;
 
 typedef struct s_mc_pair{
   int num;
@@ -325,11 +366,14 @@ 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_ddfs_init(void);
-void MC_ddfs(void);
+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 **********************************/
 
@@ -341,10 +385,10 @@ struct s_mc_object_info {
   char *start_exec, *end_exec; // Executable segment
   char *start_rw, *end_rw; // Read-write segment
   char *start_ro, *end_ro; // read-only segment
-  xbt_dynar_t subprograms; // xbt_dynar_t<dw_frame_t>
+  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 types_by_name; // xbt_dict_t<name, dw_type_t> (full defined type only)
+  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.
@@ -366,9 +410,12 @@ 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
 
@@ -386,8 +433,11 @@ typedef struct s_mc_location_list {
   mc_expression_t locations;
 } s_mc_location_list_t, *mc_location_list_t;
 
-Dwarf_Off mc_dwarf_resolve_location(mc_expression_t expression, unw_cursor_t* c, void* frame_pointer_address);
-Dwarf_Off mc_dwarf_resolve_locations(mc_location_list_t locations, unw_cursor_t* c, void* frame_pointer_address);
+uintptr_t mc_dwarf_resolve_location(mc_expression_t expression, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_snapshot_t snapshot);
+uintptr_t mc_dwarf_resolve_locations(mc_location_list_t locations, mc_object_info_t object_info, unw_cursor_t* c, void* frame_pointer_address, mc_snapshot_t snapshot);
+
+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);
 
@@ -396,6 +446,27 @@ void mc_dwarf_location_list_init(mc_location_list_t target, mc_object_info_t inf
 
 // ***** 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);
+void* mc_member_snapshot_resolve(const void* base, dw_type_t type, dw_type_t member, mc_snapshot_t snapshot);
+
 typedef struct s_dw_variable{
   Dwarf_Off dwarf_offset; /* Global offset of the field. */
   int global;
@@ -408,17 +479,21 @@ typedef struct s_dw_variable{
   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 start; /* DWARF offset of the subprogram */
-  unsigned long int end;   /* Dwarf offset of the next sibling */
+  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 {
@@ -426,6 +501,8 @@ struct s_mc_function_index_item {
   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);
@@ -434,6 +511,21 @@ void MC_dwarf_register_global_variable(mc_object_info_t info, dw_variable_t vari
 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 **********************************/
@@ -446,6 +538,7 @@ void* MC_object_base_address(mc_object_info_t info);
 #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];
@@ -453,16 +546,18 @@ typedef struct s_mc_expression_state {
 
   unw_cursor_t* cursor;
   void* frame_base;
+  mc_snapshot_t snapshot;
+  mc_object_info_t object_info;
 } s_mc_expression_state_t, *mc_expression_state_t;
 
 int mc_dwarf_execute_expression(size_t n, const Dwarf_Op* ops, mc_expression_state_t state);
 
-void* mc_find_frame_base(dw_frame_t frame, unw_cursor_t* unw_cursor);
+void* mc_find_frame_base(dw_frame_t frame, mc_object_info_t object_info, unw_cursor_t* unw_cursor);
 
 /********************************** Miscellaneous **********************************/
 
 typedef struct s_local_variable{
-  char *frame;
+  dw_frame_t subprogram;
   unsigned long ip;
   char *name;
   dw_type_t type;
@@ -476,27 +571,28 @@ typedef struct s_mc_comm_pattern{
   int num;
   smx_action_t comm;
   e_smx_comm_type_t type;
-  int completed;
   unsigned long src_proc;
   unsigned long dst_proc;
   const char *src_host;
   const char *dst_host;
   char *rdv;
-  size_t data_size;
+  ssize_t data_size;
   void *data;
-  int matched_comm;
 }s_mc_comm_pattern_t, *mc_comm_pattern_t;
 
 extern xbt_dynar_t communications_pattern;
+extern xbt_dynar_t incomplete_communications_pattern;
 
 void get_comm_pattern(xbt_dynar_t communications_pattern, smx_simcall_t request, int call);
+void complete_comm_pattern(xbt_dynar_t list, smx_action_t comm);
+void MC_pre_modelcheck_comm_determinism(void);
 
 /* *********** Sets *********** */
 
 typedef struct s_mc_address_set *mc_address_set_t;
 
 mc_address_set_t mc_address_set_new();
-mc_address_set_t mc_address_set_free(mc_address_set_t* p);
+void mc_address_set_free(mc_address_set_t* p);
 void mc_address_add(mc_address_set_t p, const void* value);
 bool mc_address_test(mc_address_set_t p, const void* value);