Fix apparent bug...
[satcheck.git] / libinterface.cc
1 /*      Copyright (c) 2015 Regents of the University of California
2  *
3  *      Author: Brian Demsky <bdemsky@uci.edu>
4  *
5  *      This program is free software; you can redistribute it and/or
6  *      modify it under the terms of the GNU General Public License
7  *      version 2 as published by the Free Software Foundation.
8  */
9
10 #define __STDC_FORMAT_MACROS
11 #include <inttypes.h>
12 #include <stdarg.h>
13
14 #include "libinterface.h"
15 #include "common.h"
16 #include "model.h"
17 #include "threads-model.h"
18 #include "mcexecution.h"
19
20 void store_8(void *addr, uint8_t val)
21 {
22         DEBUG("addr = %p, val = %" PRIu8 "\n", addr, val);
23         model->get_execution()->store(addr, val, sizeof(val));
24 }
25
26 void store_16(void *addr, uint16_t val)
27 {
28         DEBUG("addr = %p, val = %" PRIu16 "\n", addr, val);
29         model->get_execution()->store(addr, val, sizeof(val));
30 }
31
32 void store_32(void *addr, uint32_t val)
33 {
34         DEBUG("addr = %p, val = %" PRIu32 "\n", addr, val);
35         model->get_execution()->store(addr, val, sizeof(val));
36 }
37
38 void store_64(void *addr, uint64_t val)
39 {
40         DEBUG("addr = %p, val = %" PRIu64 "\n", addr, val);
41         model->get_execution()->store(addr, val, sizeof(val));
42 }
43
44 uint8_t load_8(const void *addr)
45 {
46         DEBUG("addr = %p\n", addr);
47         return (uint8_t) model->get_execution()->load(addr, sizeof(uint8_t));
48 }
49
50 uint16_t load_16(const void *addr)
51 {
52         DEBUG("addr = %p\n", addr);
53         return (uint16_t) model->get_execution()->load(addr,  sizeof(uint16_t));
54 }
55
56 uint32_t load_32(const void *addr)
57 {
58         DEBUG("addr = %p\n", addr);
59         return (uint32_t) model->get_execution()->load(addr, sizeof(uint32_t));
60 }
61
62 uint64_t load_64(const void *addr)
63 {
64         DEBUG("addr = %p\n", addr);
65         return (uint64_t) model->get_execution()->load(addr,  sizeof(uint64_t));
66 }
67
68 uint8_t rmw_8(enum atomicop op, void *addr, uint8_t oldval, uint8_t valarg) {
69         return (uint8_t) model->get_execution()->rmw(op, addr, sizeof(oldval), (uint64_t) *((uint8_t *)addr), (uint64_t) oldval, (uint64_t) valarg);
70 }
71
72 uint16_t rmw_16(enum atomicop op, void *addr, uint16_t oldval, uint16_t valarg) {
73         return (uint16_t) model->get_execution()->rmw(op, addr, sizeof(oldval), (uint64_t) *((uint16_t *)addr), (uint64_t) oldval, (uint64_t) valarg);
74 }
75
76 uint32_t rmw_32(enum atomicop op, void *addr, uint32_t oldval, uint32_t valarg) {
77         return (uint32_t) model->get_execution()->rmw(op, addr, sizeof(oldval), (uint64_t) *((uint32_t *)addr), (uint64_t) oldval, (uint64_t) valarg);
78 }
79
80 uint64_t rmw_64(enum atomicop op, void *addr, uint64_t oldval, uint64_t valarg) {
81         return model->get_execution()->rmw(op, addr, sizeof(oldval), *((uint64_t *)addr), oldval, valarg);
82 }
83
84 void MC2_nextOpThrd_create(MCID startfunc, MCID param) {
85 }
86
87 void MC2_nextOpThrd_join(MCID jointhrd) {
88 }
89
90 MCID MC2_nextOpLoad(MCID addr) {
91         return model->get_execution()->loadMCID(addr, 0);
92 }
93
94 void MC2_nextOpStore(MCID addr, MCID value) {
95         return model->get_execution()->storeMCID(addr, 0, value);
96 }
97
98 MCID MC2_nextOpLoadOffset(MCID addr, uintptr_t offset) {
99         return model->get_execution()->loadMCID(addr, offset);
100 }
101
102 void MC2_nextOpStoreOffset(MCID addr, uintptr_t offset, MCID value) {
103         return model->get_execution()->storeMCID(addr, offset, value);
104 }
105
106 MCID MC2_branchUsesID(MCID condition, int direction, int num_directions, bool anyvalue) {
107         return model->get_execution()->branchDir(condition, direction, num_directions, anyvalue);
108 }
109
110 void MC2_merge(MCID branchid) {
111         model->get_execution()->merge(branchid);
112 }
113
114 MCID MC2_phi(MCID input) {
115         return model->get_execution()->phi(input);
116 }
117
118 MCID MC2_loop_phi(MCID input) {
119         return model->get_execution()->loop_phi(input);
120 }
121
122 uint64_t MC2_equals(MCID op1, uint64_t val1, MCID op2, uint64_t val2, MCID *retval) {
123         return model->get_execution()->equals(op1, val1, op2, val2, retval);
124 }
125
126
127 MCID MC2_function(uint num_args, int numbytesretval, uint64_t val, ...) {
128         va_list vl;
129         MCID mcids[num_args];
130         va_start(vl, val);
131         uint num_real_args=0;;
132         for(uint i=0;i<num_args;i++) {
133                 MCID v=va_arg(vl, MCID);
134                 if (v!=MCID_NODEP)
135                         mcids[num_real_args++]=v;
136         }
137         va_end(vl);
138         MCID m=model->get_execution()->function(0, numbytesretval, val, num_real_args, mcids);
139         return m;
140 }
141
142 MCID MC2_function_id(unsigned int id, uint num_args, int numbytesretval, uint64_t val, ...) {
143         va_list vl;
144         MCID mcids[num_args];
145         va_start(vl, val);
146         uint num_real_args=0;;
147         for(uint i=0;i<num_args;i++) {
148                 MCID v=va_arg(vl, MCID);
149                 if (v!=MCID_NODEP)
150                         mcids[num_real_args++]=v;
151         }
152         va_end(vl);
153         MCID m=model->get_execution()->function(id, numbytesretval, val, num_real_args, mcids);
154         return m;
155 }
156
157 void MC2_enterLoop() {
158         model->get_execution()->enterLoop();
159 }
160
161 void MC2_exitLoop() {
162         model->get_execution()->exitLoop();
163 }
164
165 void MC2_loopIterate() {
166         model->get_execution()->loopIterate();
167 }
168
169 void MC2_yield() {
170         model->get_execution()->threadYield();
171 }
172
173 void MC2_fence() {
174 #ifdef TSO
175         model->get_execution()->fence();
176 #endif
177 }
178
179
180 MCID MC2_nextRMW(MCID addr, MCID oldval, MCID valarg) {
181         return model->get_execution()->nextRMW(addr, 0, oldval, valarg);
182 }
183
184 MCID MC2_nextRMWOffset(MCID addr, uintptr_t offset, MCID oldval, MCID valarg) {
185         return model->get_execution()->nextRMW(addr, offset, oldval, valarg);
186 }