Skip to content

Instantly share code, notes, and snippets.

@mdaniel
Created March 24, 2024 17:20
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save mdaniel/cdf52de6a8aa8982d591da82b160a229 to your computer and use it in GitHub Desktop.
Save mdaniel/cdf52de6a8aa8982d591da82b160a229 to your computer and use it in GitHub Desktop.
extracted from ipg-pldi-ae.tar in https://zenodo.org/records/7811236
ELF -> H[0,128]
for i = 0 to H.e_shnum in (SH[H.e_shoff+i*H.e_shentsize, H.e_shoff+(i+1)*H.e_shentsize])
for i = 1 to H.e_shnum in (Sec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size])
where Sec ->
switch(SH(i).sh_type = 6 -> DynSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ SH(i).sh_type = 3 -> StrSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ (SH(i).sh_type = 11) || (SH(i).sh_type = 2) -> DynSymSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ SH(i).sh_type = 7 -> NoteSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ SH(i).sh_type = 9 -> RelSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ SH(i).sh_type = 4 -> RelAddEndSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size]
/ SH(i).sh_type = 8 -> "@data"[0,0]
/ "@data"[0, EOI])
;
H -> "ELF"[1, 4]
{ ei_class = btoi[4, 5] }
{ ei_data = btoi[5, 6] }
{ ei_version = btoi[6, 7] }
{ abi = btoi[7, 8] }
{ abi_version = btoi[8, 9] }
{ e_type = btoi[16,18] }
{ e_machine = btoi[18,20] }
{ e_version = btoi[20,24] }
{ e_entry = btoi[24,32] }
{ e_phoff = btoi[32,40] }
{ e_shoff = btoi[40,48] }
{ e_flags = btoi[48,52] }
{ e_ehsize = btoi[52,54] }
{ e_phentsize = btoi[54,56] }
{ e_phnum = btoi[56,58] }
{ e_shentsize = btoi[58,60] }
{ e_shnum = btoi[60,62] }
{ e_shstrndx = btoi[62,64] }
;
SH -> { sh_name = btoi[0,4],
sh_type = btoi[4,8],
sh_flags = btoi[8,16],
sh_addr = btoi[16,24],
sh_offset = btoi[24,32],
sh_size = btoi[32,40],
sh_link = btoi[40,44],
sh_info = btoi[44,48],
sh_addralign = btoi[48,52],
sh_entsize = btoi[52,60] }
;
DynSec -> for i = 0 to EOI/16 in (DynSecEntry[16 * i, 16 * (i+1)])
;
DynSecEntry -> { tag = btoi[0, 8], value_or_ptr = btoi[8, 16] }
;
StrSec -> Str[0,EOI] StrSec[Str.end,EOI]
/ Str[0,EOI]
;
Str -> "\x00"[0,1] / "@data"[0,1] Str[1, EOI]
;
DynSymSec -> for i = 0 to EOI/24 in (DynSymSecEntry[24 * i, 24 * (i+1)])
;
DynSymSecEntry -> { sh_name = btoi[0,4],
st_info = btoi[4,5],
st_other = btoi[5,6],
st_shndx = btoi[6,8],
st_value = btoi[8,16],
st_size = btoi[16,24] }
;
NoteSec -> NoteSecEntry[0,EOI] NoteSec[NoteSecEntry.end, EOI]
/ NoteSecEntry[0,EOI]
;
NoteSecEntry -> { len_name = btoi[0,4] }
{ len_descriptor = btoi[4,8] }
{ type = btoi[8,12] }
Name[12,12+len_name]
"@data"[12+len_name,12+len_name+(0-len_name)%4]
Descriptor[12+len_name+(0-len_name)%4, 12+len_name+(0-len_name)%4+len_descriptor]
"@data"[12+len_name+(0-len_name)%4+len_descriptor, 12+len_name+(0-len_name)%4+len_descriptor+(0-len_descriptor)%4]
;
Name -> "@data"[0,EOI-1] "\x00"[EOI-1,EOI]
;
Descriptor -> "@data"[0,EOI]
;
RelAddEndSec -> for i = 0 to EOI/24 in (RelAddEndSecEntry[24 * i, 24 * (i+1)])
;
RelAddEndSecEntry -> { offset = btoi[0,8] }
{ info = btoi[8,16] }
{ addend = btoi[16,24] }
;
RelSec -> for i = 0 to EOI/16 in (RelSecEntry[16 * i, 16 * (i+1)])
;
RelSecEntry -> { offset = btoi[0,8] }
{ info = btoi[8,16] }
ELF -> H[0,128]
for i = 1 to H.e_shnum in (switch(SH(i).sh_type = 11 -> DynSymSec[SH(i).sh_offset, SH(i).sh_offset+SH(i).sh_size] / "@data"[0, 1]))
for i = 0 to H.e_shnum in (SH[H.e_shoff+i*H.e_shentsize, H.e_shoff+(i+1)*H.e_shentsize])
;
H -> "ELF"[1, 4]
{ ei_class = btoi[4, 5] }
{ ei_data = btoi[5, 6] }
{ ei_version = btoi[6, 7] }
{ abi = btoi[7, 8] }
{ abi_version = btoi[8, 9] }
{ e_type = btoi[16,18]}
{ e_machine = btoi[18,20]}
{ e_version = btoi[20,24]}
{ e_entry = btoi[24,32]}
{ e_phoff = btoi[32,40]}
{ e_shoff = btoi[40,48]}
{ e_flags = btoi[48,52]}
{ e_ehsize = btoi[52,54]}
{ e_phentsize = btoi[54,56]}
{ e_phnum = btoi[56,58]}
{ e_shentsize = btoi[58,60]}
{ e_shnum = btoi[60,62]}
{ e_shstrndx = btoi[62,64]}
;
SH -> { sh_name = btoi[0,4],
sh_type = btoi[4,8],
sh_flags = btoi[8,16],
sh_addr = btoi[16,24],
sh_offset = btoi[24,32],
sh_size = btoi[32,40],
sh_link = btoi[40,44],
sh_info = btoi[44,48],
sh_addralign = btoi[48,56],
sh_entsize = btoi[56, 64] }
;
DynSymSec -> for i = 0 to EOI/24 in (DynSymSecEntry[24 * i, 24 * (i+1)])
;
DynSymSecEntry -> { sh_name = btoi[0,4],
st_info = btoi[4,5],
st_other = btoi[5,6],
st_shndx = btoi[6,8],
st_value = btoi[8,16],
st_size = btoi[16,24] }
GIF -> "GIF"[0, 3] "@data"[3, 6] LSD[6, EOI] Blocks[LSD.end, EOI]
;
LSD -> { logical_width = btoi[0,2] }
{ logical_height = btoi[2,4] }
{ flag = btoi[4,5] }
{ background_color = btoi[5,6] }
{ pixel_aspect_ratio = btoi[6,7],
has_color_table = flag >> 7,
color_table_size = 3*(2 << (flag & 7)) }
switch ( has_color_table=1 -> ColorTable[7, 7+color_table_size]
/ ""[0,0] )
;
Blocks -> Block Blocks / Trailer
;
Block -> GraphicControlExtension
/ ImageDescriptor
/ ApplicationExtension
/ CommentExtension
;
Trailer -> "\x3B"
;
GraphicControlExtension -> "\x21\xF9"[0,2]
{ size = btoi[2,3] }
{ packed_field = btoi[3,4] }
{ delay_time = btoi[4,6] }
{ transparent_color_index = btoi[6,7] }
"\x00"[7, 8]
;
ImageDescriptor -> "\x2c"[0,1]
{ image_left = btoi[1,3] }
{ image_top = btoi[3,5] }
{ image_width = btoi[5,7] }
{ image_height = btoi[7,9] }
{ packed_field = btoi[9,10],
lct_flag = packed_field >> 7,
lct_size = lct_flag*(3*(2 << (packed_field & 7))) }
switch (lct_flag=1 -> ColorTable[10, 10+lct_size] / ""[0, 0])
"@data"[10+lct_size, 10+lct_size+1]
ImageData[10+lct_size+1, EOI]
;
ApplicationExtension -> "\x21\xFF"[0,2]
{ size = btoi[2,3] }
"@data"[3,3+size]
ImageData[3+size, EOI]
;
ImageData -> "\x00"[0, 1]
/ { size = btoi[0,1] }
"@data"[1, 1+size] ImageData[1+size, EOI]
;
CommentExtension -> "\x21\xFE"[0,2]
{ size = btoi[2,3] }
"@data"[3,3+size]
"\x00"[3+size, 4+size]
;
ColorTable -> RGB[0,3] ColorTable[3,EOI] / RGB[0,3]
;
RGB -> { R = btoi[0,1] }
{ G = btoi[1,2] }
{ B = btoi[2,3] }
Ipfour -> { vi = btoi[0, 1],
version = vi >> 4,
ihl = vi & 0x15 }
{ de = btoi[1, 2],
dscp = de >> 2,
ecn = de & 0x3 }
{ totallength = btoi[2, 4] }
{ ident = btoi[4, 6] }
{ zdmf = btoi[6, 8],
zero = zdmf >> 15,
df = (zdmf >> 14) & 0x1,
mf = (zdmf >> 13) & 0x1,
fragmentoff = zdmf & 0x1FFF }
{ ttl = btoi[8, 9] }
{ protocol = btoi[9, 10] }
{ hdrchecksum = btoi[10, 12] }
{ source = btoi[12, 16] }
{ dest = btoi[16, 20] }
Udp[20, EOI];
Udp -> { src = btoi[0, 2] }
{ dest = btoi[2, 4] }
{ len = btoi[4, 6] }
{ checksum = btoi[6, 8] }
for i = 0 to (len-8) in ("@data"[8+i, 8+i+1]);
Int -> { v = btoi[0,1] }
pe -> "MZ"[0,2] "@data"[2,60] { ofs_pe=btoi[60,64] }
"PE\x00\x00"[ofs_pe,ofs_pe+4] CoffHdr[ofs_pe+4,ofs_pe+24] { hdr_end = 24+CoffHdr.SizeOfOptionalHeader }
OptionalHdr[ofs_pe+24,ofs_pe+hdr_end]
for i = 0 to CoffHdr.NumSections in (section[ofs_pe+hdr_end+40*i,ofs_pe+hdr_end+40*(i+1)])
for i = 0 to CoffHdr.NumSections in ("@data"[ofs_pe+section(i).data_ofs,ofs_pe+section(i).data_ofs + section(i).data_size])
switch ( OptionalHdr.CertificateTableVa = 0 -> ""[0, 0]
/ certificate_table[OptionalHdr.CertificateTableVa, OptionalHdr.CertificateTableVa+OptionalHdr.certificate_table_size])
;
CoffHdr -> { machine = btoi[0,2],
NumSections = btoi[2,4],
TimeDateStamp = btoi[4,8],
PointerToSymbolTable = btoi[8,12],
NumSymbols = btoi[12,16],
SizeOfOptionalHeader = btoi[16,18],
characteristics = btoi[18,20] }
for i = 0 to NumSymbols in (CoffSymbol[PointerToSymbolTable+18*i,PointerToSymbolTable+18*(i+1)])
;
CoffSymbol -> { name_zeroes = btoi[0,4],
name_offset = btoi[4,8],
value = btoi[8,12],
section_number = btoi[12,14],
type = btoi[14,16],
storage_class = btoi[16,17],
number_of_aux_symbols = btoi[17,18] }
;
OptionalHdr -> OptionalHeaderStd[0,24] OptionalHeaderWindows[24,112] OptionalHeaderDataDirs[112,232]
{ CertificateTableVa = OptionalHeaderDataDirs.CertificateTableVa,
certificate_table_size = OptionalHeaderDataDirs.certificate_table_size }
;
OptionalHeaderStd -> { format = btoi[0,2],
major_linker_version = btoi[2,3],
minor_linker_version = btoi[3,4],
size_of_code = btoi[4,8],
size_of_initialized_data = btoi[8,12],
size_of_uninitialized_data = btoi[12,16],
address_of_entry_point = btoi[16,20],
base_of_code = btoi[20,24] }
;
OptionalHeaderWindows -> { image_base_64 = btoi[0,8],
section_alignment = btoi[8,12],
file_alignment = btoi[12,16],
major_operating_system_version = btoi[16,18],
minor_operating_system_version = btoi[18,20],
major_image_version = btoi[20,22],
minor_image_version = btoi[22,24],
major_subsystem_version = btoi[24,26],
minor_subsystem_version = btoi[26,28],
win32_version_value = btoi[28,32],
size_of_image = btoi[32,36],
size_of_headers = btoi[36,40],
check_sum = btoi[40,44],
subsystem = btoi[44,46],
dll_characteristics = btoi[46,48],
size_of_stack_reserve_64 = btoi[48,56],
size_of_stack_commit_64 = btoi[56,64],
size_of_heap_reserve_64 = btoi[64,72],
size_of_heap_commit_64 = btoi[72,80],
loader_flags = btoi[80,84],
number_of_rva_and_sizes = btoi[84,88] }
;
OptionalHeaderDataDirs -> DataDir[0,8]
DataDir[8,16]
DataDir[16,24]
DataDir[24,32]
DataDir[32,40]
{ CertificateTableVa = DataDir.VirtualAddress,
certificate_table_size = DataDir.size }
DataDir[40,48]
DataDir[48,56]
DataDir[56,64]
DataDir[64,72]
DataDir[72,80]
DataDir[80,88]
DataDir[88,96]
DataDir[96,104]
DataDir[104,112]
DataDir[112,120]
;
DataDir -> { VirtualAddress = btoi[0,4], size = btoi[4,8] }
;
section -> "@data"[0,8]
{ virtual_size = btoi[8,12],
VirtualAddress = btoi[12,16],
data_size = btoi[16,20],
data_ofs = btoi[20,24],
pointer_to_relocations = btoi[24,28],
pointer_to_linenumbers = btoi[28,32],
number_of_relocations = btoi[32,34],
number_of_linenumbers = btoi[34,36],
characteristics = btoi[36,40] }
;
certificate_table -> CertificateEntry[0,EOI] certificate_table[CertificateEntry.end,EOI]
/ CertificateEntry[0,EOI]
;
CertificateEntry -> { length = btoi[0,4],
revision = btoi[4,6],
certificate_type = btoi[6,8] }
"@data"[8,length]
include: "decompress.h"
extern: decompress:output_t
zip -> sections
;
sections -> section sections / section
;
section -> "PK"[0,2] { type = btoi[2,4] }
switch( type = 513 -> CentralDirEty[4,EOI]
/ type = 1027 -> LocalFile[4,EOI]
/ type = 1541 -> EndOfCentralDir[4,EOI]
/ type = 2055 -> DataDescriptor[4,EOI]
/ "err"[1,0])
;
DataDescriptor -> { crc32 = btoi[0,4],
len_body_compressed = btoi[4,8],
len_body_uncompressed = btoi[8,12] }
;
LocalFileHeader -> { version0 = btoi[0,1],
version1 = btoi[1,2],
gp_flags = btoi[2,4],
compression_method = btoi[4,6],
last_mod_dos_datetime = btoi[6, 10],
crc32 = btoi[10,14],
len_body_compressed = btoi[14,18],
len_body_uncompressed = btoi[18,22],
len_file_name = btoi[22,24],
len_extra = btoi[24,26] }
"@data"[26,26 + len_file_name]
"@data"[26 + len_file_name,26 + len_file_name + len_extra]
;
LocalFile -> LocalFileHeader[0,EOI] decompress[LocalFileHeader.end, LocalFileHeader.end + LocalFileHeader.len_body_compressed]
;
CentralDirEty -> { version_made_by0 = btoi[0,1]
, version_made_by1 = btoi[1,2]
, version_needed_to_extract0 = btoi[2,3]
, version_needed_to_extract1 = btoi[3,4]
, flags = btoi[4,6]
, compression_method = btoi[6,8]
, last_mod_dos_datetime = btoi[6, 10]
, crc32 = btoi[12,16]
, len_body_compressed = btoi[16,20]
, len_body_uncompressed = btoi[20,24]
, len_file_name = btoi[24,26]
, len_extra = btoi[26,28]
, len_comment = btoi[28,30]
, disk_number_start = btoi[30,32]
, int_file_attr = btoi[32,34]
, ext_file_attr = btoi[34,38]
, ofs_local_header = btoi[38,42] }
"@data"[42,42 + len_file_name]
"@data"[42 + len_file_name,42 + len_file_name + len_extra]
"@data"[42 + len_file_name + len_extra,42 + len_file_name + len_extra + len_comment]
;
EndOfCentralDir -> { disk_of_end_of_central_dir = btoi[0,2]
, disk_of_central_dir = btoi[2,4]
, num_central_dir_entries_on_disk = btoi[4,6]
, num_central_dir_entries_total = btoi[6,8]
, len_central_dir = btoi[8,12]
, ofs_central_dir = btoi[12,16]
, len_comment = btoi[16,18] }
"@data"[18,18 + len_comment]
zip -> sections
;
sections -> section sections
/ section
;
section -> "PK"[0,2] { type = btoi[2,4] }
switch( type = 513 -> CentralDirEty[4,EOI]
/ type = 1027 -> LocalFile[4,EOI]
/ type = 1541 -> EndOfCentralDir[4,EOI]
/ type = 2055 -> DataDescriptor[4,EOI]
/ err[1,0])
;
DataDescriptor -> { crc32 = btoi[0,4],
len_body_compressed = btoi[4,8],
len_body_uncompressed = btoi[8,12] }
;
LocalFileHeader -> { version0 = btoi[0,1],
version1 = btoi[1,2],
gp_flags = btoi[2,4],
compression_method = btoi[4,6],
last_mod_dos_datetime = btoi[6, 10],
crc32 = btoi[10,14],
len_body_compressed = btoi[14,18],
len_body_uncompressed = btoi[18,22],
len_file_name = btoi[22,24],
len_extra = btoi[24,26] }
FileName[26,26 + len_file_name]
extras[26 + len_file_name,26 + len_file_name + len_extra]
;
LocalFile -> LocalFileHeader "@data"[LocalFileHeader.end, LocalFileHeader.end + LocalFileHeader.len_body_compressed]
;
CentralDirEty -> { version_made_by0 = btoi[0,1]
, version_made_by1 = btoi[1,2]
, version_needed_to_extract0 = btoi[2,3]
, version_needed_to_extract1 = btoi[3,4]
, flags = btoi[4,6]
, compression_method = btoi[6,8]
, last_mod_dos_datetime = btoi[6, 10]
, crc32 = btoi[12,16]
, len_body_compressed = btoi[16,20]
, len_body_uncompressed = btoi[20,24]
, len_file_name = btoi[24,26]
, len_extra = btoi[26,28]
, len_comment = btoi[28,30]
, disk_number_start = btoi[30,32]
, int_file_attr = btoi[32,34]
, ext_file_attr = btoi[34,38]
, ofs_local_header = btoi[38,42] }
FileName[42,42 + len_file_name]
extras[42 + len_file_name,42 + len_file_name + len_extra]
"@data"[42 + len_file_name + len_extra,42 + len_file_name + len_extra + len_comment]
;
EndOfCentralDir -> { disk_of_end_of_central_dir = btoi[0,2]
, disk_of_central_dir = btoi[2,4]
, num_central_dir_entries_on_disk = btoi[4,6]
, num_central_dir_entries_total = btoi[6,8]
, len_central_dir = btoi[8,12]
, ofs_central_dir = btoi[12,16]
, len_comment = btoi[16,18] }
"@data"[18,18 + len_comment]
;
extras -> ExtraEntry extras
/ ExtraEntry
/ ""[0,0]
;
ExtraEntry -> { code = btoi[0,2], len_body = btoi[2,4] }
switch( code = 10 -> ntfs[4,4 + len_body]
/ code = 21589 -> ExtendedTimestamp[4,4 + len_body]
/ code = 30837 -> InfozipUnixVarSize[4,4 + len_body]
/ err[1,0] )
;
ntfs -> { reserved = btoi[0,4] } attributes[4,EOI]
;
attributes -> attribute attributes / attribute
;
attribute -> { tag = btoi[0,2], len_body = btoi[2,4] }
switch( tag = 1 -> attribute_1[4,4 + len_body] / err[1,0] )
;
attribute_1 -> { last_mod_time = btoi[0,8]
, last_access_time = btoi[8,16]
, creation_time = btoi[16,24] }
;
ExtendedTimestamp -> TODO[0,EOI]
;
InfozipUnixVarSize -> { version = btoi[0,1]
, len_uid = btoi[1,2] }
"@data"[2,2 + len_uid]
{ len_gid = btoi[2 + len_uid, 2 + len_uid + 1] }
"@data"[2 + len_uid + 1, 2 + len_uid + 1 + len_gid]
;
FileName -> "@data"[0,EOI]
;
comment -> "@data"[0,EOI]
;
err -> "@data"[0,EOI]
;
TODO -> "@data"[0,EOI]
Dns -> { id = btoi[0, 2],
flag = btoi[2, 4],
qr = flag >> 15,
opcode = (flag >> 11) & 0xF,
aa = (flag >> 10) & 0x1,
tc = (flag >> 9) & 0x1,
rd = (flag >> 8) & 0x1,
ra = (flag >> 7) & 0x1,
z = (flag >> 6) & 0x1,
ad = (flag >> 5) & 0x1,
cd = (flag >> 4) & 0x1,
rcode = flag & 0xF }
assert(opcode = 0 || opcode = 1 || opcode = 2)
{ questioncount = btoi[4,6],
answercount = btoi[6,8],
authoritycount = btoi[8,10],
additionalcount = btoi[10,12] }
for i = 0 to questioncount in (Question[if i=0 then 12 else Question_0(i-1).end, EOI])
for i = 0 to answercount in (Answer[if i=0 then (if questioncount=0 then 12 else Question(questioncount-1).end) else Answer_0(i-1).end, EOI])
for i = 0 to authoritycount in (Answer[if i=0 then (if answercount=0 then (if questioncount=0 then 12 else Question(questioncount-1).end) else Answer_0(answercount-1).end) else Answer_1(i-1).end, EOI])
for i = 0 to additionalcount in (Answer[if i=0 then (if authoritycount=0 then (if answercount=0 then (if questioncount=0 then 12 else Question(questioncount-1).end) else Answer_0(answercount-1).end) else Answer_1(authoritycount-1).end) else Answer_2(i-1).end, EOI]);
Question -> Labels
{ qtype = btoi[Labels.end, Labels.end+2]
, qclass = btoi[Labels.end+2, Labels.end+4] }
"@data"[Labels.end, Labels.end+4]
assert(qclass = 1 || qclass = 2 || qclass = 3 || qclass = 4);
Answer -> Labels
{ rtype = btoi[Labels.end, Labels.end+2] }
{ rclass = btoi[Labels.end+2, Labels.end+4] }
assert(rclass = 1 || rclass = 2 || rclass = 3 || rclass = 4)
{ ttl = btoi[Labels.end+4, Labels.end+8] }
{ rlen = btoi[Labels.end+8, Labels.end+10] }
for i = 0 to rlen in (Int[Labels.end+10+i, Labels.end+11+i]);
Labels -> { flag = btoi[0, 1] } "@data"[0,1] assert(flag = 0)
/ { flag = btoi[0, 1] } "@data"[0,2] assert((flag >> 6) = 3) { value = btoi[1, 2] }
/ { flag = btoi[0, 1] } "@data"[1, 1+flag] Labels[1+flag, EOI];
Int -> { v = btoi[0, EOI] } "@data"[0, EOI]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment