Blk.KBval lift : cfg -> block -> blk term list Bap_knowledge.knowledgelift block takes a basic block of assembly instructions and lifts it to a list of blk terms. The first term in the list is the entry.
val from_insn : ?addr:addr -> insn -> blk term list Bap_knowledge.knowledgefrom_insn ?addr insn creates an IR representation of a single machine instruction insn.
Uses the Term.slot to get the IR representation of an instruction, trying to keep the number of basic blocks minimal (by coalescing adjacent data operations).
If addr is specified then the term identifier of the first block will be specific to that address and the address attribute will be set to the passed value.
val from_insns :
?fall:[ `Inter of Jmp.dst | `Intra of Jmp.dst ] ->
?addr:addr ->
insn list ->
blk term list Bap_knowledge.knowledgefrom_insns block translates a basic block of instructions into IR.
Takes a list of instructions in the execution order and translates them into a list of IR blks that are properly connected. The instructions shall belong to a single basic block.
The first element of the result is the entry block. If addr is set then it will have the term identifier equal to Term.for_addr addr and the address attribute will be set to addr.
The fall parameter designates the fallthrough destination of the basic block. The destination could be either interprocedural (`Inter) or intraprocedural (`Intra). In the latter case it will be reified into a jump of the call kind. If the last instruction (the basic block terminator) is a barrier Insn.(is barrier) is [true], then the fall destination is ignored, even if set.
val flatten : t -> t Bap_knowledge.knowledgeflatten blk translates blk into the flattened form. In the flattened form, all operations are applied to variables, constants, or unknowns, i.e., the operands could not be compound expressions. E.g.,
#10 := 11 * (#9 + 13) - 17
is translated to,
#11 := #9 + 13
#12 := 11 * #11
#10 := #12 - 17