From 1aaec466e5234e8906fbf9075f3177bd99b88724 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Thu, 14 Sep 2023 15:42:30 +0200 Subject: [PATCH] Update malloced strings destructively where possible --- src/analyses/base.ml | 8 ++++---- src/cdomains/valueDomain.ml | 14 ++++++++------ tests/regression/73-strings/08-cursed.c | 7 +++---- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index cc8f912832..44ef339d2e 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1382,7 +1382,7 @@ struct (** [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 (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = + let set (a: Q.ask) ~(ctx: _ ctx) ?(invariant=false) ?(blob_destructive=false) ?lval_raw ?rval_raw ?t_override (gs:glob_fun) (st: store) (lval: AD.t) (lval_type: Cil.typ) (value: value) : store = let update_variable x t y z = if M.tracing then M.tracel "set" ~var:x.vname "update_variable: start '%s' '%a'\nto\n%a\n\n" x.vname VD.pretty y CPA.pretty z; let r = update_variable x t y z in (* refers to defintion that is outside of set *) @@ -1415,7 +1415,7 @@ struct let update_offset old_value = (* Projection globals to highest Precision *) let projected_value = project_val (Queries.to_value_domain_ask a) None None value (is_global a x) in - let new_value = VD.update_offset (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in + let new_value = VD.update_offset ~blob_destructive (Queries.to_value_domain_ask a) old_value offs projected_value lval_raw ((Var x), cil_offset) t in if WeakUpdates.mem x st.weak then VD.join old_value new_value else if invariant then ( @@ -2099,11 +2099,11 @@ struct | Some lv_val -> eval_lv (Analyses.ask_of_ctx ctx) gs st lv_val, Cilfacade.typeOfLval lv_val | None -> s1_a, s1_typ in begin match (get (Analyses.ask_of_ctx ctx) gs st s1_a None), get (Analyses.ask_of_ctx ctx) gs st s2_a None with - | Array array_s1, Array array_s2 -> set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) | Array array_s1, _ when 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 ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2) + set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a 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 size = ctx.ask (Q.BlobSize s1) in diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index e5c4727b72..9b4b09d930 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -19,7 +19,7 @@ sig include Lattice.S type offs val eval_offset: VDQ.t -> (AD.t -> t) -> t-> offs -> exp option -> lval option -> typ -> t - val update_offset: VDQ.t -> t -> offs -> t -> exp option -> lval -> typ -> t + val update_offset: ?blob_destructive:bool -> VDQ.t -> t -> offs -> t -> exp option -> lval -> typ -> t val update_array_lengths: (exp -> t) -> t -> Cil.typ -> t val affect_move: ?replace_with_const:bool -> VDQ.t -> t -> varinfo -> (exp -> int option) -> t val affecting_vars: t -> varinfo list @@ -288,12 +288,12 @@ struct true else false - | Some min, None -> + | Some min, None -> if Z.gt min Z.zero then true else false - | None, Some max -> + | None, Some max -> if Z.lt max Z.zero then true else @@ -953,7 +953,7 @@ struct in do_eval_offset ask f x offs exp l o v t - let update_offset (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t = + 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 (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t = if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a\n" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value; let mu = function Blob (Blob (y, s', orig), s, orig2) -> Blob (y, ID.join s s',orig) | x -> x in @@ -1001,9 +1001,11 @@ struct | (Var var, _) -> let blob_size_opt = ID.to_int s in not @@ ask.is_multiple var - && not @@ Cil.isVoidType t (* Size of value is known *) && Option.is_some blob_size_opt (* Size of blob is known *) - && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t) + && (( + not @@ Cil.isVoidType t (* Size of value is known *) + && BI.equal (Option.get blob_size_opt) (BI.of_int @@ Cil.alignOf_int t) + ) || blob_destructive) | _ -> false end in diff --git a/tests/regression/73-strings/08-cursed.c b/tests/regression/73-strings/08-cursed.c index 421f9f7b18..1507b92563 100644 --- a/tests/regression/73-strings/08-cursed.c +++ b/tests/regression/73-strings/08-cursed.c @@ -1,4 +1,4 @@ -// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval --enable ana.base.arrays.nullbytes +// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval --enable ana.base.arrays.nullbytes --set ana.malloc.unique_address_count 1 #include #include @@ -23,10 +23,9 @@ int main() { int len3 = strlen(s6); __goblint_check(len3 == 5); - // Why does this not know the string length after the copy? - // This goes into the array/array case, so it seems unrelated to blob problems. strcpy(s5, "badabingbadaboom"); - len2 = strlen(s5); // no must 0 bytes anywhere? + int len2 = strlen(s5); + __goblint_check(len2 == 16); return 0; }