Tài liệu Using SMT solver and symbolic execution to generate test inputs for C programs

U s in g E x e c u tio n S M T to S o lv e r G e n e r a te a n d S y m b o lic T e s t I n p u ts fo r C P r o g r a m s NÜ* j TRU N G T Â M J H Ô N G TIN î h u V i£ n , /A - lo / 6 6 ________________ DO Q U O C H U Y F a c u lty U n iv e rsity V ie tn a m of in fo rm a tio n of E n g in e e rin g T e c h n o lo g y an d T e c h n o lo g y N a tio n a l U n iv e rsity , H a n o i S u p e rv ise d by A thesis s u b m itte d in fulfillment of the requirem ents for the degree of M aster of Com puter Science June, 2010 T a b le 1 2 C o n t e n t s In tro d u c tio n 1 1.1 M o t i v a t i o n a n d c o n t r i b u t i o n ............................................................................................... 1 1.2 B a c k g r o u n d ...................................................................................................................................... 3 1.2.1 S M T s o l v e r ...................................................................................................................... 3 1 .2 .2 S y m b o l i c e x e c u t i o n ..................................................................................................... 5 1 . 2 .3 U sin g S M T so lv e rs a n d S y m b o lic E x e c u tio n to G e n e r a te T est I n p u t s .................................................................................................................................. 8 1.3 T e x t o v e r v i e w ................................................................................................................................. 8 1.1 R e l a t e d w o r k .................................................................................................................................. 9 CR EST 12 2.1 A r c h i t e c t u r e o f C R E S T ............................................................................................................ 12 2 .1 .1 I n s t r u m e n t a t i o n t o o l ................................................................................................ 13 2 .1 .2 C i I l i b r a r y f o r p e r f o r m i n g c o n c o l i c e x e c u t i o n ................................... 17 2 .1 .3 S e a r c h s t r a t e g i e s m o d u l e ....................................................................................... 19 2 .2 3 o f L i m i t a t i o n s o f C R E S T ............................................................................................................2 0 re a lC R E S T : A n ew te s t g e n e ra tio n to o l b a s e d o n C R E S T 3.1 M a i n i m p r o v e m e n t s c o m p a r e d t o C R E S T .................................................................2 3 3 .1 .1 H a n d lin g flo atin g -p o in t v ariab les 3 .1 .2 P r o c e s s i n g d i v i s i o n o p e r a t o r .............................................................................. 2 1 3 .1 .3 C o m b in in g m u ltip le S M T so lv e rs to e n h a n c e te st i n p u tg e n e r ­ a tio n 's a b i l i t y 3.2 23 r e a lC R E S T s arc h itec tu re ..................................................................2 3 25 ......................................................................... ......................... 2 7 4 E x p e rim e n t a n d d isc u ssio n 29 5 C o n c lu sio n a n d F u tu re W o rk 32 IV TABLE OF C O N T E N T S A S o m e im p o rta n t m e th o d s of ro a lC R E S T 33 A .l S o l v e m e t h o d o f C V C 3 S o l v c r c l a s s ................................................................................ 3 3 A .2 S o l v e m e t h o d o f Y i c e s S o l v e r c l a s s ................................................................................ 3 5 A .3 S o lv e A tB ra n c h m e th o d o f S earch class ................................................................... 3 8 L is t 1.1 o f F i g u r e s P r o g r a m ' s s e g m e n t u s e d t o e x c h a n g e t w o v a r i a b l e ’s v a l u e s a n d c o r r e l a ­ t i v e s y m b o l i c e x e c u t i o n t r e e . E a c h s t a t e ' s t r a n s f o r m a t i o n is n u m b e r e d b y t h e n u m b e r o f s t a t e m e n t in p r o g r a m s ................................................................. 6 1.2 S y m b o l i c t e s t i n g t e c h n i q u e .................................................................................................... 8 1 .3 T e s t g e n e r a t i o n life c y c l e ......................................................................................................... 9 2.1 C o - o p e r a t i o n o f t h r e e m a i n p a r t s in C R E S T ......................................................... 13 2.2 “c r e s t c ” s c r i p t file t o i n s t r u m e n t s o u r c e c o d e .......................................................... 14 2.3 A c t i v i t y o f i n s t r u m e n t a t i o n t o o l ....................................................................................... 15 2.4 O v e r v i e w o f C + 4 - l i b r a r y f o r p e r f o r m i n g s y m b o l i c e x e c u t i o n .................. 17 2.5 P r o t o t y p e o f c l a s s S y m b o l i c E x p r ....................................................................................... 18 2.6 P r o t o t y p e o f c l a s s S y m b o l i c P r c d ....................................................................................... 19 2.7 P r o t o t y p e o f c l a s s S v m b o l i c P a t h ....................................................................................... 20 2.8 P r o t o t y p e o f c l a s s S y m b o l i c E x e c u t i o n .......................................................................... 21 2.9 P r o t o t y p e o f c l a s s S y m b o l i c l n t e r p r e t e r ...................................................................... 21 2 . 1 0 P r o t o t y p e o f c l a s s Y i c e s S o l v e r ........................................................................................... 22 2.11 O v e r v i e w o f s e a r c h s t r a t e g i e s m o d u l e .......................................................................... 22 3.1 C o m b in in g m u lti so lv ers a lg o r ith m 3 .2 O v e r v i e w o f r e a l C R E S T ........................................................................................................ 2 8 1.1 T i m e c o s t s .......................................................................................................................................... 31 vi .............................................................................. 2 6 L is t 4 .1 o f T a b le s B ranches coverage C h a p t e r 1 I n t r o d u c t i o n 1 .1 M o t i v a t i o n a n d c o n t r i b u t i o n N o w a d a y s , t e s t i n g is t h e p r i m a r y w a y t o v a l i d a t e t h e c o r r e c t n e s s o f s o f tw a r e . T e s t in g w i t h m a n u a l l y g e n e r a t e d i n p u t s is t h e p r e d o m i n a n t t e c h n i q u e in p r a c t i c e t o e n s u r e so ftw a re q u ality . It a c c o u n t s fo r 5 0 -8 0 % s o f tw a r e d e v e lo p m e n t co st. i n p u t s g e n e r a t i o n is e x p e n s i v e , e r r o r - p r o n e , a n d r a r e l y e x h a u s t i v e . M a n u al te st T h u s , s e v c —1 te c h n iq u e s h a v e b e e n p r o p o s e d t o a u t o m a t e th is ta s k . T h e y c a n b e d iv id e d in to tw o m a in te c h n iq u e s: r a n d o m te s tin g a n d s y m b o lic ex e cu tio n . R a n d o m te s tin g (B ird &. S m a ra g d a k is, 2004) (P a ch e co M u n o z , 1983) (F o rre ste r Sz L M i l l e r . 2 0 0 0 ) ( C s a l l n e r &; E r n s t , 2 0 0 5 ) is s i m p l e t e c h n i q u e f o r a u t o m a t i n g t e s t g e n e r a tio n . In r a n d o m te s tin g , te s t in p u ts a re g e n e r a te d ra n d o m ly . A fte r t h a t th e y a r e u s e d t o e x e c u t e t h e p r o g r a m . A k e y a d v a n t a g e o f r a n d o m t e s t i n g is t h a t i t s c a l e s w e l l in t h e s e n s e t h a t r a n d o m t e s t i n p u t g e n e r a t i o n t a k e s n e g l i g i b l e t i m e . H o w e v e r , r a n d o m t e s t i n g is e x t r e m e l y u n l i k e l y t o t e s t a l l p o s s i b l e b e h a v i o r s o f a p r o g r a m . T o g e n e r a te t e s t in p u ts t h a t c a n e x p lo re a s m a n y b ra n c h e s o f a p r o g ra m a s p o ssi­ b le . s o m e t e c h n i q u e s b a s e d o n s y m b o l i c e x e c u t i o n ( K in g . 197 6 ) h a v e b e e n p r o p o s e d . S u ch te c h n iq u e s a t t e m p t to sy m b o lic a lly e x e c u te a p ro g ra m u n d e r te s t alo n g w ith all p o s s ib le e x e c u t i o n p a t h s o f t h e p r o g r a m , g e n e r a t i n g a n d s o lv in g c o n s t r a i n t s o f p r o g r a m v a r i a b l e s t o follo w t h e s e p a t h s t o p r o d u c e c o n c r e t e i n p u t s t h a t te s t e a c h p ath . U su a lly a n e x te r n a l S M T so lv e r ( M a u r a R u b io , 2008) (R o b e rto B ru tto m c sso B j o r n . 2 0 0 8 ) ( M i q u c l B o f i l l ÍC S c b a s t i a n i . 2 0 0 8 ) is u s e d t o s o l v i n g t h e p a t h c o n s tr a in ts to p r o d u c e a m o d e l th a t b e c o m e s te st in p u ts d ire c tin g th e p r o g ra m 's e x e cu tio n to th a t p a th . 1 2 1.1. M o t i v a t i o n a n d c o n t r i b u t i o n T h e r e a re m a n y s ta te -o f -th e - a r t so lv ers su c h a s Z 3 ( M a u r a & B jo rn . 2008). C Y C 3 ( B a r r e t t ic T i n e l l i . 2 0 0 7 ) . V i c e s ( S R I , 2 0 0 8 ) , B a r c e l o g i c ( M i q u e l B o f ill k R u b io . 2 0 0 8 ) . T h e r e a r e m a n y d i f f e r e n c e s b e t w e e n t h o s e S M T s o l v e r s in t h e i r s p e e d , m e m ­ o r y u s e . a n d a l g o r i t h m s a s w e ll a s u n d e r l y i n g t h e o r i e s t h e y s u p p o r t . w o rk o n ly o n s o m e sp ecific p la tf o r m . S o m e so lv e rs S o lv er X c a n b e b e t t e r t h a n so lv e r Y in lin ­ e a r in te g e r a r i t h m e t i c b u t w o rs e t h a n in n o n - l i n e a r re a l a r i t h m e t i c . A ll te s t i n p u t s g e n e r a tio n s to o l n o w u s e o n ly o n e S M T so lv e r t o so lv e t h e c o n s tr a in ts , th e r e f o r e t h e i r a b i l i t i e s i n t e s t i n p u t s g e n e r a t i o n a r e l i m i t e d , d e p e n d i n g o n t h e s o l v e r t h a t is used. C o m b in in g t h e p o w e r of th e s e so lv e rs m a y allo w u s to m a k e te s t g e n e r a tio n to o l m u c h m o re p ow erful. C R E S T ( J a c o b B u r n i m . 2 0 0 8 ) is a t o o l u s e d t o g e n e r a t e t e s t a u t o m a t i c a l l y f o r C program s. U s i n g C I L ( G . N e c u l a 2|ol V 0 2 | - » ( ^ l | 3 x : ¿>l|V.r : 0 1 . F r e e ( o c c u r r e n c e s ) o f v a r i a b l e s in a f o r m u l a a r e t h o s e n o t b o u n d b y a q u a n t i f i e r ( 3 , V). A s e n t e n c e is a f i r s t - o r d e r f o r m u l a w i t h n o f r e e v a r i a b l e s . A (first-o rd er) th e o ry T s e n te n c e s (over Y (over a s ig n a tu r e Yl) is a s e t o f ( d e d u c t i v e l y c l o s e d ) a n d V ). L e t D C ( [ ) b e t h e d e d u c t i v e c l o s u r e o f a s e t o f s e n t e n c e s f\ A t h e o r y T is c o n s i s t e n t if f a l s e ^ T . W e c a n v i e w a ( f i r s t - o r d e r ) t h e o r y T a s t h e c l a s s o f a ll m o d e l s o f T (d u e to c o m p l e t e n e s s o f f i r s t - o r d e r lo g ic ) . A m o d e l M is d e f i n e d ¿is fo llo w s : D o m a i n S is s e t o f e l e m e n t s : - I n t e r p r e t a t i o n a r it y (f ) —> S for e a c h / G — n. Yf = r>. - I n t e r p r e t a t i o n p A/ G Sn - for ev e ry v a ria b le A f A1 : S n A ssig n m en t fo rm u la é xM G S for e a c h p G Yip x w i t li G arity(p) V. is t r u e in a m o d e l M if i t e v a l u a t e s t o t r u e u n d e r t h e g i v e n i n t e r ­ p r e t a t i o n s o v e r t h e d o m a i n S. M is a m o d e l f o r t h e t h e o n ' T if all s e n t e n c e s o f T a r e t r u e in M . A fo rm u la That M (p(!*) is. t h e r e is a m o d e l M f o r T Tô(x). ( A is s a t i s f i a b l e in a t h e o r y T if t h e r e is a m o d e l o f fo rm u la o(~Ÿ) in w h i c h cfi(x) DC(Tu3x. ev a lu a tes to tru e , d e n o te d by T h i s is a l s o c a l l e d T - s a t i s f i a b i l i t y . is v a l i d in a t h e o r y T if V .f.<■/>(;?) G T. T h a t is o(x) e v a l u a t e s to t r u e in e v e r y m o d e l M o f T . T - v a l i d i t y is d e n o t e d b y J= To(x). T h e q u a n t if ie r free T - s a tis f ia b ility p r o b le m r e s t r i c t s D ecid in g w h ere a fo rm u la cid in g w h e th e r a m o d e l of (x) 0 t o b e q u a n t i f i e r f re e . is s a t i s f i a b l e in a t h e o r y T is e q u i v a l e n t w i t h d e ­ D C ( T U 3x.d(x)) e x i s t s o r n o t . It is t h e e s s e n t i a l m i s s i o n 1.2. B a c k g r o u n d o f S M T s o l v e r . T h e r e ¿ire s e v e r a l k i n d s o f t h e o r y d e p e n d i n g o n t h e t y p e o f v a r i a b l e s , for e x a m p l e lin e a r in te g e r a r i t h m e t i c , lin e a r re a l a r i t h m e t i c , t h e o r y o f a rra y , t h e o r y o f b it v ec to r, th e o r y o f T u p le s k. R e c o rd s, a n d so t h e o r y is a l s o a n N P - c o m p l e t e p r o b l e m . use on e of tw o m a in ap p ro a ch es. 011. F i n d i n g a m o d e l in a s p e c i a l T o so lv e t h i s p r o b le m . S M T so lv e rs o fte n T h e f irs t is E a g e r a p p r o a c h w h i c h s o l v e s S M T in stan c es by tra n s la tin g th e m to B o o lean S A T in sta n c e s a n d p assin g th e se fo rm u las t o a B o o l e a n S A T s o l v e r . T h e a d v a n t a g e o f t h i s a p p r o a c h is: w e c a n u s e b e s t a v a i l ­ a b le S A T so lv er. B u t th is a p p r o a c h h a s tw o d is a d v a n ta g e s : we need so p h istica te d e n c o d i n g s f o r e a c h t h e o r y a n d s o m e t i m e s t r a n s l a t i o n a n d / o r s o l v i n g a r e t o o s lo w . T h e s e c o n d is l a z y a p p r o a c h w h i c h t i g h t l y i n t e g r a t i n g t h e B o o l e a n r e a s o n i n g o f a D P L L - s ty le se a rc h w ith th e o ry -sp e c ific so lv e rs (T -so lv e rs) t h a t h a n d le c o n ju n c tio n s (A N D s ) o f p r e d ic a te s fro m a g iv e n th e o ry . v elo p ed by several g ro u p s: T h is a p p ro a c h w as in d e p e n d e n tly d e­ G V C (S ta n fo rd ), IC S (S R I). M a th S A T (U n iv . T re n to , Ita ly ), a n d V erifu n (H P ) . 1 .2 .2 S y m b o lic e x e c u tio n S y m b o lic E x e c u tio n (K in g . 1976): v erify p r o g r a m s re c e n tly . T h e m a i n i d e a o f t h i s t e c h n i q u e is u s i n g s y m b o l s a l t e r c o n c re te v alues as te s t in p u ts . by sy m b o lic fo rm u las. is a t e c h n i q u e ' h a t is u s e d p o p u l a r l y f o r t e s t , T h e v alues of p r o g ra m 's v a ria b le s are re p re s e n te d T h e e x e c u t i o n ’s r e s u l t is r e p r e s e n t e d a s a f u n c t i o n o f i n p u t s y m b o l ’s v a l u e s . T h e s t a t e o f p r o g r a m w h e n s y m b o l i c e x e c u t i o n is p e r f o r m e d i n c l u d e s : • T h e sy m b o lic v a lu e s o f v a ria b les. • P a t h c o n d i t i o n ( P C ) : Is a l o g i c a l f o r m u l a o f i n p u t s y m b o l i c v a r i a b l e s , w h i c h n o t c o n ta in tw o o p e ra to rs : 3 a n d V. It is a c o l l e c t i o n o f c o n s t r a i n t s in w h i c h t h e i n p u t v a r ia b le s m u s t b e s a tis f y so t h a t t h e p r o g r a m 's e x e c u t io n follow s t h e co rrela tiv e p a th . E ach sy m b o lic e x e c u tio n tree d escrib es th e ex e cu tio n p a th s g a in e d w h en p erfo rm sy m b o lic e x e c u tio n . E a c h n o d e re p re s e n ts a p r o g ra m 's s ta te a n d each arc d e s c rib e s a tr a n s f o r m from o n e s ta te to th e n e x t sta te . I n f i g u r e 1.1. i n i t i a l l y , P C e q u a l s t r u e . A t e a c h b r a n c h i n g n o d e . P C is u p d a t e d b y c o n s t r a i n t c o n d i t i o n s o f i n p u t v a r i a b l e s w i t h c o r r e l a t i v e b r a n c h e s . If a t a b r a n c h . 1.2. B a c k g r o u n d 6 x X. y. Y PC true XX. y V PC X< Y int x, y 1 if (x < y) { 2: x = x +y; 3: y = x - y; 4: x —x —y. 5 if (x - y < 0) 6: X X. y Y PC X> Y I2 x X♦ Y, y Y PC X< Y I.3. X. X♦ Y, y X PC X< Y assert (false); I4 7: XY y X PC X< Y 5 5 .... x. Y.'y X PC X 0 F i g u r e 1.1: P r o g r a m ' s s e g m e n t u s e d t o e x c h a n g e t w o v a r i a b l e ’s v a l u e s a n d c o r r e l a t i v e s y m b o l i c e x e c u t i o n t r e e . E a c h s t a t e ’s t r a n s f o r m a t i o n is n u m b e r e d b y t h e n u m b e r o f s t a t e m e n t in p r o g r a m s PC has tru e v alu e th e n it is t r u e t h a t t h e r e is n o i n p u t s e t s o t h a t c o r r e l a t i v e s t a t e m e n t s o f t h a t b r a n c h a r e c a r r i e d o u t , a n d t h a t b r a n c h is u n r e a c h a b l e . S o l v i n g th e p ro b lem " P C e q u a l s t r u e ” a t e a c h b r a n c h w ill r e t u r n s s u i t a b l e i n p u t s e t t h a t g u id e th e p r o g ra m 's e x e c u tio n to th a t b ra n c h . It is a N P - h a r d p r o b l e m a n d it is so lv e d bv u sin g S M T -S o lv e rs . In r e c e n t v e a r s , t h e r e h a v e b e e n m a n y r e s e a r c h e s in u s i n g s y m b o l i c e x e c u t i o n c o m b i n i n g w i t h S M T s o lv e r for t e s t g e n e r a tio n . S M T s o lv e rs a r e im p r o v e d s t r o n g e r a n d stro n g er. S o m e re se a rc h e s of im p ro v in g sy m b o lic ex e c u tio n te c h n iq u e h av e b een p r o p o s e d in s o m e r e c e n t p a p e r s . W e c a n d i v i d e it i n t o s o m e k i n d s a s b e l o w : D y n a m ic S y m b o lic E x e c u tio n (C . C s a lln e r k S m a r a g d a k is , 2 0 0 7 ) ( T a o X ie S c h u lte .. L isb o n P o rtu g a l J u n e J u ly 2009) (A n d r e a s G rie s m a y e r (D rie s V a n o v c rb e rg h c . 2008): k k S ch la tte , 2009) is t e c h n i q u e t h a t p r o g r a m is e x e c u t e d c o n c u r r e n t l y by b o th sym bol in p u ts a n d co n c re te in p u ts In t h e e x e c u t i o n p r o c e s s , e v e r y i n p u t c o n s t r a i n t t h a t d r i v e e x e c u t i o n f o llo w a n u n r e a c h e d b r a n c h a r e g a t h e r e d . T h i s c o n ­ s t r a i n t is s o l v e d t o c r e a t e n e w i n p u t . D y n a m i c S y m b o l i c E x e c u t i o n is u s e d in P e x ( N i k o l a i T i l l m a n n , 2 0 0 8 ) . a u n i t t e s t t o o l in N E T fra m e w o rk , t h a t u sin g S M T so lv er L o o p - E x t e n d e d S v m b o l i c E x e c u t i o n ( L E S E ) ( P r a t e c k S a x c n a , 2 0 0 9 ) : I t is a n i m ­ 7 1.2. B a c k g r o u n d p r o v e d m e t h o d o f S y m b o l i c e x e c u t i o n t h a t is u s e d f o r e n h a n c i n g a b i l i t y f o r p r o g r a m s t h a t h a v e a lo t o f lo o p s t r u c t u r e s . W ith S y m b o lic E x e c u tio n , e x e c u tio n p a t h s are g e n e ra lly g r o u p e d by se le c tio n s ta te m e n ts . T h e lo o p s t r u c t u r e s a re n o t ta k e n n o tic e v e r y m u c h : t h e r e f o r e t h e c h a n c e o f d e t e c t i n g e r r o r s t h a t c o n c e r n e d l o o p s t r u c t u r e s is lim ite d . In o r d e r to so lv e th is p r o b le m a n d g e t c o n s t r a i n t s o f lo o p s, t h e a p p r o a c h of L E S E is c r e a t i n g n e w s y m b o l i c v a r i a b l e s t h a t r e p r e s e n t i t e r a t i v e n u m b e r s o f l o o p s in t h e p r o g r a m . It a n a ly s e s S y m b o lic E x e c u t i o n m o r e d e e p l y t o d e t e r m i n e lo o p - d e p e n d e n t v a r i a b l e s , s u c h a s v a r i a b l e t h a t i t s v a l u e is a l i n e a r f u n c t i o n o f o n e o r m a n y lo o p - c o u n te r v a ria b les. I n a d d i t i o n , in o r d e r t o m a i n t a i n d a t a - d c p c n d c n c e o f s t a t e v a r i a b l e s o f S y m b o l i c E x e c u t i o n ' s i n p u t s , l o o p - d e p e n d e n t v a r i a b l e s is a l s o used as a n i n p u t o f p r o g r a m , a u x i l i a r y v a r i a b l e s is a d d e d t o c a t c h t h e l e n g t h a n d t h e n u m b e r o f i t e r a t i o n o f f i e l d s in a n p r e d e f i n e d i n p u t c o n t e x t . T hese co n stra in ts a l s o s h o w h o w l o o p - d e p e n d e n t v a r i a b l e s r e l a t e w i t h p r o g r a m ’s i n p u t . S e l e c t i v e S y m b o l i c E x e c u t i o n ( C h i p o u n o v , J u n e 2 0 0 9 ) is a n i m p r o v e m e n t o f S y m ­ b o l i c E x e c u t i o n , w h i c h is u s e d e f f e c t i v e l y f o r l a g e r p r o g r a m s , e s p e c i a l l y f o r p r o g r a m s t h a t in c lu d e m a n y in te ra c tio n w ith e n v iro n m e n t ( o p e ra tin g sy ste m , p ro g ra m m in g lib r a ry , f i r m w a r e o f d e v ic e , d a t a b a s e e t c ) . P e r f o r m i n g S y m b o l i c E x e c u t i o n for t h e s e p r o g r a m s w ill l e a d t o t h e e x p l o s i o n o f e x e c u t i o n p a t h s , s o t h a t t h e p e r f o r m i n g p r o ­ c e s s w ill b e m u c h s l o w e r . S e le c tiv e S y m b o lic E x e c u tio n (S S E ) so lv es t h i s p r o b le m b y c r e a tin g a v ir tu a l e n v i r o n m e n t t o r u n S y m b o lic E x e c u t i o n for e n t ir e s y s te m . W i t h th is v ir tu a l e n v iro n m e n t, u s e rs a rc a b le to sp e cify t h e b o u n d to r u n S y m b o lic E x e c u tio n inside, a n d ru n w ith c o n c re te v alu es o u tsid e . M e ch a n ism s of tra n sitio n a r e c o n s t r u c t e d t o e n s u r e t h a t p r o g r a m ’s s t r e a m is e x e c u t e d e x a c t l y w h e n t r a n s f e r b etw een tw o p a rts. C o n c o lic S y m b o lic E x e c u tio n 2005): (P. G o d e f r o i d Sz Sen. 2005) (K . S en k: A g h a ., It is c o n s t r u c t e d s i m i l a r l y t o D y n a m i c S y m b o l i c E x e c u t i o n w h i c h is b a s e d o n c o m b i n i n g S y m b o l i c E x e c u t i o n a n d c o n c r e t e e x e c u t i o n . H o w e v e r , it d i f f e r s f r o m D y n a m i c S y m b o l i c E x e c u t i o n , b e c a u s e it u s e s S y m b o l i c E x e c u t i o n t o c r e a t e i n p u t th a t d irec t p ro g ra m to u n re a c h e d b ra n c h e s a n d uses c o n c re te e x e c u tio n to m a k e S y m b o l i c E x e c u t i o n f o llo w c o n c r e t e p a t h . S y m b o l i c v a l u e s o f v a r i a b l e s w ill b e r e ­ p l a c e d b y c o n c r e t e v a l u e s if p r o g r a m ' s s t a t e is s o d i f f i c u l t t h a t it c a n n o t b e s o l v e d b y S M T s o l v e r . C o n c o l i c E x e c u t i o n is a p p l i e d in s o m e t o o l s lik e C U T E ( K . S e n & A g h a .. 2 0 0 5 ), C R E S T ( J a c o b B u rn im , 2008) etc. U n i v e r s a l S y m b o l i c E x e c u t i o n ( Y a m i n i K a n n a n . J u l y 2 0 2 4 2 0 0 8 ) is a k i n d o f S y m b o lic E x e c u t i o n t h a t a llo w s d a t a s t r e a m c a n b e c h e c k e d a t e v e r y m e m o r y lo c a - 8 1.3. T e x t ove rvi ew Create initial test values, Repeat Perform symbolic execution along with concrete execution, If unreached branch exists then Build a constraint system to reach that branch Solve the constraint by SMT Solver: If solving is successful then Generate test values from concrete model. End if End if Until (all branches are reached) or (solving is not successful); F i g u r e 1.2: S y m b o l i c t e s t i n g t e c h n i q u e t i o n s a l o n g w i t h a n e x e c u t i o n e v e n if i n p u t v a l u e s d o n o t l e a d p r o g r a m ' s H ow t o t h e s e l o c a t i o n s . It is p e r f o r m e d b y c r e a t i n g “ f r e s h ” s y m b o l i c v a r i a b l e s f o r e a c h s t a t e m e n t r e a d i n g a n 1 - v a lu e w h i c h is n o t in s y m b o l i c s t a t e , b e s i d e s c r e a t i n g s y m b o l i c v a r i a b l e s for in p u t. It a llo w s U n iv e r s a l S y m b o lic E x e c u t i o n t o d e a l w i t h i m m u t a b l e s t r u c t u r e d a t a t y p e in p r o g r a m , s u c h a s o r d e r l i n k l i s t , b i n a r y - s e a r c h t r e e e t c . 1 .2 .3 U s in g S M T so lv e rs a n d S y m b o lic E x e c u tio n to G e n ­ e ra te T est In p u ts W h e n w e p e r f o r m s y m b o lic e x e c u t io n for a p r o g r a m , w e c a n g e t e x e c u t io n p a t h . T h is e x e c u tio n p a th c a n b e u se d to c r e a te n e w te st in p u t s b v u sin g S M T so lv e r to so lv e t h e p a t h c o n s tr a in ts . T h e g e n e ra l te c h n iq u e o f u s in g s y m b o lic e x e c u tio n a n d S M T s o l v e r t o g e n e r a t e t e s t i n p u t a r e o u t l i n e d in f i g u r e 1.2. T h e life c y c l e o f t e s t g e n e r a t i o n is s h o w e d in f i g u r e 1.3. 1 .3 The T e x t o v e r v ie w f o l l o w i n g c h a p t e r w ill i n t r o d u c e C R E S T ' s a r c h i t e c t u r e w i t h a n d d isa d v a n ta g e s . its a d v a n ta g e s T h e n ex t c h a p te r in tro d u c es re a lG R E S T , a new to o l b a s e d o n ( ’R E S T , w h i c h h a s s o m e i m p o r t a n t e x t e n s i o n s : U s i n g d u a l - S M T s o l v e r t o s o l v e a c o n s t r a i n t , e x t e n d i n g for flo a tin g p o in t n u m b e r a n d d iv is io n o p e r a to r . A f te r t h a t , o n e c h a p t e r is d e d i c a t e d t o e x p e r i m e n t s . T h e r e s u l t s w ill b e a n a l y z e d t o s h o w t h e s t r o n g p o i n t s a n d w e a k p o in ts o f p r e s e n te d to o l. 9 1.4. H e l a t e d work Create Initial test input R u n test S o lv e using S M T S o lv e r and Monitor T e st inputs r C o nstrain t sy ste m R e p re se n t a path Execu tio n path Know n path not s e e n before Path condition F i g u r e 1.3: T e s t g e n e r a t i o n life c y c l e 1 .4 R e l a t e d w o r k T h e r e a r e s o m e t o o l s t o g e n e r a t e t e s t i n p u t for C p r o g r a m s : D ire c te d A u t o m a te d R a n d o m T e s tin g (D A R T ) (P. G o d e fro id k S e n . 2 0 0 5 ) , is a n a u t o m a t e d te s tin g to o l t h a t c o m b in in g th r e e te c h n iq u e s to ac h ie v e h ig h p a th c o v e r a g e . F i r s t , it d e t e r m i n e s a n d s i m u l a t e s t h e “m o s t g e n e r a l e n v i r o n m e n t ' w h i c h a p r o g r a m c a n r u n in b v e x t r a c t i n g t h e e x t e r n a l i n t e r f a c e o f t h e p r o g r a m . S e c o n d , it c r e a te s a te s t d riv e r w h ich en fo rces a g a in a n d a g a in th e p ro g ra m w ith irre g u la r in p u t, a lso th e e x e c u tio n o f th is in p u t allo w s th e to o l to c o m p le te d y n a m ic a l a n a ly s is to b e o n t h e t r a c k o f t h e e x e c u t io n tr e e for t h e p r o g r a m , b y t h e w a v o f a g g r e g a tin g b a s e o n ea ch e n c o u n te re d b ra n c h s tr u c tu re . E v en tu ally , D A R T ca n en fo rce th e ex e cu tio n to g e th e r w ith a n a lte rn a tiv e p a th by w o rk in g o u t a rele v an t set of c o n s tra in ts a n d ru n c o n c r e t e e x e c u t io n w ith t h e s o lu t io n . It a p p lie s a s o lv e r for lin e a r in te g e r a r i t h m e t i c . W h e n t h e c o n s t r a i n t s a r e b e y o n d t h i s t h e o r y , t h e s y s t e m s w ill b e b a c k t o t h e c o n c r e t e v alu es o f v aria b les to go on w ith th e ex e cu tio n . B y g e t t i n g in g r o u p c o n c r e t e e x e c u t i o n w i t h s y m b o l i c a n a l y s i s , D A R T s u c c e e d s in s o l v i n g t h e i s s u e o f f a l s e a l e r t s s e q u e n c e s o f t h e i m p r e c i s i o n o f t h e l a t t e r . E v e r y i n ­ a c c u r a c y r e p o r t e d b y t h e t o o l is s o n o r o u s , b e c a u s e it d e p e n d s o n a n a c t u a l e x e c u t i o n o f t h e p r o g ra m . T h e m e t h o d p ro v es to b e useful a n d a d v a n ta g e o u s , es p ec ially w ith th e use o f lib ra rv fu n c tio n s w h o se so u rce co d e ca n n o t b e an a lv z cd . W h e re a s s ta tic 10 1.4. R e l a t e d work a n a ly s is c a n n o t g et a n y t h i n g a b o u t th e i r u se , D A R T c a n g a in a lot o f b e n e f its fro m in s p e c tin g th e real v alu e b ac k by su c h a fu n c tio n . M e an w h ile , th e to o l s u p p o s e s th a t th e s e ca lls h a v e 110 s i d e effect 011 t h e a n a ly z e d p r o g ra m , a n d th e p r o c e d u r e of so lv in g t h e s e issu e s b y in s e r t in g in te r fa c e c o d e c o n t r a s t s w ith t h e a u t o m a t e d a s p e c t o f th e a p p r o a c h , a n d c o u l d b e s i m p l i f i e d b y d i s s e c t i n g t h e s p e c i f i c a t i o n f o r t h e f u n c t i o n s in q u e s t i o n a n d a l s o b y t a k i n g t h e a p p l i c a b l e b e n c h m a r k in a le s s u s e r - d e p e n d e n t w a y . C U T E (K . S e n k A g h a .. 2 0 0 5 ). a n a c r o n y m for t h e C o n c o lic U n it T e s t in g E n ­ g i n e , is a t o o l b u i l t o n t h e s a m e w o r k . L i k e D A R T , it a l s o c o m b i n e s c o n c r e t e a n d s y m b o l i c e x e c u t i o n t o e x a m i n e a l t e r n a t i v e e x e c u t i o n p a t h s in o r d e r t o d i s c l o s e p o ­ te n tia l a s se rtio n v io la tio n s. U n l i k e D A R T , it d o e s n o t o n l y u s e l p j s o l v e f o r s o l v i n g l i n e a r c o n s t r a i n t s , b u t a l s o i n t r o d u c e s o p t i m i z a t i o n s . T o d o t h i s , it f i r s t s y n t a c t i c a l l y d e t e c t s a n e w s u b - c o n s t r a i n t w h i c h is t h e n e g a t i o n o f a n o t h e r , t h e n e l i m i n a t e s c o m ­ m o n su b -co n stra in ts. It s o l v e s t h e c o n s t r a i n t s in a n i n c r e m e n t a l w a y , o n l y t a k i n g in to a c c o u n t s u b - c o n s tr a in ts w h ic h d e p e n d o n t h e n e w lv in tr o d u c e d o n e. C U T E also d e a ls w ith p r e d ic a te s t h a t in v o lv e p o in te r v a ria b le s b y in v e s tig a tin g t h e e q u iv a le n c e c la sse s for th e m . A l t h o u g h t h e r e a r e t w o m e t h o d s in c o n s t r u c t i n g i n p u t d a t a s t r u c t u r e s , t h e f o r m e r o n ly uses f u n c ti o n ca lls, a n d t h u s , su ffe rs fro m t h e d i s a d v a n t a g e o f r e ly in g fu n ctio n s. 011 ¿hese S o lv in g t h e c l a s s i n v a r i a n t for d a t a s t r u c t u r e s s h o u l d b e t h e p r i m a r y c h o i c e for t h i s p r o c e s s . S in c e C U T E d o e s n o t m a k e u s e o f e x a c t p o i n t e r a n a l y s i s , its p r e c i s i o n is o n l y s u b j e c t t o t h e p r e d i c a t e s e n c o u n t e r e d s o f a r in t h e p r o g r a m . The trad e-o ffs b e tw e e n p e rfo rm a n c e - w ith in th e e x te n ts o f tr a c ta b ility - a n d h ig h e r p a th c o v e r a g e c o u l d b e d i s c u s s e d in t h e c o n t e x t o f t h i s a s p e c t o f t h e t o o l . KLEE ( C r i s t i a n C a d a r , 2 0 0 8 ) is a s y m b o l i c e x e c u t i o n t o o l w h i c h of a u to m a tic a lly g en e ratin g te sts th a t is c a p a b l e a c h ie v e h ig h c o v e r a g e o n a d iv e rs e set of c o m p lex a n d e n v iro n m e n ta lly -in te n siv e p ro g ra m s. o n b o th , th e p a t h ex p lo sio n p ro b le m a n d th e K L E E m a n a g e s to g et a h an d le 'e n v iro n m e n t p ro b le m " . K L E E is d i f f e r e n t t o o t h e r t o o l s in o p t i m i z i n g t h e c o n s t r a i n t s e t in o r d e r t o s p e e d u p c o n s t r a i n t s a t i s f i a b i l i t y t e s t s u p o n e a c h “u n s a f e a c c e s s (v iz.. p o i n t e r d e r e f e r e n c e s , a s s e r t s , e t c ) . K L E E is d e s i g n e d a s a n o p e r a t i n g s y s t e m f o r s y m b o l i c p r o c e s s e s . J u s t lik e a " r e a l " o p e r a t i n g s y s t e m p ic k s u p o n e a m o n g s e v e r a l c o m p e t i n g p r o c e s s e s for s c h e d u lin g , K L E E ’s s c h e d u l e r s e l e c t s a s y m b o l i c p r o c e s s a m o n g s t m a n y fo r s y m b o l i c e x e c u t i o n . K L E E ’s s c h e d u l e r ' s t a r g e t is t o r u n t h o s e s y m b o l i c p r o c e s s e s t h a t h a v e p o s s i b i l i t i e s t o o f f e r b i g g e s t i m p r o v e m e n t s in c o v e r a g e . E a c h s y m b o l i c - p r o c e s s h a s a c u r r e n t s e t o f c o n s t r a i n t s on t h e e n v i r o n m e n t , w h ic h m u s t b e m e t for t h e c u r r e n t p a t h t o b e 1.4. R e l a t e d w ork reach ed . If K L E E d e t e c t s a v i o l a t i o n in t h e c o n s t r a i n t s e t . it t r i g g e r s a n e r r o r a n d g e n e ra te s a te st case. K L E E ' s a p p r o a c h o f r e d u c i n g t i m e c o s t o f s o l v i n g p r o c e s s is to o p tim iz e a w a y th e larg e p a r ts of th e s ta te of each s y m b o lic -p ro c e s s b e fo re th e c o n s t r a i n t s a r e p a s s e d o n t o t h e so lv er. A lth o u g h ea ch of D A R T , C U T E and K L E E c o n c e n t r a t e s o n d iffe ren t t a r g e t s in s y m b o l i c t e s t i n g , a ll o f t h e m d o n o t c u r r e n t l y s u p p o r t s y m b o l i c f l o a t i n g p o i n t a r i t h m e t i c . It is t h e m a i n d i s a d v a n t a g e in a p p l y i n g t h e m f o r p r a c t i c a l p r o g r a m s . C h a p t e r 2 C R E S T 2 .1 A r c h i t e c t u r e o f C R E S T C R E S T ( J a c o b B u r n i m , 2 0 0 8 ) , h a s b e i n g d e v e l o p e d b y J a c o b B u r n i m . is a n o p e n s o u r c e s y m b o l i c t e s t g e n e r a t i o n t o o l f o r C . D e s p i t e h a s s e v e r a l e s s e n t i a l d r a w b a c k s , it i n t r o d u c e s a s i m p l e , w e l l - c o n s t r u c t e d a r c h i t e c t u r e , w h i c h is e a s y t o i m p r o v e . C R E S T i n c l u d e s t h r e e m a i n p a r t s : a n i n s t r u m e n t a t i o n t o o l s w r i t t e n in O C a m l l a n g u a g e , a C + -f l i b r a r y f o r p e r f o r m i n g c o n c o l i c e x e c u t i o n f o r C p r o g r a m s , a n d a C + + s e a r c h strateg ie s m o d u le . T h e i n s t r u m e n t a t i o n t o o l is b u i l d b a s e d o n C I L ( G . N e c u l a k W e irn er, 2 0 0 2 ), a n O C a m l a p p l i c a t i o n for p a r s in g , t r a n s f o r m i n g , a n d a n a ly z in g C c o d e . It is u s e d t o in s tr u m e n t t h e s o u rc e o f t h e p r o g r a m u n d e r te s t for c o n c o lic te s tin g a n d to e x t r a c t t h e c o n t r o l f lo w a n d s t a t i c c a l l g r a p h . T h e C + + lib ra ry p e rfo rm s sy m b o lic ex e c u tio n s im u lta n e o u s ly w ith th e c o n c re te ex e cu tio n of th e p ro g ra m . T h e s e a rc h s tr a t e g y f ra m e w o r k p ro v id e s p rim itiv e s for w r itin g a c o n c o lic s e a rc h s tr a te g y , su c h a s m e t h o d s for flip p in g a n d s o lv in g p a t h c o n s t r a i n t s u s in g t h e Y ice s (S R I. 2008) S M T so lv er. C R E S T d o es not cu rren tly p erfo rm a n y s ta tic re a s o n in g a b o u t calls th r o u g h fu n ctio n p o in te rs. T h u s , w e m a y e n c o u n te r e x e c u tio n p a t h s t h a t d o n o t c o r r e s p o n d t o a n y s t a t i c p a t h s in t h e c o n t r o l flo w a n d s t a t i c c a l l g r a p h , p o t e n t i a l l y l e a d i n g t o d y n a m i c d i s t a n c e s b e t w e e n b r a n c h e s t h a t a r c s m a l l e r t h a n t h e s t a t i c d i s t a n c e s in t h e c o n t r o l H ow a n d s t a t i c c a l l g r a p h ( C F C G ) . F i g u r e 2.1 s h o w s t h e c o - o p e r a t i o n o f t h r e e m a i n p a r t s in C R E S T . 12 13 2.1. A r c h i t e c t u r e of C R E S T C source codes Instrumentation tool v_____________________ J \ / Instrumented codes, path F i g u r e 2 .1 : C o - o p e r a t i o n 2 .1 .1 r.f t h r e e m a i n p a r t s in C R E S T I n s tr u m e n ta tio n to o l T h is m o d u le c re a te s c o rre s p o n d e n tly in s tru m e n te d c o d e s from C so u rc e code. In p u t v a r i a b l e s a r e i n d i c a t e d b v m a r k e d s t a t e m e n t s t h a t a r e m a n u a l l y i n s e r t e d in C s o u r c e code. In i n s t r u m e n t e d p h r a s e , a s c r i p t c a l l e d ‘c r e s t c is e x e c u t e d . T h e s c r i p t is s h o w e d in f i g u r e 2 .2 . A t f i r s t , t h i s s c r i p t i n v o k e s “c r e s t l n s t r u m c n t . m r . a n O c a m l m o d u l e c o n t a i n ­ in g a n a ly s i s a n d t r a n s f o r m a t i o n for in s t r u m e n t i n g C p ro g ram s. T h i s m o d u l e is l i n k e d i n t o a b o i l e r p l a t e d r i v e r a p p l i c a t i o n n a m e d “c i l l y ” w h i c h is a P e r l s c r i p t t h a t p ro cesses a n d m im ics G C C and M S V C c o m m a n d - l i n e a r g u m e n t s a n d t h e n calls c i l l v . b y t e . e x e o r c i l l y . a s m . e x e ( C I L ’s O c a m l e x e c u t a b l e ) . T h i s p r o c e s s c r e a t e s t h r e e files t h a t c o n t a i n i n f o r m a t i o n o f b r a n c h e s a n d C F G o f i n p u t p r o g r a m . T h e n , a n e x ­ e c u t a b l e file c a l l e d " p r o c e s s . c f g is e x e c u t e d . T h i s p r o c e s s p r e p a r e s t h e p a t h s p a c e s f o r s e a r c h p h r a s e b y r e a d i n g a n d a n a l y z i n g o u t p u t file o f p r e v i o u s p r o c e s s . F ig u re 2 .3 d e s c r i b e t h e a c t i v i t y o f i n s t r u m e n t a t i o n to o l. D u r i n g i n s t r u m e n t a t i o n , t h e f o l l o w i n g f u n c t i o n c a l l s a r e i n s e r t e d in t h e C c o d e u n d e r test: 2.1. A r c h i t e c t u r e of C R E S T ! bi ri / 1 h h \'t I H= : i r HrlT.ri $0 / . . C! !. I.Y=$ {H ; k } / c i 1 i■ak r= e x p r 51 ‘ i r; / c. : '\ \ ! 1 1y .* \ ) \ .c ’ i $ ( C! 1. 1»V} : i e O * S t ! n ri I r u'rien I f ¡jVi 00 u r11 o r 9 furic 'ririp o f g > x r-T, - r u ]■:0 t- ri L m t , CO Un!.. b r i f i c h e y C f 9 b r -i ri rVi-fS y 4 — ;-:.i v »--1 nrips \ " l i t r, i K) / i fscl n o r -1.5 ( i) k / * $ I n i k }, b ! n / p r o c e s s C f-j F igure 2.2: "crcstc" script file to in stru m e n t source code EXTERN EXTERN void _ _ C r e s t I n i t ( ) „ S K I P : void ..C r e s t Load ( ..C R EST.ID . _CREST_ADDR. _CREST_VALUE) ..S K IP EXTERN EXTERN EXTERN void . . C r e s t St ore ( ..CR EST _ID . _CREST_ADDR) „ S K I P : void ..C r e s t C l e a r S t ack ( „C R E S T .ID ) ..S K IP : void ..C r e s t A pply 1 ( ..CH EST.ID . ..CR EST.O P, _CREST_VALUE) „ S K IP EXTERN void ..C r e s t A p p ly 2 ( ..C R EST.ID . ..CREST.OP . _CREST_VALUE) „ S K IP EXTERN v o id . . C r e s t B r a n c h ( . . C R E S T . I D . .. C R E S T J 3 R A N C I L I D . . . C R E S T J 3 0 0 L ) ..S K IP : EXTERN v o id . . C r e s t C a l l ( . . C R E S T . I D . ._ C R E S T .F U N C T I O N .I D ) ..S K IP : EXTERN v o id ..C r c s t lle t u r n ( ..C R E S T .ID ) EX T E R N v o id . . C r e s t H a n d le R e t u r n ( . . C R E S T . I D , _ C R E S T _ V A L U E ) „ S K IP : „ S K IP : T h e se calls (loosely) c o rre sp o n d to an execution of th e p ro g ra m u n d e r test by a sta c k m achine. It is in te n d e d t h a t th ese calls be used to sym bolically ex ecu te th e p ro g ram u n d e r te s t, by m a in ta in in g a sym bolic sta c k (along w ith a sym bolic m em ory m ap ). Specifically: A C expression (w ith no side effects) g e n e ra te s a series of L oad a n d A pply calls c o rre sp o n d in g to th e “postfix"' e v a lu a tio n of th e expression, using a stack (i.e. a Load in d ic a te s th a t a value is p u shed o n to th e stack , a n d u n a ry a n d b in ary o p e ra tio n s are a p p lied to o n e /tw o values p o p p e d off th e stack ). For exam ple, th e expression: ”a* b > 3 + c " w ould g e n e ra te th e in stru m e n ta tio n : L oad(& a, a) 2.1. A r c h i t e c t u r e of C R E S T 15 C source code 1 Crestlnstrument ml j Instrumented code cfg branches cfg_func_map F i g u r e 2 .3 : A c t i v i t y o f i n s t r u m e n t a t i o n t o o l L o a d (& b , b) A p p ly B in O p (M U L T IP L Y , a*b) L o a d ( 0 , 3) L o ad (& :c . c) A p p lv B in O p (A D D , 3 + c) A p p 1y B i n 0 p ( G R E A T E R _ T H A N . a * b > 3 + c ) E a c h L o a d a n d A p p l y call in c lu d e s t h e c o n c r e t e v a lu e e i t h e r lo a d e d o r c o m p u t e d . C o n s t a n t s a r e t r e a t e d a s h a v i n g a d d r e s s “0". E n te r in g th e th e n - o r else-b lo c k of a n in d ic a tin g w h ich b r a n c h w as ta k e n . sta ck . For e x a m p le , if s t a t e m e n t g e n e r a t e s a B r a n c h call T h e b r a n c h is o n t h e v a l u e p o p p e d f r o m t h e i f ( a * b > 3 + c ) ..." g e n e r a t e s t h e s e r i e s o f L o a d a n d A p p l y c a l l s a b o v e , p l u s o n e of: B r a n c h ( t r u e i d , 1) B ran c h (fa lse_ id . 0) A n a s s i g n m e n t s t a t e m e n t g e n e r a t e s a s in g le S t o r e ca ll, i n d i c a t i n g t h a t a v a lu e is p o p p e d o f f t h e s t a c k a n d s t o r e d in t h e g i v e n a d d r e s s . F o r e x a m p l e . " a g en e rate s: L o a d (0 . 3) L oad (id ), b ) A p p 1v B i n O p ( A D D . 3 + b ) S to re (fc a) 3 + b