package bap-std
A scheme of image specification.
An attribute is some statement about a program that is true, thus each attribute is a proposition in a logical database of inferred facts.
Note, in comments we use actual field names in the synopsis section of a function, e.g., section addr size
means that the section
statement has two fields Scheme.addr
and Scheme.size
.
See the OGRE library for more information.
type 'a region = {
addr : addr;
(*a starting address
*)size : size;
(*a size of the segment
*)info : 'a;
(*the attached information
*)
}
a contiguous piece of memory.
val off : off Ogre.field
offset
val size : size Ogre.field
offset
size
val addr : addr Ogre.field
size
address
val root : addr Ogre.field
name
code root
val fixup : addr Ogre.field
is_executable
an address of a fixup
arch name
a file contains code for the name
architecture.
E.g., arm, x86, x86_64
subarch name
the subarchitecture, when applicable, e.g., v7, v8, r2, etc. Should be appended to the arch name to get the full description, e.g., armv7.
vendor name
the second part of the build triplet, e.g., apple, pc, ibm, unknown. Could be just an empty string.
system name
the operating system name, for which the binary is specifically built, e.g., ananas, ios, linux.
abi name
the environment/toolchain/abi under which the binary is expected to be run, e.g., gnu, android, msvc
bits m
is the bitness of the target architecture, e.g., 16, 32, 64.
(format X)
defines the file format to be X.
Currently supported formats:
"elf"
;"macho"
;"coff"
(is-little-endian FLAG)] is set for files with words encoded in the little-endian order.
(is-executable FLAG)
is set for binaries that executable.
bias offset
the value by which all addresses are biased wrt to the real addresses in the binary.
val segment :
((bool * bool * bool) region,
(addr -> size -> bool -> bool -> bool -> 'a) ->
'a)
Ogre.attribute
segment addr size readable writable executable
a memory region (addr,size) has the specified permissions.
section addr size
a memory region is a section
code_start addr
an address starts a code sequence
entry_point addr
an address is the program entry point
symbol_chunk addr size root
a contiguous piece of a program symbol, that can be a function or some data.
named_region addr size name
a region of memory has a name
named_symbol addr name
a symbol that starts at this addr
has this name
.
mapped addr size off
sequence of bytes in a file starting at offset off
and has the given size
is mapped into memory at the given address addr
relocation fixup addr
a value referenced at the code that has the fixup
address is relocated to the specified address addr
.
external_reference addr name
a piece of code at the specified address addr
references an external symbol with the given name
.
base_address addr
this is the base address of an image, i.e., an address of a first byte of the image.
code_region addr size off
the memory region in the file with the given offset off
and size
is code that should be loaded at the specified virtual address addr
.