Module Pulselib.PulseFormula

module F = Stdlib.Format
module SatUnsat = PulseSatUnsat
module Var = PulseAbstractValue

Arithmetic solver

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

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 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 operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

type new_eq =
| EqZero of Var.t
| Equal of Var.t * Var.t

some 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 : t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.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 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.t

think 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.t
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t

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

module DynamicTypes : sig ... end

Module for reasoning about dynamic types. *