2009年12月3日 星期四

sparse type checking

因為 compiler 只能檢查 syntax.
Linus 為了檢查程式的 semantics ,創造出 sparse. 在 [ Linux Journal "Linus & Lunatics" ] 這篇文章提到了他當初的想法:

相關的 code 在 compiler.h 可以看得到 (kernel source 2.6.28 )

#ifdef __CHECKER__
# define __user        __attribute__((noderef, address_space(1)))
# define __kernel    /* default address space */
# define __safe        __attribute__((safe))
# define __force    __attribute__((force))
# define __nocast    __attribute__((nocast))
# define __iomem    __attribute__((noderef, address_space(2)))
# define __acquires(x)    __attribute__((context(x,0,1)))
# define __releases(x)    __attribute__((context(x,1,0)))
# define __acquire(x)    __context__(x,1)
# define __release(x)    __context__(x,-1)
# define __cond_lock(x,c)    ((c) ? ({ __acquire(x); 1; }) : 0)
extern void __chk_user_ptr(const volatile void __user *);
extern void __chk_io_ptr(const volatile void __iomem *);
#else
# define __user
# define __kernel
# define __safe
# define __force
# define __nocast
# define __iomem
# define __chk_user_ptr(x) (void)0
# define __chk_io_ptr(x) (void)0
# define __builtin_warning(x, y...) (1)
# define __acquires(x)
# define __releases(x)
# define __acquire(x) (void)0
# define __release(x) (void)0
# define __cond_lock(x,c) (c)
#endif

平常 gcc compile 時,不定義 __CHECKER__,所以這裡的許多 macros 就得到空定義 (程式碼 #else 部份)
那麼使用 sparse 時,就定義 __CHECKER__ ,(程式碼 #ifdef 部份) 舉例來說 第一行:

# define __user        __attribute__((noderef, address_space(1)))

使得 sparse 檢查 __user 定義的變數,是否落在 user space,例如用在 copy_to_user() :

unsigned long
copy_to_user(void __user *to, const void *from, unsigned long n)
{...}

compiler 是不會知道 "to" 的變數是不是正確!但是 sparse 檢查時,若發現 to 所指的不是在 user space 裡,就會發出 warning
因此這些 attributes 是給 sparse 用的,在 gcc 文件裡面查不到這些 attributes (是的,不要怪 gcc 文件寫不好...)

另外這篇 [ linux 內核中 compiler.h 文件的分析 ] 還解釋了 __acquire / __release 必須成對使用,否則 sparse 會發出 warning.

Linus 真神人也,可以讓 kernel source 藉由 sparse 工具來檢查 program semantic !!Technorati 標籤: ,

沒有留言:

張貼留言