gillian » Gillian » Debugger » Lifter » Gil_lifter » Make » Verifier » SMatcher

Module Verifier.SMatcher

type err_t

type state_t = SPState.state_t

type t = {

1. state : state_t;
2. preds : Engine.Preds.t;
3. wands : Engine.Wands.t;
4. pred_defs : Engine.MP.preds_tbl_t;

}

type post_res = (Gil_syntax.Flag.t * Gil_syntax.Asrt.t list) option

type search_state = (t * Symbolic.Subst.t * Engine.MP.t) list * err_t list

module Logging : sig ... end

type unfold_info_t = (string * string) list

val produce_assertion :
  t ->
  Symbolic.Subst.t ->
  Gil_syntax.Asrt.atom ->
  (t, err_t) Engine.Res_list.t

val produce :
  t ->
  Symbolic.Subst.t ->
  Gil_syntax.Asrt.t ->
  (t, err_t) Engine.Res_list.t

val produce_posts : t -> Symbolic.Subst.t -> Gil_syntax.Asrt.t list -> t list

val unfold :
  ?additional_bindings:unfold_info_t ->
  t ->
  string ->
  Gil_syntax.Expr.t list ->
  (Symbolic.Subst.t * t, err_t) Engine.Res_list.t

unfold state name args unfold_info returns a list of pairs (subst, state), resulting from unfolding the predicate name(..args..) from the given state. unfold_info contains information about how to bind new variables.

val rec_unfold :
  ?fuel:int ->
  t ->
  string ->
  Gil_syntax.Expr.t list ->
  (t, err_t) Engine.Res_list.t

val unfold_all : t -> string -> (t, err_t) Engine.Res_list.t

val try_recovering :
  t ->
  Gil_syntax.Expr.t Engine.Recovery_tactic.t ->
  (t list * Engine.Matcher.recovery_tactic, string) Stdlib.result

Tries recovering from an error using the provided recovery tactic.

val unfold_with_vals :
  auto_level:[ `High | `Low ] ->
  t ->
  Gil_syntax.Expr.t list ->
  (Symbolic.Subst.t * t) list option

Tries to unfold the given predicate in the state. If it manages, it returns the new set of states and corresponding substitutions, otherwise, it returns None.

val unfold_concrete_preds : t -> (Symbolic.Subst.t option * t) option

Unfolds 1 predicate for which all arguments are concrete.

• If it finds one:
• if it succeeds to unfold, it returns Some (Some subst, new_state )
• if it fails to unfold it returns None
• If it doesn't find one, it returns Some (None, input_state)

val match_assertion :
  ?no_auto_fold:bool ->
  t ->
  Symbolic.Subst.t ->
  Engine.MP.step ->
  (t, err_t) Engine.Res_list.t

val match_ :
  ?in_matching:bool ->
  t ->
  Symbolic.Subst.t ->
  Engine.MP.t ->
  Engine.Matcher.match_kind ->
  (t * Symbolic.Subst.t * post_res, err_t) Engine.Res_list.t

val fold :
  ?in_matching:bool ->
  ?additional_bindings:(Gil_syntax.Expr.t * Gil_syntax.Expr.t) list ->
  match_kind:Engine.Matcher.match_kind ->
  state:t ->
  Engine.MP.pred ->
  Gil_syntax.Expr.t list ->
  (t, err_t) Engine.Res_list.t

Folds a predicate in the state, consuming its definition and producing the folded predicate. If the predicate has a guard, the guard is produced.

val consume_pred :
  ?in_matching:bool ->
  ?fold_outs_info:(Symbolic.Subst.t * Engine.MP.step * Gil_syntax.Expr.t list) ->
  ?no_auto_fold:bool ->
  t ->
  string ->
  Gil_syntax.Expr.t option list ->
  (t * Gil_syntax.Expr.t list, err_t) Engine.Res_list.t

Consumes a predicate from the state. If the predicate is not "verbatim" in our set of preds, and it is not abstract and we are not in manual mode, we attempt to fold it.

val package_wand : t -> Engine.Wands.wand -> (t, err_t) Utils.List_res.t