1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
|
[kernel] Parsing assembly_gmp.c (with preprocessing)
/* Generated by Frama-C */
#include "stddef.h"
typedef long mp_limb_t;
typedef unsigned long UDItype;
typedef long *mp_srcptr;
typedef size_t mp_size_t;
void ADDC_LIMB(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
void udiv_rnnd_preinv(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
mp_limb_t mpn_mod_1_1p(mp_srcptr ap, mp_size_t n, mp_limb_t b,
mp_limb_t const bmodb[4])
{
mp_limb_t __retres;
int cnt;
mp_limb_t bi;
mp_limb_t r0;
mp_limb_t r1;
mp_limb_t r;
r0 = *(ap + (n - (mp_size_t)2));
r1 = *(ap + (n - (mp_size_t)1));
if (n > (mp_size_t)2) {
mp_limb_t B2modb;
mp_limb_t B2mb;
mp_limb_t p0;
mp_limb_t p1;
mp_limb_t r2;
mp_size_t j;
B2modb = *(bmodb + 3);
B2mb = B2modb - b;
{
UDItype __m0 = (UDItype)r1;
UDItype __m1 = (UDItype)B2modb;
/*@ assigns p1;
assigns p1 \from r1, B2modb; */
__asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
p0 = (mp_limb_t)(__m0 * __m1);
}
/*@ assigns r2, r1, r0;
assigns r2 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
assigns r1 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
assigns r0 \from r0, p1, *(ap + (mp_size_t)(n - 3)), p0;
*/
__asm__ (
"add\t%6, %q2\n\t"
"adc\t%4, %q1\n\t"
"sbb\t%q0, %q0"
: "=r" (r2), "=r" (r1), "=&r" (r0)
: "1" ((UDItype)r0), "rme" ((UDItype)p1),
"%2" ((UDItype)*(ap + (n - (mp_size_t)3))), "rme" ((UDItype)p0)
);
j = n - (mp_size_t)4;
while (j >= (mp_size_t)0) {
{
mp_limb_t cy;
{
UDItype __m0_0 = (UDItype)r1;
UDItype __m1_0 = (UDItype)B2modb;
/*@ assigns p1;
assigns p1 \from r1, B2modb; */
__asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
p0 = (mp_limb_t)(__m0_0 * __m1_0);
}
ADDC_LIMB(cy,r0,r0,r2 & B2modb);
r0 -= - cy & b;
/*@ assigns r2, r1, r0;
assigns r2 \from r0, p1, *(ap + j), p0;
assigns r1 \from r0, p1, *(ap + j), p0;
assigns r0 \from r0, p1, *(ap + j), p0;
*/
__asm__ (
"add\t%6, %q2\n\t"
"adc\t%4, %q1\n\t"
"sbb\t%q0, %q0"
: "=r" (r2), "=r" (r1), "=&r" (r0)
: "1" ((UDItype)r0), "rme" ((UDItype)p1),
"%2" ((UDItype)*(ap + j)), "rme" ((UDItype)p0)
);
}
j --;
}
r1 -= r2 & b;
}
cnt = (int)*(bmodb + 1);
if (cnt != 0) {
mp_limb_t t;
mp_limb_t B1modb = *(bmodb + 2);
{
UDItype __m0_1 = (UDItype)r1;
UDItype __m1_1 = (UDItype)B1modb;
/*@ assigns r1;
assigns r1 \from r1, B1modb; */
__asm__ ("umulh %r1,%2,%0" : "=r" (r1) : "%rJ" (r1), "rI" (B1modb));
t = (mp_limb_t)(__m0_1 * __m1_1);
}
r0 += t;
r1 += (mp_limb_t)(r0 < t);
r1 = (r1 << cnt) | (r0 >> (64 - cnt));
r0 <<= cnt;
}
else {
mp_limb_t mask = - ((mp_limb_t)(r1 >= b));
r1 -= mask & b;
}
bi = *(bmodb + 0);
udiv_rnnd_preinv(r,r1,r0,b,bi);
__retres = r >> cnt;
return __retres;
}
int loc[10];
void f(void)
{
unsigned long ulValue;
unsigned long *pulValue = & ulValue;
/*@ assigns loc[0 .. 9];
assigns loc[0 .. 9] \from loc[0 .. 9]; */
__asm__ ("sidt %0\n" : : "m" (loc));
/*@ assigns *(pulValue + (..));
assigns *(pulValue + (..))
\from (indirect: pulValue), *(pulValue + (..));
*/
__asm__ ("movq $36, (%0)" : : "r" (pulValue));
int a = 2;
int b = 3;
/*@ assigns a;
assigns a \from b; */
__asm__ ("mov %1, %0" : "=r" (a) : "r" (b) : "%eax");
return;
}
|
