Update malloced strings destructively where possible

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

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

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 <goblint.h>
 #include <string.h>
@@ -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;
 }