1 /** @file libinterface.h
2 * @brief Interface to check normal memory operations for data races.
5 #ifndef __LIBINTERFACE_H__
6 #define __LIBINTERFACE_H__
13 typedef unsigned int MCID;
14 #define MC2_PTR_LENGTH sizeof(void *)
16 #define MCID_NODEP ((MCID)0)
17 #define MCID_INIT ((MCID)0)
18 #define MCID_FIRST ((MCID)1)
20 #define MC2_OFFSET(x, y) (uintptr_t)(&((x)(0))->y)
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);
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);
34 /** Atomic operation enumeration for RMW operations. */
38 CAS /* Compare and swap */,
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. */
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);
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. */
62 MCID MC2_nextRMW(MCID addr, MCID oldval, MCID valarg);
63 MCID MC2_nextOpLoad(MCID addr);
64 void MC2_nextOpStore(MCID addr, MCID value);
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.
70 * e.g. load_8(x.f) could be instrumented with
71 * MC2_nextOpLoadOffset(_m_x, offset of f in structure x). */
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);
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. */
84 MCID MC2_branchUsesID(MCID condition, int direction, int num_directions, bool anyvalue);
86 /** Currently not used. TODO implement later. */
87 void MC2_nextOpThrd_create(MCID startfunc, MCID param);
88 void MC2_nextOpThrd_join(MCID jointhrd);
90 /** Tells MC2 that we hit the merge point of a conditional
91 * branch. branchid is the MCID returned by the corresponding
92 * MC2_branchUsesID function for the branch that just merged. */
93 void MC2_merge(MCID branchid);
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
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, ...);
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, ...);
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);
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.
125 * MC2_phi enables instrumenting cases like:
131 * // must put here: MC2_merge(_branch_id);
135 MCID MC2_phi(MCID input);
137 /** Tells MC2 about the MCID for an input used within a loop.
146 * // MC2_exitLoop(...);
147 * // MC2_loop_phi(_m_x);
151 MCID MC2_loop_phi(MCID input);
153 /** Tells MC2 about a yield. (Placed by programmers.) */
156 /** Tells MC2 that the next operation is a memory fence. */
159 /** Tells MC2 that the next statement is the head of a loop. */
160 void MC2_enterLoop();
162 /** Tells MC2 that the previous statement exits a loop. */
165 /** Tells MC2 that a loop is starting a new iteration.
166 * Not currently strictly required. */
167 void MC2_loopIterate();
172 #endif /* __LIBINTERFACE_H__ */