portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Provide spec for CTZL

Browse source 
Provides a spec for the __builtin_ctzl function and changes existing
code to use this wrapper
This commit is contained in:
Adrian Danis 2017-02-21 16:06:57 +11:00
parent b3c25ec876
commit f8606c86ad
3 changed files with 18 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
include/util.h
View file

@ -90,6 +90,7 @@ long PURE str_to_long(const char* str);
#endif /* !__ASSEMBLER__ */
int __builtin_clzl (unsigned long x);
int __builtin_ctzl (unsigned long x);
/** MODIFIES: */
/** DONT_TRANSLATE */
@ -105,7 +106,20 @@ CONST clzl(unsigned long x)
return __builtin_clzl(x);
}
int __builtin_ctzl (unsigned long x);
/** MODIFIES: */
/** DONT_TRANSLATE */
/** FNSPEC ctzl_spec:
"\<forall>s. \<Gamma> \<turnstile>
{\<sigma>. s = \<sigma> \<and> x_' s \<noteq> 0 }
\<acute>ret__long :== PROC ctzl(\<acute>x)
\<lbrace> \<acute>ret__long = of_nat (word_ctz (x_' s)) \<rbrace>"
*/
static inline long
CONST ctzl(unsigned long x)
{
return __builtin_ctzl(x);
}
#define CTZL(x) __builtin_ctzl(x)
int __builtin_popcountl (unsigned long x);

4
src/arch/arm/object/vcpu.c
View file

@ -735,9 +735,9 @@ VGICMaintenance(void)
if (flags & VGIC_MISR_EOI) {
int irq_idx;
if (eisr0) {
irq_idx = __builtin_ctz(eisr0);
irq_idx = ctzl(eisr0);
} else if (eisr1) {
irq_idx = __builtin_ctz(eisr1) + 32;
irq_idx = ctzl(eisr1) + 32;
} else {
irq_idx = -1;
}

2
src/kernel/boot.c
View file

@ -507,7 +507,7 @@ provide_untyped_cap(
/** DONT_TRANSLATE */
BOOT_CODE static word_t boot_ctzl (word_t x)
{
return CTZL (x);
return ctzl(x);
}
BOOT_CODE bool_t