Merge pull request #729 from goblint/smtprc

Interactive: improvements for smtprc story

Author: sim642

src/analyses/base.ml

@@ -2134,6 +2134,11 @@ struct
         invalidate ~ctx (Analyses.ask_of_ctx ctx) ctx.global st [Cil.mkAddrOrStartOf lv]
       | None -> st
     in
+    let addr_type_of_exp exp = 
+      let lval = mkMem ~addr:(Cil.stripCasts exp) ~off:NoOffset in
+      let addr = eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval in
+      (addr, AD.get_type addr)
+    in
     let forks = forkfun ctx lv f args in
     if M.tracing then if not (List.is_empty forks) then M.tracel "spawn" "Base.special %s: spawning functions %a\n" f.vname (d_list "," d_varinfo) (List.map BatTuple.Tuple3.second forks);
     List.iter (BatTuple.Tuple3.uncurry ctx.spawn) forks;
@@ -2146,10 +2151,7 @@ struct
         | ("memset" | "__builtin_memset"), [dest; ch; count] ->
           (* TODO: check count *)
           let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in
-          let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in
-          let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in
-          (* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
-          let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
+          let dest_a, dest_typ = addr_type_of_exp dest in
           let value =
             match eval_ch with
             | `Int i when ID.to_int i = Some Z.zero ->
@@ -2166,17 +2168,14 @@ struct
         | "__explicit_bzero_chk", [dest; count; _ (* dest_size *)]
         | ("bzero" | "__builtin_bzero" | "explicit_bzero"), [dest; count] ->
           (* TODO: check count *)
-          let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in
-          let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in
-          (* let dest_typ = Cilfacade.typeOfLval dest_lval in *)
-          let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *)
+          let dest_a, dest_typ = addr_type_of_exp dest in
           let value = VD.zero_init_value dest_typ in
           set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
         | _, _ -> failwith "strange bzero arguments"
       end
-    | `Unknown "F59" (* strcpy *)
-    | `Unknown "F60" (* strncpy *)
-    | `Unknown "F63" (* memcpy *)
+    | `Unknown ("F59" | "strcpy")
+    | `Unknown ("F60" | "strncpy")
+    | `Unknown ("F63" | "memcpy")
       ->
       begin match args with
         | [dst; src]
@@ -2188,15 +2187,9 @@ struct
           (* | _ -> ignore @@ Pretty.printf "strcpy: dst %a may point to anything!\n" d_exp dst; *)
           (*     ctx.local *)
           (* end *)
-          let rec get_lval exp = match stripCasts exp with
-            | Lval x | AddrOf x | StartOf x -> x
-            | BinOp (PlusPI, e, i, _)
-            | BinOp (MinusPI, e, i, _) -> get_lval e
-            | x ->
-              ignore @@ Pretty.printf "strcpy: dst is %a!\n" d_plainexp dst;
-              failwith "strcpy: expecting first argument to be a pointer!"
-          in
-          assign ctx (get_lval dst) src
+          let dest_a, dest_typ = addr_type_of_exp dst in
+          let value = VD.top_value dest_typ in
+          set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value
         | _ -> failwith "strcpy arguments are strange/complicated."
       end
     | `Unknown "F1" ->

src/analyses/libraryFunctions.ml

@@ -271,6 +271,7 @@ let invalidate_actions = [
     "strlen", readsAll;(*safe*)
     "strncmp", readsAll;(*safe*)
     "strncpy", writes [1];(*keep [1]*)
+    "strncat", writes [1];(*keep [1]*)
     "strstr", readsAll;(*safe*)
     "strdup", readsAll;(*safe*)
     "toupper", readsAll;(*safe*)
@@ -314,6 +315,9 @@ let invalidate_actions = [
     "pthread_attr_setdetachstate", writesAll;(*unsafe*)
     "pthread_attr_setstacksize", writesAll;(*unsafe*)
     "pthread_attr_setscope", writesAll;(*unsafe*)
+    "pthread_attr_getdetachstate", readsAll;(*safe*)
+    "pthread_attr_getstacksize", readsAll;(*safe*)
+    "pthread_attr_getscope", readsAll;(*safe*)
     "pthread_cond_init", readsAll; (*safe*)
     "pthread_cond_wait", readsAll; (*safe*)
     "pthread_cond_signal", readsAll;(*safe*)
@@ -341,7 +345,8 @@ let invalidate_actions = [
     "strcpy", writes [1];(*keep [1]*)
     "__builtin___strcpy", writes [1];(*keep [1]*)
     "__builtin___strcpy_chk", writes [1];(*keep [1]*)
-    "strcat", writes [2];(*keep [2]*)
+    "strcat", writes [1];(*keep [1]*)
+    "strtok", readsAll;(*safe*)
     "getpgrp", readsAll;(*safe*)
     "umount2", readsAll;(*safe*)
     "memchr", readsAll;(*safe*)
@@ -376,6 +381,7 @@ let invalidate_actions = [
     "fputs", readsAll;(*safe*)
     "fputc", readsAll;(*safe*)
     "fseek", writes[1];
+    "rewind", writesAll;
     "fileno", readsAll;
     "ferror", readsAll;
     "ftell", readsAll;

tests/regression/03-practical/27-charptr_null.c

@@ -0,0 +1,33 @@
+#include <string.h>
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+struct options
+{
+    char *ip_range;
+};
+
+struct options o;
+
+int get_ip_range(int *iprange)
+{
+    char *r = iprange;
+
+    while (*r++)
+    {
+        *r = '\0';
+        assert(1);
+    }
+
+    return (0);
+}
+
+int main()
+{
+    char *optarg = "was from unistd.h";
+    o.ip_range = malloc((strlen(optarg) + 1) * sizeof(char));
+    strncpy(o.ip_range, optarg, strlen(optarg));
+    o.ip_range[strlen(optarg)] = '\0';
+    get_ip_range(o.ip_range);
+}