Merge pull request #833 from goblint/yaml-witness-global-local

Privatized location invariants in YAML witnesses

Author: sim642

src/analyses/apron/apronAnalysis.apron.ml

@@ -91,6 +91,28 @@ struct
     in
     (apr', e', v_ins)
 
+  let read_globals_to_locals_inv (ask: Queries.ask) getg st vs =
+    let v_ins_inv = VH.create (List.length vs) in
+    List.iter (fun v ->
+        let v_in = Goblintutil.create_var @@ makeVarinfo false (v.vname ^ "#in") v.vtype in (* temporary local g#in for global g *)
+        VH.replace v_ins_inv v_in v;
+      ) vs;
+    let apr = AD.add_vars st.apr (List.map V.local (VH.keys v_ins_inv |> List.of_enum)) in (* add temporary g#in-s *)
+    let apr' = VH.fold (fun v_in v apr ->
+        read_global ask getg {st with apr = apr} v v_in (* g#in = g; *)
+      ) v_ins_inv apr
+    in
+    let visitor_inv = object
+      inherit nopCilVisitor
+      method! vvrbl (v: varinfo) =
+        match VH.find_option v_ins_inv v with
+        | Some v' -> ChangeTo v'
+        | None -> SkipChildren
+    end
+    in
+    let e_inv e = visitCilExpr visitor_inv e in
+    (apr', e_inv, v_ins_inv)
+
   let read_from_globals_wrapper ask getg st e f =
     let (apr', e', _) = read_globals_to_locals ask getg st e in
     f apr' e' (* no need to remove g#in-s *)
@@ -227,7 +249,7 @@ struct
     (* Also, a local *)
     let vname = Var.to_string var in
     let locals = fundec.sformals @ fundec.slocals in
-    match List.find_opt (fun v -> V.local_name v = vname) locals with
+    match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *)
     | None -> true
     | Some v -> any_local_reachable
 
@@ -257,8 +279,8 @@ struct
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     AD.remove_filter_with new_apr (fun var ->
         match V.find_metadata var with
-        | Some Local when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
-        | Some Arg when not (List.mem_cmp Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
+        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *)
+        | Some (Arg _) when not (List.mem_cmp Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
     if M.tracing then M.tracel "combine" "apron enter newd: %a\n" AD.pretty new_apr;
@@ -340,8 +362,8 @@ struct
     AD.remove_vars_with new_fun_apr arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_apr adds them back with proper constraints *)
     let new_apr = AD.keep_filter st.apr (fun var ->
         match V.find_metadata var with
-        | Some Local when not (pass_to_callee fundec any_local_reachable var) -> true (* keep caller locals, provided they were not passed to the function *)
-        | Some Arg -> true (* keep caller args *)
+        | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* keep caller locals, provided they were not passed to the function *)
+        | Some (Arg _) -> true (* keep caller args *)
         | _ -> false (* remove everything else (globals, global privs, reachable things from the caller) *)
       )
     in
@@ -392,9 +414,8 @@ struct
       match reachables ask es with
       | None ->
         (* top reachable, so try to invalidate everything *)
-        let fd = Node.find_fundec ctx.node in
         AD.vars st.apr
-        |> List.filter_map (V.to_cil_varinfo fd)
+        |> List.filter_map V.to_cil_varinfo
         |> List.map Cil.var
       | Some rs ->
         Queries.LS.elements rs
@@ -480,25 +501,50 @@ struct
   let query_invariant ctx context =
     let keep_local = GobConfig.get_bool "ana.apron.invariant.local" in
     let keep_global = GobConfig.get_bool "ana.apron.invariant.global" in
-
-    let apr = ctx.local.apr in
-    (* filter variables *)
-    let var_filter v = match V.find_metadata v with
-      | Some (Global _) -> keep_global
-      | Some Local -> keep_local
-      | _ -> false
-    in
-    let apr = AD.keep_filter apr var_filter in
-
     let one_var = GobConfig.get_bool "ana.apron.invariant.one-var" in
+
+    let ask = Analyses.ask_of_ctx ctx in
     let scope = Node.find_fundec ctx.node in
 
+    let (apr, e_inv) =
+      if ThreadFlag.is_multi ask then (
+        let priv_vars =
+          if keep_global then
+            Priv.invariant_vars ask ctx.global ctx.local
+          else
+            [] (* avoid pointless queries *)
+        in
+        let (apr, e_inv, v_ins_inv) = read_globals_to_locals_inv ask ctx.global ctx.local priv_vars in
+        (* filter variables *)
+        let var_filter v = match V.find_metadata v with
+          | Some (Local v) ->
+            if VH.mem v_ins_inv v then
+              keep_global
+            else
+              keep_local
+          | _ -> false
+        in
+        let apr = AD.keep_filter apr var_filter in
+        (apr, e_inv)
+      )
+      else (
+        (* filter variables *)
+        let var_filter v = match V.find_metadata v with
+          | Some (Global _) -> keep_global
+          | Some (Local _) -> keep_local
+          | _ -> false
+        in
+        let apr = AD.keep_filter ctx.local.apr var_filter in
+        (apr, Fun.id)
+      )
+    in
     AD.invariant ~scope apr
     |> List.enum
     |> Enum.filter_map (fun (lincons1: Lincons1.t) ->
         (* filter one-vars *)
         if one_var || Apron.Linexpr0.get_size lincons1.lincons0.linexpr0 >= 2 then
-          CilOfApron.cil_exp_of_lincons1 scope lincons1
+          CilOfApron.cil_exp_of_lincons1 lincons1
+          |> Option.map e_inv
           |> Option.filter (fun exp -> not (InvariantCil.exp_contains_tmp exp) && InvariantCil.exp_is_in_scope scope exp)
         else
           None
@@ -583,7 +629,7 @@ struct
       (* filter variables *)
       let var_filter v = match V.find_metadata v with
         | Some (Global _) -> keep_global
-        | Some Local -> keep_local
+        | Some (Local _) -> keep_local
         | _ -> false
       in
       let st = keep_filter ctx.local.apr var_filter in

src/analyses/apron/apronPriv.apron.ml

@@ -41,6 +41,9 @@ module type S =
     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. *)
 
+    val invariant_vars: Q.ask -> (V.t -> G.t) -> apron_components_t -> varinfo list
+    (** Returns global variables which are privatized. *)
+
     val init: unit -> unit
     val finalize: unit -> unit
   end
@@ -80,12 +83,7 @@ struct
     let apr = st.apr in
     let esc_vars = List.filter (fun var -> match AV.find_metadata var with
         | Some (Global _) -> false
-        | Some Local ->
-          (let fundec = Node.find_fundec node in
-           let r = AV.to_cil_varinfo fundec var in
-           match r with
-           | Some r -> EscapeDomain.EscapedVars.mem r escaped
-           | _ -> false)
+        | Some (Local r) -> EscapeDomain.EscapedVars.mem r escaped
         | _ -> false
       ) (AD.vars apr)
     in
@@ -127,6 +125,7 @@ struct
     {apr = AD.bot (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = ()
+  let invariant_vars ask getg st = []
 
   let init () = ()
   let finalize () = ()
@@ -404,6 +403,7 @@ struct
     {apr = getg (); priv = startstate ()}
 
   let iter_sys_vars getg vq vf = () (* TODO: or report singleton global for any Global query? *)
+  let invariant_vars ask getg st = protected_vars ask (* TODO: is this right? *)
 
   let finalize () = ()
 end
@@ -428,11 +428,25 @@ struct
     AD.keep_filter oct protected
 end
 
+module PerMutexMeetPrivBase (AD: ApronDomain.S3) =
+struct
+  let invariant_vars ask getg (st: (AD.t, _) ApronDomain.aproncomponents_t) =
+    (* Mutex-meet local states contain precisely the protected global variables,
+       so we can do fewer queries than {!protected_vars}. *)
+    AD.vars st.apr
+    |> List.filter_map (fun var ->
+        match ApronDomain.V.find_metadata var with
+        | Some (Global g) -> Some g
+        | _ -> None
+      )
+end
+
 (** Per-mutex meet. *)
 module PerMutexMeetPriv : S = functor (AD: ApronDomain.S3) ->
 struct
   open CommonPerMutex(AD)
   include MutexGlobals
+  include PerMutexMeetPrivBase (AD)
 
   module D = Lattice.Unit
   module G = AD
@@ -832,6 +846,7 @@ module PerMutexMeetPrivTID (Cluster: ClusterArg): S  = functor (AD: ApronDomain.
 struct
   open CommonPerMutex(AD)
   include MutexGlobals
+  include PerMutexMeetPrivBase (AD)
 
   module NC = Cluster(AD)
   module Cluster = NC

src/analyses/base.ml

@@ -1106,34 +1106,51 @@ struct
 
   let query_invariant ctx context =
     let cpa = ctx.local.BaseDomain.cpa in
+    let ask = Analyses.ask_of_ctx ctx in
 
     let module Arg =
     struct
       let context = context
       let scope = Node.find_fundec ctx.node
-      let find v = CPA.find v cpa
+      let find v = get_var ask ctx.global ctx.local v
     end
     in
     let module I = ValueDomain.ValueInvariant (Arg) in
 
-    let cpa_invariant =
-      match context.lval with
-      | None ->
-        CPA.fold (fun k v a ->
-            let i =
-              if not (InvariantCil.var_is_heap k) then
-                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 I.key_invariant k (CPA.find k cpa) with Not_found -> Invariant.none)
-      | _ -> Invariant.none
+    let var_invariant v =
+      if not (InvariantCil.var_is_heap v) then
+        I.key_invariant v (Arg.find v)
+      else
+        Invariant.none
     in
 
-    cpa_invariant
+    match context.lval with
+    | None ->
+      if !GU.earlyglobs || ThreadFlag.is_multi ask then (
+        let cpa_invariant =
+          CPA.fold (fun k v a ->
+              if not (is_global ask k) then
+                Invariant.(a && var_invariant k)
+              else
+                a
+            ) cpa Invariant.none
+        in
+        let priv_vars = Priv.invariant_vars ask (priv_getg ctx.global) ctx.local in
+        let priv_invariant =
+          List.fold_left (fun acc v ->
+              Invariant.(var_invariant v && acc)
+            ) Invariant.none priv_vars
+        in
+        Invariant.(cpa_invariant && priv_invariant)
+      )
+      else (
+        CPA.fold (fun k v a ->
+            Invariant.(a && var_invariant k)
+          ) cpa Invariant.none
+      )
+    | Some (Var k, _) ->
+      (try var_invariant k with Not_found -> Invariant.none)
+    | _ -> Invariant.none
 
   let query_invariant ctx context =
     if GobConfig.get_bool "ana.base.invariant.enabled" then