Module Pulselib.PulseOperations

module Import : sig ... end

For opening in other modules.

include module type of Import
type access_mode =
| Read
| Write
| NoAccess

The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.

Imported types for ease of use and so we can write variants without the corresponding module prefix

type 'abductive_domain_t base_t = 'abductive_domain_t PulseDomainInterface.ExecutionDomain.base_t =
| ContinueProgram of 'abductive_domain_t
| ExitProgram of PulseDomainInterface.AbductiveDomain.summary
| AbortProgram of PulseDomainInterface.AbductiveDomain.summary
| LatentAbortProgram of {
astate : PulseDomainInterface.AbductiveDomain.summary;
latent_issue : PulseDomainInterface.LatentIssue.t;
}
| ISLLatentMemoryError of 'abductive_domain_t
type 'a access_result = 'a PulseReport.access_result

Monadic syntax

include module type of IStdlib.IResult.Let_syntax
include module type of IStdlib.IStd.Result.Monad_infix
val (>>=) : ('a, 'e) Core_kernel__Result.t -> ('a -> ('b, 'e) Core_kernel__Result.t) -> ('b, 'e) Core_kernel__Result.t
val (>>|) : ('a, 'e) Core_kernel__Result.t -> ('a -> 'b) -> ('b, 'e) Core_kernel__Result.t
val let+ : ('ok, 'err) IStdlib.IStd.result -> ('ok -> 'okk) -> ('okk, 'err) IStdlib.IStd.result
val let* : ('ok, 'err) IStdlib.IStd.result -> ('ok -> ('okk, 'err) IStdlib.IStd.result) -> ('okk, 'err) IStdlib.IStd.result
val let<*> : 'a access_result -> ('a -> 'b access_result list) -> 'b access_result list

monadic "bind" but not really that turns an access_result into a list of access_results (not really because the first type is not an access_result list but just an access_result)

val let<+> : 'a access_result -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t base_t access_result list

monadic "map" but even less really that turns an access_result into an analysis result

type t = PulseDomainInterface.AbductiveDomain.t
val check_addr_access : access_mode -> IBase.Location.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

Check that the address is not known to be invalid

module Closures : sig ... end
val eval : access_mode -> IBase.Location.t -> IR.Exp.t -> t -> (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) access_result

Use the stack and heap to evaluate the given expression down to an abstract address representing its value.

Return an error state if it traverses some known invalid address or if the end destination is known to be invalid.

val eval_structure_isl : access_mode -> IBase.Location.t -> IR.Exp.t -> t -> (bool * (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) list) access_result

Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not.

val prune : IBase.Location.t -> condition:IR.Exp.t -> t -> t access_result
val eval_deref : IBase.Location.t -> IR.Exp.t -> t -> (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) access_result

Like eval but evaluates *exp.

val eval_deref_isl : IBase.Location.t -> IR.Exp.t -> t -> (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) list access_result
val eval_access : access_mode -> IBase.Location.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> Pulselib.PulseDomainInterface.BaseMemory.Access.t -> t -> (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) access_result

Like eval but starts from an address instead of an expression, checks that it is valid, and if so dereferences it according to the access.

val havoc_id : IR.Ident.t -> PulseBasicInterface.ValueHistory.t -> t -> t
val havoc_field : IBase.Location.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> IR.Fieldname.t -> PulseBasicInterface.ValueHistory.t -> t -> t access_result
val realloc_pvar : IR.Tenv.t -> IR.Pvar.t -> IR.Typ.t -> IBase.Location.t -> t -> t
val write_id : IR.Ident.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t
val write_field : IBase.Location.t -> ref:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> IR.Fieldname.t -> obj:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

write the edge ref --.field--> obj

val write_arr_index : IBase.Location.t -> ref:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> index:PulseBasicInterface.AbstractValue.t -> obj:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

write the edge ref[index]--> obj

val write_deref : IBase.Location.t -> ref:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> obj:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

write the edge ref --*--> obj

val write_deref_biad_isl : IBase.Location.t -> ref:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> PulseBasicInterface.AbstractValue.t Absint.HilExp.Access.t -> obj:(PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t list access_result
val invalidate : IBase.Location.t -> PulseBasicInterface.Invalidation.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

record that the address is invalid

val invalidate_biad_isl : IBase.Location.t -> PulseBasicInterface.Invalidation.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t list access_result

record that the address is invalid. If the address has not been allocated, abduce ISL specs for both invalid (null, free, unint) and allocated heap.

val allocate : IR.Procname.t -> IBase.Location.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t
val add_dynamic_type : IR.Typ.Name.t -> PulseBasicInterface.AbstractValue.t -> t -> t
val remove_allocation_attr : PulseBasicInterface.AbstractValue.t -> t -> t
val invalidate_access : IBase.Location.t -> PulseBasicInterface.Invalidation.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> Pulselib.PulseDomainInterface.BaseMemory.Access.t -> t -> t access_result

record that what the address points via the access to is invalid

val invalidate_array_elements : IBase.Location.t -> PulseBasicInterface.Invalidation.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> t access_result

record that all the array elements that address points to is invalid

val shallow_copy : IBase.Location.t -> (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) -> t -> (t * (PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t)) access_result

returns the address of a new cell with the same edges as the original

val get_dynamic_type_unreachable_values : IR.Var.t list -> t -> (IR.Var.t * IR.Typ.Name.t) list

Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available

val remove_vars : IR.Var.t list -> IBase.Location.t -> t -> t access_result
val check_address_escape : IBase.Location.t -> IR.Procdesc.t -> PulseBasicInterface.AbstractValue.t -> PulseBasicInterface.ValueHistory.t -> t -> t access_result
val call : IR.Tenv.t -> caller_proc_desc:IR.Procdesc.t -> callee_data:(IR.Procdesc.t * PulseSummary.t) option -> IBase.Location.t -> IR.Procname.t -> ret:(IR.Ident.t * IR.Typ.t) -> actuals:((PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) * IR.Typ.t) list -> formals_opt:(IR.Pvar.t * IR.Typ.t) list option -> t -> PulseDomainInterface.ExecutionDomain.t access_result list

perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists

val unknown_call : IR.Tenv.t -> IBase.Location.t -> PulseBasicInterface.CallEvent.t -> ret:(IR.Ident.t * IR.Typ.t) -> actuals:((PulseBasicInterface.AbstractValue.t * PulseBasicInterface.ValueHistory.t) * IR.Typ.t) list -> formals_opt:(IR.Pvar.t * IR.Typ.t) list option -> t -> t

performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate

val conservatively_initialize_args : PulseBasicInterface.AbstractValue.t list -> t -> t