The attached patch "solves" the problem reported by Peter Tummeltshammer
about spatch being slow when removing a single statement from a function
containing many complex switch statements.
The problem is in the code that checks for inconsistent paths, ie a node
that is reachable from the nodes matched by the semantic patch, but also
reachable from nodes not matched by the semantic patch. When the
control-flow structure of the function is very complicated, this test
turns out to be very very complicated.
The "solution" was just to drop the test in the case that one one node is
matched at a time, in which case there is no possible inconsistent path
problem. But this means that it will not be possible to apply a more
complicated pattern, ie including ... to such code. The only solution
would be to use the option -allow_inconsistent_paths, in which case one
should check the result very carefully to be sure that there are no such
inconsistent paths. The other solution, if working on a whole directory,
is to use the option -timeout for some reasonable number of seconds. That
way, a file containing such a complicated function will time out and have
to be treated by hand, but the treatment of other files will benefit from
the inconsistent paths check.
julia
diff -u -p a/engine/check_reachability.ml b/engine/check_reachability.ml
--- a/engine/check_reachability.ml 2010-03-12 16:34:04.000000000 +0100
+++ b/engine/check_reachability.ml 2010-03-13 08:47:36.000000000 +0100
@@ -91,19 +91,24 @@ let create_formulas _ =
let match_roots =
List.map (function n -> Ast_ctl.Pred(Node(n)))
(List.sort compare !roots) in
- let roots =
+ let or_roots =
List.fold_left
(function prev -> function cur -> Ast_ctl.Or(prev,cur))
(List.hd match_roots) (List.tl match_roots) in
- (node,
- Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT,
- Ast_ctl.Or(roots,Ast_ctl.Pred(After))),
- Ast_ctl.And
- (Ast_ctl.NONSTRICT,
- Ast_ctl.Not(roots),
- Ast_ctl.EX
- (Ast_ctl.BACKWARD,
- Ast_ctl.EU(Ast_ctl.BACKWARD,roots,match_node))))
+ (* no point to search if no path, and the presence of after
+ in the AF formula can make things slow *)
+ if List.mem node !roots
+ then acc
+ else
+ (node,
+ Ast_ctl.AF(Ast_ctl.BACKWARD,Ast_ctl.NONSTRICT,
+ Ast_ctl.Or(or_roots,Ast_ctl.Pred(After))),
+ Ast_ctl.And
+ (Ast_ctl.NONSTRICT,
+ Ast_ctl.Not(or_roots),
+ Ast_ctl.EX
+ (Ast_ctl.BACKWARD,
+ Ast_ctl.EU(Ast_ctl.BACKWARD,or_roots,match_node))))
(*exef
(wrap(Ast_ctl.And(Ast_ctl.NONSTRICT,match_node,exef(roots))))*)
:: acc)
_______________________________________________
Cocci mailing list
[email protected]
http://lists.diku.dk/mailman/listinfo/cocci
(Web access from inside DIKUs LAN only)
