CBMC
•All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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
5long _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
19long _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
31short _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
43char _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
55long _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
67short _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
79char _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
91long _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
104long 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
118long _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
130long _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
142char _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
154short _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
166long _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
178char _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
190short _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
202long _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
214char _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
226short _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
238long _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
250long _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
262void _mm_lfence(void)
263{
264 __CPROVER_HIDE:;
265}
266
267/* FUNCTION: _mm_mfence */
268
269void _mm_mfence(void)
270{
271 __CPROVER_HIDE:;
272 __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
273}
274
275/* FUNCTION: _WriteBarrier */
276
277void _WriteBarrier(void)
278{
279 __CPROVER_HIDE:;
280}
281
282/* FUNCTION: _ReadWriteBarrier */
283
284void _ReadWriteBarrier(void)
285{
286 __CPROVER_HIDE:;
287 __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
288}
289
290/* FUNCTION: _ReadBarrier */
291
292void _ReadBarrier(void)
293{
294 __CPROVER_HIDE:;
295}
296
297/* FUNCTION: _InterlockedIncrement16 */
298
299short _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
311short _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
323short _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
336char _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
455int _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
469int _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
483int _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
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
__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