(* TODO? use size *)

let exec {integer_type_widths} ~ret:(id, _) mem =

L.d_printfln_escaped "Using model std::array<_, %Ld>::at" size ;

Dom.Mem.add_stack (Loc.of_id id)

(Sem.eval_lindex integer_type_widths array_exp index_exp mem)

mem

and check {location; integer_type_widths} mem cond_set =

BoUtils.Check.lindex integer_type_widths ~array_exp ~index_exp ~last_included:false mem location

cond_set

in

let exec {integer_type_widths} ~ret:(id, _) mem =

let i1 = Sem.eval integer_type_widths e1 mem |> Dom.Val.get_itv in

let i2 = Sem.eval integer_type_widths e2 mem |> Dom.Val.get_itv in

let v = f i1 i2 |> Dom.Val.of_itv in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

| Exp.BinOp (Binop.Mult _, Exp.Sizeof {typ; nbytes}, length)

| Exp.BinOp (Binop.Mult _, length, Exp.Sizeof {typ; nbytes}) ->

Some (typ, nbytes, length, None)

(* In Java all arrays are dynamically allocated *)

| Exp.Sizeof {typ; nbytes; dynamic_length= Some arr_length} when Language.curr_language_is Java ->

Some (typ, nbytes, arr_length, Some arr_length)

| Exp.Sizeof {typ; nbytes; dynamic_length} ->

Some (typ, nbytes, Exp.one, dynamic_length)

| _ ->

let _, _, length0, _ = get_malloc_info size_exp in

let v_length = Sem.eval integer_type_widths length0 mem in

match Dom.Val.get_itv v_length with

| Bottom ->

cond_set

| NonBottom length ->

let traces = Dom.Val.get_traces v_length in

let latest_prune = Dom.Mem.get_latest_prune mem in

let exec {integer_type_widths} ~ret:(id, _) mem =

let str_v = Sem.eval integer_type_widths str_exp mem in

let num_v = Sem.eval integer_type_widths num_exp mem in

let traces = Trace.Set.join (Dom.Val.get_traces str_v) (Dom.Val.get_traces num_v) in

let update_strlen1 allocsite arrinfo acc =

let strlen =

let offset = ArrayBlk.ArrInfo.get_offset arrinfo in

let num = Dom.Val.get_itv num_v in

Itv.plus offset (Itv.set_lb_zero (Itv.decr num))

in

Dom.Mem.set_first_idx_of_null (Loc.of_allocsite allocsite) (Dom.Val.of_itv ~traces strlen) acc

in

mem

|> Dom.Mem.update_mem (Sem.eval_locs str_exp mem) Dom.Val.Itv.zero_255

|> ArrayBlk.fold update_strlen1 (Dom.Val.get_array_blk str_v)

|> Dom.Mem.add_stack (Loc.of_id id) {str_v with itv= Itv.zero}

|> Dom.Mem.fgets_alias id (Dom.Val.get_all_locs str_v)

and check {location; integer_type_widths} mem cond_set =

BoUtils.Check.lindex_byte integer_type_widths ~array_exp:str_exp ~byte_index_exp:num_exp

~last_included:true mem location cond_set

in

let exec ({pname; caller_pname; node_hash; location; tenv; integer_type_widths} as model_env)

~ret:(id, _) mem =

let size_exp = BiabductionProp.exp_normalize_noabs tenv size_exp in

let typ, stride, length0, dyn_length = get_malloc_info size_exp in

let length = Sem.eval integer_type_widths length0 mem in

let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in

let path =

Dom.Mem.find_simple_alias id mem

|> List.find_map ~f:(fun (rhs, i) -> if IntLit.iszero i then Loc.get_path rhs else None)

in

let offset, size = (Itv.zero, Dom.Val.get_itv length) in

let represents_multiple_values = not (Itv.is_one size) in

let allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path

~represents_multiple_values

in

let mem =

if Config.bo_bottom_as_default then mem

else

let loc = Loc.of_allocsite allocsite in

match Dom.Mem.find_opt loc mem with

| None ->

(* If the allocsite is not present in the abstract state, write bot as a value of

Dom.Mem.strong_update (PowLoc.singleton (Loc.of_allocsite allocsite)) Dom.Val.bot mem

| _ ->

(* If the allocsite is already in the abstract state, it means that we are in a loop.

mem

in

if Language.curr_language_is Java then

let internal_arr =

let allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None

~represents_multiple_values

in

Dom.Val.of_java_array_alloc allocsite ~length:size ~traces

in

let arr_loc = Loc.of_allocsite allocsite in

mem

|> Dom.Mem.add_heap arr_loc internal_arr

|> Dom.Mem.add_stack (Loc.of_id id) (Dom.Val.of_pow_loc ~traces (PowLoc.singleton arr_loc))

else

let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset ~size ~traces in

mem

|> Dom.Mem.add_stack (Loc.of_id id) v

|> BoUtils.Exec.init_c_array_fields model_env path typ (Dom.Val.get_array_locs v) ?dyn_length

and check = check_alloc_size ~can_be_zero size_exp in

let exec _ ~ret:_ mem =

let dest_loc = Sem.eval_locs dest_exp mem in

let v = Dom.Mem.find_set (Sem.eval_locs src_exp mem) mem in

Dom.Mem.update_mem dest_loc v mem

and check {location; integer_type_widths} mem cond_set =

BoUtils.Check.lindex_byte integer_type_widths ~array_exp:dest_exp ~byte_index_exp:size_exp

~last_included:true mem location cond_set

|> BoUtils.Check.lindex_byte integer_type_widths ~array_exp:src_exp ~byte_index_exp:size_exp

~last_included:true mem location

in

let exec _ ~ret:_ mem = mem

and check {location; integer_type_widths} mem cond_set =

BoUtils.Check.lindex_byte integer_type_widths ~array_exp:arr_exp ~byte_index_exp:size_exp

~last_included:true mem location cond_set

in

let exec _ ~ret:(id, _) mem =

let v = Sem.eval_string_len arr_exp mem in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

let exec {integer_type_widths} ~ret:(id, _) mem =

let src_loc = Sem.eval_locs src_exp mem in

let dest_loc = Sem.eval_locs dest_exp mem in

mem

|> Dom.Mem.update_mem dest_loc (Dom.Mem.find_set src_loc mem)

|> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) (Dom.Mem.get_c_strlen src_loc mem)

|> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem)

and check {integer_type_widths; location} mem cond_set =

let access_last_char =

let idx = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in

let latest_prune = Dom.Mem.get_latest_prune mem in

fun arr cond_set ->

BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune

location cond_set

in

cond_set

|> access_last_char (Sem.eval integer_type_widths dest_exp mem)

|> access_last_char (Sem.eval integer_type_widths src_exp mem)

in

let {exec= memcpy_exec; check= memcpy_check} = memcpy dest_exp src_exp size_exp in

let exec model_env ~ret mem =

let dest_strlen_loc = PowLoc.of_c_strlen (Sem.eval_locs dest_exp mem) in

let strlen = Dom.Mem.find_set (PowLoc.of_c_strlen (Sem.eval_locs src_exp mem)) mem in

mem |> memcpy_exec model_env ~ret |> Dom.Mem.update_mem dest_strlen_loc strlen

in

let exec {integer_type_widths} ~ret:(id, _) mem =

let src_loc = Sem.eval_locs src_exp mem in

let dest_loc = Sem.eval_locs dest_exp mem in

let new_contents =

let src_contents = Dom.Mem.find_set src_loc mem in

let dest_contents = Dom.Mem.find_set dest_loc mem in

Dom.Val.join dest_contents src_contents

in

let src_strlen = Dom.Mem.get_c_strlen src_loc mem in

let new_strlen =

let dest_strlen = Dom.Mem.get_c_strlen dest_loc mem in

Dom.Val.plus_a dest_strlen src_strlen

in

mem

|> Dom.Mem.update_mem dest_loc new_contents

|> Dom.Mem.update_mem (PowLoc.of_c_strlen dest_loc) new_strlen

|> Dom.Mem.add_stack (Loc.of_id id) (Sem.eval integer_type_widths dest_exp mem)

and check {integer_type_widths; location} mem cond_set =

let access_last_char arr idx cond_set =

let latest_prune = Dom.Mem.get_latest_prune mem in

BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location

cond_set

in

let src_strlen =

let str_loc = Sem.eval_locs src_exp mem in

Dom.Mem.get_c_strlen str_loc mem

in

let new_strlen =

let dest_strlen =

let dest_loc = Sem.eval_locs dest_exp mem in

Dom.Mem.get_c_strlen dest_loc mem

in

Dom.Val.plus_a dest_strlen src_strlen

in

cond_set

|> access_last_char (Sem.eval integer_type_widths dest_exp mem) new_strlen

|> access_last_char (Sem.eval integer_type_widths src_exp mem) src_strlen

in

let exec ({location; tenv; integer_type_widths} as model_env) ~ret:(id, _) mem =

let size_exp = BiabductionProp.exp_normalize_noabs tenv size_exp in

let typ, _, length0, dyn_length = get_malloc_info size_exp in

let length = Sem.eval integer_type_widths length0 mem in

let v = Sem.eval integer_type_widths src_exp mem |> Dom.Val.set_array_length location ~length in

let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in

Option.value_map dyn_length ~default:mem ~f:(fun dyn_length ->

let dyn_length = Dom.Val.get_itv (Sem.eval integer_type_widths dyn_length mem) in

BoUtils.Exec.set_dyn_length model_env typ (Dom.Val.get_array_locs v) dyn_length mem )

and check = check_alloc_size ~can_be_zero:false size_exp in

match (t1.Typ.desc, src_arg2_opt) with

| Tint _, None | Tint _, Some {typ= {Typ.desc= Tint _}} ->

malloc ~can_be_zero:true (Exp.BinOp (Binop.PlusA (Some Typ.size_t), size_exp, src_exp1))

| Tstruct (CppClass {name}), None

when [%equal: string list] (QualifiedCppName.to_list name) ["std"; "nothrow_t"] ->

malloc ~can_be_zero:true size_exp

| _, _ ->

let exec {integer_type_widths} ~ret:(id, _) mem =

let src_exp =

if Typ.is_pointer_to_void t1 then src_exp1

else

match src_arg2_opt with

| Some {exp= src_exp2; typ= t2} when Typ.is_pointer_to_void t2 ->

src_exp2

| _ ->

(* TODO: Raise an exception when given unexpected arguments. Before that, we need

L.d_error "Unexpected types of arguments for __placement_new" ;

src_exp1

in

let v = Sem.eval integer_type_widths src_exp mem in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

let exec ({pname; caller_pname; node_hash; location; integer_type_widths} as model_env)

~ret:((id, _) as ret) mem =

let v =

let src_strlen = Dom.Mem.get_c_strlen (Sem.eval_locs src_exp mem) mem in

let length = Sem.eval integer_type_widths length_exp mem in

let size = Itv.incr (Itv.min_sem (Dom.Val.get_itv src_strlen) (Dom.Val.get_itv length)) in

let allocsite =

let represents_multiple_values = not (Itv.is_one size) in

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None

~represents_multiple_values

in

let traces =

Trace.Set.join (Dom.Val.get_traces src_strlen) (Dom.Val.get_traces length)

|> Trace.Set.add_elem location Trace.Through

|> Trace.Set.add_elem location ArrayDeclaration

in

Dom.Val.of_c_array_alloc allocsite

~stride:(Some (integer_type_widths.char_width / 8))

~offset:Itv.zero ~size ~traces

in

mem

|> Dom.Mem.add_stack (Loc.of_id id) v

|> (strncpy (Exp.Var id) src_exp length_exp).exec model_env ~ret

in

let exec {integer_type_widths} ~ret:(ret_id, _) mem =

let v = Sem.eval integer_type_widths exp mem in

let v = match size_exp with Exp.Sizeof {typ} -> Dom.Val.cast typ v | _ -> v in

model_by_value v ret_id mem

in

let exec {integer_type_widths} ~ret:(ret_id, _) mem =

let v = Sem.eval integer_type_widths exp mem in

model_by_value v ret_id mem

in

let exec {location; integer_type_widths} ~ret:_ mem =

L.(debug BufferOverrun Medium)

"@[<v>=== Infer Print === at %a@,%a@]%!" Location.pp location Dom.Val.pp

(Sem.eval integer_type_widths e mem) ;

mem

in

match PowLoc.is_singleton_or_more arr_locs with

| IContainer.Singleton loc ->

Dom.Mem.load_size_alias id loc mem

| IContainer.Empty | IContainer.More ->

let exec _ ~ret:(ret_id, _) mem =

let arr_locs = Sem.eval_locs array_exp mem in

let result = Sem.eval_array_locs_length arr_locs mem in

model_by_value result ret_id mem |> load_size_alias ret_id arr_locs

in

let exec {pname; caller_pname; node_hash; location; integer_type_widths} ~ret:_ mem =

match (exp, typ) with

| Exp.Lvar array_pvar, {Typ.desc= Typ.Tarray {stride}} ->

let length = Sem.eval integer_type_widths length_exp mem in

let stride = Option.map ~f:IntLit.to_int_exn stride in

let path = Some (Symb.SymbolPath.of_pvar array_pvar) in

let traces = Trace.(Set.add_elem location ArrayDeclaration) (Dom.Val.get_traces length) in

let size = Dom.Val.get_itv length in

let allocsite =

let represents_multiple_values = not (Itv.is_one size) in

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path

~represents_multiple_values

in

let v = Dom.Val.of_c_array_alloc allocsite ~stride ~offset:Itv.zero ~size ~traces in

Dom.Mem.add_stack (Loc.of_pvar array_pvar) v mem

| _ ->

L.(die InternalError) "Unexpected type of first argument for __set_array_length() "

and check = check_alloc_size ~can_be_zero:false length_exp in

let exec ({integer_type_widths} as model) ~ret:(id, _) mem =

let array_v = Sem.eval integer_type_widths array_exp mem in

copy array_v id mem |> set_size model array_v length_exp

in

let exec {integer_type_widths} ~ret:(id, _) mem =

let array_v = Sem.eval integer_type_widths src_exp mem in

copy array_v id mem

in

let constructor _size =

let exec _model_env ~ret:_ mem =

mem

(* initialize? *)

in

{exec; check= no_check}

let at size {exp= array_exp} {exp= index_exp} = at ~size array_exp index_exp

let begin_ _size {exp= array_exp} =

let exec {location; integer_type_widths} ~ret:(id, _) mem =

let v =

Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location Itv.zero

in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

{exec; check= no_check}

let end_ size {exp= array_exp} =

let exec {location; integer_type_widths} ~ret:(id, _) mem =

let v =

let offset = Itv.of_int_lit (IntLit.of_int64 size) in

Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset

in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

{exec; check= no_check}

let back size {exp= array_exp} =

let exec {location; integer_type_widths} ~ret:(id, _) mem =

let v =

let offset = Itv.of_int_lit (IntLit.of_int64 Int64.(size - one)) in

Sem.eval integer_type_widths array_exp mem |> Dom.Val.set_array_offset location offset

in

Dom.Mem.add_stack (Loc.of_id id) v mem

in

{exec; check= no_check}

(* This is used in C++11 where there is an intermediate step for linking iterator to a temp *)

let new_ beg_exp temp_exp =

let exec _ ~ret:_ mem =

let locs_b = Sem.eval_locs beg_exp mem in

let locs_t = Sem.eval_locs temp_exp mem in

let v = Dom.Mem.find_set locs_t mem |> Dom.Val.get_itv |> Dom.Val.of_itv in

let mem = Dom.Mem.update_mem locs_b v mem in

match (beg_exp, temp_exp) with

| Exp.Lvar new_pvar, Exp.Lvar existing_pvar ->

Dom.Mem.propagate_cpp_iter_begin_or_end_alias ~new_pvar ~existing_pvar mem

| _ ->

mem

in

{exec; check= no_check}

let copy dest src =

let exec _ ~ret:_ mem =

let dest_loc = Sem.eval_locs dest mem in

let v = Dom.Mem.find_set (Sem.eval_locs src mem) mem in

Dom.Mem.update_mem dest_loc v mem

in

{exec; check= no_check}

let begin_ exp =

let exec _ ~ret:_ mem =

let locs = Sem.eval_locs exp mem in

let mem = Dom.Mem.update_mem locs Dom.Val.Itv.zero mem in

match exp with Exp.Lvar pvar -> Dom.Mem.add_cpp_iter_begin_alias pvar mem | _ -> mem

in

{exec; check= no_check}

let end_ ~size_exec temp_exp =

let exec model_env ~ret:((ret_id, _) as ret) mem =

let mem = size_exec model_env ~ret mem in

let locs = Sem.eval_locs temp_exp mem in

let v = Dom.Mem.find (Loc.of_id ret_id) mem in

let mem = Dom.Mem.update_mem locs v mem in

match temp_exp with Exp.Lvar pvar -> Dom.Mem.add_cpp_iter_end_alias pvar mem | _ -> mem

in

{exec; check= no_check}

let iterator_ne lhs_exp rhs_exp =

let exec {integer_type_widths} ~ret:(ret_id, _) mem =

let v = Sem.eval integer_type_widths (Exp.BinOp (Binop.Ne, lhs_exp, rhs_exp)) mem in

let mem =

match (lhs_exp, rhs_exp) with

| Exp.Lvar iter_lhs, Exp.Lvar iter_rhs ->

Dom.Mem.add_cpp_iterator_cmp_alias ret_id ~iter_lhs ~iter_rhs mem

| _, _ ->

mem

in

model_by_value v ret_id mem

in

{exec; check= no_check}

let iterator_incr iterator_exp =

let exec _ ~ret:_ mem =

let locs = Sem.eval_locs iterator_exp mem in

let v = Dom.Mem.find_set locs mem |> Dom.Val.get_itv |> Itv.incr |> Dom.Val.of_itv in

Dom.Mem.update_mem locs v mem

in

{exec; check= no_check}

let deref_of {integer_type_widths} exp ~fn ?fn_typ mem =

let typ = Option.map fn_typ ~f:Typ.mk_ptr in

Dom.Val.get_all_locs (Sem.eval_arr integer_type_widths exp mem) |> PowLoc.append_field ?typ ~fn

let eval_size model_env exp ~fn mem =

Sem.eval_array_locs_length (deref_of model_env exp ~fn mem) mem

let size_exec exp ~fn ?fn_typ ({integer_type_widths} as model_env) ~ret:(id, _) mem =

let locs = Sem.eval integer_type_widths exp mem |> Dom.Val.get_all_locs in

match PowLoc.is_singleton_or_more locs with

| Singleton (BoField.Prim (Loc.Allocsite (Allocsite.LiteralString s))) ->

model_by_value (Dom.Val.of_int (String.length s)) id mem

| _ ->

let arr_locs = deref_of model_env exp ~fn ?fn_typ mem in

let mem = Dom.Mem.add_stack (Loc.of_id id) (Sem.eval_array_locs_length arr_locs mem) mem in

load_size_alias id arr_locs mem

let at arr_exp ~fn ?fn_typ index_exp =

let exec ({pname; location} as model_env) ~ret:(id, typ) mem =

let array_v =

let locs = deref_of model_env arr_exp ~fn ?fn_typ mem in

if PowLoc.is_bot locs then Dom.Val.unknown_from typ ~callee_pname:(Some pname) ~location

else Dom.Mem.find_set locs mem

in

Dom.Mem.add_stack (Loc.of_id id) array_v mem

and check ({location; integer_type_widths} as model_env) mem cond_set =

let idx = Sem.eval integer_type_widths index_exp mem in

let arr = Dom.Mem.find_set (deref_of model_env arr_exp ~fn mem) mem in

let latest_prune = Dom.Mem.get_latest_prune mem in

BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included:false ~latest_prune location

cond_set

in

{exec; check}

let copy_constructor model_env deref_of_tgt ~fn ?fn_typ src_exp mem =

let deref_of_src = deref_of model_env src_exp ~fn ?fn_typ mem in

Dom.Mem.update_mem deref_of_tgt (Dom.Mem.find_set deref_of_src mem) mem

let constructor_from_char_ptr ({integer_type_widths} as model_env) tgt_deref ~fn ?char_typ src mem

=

let elem_locs = PowLoc.append_field ?typ:(Option.map char_typ ~f:Typ.mk_ptr) tgt_deref ~fn in

match src with

| Exp.Const (Const.Cstr s) ->

BoUtils.Exec.decl_string model_env ~do_alloc:true elem_locs s mem

| _ ->

let v = Sem.eval integer_type_widths src mem in

Dom.Mem.update_mem elem_locs v mem

let check_index ~last_included get_array_locs arr_id index_exp {location; integer_type_widths} mem

cond_set =

let arr =

let arr_locs = get_array_locs arr_id mem in

Dom.Mem.find_set arr_locs mem

in

let idx = Sem.eval integer_type_widths index_exp mem in

let latest_prune = Dom.Mem.get_latest_prune mem in

BoUtils.Check.array_access ~arr ~idx ~is_plus:true ~last_included ~latest_prune location

cond_set

let append_field loc ~vec_typ ~elt_typ =

Loc.append_field ~typ:(Typ.mk_ptr elt_typ) loc (BufferOverrunField.cpp_vector_elem ~vec_typ)

let append_fields locs ~vec_typ ~elt_typ =

PowLoc.append_field ~typ:(Typ.mk_ptr elt_typ) locs

~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)

let deref_of model_env elt_typ {exp= vec_exp; typ= vec_typ} mem =

let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in

ArrObjCommon.deref_of model_env vec_exp ~fn ~fn_typ:(Typ.mk_ptr elt_typ) mem

let set_size {location} locs new_size mem =

Dom.Mem.transform_mem locs mem ~f:(fun v ->

Dom.Val.set_array_length location ~length:new_size v )

(* The (3) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)

let constructor_size elt_typ {exp= vec_exp; typ= vec_typ} size_exp =

let {exec= malloc_exec; check} = malloc ~can_be_zero:true size_exp in

let exec ({pname; caller_pname; node_hash; integer_type_widths; location} as model_env)

~ret:((id, _) as ret) mem =

let mem = malloc_exec model_env ~ret mem in

let vec_locs = Sem.eval_locs vec_exp mem in

let deref_of_vec =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None

~represents_multiple_values:false

|> Loc.of_allocsite

in

let array_v =

Sem.eval integer_type_widths (Exp.Var id) mem

|> Dom.Val.add_assign_trace_elem location vec_locs

in

mem

|> Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec)

|> Dom.Mem.add_heap (append_field deref_of_vec ~vec_typ ~elt_typ) array_v

in

{exec; check}

(* The (1) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)

let constructor_empty elt_typ vec = constructor_size elt_typ vec Exp.zero

(* The (5) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)

let constructor_copy elt_typ {exp= vec_exp; typ= vec_typ} src_exp =

let exec ({integer_type_widths} as model_env) ~ret:_ mem =

let vec_locs, traces =

let v = Sem.eval integer_type_widths vec_exp mem in

(Dom.Val.get_all_locs v, Dom.Val.get_traces v)

in

let deref_of_vec = append_fields vec_locs ~vec_typ ~elt_typ in

let fn = BufferOverrunField.cpp_vector_elem ~vec_typ in

mem

|> Dom.Mem.update_mem vec_locs (Dom.Val.of_pow_loc ~traces deref_of_vec)

|> ArrObjCommon.copy_constructor model_env deref_of_vec ~fn ~fn_typ:(Typ.mk_ptr elt_typ)

src_exp

in

{exec; check= no_check}

(* The (10) constructor in https://en.cppreference.com/w/cpp/container/vector/vector *)

let constructor_initializer_list elt_typ {exp= vec_exp; typ= vec_typ} lst_exp =

let exec {pname; caller_pname; node_hash; location} ~ret:_ mem =

let arr_blk =

let internal_locs =

Sem.eval_locs lst_exp mem |> PowLoc.append_field ~fn:BoField.cpp_collection_internal_array

in

Dom.Mem.find_set internal_locs mem |> Dom.Val.get_array_blk

in

let deref_of_vec =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None

~represents_multiple_values:false

|> Loc.of_allocsite

in

let mem =

let vec_locs = Sem.eval_locs vec_exp mem in

Dom.Mem.update_mem vec_locs (Dom.Val.of_loc deref_of_vec) mem

in

let vec_arr_ploc = append_field deref_of_vec ~vec_typ ~elt_typ |> PowLoc.singleton in

let traces = Trace.Set.singleton location ArrayDeclaration in

let arr_as =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None

~represents_multiple_values:true

in

let v =

Dom.Val.of_c_array_alloc arr_as ~stride:None ~offset:Itv.zero

~size:(ArrayBlk.get_size arr_blk) ~traces

in

let vec_elt_locs = arr_as |> Loc.of_allocsite |> PowLoc.singleton in

let lst_elem_v = Dom.Mem.find_set (ArrayBlk.get_pow_loc arr_blk) mem in

mem |> Dom.Mem.strong_update vec_arr_ploc v |> Dom.Mem.update_mem vec_elt_locs lst_elem_v

in

{exec; check= no_check}

let at elt_typ {exp= vec_exp; typ= vec_typ} index_exp =

ArrObjCommon.at vec_exp

~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)

~fn_typ:(Typ.mk_ptr elt_typ) index_exp

let empty elt_typ vec_arg =

let exec model_env ~ret:(id, _) mem =

let deref_of_vec = deref_of model_env elt_typ vec_arg mem in

let array_v = Dom.Mem.find_set deref_of_vec mem in

let traces = Dom.Val.get_traces array_v in

let size = ArrayBlk.get_size (Dom.Val.get_array_blk array_v) in

let empty = Dom.Val.of_itv ~traces (Itv.of_bool (Itv.le_sem size Itv.zero)) in

let mem = model_by_value empty id mem in

match PowLoc.is_singleton_or_more deref_of_vec with

| IContainer.Singleton loc ->

Dom.Mem.load_empty_alias id loc mem

| IContainer.(Empty | More) ->

mem

in

{exec; check= no_check}

let data elt_typ vec_arg =

let exec model_env ~ret:(id, _) mem =

let arr = Dom.Mem.find_set (deref_of model_env elt_typ vec_arg mem) mem in

model_by_value arr id mem

in

{exec; check= no_check}

let add_n_element ~n elt_typ vec_arg elt_exp =

let exec ({integer_type_widths} as model_env) ~ret:_ mem =

let arr_locs = deref_of model_env elt_typ vec_arg mem in

let mem =

let new_size =

Sem.eval integer_type_widths n mem

|> Dom.Val.plus_a (Sem.eval_array_locs_length arr_locs mem)

in

set_size model_env arr_locs new_size mem

in

let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in

let elt_v = Dom.Mem.find_set (Sem.eval_locs elt_exp mem) mem in

Dom.Mem.update_mem elt_locs elt_v mem

in

{exec; check= no_check}

let push_back = add_n_element ~n:Exp.one

let insert_n elt_typ vec_arg n elt_exp = add_n_element ~n elt_typ vec_arg elt_exp

let insert_initializer_list elt_typ vec_arg lst_exp =

let exec model_env ~ret:_ mem =

let arr_locs = deref_of model_env elt_typ vec_arg mem in

let elt_locs = Dom.Val.get_all_locs (Dom.Mem.find_set arr_locs mem) in

let internal_arr =

let internal_array_locs =

Sem.eval_locs lst_exp mem |> PowLoc.append_field ~fn:BoField.cpp_collection_internal_array

in

Dom.Mem.find_set internal_array_locs mem

in

let arr_blk = Dom.Val.get_array_blk internal_arr in

let lst_elet = Dom.Mem.find_set (ArrayBlk.get_pow_loc arr_blk) mem in

let add_cnt = arr_blk |> ArrayBlk.get_size |> Dom.Val.of_itv in

let new_size = add_cnt |> Dom.Val.plus_a (Sem.eval_array_locs_length arr_locs mem) in

mem |> set_size model_env arr_locs new_size |> Dom.Mem.update_mem elt_locs lst_elet

in

{exec; check= no_check}

let size elt_typ {exp= vec_exp; typ= vec_typ} =

let exec =

ArrObjCommon.size_exec vec_exp

~fn:(BufferOverrunField.cpp_vector_elem ~vec_typ)

~fn_typ:(Typ.mk_ptr elt_typ)

in

{exec; check= no_check}

let resize elt_typ vec_arg size_exp =

let exec ({integer_type_widths} as model_env) ~ret:_ mem =

let arr_locs = deref_of model_env elt_typ vec_arg mem in

let new_size = Sem.eval integer_type_widths size_exp mem in

set_size model_env arr_locs new_size mem

in

{exec; check= no_check}

module Iterator = struct

let end_ elt_typ vec temp_exp = Iterator.end_ ~size_exec:(size elt_typ vec).exec temp_exp

end

let std_vector model_env ~adds_at_least_one ({typ= vector_typ} as vec_arg) mem =

match vector_typ with

| Typ.

{ desc=

Tptr

( {desc= Tstruct (CppClass {template_spec_info= Template {args= TType elt_typ :: _}})}

, _ ) } ->

let arr_locs = StdVector.deref_of model_env elt_typ vec_arg mem in

let size = if adds_at_least_one then Dom.Val.Itv.pos else Dom.Val.Itv.nat in

StdVector.set_size model_env arr_locs size mem

| _ ->

Logging.d_printfln_escaped "Could not find element type of vector" ;

mem

module Split = struct

let std_vector vector_arg =

let exec model_env ~ret:_ mem =

Split.std_vector model_env ~adds_at_least_one:true vector_arg mem

in

{exec; check= no_check}

end

module Split = struct

let std_vector vector_arg ignore_empty_opt =

let exec ({integer_type_widths} as model_env) ~ret:_ mem =

let adds_at_least_one =

match ignore_empty_opt with

| Some ignore_empty_exp ->

Sem.eval integer_type_widths ignore_empty_exp mem |> Dom.Val.get_itv |> Itv.is_false

| None ->

(* default: ignore_empty is false *)

true

in

Split.std_vector model_env ~adds_at_least_one vector_arg mem

in

{exec; check= no_check}

end

let constructor_from_char_ptr char_typ {exp= tgt_exp; typ= tgt_typ} src ~len_opt =

let exec ({pname; caller_pname; node_hash} as model_env) ~ret mem =

let mem =

Option.value_map len_opt ~default:mem ~f:(fun len ->

let {exec= malloc_exec} = malloc ~can_be_zero:true len in

malloc_exec model_env ~ret mem )

in

let tgt_locs = Sem.eval_locs tgt_exp mem in

let tgt_deref =

let allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None

~represents_multiple_values:false

in

PowLoc.singleton (Loc.of_allocsite allocsite)

in

let mem =

Dom.Mem.update_mem tgt_locs (Dom.Val.of_pow_loc ~traces:Trace.Set.bottom tgt_deref) mem

in

let fn = BufferOverrunField.cpp_vector_elem ~vec_typ:tgt_typ in

ArrObjCommon.constructor_from_char_ptr model_env tgt_deref src ~fn ~char_typ mem

in

let check ({location; integer_type_widths} as model_env) mem cond_set =

Option.value_map len_opt ~default:cond_set ~f:(fun len ->

let {check= malloc_check} = malloc ~can_be_zero:true len in

let cond_set = malloc_check model_env mem cond_set in

BoUtils.Check.lindex integer_type_widths ~array_exp:src ~index_exp:len ~last_included:true

mem location cond_set )

in

{exec; check}

(* The (4) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)

let constructor_from_char_ptr_with_len char_typ tgt_arg src len =

constructor_from_char_ptr char_typ tgt_arg src ~len_opt:(Some len)

(* The (5) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)

let constructor_from_char_ptr_without_len char_typ tgt_arg src =

constructor_from_char_ptr char_typ tgt_arg src ~len_opt:None

(* The (7) constructor in https://en.cppreference.com/w/cpp/string/basic_string/basic_string *)

let copy_constructor = StdVector.constructor_copy

let empty = StdVector.empty

let length = StdVector.size

let intValue exp =

let exec _ ~ret:(id, _) mem =

let powloc = Sem.eval_locs exp mem in

let v = if PowLoc.is_bot powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in

model_by_value v id mem

in

{exec; check= no_check}

let valueOf exp =

let exec {pname; caller_pname; node_hash; location; integer_type_widths} ~ret:(id, _) mem =

let represents_multiple_values = false in

let int_allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:0 ~path:None

~represents_multiple_values

in

let v = Sem.eval integer_type_widths exp mem in

let int_loc = Loc.of_allocsite int_allocsite in

mem |> Dom.Mem.add_heap int_loc v

|> Dom.Mem.add_stack (Loc.of_id id)

( int_loc |> PowLoc.singleton

|> Dom.Val.of_pow_loc ~traces:Trace.(Set.singleton location JavaIntDecleration) )

in

{exec; check= no_check}

let create_collection {pname; caller_pname; node_hash; location} ~ret:(id, _) mem ~length =

let represents_multiple_values = true in

let traces = Trace.(Set.singleton location ArrayDeclaration) in

let coll_allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None

~represents_multiple_values

in

let internal_array =

let allocsite =

Allocsite.make pname ~caller_pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None

~represents_multiple_values

in

Dom.Val.of_java_array_alloc allocsite ~length ~traces

in

let coll_loc = Loc.of_allocsite coll_allocsite in

let internal_array_loc = Loc.append_field coll_loc Lang.collection_internal_array_field in

mem

|> Dom.Mem.add_heap internal_array_loc internal_array

|> Dom.Mem.add_stack (Loc.of_id id) (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces)

let new_collection =

let exec = create_collection ~length:Itv.zero in

{exec; check= no_check}

let allocate size_exp =

let exec ({integer_type_widths} as env) ~ret mem =

let length = Sem.eval integer_type_widths size_exp mem |> Dom.Val.get_itv in

create_collection env ~ret mem ~length

in

{exec; check= no_check}