Validation of Witnesses with Ghosts

.github/workflows/unlocked.yml

@@ -238,6 +238,10 @@ jobs:
         # if: ${{ matrix.apron }}
         run: ruby scripts/update_suite.rb group apron-mukherjee -s
 
+      - name: Test concurency witnessesses # 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 ghost-witnesses -s
+
       - name: Test marshal regression
         run: ruby scripts/update_suite.rb -m -s
 

.gitignore

@@ -18,6 +18,7 @@ tests/bench.txt
 _build
 *.native
 *.byte
+.codex
 doc
 doclist.odocl
 autom4te.cache
@@ -106,3 +107,4 @@ site/
 *.coverage
 # bisect-ppx-report
 _coverage/*
+tests/regression/*/result/*

conf/svcomp-ghost-validate.json

@@ -0,0 +1,122 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true,
+      "evaluate_math_functions": true
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "abortUnless",
+      "mutexGhosts",
+      "pthreadMutexType"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      },
+      "invariant": {
+        "local": false,
+        "global": true
+      },
+      "privatization" : "mutex-meet"
+    },
+    "relation": {
+      "invariant": {
+        "local": false,
+        "global": true,
+        "one-var": false
+      }
+    },
+    "apron": {
+      "invariant": {
+        "diff-box": true
+      }
+    },
+    "var_eq": {
+      "invariant": {
+        "enabled": false
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "reduceAnalyses",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "noOverflows",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    },
+    "malloc": {
+      "fail": false,
+      "zero": "pointer"
+    }
+  },
+  "pre": {
+    "enabled": false
+  }
+}

lib/sv-comp/stub/src/sv-comp.c

@@ -53,3 +53,5 @@ __VERIFIER_nondet2(void*, pointer)
 // atomics are now special in Goblint
 // void __VERIFIER_atomic_begin() { }
 // void __VERIFIER_atomic_end() { }
+// void __VERIFIER_atomic_instrument_begin() { }
+// void __VERIFIER_atomic_instrument_end() { }

src/analyses/accessAnalysis.ml

@@ -29,7 +29,7 @@ struct
   let init _ =
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
-    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
+    emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated || List.mem (PhaseGhost.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)
 
   let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
     if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;

src/analyses/apron/relationAnalysis.apron.ml

@@ -33,6 +33,8 @@ struct
     let of_elt {priv; _} = of_elt priv
   end
 
+  module AuxiliaryPhaseInfo = Priv.AuxiliaryPhaseInfo
+
   module RV = RD.V
 
   module PCU = PCU(RD)
@@ -659,6 +661,9 @@ struct
     | _ -> Result.top q
 
 
+  let aux_phase_info man = ((Priv.aux_phase_info man.local):AuxiliaryPhaseInfo.t)
+  let consume_aux_phase_info = Priv.consume_aux_phase_info
+
   (* Thread transfer functions. *)
 
   let threadenter man ~multiple lval f args =
@@ -757,6 +762,8 @@ struct
       st
     | Events.Longjmped {lval} ->
       Option.map_default (invalidate_one ask man st) st lval
+    | Events.PhaseChange {old_phase; new_phase} ->
+      Priv.phase_change ask old_phase new_phase man.global man.sideg st
     | _ ->
       st
 
@@ -778,7 +785,7 @@ struct
       PCU.RH.replace results man.node new_value;
     end;
     WideningTokenLifter.with_local_side_tokens (fun () ->
-        Priv.sync (Analyses.ask_of_man man) man.global man.sideg man.local (reason :> [`Normal | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
+        Priv.sync (Analyses.ask_of_man man) man.global man.sideg man.local (reason :> [`Normal | `NormalInCallTF | `Join | `JoinCall of CilType.Fundec.t | `Return | `Init | `Thread])
       )
 
   let init marshal =