← Back to branch summary

~npalix/coccinelle/upstream

« back to all changes in this revision

Viewing changes to popl/popltoctl.ml

  • Committer: Julia Lawall
  • Date: 2007-05-15 15:12:20 UTC
  • Revision ID: git-v1:4d3ead9633cc54da2af4deb918afa6d228c56bea
*** empty log message ***

svn path=/coccinelle/; revision=2759

Show diffs side-by-side

added added

removed removed

Lines of Context:
popl/popltoctl.ml
 
1
module Past = Ast_popl
 
2
module Ast = Ast_cocci
 
3
module V = Visitor_ast
 
4
module CTL  = Ast_ctl
 
5
 
 
6
(* --------------------------------------------------------------------- *)
 
7
(* result type *)
 
8
 
 
9
type cocci_predicate = Lib_engine.predicate * Ast.meta_name Ast_ctl.modif
 
10
type formula =
 
11
    (cocci_predicate,Ast_cocci.meta_name, Wrapper_ctl.info) Ast_ctl.generic_ctl
 
12
 
 
13
(* --------------------------------------------------------------------- *)
 
14
 
 
15
let wrap n ctl = (ctl,n)
 
16
 
 
17
let ctl_true       = wrap 0 CTL.True
 
18
 
 
19
let ctl_false      = wrap 0 CTL.False
 
20
 
 
21
let ctl_and x y    = wrap 0 (CTL.And(CTL.STRICT,x,y))
 
22
 
 
23
let ctl_or x y     = wrap 0 (CTL.Or(x,y))
 
24
 
 
25
let ctl_seqor x y  = wrap 0 (CTL.SeqOr(x,y))
 
26
 
 
27
let ctl_not x      = wrap 0 (CTL.Not(x))
 
28
 
 
29
let ctl_ax x       = wrap 0 (CTL.AX(CTL.FORWARD,CTL.STRICT,x))
 
30
 
 
31
let after          = wrap 0 (CTL.Pred(Lib_engine.After, CTL.Control))
 
32
 
 
33
let ctl_au x y     = wrap 0 (CTL.AU(CTL.FORWARD,CTL.STRICT,x,ctl_or y after))
 
34
 
 
35
let ctl_exists v x = wrap 0 (CTL.Exists(v,x,true))
 
36
 
 
37
let contains_modif =
 
38
  let bind x y = x or y in
 
39
  let option_default = false in
 
40
  let mcode r (_,_,kind) =
 
41
    match kind with
 
42
      Ast.MINUS(_,_) -> true
 
43
    | Ast.PLUS -> failwith "not possible"
 
44
    | Ast.CONTEXT(_,info) -> not (info = Ast.NOTHING) in
 
45
  let do_nothing r k e = k e in
 
46
  let rule_elem r k re =
 
47
    let res = k re in
 
48
    match Ast.unwrap re with
 
49
      Ast.FunHeader(bef,_,fninfo,name,lp,params,rp) ->
 
50
        bind (mcode r ((),(),bef)) res
 
51
    | Ast.Decl(bef,_,decl) -> bind (mcode r ((),(),bef)) res
 
52
    | _ -> res in
 
53
  let recursor =
 
54
    V.combiner bind option_default
 
55
      mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
 
56
      do_nothing do_nothing do_nothing do_nothing
 
57
      do_nothing do_nothing do_nothing do_nothing do_nothing do_nothing
 
58
      do_nothing rule_elem do_nothing do_nothing do_nothing do_nothing in
 
59
  recursor.V.combiner_rule_elem
 
60
 
 
61
let predmaker guard term =
 
62
  if not guard && contains_modif term
 
63
  then
 
64
    let v = ("","_v") in
 
65
    ctl_exists v (wrap 0 (CTL.Pred (Lib_engine.Match(term),CTL.Modif v)))
 
66
  else wrap 0 (CTL.Pred (Lib_engine.Match(term),CTL.Control))
 
67
 
 
68
(* --------------------------------------------------------------------- *)
 
69
 
 
70
let rec ctl_seq guard a = function
 
71
    Past.Seq(elem,seq) ->
 
72
      ctl_element guard (ctl_seq guard a seq) elem
 
73
  | Past.Empty -> ctl_true
 
74
  | Past.SExists(var,seq) -> ctl_exists var (ctl_seq guard a seq)
 
75
 
 
76
and ctl_element guard a = function
 
77
    Past.Term(term) -> ctl_and (predmaker guard term) (ctl_ax a)
 
78
  | Past.Or(seq1,seq2) ->
 
79
      ctl_seqor (ctl_seq guard a seq1) (ctl_seq guard a seq2)
 
80
  | Past.DInfo(dots,seq_bef,seq_aft) ->
 
81
      let shortest =
 
82
        List.fold_left ctl_or ctl_false
 
83
          (List.map (ctl_element true ctl_true) (seq_bef@seq_aft)) in
 
84
      ctl_au (ctl_and (ctl_dots guard dots) (ctl_not shortest)) a
 
85
  | Past.EExists(var,elem) -> ctl_exists var (ctl_element guard a elem)
 
86
 
 
87
and ctl_dots guard = function
 
88
    Past.Dots -> ctl_true
 
89
  | Past.Nest(_) when guard -> ctl_true
 
90
  | Past.Nest(seq) ->
 
91
      ctl_or (ctl_seq false ctl_true seq) (ctl_not (ctl_seq true ctl_true seq))
 
92
  | Past.When(dots,seq) ->
 
93
      ctl_and (ctl_dots guard dots) (ctl_not (ctl_seq true ctl_true seq))
 
94
  | Past.DExists(var,dots) -> ctl_exists var (ctl_dots guard dots)
 
95
 
 
96
(* --------------------------------------------------------------------- *)
 
97
 
 
98
let toctl sl = ctl_seq false ctl_true sl