Skip to content

Commit

Permalink
Remove support for old ghost_variable and ghost_update entry types
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Nov 21, 2024
1 parent 554bd7f commit 2c25848
Show file tree
Hide file tree
Showing 6 changed files with 4 additions and 157 deletions.
48 changes: 0 additions & 48 deletions src/analyses/mutexGhosts.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) ->
Expand Down
2 changes: 0 additions & 2 deletions src/config/options.schema.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2673,8 +2673,6 @@
"precondition_loop_invariant_certificate",
"invariant_set",
"violation_sequence",
"ghost_variable",
"ghost_update",
"ghost_instrumentation"
]
},
Expand Down
16 changes: 1 addition & 15 deletions src/witness/witnessGhost.ml
View file
Original file line number Diff line number Diff line change
@@ -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

Expand All @@ -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 *)
Expand Down
24 changes: 3 additions & 21 deletions src/witness/yamlWitness.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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";
Expand Down Expand Up @@ -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
Expand Down
67 changes: 0 additions & 67 deletions src/witness/yamlWitnessType.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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]

Expand All @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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
Expand Down
4 changes: 0 additions & 4 deletions tests/util/yamlWitnessStripCommon.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 2c25848

Please sign in to comment.