~ubuntu-branches/ubuntu/trusty/coccinelle/trusty-proposed

« back to all changes in this revision

Viewing changes to engine/asttoctl2.ml

• browse files at revision 17
• compare with another revision
• download diff
• download tarball
• view history from revision 17

Show diffs side-by-side

added

removed

engine/asttoctl2.ml

37

37

let warning s = Printf.fprintf stderr "warning: %s\n" s

38

38

 

39

39

type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif

40

 

type formula =

41

 

    (cocci_predicate,Ast.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl

 

40

type formula = Lib_engine.ctlcocci

 

41

type top_formula = NONDECL of Lib_engine.ctlcocci | CODE of Lib_engine.ctlcocci

42

42

 

43

43

let union = Common.union_set

44

44

let intersect l1 l2 = List.filter (function x -> List.mem x l2) l1

108

108

 

109

109

(* This stays being AX even for sgrep_mode, because it is used to identify

110

110

the structure of the term, not matching the pattern. *)

 

111

let ctl_back_ag = function

 

112

    CTL.True -> CTL.True

 

113

  | CTL.False -> CTL.False

 

114

  | x -> CTL.AG(CTL.BACKWARD,CTL.NONSTRICT,x)

 

115

 

111

116

let ctl_back_ax = function

112

117

    CTL.True -> CTL.True

113

118

  | CTL.False -> CTL.False

167

172

let aftpred     = predmaker false (Lib_engine.After,       CTL.Control)

168

173

let retpred     = predmaker false (Lib_engine.Return,      CTL.Control)

169

174

let funpred     = predmaker false (Lib_engine.FunHeader,   CTL.Control)

 

175

let unsbrpred   = predmaker false (Lib_engine.UnsafeBrace, CTL.Control)

170

176

let toppred     = predmaker false (Lib_engine.Top,         CTL.Control)

171

177

let exitpred    = predmaker false (Lib_engine.ErrorExit,   CTL.Control)

172

178

let endpred     = predmaker false (Lib_engine.Exit,        CTL.Control)

374

380

 

375

381

type after = After of formula | Guard of formula | Tail | End | VeryEnd

376

382

 

 

383

type top = Top | NotTop

 

384

 

377

385

let a2n = function After x -> Guard x | a -> a

378

386

 

379

387

let print_ctl x =

445

453

    let res = k re in

446

454

    match Ast.unwrap re with

447

455

      Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->

448

 

        bind (mcode r ((),(),bef,Ast.NoMetaPos)) res

449

 

    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res

 

456

        bind (mcode r ((),(),bef,[])) res

 

457

    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res

450

458

    | _ -> res in

451

459

  let init r k i =

452

460

    let res = k i in

464

472

let contains_pos =

465

473

  let bind x y = x or y in

466

474

  let option_default = false in

467

 

  let mcode r (_,_,kind,metapos) =

468

 

    match metapos with

469

 

      Ast.MetaPos(_,_,_,_,_) -> true

470

 

    | Ast.NoMetaPos -> false in

 

475

  let mcode r (_,_,kind,metapos) = not (metapos = []) in

471

476

  let do_nothing r k e = k e in

472

477

  let rule_elem r k re =

473

478

    let res = k re in

474

479

    match Ast.unwrap re with

475

480

      Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->

476

 

        bind (mcode r ((),(),bef,Ast.NoMetaPos)) res

477

 

    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,Ast.NoMetaPos)) res

 

481

        bind (mcode r ((),(),bef,[])) res

 

482

    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef,[])) res

478

483

    | _ -> res in

479

484

  let recursor =

480

485

    V.combiner bind option_default

801

806

      let (br2,_) = get_after_e branch2 a in

802

807

      (Ast.rewrap s (Ast.IfThenElse(ifheader,br1,els,br2,aft)),[Ast.Other s])

803

808

  | Ast.While(header,body,aft) ->

804

 

      let (bd,_) = get_after_e body a in

 

809

      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in

805

810

      (Ast.rewrap s (Ast.While(header,bd,aft)),[Ast.Other s])

806

811

  | Ast.For(header,body,aft) ->

807

 

      let (bd,_) = get_after_e body a in

 

812

      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in

808

813

      (Ast.rewrap s (Ast.For(header,bd,aft)),[Ast.Other s])

809

814

  | Ast.Do(header,body,tail) ->

810

 

      let (bd,_) = get_after_e body a in

 

815

      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in

811

816

      (Ast.rewrap s (Ast.Do(header,bd,tail)),[Ast.Other s])

812

817

  | Ast.Iterator(header,body,aft) ->

813

 

      let (bd,_) = get_after_e body a in

 

818

      let (bd,_) = get_after_e body ((Ast.Other s) :: a) in

814

819

      (Ast.rewrap s (Ast.Iterator(header,bd,aft)),[Ast.Other s])

815

820

  | Ast.Switch(header,lb,decls,cases,rb) ->

816

821

      let index = count_nested_braces s in

1000

1005

    (* no point to put a label on truepred etc; it is local to this construct

1001

1006

       so it must have the same label *)

1002

1007

    make_seq guard

1003

 

      [truepred None; recurse branch Tail new_quantified new_mquantified

 

1008

      [truepred None; recurse branch NotTop Tail new_quantified new_mquantified

1004

1009

          (Some (lv,used)) llabel slabel guard] in

1005

1010

  let after_pred = aftpred None in

1006

1011

  let or_cases after_branch =

1075

1080

  let used = ref false in

1076

1081

  let true_branch =

1077

1082

    make_seq guard

1078

 

      [truepred None; recurse branch1 Tail new_quantified new_mquantified

 

1083

      [truepred None; recurse branch1 NotTop Tail new_quantified new_mquantified

1079

1084

          (Some (lv,used)) llabel slabel guard] in

1080

1085

  let false_branch =

1081

1086

    make_seq guard

1083

1088

        quantify guard

1084

1089

          (Common.minus_set (Ast.get_fvs els) new_quantified)

1085

1090

          (header_match None guard els);

1086

 

        recurse branch2 Tail new_quantified new_mquantified

 

1091

        recurse branch2 NotTop Tail new_quantified new_mquantified

1087

1092

          (Some (lv,used)) llabel slabel guard] in

1088

1093

  let after_pred = aftpred None in

1089

1094

  let or_cases after_branch =

1126

1131

    let body =

1127

1132

      make_seq guard

1128

1133

        [inlooppred None;

1129

 

          recurse body Tail new_quantified new_mquantified

 

1134

          recurse body NotTop Tail new_quantified new_mquantified

1130

1135

            (Some (lv,used)) (Some (lv,used)) None guard] in

1131

1136

    let after_pred = loopfallpred None in

1132

1137

    let or_cases after_branch = ctl_or body after_branch in

1286

1291

    | (Ast.MINUS(pos,inst,adj,l),after) ->

1287

1292

        let (first_metamatch,last_metamatch,rest_metamatch) =

1288

1293

          match l with

1289

 

            [] -> (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)

 

1294

            Ast.NOREPLACEMENT ->

 

1295

              (matcher(Ast.CONTEXT(pos,Ast.NOTHING)),CTL.True,matcher d)

1290

1296

          | _ -> (matcher d,

1291

 

                  matcher(Ast.MINUS(pos,inst,adj,[])),

 

1297

                  matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)),

1292

1298

                  ctl_and CTL.NONSTRICT

1293

1299

                    (ctl_not (make_raw_match label false ast))

1294

 

                    (matcher(Ast.MINUS(pos,inst,adj,[])))) in

 

1300

                    (matcher(Ast.MINUS(pos,inst,adj,Ast.NOREPLACEMENT)))) in

1295

1301

        (* try to follow after link *)

1296

1302

        let to_end = ctl_or (aftpred None) (loopfallpred None) in

1297

1303

        let is_compound =

1311

1317

          (CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,

1312

1318

                           ctl_and CTL.NONSTRICT label_pred

1313

1319

                             (make_raw_match label false ast),

1314

 

                           ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred))

 

1320

                           ctl_and CTL.NONSTRICT prelabel_pred rest_metamatch))

1315

1321

  in

1316

1322

  let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in

1317

1323

  let stmt_fvs = Ast.get_fvs stmt in

1612

1618

(* --------------------------------------------------------------------- *)

1613

1619

(* the main translation loop *)

1614

1620

 

1615

 

let rec statement_list stmt_list after quantified minus_quantified

 

1621

let rec statement_list stmt_list top after quantified minus_quantified

1616

1622

    label llabel slabel dots_before guard =

1617

1623

  let isdots x =

1618

1624

    (* include Disj to be on the safe side *)

1621

1627

  let compute_label l e db = if db or isdots e then l else None in

1622

1628

  match Ast.unwrap stmt_list with

1623

1629

    Ast.DOTS(x) ->

1624

 

      let rec loop quantified minus_quantified dots_before label llabel slabel

 

1630

      let rec loop top quantified minus_quantified dots_before

 

1631

          label llabel slabel

1625

1632

          = function

1626

1633

          ([],_,_) -> (match after with After f -> f | _ -> CTL.True)

1627

1634

        | ([e],_,_) ->

1628

 

            statement e after quantified minus_quantified

 

1635

            statement e top after quantified minus_quantified

1629

1636

              (compute_label label e dots_before)

1630

1637

              llabel slabel guard

1631

1638

        | (e::sl,fv::fvs,mfv::mfvs) ->

1638

1645

            let new_mquantified =

1639

1646

              Common.union_set munqshared minus_quantified in

1640

1647

            quantify guard unqshared

1641

 

              (statement e

 

1648

              (statement e top

1642

1649

                 (After

1643

1650

                    (let (label1,llabel1,slabel1) =

1644

1651

                      match Ast.unwrap e with

1647

1654

                            Ast.Goto _ -> (None,None,None)

1648

1655

                          | _ -> (label,llabel,slabel))

1649

1656

                      | _ -> (label,llabel,slabel) in

1650

 

                    loop new_quantified new_mquantified (isdots e)

 

1657

                    loop NotTop new_quantified new_mquantified (isdots e)

1651

1658

                      label1 llabel1 slabel1

1652

1659

                      (sl,fvs,mfvs)))

1653

1660

                 new_quantified new_mquantified

1654

1661

                 (compute_label label e dots_before) llabel slabel guard)

1655

1662

        | _ -> failwith "not possible" in

1656

 

      loop quantified minus_quantified dots_before

 

1663

      loop top quantified minus_quantified dots_before

1657

1664

        label llabel slabel

1658

1665

        (x,List.map Ast.get_fvs x,List.map Ast.get_mfvs x)

1659

1666

  | Ast.CIRCLES(x) -> failwith "not supported"

1661

1668

 

1662

1669

(* llabel is the label of the enclosing loop and slabel is the label of the

1663

1670

   enclosing switch *)

1664

 

and statement stmt after quantified minus_quantified

 

1671

and statement stmt top after quantified minus_quantified

1665

1672

    label llabel slabel guard =

1666

1673

  let ctl_au     = ctl_au CTL.NONSTRICT in

1667

1674

  let ctl_ax     = ctl_ax CTL.NONSTRICT in

1732

1739

                  (Ast.MINUS(_,inst1,adj1,l1),Ast.MINUS(_,_,_,l2))

1733

1740

                  when !Flag.sgrep_mode2 ->

1734

1741

                    (* in sgrep mode, we can propagate the - *)

1735

 

                    Some (Ast.MINUS(Ast.NoPos,inst1,adj1,l1@l2))

 

1742

                    let new_info =

 

1743

                      match (l1,l2) with

 

1744

                        (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->

 

1745

                          Ast.NOREPLACEMENT

 

1746

                      | _ ->

 

1747

                          failwith "no replacements allowed in sgrep mode" in

 

1748

                    Some (Ast.MINUS(Ast.NoPos,inst1,adj1,new_info))

1736

1749

                | (Ast.MINUS(_,_,_,l1),Ast.MINUS(_,_,_,l2)) ->

1737

 

                    Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,Ast.ONE)))

 

1750

                    let change =

 

1751

                      match (l1,l2) with

 

1752

                        (Ast.NOREPLACEMENT,Ast.NOREPLACEMENT) ->

 

1753

                          Ast.NOTHING

 

1754

                      | (Ast.NOREPLACEMENT,Ast.REPLACEMENT(l,ct))

 

1755

                      | (Ast.REPLACEMENT(l,ct),Ast.NOREPLACEMENT) ->

 

1756

                          Ast.BEFORE(l,ct)

 

1757

                      | (Ast.REPLACEMENT(l1,ct1),Ast.REPLACEMENT(l2,ct2)) ->

 

1758

                          Ast.BEFORE(l1@l2,Ast.lub_count ct1 ct2) in

 

1759

                    Some (Ast.CONTEXT(Ast.NoPos,change))

1738

1760

                | (Ast.CONTEXT(_,Ast.BEFORE(l1,c1)),

1739

1761

                   Ast.CONTEXT(_,Ast.AFTER(l2,c2))) ->

1740

 

                     (if not (c1 = c2) then failwith "bad + code");

1741

 

                    Some (Ast.CONTEXT(Ast.NoPos,Ast.BEFORE(l1@l2,c1)))

 

1762

                     Some

 

1763

                       (Ast.CONTEXT(Ast.NoPos,

 

1764

                                    Ast.BEFORE(l1@l2,Ast.lub_count c1 c2)))

1742

1765

                | (Ast.CONTEXT(_,Ast.BEFORE(_)),Ast.CONTEXT(_,Ast.NOTHING))

1743

1766

                | (Ast.CONTEXT(_,Ast.NOTHING),Ast.CONTEXT(_,Ast.NOTHING)) ->

1744

1767

                    Some retmc

1764

1787

                  ctl_or normal_res

1765

1788

                    (ctl_and (make_match mod_rbrace)

1766

1789

                       (ctl_and

1767

 

                          (ctl_back_ax

1768

 

                             (ctl_not

1769

 

                                (ctl_uncheck

1770

 

                                   (ctl_or simple_return return_expr))))

1771

1790

                          (ctl_au

1772

1791

                             (make_match stripped_rbrace)

1773

1792

                             (* error exit not possible; it is in the middle

1774

1793

                                of code, so a return is needed *)

1775

 

                             exit)))

 

1794

                             exit)

 

1795

                          (* worry about perf, but seems correct, not ax *)

 

1796

                          (ctl_back_ag

 

1797

                             (ctl_not

 

1798

                                (ctl_uncheck

 

1799

                                   (ctl_or simple_return return_expr))))))

1776

1800

              | _ ->

1777

1801

                  (* some change in the middle of the return, so have to

1778

1802

                     find an actual return *)

1835

1859

                  (ctl_or

1836

1860

                     (if !exists = Exists then CTL.False else (aftpred label))

1837

1861

                     (quantify guard b2fvs

1838

 

                        (statement_list body

 

1862

                        (statement_list body NotTop

1839

1863

                           (After (make_seq_after end_brace after))

1840

1864

                           new_quantified2 new_mquantified2

1841

1865

                           (Some (lv,ref true))

1852

1876

                  | _ -> false)

1853

1877

            | _ -> false)

1854

1878

        | _ -> false in

1855

 

      if empty_body && after = Tail

 

1879

      if empty_body && List.mem after [Tail;End;VeryEnd]

1856

1880

          (* for just a match of an if branch of the form { ... }, just

1857

1881

             match the first brace *)

1858

1882

      then quantify guard lbfvs (make_match lbrace)

1876

1900

                (make_match empty_rbrace)

1877

1901

                (ctl_ax (* skip the destination label *)

1878

1902

                   (quantify guard b2fvs

1879

 

                      (statement_list body End

 

1903

                      (statement_list body NotTop End

1880

1904

                         new_quantified2 new_mquantified2 None llabel slabel

1881

1905

                         true guard)))] in

1882

1906

        let pattern3 =

1894

1918

                            (* want AF even for sgrep *)

1895

1919

                            (CTL.AF(CTL.FORWARD,CTL.STRICT,end_brace))))

1896

1920

                      (quantify guard b2fvs

1897

 

                         (statement_list body Tail

 

1921

                         (statement_list body NotTop Tail

1898

1922

                            new_quantified2 new_mquantified2

1899

1923

                            None(*no label because past the goto*)

1900

1924

                            llabel slabel false guard))])) in

1916

1940

  | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)

1917

1941

      (*ctl_and        seems pointless, disjuncts see label too

1918

1942

        (label_pred_maker label)*)

1919

 

        (List.fold_left ctl_seqor CTL.False

1920

 

           (List.map

1921

 

              (function sl ->

1922

 

                statement_list sl after quantified minus_quantified label

1923

 

                  llabel slabel true guard)

1924

 

              stmt_dots_list))

 

1943

      let subformulas =

 

1944

        List.map

 

1945

          (function sl ->

 

1946

            statement_list sl top after quantified minus_quantified label

 

1947

              llabel slabel true guard)

 

1948

          stmt_dots_list in

 

1949

      let safe_subformulas =

 

1950

        match top with

 

1951

          Top -> List.map2 protect_top_level stmt_dots_list subformulas

 

1952

        | NotTop -> subformulas in

 

1953

      List.fold_left ctl_seqor CTL.False safe_subformulas

1925

1954

 

1926

1955

  | Ast.Nest(starter,stmt_dots,ender,whencode,multi,bef,aft) ->

1927

1956

      (* label in recursive call is None because label check is already

1947

1976

 

1948

1977

      quantify guard bfvs

1949

1978

        (let dots_pattern =

1950

 

          statement_list stmt_dots (a2n after) new_quantified minus_quantified

 

1979

          statement_list stmt_dots top (a2n after)

 

1980

            new_quantified minus_quantified

1951

1981

            label(*None*) llabel slabel true guard in

1952

1982

        dots_and_nests multi

1953

1983

          (Some dots_pattern) whencode bef aft dot_code after label

1954

1984

          (process_bef_aft new_quantified minus_quantified

1955

1985

             label(*None*) llabel slabel true)

1956

 

          (function x ->

1957

 

            statement_list x Tail new_quantified minus_quantified label(*None*)

 

1986

          (function x -> (* for when code *)

 

1987

            statement_list x NotTop Tail

 

1988

              new_quantified minus_quantified label(*None*)

1958

1989

              llabel slabel true true)

1959

 

          (function x ->

1960

 

            statement x Tail new_quantified minus_quantified label(*None*)

 

1990

          (function x -> (* for when code *)

 

1991

            statement x NotTop Tail

 

1992

              new_quantified minus_quantified label(*None*)

1961

1993

              llabel slabel true)

1962

1994

          guard quantified

1963

1995

          (function x -> Ast.set_fvs [] (Ast.rewrap stmt x)))

1973

2005

      dots_and_nests false None whencodes bef aft dot_code after label

1974

2006

        (process_bef_aft quantified minus_quantified None llabel slabel true)

1975

2007

        (function x ->

1976

 

          statement_list x Tail quantified minus_quantified

 

2008

          statement_list x NotTop Tail quantified minus_quantified

1977

2009

            None llabel slabel true true)

1978

2010

        (function x ->

1979

 

          statement x Tail quantified minus_quantified None llabel slabel true)

 

2011

          statement x NotTop Tail quantified minus_quantified

 

2012

            None llabel slabel true)

1980

2013

        guard quantified

1981

2014

        (function x -> Ast.set_fvs [] (Ast.rewrap stmt x))

1982

2015

 

2086

2119

        then (CTL.True,CTL.False)

2087

2120

        else

2088

2121

        let res =

2089

 

          statement_list decls Tail

 

2122

          statement_list decls NotTop Tail

2090

2123

            new2_quantified new2_mquantified (Some (lv,used)) llabel None

2091

2124

            false(*?*) guard in

2092

2125

        (res,res) in

2115

2148

                  let new3_quantified = union b1fvs new2_quantified in

2116

2149

                  let new3_mquantified = union mb1fvs new2_mquantified in

2117

2150

                  let body =

2118

 

                    statement_list body Tail

 

2151

                    statement_list body NotTop Tail

2119

2152

                      new3_quantified new3_mquantified (Some (lv,used)) llabel

2120

2153

                      (Some (lv,used)) false(*?*) guard in

2121

2154

                  quantify guard b1fvs (make_seq [case_header; body])

2222

2255

                Some

2223

2256

                  (CTL.AndAny

2224

2257

                     (CTL.FORWARD,guard_to_strict guard,start_brace,

2225

 

                      statement_list stmt_dots

 

2258

                      statement_list stmt_dots NotTop

2226

2259

                 (* discards match on right brace, but don't need it *)

2227

2260

                        (Guard (make_seq_after end_brace after))

2228

2261

                        new_quantified3 new_mquantified3

2259

2292

                                                 Ast.WhenAlways(s) -> prev

2260

2293

                                               | Ast.WhenNot(sl) ->

2261

2294

                                                   let x =

2262

 

                                                     statement_list sl Tail

 

2295

                                                     statement_list sl

 

2296

                                                       NotTop Tail

2263

2297

                                                       new_quantified3

2264

2298

                                                       new_mquantified3

2265

2299

                                                       label llabel slabel

2277

2311

                                          function

2278

2312

                                              Ast.WhenAlways(s) ->

2279

2313

                                                let x =

2280

 

                                                  statement s Tail

 

2314

                                                  statement s NotTop Tail

2281

2315

                                                    new_quantified3

2282

2316

                                                    new_mquantified3

2283

2317

                                                    label llabel slabel true in

2302

2336

          [body] ->

2303

2337

            (match Ast.unwrap body with

2304

2338

              Ast.Dots

2305

 

                ((_,i,(Ast.MINUS(_,_,_,[]) as d),_),[],_,_) ->

 

2339

                ((_,i,(Ast.MINUS(_,_,_,Ast.NOREPLACEMENT) as d),_),[],_,_) ->

2306

2340

                  (match (Ast.unwrap lbrace,Ast.unwrap rbrace) with

2307

 

                    (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,[]),_)),

2308

 

                     Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,[]),_)))

 

2341

                    (Ast.SeqStart((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)),

 

2342

                     Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),_)))

2309

2343

                    when not (contains_pos rbrace) ->

2310

2344

                      Some

2311

2345

                        (* andany drops everything to the end, including close

2328

2362

            make_seq

2329

2363

              [start_brace;

2330

2364

                quantify guard b3fvs

2331

 

                  (statement_list body

 

2365

                  (statement_list body NotTop

2332

2366

                     (After (make_seq_after end_brace after))

2333

2367

                     new_quantified3 new_mquantified3 None llabel slabel

2334

2368

                     false guard)] in

2347

2381

        | _ -> failwith "not possible" in

2348

2382

      let define_header = quantify guard hfvs (make_match header) in

2349

2383

      let body_code =

2350

 

        statement_list body after

 

2384

        statement_list body NotTop after

2351

2385

          (Common.union_set bfvs quantified)

2352

2386

          (Common.union_set mbfvs minus_quantified)

2353

2387

          None llabel slabel true guard in

2369

2403

      Ast.AddingBetweenDots (brace_term,n)

2370

2404

    | Ast.DroppingBetweenDots (brace_term,n) ->

2371

2405

        let match_brace =

2372

 

          statement brace_term after quantified minus_quantified

 

2406

          statement brace_term NotTop after quantified minus_quantified

2373

2407

            label llabel slabel guard in

2374

2408

        let v = Printf.sprintf "_r_%d" n in

2375

2409

        let case1 = ctl_and CTL.NONSTRICT (CTL.Ref v) match_brace in

2391

2425

      quantify true (get_unquantified quantified [n])

2392

2426

        (ctl_and s (make_raw_match None guard re) paren_pred)

2393

2427

  | Ast.Other s ->

2394

 

      statement s Tail quantified minus_quantified label llabel slabel guard

 

2428

      statement s NotTop Tail quantified minus_quantified

 

2429

        label llabel slabel guard

2395

2430

  | Ast.Other_dots d ->

2396

 

      statement_list d Tail quantified minus_quantified

 

2431

      statement_list d NotTop Tail quantified minus_quantified

2397

2432

        label llabel slabel true guard

2398

2433

 

 

2434

and protect_top_level stmt_dots formula =

 

2435

  let starts_with_dots =

 

2436

    match Ast.undots stmt_dots with

 

2437

      d::ds ->

 

2438

        (match Ast.unwrap d with

 

2439

          Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)

 

2440

        | Ast.Stars(_,_,_,_) -> true

 

2441

        | _ -> false)

 

2442

    | _ -> false in

 

2443

  let starts_with_non_context_brace =

 

2444

    (* None = No danger

 

2445

       Some false = OK except on function braces

 

2446

       Some true = Never OK *)

 

2447

    match Ast.undots stmt_dots with

 

2448

      d::ds ->

 

2449

        (match Ast.unwrap d with

 

2450

          Ast.Seq(before,body,after) ->

 

2451

            let beforemc =

 

2452

              match Ast.unwrap before with

 

2453

                Ast.SeqStart(obr) -> Ast.get_mcodekind obr

 

2454

              | _ -> failwith "bad seq" in

 

2455

            let aftermc =

 

2456

              match Ast.unwrap after with

 

2457

                Ast.SeqEnd(cbr) -> Ast.get_mcodekind cbr

 

2458

              | _ -> failwith "bad seq"in

 

2459

            (match (beforemc,aftermc) with

 

2460

              (* safe cases *)

 

2461

              (Ast.CONTEXT(_,(Ast.NOTHING|Ast.AFTER _)),

 

2462

               Ast.CONTEXT(_,(Ast.NOTHING|Ast.BEFORE _))) -> None

 

2463

            | (Ast.MINUS(_,_,_,Ast.NOREPLACEMENT),

 

2464

               Ast.MINUS(_,_,_,Ast.NOREPLACEMENT))

 

2465

              when List.length (Ast.undots body) = 1 -> Some false (*ok on if*)

 

2466

              (* unsafe, can't be allowed to match fn top *)

 

2467

            | _ -> Some true)

 

2468

        | _ -> None)

 

2469

    | _ -> None in

 

2470

  if starts_with_dots

 

2471

  then (* EX because there is a loop on enter/top *)

 

2472

    ctl_and CTL.NONSTRICT (toppred None) (ctl_ex formula)

 

2473

  else

 

2474

    match starts_with_non_context_brace with

 

2475

      None -> formula

 

2476

    | Some false ->

 

2477

        ctl_and CTL.NONSTRICT

 

2478

          (ctl_not(CTL.EX(CTL.BACKWARD,funpred None)))

 

2479

          formula

 

2480

    | Some true ->

 

2481

        ctl_and CTL.NONSTRICT

 

2482

          (ctl_not(CTL.EX(CTL.BACKWARD,unsbrpred None)))

 

2483

          formula

 

2484

 

 

2485

 

2399

2486

(* --------------------------------------------------------------------- *)

2400

2487

(* cleanup: convert AX to EX for pdots.

2401

2488

Concretely: AX(A[...] & E[...]) becomes AX(A[...]) & EX(E[...])

2459

2546

  used_after := ua;

2460

2547

  saved := Ast.get_saved t;

2461

2548

  let quantified = Common.minus_set (Common.union_set ua fuas) pos in

2462

 

  quantify false quantified

2463

 

    (match Ast.unwrap t with

 

2549

  let (wrap,formula) =

 

2550

    match Ast.unwrap t with

2464

2551

      Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"

2465

 

    | Ast.DECL(stmt) ->

 

2552

    | Ast.NONDECL(stmt) ->

2466

2553

        let unopt = elim_opt.V.rebuilder_statement stmt in

2467

2554

        let unopt = preprocess_dots_e unopt in

2468

 

        cleanup(statement unopt VeryEnd quantified [] None None None false)

 

2555

        let formula =

 

2556

          cleanup

 

2557

            (statement unopt Top VeryEnd quantified [] None None None false) in

 

2558

        ((function x -> NONDECL x), formula)

2469

2559

    | Ast.CODE(stmt_dots) ->

2470

2560

        let unopt = elim_opt.V.rebuilder_statement_dots stmt_dots in

2471

2561

        let unopt = preprocess_dots unopt in

2472

 

        let starts_with_dots =

2473

 

          match Ast.undots stmt_dots with

2474

 

            d::ds ->

2475

 

              (match Ast.unwrap d with

2476

 

                Ast.Dots(_,_,_,_) | Ast.Circles(_,_,_,_)

2477

 

              | Ast.Stars(_,_,_,_) -> true

2478

 

              | _ -> false)

2479

 

          | _ -> false in

2480

 

        let starts_with_brace =

2481

 

          match Ast.undots stmt_dots with

2482

 

            d::ds ->

2483

 

              (match Ast.unwrap d with

2484

 

                Ast.Seq(_) -> true

2485

 

              | _ -> false)

2486

 

          | _ -> false in

2487

 

        let res =

2488

 

          statement_list unopt VeryEnd quantified [] None None None

 

2562

        let formula =

 

2563

          statement_list unopt Top VeryEnd quantified [] None None None

2489

2564

            false false in

2490

 

        cleanup

2491

 

          (if starts_with_dots

2492

 

          then

2493

 

          (* EX because there is a loop on enter/top *)

2494

 

            ctl_and CTL.NONSTRICT (toppred None) (ctl_ex res)

2495

 

          else if starts_with_brace

2496

 

          then

2497

 

             ctl_and CTL.NONSTRICT

2498

 

              (ctl_not(CTL.EX(CTL.BACKWARD,(funpred None)))) res

2499

 

          else res)

2500

 

    | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords")

 

2565

        let clean_formula = cleanup (protect_top_level stmt_dots formula) in

 

2566

        ((function x -> CODE x), clean_formula)

 

2567

    | Ast.ERRORWORDS(exps) -> failwith "not supported errorwords" in

 

2568

  wrap (quantify false quantified formula)

2501

2569

 

2502

2570

(* --------------------------------------------------------------------- *)

2503

2571

(* Entry points *)

2530

2598

    Ast.ScriptRule _ | Ast.InitialScriptRule _ | Ast.FinalScriptRule _ -> []

2531

2599

  | Ast.CocciRule (a,b,c,_,Ast_cocci.Normal) ->

2532

2600

      asttoctlz (a,b,c) used_after positions

2533

 

  | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CTL.True]

 

2601

  | Ast.CocciRule (a,b,c,_,Ast_cocci.Generated) -> [CODE CTL.True]

2534

2602

 

2535

2603

let pp_cocci_predicate (pred,modif) =

2536

2604

  Pretty_print_engine.pp_predicate pred

• Older »

Loggerhead is a web-based interface for Breezy
Version: 2.0.1