DWARF is debug data. It is under appreciated. Debug data is a translation validation artifact. By design, it leaves breadcrumbs of how the low (assembly) code connects to the high (C) code.

Much of the information is currently nonrigorous, at a best effort by compilers writers for human debugger consumption. It could be better though.

“Where Did My Variable Go? Poking Holes in Incomplete Debug Information” https://arxiv.org/pdf/2211.09568.pdf is a really interesting paper on techniques to validate dwarf debug information. See the references and citations for more

Checking debug info dynamically is conceptually pretty straightforward. Devil in details though.

One approach is to compare -O0 execution/debug data with higher optimization levels using a debugger, running two binaries in sync. Presumably -O0 is the less likely to omit or incorrectly generate debug data.

You could also run an assembly program in a debugger in sync with a C interpreter (like https://github.com/kframework/c-semantics https://www.cl.cam.ac.uk/~pes20/cerberus/ https://www.reddit.com/r/ProgrammingLanguages/comments/hf441y/an_interpreter_for_c/ ). Set a breakpoint at every position the debug data should have an opinion and compare. Maybe throw a fuzzer on it.

These are all viable, but because of the particular hammer I’ve been forging, it makes sense to do this same process using CBMC, the C bounded model checker.

I’ve been working on a tool pcode2c which uses ghidra pcode lifting and generates a specialized C interpreter for that binary. In other words, static binary translation to C. This is not “decompilation” really, because I make zero effort to make readable idiomatic C, recover loops, recover types. All of that decreases the connection to the original binary.

Here is a baby C example from https://www.mimuw.edu.pl/~alx/konstruowanie/ACSL-by-Example.pdf It’s a function that takes in a size parameter, and checks if two arrays of that size are equal.

%%file /tmp/all_equal.c
#include <stdbool.h>
#include <assert.h>
bool equal(int n, int a[], int b[]){
    for(int i = 0; i < n; i++){
        if(a[i] != b[i]){
            return false;
        }
    }
    return true;
}

int main(){
    int a[10]; // = {42}; //calloc(10*sizeof(int));
    assert(equal(10, a, a));
}

Writing /tmp/all_equal.c
!gcc -Og -g -Wall -Wextra -std=c11 /tmp/all_equal.c -o /tmp/all_equal

We can take a peek at the assembly

!objdump -l -F -d /tmp/all_equal | grep -A 24 '001169 <equal>'
0000000000001169 <equal> (File Offset: 0x1169):
equal():
/tmp/all_equal.c:3
    1169: f3 0f 1e fa           endbr64 
/tmp/all_equal.c:4
    116d: b8 00 00 00 00        mov    $0x0,%eax
    1172: eb 03                 jmp    1177 <equal+0xe> (File Offset: 0x1177)
/tmp/all_equal.c:4 (discriminator 2)
    1174: 83 c0 01              add    $0x1,%eax
/tmp/all_equal.c:4 (discriminator 1)
    1177: 39 f8                 cmp    %edi,%eax
    1179: 7d 13                 jge    118e <equal+0x25> (File Offset: 0x118e)
/tmp/all_equal.c:5
    117b: 48 63 c8              movslq %eax,%rcx
    117e: 44 8b 04 8a           mov    (%rdx,%rcx,4),%r8d
    1182: 44 39 04 8e           cmp    %r8d,(%rsi,%rcx,4)
    1186: 74 ec                 je     1174 <equal+0xb> (File Offset: 0x1174)
/tmp/all_equal.c:6
    1188: b8 00 00 00 00        mov    $0x0,%eax
/tmp/all_equal.c:10
    118d: c3                    ret    
/tmp/all_equal.c:9
    118e: b8 01 00 00 00        mov    $0x1,%eax
    1193: c3                    ret    

A quick summary of the assembly:

  • The first arguments are in rdi,rsi,rdx. These are n a b respectively.
  • First the loop initializes by setting i in eax to 0. Then it jumps to the loop break check
  • 0x1177 compares i with n
  • The body of the loop is in 0x117b. It loads memory from a[i] intor8d and then compares it with with memory in b[i]`
  • A jump returns to loop top at 0x1174 where i in %eax is incremented if the are equal
  • Otherwise it returns false=0 in eax at 0x118d
  • If the loop is done it jumps from 0x1179 to 0x118e and returns 1 in %eax

I can dump this assembly out into a C interpreter using my pcode2c tool. You can see there is a very direct correspondence to the assembly (many C lines to 1 assembly line). There is a central switch-case that switches on the program counter and performs the pcode operations.

!python3 -m pcode2c /tmp/all_equal --start-address 0x1169 --file-offset 0x1169 --size 0x2b > /tmp/all_equal_pcode.c
!cat /tmp/all_equal_pcode.c
/* AUTOGENERATED. DO NOT EDIT. */
#include "_pcode.h"
void pcode2c(CPUState *state, size_t breakpoint){
    uint8_t* register_space = state->reg; 
    uint8_t* unique_space = state->unique; 
    uint8_t* ram_space = state->ram;
    uint8_t* ram = ram_space; // TODO: remove this
    for(;;){
    switch(state->pc){
        case 0x1169:
        L_0x1169ul:
            INSN(0x1169ul,"0x1169: ENDBR64 ")
        case 0x116d:
        L_0x116dul:
            INSN(0x116dul,"0x116d: MOV EAX,0x0")
            L_P_0x1: COPY(register_space + 0x0ul /* RAX */, 8ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x8ul);
        case 0x1172:
        L_0x1172ul:
            INSN(0x1172ul,"0x1172: JMP 0x1177")
            L_P_0x2: BRANCH_GOTO_TEMPFIX(ram_space, 0x1177ul, 8ul);
        case 0x1174:
        L_0x1174ul:
            INSN(0x1174ul,"0x1174: ADD EAX,0x1")
            L_P_0x3: INT_CARRY(register_space + 0x200ul /* CF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x4ul);
            L_P_0x4: INT_SCARRY(register_space + 0x20bul /* OF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x4ul);
            L_P_0x5: INT_ADD(register_space + 0x0ul /* EAX */, 4ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x4ul);
            L_P_0x6: INT_ZEXT(register_space + 0x0ul /* RAX */, 8ul, register_space + 0x0ul /* EAX */, 4ul);
            L_P_0x7: INT_SLESS(register_space + 0x207ul /* SF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x8: INT_EQUAL(register_space + 0x206ul /* ZF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x9: INT_AND(unique_space + 0x13180ul, 4ul, register_space + 0x0ul /* EAX */, 4ul, (uint8_t *)&(long unsigned int){0xfful}, 0x4ul);
            L_P_0xa: POPCOUNT(unique_space + 0x13200ul, 1ul, unique_space + 0x13180ul, 4ul);
            L_P_0xb: INT_AND(unique_space + 0x13280ul, 1ul, unique_space + 0x13200ul, 1ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x1ul);
            L_P_0xc: INT_EQUAL(register_space + 0x202ul /* PF */, 1ul, unique_space + 0x13280ul, 1ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x1ul);
        case 0x1177:
        L_0x1177ul:
            INSN(0x1177ul,"0x1177: CMP EAX,EDI")
            L_P_0xd: INT_LESS(register_space + 0x200ul /* CF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, register_space + 0x38ul /* EDI */, 4ul);
            L_P_0xe: INT_SBORROW(register_space + 0x20bul /* OF */, 1ul, register_space + 0x0ul /* EAX */, 4ul, register_space + 0x38ul /* EDI */, 4ul);
            L_P_0xf: INT_SUB(unique_space + 0x29700ul, 4ul, register_space + 0x0ul /* EAX */, 4ul, register_space + 0x38ul /* EDI */, 4ul);
            L_P_0x10: INT_SLESS(register_space + 0x207ul /* SF */, 1ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x11: INT_EQUAL(register_space + 0x206ul /* ZF */, 1ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x12: INT_AND(unique_space + 0x13180ul, 4ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0xfful}, 0x4ul);
            L_P_0x13: POPCOUNT(unique_space + 0x13200ul, 1ul, unique_space + 0x13180ul, 4ul);
            L_P_0x14: INT_AND(unique_space + 0x13280ul, 1ul, unique_space + 0x13200ul, 1ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x1ul);
            L_P_0x15: INT_EQUAL(register_space + 0x202ul /* PF */, 1ul, unique_space + 0x13280ul, 1ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x1ul);
        case 0x1179:
        L_0x1179ul:
            INSN(0x1179ul,"0x1179: JGE 0x118e")
            L_P_0x16: INT_EQUAL(unique_space + 0xcf80ul, 1ul, register_space + 0x20bul /* OF */, 1ul, register_space + 0x207ul /* SF */, 1ul);
            L_P_0x17: CBRANCH_GOTO_TEMPFIX(ram_space, 0x118eul, 8ul, unique_space, 0xcf80ul, 1ul);
        case 0x117b:
        L_0x117bul:
            INSN(0x117bul,"0x117b: MOVSXD RCX,EAX")
            L_P_0x18: INT_SEXT(register_space + 0x8ul /* RCX */, 8ul, register_space + 0x0ul /* EAX */, 4ul);
        case 0x117e:
        L_0x117eul:
            INSN(0x117eul,"0x117e: MOV R8D,dword ptr [RDX + RCX*0x4]")
            L_P_0x19: INT_MULT(unique_space + 0x3300ul, 8ul, register_space + 0x8ul /* RCX */, 8ul, (uint8_t *)&(long unsigned int){0x4ul}, 0x8ul);
            L_P_0x1a: INT_ADD(unique_space + 0x3400ul, 8ul, register_space + 0x10ul /* RDX */, 8ul, unique_space + 0x3300ul, 8ul);
            L_P_0x1b: LOAD(unique_space + 0xbf00ul, 4ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, unique_space + 0x3400ul, 8ul);
            L_P_0x1c: COPY(register_space + 0x80ul /* R8D */, 4ul, unique_space + 0xbf00ul, 4ul);
            L_P_0x1d: INT_ZEXT(register_space + 0x80ul /* R8 */, 8ul, register_space + 0x80ul /* R8D */, 4ul);
        case 0x1182:
        L_0x1182ul:
            INSN(0x1182ul,"0x1182: CMP dword ptr [RSI + RCX*0x4],R8D")
            L_P_0x1e: INT_MULT(unique_space + 0x3300ul, 8ul, register_space + 0x8ul /* RCX */, 8ul, (uint8_t *)&(long unsigned int){0x4ul}, 0x8ul);
            L_P_0x1f: INT_ADD(unique_space + 0x3400ul, 8ul, register_space + 0x30ul /* RSI */, 8ul, unique_space + 0x3300ul, 8ul);
            L_P_0x20: LOAD(unique_space + 0xbf00ul, 4ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, unique_space + 0x3400ul, 8ul);
            L_P_0x21: INT_LESS(register_space + 0x200ul /* CF */, 1ul, unique_space + 0xbf00ul, 4ul, register_space + 0x80ul /* R8D */, 4ul);
            L_P_0x22: LOAD(unique_space + 0xbf00ul, 4ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, unique_space + 0x3400ul, 8ul);
            L_P_0x23: INT_SBORROW(register_space + 0x20bul /* OF */, 1ul, unique_space + 0xbf00ul, 4ul, register_space + 0x80ul /* R8D */, 4ul);
            L_P_0x24: LOAD(unique_space + 0xbf00ul, 4ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, unique_space + 0x3400ul, 8ul);
            L_P_0x25: INT_SUB(unique_space + 0x29700ul, 4ul, unique_space + 0xbf00ul, 4ul, register_space + 0x80ul /* R8D */, 4ul);
            L_P_0x26: INT_SLESS(register_space + 0x207ul /* SF */, 1ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x27: INT_EQUAL(register_space + 0x206ul /* ZF */, 1ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x4ul);
            L_P_0x28: INT_AND(unique_space + 0x13180ul, 4ul, unique_space + 0x29700ul, 4ul, (uint8_t *)&(long unsigned int){0xfful}, 0x4ul);
            L_P_0x29: POPCOUNT(unique_space + 0x13200ul, 1ul, unique_space + 0x13180ul, 4ul);
            L_P_0x2a: INT_AND(unique_space + 0x13280ul, 1ul, unique_space + 0x13200ul, 1ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x1ul);
            L_P_0x2b: INT_EQUAL(register_space + 0x202ul /* PF */, 1ul, unique_space + 0x13280ul, 1ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x1ul);
        case 0x1186:
        L_0x1186ul:
            INSN(0x1186ul,"0x1186: JZ 0x1174")
            L_P_0x2c: CBRANCH_GOTO_TEMPFIX(ram_space, 0x1174ul, 8ul, register_space, 0x206ul /* ZF */, 1ul);
        case 0x1188:
        L_0x1188ul:
            INSN(0x1188ul,"0x1188: MOV EAX,0x0")
            L_P_0x2d: COPY(register_space + 0x0ul /* RAX */, 8ul, (uint8_t *)&(long unsigned int){0x0ul}, 0x8ul);
        case 0x118d:
        L_0x118dul:
            INSN(0x118dul,"0x118d: RET ")
            L_P_0x2e: LOAD(register_space + 0x288ul /* RIP */, 8ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, register_space + 0x20ul /* RSP */, 8ul);
            L_P_0x2f: INT_ADD(register_space + 0x20ul /* RSP */, 8ul, register_space + 0x20ul /* RSP */, 8ul, (uint8_t *)&(long unsigned int){0x8ul}, 0x8ul);
            L_P_0x30: RETURN(register_space + 0x288ul /* RIP */, 8ul);
        case 0x118e:
        L_0x118eul:
            INSN(0x118eul,"0x118e: MOV EAX,0x1")
            L_P_0x31: COPY(register_space + 0x0ul /* RAX */, 8ul, (uint8_t *)&(long unsigned int){0x1ul}, 0x8ul);
        case 0x1193:
        L_0x1193ul:
            INSN(0x1193ul,"0x1193: RET ")
            L_P_0x32: LOAD(register_space + 0x288ul /* RIP */, 8ul, (uint8_t *)&(long unsigned int){0x580b8e69e1c0ul}, 0x8ul, register_space + 0x20ul /* RSP */, 8ul);
            L_P_0x33: INT_ADD(register_space + 0x20ul /* RSP */, 8ul, register_space + 0x20ul /* RSP */, 8ul, (uint8_t *)&(long unsigned int){0x8ul}, 0x8ul);
            L_P_0x34: RETURN(register_space + 0x288ul /* RIP */, 8ul);
        default: assert(state->pc != -1); // Unexpected PC value
}}}

We can compile using gcc, or run through cbmc or AFL or what have you.

It requires some harness setup to do anything with it though. We need to allocate memory for ram, registers, and temporary values. This is handled in the init_CPUState library function.

We set state.pc to 0x1169 to go to the entrypoint of the all_equal. We can also set some registers. The x86.h header file is autogenerated and has define pcode register offsets for the architecture.

pcode2c(&state,-1); runs the interpreter without a breakpoint set. It is currently setup to return at every CALL or RETURN pcode instruction. In this case, it returns at the end of the function.

%%file /tmp/harness.c
#include "all_equal_pcode.c"
#include "x86.h"
#include <stdlib.h>

int main() {
  CPUState state;
  init_CPUState(&state);

  // Initialize state here, including pc address.
  state.pc = 0x1169;

  memset(state.reg + RDI, 1, 8); // n 
  memset(state.reg + RSI, 64, 8); // a
  memset(state.reg + RDX, 64, 8); // b
  memset(state.reg + RCX, 0, 8);
  memset(state.reg + RAX, 0, 8);
  memset(state.reg + RSP, 0, 8);

  pcode2c(&state, -1); // Run decompiled function
  printf("RAX: %ld\n", *(uint64_t *)(state.reg + RAX));
  __CPROVER_printf("RAX: %ld\n", *(uint64_t *)(state.reg + RAX));
  assert(*(uint8_t *)(state.reg + RAX) != 0);

  return 0;
}

Because I exported debug data with -g when I called gcc, there is useful translation validation data in the debug section. Let’s take a look at the big dump. I put most of it at the end of the post

!objdump -W /tmp/all_equal
/tmp/all_equal:     file format elf64-x86-64

Contents of the .eh_frame section:


00000000 0000000000000014 00000000 CIE
  Version:               1
  Augmentation:          "zR"
  Code alignment factor: 1
  Data alignment factor: -8
  Return address column: 16
  Augmentation data:     1b
  DW_CFA_def_cfa: r7 (rsp) ofs 8
  DW_CFA_offset: r16 (rip) at cfa-8
  DW_CFA_nop
  DW_CFA_nop

  ....

Let’s point out some interesting stuff in particular


 <2><16d>: Abbrev Number: 4 (DW_TAG_formal_parameter)
    <16e>   DW_AT_name        : n
    <170>   DW_AT_decl_file   : 1
    <170>   DW_AT_decl_line   : 3
    <170>   DW_AT_decl_column : 16
    <171>   DW_AT_type        : <0x118>
    <175>   DW_AT_location    : 1 byte block: 55        (DW_OP_reg5 (rdi))
 <2><177>: Abbrev Number: 4 (DW_TAG_formal_parameter)
    <178>   DW_AT_name        : a
    <17a>   DW_AT_decl_file   : 1
    <17a>   DW_AT_decl_line   : 3
    <17a>   DW_AT_decl_column : 23
    <17b>   DW_AT_type        : <0x1ab>
    <17f>   DW_AT_location    : 1 byte block: 54        (DW_OP_reg4 (rsi))
 <2><181>: Abbrev Number: 4 (DW_TAG_formal_parameter)
    <182>   DW_AT_name        : b
    <184>   DW_AT_decl_file   : 1
    <184>   DW_AT_decl_line   : 3
    <184>   DW_AT_decl_column : 32
    <185>   DW_AT_type        : <0x1ab>
    <189>   DW_AT_location    : 1 byte block: 51        (DW_OP_reg1 (rdx))

These entries say that the parameters to the function are in rdi, rsi rdx, but we already expected that from the calling conventions.

More interesting is i


 <3><190>: Abbrev Number: 19 (DW_TAG_variable)
    <191>   DW_AT_name        : i
    <193>   DW_AT_decl_file   : 1
    <194>   DW_AT_decl_line   : 4
    <195>   DW_AT_decl_column : 13
    <196>   DW_AT_type        : <0x118>
    <19a>   DW_AT_location    : 0x14 (location list)
    <19e>   DW_AT_GNU_locviews: 0xc

In the .debug_loclists section we can see


    Offset   Begin            End              Expression
    00000014 v000000000000002 v000000000000000 views at 0000000c for:
             000000000000116d 0000000000001174 (DW_OP_lit0; DW_OP_stack_value)
    0000001a v000000000000000 v000000000000000 views at 0000000e for:
             0000000000001174 000000000000118d (DW_OP_reg0 (rax))
    0000001f v000000000000000 v000000000000000 views at 00000010 for:
             000000000000118d 000000000000118e (DW_OP_reg2 (rcx))
    00000024 v000000000000000 v000000000000000 views at 00000012 for:
             000000000000118e 0000000000001193 (DW_OP_reg0 (rax))

Indeed looking at the assembly, these chunks correspond to pieces of the for loop, incrementing i by 1. We also use i to index into the arrays and it is temporarily see that it is copied over to rcx at addresses 0x117e to 0x1182

I don’t know what it is getting at with the DW_OP_stack_value code. i is never on the stack in any obvious sense. Perhaps I need to dig into the DWARF spec of perhaps this is nonsense.


/tmp/all_equal.c:4 (discriminator 2)
    1174: 83 c0 01              add    $0x1,%eax
/tmp/all_equal.c:4 (discriminator 1)
    1177: 39 f8                 cmp    %edi,%eax
    1179: 7d 13                 jge    118e <equal+0x25> (File Offset: 0x118e)

The addr2line command line program can map addresses to lines using this dwarf information. The table itself is bit tough to read. It’s a compact representation. I already put some flags on the objdump above.

!addr2line -a -e /tmp/all_equal 0x1169 0x1174 0x1186 0x1188
0x0000000000001169
/tmp/all_equal.c:3
0x0000000000001174
/tmp/all_equal.c:4 (discriminator 2)
0x0000000000001186
/tmp/all_equal.c:5
0x0000000000001188
/tmp/all_equal.c:6

Ok, so how can we use this to perform translation validation?

Well, I can annotate my original function with calls to the interpreter. By setting breakpoint addresses and then asserting that variables are in the appropriate level locations.

One typically annoying thing is that DWARf annotates with respect to syntactic positions. The line table can encode line and column information in the source, which is nice because it is highly generic with respect to language, but obviously a bummer because it can be very unclear semantically what a particular syntactic position corresponds to.

It is kind of cool though that also if I want to annotate the original source, it is in principle a very easy syntactic insertion. I’ve been writing a tool to do this but have lost steam on doing so, so I think it is best to just get the idea out the showing how this can be done manually.

Basically, I’d want my pcode2c.dwarf_annot tool to do something like this:

%%file /tmp/all_equal_debug.c
#include <assert.h>
#include <stdbool.h>
bool equal(int n, int a[], int b[]) {
  for (int i = 0; i < n; i++) {

    pcode2c(&state, 0x117b);
    assert(i == state.reg[RAX]);
    pcode2c(&state, 0x117e); //continue
    
    if (a[i] != b[i]) {
      return false;
    }
  }
  return true;
}

While I could write dwarf_annot to get this started, I would anticipate it being loosy goosy enough toi need hand tweaking.

The basic idea though is this:

  • For every line table entry, insert a call to pcode2c(&state , addr ); at the syntactic position stated by the line table
  • At these positions, if we fall in the loclist range of a dwarf annotated DW_TAG_variable, output an assertion that the C variable has the same contents as the DWARF expression describing where it should be (DW_OP_reg0 (rax) for example)

Bits and Bobbles

This post is almost more aspirational than true. I think the basic vision makes sense but I have a hard time getting cbmc to run on these examples.

I’m running out of motivation on pcode2c. There is a huge hill of getting the semantics tighter, improving usability (reducing harness code needed), increasing scale. A constant fear is CBMC not scaling. It does ok on small stuff.

The big “killer” application of this was supposed to be micropatching. You need to verify the locations of variables internal to a function if you want to hijack them with a trustworthy tiny pacth.

It is pretty nice having a hackable little interpreter you can toss print statements and whatnot into.

CBMC got some more printf support which was crucial for me to interpret their counterexample traces. I grep out the printf statements from the rest

Maybe make a standalone pcode interpreter? Ghidra has an interpreter and maybe I should work on pulling it out. It’s a C++ thing. I feel like mine is more direct, but so what.

It is a confusing thing, because debug info is not guaranteed. And yet if it is possible to generate it, the compiler should.

It’d be cool to do ghidra plays mario usjing pcode2c https://github.com/nevesnunes/ghidra-plays-mario

There could be a more self contained “asmbmc”. I didn’t do this for two reasons

  • I wanted to be decoupled from specifically cbmc’s IR. I haven’t really moved beyond cbmc though. It is not the obvious top contender in the SVComp
  • I wanted the flexibility to control the interpreter from C and run it through gcc
  • I wanted to compare against C implementations of the same function as “spec”

PCode2C pt 2: DWARF Verification via Ghidra and CBMC

Comparative verification is a really useful paradigm

  • Spec writing. It is easier for users to grok that you are compring two programs rather than bringing in a complicated logic.
  • Comper correctness

My basic model of what a dwarf correctness property is is that it should be specifying optionally observable effects.

{impl_defined} -> State -> Option State {impl_defined} -> Interaction type Interaction = Out Value interaction | Input (Value -> interaction)

type compiler = prog1 : HighCode -> (prog2 : LowCode, exec_high prog1 ~ exec_low prog2)

What is ~ though? Effects

Objdump Dwarf dump

    
    00000018 0000000000000014 0000001c FDE cie=00000000 pc=0000000000001080..00000000000010a6
      DW_CFA_advance_loc: 4 to 0000000000001084
      DW_CFA_undefined: r16 (rip)
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
    
    00000030 0000000000000024 00000034 FDE cie=00000000 pc=0000000000001020..0000000000001050
      DW_CFA_def_cfa_offset: 16
      DW_CFA_advance_loc: 6 to 0000000000001026
      DW_CFA_def_cfa_offset: 24
      DW_CFA_advance_loc: 10 to 0000000000001030
      DW_CFA_def_cfa_expression (DW_OP_breg7 (rsp): 8; DW_OP_breg16 (rip): 0; DW_OP_lit15; DW_OP_and; DW_OP_lit10; DW_OP_ge; DW_OP_lit3; DW_OP_shl; DW_OP_plus)
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
    
    00000058 0000000000000014 0000005c FDE cie=00000000 pc=0000000000001050..0000000000001060
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
    
    00000070 0000000000000014 00000074 FDE cie=00000000 pc=0000000000001060..0000000000001080
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
    
    00000088 0000000000000010 0000008c FDE cie=00000000 pc=0000000000001169..0000000000001194
      DW_CFA_nop
      DW_CFA_nop
      DW_CFA_nop
    
    0000009c 0000000000000018 000000a0 FDE cie=00000000 pc=0000000000001194..00000000000011fe
      DW_CFA_advance_loc: 8 to 000000000000119c
      DW_CFA_def_cfa_offset: 64
      DW_CFA_advance_loc: 61 to 00000000000011d9
      DW_CFA_remember_state
      DW_CFA_def_cfa_offset: 8
      DW_CFA_advance_loc: 1 to 00000000000011da
      DW_CFA_restore_state
      DW_CFA_nop
      DW_CFA_nop
    
    000000b8 ZERO terminator
    
    
    Contents of the .debug_aranges section:
    
      Length:                   44
      Version:                  2
      Offset into .debug_info:  0x0
      Pointer Size:             8
      Segment Size:             0
    
        Address            Length
        0000000000001169 0000000000000095 
        0000000000000000 0000000000000000 
    
    Contents of the .debug_info section:
    
      Compilation Unit @ offset 0x0:
       Length:        0x1b6 (32-bit)
       Version:       5
       Unit Type:     DW_UT_compile (1)
       Abbrev Offset: 0x0
       Pointer Size:  8
     <0><c>: Abbrev Number: 10 (DW_TAG_compile_unit)
        <d>   DW_AT_producer    : (indirect string, offset: 0x50): GNU C11 11.4.0 -mtune=generic -march=x86-64 -g -Og -std=c11 -fasynchronous-unwind-tables -fstack-protector-strong -fstack-clash-protection -fcf-protection
        <11>   DW_AT_language    : 29 (C11)
        <12>   DW_AT_name        : (indirect line string, offset: 0x2a): /tmp/all_equal.c
        <16>   DW_AT_comp_dir    : (indirect line string, offset: 0x0): /home/philip/philzook58.github.io/_drafts
        <1a>   DW_AT_low_pc      : 0x1169
        <22>   DW_AT_high_pc     : 0x95
        <2a>   DW_AT_stmt_list   : 0x0
     <1><2e>: Abbrev Number: 11 (DW_TAG_subprogram)
        <2f>   DW_AT_external    : 1
        <2f>   DW_AT_name        : (indirect string, offset: 0x42): __assert_fail
        <33>   DW_AT_decl_file   : 2
        <34>   DW_AT_decl_line   : 69
        <35>   DW_AT_decl_column : 13
        <36>   DW_AT_prototyped  : 1
        <36>   DW_AT_noreturn    : 1
        <36>   DW_AT_declaration : 1
        <36>   DW_AT_sibling     : <0x4f>
     <2><3a>: Abbrev Number: 2 (DW_TAG_formal_parameter)
        <3b>   DW_AT_type        : <0x4f>
     <2><3f>: Abbrev Number: 2 (DW_TAG_formal_parameter)
        <40>   DW_AT_type        : <0x4f>
     <2><44>: Abbrev Number: 2 (DW_TAG_formal_parameter)
        <45>   DW_AT_type        : <0x60>
     <2><49>: Abbrev Number: 2 (DW_TAG_formal_parameter)
        <4a>   DW_AT_type        : <0x4f>
     <2><4e>: Abbrev Number: 0
     <1><4f>: Abbrev Number: 5 (DW_TAG_pointer_type)
        <50>   DW_AT_byte_size   : 8
        <50>   DW_AT_type        : <0x5b>
     <1><54>: Abbrev Number: 3 (DW_TAG_base_type)
        <55>   DW_AT_byte_size   : 1
        <56>   DW_AT_encoding    : 6 (signed char)
        <57>   DW_AT_name        : (indirect string, offset: 0xeb): char
     <1><5b>: Abbrev Number: 6 (DW_TAG_const_type)
        <5c>   DW_AT_type        : <0x54>
     <1><60>: Abbrev Number: 3 (DW_TAG_base_type)
        <61>   DW_AT_byte_size   : 4
        <62>   DW_AT_encoding    : 7 (unsigned)
        <63>   DW_AT_name        : (indirect string, offset: 0x5): unsigned int
     <1><67>: Abbrev Number: 12 (DW_TAG_subprogram)
        <68>   DW_AT_external    : 1
        <68>   DW_AT_name        : (indirect string, offset: 0x3d): main
        <6c>   DW_AT_decl_file   : 1
        <6d>   DW_AT_decl_line   : 12
        <6e>   DW_AT_decl_column : 5
        <6f>   DW_AT_type        : <0x118>
        <73>   DW_AT_low_pc      : 0x1194
        <7b>   DW_AT_high_pc     : 0x6a
        <83>   DW_AT_frame_base  : 1 byte block: 9c  (DW_OP_call_frame_cfa)
        <85>   DW_AT_call_all_calls: 1
        <85>   DW_AT_sibling     : <0x118>
     <2><89>: Abbrev Number: 13 (DW_TAG_variable)
        <8a>   DW_AT_name        : a
        <8c>   DW_AT_decl_file   : 1
        <8d>   DW_AT_decl_line   : 13
        <8e>   DW_AT_decl_column : 9
        <8f>   DW_AT_type        : <0x11f>
        <93>   DW_AT_location    : 2 byte block: 91 40  (DW_OP_fbreg: -64)
     <2><96>: Abbrev Number: 14 (DW_TAG_variable)
        <97>   DW_AT_name        : (indirect string, offset: 0x23): __PRETTY_FUNCTION__
        <9b>   DW_AT_type        : <0x146>
        <9f>   DW_AT_artificial  : 1
        <9f>   DW_AT_location    : 9 byte block: 3 25 20 0 0 0 0 0 0  (DW_OP_addr: 2025)
     <2><a9>: Abbrev Number: 7 (DW_TAG_call_site)
        <aa>   DW_AT_call_return_pc: 0x11bc
        <b2>   DW_AT_call_origin : <0x14b>
        <b6>   DW_AT_sibling     : <0xcc>
     <3><ba>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <bb>   DW_AT_location    : 1 byte block: 55  (DW_OP_reg5 (rdi))
        <bd>   DW_AT_call_value  : 1 byte block: 3a  (DW_OP_lit10)
     <3><bf>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <c0>   DW_AT_location    : 1 byte block: 54  (DW_OP_reg4 (rsi))
        <c2>   DW_AT_call_value  : 2 byte block: 91 40  (DW_OP_fbreg: -64)
     <3><c5>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <c6>   DW_AT_location    : 1 byte block: 51  (DW_OP_reg1 (rdx))
        <c8>   DW_AT_call_value  : 2 byte block: 91 40  (DW_OP_fbreg: -64)
     <3><cb>: Abbrev Number: 0
     <2><cc>: Abbrev Number: 7 (DW_TAG_call_site)
        <cd>   DW_AT_call_return_pc: 0x11f9
        <d5>   DW_AT_call_origin : <0x2e>
        <d9>   DW_AT_sibling     : <0x10a>
     <3><dd>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <de>   DW_AT_location    : 1 byte block: 55  (DW_OP_reg5 (rdi))
        <e0>   DW_AT_call_value  : 9 byte block: 3 15 20 0 0 0 0 0 0  (DW_OP_addr: 2015)
     <3><ea>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <eb>   DW_AT_location    : 1 byte block: 54  (DW_OP_reg4 (rsi))
        <ed>   DW_AT_call_value  : 9 byte block: 3 4 20 0 0 0 0 0 0  (DW_OP_addr: 2004)
     <3><f7>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <f8>   DW_AT_location    : 1 byte block: 51  (DW_OP_reg1 (rdx))
        <fa>   DW_AT_call_value  : 1 byte block: 3e  (DW_OP_lit14)
     <3><fc>: Abbrev Number: 1 (DW_TAG_call_site_parameter)
        <fd>   DW_AT_location    : 1 byte block: 52  (DW_OP_reg2 (rcx))
        <ff>   DW_AT_call_value  : 9 byte block: 3 25 20 0 0 0 0 0 0  (DW_OP_addr: 2025)
     <3><109>: Abbrev Number: 0
     <2><10a>: Abbrev Number: 15 (DW_TAG_call_site)
        <10b>   DW_AT_call_return_pc: 0x11fe
        <113>   DW_AT_call_origin : <0x1b0>
     <2><117>: Abbrev Number: 0
     <1><118>: Abbrev Number: 16 (DW_TAG_base_type)
        <119>   DW_AT_byte_size   : 4
        <11a>   DW_AT_encoding    : 5 (signed)
        <11b>   DW_AT_name        : int
     <1><11f>: Abbrev Number: 8 (DW_TAG_array_type)
        <120>   DW_AT_type        : <0x118>
        <124>   DW_AT_sibling     : <0x12f>
     <2><128>: Abbrev Number: 9 (DW_TAG_subrange_type)
        <129>   DW_AT_type        : <0x12f>
        <12d>   DW_AT_upper_bound : 9
     <2><12e>: Abbrev Number: 0
     <1><12f>: Abbrev Number: 3 (DW_TAG_base_type)
        <130>   DW_AT_byte_size   : 8
        <131>   DW_AT_encoding    : 7 (unsigned)
        <132>   DW_AT_name        : (indirect string, offset: 0x0): long unsigned int
     <1><136>: Abbrev Number: 8 (DW_TAG_array_type)
        <137>   DW_AT_type        : <0x5b>
        <13b>   DW_AT_sibling     : <0x146>
     <2><13f>: Abbrev Number: 9 (DW_TAG_subrange_type)
        <140>   DW_AT_type        : <0x12f>
        <144>   DW_AT_upper_bound : 4
     <2><145>: Abbrev Number: 0
     <1><146>: Abbrev Number: 6 (DW_TAG_const_type)
        <147>   DW_AT_type        : <0x136>
     <1><14b>: Abbrev Number: 17 (DW_TAG_subprogram)
        <14c>   DW_AT_external    : 1
        <14c>   DW_AT_name        : (indirect string, offset: 0x37): equal
        <150>   DW_AT_decl_file   : 1
        <151>   DW_AT_decl_line   : 3
        <152>   DW_AT_decl_column : 6
        <153>   DW_AT_prototyped  : 1
        <153>   DW_AT_type        : <0x1a4>
        <157>   DW_AT_low_pc      : 0x1169
        <15f>   DW_AT_high_pc     : 0x2b
        <167>   DW_AT_frame_base  : 1 byte block: 9c  (DW_OP_call_frame_cfa)
        <169>   DW_AT_call_all_calls: 1
        <169>   DW_AT_sibling     : <0x1a4>
     <2><16d>: Abbrev Number: 4 (DW_TAG_formal_parameter)
        <16e>   DW_AT_name        : n
        <170>   DW_AT_decl_file   : 1
        <170>   DW_AT_decl_line   : 3
        <170>   DW_AT_decl_column : 16
        <171>   DW_AT_type        : <0x118>
        <175>   DW_AT_location    : 1 byte block: 55  (DW_OP_reg5 (rdi))
     <2><177>: Abbrev Number: 4 (DW_TAG_formal_parameter)
        <178>   DW_AT_name        : a
        <17a>   DW_AT_decl_file   : 1
        <17a>   DW_AT_decl_line   : 3
        <17a>   DW_AT_decl_column : 23
        <17b>   DW_AT_type        : <0x1ab>
        <17f>   DW_AT_location    : 1 byte block: 54  (DW_OP_reg4 (rsi))
     <2><181>: Abbrev Number: 4 (DW_TAG_formal_parameter)
        <182>   DW_AT_name        : b
        <184>   DW_AT_decl_file   : 1
        <184>   DW_AT_decl_line   : 3
        <184>   DW_AT_decl_column : 32
        <185>   DW_AT_type        : <0x1ab>
        <189>   DW_AT_location    : 1 byte block: 51  (DW_OP_reg1 (rdx))
     <2><18b>: Abbrev Number: 18 (DW_TAG_lexical_block)
        <18c>   DW_AT_ranges      : 0xc
     <3><190>: Abbrev Number: 19 (DW_TAG_variable)
        <191>   DW_AT_name        : i
        <193>   DW_AT_decl_file   : 1
        <194>   DW_AT_decl_line   : 4
        <195>   DW_AT_decl_column : 13
        <196>   DW_AT_type        : <0x118>
        <19a>   DW_AT_location    : 0x14 (location list)
        <19e>   DW_AT_GNU_locviews: 0xc
     <3><1a2>: Abbrev Number: 0
     <2><1a3>: Abbrev Number: 0
     <1><1a4>: Abbrev Number: 3 (DW_TAG_base_type)
        <1a5>   DW_AT_byte_size   : 1
        <1a6>   DW_AT_encoding    : 2 (boolean)
        <1a7>   DW_AT_name        : (indirect string, offset: 0xf0): _Bool
     <1><1ab>: Abbrev Number: 5 (DW_TAG_pointer_type)
        <1ac>   DW_AT_byte_size   : 8
        <1ac>   DW_AT_type        : <0x118>
     <1><1b0>: Abbrev Number: 20 (DW_TAG_subprogram)
        <1b1>   DW_AT_external    : 1
        <1b1>   DW_AT_declaration : 1
        <1b1>   DW_AT_linkage_name: (indirect string, offset: 0x12): __stack_chk_fail
        <1b5>   DW_AT_name        : (indirect string, offset: 0x12): __stack_chk_fail
     <1><1b9>: Abbrev Number: 0
    
    Contents of the .debug_abbrev section:
    
      Number TAG (0x0)
       1      DW_TAG_call_site_parameter    [no children]
        DW_AT_location     DW_FORM_exprloc
        DW_AT_call_value   DW_FORM_exprloc
        DW_AT value: 0     DW_FORM value: 0
       2      DW_TAG_formal_parameter    [no children]
        DW_AT_type         DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       3      DW_TAG_base_type    [no children]
        DW_AT_byte_size    DW_FORM_data1
        DW_AT_encoding     DW_FORM_data1
        DW_AT_name         DW_FORM_strp
        DW_AT value: 0     DW_FORM value: 0
       4      DW_TAG_formal_parameter    [no children]
        DW_AT_name         DW_FORM_string
        DW_AT_decl_file    DW_FORM_implicit_const: 1
        DW_AT_decl_line    DW_FORM_implicit_const: 3
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_type         DW_FORM_ref4
        DW_AT_location     DW_FORM_exprloc
        DW_AT value: 0     DW_FORM value: 0
       5      DW_TAG_pointer_type    [no children]
        DW_AT_byte_size    DW_FORM_implicit_const: 8
        DW_AT_type         DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       6      DW_TAG_const_type    [no children]
        DW_AT_type         DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       7      DW_TAG_call_site    [has children]
        DW_AT_call_return_pc DW_FORM_addr
        DW_AT_call_origin  DW_FORM_ref4
        DW_AT_sibling      DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       8      DW_TAG_array_type    [has children]
        DW_AT_type         DW_FORM_ref4
        DW_AT_sibling      DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       9      DW_TAG_subrange_type    [no children]
        DW_AT_type         DW_FORM_ref4
        DW_AT_upper_bound  DW_FORM_data1
        DW_AT value: 0     DW_FORM value: 0
       10      DW_TAG_compile_unit    [has children]
        DW_AT_producer     DW_FORM_strp
        DW_AT_language     DW_FORM_data1
        DW_AT_name         DW_FORM_line_strp
        DW_AT_comp_dir     DW_FORM_line_strp
        DW_AT_low_pc       DW_FORM_addr
        DW_AT_high_pc      DW_FORM_data8
        DW_AT_stmt_list    DW_FORM_sec_offset
        DW_AT value: 0     DW_FORM value: 0
       11      DW_TAG_subprogram    [has children]
        DW_AT_external     DW_FORM_flag_present
        DW_AT_name         DW_FORM_strp
        DW_AT_decl_file    DW_FORM_data1
        DW_AT_decl_line    DW_FORM_data1
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_prototyped   DW_FORM_flag_present
        DW_AT_noreturn     DW_FORM_flag_present
        DW_AT_declaration  DW_FORM_flag_present
        DW_AT_sibling      DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       12      DW_TAG_subprogram    [has children]
        DW_AT_external     DW_FORM_flag_present
        DW_AT_name         DW_FORM_strp
        DW_AT_decl_file    DW_FORM_data1
        DW_AT_decl_line    DW_FORM_data1
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_type         DW_FORM_ref4
        DW_AT_low_pc       DW_FORM_addr
        DW_AT_high_pc      DW_FORM_data8
        DW_AT_frame_base   DW_FORM_exprloc
        DW_AT_call_all_calls DW_FORM_flag_present
        DW_AT_sibling      DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       13      DW_TAG_variable    [no children]
        DW_AT_name         DW_FORM_string
        DW_AT_decl_file    DW_FORM_data1
        DW_AT_decl_line    DW_FORM_data1
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_type         DW_FORM_ref4
        DW_AT_location     DW_FORM_exprloc
        DW_AT value: 0     DW_FORM value: 0
       14      DW_TAG_variable    [no children]
        DW_AT_name         DW_FORM_strp
        DW_AT_type         DW_FORM_ref4
        DW_AT_artificial   DW_FORM_flag_present
        DW_AT_location     DW_FORM_exprloc
        DW_AT value: 0     DW_FORM value: 0
       15      DW_TAG_call_site    [no children]
        DW_AT_call_return_pc DW_FORM_addr
        DW_AT_call_origin  DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       16      DW_TAG_base_type    [no children]
        DW_AT_byte_size    DW_FORM_data1
        DW_AT_encoding     DW_FORM_data1
        DW_AT_name         DW_FORM_string
        DW_AT value: 0     DW_FORM value: 0
       17      DW_TAG_subprogram    [has children]
        DW_AT_external     DW_FORM_flag_present
        DW_AT_name         DW_FORM_strp
        DW_AT_decl_file    DW_FORM_data1
        DW_AT_decl_line    DW_FORM_data1
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_prototyped   DW_FORM_flag_present
        DW_AT_type         DW_FORM_ref4
        DW_AT_low_pc       DW_FORM_addr
        DW_AT_high_pc      DW_FORM_data8
        DW_AT_frame_base   DW_FORM_exprloc
        DW_AT_call_all_calls DW_FORM_flag_present
        DW_AT_sibling      DW_FORM_ref4
        DW_AT value: 0     DW_FORM value: 0
       18      DW_TAG_lexical_block    [has children]
        DW_AT_ranges       DW_FORM_sec_offset
        DW_AT value: 0     DW_FORM value: 0
       19      DW_TAG_variable    [no children]
        DW_AT_name         DW_FORM_string
        DW_AT_decl_file    DW_FORM_data1
        DW_AT_decl_line    DW_FORM_data1
        DW_AT_decl_column  DW_FORM_data1
        DW_AT_type         DW_FORM_ref4
        DW_AT_location     DW_FORM_sec_offset
        DW_AT_GNU_locviews DW_FORM_sec_offset
        DW_AT value: 0     DW_FORM value: 0
       20      DW_TAG_subprogram    [no children]
        DW_AT_external     DW_FORM_flag_present
        DW_AT_declaration  DW_FORM_flag_present
        DW_AT_linkage_name DW_FORM_strp
        DW_AT_name         DW_FORM_strp
        DW_AT value: 0     DW_FORM value: 0
    
    Raw dump of debug contents of section .debug_line:
    
      Offset:                      0x0
      Length:                      162
      DWARF Version:               5
      Address size (bytes):        8
      Segment selector (bytes):    0
      Prologue Length:             55
      Minimum Instruction Length:  1
      Maximum Ops per Instruction: 1
      Initial value of 'is_stmt':  1
      Line Base:                   -5
      Line Range:                  14
      Opcode Base:                 13
    
     Opcodes:
      Opcode 1 has 0 args
      Opcode 2 has 1 arg
      Opcode 3 has 1 arg
      Opcode 4 has 1 arg
      Opcode 5 has 1 arg
      Opcode 6 has 0 args
      Opcode 7 has 0 args
      Opcode 8 has 0 args
      Opcode 9 has 1 arg
      Opcode 10 has 0 args
      Opcode 11 has 0 args
      Opcode 12 has 1 arg
    
     The Directory Table (offset 0x22, lines 3, columns 1):
      Entry Name
      0 (indirect line string, offset: 0x0): /home/philip/philzook58.github.io/_drafts
      1 (indirect line string, offset: 0x3b): /tmp
      2 (indirect line string, offset: 0x40): /usr/include
    
     The File Name Table (offset 0x34, lines 3, columns 2):
      Entry Dir Name
      0 1 (indirect line string, offset: 0x2f): all_equal.c
      1 1 (indirect line string, offset: 0x2f): all_equal.c
      2 2 (indirect line string, offset: 0x4d): assert.h
    
     Line Number Statements:
      [0x00000043]  Set column to 36
      [0x00000045]  Extended opcode 2: set Address to 0x1169
      [0x00000050]  Special opcode 7: advance Address by 0 to 0x1169 and Line by 2 to 3
      [0x00000051]  Set is_stmt to 0
      [0x00000052]  Copy (view 1)
      [0x00000053]  Set column to 5
      [0x00000055]  Set is_stmt to 1
      [0x00000056]  Special opcode 62: advance Address by 4 to 0x116d and Line by 1 to 4
      [0x00000057]  Set column to 9
      [0x00000059]  Copy (view 1)
      [0x0000005a]  Set column to 13
      [0x0000005c]  Set is_stmt to 0
      [0x0000005d]  Copy (view 2)
      [0x0000005e]  Set column to 5
      [0x00000060]  Special opcode 75: advance Address by 5 to 0x1172 and Line by 0 to 4
      [0x00000061]  Set column to 28
      [0x00000063]  Extended opcode 4: set Discriminator to 2
      [0x00000067]  Set is_stmt to 1
      [0x00000068]  Special opcode 33: advance Address by 2 to 0x1174 and Line by 0 to 4
      [0x00000069]  Set column to 22
      [0x0000006b]  Extended opcode 4: set Discriminator to 1
      [0x0000006f]  Special opcode 47: advance Address by 3 to 0x1177 and Line by 0 to 4
      [0x00000070]  Set column to 9
      [0x00000072]  Special opcode 62: advance Address by 4 to 0x117b and Line by 1 to 5
      [0x00000073]  Set column to 13
      [0x00000075]  Set is_stmt to 0
      [0x00000076]  Copy (view 1)
      [0x00000077]  Set column to 11
      [0x00000079]  Special opcode 47: advance Address by 3 to 0x117e and Line by 0 to 5
      [0x0000007a]  Set column to 20
      [0x0000007c]  Special opcode 146: advance Address by 10 to 0x1188 and Line by 1 to 6
      [0x0000007d]  Special opcode 75: advance Address by 5 to 0x118d and Line by 0 to 6
      [0x0000007e]  Set column to 1
      [0x00000080]  Special opcode 9: advance Address by 0 to 0x118d and Line by 4 to 10 (view 1)
      [0x00000081]  Set column to 12
      [0x00000083]  Special opcode 18: advance Address by 1 to 0x118e and Line by -1 to 9
      [0x00000084]  Special opcode 75: advance Address by 5 to 0x1193 and Line by 0 to 9
      [0x00000085]  Set column to 11
      [0x00000087]  Set is_stmt to 1
      [0x00000088]  Special opcode 22: advance Address by 1 to 0x1194 and Line by 3 to 12
      [0x00000089]  Set is_stmt to 0
      [0x0000008a]  Special opcode 117: advance Address by 8 to 0x119c and Line by 0 to 12
      [0x0000008b]  Set column to 5
      [0x0000008d]  Set is_stmt to 1
      [0x0000008e]  Special opcode 230: advance Address by 16 to 0x11ac and Line by 1 to 13
      [0x0000008f]  Special opcode 6: advance Address by 0 to 0x11ac and Line by 1 to 14 (view 1)
      [0x00000090]  Set column to 1
      [0x00000092]  Set is_stmt to 0
      [0x00000093]  Advance PC by constant 17 to 0x11bd
      [0x00000094]  Special opcode 48: advance Address by 3 to 0x11c0 and Line by 1 to 15
      [0x00000095]  Set column to 5
      [0x00000097]  Extended opcode 4: set Discriminator to 1
      [0x0000009b]  Advance PC by constant 17 to 0x11d1
      [0x0000009c]  Special opcode 130: advance Address by 9 to 0x11da and Line by -1 to 14
      [0x0000009d]  Set column to 1
      [0x0000009f]  Advance PC by constant 17 to 0x11eb
      [0x000000a0]  Special opcode 202: advance Address by 14 to 0x11f9 and Line by 1 to 15
      [0x000000a1]  Advance PC by 5 to 0x11fe
      [0x000000a3]  Extended opcode 1: End of Sequence
    
    
    Contents of the .debug_str section:
    
      0x00000000 6c6f6e67 20756e73 69676e65 6420696e long unsigned in
      0x00000010 74005f5f 73746163 6b5f6368 6b5f6661 t.__stack_chk_fa
      0x00000020 696c005f 5f505245 5454595f 46554e43 il.__PRETTY_FUNC
      0x00000030 54494f4e 5f5f0065 7175616c 006d6169 TION__.equal.mai
      0x00000040 6e005f5f 61737365 72745f66 61696c00 n.__assert_fail.
      0x00000050 474e5520 43313120 31312e34 2e30202d GNU C11 11.4.0 -
      0x00000060 6d74756e 653d6765 6e657269 63202d6d mtune=generic -m
      0x00000070 61726368 3d783836 2d363420 2d67202d arch=x86-64 -g -
      0x00000080 4f67202d 7374643d 63313120 2d666173 Og -std=c11 -fas
      0x00000090 796e6368 726f6e6f 75732d75 6e77696e ynchronous-unwin
      0x000000a0 642d7461 626c6573 202d6673 7461636b d-tables -fstack
      0x000000b0 2d70726f 74656374 6f722d73 74726f6e -protector-stron
      0x000000c0 67202d66 73746163 6b2d636c 6173682d g -fstack-clash-
      0x000000d0 70726f74 65637469 6f6e202d 6663662d protection -fcf-
      0x000000e0 70726f74 65637469 6f6e0063 68617200 protection.char.
      0x000000f0 5f426f6f 6c00                       _Bool.
    
    Contents of the .debug_line_str section:
    
      0x00000000 2f686f6d 652f7068 696c6970 2f706869 /home/philip/phi
      0x00000010 6c7a6f6f 6b35382e 67697468 75622e69 lzook58.github.i
      0x00000020 6f2f5f64 72616674 73002f74 6d702f61 o/_drafts./tmp/a
      0x00000030 6c6c5f65 7175616c 2e63002f 746d7000 ll_equal.c./tmp.
      0x00000040 2f757372 2f696e63 6c756465 00617373 /usr/include.ass
      0x00000050 6572742e 6800                       ert.h.
    
    Contents of the .debug_loclists section:
    
        Offset   Begin            End              Expression
    
        0000000c v000000000000002 v000000000000000 location view pair
        0000000e v000000000000000 v000000000000000 location view pair
        00000010 v000000000000000 v000000000000000 location view pair
        00000012 v000000000000000 v000000000000000 location view pair
    
        00000014 v000000000000002 v000000000000000 views at 0000000c for:
                 000000000000116d 0000000000001174 (DW_OP_lit0; DW_OP_stack_value)
        0000001a v000000000000000 v000000000000000 views at 0000000e for:
                 0000000000001174 000000000000118d (DW_OP_reg0 (rax))
        0000001f v000000000000000 v000000000000000 views at 00000010 for:
                 000000000000118d 000000000000118e (DW_OP_reg2 (rcx))
        00000024 v000000000000000 v000000000000000 views at 00000012 for:
                 000000000000118e 0000000000001193 (DW_OP_reg0 (rax))
        00000029 <End of list>
    
    Contents of the .debug_rnglists section:
    
        Offset   Begin    End
        0000000c 000000000000116d 000000000000118d 
        0000000f 0000000000001193 0000000000001194 
        00000012 <End of list>