Skip to content

Remove type argument from do_update_offset, fix calls with incorrect offset type #1984

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
sim642 wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Remove type argument from do_update_offset, fix calls with incorrect offset type #1984

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
01ac79a
Remove type argument from do_update_offset
sim642 Apr 9, 2026
cc6efe6
Fix lval type in base globals initialization
sim642 Apr 9, 2026
3014833
Fix offset used for lval type calculation in base set_mval
sim642 Apr 9, 2026
4d3d8e3
Fix lval type in base entire var refinement
sim642 Apr 9, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions src/analyses/base.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand All @@ -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 =
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/baseInvariant.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand Down
33 changes: 14 additions & 19 deletions src/cdomain/value/cdomains/valueDomain.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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 *)
Expand Down Expand Up @@ -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 ->
Expand All @@ -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) ->
Expand Down Expand Up @@ -1125,20 +1123,17 @@ 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
| `Index (idx, offs) -> begin
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 ->
Expand All @@ -1147,15 +1142,15 @@ 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
let newl = BatOption.default (ID.starting (Cilfacade.ptrdiff_ikind ()) Z.zero) len_id in
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
Expand All @@ -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
Expand Down
Loading