Skip to content

WIP: Generalize phase ghost #2052

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
michael-schwarz wants to merge 1 commit into
base: ghosts
Choose a base branch
from
Draft

WIP: Generalize phase ghost #2052

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
60 changes: 19 additions & 41 deletions src/analyses/phaseGhost.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
(** Analysis for checking whether ghost globals are only accessed by one unique thread ([phaseGhost]). *)
(** Analysis for checking whether ghost globals are only accessed by one unique thread
and monotonically increased to known bounds ([phaseGhost]). *)

open Analyses
open GoblintCil
Expand All @@ -12,10 +13,10 @@ struct
let name () = "ghost-constant"
end

module IncByOne =
module MonotoneBounded =
struct
include BoolDomain.MustBool
let name () = "increment-by-one"
let name () = "monotone-bounded"
end

module Spec =
Expand All @@ -33,11 +34,11 @@ struct
module V = VarinfoV
module G =
struct
include Lattice.Prod (TIDs) (IncByOne)
include Lattice.Prod (TIDs) (MonotoneBounded)
let tids = fst
let inc_by_one = snd
let create_tids tids = (tids, IncByOne.bot ())
let create_inc_by_one inc_by_one = (TIDs.bot (), inc_by_one)
let monotone_bounded = snd
let create_tids tids = (tids, MonotoneBounded.bot ())
let create_monotone_bounded monotone_bounded = (TIDs.bot (), monotone_bounded)
end

let initial_ghost_values () =
Expand Down Expand Up @@ -66,28 +67,6 @@ struct
| `Lifted tid when TID.is_unique tid -> TIDs.singleton tid
| _ -> TIDs.top ()

let increment_constant lval rval =
let is_same_lval e =
match Cil.stripCasts e with
| Lval lval' -> CilType.Lval.equal lval lval'
| _ -> false
in
let is_one_constant e =
match Cil.getInteger (Cil.constFold true e) with
| Some k -> Z.equal k Z.one
| None -> false
in
match Cil.stripCasts rval with
| BinOp (PlusA, e1, e2, _) ->
if is_same_lval e1 then
is_one_constant e2
else if is_same_lval e2 then
is_one_constant e1
else
false
| _ ->
false

(* This local constant folding intentionally disregards writes from other threads.
It is only for the phaseGhost checker itself. *)
(* This information must **not** be used to refine other analyses or returned by any query,
Expand Down Expand Up @@ -121,11 +100,10 @@ struct
| _ ->
None

let is_increment_by_one state lval rval =
increment_constant lval rval ||
let is_monotone_bounded_update state lval rval =
match eval_const state (Lval lval), eval_const state rval with
| Some old_value, Some new_value ->
Z.equal new_value (Z.succ old_value)
Z.lt old_value new_value
| _ ->
false

Expand Down Expand Up @@ -153,13 +131,13 @@ struct
else
match lval with
| Var var, NoOffset when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) ->
let inc_by_one = is_increment_by_one man.local lval rval in
let monotone_bounded = is_monotone_bounded_update man.local lval rval in
let local =
match inc_by_one, eval_const man.local rval with
match monotone_bounded, eval_const man.local rval with
| true, Some z -> D.add var (`Lifted z) man.local
| _ -> D.add var (Const.top ()) man.local
in
man.sideg var (G.create_inc_by_one inc_by_one);
man.sideg var (G.create_monotone_bounded monotone_bounded);
local
| _ ->
man.local
Expand All @@ -176,8 +154,8 @@ struct
| _ ->
false
in
let (tids, inc_by_one) = man.global var in
inc_by_one && unique_owner tids
let (tids, monotone_bounded) = man.global var in
monotone_bounded && unique_owner tids
| Queries.Owner var when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) ->
let tidset = G.tids (man.global var) in
begin match TIDs.elements tidset with
Expand All @@ -190,16 +168,16 @@ struct
end
| Queries.WarnGlobal g ->
let g: V.t = Obj.obj g in
let (tidset, inc_by_one) = man.global g in
let (tidset, monotone_bounded) = man.global g in
if TIDs.is_top tidset then
(M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by a non-unique or unknown thread id" CilType.Varinfo.pretty g;)
else
(match TIDs.elements tidset with
| [tid] when TID.is_unique tid ->
if inc_by_one then
M.info_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a and is only ever increased by one" CilType.Varinfo.pretty g TID.pretty tid
if monotone_bounded then
M.info_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a and is monotonically increased to known bounds" CilType.Varinfo.pretty g TID.pretty tid
else
M.warn_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a, but is not only ever increased by one" CilType.Varinfo.pretty g TID.pretty tid
M.warn_noloc ~category:Witness "phaseGhost: global %a is only accessed by unique thread %a, but is not monotonically increased to known bounds" CilType.Varinfo.pretty g TID.pretty tid
| _ ->
M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by multiple unique threads: %a" CilType.Varinfo.pretty g TIDs.pretty tidset)
| _ ->
Expand Down
88 changes: 27 additions & 61 deletions src/analyses/phaseGhostSplit.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
(** Analysis for checking whether ghost globals are only accessed by one unique thread ([phaseGhostSplit]). *)
(** Analysis for propagating phase changes of ghost globals accepted by [phaseGhost]. *)

open Analyses
open GoblintCil
Expand Down Expand Up @@ -57,12 +57,14 @@ struct
let create_const_at_thread_end const = (const, PhaseChanges.bot ())
let create_change phase mhp pinfo = (Const.bot (), (PhaseChanges.singleton phase (MHPs.singleton mhp, pinfo)))

let can_change_to (_, changes) target currmhp =
match PhaseChanges.find_opt (`Lifted target) changes with
| Some (accesses, pinfo) when MHPs.can_any_mhp currmhp accesses ->
Some pinfo
| _ ->
None
let possible_changes_after (_, changes) current currmhp =
PhaseChanges.fold (fun target (accesses, pinfo) acc ->
match target with
| `Lifted target when Z.lt current target && MHPs.can_any_mhp currmhp accesses ->
(target, pinfo) :: acc
| _ ->
acc
) changes []
end

let initial_ghost_values () =
Expand Down Expand Up @@ -105,28 +107,6 @@ struct
| `Lifted tid when TID.is_unique tid -> TIDs.singleton tid
| _ -> TIDs.top ()

let increment_constant lval rval =
let is_same_lval e =
match Cil.stripCasts e with
| Lval lval' -> CilType.Lval.equal lval lval'
| _ -> false
in
let is_one_constant e =
match Cil.getInteger (Cil.constFold true e) with
| Some k -> Z.equal k Z.one
| None -> false
in
match Cil.stripCasts rval with
| BinOp (PlusA, e1, e2, _) ->
if is_same_lval e1 then
is_one_constant e2
else if is_same_lval e2 then
is_one_constant e1
else
false
| _ ->
false

(* This local constant folding intentionally disregards writes from other threads.
It is only for the phaseGhost checker itself. *)
(* This information must **not** be used to refine other analyses,
Expand Down Expand Up @@ -160,14 +140,6 @@ struct
| _ ->
None

let is_increment_by_one state lval rval =
increment_constant lval rval ||
match eval_const state (Lval lval), eval_const state rval with
| Some old_value, Some new_value ->
Z.equal new_value (Z.succ old_value)
| _ ->
false

let current_mhp man: MCPAccess.A.t =
Obj.obj (man.ask (PartAccess Point))

Expand All @@ -181,42 +153,36 @@ struct
man.local
else
let local = top_non_phase_ghosts man man.local in
let may_be_advanced_here m var =
let possible_advances_here m var =
if man.ask Queries.MustBeAtomic then
(* Shortcut, would also be caught below, but as it is common cheaper to check here *)
(if M.tracing then M.tracel "phaseGhost" "Is atomic -> not advancing phase"; None)
(if M.tracing then M.tracel "phaseGhost" "Is atomic -> not advancing phase"; [])
else
match man.ask (Queries.Owner var), man.ask Queries.CurrentThreadId, D.find var m with
| `Bot, _, _
| _, `Bot, _ ->
None
| `Lifted owner, _ , `Lifted z ->
G.can_change_to (man.global var) (Z.succ z) (current_mhp man)
[]
| `Lifted _owner, _ , `Lifted z ->
G.possible_changes_after (man.global var) z (current_mhp man)
| _ ->
failwith "assumption about ghost owner violated"
in
let rec handle_vars (m, (pinfo:MCPPhaseInfo.t)) = function
| [] ->
man.split m [Events.PropAuxiliaryPhaseInfo (Obj.repr pinfo)]
| var :: vars ->
match may_be_advanced_here m var with
| Some curr_pinfo ->
(let v' = (match (D.find var m) with
| `Lifted x -> Z.succ x
| _ -> failwith "assumption")
in
let advanced = D.add var (`Lifted v') m in
let pinfo' = MCPPhaseInfo.meet pinfo curr_pinfo in
handle_vars (advanced, pinfo') (var::vars);
handle_vars (m, pinfo) vars)
| None ->
handle_vars (m, pinfo) vars
List.iter (fun (target, curr_pinfo) ->
let advanced = D.add var (`Lifted target) m in
let pinfo' = MCPPhaseInfo.meet pinfo curr_pinfo in
handle_vars (advanced, pinfo') (var::vars)
) (possible_advances_here m var);
handle_vars (m, pinfo) vars
in
let traceEvolution () =
YamlWitness.VarSet.iter (fun var ->
let owner = man.ask (Queries.Owner var) in
let phase_ghost = is_phase_ghost man var in
let may_advance = phase_ghost && Option.is_some (may_be_advanced_here local var) in
let may_advance = phase_ghost && possible_advances_here local var <> [] in
M.tracel "phaseGhost" "Ghost %a is %sa phase ghost, has owner %a and may %s be advanced here" (* nosemgrep: trace-not-in-tracing *)
CilType.Varinfo.pretty var
(if phase_ghost then "" else "not ")
Expand All @@ -238,17 +204,17 @@ struct
| Var var, NoOffset when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) && not (is_phase_ghost man var) ->
D.add var (Const.top ()) local
| Var var, NoOffset when is_phase_ghost man var ->
(match eval_const local (Lval lval) with
| Some z ->
(let v = Z.succ z in
let local_new = D.add var (`Lifted v) local in
(match eval_const local (Lval lval), eval_const local rval with
| Some old_value, Some new_value when Z.lt old_value new_value ->
(let local_new = D.add var (`Lifted new_value) local in
let local_pinfo = current_pinfo man in
man.sideg var (G.create_change (`Lifted v) (current_mhp man) (local_pinfo));
man.sideg var (G.create_change (`Lifted new_value) (current_mhp man) (local_pinfo));
(* TODO: Prolong until after atomic is over? *)
if not (D.equal local local_new) then
man.emit (Events.PhaseChange {old_phase = `Lifted local; new_phase = `Lifted local_new});
local_new)
| None -> failwith "Failed to evaluate ghost to constant")
| _ ->
D.add var (Const.top ()) local)
| _ ->
local

Expand Down
8 changes: 4 additions & 4 deletions tests/regression/19-ghost-witness/02-empire-detect.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ The ghost invariants from the witness are confirmed.

Both witness ghosts are recognized as phase ghosts.

$ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is only ever increased by one" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
[Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is only ever increased by one
$ grep -E "phaseGhost: global ghost_a is only accessed by unique thread .* and is monotonically increased to known bounds" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
[Info][Witness] phaseGhost: global ghost_a is only accessed by unique thread <tid> and is monotonically increased to known bounds

$ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* and is only ever increased by one" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is only ever increased by one/'
[Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid> and is only ever increased by one
$ grep -E "phaseGhost: global ghost_b is only accessed by unique thread .* and is monotonically increased to known bounds" 02-empire-detect.out | sed -E 's/unique thread .*/unique thread <tid> and is monotonically increased to known bounds/'
[Info][Witness] phaseGhost: global ghost_b is only accessed by unique thread <tid> and is monotonically increased to known bounds
10 changes: 5 additions & 5 deletions tests/regression/19-ghost-witness/03-phase-ghost-matrix.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,27 +5,27 @@
extern int __VERIFIER_nondet_int(void);

int ghost_a = 0; // phase ghost: accessed only by main and incremented by 1.
int ghost_b = 0; // not a phase ghost: accessed only by main, but assigned a constant not equal to old + 1.
int ghost_b = 0; // phase ghost: accessed only by main and updated from known constant 0 to 5.
int ghost_c = 0; // phase ghost: accessed only by main and updated syntactically as 1 + ghost_c.
int ghost_d = 0; // not a phase ghost: accessed only by main, but incremented by 2.
int ghost_d = 0; // phase ghost: accessed only by main and incremented by 2.
int ghost_e = 0; // not a phase ghost: accessed only by main, but increment amount is nondeterministic.
int ghost_f = 0; // not exercised: never accessed in this test.
int ghost_g = 0; // not a phase ghost: incremented by both main and a different unique worker thread.
int ghost_h = 0; // not a phase ghost: incremented by a non-unique thread id.
int ghost_i = 0; // phase ghost: accessed only by one unique worker thread and incremented by 1.
int ghost_j = 0; // not a phase ghost: accessed only by one unique worker thread, but assigned 7.
int ghost_j = 0; // phase ghost: accessed only by one unique worker thread and updated from known constant 0 to 7.
int ghost_k = 0; // phase ghost: accessed only by one unique worker thread and incremented by 1 twice.
int ghost_l = 0; // not a phase ghost: accessed only by one unique worker thread, but decremented.
int ghost_m = 0; // not a phase ghost: incremented by both main and a different unique worker thread.
int ghost_n = 0; // not a phase ghost: updated by 0, so it is not an increment by 1.
int ghost_o = 0; // not a phase ghost: updated by the constant expression 1 - 1, which is not +1.
int ghost_p = 0; // not a phase ghost: assigned by a non-unique thread id.
int ghost_q = 4; // phase ghost: accessed only by main and updated from known constant 4 to 5.
int ghost_r = 4; // not a phase ghost: accessed only by main, but updated from 4 to 6.
int ghost_r = 4; // phase ghost: accessed only by main and updated from 4 to 6.
int ghost_s = 0; // not exercised: never accessed in this test.
int ghost_t = 0; // not exercised: never accessed in this test.
int ghost_u = 0; // phase ghost: main first sets it from 0 to 1, then increments it by 1.
int ghost_v = 0; // not a phase ghost: main sets it from 0 to 2.
int ghost_v = 0; // phase ghost: main sets it from 0 to 2.
int ghost_w = 0; // phase ghost: worker_unique sets it from 0 to 1.
int ghost_x = 0; // not a phase ghost: incremented by a non-unique thread id.
int ghost_y = 0; // phase ghost: accessed only by main and incremented by 1 twice.
Expand Down
Loading
Loading