src/mc/api.cpp

   1 /* Copyright (c) 2020-2022. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "api.hpp"
   7
   8 #include "src/kernel/activity/MailboxImpl.hpp"
   9 #include "src/kernel/activity/MutexImpl.hpp"
  10 #include "src/kernel/actor/SimcallObserver.hpp"
  11 #include "src/mc/Session.hpp"
  12 #include "src/mc/explo/Exploration.hpp"
  13 #include "src/mc/mc_base.hpp"
  14 #include "src/mc/mc_exit.hpp"
  15 #include "src/mc/mc_pattern.hpp"
  16 #include "src/mc/mc_private.hpp"
  17 #include "src/mc/remote/RemoteProcess.hpp"
  18 #include "src/surf/HostImpl.hpp"
  19
  20 #include <xbt/asserts.h>
  21 #include <xbt/log.h>
  22 #include "simgrid/s4u/Host.hpp"
  23 #include "xbt/string.hpp"
  24 #if HAVE_SMPI
  25 #include "src/smpi/include/smpi_request.hpp"
  26 #endif
  27
  28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(Api, mc, "Logging specific to MC Facade APIs ");
  29 XBT_LOG_EXTERNAL_CATEGORY(mc_global);
  30
  31 using Simcall = simgrid::simix::Simcall;
  32
  33 namespace simgrid {
  34 namespace mc {
  35
  36 simgrid::mc::Exploration* Api::initialize(char** argv, simgrid::mc::CheckerAlgorithm algo)
  37 {
  38   session_ = std::make_unique<simgrid::mc::Session>([argv] {
  39     int i = 1;
  40     while (argv[i] != nullptr && argv[i][0] == '-')
  41       i++;
  42     xbt_assert(argv[i] != nullptr,
  43                "Unable to find a binary to exec on the command line. Did you only pass config flags?");
  44     execvp(argv[i], argv + i);
  45     xbt_die("The model-checked process failed to exec(%s): %s", argv[i], strerror(errno));
  46   });
  47
  48   simgrid::mc::Exploration* explo;
  49   switch (algo) {
  50     case CheckerAlgorithm::CommDeterminism:
  51       explo = simgrid::mc::create_communication_determinism_checker(session_.get());
  52       break;
  53
  54     case CheckerAlgorithm::UDPOR:
  55       explo = simgrid::mc::create_udpor_checker(session_.get());
  56       break;
  57
  58     case CheckerAlgorithm::Safety:
  59       explo = simgrid::mc::create_safety_checker(session_.get());
  60       break;
  61
  62     case CheckerAlgorithm::Liveness:
  63       explo = simgrid::mc::create_liveness_checker(session_.get());
  64       break;
  65
  66     default:
  67       THROW_IMPOSSIBLE;
  68   }
  69
  70   mc_model_checker->set_exploration(explo);
  71   return explo;
  72 }
  73
  74 std::vector<simgrid::mc::ActorInformation>& Api::get_actors() const
  75 {
  76   return mc_model_checker->get_remote_process().actors();
  77 }
  78
  79 unsigned long Api::get_maxpid() const
  80 {
  81   return mc_model_checker->get_remote_process().get_maxpid();
  82 }
  83
  84 std::size_t Api::get_remote_heap_bytes() const
  85 {
  86   RemoteProcess& process    = mc_model_checker->get_remote_process();
  87   auto heap_bytes_used      = mmalloc_get_bytes_used_remote(process.get_heap()->heaplimit, process.get_malloc_info());
  88   return heap_bytes_used;
  89 }
  90
  91 void Api::mc_inc_visited_states() const
  92 {
  93   mc_model_checker->visited_states++;
  94 }
  95
  96 unsigned long Api::mc_get_visited_states() const
  97 {
  98   return mc_model_checker->visited_states;
  99 }
 100
 101 void Api::mc_exit(int status) const
 102 {
 103   mc_model_checker->exit(status);
 104 }
 105
 106 void Api::restore_state(std::shared_ptr<simgrid::mc::Snapshot> system_state) const
 107 {
 108   system_state->restore(&mc_model_checker->get_remote_process());
 109 }
 110
 111 bool Api::snapshot_equal(const Snapshot* s1, const Snapshot* s2) const
 112 {
 113   return simgrid::mc::snapshot_equal(s1, s2);
 114 }
 115
 116 simgrid::mc::Snapshot* Api::take_snapshot(long num_state) const
 117 {
 118   auto snapshot = new simgrid::mc::Snapshot(num_state);
 119   return snapshot;
 120 }
 121
 122 void Api::s_close()
 123 {
 124   session_.reset();
 125   if (simgrid::mc::property_automaton != nullptr) {
 126     xbt_automaton_free(simgrid::mc::property_automaton);
 127     simgrid::mc::property_automaton = nullptr;
 128   }
 129 }
 130
 131 void Api::automaton_load(const char* file) const
 132 {
 133   if (simgrid::mc::property_automaton == nullptr)
 134     simgrid::mc::property_automaton = xbt_automaton_new();
 135
 136   xbt_automaton_load(simgrid::mc::property_automaton, file);
 137 }
 138
 139 std::vector<int> Api::automaton_propositional_symbol_evaluate() const
 140 {
 141   unsigned int cursor = 0;
 142   std::vector<int> values;
 143   xbt_automaton_propositional_symbol_t ps = nullptr;
 144   xbt_dynar_foreach (mc::property_automaton->propositional_symbols, cursor, ps)
 145     values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
 146   return values;
 147 }
 148
 149 std::vector<xbt_automaton_state_t> Api::get_automaton_state() const
 150 {
 151   std::vector<xbt_automaton_state_t> automaton_stack;
 152   unsigned int cursor = 0;
 153   xbt_automaton_state_t automaton_state;
 154   xbt_dynar_foreach (mc::property_automaton->states, cursor, automaton_state)
 155     if (automaton_state->type == -1)
 156       automaton_stack.push_back(automaton_state);
 157   return automaton_stack;
 158 }
 159
 160 int Api::compare_automaton_exp_label(const xbt_automaton_exp_label* l) const
 161 {
 162   unsigned int cursor                    = 0;
 163   xbt_automaton_propositional_symbol_t p = nullptr;
 164   xbt_dynar_foreach (simgrid::mc::property_automaton->propositional_symbols, cursor, p) {
 165     if (std::strcmp(xbt_automaton_propositional_symbol_get_name(p), l->u.predicat) == 0)
 166       return cursor;
 167   }
 168   return -1;
 169 }
 170
 171 void Api::set_property_automaton(xbt_automaton_state_t const& automaton_state) const
 172 {
 173   mc::property_automaton->current_state = automaton_state;
 174 }
 175
 176 xbt_automaton_exp_label_t Api::get_automaton_transition_label(xbt_dynar_t const& dynar, int index) const
 177 {
 178   const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
 179   return transition->label;
 180 }
 181
 182 xbt_automaton_state_t Api::get_automaton_transition_dst(xbt_dynar_t const& dynar, int index) const
 183 {
 184   const xbt_automaton_transition* transition = xbt_dynar_get_as(dynar, index, xbt_automaton_transition_t);
 185   return transition->dst;
 186 }
 187
 188 } // namespace mc
 189 } // namespace simgrid