Module Pulselib__PulsePathCondition

module F = Stdlib.Format
module AbstractValue = Pulselib.PulseAbstractValue
module SatUnsat = Pulselib.PulseSatUnsat
module ValueHistory = Pulselib.PulseValueHistory
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val true_ : t
val false_ : t
val pp : F.formatter -> t -> unit
type new_eqs = Pulselib.PulseFormula.new_eqs

Building arithmetic constraints

val and_nonnegative : AbstractValue.t -> t -> t * new_eqs

and_nonnegative v phi is phi ∧ v≥0

val and_positive : AbstractValue.t -> t -> t * new_eqs

and_positive v phi is phi ∧ v>0

val and_eq_int : AbstractValue.t -> IR.IntLit.t -> t -> t * new_eqs

and_eq_int v i phi is phi ∧ v=i

val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
val simplify : keep:AbstractValue.Set.t -> t -> (t * new_eqs) SatUnsat.t

simplify ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible

val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t -> callee:t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs

Operations

type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
val compare_operand : operand -> operand -> int
val pp_operand : IStdlib.IStd.Formatter.t -> operand -> unit
val eval_binop : AbstractValue.t -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> IR.Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> IR.Typ.t -> t -> t * new_eqs

Queries

val is_known_zero : t -> AbstractValue.t -> bool

is_known_zero phi t returns true if phi |- t = 0, false if we don't know for sure

val is_known_not_equal_zero : t -> AbstractValue.t -> bool

is_known_not_equal_zero phi t returns true if phi |- t != 0, false if we don't know for sure

val is_unsat_cheap : t -> bool

whether the state contains a contradiction, call this as often as you want

val is_unsat_expensive : t -> t * bool * new_eqs

whether the state contains a contradiction, only call this when you absolutely have to

val as_int : t -> AbstractValue.t -> int option

as_int phi t returns an integer x such that phi |- t = x, if known for sure; see also is_known_zero

val has_no_assumptions : t -> bool

whether the current path is independent of any calling context

val get_var_repr : t -> AbstractValue.t -> AbstractValue.t

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