src/mc/mc_client_api.cpp

   1 /* Copyright (c) 2008-2015. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <xbt/log.h>
   8 #include <xbt/fifo.h>
   9 #include <xbt/sysdep.h>
  10 #include <simgrid/modelchecker.h>
  11
  12 #include "mc_record.h"
  13 #include "mc_private.h"
  14 #include "mc_mmalloc.h"
  15 #include "mc_ignore.h"
  16 #include "mc_protocol.h"
  17 #include "mc_client.h"
  18 #include "ModelChecker.hpp"
  19
  20 /** \file mc_client_api.cpp
  21  *
  22  *  This is the implementation of the API used by the user simulated program to
  23  *  communicate with the MC (declared in modelchecker.h).
  24  */
  25
  26 extern "C" {
  27
  28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
  29   "Public API for the model-checked application");
  30
  31 int MC_random(int min, int max)
  32 {
  33   xbt_assert(mc_mode != MC_MODE_SERVER);
  34   // TODO, if the MC is disabled we do not really need to make a simcall for this :)
  35   /* FIXME: return mc_current_state->executed_transition->random.value; */
  36   return simcall_mc_random(min, max);
  37 }
  38
  39 void MC_assert(int prop)
  40 {
  41   if (MC_is_active() && !prop) {
  42     MC_client_send_simple_message(MC_MESSAGE_ASSERTION_FAILED);
  43     MC_client_handle_messages();
  44   }
  45 }
  46
  47 // TODO, MC_automaton_new_propositional_symbol
  48
  49 void *MC_snapshot(void)
  50 {
  51   return simcall_mc_snapshot();
  52 }
  53
  54 int simcall_HANDLER_mc_compare_snapshots(smx_simcall_t simcall,
  55                                    mc_snapshot_t s1, mc_snapshot_t s2)
  56 {
  57   return snapshot_compare(s1, s2);
  58 }
  59
  60 int MC_compare_snapshots(void *s1, void *s2)
  61 {
  62   return simcall_mc_compare_snapshots(s1, s2);
  63 }
  64
  65 void MC_cut(void)
  66 {
  67   user_max_depth_reached = 1;
  68 }
  69
  70 void MC_ignore(void* addr, size_t size)
  71 {
  72   xbt_assert(mc_mode != MC_MODE_SERVER);
  73   if (mc_mode != MC_MODE_CLIENT)
  74     return;
  75
  76   s_mc_ignore_memory_message_t message;
  77   message.type = MC_MESSAGE_IGNORE_MEMORY;
  78   message.addr = (std::uintptr_t) addr;
  79   message.size = size;
  80   MC_client_send_message(&message, sizeof(message));
  81 }
  82
  83 void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
  84 {
  85   xbt_assert(mc_mode != MC_MODE_SERVER);
  86   if (mc_mode != MC_MODE_CLIENT)
  87     return;
  88
  89   xbt_die("Support for client-side function proposition is not implemented: "
  90     "use MC_automaton_new_propositional_symbol_pointer instead."
  91   );
  92 }
  93
  94 void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
  95 {
  96   xbt_assert(mc_mode != MC_MODE_SERVER);
  97   if (mc_mode != MC_MODE_CLIENT)
  98     return;
  99
 100   s_mc_register_symbol_message_t message;
 101   message.type = MC_MESSAGE_REGISTER_SYMBOL;
 102   if (strlen(name) + 1 > sizeof(message.name))
 103     xbt_die("Symbol is too long");
 104   strncpy(message.name, name, sizeof(message.name));
 105   message.callback = nullptr;
 106   message.data = value;
 107   MC_client_send_message(&message, sizeof(message));
 108 }
 109
 110 }