|
| 1 | +(** Analysis for checking whether ghost globals are only accessed by one unique thread ([phaseGhost]). *) |
| 2 | + |
| 3 | +open Analyses |
| 4 | +open GoblintCil |
| 5 | + |
| 6 | +module TID = ThreadIdDomain.Thread |
| 7 | +module TIDs = ConcDomain.ThreadSet |
| 8 | + |
| 9 | +module Const = |
| 10 | +struct |
| 11 | + include Lattice.Flat (IntOps.BigIntOps) |
| 12 | + let name () = "ghost-constant" |
| 13 | +end |
| 14 | + |
| 15 | +module IncByOne = |
| 16 | +struct |
| 17 | + include BoolDomain.MustBool |
| 18 | + let name () = "increment-by-one" |
| 19 | +end |
| 20 | + |
| 21 | +module Spec = |
| 22 | +struct |
| 23 | + include IdentitySpec |
| 24 | + |
| 25 | + let name () = "phaseGhost" |
| 26 | + |
| 27 | + module D = MapDomain.MapBot (Basetype.Variables) (Const) |
| 28 | + include ValueContexts (D) |
| 29 | + module P = IdentityP (D) |
| 30 | + |
| 31 | + module V = VarinfoV |
| 32 | + module G = |
| 33 | + struct |
| 34 | + include Lattice.Prod (TIDs) (IncByOne) |
| 35 | + let tids = fst |
| 36 | + let inc_by_one = snd |
| 37 | + let create_tids tids = (tids, IncByOne.bot ()) |
| 38 | + let create_inc_by_one inc_by_one = (TIDs.bot (), inc_by_one) |
| 39 | + end |
| 40 | + |
| 41 | + let initial_ghost_values () = |
| 42 | + List.fold_left (fun acc -> function |
| 43 | + | GVar (v, initinfo, _) when YamlWitness.VarSet.mem v !(YamlWitness.ghostVars) -> |
| 44 | + begin match initinfo.init with |
| 45 | + | Some (SingleInit exp) -> |
| 46 | + begin match Cil.getInteger (Cil.constFold true exp) with |
| 47 | + | Some z -> D.add v (`Lifted z) acc |
| 48 | + | None -> acc |
| 49 | + end |
| 50 | + | None when Cil.isIntegralType v.vtype -> |
| 51 | + D.add v (`Lifted Z.zero) acc |
| 52 | + | _ -> |
| 53 | + acc |
| 54 | + end |
| 55 | + | _ -> |
| 56 | + acc |
| 57 | + ) (D.bot ()) !Cilfacade.current_file.globals |
| 58 | + |
| 59 | + let startstate _ = initial_ghost_values () |
| 60 | + let exitstate _ = initial_ghost_values () |
| 61 | + |
| 62 | + let tids_of_current_thread man = |
| 63 | + match man.ask Queries.CurrentThreadId with |
| 64 | + | `Lifted tid when TID.is_unique tid -> TIDs.singleton tid |
| 65 | + | _ -> TIDs.top () |
| 66 | + |
| 67 | + let increment_constant lval rval = |
| 68 | + let is_same_lval e = |
| 69 | + match Cil.stripCasts e with |
| 70 | + | Lval lval' -> CilType.Lval.equal lval lval' |
| 71 | + | _ -> false |
| 72 | + in |
| 73 | + let is_one_constant e = |
| 74 | + match Cil.getInteger (Cil.constFold true e) with |
| 75 | + | Some k -> Z.equal k Z.one |
| 76 | + | None -> false |
| 77 | + in |
| 78 | + match Cil.stripCasts rval with |
| 79 | + | BinOp (PlusA, e1, e2, _) -> |
| 80 | + if is_same_lval e1 then |
| 81 | + is_one_constant e2 |
| 82 | + else if is_same_lval e2 then |
| 83 | + is_one_constant e1 |
| 84 | + else |
| 85 | + false |
| 86 | + | _ -> |
| 87 | + false |
| 88 | + |
| 89 | + (* This local constant folding intentionally disregards writes from other threads. |
| 90 | + It is only for the phaseGhost checker itself. *) |
| 91 | + (* This information must **not** be used to refine other analyses or returned by any query, |
| 92 | + because it is unsound in the presence of other threads interfering. By the same token, it must |
| 93 | + be not used to raise Deadcode in branch. *) |
| 94 | + let rec eval_const state e = |
| 95 | + match Cil.stripCasts e with |
| 96 | + | Const _ -> |
| 97 | + Cil.getInteger (Cil.constFold true e) |
| 98 | + | Lval (Var var, NoOffset) when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) -> |
| 99 | + begin match D.find_opt var state with |
| 100 | + | Some (`Lifted z) -> Some z |
| 101 | + | _ -> None |
| 102 | + end |
| 103 | + | UnOp (Neg, e, _) -> |
| 104 | + Option.map Z.neg (eval_const state e) |
| 105 | + | BinOp (PlusA, e1, e2, _) |
| 106 | + | BinOp (IndexPI, e1, e2, _) |
| 107 | + | BinOp (PlusPI, e1, e2, _) -> |
| 108 | + Option.bind (eval_const state e1) (fun z1 -> |
| 109 | + Option.map (Z.add z1) (eval_const state e2) |
| 110 | + ) |
| 111 | + | BinOp (MinusA, e1, e2, _) -> |
| 112 | + Option.bind (eval_const state e1) (fun z1 -> |
| 113 | + Option.map (Z.sub z1) (eval_const state e2) |
| 114 | + ) |
| 115 | + | BinOp (Mult, e1, e2, _) -> |
| 116 | + Option.bind (eval_const state e1) (fun z1 -> |
| 117 | + Option.map (Z.mul z1) (eval_const state e2) |
| 118 | + ) |
| 119 | + | _ -> |
| 120 | + None |
| 121 | + |
| 122 | + let is_increment_by_one state lval rval = |
| 123 | + increment_constant lval rval || |
| 124 | + match eval_const state (Lval lval), eval_const state rval with |
| 125 | + | Some old_value, Some new_value -> |
| 126 | + Z.equal new_value (Z.succ old_value) |
| 127 | + | _ -> |
| 128 | + false |
| 129 | + |
| 130 | + let event man e oman = |
| 131 | + match e with |
| 132 | + | Events.Access {ad; _} -> |
| 133 | + let tids = tids_of_current_thread man in |
| 134 | + Queries.AD.iter (function |
| 135 | + | Queries.AD.Addr.Addr (var, _) when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) -> |
| 136 | + man.sideg var (G.create_tids tids) |
| 137 | + | _ -> |
| 138 | + () |
| 139 | + ) ad; |
| 140 | + man.local |
| 141 | + | _ -> |
| 142 | + man.local |
| 143 | + |
| 144 | + let assign man lval rval = |
| 145 | + if !AnalysisState.global_initialization then |
| 146 | + man.local |
| 147 | + else |
| 148 | + match lval with |
| 149 | + | Var var, NoOffset when YamlWitness.VarSet.mem var !(YamlWitness.ghostVars) -> |
| 150 | + let inc_by_one = is_increment_by_one man.local lval rval in |
| 151 | + let local = |
| 152 | + match inc_by_one, eval_const man.local rval with |
| 153 | + | true, Some z -> D.add var (`Lifted z) man.local |
| 154 | + | _ -> D.add var (Const.top ()) man.local |
| 155 | + in |
| 156 | + man.sideg var (G.create_inc_by_one inc_by_one); |
| 157 | + local |
| 158 | + | _ -> |
| 159 | + man.local |
| 160 | + |
| 161 | + let query man (type a) (q: a Queries.t): a Queries.result = |
| 162 | + match q with |
| 163 | + | Queries.WarnGlobal g -> |
| 164 | + let g: V.t = Obj.obj g in |
| 165 | + let (tidset, inc_by_one) = man.global g in |
| 166 | + if TIDs.is_top tidset then |
| 167 | + M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by a non-unique or unknown thread id" CilType.Varinfo.pretty g |
| 168 | + else |
| 169 | + (match TIDs.elements tidset with |
| 170 | + | [tid] when TID.is_unique tid -> |
| 171 | + if inc_by_one then |
| 172 | + 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 |
| 173 | + else |
| 174 | + 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 |
| 175 | + | _ -> |
| 176 | + M.warn_noloc ~category:Witness "phaseGhost: global %a is accessed by multiple unique threads: %a" CilType.Varinfo.pretty g TIDs.pretty tidset) |
| 177 | + | _ -> |
| 178 | + Queries.Result.top q |
| 179 | +end |
| 180 | + |
| 181 | +let _ = |
| 182 | + MCP.register_analysis ~dep:["access"; "threadid"] (module Spec : MCPSpec) |
0 commit comments