From 6c38c1cb8fee69832579b0ec2047df15b01144b1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 15:13:18 +0300 Subject: [PATCH 1/4] Name lval_type argument for base set --- src/analyses/base.ml | 84 ++++++++++++++++++++++---------------------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 3cde51b49b..bacac4ec50 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1673,7 +1673,7 @@ struct (* Updating a single varinfo*offset pair. NB! This function's type does * not include the flag. *) - let set_mval ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) ((x, offs): Addr.Mval.t) (lval_type: Cil.typ) (value: value): store = + let set_mval ~(man: _ man) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (st: store) ((x, offs): Addr.Mval.t) ~(lval_type: Cil.typ) (value: value): store = let ask = Analyses.ask_of_man man in let cil_offset = Offs.to_cil_offset offs in let t = match t_override with @@ -1812,20 +1812,20 @@ struct effect_on_arrays ask with_dep end - let set_var ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Cil.varinfo) (lval_type: Cil.typ) (value: value): store = - set_mval ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st (x, `NoOffset) lval_type value + let set_var ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Cil.varinfo) ~(lval_type: Cil.typ) (value: value): store = + set_mval ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st (x, `NoOffset) ~lval_type value - let set_addr ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Addr.t) (lval_type: Cil.typ) (value: value): store = - Option.map_default (fun x -> set_mval ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st x lval_type value) st (Addr.to_mval x) + let set_addr ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Addr.t) ~(lval_type: Cil.typ) (value: value): store = + Option.map_default (fun x -> set_mval ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st x ~lval_type value) st (Addr.to_mval x) (** [set st addr val] returns a state where [addr] is set to [val] * it is always ok to put None for lval_raw and rval_raw, this amounts to not using/maintaining * precise information about arrays. *) - let set ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = + let set ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (lval: AD.t) ~(lval_type: Cil.typ) (value: value) : store = let lval_raw = (Option.map (fun x -> Lval x) lval_raw) in if M.tracing then M.tracel "set" "lval: %a\nvalue: %a\nstate: %a" AD.pretty lval VD.pretty value CPA.pretty st.cpa; let update_one x store = - set_addr ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override store x lval_type value + set_addr ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override store x ~lval_type value in try (* We start from the current state and an empty list of global deltas, * and we assign to all the different possible places: *) @@ -1845,7 +1845,7 @@ struct let set_many ~man (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store = - set ~man acc lval typ value + set ~man acc lval ~lval_type:typ value in (* And fold over the list starting from the store turned wstore: *) List.fold_left f st lval_value_list @@ -1899,7 +1899,7 @@ struct let get_var = get_var let get_mval ~man st mval exp = get_mval ~man st mval exp let get ~man st addrs exp = get ~man st addrs exp - let set ~man st lval lval_type ?lval_raw value = set ~man ~invariant:true st lval lval_type ?lval_raw value + let set ~man st lval lval_type ?lval_raw value = set ~man ~invariant:true st lval ~lval_type ?lval_raw value (* TODO: name lval_type in BaseInvariant *) let refine_entire_var = true let map_oldval oldval _ = oldval @@ -1919,8 +1919,8 @@ struct let set_savetop ~man ?lval_raw ?rval_raw st adr lval_t v : store = if M.tracing then M.tracel "set" "savetop %a %a %a" AD.pretty adr d_type lval_t VD.pretty v; match v with - | Top -> set ~man st adr lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw - | v -> set ~man st adr lval_t v ?lval_raw ?rval_raw + | Top -> set ~man st adr ~lval_type:lval_t (VD.top_value (AD.type_of adr)) ?lval_raw ?rval_raw + | v -> set ~man st adr ~lval_type:lval_t v ?lval_raw ?rval_raw (************************************************************************** @@ -2058,7 +2058,7 @@ struct let body man f = let init_var (acc: store) v: store = - set_var ~man acc v v.vtype (VD.init_value ~varAttr:v.vattr v.vtype) + set_var ~man acc v ~lval_type:v.vtype (VD.init_value ~varAttr:v.vattr v.vtype) in List.fold_left init_var man.local f.slocals @@ -2082,7 +2082,7 @@ struct let t_override = Cilfacade.fundec_return_type fundec in assert (not (Cil.isVoidType t_override)); (* Returning a value from a void function, CIL removes the Return expression for us anyway. *) let rv = eval_rv ~man man.local exp in - let st' = set_var ~man ~t_override nst (return_varinfo ()) t_override rv in + let st' = set_var ~man ~t_override nst (return_varinfo ()) ~lval_type:t_override rv in match ThreadId.get_current ask with | `Lifted tid when ThreadReturn.is_current ask -> if not (ThreadIdDomain.Thread.is_main tid) then ( (* Only non-main return constitutes an implicit pthread_exit according to man page (https://github.com/goblint/analyzer/issues/1767#issuecomment-3642590227). *) @@ -2101,7 +2101,7 @@ struct else let current_value = eval_rv ~man man.local (Lval (Var v, NoOffset)) in let new_value = VD.update_array_lengths (eval_rv ~man man.local) current_value v.vtype in - set_var ~man man.local v v.vtype new_value + set_var ~man man.local v ~lval_type:v.vtype new_value (************************************************************************** * Function calls @@ -2154,7 +2154,7 @@ struct ); (* copied from set_many *) let f (acc: store) ((lval:Addr.t),(typ:Cil.typ),(value:value)): store = - let acc' = set_addr ~man acc lval typ value in + let acc' = set_addr ~man acc lval ~lval_type:typ value in if must then acc' else @@ -2421,7 +2421,7 @@ struct else VD.top_value (unrollType dest_typ) in - set ~man st dest_a dest_typ value in + set ~man st dest_a ~lval_type:dest_typ value in (* for string functions *) let eval_n = function (* if only n characters of a given string are needed, evaluate expression n to an integer option *) @@ -2467,15 +2467,15 @@ struct let lv_a = eval_lv ~man st lv_val in let lv_typ = Cilfacade.typeOfLval lv_val in if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *) - set ~man st lv_a lv_typ (f s1_a s2_a) + set ~man st lv_a ~lval_type:lv_typ (f s1_a s2_a) else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) - set ~man st lv_a lv_typ (f s1_a s2_a) + set ~man st lv_a ~lval_type:lv_typ (f s1_a s2_a) else - set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~man st lv_a ~lval_type:lv_typ (VD.top_value (unrollType lv_typ)) | _ -> (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) let _ = AD.string_writing_defined s1_a in - set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~man st s1_a ~lval_type:s1_typ (VD.top_value (unrollType s1_typ)) end (* else compute value in array domain *) else @@ -2483,11 +2483,11 @@ struct Option.map_default (fun lv -> eval_lv ~man st lv, Cilfacade.typeOfLval lv) (s1_a, s1_typ) lv in match (get ~man st s1_a None), get ~man st s2_a None with - | Array array_s1, Array array_s2 -> set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2) + | Array array_s1, Array array_s2 -> set ~man ~blob_destructive:true st lv_a ~lval_type:lv_typ (op_array array_s1 array_s2) | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType -> let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in - set ~man ~blob_destructive:true st lv_a lv_typ (op_array array_s1 array_s2) + set ~man ~blob_destructive:true st lv_a ~lval_type:lv_typ (op_array array_s1 array_s2) | Bot, Array array_s2 -> (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in @@ -2496,7 +2496,7 @@ struct try ValueDomainQueries.ID.unlift (ID.cast_to ~kind:Internal ptrdiff_ik) size (* TODO: proper castkind *) with Failure _ -> ID.top_of ptrdiff_ik in let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in - set ~man st lv_a lv_typ (op_array empty_array array_s2) + set ~man st lv_a ~lval_type:lv_typ (op_array empty_array array_s2) | Bot , _ when CilType.Typ.equal s2_typ charPtrType -> (* If we have bot inside here, we assume the blob is used as a char array and create one inside *) let ptrdiff_ik = Cilfacade.ptrdiff_ikind () in @@ -2507,19 +2507,19 @@ struct let empty_array = CArrays.make s_id (Int (ID.top_of IChar)) in let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in - set ~man st lv_a lv_typ (op_array empty_array array_s2) + set ~man st lv_a ~lval_type:lv_typ (op_array empty_array array_s2) | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType -> (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *) if op_addr = None then (* triggers warning, function only evaluated for side-effects *) let _ = AD.string_writing_defined s1_a in - set ~man st s1_a s1_typ (VD.top_value (unrollType s1_typ)) + set ~man st s1_a ~lval_type:s1_typ (VD.top_value (unrollType s1_typ)) else let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in - set ~man st lv_a lv_typ (op_array array_s1 array_s2) + set ~man st lv_a ~lval_type:lv_typ (op_array array_s1 array_s2) | _ -> - set ~man st lv_a lv_typ (VD.top_value (unrollType lv_typ)) + set ~man st lv_a ~lval_type:lv_typ (VD.top_value (unrollType lv_typ)) in (* Returns a tuple, the first is the address of the blob if one was allocated, the second is the returned address (may contain null pointer or be only null-pointer) *) let alloc loc size = @@ -2557,13 +2557,13 @@ struct | _ -> VD.top_value dest_typ in - set ~man st dest_a dest_typ value + set ~man st dest_a ~lval_type:dest_typ value | Bzero { dest; count; }, _ -> (* TODO: share something with memset special case? *) (* TODO: check count *) let dest_a, dest_typ = addr_type_of_exp dest in let value = VD.zero_init_value dest_typ in - set ~man st dest_a dest_typ value + set ~man st dest_a ~lval_type:dest_typ value | Memcpy { dest = dst; src; n; }, _ -> (* TODO: use n *) memory_copying dst src (Some n) | Strcpy { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_copy ar1 ar2 (eval_n n))) @@ -2585,7 +2585,7 @@ struct | Array array_s -> Int (CArrays.to_string_length array_s) | _ -> VD.top_value (unrollType dest_typ) in - set ~man st dest_a dest_typ value + set ~man st dest_a ~lval_type:dest_typ value ) st lv | Strstr { haystack; needle }, _ -> Option.map_default (fun lv_val -> @@ -2634,12 +2634,12 @@ struct let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in let dest_typ = get_type dst_lval in let dest_a = eval_lv ~man st dst_lval in - let fallback () = set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) in + let fallback () = set ~man st dest_a ~lval_type:dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) in match eval_rv ~man st mtyp with | Int x -> Option.map_default_delayed (fun z -> if M.tracing then M.tracel "attr" "setting"; - set ~man st dest_a dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z)) + set ~man st dest_a ~lval_type:dest_typ (MutexAttr (ValueDomain.MutexAttr.of_int z)) ) fallback (ID.to_int x) | _ -> fallback () end @@ -2713,7 +2713,7 @@ struct | Abs (ik, x) -> Int (ID.cast_to ~kind:Internal ik (apply_abs ik x)) (* TODO: proper castkind *) end in - Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) result) st lv + Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) result) st lv (* handling thread creations *) | ThreadCreate _, _ -> invalidate_ret_lv man.local (* actual results joined via threadspawn *) @@ -2729,7 +2729,7 @@ struct | Thread a -> let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (man.global (V.thread x))) (ValueDomain.Threads.elements a)) in (* TODO: is this type right? *) - set ~man st ret_a (Cilfacade.typeOf ret_var) v + set ~man st ret_a ~lval_type:(Cilfacade.typeOf ret_var) v | _ -> invalidate ~must:true ~man st [ret_var] end | _ -> invalidate ~must:true ~man st [ret_var] @@ -2742,7 +2742,7 @@ struct | ThreadSelf, _ -> begin match lv, ThreadId.get_current (Analyses.ask_of_man man) with | Some lv, `Lifted tid -> - set ~man st (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid)) + set ~man st (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid)) | Some lv, _ -> invalidate_ret_lv st | None, _ -> @@ -2816,13 +2816,13 @@ struct let st' = match eval_rv ~man st env with | Address jmp_buf -> let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (man.prev_node, man.control_context ())), false) in - let r = set ~man st jmp_buf (Cilfacade.typeOf env) value in + let r = set ~man st jmp_buf ~lval_type:(Cilfacade.typeOf env) value in if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a" d_exp env D.pretty st D.pretty r; r | _ -> failwith "problem?!" in Option.map_default (fun lv -> - set ~man st' (eval_lv ~man st lv) (Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero)) + set ~man st' (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero)) ) st' lv | Longjmp {env; value}, _ -> let ensure_not_zero (rv:value) = match rv with @@ -2843,11 +2843,11 @@ struct in let rv = ensure_not_zero @@ eval_rv ~man man.local value in let t = Cilfacade.typeOf value in - set_var ~man ~t_override:t man.local !longjmp_return t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) + set_var ~man ~t_override:t man.local !longjmp_return ~lval_type:t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) | Rand, _ -> Option.map_default (fun x -> let result:value = (Int (ID.starting IInt Z.zero)) in - set ~man st (eval_lv ~man st x) (Cilfacade.typeOfLval x) result + set ~man st (eval_lv ~man st x) ~lval_type:(Cilfacade.typeOfLval x) result ) st lv | _, _ -> let st = @@ -3076,7 +3076,7 @@ struct let get_var = get_var let get ~man st addrs exp = get ~man st addrs exp let get_mval ~man st mval exp = get_mval ~man st mval exp - let set ~man st lval lval_type ?lval_raw value = set ~man ~invariant:false st lval lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *) + let set ~man st lval lval_type ?lval_raw value = set ~man ~invariant:false st lval ~lval_type ?lval_raw value (* TODO: should have invariant false? doesn't work with empty cpa then, because meets *) let refine_entire_var = false let map_oldval oldval t_lval = @@ -3119,7 +3119,7 @@ struct let e_d' = WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () -> CPA.fold (fun x v acc -> - set_var ~man ~invariant:false acc x x.vtype v + set_var ~man ~invariant:false acc x ~lval_type:x.vtype v ) e_d.cpa man.local ) in @@ -3146,7 +3146,7 @@ struct Priv.enter_multithreaded ask (priv_getg man.global) (priv_sideg man.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) - set ~man man.local (eval_lv ~man man.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) + set ~man man.local (eval_lv ~man man.local lval) ~lval_type:(Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) | Events.Assert exp -> assert_fn man exp true | Events.Unassume {exp; tokens} -> From 3fc99dd1a79fd6fe3e1a274dd692d1822fb5702a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 15:24:15 +0300 Subject: [PATCH 2/4] Make base set_var lval_type argument optional --- src/analyses/base.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index bacac4ec50..ccb21bfb42 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1812,7 +1812,7 @@ struct effect_on_arrays ask with_dep end - let set_var ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Cil.varinfo) ~(lval_type: Cil.typ) (value: value): store = + let set_var ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Cil.varinfo) ?(lval_type: Cil.typ = x.vtype) (value: value): store = (* TODO: push default lval_type into set_mval *) set_mval ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st (x, `NoOffset) ~lval_type value let set_addr ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (x: Addr.t) ~(lval_type: Cil.typ) (value: value): store = @@ -2058,7 +2058,7 @@ struct let body man f = let init_var (acc: store) v: store = - set_var ~man acc v ~lval_type:v.vtype (VD.init_value ~varAttr:v.vattr v.vtype) + set_var ~man acc v (VD.init_value ~varAttr:v.vattr v.vtype) in List.fold_left init_var man.local f.slocals @@ -2082,7 +2082,7 @@ struct let t_override = Cilfacade.fundec_return_type fundec in assert (not (Cil.isVoidType t_override)); (* Returning a value from a void function, CIL removes the Return expression for us anyway. *) let rv = eval_rv ~man man.local exp in - let st' = set_var ~man ~t_override nst (return_varinfo ()) ~lval_type:t_override rv in + let st' = set_var ~man ~t_override nst (return_varinfo ()) ~lval_type:t_override rv in (* TODO: lval_type is ignored if t_override is provided, so doesn't matter *) match ThreadId.get_current ask with | `Lifted tid when ThreadReturn.is_current ask -> if not (ThreadIdDomain.Thread.is_main tid) then ( (* Only non-main return constitutes an implicit pthread_exit according to man page (https://github.com/goblint/analyzer/issues/1767#issuecomment-3642590227). *) @@ -2101,7 +2101,7 @@ struct else let current_value = eval_rv ~man man.local (Lval (Var v, NoOffset)) in let new_value = VD.update_array_lengths (eval_rv ~man man.local) current_value v.vtype in - set_var ~man man.local v ~lval_type:v.vtype new_value + set_var ~man man.local v new_value (************************************************************************** * Function calls @@ -2843,7 +2843,7 @@ struct in let rv = ensure_not_zero @@ eval_rv ~man man.local value in let t = Cilfacade.typeOf value in - set_var ~man ~t_override:t man.local !longjmp_return ~lval_type:t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) + set_var ~man ~t_override:t man.local !longjmp_return ~lval_type:t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *) (* TODO: lval_type is ignored if t_override is provided, so doesn't matter *) | Rand, _ -> Option.map_default (fun x -> let result:value = (Int (ID.starting IInt Z.zero)) in @@ -3119,7 +3119,7 @@ struct let e_d' = WideningTokenLifter.with_side_tokens (WideningTokenLifter.TS.of_list uuids) (fun () -> CPA.fold (fun x v acc -> - set_var ~man ~invariant:false acc x ~lval_type:x.vtype v + set_var ~man ~invariant:false acc x v ) e_d.cpa man.local ) in From e17e3aaca5532765cb74975c429a41fe19ca8bab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 16:01:24 +0300 Subject: [PATCH 3/4] Extract set_lval in base --- src/analyses/base.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index ccb21bfb42..74fe3a354f 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1842,6 +1842,9 @@ struct (* if M.tracing then M.tracel "set" "set got an exception '%s'" x; *) M.info ~category:Unsound "Assignment to unknown address, assuming no write happened."; st + let set_lval ~(man: _ man) ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override (st: store) (lv: Cil.lval) ?(lval_type: Cil.typ = Cilfacade.typeOfLval lv) (value: value): store = (* TODO: push default lval_type into set? *) + set ~man ?invariant ?blob_destructive ?lval_raw ?rval_raw ?t_override st (eval_lv ~man st lv) ~lval_type value + let set_many ~man (st: store) lval_value_list: store = (* Maybe this can be done with a simple fold *) let f (acc: store) ((lval:AD.t),(typ:Cil.typ),(value:value)): store = @@ -2464,14 +2467,13 @@ struct begin match lv, op_addr with | Some lv_val, Some f -> (* when whished types coincide, compute result of operation op_addr, otherwise use top *) - let lv_a = eval_lv ~man st lv_val in let lv_typ = Cilfacade.typeOfLval lv_val in if all && typeSig s1_typ = typeSig s2_typ && typeSig s2_typ = typeSig lv_typ then (* all types need to coincide *) - set ~man st lv_a ~lval_type:lv_typ (f s1_a s2_a) + set_lval ~man st lv_val (f s1_a s2_a) else if not all && typeSig s1_typ = typeSig s2_typ then (* only the types of s1 and s2 need to coincide *) - set ~man st lv_a ~lval_type:lv_typ (f s1_a s2_a) + set_lval ~man st lv_val (f s1_a s2_a) else - set ~man st lv_a ~lval_type:lv_typ (VD.top_value (unrollType lv_typ)) + set_lval ~man st lv_val (VD.top_value (unrollType lv_typ)) | _ -> (* check if s1 is potentially a string literal as writing to it would be undefined behavior; then return top *) let _ = AD.string_writing_defined s1_a in @@ -2570,8 +2572,6 @@ struct | Strcat { dest = dst; src; n }, _ -> string_manipulation dst src None false None (fun ar1 ar2 -> Array (CArrays.string_concat ar1 ar2 (eval_n n))) | Strlen s, _ -> Option.map_default (fun lv -> - let dest_a = eval_lv ~man st lv in - let dest_typ = Cilfacade.typeOfLval lv in let v = eval_rv ~man st s in let a = address_from_value v in let value:value = @@ -2583,9 +2583,9 @@ struct else match get ~man st a None with | Array array_s -> Int (CArrays.to_string_length array_s) - | _ -> VD.top_value (unrollType dest_typ) + | _ -> VD.top_value (unrollType (Cilfacade.typeOfLval lv)) in - set ~man st dest_a ~lval_type:dest_typ value + set_lval ~man st lv value ) st lv | Strstr { haystack; needle }, _ -> Option.map_default (fun lv_val -> @@ -2713,7 +2713,7 @@ struct | Abs (ik, x) -> Int (ID.cast_to ~kind:Internal ik (apply_abs ik x)) (* TODO: proper castkind *) end in - Option.map_default (fun lv -> set ~man st (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) result) st lv + Option.map_default (fun lv -> set_lval ~man st lv result) st lv (* handling thread creations *) | ThreadCreate _, _ -> invalidate_ret_lv man.local (* actual results joined via threadspawn *) @@ -2742,7 +2742,7 @@ struct | ThreadSelf, _ -> begin match lv, ThreadId.get_current (Analyses.ask_of_man man) with | Some lv, `Lifted tid -> - set ~man st (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid)) + set_lval ~man st lv (Thread (ValueDomain.Threads.singleton tid)) | Some lv, _ -> invalidate_ret_lv st | None, _ -> @@ -2822,7 +2822,7 @@ struct | _ -> failwith "problem?!" in Option.map_default (fun lv -> - set ~man st' (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero)) + set ~man st' (eval_lv ~man st lv) ~lval_type:(Cilfacade.typeOfLval lv) (Int (ID.of_int IInt Z.zero)) (* TODO: why lv is evaled in st but set in st'? *) ) st' lv | Longjmp {env; value}, _ -> let ensure_not_zero (rv:value) = match rv with @@ -2847,7 +2847,7 @@ struct | Rand, _ -> Option.map_default (fun x -> let result:value = (Int (ID.starting IInt Z.zero)) in - set ~man st (eval_lv ~man st x) ~lval_type:(Cilfacade.typeOfLval x) result + set_lval ~man st x result ) st lv | _, _ -> let st = @@ -3146,7 +3146,7 @@ struct Priv.enter_multithreaded ask (priv_getg man.global) (priv_sideg man.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) - set ~man man.local (eval_lv ~man man.local lval) ~lval_type:(Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) + set_lval ~man man.local lval (Thread (ValueDomain.Threads.singleton tid)) | Events.Assert exp -> assert_fn man exp true | Events.Unassume {exp; tokens} -> From 8550336da7503dbb08cb986ca3ba2a39a0c01837 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 16:52:27 +0300 Subject: [PATCH 4/4] Use addr_type_of_exp more in base --- src/analyses/base.ml | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 74fe3a354f..73f1929d5d 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2413,9 +2413,7 @@ struct | _ -> false in let dest_a, dest_typ = addr_type_of_exp dst in - let src_lval = mkMem ~addr:(Cil.stripCasts src) ~off:NoOffset in - let src_typ = eval_lv ~man man.local src_lval - |> AD.type_of in + let _, src_typ = addr_type_of_exp src in (* when src and destination type coincide, take value from the source, otherwise use top *) let value = if (typeSig dest_typ = typeSig src_typ) && dest_size_equal_n then (* TODO: why cast if types coincide? *) @@ -2627,13 +2625,7 @@ struct raise Deadcode | MutexAttrSetType {attr = attr; typ = mtyp}, _ -> begin - let get_type lval = - let address = eval_lv ~man st lval in - AD.type_of address - in - let dst_lval = mkMem ~addr:(Cil.stripCasts attr) ~off:NoOffset in - let dest_typ = get_type dst_lval in - let dest_a = eval_lv ~man st dst_lval in + let dest_a, dest_typ = addr_type_of_exp attr in let fallback () = set ~man st dest_a ~lval_type:dest_typ (MutexAttr (ValueDomain.MutexAttr.top ())) in match eval_rv ~man st mtyp with | Int x ->