Module Pulselib.PulseOperations

Check that the address is not known to be invalid

module Closures : sig ... end
val pulse_model_type : IR.Typ.name

Struct type name of "__infer_pulse_model"

module ModeledField : sig ... end
val conservatively_initialize_args : Pulselib.PulseBasicInterface.AbstractValue.t list -> t -> t

Set all reachable values from the given list as initialized conservatively.

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.

Similar to eval but for pvar only. Always succeeds.

Like eval but evaluates *exp.

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.

Like eval_access but does additional dereference.

val add_static_type_objc_class : IR.Tenv.t -> IR.Typ.t -> Pulselib.PulseBasicInterface.AbstractValue.t -> IBase.Location.t -> t -> t

Havoc dereferenced field address.

val realloc_pvar : IR.Tenv.t -> Pulselib.PulseDomainInterface.PathContext.t -> set_uninitialized:bool -> IR.Pvar.t -> IR.Typ.t -> IBase.Location.t -> t -> t

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

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

write the edge ref[index]--> obj

write the edge ref --*--> obj

type invalidation_access =
  1. | MemoryAccess of {
    1. pointer : Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t;
    2. access : Pulselib.PulseBasicInterface.Access.t;
    3. hist_obj_default : Pulselib.PulseBasicInterface.ValueHistory.t;
    }
    (*

    the value was read from the heap following the access edge at address pointer

    *)
  2. | StackAddress of IR.Var.t * Pulselib.PulseBasicInterface.ValueHistory.t
    (*

    the value was read from the stack

    *)
  3. | UntraceableAccess
    (*

    we don't know where the value came from; avoid using if possible

    *)

the way that was used to get to the invalidated address in the state; this is used to record the invalidation point in its history in addition to inside the Invalid attribute

record that the address is invalid

check that the address is currently valid then record that the address is now invalid

val always_reachable : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val java_resource_release : recursive:bool -> Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t

releases the resource of the argument, and recursively calls itself on the delegated resource if recursive==true

val csharp_resource_release : recursive:bool -> Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t

releases the resource of the argument, and recursively calls itself on the delegated resource if recursive==true

val add_dict_contain_const_keys : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val remove_dict_contain_const_keys : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t
val remove_allocation_attr : Pulselib.PulseBasicInterface.AbstractValue.t -> t -> t

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

Like invalidate_access but invalidates dereferenced address.

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

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

returns the address of a new cell with the copied edges from the original. The content is deeply copied up until max_depth edges deep in memory. The deepest copied value is then shallow copied. If no max_depth is specified, then there is no shallow copy and everything is deeply copied until there is no more edge to follow

val get_dynamic_type_unreachable_values : IR.Var.t list -> t -> (IR.Var.t * IR.Typ.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

type call_kind = [
  1. | `Closure of (IR.Exp.t * IR.Pvar.t * IR.Typ.t * IR.CapturedVar.capture_mode) list
  2. | `Var of IR.Ident.t
  3. | `ResolvedProcname
]

Check and report config usage issue on the abstract value that is used as branch condition. If it is not certain that tha abstract value is a config, it adds UsedAsBranchCond attribute.

When we find the store defer_ref = ref, where defer_ref has the cleanup attribute, we remove the allocation attribute from ref. This is because the cleanup attribute is often used to defer freeing variables, so we avoid false positives.