Enhanced substring_extraction, added new regression test

src/analyses/apron/relationalStringAnalyses.apron.ml

@@ -15,7 +15,7 @@ struct
       let module Spec =
       struct
         include SpecFunctor (Priv) (RSD) (PCU)
-        let name () = "relational_substr"    
+        let name () = "substr"    
       end
       in
       (module Spec)

src/cdomains/apron/relationalStringDomains.apron.ml

@@ -15,7 +15,7 @@ sig
   val string_copy: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> int option -> t
   val string_concat: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> int option -> t
   val to_string_length: ('a, 'b, 'c, 'd) ctx -> t  -> varinfo -> ID.t
-  val substring_extraction: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> bool * bool
+  val substring_extraction: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> varinfo -> t * bool * bool
   val string_comparison: ('a, 'b, 'c, 'd) ctx -> t -> varinfo -> varinfo -> int option -> ID.t
 end
 
@@ -137,7 +137,9 @@ struct
     let t_with_new_dest = {r_set = S.add (dest', src') (S.add (src', dest') t_without_dest.r_set); env = t_without_dest.env} in
     let t_with_new_relations = {r_set = transitive_closure t_with_new_dest.r_set; env = t_with_new_dest.env} in
 
-    (* ask for size(dest) and strlen(src) *)
+    (* ask for size(dest) and strlen(src); 
+     * no check for string literals as query returns top for size;
+     * no check for null_ptr as query return top for them for both size and len *)
     let size_dest = vid_to_id ILong (ctx.ask (VarArraySize dest)) in
     let len_src = vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength src)) in
 
@@ -211,18 +213,29 @@ struct
       t.r_set (vid_to_id !Cil.kindOfSizeOf (ctx.ask (VarStringLength s)))
 
   (* returns is_maybe_null_ptr, is_surely_offset_0 *)
-  let substring_extraction ctx t haystack needle =
+  let substring_extraction ctx t lval haystack needle =
+    let lval' = varinfo_to_var lval in
     let haystack' = varinfo_to_var haystack in
     let needle' = varinfo_to_var needle in
-    (* if needle = haystack, strstr returns a pointer to haystack at offset 0 *)
+    (* if needle = haystack, strstr returns a pointer to haystack at offset 0 and lval = haystack = needle *)
     if S.mem (needle', haystack') t.r_set && S.mem (haystack', needle') t.r_set then
-      false, true
-      (* if needle <= haystack, strstr returns a pointer to haystack, offset unknown *)
+      let new_r_set =
+        S.add (lval', haystack') t.r_set
+        |> S.add (haystack', lval')
+        |> S.add (lval', needle')
+        |> S.add (needle', lval')
+        |> transitive_closure in
+      {r_set = new_r_set; env = t.env}, false, true
+      (* if needle <= haystack, strstr returns a pointer to haystack with unknown offset and needle <= lval <= haystack *)
     else if S.mem (needle', haystack') t.r_set then
-      false, false
+      let new_r_set =
+        S.add (lval', haystack') t.r_set
+        |> S.add (needle', lval')
+        |> transitive_closure in
+      {r_set = new_r_set; env = t.env}, false, false
       (* else strstr could return a pointer to haystack with unknown offset or a null_ptr *)
     else
-      true, false
+      t, true, false
 
   let string_comparison ctx t s1 s2 n =
     let s1' = varinfo_to_var s1 in

tests/regression/73-strings/05-substrings.c

@@ -0,0 +1,32 @@
+// PARAM: --disable ana.base.limit-string-addresses --enable ana.int.interval --enable ana.base.arrays.nullbytes --set ana.activated[+] substr
+
+#include <goblint.h>
+#include <string.h>
+#include <stdlib.h>
+
+int main() {
+    example1();
+
+    return 0;
+}
+
+void example1() {
+    char s1[] = "string";
+    char s2[100];
+    s2[42] = '\0';
+
+    if (rand() == 42) {
+        strcpy(s2, "C-");
+        strcat(s2, s1);
+    } else {
+        strcpy(s2, "sub");
+        strncat(s2, s1, 20);
+    }
+
+    char* s3 = strstr(s2, s1);
+    __goblint_check(s3 != NULL);
+
+    size_t len = strlen(s3);
+    __goblint_check(len >= 0);
+    __goblint_check(len <= 42);
+}