package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Library
Module
Module type
Parameter
Class
Class type

In Sail, we need to distinguish between pure and impure (side-effecting) functions. This is because there are few places, such as top-level let-bindings and loop termination measures where side effects must clearly be forbidden. This module implements inference for which functions are pure and which are effectful, and checking the above purity restrictions.

type side_effect

A function is side-effectful if it throws an exception, can exit abnormally (either via an assertion failing or an explicit exit statement), contains a (possibly) incomplete pattern match, or touches a register. Finally, it is transitively side-effectful if it calls another function doing any of the above.

module EffectSet : sig ... end
val throws : EffectSet.t -> bool
val pure : EffectSet.t -> bool
val effectful : EffectSet.t -> bool
val has_outcome : Ast.id -> EffectSet.t -> bool

Outcome identifiers correspond to the set of user-defined prompt monad constructors in the concurrency interface, replacing the various ad-hoc rmem, wmem, barrier, and so on effects in previous Sail versions. For example, using the concurrency interface in the Sail library, the equivalent to checking for the wmem effect would be:

has_outcome (mk_id "sail_mem_write_request") effects

type side_effect_info = {
  1. functions : EffectSet.t Ast_util.Bindings.t;
  2. letbinds : EffectSet.t Ast_util.Bindings.t;
  3. mappings : EffectSet.t Ast_util.Bindings.t;
}
val empty_side_effect_info : side_effect_info
val function_is_pure : Ast.id -> side_effect_info -> bool
val infer_side_effects : bool -> Type_check.tannot Ast_defs.ast -> side_effect_info

infer_side_effects asserts_termination ast infers all of the side effect information for ast. If asserts_termination is true then it is assumed that the backend will enforce the termination measures with assertions.

val check_side_effects : side_effect_info -> Type_check.tannot Ast_defs.ast -> unit

Checks constraints on side effects, raising an error if they are violated. Currently these are that termination measures and top-level letbindings must be pure.

val copy_function_effect : Ast.id -> side_effect_info -> Ast.id -> side_effect_info

copy_function_effect id_from info id_to copies the effect information from id_from to id_to in the side effect information. The order of arguments is to make it convenient to use with List.fold_left.

val copy_mapping_to_function : Ast.id -> side_effect_info -> Ast.id -> side_effect_info
val add_function_effect : Ast.id -> side_effect_info -> Ast.id -> side_effect_info

add_function_effect id_from info id_to adds the effect information from id_from to id_to in the side effect information, preserving any existing effects for id_to. The order of arguments is to make it convenient to use with List.fold_left.

val add_monadic_built_in : Ast.id -> side_effect_info -> side_effect_info

add_monadic_built_in id info notes that id is a monadic external function.

Previous code mostly assumes that side effect info is attached to nodes in the AST. To keep this code working, this rewrite pass attaches effect info into to the AST. Note that the effect info is simplified in its annotated form - it just becomes a boolean representing effectful/non-effectful

val dump_effects : side_effect_info -> unit

Dumps the given side effect information to stderr.