Relational Mutex-Meet-Privatization making use of Thread IDs

.github/workflows/locked.yml

@@ -43,6 +43,9 @@ jobs:
       - name: Test apron regression # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
         run: ruby scripts/update_suite.rb group apron -s
 
+      - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        run: ruby scripts/update_suite.rb group apron-mukherjee -s
+
       - name: Build domaintest
         run: ./make.sh domaintest
 

.github/workflows/unlocked.yml

@@ -59,6 +59,10 @@ jobs:
         if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron -s
 
+      - name: Test apron regression (Mukherjee et. al  SAS '17 paper') # skipped by default but CI has apron, so explicitly test group (which ignores skipping -- it's now a feature!)
+        if: ${{ matrix.apron }}
+        run: ruby scripts/update_suite.rb group apron-mukherjee -s
+
       - name: Build domaintest
         run: ./make.sh domaintest
 

conf/traces-rel.json

@@ -0,0 +1,57 @@
+{
+  "ana": {
+    "int": {
+      "def_exc": true,
+      "interval": false,
+      "enums": true
+    },
+    "exp": {
+
+    }
+  },
+  "sem": {
+    "unknown_function": {
+      "invalidate": {
+        "globals": false
+      },
+      "spawn": true
+    },
+    "builtin_unreachable": {
+      "dead_code": true
+    }
+  },
+  "exp": {
+    "privatization": "mutex-meet",
+    "priv-distr-init": false,
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+
+        "ldv_malloc",
+
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc"
+      ]
+    },
+    "solver" : {
+      "td3": {
+        "side_widen" : "sides-pp"
+      }
+    }
+  },
+  "dbg" : {
+    "print_tids" : true,
+    "print_wpoints" : true,
+    "print_protection": true
+  }
+}

src/analyses/apron/apronAnalysis.apron.ml

@@ -10,7 +10,6 @@ module SpecFunctor (AD: ApronDomain.S2) (Priv: ApronPriv.S) : Analyses.MCPSpec =
 struct
   include Analyses.DefaultSpec
 
-
   let name () = "apron"
 
   module Priv = Priv(AD)
@@ -216,6 +215,7 @@ struct
 
   let return ctx e f =
     let st = ctx.local in
+    let ask = Analyses.ask_of_ctx ctx in
     let new_apr =
       if AD.type_tracked (Cilfacade.fundec_return_type f) then (
         let apr' = AD.add_vars st.apr [V.return] in
@@ -235,8 +235,15 @@ struct
       |> List.filter AD.varinfo_tracked
       |> List.map V.local
     in
+
     AD.remove_vars_with new_apr local_vars;
-    {st with apr = new_apr}
+    let st' = {st with apr = new_apr} in
+    begin match ThreadId.get_current ask with
+      | `Lifted tid when ThreadReturn.is_current ask ->
+        Priv.thread_return ask ctx.global ctx.sideg tid st'
+      | _ ->
+        st'
+    end
 
   let combine ctx r fe f args fc fun_st =
     let st = ctx.local in
@@ -288,13 +295,28 @@ struct
       unify_st
 
   let special ctx r f args =
+    let ask = Analyses.ask_of_ctx ctx in
+    let invalidate_one st lv =
+      assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
+          let apr' = AD.forget_vars st.apr [V.local v] in
+          assert_type_bounds apr' v (* re-establish type bounds after forget *)
+        )
+    in
     let st = ctx.local in
     match LibraryFunctions.classify f.vname args with
     (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
     | `Assert expression -> st
     | `Unknown "__goblint_check" -> st
     | `Unknown "__goblint_commit" -> st
     | `Unknown "__goblint_assert" -> st
+    | `ThreadJoin (id,retvar) ->
+      (* nothing to invalidate as only arguments that have their AddrOf taken may be invalidated *)
+      (
+        let st' = Priv.thread_join ask ctx.global id st in
+        match r with
+        | Some lv -> invalidate_one st' lv
+        | None -> st'
+      )
     | _ ->
       let ask = Analyses.ask_of_ctx ctx in
       let invalidate_one st lv =