package libsail

  1. Overview
  2. Docs
module StringMap : sig ... end
val optimize_constant_fold : bool ref
val fexp_of_ctor : (Value.StringMap.key * Value.value) -> unit Ast.fexp
val exp_of_value : Value.value -> unit Ast.exp
val safe_primops : (Value.value list -> Value.value) StringMap.t
val opt_fold_to_unit : string list ref

We can specify a list of identifiers that we want to remove from the final AST here. This is useful for removing tracing features in optimized builds, e.g. for booting an OS as fast as possible.

Basically we just do this by mapping

f(x, y, z) -> ()

when f is in the list of identifiers to be mapped to unit. The advantage of doing it like this is if x, y, and z are computationally expensive then we remove them also. String concatentation is very expensive at runtime so this is something we really want when cutting out tracing features. Obviously it's important that they don't have any meaningful side effects, and that f does actually have type unit.

val fold_to_unit : Ast_util.IdSet.elt -> bool
val is_constant : Type_check.tannot Ast.exp -> bool
val is_constant_fexp : Type_check.tannot Ast.fexp -> bool

This rewriting pass looks for function applications (E_app) expressions where every argument is a literal. It passes these expressions to the OCaml interpreter in interpreter.ml, and reconstructs the values returned back into expressions which are then re-typechecked and re-inserted back into the AST.

We don't use the effect system to decide if expressions are safe to evaluate, because this ignores I/O, and would force us to ignore functions that maybe throw exceptions internally but as called are totally safe. Instead any exceptions during evaluation are caught, and the original expression is kept. Some causes of this could be:

  • Function tries to read/write register.
  • Calls an unsafe primop.
  • Throws an exception that isn't caught.
val no_fixed : fixed
val rw_exp : fixed -> string -> (unit -> 'a) -> (unit -> 'b) -> Interpreter.state -> Type_check.tannot Ast.exp -> Type_check.tannot Ast.exp
val rewrite_constant_function_calls' : fixed -> string -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast
val rewrite_constant_function_calls : fixed -> string -> Type_check.tannot Ast_defs.ast -> Type_check.tannot Ast_defs.ast
type to_constant =
  1. | Register of Ast.id * Ast.typ * Type_check.tannot Ast.exp
  2. | Register_field of Ast.id * Ast.id * Ast.typ * Type_check.tannot Ast.exp
OCaml

Innovation. Community. Security.