CBMC
intrin.c
Go to the documentation of this file.
1 /* intrin.h is an include file provided by Visual Studio */
2 
3 /* FUNCTION: _InterlockedDecrement */
4 
5 long _InterlockedDecrement(long volatile *p)
6 {
7  __CPROVER_HIDE:;
8  // This function generates a full memory barrier (or fence) to ensure that
9  // memory operations are completed in order.
10  __CPROVER_atomic_begin();
11  long result=--(*p);
12  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
13  __CPROVER_atomic_end();
14  return result;
15 }
16 
17 /* FUNCTION: _InterlockedExchange */
18 
19 long _InterlockedExchange(long volatile *p, long v)
20 {
21  __CPROVER_HIDE:;
22  __CPROVER_atomic_begin();
23  long old=*p;
24  *p=v;
25  __CPROVER_atomic_end();
26  return old;
27 }
28 
29 /* FUNCTION: _InterlockedExchange16 */
30 
31 short _InterlockedExchange16(short volatile *p, short v)
32 {
33  __CPROVER_HIDE:;
34  __CPROVER_atomic_begin();
35  short old=*p;
36  *p=v;
37  __CPROVER_atomic_end();
38  return old;
39 }
40 
41 /* FUNCTION: _InterlockedExchange8 */
42 
43 char _InterlockedExchange8(char volatile *p, char v)
44 {
45  __CPROVER_HIDE:;
46  __CPROVER_atomic_begin();
47  char old=*p;
48  *p=v;
49  __CPROVER_atomic_end();
50  return old;
51 }
52 
53 /* FUNCTION: _InterlockedExchangeAdd */
54 
55 long _InterlockedExchangeAdd(long volatile *p, long v)
56 {
57  __CPROVER_HIDE:;
58  __CPROVER_atomic_begin();
59  long result=(*p)+=v;
60  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
61  __CPROVER_atomic_end();
62  return result;
63 }
64 
65 /* FUNCTION: _InterlockedExchangeAdd16 */
66 
67 short _InterlockedExchangeAdd16(short volatile *p, short v)
68 {
69  __CPROVER_HIDE:;
70  __CPROVER_atomic_begin();
71  short result=(*p)+=v;
72  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
73  __CPROVER_atomic_end();
74  return result;
75 }
76 
77 /* FUNCTION: _InterlockedExchangeAdd8 */
78 
79 char _InterlockedExchangeAdd8(char volatile *p, char v)
80 {
81  __CPROVER_HIDE:;
82  __CPROVER_atomic_begin();
83  char result=(*p)+=v;
84  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
85  __CPROVER_atomic_end();
86  return result;
87 }
88 
89 /* FUNCTION: _InterlockedCompareExchange */
90 
91 long _InterlockedCompareExchange(long volatile *p, long v1, long v2)
92 {
93  __CPROVER_HIDE:;
94  __CPROVER_atomic_begin();
95  long old=(*p);
96  *p=(old==v2)?v1:old;
97  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
98  __CPROVER_atomic_end();
99  return old;
100 }
101 
102 /* FUNCTION: _InterlockedCompareExchange64 */
103 
104 long long
105 _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2)
106 {
107  __CPROVER_HIDE:;
108  __CPROVER_atomic_begin();
109  long long old=(*p);
110  *p=(old==v2)?v1:old;
111  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
112  __CPROVER_atomic_end();
113  return old;
114 }
115 
116 /* FUNCTION: __InterlockedIncrement */
117 
118 long _InterlockedIncrement(long volatile *p)
119 {
120  __CPROVER_HIDE:;
121  __CPROVER_atomic_begin();
122  long result=++(*p);
123  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
124  __CPROVER_atomic_end();
125  return result;
126 }
127 
128 /* FUNCTION: _InterlockedOr */
129 
130 long _InterlockedOr(long volatile *p, long v)
131 {
132  __CPROVER_HIDE:;
133  __CPROVER_atomic_begin();
134  long result=(*p)|=v;
135  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
136  __CPROVER_atomic_end();
137  return result;
138 }
139 
140 /* FUNCTION: _InterlockedOr8 */
141 
142 char _InterlockedOr8(char volatile *p, char v)
143 {
144  __CPROVER_HIDE:;
145  __CPROVER_atomic_begin();
146  char result=(*p)|=v;
147  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
148  __CPROVER_atomic_end();
149  return result;
150 }
151 
152 /* FUNCTION: _InterlockedOr16 */
153 
154 short _InterlockedOr16(short volatile *p, short v)
155 {
156  __CPROVER_HIDE:;
157  __CPROVER_atomic_begin();
158  short result=(*p)|=v;
159  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
160  __CPROVER_atomic_end();
161  return result;
162 }
163 
164 /* FUNCTION: _InterlockedXor */
165 
166 long _InterlockedXor(long volatile *p, long v)
167 {
168  __CPROVER_HIDE:;
169  __CPROVER_atomic_begin();
170  long result=(*p)^=v;
171  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
172  __CPROVER_atomic_end();
173  return result;
174 }
175 
176 /* FUNCTION: _InterlockedXor8 */
177 
178 char _InterlockedXor8(char volatile *p, char v)
179 {
180  __CPROVER_HIDE:;
181  __CPROVER_atomic_begin();
182  char result=(*p)^=v;
183  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
184  __CPROVER_atomic_end();
185  return result;
186 }
187 
188 /* FUNCTION: _InterlockedXor16 */
189 
190 short _InterlockedXor16(short volatile *p, short v)
191 {
192  __CPROVER_HIDE:;
193  __CPROVER_atomic_begin();
194  short result=(*p)^=v;
195  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
196  __CPROVER_atomic_end();
197  return result;
198 }
199 
200 /* FUNCTION: _InterlockedAnd */
201 
202 long _InterlockedAnd(long volatile *p, long v)
203 {
204  __CPROVER_HIDE:;
205  __CPROVER_atomic_begin();
206  long result=(*p)&=v;
207  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
208  __CPROVER_atomic_end();
209  return result;
210 }
211 
212 /* FUNCTION: _InterlockedAnd8 */
213 
214 char _InterlockedAnd8(char volatile *p, char v)
215 {
216  __CPROVER_HIDE:;
217  __CPROVER_atomic_begin();
218  char result=(*p)&=v;
219  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
220  __CPROVER_atomic_end();
221  return result;
222 }
223 
224 /* FUNCTION: _InterlockedAnd16 */
225 
226 short _InterlockedAnd16(short volatile *p, short v)
227 {
228  __CPROVER_HIDE:;
229  __CPROVER_atomic_begin();
230  short result=(*p)&=v;
231  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
232  __CPROVER_atomic_end();
233  return result;
234 }
235 
236 /* FUNCTION: _InterlockedAdd */
237 
238 long _InterlockedAdd(long volatile *p, long v)
239 {
240  __CPROVER_HIDE:;
241  __CPROVER_atomic_begin();
242  long result=(*p)+=v;
243  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
244  __CPROVER_atomic_end();
245  return result;
246 }
247 
248 /* FUNCTION: _InterlockedAddLargeStatistic */
249 
250 long _InterlockedAddLargeStatistic(long long volatile *p, long v)
251 {
252  __CPROVER_HIDE:;
253  // not atomic:
254  // http://msdn.microsoft.com/en-us/library/yc92ytxy%28v=vs.90%29.aspx
255  (*p)+=v;
256  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
257  return v;
258 }
259 
260 /* FUNCTION: _mm_lfence */
261 
262 void _mm_lfence(void)
263 {
264  __CPROVER_HIDE:;
265 }
266 
267 /* FUNCTION: _mm_mfence */
268 
269 void _mm_mfence(void)
270 {
271  __CPROVER_HIDE:;
272  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
273 }
274 
275 /* FUNCTION: _WriteBarrier */
276 
277 void _WriteBarrier(void)
278 {
279  __CPROVER_HIDE:;
280 }
281 
282 /* FUNCTION: _ReadWriteBarrier */
283 
284 void _ReadWriteBarrier(void)
285 {
286  __CPROVER_HIDE:;
287  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
288 }
289 
290 /* FUNCTION: _ReadBarrier */
291 
292 void _ReadBarrier(void)
293 {
294  __CPROVER_HIDE:;
295 }
296 
297 /* FUNCTION: _InterlockedIncrement16 */
298 
299 short _InterlockedIncrement16(short volatile *p)
300 {
301  __CPROVER_HIDE:;
302  __CPROVER_atomic_begin();
303  short result=++(*p);
304  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
305  __CPROVER_atomic_end();
306  return result;
307 }
308 
309 /* FUNCTION: _InterlockedDecrement16 */
310 
311 short _InterlockedDecrement16(short volatile *p)
312 {
313  __CPROVER_HIDE:;
314  __CPROVER_atomic_begin();
315  short result=--(*p);
316  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
317  __CPROVER_atomic_end();
318  return result;
319 }
320 
321 /* FUNCTION: _InterlockedCompareExchange16 */
322 
323 short _InterlockedCompareExchange16(short volatile *p, short v1, short v2)
324 {
325  __CPROVER_HIDE:;
326  __CPROVER_atomic_begin();
327  short old=(*p);
328  *p=(old==v2)?v1:old;
329  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
330  __CPROVER_atomic_end();
331  return old;
332 }
333 
334 /* FUNCTION: _InterlockedCompareExchange8 */
335 
336 char _InterlockedCompareExchange8(char volatile *p, char v1, char v2)
337 {
338  __CPROVER_HIDE:;
339  __CPROVER_atomic_begin();
340  char old=(*p);
341  *p=(old==v2)?v1:old;
342  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
343  __CPROVER_atomic_end();
344  return old;
345 }
346 
347 /* FUNCTION: _mm_set_epi32 */
348 
349 #ifdef _MSC_VER
350 # ifndef __CPROVER_INTRIN_H_INCLUDED
351 # include <intrin.h>
352 # define __CPROVER_INTRIN_H_INCLUDED
353 # endif
354 
355 __m128i _mm_set_epi32(int e3, int e2, int e1, int e0)
356 {
357  return (__m128i){.m128i_i32 = {e0, e1, e2, e3}};
358 }
359 #endif
360 
361 /* FUNCTION: _mm_setr_epi32 */
362 
363 #ifdef _MSC_VER
364 # ifndef __CPROVER_INTRIN_H_INCLUDED
365 # include <intrin.h>
366 # define __CPROVER_INTRIN_H_INCLUDED
367 # endif
368 
369 __m128i _mm_setr_epi32(int e3, int e2, int e1, int e0)
370 {
371  return (__m128i){.m128i_i32 = {e3, e2, e1, e0}};
372 }
373 #endif
374 
375 /* FUNCTION: _mm_set_epi16 */
376 
377 #ifdef _MSC_VER
378 # ifndef __CPROVER_INTRIN_H_INCLUDED
379 # include <intrin.h>
380 # define __CPROVER_INTRIN_H_INCLUDED
381 # endif
382 
383 __m128i _mm_set_epi16(
384  short e7,
385  short e6,
386  short e5,
387  short e4,
388  short e3,
389  short e2,
390  short e1,
391  short e0)
392 {
393  return (__m128i){.m128i_i16 = {e0, e1, e2, e3, e4, e5, e6, e7}};
394 }
395 #endif
396 
397 /* FUNCTION: _mm_setr_epi16 */
398 
399 #ifdef _MSC_VER
400 # ifndef __CPROVER_INTRIN_H_INCLUDED
401 # include <intrin.h>
402 # define __CPROVER_INTRIN_H_INCLUDED
403 # endif
404 
405 __m128i _mm_setr_epi16(
406  short e7,
407  short e6,
408  short e5,
409  short e4,
410  short e3,
411  short e2,
412  short e1,
413  short e0)
414 {
415  return (__m128i){.m128i_i16 = {e7, e6, e5, e4, e3, e2, e1, e0}};
416 }
417 #endif
418 
419 /* FUNCTION: _mm_set_pi16 */
420 
421 #ifdef _MSC_VER
422 # ifndef __CPROVER_INTRIN_H_INCLUDED
423 # include <intrin.h>
424 # define __CPROVER_INTRIN_H_INCLUDED
425 # endif
426 
427 __m64 _mm_set_pi16(short e3, short e2, short e1, short e0)
428 {
429  return (__m64){.m64_i16 = {e0, e1, e2, e3}};
430 }
431 #endif
432 
433 /* FUNCTION: _mm_setr_pi16 */
434 
435 #ifdef _MSC_VER
436 # ifndef __CPROVER_INTRIN_H_INCLUDED
437 # include <intrin.h>
438 # define __CPROVER_INTRIN_H_INCLUDED
439 # endif
440 
441 __m64 _mm_setr_pi16(short e3, short e2, short e1, short e0)
442 {
443  return (__m64){.m64_i16 = {e3, e2, e1, e0}};
444 }
445 #endif
446 
447 /* FUNCTION: _mm_extract_epi32 */
448 
449 #ifdef _MSC_VER
450 # ifndef __CPROVER_INTRIN_H_INCLUDED
451 # include <intrin.h>
452 # define __CPROVER_INTRIN_H_INCLUDED
453 # endif
454 
455 int _mm_extract_epi32(__m128i a, const int imm8)
456 {
457  return a.m128i_i32[imm8];
458 }
459 #endif
460 
461 /* FUNCTION: _mm_extract_epi16 */
462 
463 #ifdef _MSC_VER
464 # ifndef __CPROVER_INTRIN_H_INCLUDED
465 # include <intrin.h>
466 # define __CPROVER_INTRIN_H_INCLUDED
467 # endif
468 
469 int _mm_extract_epi16(__m128i a, const int imm8)
470 {
471  return a.m128i_i16[imm8];
472 }
473 #endif
474 
475 /* FUNCTION: _mm_extract_pi16 */
476 
477 #ifdef _MSC_VER
478 # ifndef __CPROVER_INTRIN_H_INCLUDED
479 # include <intrin.h>
480 # define __CPROVER_INTRIN_H_INCLUDED
481 # endif
482 
483 int _mm_extract_pi16(__m64 a, const int imm8)
484 {
485  return a.m64_i16[imm8];
486 }
487 #endif
488 
489 /* FUNCTION: _mm_adds_epi16 */
490 
491 #ifdef _MSC_VER
492 # ifndef __CPROVER_INTRIN_H_INCLUDED
493 # include <intrin.h>
494 # define __CPROVER_INTRIN_H_INCLUDED
495 # endif
496 
497 __m128i _mm_adds_epi16(__m128i a, __m128i b)
498 {
499  return (__m128i){
500  .m128i_i16 = {
501  __CPROVER_saturating_plus(a.m128i_i16[0], b.m128i_i16[0]),
502  __CPROVER_saturating_plus(a.m128i_i16[1], b.m128i_i16[1]),
503  __CPROVER_saturating_plus(a.m128i_i16[2], b.m128i_i16[2]),
504  __CPROVER_saturating_plus(a.m128i_i16[3], b.m128i_i16[3]),
505  __CPROVER_saturating_plus(a.m128i_i16[4], b.m128i_i16[4]),
506  __CPROVER_saturating_plus(a.m128i_i16[5], b.m128i_i16[5]),
507  __CPROVER_saturating_plus(a.m128i_i16[6], b.m128i_i16[6]),
508  __CPROVER_saturating_plus(a.m128i_i16[7], b.m128i_i16[7]),
509  }};
510 }
511 #endif
512 
513 /* FUNCTION: _mm_subs_epi16 */
514 
515 #ifdef _MSC_VER
516 # ifndef __CPROVER_INTRIN_H_INCLUDED
517 # include <intrin.h>
518 # define __CPROVER_INTRIN_H_INCLUDED
519 # endif
520 
521 __m128i _mm_subs_epi16(__m128i a, __m128i b)
522 {
523  return (__m128i){
524  .m128i_i16 = {
525  __CPROVER_saturating_minus(a.m128i_i16[0], b.m128i_i16[0]),
526  __CPROVER_saturating_minus(a.m128i_i16[1], b.m128i_i16[1]),
527  __CPROVER_saturating_minus(a.m128i_i16[2], b.m128i_i16[2]),
528  __CPROVER_saturating_minus(a.m128i_i16[3], b.m128i_i16[3]),
529  __CPROVER_saturating_minus(a.m128i_i16[4], b.m128i_i16[4]),
530  __CPROVER_saturating_minus(a.m128i_i16[5], b.m128i_i16[5]),
531  __CPROVER_saturating_minus(a.m128i_i16[6], b.m128i_i16[6]),
532  __CPROVER_saturating_minus(a.m128i_i16[7], b.m128i_i16[7]),
533  }};
534 }
535 #endif
536 
537 /* FUNCTION: _mm_adds_epu16 */
538 
539 #ifdef _MSC_VER
540 # ifndef __CPROVER_INTRIN_H_INCLUDED
541 # include <intrin.h>
542 # define __CPROVER_INTRIN_H_INCLUDED
543 # endif
544 
545 __m128i _mm_adds_epu16(__m128i a, __m128i b)
546 {
547  return (__m128i){
548  .m128i_i16 = {
549  __CPROVER_saturating_plus(a.m128i_u16[0], b.m128i_u16[0]),
550  __CPROVER_saturating_plus(a.m128i_u16[1], b.m128i_u16[1]),
551  __CPROVER_saturating_plus(a.m128i_u16[2], b.m128i_u16[2]),
552  __CPROVER_saturating_plus(a.m128i_u16[3], b.m128i_u16[3]),
553  __CPROVER_saturating_plus(a.m128i_u16[4], b.m128i_u16[4]),
554  __CPROVER_saturating_plus(a.m128i_u16[5], b.m128i_u16[5]),
555  __CPROVER_saturating_plus(a.m128i_u16[6], b.m128i_u16[6]),
556  __CPROVER_saturating_plus(a.m128i_u16[7], b.m128i_u16[7]),
557  }};
558 }
559 #endif
560 
561 /* FUNCTION: _mm_subs_epu16 */
562 
563 #ifdef _MSC_VER
564 # ifndef __CPROVER_INTRIN_H_INCLUDED
565 # include <intrin.h>
566 # define __CPROVER_INTRIN_H_INCLUDED
567 # endif
568 
569 __m128i _mm_subs_epu16(__m128i a, __m128i b)
570 {
571  return (__m128i){
572  .m128i_u16 = {
573  __CPROVER_saturating_minus(a.m128i_u16[0], b.m128i_u16[0]),
574  __CPROVER_saturating_minus(a.m128i_u16[1], b.m128i_u16[1]),
575  __CPROVER_saturating_minus(a.m128i_u16[2], b.m128i_u16[2]),
576  __CPROVER_saturating_minus(a.m128i_u16[3], b.m128i_u16[3]),
577  __CPROVER_saturating_minus(a.m128i_u16[4], b.m128i_u16[4]),
578  __CPROVER_saturating_minus(a.m128i_u16[5], b.m128i_u16[5]),
579  __CPROVER_saturating_minus(a.m128i_u16[6], b.m128i_u16[6]),
580  __CPROVER_saturating_minus(a.m128i_u16[7], b.m128i_u16[7]),
581  }};
582 }
583 #endif
__CPROVER_fence
void __CPROVER_fence(const char *kind,...)
__CPROVER_atomic_begin
void __CPROVER_atomic_begin(void)
__CPROVER_atomic_end
void __CPROVER_atomic_end(void)
_InterlockedDecrement
long _InterlockedDecrement(long volatile *p)
Definition: intrin.c:5
_WriteBarrier
void _WriteBarrier(void)
Definition: intrin.c:277
_InterlockedXor16
short _InterlockedXor16(short volatile *p, short v)
Definition: intrin.c:190
_InterlockedExchangeAdd
long _InterlockedExchangeAdd(long volatile *p, long v)
Definition: intrin.c:55
_InterlockedOr
long _InterlockedOr(long volatile *p, long v)
Definition: intrin.c:130
_InterlockedOr8
char _InterlockedOr8(char volatile *p, char v)
Definition: intrin.c:142
_ReadWriteBarrier
void _ReadWriteBarrier(void)
Definition: intrin.c:284
_InterlockedAnd8
char _InterlockedAnd8(char volatile *p, char v)
Definition: intrin.c:214
_InterlockedExchangeAdd16
short _InterlockedExchangeAdd16(short volatile *p, short v)
Definition: intrin.c:67
_InterlockedCompareExchange
long _InterlockedCompareExchange(long volatile *p, long v1, long v2)
Definition: intrin.c:91
_InterlockedOr16
short _InterlockedOr16(short volatile *p, short v)
Definition: intrin.c:154
_mm_mfence
void _mm_mfence(void)
Definition: intrin.c:269
_InterlockedExchange16
short _InterlockedExchange16(short volatile *p, short v)
Definition: intrin.c:31
_InterlockedXor
long _InterlockedXor(long volatile *p, long v)
Definition: intrin.c:166
_InterlockedExchange
long _InterlockedExchange(long volatile *p, long v)
Definition: intrin.c:19
_InterlockedAdd
long _InterlockedAdd(long volatile *p, long v)
Definition: intrin.c:238
_mm_lfence
void _mm_lfence(void)
Definition: intrin.c:262
_InterlockedAddLargeStatistic
long _InterlockedAddLargeStatistic(long long volatile *p, long v)
Definition: intrin.c:250
_InterlockedCompareExchange64
long long _InterlockedCompareExchange64(long long volatile *p, long long v1, long long v2)
Definition: intrin.c:105
_InterlockedExchangeAdd8
char _InterlockedExchangeAdd8(char volatile *p, char v)
Definition: intrin.c:79
_InterlockedCompareExchange16
short _InterlockedCompareExchange16(short volatile *p, short v1, short v2)
Definition: intrin.c:323
_InterlockedAnd16
short _InterlockedAnd16(short volatile *p, short v)
Definition: intrin.c:226
_InterlockedIncrement
long _InterlockedIncrement(long volatile *p)
Definition: intrin.c:118
_ReadBarrier
void _ReadBarrier(void)
Definition: intrin.c:292
_InterlockedExchange8
char _InterlockedExchange8(char volatile *p, char v)
Definition: intrin.c:43
_InterlockedAnd
long _InterlockedAnd(long volatile *p, long v)
Definition: intrin.c:202
_InterlockedDecrement16
short _InterlockedDecrement16(short volatile *p)
Definition: intrin.c:311
_InterlockedCompareExchange8
char _InterlockedCompareExchange8(char volatile *p, char v1, char v2)
Definition: intrin.c:336
_InterlockedXor8
char _InterlockedXor8(char volatile *p, char v)
Definition: intrin.c:178
_InterlockedIncrement16
short _InterlockedIncrement16(short volatile *p)
Definition: intrin.c:299