component---src-docs-advanced-symbolic-execution-md-bc1435f0f919bef3611c.js

"use strict";(self.webpackChunkunittestbot_web=self.webpackChunkunittestbot_web||[]).push([[3669],{14247:function(e,t,n){n.r(t),n.d(t,{_frontmatter:function(){return r},default:function(){return d}});var i=n(87462),o=n(63366),a=(n(15007),n(64983)),s=n(23017),l=(n(8156),["components"]),r={};void 0!==r&&r&&r===Object(r)&&Object.isExtensible(r)&&!Object.prototype.hasOwnProperty.call(r,"__filemeta")&&Object.defineProperty(r,"__filemeta",{configurable:!0,value:{name:"_frontmatter",filename:"src/docs/advanced/symbolic-execution.md"}});var c={_frontmatter:r},u=s.Z;function d(e){var t=e.components,n=(0,o.Z)(e,l);return(0,a.kt)(u,(0,i.Z)({},c,n,{components:t,mdxType:"MDXLayout"}),(0,a.kt)("p",null,"UTBot runs KLEE by fork() + exec() method and controls symbolic execution via waitpid(). UTBot uses Z3 version 4.8.7 as\nSMT-solver for KLEE. Symbolic execution of each function under test issues a separate KLEE run, which symbolically\nexecutes the function wrapper generated by UTBot. UTBot gives KLEE a configurable amount of time to symbolically execute\ngiven bitcode, and, when it ends, sends KLEE a SIGINT signal, which is correctly handled by KLEE in many cases — the\nengine saves explored paths and finishes the execution. However, there are scenarios where KLEE does not handle SIGINTs\ncorrectly due to missing handlers in some parts of its code; so UTBot waits a specified amount of time and then sends\nstronger signals: SIGSTOP, and, eventually, SIGKILL. UTBot KLEE configuration. UTBot runs KLEE with the following\nparameters:"),(0,a.kt)("pre",null,(0,a.kt)("code",{parentName:"pre",className:"language-shell"},"klee --entry-point=klee_entry__max\n--libc=klee --posix-runtime --fp-runtime\n--only-output-states-covering-new \n--allocate-determ --external-calls=all \n--timer-interval=1s --bcov-check-interval=5s\n--disable-verify --output-dir=klee-out-dir\nbitcode.bc --sym-stdin 64\n")),(0,a.kt)("p",null,"Let us explain every KLEE command line option passed by UTBot in detail:"),(0,a.kt)("ul",null,(0,a.kt)("li",{parentName:"ul"},"KLEE is given a bitcode representation of a project target, which may contain many functions, so KLEE understands\nwhere to begin symbolic execution by an entry-point option. To improve symbolic execution possibilities, KLEE needs to\nbe supplied with standard C library, i.e. libc, compiled into LLVM IR. There is a choice one can make between using\nKLEE libc — a small set of libc functions shipped with KLEE itself,\nor ",(0,a.kt)("a",{parentName:"li",href:"https://github.com/klee/klee-uclibc"},"klee-uclibc"),", a more complete package, which can be linked with KLEE and used\nduring symbolic execution. Again (as with POSIX runtime), this KLEE libc or klee-uclibc library can be treated as\nstubs that used by KLEE instead of real libc. UTBot uses KLEE libc. Despite that a wider set of functions is\nimplemented in klee-uclibc, using it forces KLEE to analyse additional several thousands of LLVM instructions prior to\nanalysing actual code of UTBot wrapper, consequently, slowing down UTBot test generation. It is understood that\ncoverage may be lost using –libc=klee instead of –libc=uclibc, so it is planned to make the libc selection\nconfigurable;"),(0,a.kt)("li",{parentName:"ul"},"UTBot uses KLEE POSIX runtime and self-developed floatingpoint runtime library to allow symbolic execution of programs\noperating with file descriptors and floating-point values;"),(0,a.kt)("li",{parentName:"ul"},"–only-output-states-covering-new option is used to not generate tests executing the same path in user functions;"),(0,a.kt)("li",{parentName:"ul"},"UTBot allows all external calls to discard minimal number of branches. External call is a possibility of KLEE to\nexecute a function not implemented in LLVM IR. For that, function arguments are concretized, which potentially leads\nto a coverage loss, but other options of handling external function calls, like killing an execution branch, are even\nworse in terms of achieving maximal coverage;"),(0,a.kt)("li",{parentName:"ul"},"timer-interval and self-invented bcov-check-interval are used to stop symbolic execution of branches not promising to\nincrease coverage;"),(0,a.kt)("li",{parentName:"ul"},"UTBot allows using 64 bytes of symbolic stdin;"),(0,a.kt)("li",{parentName:"ul"},"UTBot uses –disable-verify as its linking procedure (Section 3.3) passes only correct bitcode to KLEE.")))}d&&d===Object(d)&&Object.isExtensible(d)&&!Object.prototype.hasOwnProperty.call(d,"__filemeta")&&Object.defineProperty(d,"__filemeta",{configurable:!0,value:{name:"MDXContent",filename:"src/docs/advanced/symbolic-execution.md"}}),d.isMDXComponent=!0}}]);
//# sourceMappingURL=component---src-docs-advanced-symbolic-execution-md-bc1435f0f919bef3611c.js.map