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
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
|
[kernel] Parsing assembly_gmp.c (with preprocessing)
[kernel:typing:implicit-function-declaration] assembly_gmp.c:137: Warning:
Calling undeclared function USItype. Old style K&R code?
/* 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);
extern int ( /* missing proto */ USItype)(long x_0);
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;
int tmp;
int tmp_0;
int tmp_1;
int tmp_2;
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);
}
tmp = USItype(r0);
tmp_0 = USItype(p1);
tmp_1 = USItype(*(ap + (n - (mp_size_t)3)));
tmp_2 = USItype(p0);
/*@ assigns r2, r1, r0;
assigns r2 \from tmp, tmp_0, tmp_1, tmp_2;
assigns r1 \from tmp, tmp_0, tmp_1, tmp_2;
assigns r0 \from tmp, tmp_0, tmp_1, tmp_2;
*/
__asm__ (
"add\t%6, %k2\n\t"
"adc\t%4, %k1\n\t"
"sbb\t%k0, %k0"
: "=r" (r2), "=r" (r1), "=&r" (r0)
: "1" (tmp), "g" (tmp_0), "%2" (tmp_1), "g" (tmp_2)
);
j = n - (mp_size_t)4;
while (j >= (mp_size_t)0) {
{
mp_limb_t cy;
int tmp_3;
int tmp_4;
int tmp_5;
int tmp_6;
{
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;
tmp_3 = USItype(r0);
tmp_4 = USItype(p1);
tmp_5 = USItype(*(ap + j));
tmp_6 = USItype(p0);
/*@ assigns r2, r1, r0;
assigns r2 \from tmp_3, tmp_4, tmp_5, tmp_6;
assigns r1 \from tmp_3, tmp_4, tmp_5, tmp_6;
assigns r0 \from tmp_3, tmp_4, tmp_5, tmp_6;
*/
__asm__ (
"add\t%6, %k2\n\t"
"adc\t%4, %k1\n\t"
"sbb\t%k0, %k0"
: "=r" (r2), "=r" (r1), "=&r" (r0)
: "1" (tmp_3), "g" (tmp_4), "%2" (tmp_5), "g" (tmp_6)
);
}
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 >> (32 - 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;
}
|
