gillian » Gillian » Symbolic » Memory_S

Module type Symbolic.Memory_S

type init_data

Type of data that is given the first time memory is created. Useful when there's global context to know about like a type-system

type vt := Symbolic.Values.t

Type of GIL values

type st := Symbolic.Subst.t

Type of GIL substitutions

type err_t

val err_t_to_yojson : err_t -> Yojson.Safe.t

val err_t_of_yojson :
  Yojson.Safe.t ->
  err_t Ppx_deriving_yojson_runtime.error_or

val pp_err_t :
  Ppx_deriving_runtime.Format.formatter ->
  err_t ->
  Ppx_deriving_runtime.unit

val show_err_t : err_t -> Ppx_deriving_runtime.string

type t

Type of GIL general states

val to_yojson : t -> Yojson.Safe.t

val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or

val init : init_data -> t

Initialisation

val get_init_data : t -> init_data

val clear : t -> t

val execute_action :
  string ->
  t ->
  Engine.Gpc.t ->
  vt list ->
  (t * vt list, err_t) Engine.Symex.result

Execute action

val consume :
  string ->
  t ->
  Engine.Gpc.t ->
  vt list ->
  (t * vt list, err_t) Engine.Symex.result

val produce : string -> t -> Engine.Gpc.t -> vt list -> t Engine.Symex.t

val is_overlapping_asrt : string -> bool

val copy : t -> t

State Copy

val pp : Stdlib.Format.formatter -> t -> unit

Printer

val pp_by_need : Utils.Containers.SS.t -> Stdlib.Format.formatter -> t -> unit

val get_print_info :
  Utils.Containers.SS.t ->
  t ->
  Utils.Containers.SS.t * Utils.Containers.SS.t

val substitution_in_place :
  pfs:Pure_context.t ->
  gamma:Type_env.t ->
  st ->
  t ->
  (t * Gil_syntax.Expr.Set.t * (string * Gil_syntax.Type.t) list) list

val clean_up :
  ?keep:Gil_syntax.Expr.Set.t ->
  t ->
  Gil_syntax.Expr.Set.t * Gil_syntax.Expr.Set.t

val lvars : t -> Utils.Containers.SS.t

val alocs : t -> Utils.Containers.SS.t

val assertions : ?to_keep:Utils.Containers.SS.t -> t -> Gil_syntax.Asrt.t

val mem_constraints : t -> Gil_syntax.Expr.t list

val get_recovery_tactic : t -> err_t -> vt Engine.Recovery_tactic.t

val pp_err : Stdlib.Format.formatter -> err_t -> unit

val get_failing_constraint : err_t -> Gil_syntax.Expr.t

val get_fixes : err_t -> Gil_syntax.Asrt.t list

val can_fix : err_t -> bool

val sure_is_nonempty : t -> bool

val split_further :
  t ->
  string ->
  vt list ->
  err_t ->
  (vt list list * vt list) option

split_further core_pred ins err returns a way to split further a core_predicate if consuming it failed with error, if there is one. In that case, it returns a pair containing

• a list of new ins. Each element is the list of ins for each sub-component of the core predicate;
• new way of learning the outs, as explained under.

For example let's say the core predicate (x, []) ↦ [a, b] (with 2 ins and 1 out) can be split into

• (x, [0]) ↦ [a]
• (x, [1]) ↦ [b] And we try and consume the whole thing, but the memory only had (x, [0]) ↦ [a] in it. Then this function, given the appropriate error, should a pair of two elements:
• the new ins: [ [x, [0]], [x, [1]] ]
• the new way of learning the outs: [ {{ l-nth(PVar("0:0"), 0), l-nth(PVar("1:0"), 0) }} ]

Important: it is always sound for this function to return None, it will just reduce the amount of automation.