प्रतीकात्मक कोड निष्पादन के लिए KLEE वर्चुअल मशीन

इस पोस्ट में, हम एक साधारण ASCII भूलभुलैया को हल करने के लिए एक उदाहरण के रूप में KLEE प्रतीकात्मक वीएम का उपयोग करके प्रतीकात्मक निष्पादन तकनीक को लागू करने का प्रयास करेंगे। आपको लगता है कि हम कितने सही निर्णय ले सकते हैं?

भूलभुलैया

भूलभुलैया अपने आप में एक C प्रोग्राम है, जिसका कोड आप यहाँ ले जा सकते हैं । शुरू करने के बाद, खेल कदम (बाएं से दाएं, डी - दाईं ओर, डब्ल्यू - अप और एस - डाउन) के एक क्रम में प्रवेश करने की उम्मीद करता है। यह इस तरह दिखता है:

  प्लेयर पॉज़: 1x4
 Iteration सं।  2. कार्रवाई: एस।
 + - + --- + --- +
 | एक्स |  | # |
 | एक्स |  - + |  |
 | एक्स |  |  |  |
 | एक्स + - |  |  |
 |  |  |
 + ----- + --- + 

अपनी स्पष्ट सादगी के बावजूद, भूलभुलैया एक रहस्य को छिपाती है और इसलिए एक से अधिक समाधान हैं।

क्ली

KLEE LLVM बिटकोड का चरित्र दुभाषिया है, अर्थात यह किसी भी फ्रंट एंड द्वारा उत्पन्न कोड को निष्पादित कर सकता है। प्रतीकात्मक निष्पादन का सार इस तथ्य से नीचे आता है कि लॉन्च किए गए कार्यक्रम के सभी इनपुट मूल्यों में विशिष्ट मूल्य नहीं हैं, लेकिन संभव मूल्यों के लिए प्रतीकात्मक प्रतिबंध हैं। निष्पादन के दौरान, नए प्रतीकात्मक चर बनाए जा सकते हैं (उदाहरण के लिए, जब उनके मूल्य एक प्रतीकात्मक ऑपरेंड के साथ कुछ ऑपरेशन के परिणाम पर निर्भर करते हैं), साथ ही साथ मौजूदा (जब प्रोग्राम निष्पादन पथ पर शाखाएं)। दूसरे मामले में, केएलई एसएमटी सॉल्वर का उपयोग यह निर्धारित करने के लिए करता है कि, सिद्धांत रूप में, किसी दिए गए पथ के साथ एक कार्यक्रम को निष्पादित करना संभव है।
यदि आप इस विषय में रुचि रखते हैं, तो आप यहां देख सकते हैं और इसे पढ़ सकते हैं या यह भी पढ़ सकते हैं।

पोस्ट का विचार सरल है - एक चरित्र स्ट्रिंग को भूलभुलैया कार्यक्रम में खिलाएं और देखें कि केएलई कैसे समाधान पाता है।

कोड का विश्लेषण करते हैं

भूलभुलैया को वर्णों के द्वि-आयामी सरणी के रूप में परिभाषित किया गया है।

#define H 7 #define W 11 char maze[H][W] = { "+-+---+---+", "| | |#|", "| | --+ | |", "| | | | |", "| +-- | | |", "| | |", "+-----+---+" }; 

ड्रा () का कार्य स्क्रीन पर हमारे सरणी को आकर्षित करना है।

 void draw () { int i, j; for (i = 0; i < H; i++) { for (j = 0; j < W; j++) printf ("%c", maze[i][j]); printf ("\n"); } printf ("\n"); } 

मुख्य () फ़ंक्शन खिलाड़ी की स्थिति, पुनरावृत्तिकर्ता और क्रियाओं को संग्रहीत करने वाले 28-बाइट सरणी को संग्रहीत करने वाले चर घोषित करके शुरू होता है। फिर, खिलाड़ी की प्रारंभिक स्थिति (1,1) पर सेट होती है और इस बिंदु पर एक क्रॉस बनाया जाता है।

 int main (int argc, char *argv[]) { int x, y; //Player position int ox, oy; //Old player position int i = 0; //Iteration number #define ITERS 28 char program[ITERS]; x = 1; y = 1; maze[y][x]='X'; 

हम स्टड से पढ़ते हैं कि खिलाड़ी ने वहां क्या पेश किया।

  read(0,program,ITERS); 

इसके अलावा, चक्र के प्रत्येक पुनरावृत्ति पर, हम उपयोगकर्ता के पुराने निर्देशांक को सहेजते हैं और उसे एक नए स्थान पर ले जाते हैं।

  while(i < ITERS) { ox = x; //Save old player position oy = y; switch (program[i]) { case 'w': y--; break; case 's': y++; break; case 'a': x--; break; case 'd': x++; break; default: printf("Wrong command!(only w,s,a,d accepted!)\n"); printf("You loose!\n"); exit(-1); } 

यदि खिलाड़ी अंत तक पहुँच गया है - उसे बधाई।

  if (maze[y][x] == '#') { printf ("You win!\n"); printf ("Your solution \n",program); exit (1); } 

अगर कुछ गलत है - हम उस जगह पर लौटते हैं जहां हम खड़े थे।

  if (maze[y][x] != ' ' && !((y == 2 && maze[y][x] == '|' && x > 0 && x < W))) { x = ox; y = oy; } 

यदि वे दीवार से टकराते हैं, तो खिलाड़ी हार जाता है।

  if (ox==x && oy==y){ printf("You loose\n"); exit(-2); } 

खैर, अगर कुछ नहीं हुआ, तो हमने सिर्फ एक कदम उठाया। हम खिलाड़ी को स्थानांतरित करते हैं, एक तस्वीर खींचते हैं, पुनरावृत्ति बढ़ाते हैं और शुरुआत में लौटते हैं।

  maze[y][x]='X'; draw (); //draw it i++; sleep(1); //me wait to human } 

चलो मैन्युअल रूप से भूलभुलैया के माध्यम से चलते हैं

यदि आप अचानक खुद को गेम पूरा करना चाहते हैं, तो सबसे अधिक संभावना है कि आपको निम्नलिखित समाधान मिलेगा: ssssddddwwaawwddddssssddwwww

और अब KLEE के साथ

सबसे पहले, हमें LLVM, अनुवादक C -> LLVM IR (llvm-gcc या clang) और, वास्तव में, KLEE की आवश्यकता है। अधिकांश लिनक्स वितरण में पहले से ही रिपॉजिटरी में ये पैकेज हैं।
LLVM बिटकोड में mace.c का अनुवाद करने के लिए, आपको कमांड चलाने की आवश्यकता है

  $ llvm-gcc -c –emit-llvm maze.c -o maze.bc 

जैसा कि पहले उल्लेख किया गया है, आप llvm-gcc के बजाय क्लैंग का उपयोग कर सकते हैं।

इस कमांड के परिणामस्वरूप, हमें maze.bc फ़ाइल मिली, जो भूलभुलैया प्रोग्राम का बिटकोड है। इसे LLVM दुभाषिया पर भी चलाया जा सकता है:

  $ ल्ली भूलभुलैया। बीसी 

KLEE का उपयोग करके कोड का परीक्षण करने के लिए, हमें कुछ चर को प्रतीकात्मक के रूप में चिह्नित करना होगा। इस मामले में, यह मुख्य () की शुरुआत में घोषित कार्यों की सरणी होगी। तो, लाइन की जगह

  read(0,program,ITERS); 

पर

  klee_make_symbolic(program,ITERS,"program"); 

और KLEE हेडर फ़ाइल जोड़ना न भूलें

 #include <klee/klee.h> 

अब KLEE निष्पादन के किसी भी संभावित मार्ग (और भूलभुलैया के गलियारे) से गुजरने में सक्षम होगा। इसके अलावा, अगर ये रास्ते किसी तरह की त्रुटि का कारण बन सकते हैं (उदाहरण के लिए, बफर अतिप्रवाह के लिए), तो KLEE हमें इस बारे में संकेत देता है। हम बाहर ले जाते हैं

  $ klee maze.bc 

और निम्नलिखित चित्र देखें:

जैसा कि आप पिछले 3 पोस्ट से देख सकते हैं, KLEE ने 321 अलग-अलग रास्ते पाए। सच है, यह एक 321 सही निर्णय नहीं है।

  KLEE: किया गया: कुल निर्देश = 112773
 KLEE: किया: पूर्ण पथ = 321
 KLEE: किया: उत्पन्न परीक्षण = 318 

एक विस्तृत रिपोर्ट klee-last निर्देशिका में सहेजी जाती है

  $ ls klee-last /
 असेम्बली। सभी test000078.ktest test000158.ktest
 जानकारी test000079.ktest test000159.ktest
 messages.txt test000080.ktest test000160.ktest
 run.istats test000081.ktest test000161.ktest
 run.stats test000082.ktest test000162.ktest
 test000001.ktest test000083.ktest test000163.ktest
 test000075.ktest test000155.ktest चेतावनी 

प्रत्येक परीक्षण ktest- उपकरण उपयोगिता का उपयोग करके देखा जा सकता है।

  $ ktest-tool klee-last / test000222.ktest
 ktest फ़ाइल: 'klee-last / test000222.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'ssssddddwwawwdddssssddwwwd \ x00' 

इस स्थिति में, आप बस यहाँ से प्रोग्राम वेरिएबल का मान ले सकते हैं और उस मान को भूलभुलैया प्रोग्राम में पास करके टेस्ट खेल सकते हैं।

इसलिए, हमें कार्यक्रम में सभी संभावित रास्ते मिले। लेकिन सभी सही समाधान खोजने के लिए प्रत्येक परीक्षण को न देखें! हमें KLEE को उन परीक्षणों को उजागर करने की आवश्यकता है जो वास्तव में "आप जीतते हैं!"।
KLEE इंटरफ़ेस में klee_assert () फ़ंक्शन होता है, जो सी में समानार्थी मुखर () के समान होता है - एक बूलियन अभिव्यक्ति के मूल्य की गणना करता है और, यदि गलत है, तो प्रोग्राम निष्पादन को बाधित करता है। हमारे मामले के लिए, यह वही है जो डॉक्टर ने आदेश दिया था।
लाइन के बाद जोड़ें

 printf ("You win!\n"); 

बिना शर्त कॉल klee_assert ()

 printf ("You win!\n"); klee_assert(0); //Signal The solution!! 

अब KLEE सभी संभावित निष्पादन रास्तों के लिए परीक्षण करना बंद नहीं करेगा, हालाँकि, klee_assert (!) के लिए परीक्षण उनके नाम में .err होगा:

  $ ls -1 klee-last / | grep -A2 -B2 इरेट करें
 test000096.ktest
 test000097.ktest
 test000098.assert.err
 test000098.ktest
 test000098.pc 

आइए उनमें से एक को देखें।

  $ ktest-tool klee-last / test000098.ktest
 ktest फ़ाइल: 'klee-last / test000098.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'sddwddddssssddwwww \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00' 

तो, प्रस्तावित KLEE समाधान sddwddddssssddwwww है
अरे मुझे जाने दो यह छोटा लग रहा है! आइए इसे असली चक्रव्यूह पर आजमाते हैं:

मुझे पता था !!! भूलभुलैया में नकली दीवारें हैं! और KLEE सुरक्षित रूप से उनके पास से गुजरा! लेकिन हे, अगर केएलई को सभी समाधान खोजने थे, तो हमारा पहला स्थान कहां है? KLEE ने उसे क्यों नहीं खोजा?
ठीक है, आम तौर पर त्रुटि का एक तरीका हमारे लिए पर्याप्त है यदि हम स्वयं त्रुटि की तलाश कर रहे हैं, और हमें इसके लिए वैकल्पिक तरीकों की आवश्यकता नहीं है। इसलिए, इस मामले में, हम 10,000 कमांड लाइन विकल्पों में से एक का उपयोग करेंगे।

  $ klee -emit-all-त्रुटियाँ maze_klee.o 

हम परिणाम को देखते हैं:

अब हमें 4 परीक्षण मिले हैं, जो हमारे भूलभुलैया के 4 संभावित समाधान हैं:

  $ ktest-tool klee-last / test000097.ktest
 ktest फ़ाइल: 'klee-last / test000097.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'sddwddddsddw \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00'
 $ ktest-tool klee-last / test000136.ktest
 ktest फ़ाइल: 'klee-last / test000136.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'sddwddddssssddwwww \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00'
 $ ktest-tool klee-last / test000239.ktest
 ktest फ़ाइल: 'klee-last / test000239.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'ssssddddwwaawwddddsddw \ x00 \ x00 \ x00 \ x00 \ x00 \ x00 \ x00'
 $ ktest-tool klee-last / test000268.ktest
 ktest फ़ाइल: 'klee-last / test000268.ktest'
 args: ['maze_klee.o']
 संख्या वस्तुओं: 1
 ऑब्जेक्ट 0: नाम: 'प्रोग्राम'
 ऑब्जेक्ट 0: आकार: 29
 ऑब्जेक्ट 0: डेटा: 'ssssddddwwaawwddddssssddwwww \ x00' 

तो, इस भूलभुलैया के समाधान:
1. ssssddddwwaawwddddssssddwwww
2. ssssddddwwaawwddddsddw
3. sddwddddssssddwwww
4. sddwddddsddw