Using ASLi with Arm's v8.6-A ISA specification
ASLi is an interpreter for Arm’s Architecture Specification Language. To use it, you need to download the MRA tools, Arm’s Architecture Specifications and, of course, ASLi. (Note: that I am linking to an updated version of ASLi instead of to Arm’s official release – I had to extend ASLi a bit to be able to execute programs with it.)
First, setup OCaml with all the libraries you will need. (These instructions are for MacOS.)
brew install opam gmp mpir opam install ocaml.4.09.0 menhir ocamlfind ott linenoise pprint z22.214.171.124 env CFLAGS="-I$HOME/homebrew/include/" LDFLAGS="-L$HOME/homebrew/lib/" opam install zarith eval `opam config env` export DYLD_LIBRARY_PATH=`opam config var z3:lib`
On Linux, the following is probably what you need (untested)
sudo apt-get install opam gmp mpir opam install ocaml.4.09.0 menhir ocamlfind ott linenoise pprint z126.96.36.199 zarith eval `opam config env` export LD_LIBRARY_PATH=`opam config var z3:lib`
These commands may take a while to run …
Once you have installed OCaml, download and build the tools as follows
git clone https://github.com/alastairreid/mra_tools.git git clone https://github.com/alastairreid/asl-interpreter.git make -C asl-interpreter asli
Downloading Arm’s specification
Once you have the tools setup, download the Arm specification
pushd mra_tools mkdir -p v8.6 pushd v8.6 wget https://developer.arm.com/-/media/developer/products/architecture/armv8-a-architecture/2019-12/SysReg_xml_v86A-2019-12.tar.gz wget https://developer.arm.com/-/media/developer/products/architecture/armv8-a-architecture/2019-12/A64_ISA_xml_v86A-2019-12.tar.gz wget https://developer.arm.com/-/media/developer/products/architecture/armv8-a-architecture/2019-12/AArch32_ISA_xml_v86A-2019-12.tar.gz tar zxf A64_ISA_xml_v86A-2019-12.tar.gz tar zxf AArch32_ISA_xml_v86A-2019-12.tar.gz tar zxf SysReg_xml_v86A-2019-12.tar popd
and unpack the specification using the mra_tools scripts
make all popd
This extracts the ASL code from the XML files that Arm distributes it in, generates declarations of all the system registers and patches some minor type errors in the ASL code. (The patches are required because ASLi has slightly stricter typechecking than the default configuration of Arm’s internal tool.)
The mra_tools repository also contains some support code that turns Arm’s specification into a simulator. This is in the directory mra_tools/support.
$ ls mra_tools/support README.txt debug.asl hints.asl stubs.asl aes.asl feature.asl interrupts.asl usermode.asl barriers.asl fetchdecode.asl memory.asl
You can run ASLi directly
cd asl-interpreter ./asli
This loads the ASL standard library and then prints the following banner that may feel familiar to users of Haskell interpreters like Hugs or GHCi.
_____ _ _ ___________________________________ /\ / ____|| | (_) ASL interpreter / \ | (___ | | _ Copyright Arm Limited (c) 2017-2019 / /\ \ \___ \ | | | | / ____ \ ____) || |____ | | ASL 0.1 alpha /_/ \_\|_____/ |______||_| ___________________________________ Type :? for help
ASLi is an interactive environment and you can type ASL expressions and ASL statements and see the result. (ASL statements must end with a semicolon for ASLi to execute them.)
ASLi> 1+1 2 ASLi> ZeroExtend('11', 32) '00000000000000000000000000000011' ASLi> bits(32) x = ZeroExtend('11', 32); ASLi> x '00000000000000000000000000000011'
You can also type commands starting with colon such as “:help”.
You can also tell ASLi to generate a trace as it executes using commands like this that trace calls to functions
For example, you can see evaluating ZeroExtend calls the function Zeros.
ASLi> :set +trace:fun ASLi> ZeroExtend('11', 32) TRACE funcall: ZeroExtend.0   2'11' 32 TRACE funcall: Zeros.0  30 32'00000000000000000000000000000011'
Running Arm’s specification
Once the specification is unpacked, we can use ASLi to parse and typecheck all the files
./asli prelude.asl ../mra_tools/arch/regs.asl ../mra_tools/types.asl ../mra_tools/arch/arch.asl ../mra_tools/arch/arch_instrs.asl ../mra_tools/arch/arch_decode.asl ../mra_tools/support/aes.asl ../mra_tools/support/barriers.asl ../mra_tools/support/debug.asl ../mra_tools/support/feature.asl ../mra_tools/support/hints.asl ../mra_tools/support/interrupts.asl ../mra_tools/support/memory.asl ../mra_tools/support/stubs.asl ../mra_tools/support/fetchdecode.asl
Arm’s architecture specification can be configured to match the behaviour of particular processors by specifying certain “implementation defined” constants. This is done using commands like the following.
:set impdef "Maximum Physical Address Size" = 52 :set impdef "Maximum Virtual Address Size" = 56 :set impdef "Reserved Intermediate Physical Address size value" = 52
Before running a program, you need to reset the processor
load a binary file and set the program counter and the stack pointer to appropriate addresses
:elf tests/test_O2.elf _PC = 0x400168[63:0]; SP = 0x100000[63:0];
and run the program
The example binary writes the word “Test” to a serial port and then writes the ASCII character EOT (end of transmission) to stop the interpreter. This produces output like this
Loading ELF file tests/test_O2.elf. Entry point = 0x400168 Test Program exited by writing ^D to TUBE Exception taken
All these commands are in the “project” file “tests/test.prj” and can be executed using the “:project” command
There are a few limitations on what I have done so far
- I did virtually no testing. If you try any other binaries, you might use some ASL feature that has not been tested yet and find a bug.
- The ELF loader only works for 64-bit little-endian files. So if you want to try 32-bit binaries or mixed endian tests, you will have to extend the ELF loader. (This is surprisingly easy to do.)
- Most seriously, the mra_tools scripts cannot generate all the ASL required to fully implement system registers. So it is very, very unlikely that you can boot Linux with what is there at the moment. It would be great if Arm would publicly release the system register support code they have internally.
OK, that’s enough for one post…
Related posts and papers
- Code: ASLi
- Code: MRA Tools
- Paper: End-to-End Verification of ARM Processors with ISA-Formal, CAV 2016.
- Paper: Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture, FMCAD 2016.
- Paper: Who guards the guards? Formal Validation of the Arm v8-M Architecture Specification), OOPSLA 2017.
- Verifying against the official ARM specification
- Finding Bugs versus Proving Absence of Bugs
- Limitations of ISA-Formal
- ARM’s ASL Specification Language
- ARM Releases Machine Readable Architecture Specification
- Dissecting the ARM Machine Readable Architecture files
- ASL Lexical Syntax
- Arm v8.3 Machine Readable Specifications
- Are Natural Language Specifications Useful?
- Formal validation of the Arm v8-M specification
- Bidirectional ARM Assembly Syntax Specifications
- Talk: [How can you trust formally verified software (pdf)], Chaos Communication Congress, 2017.
The opinions expressed are my own views and not my employer's.