Pulselib.PulseOperations
val check_addr_access :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
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.
val eval :
Pulselib.PulseDomainInterface.PathContext.t ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
IR.Exp.t ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
PulseOperationResult.t
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_to_value_origin :
Pulselib.PulseDomainInterface.PathContext.t ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
IR.Exp.t ->
t ->
(t * Pulselib.PulseBasicInterface.ValueOrigin.t) PulseOperationResult.t
val eval_var :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
IR.Pvar.t ->
t ->
t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
Similar to eval but for pvar only. Always succeeds.
val eval_ident :
IR.Ident.t ->
t ->
t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
val eval_deref :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
IBase.Location.t ->
IR.Exp.t ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.t
Like eval
but evaluates *exp
.
val eval_deref_to_value_origin :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
IBase.Location.t ->
IR.Exp.t ->
t ->
(t * Pulselib.PulseBasicInterface.ValueOrigin.t)
Pulselib.PulseDomainInterface.AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.t
val eval_access :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.Access.t ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
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 eval_access_to_value_origin :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.Access.t ->
t ->
(t * Pulselib.PulseBasicInterface.ValueOrigin.t)
Pulselib.PulseDomainInterface.AccessResult.t
val eval_deref_access :
Pulselib.PulseDomainInterface.PathContext.t ->
?must_be_valid_reason:
Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
PulseOperationResult.Import.access_mode ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.Access.t ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
Like eval_access
but does additional dereference.
val eval_proc_name :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
IR.Exp.t ->
t ->
(t * IR.Procname.t option) Pulselib.PulseDomainInterface.AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.t
val hack_python_propagates_type_on_load :
IR.Tenv.t ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
IR.Exp.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
t
val add_static_type_objc_class :
IR.Tenv.t ->
IR.Typ.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
IBase.Location.t ->
t ->
t
val havoc_id :
IR.Ident.t ->
Pulselib.PulseBasicInterface.ValueHistory.t ->
t ->
t
val havoc_deref_field :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
IR.Fieldname.t ->
Pulselib.PulseBasicInterface.ValueHistory.t ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.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
val write_id :
IR.Ident.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t
val read_id :
IR.Ident.t ->
t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
option
val write_field :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
ref:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
IR.Fieldname.t ->
obj:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
write the edge ref --.field--> obj
val write_deref_field :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
ref:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
IR.Fieldname.t ->
obj:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
write the edge ref --.field--> _ --*--> obj
val write_arr_index :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
ref:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
index:Pulselib.PulseBasicInterface.AbstractValue.t ->
obj:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
write the edge ref[index]--> obj
val write_deref :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
ref:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
obj:
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
write the edge ref --*--> obj
type invalidation_access =
| MemoryAccess of {
pointer : Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t;
access : Pulselib.PulseBasicInterface.Access.t;
hist_obj_default : Pulselib.PulseBasicInterface.ValueHistory.t;
}
the value was read from the heap following the access
edge at address pointer
| StackAddress of IR.Var.t * Pulselib.PulseBasicInterface.ValueHistory.t
the value was read from the stack
*)| 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
val invalidate :
Pulselib.PulseDomainInterface.PathContext.t ->
invalidation_access ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.Invalidation.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t
record that the address is invalid
val check_and_invalidate :
Pulselib.PulseDomainInterface.PathContext.t ->
invalidation_access ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.Invalidation.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
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 allocate :
Pulselib.PulseBasicInterface.Attribute.allocator ->
IBase.Location.t ->
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 add_dict_read_const_key :
Pulselib.PulseBasicInterface.Timestamp.t ->
Pulselib.PulseBasicInterface.Trace.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
IR.Fieldname.t ->
t ->
(t, Pulselib.PulseDomainInterface.AccessResult.error) PulseResult.t
val remove_allocation_attr :
Pulselib.PulseBasicInterface.AbstractValue.t ->
t ->
t
val invalidate_access :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.Invalidation.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.Access.t ->
t ->
t
record that what the address points via the access to is invalid
val invalidate_deref_access :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.Invalidation.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
Pulselib.PulseBasicInterface.Access.t ->
t ->
t
Like invalidate_access
but invalidates dereferenced address.
val invalidate_array_elements :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.Invalidation.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
record that all the array elements that address points to is invalid
val shallow_copy :
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
returns the address of a new cell with the same edges as the original
val deep_copy :
?depth_max:int ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
t ->
(t
* (Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t))
Pulselib.PulseDomainInterface.AccessResult.t
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
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 Pulselib.PulseBasicInterface.SatUnsat.t
val check_address_escape :
IBase.Location.t ->
IR.Procdesc.t ->
Pulselib.PulseBasicInterface.AbstractValue.t ->
Pulselib.PulseBasicInterface.ValueHistory.t ->
t ->
t Pulselib.PulseDomainInterface.AccessResult.t
type call_kind = [
| `Closure of
(IR.Exp.t * IR.Pvar.t * IR.Typ.t * IR.CapturedVar.capture_mode) list
| `Var of IR.Ident.t
| `ResolvedProcname
]
val get_captured_actuals :
IR.Procname.t ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
captured_formals:(IR.Pvar.t * IR.CapturedVar.capture_mode * IR.Typ.t) list ->
call_kind:call_kind ->
actuals:
((Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
* IR.Typ.t)
list ->
t ->
(t
* ((Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
* IR.Typ.t)
list)
Pulselib.PulseDomainInterface.AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.t
val check_used_as_branch_cond :
(Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t) ->
pname_using_config:IR.Procname.t ->
branch_location:IBase.Location.t ->
location:IBase.Location.t ->
Pulselib.PulseBasicInterface.Trace.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t
Pulselib.PulseDomainInterface.AccessResult.t
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.
val cleanup_attribute_store :
IR.Procdesc.t ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
t ->
lhs_exp:IR.Exp.t ->
rhs_exp:IR.Exp.t ->
t Pulselib.PulseDomainInterface.AccessResult.t
PulseBasicInterface.sat_unsat_t
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.