Module Flags

Parsing of command line arguments

Workflow

Flags are separated based on the technique(s) they impact. Global flags are the ones that don't impact any technique, or impact all of them. Log flags, help flags, timeout flags... are global flags.

NB: when adding a boolean flag, make sure to parse its value with the bool_of_string function.

Adding a new (non-global) flag to an existing module

Adding a new flag impacts three pieces of code. The first is the body of the module you're adding the flag to. Generally speaking, adding a flag looks like

(* Default value of the flag. *)
let my_flag_default = ...
(* Reference storing the value of the flag. *)
let my_flag = ref my_flag_default
(* Add flag specification to module specs. *)
let _ = add_spec (
  (* The actual flag. *)
  "--my_flag",
  (* What to do with the value given to the flag, see other flags. *)
  ...,
  (* Flag description. *)
  fun fmt ->
    Format.fprintf fmt
      "@[<v>Description of my flag.@ Default: %a@]"
      pp_print_default_value_of_my_flag my_flag_default
)
(* Flag value accessor. *)
let my_flag () = !my_flag

At this point your flag is integrated in the Kind 2 flags.

To make it available to the rest of Kind 2, you need to modify the signature of the module you added the flag to

The update to the signature is typically

  val my_flag : unit -> type_of_my_flag

Adding a new flag module

The template to add a new module is

module MyModule : sig
  include FlagModule
end = struct

  (* Identifier of the module. No space or special characters. *)
  let id = "..."
  (* Short description of the module. *)
  let desc = "..."
  (* Explanation of the module. *)
  let fmt_explain fmt =
    Format.fprintf fmt "@[<v>\
      ...\
    @]"

  (* All the flag specification of this module. *)
  let all_specs = ref []
  let add_specs specs = all_specs := !all_specs @ specs
  let add_spec spec = add_specs [spec]

  (* Returns all the flag specification of this module. *)
  let all_specs () = !all_specs

end

Don't forget to update `flags.mli`:

module MyModule : sig
  include FlagModule
end

You then need to add your module to the module_map, the association map between module identifiers and modules. Make sure the identifier for your module is not used yet.

You can now add modules following the instructions in the previous section.

exception Error
exception SolverNotFound of string

A solver is not found, or not supported; with the message logged

exception UnsupportedSolver of string
exception UsageError of string

An error on the command line, with its message: raised by parse_argv instead of printing the usage, if the profile says so, as kmoxi's does

Accessors for flags

Meta flags

Generic flags

val input_file : unit -> string

Input file

val all_input_files : unit -> string list

All lustre files in the cone of influence of the input file.

val clear_input_files : unit -> unit

Clears the lustre files in the cone of influence of the input file.

val add_input_file : string -> bool

Adds a lustre file in the cone of influence of the input file.

Returns false if the cone of influence already contains the file

val lus_main : unit -> string option

Main node in Lustre file

val lus_main_const : unit -> string option

Main constant identifier in Lustre file

val lus_main_type : unit -> string option

Main type alias in Lustre file

type input_format = [
  1. | `Lustre
  2. | `Horn
  3. | `Native
]

Format of input file

val input_format : unit -> input_format
val output_dir : unit -> string

Output directory for the files Kind 2 generates.

val include_dirs : unit -> string list
type real_precision = [
  1. | `Rational
  2. | `Float
]
val real_precision : unit -> real_precision
val arr_elements_printed : unit -> int
val log_invs : unit -> bool

Minimizes and logs invariants as contracts.

val print_invs : unit -> bool

Prints invariants *

val print_cex : unit -> bool

Print counterexamples *

val print_witness : unit -> bool

Print witnesses *

val dump_cex : unit -> bool

Dump counterexample to disproven invariant property to a file *

val set_dump_cex : bool -> unit

Set whether dumping counterexamples

val dump_witness : unit -> bool

Dump witness of proven reachability property to a file *

val debug : unit -> string list

Debug sections to enable

val debug_log : unit -> string option

Logfile for debug output

type exit_code_convention = [
  1. | `RESULTS_AND_ERRORS
  2. | `ONLY_ERRORS
]
val exit_code_mode : unit -> exit_code_convention
val log_level : unit -> Lib.log_level

Verbosity level

val log_format_xml : unit -> bool

Output in XML format

val log_format_json : unit -> bool

Output in JSON format

val log_format_ijson : unit -> bool

Output in incremental JSON format

val timeout_wall : unit -> float

Wallclock timeout.

val timeout_analysis : unit -> float

Per-run wallclock timeout.

val memory_limit : unit -> int

Memory limit in MB of the analysis, solvers included, or 0 for that of the cgroup of the process (see MemoryWatch).

type enable = Lib.kind_module list

The Kind modules enabled is a list of kind_modules.

val only_parse : unit -> bool

Only parse the Lustre program. No analysis is performed.

val enabled : unit -> enable

The modules enabled.

val invgen_enabled : unit -> enable

Returns the invariant generation techniques currently enabled.

val disable : Lib.kind_module -> unit

Manually disables a module.

val modular : unit -> bool

Modular analysis.

type slice_nodes = [
  1. | `On
  2. | `Off
  3. | `Experimental
]

Node slicing

val slice_nodes : unit -> slice_nodes
val check_reach : unit -> bool

Check reachability properties

val check_nonvacuity : unit -> bool

Check non-vacuity of contract modes and conditional properties

val check_subproperties : unit -> bool

Check properties of subnodes

val lus_strict : unit -> bool

Strict Lustre mode.

val lus_no_include : unit -> bool

Reject include directives in Lustre files.

val lus_push_pre : unit -> bool

Activates transformation that pushes pre expressions

val color : unit -> bool

Colored output.

val support_new_bv_cast_operators : unit -> bool

True iff the current solver support sbv_to_int and ubv_to_int operators

module Smt : sig ... end
module BmcKind : sig ... end
module IC3QE : sig ... end
module IC3IA : sig ... end
module QE : sig ... end
module Contracts : sig ... end
module Certif : sig ... end
module IVC : sig ... end
module MCS : sig ... end
module Arrays : sig ... end

Quantifier instantiation flags

module Quant : sig ... end

Testgen flags

module Testgen : sig ... end
module Invgen : sig ... end
module C2I : sig ... end
module Interpreter : sig ... end
module ContractMonitor : sig ... end
module Lsp : sig ... end

Convenience functions

val subdir_for : string list -> string

Path to subdirectory for a system (in the output directory).

Parsing of the command line

type profile

What an executable shows and accepts on its command line: the modules whose flags it registers, and how its usage message describes the input. The global flags are always registered, less the ones that concern kind2 only.

val kind2_profile : profile

kind2: every module

val kmoxi_profile : profile

kmoxi: the engine, solver and theory flags, and the global flags that are not about the Lustre front end. The SMT solvers are checked and detected once the input is read, with check_solvers, and an error on the command line is raised as UsageError.

val check_solvers : unit -> unit

Check the SMT solvers given on the command line, detect the others, and adjust the options to the solvers in use: what parse_argv does, unless its profile leaves it until the input is read, as kmoxi's does. Solver preferences (Smt.prefer_solvers) are to be set before.

val parse_argv : ?profile:profile -> unit -> unit

Parse the command line of the executable of profile (kind2 by default): a flag outside the profile is unknown.