map_val(1) + 0 results in wrong type

[Alan-Jowett]

PS F:\sonde> llvm-objdump -Sl test-programs\send.o

test-programs\send.o:   file format elf64-bpf

Disassembly of section sonde:

0000000000000000 <program>:
; program():
       0:       18 01 00 00 00 00 00 00 00 00 00 00 00 00 00 00 r1 = 0x0 ll
       2:       b7 02 00 00 02 00 00 00 r2 = 0x2
       3:       85 00 00 00 08 00 00 00 call 0x8
       4:       b7 00 00 00 00 00 00 00 r0 = 0x0
       5:       95 00 00 00 00 00 00 00 exit

PS F:\sonde> llvm-objdump -r test-programs\send.o

test-programs\send.o:   file format elf64-bpf

RELOCATION RECORDS FOR [sonde]:
OFFSET           TYPE                     VALUE
0000000000000000 R_BPF_64_64              .rodata

Error: verification failed: program `program` failed verification
3: Invalid type (r1.type in {stack, packet, shared})

Pre-invariant : [
    r1.type=ctx,
    r10.type=stack][
    meta_offset=0,
    packet_size=0,
    r1.ctx_offset=0, r1.svalue=[1, 2147418112],
    r10.stack_offset=4096, r10.svalue=[4096, 2147418112]]
Stack: Numbers -> {}
  from entry;
0:
  r1 = map_val(1) + 0;
  goto 2;

Post-invariant : [
    r1.type=ctx,
    r10.type=stack][
    meta_offset=0,
    packet_size=0,
    r1.ctx_offset=0, r1.svalue=[1, 2147418112], r1.uvalue=r1.svalue,
    r10.stack_offset=4096, r10.svalue=[4096, 2147418112]]
Stack: Numbers -> {}

Pre-invariant : [
    r1.type=ctx,
    r10.type=stack][
    meta_offset=0,
    packet_size=0,
    r1.ctx_offset=0, r1.svalue=[1, 2147418112], r1.uvalue=r1.svalue,
    r10.stack_offset=4096, r10.svalue=[4096, 2147418112]]
Stack: Numbers -> {}
  from 0;
2:
  r2 = 2;
  goto 3;

Post-invariant : [
    r1.type=ctx,
    r10.type=stack,
    r2.type=number][
    meta_offset=0,
    packet_size=0,
    r1.ctx_offset=0, r1.svalue=[1, 2147418112], r1.uvalue=r1.svalue,
    r10.stack_offset=4096, r10.svalue=[4096, 2147418112],
    r2.svalue=2, r2.uvalue=2]
Stack: Numbers -> {}

Pre-invariant : [
    r1.type=ctx,
    r10.type=stack,
    r2.type=number][
    meta_offset=0,
    packet_size=0,
    r1.ctx_offset=0, r1.svalue=[1, 2147418112], r1.uvalue=r1.svalue,
    r10.stack_offset=4096, r10.svalue=[4096, 2147418112],
    r2.svalue=2, r2.uvalue=2]
Stack: Numbers -> {}
  from 2;
3:
  assert r2.type == number;
  assert r2.value > 0;
  assert r1.type in {stack, packet, shared};
  assert valid_access(r1.offset, width=r2) for read;
  r0 = send:8(mem r1[r2], uint64_t r2);

Verification error:
3: Invalid type (r1.type in {stack, packet, shared})

[Alan-Jowett]

prevail-rust/src/crab/ebpf_transformer.rs

Lines 335 to 348 in bc5be2e

	if let Some(desc) = desc {
	let map_type = ctx.platform.get_map_type(desc.map_type);
	if map_type.value_type == EbpfMapValueType::Program {
	panic!("Cannot load address of program map type - only data maps are supported");
	}
	dom.state.assign_type_encoding(dst_reg, T_SHARED, registry);
	let dst = reg_pack(dst_reg, registry);
	dom.state
	.values
	.assign_i64(dst.shared_offset, offset as i64, registry);
	dom.state
	.values
	.assign_i64(dst.shared_region_size, desc.value_size as i64, registry);
	}

vs:
https://github.com/vbpf/prevail/blob/32b23b8a9db9f8c03f1cbd3d4c2d4f251a1d2a22/src/crab/ebpf_transformer.cpp#L1019

[elazarg]

I think this is fixed now