gillian » Gillian » Debugger » Lifter » Gil_lifter » Make

Module type Gil_lifter.Make

Parameters

moduleSMemory : Engine.SMemory.S

modulePC : Command_line.ParserAndCompiler.S

moduleVerifier : 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 = PC.init_data

type pc_err = PC.err

type memory = SMemory.t

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

type annot = PC.Annot.t

type Stdlib.Effect.t +=

1. | Step : (Logging.Report_id.t option
        * Gil_syntax.Branch_case.t option
        * 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) Gil_syntax.Prog.t ->
  (t * (unit -> Logging.Report_id.t * 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) Gil_syntax.Prog.t ->
  t * (unit -> Logging.Report_id.t * 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 ->
  Logging.Report_id.t ->
  Logging.Report_id.t * Utils.stop_reason

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

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

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

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

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

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

val get_matches_at_id :
  Logging.Report_id.t ->
  t ->
  Utils.Match_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 ->
  Utils.exception_info

val pp_expr : t -> Gil_syntax.Expr.t Fmt.t

val pp_asrt : t -> Gil_syntax.Asrt.atom Fmt.t

val get_variables :
  t ->
  memory Utils.astate ->
  Logging.Report_id.t ->
  Utils.Variable.scope list * Utils.Variable.ts

val parse_and_compile_files :
  entrypoint:string ->
  string list ->
  ((annot, tl_ast, init_data) Command_line.ParserAndCompiler.compiled_progs
   * string)
    Utils.Gillian_result.t

val init_manual :
  string ->
  string list ->
  t
  * (cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data option ->
  unit ->
  Logging.Report_id.t * Utils.stop_reason)

A version of init that allows manually supplying exec_data instead of triggering the Step effect - this is used when Gil is not the primary lifter.

val handle_cmd :
  Logging.Report_id.t ->
  Gil_syntax.Branch_case.t option ->
  cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data ->
  t ->
  unit

val path_of_id : Logging.Report_id.t -> t -> Gil_syntax.Branch_case.path

val should_skip_cmd :
  cmd_report Debugger_lifter__.Lifter_intf.Types.executed_cmd_data ->
  t ->
  bool

val cases_at_id : Logging.Report_id.t -> t -> Gil_syntax.Branch_case.t list

val get_type_env_vars : Symbolic.Type_env.t -> Utils.Variable.t list

val get_pred_vars : Engine.Preds.t -> Utils.Variable.t list

val get_pure_formulae_vars : Symbolic.Pure_context.t -> Utils.Variable.t list