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
|
[kernel] Parsing share/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing tests/syntax/assembly_gmp.c (with preprocessing)
/* Generated by Frama-C */
typedef unsigned long 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);
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;
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);
}
/*@ assigns r2, r1, r0;
assigns r2 \from r0, p1, *(ap + (n - 3)), p0;
assigns r1 \from r0, p1, *(ap + (n - 3)), p0;
assigns r0 \from r0, p1, *(ap + (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" ((unsigned long)r0), "rme" ((unsigned long)p1),
"%2" ((unsigned long)*(ap + (n - (mp_size_t)3))),
"rme" ((unsigned long)p0)
);
j = n - (mp_size_t)4;
while (j >= (mp_size_t)0) {
{
mp_limb_t cy;
{
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;
/*@ 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" ((unsigned long)r0), "rme" ((unsigned long)p1),
"%2" ((unsigned long)*(ap + j)), "rme" ((unsigned long)p0)
);
}
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 >> (64 - 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;
}
|
