Merge pull request #724 from goblint/chrony

Interactive: improvements for chrony story

Author: sim642

docs/user-guide/annotating.md

@@ -25,3 +25,11 @@ The following string arguments are supported:
 3. `base.non-ptr`/`base.no-non-ptr` to override the `ana.base.context.non-ptr` option.
 4. `apron.context`/`apron.no-context` to override the `ana.apron.context` option.
 5. `widen`/`no-widen` to override the `ana.context.widen` option.
+
+
+## Functions
+Goblint-specific functions can be called in the code, where they assist the analyzer but have no runtime effect.
+
+* `__goblint_assume_join(id)` is like `pthread_join(id)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
+  Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
+  _Misuse of this annotation can cause unsoundness._

scripts/update_suite.rb

@@ -159,6 +159,7 @@ def collect_warnings
                     when /Assertion .* is unknown/   then "unknown"
                     when /^\[Warning\]/              then "warn"
                     when /^\[Error\]/                then "warn"
+                    when /^\[Info\]/                 then "warn"
                     when /\[Debug\]/                 then next # debug "warnings" shouldn't count as other warnings (against NOWARN)
                     when /^  on line \d+ $/          then next # dead line warnings shouldn't count (used for unreachability with NOWARN)
                     when /^  on lines \d+..\d+ $/    then next # dead line warnings shouldn't count (used for unreachability with NOWARN)

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/apron/apronAnalysis.apron.ml

@@ -323,6 +323,9 @@ struct
         | Some lv -> invalidate_one st' lv
         | None -> st'
       )
+    | `Unknown "__goblint_assume_join" ->
+      let id = List.hd args in
+      Priv.thread_join ~force:true ask ctx.global id st
     | _ ->
       let ask = Analyses.ask_of_ctx ctx in
       let invalidate_one st lv =

src/analyses/apron/apronPriv.apron.ml

@@ -37,7 +37,7 @@ module type S =
     val enter_multithreaded: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> apron_components_t -> apron_components_t
     val threadenter: Q.ask -> (V.t -> G.t) -> apron_components_t -> apron_components_t
 
-    val thread_join: Q.ask -> (V.t -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
+    val thread_join: ?force:bool -> Q.ask -> (V.t -> G.t) -> Cil.exp -> apron_components_t -> apron_components_t
     val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> apron_components_t -> apron_components_t
     val iter_sys_vars: (V.t -> G.t) -> VarQuery.t -> V.t VarQuery.f -> unit (** [Queries.IterSysVars] for apron. *)
 
@@ -62,7 +62,7 @@ struct
   let lock ask getg st m = st
   let unlock ask getg sideg st m = st
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg st reason = st
@@ -270,7 +270,7 @@ struct
     {apr = apr_local'; priv = (p', w')}
 
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg (st: apron_components_t) reason =
@@ -461,7 +461,7 @@ struct
     let apr_local = remove_globals_unprotected_after_unlock ask m apr in
     {st with apr = apr_local}
 
-  let thread_join ask getg exp st = st
+  let thread_join ?(force=false) ask getg exp st = st
   let thread_return ask getg sideg tid st = st
 
   let sync ask getg sideg (st: apron_components_t) reason =
@@ -983,22 +983,40 @@ struct
       let l' = L.add lm apr_side l in
       {apr = apr_local; priv = (w',LMust.add lm lmust,l')}
 
-  let thread_join (ask:Q.ask) getg exp (st: apron_components_t) =
+  let thread_join ?(force=false) (ask:Q.ask) getg exp (st: apron_components_t) =
     let w,lmust,l = st.priv in
     let tids = ask.f (Q.EvalThread exp) in
-    if ConcDomain.ThreadSet.is_top tids then
-      st (* TODO: why needed? *)
+    if force then (
+      if ConcDomain.ThreadSet.is_top tids then (
+        M.info ~category:Unsound "Unknown thread ID assume-joined, Apron privatization unsound"; (* TODO: something more sound *)
+        st (* cannot find all thread IDs to join them all *)
+      )
+      else (
+        (* fold throws if the thread set is top *)
+        let tids' = ConcDomain.ThreadSet.diff tids (ask.f Q.MustJoinedThreads) in (* avoid unnecessary imprecision by force joining already must-joined threads, e.g. 46-apron2/04-other-assume-inprec *)
+        let (lmust', l') = ConcDomain.ThreadSet.fold (fun tid (lmust, l) ->
+            let lmust',l' = G.thread (getg (V.thread tid)) in
+            (LMust.union lmust' lmust, L.join l l')
+          ) tids' (lmust, l)
+        in
+        {st with priv = (w, lmust', l')}
+      )
+    )
     else (
-      (* elements throws if the thread set is top *)
-      let tids = ConcDomain.ThreadSet.elements tids in
-      match tids with
-      | [tid] ->
-        let lmust',l' = G.thread (getg (V.thread tid)) in
-        {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
-      | _ ->
-        (* To match the paper more closely, one would have to join in the non-definite case too *)
-        (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
-        st
+      if ConcDomain.ThreadSet.is_top tids then
+        st (* TODO: why needed? *)
+      else (
+        (* elements throws if the thread set is top *)
+        let tids = ConcDomain.ThreadSet.elements tids in
+        match tids with
+        | [tid] ->
+          let lmust',l' = G.thread (getg (V.thread tid)) in
+          {st with priv = (w, LMust.union lmust' lmust, L.join l l')}
+        | _ ->
+          (* To match the paper more closely, one would have to join in the non-definite case too *)
+          (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *)
+          st
+      )
     )
 
   let thread_return ask getg sideg tid (st: apron_components_t) =

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,8 +45,35 @@ 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 (
+        M.info ~category:Unsound "Unknown thread ID assume-joined, assuming ALL threads must-joined.";
+        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 threadspawn ctx lval f args fctx =
+    if D.is_bot ctx.local then ( (* bot is All threads *)
+      M.info ~category:Imprecise "Thread created while ALL threads must-joined, continuing with no threads joined.";
+      D.top () (* top is no threads *)
+    )
+    else
+      match ThreadId.get_current (Analyses.ask_of_ctx fctx) with
+      | `Lifted tid ->
+        D.remove tid ctx.local
+      | _ ->
+        ctx.local
+
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
     | Queries.MustJoinedThreads -> (ctx.local:ConcDomain.MustThreadSet.t) (* type annotation needed to avoid "would escape the scope of its equation" *)

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,18 @@ 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
+    | AddrOf (Mem (BinOp (IndexPI, a, i, _)), os) ->
+      (* convert IndexPI to Index offset *)
+      (* TODO: this applies eq_set_clos under the offset, unlike cases below; should generalize? *)
+      Queries.ES.fold (fun e acc -> (* filter_map *)
+        match e with
+        | CastE (_, StartOf a') -> (* eq_set adds casts *)
+          let e' = AddrOf (Cil.addOffsetLval (Index (i, os)) a') in (* TODO: re-add cast? *)
+          Queries.ES.add e' acc
+        | _ -> acc
+      ) (eq_set_clos a s) (Queries.ES.empty ())
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -541,6 +561,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 +573,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
+    | AddrOf (Mem (BinOp (IndexPI, a, _i, _)), _os) ->
+      interesting a
     | SizeOf _
     | SizeOfE _
     | SizeOfStr _
@@ -290,19 +294,21 @@ struct
     in
     let rec helper exp =
       match exp with
+      (* TODO: handle IndexPI like var_eq eq_set_clos? *)
       | 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 +337,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 =