Merge pull request #830 from goblint/yaml-witness-global

Flow-insensitive YAML witness invariants

Author: sim642

src/analyses/base.ml

@@ -1106,109 +1106,30 @@ struct
 
   let query_invariant ctx context =
     let cpa = ctx.local.BaseDomain.cpa in
-    let scope = Node.find_fundec ctx.node in
 
-    (* VS is used to detect and break cycles in deref_invariant calls *)
-    let module VS = Set.Make (Basetype.Variables) in
-
-    let rec ad_invariant ~vs ~offset c x =
-      let c_exp = Cil.(Lval (BatOption.get c.Invariant.lval)) in
-      let i_opt = AD.fold (fun addr acc_opt ->
-          BatOption.bind acc_opt (fun acc ->
-              match addr with
-              | Addr.UnknownPtr ->
-                None
-              | Addr.Addr (vi, offs) when Addr.Offs.is_definite offs ->
-                let rec offs_to_offset = function
-                  | `NoOffset -> NoOffset
-                  | `Field (f, offs) -> Field (f, offs_to_offset offs)
-                  | `Index (i, offs) ->
-                    (* Addr.Offs.is_definite implies Idx.to_int returns Some *)
-                    let i_definite = BatOption.get (ValueDomain.IndexDomain.to_int i) in
-                    let i_exp = Cil.(kinteger64 ILongLong (IntOps.BigIntOps.to_int64 i_definite)) in
-                    Index (i_exp, offs_to_offset offs)
-                in
-                let offset = offs_to_offset offs in
-
-                let i =
-                  if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp && not (var_is_tmp vi) && var_is_in_scope scope vi && not (var_is_heap vi)) then
-                    let addr_exp = AddrOf (Var vi, offset) in (* AddrOf or Lval? *)
-                    Invariant.of_exp Cil.(BinOp (Eq, c_exp, addr_exp, intType))
-                  else
-                    Invariant.none
-                in
-                let i_deref = deref_invariant ~vs c vi offset (Mem c_exp, NoOffset) in
-
-                Some (Invariant.(acc || (i && i_deref)))
-              | Addr.NullPtr ->
-                let i =
-                  let addr_exp = integer 0 in
-                  if InvariantCil.(not (exp_contains_tmp c_exp) && exp_is_in_scope scope c_exp) then
-                    Invariant.of_exp Cil.(BinOp (Eq, c_exp, addr_exp, intType))
-                  else
-                    Invariant.none
-                in
-                Some (Invariant.(acc || i))
-              (* TODO: handle Addr.StrPtr? *)
-              | _ ->
-                None
-            )
-        ) x (Some (Invariant.bot ()))
-      in
-      match i_opt with
-      | Some i -> i
-      | None -> Invariant.none
-
-    and blob_invariant ~vs ~offset c (v, _, _) =
-      vd_invariant ~vs ~offset c v
-
-    and vd_invariant ~vs ~offset c = function
-      | `Int n ->
-        let e = Lval (BatOption.get c.Invariant.lval) in
-        if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
-          ID.invariant e n
-        else
-          Invariant.none
-      | `Float n ->
-        let e = Lval (BatOption.get c.Invariant.lval) in
-        if InvariantCil.(not (exp_contains_tmp e) && exp_is_in_scope scope e) then
-          FD.invariant e n
-        else
-          Invariant.none
-      | `Address n -> ad_invariant ~vs ~offset c n
-      | `Blob n -> blob_invariant ~vs ~offset c n
-      | `Struct n -> ValueDomain.Structs.invariant ~value_invariant:(vd_invariant ~vs) ~offset c n
-      | `Union n -> ValueDomain.Unions.invariant ~value_invariant:(vd_invariant ~vs) ~offset c n
-      | _ -> Invariant.none (* TODO *)
-
-    and deref_invariant ~vs c vi offset lval =
-      let v = CPA.find vi cpa in
-      key_invariant_lval ~vs c vi offset lval v
-
-    and key_invariant_lval ~vs c k offset lval v =
-      if not (VS.mem k vs) then
-        let vs' = VS.add k vs in
-        let key_context: Invariant.context = {c with lval=Some lval} in
-        vd_invariant ~vs:vs' ~offset key_context v
-      else
-        Invariant.none
+    let module Arg =
+    struct
+      let context = context
+      let scope = Node.find_fundec ctx.node
+      let find v = CPA.find v cpa
+    end
     in
+    let module I = ValueDomain.ValueInvariant (Arg) in
 
     let cpa_invariant =
-      let key_invariant k v = key_invariant_lval ~vs:VS.empty context k NoOffset (var k) v in
       match context.lval with
       | None ->
         CPA.fold (fun k v a ->
             let i =
               if not (InvariantCil.var_is_heap k) then
-                key_invariant k v
+                I.key_invariant k v
               else
                 Invariant.none
             in
             Invariant.(a && i)
           ) cpa Invariant.none
       | Some (Var k, _) when not (InvariantCil.var_is_heap k) ->
-        (try key_invariant k (CPA.find k cpa) with Not_found -> Invariant.none)
+        (try I.key_invariant k (CPA.find k cpa) with Not_found -> Invariant.none)
       | _ -> Invariant.none
     in
 
@@ -1220,6 +1141,20 @@ struct
     else
       Invariant.none
 
+  let query_invariant_global ctx g =
+    if GobConfig.get_bool "ana.base.invariant.enabled" && get_bool "exp.earlyglobs" then (
+      (* Currently these global invariants are only sound with earlyglobs enabled for both single- and multi-threaded programs.
+         Otherwise, the values of globals in single-threaded mode are not accounted for. *)
+      (* TODO: account for single-threaded values without earlyglobs. *)
+      match g with
+      | `Left g' -> (* priv *)
+        Priv.invariant_global (priv_getg ctx.global) g'
+      | `Right _ -> (* thread return *)
+        Invariant.none
+    )
+    else
+      Invariant.none
+
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
     | Q.EvalFunvar e ->
@@ -1331,6 +1266,9 @@ struct
       let vf' x = vf (Obj.repr (V.priv x)) in
       Priv.iter_sys_vars (priv_getg ctx.global) vq vf'
     | Q.Invariant context -> query_invariant ctx context
+    | Q.InvariantGlobal g ->
+      let g: V.t = Obj.obj g in
+      query_invariant_global ctx g
     | _ -> Q.Result.top q
 
   let update_variable variable typ value cpa =

src/analyses/basePriv.ml

@@ -40,6 +40,8 @@ sig
   val thread_join: ?force:bool -> Q.ask -> (V.t -> G.t) -> Cil.exp -> BaseComponents (D).t -> BaseComponents (D).t
   val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> BaseComponents (D).t -> BaseComponents (D).t
 
+  val invariant_global: (V.t -> G.t) -> V.t -> Invariant.t
+
   val init: unit -> unit
   val finalize: unit -> unit
 end
@@ -124,6 +126,9 @@ struct
 
   let thread_join ?(force=false) ask get e st = st
   let thread_return ask get set tid st = st
+
+  let invariant_global getg g =
+    ValueDomain.invariant_global getg g
 end
 
 module PerMutexPrivBase =
@@ -156,6 +161,11 @@ struct
       | None, Some v -> Some v
       | None, None -> None
 
+  let read_unprotected_global getg x =
+    let get_mutex_global_x = get_mutex_global_x_with_mutex_inits getg x in
+    (* None is VD.top () *)
+    get_mutex_global_x |? VD.bot ()
+
   let escape ask getg sideg (st: BaseComponents (D).t) escaped =
     let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in
     sideg V.mutex_inits escaped_cpa;
@@ -193,6 +203,13 @@ struct
 
   let thread_join ?(force=false) ask get e st = st
   let thread_return ask get set tid st = st
+
+  let invariant_global getg g =
+    match g with
+    | `Left _ -> (* mutex *)
+      Invariant.none
+    | `Right g' -> (* global *)
+      ValueDomain.invariant_global (read_unprotected_global getg) g'
 end
 
 module PerMutexOplusPriv: S =
@@ -201,8 +218,7 @@ struct
 
   let read_global ask getg (st: BaseComponents (D).t) x =
     if is_unprotected ask x then
-      let get_mutex_global_x = get_mutex_global_x_with_mutex_inits getg x in
-      get_mutex_global_x |? VD.bot ()
+      read_unprotected_global getg x
     else
       CPA.find x st.cpa
   (* let read_global ask getg cpa x =
@@ -271,9 +287,8 @@ struct
 
   let read_global ask getg (st: BaseComponents (D).t) x =
     if is_unprotected ask x then (
-      let get_mutex_global_x = get_mutex_global_x_with_mutex_inits getg x in
       (* If the global is unprotected, all appropriate information should come via the appropriate globals, local value may be too small due to stale values surviving widening *)
-      get_mutex_global_x |? VD.bot ()
+      read_unprotected_global getg x
     )
     else
       CPA.find x st.cpa
@@ -550,6 +565,21 @@ struct
     let _,lmust,l = st.priv in
     {st with cpa = new_cpa; priv = (W.bot (),lmust,l)}
 
+  let read_unprotected_global getg x =
+    let get_mutex_global_x = merge_all @@ G.mutex @@ getg (V.global x) in
+    let get_mutex_global_x' = CPA.find x get_mutex_global_x in
+    let get_mutex_inits = merge_all @@ G.mutex @@ getg V.mutex_inits in
+    let get_mutex_inits' = CPA.find x get_mutex_inits in
+    VD.join get_mutex_global_x' get_mutex_inits'
+
+  let invariant_global getg g =
+    match g with
+    | `Left (`Left _) -> (* mutex *)
+      Invariant.none
+    | `Left (`Right g') -> (* global *)
+      ValueDomain.invariant_global (read_unprotected_global getg) g'
+    | `Right _ -> (* thread *)
+      Invariant.none
 end
 
 
@@ -690,6 +720,13 @@ struct
       vf (V.unprotected g);
       vf (V.protected g);
     | _ -> ()
+
+  let invariant_global getg g =
+    match g with
+    | `Left g' -> (* unprotected *)
+      ValueDomain.invariant_global (fun g -> getg (V.unprotected g)) g'
+    | `Right g -> (* protected *)
+      Invariant.none
 end
 
 module AbstractLockCenteredGBase (WeakRange: Lattice.S) (SyncRange: Lattice.S) =
@@ -725,11 +762,42 @@ struct
   end
 end
 
-module LockCenteredGBase =
+module type WeakRangeS =
+sig
+  include Lattice.S
+  val fold_weak: (VD.t -> 'a -> 'a) -> t -> 'a -> 'a
+  (** Fold over all values represented by weak range. *)
+end
+
+module AbstractLockCenteredBase (WeakRange: WeakRangeS) (SyncRange: Lattice.S) =
 struct
+  include AbstractLockCenteredGBase (WeakRange) (SyncRange)
+  include MutexGlobals
+
+  let invariant_global getg g =
+    match g with
+    | `Left _ -> (* mutex *)
+      Invariant.none
+    | `Right g' -> (* global *)
+      ValueDomain.invariant_global (fun x ->
+          GWeak.fold (fun s' tm acc ->
+              WeakRange.fold_weak VD.join tm acc
+            ) (G.weak (getg (V.global x))) (VD.bot ())
+        ) g'
+end
+
+module LockCenteredBase =
+struct
+  module VD =
+  struct
+    include VD
+
+    let fold_weak f v a = f v a
+  end
+
   (* weak: G -> (2^M -> D) *)
   (* sync: M -> (2^M -> (G -> D)) *)
-  include AbstractLockCenteredGBase (VD) (CPA)
+  include AbstractLockCenteredBase (VD) (CPA)
 end
 
 module MinePrivBase =
@@ -760,11 +828,16 @@ struct
   open Locksets
 
   module Thread = ThreadIdDomain.Thread
-  module ThreadMap = MapDomain.MapBot (Thread) (VD)
+  module ThreadMap =
+  struct
+    include MapDomain.MapBot (Thread) (VD)
+
+    let fold_weak f m a = fold (fun _ v a -> f v a) m a
+  end
 
   (* weak: G -> (2^M -> (T -> D)) *)
   (* sync: M -> (2^M -> (G -> D)) *)
-  include AbstractLockCenteredGBase (ThreadMap) (CPA)
+  include AbstractLockCenteredBase (ThreadMap) (CPA)
 
   let global_init_thread = RichVarinfo.single ~name:"global_init"
   let current_thread (ask: Q.ask): Thread.t =
@@ -831,7 +904,7 @@ end
 module MineNoThreadPriv: S =
 struct
   include MineNaivePrivBase
-  include LockCenteredGBase
+  include LockCenteredBase
   open Locksets
 
   let read_global ask getg (st: BaseComponents (D).t) x =
@@ -893,7 +966,7 @@ end
 module MineWPriv (Param: MineWPrivParam): S =
 struct
   include MinePrivBase
-  include LockCenteredGBase
+  include LockCenteredBase
   open Locksets
 
   module W =
@@ -996,7 +1069,7 @@ end
 module LockCenteredPriv: S =
 struct
   include MinePrivBase
-  include LockCenteredGBase
+  include LockCenteredBase
   open Locksets
 
   open LockCenteredD
@@ -1124,23 +1197,28 @@ struct
   let threadenter = startstate_threadenter startstate
 end
 
-module WriteCenteredGBase =
+module WriteCenteredBase =
 struct
   open Locksets
 
-  module GWeakW = MapDomain.MapBot (Lockset) (VD)
+  module GWeakW =
+  struct
+    include MapDomain.MapBot (Lockset) (VD)
+
+    let fold_weak f m a = fold (fun _ v a -> f v a) m a
+  end
   module GSyncW = MapDomain.MapBot (Lockset) (CPA)
 
   (* weak: G -> (S:2^M -> (W:2^M -> D)) *)
   (* sync: M -> (S:2^M -> (W:2^M -> (G -> D))) *)
-  include AbstractLockCenteredGBase (GWeakW) (GSyncW)
+  include AbstractLockCenteredBase (GWeakW) (GSyncW)
 end
 
 (** Write-Centered Reading. *)
 module WriteCenteredPriv: S =
 struct
   include MinePrivBase
-  include WriteCenteredGBase
+  include WriteCenteredBase
   open Locksets
 
   open WriteCenteredD
@@ -1280,7 +1358,7 @@ end
 module WriteAndLockCenteredPriv: S =
 struct
   include MinePrivBase
-  include WriteCenteredGBase
+  include WriteCenteredBase
   open Locksets
 
   open LockCenteredD
@@ -1462,6 +1540,7 @@ struct
   let enter_multithreaded ask getg sideg st = time "enter_multithreaded" (Priv.enter_multithreaded ask getg sideg) st
   let threadenter ask st = time "threadenter" (Priv.threadenter ask) st
   let iter_sys_vars getg vq vf = time "iter_sys_vars" (Priv.iter_sys_vars getg vq) vf
+  let invariant_global getg v = time "invariant_global" (Priv.invariant_global getg) v
 
   let thread_join ?(force=false) ask get e st = time "thread_join" (Priv.thread_join ~force ask get e) st
   let thread_return ask get set tid st = time "thread_return" (Priv.thread_return ask get set tid) st