Interactive: improvements for chrony story

src/analyses/accessAnalysis.ml

@@ -207,7 +207,11 @@ struct
       let arg_acc act =
         match act, LF.get_threadsafe_inv_ac x with
         | _, Some fnc -> (fnc act arglist)
-        | `Read, None -> arglist
+        | `Read, None ->
+          if get_bool "sem.unknown_function.read.args" then
+            arglist
+          else
+            []
         | (`Write | `Free), None ->
           if get_bool "sem.unknown_function.invalidate.args" then
             arglist
@@ -220,6 +224,7 @@ struct
         | "memset" | "__builtin_memset" | "__builtin___memset_chk" -> false
         | "bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk" -> false
         | "__builtin_object_size" -> false
+        | "realloc" -> false
         | _ -> true
       in
       List.iter (access_one_top ctx `Read reach) (arg_acc `Read);

src/analyses/libraryFunctions.ml

@@ -521,6 +521,7 @@ let invalidate_actions = [
     "down_trylock", readsAll;
     "up", readsAll;
     "ZSTD_customFree", frees [1]; (* only used with extraspecials *)
+    "__goblint_assume_join", readsAll;
   ]
 
 (* used by get_invalidate_action to make sure

src/analyses/symbLocks.ml

@@ -59,8 +59,12 @@ struct
       | a when not (Queries.ES.is_bot a) -> Queries.ES.add e a
       | _ -> Queries.ES.singleton e
     in
+    if M.tracing then M.tracel "symb_locks" "get_all_locks exps %a = %a\n" d_plainexp e Queries.ES.pretty exps;
+    if M.tracing then M.tracel "symb_locks" "get_all_locks st = %a\n" D.pretty st;
     let add_locks x xs = PS.union (get_locks x st) xs in
-    Queries.ES.fold add_locks exps (PS.empty ())
+    let r = Queries.ES.fold add_locks exps (PS.empty ()) in
+    if M.tracing then M.tracel "symb_locks" "get_all_locks %a = %a\n" d_plainexp e PS.pretty r;
+    r
 
   let same_unknown_index (ask: Queries.ask) exp slocks =
     let uk_index_equal i1 i2 = ask.f (Queries.MustBeEqual (i1, i2)) in
@@ -148,6 +152,7 @@ struct
     *)
     let one_perelem (e,a,l) xs =
       (* ignore (printf "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l); *)
+      if M.tracing then M.tracel "symb_locks" "one_perelem (%a,%a,%a)\n" Exp.pretty e Exp.pretty a Exp.pretty l;
       match Exp.fold_offs (Exp.replace_base (dummyFunDec.svar,`NoOffset) e l) with
       | Some (v, o) ->
         (* ignore (printf "adding lock %s\n" l); *)

src/analyses/threadJoins.ml

@@ -45,6 +45,19 @@ struct
         | _ -> ctx.local (* if multiple possible thread ids are joined, none of them is must joined*)
         (* Possible improvement: Do the intersection first, things that are must joined in all possibly joined threads are must-joined *)
       )
+    | `Unknown "__goblint_assume_join" ->
+      let id = List.hd arglist in
+      let threads = ctx.ask (Queries.EvalThread id) in
+      if TIDs.is_top threads then
+        D.bot () (* consider everything joined, D is reversed so bot is All threads *)
+      else (
+        (* elements throws if the thread set is top *)
+        let threads = TIDs.elements threads in
+        List.fold_left (fun acc tid ->
+            let joined = ctx.global tid in
+            D.union (D.add tid acc) joined
+          ) ctx.local threads
+      )
     | _ -> ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =

src/analyses/varEq.ml

@@ -315,15 +315,18 @@ struct
            | _ -> failwith "Unmatched pattern."
     in
     let r =
-      if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
+      if Cil.isConstant b then false
+      else if Queries.LS.is_top bls || Queries.LS.mem (dummyFunDec.svar, `NoOffset) bls
       then ((*Messages.warn "No PT-set: switching to types ";*) type_may_change_apt a )
       else Queries.LS.exists (lval_may_change_pt a) bls
     in
     (*    if r
           then (Messages.warn ~msg:("Kill " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
           else (Messages.warn ~msg:("Keep " ^sprint 80 (Exp.pretty () a)^" because of "^sprint 80 (Exp.pretty () b)) (); r)
           Messages.warn ~msg:(sprint 80 (Exp.pretty () b) ^" changed lvalues: "^sprint 80 (Queries.LS.pretty () bls)) ();
-    *)    r
+    *)
+    if M.tracing then M.tracel "var_eq" "may_change %a %a = %B\n" CilType.Exp.pretty b CilType.Exp.pretty a r;
+    r
 
   (* Remove elements, that would change if the given lval would change.*)
   let remove_exp ask (e:exp) (st:D.t) : D.t =
@@ -376,6 +379,12 @@ struct
           let st =
     *)  let lvt = unrollType @@ Cilfacade.typeOfLval lv in
     (*     Messages.warn ~msg:(sprint 80 (d_type () lvt)) (); *)
+    if M.tracing then (
+      M.tracel "var_eq" "add_eq is_global_var %a = %B\n" d_plainlval lv (is_global_var ask (Lval lv) = Some false);
+      M.tracel "var_eq" "add_eq interesting %a = %B\n" d_plainexp rv (Exp.interesting rv);
+      M.tracel "var_eq" "add_eq is_global_var %a = %B\n" d_plainexp rv (is_global_var ask rv = Some false);
+      M.tracel "var_eq" "add_eq type %a = %B\n" d_plainlval lv ((isArithmeticType lvt && match lvt with | TFloat _ -> false | _ -> true ) || isPointerType lvt);
+    );
     if is_global_var ask (Lval lv) = Some false
     && Exp.interesting rv
     && is_global_var ask rv = Some false
@@ -519,7 +528,10 @@ struct
       D.B.fold add es (Queries.ES.empty ())
 
   let rec eq_set_clos e s =
-    match e with
+    if M.tracing then M.traceli "var_eq" "eq_set_clos %a\n" d_plainexp e;
+    let r = match e with
+    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+      eq_set_clos e1 s (* TODO: what about e2? add to some Index offset to all? *)
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -541,6 +553,9 @@ struct
       Queries.ES.map (fun e -> CastE (t,e)) (eq_set_clos e s)
     | Question _ -> failwith "Logical operations should be compiled away by CIL."
     | _ -> failwith "Unmatched pattern."
+    in
+    if M.tracing then M.traceu "var_eq" "eq_set_clos %a = %a\n" d_plainexp e Queries.ES.pretty r;
+    r
 
 
   let query ctx (type a) (x: a Queries.t): a Queries.result =
@@ -550,6 +565,7 @@ struct
     | Queries.EqualSet e ->
       let r = eq_set_clos e ctx.local in
       (*          Messages.warn ~msg:("equset of "^(sprint 80 (d_exp () e))^" is "^(Queries.ES.short 80 r)) ();  *)
+      if M.tracing then M.tracel "var_eq" "equalset %a = %a\n" d_plainexp e Queries.ES.pretty r;
       r
     | _ -> Queries.Result.top x
 

src/cdomains/exp.ml

@@ -1,6 +1,8 @@
 open Pretty
 open Cil
 
+module M = Messages
+
 module Exp =
 struct
   include CilType.Exp
@@ -10,6 +12,8 @@ struct
   (* TODO: what does interesting mean? *)
   let rec interesting x =
     match x with
+    | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+    interesting e1 (* TODO: what about e2? *)
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -290,19 +294,22 @@ struct
     in
     let rec helper exp =
       match exp with
+      | BinOp ((PlusPI | IndexPI), e1, e2, _) ->
+        helper e1 (* TODO: what about e2? add to some Index offset to all? *)
       | SizeOf _
       | SizeOfE _
       | SizeOfStr _
       | AlignOf _
       | AlignOfE _
       | UnOp _
       | BinOp _
-      | StartOf _
       | Const _ -> raise NotSimpleEnough
       | Lval (Var v, os) -> EVar v :: conv_o os
       | Lval (Mem e, os) -> helper e @ [EDeref] @ conv_o os
       | AddrOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
       | AddrOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
+      | StartOf (Var v, os) -> EVar v :: conv_o os @ [EAddr]
+      | StartOf (Mem e, os) -> helper e @ [EDeref] @ conv_o os @ [EAddr]
       | CastE (_,e) -> helper e
       | Question _ -> failwith "Logical operations should be compiled away by CIL."
       | _ -> failwith "Unmatched pattern."
@@ -331,6 +338,7 @@ struct
     List.rev el, fs
 
   let from_exps a l : t option =
+    if M.tracing then M.tracel "symb_locks" "from_exps %a (%s) %a (%s)\n" d_plainexp a (ees_to_str (toEl a)) d_plainexp l (ees_to_str (toEl l));
     let a, l = toEl a, toEl l in
     (* ignore (printf "from_exps:\n %s\n %s\n" (ees_to_str a) (ees_to_str l)); *)
     (*let rec fold_left2 f a xs ys =

src/cdomains/mHP.ml

@@ -54,7 +54,7 @@ let exists_definitely_not_started_in_joined (current,created) other_joined =
 (** Must the thread with thread id other be already joined  *)
 let must_be_joined other joined =
   if ConcDomain.ThreadSet.is_top joined then
-    false
+    true (* top means all threads are joined, so [other] must be as well *)
   else
     List.mem other (ConcDomain.ThreadSet.elements joined)
 

src/util/options.schema.json

@@ -1136,6 +1136,20 @@
                 }
               },
               "additionalProperties": false
+            },
+            "read": {
+              "title": "sem.unknown_function.read",
+              "type": "object",
+              "properties": {
+                "args": {
+                  "title": "sem.unknown_function.read.args",
+                  "description":
+                    "Unknown function call reads arguments passed to it",
+                  "type": "boolean",
+                  "default": true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false

tests/regression/02-base/78-realloc-free.c

@@ -21,15 +21,15 @@ void test1() {
 
 void* test2_f(void *arg) {
   int *p = arg;
-  *p = 1; // RACE!
+  *p = 1; // NORACE
   return NULL;
 }
 
 void test2() {
   int *p = malloc(sizeof(int));
   pthread_t id;
   pthread_create(&id, NULL, test2_f, p);
-  realloc(p, sizeof(int)); // RACE!
+  realloc(p, sizeof(int)); // NORACE
 }
 
 void* test3_f(void *arg) {

tests/regression/06-symbeq/37-funloop_index.c

@@ -0,0 +1,36 @@
+// PARAM: --disable ana.mutex.disjoint_types --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// copy of 06/02 with additional index accesses
+#include<pthread.h>
+#include<stdio.h>
+
+struct cache_entry {
+  int refs;
+  pthread_mutex_t refs_mutex;
+} cache[10];
+
+void cache_entry_addref(struct cache_entry *entry) {
+  pthread_mutex_lock(&entry->refs_mutex);
+  entry->refs++; // NORACE
+  (*entry).refs++; // NORACE
+  entry[0].refs++; // NORACE
+  pthread_mutex_unlock(&entry->refs_mutex);
+}
+
+void *t_fun(void *arg) {
+  int i;
+  for(i=0; i<10; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return NULL;
+}
+
+int main () {
+  for (int i = 0; i < 10; i++)
+    pthread_mutex_init(&cache[i].refs_mutex, NULL);
+
+  int i;
+  pthread_t t1;
+  pthread_create(&t1, NULL, t_fun, NULL);
+  for(i=0; i<10; i++)
+    cache_entry_addref(&cache[i]); // NORACE
+  return 0;
+}