[ 0:00] + SRC=/home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c [ 0:00] + sim /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c [ 0:00] compiling /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c [ 0:01] [ 0:11] ^ —————. —.— . . —.— . . .————— . . [ 0:11] ——— | | | | | | |\ | | | | [ 0:11] —(o)— | | | | | | | \ | |———— '————| [ 0:11] ——————— | | | \ / | | \| | | [ 0:11] ————————— —————' —'— ' —'— ' ' '————— ' [ 0:11] [ 0:11] Welcome to 'divine sim', an interactive debugger. Type 'help' to get started. [ 0:11] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:11] > help [ 0:11] # Interactive Debugging {#sim} [ 0:11] [ 0:11] DIVINE comes with an interactive debugger, available as `divine sim`. The [ 0:11] debugger loads programs the same way `verify` and other DIVINE commands do, so [ 0:11] you can run it on standalone C or C++ source files directly, or you can compile [ 0:11] larger programs into bitcode and load that. [ 0:11] [ 0:11] ## Tutorial [ 0:11] [ 0:11] Let's say you have a small C program which you wish to debug. We will refer to [ 0:11] this program as `program.c`. To load the program into the debugger, simply execute [ 0:11] [ 0:11] $ divine sim program.c [ 0:11] [ 0:11] and DIVINE will take care of compiling and linking your program. It will load [ 0:11] the resulting bitcode but will not execute it immediately: instead, `sim` will [ 0:11] present a prompt to you, looking like this: [ 0:11] [ 0:11] # executing __boot at /divine/src/dios/dios.cpp:79 [ 0:11] > [ 0:11] [ 0:11] The `__boot` function is common to all DIVINE-compiled programs and belongs to [ 0:11] DiOS, our minimalist operating system. When debugging user-mode programs, the [ 0:11] good first command to run is [ 0:11] [ 0:11] > start [ 0:11] [ 0:11] which will start executing the program until it enters the `main` function: [ 0:11] [ 0:11] # a new program state was stored as #1 [ 0:11] # active threads: [0:0] [ 0:11] # a new program state was stored as #2 [ 0:11] # active threads: [0:0] [ 0:11] # executing main at program.c:14 [ 0:11] > [ 0:11] [ 0:11] We can already see a few DIVINE-specific features of the debugger. First, [ 0:11] program states are stored and retained for future reference. Second, thread [ 0:11] switching is quite explicit -- every time a scheduling decision is made, `sim` [ 0:11] informs you of this fact. We will look at how to influence these decisions [ 0:11] later. [ 0:11] [ 0:11] Now is a good time to familiarise ourselves with how to inspect the [ 0:11] program. There are two commands for listing the program itself: `source` and [ 0:11] `bitcode` and each will print the currently executing function in the [ 0:11] appropriate form (the original C source code and LLVM bitcode, [ 0:11] respectively). Additionally, when printing bitcode, the current values of all [ 0:11] LLVM registers are shown as inline comments: [ 0:11] [ 0:11] label %entry: [ 0:11] >> %01 = alloca [i32 1 d] # [global* 0 0 uun] [ 0:11] dbg.declare [ 0:11] %03 = getelementptr %01 [i32 0 d] [i32 0 d] # [global* 0 0 uun] [ 0:11] call @init %03 [ 0:11] [ 0:11] Besides printing the currently executing function, both `source` and `bitcode` [ 0:11] can print code corresponding to other functions; in fact, by default they print [ 0:11] whatever function the debugger variable `$frame` refers to. To print the source [ 0:11] code of the current function's caller, you can issue [ 0:11] [ 0:11] > source caller [ 0:11] 97 void _start( int l, int argc, char **argv, char **envp ) { [ 0:11] >> 98 int res = __execute_main( l, argc, argv, envp ); [ 0:11] 99 exit( res ); [ 0:11] 100 } [ 0:11] [ 0:11] To inspect data, we can instead use `show` and `inspect`. We have mentioned [ 0:11] `$frame` earlier: there is, in fact, a number of variables set by `sim`. The [ 0:11] most interesting of those is `$_` which normally refers to the most interesting [ 0:11] object at hand, typically the executing frame. By default, `show` will print [ 0:11] the content of `$_` (like many other commands). However, when we pass an [ 0:11] explicit parameter to these commands, the difference between `show` and [ 0:11] `inspect` becomes apparent: the latter also sets `$_` to its parameter. This [ 0:11] makes `inspect` more suitable for exploring more complex data, while `show` is [ 0:11] useful for quickly glancing at nearby values: [ 0:11] [ 0:11] > step --count 2 [ 0:11] > show [ 0:11] attributes: [ 0:11] address: heap* 9cd25662 0+0 [ 0:11] shared: 0 [ 0:11] pc: code* 2 2 [ 0:11] insn: dbg.declare [ 0:11] location: program.c:16 [ 0:11] symbol: main [ 0:11] .x: [ 0:11] type: int[] [ 0:11] .[0]: [ 0:11] type: int [ 0:11] value: [i32 0 u] [ 0:11] .[1]: [ 0:11] type: int [ 0:11] value: [i32 0 u] [ 0:11] .[2]: [ 0:11] type: int [ 0:11] value: [i32 0 u] [ 0:11] .[3]: [ 0:11] type: int [ 0:11] value: [i32 0 u] [ 0:11] related: [ caller ] [ 0:11] [ 0:11] This is how a frame is presented when we look at it with `show`. [ 0:11] [ 0:11] ## Collecting Information [ 0:11] [ 0:11] Apart from `show` and `inspect` which simply print structured program data to [ 0:11] the screen, there are additional commands for data extraction. First, [ 0:11] `backtrace` will print the entire stack trace in one go, by default starting [ 0:11] with the currently executing frame. It is also possible to obtain *all* stack [ 0:11] traces reachable from a given heap variable, e.g. [ 0:11] [ 0:11] > backtrace $state [ 0:11] # backtrace 1: [ 0:11] __dios::_InterruptMask::Without::Without(__dios::_InterruptMask&) [ 0:11] at /divine/include/libc/include/sys/interrupt.h:42 [ 0:11] _pthread_join(__dios::_InterruptMask&, _DiOS_TLS*, void**) [ 0:11] at /divine/include/libc/include/sys/interrupt.h:77 [ 0:11] pthread_join at /divine/src/libc/functions/sys/pthread.cpp:539 [ 0:11] main at test/pthread/2.mutex-good.c:22 [ 0:11] _start at /divine/src/libc/functions/sys/start.cpp:76 [ 0:11] # backtrace 2: [ 0:11] __pthread_entry at /divine/src/libc/functions/sys/pthread.cpp:447 [ 0:11] [ 0:11] Another command to gather data is `call`, which allows you to call a function [ 0:11] defined in the program. The function must not take any parameters and will be [ 0:11] executed in *debug mode* (see [@sec:debugmode] -- the important caveat is that [ 0:11] any `dbg.call` instructions in your info function will be ignored). Execution [ 0:11] of the function will have no effect on the state of the simulated program. If [ 0:11] you have a program like this: [ 0:11] [ 0:11] ~~~ {.c} [ 0:11] #include [ 0:11] [ 0:11] void print_hello() [ 0:11] { [ 0:11] __vm_trace( _VM_T_Text, "hello world" ); [ 0:11] } [ 0:11] [ 0:11] int main() {} [ 0:11] ~~~ [ 0:11] [ 0:11] The `call` command works like this: [ 0:11] [ 0:11] > call print_hello [ 0:11] hello world [ 0:11] [ 0:11] Finally, the `info` command serves as a universal information gathering alias [ 0:11] -- you can set up your own commands that then become available as `info` [ 0:11] sub-commands: [ 0:11] [ 0:11] > info --setup "call print_hello" hello [ 0:11] > info hello [ 0:11] hello world [ 0:11] [ 0:11] The `info` command also provides a built-in sub-command `registers` which [ 0:11] prints the current values of machine control registers (see also [ 0:11] [@sec:control]): [ 0:11] [ 0:11] > info registers [ 0:11] Constants: 220000000 [ 0:11] Globals: 120000000 [ 0:11] Frame: 9cd2566220000000 [ 0:11] PC: 340000000 [ 0:11] Scheduler: eb40000000 [ 0:11] State: 4d7b876d20000000 [ 0:11] IntFrame: 1020000000 [ 0:11] Flags: 0 [ 0:11] FaultHandler: b940000000 [ 0:11] ObjIdShuffle: faa6693f [ 0:11] User1: 0 [ 0:11] User2: 201879b120000000 [ 0:11] User3: 6ca5bc2260000000 [ 0:11] User4: 0 [ 0:11] [ 0:11] # Command overview [ 0:11] [ 0:11] exit [options] exit from divine [ 0:11] help [options] show this help or describe a particular command in more detail [ 0:11] start [options] boot the system and stop at main() [ 0:11] break [options] insert a breakpoint [ 0:11] stepa [options] execute one atomic action [ 0:11] step [options] execute source line [ 0:11] stepi [options] execute one instruction [ 0:11] rewind [options] rewind to a stored program state [ 0:11] set [options] set a variable [ 0:11] bitcode [options] show the bitcode of the current function [ 0:11] source [options] show the source code of the current function [ 0:11] thread [options] control thread scheduling [ 0:11] trace [options] --choices {int} load a counterexample trace [ 0:11] show [options] show an object [ 0:11] call [options] {string} run a custom information-gathering function [ 0:11] info [options] {string} print information [ 0:11] draw [options] draw a portion of the heap [ 0:11] dot [options] draw a portion of the heap to a file of given type [ 0:11] setup [options] set configuration options [ 0:11] inspect [options] like show, but also set $_ [ 0:11] backtrace [options] show a stack trace [ 0:11] up [options] move up the stack (towards caller) [ 0:11] down [options] move down the stack (towards callee) [ 0:11] # executing __boot at /divine/src/dios/core/dios.cpp:169 [ 0:11] > start [ 0:11] # a new program state was stored as #1 [ 0:14] # active threads: [0:0] [ 0:14] # a new program state was stored as #2 [ 0:15] # active threads: [0:0] [ 0:15] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:6 [ 0:15] > step --over [ 0:15] %02 = call @malloc [i64 4 d] # [global* 0 0 uun] [ 0:15] %04 = getelementptr %02 [i64 1 d] # [global* 0 1 ddp] [ 0:15] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:7 [ 0:15] > step --over [ 0:15] %05 = ptrtoint %04 # [i64 1 d] [ 0:15] %06 = ptrtoint %02 # [i64 0 d] [ 0:15] %07 = sub %05 %06 # [i64 1 d] [ 0:15] %08 = icmp.eq %07 [i64 1 d] # [i1 1 1] [ 0:15] br %08 label %if.then label %if.end [ 0:15] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:8 [ 0:15] [ 0:16] = expected ========== [ 0:16] + ^# executing __boot [ 0:16] > help [ 0:16] + start [ 0:16] > start [ 0:16] + ^# executing main [ 0:16] > step --over [ 0:16] + ^# executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:7 [ 0:16] > step --over [ 0:16] + ^# executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:8 [ 0:16] [ 0:16] = matched =========== [ 0:16] # executing __boot at /divine/src/dios/core/dios.cpp:169 | ^# executing __boot [ 0:16] > help | ^> help [ 0:16] > start | start [ 0:16] > start | ^> start [ 0:16] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:6 | ^# executing main [ 0:16] > step --over | ^> step --over [ 0:16] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:7 | ^# executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:7 [ 0:16] > step --over | ^> step --over [ 0:16] # executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:8 | ^# executing main at /home/xrockai/src/divine/nightly/test/c/2.pointer-arith.c:8 [ 0:16] + check debris