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.
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 ... endval throws : EffectSet.t -> boolval pure : EffectSet.t -> boolval effectful : EffectSet.t -> boolval has_outcome : Ast.id -> EffectSet.t -> boolOutcome 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 = {functions : EffectSet.t Ast_util.Bindings.t;letbinds : EffectSet.t Ast_util.Bindings.t;mappings : EffectSet.t Ast_util.Bindings.t;}val empty_side_effect_info : side_effect_infoval function_is_pure : Ast.id -> side_effect_info -> boolval infer_side_effects : bool -> Type_check.typed_ast -> side_effect_infoinfer_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.typed_ast -> unitChecks 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_infocopy_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_infoval add_function_effect :
Ast.id ->
side_effect_info ->
Ast.id ->
side_effect_infoadd_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_infoadd_monadic_built_in id info notes that id is a monadic external function.
val rewrite_attach_effects :
side_effect_info ->
Type_check.typed_ast ->
Type_check.typed_astPrevious 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 -> unitDumps the given side effect information to stderr.