asli 0.2.0 · OCaml Package

README

Introduction

Example implementation of Arm's Architecture Specification Language (ASL).

The ASL interpreter is a collection of resources to help you to
understand and make use of Arm's architecture specifications.
It consists of lexer, parser, typechecker and interpreter for the ASL language
and an interactive interface for evaluating ASL statements and expressions.

There is a blog post
describing how to use ASLi with Arm's v8.6-A ISA specification.

Requirements

To build and run the ASL interpreter, you will need:

OCaml version 4.09 or later
OPAM OCaml version 2.0.5 (other versions may work)
The following OPAM packages
- ocaml - OCaml compiler
- odoc - OCaml documentation generator (optional)
- dune - OCaml build system
- menhir - parser generator tool
- ott.0.29 - tool for defining language grammars and semantics (this version or later required)
- linenoise - OCaml line editing library
- pprint - OCaml pretty-printing library
- z3.4.7.1 - OCaml bindings for the Z3 SMT solver (exactly this version is required)
- zarith - OCaml multiprecision arithmetic library

License and contribution

The software is provided under the BSD-3-Clause licence.
Contributions to this project are accepted under the same licence.

This software includes code from one other open source projects

The CIL project
defines a useful
visitor class
for traversing C ASTs.
The file visitor.ml is a modified copy of this class that generalizes
the type to work with an arbitrary AST.
CIL is distributed under a BSD-3-Clause licence.

Building and development

Directory structure

This interpreter consists of a single directory organized as follows

Metadata, documentation, etc:
- LICENCE - Software licence
- README.md - This file
- Makefile - build system file
Source code consisting of
- Lexer
  - libASL/lexer.mll - ASL lexer (ocamllex file)
  - libASL/lexersupport.ml - indentation-based parsing support
- Grammar and Parser
  - libASL/asl.ott - used to generate the ASL parser and abstract syntax tree (OTT file)
  - libASL/asl_visitor.ml - code to traverse abstract syntax tree
  - libASL/asl_utils.ml - code to transform abstract syntax tree
- Typechecker
  - libASL/tcheck.ml - typechecker
- Interpreter
  - libASL/primops.ml - implementation of ASL builtin types and operations
  - libASL/value.ml - interpreter support code
  - libASL/eval.ml - evaluator for ASL language
- ASL standard library
  - libASL/prelude.asl - builtin types and functions
- Programs
  - bin/asli.ml - interactive ASL tool
  - bin/testlexer.ml - test program that converts ASL code to list of tokens
- Misc
  - libASL/utils.ml - utility code
Code copied from other open source projects
- libASL/visitor.ml

Installing dependencies

Platform specific instructions:

    MacOS:
        brew install opam
        brew install gmp mpir
    Ubuntu:
        sudo apt-get install opam

Platform independent instructions:

    opam install ocaml.4.09.0
    opam install dune
    opam install menhir
    opam install ott
    opam install linenoise
    opam install pprint
    opam install z3.4.7.1
    opam install zarith

    # the following are optional and only needed if modifying asli code
    opam install odoc
    opam install ocamlformat

    # On OSX, you may need to use this command to install zarith
    env CFLAGS="-I$HOME/homebrew/include/" LDFLAGS="-L$HOME/homebrew/lib/" opam install zarith

    eval `opam config env`

You also need to execute this command

    MacOS: export DYLD_LIBRARY_PATH=`opam config var z3:lib`
    Linux: export LD_LIBRARY_PATH=`opam config var z3:lib`

Building

To build the ASL lexer and ASL interpreter, execute this command.

    make install

If you get a lot of linker errors involving Z3, double-check that you installed
the right version.

Using ASL lexer

This displays a list of tokens in an ASL file including the indent
and dedent tokens used to support indentation-based parsing.

    $ dune exec bin/testlexer.exe prelude.asl

Using ASL interpreter

This reads ASL files specified on the command line and
provides an interactive environment for executing ASL
statements and expressions.

    $ asli
                _____  _       _    ___________________________________
        /\     / ____|| |     (_)   ASL interpreter
       /  \   | (___  | |      _    Copyright Arm Limited (c) 2017-2019
      / /\ \   \___ \ | |     | |
     / ____ \  ____) || |____ | |   Version 0.1.1 alpha
    /_/    \_\|_____/ |______||_|   ___________________________________

    Type :? for help
    ASLi> 1+1
    2
    ASLi> ZeroExtend('11', 32)
    '00000000000000000000000000000011'
    ASLi> bits(32) x = ZeroExtend('11', 32);
    ASLi> x
    '00000000000000000000000000000011'
    ASLi> :quit

Using ASL interpreter with Arm's public specifications

You can download Arm's v8-A architecture specification at
https://developer.arm.com/architectures/cpu-architecture/a-profile/exploration-tools.
Historically, these are updated every 6 months with the latest "8.x" release
released in December.
You can download tools to unpack Arm's specification from
https://github.com/alastairreid/mra_tools.

Clone the MRA tools release and follow the instructions to unpack Arm's
specification.
In the following, I will assume that this is in directory "../mra_tools".

    # follow the instructions in ../mra_tools/README.md for downloading the Arm specs
    make -C ../mra_tools clean
    make -C ../mra_tools
    make install
    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

After loading the v8.6-A architecture spec, you can configure the
implementation defined behaviour, load an ELF file and run the
program as follows.

    :project tests/test.prj
    :quit

The test program prints the line "Test" so you should see output like this

ASLi> :project tests/test.prj
Loading ELF file tests/test_O2.elf.
Entry point = 0x400168
Test
Program exited by writing ^D to TUBE
Exception taken

Enjoy!