Getting started with ASLRef

Disclaimer

This material covers both ASLv0 (viz, the existing ASL pseudocode language which appears in the Arm Architecture Reference Manual) and ASLv1, a new, experimental, and as yet unreleased version of ASL.

This material is work in progress, more precisely at pre-Alpha quality as per Arm’s quality standards. In particular, this means that it would be premature to base any production tool development on this material.

However, any feedback, question, query and feature request would be most welcome; those can be sent to Arm’s Architecture Formal Team Lead Jade Alglave <jade.alglave@arm.com> or by raising issues or PRs to the herdtools7 github repository.

Installation

Pre-requisites

The following steps have been tested on Unix.

1. Install ocaml and opam (ocaml package manager), see the manual. For example on MacOS:

     $ brew install opam

2. Install dependencies:

     $ opam install dune menhir zarith

Building

1. Clone herdtools7:

     $ git clone https://github.com/herd/herdtools7.git

2. Build and install into a location $PREFIX:

     $ make build install PREFIX=$PREFIX

It's done!

Checking

If $PREFIX is in your $PATH, the following command should return a similar output:

  $ aslref --version
  aslref version 7.56+03 rev 7aa9d1f3cee2598ec64f14372f210e008ac5510f

Please note that building herdtools7 depends on the installation path $PREFIX. If you want to move your installation from $OLD_PREFIX to $NEW_PREFIX, please use:

  make uninstall PREFIX=$OLD_PREFIX
  make build install PREFIX=$NEW_PREFIX

Running

Basics

If my-test.asl contains a valid ASL specification returning 0, the tool aslref does not print anything and exit with code 0.

  $ aslref my-test.asl

Version and type-checking flags

For a complete reference of arguments, see aslref --help.

ASL Version

To use the ASLv0 parser, use the -0 flag.

The default parser is the ASLv1, but you can still specify it with -1.

Type-checking

There are currently three possible type-checking settings, listed here from the strongest to the weakest:

1. --type-check-strict fails on the first error encountered while type-checking the specification. This is the default setting for ASLv1.
2. --type-check-warn logs every error on the standard error output, but does not fail on any of them. The specification might not be able to run through the interpreter if the type-checking phase failed.
3. --no-type-check only performs minimal type-inference. Tries to fail as little as possible. This is the default for ASLv0.

Examples

You can find examples of ASLv1 specifications that aslref supports in herdtools7/asllib/tests/asl/required.

Building HTML pages locally from .mld files

In the directory herdtools7/:

1. Run:

     $ dune build @doc

1. Open _build/default/_doc/_html/herdtools7/aslref.html

Contributing examples and regression tests

We welcome new examples to add to both the ASL Semantics and Typing Reference Documents. We use those examples as regression tests also. Therefore, please make sure that each example which appears in an ASL Reference Document also appears in the corresponding asllib test suite, as follows.

Contributing examples to the ASL Semantics Reference document and regression suite

In asllib/tests/ASLSemanticsReference.t:

• add a new example SemanticsRule.MyNewTest.asl;
• edit run.t to mention SemanticsRule.MyNewTest.asl.

In herdtools7:

• do: dune runtest asllib
• if the tests pass, do: dune promote

In asllib/ASLSemanticsReference.mld

• add a new section titled SemanticsRule.MyNewTest.asl;
• add a comment about how the test should behave and why.

Contributing examples to the ASL Typing Reference document and regression suite

In asllib/tests/ASLTypingReference.t:

• add a new example TypingRule.MyNewTest.asl;
• edit run.t to mention TypingRule.MyNewTest.asl.

In herdtools7:

• do: dune runtest asllib
• if the tests pass, do: dune promote

In asllib/ASLTypingReference.mld

• add a new section titled TypingRule.MyNewTest.asl;
• add a comment about how the test should behave and why.