Module Pulselib.PulseFormula
module SatUnsat = PulseSatUnsatmodule Var = PulseAbstractValueArithmetic solver
Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.
val pp : F.formatter -> t -> unitval pp_with_pp_var : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unitonly used for unit tests
type operand=|LiteralOperand of IR.IntLit.t|AbstractValueOperand of Var.t
Build formulas
type new_eq=|EqZero of Var.t|Equal of Var.t * Var.tsome operations will return a set of new facts discovered that are relevant to communicate to the memory domain
type new_eqs= new_eq list
val ttrue : tval and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.tval and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.tval and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.tval and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.tval and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.tval and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.tval prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
Operations
val normalize : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.tthink a bit harder about the formula
val simplify : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> keep_pre:Var.Set.t -> keep_post:Var.Set.t -> t -> (t * new_eqs) SatUnsat.tval and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.tval is_known_zero : t -> Var.t -> boolval has_no_assumptions : t -> boolval get_var_repr : t -> Var.t -> Var.tget the canonical representative for the variable according to the equality relation
module DynamicTypes : sig ... endModule for reasoning about dynamic types. *