Specifying the Semantics of Machine Instructions

Computer architecture manuals describe the instruction set of the machine and the semantics of those instructions by a combination of natural language and ISP (Instruction Set Processor) descriptions. The syntax of the instructions in assembly is well define in the form of tables in the manual. However, the semantics is not so well specified and descriptions vary widely from one manual to another. When developing a retargetable binary translator, as much as possible needs to be specified in order to automatically generate code from specifications, hence separating machine-independent issues from the manual coding stage. The specification of the semantics of machine instructions is one such task, with the aim of generating suitable code for an intermediate representation that is to be used during the analysis stage. We describe the design process used to develop a semantic specification language, SSL, to integrate into a retargetable binary translation framework. The techniques described herein are suitable not just to binary translators but also to machine-code manipulation tools such as optimizing compilers, binary profilers, instrumentors, and binary debuggers