Hi there, I would like to show you my efforts on adding the missing dowhile loop in SmPL. The following code consist of the functional part and tests part. So far, it works well, the tests set have most cases that come to my mind.
Cause I have some problem with the latest master code, the patch was generated by rebasing from a old version. I think it's rustic and I could use your professional suggestions to refine the code and complete the test set. Thx! Yimin
From 8d2c25f0a41cf67e80bde07cfdae5b9abe8d6823 Mon Sep 17 00:00:00 2001 From: tacinight <tacing...@gmail.com> Date: Mon, 22 Apr 2019 21:09:59 +0800 Subject: [PATCH] add dowhile support Signed-off-by: tacinight <tacing...@gmail.com> --- engine/asttoctl2.ml | 43 +++++++++++++++++++++++++++++++++++++++++ engine/asttomember.ml | 5 +++++ parsing_cocci/adjacency.ml | 3 +++ parsing_cocci/adjust_pragmas.ml | 6 ++++++ parsing_cocci/context_neg.ml | 5 +++++ parsing_cocci/free_vars.ml | 5 +++++ parsing_cocci/get_constants2.ml | 4 ++++ parsing_cocci/insert_plus.ml | 4 ++++ parsing_cocci/iso_pattern.ml | 7 +++++++ tests/dowhile_.c | 8 ++++++++ tests/dowhile_.cocci | 9 +++++++++ tests/dowhile_1.cocci | 9 +++++++++ tests/dowhile_2.cocci | 9 +++++++++ tests/dowhile_3.c | 10 ++++++++++ tests/dowhile_3.cocci | 9 +++++++++ tests/dowhile_4.c | 6 ++++++ tests/dowhile_4.cocci | 6 ++++++ tests/dowhile_6.c | 9 +++++++++ tests/dowhile_6.cocci | 17 ++++++++++++++++ tests/dowhile_for_complex.c | 10 ++++++++++ tests/dowhile_for_complex.cocci | 17 ++++++++++++++++ tests/dowhile_nested.c | 11 +++++++++++ tests/dowhile_nested.cocci | 11 +++++++++++ tests/dowhile_plus.c | 8 ++++++++ tests/dowhile_plus.cocci | 9 +++++++++ tests/dowhile_plus_below.cocci | 9 +++++++++ 26 files changed, 249 insertions(+) create mode 100755 tests/dowhile_.c create mode 100755 tests/dowhile_.cocci create mode 100755 tests/dowhile_1.cocci create mode 100755 tests/dowhile_2.cocci create mode 100755 tests/dowhile_3.c create mode 100755 tests/dowhile_3.cocci create mode 100644 tests/dowhile_4.c create mode 100644 tests/dowhile_4.cocci create mode 100755 tests/dowhile_6.c create mode 100755 tests/dowhile_6.cocci create mode 100755 tests/dowhile_for_complex.c create mode 100755 tests/dowhile_for_complex.cocci create mode 100755 tests/dowhile_nested.c create mode 100755 tests/dowhile_nested.cocci create mode 100755 tests/dowhile_plus.c create mode 100755 tests/dowhile_plus.cocci create mode 100755 tests/dowhile_plus_below.cocci diff --git a/engine/asttoctl2.ml b/engine/asttoctl2.ml index 814c1293..a7e0df07 100644 --- a/engine/asttoctl2.ml +++ b/engine/asttoctl2.ml @@ -1227,6 +1227,44 @@ let forwhile header body ((afvs,_,_,_) as aft) after | _ -> process()) | _ -> process() +let dowhile doheader body whiletail after quantified + minus_quantified label recurse make_match guard = + let tail_fvs = Ast.get_fvs whiletail in + let aft = ([],[],[], Ast.CONTEXT(Ast.NoPos,Ast.NOTHING)) in + let (efvs, bfvs, e1fvs) = + let header_fvs = Common.union_set (Ast.get_fvs doheader) tail_fvs in + match seq_fvs quantified [Ast.get_fvs doheader; Ast.get_fvs body; Ast.get_fvs whiletail] with + [(efvs, b1fvs);(_,b2fvs);e1fvs] -> (efvs, Common.union_set b1fvs b2fvs,e1fvs) + | _ -> failwith "asttoctl2: not possible 103" in + let new_quantified = Common.union_set bfvs quantified in + let (mefvs, mbfvs) = + let mheader_fvs = Common.union_set (Ast.get_mfvs doheader) (Ast.get_mfvs whiletail) in + match seq_fvs quantified [Ast.get_mfvs doheader; Ast.get_mfvs body; Ast.get_mfvs whiletail] with + [(efvs, b1fvs);(_,b2fvs);_] -> (efvs, Common.union_set b1fvs b2fvs) + | _ -> failwith "asttoctl2: not possible 104" in + let new_mquantified = Common.union_set mbfvs minus_quantified in + let header = quantify guard efvs (make_match doheader) in + let tailer = quantify guard efvs (make_match whiletail) in + let lv = get_label_ctr() in + let tail_branch = + ctl_and CTL.NONSTRICT tailer + (ctl_and CTL.NONSTRICT (ctl_ex (inlooppred None)) (ctl_ex (fallpred None))) in + let used = ref false in + let body = + make_seq guard + [recurse body NotTop (After (tail_branch)) new_quantified new_mquantified (Some (lv, used)) + (Some (lv, used)) None guard] in + let after_branch = aftpred None in + let or_cases after_branch = Common.Left [body; after_branch] in + let (header, wrapper) = + if !used + then + let label_pred = CTL.Pred (Lib_engine.Label(lv), CTL.Control) in + (ctl_and CTL.NONSTRICT header label_pred, (function body -> quantify true [lv] body)) + else (header, function x -> x) in + wrapper (end_control_structure bfvs header or_cases after_branch + (Some(ctl_ex after_branch)) None aft after label guard) + (* --------------------------------------------------------------------- *) (* statement metavariables *) @@ -2047,6 +2085,11 @@ and statement stmt top after quantified minus_quantified forwhile header body aft after quantified minus_quantified label statement make_match guard + | Ast.Do(doheader,body,whiletail) -> + dots_done := true; + dowhile doheader body whiletail after quantified minus_quantified + label statement make_match guard + | Ast.Disj(stmt_dots_list) -> (* list shouldn't be empty *) (*ctl_and seems pointless, disjuncts see label too (label_pred_maker label)*) diff --git a/engine/asttomember.ml b/engine/asttomember.ml index 9eb2d4b9..16669932 100644 --- a/engine/asttomember.ml +++ b/engine/asttomember.ml @@ -222,6 +222,11 @@ and statement testfn mcode tail stmt : 'a list list = then conj (rule_elem header) (statement testfn mcode tail branch) else statement testfn mcode tail branch + | Ast.Do(header,branch,whiletail) -> + if testfn header || testfn whiletail + then conj_wrapped [header;whiletail] (statement testfn mcode tail branch) + else statement testfn mcode tail branch + | Ast.Switch(header,lb,decls,cases,rb) -> let body_info = conj diff --git a/parsing_cocci/adjacency.ml b/parsing_cocci/adjacency.ml index 8c4b1529..89f54086 100644 --- a/parsing_cocci/adjacency.ml +++ b/parsing_cocci/adjacency.ml @@ -57,6 +57,9 @@ let compute_adjacency p = | Ast0.Iterator(nm,lp,args,rp,body,(info,mc,_)) -> let body = redo rp body in Ast0.Iterator(nm,lp,args,rp,body,(info,mc,!counter)) + | Ast0.Do(doo,body,tail,lp,args,rp,(str,arit,info,mc,any,_)) -> + let body = redo rp body in + Ast0.Do(doo,body,tail,lp,args,rp,(str,arit,info,mc,any,!counter)) | s -> s) in let fn = V0.rebuilder diff --git a/parsing_cocci/adjust_pragmas.ml b/parsing_cocci/adjust_pragmas.ml index 1570a108..c02fa886 100644 --- a/parsing_cocci/adjust_pragmas.ml +++ b/parsing_cocci/adjust_pragmas.ml @@ -351,6 +351,12 @@ let process = None -> Ast0.unwrap s | Some (pragmas,body) -> Ast0.Iterator(nm,lp,args,rp,body,update_before pragmas aft)) + | Ast0.Do(doo,body,tail,lp,args,rp,(a,b,info,mc,c,adj)) -> + (match right_statement body with + None -> Ast0.unwrap s + | Some (pragmas,body) -> + let (info,mc,adj) = update_before pragmas (info,mc,adj) in + Ast0.Do(doo,body,tail,lp,args,rp,(a,b,info,mc,c,adj))) | _ -> Ast0.unwrap s) in let res = V0.rebuilder diff --git a/parsing_cocci/context_neg.ml b/parsing_cocci/context_neg.ml index 154fd4f0..248701f9 100644 --- a/parsing_cocci/context_neg.ml +++ b/parsing_cocci/context_neg.ml @@ -168,6 +168,8 @@ let collect_plus_lines top = | Ast0.While(_,_,_,_,_,(info,aft,adj)) | Ast0.For(_,_,_,_,_,_,_,_,(info,aft,adj)) -> bind (k s) (mcode info aft) + | Ast0.Do(_,_,_,_,_,_,(_,_,info,aft,_,adj)) -> + bind (k s) (mcode info aft) | _ -> k s in let fn = V0.flat_combiner bind option_default @@ -512,6 +514,9 @@ let classify is_minus all_marked table code = | Ast0.For(start,_,_,_,_,_,_,_,(info,aft,adj)) -> let mcode_info (_,_,info,_,_,_) = info in bind (k s) (nc_mcode ((),(),mcode_info start,aft,(),adj)) + | Ast0.Do(start,_,_,_,_,_,(_,_,info,aft,_,adj)) -> + let mcode_info (_,_,info,_,_,_) = info in + bind (k s) (nc_mcode ((),(),mcode_info start,aft,(),adj)) | _ -> k s) in let string_fragment r k s = diff --git a/parsing_cocci/free_vars.ml b/parsing_cocci/free_vars.ml index 19fb8d27..ac768f9a 100644 --- a/parsing_cocci/free_vars.ml +++ b/parsing_cocci/free_vars.ml @@ -588,6 +588,11 @@ let collect_in_plus_term = | Ast.While(_,_,(_,_,_,aft)) | Ast.For(_,_,(_,_,_,aft)) | Ast.Iterator(_,_,(_,_,_,aft)) | Ast.FunDecl(_,_,_,_,(_,_,_,aft)) -> bind (k s) (cip_mcodekind recursor aft) + | Ast.Do(_,_,tail) -> + (match Ast.unwrap tail with + Ast.WhileTail(_,_,_,_,sem) -> (let aft = Ast.get_mcodekind sem in + bind (k s) (cip_mcodekind recursor aft)) + | _ -> k s) | _ -> k s in V.combiner bind option_default diff --git a/parsing_cocci/get_constants2.ml b/parsing_cocci/get_constants2.ml index d2e9f72e..87e949b5 100644 --- a/parsing_cocci/get_constants2.ml +++ b/parsing_cocci/get_constants2.ml @@ -691,6 +691,10 @@ let all_context = | Ast.While(_,_,ei) | Ast.For(_,_,ei) | Ast.Iterator(_,_,ei) | Ast.FunDecl(_,_,_,_,ei) -> bind (k e) (end_info ei) + | Ast.Do(_,_,whiletail) -> + (match Ast.unwrap whiletail with + Ast.WhileTail(_,_,_,_,ed) -> bind (k e) (mcode r ed) + | _ -> k e) | _ -> k e in V.combiner bind option_default diff --git a/parsing_cocci/insert_plus.ml b/parsing_cocci/insert_plus.ml index b7b50f10..7b934517 100644 --- a/parsing_cocci/insert_plus.ml +++ b/parsing_cocci/insert_plus.ml @@ -593,6 +593,8 @@ let collect_plus_nodes root = do_nothing_extra [] (info aft)mk_statement r k e | Ast0.Iterator(nm,lp,args,rp,body,aft) -> do_nothing_extra [] (info aft) mk_statement r k e + | Ast0.Do(doo,body,tail,lp,exp,rp,(_,_,inf,aft,_,adj)) -> + do_nothing_extra [] (info (inf,aft,adj)) mk_statement r k e | _ -> do_nothing mk_statement r k e in (* statementTag is preferred, because it indicates that one statement is @@ -1168,6 +1170,8 @@ let reevaluate_contextness = donothing_extra (info aft) r k e | Ast0.Iterator(nm,lp,args,rp,body,aft) -> donothing_extra (info aft) r k e + | Ast0.Do(doo,body,tail,lp,args,rb,(_,_,inf,mck,_,adj)) -> + donothing_extra (info (inf,mck,adj)) r k e | _ -> donothing r k e in let res = diff --git a/parsing_cocci/iso_pattern.ml b/parsing_cocci/iso_pattern.ml index 0ddad5e0..8b3cae70 100644 --- a/parsing_cocci/iso_pattern.ml +++ b/parsing_cocci/iso_pattern.ml @@ -1616,6 +1616,8 @@ let rebuild_mcode start_line = (info,copy_mcodekind mc,adj)) | Ast0.Iterator(nm,lp,args,rp,body,(info,mc,adj)) -> Ast0.Iterator(nm,lp,args,rp,body,(info,copy_mcodekind mc,adj)) + | Ast0.Do(doo,body,tail,lp,args,rp,(a,b,info,mc,c,adj)) -> + Ast0.Do(doo,body,tail,lp,args,rp,(a,b,info,copy_mcodekind mc,c,adj)) | Ast0.FunDecl ((info,mc),fninfo,name,lp,params,va,rp,lbrace,body,rbrace, (aftinfo,aftmc)) -> @@ -2288,6 +2290,11 @@ let extra_copy_stmt_plus model e = | Ast0.Iterator(_,_,_,_,_,(_,aft1,_)) -> merge_plus_after aft aft1 | _ -> merge_plus_after aft (Ast0.get_mcodekind e)) + | Ast0.Do(_,_,_,_,_,_,(_,_,_,aft,_,_)) -> + (match Ast0.unwrap e with + Ast0.Do(_,_,_,_,_,_,(_,_,_,aft1,_,_)) -> + merge_plus_after aft aft1 + | _ -> merge_plus_after aft (Ast0.get_mcodekind e)) | _ -> ())); e diff --git a/tests/dowhile_.c b/tests/dowhile_.c new file mode 100755 index 00000000..bbc08746 --- /dev/null +++ b/tests/dowhile_.c @@ -0,0 +1,8 @@ +int fun() { + int i = 1; + printf("message before dowhile"); + do { + i++; + } while (i < 100); + return 0; +} diff --git a/tests/dowhile_.cocci b/tests/dowhile_.cocci new file mode 100755 index 00000000..68605263 --- /dev/null +++ b/tests/dowhile_.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +expression E; +@@ + +do@p{ + ... +* } while (...); + diff --git a/tests/dowhile_1.cocci b/tests/dowhile_1.cocci new file mode 100755 index 00000000..d15bbdae --- /dev/null +++ b/tests/dowhile_1.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +statement S; +@@ + +do@p{ + ... +* } while (...); +* S \ No newline at end of file diff --git a/tests/dowhile_2.cocci b/tests/dowhile_2.cocci new file mode 100755 index 00000000..c6e69eb1 --- /dev/null +++ b/tests/dowhile_2.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +statement S; +@@ + +* S +* do@p{ + ... +} while (...); diff --git a/tests/dowhile_3.c b/tests/dowhile_3.c new file mode 100755 index 00000000..c2d90e3c --- /dev/null +++ b/tests/dowhile_3.c @@ -0,0 +1,10 @@ +int fun() { + int i = 1; + int* ptr; + ptr = kmalloc(100); + do { + *(ptr + i) = i++; + } while (i < 100); + + return 0; +} \ No newline at end of file diff --git a/tests/dowhile_3.cocci b/tests/dowhile_3.cocci new file mode 100755 index 00000000..a21d0b18 --- /dev/null +++ b/tests/dowhile_3.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +identifier m; +@@ + +* m = kmalloc(...); +* do@p{ + <...m...> +} while (...); diff --git a/tests/dowhile_4.c b/tests/dowhile_4.c new file mode 100644 index 00000000..c1984021 --- /dev/null +++ b/tests/dowhile_4.c @@ -0,0 +1,6 @@ +int fun() { + do { + printf("dummy message"); + } while (0); + printf("done printing"); +} \ No newline at end of file diff --git a/tests/dowhile_4.cocci b/tests/dowhile_4.cocci new file mode 100644 index 00000000..c69a23de --- /dev/null +++ b/tests/dowhile_4.cocci @@ -0,0 +1,6 @@ +@rule1@ +statement S1, S2; +@@ + +S1 +* S2 \ No newline at end of file diff --git a/tests/dowhile_6.c b/tests/dowhile_6.c new file mode 100755 index 00000000..1827305a --- /dev/null +++ b/tests/dowhile_6.c @@ -0,0 +1,9 @@ +int fun() { + int i = 1; + printf("start of dowhile"); + do { + i++; + } while (i < 100); + printf("end of dowhile"); + return 0; +} \ No newline at end of file diff --git a/tests/dowhile_6.cocci b/tests/dowhile_6.cocci new file mode 100755 index 00000000..6e839811 --- /dev/null +++ b/tests/dowhile_6.cocci @@ -0,0 +1,17 @@ +@dowhile_constant@ +position p; +constant C; +@@ + +do@p{ + ... +* } while (C); + +@dowhile_exp@ +position p; +expression E; +@@ + +do@p{ + ... +* } while (E); diff --git a/tests/dowhile_for_complex.c b/tests/dowhile_for_complex.c new file mode 100755 index 00000000..44ed7734 --- /dev/null +++ b/tests/dowhile_for_complex.c @@ -0,0 +1,10 @@ +int fun() { + int i = 1, j = 1; + do { + i++; + for (j = 1; j < 100; j++) { + ++j; + } + } while (i < 100); + return 0; +} \ No newline at end of file diff --git a/tests/dowhile_for_complex.cocci b/tests/dowhile_for_complex.cocci new file mode 100755 index 00000000..14f4afd6 --- /dev/null +++ b/tests/dowhile_for_complex.cocci @@ -0,0 +1,17 @@ +@nested@ +position p; +statement S; +@@ + +do@p{ + <+... +* for(...;...;...) S + ...+> +} while (...); + +@script:python@ +p << nested.p; +n << nested.S; +@@ + +print("nested [%s](%s#%s)" % (n, p[0].file, p[0].line)) \ No newline at end of file diff --git a/tests/dowhile_nested.c b/tests/dowhile_nested.c new file mode 100755 index 00000000..2b495855 --- /dev/null +++ b/tests/dowhile_nested.c @@ -0,0 +1,11 @@ +int fun() { + int i = 1, j = 1; + do { + i++; + do { + j++; + } while (j < 100); + printf(“end of innner dowhile”); + } while (i < 100); + return 0; +} diff --git a/tests/dowhile_nested.cocci b/tests/dowhile_nested.cocci new file mode 100755 index 00000000..b1fd1d39 --- /dev/null +++ b/tests/dowhile_nested.cocci @@ -0,0 +1,11 @@ +@nested@ +position p; +statement S; +@@ + +do@p{ + S + <+... +* do {...} while(...); + ...+> +* } while (...); diff --git a/tests/dowhile_plus.c b/tests/dowhile_plus.c new file mode 100755 index 00000000..c25ada03 --- /dev/null +++ b/tests/dowhile_plus.c @@ -0,0 +1,8 @@ +int fun() { + int i = 1; + do { + i++; + } + while (i < 100); + return 0; +} diff --git a/tests/dowhile_plus.cocci b/tests/dowhile_plus.cocci new file mode 100755 index 00000000..9d53861f --- /dev/null +++ b/tests/dowhile_plus.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +statement S; +@@ + +do@p { + ... ++ print("message"); + } while (...); \ No newline at end of file diff --git a/tests/dowhile_plus_below.cocci b/tests/dowhile_plus_below.cocci new file mode 100755 index 00000000..d1f5a036 --- /dev/null +++ b/tests/dowhile_plus_below.cocci @@ -0,0 +1,9 @@ +@dowhile@ +position p; +statement S; +@@ + +do@p { + ... + } while (...); ++ print("message"); \ No newline at end of file -- 2.11.0
_______________________________________________ Cocci mailing list Cocci@systeme.lip6.fr https://systeme.lip6.fr/mailman/listinfo/cocci