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