include/libinterface.h

   1 /** @file libinterface.h
   2  *  @brief Interface to check normal memory operations for data races.
   3  */
   4
   5 #ifndef __LIBINTERFACE_H__
   6 #define __LIBINTERFACE_H__
   7
   8 #include <stdint.h>
   9
  10 #ifdef __cplusplus
  11 extern "C" {
  12 #endif
  13         typedef unsigned int MCID;
  14 #define MC2_PTR_LENGTH sizeof(void *)
  15
  16 #define MCID_NODEP ((MCID)0)
  17 #define MCID_INIT ((MCID)0)
  18 #define MCID_FIRST ((MCID)1)
  19
  20 #define MC2_OFFSET(x, y) (uintptr_t)(&((x)(0))->y)
  21
  22         /** Stores N bits of val to the location given by addr. */
  23         void store_8(void *addr, uint8_t val);
  24         void store_16(void *addr, uint16_t val);
  25         void store_32(void *addr, uint32_t val);
  26         void store_64(void *addr, uint64_t val);
  27
  28         /** Loads N bits from the location given by addr. */
  29         uint8_t load_8(const void *addr);
  30         uint16_t load_16(const void *addr);
  31         uint32_t load_32(const void *addr);
  32         uint64_t load_64(const void *addr);
  33
  34         /** Atomic operation enumeration for RMW operations. */
  35
  36         enum atomicop {
  37                 ADD,
  38                 CAS /* Compare and swap */,
  39                 EXC /* Exchange */
  40         };
  41
  42         /** Performs an atomic N bit RMW (read-modify-write) operation as
  43          *      specified by op to data located at addr.
  44          *  For CAS, valarg is the value to be written, while
  45          *                                              oldval gives the value to be compared against.
  46          *      For EXC, valarg is the value to be written and oldval is ignored.
  47          *      For ADD, valarg is the value to be added and oldval is ignored. */
  48
  49         uint8_t rmw_8(enum atomicop op, void *addr, uint8_t oldval, uint8_t valarg);
  50         uint16_t rmw_16(enum atomicop op, void *addr, uint16_t oldval, uint16_t valarg);
  51         uint32_t rmw_32(enum atomicop op, void *addr, uint32_t oldval, uint32_t valarg);
  52         uint64_t rmw_64(enum atomicop op, void *addr, uint64_t oldval, uint64_t valarg);
  53
  54         /** Supplies to MC2 the MCIDs for the addrs of the
  55          *      immediately-following RMW/Load/Store operation. All
  56          *      RMW/Load/Store operations must be immediately preceded by either
  57          *      a MC2_nextRMW/MC2_nextOpLoad/MC2_nextOpStore or one of the
  58          *      offset calls specified in the next section. For MC2_nextRMW and
  59          *      MC2_nextOpLoad, MC2 returns an MCID for the value read by the
  60          *      RMW/load operation. */
  61
  62         MCID MC2_nextRMW(MCID addr, MCID oldval, MCID valarg);
  63         MCID MC2_nextOpLoad(MCID addr);
  64         void MC2_nextOpStore(MCID addr, MCID value);
  65
  66         /** Supplies to MC2 the MCIDs representing the target of the
  67          *      immediately-following RMW/Load/Store operation, which accesses
  68          *      memory at a fixed offset from addr.
  69          *
  70          *      e.g. load_8(x.f) could be instrumented with
  71          *      MC2_nextOpLoadOffset(_m_x, offset of f in structure x). */
  72
  73         MCID MC2_nextRMWOffset(MCID addr, uintptr_t offset, MCID oldval, MCID valarg);
  74         MCID MC2_nextOpLoadOffset(MCID addr, uintptr_t offset);
  75         void MC2_nextOpStoreOffset(MCID addr, uintptr_t offset, MCID value);
  76
  77         /** Tells MC2 that we just took direction "direction" of a
  78          *      conditional branch with "num_directions" possible directions.
  79          *      "condition" gives the MCID for the concrete condition variable
  80          *      that we conditionally branched on. Boolean anyvalue = true means
  81          *      that any non-zero concrete condition implies the branch will
  82          *      take direction 1. */
  83
  84         MCID MC2_branchUsesID(MCID condition, int direction, int num_directions, bool anyvalue);
  85
  86         /** Currently not used. TODO implement later. */
  87         void MC2_nextOpThrd_create(MCID startfunc, MCID param);
  88         void MC2_nextOpThrd_join(MCID jointhrd);
  89
  90         /** Tells MC2 that we hit the merge point of a conditional
  91          *      branch. branchid is the MCID for the condition variable of the
  92          *      branch that just merged. */
  93         void MC2_merge(MCID branchid);
  94
  95         /** Tells MC2 that we just computed something that MC2 should treat
  96          *      as an uninterpreted function. The uninterpreted function takes
  97          *      num_args parameters and produces a return value of
  98          *      numbytesretval bytes; the actual return value is val.  The
  99          *      following varargs parameters supply MCIDs for inputs.  MC2
 100          *      returns an MCID for the return value of the uninterpreted
 101          *      function.
 102          *
 103          *      Uninterpreted functions annotated with MC2_function are unique
 104          *      to the given dynamic instance. That is, for an unintepreted
 105          *      function call annotated by MC2_function which lives inside a
 106          *      loop, results from the first iteration will NOT be aggregated
 107          *      with results from subsequent iterations. */
 108         MCID MC2_function(unsigned int num_args, int numbytesretval, uint64_t val, ...);
 109
 110         /** Same as MC2_function, but MC2 aggregates results for all
 111          *      instances with the same id. The id must be greater than 0.
 112          *      Useful for functions which have MCIDs for all inputs.
 113          *      (MC2_function, by contrast, may omit MCIDs for some inputs.) */
 114         MCID MC2_function_id(unsigned int id, unsigned int num_args, int numbytesretval, uint64_t val, ...);
 115
 116         /** Asks MC2 to compare val1 (with MCID op1) and val2 (MCID op2);
 117          *      returns val1==val2, and sets *retval to the MCID for the return value. */
 118         // This function's API should change to take only op1 and op2, and return the MCID for the retval. This is difficult with the old frontend.
 119         uint64_t MC2_equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval);
 120
 121         /** Tells MC2 about the MCID of an input which was merged at a merge
 122          *  point. (The merge point must also be annotated, first, with an
 123          *  MC2_merge). Returns an MCID for the output of the phi function.
 124          *
 125          *      MC2_phi enables instrumenting cases like:
 126          *      if (x) {
 127          *              y=0;
 128          *      } else {
 129          *              y=1;
 130          *      }
 131          *      // must put here: MC2_merge(_m_x);
 132          *      //                                                              MC2_phi(_m_y);
 133         */
 134
 135         MCID MC2_phi(MCID input);
 136
 137         /** Tells MC2 about the MCID for an input used within a loop.
 138          *
 139          *      Example:
 140          *
 141          *      while (...) {
 142          *              x=x+1;
 143          *              if (...)
 144          *                      break;
 145          *      }
 146          *      // MC2_exitLoop(...);
 147          *      // MC2_loop_phi(_m_x);
 148          *
 149          */
 150
 151         MCID MC2_loop_phi(MCID input);
 152
 153         /** Tells MC2 about a yield. (Placed by programmers.) */
 154         void MC2_yield();
 155
 156         /** Tells MC2 that the next operation is a memory fence. */
 157         void MC2_fence();
 158
 159         /** Tells MC2 that the next statement is the head of a loop. */
 160         void MC2_enterLoop();
 161
 162         /** Tells MC2 that the previous statement exits a loop. */
 163         void MC2_exitLoop();
 164
 165         /** Tells MC2 that a loop is starting a new iteration.
 166          *      Not currently strictly required. */
 167         void MC2_loopIterate();
 168 #ifdef __cplusplus
 169 }
 170 #endif
 171
 172 #endif /* __LIBINTERFACE_H__ */