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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/assembly_gmp.c (with preprocessing)
tests/syntax/assembly_gmp.c:137:[kernel] warning: Calling undeclared function USItype. Old style K&R code?
/* Generated by Frama-C */
typedef unsigned int size_t;
typedef long mp_limb_t;
typedef unsigned long UDItype;
typedef long *mp_srcptr;
typedef size_t mp_size_t;
extern void ADDC_LIMB(mp_limb_t, mp_limb_t, mp_limb_t, mp_limb_t);
extern 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 * /*[4]*/ bmodb)
{
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 __m1;
__m0 = (unsigned long)r1;
__m1 = (unsigned long)B2modb;
/*@ assigns p1;
assigns p1 \from r1, B2modb; */
__asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
p0 = (long)(__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 __m1_0;
__m0_0 = (unsigned long)r1;
__m1_0 = (unsigned long)B2modb;
/*@ assigns p1;
assigns p1 \from r1, B2modb; */
__asm__ ("umulh %r1,%2,%0" : "=r" (p1) : "%rJ" (r1), "rI" (B2modb));
p0 = (long)(__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_0;
B1modb_0 = *(bmodb + 2);
{
UDItype __m0_1;
UDItype __m1_1;
__m0_1 = (unsigned long)r1;
__m1_1 = (unsigned long)B1modb_0;
/*@ assigns r1;
assigns r1 \from r1, B1modb_0; */
__asm__ ("umulh %r1,%2,%0" : "=r" (r1) : "%rJ" (r1), "rI" (B1modb_0));
t = (long)(__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;
mask = - ((long)(r1 >= b));
r1 -= mask & b;
}
bi = *(bmodb + 0);
udiv_rnnd_preinv(r,r1,r0,b,bi);
__retres = r >> cnt;
return __retres;
}
|
