Lifter (gillian.Command_line.Make.Lifter)

Parameters

module V : Engine.Verifier.S with type annot = PC.Annot.t

Signature

type t

The lifter's state

type memory_error = SMemory.err_t

type tl_ast = PC.tl_ast

type init_data = ID.t

type pc_err = PC.err

type memory = SMemory.t

type cmd_report = V.SAInterpreter.Logging.ConfigReport.t

type annot = PC.Annot.t

type Stdlib.Effect.t +=

| Step : (Gillian.Logging.Report_id.t option * Gillian.Gil_syntax.Branch_case.t option * Gillian.Gil_syntax.Branch_case.path) -> cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data Stdlib.Effect.t

val init : 
  proc_name:string ->
  all_procs:string list ->
  tl_ast option ->
  (annot, int) Gillian.Gil_syntax.Prog.t ->
  (t
   * (unit ->
   Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason))
    option

Given a proc name, a tl_ast, and the data from the first executed GIL command, initialise the lifter's state and handle the first command.

Returns None if lifting is unsupported (i.e. if tl_ast is None).

val init_exn : 
  proc_name:string ->
  all_procs:string list ->
  tl_ast option ->
  (annot, int) Gillian.Gil_syntax.Prog.t ->
  t
  * (unit ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason)

Exception-raising version of init.

val dump : t -> Yojson.Safe.t

Gives a JSON representation of the lifter's state.

Used for debugging problems with the lifter.

val step_over : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_in : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_out : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_back : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val step_branch : 
  t ->
  Gillian.Logging.Report_id.t ->
  Debugger_utils.Exec_map.Packaged.branch_case option ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val continue : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val continue_back : 
  t ->
  Gillian.Logging.Report_id.t ->
  Gillian.Logging.Report_id.t * Gillian.Debugger.Utils.stop_reason

val get_gil_map : t -> Debugger_utils.Exec_map.Packaged.t

Gets the non-lifted execution map of GIL commands.

In most cases, it's recommended to use a Gil_fallback_lifter, and just defer this call to the GIL lifter.

val get_lifted_map : t -> Debugger_utils.Exec_map.Packaged.t option

Gets the lifted execution map.

Returns None if lifting is not supported.

val get_lifted_map_exn : t -> Debugger_utils.Exec_map.Packaged.t

Exception-raising version of get_lifted_map.

val get_matches_at_id : 
  Gillian.Logging.Report_id.t ->
  t ->
  Gillian.Debugger.Utils.Exec_map.matching list

Gives a list of matches that occurred at the specified command.

val memory_error_to_exception_info : 
  (memory_error, annot, tl_ast)
    Debugger_lifter__.Lifter_intf.Types.memory_error_info ->
  Gillian.Debugger.Utils.exception_info

val add_variables : 
  store:(string * Gillian.Gil_syntax.Expr.t) list ->
  memory:memory ->
  is_gil_file:bool ->
  get_new_scope_id:(unit -> int) ->
  Gillian.Debugger.Utils.Variable.ts ->
  Gillian.Debugger.Utils.Variable.scope list

val parse_and_compile_files : 
  entrypoint:string ->
  string list ->
  ((annot, tl_ast, init_data)
     Gillian.Command_line.ParserAndCompiler.compiled_progs
   * string,
    pc_err)
    Stdlib.result