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.
The following steps have been tested on Unix.
Install ocaml and opam (ocaml package manager), see the manual. For example on MacOS:
$ brew install opamInstall dependencies:
$ opam install dune menhir zarithClone herdtools7:
$ git clone https://github.com/herd/herdtools7.gitBuild and install into a location $PREFIX:
$ make build install PREFIX=$PREFIXIt's done!
If $PREFIX is in your $PATH, the following command should return a similar output:
$ aslref --version
+ASLRefREADME (herdtools7.ASLRefREADME) 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.
Install ocaml and opam (ocaml package manager), see the manual. For example on MacOS:
$ brew install opam
Install dependencies:
$ opam install dune menhir zarith
Building
Clone herdtools7:
$ git clone https://github.com/herd/herdtools7.git
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 program 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:
--type-check-strict fails on the first error encountered while type-checking the program. This is the default setting for ASLv1.--type-check-warn logs every error on the standard error output, but does not fail on any of them. The program might not be able to run through the interpreter if the type-checking phase failed.--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 programs that aslref supports in herdtools7/asllib/tests/asl/required.
\ No newline at end of file
+make build install PREFIX=$NEW_PREFIXIf my-test.asl contains a valid ASL program returning 0, the tool aslref does not print anything and exit with code 0.
$ aslref my-test.aslFor a complete reference of arguments, see aslref --help.
To use the ASLv0 parser, use the -0 flag.
The default parser is the ASLv1, but you can still specify it with -1.
There are currently three possible type-checking settings, listed here from the strongest to the weakest:
--type-check-strict fails on the first error encountered while type-checking the program. This is the default setting for ASLv1.--type-check-warn logs every error on the standard error output, but does not fail on any of them. The program might not be able to run through the interpreter if the type-checking phase failed.--no-type-check only performs minimal type-inference. Tries to fail as little as possible. This is the default for ASLv0.You can find examples of ASLv1 programs that aslref supports in herdtools7/asllib/tests/asl/required.
In the directory herdtools7/:
Run:
$ dune build @doc_build/default/_doc/_html/herdtools7/aslref.htmlThis 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.
Typing a program is typing its main function. Constructively, typing a program requires following its Abstract Syntax Tree and typing each of its components.
Formally, the types of a program are given by applying a set of annotate_<object> functions. Each annotate_<object> function describes how to annotate a specific object, as follows.
annotate_expr annotates expressions;annotate_slices annotates slices;annotate_pattern annotates pattern;annotate_local_decl_item annotates local declarations;annotate_lexpr annotates left-hand sides of assignments;annotate_stmt annotates statements;annotate_block annotates blocks;annotate_catcher annotates catchers;annotate_call annotates functions calls;annotate_func annotates functions.check_binop op t1 t2 checks that the types t1 and t2 are valid for the operation op, as is defined in chapter 7 of the Language Reference Manual.check_unop op t checks that the type t is valid for the operation op, as defined in chapter 7 of the Language Reference Manual.annotate_expr specifies how to annotate an expression e in an environment env. Formally, the result of annotating the expression e in env is t,new_e and one of the following applies:
All of the following applies:
e is a Literal v;t is the type of v;new_e is e.All of the following applies:
e is a typed expression (e',t');t'',e'' is the result of annotating e' in env;t'' is a structural subtype of t' in env;t'' is a domain subtype of t' in env;t is t';new_e is e''.t'' is a structural subtype of t' in env;t'' is not a domain subtype of t' in env;t'' is not a structural subtype of t' in env;All of the following applies:
e is a variable x;x maps to a type ty in the storage_types of the local environment given by env;x maps to a local constant v;t is ty;new_e is the Literal v.All of the following applies:
e is a variable x;x maps to a type ty in the storage_types of the local environment given by env;x does not map to a local constant;t is ty;new_e is e.All of the following applies:
e is a variable x;x maps to a type ty in the constant_values of the global environment given by env;x maps to a global constant;x maps to a value v;t is ty;new_e is E_Literal v.All of the following applies:
e is a variable x;x maps to a type ty in the constant_values of the global environment given by env;x does not map to a global constant;t is ty;new_e is e.All of the following applies:
e is a variable x;x is not bound in env;All of the following applies:
e denotes a binary operation op over two expressions e1 and e2;t1,e1' is the result of annotating e1 in env;t2,e2' is the result of annotating e2 in env;t is the result of checking compatibility of op with t1 and t2;new_e denotes op over e1' and e2'.All of the following applies:
e denotes a unary operation op over an expression e';t'',e'' is the result of annotating e' in env;t is the result of checking compatibility of op with t'';new_e denotes op over e''.All of the following applies:
e denotes a condition e_cond with two options e_true and e_false;t_cond, e'_cond is the result of annotating e_cond in env;t_true, e'_true is the result of annotating e_true in env;t_false, e'_false is the result of annotating e_false in env;t is the lowest common ancestor of t_true and t_false;new_e is the condition e'_cond with two options e'_true and e'_false.t_true and t_false;All of the following applies:
e denotes a tuple li;ts, es is the result of annotating in env each expression in li;t is ts;new_e is es.All of the following applies:
e denotes the empty concatenation;t is bits(0);new_e is e.All of the following applies:
e denotes the concatenation of a non-empty list of expressions li;ts, es is the result of annotating li in env;w is the sum of the widths of the bitvector types ts;t is bits(w);new_e is es.All of the following applies:
e denotes the record expression of type ty with fields fields;ty is neither a record nor an exception type;All of the following applies:
e denotes the record expression of type ty with fields fields;ty is the name of a record type with fields field_types;field_types is not initialised by fields;All of the following applies:
e denotes the record expression of type ty with fields fields;ty is the name of a record type with fields field_types;name associated with the expression e' in field_types, all of the following applies:t',e'' is the result of annotating e' in env;t_spec' is the type associated to name in field_types;t' type-satisfies t_spec';fields' associates name to e'';t is ty;new_e is the record expression of type ty with fields fields'.All of the following applies:
e denotes a call to a function named name with arguments args and parameters eqs;name', args', eqs', ty is the result of annotating the call of that function in env;t is ty;new_e is the call the function named name' with arguments args' and parameters eqs'.All of the following applies:
e denotes an unknown expression of type ty;ty' is the structure of ty in env;t is ty;new_e is an unknown expression of type ty'.All of the following applies:
e denotes the slicing of expression e' by the slices slices;t_e',e' is the result of annotating the expression e' in env;t_e' has the structure of an integer or a bitvector;w is the width of slices;slices' is the result of annotating slices in env;t is the bitvector type of width w;new_e is the slicing of expression e' by the slices slices'.All of the following applies:
e denotes the slicing of expression e' by the slices slices;t_e',e' is the result of annotating the expression e' in env;t_e' has the structure of an array of size size and type t;wanted_t_index is an enumeration type of name size;wanted_t_index is the type integer {0..size-1};slices is single expression e_index;t_index', e_index' is the result of annotating e_index in env;t_index' type-satisfies wanted_t_index;new_e is an access to array e' at index e_index'.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is an Exception or a Record type with fields fields;field_name is not declared in fields;field_name is declared in fields;t is the type corresponding to field_name in fields;new_e is the access of field field_name on expression e2.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is not declared in bitfields;All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;e3 denotes the slicing of the expression e2 by the slices slices;t,new_e is the result of annotating e3.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;e3 denotes the slicing of the expression e2 by the slices slices;t4, e4 is the result of annotating e3 in env;bitfields' gives the bitfields corresponding to the bitfield field_name in bitfields;t is the bitvector type with the width of t4 and the bitfields bitfields'new_e is e4.All of the following applies:
e denotes e1, field_name;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;t_e3,e3 is the result of annotating e2,slices in env;t gives the type corresponding to the bitfield field_name in bitfields;t_e3 type-satisfies t in env;new_e is e3.<description>
<minimal example>
All of the following applies:
e denotes whether the expression e' matches patterns;t_e', e'' is the result of annotating e' in env;patterns' is the result of annotating patterns in env;t is boolean;new_e denotes whether the expression e'' matches patterns'.annotate_lexpr version env le t_e is new_le and one of the following applies:
All of the following applies:
le denotes an expression which can be ignored;new_le is le.All of the following applies:
le denotes a local variable x of type ty;x is locally declared as a variable of type ty in env;new_le is le.All of the following applies:
le denotes a tuple les;t_e denotes a tuple type sub_tys;les and sub_tys have the same length;new_le is the result of annotating les with sub_tys in envles and sub_tys do not have the same length;<description>
<minimal example>
annotate_local_decl_item loc env ty ldk ldi is new_env, new_ldi and one of the following applies:
All of the following applies:
ldi is a local declaration which can be ignored;new_env is env;new_ldi is ldi.All of the following applies:
ldi is a local declaration which can be ignored;t is given;t can be initialised with ty in env;new_env is env;new_ldi is ldi.t cannot be initialised with ty in env;All of the following applies:
ldi denotes a variable x with an optional type ty_opt;x is not declared in env;ty_opt is None;t is tyty_opt is Some t;t can be initialized with ty in env;new_env is env modified so that x is locally declared of type t;new_ldi is the declaration of variable x with type t.All of the following applies:
ldi denotes a singleton list ld;new_env, new_ldi is the result of annotating the local declaration ld with ty in env.annotate_stmt env s is <description> and one of the following applies:
<description>
<minimal example>
<minimal example>
annotate_slices env slices is <description> Formally, one of the following applies:
annotate_pattern env pos v p is <description>. Formally, one of the following applies:
annotate_block env stm is <description>.
<minimal example>
annotate_catchers env catchers otherwise_opt s_m
<description>
<minimal example>
annotate_call pos name env args named_args annotates the call to function name with arguments args and parameters named_args.
<description>
At the begining of a program, the interpreter annotates the function "main".
annotate_func genv name pos actual_args params annotates the function named name <description> and one of the following applies:
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.
Typing a program is typing its main function. Constructively, typing a program requires following its Abstract Syntax Tree and typing each of its components.
Formally, the types of a program are given by applying a set of annotate_<object> functions. Each annotate_<object> function describes how to annotate a specific object, as follows.
annotate_expr annotates expressions;annotate_slices annotates slices;annotate_pattern annotates pattern;annotate_local_decl_item annotates local declarations;annotate_lexpr annotates left-hand sides of assignments;annotate_stmt annotates statements;annotate_block annotates blocks;annotate_catcher annotates catchers;annotate_call annotates functions calls;annotate_func annotates functions.check_binop op t1 t2 checks that the types t1 and t2 are valid for the operation op, as is defined in chapter 7 of the Language Reference Manual.check_unop op t checks that the type t is valid for the operation op, as defined in chapter 7 of the Language Reference Manual.annotate_expr specifies how to annotate an expression e in an environment env. Formally, the result of annotating the expression e in env is t,new_e and one of the following applies:
All of the following applies:
e is a Literal v;t is the type of v;new_e is e.All of the following applies:
e is a typed expression (e',t');t'',e'' is the result of annotating e' in env;t'' is a structural subtype of t' in env;t'' is a domain subtype of t' in env;t is t';new_e is e''.t'' is a structural subtype of t' in env;t'' is not a domain subtype of t' in env;t'' is not a structural subtype of t' in env;All of the following applies:
e is a variable x;x maps to a type ty in the storage_types of the local environment given by env;x maps to a local constant v;t is ty;new_e is the Literal v.All of the following applies:
e is a variable x;x maps to a type ty in the storage_types of the local environment given by env;x does not map to a local constant;t is ty;new_e is e.All of the following applies:
e is a variable x;x maps to a type ty in the constant_values of the global environment given by env;x maps to a global constant;x maps to a value v;t is ty;new_e is E_Literal v.All of the following applies:
e is a variable x;x maps to a type ty in the constant_values of the global environment given by env;x does not map to a global constant;t is ty;new_e is e.All of the following applies:
e is a variable x;x is not bound in env;All of the following applies:
e denotes a binary operation op over two expressions e1 and e2;t1,e1' is the result of annotating e1 in env;t2,e2' is the result of annotating e2 in env;t is the result of checking compatibility of op with t1 and t2;new_e denotes op over e1' and e2'.All of the following applies:
e denotes a unary operation op over an expression e';t'',e'' is the result of annotating e' in env;t is the result of checking compatibility of op with t'';new_e denotes op over e''.All of the following applies:
e denotes a condition e_cond with two options e_true and e_false;t_cond, e'_cond is the result of annotating e_cond in env;t_true, e'_true is the result of annotating e_true in env;t_false, e'_false is the result of annotating e_false in env;t is the lowest common ancestor of t_true and t_false;new_e is the condition e'_cond with two options e'_true and e'_false.t_true and t_false;All of the following applies:
e denotes a tuple li;ts, es is the result of annotating in env each expression in li;t is ts;new_e is es.All of the following applies:
e denotes the empty concatenation;t is bits(0);new_e is e.All of the following applies:
e denotes the concatenation of a non-empty list of expressions li;ts, es is the result of annotating li in env;w is the sum of the widths of the bitvector types ts;t is bits(w);new_e is es.All of the following applies:
e denotes the record expression of type ty with fields fields;ty is neither a record nor an exception type;All of the following applies:
e denotes the record expression of type ty with fields fields;ty is the name of a record type with fields field_types;field_types is not initialised by fields;All of the following applies:
e denotes the record expression of type ty with fields fields;ty is the name of a record type with fields field_types;name associated with the expression e' in field_types, all of the following applies:t',e'' is the result of annotating e' in env;t_spec' is the type associated to name in field_types;t' type-satisfies t_spec';fields' associates name to e'';t is ty;new_e is the record expression of type ty with fields fields'.All of the following applies:
e denotes a call to a function named name with arguments args and parameters eqs;name', args', eqs', ty is the result of annotating the call of that function in env;t is ty;new_e is the call the function named name' with arguments args' and parameters eqs'.All of the following applies:
e denotes an unknown expression of type ty;ty' is the structure of ty in env;t is ty;new_e is an unknown expression of type ty'.All of the following applies:
e denotes the slicing of expression e' by the slices slices;t_e',e' is the result of annotating the expression e' in env;t_e' has the structure of an integer or a bitvector;w is the width of slices;slices' is the result of annotating slices in env;t is the bitvector type of width w;new_e is the slicing of expression e' by the slices slices'.All of the following applies:
e denotes the slicing of expression e' by the slices slices;t_e',e' is the result of annotating the expression e' in env;t_e' has the structure of an array of size size and type t;wanted_t_index is an enumeration type of name size;wanted_t_index is the type integer {0..size-1};slices is a single expression e_index;t_index', e_index' is the result of annotating e_index in env;t_index' type-satisfies wanted_t_index;new_e is an access to array e' at index e_index'.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is an Exception or a Record type with fields fields;field_name is declared in fields;t is the type corresponding to field_name in fields;new_e is the access of field field_name on expression e2.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is an Exception or a Record type with fields fields;field_name is not declared in fields;All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is not declared in bitfields;All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e1 does not have the structure of a record or an exception or a bitvector type;All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;e3 denotes the slicing of the expression e2 by the slices slices;t,new_e is the result of annotating e3.All of the following applies:
e denotes the access of field field_name on expression e1;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;e3 denotes the slicing of the expression e2 by the slices slices;t4, e4 is the result of annotating e3 in env;bitfields' gives the bitfields corresponding to the bitfield field_name in bitfields;t is the bitvector type with the width of t4 and the bitfields bitfields'new_e is e4.All of the following applies:
e denotes e1, field_name;t_e1, e2 is the result of annotating e1 in env;t_e2 is the anonymous type corresponding to t_e1 in env;t_e2 is a bitvector type with bitfields bitfields;field_name is declared in bitfields;slices gives the slices corresponding to the bitfield field_name in bitfields;t_e3,e3 is the result of annotating e2,slices in env;t gives the type corresponding to the bitfield field_name in bitfields;t_e3 type-satisfies t in env;new_e is e3.<description>
<minimal example>
All of the following applies:
e denotes whether the expression e' matches patterns;t_e', e'' is the result of annotating e' in env;patterns' is the result of annotating patterns in env;t is boolean;new_e denotes whether the expression e'' matches patterns'.annotate_lexpr version env le t_e is new_le and one of the following applies:
All of the following applies:
le denotes an expression which can be ignored;new_le is le.All of the following applies:
le denotes a local variable x of type ty;x is locally declared as a variable of type ty in env;new_le is le.All of the following applies:
le denotes a tuple les;t_e denotes a tuple type sub_tys;les and sub_tys have the same length;new_le is the result of annotating les with sub_tys in envles and sub_tys do not have the same length;All of the following applies:
le denotes the slicing of a left-hand-side expression le1 by the slices slices;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;t_le1 has the structure of a bitvector type;le2 is the result of annotating le1 in env;width is the width of the slices slices in env;t is the bitvector type of width width;slices2 is the result of annotating slices in env;new_le is the slicing of le2 by slices2.All of the following applies:
le denotes the slicing of a left-hand-side expression le1 by the slices slices;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;t_le1 has the structure of an array type of size size and item type t;le2 is the result of annotating le1 in env;wanted_t_index is an enumeration type of name size;wanted_t_index is the type integer {0..size-1};slices is a single expression e_index;t_index', e_index' is the result of annotating e_index in env;t_index' type-satisfies wanted_t_index;new_le is an access to array le2 at index e_index'.All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of an exception or a record type with fields fields;field is not declared in fields;All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of an exception or a record type with fields fields;field is bound to type t in fields;t_e type-satisfies t;new_le is the access to the field field in le2.All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of a bitvector with bitfields bitfields;field is not declared in bitfields;All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of a bitvector with bitfields bitfields;field is declared in bitfields;slices gives the slices corresponding to the bitfield field in bitfields;w is the width of slices;t is the bitvector type of width w;t_e type-satisfies t;le2 is the slicing of le1 by slices;new_le is the result of annotating le2 in env.All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of a bitvector with bitfields bitfields;slices gives the slices corresponding to the bitfield field in bitfields;w is the width of slices;bitfields' gives the bitfields corresponding to field in bitfields;t is the bitvector type of width w and bitfields bitfields';t_e type-satisfies t;le2 is the slicing of le1 by slices;new_le is the result of annotating le2 in env.All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 has the structure of a bitvector with bitfields bitfields;slices gives the slices corresponding to the bitfield field in bitfields;w is the width of slices;t' is the bitvector type of width w;t gives the type corresponding to the bitfield field in bitfields;t' type-satisfies t;t_e type-satisfies t;le2 is the slicing of le1 by slices;new_le is the result of annotating le2 in env.All of the following applies:
le denotes the access to the field named field in le1;t_le1 is the type result of annotating the right-hand-side expression corresponding to le1 in env;le2 is the result of annotating le1 in env;t_le1 does not have the structure of a record, or an exception or a bitvector type;annotate_local_decl_item loc env ty ldk ldi is new_env, new_ldi and one of the following applies:
All of the following applies:
ldi is a local declaration which can be ignored;new_env is env;new_ldi is ldi.All of the following applies:
ldi is a local declaration which can be ignored;t is given;t can be initialised with ty in env;new_env is env;new_ldi is ldi.t cannot be initialised with ty in env;All of the following applies:
ldi denotes a variable x with an optional type ty_opt;x is not declared in env;ty_opt is None;t is tyty_opt is Some t;t can be initialized with ty in env;new_env is env modified so that x is locally declared of type t;new_ldi is the declaration of variable x with type t.All of the following applies:
ldi denotes a singleton list ld;new_env, new_ldi is the result of annotating the local declaration ld with ty in env.annotate_stmt env s is <description> and one of the following applies:
<description>
<minimal example>
<minimal example>
annotate_slices env slices is <description> Formally, one of the following applies:
annotate_pattern env pos v p is <description>. Formally, one of the following applies:
annotate_block env stm is <description>.
<minimal example>
annotate_catchers env catchers otherwise_opt s_m
<description>
<minimal example>
annotate_call pos name env args named_args annotates the call to function name with arguments args and parameters named_args.
<description>
At the begining of a program, the interpreter annotates the function "main".
annotate_func genv name pos actual_args params annotates the function named name <description> and one of the following applies:
Instrumentation.TypingRuletype t = | Lit| TypedExpr| ELocalVarConstant| ELocalVar| EGlobalVarConstantVal| EGlobalVarConstantNoVal| EGlobalVar| EUndefIdent| Binop| Unop| ECondSimple| ECond| ESlice| ECall| EGetArray| ERecord| ERecordMissingField| ERecordNotARecord| EGetRecordField| EGetBitField| EGetBadBitField| EGetBitFieldNested| EGetBitFieldTyped| EGetBitFields| EConcatEmpty| EConcat| ETuple| EUnknown| EPattern| LEIgnore| LELocalVar| LEGlobalVar| LEUndefIdentV0| LEUndefIdentV1| LESlice| LESetArray| LESetField| LESetFields| LETuple| PAll| PAny| PGeq| PLeq| PNot| PRange| PSingle| PMask| PTuple| LDIgnoreNone| LDIgnoreSome| LDUninitialisedVar| LDUninitialisedTypedVar| LDVar| LDTypedVar| LDUninitialisedTuple| LDUninitialisedTypedTuple| LDTuple| LDTypedTuple| SPass| SAssignCall| SAssignTuple| SAssign| SReturnOne| SReturnSome| SReturnNone| SThen| SCall| SCond| SCase| SAssert| SWhile| SRepeat| SFor| SThrowNone| SThrowSomeTyped| SThrowSome| STry| SDeclSome| SDeclNone| SDebug| FUndefIdent| FPrimitive| FBadArity| FCall| Block| Loop| For| SliceLength| SliceSingle| SliceRange| SliceStar| Catcher| Funcval to_string : t -> stringval pp : Stdlib.Format.formatter -> t -> unitval all : t listval index : t -> intval of_string : string -> tInstrumentation.TypingRuletype t = | Lit| TypedExpr| ELocalVarConstant| ELocalVar| EGlobalVarConstantVal| EGlobalVarConstantNoVal| EGlobalVar| EUndefIdent| Binop| Unop| ECondSimple| ECond| ESlice| ECall| EGetArray| ERecord| ERecordMissingField| ERecordNotARecord| EGetRecordField| EGetBitField| EGetBadField| EGetBadBitField| EGetBadRecordField| EGetBitFieldNested| EGetBitFieldTyped| EGetBitFields| EConcatEmpty| EConcat| ETuple| EUnknown| EPattern| LEIgnore| LELocalVar| LEGlobalVar| LEUndefIdentV0| LEUndefIdentV1| LETuple| LESlice| LESetArray| LESetBadRecordField| LESetRecordField| LESetBadBitField| LESetBitField| LESetBitFieldNested| LESetBitFieldTyped| LESetBadField| LESetFields| LEConcat| PAll| PAny| PGeq| PLeq| PNot| PRange| PSingle| PMask| PTuple| LDIgnoreNone| LDIgnoreSome| LDUninitialisedVar| LDUninitialisedTypedVar| LDVar| LDTypedVar| LDUninitialisedTuple| LDUninitialisedTypedTuple| LDTuple| LDTypedTuple| SPass| SAssignCall| SAssignTuple| SAssign| SReturnOne| SReturnSome| SReturnNone| SThen| SCall| SCond| SCase| SAssert| SWhile| SRepeat| SFor| SThrowNone| SThrowSomeTyped| SThrowSome| STry| SDeclSome| SDeclNone| SDebug| FUndefIdent| FPrimitive| FBadArity| FCall| Block| Loop| For| SliceLength| SliceSingle| SliceRange| SliceStar| Catcher| Funcval to_string : t -> stringval pp : Stdlib.Format.formatter -> t -> unitval all : t listval index : t -> intval of_string : string -> t