};
/** Representation of a process
+ *
+ * This class is mixing a lot of differents responsabilities and is tied
+ * to SIMIX. It should probably split into different classes.
+ *
+ * Responsabilities:
+ *
+ * - reading from the process memory (`AddressSpace`);
+ * - accessing the system state of the porcess (heap, …);
+ * - storing the SIMIX state of the process;
+ * - privatization;
+ * - communication with the model-checked process;
+ * - stack unwinding;
+ * - etc.
*/
class Process final : public AddressSpace {
public:
void ignore_local_variable(const char *var_name, const char *frame_name);
int socket() { return socket_; }
std::vector<simgrid::mc::SimixProcessInformation>& simix_processes();
+ std::vector<simgrid::mc::SimixProcessInformation>& old_simix_processes();
private:
void init_memory_map_info();
void refresh_heap();
void refresh_malloc_info();
+ void refresh_simix();
private:
pid_t pid_ = -1;
assert(i == swag.count);
}
-void MC_process_smx_refresh(simgrid::mc::Process* process)
+namespace simgrid {
+namespace mc {
+
+void Process::refresh_simix()
{
xbt_assert(mc_mode == MC_MODE_SERVER);
- if (process->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
+ if (this->cache_flags & MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES)
return;
// TODO, avoid to reload `&simix_global`, `simix_global`, `*simix_global`
// simix_global_p = REMOTE(simix_global);
smx_global_t simix_global_p;
- process->read_variable("simix_global", &simix_global_p, sizeof(simix_global_p));
+ this->read_variable("simix_global", &simix_global_p, sizeof(simix_global_p));
// simix_global = REMOTE(*simix_global)
s_smx_global_t simix_global;
- process->read_bytes(&simix_global, sizeof(simix_global),
+ this->read_bytes(&simix_global, sizeof(simix_global),
remote(simix_global_p));
MC_process_refresh_simix_process_list(
- process, process->smx_process_infos, simix_global.process_list);
+ this, this->smx_process_infos, simix_global.process_list);
MC_process_refresh_simix_process_list(
- process, process->smx_old_process_infos, simix_global.process_to_destroy);
+ this, this->smx_old_process_infos, simix_global.process_to_destroy);
- process->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+ this->cache_flags |= MC_PROCESS_CACHE_FLAG_SIMIX_PROCESSES;
+}
+
+}
}
/** Get the issuer of a simcall (`req->issuer`)
if (mc_mode == MC_MODE_CLIENT)
return req->issuer;
- MC_process_smx_refresh(&mc_model_checker->process());
-
// This is the address of the smx_process in the MCed process:
void* address = req->issuer;
// Lookup by address:
- for (auto& p : mc_model_checker->process().smx_process_infos)
+ for (auto& p : mc_model_checker->process().simix_processes())
if (p.address == address)
return &p.copy;
- for (auto& p : mc_model_checker->process().smx_old_process_infos)
+ for (auto& p : mc_model_checker->process().old_simix_processes())
if (p.address == address)
return &p.copy;
process->get_heap()->heaplimit,
process->get_malloc_info());
- MC_process_smx_refresh(&mc_model_checker->process());
this->nb_processes =
- mc_model_checker->process().smx_process_infos.size();
+ mc_model_checker->process().simix_processes().size();
this->num = mc_stats->expanded_states;
this->other_num = -1;
process->get_heap()->heaplimit,
process->get_malloc_info());
- MC_process_smx_refresh(&mc_model_checker->process());
this->nb_processes =
- mc_model_checker->process().smx_process_infos.size();
+ mc_model_checker->process().simix_processes().size();
this->automaton_state = automaton_state;
this->num = pair_num;