aslt changes + grammar + testing

[katrinafyi]

This PR will aim to address some inconveniences in the current aslt format (i.e. that from the AST's pp_raw methods). This should make the syntax more similar to a regular programming language (in particular, Python) and hence easier to parse with a variety of generic tools.

In the format itself,

• [x] Format integer literals with a prefix (e.g. 0x) and without wrapping in Expr_Lit*.
  • [ ] Possibly, strip non-digit characters when emitting.
• [x] Wrap identifiers (e.g. function identifiers) in double quotes, denoting them as strings.
• [x] Format else branches consistently (done in #51).
• [x] Investigate unnecessary parentheses.
• [x] Investigate use of space and semicolon delimited lists.

In the ANTLR grammar,

• [x] Update grammar with these changes.
• [x] Maintain a reference version of the grammar within this repository (#45).

In downstream projects,

• [x] Update downstream users to support the new format (https://github.com/UQ-PAC/bil-to-boogie-translator/pull/197)

[mmcloughlin]

In case it's of interest, I'm working on a Rust parser for ASLT (based on pest). It's a work in progress but it parses a reasonable subset right now.

[katrinafyi]

@mmcloughlin, that is interesting! Do you have plans to make use of ASLp for a verification project?

[mmcloughlin]

Do you have plans to make use of ASLp for a verification project?

Potentially, yes. I'm trying to see if it will work for our use case at the moment. The ASLT format is quite convenient.

The other thing we'll probably need is symbolic opcodes #52.

[mmcloughlin]

I've updated my Rust parser to support these new changes. All works fine.

[katrinafyi]

With the go-ahead of the Basil PR, this is scheduled for merge next Monday.

[katrinafyi]

@ncough Are the changes in this diff to be expected? It looks like some more CSE and some distributivity simplifications have been added?

[ncough]

Yeah, these should correspond to some simplifications over mul_int and add_int that were necessary to reduce bitvector slices down to a constant width. Given the resulting CSE mess, I may consider an alternative approach down the line. Nice to have this testing!