Tracking Benchmark Changes for Thesis

.github/workflows/locked.yml

@@ -18,7 +18,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
           # don't add any other because they won't be used

.github/workflows/unlocked.yml

@@ -16,7 +16,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - 5.0.x
           - ocaml-variants.4.14.0+options,ocaml-option-flambda
@@ -91,7 +91,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file, downgrade deps step
 
@@ -189,7 +189,7 @@ jobs:
       matrix:
         os:
           - ubuntu-latest
-          - macos-latest
+          - macos-13
         ocaml-compiler:
           - ocaml-variants.4.14.0+options,ocaml-option-flambda # matches opam lock file
 

conf/traces-rel.json

@@ -3,7 +3,8 @@
     "int": {
       "def_exc": true,
       "interval": false,
-      "enums": true
+      "enums": true,
+      "def_exc_widen_by_join": true
     },
     "malloc": {
       "wrappers": [
@@ -79,6 +80,9 @@
       "other": false,
       "loop-head": false,
       "after-lock": true
+    },
+    "yaml" : {
+      "entry-types": ["location_invariant"]
     }
   },
   "pre": {

conf/traces.json

@@ -3,7 +3,8 @@
     "int": {
       "def_exc": true,
       "interval": false,
-      "enums": true
+      "enums": true,
+      "def_exc_widen_by_join": true
     },
     "malloc": {
       "wrappers": [
@@ -24,6 +25,14 @@
         "ldv_xzalloc",
         "ldv_calloc"
       ]
+    },
+    "base" : {
+      "invariant": {
+        "enabled": false
+      },
+      "eval": {
+        "deep-query": false
+      }
     }
   },
   "sem": {
@@ -35,9 +44,18 @@
     },
     "builtin_unreachable": {
       "dead_code": true
+    },
+    "int": {
+      "signed_overflow": "assume_none"
     }
   },
   "exp": {
-    "priv-distr-init": false
+    "priv-distr-init": false,
+    "priv-prec-dump-proj" : true
+  },
+  "solvers" : {
+    "td3": {
+      "side_widen" : "sides-pp"
+    }
   }
 }

example_widening_effects.c

@@ -0,0 +1,30 @@
+#include <pthread.h>
+int occupied;
+
+pthread_mutex_t mtx;
+
+
+void* thread(void* arg) {
+  pthread_mutex_lock(&mtx);
+
+  if(occupied < 2) {
+    occupied++;
+  }
+
+  pthread_mutex_unlock(&mtx);
+ }
+
+int main() {
+  pthread_t worker;
+
+  pthread_create(&worker, 0, &thread, 0);
+
+  pthread_mutex_lock(&mtx);
+  occupied = 0;
+  pthread_mutex_unlock(&mtx);
+
+  return 0;
+}
+
+
+// rm out.txt && ./goblint --conf conf/traces.json --set ana.base.privatization protection 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.protection.prec --enable ana.int.interval && ./goblint --conf conf/traces.json --set ana.base.privatization write 2.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.write.prec --enable ana.int.interval &&  ./privPrecCompare level-ip.protection.prec level-ip.write.prec &> out.txt

reduce_difference.sh

@@ -0,0 +1,23 @@
+#!/bin/bash
+grep "void (\*argmatch_die)(void)  =    & __argmatch_die;" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+grep "static void __argmatch_die(void)" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+grep "usage(1)" reduce.c
+if [ $? -eq 1 ]; then
+    exit 17
+fi
+
+
+/home/michael/Documents/goblint-cil/analyzer/goblint-2  --conf /home/michael/Documents/goblint-cil/analyzer/conf/traces.json --set dbg.timeout 900 --set ana.base.privatization protection 1.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.protection.prec
+/home/michael/Documents/goblint-cil/analyzer/goblint-2  --conf /home/michael/Documents/goblint-cil/analyzer/conf/traces.json --set dbg.timeout 900 --set ana.base.privatization write 1.c --enable allglobs --enable dbg.timing.enabled --enable warn.debug -v --sets exp.priv-prec-dump level-ip.write.prec
+/home/michael/Documents/goblint-cil/analyzer/privPrecCompare level-ip.protection.prec level-ip.write.prec  2> details.txt 1> res.txt
+if [ $? -eq 0 ]; then
+    grep "protection more precise than write" res.txt >/dev/null 2>&1
+else
+    exit 5
+fi

src/analyses/apron/relationAnalysis.apron.ml

@@ -56,7 +56,8 @@ struct
       Priv.read_global ask getg st g x
     else (
       let rel = st.rel in
-      let g_var = RV.global g in
+      (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
+      let g_var = if g.vglob then RV.global g else RV.local g in
       let x_var = RV.local x in
       let rel' = RD.add_vars rel [g_var] in
       let rel' = RD.assign_var rel' x_var g_var in
@@ -245,25 +246,21 @@ struct
   (* Basic transfer functions. *)
   let assign ctx (lv:lval) e =
     let st = ctx.local in
-    if !AnalysisState.global_initialization && e = MyCFG.unknown_exp then
-      st (* ignore extern inits because there's no body before assign, so env is empty... *)
-    else (
-      let simplified_e = replace_deref_exps ctx.ask e in
-      if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv  d_exp e d_exp simplified_e;
-      let ask = Analyses.ask_of_ctx ctx in
-      let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
-          assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
-              if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
-              if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
-              let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
-              if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
-              r
-            )
-        )
-      in
-      if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
-      r
-    )
+    let simplified_e = replace_deref_exps ctx.ask e in
+    if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv  d_exp e d_exp simplified_e;
+    let ask = Analyses.ask_of_ctx ctx in
+    let r = assign_to_global_wrapper ask ctx.global ctx.sideg st lv (fun st v ->
+        assign_from_globals_wrapper ask ctx.global st simplified_e (fun apr' e' ->
+            if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
+            if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
+            let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
+            if M.tracing then M.traceu "relation" "-> %a" RD.pretty r;
+            r
+          )
+      )
+    in
+    if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
+    r
 
   let branch ctx e b =
     let st = ctx.local in
@@ -469,10 +466,9 @@ struct
       | None -> None
       | Some st ->
         let ad = ask.f (Queries.ReachableFrom e) in
-        if Queries.AD.is_top ad then
-          None
-        else
-          Some (Queries.AD.join ad st)
+        (* See https://github.com/goblint/analyzer/issues/1535 *)
+        let ad = Queries.AD.remove UnknownPtr ad in
+        Some (Queries.AD.join ad st)
     in
     List.fold_right reachable es (Some (Queries.AD.empty ()))
 
@@ -513,6 +509,35 @@ struct
       if RD.is_bot_env res then raise Deadcode;
       {st with rel = res}
 
+  let special_unknown_invalidate ctx f args =
+    (* No warning here, base already produces the appropriate warnings *)
+    let desc = LibraryFunctions.find f in
+    let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
+    let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
+    let deep_addrs =
+      if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
+        foldGlobals !Cilfacade.current_file (fun acc global ->
+            match global with
+            | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
+              mkAddrOf (Var vi, NoOffset) :: acc
+            (* TODO: what about GVarDecl? *)
+            | _ -> acc
+          ) deep_addrs
+      )
+      else
+        deep_addrs
+    in
+    let lvallist e =
+      match ctx.ask (Queries.MayPointTo e) with
+      | ad when Queries.AD.is_top ad -> []
+      | ad ->
+        Queries.AD.to_mval ad
+        |> List.map ValueDomain.Addr.Mval.to_cil
+    in
+    let st' = forget_reachable ctx ctx.local deep_addrs in
+    let shallow_lvals = List.concat_map lvallist shallow_addrs in
+    List.fold_left (invalidate_one (Analyses.ask_of_ctx ctx) ctx) st' shallow_lvals
+
   let special ctx r f args =
     let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
@@ -548,31 +573,7 @@ struct
          assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
        | None -> st)
     | _, _ ->
-      let lvallist e =
-        match ask.f (Queries.MayPointTo e) with
-        | ad when Queries.AD.is_top ad -> []
-        | ad ->
-          Queries.AD.to_mval ad
-          |> List.map ValueDomain.Addr.Mval.to_cil
-      in
-      let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
-      let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
-      let deep_addrs =
-        if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
-          foldGlobals !Cilfacade.current_file (fun acc global ->
-              match global with
-              | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                mkAddrOf (Var vi, NoOffset) :: acc
-              (* TODO: what about GVarDecl? *)
-              | _ -> acc
-            ) deep_addrs
-        )
-        else
-          deep_addrs
-      in
-      let st' = forget_reachable ctx st deep_addrs in
-      let shallow_lvals = List.concat_map lvallist shallow_addrs in
-      let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
+      let st' = special_unknown_invalidate ctx f args in
       (* invalidate lval if present *)
       match r with
       | Some lv -> invalidate_one ask ctx st' lv
@@ -602,6 +603,10 @@ struct
           | Some (Local v) ->
             if VH.mem v_ins_inv v then
               keep_global
+            else if ThreadEscape.has_escaped ask v then
+              (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *)
+              (* and is not a sound description of the C variable. *)
+              false
             else
               keep_local
           | _ -> false
@@ -662,35 +667,36 @@ struct
 
   let threadenter ctx ~multiple lval f args =
     let st = ctx.local in
+    (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
+       Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
+       sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
+       EnterMultithreaded events only execute after threadenter and threadspawn. *)
+    if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
+      ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
     match Cilfacade.find_varinfo_fundec f with
     | fd ->
-      (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread.
-         Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published...
-         sync `Thread doesn't help us here, it's not specific to entering multithreaded mode.
-         EnterMultithreaded events only execute after threadenter and threadspawn. *)
-      if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
-        ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
       let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in
       let new_rel = make_callee_rel ~thread:true ctx fd args in
       [{st' with rel = new_rel}]
     | exception Not_found ->
-      (* Unknown functions *)
-      (* TODO: do something like base? *)
-      failwith "relation.threadenter: unknown function"
+      [special_unknown_invalidate ctx f args]
 
   let threadspawn ctx ~multiple lval f args fctx =
     ctx.local
 
   let event ctx e octx =
+    let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
     match e with
-    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
-    | Events.Unlock addr when ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      if addr = UnknownPtr then
-        M.info ~category:Unsound "Unknown mutex unlocked, relation privatization unsound"; (* TODO: something more sound *)
+    | Events.Lock (addr, _) when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
+      CommonPriv.lift_lock ask (fun st m ->
+          Priv.lock ask ctx.global st m
+        ) st addr
+    | Events.Unlock addr when ThreadFlag.has_ever_been_multi ask -> (* TODO: is this condition sound? *)
       WideningTokens.with_local_side_tokens (fun () ->
-          Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr
+          CommonPriv.lift_unlock ask (fun st m ->
+              Priv.unlock ask ctx.global ctx.sideg st m
+            ) st addr
         )
     | Events.EnterMultiThreaded ->
       Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
@@ -769,7 +775,7 @@ struct
       PCU.RH.replace results ctx.node new_value;
     end;
     WideningTokens.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg ctx.local (reason :> [`Normal | `Join | `JoinCall | `Return | `Init | `Thread])
       )
 
   let init marshal =
@@ -778,7 +784,7 @@ struct
   let store_data file =
     let results = PCU.RH.map (fun _ v -> RD.marshal v) results in
     let name = RD.name () ^ "(domain: " ^ (RD.name ()) ^ ", privatization: " ^ (Priv.name ()) ^ (if GobConfig.get_bool "ana.apron.threshold_widening" then ", th" else "" ) ^ ")" in
-    let results: PCU.dump = {marshalled = results; name } in
+    let results: PCU.dump = {marshalled = results; name; disregard = None } in
     Serialize.marshal results file
 
   let finalize () =