From 4cd2e3bdc28d744f41e99ff536daf138c72e0c04 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 10 Oct 2024 15:14:58 +1000 Subject: [PATCH] finish online docs? --- docs/online.md | 99 ++++++++++++++++++++++++++++++++-------------- docs/vectoriser.md | 3 ++ 2 files changed, 73 insertions(+), 29 deletions(-) diff --git a/docs/online.md b/docs/online.md index 05bd43c0..fc49d436 100644 --- a/docs/online.md +++ b/docs/online.md @@ -64,21 +64,52 @@ For instance, there are corresponding functions for expressions: val dis_expr : AST.l -> AST.expr -> sym rws val eval_expr : AST.l -> Env.t -> AST.expr -> value ``` -Here, the _'a rws_ return value is a computation inside the reader-writer-state monad: -``` +Here, the _'a rws_ return value is a computation inside the reader-writer-state monad (discussed below). + +The entry-point to the entire partial evaluator is the _dis\_core_ method. +This invokes the appropriate "dis" functions then performs a number of post-processing +transformations, described next. + +#### LocalEnv / DisEnv + +The LocalEnv structure stores and manipulates location-sensitive information during the +partial evaluation. +Most importantly, this includes the stack +mappings of variables to their concrete value or pure symbolic expression. +To facilitate easier debugging, this also manually records a stack of the +AST nodes currently being evaluated +(the ordinary stack trace is not useful in the presence of the monad abstraction). + +The DisEnv contains the _'a rws_ type — a reader-writer-state monad: +```ocaml type 'a rws = Eval.Env.t -> LocalEnv.t -> ('a, LocalEnv.t, stmt list) ``` This implements an abstraction for: - a read-only view of globals and constants ("eval env"), -- a mutable state with a mapping of variables to their concrete value or pure symbolic expression ("local env"), and +- a mutable LocalEnv state ("local env"), and - a write-only list of statements making up the residual program. -This mechanism is invoked in the `let@` and `let+` syntaxes -which composes RWS computations in a sensible way (explained more below, if desired). - -The entry-point to the entire partial evaluator is the _dis\_core_ method. -This invokes the appropriate "dis" functions then performs a number of post-processing -transformations, described next. +This mechanism is invoked by the `let@` and `let+` syntaxes +which composes RWS computations in a sensible way. +As an example, with many type annotations, consider +```ocaml +val int_is_zero : int rws -> bool rws = + fun (x : int rws) -> + let@ y : int = x in + DisEnv.pure (y = 0) +``` +Essentially, the `let@` notation has the function of "unwrapping" a rws computation +and placing it within another rws computation. +`let+` can be used where the final result (at the bottom of the let expression) +is a `DisEnv.pure` computation. +By using `let+`, the `DisEnv.pure` can be omitted. +Other functions exist to manipulate particular rws computations in particular ways +(e.g. a list of rws can become a rws of list). + +The DisEnv struct also contains methods to retrieve variables +(searching the local bindings and then the global bindings), +all returning rws computations. +To emit a statement into the residual program, it provides a `write` function. ### transforms.ml @@ -88,28 +119,38 @@ Some of these are conventional compiler transformations (e.g. removing unused variables, common subexpression factoring, and copy-propagation). The majority, however, are designed to address deficiencies (verbosity or unsupported constructs) in the residual program. -We discuss a few transformations which are of particular interest. - -## StatefulIntToBits / IntToBits - -This transformation converts expressions involving arbitrary-precision integers -into expressions of fixed-length bitvectors -by way of an interval analysis. - -The StatefulIntToBits modules implements this through an abstract interpretation -with an abstract domain of $\text{Width}\times \text{IsSigned} \times \mathbb Z^2$ - - - - - +We list a few transformations which are of particular interest. + +- StatefulIntToBits / IntToBits: + This transformation converts expressions involving arbitrary-precision integers + into expressions of fixed-length bitvectors + by way of an interval analysis. + + The StatefulIntToBits modules implements this through abstract interpretation + with a domain of $\text{Width}\times \text{IsSigned} \times \mathbb Z^2$, + recording bit-width, signedness, and lower and upper bounds. + +- RedundantSlice: Eliminates slice operations which do not reduce the bit-width. + Crucially, this is also responsible for converting slices with non-static indices + into shift/truncate operations. +- bits_coerce_narrow: Pushes slices into sub-expressions where possible. +- CaseSimp: Removes unreachable assertions placed after exhaustive case checks. +- RemoveRegisters: Replaces expressions of ASL's register type with ordinary bit-vectors. +- CopyProp +- CommonSubExprElim +- RemoveUnused ## Grammar -## Supporting +The ASL grammar is defined in [asl.ott](/libASL/asl.ott). +The ott program translates this into a Menhir grammar +which then generates a parser and an associated Ocaml AST. +The generated code modules include Asl_ast, Asl_parser, and Asl_parser_pp. + -- asl_ast (auto-generated) -- monads -- asl\_utils -- utils +For printing AST nodes and other structures, functions beginning with `pp_` are available +in [asl_utils.ml](/libASL/asl_utils.ml) and [utils.ml](/libASL/utils.ml). +These will produce an indented human-readable string. +To emit AST nodes in the structured "aslt" format, +use `Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt)` or similar. diff --git a/docs/vectoriser.md b/docs/vectoriser.md index e69de29b..11af4184 100644 --- a/docs/vectoriser.md +++ b/docs/vectoriser.md @@ -0,0 +1,3 @@ +# vectoriser + +todo