Syntax (infer.Pulselib.PulseModelsDSL.Syntax)

module ModeledField = PulseOperations.ModeledField

val to_aval : Pulselib.PulseBasicInterface.ValueOrigin.t -> aval

Polymorphic Operations

val let* : 'a model_monad -> ('a -> 'b model_monad) -> 'b model_monad

val (>>=) : 'a model_monad -> ('a -> 'b model_monad) -> 'b model_monad

val (@=) : ('a -> 'b model_monad) -> 'a model_monad -> 'b model_monad

val (@@>) : unit model_monad -> 'a model_monad -> 'a model_monad

sequential composition

val compose1 : 
  ('a -> PulseModelsImport.model) ->
  ('a -> PulseModelsImport.model) ->
  'a ->
  PulseModelsImport.model

val compose2 : 
  ('a -> 'b -> PulseModelsImport.model) ->
  ('a -> 'b -> PulseModelsImport.model) ->
  'a ->
  'b ->
  PulseModelsImport.model

val ret : 'a -> 'a model_monad

val throw : unit model_monad

val unreachable : 'a model_monad

val report : Pulselib.PulseDomainInterface.Diagnostic.t -> unit model_monad

val report_assert_error : unit model_monad

val list_fold : 
  'a list ->
  init:'accum ->
  f:('accum -> 'a -> 'accum model_monad) ->
  'accum model_monad

val list_iter : 'a list -> f:('a -> unit model_monad) -> unit model_monad

val list_filter_map : 
  'a list ->
  f:('a -> 'b option model_monad) ->
  'b list model_monad

val option_iter : 'a option -> f:('a -> unit model_monad) -> unit model_monad

val absvalue_set_fold : 
  Pulselib.PulseBasicInterface.AbstractValue.Set.t ->
  init:'accum ->
  f:
    ('accum ->
      Pulselib.PulseBasicInterface.AbstractValue.t ->
      'accum model_monad) ->
  'accum model_monad

val absvalue_set_iter : 
  Pulselib.PulseBasicInterface.AbstractValue.Set.t ->
  f:(Pulselib.PulseBasicInterface.AbstractValue.t -> unit model_monad) ->
  unit model_monad

val ignore : 'a model_monad -> unit model_monad

val assign_ret : aval -> unit model_monad

val dynamic_dispatch : 
  cases:(IR.Typ.name * (unit -> 'a model_monad)) list ->
  ?default:(unit -> 'a model_monad) ->
  aval ->
  'a model_monad

val dispatch_call : 
  (IR.Ident.t * IR.Typ.t) ->
  IR.Procname.t ->
  Pulselib.PulseBasicInterface.ValueOrigin.t
    Absint.ProcnameDispatcher.Call.FuncArg.t
    list ->
  unit model_monad

val python_call : IR.Procname.t -> (string * aval) list -> aval model_monad

val apply_hack_closure : aval -> aval list -> aval model_monad

val apply_python_closure : 
  aval ->
  (IR.ProcAttributes.t option -> aval list model_monad) ->
  aval model_monad

val get_data : PulseModelsImport.model_data model_monad

val add_model_call : 
  Pulselib.PulseBasicInterface.ValueHistory.t ->
  Pulselib.PulseBasicInterface.ValueHistory.t model_monad

Disjunctive reasoning

val disj : 'a model_monad list -> 'a model_monad

val start_model : (unit -> unit model_monad) -> PulseModelsImport.model

get a model from a disjunctive model_monad

val start_named_model : 
  string ->
  (unit -> unit model_monad) ->
  PulseModelsImport.model

val lift_to_monad : PulseModelsImport.model -> unit model_monad

beware that the model may modify the model_data.ret field

val lift_to_monad_and_get_result : PulseModelsImport.model -> aval model_monad

apply the model and return its result. fails if the model did not assign the reserved model_data.ret variable.

Operations

PulseOperations functions you need should be copied here

val allocation : 
  Pulselib.PulseBasicInterface.Attribute.allocator ->
  aval ->
  unit model_monad

val is_allocated : aval -> bool model_monad

val data_dependency : 
  Pulselib.PulseBasicInterface.ValueOrigin.t ->
  Pulselib.PulseBasicInterface.ValueOrigin.t list ->
  unit model_monad

val data_dependency_to_ret : 
  Pulselib.PulseBasicInterface.ValueOrigin.t list ->
  unit model_monad

val add_dict_read_const_key : aval -> IR.Fieldname.t -> unit model_monad

val is_dict_contain_const_keys : aval -> bool model_monad

val remove_dict_contain_const_keys : aval -> unit model_monad

val is_hack_constinit_called : aval -> bool model_monad

val set_hack_constinit_called : aval -> unit model_monad

val add_static_type : IR.Typ.name -> aval -> unit model_monad

val get_static_type : aval -> IR.Typ.name option model_monad

val deep_copy : ?depth_max:int -> aval -> aval model_monad

val check_valid : 
  ?must_be_valid_reason:
    Pulselib.PulseBasicInterface.Invalidation.must_be_valid_reason ->
  Pulselib.PulseBasicInterface.ValueOrigin.t ->
  unit model_monad

val binop : IR.Binop.t -> aval -> aval -> aval model_monad

val binop_int : IR.Binop.t -> aval -> IR.IntLit.t -> aval model_monad

val unop : IR.Unop.t -> aval -> aval model_monad

val read : IR.Exp.t -> aval model_monad

val remove_allocation_attr_transitively : aval list -> unit model_monad

val int : 
  ?hist:Pulselib.PulseBasicInterface.ValueHistory.t ->
  int ->
  aval model_monad

val string : string -> aval model_monad

val string_concat : aval -> aval -> aval model_monad

val access : 
  PulseOperationResult.Import.access_mode ->
  aval ->
  Pulselib.PulseBasicInterface.Access.t ->
  aval model_monad

val load_access : 
  ?no_access:bool ->
  ?deref:bool ->
  aval ->
  Pulselib.PulseBasicInterface.Access.t ->
  aval model_monad

val load : aval -> aval model_monad

read the Dereference access from the value

val and_dynamic_type_is : aval -> IR.Typ.t -> unit model_monad

val get_dynamic_type : 
  ask_specialization:bool ->
  aval ->
  Pulselib.PulseBasicInterface.Formula.dynamic_type_data option model_monad

val new_ : IR.Exp.t -> aval model_monad

val constructor : 
  ?deref:bool ->
  ?field_of_string:(string -> IR.Fieldname.t) ->
  IR.Typ.Name.t ->
  (string * aval) list ->
  aval model_monad

constructor_dsl typ_name fields builds a fresh object of type typ_name and initializes its fields using list fields

val construct_dict : 
  ?deref:bool ->
  ?field_of_string:(string -> IR.Fieldname.t) ->
  IR.Typ.name ->
  (string
   * (Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t))
    list ->
  const_strings_only:bool ->
  aval model_monad

val remove_hack_builder_attributes : aval -> unit model_monad

val fresh : ?more:string -> unit -> aval model_monad

val fresh_nonneg : ?more:string -> unit -> aval model_monad

val write_field : ref:aval -> IR.Fieldname.t -> aval -> unit model_monad

val store_field : 
  ?deref:bool ->
  ref:aval ->
  IR.Fieldname.t ->
  aval ->
  unit model_monad

val store : ref:aval -> aval -> unit model_monad

val get_known_fields : 
  aval ->
  Pulselib.PulseBasicInterface.Access.t list model_monad

Return the fields we know about. There may be more, so use with caution

val is_known_field : aval -> IR.Fieldname.t -> bool model_monad

Return true if the given field appears for sure. Otherwise (missing or if we don't know), return false

PulseFormula operations

val prune_eq : aval -> aval -> unit model_monad

val prune_eq_int : aval -> IR.IntLit.t -> unit model_monad

val prune_eq_string : aval -> string -> unit model_monad

val prune_ne_string : aval -> string -> unit model_monad

val prune_eq_zero : aval -> unit model_monad

val prune_positive : aval -> unit model_monad

val prune_lt : aval -> aval -> unit model_monad

val prune_lt_int : aval -> IR.IntLit.t -> unit model_monad

val prune_le : aval -> aval -> unit model_monad

val prune_gt : aval -> aval -> unit model_monad

val prune_gt_int : aval -> IR.IntLit.t -> unit model_monad

val prune_ge : aval -> aval -> unit model_monad

val prune_ge_int : aval -> IR.IntLit.t -> unit model_monad

val prune_ne : aval -> aval -> unit model_monad

val prune_ne_int : aval -> IR.IntLit.t -> unit model_monad

val prune_ne_zero : aval -> unit model_monad

val and_eq_int : aval -> IR.IntLit.t -> unit model_monad

val and_eq : aval -> aval -> unit model_monad

val and_equal_instanceof : 
  aval ->
  aval ->
  IR.Typ.t ->
  nullable:bool ->
  unit model_monad

val and_positive : aval -> unit model_monad

val as_constant_q : aval -> Q.t option model_monad

val as_constant_int : aval -> int option model_monad

val as_constant_bool : aval -> bool option model_monad

val as_constant_string : aval -> string option model_monad

val null : aval model_monad

Tenv operations

val tenv_get_supers : IR.Typ.name -> IR.Typ.name list model_monad

val tenv_resolve_field_info : 
  IR.Typ.name ->
  IR.Fieldname.t ->
  IR.Struct.field_info option model_monad

val tenv_resolve_fieldname : 
  IR.Typ.name ->
  string ->
  (IR.Fieldname.t option * IR.Tenv.unresolved_reason option) model_monad

val tenv_type_is_defined : IR.Typ.name -> bool model_monad

Invalidation operations

val invalidate_access : 
  Pulselib.PulseBasicInterface.Invalidation.t ->
  aval ->
  Pulselib.PulseBasicInterface.Access.t ->
  unit model_monad

Escape Hatches

if necessary you can convert an operation outside of this module with the following operators

val exec_command : (astate -> astate) -> unit model_monad

val exec_partial_command : 
  (astate -> astate PulseOperationResult.t) ->
  unit model_monad

val exec_operation : (astate -> 'a * astate) -> 'a model_monad

val exec_partial_operation : 
  (astate -> (astate * 'a) PulseOperationResult.t) ->
  'a model_monad

val exec_pure_operation : (astate -> 'a) -> 'a model_monad

val register_class_object_for_value : aval -> aval -> unit model_monad

This is used to make hack_get_static_class behave like a pure function

module Basic : sig ... end