| 1 | (* |
| 2 | * Copyright 2010, INRIA, University of Copenhagen |
| 3 | * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix |
| 4 | * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen |
| 5 | * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix |
| 6 | * This file is part of Coccinelle. |
| 7 | * |
| 8 | * Coccinelle is free software: you can redistribute it and/or modify |
| 9 | * it under the terms of the GNU General Public License as published by |
| 10 | * the Free Software Foundation, according to version 2 of the License. |
| 11 | * |
| 12 | * Coccinelle is distributed in the hope that it will be useful, |
| 13 | * but WITHOUT ANY WARRANTY; without even the implied warranty of |
| 14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| 15 | * GNU General Public License for more details. |
| 16 | * |
| 17 | * You should have received a copy of the GNU General Public License |
| 18 | * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>. |
| 19 | * |
| 20 | * The authors reserve the right to distribute this or future versions of |
| 21 | * Coccinelle under other licenses. |
| 22 | *) |
| 23 | |
| 24 | |
| 25 | (* for MINUS and CONTEXT, pos is always None in this file *) |
| 26 | (*search for require*) |
| 27 | (* true = don't see all matched nodes, only modified ones *) |
| 28 | let onlyModif = ref true(*false*) |
| 29 | |
| 30 | type ex = Exists | Forall |
| 31 | let exists = ref Forall |
| 32 | |
| 33 | module Ast = Ast_cocci |
| 34 | module V = Visitor_ast |
| 35 | module CTL = Ast_ctl |
| 36 | |
| 37 | let warning s = Printf.fprintf stderr "warning: %s\n" s |
| 38 | |
| 39 | type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif |
| 40 | type formula = Lib_engine.ctlcocci |
| 41 | type top_formula = NONDECL of Lib_engine.ctlcocci | CODE of Lib_engine.ctlcocci |
| 42 | |
| 43 | let union = Common.union_set |
| 44 | let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1 |
| 45 | let subset l1 l2 = List.for_all (function x -> List.mem x l2) l1 |
| 46 | |
| 47 | let foldl1 f xs = List.fold_left f (List.hd xs) (List.tl xs) |
| 48 | let foldr1 f xs = |
| 49 | let xs = List.rev xs in List.fold_left f (List.hd xs) (List.tl xs) |
| 50 | |
| 51 | let used_after = ref ([] : Ast.meta_name list) |
| 52 | let guard_to_strict guard = if guard then CTL.NONSTRICT else CTL.STRICT |
| 53 | |
| 54 | let saved = ref ([] : Ast.meta_name list) |
| 55 | |
| 56 | let string2var x = ("",x) |
| 57 | |
| 58 | (* --------------------------------------------------------------------- *) |
| 59 | (* predicates matching various nodes in the graph *) |
| 60 | |
| 61 | let ctl_and s x y = |
| 62 | match (x,y) with |
| 63 | (CTL.False,_) | (_,CTL.False) -> CTL.False |
| 64 | | (CTL.True,a) | (a,CTL.True) -> a |
| 65 | | _ -> CTL.And(s,x,y) |
| 66 | |
| 67 | let ctl_or x y = |
| 68 | match (x,y) with |
| 69 | (CTL.True,_) | (_,CTL.True) -> CTL.True |
| 70 | | (CTL.False,a) | (a,CTL.False) -> a |
| 71 | | _ -> CTL.Or(x,y) |
| 72 | |
| 73 | let ctl_or_fl x y = |
| 74 | match (x,y) with |
| 75 | (CTL.True,_) | (_,CTL.True) -> CTL.True |
| 76 | | (CTL.False,a) | (a,CTL.False) -> a |
| 77 | | _ -> CTL.Or(y,x) |
| 78 | |
| 79 | let ctl_seqor x y = |
| 80 | match (x,y) with |
| 81 | (* drop x or true case because x might have side effects *) |
| 82 | (CTL.True,_) (* | (_,CTL.True) *) -> CTL.True |
| 83 | | (CTL.False,a) | (a,CTL.False) -> a |
| 84 | | _ -> CTL.SeqOr(x,y) |
| 85 | |
| 86 | let ctl_not = function |
| 87 | CTL.True -> CTL.False |
| 88 | | CTL.False -> CTL.True |
| 89 | | x -> CTL.Not(x) |
| 90 | |
| 91 | let ctl_ax s = function |
| 92 | CTL.True -> CTL.True |
| 93 | | CTL.False -> CTL.False |
| 94 | | x -> |
| 95 | match !exists with |
| 96 | Exists -> CTL.EX(CTL.FORWARD,x) |
| 97 | | Forall -> CTL.AX(CTL.FORWARD,s,x) |
| 98 | |
| 99 | let ctl_ax_absolute s = function |
| 100 | CTL.True -> CTL.True |
| 101 | | CTL.False -> CTL.False |
| 102 | | x -> CTL.AX(CTL.FORWARD,s,x) |
| 103 | |
| 104 | let ctl_ex = function |
| 105 | CTL.True -> CTL.True |
| 106 | | CTL.False -> CTL.False |
| 107 | | x -> CTL.EX(CTL.FORWARD,x) |
| 108 | |
| 109 | (* This stays being AX even for sgrep_mode, because it is used to identify |
| 110 | the structure of the term, not matching the pattern. *) |
| 111 | let ctl_back_ax = function |
| 112 | CTL.True -> CTL.True |
| 113 | | CTL.False -> CTL.False |
| 114 | | x -> CTL.AX(CTL.BACKWARD,CTL.NONSTRICT,x) |
| 115 | |
| 116 | let ctl_back_ex = function |
| 117 | CTL.True -> CTL.True |
| 118 | | CTL.False -> CTL.False |
| 119 | | x -> CTL.EX(CTL.BACKWARD,x) |
| 120 | |
| 121 | let ctl_ef = function |
| 122 | CTL.True -> CTL.True |
| 123 | | CTL.False -> CTL.False |
| 124 | | x -> CTL.EF(CTL.FORWARD,x) |
| 125 | |
| 126 | let ctl_ag s = function |
| 127 | CTL.True -> CTL.True |
| 128 | | CTL.False -> CTL.False |
| 129 | | x -> CTL.AG(CTL.FORWARD,s,x) |
| 130 | |
| 131 | let ctl_au s x y = |
| 132 | match (x,!exists) with |
| 133 | (CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y) |
| 134 | | (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y) |
| 135 | | (_,Exists) -> CTL.EU(CTL.FORWARD,x,y) |
| 136 | | (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y) |
| 137 | |
| 138 | let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *) |
| 139 | CTL.XX |
| 140 | (match (x,!exists) with |
| 141 | (CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y) |
| 142 | | (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y) |
| 143 | | (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y) |
| 144 | | (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)) |
| 145 | |
| 146 | let ctl_uncheck = function |
| 147 | CTL.True -> CTL.True |
| 148 | | CTL.False -> CTL.False |
| 149 | | x -> CTL.Uncheck x |
| 150 | |
| 151 | let label_pred_maker = function |
| 152 | None -> CTL.True |
| 153 | | Some (label_var,used) -> |
| 154 | used := true; |
| 155 | CTL.Pred(Lib_engine.PrefixLabel(label_var),CTL.Control) |
| 156 | |
| 157 | let bclabel_pred_maker = function |
| 158 | None -> CTL.True |
| 159 | | Some (label_var,used) -> |
| 160 | used := true; |
| 161 | CTL.Pred(Lib_engine.BCLabel(label_var),CTL.Control) |
| 162 | |
| 163 | (* label used to be used here, but it is not used; label is only needed after |
| 164 | and within dots *) |
| 165 | let predmaker guard pred label = CTL.Pred pred |
| 166 | |
| 167 | let aftpred = predmaker false (Lib_engine.After, CTL.Control) |
| 168 | let retpred = predmaker false (Lib_engine.Return, CTL.Control) |
| 169 | let funpred = predmaker false (Lib_engine.FunHeader, CTL.Control) |
| 170 | let toppred = predmaker false (Lib_engine.Top, CTL.Control) |
| 171 | let exitpred = predmaker false (Lib_engine.ErrorExit, CTL.Control) |
| 172 | let endpred = predmaker false (Lib_engine.Exit, CTL.Control) |
| 173 | let gotopred = predmaker false (Lib_engine.Goto, CTL.Control) |
| 174 | let inlooppred = predmaker false (Lib_engine.InLoop, CTL.Control) |
| 175 | let truepred = predmaker false (Lib_engine.TrueBranch, CTL.Control) |
| 176 | let falsepred = predmaker false (Lib_engine.FalseBranch, CTL.Control) |
| 177 | let fallpred = predmaker false (Lib_engine.FallThrough, CTL.Control) |
| 178 | let loopfallpred = predmaker false (Lib_engine.LoopFallThrough, CTL.Control) |
| 179 | |
| 180 | (*let aftret label_var = |
| 181 | ctl_or (aftpred label_var) |
| 182 | (ctl_or (loopfallpred label_var) (exitpred label_var))*) |
| 183 | |
| 184 | let letctr = ref 0 |
| 185 | let get_let_ctr _ = |
| 186 | let cur = !letctr in |
| 187 | letctr := cur + 1; |
| 188 | Printf.sprintf "r%d" cur |
| 189 | |
| 190 | (* --------------------------------------------------------------------- *) |
| 191 | (* --------------------------------------------------------------------- *) |
| 192 | (* Eliminate OptStm *) |
| 193 | |
| 194 | (* for optional thing with nothing after, should check that the optional thing |
| 195 | never occurs. otherwise the matching stops before it occurs *) |
| 196 | let elim_opt = |
| 197 | let mcode x = x in |
| 198 | let donothing r k e = k e in |
| 199 | |
| 200 | let fvlist l = |
| 201 | List.fold_left Common.union_set [] (List.map Ast.get_fvs l) in |
| 202 | |
| 203 | let mfvlist l = |
| 204 | List.fold_left Common.union_set [] (List.map Ast.get_mfvs l) in |
| 205 | |
| 206 | let freshlist l = |
| 207 | List.fold_left Common.union_set [] (List.map Ast.get_fresh l) in |
| 208 | |
| 209 | let inheritedlist l = |
| 210 | List.fold_left Common.union_set [] (List.map Ast.get_inherited l) in |
| 211 | |
| 212 | let savedlist l = |
| 213 | List.fold_left Common.union_set [] (List.map Ast.get_saved l) in |
| 214 | |
| 215 | let varlists l = |
| 216 | (fvlist l, mfvlist l, freshlist l, inheritedlist l, savedlist l) in |
| 217 | |
| 218 | let rec dots_list unwrapped wrapped = |
| 219 | match (unwrapped,wrapped) with |
| 220 | ([],_) -> [] |
| 221 | |
| 222 | | (Ast.Dots(_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u)::urest, |
| 223 | d0::s::d1::rest) |
| 224 | | (Ast.Nest(_,_,_,_,_,_,_)::Ast.OptStm(stm)::(Ast.Dots(_,_,_,_) as u) |
| 225 | ::urest, |
| 226 | d0::s::d1::rest) -> (* why no case for nest as u? *) |
| 227 | let l = Ast.get_line stm in |
| 228 | let new_rest1 = stm :: (dots_list (u::urest) (d1::rest)) in |
| 229 | let new_rest2 = dots_list urest rest in |
| 230 | let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) = |
| 231 | varlists new_rest1 in |
| 232 | let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) = |
| 233 | varlists new_rest2 in |
| 234 | [d0; |
| 235 | {(Ast.make_term |
| 236 | (Ast.Disj |
| 237 | [{(Ast.make_term(Ast.DOTS(new_rest1))) with |
| 238 | Ast.node_line = l; |
| 239 | Ast.free_vars = fv_rest1; |
| 240 | Ast.minus_free_vars = mfv_rest1; |
| 241 | Ast.fresh_vars = fresh_rest1; |
| 242 | Ast.inherited = inherited_rest1; |
| 243 | Ast.saved_witness = s1}; |
| 244 | {(Ast.make_term(Ast.DOTS(new_rest2))) with |
| 245 | Ast.node_line = l; |
| 246 | Ast.free_vars = fv_rest2; |
| 247 | Ast.minus_free_vars = mfv_rest2; |
| 248 | Ast.fresh_vars = fresh_rest2; |
| 249 | Ast.inherited = inherited_rest2; |
| 250 | Ast.saved_witness = s2}])) with |
| 251 | Ast.node_line = l; |
| 252 | Ast.free_vars = fv_rest1; |
| 253 | Ast.minus_free_vars = mfv_rest1; |
| 254 | Ast.fresh_vars = fresh_rest1; |
| 255 | Ast.inherited = inherited_rest1; |
| 256 | Ast.saved_witness = s1}] |
| 257 | |
| 258 | | (Ast.OptStm(stm)::urest,_::rest) -> |
| 259 | let l = Ast.get_line stm in |
| 260 | let new_rest1 = dots_list urest rest in |
| 261 | let new_rest2 = stm::new_rest1 in |
| 262 | let (fv_rest1,mfv_rest1,fresh_rest1,inherited_rest1,s1) = |
| 263 | varlists new_rest1 in |
| 264 | let (fv_rest2,mfv_rest2,fresh_rest2,inherited_rest2,s2) = |
| 265 | varlists new_rest2 in |
| 266 | [{(Ast.make_term |
| 267 | (Ast.Disj |
| 268 | [{(Ast.make_term(Ast.DOTS(new_rest2))) with |
| 269 | Ast.node_line = l; |
| 270 | Ast.free_vars = fv_rest2; |
| 271 | Ast.minus_free_vars = mfv_rest2; |
| 272 | Ast.fresh_vars = fresh_rest2; |
| 273 | Ast.inherited = inherited_rest2; |
| 274 | Ast.saved_witness = s2}; |
| 275 | {(Ast.make_term(Ast.DOTS(new_rest1))) with |
| 276 | Ast.node_line = l; |
| 277 | Ast.free_vars = fv_rest1; |
| 278 | Ast.minus_free_vars = mfv_rest1; |
| 279 | Ast.fresh_vars = fresh_rest1; |
| 280 | Ast.inherited = inherited_rest1; |
| 281 | Ast.saved_witness = s1}])) with |
| 282 | Ast.node_line = l; |
| 283 | Ast.free_vars = fv_rest2; |
| 284 | Ast.minus_free_vars = mfv_rest2; |
| 285 | Ast.fresh_vars = fresh_rest2; |
| 286 | Ast.inherited = inherited_rest2; |
| 287 | Ast.saved_witness = s2}] |
| 288 | |
| 289 | | ([Ast.Dots(_,_,_,_);Ast.OptStm(stm)],[d1;_]) -> |
| 290 | let l = Ast.get_line stm in |
| 291 | let fv_stm = Ast.get_fvs stm in |
| 292 | let mfv_stm = Ast.get_mfvs stm in |
| 293 | let fresh_stm = Ast.get_fresh stm in |
| 294 | let inh_stm = Ast.get_inherited stm in |
| 295 | let saved_stm = Ast.get_saved stm in |
| 296 | let fv_d1 = Ast.get_fvs d1 in |
| 297 | let mfv_d1 = Ast.get_mfvs d1 in |
| 298 | let fresh_d1 = Ast.get_fresh d1 in |
| 299 | let inh_d1 = Ast.get_inherited d1 in |
| 300 | let saved_d1 = Ast.get_saved d1 in |
| 301 | let fv_both = Common.union_set fv_stm fv_d1 in |
| 302 | let mfv_both = Common.union_set mfv_stm mfv_d1 in |
| 303 | let fresh_both = Common.union_set fresh_stm fresh_d1 in |
| 304 | let inh_both = Common.union_set inh_stm inh_d1 in |
| 305 | let saved_both = Common.union_set saved_stm saved_d1 in |
| 306 | [d1; |
| 307 | {(Ast.make_term |
| 308 | (Ast.Disj |
| 309 | [{(Ast.make_term(Ast.DOTS([stm]))) with |
| 310 | Ast.node_line = l; |
| 311 | Ast.free_vars = fv_stm; |
| 312 | Ast.minus_free_vars = mfv_stm; |
| 313 | Ast.fresh_vars = fresh_stm; |
| 314 | Ast.inherited = inh_stm; |
| 315 | Ast.saved_witness = saved_stm}; |
| 316 | {(Ast.make_term(Ast.DOTS([d1]))) with |
| 317 | Ast.node_line = l; |
| 318 | Ast.free_vars = fv_d1; |
| 319 | Ast.minus_free_vars = mfv_d1; |
| 320 | Ast.fresh_vars = fresh_d1; |
| 321 | Ast.inherited = inh_d1; |
| 322 | Ast.saved_witness = saved_d1}])) with |
| 323 | Ast.node_line = l; |
| 324 | Ast.free_vars = fv_both; |
| 325 | Ast.minus_free_vars = mfv_both; |
| 326 | Ast.fresh_vars = fresh_both; |
| 327 | Ast.inherited = inh_both; |
| 328 | Ast.saved_witness = saved_both}] |
| 329 | |
| 330 | | ([Ast.Nest(_,_,_,_,_,_,_);Ast.OptStm(stm)],[d1;_]) -> |
| 331 | let l = Ast.get_line stm in |
| 332 | let rw = Ast.rewrap stm in |
| 333 | let rwd = Ast.rewrap stm in |
| 334 | let dots = Ast.Dots(Ast.make_mcode "...",[],[],[]) in |
| 335 | [d1;rw(Ast.Disj |
| 336 | [rwd(Ast.DOTS([stm])); |
| 337 | {(Ast.make_term(Ast.DOTS([rw dots]))) |
| 338 | with Ast.node_line = l}])] |
| 339 | |
| 340 | | (_::urest,stm::rest) -> stm :: (dots_list urest rest) |
| 341 | | _ -> failwith "not possible" in |
| 342 | |
| 343 | let stmtdotsfn r k d = |
| 344 | let d = k d in |
| 345 | Ast.rewrap d |
| 346 | (match Ast.unwrap d with |
| 347 | Ast.DOTS(l) -> Ast.DOTS(dots_list (List.map Ast.unwrap l) l) |
| 348 | | Ast.CIRCLES(l) -> failwith "elimopt: not supported" |
| 349 | | Ast.STARS(l) -> failwith "elimopt: not supported") in |
| 350 | |
| 351 | V.rebuilder |
| 352 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode |
| 353 | donothing donothing stmtdotsfn donothing donothing |
| 354 | donothing donothing donothing donothing donothing donothing donothing |
| 355 | donothing donothing donothing donothing donothing |
| 356 | |
| 357 | (* --------------------------------------------------------------------- *) |
| 358 | (* after management *) |
| 359 | (* We need Guard for the following case: |
| 360 | <... |
| 361 | a |
| 362 | <... |
| 363 | b |
| 364 | ...> |
| 365 | ...> |
| 366 | foo(); |
| 367 | |
| 368 | Here the inner <... b ...> should not go past foo. But foo is not the |
| 369 | "after" of the body of the outer nest, because we don't want to search for |
| 370 | it in the case where the body of the outer nest ends in something other |
| 371 | than dots or a nest. *) |
| 372 | |
| 373 | (* what is the difference between tail and end??? *) |
| 374 | |
| 375 | type after = After of formula | Guard of formula | Tail | End | VeryEnd |
| 376 | |
| 377 | let a2n = function After x -> Guard x | a -> a |
| 378 | |
| 379 | let print_ctl x = |
| 380 | let pp_pred (x,_) = Pretty_print_engine.pp_predicate x in |
| 381 | let pp_meta (_,x) = Common.pp x in |
| 382 | Pretty_print_ctl.pp_ctl (pp_pred,pp_meta) false x; |
| 383 | Format.print_newline() |
| 384 | |
| 385 | let print_after = function |
| 386 | After ctl -> Printf.printf "After:\n"; print_ctl ctl |
| 387 | | Guard ctl -> Printf.printf "Guard:\n"; print_ctl ctl |
| 388 | | Tail -> Printf.printf "Tail\n" |
| 389 | | VeryEnd -> Printf.printf "Very End\n" |
| 390 | | End -> Printf.printf "End\n" |
| 391 | |
| 392 | (* --------------------------------------------------------------------- *) |
| 393 | (* Top-level code *) |
| 394 | |
| 395 | let fresh_var _ = string2var "_v" |
| 396 | let fresh_pos _ = string2var "_pos" (* must be a constant *) |
| 397 | |
| 398 | let fresh_metavar _ = "_S" |
| 399 | |
| 400 | (* fvinfo is going to end up being from the whole associated statement. |
| 401 | it would be better if it were just the free variables in d, but free_vars.ml |
| 402 | doesn't keep track of free variables on + code *) |
| 403 | let make_meta_rule_elem d fvinfo = |
| 404 | let nm = fresh_metavar() in |
| 405 | Ast.make_meta_rule_elem nm d fvinfo |
| 406 | |
| 407 | let get_unquantified quantified vars = |
| 408 | List.filter (function x -> not (List.mem x quantified)) vars |
| 409 | |
| 410 | let make_seq guard l = |
| 411 | let s = guard_to_strict guard in |
| 412 | foldr1 (function rest -> function cur -> ctl_and s cur (ctl_ax s rest)) l |
| 413 | |
| 414 | let make_seq_after2 guard first rest = |
| 415 | let s = guard_to_strict guard in |
| 416 | match rest with |
| 417 | After rest -> ctl_and s first (ctl_ax s (ctl_ax s rest)) |
| 418 | | _ -> first |
| 419 | |
| 420 | let make_seq_after guard first rest = |
| 421 | match rest with |
| 422 | After rest -> make_seq guard [first;rest] |
| 423 | | _ -> first |
| 424 | |
| 425 | let opt_and guard first rest = |
| 426 | let s = guard_to_strict guard in |
| 427 | match first with |
| 428 | None -> rest |
| 429 | | Some first -> ctl_and s first rest |
| 430 | |
| 431 | let and_after guard first rest = |
| 432 | let s = guard_to_strict guard in |
| 433 | match rest with After rest -> ctl_and s first rest | _ -> first |
| 434 | |
| 435 | let contains_modif = |
| 436 | let bind x y = x or y in |
| 437 | let option_default = false in |
| 438 | let mcode r (_,_,kind,metapos) = |
| 439 | match kind with |
| 440 | Ast.MINUS(_,_,_,_) -> true |
| 441 | | Ast.PLUS _ -> failwith "not possible" |
| 442 | | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in |
| 443 | let do_nothing r k e = k e in |
| 444 | let rule_elem r k re = |
| 445 | let res = k re in |
| 446 | match Ast.unwrap re with |
| 447 | Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) -> |
| 448 | bind (mcode r ((),(),bef,[])) res |
| 449 | | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res |
| 450 | | _ -> res in |
| 451 | let init r k i = |
| 452 | let res = k i in |
| 453 | match Ast.unwrap i with |
| 454 | Ast.StrInitList(allminus,_,_,_,_) -> allminus or res |
| 455 | | _ -> res in |
| 456 | let recursor = |
| 457 | V.combiner bind option_default |
| 458 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode |
| 459 | do_nothing do_nothing do_nothing do_nothing do_nothing |
| 460 | do_nothing do_nothing do_nothing do_nothing init do_nothing |
| 461 | do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in |
| 462 | recursor.V.combiner_rule_elem |
| 463 | |
| 464 | let contains_pos = |
| 465 | let bind x y = x or y in |
| 466 | let option_default = false in |
| 467 | let mcode r (_,_,kind,metapos) = not (metapos = []) in |
| 468 | let do_nothing r k e = k e in |
| 469 | let rule_elem r k re = |
| 470 | let res = k re in |
| 471 | match Ast.unwrap re with |
| 472 | Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) -> |
| 473 | bind (mcode r ((),(),bef,[])) res |
| 474 | | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res |
| 475 | | _ -> res in |
| 476 | let recursor = |
| 477 | V.combiner bind option_default |
| 478 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode |
| 479 | do_nothing do_nothing do_nothing do_nothing do_nothing |
| 480 | do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing |
| 481 | do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in |
| 482 | recursor.V.combiner_rule_elem |
| 483 | |
| 484 | (* code is not a DisjRuleElem *) |
| 485 | let make_match label guard code = |
| 486 | let v = fresh_var() in |
| 487 | let matcher = Lib_engine.Match(code) in |
| 488 | if contains_modif code && not guard |
| 489 | then CTL.Exists(true,v,predmaker guard (matcher,CTL.Modif v) label) |
| 490 | else |
| 491 | let iso_info = !Flag.track_iso_usage && not (Ast.get_isos code = []) in |
| 492 | (match (iso_info,!onlyModif,guard, |
| 493 | intersect !used_after (Ast.get_fvs code)) with |
| 494 | (false,true,_,[]) | (_,_,true,_) -> |
| 495 | predmaker guard (matcher,CTL.Control) label |
| 496 | | _ -> CTL.Exists(true,v,predmaker guard (matcher,CTL.UnModif v) label)) |
| 497 | |
| 498 | let make_raw_match label guard code = |
| 499 | match intersect !used_after (Ast.get_fvs code) with |
| 500 | [] -> predmaker guard (Lib_engine.Match(code),CTL.Control) label |
| 501 | | _ -> |
| 502 | let v = fresh_var() in |
| 503 | CTL.Exists(true,v,predmaker guard (Lib_engine.Match(code),CTL.UnModif v) |
| 504 | label) |
| 505 | |
| 506 | let rec seq_fvs quantified = function |
| 507 | [] -> [] |
| 508 | | fv1::fvs -> |
| 509 | let t1fvs = get_unquantified quantified fv1 in |
| 510 | let termfvs = |
| 511 | List.fold_left Common.union_set [] |
| 512 | (List.map (get_unquantified quantified) fvs) in |
| 513 | let bothfvs = Common.inter_set t1fvs termfvs in |
| 514 | let t1onlyfvs = Common.minus_set t1fvs bothfvs in |
| 515 | let new_quantified = Common.union_set bothfvs quantified in |
| 516 | (t1onlyfvs,bothfvs)::(seq_fvs new_quantified fvs) |
| 517 | |
| 518 | let quantify guard = |
| 519 | List.fold_right |
| 520 | (function cur -> |
| 521 | function code -> CTL.Exists (not guard && List.mem cur !saved,cur,code)) |
| 522 | |
| 523 | let non_saved_quantify = |
| 524 | List.fold_right |
| 525 | (function cur -> function code -> CTL.Exists (false,cur,code)) |
| 526 | |
| 527 | let intersectll lst nested_list = |
| 528 | List.filter (function x -> List.exists (List.mem x) nested_list) lst |
| 529 | |
| 530 | (* --------------------------------------------------------------------- *) |
| 531 | (* Count depth of braces. The translation of a closed brace appears deeply |
| 532 | nested within the translation of the sequence term, so the name of the |
| 533 | paren var has to take into account the names of the nested braces. On the |
| 534 | other hand the close brace does not escape, so we don't have to take into |
| 535 | account other paren variable names. *) |
| 536 | |
| 537 | (* called repetitively, which is inefficient, but less trouble than adding a |
| 538 | new field to Seq and FunDecl *) |
| 539 | let count_nested_braces s = |
| 540 | let bind x y = max x y in |
| 541 | let option_default = 0 in |
| 542 | let stmt_count r k s = |
| 543 | match Ast.unwrap s with |
| 544 | Ast.Seq(_,_,_) | Ast.FunDecl(_,_,_,_) -> (k s) + 1 |
| 545 | | _ -> k s in |
| 546 | let donothing r k e = k e in |
| 547 | let mcode r x = 0 in |
| 548 | let recursor = V.combiner bind option_default |
| 549 | mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode |
| 550 | donothing donothing donothing donothing donothing |
| 551 | donothing donothing donothing donothing donothing donothing |
| 552 | donothing donothing stmt_count donothing donothing donothing in |
| 553 | let res = string_of_int (recursor.V.combiner_statement s) in |
| 554 | string2var ("p"^res) |
| 555 | |
| 556 | let labelctr = ref 0 |
| 557 | let get_label_ctr _ = |
| 558 | let cur = !labelctr in |
| 559 | labelctr := cur + 1; |
| 560 | string2var (Printf.sprintf "l%d" cur) |
| 561 | |
| 562 | (* --------------------------------------------------------------------- *) |
| 563 | (* annotate dots with before and after neighbors *) |
| 564 | |
| 565 | let print_bef_aft = function |
| 566 | Ast.WParen (re,n) -> |
| 567 | Printf.printf "bef/aft\n"; |
| 568 | Pretty_print_cocci.rule_elem "" re; |
| 569 | Format.print_newline() |
| 570 | | Ast.Other s -> |
| 571 | Printf.printf "bef/aft\n"; |
| 572 | Pretty_print_cocci.statement "" s; |
| 573 | Format.print_newline() |
| 574 | | Ast.Other_dots d -> |
| 575 | Printf.printf "bef/aft\n"; |
| 576 | Pretty_print_cocci.statement_dots d; |
| 577 | Format.print_newline() |
| 578 | |
| 579 | (* [] can only occur if we are in a disj, where it comes from a ? In that |
| 580 | case, we want to use a, which accumulates all of the previous patterns in |
| 581 | their entirety. *) |
| 582 | let rec get_before_elem sl a = |
| 583 | match Ast.unwrap sl with |
| 584 | Ast.DOTS(x) -> |
| 585 | let rec loop sl a = |
| 586 | match sl with |
| 587 | [] -> ([],Common.Right a) |
| 588 | | [e] -> |
| 589 | let (e,ea) = get_before_e e a in |
| 590 | ([e],Common.Left ea) |
| 591 | | e::sl -> |
| 592 | let (e,ea) = get_before_e e a in |
| 593 | let (sl,sla) = loop sl ea in |
| 594 | (e::sl,sla) in |
| 595 | let (l,a) = loop x a in |
| 596 | (Ast.rewrap sl (Ast.DOTS(l)),a) |
| 597 | | Ast.CIRCLES(x) -> failwith "not supported" |
| 598 | | Ast.STARS(x) -> failwith "not supported" |
| 599 | |
| 600 | and get_before sl a = |
| 601 | match get_before_elem sl a with |
| 602 | (term,Common.Left x) -> (term,x) |
| 603 | | (term,Common.Right x) -> (term,x) |
| 604 | |
| 605 | and get_before_whencode wc = |
| 606 | List.map |
| 607 | (function |
| 608 | Ast.WhenNot w -> let (w,_) = get_before w [] in Ast.WhenNot w |
| 609 | | Ast.WhenAlways w -> let (w,_) = get_before_e w [] in Ast.WhenAlways w |
| 610 | | Ast.WhenModifier(x) -> Ast.WhenModifier(x) |
| 611 | | Ast.WhenNotTrue w -> Ast.WhenNotTrue w |
| 612 | | Ast.WhenNotFalse w -> Ast.WhenNotFalse w) |
| 613 | wc |
| 614 | |
| 615 | and get_before_e s a = |
| 616 | match Ast.unwrap s with |
| 617 | Ast.Dots(d,w,_,aft) -> |
| 618 | (Ast.rewrap s (Ast.Dots(d,get_before_whencode w,a,aft)),a) |
| 619 | | Ast.Nest(starter,stmt_dots,ender,w,multi,_,aft) -> |
| 620 | let w = get_before_whencode w in |
| 621 | let (sd,_) = get_before stmt_dots a in |
| 622 | (*let a = |
| 623 | got rid of this, don't want to let nests overshoot |
| 624 | List.filter |
| 625 | (function |
| 626 | Ast.Other a -> |
| 627 | let unifies = |
| 628 | Unify_ast.unify_statement_dots |
| 629 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in |
| 630 | (match unifies with |
| 631 | Unify_ast.MAYBE -> false |
| 632 | | _ -> true) |
| 633 | | Ast.Other_dots a -> |
| 634 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in |
| 635 | (match unifies with |
| 636 | Unify_ast.MAYBE -> false |
| 637 | | _ -> true) |
| 638 | | _ -> true) |
| 639 | a in*) |
| 640 | (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,a,aft)), |
| 641 | [Ast.Other_dots stmt_dots]) |
| 642 | | Ast.Disj(stmt_dots_list) -> |
| 643 | let (dsl,dsla) = |
| 644 | List.split (List.map (function e -> get_before e a) stmt_dots_list) in |
| 645 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) |
| 646 | | Ast.Atomic(ast) -> |
| 647 | (match Ast.unwrap ast with |
| 648 | Ast.MetaStmt(_,_,_,_) -> (s,[]) |
| 649 | | _ -> (s,[Ast.Other s])) |
| 650 | | Ast.Seq(lbrace,body,rbrace) -> |
| 651 | let index = count_nested_braces s in |
| 652 | let (bd,_) = get_before body [Ast.WParen(lbrace,index)] in |
| 653 | (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)),[Ast.WParen(rbrace,index)]) |
| 654 | | Ast.Define(header,body) -> |
| 655 | let (body,_) = get_before body [] in |
| 656 | (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s]) |
| 657 | | Ast.IfThen(ifheader,branch,aft) -> |
| 658 | let (br,_) = get_before_e branch [] in |
| 659 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)), [Ast.Other s]) |
| 660 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> |
| 661 | let (br1,_) = get_before_e branch1 [] in |
| 662 | let (br2,_) = get_before_e branch2 [] in |
| 663 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) |
| 664 | | Ast.While(header,body,aft) -> |
| 665 | let (bd,_) = get_before_e body [] in |
| 666 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) |
| 667 | | Ast.For(header,body,aft) -> |
| 668 | let (bd,_) = get_before_e body [] in |
| 669 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) |
| 670 | | Ast.Do(header,body,tail) -> |
| 671 | let (bd,_) = get_before_e body [] in |
| 672 | (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s]) |
| 673 | | Ast.Iterator(header,body,aft) -> |
| 674 | let (bd,_) = get_before_e body [] in |
| 675 | (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s]) |
| 676 | | Ast.Switch(header,lb,decls,cases,rb) -> |
| 677 | let index = count_nested_braces s in |
| 678 | let (de,dea) = get_before decls [Ast.WParen(lb,index)] in |
| 679 | let cases = |
| 680 | List.map |
| 681 | (function case_line -> |
| 682 | match Ast.unwrap case_line with |
| 683 | Ast.CaseLine(header,body) -> |
| 684 | let (body,_) = get_before body [] in |
| 685 | Ast.rewrap case_line (Ast.CaseLine(header,body)) |
| 686 | | Ast.OptCase(case_line) -> failwith "not supported") |
| 687 | cases in |
| 688 | (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)), |
| 689 | [Ast.WParen(rb,index)]) |
| 690 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
| 691 | let (bd,_) = get_before body [] in |
| 692 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[]) |
| 693 | | _ -> |
| 694 | Pretty_print_cocci.statement "" s; Format.print_newline(); |
| 695 | failwith "get_before_e: not supported" |
| 696 | |
| 697 | let rec get_after sl a = |
| 698 | match Ast.unwrap sl with |
| 699 | Ast.DOTS(x) -> |
| 700 | let rec loop sl = |
| 701 | match sl with |
| 702 | [] -> ([],a) |
| 703 | | e::sl -> |
| 704 | let (sl,sla) = loop sl in |
| 705 | let (e,ea) = get_after_e e sla in |
| 706 | (e::sl,ea) in |
| 707 | let (l,a) = loop x in |
| 708 | (Ast.rewrap sl (Ast.DOTS(l)),a) |
| 709 | | Ast.CIRCLES(x) -> failwith "not supported" |
| 710 | | Ast.STARS(x) -> failwith "not supported" |
| 711 | |
| 712 | and get_after_whencode a wc = |
| 713 | List.map |
| 714 | (function |
| 715 | Ast.WhenNot w -> let (w,_) = get_after w a (*?*) in Ast.WhenNot w |
| 716 | | Ast.WhenAlways w -> let (w,_) = get_after_e w a in Ast.WhenAlways w |
| 717 | | Ast.WhenModifier(x) -> Ast.WhenModifier(x) |
| 718 | | Ast.WhenNotTrue w -> Ast.WhenNotTrue w |
| 719 | | Ast.WhenNotFalse w -> Ast.WhenNotFalse w) |
| 720 | wc |
| 721 | |
| 722 | and get_after_e s a = |
| 723 | match Ast.unwrap s with |
| 724 | Ast.Dots(d,w,bef,_) -> |
| 725 | (Ast.rewrap s (Ast.Dots(d,get_after_whencode a w,bef,a)),a) |
| 726 | | Ast.Nest(starter,stmt_dots,ender,w,multi,bef,_) -> |
| 727 | let w = get_after_whencode a w in |
| 728 | let (sd,_) = get_after stmt_dots a in |
| 729 | (*let a = |
| 730 | got rid of this. don't want to let nests overshoot |
| 731 | List.filter |
| 732 | (function |
| 733 | Ast.Other a -> |
| 734 | let unifies = |
| 735 | Unify_ast.unify_statement_dots |
| 736 | (Ast.rewrap s (Ast.DOTS([a]))) stmt_dots in |
| 737 | (match unifies with |
| 738 | Unify_ast.MAYBE -> false |
| 739 | | _ -> true) |
| 740 | | Ast.Other_dots a -> |
| 741 | let unifies = Unify_ast.unify_statement_dots a stmt_dots in |
| 742 | (match unifies with |
| 743 | Unify_ast.MAYBE -> false |
| 744 | | _ -> true) |
| 745 | | _ -> true) |
| 746 | a in*) |
| 747 | (Ast.rewrap s (Ast.Nest(starter,sd,ender,w,multi,bef,a)), |
| 748 | [Ast.Other_dots stmt_dots]) |
| 749 | | Ast.Disj(stmt_dots_list) -> |
| 750 | let (dsl,dsla) = |
| 751 | List.split (List.map (function e -> get_after e a) stmt_dots_list) in |
| 752 | (Ast.rewrap s (Ast.Disj(dsl)),List.fold_left Common.union_set [] dsla) |
| 753 | | Ast.Atomic(ast) -> |
| 754 | (match Ast.unwrap ast with |
| 755 | Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots _,i) -> |
| 756 | (* check "after" information for metavar optimization *) |
| 757 | (* if the error is not desired, could just return [], then |
| 758 | the optimization (check for EF) won't take place *) |
| 759 | List.iter |
| 760 | (function |
| 761 | Ast.Other x -> |
| 762 | (match Ast.unwrap x with |
| 763 | Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) -> |
| 764 | failwith |
| 765 | "dots/nest not allowed before and after stmt metavar" |
| 766 | | _ -> ()) |
| 767 | | Ast.Other_dots x -> |
| 768 | (match Ast.undots x with |
| 769 | x::_ -> |
| 770 | (match Ast.unwrap x with |
| 771 | Ast.Dots(_,_,_,_) | Ast.Nest(_,_,_,_,_,_,_) -> |
| 772 | failwith |
| 773 | ("dots/nest not allowed before and after stmt "^ |
| 774 | "metavar") |
| 775 | | _ -> ()) |
| 776 | | _ -> ()) |
| 777 | | _ -> ()) |
| 778 | a; |
| 779 | (Ast.rewrap s |
| 780 | (Ast.Atomic |
| 781 | (Ast.rewrap s |
| 782 | (Ast.MetaStmt(nm,keep,Ast.SequencibleAfterDots a,i)))),[]) |
| 783 | | Ast.MetaStmt(_,_,_,_) -> (s,[]) |
| 784 | | _ -> (s,[Ast.Other s])) |
| 785 | | Ast.Seq(lbrace,body,rbrace) -> |
| 786 | let index = count_nested_braces s in |
| 787 | let (bd,_) = get_after body [Ast.WParen(rbrace,index)] in |
| 788 | (Ast.rewrap s (Ast.Seq(lbrace,bd,rbrace)), |
| 789 | [Ast.WParen(lbrace,index)]) |
| 790 | | Ast.Define(header,body) -> |
| 791 | let (body,_) = get_after body a in |
| 792 | (Ast.rewrap s (Ast.Define(header,body)), [Ast.Other s]) |
| 793 | | Ast.IfThen(ifheader,branch,aft) -> |
| 794 | let (br,_) = get_after_e branch a in |
| 795 | (Ast.rewrap s (Ast.IfThen(ifheader,br,aft)),[Ast.Other s]) |
| 796 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> |
| 797 | let (br1,_) = get_after_e branch1 a in |
| 798 | let (br2,_) = get_after_e branch2 a in |
| 799 | (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s]) |
| 800 | | Ast.While(header,body,aft) -> |
| 801 | let (bd,_) = get_after_e body a in |
| 802 | (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s]) |
| 803 | | Ast.For(header,body,aft) -> |
| 804 | let (bd,_) = get_after_e body a in |
| 805 | (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s]) |
| 806 | | Ast.Do(header,body,tail) -> |
| 807 | let (bd,_) = get_after_e body a in |
| 808 | (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s]) |
| 809 | | Ast.Iterator(header,body,aft) -> |
| 810 | let (bd,_) = get_after_e body a in |
| 811 | (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s]) |
| 812 | | Ast.Switch(header,lb,decls,cases,rb) -> |
| 813 | let index = count_nested_braces s in |
| 814 | let cases = |
| 815 | List.map |
| 816 | (function case_line -> |
| 817 | match Ast.unwrap case_line with |
| 818 | Ast.CaseLine(header,body) -> |
| 819 | let (body,_) = get_after body [Ast.WParen(rb,index)] in |
| 820 | Ast.rewrap case_line (Ast.CaseLine(header,body)) |
| 821 | | Ast.OptCase(case_line) -> failwith "not supported") |
| 822 | cases in |
| 823 | let (de,_) = get_after decls [] in |
| 824 | (Ast.rewrap s (Ast.Switch(header,lb,de,cases,rb)),[Ast.WParen(lb,index)]) |
| 825 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
| 826 | let (bd,_) = get_after body [] in |
| 827 | (Ast.rewrap s (Ast.FunDecl(header,lbrace,bd,rbrace)),[]) |
| 828 | | _ -> failwith "get_after_e: not supported" |
| 829 | |
| 830 | let preprocess_dots sl = |
| 831 | let (sl,_) = get_before sl [] in |
| 832 | let (sl,_) = get_after sl [] in |
| 833 | sl |
| 834 | |
| 835 | let preprocess_dots_e sl = |
| 836 | let (sl,_) = get_before_e sl [] in |
| 837 | let (sl,_) = get_after_e sl [] in |
| 838 | sl |
| 839 | |
| 840 | (* --------------------------------------------------------------------- *) |
| 841 | (* various return_related things *) |
| 842 | |
| 843 | let rec ends_in_return stmt_list = |
| 844 | match Ast.unwrap stmt_list with |
| 845 | Ast.DOTS(x) -> |
| 846 | (match List.rev x with |
| 847 | x::_ -> |
| 848 | (match Ast.unwrap x with |
| 849 | Ast.Atomic(x) -> |
| 850 | let rec loop x = |
| 851 | match Ast.unwrap x with |
| 852 | Ast.Return(_,_) | Ast.ReturnExpr(_,_,_) -> true |
| 853 | | Ast.DisjRuleElem((_::_) as l) -> List.for_all loop l |
| 854 | | _ -> false in |
| 855 | loop x |
| 856 | | Ast.Disj(disjs) -> List.for_all ends_in_return disjs |
| 857 | | _ -> false) |
| 858 | | _ -> false) |
| 859 | | Ast.CIRCLES(x) -> failwith "not supported" |
| 860 | | Ast.STARS(x) -> failwith "not supported" |
| 861 | |
| 862 | (* --------------------------------------------------------------------- *) |
| 863 | (* expressions *) |
| 864 | |
| 865 | let exptymatch l make_match make_guard_match = |
| 866 | let pos = fresh_pos() in |
| 867 | let matches_guard_matches = |
| 868 | List.map |
| 869 | (function x -> |
| 870 | let pos = Ast.make_mcode pos in |
| 871 | (make_match (Ast.set_pos x (Some pos)), |
| 872 | make_guard_match (Ast.set_pos x (Some pos)))) |
| 873 | l in |
| 874 | let (matches,guard_matches) = List.split matches_guard_matches in |
| 875 | let rec suffixes = function |
| 876 | [] -> [] |
| 877 | | x::xs -> xs::(suffixes xs) in |
| 878 | let prefixes = |
| 879 | (* normally, we check that an expression does not match something |
| 880 | earlier in the disjunction (calculated as prefixes). But for large |
| 881 | disjunctions, this can result in a very big CTL formula. So we |
| 882 | give the user the option to say he doesn't want this feature, if that is |
| 883 | the case. *) |
| 884 | if !Flag_matcher.no_safe_expressions |
| 885 | then List.map (function _ -> []) matches |
| 886 | else List.rev (suffixes (List.rev guard_matches)) in |
| 887 | let info = (* not null *) |
| 888 | List.map2 |
| 889 | (function matcher -> |
| 890 | function negates -> |
| 891 | CTL.Exists |
| 892 | (false,pos, |
| 893 | ctl_and CTL.NONSTRICT matcher |
| 894 | (ctl_not |
| 895 | (ctl_uncheck (List.fold_left ctl_or_fl CTL.False negates))))) |
| 896 | matches prefixes in |
| 897 | CTL.InnerAnd(List.fold_left ctl_or_fl CTL.False (List.rev info)) |
| 898 | |
| 899 | (* code might be a DisjRuleElem, in which case we break it apart |
| 900 | code might contain an Exp or Ty |
| 901 | this one pushes the quantifier inwards *) |
| 902 | let do_re_matches label guard res quantified minus_quantified = |
| 903 | let make_guard_match x = |
| 904 | let stmt_fvs = Ast.get_mfvs x in |
| 905 | let fvs = get_unquantified minus_quantified stmt_fvs in |
| 906 | non_saved_quantify fvs (make_match None true x) in |
| 907 | let make_match x = |
| 908 | let stmt_fvs = Ast.get_fvs x in |
| 909 | let fvs = get_unquantified quantified stmt_fvs in |
| 910 | quantify guard fvs (make_match None guard x) in |
| 911 | (* label used to be used here, but it is not use; label is only needed after |
| 912 | and within dots |
| 913 | ctl_and CTL.NONSTRICT (label_pred_maker label) *) |
| 914 | (match List.map Ast.unwrap res with |
| 915 | [] -> failwith "unexpected empty disj" |
| 916 | | Ast.Exp(e)::rest -> exptymatch res make_match make_guard_match |
| 917 | | Ast.Ty(t)::rest -> exptymatch res make_match make_guard_match |
| 918 | | all -> |
| 919 | if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false) |
| 920 | all |
| 921 | then failwith "unexpected exp or ty"; |
| 922 | List.fold_left ctl_seqor CTL.False (List.map make_match res)) |
| 923 | |
| 924 | (* code might be a DisjRuleElem, in which case we break it apart |
| 925 | code doesn't contain an Exp or Ty |
| 926 | this one is for use when it is not practical to push the quantifier inwards |
| 927 | *) |
| 928 | let header_match label guard code : ('a, Ast.meta_name, 'b) CTL.generic_ctl = |
| 929 | match Ast.unwrap code with |
| 930 | Ast.DisjRuleElem(res) -> |
| 931 | let make_match = make_match None guard in |
| 932 | let orop = if guard then ctl_or else ctl_seqor in |
| 933 | (* label used to be used here, but it is not use; label is only needed after |
| 934 | and within dots |
| 935 | ctl_and CTL.NONSTRICT (label_pred_maker label) *) |
| 936 | (List.fold_left orop CTL.False (List.map make_match res)) |
| 937 | | _ -> make_match label guard code |
| 938 | |
| 939 | (* --------------------------------------------------------------------- *) |
| 940 | (* control structures *) |
| 941 | |
| 942 | let end_control_structure fvs header body after_pred |
| 943 | after_checks no_after_checks (afvs,afresh,ainh,aft) after label guard = |
| 944 | (* aft indicates what is added after the whole if, which has to be added |
| 945 | to the endif node *) |
| 946 | let (aft_needed,after_branch) = |
| 947 | match aft with |
| 948 | Ast.CONTEXT(_,Ast.NOTHING) -> |
| 949 | (false,make_seq_after2 guard after_pred after) |
| 950 | | _ -> |
| 951 | let match_endif = |
| 952 | make_match label guard |
| 953 | (make_meta_rule_elem aft (afvs,afresh,ainh)) in |
| 954 | (true, |
| 955 | make_seq_after guard after_pred |
| 956 | (After(make_seq_after guard match_endif after))) in |
| 957 | let body = body after_branch in |
| 958 | let s = guard_to_strict guard in |
| 959 | (* the code *) |
| 960 | quantify guard fvs |
| 961 | (ctl_and s header |
| 962 | (opt_and guard |
| 963 | (match (after,aft_needed) with |
| 964 | (After _,_) (* pattern doesn't end here *) |
| 965 | | (_,true) (* + code added after *) -> after_checks |
| 966 | | _ -> no_after_checks) |
| 967 | (ctl_ax_absolute s body))) |
| 968 | |
| 969 | let ifthen ifheader branch ((afvs,_,_,_) as aft) after |
| 970 | quantified minus_quantified label llabel slabel recurse make_match guard = |
| 971 | (* "if (test) thn" becomes: |
| 972 | if(test) & AX((TrueBranch & AX thn) v FallThrough v After) |
| 973 | |
| 974 | "if (test) thn; after" becomes: |
| 975 | if(test) & AX((TrueBranch & AX thn) v FallThrough v (After & AXAX after)) |
| 976 | & EX After |
| 977 | *) |
| 978 | (* free variables *) |
| 979 | let (efvs,bfvs) = |
| 980 | match seq_fvs quantified |
| 981 | [Ast.get_fvs ifheader;Ast.get_fvs branch;afvs] with |
| 982 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) |
| 983 | | _ -> failwith "not possible" in |
| 984 | let new_quantified = Common.union_set bfvs quantified in |
| 985 | let (mefvs,mbfvs) = |
| 986 | match seq_fvs minus_quantified |
| 987 | [Ast.get_mfvs ifheader;Ast.get_mfvs branch;[]] with |
| 988 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) |
| 989 | | _ -> failwith "not possible" in |
| 990 | let new_mquantified = Common.union_set mbfvs minus_quantified in |
| 991 | (* if header *) |
| 992 | let if_header = quantify guard efvs (make_match ifheader) in |
| 993 | (* then branch and after *) |
| 994 | let lv = get_label_ctr() in |
| 995 | let used = ref false in |
| 996 | let true_branch = |
| 997 | (* no point to put a label on truepred etc; it is local to this construct |
| 998 | so it must have the same label *) |
| 999 | make_seq guard |
| 1000 | [truepred None; recurse branch Tail new_quantified new_mquantified |
| 1001 | (Some (lv,used)) llabel slabel guard] in |
| 1002 | let after_pred = aftpred None in |
| 1003 | let or_cases after_branch = |
| 1004 | ctl_or true_branch (ctl_or (fallpred None) after_branch) in |
| 1005 | let (if_header,wrapper) = |
| 1006 | if !used |
| 1007 | then |
| 1008 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in |
| 1009 | (ctl_and CTL.NONSTRICT(*???*) if_header label_pred, |
| 1010 | (function body -> quantify true [lv] body)) |
| 1011 | else (if_header,function x -> x) in |
| 1012 | wrapper |
| 1013 | (end_control_structure bfvs if_header or_cases after_pred |
| 1014 | (Some(ctl_ex after_pred)) None aft after label guard) |
| 1015 | |
| 1016 | let ifthenelse ifheader branch1 els branch2 ((afvs,_,_,_) as aft) after |
| 1017 | quantified minus_quantified label llabel slabel recurse make_match guard = |
| 1018 | (* "if (test) thn else els" becomes: |
| 1019 | if(test) & AX((TrueBranch & AX thn) v |
| 1020 | (FalseBranch & AX (else & AX els)) v After) |
| 1021 | & EX FalseBranch |
| 1022 | |
| 1023 | "if (test) thn else els; after" becomes: |
| 1024 | if(test) & AX((TrueBranch & AX thn) v |
| 1025 | (FalseBranch & AX (else & AX els)) v |
| 1026 | (After & AXAX after)) |
| 1027 | & EX FalseBranch |
| 1028 | & EX After |
| 1029 | *) |
| 1030 | (* free variables *) |
| 1031 | let (e1fvs,b1fvs,s1fvs) = |
| 1032 | match seq_fvs quantified |
| 1033 | [Ast.get_fvs ifheader;Ast.get_fvs branch1;afvs] with |
| 1034 | [(e1fvs,b1fvs);(s1fvs,b1afvs);_] -> |
| 1035 | (e1fvs,Common.union_set b1fvs b1afvs,s1fvs) |
| 1036 | | _ -> failwith "not possible" in |
| 1037 | let (e2fvs,b2fvs,s2fvs) = |
| 1038 | (* fvs on else? *) |
| 1039 | (* just combine with the else branch. no point to have separate |
| 1040 | quantifier, since there is only one possible control-flow path *) |
| 1041 | let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in |
| 1042 | match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with |
| 1043 | [(e2fvs,b2fvs);(s2fvs,b2afvs);_] -> |
| 1044 | (e2fvs,Common.union_set b2fvs b2afvs,s2fvs) |
| 1045 | | _ -> failwith "not possible" in |
| 1046 | let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in |
| 1047 | let exponlyfvs = intersect e1fvs e2fvs in |
| 1048 | let new_quantified = union bothfvs quantified in |
| 1049 | (* minus free variables *) |
| 1050 | let (me1fvs,mb1fvs,ms1fvs) = |
| 1051 | match seq_fvs minus_quantified |
| 1052 | [Ast.get_mfvs ifheader;Ast.get_mfvs branch1;[]] with |
| 1053 | [(e1fvs,b1fvs);(s1fvs,b1afvs);_] -> |
| 1054 | (e1fvs,Common.union_set b1fvs b1afvs,s1fvs) |
| 1055 | | _ -> failwith "not possible" in |
| 1056 | let (me2fvs,mb2fvs,ms2fvs) = |
| 1057 | (* fvs on else? *) |
| 1058 | (* just combine with the else branch. no point to have separate |
| 1059 | quantifier, since there is only one possible control-flow path *) |
| 1060 | let else_mfvs = |
| 1061 | Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in |
| 1062 | match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with |
| 1063 | [(e2fvs,b2fvs);(s2fvs,b2afvs);_] -> |
| 1064 | (e2fvs,Common.union_set b2fvs b2afvs,s2fvs) |
| 1065 | | _ -> failwith "not possible" in |
| 1066 | let mbothfvs = union (union mb1fvs mb2fvs) (intersect ms1fvs ms2fvs) in |
| 1067 | let new_mquantified = union mbothfvs minus_quantified in |
| 1068 | (* if header *) |
| 1069 | let if_header = quantify guard exponlyfvs (make_match ifheader) in |
| 1070 | (* then and else branches *) |
| 1071 | let lv = get_label_ctr() in |
| 1072 | let used = ref false in |
| 1073 | let true_branch = |
| 1074 | make_seq guard |
| 1075 | [truepred None; recurse branch1 Tail new_quantified new_mquantified |
| 1076 | (Some (lv,used)) llabel slabel guard] in |
| 1077 | let false_branch = |
| 1078 | make_seq guard |
| 1079 | [falsepred None; |
| 1080 | quantify guard |
| 1081 | (Common.minus_set (Ast.get_fvs els) new_quantified) |
| 1082 | (header_match None guard els); |
| 1083 | recurse branch2 Tail new_quantified new_mquantified |
| 1084 | (Some (lv,used)) llabel slabel guard] in |
| 1085 | let after_pred = aftpred None in |
| 1086 | let or_cases after_branch = |
| 1087 | ctl_or true_branch (ctl_or false_branch after_branch) in |
| 1088 | let s = guard_to_strict guard in |
| 1089 | let (if_header,wrapper) = |
| 1090 | if !used |
| 1091 | then |
| 1092 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in |
| 1093 | (ctl_and CTL.NONSTRICT(*???*) if_header label_pred, |
| 1094 | (function body -> quantify true [lv] body)) |
| 1095 | else (if_header,function x -> x) in |
| 1096 | wrapper |
| 1097 | (end_control_structure bothfvs if_header or_cases after_pred |
| 1098 | (Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred))) |
| 1099 | (Some(ctl_ex (falsepred None))) |
| 1100 | aft after label guard) |
| 1101 | |
| 1102 | let forwhile header body ((afvs,_,_,_) as aft) after |
| 1103 | quantified minus_quantified label recurse make_match guard = |
| 1104 | let process _ = |
| 1105 | (* the translation in this case is similar to that of an if with no else *) |
| 1106 | (* free variables *) |
| 1107 | let (efvs,bfvs) = |
| 1108 | match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body;afvs] with |
| 1109 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) |
| 1110 | | _ -> failwith "not possible" in |
| 1111 | let new_quantified = Common.union_set bfvs quantified in |
| 1112 | (* minus free variables *) |
| 1113 | let (mefvs,mbfvs) = |
| 1114 | match seq_fvs minus_quantified |
| 1115 | [Ast.get_mfvs header;Ast.get_mfvs body;[]] with |
| 1116 | [(efvs,b1fvs);(_,b2fvs);_] -> (efvs,Common.union_set b1fvs b2fvs) |
| 1117 | | _ -> failwith "not possible" in |
| 1118 | let new_mquantified = Common.union_set mbfvs minus_quantified in |
| 1119 | (* loop header *) |
| 1120 | let header = quantify guard efvs (make_match header) in |
| 1121 | let lv = get_label_ctr() in |
| 1122 | let used = ref false in |
| 1123 | let body = |
| 1124 | make_seq guard |
| 1125 | [inlooppred None; |
| 1126 | recurse body Tail new_quantified new_mquantified |
| 1127 | (Some (lv,used)) (Some (lv,used)) None guard] in |
| 1128 | let after_pred = loopfallpred None in |
| 1129 | let or_cases after_branch = ctl_or body after_branch in |
| 1130 | let (header,wrapper) = |
| 1131 | if !used |
| 1132 | then |
| 1133 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in |
| 1134 | (ctl_and CTL.NONSTRICT(*???*) header label_pred, |
| 1135 | (function body -> quantify true [lv] body)) |
| 1136 | else (header,function x -> x) in |
| 1137 | wrapper |
| 1138 | (end_control_structure bfvs header or_cases after_pred |
| 1139 | (Some(ctl_ex after_pred)) None aft after label guard) in |
| 1140 | match (Ast.unwrap body,aft) with |
| 1141 | (Ast.Atomic(re),(_,_,_,Ast.CONTEXT(_,Ast.NOTHING))) -> |
| 1142 | (match Ast.unwrap re with |
| 1143 | Ast.MetaStmt((_,_,Ast.CONTEXT(_,Ast.NOTHING),_), |
| 1144 | Type_cocci.Unitary,_,false) |
| 1145 | when after = Tail or after = End or after = VeryEnd -> |
| 1146 | let (efvs) = |
| 1147 | match seq_fvs quantified [Ast.get_fvs header] with |
| 1148 | [(efvs,_)] -> efvs |
| 1149 | | _ -> failwith "not possible" in |
| 1150 | quantify guard efvs (make_match header) |
| 1151 | | _ -> process()) |
| 1152 | | _ -> process() |
| 1153 | |
| 1154 | (* --------------------------------------------------------------------- *) |
| 1155 | (* statement metavariables *) |
| 1156 | |
| 1157 | (* issue: an S metavariable that is not an if branch/loop body |
| 1158 | should not match an if branch/loop body, so check that the labels |
| 1159 | of the nodes before the first node matched by the S are different |
| 1160 | from the label of the first node matched by the S *) |
| 1161 | let sequencibility body label_pred process_bef_aft = function |
| 1162 | Ast.Sequencible | Ast.SequencibleAfterDots [] -> |
| 1163 | body |
| 1164 | (function x -> |
| 1165 | (ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x)) |
| 1166 | | Ast.SequencibleAfterDots l -> |
| 1167 | (* S appears after some dots. l is the code that comes after the S. |
| 1168 | want to search for that first, because S can match anything, while |
| 1169 | the stuff after is probably more restricted *) |
| 1170 | let afts = List.map process_bef_aft l in |
| 1171 | let ors = foldl1 ctl_or afts in |
| 1172 | ctl_and CTL.NONSTRICT |
| 1173 | (ctl_ef (ctl_and CTL.NONSTRICT ors (ctl_back_ax label_pred))) |
| 1174 | (body |
| 1175 | (function x -> |
| 1176 | ctl_and CTL.NONSTRICT (ctl_not (ctl_back_ax label_pred)) x)) |
| 1177 | | Ast.NotSequencible -> body (function x -> x) |
| 1178 | |
| 1179 | let svar_context_with_add_after stmt s label quantified d ast |
| 1180 | seqible after process_bef_aft guard fvinfo = |
| 1181 | let label_var = (*fresh_label_var*) string2var "_lab" in |
| 1182 | let label_pred = |
| 1183 | CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in |
| 1184 | (*let prelabel_pred = |
| 1185 | CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in*) |
| 1186 | let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in |
| 1187 | let full_metamatch = matcher d in |
| 1188 | let first_metamatch = |
| 1189 | matcher |
| 1190 | (match d with |
| 1191 | Ast.CONTEXT(pos,Ast.BEFOREAFTER(bef,_,c)) -> |
| 1192 | Ast.CONTEXT(pos,Ast.BEFORE(bef,c)) |
| 1193 | | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING) |
| 1194 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
| 1195 | (* |
| 1196 | let middle_metamatch = |
| 1197 | matcher |
| 1198 | (match d with |
| 1199 | Ast.CONTEXT(pos,_) -> Ast.CONTEXT(pos,Ast.NOTHING) |
| 1200 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
| 1201 | *) |
| 1202 | let last_metamatch = |
| 1203 | matcher |
| 1204 | (match d with |
| 1205 | Ast.CONTEXT(pos,Ast.BEFOREAFTER(_,aft,c)) -> |
| 1206 | Ast.CONTEXT(pos,Ast.AFTER(aft,c)) |
| 1207 | | Ast.CONTEXT(_,_) -> d |
| 1208 | | Ast.MINUS(_,_,_,_) | Ast.PLUS _ -> failwith "not possible") in |
| 1209 | |
| 1210 | (* |
| 1211 | let rest_nodes = |
| 1212 | ctl_and CTL.NONSTRICT middle_metamatch prelabel_pred in |
| 1213 | *) |
| 1214 | |
| 1215 | let to_end = ctl_or (aftpred None) (loopfallpred None) in |
| 1216 | let left_or = (* the whole statement is one node *) |
| 1217 | make_seq_after guard |
| 1218 | (ctl_and CTL.NONSTRICT (ctl_not (ctl_ex to_end)) full_metamatch) after in |
| 1219 | let right_or = (* the statement covers multiple nodes *) |
| 1220 | ctl_and CTL.NONSTRICT |
| 1221 | (ctl_ex |
| 1222 | (make_seq guard |
| 1223 | [to_end; make_seq_after guard last_metamatch after])) |
| 1224 | first_metamatch in |
| 1225 | |
| 1226 | (* |
| 1227 | let left_or = |
| 1228 | make_seq guard |
| 1229 | [full_metamatch; and_after guard (ctl_not prelabel_pred) after] in |
| 1230 | let right_or = |
| 1231 | make_seq guard |
| 1232 | [first_metamatch; |
| 1233 | ctl_au CTL.NONSTRICT |
| 1234 | rest_nodes |
| 1235 | (make_seq guard |
| 1236 | [ctl_and CTL.NONSTRICT last_metamatch label_pred; |
| 1237 | and_after guard |
| 1238 | (ctl_not prelabel_pred) after])] in |
| 1239 | *) |
| 1240 | |
| 1241 | let body f = |
| 1242 | ctl_and CTL.NONSTRICT label_pred |
| 1243 | (f (ctl_and CTL.NONSTRICT |
| 1244 | (make_raw_match label false ast) (ctl_or left_or right_or))) in |
| 1245 | let stmt_fvs = Ast.get_fvs stmt in |
| 1246 | let fvs = get_unquantified quantified stmt_fvs in |
| 1247 | quantify guard (label_var::fvs) |
| 1248 | (sequencibility body label_pred process_bef_aft seqible) |
| 1249 | |
| 1250 | let svar_minus_or_no_add_after stmt s label quantified d ast |
| 1251 | seqible after process_bef_aft guard fvinfo = |
| 1252 | let label_var = (*fresh_label_var*) string2var "_lab" in |
| 1253 | let label_pred = |
| 1254 | CTL.Pred (Lib_engine.Label(label_var),CTL.Control) in |
| 1255 | let prelabel_pred = |
| 1256 | CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in |
| 1257 | let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in |
| 1258 | let ender = |
| 1259 | match (d,after) with |
| 1260 | (Ast.PLUS _, _) -> failwith "not possible" |
| 1261 | | (Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) -> |
| 1262 | (* just match the root. don't care about label; always ok *) |
| 1263 | make_raw_match None false ast |
| 1264 | | (Ast.CONTEXT(pos,Ast.BEFORE(_,_)),(Tail|End|VeryEnd)) -> |
| 1265 | ctl_and CTL.NONSTRICT |
| 1266 | (make_raw_match None false ast) (* statement *) |
| 1267 | (matcher d) (* transformation *) |
| 1268 | | (Ast.CONTEXT(pos,(Ast.NOTHING|Ast.BEFORE(_,_))),(After a | Guard a)) -> |
| 1269 | (* This case and the MINUS one couldprobably be merged, if |
| 1270 | HackForStmt were to notice when its arguments are trivial *) |
| 1271 | let first_metamatch = matcher d in |
| 1272 | (* try to follow after link *) |
| 1273 | let to_end = ctl_or (aftpred None) (loopfallpred None) in |
| 1274 | let is_compound = |
| 1275 | ctl_ex(make_seq guard [to_end; CTL.True; a]) in |
| 1276 | let not_compound = |
| 1277 | make_seq_after guard (ctl_not (ctl_ex to_end)) after in |
| 1278 | ctl_and CTL.NONSTRICT (make_raw_match label false ast) |
| 1279 | (ctl_and CTL.NONSTRICT |
| 1280 | first_metamatch (ctl_or is_compound not_compound)) |
| 1281 | | (Ast.CONTEXT(pos,(Ast.AFTER _|Ast.BEFOREAFTER _)),_) -> |
| 1282 | failwith "not possible" |
| 1283 | | (Ast.MINUS(pos,inst,adj,l),after) -> |
| 1284 | let (first_metamatch,last_metamatch,rest_metamatch) = |
| 1285 | match l with |
| 1286 | Ast.NOREPLACEMENT -> |
| 1287 | (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d) |
| 1288 | | _ -> (matcher d, |
| 1289 | matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)), |
| 1290 | ctl_and CTL.NONSTRICT |
| 1291 | (ctl_not (make_raw_match label false ast)) |
| 1292 | (matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)))) in |
| 1293 | (* try to follow after link *) |
| 1294 | let to_end = ctl_or (aftpred None) (loopfallpred None) in |
| 1295 | let is_compound = |
| 1296 | ctl_ex |
| 1297 | (make_seq guard |
| 1298 | [to_end; make_seq_after guard last_metamatch after]) in |
| 1299 | let not_compound = |
| 1300 | make_seq_after guard (ctl_not (ctl_ex to_end)) after in |
| 1301 | ctl_and CTL.NONSTRICT |
| 1302 | (ctl_and CTL.NONSTRICT (make_raw_match label false ast) |
| 1303 | (ctl_and CTL.NONSTRICT |
| 1304 | first_metamatch (ctl_or is_compound not_compound))) |
| 1305 | (* don't have to put anything before the beginning, so don't have to |
| 1306 | distinguish the first node. so don't have to bother about paths, |
| 1307 | just use the label. label ensures that found nodes match up with |
| 1308 | what they should because it is in the lhs of the andany. *) |
| 1309 | (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT, |
| 1310 | ctl_and CTL.NONSTRICT label_pred |
| 1311 | (make_raw_match label false ast), |
| 1312 | ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred)) |
| 1313 | in |
| 1314 | let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in |
| 1315 | let stmt_fvs = Ast.get_fvs stmt in |
| 1316 | let fvs = get_unquantified quantified stmt_fvs in |
| 1317 | quantify guard (label_var::fvs) |
| 1318 | (sequencibility body label_pred process_bef_aft seqible) |
| 1319 | |
| 1320 | (* --------------------------------------------------------------------- *) |
| 1321 | (* dots and nests *) |
| 1322 | |
| 1323 | let dots_au is_strict toend label s wrapcode n x seq_after y quantifier = |
| 1324 | let matchgoto = gotopred None in |
| 1325 | let matchbreak = |
| 1326 | make_match None false |
| 1327 | (wrapcode |
| 1328 | (Ast.Break(Ast.make_mcode "break",Ast.make_mcode ";"))) in |
| 1329 | let matchcontinue = |
| 1330 | make_match None false |
| 1331 | (wrapcode |
| 1332 | (Ast.Continue(Ast.make_mcode "continue",Ast.make_mcode ";"))) in |
| 1333 | let stop_early = |
| 1334 | if quantifier = Exists |
| 1335 | then Common.Left(CTL.False) |
| 1336 | else if toend |
| 1337 | then Common.Left(CTL.Or(aftpred label,exitpred label)) |
| 1338 | else if is_strict |
| 1339 | then Common.Left(aftpred label) |
| 1340 | else |
| 1341 | Common.Right |
| 1342 | (function vx -> function v -> |
| 1343 | (* vx is the contents of the nest, if any. we can only stop early |
| 1344 | if we find neither the ending code nor the nest contents in |
| 1345 | the if branch. not sure if this is a good idea. *) |
| 1346 | let lv = get_label_ctr() in |
| 1347 | let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in |
| 1348 | let preflabelpred = label_pred_maker (Some (lv,ref true)) in |
| 1349 | (*let is_paren = |
| 1350 | (* Rather a special case. But if the code afterwards is just |
| 1351 | a } then there is no point checking after a goto that it does |
| 1352 | not appear. *) |
| 1353 | (* this optimization doesn't work. probably depends on whether |
| 1354 | the destination of the break/goto is local or more global than |
| 1355 | the dots *) |
| 1356 | match seq_after with |
| 1357 | CTL.And(_,e1,e2) -> |
| 1358 | let is_paren = function |
| 1359 | CTL.Pred(Lib_engine.Paren _,_) -> true |
| 1360 | | _ -> false in |
| 1361 | is_paren e1 or is_paren e2 |
| 1362 | | _ -> false in *) |
| 1363 | ctl_or (aftpred label) |
| 1364 | (quantify false [lv] |
| 1365 | (ctl_and CTL.NONSTRICT |
| 1366 | (ctl_and CTL.NONSTRICT (truepred label) labelpred) |
| 1367 | (ctl_au CTL.NONSTRICT |
| 1368 | (ctl_and CTL.NONSTRICT (ctl_not v) |
| 1369 | (ctl_and CTL.NONSTRICT vx preflabelpred)) |
| 1370 | (ctl_and CTL.NONSTRICT preflabelpred |
| 1371 | (if !Flag_matcher.only_return_is_error_exit |
| 1372 | then |
| 1373 | (ctl_and CTL.NONSTRICT |
| 1374 | (retpred None) (ctl_not seq_after)) |
| 1375 | else |
| 1376 | (ctl_or |
| 1377 | (ctl_and CTL.NONSTRICT |
| 1378 | (ctl_or (retpred None) matchcontinue) |
| 1379 | (ctl_not seq_after)) |
| 1380 | (ctl_and CTL.NONSTRICT |
| 1381 | (ctl_or matchgoto matchbreak) |
| 1382 | ((*if is_paren |
| 1383 | (* an optim that failed see defn is_paren |
| 1384 | and tests/makes_a_loop *) |
| 1385 | then CTL.True |
| 1386 | else*) |
| 1387 | (ctl_ag s |
| 1388 | (ctl_not seq_after))))))))))) in |
| 1389 | let op = if quantifier = !exists then ctl_au else ctl_anti_au in |
| 1390 | let v = get_let_ctr() in |
| 1391 | op s x |
| 1392 | (match stop_early with |
| 1393 | Common.Left x1 -> ctl_or y x1 |
| 1394 | | Common.Right stop_early -> |
| 1395 | CTL.Let(v,y, |
| 1396 | ctl_or (CTL.Ref v) |
| 1397 | (ctl_and CTL.NONSTRICT (label_pred_maker label) |
| 1398 | (stop_early n (CTL.Ref v))))) |
| 1399 | |
| 1400 | let rec dots_and_nests plus nest whencodes bef aft dotcode after label |
| 1401 | process_bef_aft statement_list statement guard quantified wrapcode = |
| 1402 | let ctl_and_ns = ctl_and CTL.NONSTRICT in |
| 1403 | (* proces bef_aft *) |
| 1404 | let shortest l = |
| 1405 | List.fold_left ctl_or_fl CTL.False (List.map process_bef_aft l) in |
| 1406 | let bef_aft = (* to be negated *) |
| 1407 | try |
| 1408 | let _ = |
| 1409 | List.find |
| 1410 | (function Ast.WhenModifier(Ast.WhenAny) -> true | _ -> false) |
| 1411 | whencodes in |
| 1412 | CTL.False |
| 1413 | with Not_found -> shortest (Common.union_set bef aft) in |
| 1414 | let is_strict = |
| 1415 | List.exists |
| 1416 | (function Ast.WhenModifier(Ast.WhenStrict) -> true | _ -> false) |
| 1417 | whencodes in |
| 1418 | let check_quantifier quant other = |
| 1419 | if List.exists |
| 1420 | (function Ast.WhenModifier(x) -> x = quant | _ -> false) |
| 1421 | whencodes |
| 1422 | then |
| 1423 | if List.exists |
| 1424 | (function Ast.WhenModifier(x) -> x = other | _ -> false) |
| 1425 | whencodes |
| 1426 | then failwith "inconsistent annotation on dots" |
| 1427 | else true |
| 1428 | else false in |
| 1429 | let quantifier = |
| 1430 | if check_quantifier Ast.WhenExists Ast.WhenForall |
| 1431 | then Exists |
| 1432 | else |
| 1433 | if check_quantifier Ast.WhenForall Ast.WhenExists |
| 1434 | then Forall |
| 1435 | else !exists in |
| 1436 | (* the following is used when we find a goto, etc and consider accepting |
| 1437 | without finding the rest of the pattern *) |
| 1438 | let aft = shortest aft in |
| 1439 | (* process whencode *) |
| 1440 | let labelled = label_pred_maker label in |
| 1441 | let whencodes arg = |
| 1442 | let (poswhen,negwhen) = |
| 1443 | List.fold_left |
| 1444 | (function (poswhen,negwhen) -> |
| 1445 | function |
| 1446 | Ast.WhenNot whencodes -> |
| 1447 | (poswhen,ctl_or (statement_list whencodes) negwhen) |
| 1448 | | Ast.WhenAlways stm -> |
| 1449 | (ctl_and CTL.NONSTRICT (statement stm) poswhen,negwhen) |
| 1450 | | Ast.WhenModifier(_) -> (poswhen,negwhen) |
| 1451 | | Ast.WhenNotTrue(e) -> |
| 1452 | (poswhen, |
| 1453 | ctl_or (whencond_true e label guard quantified) negwhen) |
| 1454 | | Ast.WhenNotFalse(e) -> |
| 1455 | (poswhen, |
| 1456 | ctl_or (whencond_false e label guard quantified) negwhen)) |
| 1457 | (CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in |
| 1458 | (*bef_aft modifies arg so that inside of a nest can't cause the next |
| 1459 | to overshoot its boundaries, eg a() <...f()...> b() where f is |
| 1460 | a metavariable and the whole thing matches code in a loop; |
| 1461 | don't want f to match eg b(), allowing to go around the loop again*) |
| 1462 | let poswhen = ctl_and_ns arg poswhen in |
| 1463 | let negwhen = |
| 1464 | (* if !exists |
| 1465 | then*) |
| 1466 | (* add in After, because it's not part of the program *) |
| 1467 | ctl_or (aftpred label) negwhen |
| 1468 | (*else negwhen*) in |
| 1469 | ctl_and_ns poswhen (ctl_not negwhen) in |
| 1470 | (* process dot code, if any *) |
| 1471 | let dotcode = |
| 1472 | match (dotcode,guard) with |
| 1473 | (None,_) | (_,true) -> CTL.True |
| 1474 | | (Some dotcode,_) -> dotcode in |
| 1475 | (* process nest code, if any *) |
| 1476 | (* whencode goes in the negated part of the nest; if no nest, just goes |
| 1477 | on the "true" in between code *) |
| 1478 | let plus_var = if plus then get_label_ctr() else string2var "" in |
| 1479 | let plus_var2 = if plus then get_label_ctr() else string2var "" in |
| 1480 | let (ornest,just_nest) = |
| 1481 | (* just_nest is used when considering whether to stop early, to continue |
| 1482 | to collect nest information in the if branch *) |
| 1483 | match (nest,guard && not plus) with |
| 1484 | (None,_) | (_,true) -> (whencodes CTL.True,CTL.True) |
| 1485 | | (Some nest,false) -> |
| 1486 | let v = get_let_ctr() in |
| 1487 | let is_plus x = |
| 1488 | if plus |
| 1489 | then |
| 1490 | (* the idea is that BindGood is sort of a witness; a witness to |
| 1491 | having found the subterm in at least one place. If there is |
| 1492 | not a witness, then there is a risk that it will get thrown |
| 1493 | away, if it is merged with a node that has an empty |
| 1494 | environment. See tests/nestplus. But this all seems |
| 1495 | rather suspicious *) |
| 1496 | CTL.And(CTL.NONSTRICT,x, |
| 1497 | CTL.Exists(true,plus_var2, |
| 1498 | CTL.Pred(Lib_engine.BindGood(plus_var), |
| 1499 | CTL.Modif plus_var2))) |
| 1500 | else x in |
| 1501 | let body = |
| 1502 | CTL.Let(v,nest, |
| 1503 | CTL.Or(is_plus (CTL.Ref v), |
| 1504 | whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in |
| 1505 | (body,body) in |
| 1506 | let plus_modifier x = |
| 1507 | if plus |
| 1508 | then |
| 1509 | CTL.Exists |
| 1510 | (false,plus_var, |
| 1511 | (CTL.And |
| 1512 | (CTL.NONSTRICT,x, |
| 1513 | CTL.Not(CTL.Pred(Lib_engine.BindBad(plus_var),CTL.Control))))) |
| 1514 | else x in |
| 1515 | |
| 1516 | let ender = |
| 1517 | match after with |
| 1518 | (* label within dots is taken care of elsewhere. the next two lines |
| 1519 | put the label on the code following dots *) |
| 1520 | After f -> ctl_and (guard_to_strict guard) f labelled |
| 1521 | | Guard f -> |
| 1522 | (* actually, label should be None based on the only use of Guard... *) |
| 1523 | assert (label = None); |
| 1524 | ctl_and CTL.NONSTRICT (ctl_uncheck f) labelled |
| 1525 | | VeryEnd -> |
| 1526 | let exit = endpred label in |
| 1527 | let errorexit = exitpred label in |
| 1528 | ctl_or exit errorexit |
| 1529 | (* not at all sure what the next two mean... *) |
| 1530 | | End -> CTL.True |
| 1531 | | Tail -> |
| 1532 | (match label with |
| 1533 | Some (lv,used) -> used := true; |
| 1534 | ctl_or (CTL.Pred(Lib_engine.Label lv,CTL.Control)) |
| 1535 | (ctl_back_ex (ctl_or (retpred label) (gotopred label))) |
| 1536 | | None -> endpred label) |
| 1537 | (* was the following, but not clear why sgrep should allow |
| 1538 | incomplete patterns |
| 1539 | let exit = endpred label in |
| 1540 | let errorexit = exitpred label in |
| 1541 | if !exists |
| 1542 | then ctl_or exit errorexit (* end anywhere *) |
| 1543 | else exit (* end at the real end of the function *) *) in |
| 1544 | plus_modifier |
| 1545 | (dots_au is_strict ((after = Tail) or (after = VeryEnd)) |
| 1546 | label (guard_to_strict guard) wrapcode just_nest |
| 1547 | (ctl_and_ns dotcode |
| 1548 | (ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled)) |
| 1549 | aft ender quantifier) |
| 1550 | |
| 1551 | and get_whencond_exps e = |
| 1552 | match Ast.unwrap e with |
| 1553 | Ast.Exp e -> [e] |
| 1554 | | Ast.DisjRuleElem(res) -> |
| 1555 | List.fold_left Common.union_set [] (List.map get_whencond_exps res) |
| 1556 | | _ -> failwith "not possible" |
| 1557 | |
| 1558 | and make_whencond_headers e e1 label guard quantified = |
| 1559 | let fvs = Ast.get_fvs e in |
| 1560 | let header_pred h = |
| 1561 | quantify guard (get_unquantified quantified fvs) |
| 1562 | (make_match label guard h) in |
| 1563 | let if_header e1 = |
| 1564 | header_pred |
| 1565 | (Ast.rewrap e |
| 1566 | (Ast.IfHeader |
| 1567 | (Ast.make_mcode "if", |
| 1568 | Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in |
| 1569 | let while_header e1 = |
| 1570 | header_pred |
| 1571 | (Ast.rewrap e |
| 1572 | (Ast.WhileHeader |
| 1573 | (Ast.make_mcode "while", |
| 1574 | Ast.make_mcode "(",e1,Ast.make_mcode ")"))) in |
| 1575 | let for_header e1 = |
| 1576 | header_pred |
| 1577 | (Ast.rewrap e |
| 1578 | (Ast.ForHeader |
| 1579 | (Ast.make_mcode "for",Ast.make_mcode "(",None,Ast.make_mcode ";", |
| 1580 | Some e1,Ast.make_mcode ";",None,Ast.make_mcode ")"))) in |
| 1581 | let if_headers = |
| 1582 | List.fold_left ctl_or CTL.False (List.map if_header e1) in |
| 1583 | let while_headers = |
| 1584 | List.fold_left ctl_or CTL.False (List.map while_header e1) in |
| 1585 | let for_headers = |
| 1586 | List.fold_left ctl_or CTL.False (List.map for_header e1) in |
| 1587 | (if_headers, while_headers, for_headers) |
| 1588 | |
| 1589 | and whencond_true e label guard quantified = |
| 1590 | let e1 = get_whencond_exps e in |
| 1591 | let (if_headers, while_headers, for_headers) = |
| 1592 | make_whencond_headers e e1 label guard quantified in |
| 1593 | ctl_or |
| 1594 | (ctl_and CTL.NONSTRICT (truepred label) (ctl_back_ex if_headers)) |
| 1595 | (ctl_and CTL.NONSTRICT |
| 1596 | (inlooppred label) (ctl_back_ex (ctl_or while_headers for_headers))) |
| 1597 | |
| 1598 | and whencond_false e label guard quantified = |
| 1599 | let e1 = get_whencond_exps e in |
| 1600 | let (if_headers, while_headers, for_headers) = |
| 1601 | make_whencond_headers e e1 label guard quantified in |
| 1602 | (* if with else *) |
| 1603 | ctl_or (ctl_and CTL.NONSTRICT (falsepred label) (ctl_back_ex if_headers)) |
| 1604 | (* if without else *) |
| 1605 | (ctl_or (ctl_and CTL.NONSTRICT (fallpred label) (ctl_back_ex if_headers)) |
| 1606 | (* failure of loop test *) |
| 1607 | (ctl_and CTL.NONSTRICT (loopfallpred label) |
| 1608 | (ctl_or (ctl_back_ex while_headers) (ctl_back_ex for_headers)))) |
| 1609 | |
| 1610 | (* --------------------------------------------------------------------- *) |
| 1611 | (* the main translation loop *) |
| 1612 | |
| 1613 | let rec statement_list stmt_list after quantified minus_quantified |
| 1614 | label llabel slabel dots_before guard = |
| 1615 | let isdots x = |
| 1616 | (* include Disj to be on the safe side *) |
| 1617 | match Ast.unwrap x with |
| 1618 | Ast.Dots _ | Ast.Nest _ | Ast.Disj _ -> true | _ -> false in |
| 1619 | let compute_label l e db = if db or isdots e then l else None in |
| 1620 | match Ast.unwrap stmt_list with |
| 1621 | Ast.DOTS(x) -> |
| 1622 | let rec loop quantified minus_quantified dots_before label llabel slabel |
| 1623 | = function |
| 1624 | ([],_,_) -> (match after with After f -> f | _ -> CTL.True) |
| 1625 | | ([e],_,_) -> |
| 1626 | statement e after quantified minus_quantified |
| 1627 | (compute_label label e dots_before) |
| 1628 | llabel slabel guard |
| 1629 | | (e::sl,fv::fvs,mfv::mfvs) -> |
| 1630 | let shared = intersectll fv fvs in |
| 1631 | let unqshared = get_unquantified quantified shared in |
| 1632 | let new_quantified = Common.union_set unqshared quantified in |
| 1633 | let minus_shared = intersectll mfv mfvs in |
| 1634 | let munqshared = |
| 1635 | get_unquantified minus_quantified minus_shared in |
| 1636 | let new_mquantified = |
| 1637 | Common.union_set munqshared minus_quantified in |
| 1638 | quantify guard unqshared |
| 1639 | (statement e |
| 1640 | (After |
| 1641 | (let (label1,llabel1,slabel1) = |
| 1642 | match Ast.unwrap e with |
| 1643 | Ast.Atomic(re) -> |
| 1644 | (match Ast.unwrap re with |
| 1645 | Ast.Goto _ -> (None,None,None) |
| 1646 | | _ -> (label,llabel,slabel)) |
| 1647 | | _ -> (label,llabel,slabel) in |
| 1648 | loop new_quantified new_mquantified (isdots e) |
| 1649 | label1 llabel1 slabel1 |
| 1650 | (sl,fvs,mfvs))) |
| 1651 | new_quantified new_mquantified |
| 1652 | (compute_label label e dots_before) llabel slabel guard) |
| 1653 | | _ -> failwith "not possible" in |
| 1654 | loop quantified minus_quantified dots_before |
| 1655 | label llabel slabel |
| 1656 | (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x) |
| 1657 | | Ast.CIRCLES(x) -> failwith "not supported" |
| 1658 | | Ast.STARS(x) -> failwith "not supported" |
| 1659 | |
| 1660 | (* llabel is the label of the enclosing loop and slabel is the label of the |
| 1661 | enclosing switch *) |
| 1662 | and statement stmt after quantified minus_quantified |
| 1663 | label llabel slabel guard = |
| 1664 | let ctl_au = ctl_au CTL.NONSTRICT in |
| 1665 | let ctl_ax = ctl_ax CTL.NONSTRICT in |
| 1666 | let ctl_and = ctl_and CTL.NONSTRICT in |
| 1667 | let make_seq = make_seq guard in |
| 1668 | let make_seq_after = make_seq_after guard in |
| 1669 | let real_make_match = make_match in |
| 1670 | let make_match = header_match label guard in |
| 1671 | |
| 1672 | let dots_done = ref false in (* hack for dots cases we can easily handle *) |
| 1673 | |
| 1674 | let term = |
| 1675 | match Ast.unwrap stmt with |
| 1676 | Ast.Atomic(ast) -> |
| 1677 | (match Ast.unwrap ast with |
| 1678 | (* the following optimisation is not a good idea, because when S |
| 1679 | is alone, we would like it not to match a declaration. |
| 1680 | this makes more matching for things like when (...) S, but perhaps |
| 1681 | that matching is not so costly anyway *) |
| 1682 | (*Ast.MetaStmt(_,Type_cocci.Unitary,_,false) when guard -> CTL.True*) |
| 1683 | | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.BEFOREAFTER(_,_,_)) as d),_), |
| 1684 | keep,seqible,_) |
| 1685 | | Ast.MetaStmt((s,_,(Ast.CONTEXT(_,Ast.AFTER(_,_)) as d),_), |
| 1686 | keep,seqible,_)-> |
| 1687 | svar_context_with_add_after stmt s label quantified d ast seqible |
| 1688 | after |
| 1689 | (process_bef_aft quantified minus_quantified |
| 1690 | label llabel slabel true) |
| 1691 | guard |
| 1692 | (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt) |
| 1693 | |
| 1694 | | Ast.MetaStmt((s,_,d,_),keep,seqible,_) -> |
| 1695 | svar_minus_or_no_add_after stmt s label quantified d ast seqible |
| 1696 | after |
| 1697 | (process_bef_aft quantified minus_quantified |
| 1698 | label llabel slabel true) |
| 1699 | guard |
| 1700 | (Ast.get_fvs stmt, Ast.get_fresh stmt, Ast.get_inherited stmt) |
| 1701 | |
| 1702 | | _ -> |
| 1703 | let term = |
| 1704 | match Ast.unwrap ast with |
| 1705 | Ast.DisjRuleElem(res) -> |
| 1706 | do_re_matches label guard res quantified minus_quantified |
| 1707 | | Ast.Exp(_) | Ast.Ty(_) -> |
| 1708 | let stmt_fvs = Ast.get_fvs stmt in |
| 1709 | let fvs = get_unquantified quantified stmt_fvs in |
| 1710 | CTL.InnerAnd(quantify guard fvs (make_match ast)) |
| 1711 | | _ -> |
| 1712 | let stmt_fvs = Ast.get_fvs stmt in |
| 1713 | let fvs = get_unquantified quantified stmt_fvs in |
| 1714 | quantify guard fvs (make_match ast) in |
| 1715 | match Ast.unwrap ast with |
| 1716 | Ast.Break(brk,semi) -> |
| 1717 | (match (llabel,slabel) with |
| 1718 | (_,Some(lv,used)) -> (* use switch label if there is one *) |
| 1719 | ctl_and term (bclabel_pred_maker slabel) |
| 1720 | | _ -> ctl_and term (bclabel_pred_maker llabel)) |
| 1721 | | Ast.Continue(brk,semi) -> ctl_and term (bclabel_pred_maker llabel) |
| 1722 | | Ast.Return((_,info,retmc,pos),(_,_,semmc,_)) -> |
| 1723 | (* discard pattern that comes after return *) |
| 1724 | let normal_res = make_seq_after term after in |
| 1725 | (* the following code tries to propagate the modifications on |
| 1726 | return; to a close brace, in the case where the final return |
| 1727 | is absent *) |
| 1728 | let new_mc = |
| 1729 | match (retmc,semmc) with |
| 1730 | (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2)) |
| 1731 | when !Flag.sgrep_mode2 -> |
| 1732 | (* in sgrep mode, we can propagate the - *) |
| 1733 | let new_info = |
| 1734 | match (l1,l2) with |
| 1735 | (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) -> |
| 1736 | Ast.NOREPLACEMENT |
| 1737 | | _ -> |
| 1738 | failwith "no replacements allowed in sgrep mode" in |
| 1739 | Some (Ast.MINUS(Ast.NoPos,inst1,adj1,new_info)) |
| 1740 | | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) -> |
| 1741 | let change = |
| 1742 | match (l1,l2) with |
| 1743 | (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) -> |
| 1744 | Ast.NOTHING |
| 1745 | | (Ast.NOREPLACEMENT,Ast.REPLACEMENT(l,ct)) |
| 1746 | | (Ast.REPLACEMENT(l,ct),Ast.NOREPLACEMENT) -> |
| 1747 | Ast.BEFORE(l,ct) |
| 1748 | | (Ast.REPLACEMENT(l1,ct1),Ast.REPLACEMENT(l2,ct2)) -> |
| 1749 | Ast.BEFORE(l1@l2,Ast.lub_count ct1 ct2) in |
| 1750 | Some (Ast.CONTEXT(Ast.NoPos,change)) |
| 1751 | | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)), |
| 1752 | Ast.CONTEXT(_,Ast.AFTER(l2,c2))) -> |
| 1753 | Some |
| 1754 | (Ast.CONTEXT(Ast.NoPos, |
| 1755 | Ast.BEFORE(l1@l2,Ast.lub_count c1 c2))) |
| 1756 | | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING)) |
| 1757 | | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) -> |
| 1758 | Some retmc |
| 1759 | | (Ast.CONTEXT(_,Ast.NOTHING), |
| 1760 | Ast.CONTEXT(_,Ast.AFTER(l,c))) -> |
| 1761 | Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l,c))) |
| 1762 | | _ -> None in |
| 1763 | let ret = Ast.make_mcode "return" in |
| 1764 | let edots = |
| 1765 | Ast.rewrap ast (Ast.Edots(Ast.make_mcode "...",None)) in |
| 1766 | let semi = Ast.make_mcode ";" in |
| 1767 | let simple_return = |
| 1768 | make_match(Ast.rewrap ast (Ast.Return(ret,semi))) in |
| 1769 | let return_expr = |
| 1770 | make_match(Ast.rewrap ast (Ast.ReturnExpr(ret,edots,semi))) in |
| 1771 | (match new_mc with |
| 1772 | Some new_mc -> |
| 1773 | let exit = endpred None in |
| 1774 | let mod_rbrace = |
| 1775 | Ast.rewrap ast (Ast.SeqEnd (("}",info,new_mc,pos))) in |
| 1776 | let stripped_rbrace = |
| 1777 | Ast.rewrap ast (Ast.SeqEnd(Ast.make_mcode "}")) in |
| 1778 | ctl_or normal_res |
| 1779 | (ctl_and (make_match mod_rbrace) |
| 1780 | (ctl_and |
| 1781 | (ctl_back_ax |
| 1782 | (ctl_not |
| 1783 | (ctl_uncheck |
| 1784 | (ctl_or simple_return return_expr)))) |
| 1785 | (ctl_au |
| 1786 | (make_match stripped_rbrace) |
| 1787 | (* error exit not possible; it is in the middle |
| 1788 | of code, so a return is needed *) |
| 1789 | exit))) |
| 1790 | | _ -> |
| 1791 | (* some change in the middle of the return, so have to |
| 1792 | find an actual return *) |
| 1793 | normal_res) |
| 1794 | | _ -> |
| 1795 | (* should try to deal with the dots_bef_aft problem elsewhere, |
| 1796 | but don't have the courage... *) |
| 1797 | let term = |
| 1798 | if guard |
| 1799 | then term |
| 1800 | else |
| 1801 | do_between_dots stmt term End |
| 1802 | quantified minus_quantified label llabel slabel guard in |
| 1803 | dots_done := true; |
| 1804 | make_seq_after term after) |
| 1805 | | Ast.Seq(lbrace,body,rbrace) -> |
| 1806 | let (lbfvs,b1fvs,b2fvs,rbfvs) = |
| 1807 | match |
| 1808 | seq_fvs quantified |
| 1809 | [Ast.get_fvs lbrace;Ast.get_fvs body;Ast.get_fvs rbrace] |
| 1810 | with |
| 1811 | [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> (lbfvs,b1fvs,b2fvs,rbfvs) |
| 1812 | | _ -> failwith "not possible" in |
| 1813 | let (mlbfvs,mb1fvs,mb2fvs,mrbfvs) = |
| 1814 | match |
| 1815 | seq_fvs minus_quantified |
| 1816 | [Ast.get_mfvs lbrace;Ast.get_mfvs body;Ast.get_mfvs rbrace] |
| 1817 | with |
| 1818 | [(lbfvs,b1fvs);(_,b2fvs);(rbfvs,_)] -> |
| 1819 | (lbfvs,b1fvs,b2fvs,rbfvs) |
| 1820 | | _ -> failwith "not possible" in |
| 1821 | let pv = count_nested_braces stmt in |
| 1822 | let lv = get_label_ctr() in |
| 1823 | let paren_pred = CTL.Pred(Lib_engine.Paren pv,CTL.Control) in |
| 1824 | let label_pred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in |
| 1825 | let start_brace = |
| 1826 | ctl_and |
| 1827 | (quantify guard lbfvs (make_match lbrace)) |
| 1828 | (ctl_and paren_pred label_pred) in |
| 1829 | let empty_rbrace = |
| 1830 | match Ast.unwrap rbrace with |
| 1831 | Ast.SeqEnd((data,info,_,pos)) -> |
| 1832 | Ast.rewrap rbrace(Ast.SeqEnd(Ast.make_mcode data)) |
| 1833 | | _ -> failwith "unexpected close brace" in |
| 1834 | let end_brace = |
| 1835 | (* label is not needed; paren_pred is enough *) |
| 1836 | quantify guard rbfvs |
| 1837 | (ctl_au (make_match empty_rbrace) |
| 1838 | (ctl_and (real_make_match None guard rbrace) paren_pred)) in |
| 1839 | let new_quantified2 = |
| 1840 | Common.union_set b1fvs (Common.union_set b2fvs quantified) in |
| 1841 | let new_mquantified2 = |
| 1842 | Common.union_set mb1fvs (Common.union_set mb2fvs minus_quantified) in |
| 1843 | let pattern_as_given = |
| 1844 | let new_quantified2 = Common.union_set [pv] new_quantified2 in |
| 1845 | quantify true [pv;lv] |
| 1846 | (quantify guard b1fvs |
| 1847 | (make_seq |
| 1848 | [start_brace; |
| 1849 | (ctl_or |
| 1850 | (if !exists = Exists then CTL.False else (aftpred label)) |
| 1851 | (quantify guard b2fvs |
| 1852 | (statement_list body |
| 1853 | (After (make_seq_after end_brace after)) |
| 1854 | new_quantified2 new_mquantified2 |
| 1855 | (Some (lv,ref true)) |
| 1856 | llabel slabel false guard)))])) in |
| 1857 | let empty_body = |
| 1858 | match Ast.undots body with |
| 1859 | [body] -> |
| 1860 | (match Ast.unwrap body with |
| 1861 | Ast.Dots |
| 1862 | ((_,i,Ast.CONTEXT(_,Ast.NOTHING),_),[],_,_) -> |
| 1863 | (match Ast.unwrap rbrace with |
| 1864 | Ast.SeqEnd((_,_,Ast.CONTEXT(_,Ast.NOTHING),_)) |
| 1865 | when not (contains_pos rbrace) -> true |
| 1866 | | _ -> false) |
| 1867 | | _ -> false) |
| 1868 | | _ -> false in |
| 1869 | if empty_body && after = Tail |
| 1870 | (* for just a match of an if branch of the form { ... }, just |
| 1871 | match the first brace *) |
| 1872 | then quantify guard lbfvs (make_match lbrace) |
| 1873 | else if ends_in_return body |
| 1874 | then |
| 1875 | (* matching error handling code *) |
| 1876 | (* Cases: |
| 1877 | 1. The pattern as given |
| 1878 | 2. A goto, and then some close braces, and then the pattern as |
| 1879 | given, but without the braces (only possible if there are no |
| 1880 | decls, and open and close braces are unmodified) |
| 1881 | 3. Part of the pattern as given, then a goto, and then the rest |
| 1882 | of the pattern. For this case, we just check that all paths have |
| 1883 | a goto within the current braces. checking for a goto at every |
| 1884 | point in the pattern seems expensive and not worthwhile. *) |
| 1885 | let pattern2 = |
| 1886 | let body = preprocess_dots body in (* redo, to drop braces *) |
| 1887 | make_seq |
| 1888 | [gotopred label; |
| 1889 | ctl_au |
| 1890 | (make_match empty_rbrace) |
| 1891 | (ctl_ax (* skip the destination label *) |
| 1892 | (quantify guard b2fvs |
| 1893 | (statement_list body End |
| 1894 | new_quantified2 new_mquantified2 None llabel slabel |
| 1895 | true guard)))] in |
| 1896 | let pattern3 = |
| 1897 | let new_quantified2 = Common.union_set [pv] new_quantified2 in |
| 1898 | quantify true [pv;lv] |
| 1899 | (quantify guard b1fvs |
| 1900 | (make_seq |
| 1901 | [start_brace; |
| 1902 | ctl_and |
| 1903 | (CTL.AU (* want AF even for sgrep *) |
| 1904 | (CTL.FORWARD,CTL.STRICT, |
| 1905 | CTL.Pred(Lib_engine.PrefixLabel(lv),CTL.Control), |
| 1906 | ctl_and (* brace must be eventually after goto *) |
| 1907 | (gotopred (Some (lv,ref true))) |
| 1908 | (* want AF even for sgrep *) |
| 1909 | (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace)))) |
| 1910 | (quantify guard b2fvs |
| 1911 | (statement_list body Tail |
| 1912 | new_quantified2 new_mquantified2 |
| 1913 | None(*no label because past the goto*) |
| 1914 | llabel slabel false guard))])) in |
| 1915 | ctl_or pattern_as_given (ctl_or pattern2 pattern3) |
| 1916 | else pattern_as_given |
| 1917 | | Ast.IfThen(ifheader,branch,aft) -> |
| 1918 | ifthen ifheader branch aft after quantified minus_quantified |
| 1919 | label llabel slabel statement make_match guard |
| 1920 | |
| 1921 | | Ast.IfThenElse(ifheader,branch1,els,branch2,aft) -> |
| 1922 | ifthenelse ifheader branch1 els branch2 aft after quantified |
| 1923 | minus_quantified label llabel slabel statement make_match guard |
| 1924 | |
| 1925 | | Ast.While(header,body,aft) | Ast.For(header,body,aft) |
| 1926 | | Ast.Iterator(header,body,aft) -> |
| 1927 | forwhile header body aft after quantified minus_quantified |
| 1928 | label statement make_match guard |
| 1929 | |
| 1930 | | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *) |
| 1931 | (*ctl_and seems pointless, disjuncts see label too |
| 1932 | (label_pred_maker label)*) |
| 1933 | (List.fold_left ctl_seqor CTL.False |
| 1934 | (List.map |
| 1935 | (function sl -> |
| 1936 | statement_list sl after quantified minus_quantified label |
| 1937 | llabel slabel true guard) |
| 1938 | stmt_dots_list)) |
| 1939 | |
| 1940 | | Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) -> |
| 1941 | (* label in recursive call is None because label check is already |
| 1942 | wrapped around the corresponding code. not good enough, want to stay |
| 1943 | in a specific region, dots and nests will keep going *) |
| 1944 | |
| 1945 | let bfvs = |
| 1946 | match seq_fvs quantified [Ast.get_wcfvs whencode;Ast.get_fvs stmt_dots] |
| 1947 | with |
| 1948 | [(wcfvs,bothfvs);(bdfvs,_)] -> bothfvs |
| 1949 | | _ -> failwith "not possible" in |
| 1950 | |
| 1951 | (* no minus version because when code doesn't contain any minus code *) |
| 1952 | let new_quantified = Common.union_set bfvs quantified in |
| 1953 | |
| 1954 | let dot_code = |
| 1955 | match Ast.get_mcodekind starter with (*ender must have the same mcode*) |
| 1956 | Ast.MINUS(_,_,_,_) as d -> |
| 1957 | (* no need for the fresh metavar, but ... is a bit weird as a |
| 1958 | variable name *) |
| 1959 | Some(make_match (make_meta_rule_elem d ([],[],[]))) |
| 1960 | | _ -> None in |
| 1961 | |
| 1962 | quantify guard bfvs |
| 1963 | (let dots_pattern = |
| 1964 | statement_list stmt_dots (a2n after) new_quantified minus_quantified |
| 1965 | label(*None*) llabel slabel true guard in |
| 1966 | dots_and_nests multi |
| 1967 | (Some dots_pattern) whencode bef aft dot_code after label |
| 1968 | (process_bef_aft new_quantified minus_quantified |
| 1969 | label(*None*) llabel slabel true) |
| 1970 | (function x -> |
| 1971 | statement_list x Tail new_quantified minus_quantified label(*None*) |
| 1972 | llabel slabel true true) |
| 1973 | (function x -> |
| 1974 | statement x Tail new_quantified minus_quantified label(*None*) |
| 1975 | llabel slabel true) |
| 1976 | guard quantified |
| 1977 | (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))) |
| 1978 | |
| 1979 | | Ast.Dots((_,i,d,_),whencodes,bef,aft) -> |
| 1980 | let dot_code = |
| 1981 | match d with |
| 1982 | Ast.MINUS(_,_,_,_) -> |
| 1983 | (* no need for the fresh metavar, but ... is a bit weird as a |
| 1984 | variable name *) |
| 1985 | Some(make_match (make_meta_rule_elem d ([],[],[]))) |
| 1986 | | _ -> None in |
| 1987 | dots_and_nests false None whencodes bef aft dot_code after label |
| 1988 | (process_bef_aft quantified minus_quantified None llabel slabel true) |
| 1989 | (function x -> |
| 1990 | statement_list x Tail quantified minus_quantified |
| 1991 | None llabel slabel true true) |
| 1992 | (function x -> |
| 1993 | statement x Tail quantified minus_quantified None llabel slabel true) |
| 1994 | guard quantified |
| 1995 | (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)) |
| 1996 | |
| 1997 | | Ast.Switch(header,lb,decls,cases,rb) -> |
| 1998 | let rec intersect_all = function |
| 1999 | [] -> [] |
| 2000 | | [x] -> x |
| 2001 | | x::xs -> intersect x (intersect_all xs) in |
| 2002 | let rec intersect_all2 = function (* pairwise *) |
| 2003 | [] -> [] |
| 2004 | | x::xs -> |
| 2005 | let front = |
| 2006 | List.filter |
| 2007 | (function elem -> List.exists (List.mem elem) xs) |
| 2008 | x in |
| 2009 | Common.union_set front (intersect_all2 xs) in |
| 2010 | let rec union_all l = List.fold_left union [] l in |
| 2011 | (* start normal variables *) |
| 2012 | let header_fvs = Ast.get_fvs header in |
| 2013 | let lb_fvs = Ast.get_fvs lb in |
| 2014 | let decl_fvs = union_all (List.map Ast.get_fvs (Ast.undots decls)) in |
| 2015 | let case_fvs = List.map Ast.get_fvs cases in |
| 2016 | let rb_fvs = Ast.get_fvs rb in |
| 2017 | let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, |
| 2018 | all_casefvs,all_b3fvs,all_rbfvs) = |
| 2019 | List.fold_left |
| 2020 | (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, |
| 2021 | all_casefvs,all_b3fvs,all_rbfvs) -> |
| 2022 | function case_fvs -> |
| 2023 | match seq_fvs quantified [header_fvs;lb_fvs;case_fvs;rb_fvs] with |
| 2024 | [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] -> |
| 2025 | (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs, |
| 2026 | b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs, |
| 2027 | rbfvs::all_rbfvs) |
| 2028 | | _ -> failwith "not possible") |
| 2029 | ([],[],[],[],[],[],[]) (decl_fvs :: case_fvs) in |
| 2030 | let (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, |
| 2031 | all_casefvs,all_b3fvs,all_rbfvs) = |
| 2032 | (List.rev all_efvs,List.rev all_b1fvs,List.rev all_lbfvs, |
| 2033 | List.rev all_b2fvs,List.rev all_casefvs,List.rev all_b3fvs, |
| 2034 | List.rev all_rbfvs) in |
| 2035 | let exponlyfvs = intersect_all all_efvs in |
| 2036 | let lbonlyfvs = intersect_all all_lbfvs in |
| 2037 | (* don't do anything with right brace. Hope there is no + code on it *) |
| 2038 | (* let rbonlyfvs = intersect_all all_rbfvs in*) |
| 2039 | let b1fvs = union_all all_b1fvs in |
| 2040 | let new1_quantified = union b1fvs quantified in |
| 2041 | let b2fvs = |
| 2042 | union (union_all all_b2fvs) (intersect_all2 all_casefvs) in |
| 2043 | let new2_quantified = union b2fvs new1_quantified in |
| 2044 | (* let b3fvs = union_all all_b3fvs in*) |
| 2045 | (* ------------------- start minus free variables *) |
| 2046 | let header_mfvs = Ast.get_mfvs header in |
| 2047 | let lb_mfvs = Ast.get_mfvs lb in |
| 2048 | let decl_mfvs = union_all (List.map Ast.get_mfvs (Ast.undots decls)) in |
| 2049 | let case_mfvs = List.map Ast.get_mfvs cases in |
| 2050 | let rb_mfvs = Ast.get_mfvs rb in |
| 2051 | let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs, |
| 2052 | all_mcasefvs,all_mb3fvs,all_mrbfvs) = |
| 2053 | List.fold_left |
| 2054 | (function (all_efvs,all_b1fvs,all_lbfvs,all_b2fvs, |
| 2055 | all_casefvs,all_b3fvs,all_rbfvs) -> |
| 2056 | function case_mfvs -> |
| 2057 | match |
| 2058 | seq_fvs quantified |
| 2059 | [header_mfvs;lb_mfvs;case_mfvs;rb_mfvs] with |
| 2060 | [(efvs,b1fvs);(lbfvs,b2fvs);(casefvs,b3fvs);(rbfvs,_)] -> |
| 2061 | (efvs::all_efvs,b1fvs::all_b1fvs,lbfvs::all_lbfvs, |
| 2062 | b2fvs::all_b2fvs,casefvs::all_casefvs,b3fvs::all_b3fvs, |
| 2063 | rbfvs::all_rbfvs) |
| 2064 | | _ -> failwith "not possible") |
| 2065 | ([],[],[],[],[],[],[]) (decl_mfvs::case_mfvs) in |
| 2066 | let (all_mefvs,all_mb1fvs,all_mlbfvs,all_mb2fvs, |
| 2067 | all_mcasefvs,all_mb3fvs,all_mrbfvs) = |
| 2068 | (List.rev all_mefvs,List.rev all_mb1fvs,List.rev all_mlbfvs, |
| 2069 | List.rev all_mb2fvs,List.rev all_mcasefvs,List.rev all_mb3fvs, |
| 2070 | List.rev all_mrbfvs) in |
| 2071 | (* don't do anything with right brace. Hope there is no + code on it *) |
| 2072 | (* let rbonlyfvs = intersect_all all_rbfvs in*) |
| 2073 | let mb1fvs = union_all all_mb1fvs in |
| 2074 | let new1_mquantified = union mb1fvs quantified in |
| 2075 | let mb2fvs = |
| 2076 | union (union_all all_mb2fvs) (intersect_all2 all_mcasefvs) in |
| 2077 | let new2_mquantified = union mb2fvs new1_mquantified in |
| 2078 | (* let b3fvs = union_all all_b3fvs in*) |
| 2079 | (* ------------------- end collection of free variables *) |
| 2080 | let switch_header = quantify guard exponlyfvs (make_match header) in |
| 2081 | let lb = quantify guard lbonlyfvs (make_match lb) in |
| 2082 | (* let rb = quantify guard rbonlyfvs (make_match rb) in*) |
| 2083 | let case_headers = |
| 2084 | List.map |
| 2085 | (function case_line -> |
| 2086 | match Ast.unwrap case_line with |
| 2087 | Ast.CaseLine(header,body) -> |
| 2088 | let e1fvs = |
| 2089 | match seq_fvs new2_quantified [Ast.get_fvs header] with |
| 2090 | [(e1fvs,_)] -> e1fvs |
| 2091 | | _ -> failwith "not possible" in |
| 2092 | quantify guard e1fvs (real_make_match label true header) |
| 2093 | | Ast.OptCase(case_line) -> failwith "not supported") |
| 2094 | cases in |
| 2095 | let lv = get_label_ctr() in |
| 2096 | let used = ref false in |
| 2097 | let (decls_exists_code,decls_all_code) = |
| 2098 | (*don't really understand this*) |
| 2099 | if (Ast.undots decls) = [] |
| 2100 | then (CTL.True,CTL.False) |
| 2101 | else |
| 2102 | let res = |
| 2103 | statement_list decls Tail |
| 2104 | new2_quantified new2_mquantified (Some (lv,used)) llabel None |
| 2105 | false(*?*) guard in |
| 2106 | (res,res) in |
| 2107 | let no_header = |
| 2108 | ctl_not |
| 2109 | (List.fold_left ctl_or_fl CTL.False |
| 2110 | (List.map ctl_uncheck |
| 2111 | (decls_all_code::case_headers))) in |
| 2112 | let case_code = |
| 2113 | List.map |
| 2114 | (function case_line -> |
| 2115 | match Ast.unwrap case_line with |
| 2116 | Ast.CaseLine(header,body) -> |
| 2117 | let (e1fvs,b1fvs,s1fvs) = |
| 2118 | let fvs = [Ast.get_fvs header;Ast.get_fvs body] in |
| 2119 | match seq_fvs new2_quantified fvs with |
| 2120 | [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs) |
| 2121 | | _ -> failwith "not possible" in |
| 2122 | let (me1fvs,mb1fvs,ms1fvs) = |
| 2123 | let fvs = [Ast.get_mfvs header;Ast.get_mfvs body] in |
| 2124 | match seq_fvs new2_mquantified fvs with |
| 2125 | [(e1fvs,b1fvs);(s1fvs,_)] -> (e1fvs,b1fvs,s1fvs) |
| 2126 | | _ -> failwith "not possible" in |
| 2127 | let case_header = |
| 2128 | quantify guard e1fvs (make_match header) in |
| 2129 | let new3_quantified = union b1fvs new2_quantified in |
| 2130 | let new3_mquantified = union mb1fvs new2_mquantified in |
| 2131 | let body = |
| 2132 | statement_list body Tail |
| 2133 | new3_quantified new3_mquantified (Some (lv,used)) llabel |
| 2134 | (Some (lv,used)) false(*?*) guard in |
| 2135 | quantify guard b1fvs (make_seq [case_header; body]) |
| 2136 | | Ast.OptCase(case_line) -> failwith "not supported") |
| 2137 | cases in |
| 2138 | let default_required = |
| 2139 | if List.exists |
| 2140 | (function case -> |
| 2141 | match Ast.unwrap case with |
| 2142 | Ast.CaseLine(header,_) -> |
| 2143 | (match Ast.unwrap header with |
| 2144 | Ast.Default(_,_) -> true |
| 2145 | | _ -> false) |
| 2146 | | _ -> false) |
| 2147 | cases |
| 2148 | then function x -> x |
| 2149 | else function x -> ctl_or (fallpred label) x in |
| 2150 | let after_pred = aftpred label in |
| 2151 | let body after_branch = |
| 2152 | ctl_or |
| 2153 | (default_required |
| 2154 | (quantify guard b2fvs |
| 2155 | (make_seq |
| 2156 | [ctl_and lb |
| 2157 | (List.fold_left ctl_and CTL.True |
| 2158 | (List.map ctl_ex |
| 2159 | (decls_exists_code :: case_headers))); |
| 2160 | List.fold_left ctl_or_fl no_header |
| 2161 | (decls_all_code :: case_code)]))) |
| 2162 | after_branch in |
| 2163 | let aft = |
| 2164 | (rb_fvs,Ast.get_fresh rb,Ast.get_inherited rb, |
| 2165 | match Ast.unwrap rb with |
| 2166 | Ast.SeqEnd(rb) -> Ast.get_mcodekind rb |
| 2167 | | _ -> failwith "not possible") in |
| 2168 | let (switch_header,wrapper) = |
| 2169 | if !used |
| 2170 | then |
| 2171 | let label_pred = CTL.Pred (Lib_engine.Label(lv),CTL.Control) in |
| 2172 | (ctl_and switch_header label_pred, |
| 2173 | (function body -> quantify true [lv] body)) |
| 2174 | else (switch_header,function x -> x) in |
| 2175 | wrapper |
| 2176 | (end_control_structure b1fvs switch_header body |
| 2177 | after_pred (Some(ctl_ex after_pred)) None aft after label guard) |
| 2178 | | Ast.FunDecl(header,lbrace,body,rbrace) -> |
| 2179 | let (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) = |
| 2180 | match |
| 2181 | seq_fvs quantified |
| 2182 | [Ast.get_fvs header;Ast.get_fvs lbrace; |
| 2183 | Ast.get_fvs body;Ast.get_fvs rbrace] |
| 2184 | with |
| 2185 | [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] -> |
| 2186 | (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) |
| 2187 | | _ -> failwith "not possible" in |
| 2188 | let (mhfvs,mb1fvs,mlbfvs,mb2fvs,mb3fvs,mrbfvs) = |
| 2189 | match |
| 2190 | seq_fvs quantified |
| 2191 | [Ast.get_mfvs header;Ast.get_mfvs lbrace; |
| 2192 | Ast.get_mfvs body;Ast.get_mfvs rbrace] |
| 2193 | with |
| 2194 | [(hfvs,b1fvs);(lbfvs,b2fvs);(_,b3fvs);(rbfvs,_)] -> |
| 2195 | (hfvs,b1fvs,lbfvs,b2fvs,b3fvs,rbfvs) |
| 2196 | | _ -> failwith "not possible" in |
| 2197 | let function_header = quantify guard hfvs (make_match header) in |
| 2198 | let start_brace = quantify guard lbfvs (make_match lbrace) in |
| 2199 | let stripped_rbrace = |
| 2200 | match Ast.unwrap rbrace with |
| 2201 | Ast.SeqEnd((data,info,_,_)) -> |
| 2202 | Ast.rewrap rbrace(Ast.SeqEnd (Ast.make_mcode data)) |
| 2203 | | _ -> failwith "unexpected close brace" in |
| 2204 | let end_brace = |
| 2205 | let exit = CTL.Pred (Lib_engine.Exit,CTL.Control) in |
| 2206 | let errorexit = CTL.Pred (Lib_engine.ErrorExit,CTL.Control) in |
| 2207 | let fake_brace = CTL.Pred (Lib_engine.FakeBrace,CTL.Control) in |
| 2208 | ctl_and |
| 2209 | (quantify guard rbfvs (make_match rbrace)) |
| 2210 | (ctl_and |
| 2211 | (* the following finds the beginning of the fake braces, |
| 2212 | if there are any, not completely sure how this works. |
| 2213 | sse the examples sw and return *) |
| 2214 | (ctl_back_ex (ctl_not fake_brace)) |
| 2215 | (ctl_au (make_match stripped_rbrace) (ctl_or exit errorexit))) in |
| 2216 | let new_quantified3 = |
| 2217 | Common.union_set b1fvs |
| 2218 | (Common.union_set b2fvs (Common.union_set b3fvs quantified)) in |
| 2219 | let new_mquantified3 = |
| 2220 | Common.union_set mb1fvs |
| 2221 | (Common.union_set mb2fvs |
| 2222 | (Common.union_set mb3fvs minus_quantified)) in |
| 2223 | let not_minus = function Ast.MINUS(_,_,_,_) -> false | _ -> true in |
| 2224 | let optim1 = |
| 2225 | match (Ast.undots body, |
| 2226 | contains_modif rbrace or contains_pos rbrace) with |
| 2227 | ([body],false) -> |
| 2228 | (match Ast.unwrap body with |
| 2229 | Ast.Nest(starter,stmt_dots,ender,[],false,_,_) |
| 2230 | (* perhaps could optimize for minus case too... TODO *) |
| 2231 | when not_minus (Ast.get_mcodekind starter) |
| 2232 | -> |
| 2233 | (* special case for function header + body - header is unambiguous |
| 2234 | and unique, so we can just look for the nested body anywhere |
| 2235 | else in the CFG *) |
| 2236 | Some |
| 2237 | (CTL.AndAny |
| 2238 | (CTL.FORWARD,guard_to_strict guard,start_brace, |
| 2239 | statement_list stmt_dots |
| 2240 | (* discards match on right brace, but don't need it *) |
| 2241 | (Guard (make_seq_after end_brace after)) |
| 2242 | new_quantified3 new_mquantified3 |
| 2243 | None llabel slabel true guard)) |
| 2244 | | Ast.Dots((_,i,d,_),whencode,_,_) when |
| 2245 | (List.for_all |
| 2246 | (* flow sensitive, so not optimizable *) |
| 2247 | (function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) -> |
| 2248 | false |
| 2249 | | _ -> true) whencode) -> |
| 2250 | (* try to be more efficient for the case where the body is just |
| 2251 | ... Perhaps this is too much of a special case, but useful |
| 2252 | for dropping a parameter and checking that it is never used. *) |
| 2253 | (match d with |
| 2254 | Ast.MINUS(_,_,_,_) -> None |
| 2255 | | _ -> |
| 2256 | let pv = |
| 2257 | (* no nested braces, because only dots *) |
| 2258 | string2var ("p1") in |
| 2259 | let paren_pred = |
| 2260 | CTL.Pred(Lib_engine.Paren pv,CTL.Control) in |
| 2261 | Some ( |
| 2262 | make_seq |
| 2263 | [ctl_and start_brace paren_pred; |
| 2264 | match whencode with |
| 2265 | [] -> CTL.True |
| 2266 | | _ -> |
| 2267 | let leftarg = |
| 2268 | ctl_and |
| 2269 | (ctl_not |
| 2270 | (List.fold_left |
| 2271 | (function prev -> |
| 2272 | function |
| 2273 | Ast.WhenAlways(s) -> prev |
| 2274 | | Ast.WhenNot(sl) -> |
| 2275 | let x = |
| 2276 | statement_list sl Tail |
| 2277 | new_quantified3 |
| 2278 | new_mquantified3 |
| 2279 | label llabel slabel |
| 2280 | true true in |
| 2281 | ctl_or prev x |
| 2282 | | Ast.WhenNotTrue(_) |
| 2283 | | Ast.WhenNotFalse(_) -> |
| 2284 | failwith "unexpected" |
| 2285 | | Ast.WhenModifier |
| 2286 | (Ast.WhenAny) -> CTL.False |
| 2287 | | Ast.WhenModifier(_) -> prev) |
| 2288 | CTL.False whencode)) |
| 2289 | (List.fold_left |
| 2290 | (function prev -> |
| 2291 | function |
| 2292 | Ast.WhenAlways(s) -> |
| 2293 | let x = |
| 2294 | statement s Tail |
| 2295 | new_quantified3 |
| 2296 | new_mquantified3 |
| 2297 | label llabel slabel true in |
| 2298 | ctl_and prev x |
| 2299 | | Ast.WhenNot(sl) -> prev |
| 2300 | | Ast.WhenNotTrue(_) |
| 2301 | | Ast.WhenNotFalse(_) -> |
| 2302 | failwith "unexpected" |
| 2303 | | Ast.WhenModifier(Ast.WhenAny) -> |
| 2304 | CTL.True |
| 2305 | | Ast.WhenModifier(_) -> prev) |
| 2306 | CTL.True whencode) in |
| 2307 | ctl_au leftarg |
| 2308 | (ctl_and |
| 2309 | (make_match stripped_rbrace) |
| 2310 | paren_pred)])) |
| 2311 | | _ -> None) |
| 2312 | | _ -> None in |
| 2313 | let optim2 = |
| 2314 | (* function body is all minus, no whencode *) |
| 2315 | match Ast.undots body with |
| 2316 | [body] -> |
| 2317 | (match Ast.unwrap body with |
| 2318 | Ast.Dots |
| 2319 | ((_,i,(Ast.MINUS(_,_,_,Ast.NOREPLACEMENT) as d),_),[],_,_) -> |
| 2320 | (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with |
| 2321 | (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)), |
| 2322 | Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_))) |
| 2323 | when not (contains_pos rbrace) -> |
| 2324 | Some |
| 2325 | (* andany drops everything to the end, including close |
| 2326 | braces - not just function body, could check |
| 2327 | label to keep braces *) |
| 2328 | (ctl_and start_brace |
| 2329 | (ctl_ax |
| 2330 | (CTL.AndAny |
| 2331 | (CTL.FORWARD,guard_to_strict guard,CTL.True, |
| 2332 | make_match |
| 2333 | (make_meta_rule_elem d ([],[],[])))))) |
| 2334 | | _ -> None) |
| 2335 | | _ -> None) |
| 2336 | | _ -> None in |
| 2337 | let body_code = |
| 2338 | match (optim1,optim2) with |
| 2339 | (Some o1,_) -> o1 |
| 2340 | | (_,Some o2) -> o2 |
| 2341 | | _ -> |
| 2342 | make_seq |
| 2343 | [start_brace; |
| 2344 | quantify guard b3fvs |
| 2345 | (statement_list body |
| 2346 | (After (make_seq_after end_brace after)) |
| 2347 | new_quantified3 new_mquantified3 None llabel slabel |
| 2348 | false guard)] in |
| 2349 | quantify guard b1fvs |
| 2350 | (make_seq [function_header; quantify guard b2fvs body_code]) |
| 2351 | | Ast.Define(header,body) -> |
| 2352 | let (hfvs,bfvs,bodyfvs) = |
| 2353 | match seq_fvs quantified [Ast.get_fvs header;Ast.get_fvs body] |
| 2354 | with |
| 2355 | [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs) |
| 2356 | | _ -> failwith "not possible" in |
| 2357 | let (mhfvs,mbfvs,mbodyfvs) = |
| 2358 | match seq_fvs minus_quantified [Ast.get_mfvs header;Ast.get_mfvs body] |
| 2359 | with |
| 2360 | [(hfvs,b1fvs);(bodyfvs,_)] -> (hfvs,b1fvs,bodyfvs) |
| 2361 | | _ -> failwith "not possible" in |
| 2362 | let define_header = quantify guard hfvs (make_match header) in |
| 2363 | let body_code = |
| 2364 | statement_list body after |
| 2365 | (Common.union_set bfvs quantified) |
| 2366 | (Common.union_set mbfvs minus_quantified) |
| 2367 | None llabel slabel true guard in |
| 2368 | quantify guard bfvs (make_seq [define_header; body_code]) |
| 2369 | | Ast.OptStm(stm) -> |
| 2370 | failwith "OptStm should have been compiled away\n" |
| 2371 | | Ast.UniqueStm(stm) -> failwith "arities not yet supported" |
| 2372 | | _ -> failwith "not supported" in |
| 2373 | if guard or !dots_done |
| 2374 | then term |
| 2375 | else |
| 2376 | do_between_dots stmt term after quantified minus_quantified |
| 2377 | label llabel slabel guard |
| 2378 | |
| 2379 | (* term is the translation of stmt *) |
| 2380 | and do_between_dots stmt term after quantified minus_quantified |
| 2381 | label llabel slabel guard = |
| 2382 | match Ast.get_dots_bef_aft stmt with |
| 2383 | Ast.AddingBetweenDots (brace_term,n) |
| 2384 | | Ast.DroppingBetweenDots (brace_term,n) -> |
| 2385 | let match_brace = |
| 2386 | statement brace_term after quantified minus_quantified |
| 2387 | label llabel slabel guard in |
| 2388 | let v = Printf.sprintf "_r_%d" n in |
| 2389 | let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in |
| 2390 | let case2 = ctl_and CTL.NONSTRICT (ctl_not (CTL.Ref v)) term in |
| 2391 | CTL.Let |
| 2392 | (v,ctl_or |
| 2393 | (ctl_back_ex (ctl_or (truepred label) (inlooppred label))) |
| 2394 | (ctl_back_ex (ctl_back_ex (falsepred label))), |
| 2395 | ctl_or case1 case2) |
| 2396 | | Ast.NoDots -> term |
| 2397 | |
| 2398 | (* un_process_bef_aft is because we don't want to do transformation in this |
| 2399 | code, and thus don't case about braces before or after it *) |
| 2400 | and process_bef_aft quantified minus_quantified label llabel slabel guard = |
| 2401 | function |
| 2402 | Ast.WParen (re,n) -> |
| 2403 | let paren_pred = CTL.Pred (Lib_engine.Paren n,CTL.Control) in |
| 2404 | let s = guard_to_strict guard in |
| 2405 | quantify true (get_unquantified quantified [n]) |
| 2406 | (ctl_and s (make_raw_match None guard re) paren_pred) |
| 2407 | | Ast.Other s -> |
| 2408 | statement s Tail quantified minus_quantified label llabel slabel guard |
| 2409 | | Ast.Other_dots d -> |
| 2410 | statement_list d Tail quantified minus_quantified |
| 2411 | label llabel slabel true guard |
| 2412 | |
| 2413 | (* --------------------------------------------------------------------- *) |
| 2414 | (* cleanup: convert AX to EX for pdots. |
| 2415 | Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...]) |
| 2416 | This is what we wanted in the first place, but it wasn't possible to make |
| 2417 | because the AX and its argument are not created in the same place. |
| 2418 | Rather clunky... *) |
| 2419 | (* also cleanup XX, which is a marker for the case where the programmer |
| 2420 | specifies to change the quantifier on .... Assumed to only occur after one AX |
| 2421 | or EX, or at top level. *) |
| 2422 | |
| 2423 | let rec cleanup c = |
| 2424 | let c = match c with CTL.XX(c) -> c | _ -> c in |
| 2425 | match c with |
| 2426 | CTL.False -> CTL.False |
| 2427 | | CTL.True -> CTL.True |
| 2428 | | CTL.Pred(p) -> CTL.Pred(p) |
| 2429 | | CTL.Not(phi) -> CTL.Not(cleanup phi) |
| 2430 | | CTL.Exists(keep,v,phi) -> CTL.Exists(keep,v,cleanup phi) |
| 2431 | | CTL.AndAny(dir,s,phi1,phi2) -> |
| 2432 | CTL.AndAny(dir,s,cleanup phi1,cleanup phi2) |
| 2433 | | CTL.HackForStmt(dir,s,phi1,phi2) -> |
| 2434 | CTL.HackForStmt(dir,s,cleanup phi1,cleanup phi2) |
| 2435 | | CTL.And(s,phi1,phi2) -> CTL.And(s,cleanup phi1,cleanup phi2) |
| 2436 | | CTL.Or(phi1,phi2) -> CTL.Or(cleanup phi1,cleanup phi2) |
| 2437 | | CTL.SeqOr(phi1,phi2) -> CTL.SeqOr(cleanup phi1,cleanup phi2) |
| 2438 | | CTL.Implies(phi1,phi2) -> CTL.Implies(cleanup phi1,cleanup phi2) |
| 2439 | | CTL.AF(dir,s,phi1) -> CTL.AF(dir,s,cleanup phi1) |
| 2440 | | CTL.AX(CTL.FORWARD,s, |
| 2441 | CTL.Let(v1,e1, |
| 2442 | CTL.And(CTL.NONSTRICT,CTL.AU(CTL.FORWARD,s2,e2,e3), |
| 2443 | CTL.EU(CTL.FORWARD,e4,e5)))) -> |
| 2444 | CTL.Let(v1,e1, |
| 2445 | CTL.And(CTL.NONSTRICT, |
| 2446 | CTL.AX(CTL.FORWARD,s,CTL.AU(CTL.FORWARD,s2,e2,e3)), |
| 2447 | CTL.EX(CTL.FORWARD,CTL.EU(CTL.FORWARD,e4,e5)))) |
| 2448 | | CTL.AX(dir,s,CTL.XX(phi)) -> CTL.EX(dir,cleanup phi) |
| 2449 | | CTL.EX(dir,CTL.XX((CTL.AU(_,s,_,_)) as phi)) -> |
| 2450 | CTL.AX(dir,s,cleanup phi) |
| 2451 | | CTL.XX(phi) -> failwith "bad XX" |
| 2452 | | CTL.AX(dir,s,phi1) -> CTL.AX(dir,s,cleanup phi1) |
| 2453 | | CTL.AG(dir,s,phi1) -> CTL.AG(dir,s,cleanup phi1) |
| 2454 | | CTL.EF(dir,phi1) -> CTL.EF(dir,cleanup phi1) |
| 2455 | | CTL.EX(dir,phi1) -> CTL.EX(dir,cleanup phi1) |
| 2456 | | CTL.EG(dir,phi1) -> CTL.EG(dir,cleanup phi1) |
| 2457 | | CTL.AW(dir,s,phi1,phi2) -> CTL.AW(dir,s,cleanup phi1,cleanup phi2) |
| 2458 | | CTL.AU(dir,s,phi1,phi2) -> CTL.AU(dir,s,cleanup phi1,cleanup phi2) |
| 2459 | | CTL.EU(dir,phi1,phi2) -> CTL.EU(dir,cleanup phi1,cleanup phi2) |
| 2460 | | CTL.Let (x,phi1,phi2) -> CTL.Let (x,cleanup phi1,cleanup phi2) |
| 2461 | | CTL.LetR (dir,x,phi1,phi2) -> CTL.LetR (dir,x,cleanup phi1,cleanup phi2) |
| 2462 | | CTL.Ref(s) -> CTL.Ref(s) |
| 2463 | | CTL.Uncheck(phi1) -> CTL.Uncheck(cleanup phi1) |
| 2464 | | CTL.InnerAnd(phi1) -> CTL.InnerAnd(cleanup phi1) |
| 2465 | |
| 2466 | (* --------------------------------------------------------------------- *) |
| 2467 | (* Function declaration *) |
| 2468 | |
| 2469 | (* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *) |
| 2470 | |
| 2471 | let top_level name ((ua,pos),fua) (fuas,t) = |
| 2472 | let ua = List.filter (function (nm,_) -> nm = name) ua in |
| 2473 | used_after := ua; |
| 2474 | saved := Ast.get_saved t; |
| 2475 | let quantified = Common.minus_set (Common.union_set ua fuas) pos in |
| 2476 | let (wrap,formula) = |
| 2477 | match Ast.unwrap t with |
| 2478 | Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo" |
| 2479 | | Ast.NONDECL(stmt) -> |
| 2480 | let unopt = elim_opt.V.rebuilder_statement stmt in |
| 2481 | let unopt = preprocess_dots_e unopt in |
| 2482 | let formula = |
| 2483 | cleanup(statement unopt VeryEnd quantified [] None None None false) in |
| 2484 | ((function x -> NONDECL x), formula) |
| 2485 | | Ast.CODE(stmt_dots) -> |
| 2486 | let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in |
| 2487 | let unopt = preprocess_dots unopt in |
| 2488 | let starts_with_dots = |
| 2489 | match Ast.undots stmt_dots with |
| 2490 | d::ds -> |
| 2491 | (match Ast.unwrap d with |
| 2492 | Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_) |
| 2493 | | Ast.Stars(_,_,_,_) -> true |
| 2494 | | _ -> false) |
| 2495 | | _ -> false in |
| 2496 | let starts_with_brace = |
| 2497 | match Ast.undots stmt_dots with |
| 2498 | d::ds -> |
| 2499 | (match Ast.unwrap d with |
| 2500 | Ast.Seq(_) -> true |
| 2501 | | _ -> false) |
| 2502 | | _ -> false in |
| 2503 | let res = |
| 2504 | statement_list unopt VeryEnd quantified [] None None None |
| 2505 | false false in |
| 2506 | let formula = |
| 2507 | cleanup |
| 2508 | (if starts_with_dots |
| 2509 | then |
| 2510 | (* EX because there is a loop on enter/top *) |
| 2511 | ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res) |
| 2512 | else if starts_with_brace |
| 2513 | then |
| 2514 | ctl_and CTL.NONSTRICT |
| 2515 | (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res |
| 2516 | else res) in |
| 2517 | ((function x -> CODE x), formula) |
| 2518 | | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" in |
| 2519 | wrap (quantify false quantified formula) |
| 2520 | |
| 2521 | (* --------------------------------------------------------------------- *) |
| 2522 | (* Entry points *) |
| 2523 | |
| 2524 | let asttoctlz (name,(_,_,exists_flag),l) |
| 2525 | (used_after,fresh_used_after,fresh_used_after_seeds) positions = |
| 2526 | letctr := 0; |
| 2527 | labelctr := 0; |
| 2528 | (match exists_flag with |
| 2529 | Ast.Exists -> exists := Exists |
| 2530 | | Ast.Forall -> exists := Forall |
| 2531 | | Ast.Undetermined -> |
| 2532 | exists := if !Flag.sgrep_mode2 then Exists else Forall); |
| 2533 | |
| 2534 | let (l,used_after) = |
| 2535 | List.split |
| 2536 | (List.filter |
| 2537 | (function (t,_) -> |
| 2538 | match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true) |
| 2539 | (List.combine l (List.combine used_after positions))) in |
| 2540 | let res = |
| 2541 | List.map2 (top_level name) |
| 2542 | (List.combine used_after fresh_used_after) |
| 2543 | (List.combine fresh_used_after_seeds l) in |
| 2544 | exists := Forall; |
| 2545 | res |
| 2546 | |
| 2547 | let asttoctl r used_after positions = |
| 2548 | match r with |
| 2549 | Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> [] |
| 2550 | | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) -> |
| 2551 | asttoctlz (a,b,c) used_after positions |
| 2552 | | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CODE CTL.True] |
| 2553 | |
| 2554 | let pp_cocci_predicate (pred,modif) = |
| 2555 | Pretty_print_engine.pp_predicate pred |
| 2556 | |
| 2557 | let cocci_predicate_to_string (pred,modif) = |
| 2558 | Pretty_print_engine.predicate_to_string pred |