Module Pulselib.PulsePathCondition

module F = Stdlib.Format
module AbstractValue = PulseAbstractValue
module SatUnsat = PulseSatUnsat
module ValueHistory = 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 = 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 : IR.Tenv.t -> can_be_pruned:AbstractValue.Set.t -> keep:AbstractValue.Set.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> (t * AbstractValue.Set.t * new_eqs) SatUnsat.t

simplify ~can_be_pruned ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible, and tries to eliminate variables not in can_be_pruned from the "pruned" part of the formula

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 = PulseFormula.operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
| FunctionApplicationOperand of {
f : PulseFormula.function_symbol;
actuals : AbstractValue.t list;
}
val compare_operand : operand -> operand -> int
val and_equal : operand -> operand -> t -> t * new_eqs
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 : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> t * bool * new_eqs

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

val has_no_assumptions : t -> bool

whether the current path is independent of any calling context

val get_known_var_repr : t -> AbstractValue.t -> AbstractValue.t

get the canonical representative for the variable according to the equality relation in the "known" part of the formula

val get_both_var_repr : t -> AbstractValue.t -> AbstractValue.t

get the canonical representative for the variable according to the equality relation in the "both" (known + pruned) part of the formula