Pulselib.PulseFormula
module SatUnsat = PulseSatUnsat
module ValueHistory = PulseValueHistory
module Var :
module type of PulseAbstractValue
with type t = PulseAbstractValue.t
and module Set = PulseAbstractValue.Set
and module Map = PulseAbstractValue.Map
Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.
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
val pp : F.formatter -> t -> unit
only used for unit tests
val compare_function_symbol : function_symbol -> function_symbol -> int
val equal_function_symbol : function_symbol -> function_symbol -> bool
type operand =
| AbstractValueOperand of Var.t
| ConstOperand of IR.Const.t
| FunctionApplicationOperand of {
f : function_symbol;
actuals : Var.t list;
}
val pp_operand : F.formatter -> operand -> unit
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
and_equal_vars v1 v2 phi
is and_equal (AbstractValueOperand v1) (AbstractValueOperand v2) phi
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 and_equal_binop :
Var.t ->
IR.Binop.t ->
operand ->
operand ->
t ->
(t * new_eqs) SatUnsat.t
val and_is_int : Var.t -> t -> (t * new_eqs) SatUnsat.t
val prune_binop :
negated:bool ->
IR.Binop.t ->
operand ->
operand ->
t ->
(t * new_eqs) SatUnsat.t
val normalize : ?location:IBase.Location.t -> t -> (t * new_eqs) SatUnsat.t
think a bit harder about the formula
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).
Some equalities might be represented implicitly in the precondition, see the documentation of PulseArithmetic.is_manifest
.
get the canonical representative for the variable according to the equality relation
val and_callee_formula :
(Var.t * ValueHistory.t) Var.Map.t ->
t ->
callee:t ->
((Var.t * ValueHistory.t) Var.Map.t * t * new_eqs) SatUnsat.t
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.