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