{"id":1113,"date":"2023-11-13T12:22:59","date_gmt":"2023-11-13T03:22:59","guid":{"rendered":"https:\/\/h4ck.kr\/?p=1113"},"modified":"2023-11-13T13:17:24","modified_gmt":"2023-11-13T04:17:24","slug":"klee-%ec%b2%ab%eb%b2%88%ec%a7%b8-%ed%8a%9c%ed%86%a0%eb%a6%ac%ec%96%bc-%ec%9e%91%ec%9d%80-%ed%95%a8%ec%88%98%eb%a5%bc-%ed%85%8c%ec%8a%a4%ed%8a%b8%ed%95%b4%eb%b3%b4%ea%b8%b0","status":"publish","type":"post","link":"https:\/\/h4ck.kr\/?p=1113","title":{"rendered":"KLEE \uccab\ubc88\uc9f8 \ud29c\ud1a0\ub9ac\uc5bc: \uc791\uc740 \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud574\ubcf4\uae30"},"content":{"rendered":"\n<h2 class=\"wp-block-heading\">\uc791\uc740 \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud574\ubcf4\uae30<\/h2>\n\n\n\n<p>\uc774 \ud29c\ud1a0\ub9ac\uc5bc\uc740 KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \uac04\ub2e8\ud55c \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud558\ub294 \ub370 \ud544\uc694\ud55c \uc8fc\uc694 \ub2e8\uacc4\ub97c \uc124\uba85\ud55c\ub2e4.<\/p>\n\n\n\n<p>\ub2e4\uc74c\uc740 <strong>get_sign<\/strong>\uc774\ub77c\ub294 \uac04\ub2e8\ud55c \ud568\uc218\uc774\ub2e4.<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li><a href=\"https:\/\/klee.github.io\/resources\/get_sign.c.html\">get_sign.c<\/a><\/li>\n<\/ul>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"c\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">int get_sign(int x) {\n  if (x == 0)\n    return 0;\n\n  if (x &lt; 0)\n    return -1;\n  else\n    return 1;\n}<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uc774 \uc608\uc81c\uc758 \uc804\uccb4 \ucf54\ub4dc\ub294 <strong>examples\/get_sign<\/strong> \uc544\ub798\uc758 \uc18c\uc2a4 \ud2b8\ub9ac\uc5d0\uc11c \ucc3e\uc744 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n<p>\uc18c\uc2a4 \ucf54\ub4dc\uc758 \ubc84\uc804\uc740 <a href=\"http:\/\/klee.github.io\/resources\/get_sign.c.html\">\uc5ec\uae30<\/a>\uc5d0\uc11c\ub3c4 \ud655\uc778\ud560 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">\uc2ec\ubcfc\ub9ad\uc73c\ub85c \uc785\ub825 \ud45c\uc2dc\ud558\uae30<\/h2>\n\n\n\n<p><strong>get_sign<\/strong> \ud568\uc218\ub97c KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ud14c\uc2a4\ud2b8\ud558\uae30 \uc704\ud574\uc11c\ub294, \uc6b0\ub9ac\uac00 \uc2ec\ubcfc\ub9ad \uc785\ub825\uc744 \ud1b5\ud574 \uc2e4\ud589\uc2dc\ud0ac \ud544\uc694\uac00 \uc788\ub2e4.<\/p>\n\n\n\n<p>\ubcc0\uc218\ub97c \uc2ec\ubcfc\ub9ad\uc73c\ub85c \ud45c\uc2dc\ud558\uae30 \uc704\ud574\uc11c\ub294, <strong>klee\/klee.h <\/strong>\ud5e4\ub354\uc5d0 \uc815\uc758\ub41c <strong>klee_make_symbolic()<\/strong> \ud568\uc218\ub97c \uc0ac\uc6a9\ud560 \uc218 \uc788\ub2e4.<\/p>\n\n\n\n<p>\uc774 \ud568\uc218\ub294 \uc138 \uac1c\uc758 \uc778\uc218\ub97c \ubc1b\uc744 \uc218 \uc788\ub294\ub370, \uc6b0\ub9ac\uac00 \uc2ec\ubcfc\ub85c \ub2e4\ub8e8\uace0\uc790 \ud558\ub294 \ubcc0\uc218\uc758 \uc8fc\uc18c (=\uba54\ubaa8\ub9ac \uc704\uce58), \uadf8 \ud06c\uae30, \uadf8\ub9ac\uace0 \uc774\ub984(\uc784\uc758\ub85c \uc9c0\uc815 \uac00\ub2a5) \uc774\ub807\uac8c \uad6c\uc131\ub418\uc5b4 \uc788\ub2e4.<\/p>\n\n\n\n<p>\ub2e4\uc74c\uc740 \ubcc0\uc218 \u2018a\u2019 \ub97c \uc2ec\ubcfc\ub9ad\uc73c\ub85c \ud45c\uc2dc\ud558\uace0, \uc774\ub97c \ud1b5\ud574 <strong>get_sign()<\/strong> \ud568\uc218\ub97c \ud638\ucd9c\ud558\ub294 \uac04\ub2e8\ud55c<strong> main()<\/strong> \ud568\uc218 \uc608\uc81c\uc774\ub2e4!<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"c\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">int main() {\n  int a;\n  klee_make_symbolic(&amp;a, sizeof(a), \"a\");\n  return get_sign(a);\n}<\/pre>\n<\/div>\n<\/div>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"577\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1024x577.png\" alt=\"\" class=\"wp-image-1114\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1024x577.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-300x169.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-768x433.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">LLVM bitCode\ub85c \ucef4\ud30c\uc77c\ud558\uae30<\/h2>\n\n\n\n<p>KLEE\ub294 LLVM bitCode\uc5d0\uc11c \uc791\ub3d9\ud55c\ub2e4.<\/p>\n\n\n\n<p>KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ud504\ub85c\uadf8\ub7a8\uc744 \uc2e4\ud589\uc2dc\ud0a4\ub824\uba74, \uba3c\uc800 clang \ucef4\ud30c\uc77c\ub7ec\uc5d0\uc11c <strong>-emit-llvm<\/strong> \uc635\uc158\uc744 \uc0ac\uc6a9\ud558\uc5ec LLVM bitCode\ub85c \ucef4\ud30c\uc77c\ud574\uc57c \ub41c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ clang -I \/snap\/klee\/6\/usr\/local\/include -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone get_sign.c<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uc704 \uba85\ub839\uc744 \uc2e4\ud589\ud558\uba74, LLVM bitCode \ud615\uc2dd\uc778 <strong>get_sign.bc<\/strong> \ud30c\uc77c\uc744 \uc0dd\uc131\uc2dc\ud0a8\ub2e4.<\/p>\n\n\n\n<p><strong>-I<\/strong> \uc635\uc158\uc740 \ucef4\ud30c\uc77c\ub7ec\uac00 KLEE \uac00\uc0c1 \uba38\uc2e0\uacfc \uc0c1\ud638 \uc791\uc6a9\ud558\uae30 \uc704\ud574 \uc0ac\uc6a9\ub418\ub294 \ub0b4\uc7a5 \ud568\uc218\uc758 \uc815\uc758\ub97c \ud3ec\ud568\ud558\ub294 <strong>klee\/klee.h<\/strong> \ud5e4\ub354 \ud30c\uc77c\uc744 \ucc3e\uc744 \uc218 \uc788\ub3c4\ub85d \uc0ac\uc6a9\ub41c\ub2e4.<\/p>\n\n\n\n<p>\uc774\ub7ec\ud55c \ub0b4\uc7a5 \ud568\uc218\uc5d0\ub294 <strong>klee_make_symbolic<\/strong>\uacfc \uac19\uc740 \ud568\uc218\ub4e4\ub3c4 \ud3ec\ud568\ub41c\ub2e4.<\/p>\n\n\n\n<p><strong>-g<\/strong> \uc635\uc158\uc740 bitCode \ud30c\uc77c\uc5d0 \uc18c\uc2a4 \uc904\ubc88\ud638\uc640 \ud568\uaed8 \ub2f4\uae34 \ub514\ubc84\uae45 \uc815\ubcf4\ub97c \uc0dd\uc131\ud558\ub3c4\ub85d \ub9cc\ub4e0\ub2e4.<\/p>\n\n\n\n<div style=\"height:20px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n<p>KLEE\uc5d0 \uc804\ub2ec\ub418\ub294 bitcode\uac00 \ucd5c\uc801\ud654\ub418\uc5b4\uc11c\ub294 \uc548\ub41c\ub2e4. KLEE\uc758 <strong>&#8211;optimize<\/strong> \ucee4\ub9e8\ub4dc \ub77c\uc778 \uc635\uc158\uc744 \uc0ac\uc6a9\ud558\uc5ec \ud65c\uc131\ud654\ud560 \uc218 \uc788\ub294 KLEE\uc758 \ucd5c\uc801\ud654\ub97c \uc774\ubbf8 \uc9c1\uc811 \uc120\ud0dd\ud588\uae30 \ub54c\ubb38\uc774\ub2e4.<\/p>\n\n\n\n<p>\uadf8\ub7ec\ub098 \ucd5c\uc2e0 LLVM \ubc84\uc804(5.0 \uc774\uc0c1)\uc5d0\uc11c\ub294 <strong>-O0<\/strong> \uc635\uc158\uc744 KLEE\ub97c \uc704\ud574 \ucef4\ud30c\uc77c\ud560 \ub54c \uc0ac\uc6a9\ud574\uc11c\ub294 \uc548\ub41c\ub2e4.<\/p>\n\n\n\n<p>KLEE\uac00 \uc790\uccb4 \ucd5c\uc801\ud654\ub97c \uc218\ud589\ud558\ub294 \uac83\uc744 \ubc29\ud574\ud558\uae30 \ub54c\ubb38\uc774\ub2e4. \uadf8 \ub300\uc2e0\uc5d0 <strong>-O0 -Xclang -disable-O0-optnone<\/strong> \uc635\uc158\uc744 \uc0ac\uc6a9\ud574\uc57c \ub41c\ub2e4.<\/p>\n\n\n\n<p>(\uc790\uc138\ud55c \ub0b4\uc6a9\uc740 <a href=\"https:\/\/github.com\/klee\/klee\/issues\/902\">\uc774 \uc774\uc288<\/a>\ub97c \ucc38\uc870\ud560 \uac83)<\/p>\n\n\n\n<div style=\"height:20px\" aria-hidden=\"true\" class=\"wp-block-spacer\"><\/div>\n\n\n\n<p>\ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \ub2e4\uc2dc \uc2e4\ud589\uc2dc\ud0ac \uc758\ub3c4\uac00 \uc5c6\uace0 \ub514\ubc84\uadf8 \uc815\ubcf4\ub098 \ucd5c\uc801\ud654\uc5d0 \uad00\uc2ec\uc774 \uc5c6\ub2e4\uba74 <strong>klee\/klee.h<\/strong>\ub97c \uc0ad\uc81c\ud55c \ud6c4 <strong>get_sign.c<\/strong>\ub97c \ub2e4\uc74c\uacfc \uac19\uc774 \ucef4\ud30c\uc77c\ud560 \uc218 \uc788\ub2e4:<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ clang -emit-llvm -c get_sign.c<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uadf8\ub7ec\ub098 \ub354 \uae34 \uba85\ub839\uc5b4\ub97c \uc0ac\uc6a9\ud558\ub294 \uac83\uc744 \uad8c\uc7a5\ud55c\ub2e4.<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"577\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1-1024x577.png\" alt=\"\" class=\"wp-image-1115\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1-1024x577.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1-300x169.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1-768x433.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-1.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">KLEE \uc2e4\ud589\ud558\uae30<\/h2>\n\n\n\n<p>bitCode \ud30c\uc77c\uc5d0\uc11c KLEE\ub97c \uc2e4\ud589\ud558\ub824\uba74 \ub2e4\uc74c \uba85\ub839\uc744 \uc2e4\ud589\ud55c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ klee get_sign.bc<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uadf8\ub7ec\uba74 \ub2e4\uc74c\uacfc \uac19\uc740 \ucd9c\ub825\uc744 \uc5bb\uac8c \ub41c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">KLEE: output directory is \"\/home\/ubuntu\/whitehat\/IOT-research\/klee-study\/klee-out-0\"\nKLEE: Using STP solver backend\nKLEE: SAT solver: MiniSat\n\nKLEE: done: total instructions = 33\nKLEE: done: completed paths = 3\nKLEE: done: partially completed paths = 0\nKLEE: done: generated tests = 3<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uac04\ub2e8\ud55c \ud568\uc218\ub97c \ud1b5\uacfc\ud558\ub294 \uc138 \uac00\uc9c0 \uacbd\ub85c\uac00 \uc788\ub294\ub370, <br>a\uac00 0\uc778 \uacbd\uc6b0, 0\ubcf4\ub2e4 \uc791\uc740 \uacbd\uc6b0, \uadf8\ub9ac\uace0 0\ubcf4\ub2e4 \ud070 \uacbd\uc6b0 <br>\u2192 \uc774\ub807\uac8c 3\uac00\uc9c0\ub2e4.<\/p>\n\n\n\n<p>\uc608\uc0c1\ub300\ub85c, KLEE\ub294 \ud504\ub85c\uadf8\ub7a8\uc5d0\uc11c 3\uac00\uc9c0 \uacbd\ub85c\ub97c \ud0d0\uc0c9\ud558\uace0 \uac01 \uacbd\ub85c\uc5d0 \ub300\ud574 \ud558\ub098\uc758 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc0dd\uc131\ud588\ub2e4\uace0 \uc54c\ub824\uc900\ub2e4.<\/p>\n\n\n\n<p>\ud070 \ud504\ub85c\uadf8\ub7a8\uc758 \uacbd\uc6b0, KLEE\ub294 \uc2dc\uac04 \ub610\ub294 \uba54\ubaa8\ub9ac \uc81c\uc57d\uc73c\ub85c \uc778\ud574\uc11c \uac01 \uacbd\ub85c\ub97c \ub05d\uae4c\uc9c0 \ud0d0\uc0c9\ud560 \uc218 \uc5c6\uc744 \uc218\ub3c4 \uc788\ub2e4.<\/p>\n\n\n\n<p>\uc774\ub7ec\ud55c \uacbd\uc6b0\uc5d0\ub294, \uc77c\ubd80 \uc644\ub8cc\ub41c \uacbd\ub85c\uc758 \uc218\uc5d0 \ub300\ud574 \uc54c\ub824\uc900\ub2e4.<\/p>\n\n\n\n<p>KLEE \uc2e4\ud589\uc758 \ucd9c\ub825\uc740 KLEE\uc5d0 \uc758\ud574 \uc0dd\uc131\ub41c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub4e4\uc744 \ud3ec\ud568\ud558\ub294 \ub514\ub809\ud1a0\ub9ac\uac00 \ub41c\ub2e4. <br>(ex: klee-out-0)<\/p>\n\n\n\n<p>KLEE\ub294 \ucd9c\ub825 \ub514\ub809\ud1a0\ub9ac\ub97c <strong>klee-out-N<\/strong>\uc774\ub77c\uace0 \uba85\uba85\ud558\uba70, <code>N<\/code>\uc740 \uc0ac\uc6a9 \uac00\ub2a5\ud55c \uac00\uc7a5 \ub0ae\uc740 \uc22b\uc790\ub97c \uc758\ubbf8\ud55c\ub2e4. (0\ubc88\uc9c0\ubd80\ud130 \ucb49 \ud558\ub098\uc529.. \uc0dd\uc131, \ub530\ub77c\uc11c KLEE\ub97c \ub2e4\uc2dc \uc2e4\ud589\ud558\uba74 <strong>klee-out-1<\/strong>\uc774\ub77c\ub294 \ub514\ub809\ud1a0\ub9ac\ub97c \uc0dd\uc131\ud55c\ub2e4)<\/p>\n\n\n\n<p>\ub610\ud55c \ud3b8\uc758\ub97c \uc704\ud574 \uc774 \ub514\ub809\ud1a0\ub9ac\uc5d0 \ub300\ud55c \uc2ec\ubcfc\ub9ad \ub9c1\ud06c\uc778 <strong>klee-last<\/strong>\ub3c4 \uc0dd\uc131\ud55c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ ls klee-last\/\nassembly.ll  messages.txt  run.stats         test000002.ktest  warnings.txt\ninfo         run.istats    test000001.ktest  test000003.ktest<\/pre>\n<\/div>\n<\/div>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"623\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-2-1024x623.png\" alt=\"\" class=\"wp-image-1116\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-2-1024x623.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-2-300x182.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-2-768x467.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-2.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<p>KLEE\uc5d0\uc11c \uc0dd\uc131\ub41c \ud30c\uc77c\ub4e4\uc758 \uac1c\uc694\ub97c \ubcf4\uace0 \uc2f6\ub2e4\uba74 <a href=\"https:\/\/klee.github.io\/docs\/files\/\">\uc5ec\uae30<\/a>\ub97c \ucc38\uace0\ud560 \uac83.<\/p>\n\n\n\n<p>\uc774 \ud29c\ud1a0\ub9ac\uc5bc\uc5d0\uc11c\ub294 KLEE\uc5d0\uc11c \uc0dd\uc131\ud55c \uc2e4\uc81c \ud14c\uc2a4\ud2b8 \ud30c\uc77c\uc5d0\ub9cc \ucd08\uc810\uc744 \ub9de\ucd98\ub2e4.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">KLEE\uc5d0\uc11c \uc0dd\uc131\ub41c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4<\/h2>\n\n\n\n<p>KLEE\uc5d0\uc11c \uc0dd\uc131\ub41c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub294 <strong>.ktest<\/strong> \ud655\uc7a5\uc790\ub97c \uac00\uc9c4 \ud30c\uc77c\ub85c \uc791\uc131\ub41c\ub2e4.<\/p>\n\n\n\n<p>\uc774\ub4e4\uc740 <strong>ktest-tool<\/strong> \uc720\ud2f8\ub9ac\ud2f0\ub85c \uc77d\uc744 \uc218 \uc788\ub294 \ubc14\uc774\ub108\ub9ac \ud30c\uc77c\ub4e4\uc774\ub2e4.<\/p>\n\n\n\n<p><strong>ktest-tool<\/strong>\uc740 \ub3d9\uc77c\ud55c \uac1d\uccb4\uc5d0 \ub300\ud574 \ub2e4\uc591\ud55c \ud45c\ud604\uc744 \ucd9c\ub825\ud558\uba70, \uc774\ub97c \ud14c\uba74 Python \ubc14\uc774\ud2b8 \ubb38\uc790\uc5f4(\ub370\uc774\ud130), \uc815\uc218(int) \ub610\ub294 ASCII \ud14d\uc2a4\ud2b8(\ud14d\uc2a4\ud2b8) \ub4f1\uc774 \ub418\uaca0\ub2e4.<\/p>\n\n\n\n<p>\ub530\ub77c\uc11c \uac01 \ud30c\uc77c\uc744 \uc0b4\ud3b4\ubcf4\ub3c4\ub85d \ud558\uc790.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"generic\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ \/snap\/klee\/6\/usr\/local\/bin\/ktest-tool klee-last\/test000001.ktest\nktest file : 'klee-last\/test000001.ktest'\nargs       : ['get_sign.bc']\nnum objects: 1\nobject 0: name: 'a'\nobject 0: size: 4\nobject 0: data: b'\\\\x00\\\\x00\\\\x00\\\\x00'\nobject 0: hex : 0x00000000\nobject 0: int : 0\nobject 0: uint: 0\nobject 0: text: ....\n$ \/snap\/klee\/6\/usr\/local\/bin\/ktest-tool klee-last\/test000002.ktest\nktest file : 'klee-last\/test000002.ktest'\nargs       : ['get_sign.bc']\nnum objects: 1\nobject 0: name: 'a'\nobject 0: size: 4\nobject 0: data: b'\\\\x01\\\\x01\\\\x01\\\\x01'\nobject 0: hex : 0x01010101\nobject 0: int : 16843009\nobject 0: uint: 16843009\nobject 0: text: ....\n$ \/snap\/klee\/6\/usr\/local\/bin\/ktest-tool klee-last\/test000003.ktest\nktest file : 'klee-last\/test000003.ktest'\nargs       : ['get_sign.bc']\nnum objects: 1\nobject 0: name: 'a'\nobject 0: size: 4\nobject 0: data: b'\\\\x00\\\\x00\\\\x00\\\\x80'\nobject 0: hex : 0x00000080\nobject 0: int : -2147483648\nobject 0: uint: 2147483648\nobject 0: text: ....\n<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uac01 \ud14c\uc2a4\ud2b8 \ud30c\uc77c\uc5d0 \ub300\ud574 KLEE\ub294 \ud504\ub85c\uadf8\ub7a8\uc774 \ud638\ucd9c\ub41c \uc778\uc218(\ud544\uc790\uc758 \uacbd\uc6b0, \uc778\uc790\uac00 \uc5c6\uace0 \ud504\ub85c\uadf8\ub7a8 \uc774\ub984\ub9cc \uc788\uc74c), \ud574\ub2f9 \uacbd\ub85c\uc758 \uc2ec\ubcfc\ub9ad \uac1d\uccb4 \uc218(\ud544\uc790\uc758 \uacbd\uc6b0, \ud558\ub098\ubfd0), \uc2ec\ubcfc\ub9ad \uac1d\uccb4\uc758 \uc774\ub984(<strong>&#8216;a&#8217;<\/strong>) \ubc0f \ud06c\uae30(<strong>4<\/strong>)\ub97c \ubcf4\uace0\ud574\uc900\ub2e4.<\/p>\n\n\n\n<p>\uc2e4\uc81c \ud14c\uc2a4\ud2b8 \uc790\uccb4\ub294 \uc785\ub825\uac12\uc73c\ub85c \ub098\ud0c0\ub09c\ub2e4:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>\uccab \ubc88\uc9f8 \ud14c\uc2a4\ud2b8\uc758 \uacbd\uc6b0 <strong>0<\/strong><\/li>\n\n\n\n<li>\ub450 \ubc88\uc9f8 \ud14c\uc2a4\ud2b8\uc758 \uacbd\uc6b0 <strong>16843009<\/strong><\/li>\n\n\n\n<li>\ub9c8\uc9c0\ub9c9 \ud14c\uc2a4\ud2b8\uc758 \uacbd\uc6b0 <strong>-2147483648<\/strong><\/li>\n<\/ul>\n\n\n\n<p>\uc608\uc0c1\ub300\ub85c, KLEE\ub294 <strong>0<\/strong>\uc774\ub77c\ub294 \uac12\uacfc, \uc591\uc758 \uac12 \ud558\ub098(<strong>16843009<\/strong>), \uadf8\ub9ac\uace0 \uc74c\uc758 \uac12 \ud558\ub098(<strong>-2147483648<\/strong>)\uc744 \uc0dd\uc131\ud588\ub2e4.<\/p>\n\n\n\n<p>\uc774\uc81c \uc774\ub7ec\ud55c \uac12\ub4e4\uc744 \uc6b0\ub9ac \ucf54\ub4dc\uc758 \ub124\uc774\ud2f0\ube0c \ubc84\uc804\uc5d0\uc11c \uc2e4\ud589\uc2dc\ucf1c \ucf54\ub4dc\ub97c \ud1b5\uacfc\ud558\ub294 \ubaa8\ub4e0 \uacbd\ub85c\ub97c \ud655\uc778\ud560 \uc218 \uc788\ub2e4!<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"788\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-3-1024x788.png\" alt=\"\" class=\"wp-image-1118\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-3-1024x788.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-3-300x231.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-3-768x591.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-3.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">\ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \ub2e4\uc2dc \uc2e4\ud589\ud558\uae30<\/h2>\n\n\n\n<p>KLEE\uac00 \uc0dd\uc131\ud55c \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc218\ub3d9\uc73c\ub85c (\ub610\ub294 \uae30\uc874\uc758 \ud14c\uc2a4\ud2b8 \uc778\ud504\ub77c \ub3c4\uc6c0\uc744 \ubc1b\uc544) \ud504\ub85c\uadf8\ub7a8\uc5d0\uc11c \uc2e4\ud589\ud560 \uc218\ub3c4 \uc788\uc9c0\ub9cc,<\/p>\n\n\n\n<p>KLEE\ub294 \uac04\ub2e8\ud55c \uc7ac\uc0dd \ub77c\uc774\ube0c\ub7ec\ub9ac\ub97c \uc81c\uacf5\ud558\uba70, \uc774\ub97c \uc0ac\uc6a9\ud558\uba74 <strong>klee_make_symbolic<\/strong> \ud638\ucd9c\uc744 <strong>.ktest<\/strong> \ud30c\uc77c\uc5d0 \uc800\uc7a5\ub41c \uac12\uc73c\ub85c \ub300\uccb4\ud558\ub294 \ud568\uc218 \ud638\ucd9c\uc774 \uc218\ud589\ub41c\ub2e4.<\/p>\n\n\n\n<p>\uc774\ub97c \uc0ac\uc6a9\ud558\ub824\uba74 \ud504\ub85c\uadf8\ub7a8\uc744 <strong>libkleeRuntest<\/strong> \ub77c\uc774\ube0c\ub7ec\ub9ac\ub85c \ub9c1\ud06c\ud558\uace0 <strong>KTEST_FILE<\/strong> \ud658\uacbd \ubcc0\uc218\ub97c \uc6d0\ud558\ub294 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\uc758 \uc774\ub984\uc744 \uac00\ub9ac\ud0a4\ub3c4\ub85d \uc124\uc815\ud574\uc8fc\uba74 \ub41c\ub2e4.<\/p>\n\n\n\n<div class=\"wp-block-columns is-layout-flex wp-container-core-columns-is-layout-9d6595d7 wp-block-columns-is-layout-flex\">\n<div class=\"wp-block-column is-layout-flow wp-block-column-is-layout-flow\" style=\"flex-basis:100%\">\n<pre class=\"EnlighterJSRAW\" data-enlighter-language=\"raw\" data-enlighter-theme=\"dracula\" data-enlighter-highlight=\"\" data-enlighter-linenumbers=\"\" data-enlighter-lineoffset=\"\" data-enlighter-title=\"\" data-enlighter-group=\"\">$ export LD_LIBRARY_PATH=path-to-klee-build-dir\/lib\/:$LD_LIBRARY_PATH\n$ gcc -I ..\/..\/include -L path-to-klee-build-dir\/lib\/ get_sign.c -lkleeRuntest\n$ KTEST_FILE=klee-last\/test000001.ktest .\/a.out\n$ echo $?\n0\n$ KTEST_FILE=klee-last\/test000002.ktest .\/a.out\n$ echo $?\n1\n$ KTEST_FILE=klee-last\/test000003.ktest .\/a.out\n$ echo $?\n255<\/pre>\n<\/div>\n<\/div>\n\n\n\n<p>\uc608\uc0c1\ub300\ub85c, \uccab \ubc88\uc9f8 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc2e4\ud589\ud560 \ub54c \ud504\ub85c\uadf8\ub7a8\uc740 <strong>0<\/strong>\uc744 \ubc18\ud658\ud558\uace0,<\/p>\n\n\n\n<p>\ub450 \ubc88\uc9f8 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc2e4\ud589\ud560 \ub54c, <strong>1<\/strong>\uc744 \ubc18\ud658\ud558\uba70,<\/p>\n\n\n\n<p>\ub9c8\uc9c0\ub9c9 \ud14c\uc2a4\ud2b8 \ucf00\uc774\uc2a4\ub97c \uc2e4\ud589\ud560 \ub54c, <strong>255<\/strong>(-1\uc744 0-255 \ubc94\uc704\uc758 \uc720\ud6a8\ud55c \uc885\ub8cc \ucf54\ub4dc \uac12\uc73c\ub85c \ubcc0\ud658)\ub97c \ubc18\ud658\ud55c\ub2e4.<\/p>\n\n\n\n<figure class=\"wp-block-image size-large\"><img loading=\"lazy\" decoding=\"async\" width=\"1024\" height=\"788\" src=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-4-1024x788.png\" alt=\"\" class=\"wp-image-1120\" srcset=\"https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-4-1024x788.png 1024w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-4-300x231.png 300w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-4-768x591.png 768w, https:\/\/h4ck.kr\/wp-content\/uploads\/2023\/11\/Untitled-4.png 1115w\" sizes=\"auto, (max-width: 1024px) 100vw, 1024px\" \/><\/figure>\n\n\n\n<h2 class=\"wp-block-heading\">\ucd9c\ucc98 \ubc0f \ubc88\uc5ed<\/h2>\n\n\n\n<p><a href=\"https:\/\/klee.github.io\/tutorials\/testing-function\/\">https:\/\/klee.github.io\/tutorials\/testing-function\/<\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>\uc791\uc740 \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud574\ubcf4\uae30 \uc774 \ud29c\ud1a0\ub9ac\uc5bc\uc740 KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \uac04\ub2e8\ud55c \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud558\ub294 \ub370 \ud544\uc694\ud55c \uc8fc\uc694 \ub2e8\uacc4\ub97c \uc124\uba85\ud55c\ub2e4. \ub2e4\uc74c\uc740 get_sign\uc774\ub77c\ub294 \uac04\ub2e8\ud55c \ud568\uc218\uc774\ub2e4. \uc774 \uc608\uc81c\uc758 \uc804\uccb4 \ucf54\ub4dc\ub294 examples\/get_sign \uc544\ub798\uc758 \uc18c\uc2a4 \ud2b8\ub9ac\uc5d0\uc11c \ucc3e\uc744 \uc218 \uc788\ub2e4. \uc18c\uc2a4 \ucf54\ub4dc\uc758 \ubc84\uc804\uc740 \uc5ec\uae30\uc5d0\uc11c\ub3c4 \ud655\uc778\ud560 \uc218 \uc788\ub2e4. \uc2ec\ubcfc\ub9ad\uc73c\ub85c \uc785\ub825 \ud45c\uc2dc\ud558\uae30 get_sign \ud568\uc218\ub97c KLEE\ub97c \uc0ac\uc6a9\ud558\uc5ec \ud14c\uc2a4\ud2b8\ud558\uae30 \uc704\ud574\uc11c\ub294, \uc6b0\ub9ac\uac00 \uc2ec\ubcfc\ub9ad \uc785\ub825\uc744 \ud1b5\ud574 \uc2e4\ud589\uc2dc\ud0ac \ud544\uc694\uac00 \uc788\ub2e4. \ubcc0\uc218\ub97c \uc2ec\ubcfc\ub9ad\uc73c\ub85c&hellip;&nbsp;<a href=\"https:\/\/h4ck.kr\/?p=1113\" rel=\"bookmark\">\ub354 \ubcf4\uae30 &raquo;<span class=\"screen-reader-text\">KLEE \uccab\ubc88\uc9f8 \ud29c\ud1a0\ub9ac\uc5bc: \uc791\uc740 \ud568\uc218\ub97c \ud14c\uc2a4\ud2b8\ud574\ubcf4\uae30<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"neve_meta_sidebar":"","neve_meta_container":"","neve_meta_enable_content_width":"","neve_meta_content_width":0,"neve_meta_title_alignment":"","neve_meta_author_avatar":"","neve_post_elements_order":"","neve_meta_disable_header":"","neve_meta_disable_footer":"","neve_meta_disable_title":"","footnotes":""},"categories":[15],"tags":[20],"class_list":["post-1113","post","type-post","status-publish","format-standard","hentry","category-whitehat1","tag-klee"],"_links":{"self":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1113","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=1113"}],"version-history":[{"count":13,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1113\/revisions"}],"predecessor-version":[{"id":1163,"href":"https:\/\/h4ck.kr\/index.php?rest_route=\/wp\/v2\/posts\/1113\/revisions\/1163"}],"wp:attachment":[{"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=1113"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=1113"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/h4ck.kr\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=1113"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}