Remove support for old ghost_variable and ghost_update entry types

Author: sim642

src/analyses/mutexGhosts.ml

@@ -122,54 +122,6 @@ struct
     | YamlEntryGlobal (g, task) ->
       let g: V.t = Obj.obj g in
       begin match g with
-        | `Left g' when YamlWitness.entry_type_enabled YamlWitnessType.GhostVariable.entry_type && YamlWitness.entry_type_enabled YamlWitnessType.GhostUpdate.entry_type ->
-          let (locked, unlocked, multithread) = G.node (ctx.global g) in
-          let g = g' in
-          let entries =
-            (* TODO: do variable_entry-s only once *)
-            Locked.fold (fun l acc ->
-                match mustlock_of_addr l with
-                | Some l when ghost_var_available ctx (Locked l) ->
-                  let entry = WitnessGhost.variable_entry ~task (Locked l) in
-                  Queries.YS.add entry acc
-                | _ ->
-                  acc
-              ) (Locked.union locked unlocked) (Queries.YS.empty ())
-          in
-          let entries =
-            Locked.fold (fun l acc ->
-                match mustlock_of_addr l with
-                | Some l when ghost_var_available ctx (Locked l) ->
-                  let entry = WitnessGhost.update_entry ~task ~node:g (Locked l) GoblintCil.one in
-                  Queries.YS.add entry acc
-                | _ ->
-                  acc
-              ) locked entries
-          in
-          let entries =
-            Unlocked.fold (fun l acc ->
-                match mustlock_of_addr l with
-                | Some l when ghost_var_available ctx (Locked l) ->
-                  let entry = WitnessGhost.update_entry ~task ~node:g (Locked l) GoblintCil.zero in
-                  Queries.YS.add entry acc
-                | _ ->
-                  acc
-              ) unlocked entries
-          in
-          let entries =
-            if not (GobConfig.get_bool "exp.earlyglobs") && multithread then (
-              if ghost_var_available ctx Multithreaded then (
-                let entry = WitnessGhost.variable_entry ~task Multithreaded in
-                let entry' = WitnessGhost.update_entry ~task ~node:g Multithreaded GoblintCil.one in
-                Queries.YS.add entry (Queries.YS.add entry' entries)
-              )
-              else
-                entries
-            )
-            else
-              entries
-          in
-          entries
         | `Right true when YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type ->
           let nodes = G.update (ctx.global g) in
           let (variables, location_updates) = NodeSet.fold (fun node (variables, location_updates) ->

src/config/options.schema.json

@@ -2673,8 +2673,6 @@
                   "precondition_loop_invariant_certificate",
                   "invariant_set",
                   "violation_sequence",
-                  "ghost_variable",
-                  "ghost_update",
                   "ghost_instrumentation"
                 ]
               },

src/witness/witnessGhost.ml

@@ -1,7 +1,7 @@
 (** Ghost variables for YAML witnesses. *)
 
 let enabled () =
-  (YamlWitness.entry_type_enabled YamlWitnessType.GhostVariable.entry_type && YamlWitness.entry_type_enabled YamlWitnessType.GhostUpdate.entry_type) || YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type
+  YamlWitness.entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type
 
 module Var = WitnessGhostVar
 
@@ -11,20 +11,6 @@ module Map = RichVarinfo.BiVarinfoMap.Make (Var)
 
 include Map
 
-let variable_entry ~task x =
-  let variable = name_varinfo x in
-  let type_ = String.trim (CilType.Typ.show (typ x)) in (* CIL printer puts space at the end of some types *)
-  let initial = CilType.Exp.show (initial x) in
-  YamlWitness.Entry.ghost_variable ~task ~variable ~type_ ~initial
-
-let update_entry ~task ~node x e =
-  let loc = Node.location node in
-  let location_function = (Node.find_fundec node).svar.vname in
-  let location = YamlWitness.Entry.location ~location:loc ~location_function in
-  let variable = name_varinfo x in
-  let expression = CilType.Exp.show e in
-  YamlWitness.Entry.ghost_update ~task ~location ~variable ~expression
-
 let variable' x =
   let variable = name_varinfo x in
   let type_ = String.trim (CilType.Typ.show (typ x)) in (* CIL printer puts space at the end of some types *)

src/witness/yamlWitness.ml

@@ -149,25 +149,6 @@ struct
     metadata = metadata ();
   }
 
-  let ghost_variable ~task ~variable ~type_ ~(initial): Entry.t = {
-    entry_type = GhostVariable {
-        variable;
-        scope = "global";
-        type_;
-        initial;
-      };
-    metadata = metadata ~task ();
-  }
-
-  let ghost_update ~task ~location ~variable ~(expression): Entry.t = {
-    entry_type = GhostUpdate {
-        variable;
-        expression;
-        location;
-      };
-    metadata = metadata ~task ();
-  }
-
   let ghost_variable' ~variable ~type_ ~(initial): GhostInstrumentation.Variable.t = {
     name = variable;
     scope = "global";
@@ -410,9 +391,10 @@ struct
         entries
     in
 
-    (* Generate flow-insensitive entries (ghost variables and ghost updates) *)
+    (* Generate flow-insensitive entries (ghost instrumentation) *)
     let entries =
-      if (entry_type_enabled YamlWitnessType.GhostVariable.entry_type && entry_type_enabled YamlWitnessType.GhostUpdate.entry_type) || entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type then (
+      if entry_type_enabled YamlWitnessType.GhostInstrumentation.entry_type then (
+        (* TODO: only at most one ghost_instrumentation entry can ever be produced, so this fold and deduplication is overkill *)
         let module EntrySet = Queries.YS in
         fst @@ GHT.fold (fun g v accs ->
             match g with

src/witness/yamlWitnessType.ml

@@ -644,61 +644,6 @@ struct
     {content}
 end
 
-module GhostVariable =
-struct
-  type t = {
-    variable: string;
-    scope: string;
-    type_: string;
-    initial: string;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "ghost_variable"
-
-  let to_yaml' {variable; scope; type_; initial} =
-    [
-      ("variable", `String variable);
-      ("scope", `String scope);
-      ("type", `String type_);
-      ("initial", `String initial);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ variable = y |> find "variable" >>= to_string
-    and+ scope = y |> find "scope" >>= to_string
-    and+ type_ = y |> find "type" >>= to_string
-    and+ initial = y |> find "initial" >>= to_string in
-    {variable; scope; type_; initial}
-end
-
-module GhostUpdate =
-struct
-  type t = {
-    variable: string;
-    expression: string;
-    location: Location.t;
-  }
-  [@@deriving eq, ord, hash]
-
-  let entry_type = "ghost_update"
-
-  let to_yaml' {variable; expression; location} =
-    [
-      ("variable", `String variable);
-      ("expression", `String expression);
-      ("location", Location.to_yaml location);
-    ]
-
-  let of_yaml y =
-    let open GobYaml in
-    let+ variable = y |> find "variable" >>= to_string
-    and+ expression = y |> find "expression" >>= to_string
-    and+ location = y |> find "location" >>= Location.of_yaml in
-    {variable; expression; location}
-end
-
 module GhostInstrumentation =
 struct
 
@@ -831,8 +776,6 @@ struct
     | PreconditionLoopInvariantCertificate of PreconditionLoopInvariantCertificate.t
     | InvariantSet of InvariantSet.t
     | ViolationSequence of ViolationSequence.t
-    | GhostVariable of GhostVariable.t
-    | GhostUpdate of GhostUpdate.t
     | GhostInstrumentation of GhostInstrumentation.t
   [@@deriving eq, ord, hash]
 
@@ -845,8 +788,6 @@ struct
     | PreconditionLoopInvariantCertificate _ -> PreconditionLoopInvariantCertificate.entry_type
     | InvariantSet _ -> InvariantSet.entry_type
     | ViolationSequence _ -> ViolationSequence.entry_type
-    | GhostVariable _ -> GhostVariable.entry_type
-    | GhostUpdate _ -> GhostUpdate.entry_type
     | GhostInstrumentation _ -> GhostInstrumentation.entry_type
 
   let to_yaml' = function
@@ -858,8 +799,6 @@ struct
     | PreconditionLoopInvariantCertificate x -> PreconditionLoopInvariantCertificate.to_yaml' x
     | InvariantSet x -> InvariantSet.to_yaml' x
     | ViolationSequence x -> ViolationSequence.to_yaml' x
-    | GhostVariable x -> GhostVariable.to_yaml' x
-    | GhostUpdate x -> GhostUpdate.to_yaml' x
     | GhostInstrumentation x -> GhostInstrumentation.to_yaml' x
 
   let of_yaml y =
@@ -889,12 +828,6 @@ struct
     else if entry_type = ViolationSequence.entry_type then
       let+ x = y |> ViolationSequence.of_yaml in
       ViolationSequence x
-    else if entry_type = GhostVariable.entry_type then
-      let+ x = y |> GhostVariable.of_yaml in
-      GhostVariable x
-    else if entry_type = GhostUpdate.entry_type then
-      let+ x = y |> GhostUpdate.of_yaml in
-      GhostUpdate x
     else if entry_type = GhostInstrumentation.entry_type then
       let+ x = y |> GhostInstrumentation.of_yaml in
       GhostInstrumentation x

tests/util/yamlWitnessStripCommon.ml

@@ -74,10 +74,6 @@ struct
         InvariantSet {content = List.sort InvariantSet.Invariant.compare (List.map invariant_strip_file_hash x.content)} (* Sort, so order is deterministic regardless of Goblint. *)
       | ViolationSequence x ->
         ViolationSequence {content = List.map segment_strip_file_hash x.content}
-      | GhostVariable x ->
-        GhostVariable x (* no location to strip *)
-      | GhostUpdate x ->
-        GhostUpdate {x with location = location_strip_file_hash x.location}
       | GhostInstrumentation x ->
         GhostInstrumentation { (* Sort, so order is deterministic regardless of Goblint. *)
           ghost_variables = List.sort GhostInstrumentation.Variable.compare x.ghost_variables;