Overview

This repository implements a translation of the Arm Architecture Specification Language (ASL) into a closed What4 expression using the Crucible symbolic execution library.

The ASL source is extracted from the official XML specifications from ARM using a set of tools developed by Alastair Reid. This source text is converted into a parse tree by the asl parser, which is the representation used by this tool.

Building

The dependencies of the project that are not on Hackage are specified using git submodules. To build the code with a modern version of cabal (assuming you are in the root of the repository):

$ git submodule update --init
$ ln -s cabal.project.newbuild cabal.project
$ cabal v2-configure
$ cabal v2-build asl-translator

Running

By default, this repository comes with an archived version of a successful translation of the ASL semantics, contained as two gzipped s-expressions file in archived/functions-norm.what4.gz and archived/instructions-norm.what4.gz. The module Language.ASL.Formulas provides an interface to these files through the functions getFunctionFormulas and getInstructionFormulas.

The translator can be run via cabal with cabal v2-run asl-translator-exec or equivalently make genarm. The default options will use the source files in data/Parsed to build a collection of serialized what4 expressions representing the instructions and helper functions for the A32 and T32 instructions. By default these are written out to output/instructions.what4 and output/functions.what4. Once these files exist, the normalized specification can be generated from them via cabal v2-run asl-translator-exec --normalize-mode=all. By default these are written out to output/instructions-norm.what4 and output/functions-norm.what4. The genarm make target will build these automatically.

The interface functions in Language.ASL.Formulas will prefer to use the normalized files in output if they exist, otherwise falling back on the archived files in archived.

The make genarm target will use cabal to run the translator, but also can build the source s-expression and asl files in data from the source ARM XML specification (via the Makefile in the arm-asl-parser subrepository).

Archiving

Any changes to the final normalized specification should be archived for consistency. The archive can be created with make archive, which will first build and normalize the specification if necessary.

Source Files

ASL Source

The data subdirectory contains 5 asl source files used for translation.

arm_instrs.asl

This file describes the semantics for each ARM instruction, including how to decode each instruction from an opcode.

This translator is not concerned with decoding, and represents each instruction as a function from its fields (as decoded operands) to a modification of the registers of the CPU.

arm_defs.asl

This file contains supporting definitions for auxiliary functions called by the instructions defined in arm_instrs.asl.

arm_regs.asl

This file describes the system registers referred to by both arm_defs.asl and arm_regs.asl.

support.asl

This file is the concatenation of several support asl source files generated by mra_tools, which provides stub definitions for functions whose semantics are implementation-defined.

extra_defs.asl

This is a manually written asl source file which overrides several functions from arm_defs.asl as well as providing definitions for functions which are used internally by the translator.

Parsed

The Parsed subdirectory contains the output of the arm-asl-parser tool on each of the asl source files described above. These are s-expressions representing the parse tree of each file.