Module Pulselib.PulseFormula

module F = Stdlib.Format
module Atom = PulseFormulaAtom
module SatUnsat = PulseSatUnsat
module Var = PulseFormulaVar
module LinArith : sig ... end

Linear Arithmetic

module Term : sig ... end
module Formula : sig ... end
type t = {
  1. conditions : int Atom.Map.t;
    (*

    collection of conditions that have been assumed (via PRUNE CFG nodes) along the path. Note that these conditions are *not* normalized w.r.t. phi: phi already contains them so normalization w.r.t. phi would make them trivially true most of the time.

    *)
  2. phi : Formula.t;
    (*

    the arithmetic constraints of the current symbolic state; true in both the pre and post since abstract values Var.t have immutable semantics

    *)
}
include Ppx_compare_lib.Comparable.S with type t := t
val compare : t Base__Ppx_compare_lib.compare
include Ppx_compare_lib.Equal.S with type t := t
val equal : t Base__Ppx_compare_lib.equal
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
type path_stamp = {
  1. path_cond : int Atom.Map.t;
  2. atom_set : Atom.Set.t;
  3. term_set : Term.Set.t;
}
val compare_path_stamp : path_stamp -> path_stamp -> int
val equal_path_stamp : path_stamp -> path_stamp -> bool
val extract_path_stamp : t -> path_stamp
val is_empty_path_stamp : path_stamp -> bool
val pp_path_stamp : F.formatter -> path_stamp -> unit
val extract_path_cond : t -> int Atom.Map.t
val extract_term_cond : t -> Atom.Set.t
val extract_term_cond2 : t -> Term.Set.t
val map_is_empty : int Atom.Map.t -> bool
val set_is_empty : Atom.Set.t -> bool
val termset_is_empty : Term.Set.t -> bool
val formula_is_empty : t -> bool

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

val pp : F.formatter -> t -> unit
val pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit

only used for unit tests

type function_symbol =
  1. | Unknown of Var.t
  2. | Procname of IR.Procname.t
val compare_function_symbol : function_symbol -> function_symbol -> int
val equal_function_symbol : function_symbol -> function_symbol -> bool
type operand =
  1. | AbstractValueOperand of Var.t
  2. | ConstOperand of IR.Const.t
  3. | FunctionApplicationOperand of {
    1. f : function_symbol;
    2. actuals : Var.t list;
    }
val compare_operand : operand -> operand -> int
val equal_operand : operand -> operand -> bool
val pp_operand : F.formatter -> operand -> unit

Build formulas

type new_eq =
  1. | EqZero of Var.t
    (*

    v=0

    *)
  2. | Equal of Var.t * Var.t
    (*

    v_old = v_new: v_old is to be replaced with v_new

    *)

some operations will return a set of new facts discovered that are relevant to communicate to the memory domain

val pp_new_eq : F.formatter -> new_eq -> unit
type new_eqs = new_eq IStdlib.RevList.t
val ttrue : t
val and_path_flush : t -> t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_vars : Var.t -> Var.t -> t -> (t * new_eqs) SatUnsat.t

and_equal_vars v1 v2 phi is and_equal (AbstractValueOperand v1) (AbstractValueOperand v2) phi

val and_not_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> nullable:bool -> t -> (t * new_eqs) SatUnsat.t
type dynamic_type_data = {
  1. typ : IR.Typ.t;
  2. source_file : IBase.SourceFile.t option;
}
val get_dynamic_type : Var.t -> t -> dynamic_type_data option
val and_dynamic_type : Var.t -> IR.Typ.t -> ?source_file:IBase.SourceFile.t -> t -> (t * new_eqs) SatUnsat.t
val add_dynamic_type_unsafe : Var.t -> IR.Typ.t -> ?source_file:IBase.SourceFile.t -> IBase.Location.t -> t -> t
val copy_type_constraints : Var.t -> Var.t -> t -> t
val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_string_concat : Var.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_is_int : Var.t -> t -> (t * new_eqs) SatUnsat.t
val prune_binop : ?depth:int -> negated:bool -> IR.Binop.t -> ?need_atom:bool -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t

Operations

val simplify : precondition_vocabulary:Var.Set.t -> keep:Var.Set.t -> t -> (t * Var.Set.t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val as_constant_q : t -> Var.t -> Q.t option
val as_constant_string : t -> Var.t -> string option
val is_known_non_pointer : t -> Var.t -> bool
val is_manifest : is_allocated:(Var.t -> bool) -> t -> bool

Some types or errors detected by Pulse require that the state be *manifest*, which corresponds to the fact that the error can happen in *any reasonable* calling context (see below). If not, the error is flagged as *latent* and not reported until it becomes manifest.

A state is *manifest* when its path condition (here meaning the conjunction of conditions encountered in if statements, loop conditions, etc., i.e. anything in a IR.Sil.instr.Prune node) is either a) empty or b) comprised only of facts of the form p>0 or p≠0 where p is known to be allocated. The latter condition captures the idea that addresses being valid pointers in memory should not deter us from reporting any error that we find on that program path as it is somewhat the happy/expected case (also, the fact p is allocated already implies p≠0). The unhappy/unexpected case here would be to report errors that require a pointer to be invalid or null in the precondition; we do not want to report such errors until we see that there exists a calling context in which the pointer is indeed invalid or null! But, to reiterate, we do want to report errors that only have valid pointers in their precondition. Similarly, ignore conditions of the form x≠y where x and y are already different according to the heap (because they are separate memory allocations).

In addition, only conditions in callees of the current procedure may cause a path to become latent, i.e. direct tests in the current function do not make an issue latent. The rationale for this is that, if the current function branches on a particular condition, it must have some reason to believe both paths are possible in its calling contexts, hence should not exhibit a bug under these conditions. This is different from conditions arising from tests in callees, which may be written more defensively than the current function. (NOTE: this doesn't apply to Erlang)

Some equalities might be represented implicitly in the precondition, see the documentation of PulseArithmetic.is_manifest.

val get_var_repr : t -> Var.t -> Var.t

get the canonical representative for the variable according to the equality relation

val and_callee_formula : default:'metadata -> subst:(Var.t * 'metadata) Var.Map.t -> t -> callee:t -> ((Var.t * 'metadata) Var.Map.t * t * new_eqs) SatUnsat.t
val implies_conditions_up_to : subst:Var.t Var.Map.t -> t -> implies:t -> (unit, [> `Contradiction of SatUnsat.unsat_info | `NotImplied of Atom.t ]) IStdlib.IStd.result
val fold_variables : (t, Var.t, 'acc) IStdlib.IStd.Container.fold

note: each variable mentioned in the formula is visited at least once, possibly more

val absval_of_int : t -> IR.IntLit.t -> t * Var.t

Get or create an abstract value (Var.t is AbstractValue.t) associated with a constant IR.IntLit.t. The idea is that clients will record in the abstract state that the returned t is equal to the given integer. If the same integer is queried later on then this module will return the same abstract variable.

val absval_of_string : t -> string -> t * Var.t
type term
val explain_as_term : t -> Var.t -> term option
val pp_term : (F.formatter -> Var.t -> unit) -> F.formatter -> term -> unit
val pp_conditions_explained : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
val pp_formula_explained : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
val join : t -> t -> t