Merge branch 'master' into yaml-witness-default

Author: sim642

.gitattributes

@@ -0,0 +1,13 @@
+# GitHub repository language overrides
+# https://github.com/github-linguist/linguist/blob/main/docs/overrides.md
+
+# currently only dune-project is classified: https://github.com/github-linguist/linguist/pull/7126
+dune linguist-language=dune
+dune.inc linguist-language=dune
+
+# avoid misclassification as Standard ML
+*.ml linguist-language=ocaml
+*.mli linguist-language=ocaml
+
+# cram tests are classified as Raku/Terra/Turing, cram isn't separate language so consider them also dune
+*.t linguist-language=dune

goblint.opam

@@ -97,8 +97,8 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
+  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

goblint.opam.locked

@@ -64,7 +64,7 @@ depends: [
   "fileutils" {= "0.6.4"}
   "fmt" {= "0.9.0"}
   "fpath" {= "0.7.3"}
-  "goblint-cil" {= "2.0.5"}
+  "goblint-cil" {= "2.0.6"}
   "hex" {= "1.5.0"}
   "integers" {= "0.7.0"}
   "json-data-encoding" {= "1.0.1"}
@@ -139,8 +139,8 @@ post-messages: [
 ]
 pin-depends: [
   [
-    "goblint-cil.2.0.5"
-    "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f"
+    "goblint-cil.2.0.6"
+    "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a"
   ]
   [
     "camlidl.1.12"

goblint.opam.template

@@ -2,8 +2,8 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
-  # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
+  # published goblint-cil 2.0.6 is currently up-to-date, but pinned for reproducibility
+  [ "goblint-cil.2.0.6" "git+https://github.com/goblint/cil.git#8385ab315bc7461f6801af57673c64731bfa036a" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

gobview

@@ -740,7 +740,12 @@ struct
         in
         ({ f } : Queries.ask) in
       let rel = RD.assert_inv dummyask rel e false (no_overflow ask e_orig) in (* assume *)
-      let rel = RD.keep_vars rel (List.map RV.local vars) in (* restrict *)
+      let rel =
+        if GobConfig.get_bool "ana.apron.strengthening" then
+          RD.keep_vars rel (List.map RV.local vars) (* restrict *)
+        else
+          rel (* naive unassume: will be homogeneous join below *)
+      in
 
       (* TODO: parallel write_global? *)
       let st =

src/analyses/apron/relationAnalysis.apron.ml

@@ -866,6 +866,47 @@ sig
   include AtomicParam
 end
 
+module P =
+struct
+  include MustVars
+  let name () = "P"
+end
+
+module Sigma' =
+struct
+  include CPA
+  let name () = "Protected Changes"
+end
+
+module type ProtectionDom =
+sig
+  include Lattice.S
+  val add: bool -> varinfo -> VD.t -> t -> t
+  val remove: varinfo -> t -> t
+  val precise_side: varinfo -> VD.t -> t -> VD.t option
+  val empty: unit -> t
+  val getP: t -> P.t
+end
+
+module ProtectionCPASide: ProtectionDom =
+struct
+  include P
+
+  let add _ x _ t = P.add x t
+  let precise_side x v t = Some v
+  let getP t = t
+end
+
+module ProtectionChangesOnlySide: ProtectionDom =
+struct
+  include Lattice.Prod (P) (Sigma')
+  let add invariant x v t = P.add x @@ fst t, if not invariant then Sigma'.add x v @@ snd t else snd t
+  let remove x t = P.remove x @@ fst t, Sigma'.remove x @@ snd t
+  let precise_side x v t = Sigma'.find_opt x @@ snd t
+  let empty () = P.empty (), Sigma'.empty ()
+  let getP t = fst t
+end
+
 (** Protection-Based Reading. *)
 module ProtectionBasedV = struct
   module VUnprot =
@@ -887,30 +928,24 @@ module ProtectionBasedV = struct
 end
 
 (** Protection-Based Reading. *)
-module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
+module ProtectionBasedPriv (D: ProtectionDom) (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
 struct
   include NoFinalize
   include ConfCheck.RequireMutexActivatedInit
   open Protection
 
-  module P =
-  struct
-    include MustVars
-    let name () = "P"
-  end
-
   (* W is implicitly represented by CPA domain *)
-  module D = P
+  module D = D
 
   module Wrapper = Wrapper (VD)
   module G = Wrapper.G
   module V = ProtectionBasedV.V
 
-  let startstate () = P.empty ()
+  let startstate () = D.empty ()
 
   let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     let getg = Wrapper.getg ask getg in
-    if P.mem x st.priv then
+    if P.mem x @@ D.getP st.priv then
       CPA.find x st.cpa
     else if Param.handle_atomic && ask.f MustBeAtomic then
       VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
@@ -921,6 +956,7 @@ struct
 
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     let sideg = Wrapper.sideg ask sideg in
+    let unprotected = is_unprotected ask x in
     if not invariant then (
       if not (Param.handle_atomic && ask.f MustBeAtomic) then
         sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
@@ -929,11 +965,11 @@ struct
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
     if Param.handle_atomic && ask.f MustBeAtomic then
-      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
-    else if is_unprotected ask x then
+      {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv} (* Keep write local as if it were protected by the atomic section. *)
+    else if unprotected then
       st
     else
-      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
+      {st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv}
 
   let lock ask getg st m = st
 
@@ -943,16 +979,22 @@ struct
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
-          (* Extra precision in implementation to pass tests:
-             If global is read-protected by multiple locks,
-             then inner unlock shouldn't yet publish. *)
-          if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
-            sideg (V.protected x) v;
-          if atomic then
-            sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
-
+          (* Only apply sides for values that were actually written to globals!
+             This excludes invariants inferred through guards. *)
+          begin match D.precise_side x v st.priv with
+            | Some v -> begin
+                (* Extra precision in implementation to pass tests:
+                   If global is read-protected by multiple locks,
+                   then inner unlock shouldn't yet publish. *)
+                if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
+                  sideg (V.protected x) v;
+                if atomic then
+                  sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
+              end
+            | None -> ()
+          end;
           if is_unprotected_without ask x m then (* is_in_V' *)
-            {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+            {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
           else
             st
         )
@@ -968,7 +1010,7 @@ struct
           if is_global ask x && is_unprotected ask x then (
             sideg (V.unprotected x) v;
             sideg (V.protected x) v; (* must be like enter_multithreaded *)
-            {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+            {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
           )
           else
             st
@@ -1007,7 +1049,7 @@ struct
         if is_global ask x then (
           sideg (V.unprotected x) v;
           sideg (V.protected x) v;
-          {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
+          {st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
         )
         else
           st
@@ -2116,19 +2158,21 @@ end
 
 let priv_module: (module S) Lazy.t =
   lazy (
+    let changes_only = get_bool "ana.base.priv.protection.changes-only" in
+    let module ProtDom: ProtectionDom = (val if changes_only then (module ProtectionChangesOnlySide : ProtectionDom) else (module ProtectionCPASide)) in
     let module Priv: S =
       (val match get_string "ana.base.privatization" with
         | "none" -> (module NonePriv: S)
         | "vojdani" -> (module VojdaniPriv: S)
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
-        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
-        | "protection-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
-        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
-        | "protection-read-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
-        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
+        | "protection" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
+        | "protection-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
+        | "protection-read" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
+        | "protection-read-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))