Support threads with empty code section

[Nils-Lauermann]

Empty threads (i.e. only comments/labels) are detected and manually added to assembled HashMap

Note: I believe empty thread sections are optimised away by the linker after resolving references, so labels in empty threads don't appear in nm output or debugging logs.

Here is the test I used for debugging this

arch = "AArch64"
name = "empty_thread_with_label"
symbolic = ["x"]

page_table_setup = """
	physical pa_x;
	x |-> pa_x;
	*pa_x = 0;
	identity 0x1000 with code;
	identity 0x2000 with code;
"""

[types]
"pa_x" = "uint64_t"

[thread.0]
code = """
	// Empty thread for testing label-only code
done:
"""

[thread.0.reset]
R0 = "x"
VBAR_EL1 = "extz(0x1000, 64)"
"PSTATE.EL" = "0b01"

[section.thread0_el1_handler]
address = "0x1000"
code = """
	ADRP X29,done
	ADD X29,X29,:lo12:done
	MSR ELR_EL1,X29
	ERET
"""

[thread.1]
code = """
	MOV X1,#42
	STR X1,[X0]
finish:
"""

[thread.1.reset]
R0 = "x"
VBAR_EL1 = "extz(0x2000, 64)"
"PSTATE.EL" = "0b01"

[section.thread1_el1_handler]
address = "0x2000"
code = """
	ADRP X29,finish
	ADD X29,X29,:lo12:finish
	MSR ELR_EL1,X29
	ERET
"""

[final]
expect = "sat"
assertion = "*pa_x = 42"

The isla debug output

No primop emulator_read_tag (Name { id: 2694 })
No primop emulator_write_tag (Name { id: 2695 })
[log]: Using separate footprint config
No primop emulator_read_tag (Name { id: 2694 })
No primop emulator_write_tag (Name { id: 2695 })
[log]: Architecture + config hash: e8e5a696bbc81521e437a60e0da93bbc32058f5a092e6dcf2a0aa39bbb3f1128
[log]: Parsing took: 21554ms
[log]: Thread 0 has empty code
[log]: Linker script:
start = 0;
ENTRY(start);
SECTIONS
{
  . = 0x1000;
  thread0_el1_handler : { *(thread0_el1_handler) }
  . = 0x2000;
  thread1_el1_handler : { *(thread1_el1_handler) }
  . = 0x400000;
  litmus_0 : { *(litmus_0) }
  . = 0x401000;
  litmus_1 : { *(litmus_1) }
}

[log]: Thread 0 is empty, adding with address 0x400000
[log]: Objdump:

/tmp/isla/isla_71834_1:     file format elf64-littleaarch64


Disassembly of section thread0_el1_handler:

0000000000001000 <thread0_el1_handler>:
    1000:       f0001ffd        adrp    x29, 400000 <start+0x400000>
    1004:       910003bd        add     x29, x29, #0x0
    1008:       d518403d        msr     elr_el1, x29
    100c:       d69f03e0        eret

Disassembly of section thread1_el1_handler:

0000000000002000 <thread1_el1_handler>:
    2000:       f0001ffd        adrp    x29, 401000 <start+0x401000>
    2004:       910023bd        add     x29, x29, #0x8
    2008:       d518403d        msr     elr_el1, x29
    200c:       d69f03e0        eret

Disassembly of section litmus_1:

0000000000401000 <finish-0x8>:
  401000:       d2800541        mov     x1, #0x2a                       // #42
  401004:       f9000001        str     x1, [x0]

[log]: Names:
0000000000401008 t finish
0000000000000000 A start

[log]: Thread 0 @ 0x400000
[log]: Thread 1 @ 0x401000
[log]: Section thread0_el1_handler @ 0x1000
[log]: Section thread1_el1_handler @ 0x2000
[log]: Symbolic execution took: 1135ms
[log]: Footprint cache: Some("/tmp")
[log]: Got 0 uncached concrete opcodes for footprint analysis
[log]: Footprint analysis symbolic execution took: 0ms
[log]: There are 0 footprints
[log]: There are 1 candidate executions
[log]: with 28431 events
[log]: generating smt for candidate
[log]: generating smt events
[log]: generating smt basic relations
[log]: generating smtlib
[log]: generating smt final assertion
[log]: generating final smt
[log]: accessor function fault_is_from_write
[log]: accessor function F
[log]: accessor function Ifetch
[log]: accessor function is_cacheop
[log]: accessor function ak_strength
[log]: accessor function is_fault
[log]: accessor function tlbi_asid
[log]: accessor function tlbi_vmid
[log]: accessor function TLBI
[log]: accessor function z_dmb
[log]: accessor function is_tlbi
[log]: accessor function tlbi_shareability
[log]: accessor function translation_vmid
[log]: accessor function cache_op_shareability
[log]: accessor function is_DxB
[log]: accessor function write_phys_addr
[log]: accessor function MSR
[log]: accessor function barrier_domain
[log]: accessor function TE
[log]: accessor function Explicit
[log]: accessor function tlbi_op
[log]: accessor function ERET
[log]: accessor function z_isb
[log]: accessor function read_phys_addr
[log]: accessor function cache_op_type
[log]: accessor function cache_op_scope
[log]: accessor function cacheop_phys_addr
[log]: accessor function translation_asid
[log]: accessor function tlbi_address
[log]: accessor function fault_type
[log]: accessor function is_atomic
[log]: accessor function cache_op_kind
[log]: accessor function fault_acc_type
[log]: accessor function acch0l0fzdata
[log]: accessor function barrier_types
[log]: accessor function z_dsb
[log]: accessor function tlbi_regime
[log]: finished generating /tmp/isla_candidate_emptythreadwithlabel_g0t0_71834_0.smt2
[log]: solver took: 771ms
[log]: output model written to /tmp/isla_candidate_emptythreadwithlabel_g0t0_71834_0_model.smt2
[log]: warning: failed to get final state for execution: Failed to get final register state: Failed to parse smt model: failed to interpret smt during parse: in '(phys_addr (store ((as const (Array Event (_ BitVec 64))) #x0000000000000000) W2_2035_1 #x0000000000600000))', '(store ((as const (Array Event (_ BitVec 64))) #x0000000000000000) W2_2035_1 #x0000000000600000)', '((as const (Array Event (_ BitVec 64))) #x0000000000000000)', Bad function call
empty_thread_with_label allowed (1 of 1) 2798ms .................................................... ?