package libsail

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Target type and accessor functions
Target registration

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Infix_parser
    
    Incremental
    
    MenhirInterpreter
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    CONFIG
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Jib_visitor
    
    empty_jib_visitor
    
    jib_visitor
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
    
    PC
    
    PC_config
  - Smt_exp
  - Smt_gen
    
    CONFIG
    
    Make
    
    Config
    
    Primop_gen
    
    PRIMOP_GEN
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_env
  - Type_error
  - Type_internal
  - Util
    
    Duplicate
  - Value
    
    StringMap
  - Value2
  - Visitor

Legend:
Library
Module
Module type
Parameter
Class
Class type

Infrastructure for plugins to register Sail targets.

A target is essentially a custom backend for the Sail compiler, along with various hooks and options that toggle various frontend behaviours. A target therefore specifies what kind of output Sail will produce. For example, we provide default plugins that define targets to output Lem, C, OCaml, Coq, and so on.

Target type and accessor functions

type target

val name : target -> string

val run_pre_parse_hook : target -> unit -> unit

val run_pre_rewrites_hook : 
  target ->
  Type_check.tannot Ast_defs.ast ->
  Effects.side_effect_info ->
  Type_check.Env.t ->
  unit

val rewrites : target -> Rewrites.rewrite_sequence

val action : 
  target ->
  Yojson.Basic.t option ->
  string ->
  string option ->
  Type_check.tannot Ast_defs.ast ->
  Effects.side_effect_info ->
  Type_check.Env.t ->
  unit

val asserts_termination : target -> bool

Target registration

val register : 
  name:string ->
  ?flag:string ->
  ?description:string ->
  ?options:(Stdlib.Arg.key * Stdlib.Arg.spec * Stdlib.Arg.doc) list ->
  ?pre_parse_hook:(unit -> unit) ->
  ?pre_rewrites_hook:
    (Type_check.tannot Ast_defs.ast ->
      Effects.side_effect_info ->
      Type_check.Env.t ->
      unit) ->
  ?rewrites:(string * Rewrites.rewriter_arg list) list ->
  ?asserts_termination:bool ->
  (Yojson.Basic.t option ->
    string ->
    string option ->
    Type_check.tannot Ast_defs.ast ->
    Effects.side_effect_info ->
    Type_check.Env.t ->
    unit) ->
  target

Used for plugins to register custom Sail targets/backends.

register_target ~name:"foo" action will create an option -foo, that will run the provided action on the Sail abstract syntax tree after performing common frontend processing.

The various arguments can be used to further control the behavior of the target:

parameter ~name
The name of the target

parameter ?flag
A custom command line flag to invoke the target. By default it will use the name parameter

parameter ?description
A custom description for the command line flag

parameter ?options
Additional options for the Sail executable

parameter ?pre_parse_hook
A function to call right at the start, before parsing

parameter ?pre_rewrites_hook
A function to call before doing any rewrites

parameter ?rewrites
A sequence of Sail to Sail rewrite passes for the target

parameter ?asserts_termination
Whether termination measures are enforced by assertions in the target
The final unnamed parameter is the main backend function that is called after the frontend has finished processing the input.

val get_the_target : unit -> target option

Return the current target. For example, if we register a 'coq' target, and Sail is invoked with `sail -coq`, then this function will return the coq target.

val get : name:string -> target option

val extract_options : 
  unit ->
  (Stdlib.Arg.key * Stdlib.Arg.spec * Stdlib.Arg.doc) list

Used internally to dynamically update the option list when loading plugins