src/mc/mc_client_api.cpp

   1 /* Copyright (c) 2008-2019. 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 "src/mc/ModelChecker.hpp"
   8 #include "src/mc/mc_ignore.hpp"
   9 #include "src/mc/mc_private.hpp"
  10 #include "src/mc/mc_record.hpp"
  11 #include "src/mc/mc_replay.hpp"
  12 #include "src/mc/remote/Client.hpp"
  13 #include "xbt/asserts.h"
  14
  15 /** @file mc_client_api.cpp
  16  *
  17  *  This is the implementation of the API used by the user simulated program to
  18  *  communicate with the MC (declared in modelchecker.h).
  19  */
  20
  21 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_client_api, mc,
  22   "Public API for the model-checked application");
  23
  24 // MC_random() is in mc_base.cpp
  25
  26 void MC_assert(int prop)
  27 {
  28   xbt_assert(mc_model_checker == nullptr);
  29   if (not prop) {
  30     if (MC_is_active())
  31       simgrid::mc::Client::get()->report_assertion_failure();
  32     if (MC_record_replay_is_active())
  33       xbt_die("MC assertion failed");
  34   }
  35 }
  36
  37 void MC_cut()
  38 {
  39   xbt_assert(mc_model_checker == nullptr);
  40   if (not MC_is_active())
  41     return;
  42   // FIXME, We want to do this in the model-checker:
  43   xbt_die("MC_cut() not implemented");
  44 }
  45
  46 void MC_ignore(void* addr, size_t size)
  47 {
  48   xbt_assert(mc_model_checker == nullptr);
  49   if (not MC_is_active())
  50     return;
  51   simgrid::mc::Client::get()->ignore_memory(addr, size);
  52 }
  53
  54 void MC_automaton_new_propositional_symbol(const char* /*id*/, int (*/*fct*/)())
  55 {
  56   xbt_assert(mc_model_checker == nullptr);
  57   if (not MC_is_active())
  58     return;
  59   xbt_die("Support for client-side function proposition is not implemented: "
  60     "use MC_automaton_new_propositional_symbol_pointer instead.");
  61 }
  62
  63 void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)
  64 {
  65   xbt_assert(mc_model_checker == nullptr);
  66   if (not MC_is_active())
  67     return;
  68   simgrid::mc::Client::get()->declare_symbol(name, value);
  69 }
  70
  71 /** @brief Register a stack in the model checker
  72  *
  73  *  The stacks are allocated in the heap. The MC handle them specifically
  74  *  when we analyze/compare the content of the heap so it must be told where
  75  *  they are with this function.
  76  *
  77  *  @param stack Where the stack is
  78  *  @param actor Actor owning the stack
  79  *  @param context The context associated to that stack
  80  *  @param size    Size of the stack
  81  */
  82 void MC_register_stack_area(void* stack, ucontext_t* context, size_t size)
  83 {
  84   xbt_assert(mc_model_checker == nullptr);
  85   if (not MC_is_active())
  86     return;
  87   simgrid::mc::Client::get()->declare_stack(stack, size, context);
  88 }
  89
  90 void MC_ignore_global_variable(const char* /*name*/)
  91 {
  92   xbt_assert(mc_model_checker == nullptr);
  93   if (not MC_is_active())
  94     return;
  95   // TODO, send a message to the model_checker
  96   xbt_die("Unimplemented");
  97 }
  98
  99 void MC_ignore_heap(void *address, size_t size)
 100 {
 101   xbt_assert(mc_model_checker == nullptr);
 102   if (not MC_is_active())
 103     return;
 104   simgrid::mc::Client::get()->ignore_heap(address, size);
 105 }
 106
 107 void MC_unignore_heap(void* address, size_t size)
 108 {
 109   xbt_assert(mc_model_checker == nullptr);
 110   if (not MC_is_active())
 111     return;
 112   simgrid::mc::Client::get()->unignore_heap(address, size);
 113 }