« back to all changes in this revision
Viewing changes to engine/asttoctl2.ml
- browse files at revision 9
- compare with another revision
- download diff
- download tarball
- view history from revision 9
- Committer: Bazaar Package Importer
- Author(s): Daniel T Chen
- Date: 2009-08-10 01:01:24 UTC
- mfrom: (7.1.1 sid)
- Revision ID: james.westby@ubuntu.com-20090810010124-9fn4c8m93ic60fqx
Tags: 0.1.9.deb-1ubuntu1
* Merge from Debian unstable, remaining changes:
- debian/control: build-depend on python2.6-dev,
set XB-Python-Version to 2.6
* New upstream (Debian) packaging applied fix for
LP: #410907 (see changelog entry below)
- debian/control: build-depend on python2.6-dev,
set XB-Python-Version to 2.6
* New upstream (Debian) packaging applied fix for
LP: #410907 (see changelog entry below)
- files added:
- commons/ograph_simple.ml
- files removed:
- debian/patches/fixes/unsafe-tmp-handling.diff
- files modified:
- Makefile
added
removed
engine/asttoctl2.ml
25
25
(* true = don't see all matched nodes, only modified ones *)
26
26
let onlyModif = ref true(*false*)
27
27
28
type ex = Exists | Forall | ReverseForall
28
type ex = Exists | Forall
29
29
let exists = ref Forall
30
30
31
31
module Ast = Ast_cocci
92
92
match !exists with
93
93
Exists -> CTL.EX(CTL.FORWARD,x)
94
94
| Forall -> CTL.AX(CTL.FORWARD,s,x)
95
| ReverseForall -> failwith "not supported"
96
95
97
96
let ctl_ax_absolute s = function
98
97
CTL.True -> CTL.True
130
129
match (x,!exists) with
131
130
(CTL.True,Exists) -> CTL.EF(CTL.FORWARD,y)
132
131
| (CTL.True,Forall) -> CTL.AF(CTL.FORWARD,s,y)
133
| (CTL.True,ReverseForall) -> failwith "not supported"
134
132
| (_,Exists) -> CTL.EU(CTL.FORWARD,x,y)
135
133
| (_,Forall) -> CTL.AU(CTL.FORWARD,s,x,y)
136
| (_,ReverseForall) -> failwith "not supported"
137
134
138
135
let ctl_anti_au s x y = (* only for ..., where the quantifier is changed *)
139
136
CTL.XX
140
137
(match (x,!exists) with
141
138
(CTL.True,Exists) -> CTL.AF(CTL.FORWARD,s,y)
142
139
| (CTL.True,Forall) -> CTL.EF(CTL.FORWARD,y)
143
| (CTL.True,ReverseForall) -> failwith "not supported"
144
140
| (_,Exists) -> CTL.AU(CTL.FORWARD,s,x,y)
145
| (_,Forall) -> CTL.EU(CTL.FORWARD,x,y)
146
| (_,ReverseForall) -> failwith "not supported")
141
| (_,Forall) -> CTL.EU(CTL.FORWARD,x,y))
147
142
148
143
let ctl_uncheck = function
149
144
CTL.True -> CTL.True
609
604
| Ast.Nest(stmt_dots,w,multi,_,aft) ->
610
605
let w = get_before_whencode w in
611
606
let (sd,_) = get_before stmt_dots a in
612
let a =
607
(*let a =
608
got rid of this, don't want to let nests overshoot
613
609
List.filter
614
610
(function
615
611
Ast.Other a ->
625
621
Unify_ast.MAYBE -> false
626
622
| _ -> true)
627
623
| _ -> true)
628
a in
624
a in*)
629
625
(Ast.rewrap s (Ast.Nest(sd,w,multi,a,aft)),[Ast.Other_dots stmt_dots])
630
626
| Ast.Disj(stmt_dots_list) ->
631
627
let (dsl,dsla) =
711
707
| Ast.Nest(stmt_dots,w,multi,bef,_) ->
712
708
let w = get_after_whencode a w in
713
709
let (sd,_) = get_after stmt_dots a in
714
let a =
710
(*let a =
711
got rid of this. don't want to let nests overshoot
715
712
List.filter
716
713
(function
717
714
Ast.Other a ->
727
724
Unify_ast.MAYBE -> false
728
725
| _ -> true)
729
726
| _ -> true)
730
a in
727
a in*)
731
728
(Ast.rewrap s (Ast.Nest(sd,w,multi,bef,a)),[Ast.Other_dots stmt_dots])
732
729
| Ast.Disj(stmt_dots_list) ->
733
730
let (dsl,dsla) =
856
853
let rec suffixes = function
857
854
[] -> []
858
855
| x::xs -> xs::(suffixes xs) in
859
let prefixes = List.rev (suffixes (List.rev guard_matches)) in
856
let prefixes =
857
(* normally, we check that an expression does not match something
858
earlier in the disjunction (calculated as prefixes). But for large
859
disjunctions, this can result in a very big CTL formula. So we
860
give the user the option to say he doesn't want this feature, if that is
861
the case. *)
862
if !Flag_matcher.no_safe_expressions
863
then List.map (function _ -> []) matches
864
else List.rev (suffixes (List.rev guard_matches)) in
860
865
let info = (* not null *)
861
866
List.map2
862
867
(function matcher ->
890
895
if List.exists (function Ast.Exp(_) | Ast.Ty(_) -> true | _ -> false)
891
896
all
892
897
then failwith "unexpected exp or ty";
893
List.fold_left ctl_seqor CTL.False
894
(List.rev (List.map make_match res)))
898
List.fold_left ctl_seqor CTL.False (List.map make_match res))
895
899
896
900
(* code might be a DisjRuleElem, in which case we break it apart
897
901
code doesn't contain an Exp or Ty
964
968
let lv = get_label_ctr() in
965
969
let used = ref false in
966
970
let true_branch =
971
(* no point to put a label on truepred etc; it is local to this construct
972
so it must have the same label *)
967
973
make_seq guard
968
[truepred label; recurse branch Tail new_quantified new_mquantified
974
[truepred None; recurse branch Tail new_quantified new_mquantified
969
975
(Some (lv,used)) llabel slabel guard] in
970
let after_pred = aftpred label in
976
let after_pred = aftpred None in
971
977
let or_cases after_branch =
972
ctl_or true_branch (ctl_or (fallpred label) after_branch) in
978
ctl_or true_branch (ctl_or (fallpred None) after_branch) in
973
979
let (if_header,wrapper) =
974
980
if !used
975
981
then
1004
1010
| _ -> failwith "not possible" in
1005
1011
let (e2fvs,b2fvs,s2fvs) =
1006
1012
(* fvs on else? *)
1007
match seq_fvs quantified
1008
[Ast.get_fvs ifheader;Ast.get_fvs branch2;afvs] with
1013
(* just combine with the else branch. no point to have separate
1014
quantifier, since there is only one possible control-flow path *)
1015
let else_fvs = Common.union_set (Ast.get_fvs els) (Ast.get_fvs branch2) in
1016
match seq_fvs quantified [Ast.get_fvs ifheader;else_fvs;afvs] with
1009
1017
[(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1010
(e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1018
(e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1011
1019
| _ -> failwith "not possible" in
1012
1020
let bothfvs = union (union b1fvs b2fvs) (intersect s1fvs s2fvs) in
1013
1021
let exponlyfvs = intersect e1fvs e2fvs in
1021
1029
| _ -> failwith "not possible" in
1022
1030
let (me2fvs,mb2fvs,ms2fvs) =
1023
1031
(* fvs on else? *)
1024
match seq_fvs minus_quantified
1025
[Ast.get_mfvs ifheader;Ast.get_mfvs branch2;[]] with
1032
(* just combine with the else branch. no point to have separate
1033
quantifier, since there is only one possible control-flow path *)
1034
let else_mfvs =
1035
Common.union_set (Ast.get_mfvs els) (Ast.get_mfvs branch2) in
1036
match seq_fvs minus_quantified [Ast.get_mfvs ifheader;else_mfvs;[]] with
1026
1037
[(e2fvs,b2fvs);(s2fvs,b2afvs);_] ->
1027
1038
(e2fvs,Common.union_set b2fvs b2afvs,s2fvs)
1028
1039
| _ -> failwith "not possible" in
1035
1046
let used = ref false in
1036
1047
let true_branch =
1037
1048
make_seq guard
1038
[truepred label; recurse branch1 Tail new_quantified new_mquantified
1049
[truepred None; recurse branch1 Tail new_quantified new_mquantified
1039
1050
(Some (lv,used)) llabel slabel guard] in
1040
1051
let false_branch =
1041
1052
make_seq guard
1042
[falsepred label; make_match els;
1053
[falsepred None;
1054
quantify guard
1055
(Common.minus_set (Ast.get_fvs els) new_quantified)
1056
(header_match None guard els);
1043
1057
recurse branch2 Tail new_quantified new_mquantified
1044
1058
(Some (lv,used)) llabel slabel guard] in
1045
let after_pred = aftpred label in
1059
let after_pred = aftpred None in
1046
1060
let or_cases after_branch =
1047
1061
ctl_or true_branch (ctl_or false_branch after_branch) in
1048
1062
let s = guard_to_strict guard in
1055
1069
else (if_header,function x -> x) in
1056
1070
wrapper
1057
1071
(end_control_structure bothfvs if_header or_cases after_pred
1058
(Some(ctl_and s (ctl_ex (falsepred label)) (ctl_ex after_pred)))
1059
(Some(ctl_ex (falsepred label)))
1072
(Some(ctl_and s (ctl_ex (falsepred None)) (ctl_ex after_pred)))
1073
(Some(ctl_ex (falsepred None)))
1060
1074
aft after label guard)
1061
1075
1062
1076
let forwhile header body ((afvs,_,_,_) as aft) after
1082
1096
let used = ref false in
1083
1097
let body =
1084
1098
make_seq guard
1085
[inlooppred label;
1099
[inlooppred None;
1086
1100
recurse body Tail new_quantified new_mquantified
1087
1101
(Some (lv,used)) (Some (lv,used)) None guard] in
1088
let after_pred = fallpred label in
1102
let after_pred = fallpred None in
1089
1103
let or_cases after_branch = ctl_or body after_branch in
1090
1104
let (header,wrapper) =
1091
1105
if !used
1196
1210
let prelabel_pred =
1197
1211
CTL.Pred (Lib_engine.PrefixLabel(label_var),CTL.Control) in
1198
1212
let matcher d = make_match None guard (make_meta_rule_elem d fvinfo) in
1199
let ender =
1213
let stmt_fvs = Ast.get_fvs stmt in
1214
let fvs = get_unquantified quantified stmt_fvs in
1215
let (new_fvs,body) =
1200
1216
match (d,after) with
1201
1217
(Ast.CONTEXT(pos,Ast.NOTHING),(Tail|End|VeryEnd)) ->
1202
1218
(* just match the root. don't care about label; always ok *)
1203
make_raw_match None false ast
1219
(fvs,function f -> f(make_raw_match None false ast))
1204
1220
| (Ast.MINUS(pos,inst,adj,[]),(Tail|End|VeryEnd)) ->
1205
1221
(* don't have to put anything before the beginning, so don't have to
1206
1222
distinguish the first node. so don't have to bother about paths,
1207
1223
just use the label. label ensures that found nodes match up with
1208
1224
what they should because it is in the lhs of the andany. *)
1209
CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
1210
ctl_and CTL.NONSTRICT label_pred
1211
(make_raw_match label false ast),
1212
ctl_and CTL.NONSTRICT (matcher d) prelabel_pred)
1225
let ender =
1226
CTL.HackForStmt(CTL.FORWARD,CTL.NONSTRICT,
1227
ctl_and CTL.NONSTRICT label_pred
1228
(make_raw_match label false ast),
1229
ctl_and CTL.NONSTRICT (matcher d) prelabel_pred) in
1230
(label_var::fvs,
1231
function f -> ctl_and CTL.NONSTRICT label_pred (f ender))
1213
1232
| _ ->
1214
1233
(* more safe but less efficient *)
1215
1234
let first_metamatch = matcher d in
1221
1240
| Ast.PLUS -> failwith "not possible") in
1222
1241
let rest_nodes = ctl_and CTL.NONSTRICT rest_metamatch prelabel_pred in
1223
1242
let last_node = and_after guard (ctl_not prelabel_pred) after in
1224
(ctl_and CTL.NONSTRICT (make_raw_match label false ast)
1225
(make_seq guard
1226
[first_metamatch;
1227
ctl_au CTL.NONSTRICT rest_nodes last_node])) in
1228
let body f = ctl_and CTL.NONSTRICT label_pred (f ender) in
1229
let stmt_fvs = Ast.get_fvs stmt in
1230
let fvs = get_unquantified quantified stmt_fvs in
1231
quantify guard (label_var::fvs)
1243
let ender =
1244
ctl_and CTL.NONSTRICT (make_raw_match label false ast)
1245
(make_seq guard
1246
[first_metamatch;
1247
ctl_au CTL.NONSTRICT rest_nodes last_node]) in
1248
(label_var::fvs,
1249
function f -> ctl_and CTL.NONSTRICT label_pred (f ender)) in
1250
quantify guard new_fvs
1232
1251
(sequencibility body label_pred process_bef_aft seqible)
1233
1252
1234
1253
(* --------------------------------------------------------------------- *)
1235
1254
(* dots and nests *)
1236
1255
1237
let dots_au is_strict toend label s wrapcode x seq_after y quantifier =
1256
let dots_au is_strict toend label s wrapcode n x seq_after y quantifier =
1238
1257
let matchgoto = gotopred None in
1239
1258
let matchbreak =
1240
1259
make_match None false
1253
1272
then Common.Left(aftpred label)
1254
1273
else
1255
1274
Common.Right
1256
(function v ->
1275
(function vx -> function v ->
1276
(* vx is the contents of the nest, if any. we can only stop early
1277
if we find neither the ending code nor the nest contents in
1278
the if branch. not sure if this is a good idea. *)
1257
1279
let lv = get_label_ctr() in
1258
1280
let labelpred = CTL.Pred(Lib_engine.Label lv,CTL.Control) in
1259
1281
let preflabelpred = label_pred_maker (Some (lv,ref true)) in
1262
1284
(ctl_and CTL.NONSTRICT
1263
1285
(ctl_and CTL.NONSTRICT (truepred label) labelpred)
1264
1286
(ctl_au CTL.NONSTRICT
1265
(ctl_and CTL.NONSTRICT (ctl_not v) preflabelpred)
1287
(ctl_and CTL.NONSTRICT (ctl_not v)
1288
(ctl_and CTL.NONSTRICT vx preflabelpred))
1266
1289
(ctl_and CTL.NONSTRICT preflabelpred
1267
1290
(if !Flag_matcher.only_return_is_error_exit
1268
1291
then
1280
1303
let v = get_let_ctr() in
1281
1304
op s x
1282
1305
(match stop_early with
1283
Common.Left x -> ctl_or y x
1306
Common.Left x1 -> ctl_or y x1
1284
1307
| Common.Right stop_early ->
1285
CTL.Let(v,y,ctl_or (CTL.Ref v) (stop_early (CTL.Ref v))))
1308
CTL.Let(v,y,
1309
ctl_or (CTL.Ref v)
1310
(stop_early n (CTL.Ref v))))
1286
1311
1287
1312
let rec dots_and_nests plus nest whencodes bef aft dotcode after label
1288
1313
process_bef_aft statement_list statement guard quantified wrapcode =
1341
1366
| Ast.WhenNotFalse(e) ->
1342
1367
(poswhen,
1343
1368
ctl_or (whencond_false e label guard quantified) negwhen))
1344
(CTL.True,bef_aft) (List.rev whencodes) in
1369
(CTL.True,CTL.False(*bef_aft*)) (List.rev whencodes) in
1370
(*bef_aft modifies arg so that inside of a nest can't cause the next
1371
to overshoot its boundaries, eg a() <...f()...> b() where f is
1372
a metavariable and the whole thing matches code in a loop;
1373
don't want f to match eg b(), allowing to go around the loop again*)
1345
1374
let poswhen = ctl_and_ns arg poswhen in
1346
1375
let negwhen =
1347
1376
(* if !exists
1360
1389
on the "true" in between code *)
1361
1390
let plus_var = if plus then get_label_ctr() else string2var "" in
1362
1391
let plus_var2 = if plus then get_label_ctr() else string2var "" in
1363
let ornest =
1392
let (ornest,just_nest) =
1393
(* just_nest is used when considering whether to stop early, to continue
1394
to collect nest information in the if branch *)
1364
1395
match (nest,guard && not plus) with
1365
(None,_) | (_,true) -> whencodes CTL.True
1396
(None,_) | (_,true) -> (whencodes CTL.True,CTL.True)
1366
1397
| (Some nest,false) ->
1367
1398
let v = get_let_ctr() in
1368
1399
let is_plus x =
1379
1410
CTL.Pred(Lib_engine.BindGood(plus_var),
1380
1411
CTL.Modif plus_var2)))
1381
1412
else x in
1382
CTL.Let(v,nest,
1383
CTL.Or(is_plus (CTL.Ref v),
1384
whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
1413
let body =
1414
CTL.Let(v,nest,
1415
CTL.Or(is_plus (CTL.Ref v),
1416
whencodes (CTL.Not(ctl_uncheck (CTL.Ref v))))) in
1417
(body,body) in
1385
1418
let plus_modifier x =
1386
1419
if plus
1387
1420
then
1417
1450
else exit (* end at the real end of the function *) *) in
1418
1451
plus_modifier
1419
1452
(dots_au is_strict ((after = Tail) or (after = VeryEnd))
1420
label (guard_to_strict guard) wrapcode
1421
(ctl_and_ns dotcode (ctl_and_ns ornest labelled))
1453
label (guard_to_strict guard) wrapcode just_nest
1454
(ctl_and_ns dotcode
1455
(ctl_and_ns (ctl_and_ns (ctl_not bef_aft) ornest) labelled))
1422
1456
aft ender quantifier)
1423
1457
1424
1458
and get_whencond_exps e =
1748
1782
(quantify guard b2fvs
1749
1783
(statement_list body Tail
1750
1784
new_quantified2 new_mquantified2
1751
(Some (lv,ref true))
1785
None(*no label because past the goto*)
1752
1786
llabel slabel false guard))])) in
1753
1787
ctl_or pattern_as_given (ctl_or pattern2 pattern3)
1754
1788
else pattern_as_given
1766
1800
label statement make_match guard
1767
1801
1768
1802
| Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *)
1769
ctl_and
1770
(label_pred_maker label)
1803
(*ctl_and seems pointless, disjuncts see label too
1804
(label_pred_maker label)*)
1771
1805
(List.fold_left ctl_seqor CTL.False
1772
1806
(List.map
1773
1807
(function sl ->
2022
2056
Common.union_set mb1fvs
2023
2057
(Common.union_set mb2fvs
2024
2058
(Common.union_set mb3fvs minus_quantified)) in
2025
let fn_nest =
2059
let optim1 =
2026
2060
match (Ast.undots body,
2027
2061
contains_modif rbrace or contains_pos rbrace) with
2028
2062
([body],false) ->
2029
2063
(match Ast.unwrap body with
2030
Ast.Nest(stmt_dots,[],multi,_,_) ->
2031
if multi
2032
then None (* not sure how to optimize this case *)
2033
else Some (Common.Left stmt_dots)
2034
| Ast.Dots(_,whencode,_,_) when
2064
Ast.Nest(stmt_dots,[],false,_,_) ->
2065
(* special case for function header + body - header is unambiguous
2066
and unique, so we can just look for the nested body anywhere
2067
else in the CFG *)
2068
Some
2069
(CTL.AndAny
2070
(CTL.FORWARD,guard_to_strict guard,start_brace,
2071
statement_list stmt_dots
2072
(* discards match on right brace, but don't need it *)
2073
(Guard (make_seq_after end_brace after))
2074
new_quantified3 new_mquantified3
2075
None llabel slabel true guard))
2076
| Ast.Dots((_,i,d,_),whencode,_,_) when
2035
2077
(List.for_all
2036
2078
(* flow sensitive, so not optimizable *)
2037
2079
(function Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2038
2080
false
2039
2081
| _ -> true) whencode) ->
2040
Some (Common.Right whencode)
2041
| _ -> None)
2042
| _ -> None in
2043
let body_code =
2044
match fn_nest with
2045
Some (Common.Left stmt_dots) ->
2046
(* special case for function header + body - header is unambiguous
2047
and unique, so we can just look for the nested body anywhere
2048
else in the CFG *)
2049
CTL.AndAny
2050
(CTL.FORWARD,guard_to_strict guard,start_brace,
2051
statement_list stmt_dots
2052
(* discards match on right brace, but don't need it *)
2053
(Guard (make_seq_after end_brace after))
2054
new_quantified3 new_mquantified3
2055
None llabel slabel true guard)
2056
| Some (Common.Right whencode) ->
2057
(* try to be more efficient for the case where the body is just
2082
(* try to be more efficient for the case where the body is just
2058
2083
... Perhaps this is too much of a special case, but useful
2059
2084
for dropping a parameter and checking that it is never used. *)
2060
make_seq
2061
[start_brace;
2062
match whencode with
2063
[] -> CTL.True
2064
| _ ->
2065
let leftarg =
2066
ctl_and
2067
(ctl_not
2068
(List.fold_left
2069
(function prev ->
2070
function
2071
Ast.WhenAlways(s) -> prev
2072
| Ast.WhenNot(sl) ->
2073
let x =
2074
statement_list sl Tail
2075
new_quantified3 new_mquantified3
2076
label llabel slabel true true in
2077
ctl_or prev x
2078
| Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2079
failwith "unexpected"
2080
| Ast.WhenModifier(Ast.WhenAny) -> CTL.False
2081
| Ast.WhenModifier(_) -> prev)
2082
CTL.False whencode))
2083
(List.fold_left
2084
(function prev ->
2085
function
2086
Ast.WhenAlways(s) ->
2087
let x =
2088
statement s Tail
2089
new_quantified3 new_mquantified3
2090
label llabel slabel true in
2091
ctl_and prev x
2092
| Ast.WhenNot(sl) -> prev
2093
| Ast.WhenNotTrue(_) | Ast.WhenNotFalse(_) ->
2094
failwith "unexpected"
2095
| Ast.WhenModifier(Ast.WhenAny) -> CTL.True
2096
| Ast.WhenModifier(_) -> prev)
2097
CTL.True whencode) in
2098
ctl_au leftarg (make_match stripped_rbrace)]
2099
| None ->
2085
(match d with
2086
Ast.MINUS(_,_,_,_) -> None
2087
| _ ->
2088
Some (
2089
make_seq
2090
[start_brace;
2091
match whencode with
2092
[] -> CTL.True
2093
| _ ->
2094
let leftarg =
2095
ctl_and
2096
(ctl_not
2097
(List.fold_left
2098
(function prev ->
2099
function
2100
Ast.WhenAlways(s) -> prev
2101
| Ast.WhenNot(sl) ->
2102
let x =
2103
statement_list sl Tail
2104
new_quantified3
2105
new_mquantified3
2106
label llabel slabel
2107
true true in
2108
ctl_or prev x
2109
| Ast.WhenNotTrue(_)
2110
| Ast.WhenNotFalse(_) ->
2111
failwith "unexpected"
2112
| Ast.WhenModifier
2113
(Ast.WhenAny) -> CTL.False
2114
| Ast.WhenModifier(_) -> prev)
2115
CTL.False whencode))
2116
(List.fold_left
2117
(function prev ->
2118
function
2119
Ast.WhenAlways(s) ->
2120
let x =
2121
statement s Tail
2122
new_quantified3
2123
new_mquantified3
2124
label llabel slabel true in
2125
ctl_and prev x
2126
| Ast.WhenNot(sl) -> prev
2127
| Ast.WhenNotTrue(_)
2128
| Ast.WhenNotFalse(_) ->
2129
failwith "unexpected"
2130
| Ast.WhenModifier(Ast.WhenAny) ->
2131
CTL.True
2132
| Ast.WhenModifier(_) -> prev)
2133
CTL.True whencode) in
2134
ctl_au leftarg (make_match stripped_rbrace)]))
2135
| _ -> None)
2136
| _ -> None in
2137
let optim2 =
2138
(* function body is all minus, no whencode *)
2139
match Ast.undots body with
2140
[body] ->
2141
(match Ast.unwrap body with
2142
Ast.Dots
2143
((_,i,(Ast.MINUS(_,_,_,[]) as d),_),[],_,_) ->
2144
(match (Ast.unwrap lbrace,Ast.unwrap rbrace) with
2145
(Ast.SeqStart((_,_,Ast.MINUS(_,_,_,[]),_)),
2146
Ast.SeqEnd((_,_,Ast.MINUS(_,_,_,[]),_)))
2147
when not (contains_pos rbrace) ->
2148
Some
2149
(* andany drops everything to the end, including close
2150
braces - not just function body, could check
2151
label to keep braces *)
2152
(ctl_and start_brace
2153
(ctl_ax
2154
(CTL.AndAny
2155
(CTL.FORWARD,guard_to_strict guard,CTL.True,
2156
make_match
2157
(make_meta_rule_elem d ([],[],[]))))))
2158
| _ -> None)
2159
| _ -> None)
2160
| _ -> None in
2161
let body_code =
2162
match (optim1,optim2) with
2163
(Some o1,_) -> o1
2164
| (_,Some o2) -> o2
2165
| _ ->
2100
2166
make_seq
2101
2167
[start_brace;
2102
2168
quantify guard b3fvs
2224
2290
(* --------------------------------------------------------------------- *)
2225
2291
(* Function declaration *)
2226
2292
2227
let top_level name (ua,pos) t =
2293
(* ua = used_after, fua = fresh_used_after, fuas = fresh_used_after_seeds *)
2294
2295
let top_level name ((ua,pos),fua) (fuas,t) =
2228
2296
let ua = List.filter (function (nm,_) -> nm = name) ua in
2229
2297
used_after := ua;
2230
2298
saved := Ast.get_saved t;
2231
let quantified = Common.minus_set ua pos in
2299
let quantified = Common.minus_set (Common.union_set ua fuas) pos in
2232
2300
quantify false quantified
2233
2301
(match Ast.unwrap t with
2234
2302
Ast.FILEINFO(old_file,new_file) -> failwith "not supported fileinfo"
2272
2340
(* --------------------------------------------------------------------- *)
2273
2341
(* Entry points *)
2274
2342
2275
let asttoctlz (name,(_,_,exists_flag),l) used_after positions =
2343
let asttoctlz (name,(_,_,exists_flag),l)
2344
(used_after,fresh_used_after,fresh_used_after_seeds) positions =
2276
2345
letctr := 0;
2277
2346
labelctr := 0;
2278
2347
(match exists_flag with
2279
2348
Ast.Exists -> exists := Exists
2280
2349
| Ast.Forall -> exists := Forall
2281
| Ast.ReverseForall -> exists := ReverseForall
2282
2350
| Ast.Undetermined ->
2283
2351
exists := if !Flag.sgrep_mode2 then Exists else Forall);
2284
2352
2288
2356
(function (t,_) ->
2289
2357
match Ast.unwrap t with Ast.ERRORWORDS(exps) -> false | _ -> true)
2290
2358
(List.combine l (List.combine used_after positions))) in
2291
let res = List.map2 (top_level name) used_after l in
2359
let res =
2360
List.map2 (top_level name)
2361
(List.combine used_after fresh_used_after)
2362
(List.combine fresh_used_after_seeds l) in
2292
2363
exists := Forall;
2293
2364
res
2294
2365
Loggerhead is a web-based interface for Breezy
Version: 2.0.1