PulseModelsDSL.Syntax
module ModeledField = PulseOperations.ModeledField
val let* : 'a model_monad -> ('a -> 'b model_monad) -> 'b model_monad
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 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
assign the value to the return variable of the current function
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 ->
(IR.Exp.t * IR.Typ.t) list ->
Pulselib.PulseBasicInterface.ValueOrigin.t
Absint.ProcnameDispatcher.Call.FuncArg.t
list ->
unit model_monad
val get_data : PulseModelsImport.model_data model_monad
val disjuncts : 'a model_monad list -> 'a model_monad
val start_model : unit model_monad -> PulseModelsImport.model
get a model from a disjunctive model_monad
val lift_to_monad : PulseModelsImport.model -> unit model_monad
beware that the model may modify the PulseModelsImport.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.
PulseOperations
functions you need should be copied here
val allocation :
Pulselib.PulseBasicInterface.Attribute.allocator ->
aval ->
unit model_monad
val add_dict_contain_const_keys : aval -> unit model_monad
val add_dict_read_const_key : aval -> IR.Fieldname.t -> unit model_monad
val remove_dict_contain_const_keys : aval -> unit model_monad
val add_static_type : IR.Typ.name -> aval -> unit model_monad
val deep_copy : ?depth_max:int -> aval -> aval model_monad
val eval_binop : IR.Binop.t -> aval -> aval -> aval model_monad
val eval_binop_int : IR.Binop.t -> aval -> IR.IntLit.t -> aval model_monad
val eval_read : IR.Exp.t -> aval model_monad
val eval_const_int : int -> aval model_monad
val eval_const_string : string -> aval model_monad
val eval_string_concat : aval -> aval -> aval model_monad
val eval_to_value_origin :
IR.Exp.t ->
Pulselib.PulseBasicInterface.ValueOrigin.t model_monad
val eval_access :
?desc:string ->
PulseOperationResult.Import.access_mode ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
aval model_monad
val eval_deref_access :
PulseOperationResult.Import.access_mode ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
aval 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 : 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 get_const_string : aval -> string option model_monad
val mk_fresh : model_desc:string -> ?more:string -> unit -> aval model_monad
val write_field : ref:aval -> obj:aval -> IR.Fieldname.t -> unit model_monad
val write_deref_field :
ref:aval ->
obj:aval ->
IR.Fieldname.t ->
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 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_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 aval_of_int :
Pulselib.PulseBasicInterface.ValueHistory.t ->
int ->
aval 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 model_monad
val write_deref : ref:aval -> obj:aval -> unit model_monad
val invalidate_access :
Pulselib.PulseBasicInterface.Invalidation.t ->
aval ->
Pulselib.PulseBasicInterface.Access.t ->
unit model_monad
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