From 01ac79a23005045f124b0cc3e8f92817489043fe Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 13:32:39 +0300 Subject: [PATCH 1/4] Remove type argument from do_update_offset Makes it consistent with do_eval_offset. This breaks a lot of tests. --- src/cdomain/value/cdomains/valueDomain.ml | 33 ++++++++++------------- 1 file changed, 14 insertions(+), 19 deletions(-) diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index 401da647a2..761476fef0 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -978,7 +978,7 @@ struct do_eval_offset x offs l o let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = - let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option) (t:typ):t = (* TODO: why does inner t argument change here, but not in eval_offset? *) + let rec do_update_offset ?(bitfield:int option=None) (x:t) (offs:offs) (l:lval option) (o:offset option):t = if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value; let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in let r = @@ -989,7 +989,7 @@ struct begin let l', o' = shift_one_over l o in let x = zero_init_calloced_memory zeroinit x t in - mu (Blob (join x (do_update_offset x ofs l' o' t), s, zeroinit)) + mu (Blob (join x (do_update_offset x ofs l' o'), s, zeroinit)) end | Blob (x,s,zeroinit), `Field(f, _) -> begin @@ -1009,9 +1009,9 @@ struct | _ -> false in if do_strong_update then - Blob ((do_update_offset x offs l' o' t), s, zeroinit) + Blob ((do_update_offset x offs l' o'), s, zeroinit) else - mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit)) + mu (Blob (join x (do_update_offset x offs l' o'), s, zeroinit)) end | Blob (x,s,zeroinit), `NoOffset -> (* `NoOffset is only remaining possibility for Blob here *) begin @@ -1036,9 +1036,9 @@ struct end in if do_strong_update then - Blob ((do_update_offset x offs l' o' t), s, zeroinit) + Blob ((do_update_offset x offs l' o'), s, zeroinit) else - mu (Blob (join x (do_update_offset x offs l' o' t), s, zeroinit)) + mu (Blob (join x (do_update_offset x offs l' o'), s, zeroinit)) end | Thread _, _ -> (* hack for pthread_t variables *) @@ -1076,12 +1076,11 @@ struct | _ -> value end | `Field (fld, offs) when fld.fcomp.cstruct -> begin - let t = fld.ftype in match x with | Struct str -> begin let l', o' = shift_one_over l o in - let value' = do_update_offset ~bitfield:fld.fbitfield (Structs.get str fld) offs l' o' t in + let value' = do_update_offset ~bitfield:fld.fbitfield (Structs.get str fld) offs l' o' in Struct (Structs.replace str fld value') end | Bot -> @@ -1092,12 +1091,11 @@ struct in let strc = init_comp fld.fcomp in let l', o' = shift_one_over l o in - Struct (Structs.replace strc fld (do_update_offset Bot offs l' o' t)) + Struct (Structs.replace strc fld (do_update_offset Bot offs l' o')) | Top -> M.warn ~category:Imprecise "Trying to update a field, but the struct is unknown"; top () | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a struct"; top () end | `Field (fld, offs) -> begin - let t = fld.ftype in let l', o' = shift_one_over l o in match x with | Union (last_fld, prev_val) -> @@ -1125,8 +1123,8 @@ struct top (), offs end in - Union (`Lifted fld, do_update_offset tempval tempoffs l' o' t) - | Bot -> Union (`Lifted fld, do_update_offset Bot offs l' o' t) + Union (`Lifted fld, do_update_offset tempval tempoffs l' o') + | Bot -> Union (`Lifted fld, do_update_offset Bot offs l' o') | Top -> M.warn ~category:Imprecise "Trying to update a field, but the union is unknown"; top () | _ -> M.warn ~category:Imprecise "Trying to update a field, but was not given a union"; top () end @@ -1134,11 +1132,8 @@ struct let l', o' = shift_one_over l o in match x with | Array x' -> - let t = (match Cil.unrollType t with - | TArray(t1 ,_,_) -> t1 - | _ -> t) in (* This is necessary because t is not a TArray in case of calloc *) let e = determine_offset ask l o exp (Some v) in - let new_value_at_index = do_update_offset (CArrays.get ask x' (e,idx)) offs l' o' t in + let new_value_at_index = do_update_offset (CArrays.get ask x' (e,idx)) offs l' o' in let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in Array new_array_value | Bot -> @@ -1147,7 +1142,7 @@ struct | _ -> t, None) in (* This is necessary because t is not a TArray in case of calloc *) let x' = CArrays.bot () in let e = determine_offset ask l o exp (Some v) in - let new_value_at_index = do_update_offset Bot offs l' o' t in + let new_value_at_index = do_update_offset Bot offs l' o' in let new_array_value = CArrays.set ask x' (e, idx) new_value_at_index in let len_ci = BatOption.bind len (fun e -> Cil.getInteger @@ Cil.constFold true e) in let len_id = BatOption.map (IndexDomain.of_int (Cilfacade.ptrdiff_ikind ())) len_ci in @@ -1155,7 +1150,7 @@ struct let new_array_value = CArrays.update_length newl new_array_value in Array new_array_value | Top -> M.warn ~category:Imprecise "Trying to update an index, but the array is unknown"; top () - | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o' t + | x when GobOption.exists (Z.equal Z.zero) (IndexDomain.to_int idx) -> do_update_offset x offs l' o' | _ -> M.warn ~category:Imprecise "Trying to update an index, but was not given an array(%a)" pretty x; top () end in mu result @@ -1167,7 +1162,7 @@ struct | Some(Lval (x,o)) -> Some ((x, NoOffset)), Some(o) | _ -> None, None in - do_update_offset x offs l o t + do_update_offset x offs l o let rec affect_move ?(replace_with_const=false) ask (x:t) (v:varinfo) movement_for_expr:t = let move_fun x = affect_move ~replace_with_const:replace_with_const ask x v movement_for_expr in From cc6efe6c66cdadf9d189663d1b87977dd1498aad Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 13:38:44 +0300 Subject: [PATCH 2/4] Fix lval type in base globals initialization The bot_value is constructed for the variable, but update_offset goes deeper into fields. --- src/analyses/base.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 3cde51b49b..b4cbc3a3dd 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2002,7 +2002,7 @@ struct let t = v.vtype in let iv = VD.bot_value ~varAttr:v.vattr t in (* correct bottom value for top level variable *) if M.tracing then M.tracel "set" "init bot value (%a): %a" d_plaintype t VD.pretty iv; - let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some (Lval lval)) lval t in (* do desired update to value *) + let nv = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) iv offs rval_val (Some (Lval lval)) lval lval_t in (* do desired update to value *) set_savetop ~man man.local (AD.of_var v) lval_t nv ~lval_raw:lval ~rval_raw:rval (* set top-level variable to updated value *) | _ -> set_savetop ~man man.local lval_val lval_t rval_val ~lval_raw:lval ~rval_raw:rval From 30148336f42f99aa95285a6e92456f7077645fc9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 13:47:33 +0300 Subject: [PATCH 3/4] Fix offset used for lval type calculation in base set_mval to_cil_offset is specific for partitioned arrays and drops indices. Thus, it can compute an incorrect type which doesn't match the actual offset. --- src/analyses/base.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index b4cbc3a3dd..80572a3b14 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1675,7 +1675,7 @@ struct * 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 ask = Analyses.ask_of_man man in - let cil_offset = Offs.to_cil_offset offs in + let cil_offset = Offs.to_cil_offset offs in (* Only for partitioned arrays! Drops indices. *) let t = match t_override with | Some t -> t | None -> @@ -1685,11 +1685,11 @@ struct lval_type else try - Cilfacade.typeOfLval (Var x, cil_offset) - with Cilfacade.TypeOfError _ -> + Offs.type_of ~base:x.vtype offs + with Offset.Type_of_error _ -> (* If we cannot determine the correct type here, we go with the one of the LVal *) (* This will usually lead to a type mismatch in the ValueDomain (and hence supertop) *) - M.debug ~category:Analyzer "Cilfacade.typeOfLval failed Could not obtain the type of %a" d_lval (Var x, cil_offset); + M.debug ~category:Analyzer "Could not obtain the type of %a" Addr.Mval.pretty (x, offs); lval_type in let update_offset old_value = @@ -1708,7 +1708,7 @@ struct else new_value in - if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" AD.pretty (AD.of_mval (x,offs)) d_type x.vtype D.pretty st; + if M.tracing then M.tracel "set" "update_one_addr: start with '%a' (type '%a') \nstate:%a" Addr.Mval.pretty (x,offs) d_type t D.pretty st; if isFunctionType x.vtype then begin if M.tracing then M.tracel "set" "update_one_addr: returning: '%a' is a function type " d_type x.vtype; st From 4d3d8e398a77be959e13cf5e5c795114d6a69051 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Apr 2026 13:50:13 +0300 Subject: [PATCH 4/4] Fix lval type in base entire var refinement The entire var is refined, but update_offset goes deeper into fields. --- src/analyses/baseInvariant.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index 1386df31aa..e159c9834e 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -103,7 +103,7 @@ struct let old_val = get_var ~man st var in let old_val = map_oldval old_val var.vtype in let offs = convert_offset ~man st o in - let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (var.vtype) in + let new_val = VD.update_offset (Queries.to_value_domain_ask (Analyses.ask_of_man man)) old_val offs c' (Some exp) x (Cilfacade.typeOfLval x) in let v = apply_invariant ~old_val ~new_val in if is_some_bot v then contra st else (