From 4c3c3328e0ebd9c90bf545a2c7b096b42474ff5a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 20 Feb 2024 17:13:59 +0200 Subject: [PATCH 01/14] Remove duplicate matching in loop unrolling visitor --- src/util/loopUnrolling.ml | 40 +++++++++++++++++++-------------------- 1 file changed, 19 insertions(+), 21 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 519477557b..55e72ee62a 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -445,32 +445,30 @@ class loopUnrollingVisitor(func, totalLoops) = object inherit nopCilVisitor method! vstmt s = - match s.skind with - | Loop (b,loc, loc2, break , continue) -> - let duplicate_and_rem_labels s = + let duplicate_and_rem_labels s = + match s.skind with + | Loop (b,loc, loc2, break , continue) -> let factor = loop_unrolling_factor s func totalLoops in if(factor > 0) then ( Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor; annotateArrays b; - match s.skind with - | Loop (b,loc, loc2, break , continue) -> - (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) - let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in - (* continues should go to the next unrolling *) - let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in - (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) - let current_continue_target = ref dummyStmt in - let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in - let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - let copies = List.init (factor) (fun i -> - current_continue_target := continue_target i; - mkStmt (Block (mkBlock [one_copy (); !current_continue_target]))) - in - mkStmt (Block (mkBlock (copies@[s]@[break_target]))) - | _ -> failwith "invariant broken" + (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) + let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in + (* continues should go to the next unrolling *) + let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in + (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) + let current_continue_target = ref dummyStmt in + let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in + let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in + let copies = List.init (factor) (fun i -> + current_continue_target := continue_target i; + mkStmt (Block (mkBlock [one_copy (); !current_continue_target]))) + in + mkStmt (Block (mkBlock (copies@[s]@[break_target]))) ) else s (*no change*) - in ChangeDoChildrenPost(s, duplicate_and_rem_labels); - | _ -> DoChildren + | _ -> s + in + ChangeDoChildrenPost(s, duplicate_and_rem_labels) end let unroll_loops fd totalLoops = From c4e2f31240efe5c85b37852d38e4b659adbd85fa Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 20 Feb 2024 17:48:26 +0200 Subject: [PATCH 02/14] Add clean justcil output --- src/common/util/cilfacade.ml | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 9d2f8b2d3a..3df3a71ae5 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -66,8 +66,27 @@ let parse fileName = E.s (E.error "There were parsing errors in %s" fileName_str); file +class myCilPrinter = +object + inherit defaultCilPrinterClass as super + + method! pLineDirective ?(forcefile=false) l = + Pretty.nil + + method! pGlobal () (g: global) = + match g with + | GVarDecl (vi, l) when Hashtbl.mem builtinFunctions vi.vname -> Pretty.nil + | _ -> super#pGlobal () g +end + +let dumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file = + Pretty.printDepth := 99999; + Pretty.fastMode := true; + iterGlobals file (fun g -> dumpGlobal pp out g); + flush out + let print (fileAST: file) = - dumpFile defaultCilPrinter stdout "stdout" fileAST + dumpFile (new myCilPrinter) stdout "stdout" fileAST let rmTemps fileAST = RmUnused.removeUnused fileAST From b3ff1cb4f466686d5e37c8a689cc3989492f5a20 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 20 Feb 2024 17:55:08 +0200 Subject: [PATCH 03/14] Add unrolling cram tests --- .../55-loop-unrolling/01-simple-cases.t | 1355 +++++++++++++++++ tests/regression/55-loop-unrolling/02-break.t | 176 +++ .../55-loop-unrolling/03-break-right-place.t | 104 ++ .../regression/55-loop-unrolling/04-simple.t | 86 ++ .../55-loop-unrolling/05-continue.t | 128 ++ .../06-simple-cases-unrolled.t | 1355 +++++++++++++++++ .../55-loop-unrolling/07-nested-unroll.t | 923 +++++++++++ tests/regression/55-loop-unrolling/08-bad.t | 58 + tests/regression/55-loop-unrolling/09-weird.t | 62 + tests/regression/55-loop-unrolling/dune | 2 + 10 files changed, 4249 insertions(+) create mode 100644 tests/regression/55-loop-unrolling/01-simple-cases.t create mode 100644 tests/regression/55-loop-unrolling/02-break.t create mode 100644 tests/regression/55-loop-unrolling/03-break-right-place.t create mode 100644 tests/regression/55-loop-unrolling/04-simple.t create mode 100644 tests/regression/55-loop-unrolling/05-continue.t create mode 100644 tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t create mode 100644 tests/regression/55-loop-unrolling/07-nested-unroll.t create mode 100644 tests/regression/55-loop-unrolling/08-bad.t create mode 100644 tests/regression/55-loop-unrolling/09-weird.t create mode 100644 tests/regression/55-loop-unrolling/dune diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t new file mode 100644 index 0000000000..30d393eec2 --- /dev/null +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -0,0 +1,1355 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 01-simple-cases.c + [Info] unrolling loop at 01-simple-cases.c:27:5-30:5 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:42:5-45:19 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:57:5-60:5 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:74:5-80:5 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:95:5-105:5 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:119:5-123:5 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:143:2-146:2 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:160:9-163:9 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:157:2-165:2 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:174:2-178:2 with factor 5 + [Info] unrolling loop at 01-simple-cases.c:187:2-194:2 with factor 5 + extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int global ; + void example1(void) ; + void example2(void) ; + void example3(void) ; + void example4(void) ; + void example5(void) ; + void example6(void) ; + void example7(void) ; + void example8(void) ; + void example9(void) ; + void example10(void) ; + int main(void) + { + + + { + example1(); + example2(); + example3(); + example4(); + example5(); + example6(); + example7(); + example8(); + example9(); + example10(); + return (0); + } + } + void example1(void) + { + int a[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 3); + return; + } + } + void example2(void) + { + int a[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_0: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_1: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_2: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_3: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + a[i] = i; + i ++; + if (! (i <= 5)) { + goto while_break; + } + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 3); + return; + } + } + void example3(void) + { + int a[10] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(a[7] == 0); + return; + } + } + void example4(void) + { + int a[10] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + first_iteration = 1; + { + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 10)) { + goto while_break; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(first_iteration == 0); + return; + } + } + void example5(void) + { + int a[4] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int top __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + top = 0; + { + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 4)) { + goto while_break; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(top == 6); + return; + } + } + void example6(void) + { + int a[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int top ; + + { + i = 0; + top = 0; + { + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 3)) { + goto while_break; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(top == 6); + return; + } + } + int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; + int update(int i ) + { + + + { + if (i > 5) { + return (0); + } else { + return (1); + } + } + } + void example7(void) + { + int a[10] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + tmp = update(i); + if (! tmp) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[6] == 0); + return; + } + } + void example8(void) + { + int a[5] ; + int b[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j __attribute__((__goblint_array_domain__("unroll"))) ; + + { + b[0] = 0; + b[1] = 0; + b[2] = 0; + b[3] = 0; + b[4] = 0; + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___0: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break; + } + b[j] += a[i]; + j ++; + } + while_break: /* CIL Label */ ; + } + loop_end___1: ; + } + i ++; + } + loop_continue_0___0: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___1: ; + } + { + while (1) { + while_continue___0: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___0; + } + b[j] += a[i]; + j ++; + } + while_break___0: /* CIL Label */ ; + } + loop_end___2: ; + } + i ++; + } + loop_continue_1___1: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___2: ; + } + { + while (1) { + while_continue___1: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___1; + } + b[j] += a[i]; + j ++; + } + while_break___1: /* CIL Label */ ; + } + loop_end___3: ; + } + i ++; + } + loop_continue_2___2: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___3: ; + } + { + while (1) { + while_continue___2: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___2; + } + b[j] += a[i]; + j ++; + } + while_break___2: /* CIL Label */ ; + } + loop_end___4: ; + } + i ++; + } + loop_continue_3___3: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___5: ; + } + { + while (1) { + while_continue___3: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___3; + } + b[j] += a[i]; + j ++; + } + while_break___3: /* CIL Label */ ; + } + loop_end___5: ; + } + i ++; + } + loop_continue_4___4: ; + } + { + while (1) { + while_continue___4: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break___4; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_0: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_1: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_2: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_3: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue___5: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___5; + } + b[j] += a[i]; + j ++; + } + while_break___5: /* CIL Label */ ; + } + loop_end: ; + } + i ++; + } + while_break___4: /* CIL Label */ ; + } + loop_end___0: ; + } + return; + } + } + void example9(void) + { + int a[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_0: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_1: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_2: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_3: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! 1) { + goto while_break; + } + a[i] = i; + i ++; + if (i == 5) { + goto while_break; + } + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + return; + } + } + void example10(void) + { + int a[5] ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + if (i == 3) { + i ++; + goto while_continue; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + return; + } + } diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t new file mode 100644 index 0000000000..fa3aba7f69 --- /dev/null +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -0,0 +1,176 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 02-break.c + [Info] unrolling loop at 02-break.c:6:5-15:2 with factor 5 + extern void __goblint_check(int exp ) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int main(void) + { + int r __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + r = 5; + i = 0; + { + { + { + if (! (i < 2)) { + goto loop_end; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break; + case_0: /* CIL Label */ + goto loop_end; + case_1: /* CIL Label */ + r = 8; + switch_break: /* CIL Label */ ; + } + r = 17; + goto loop_end; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 2)) { + goto loop_end; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break___0; + case_0___0: /* CIL Label */ + goto loop_end; + case_1___0: /* CIL Label */ + r = 8; + switch_break___0: /* CIL Label */ ; + } + r = 17; + goto loop_end; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 2)) { + goto loop_end; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break___1; + case_0___1: /* CIL Label */ + goto loop_end; + case_1___1: /* CIL Label */ + r = 8; + switch_break___1: /* CIL Label */ ; + } + r = 17; + goto loop_end; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 2)) { + goto loop_end; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break___2; + case_0___2: /* CIL Label */ + goto loop_end; + case_1___2: /* CIL Label */ + r = 8; + switch_break___2: /* CIL Label */ ; + } + r = 17; + goto loop_end; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 2)) { + goto loop_end; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break___3; + case_0___3: /* CIL Label */ + goto loop_end; + case_1___3: /* CIL Label */ + r = 8; + switch_break___3: /* CIL Label */ ; + } + r = 17; + goto loop_end; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 2)) { + goto while_break; + } + { + if (i == 0) { + goto case_0___4; + } + if (i == 1) { + goto case_1___4; + } + goto switch_break___4; + case_0___4: /* CIL Label */ + goto switch_break___4; + case_1___4: /* CIL Label */ + r = 8; + switch_break___4: /* CIL Label */ ; + } + r = 17; + goto while_break; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(r == 17); + return (0); + } + } diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t new file mode 100644 index 0000000000..d6c9f155b5 --- /dev/null +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -0,0 +1,104 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 03-break-right-place.c + [Info] unrolling loop at 03-break-right-place.c:8:5-15:5 with factor 5 + extern void __goblint_check(int exp ) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int main(void) + { + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + j = 0; + { + { + { + if (! (i < 17)) { + goto loop_end; + } + if (j == 0) { + j = 1; + goto loop_end; + } + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 17)) { + goto loop_end; + } + if (j == 0) { + j = 1; + goto loop_end; + } + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 17)) { + goto loop_end; + } + if (j == 0) { + j = 1; + goto loop_end; + } + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 17)) { + goto loop_end; + } + if (j == 0) { + j = 1; + goto loop_end; + } + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 17)) { + goto loop_end; + } + if (j == 0) { + j = 1; + goto loop_end; + } + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 17)) { + goto while_break; + } + if (j == 0) { + j = 1; + goto while_break; + } + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(i == 0); + return (0); + } + } diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t new file mode 100644 index 0000000000..c951e1b4a2 --- /dev/null +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -0,0 +1,86 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 04-simple.c + [Info] unrolling loop at 04-simple.c:10:5-13:5 with factor 5 + extern void __goblint_check(int exp ) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + void main(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 3); + return; + } + } diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t new file mode 100644 index 0000000000..b8324b1654 --- /dev/null +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -0,0 +1,128 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 05-continue.c + [Info] unrolling loop at 05-continue.c:9:5-17:5 with factor 5 + extern void __goblint_check(int exp ) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + void main(void) + { + int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + j = 0; + i = 0; + { + { + { + if (! (i < 50)) { + goto loop_end; + } + if (i < 2) { + goto __Cont___0; + } + if (i > 4) { + goto loop_end; + } + j ++; + __Cont___0: /* CIL Label */ + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 50)) { + goto loop_end; + } + if (i < 2) { + goto __Cont___1; + } + if (i > 4) { + goto loop_end; + } + j ++; + __Cont___1: /* CIL Label */ + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 50)) { + goto loop_end; + } + if (i < 2) { + goto __Cont___2; + } + if (i > 4) { + goto loop_end; + } + j ++; + __Cont___2: /* CIL Label */ + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 50)) { + goto loop_end; + } + if (i < 2) { + goto __Cont___3; + } + if (i > 4) { + goto loop_end; + } + j ++; + __Cont___3: /* CIL Label */ + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 50)) { + goto loop_end; + } + if (i < 2) { + goto __Cont___4; + } + if (i > 4) { + goto loop_end; + } + j ++; + __Cont___4: /* CIL Label */ + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 50)) { + goto while_break; + } + if (i < 2) { + goto __Cont; + } + if (i > 4) { + goto while_break; + } + j ++; + __Cont: /* CIL Label */ + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(j == 3); + return; + } + } diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t new file mode 100644 index 0000000000..1779d03476 --- /dev/null +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -0,0 +1,1355 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 06-simple-cases-unrolled.c + [Info] unrolling loop at 06-simple-cases-unrolled.c:27:5-30:5 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:42:5-45:19 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:57:5-60:5 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:74:5-80:5 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:95:5-105:5 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:119:5-123:5 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:143:2-146:2 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:160:9-163:9 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:157:2-165:2 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:174:2-178:2 with factor 5 + [Info] unrolling loop at 06-simple-cases-unrolled.c:187:2-194:2 with factor 5 + extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int global ; + void example1(void) ; + void example2(void) ; + void example3(void) ; + void example4(void) ; + void example5(void) ; + void example6(void) ; + void example7(void) ; + void example8(void) ; + void example9(void) ; + void example10(void) ; + int main(void) + { + + + { + example1(); + example2(); + example3(); + example4(); + example5(); + example6(); + example7(); + example8(); + example9(); + example10(); + return (0); + } + } + void example1(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 3); + return; + } + } + void example2(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_0: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_1: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_2: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_3: ; + } + { + { + a[i] = i; + i ++; + if (! (i <= 5)) { + goto loop_end; + } + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + a[i] = i; + i ++; + if (! (i <= 5)) { + goto while_break; + } + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 3); + return; + } + } + void example3(void) + { + int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(a[7] == 0); + return; + } + } + void example4(void) + { + int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + first_iteration = 1; + { + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 10)) { + goto loop_end; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 10)) { + goto while_break; + } + if (first_iteration == 1) { + __goblint_check(i == 0); + } else + if (i > 5) { + __goblint_check(i == 6); + } + first_iteration = 0; + a[i] = 0; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(first_iteration == 0); + return; + } + } + void example5(void) + { + int a[4] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int top __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + top = 0; + { + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 4)) { + goto loop_end; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 4)) { + goto while_break; + } + a[i] = 0; + top += i; + if (i == 2) { + __goblint_check(top == 3); + } else { + __goblint_check(top == 3); + } + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(top == 6); + return; + } + } + void example6(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int top ; + + { + i = 0; + top = 0; + { + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 3)) { + goto loop_end; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 3)) { + goto while_break; + } + a[i] = 0; + __goblint_check(a[0] == 0); + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[3] == 0); + __goblint_check(top == 6); + return; + } + } + int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; + int update(int i ) + { + + + { + if (i > 5) { + return (0); + } else { + return (1); + } + } + } + void example7(void) + { + int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + tmp = update(i); + if (! tmp) { + goto loop_end; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + tmp = update(i); + if (! tmp) { + goto while_break; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(a[0] == 0); + __goblint_check(a[6] == 0); + return; + } + } + void example8(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int b[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j __attribute__((__goblint_array_domain__("unroll"))) ; + + { + b[0] = 0; + b[1] = 0; + b[2] = 0; + b[3] = 0; + b[4] = 0; + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___0: ; + } + { + { + if (! (j < 5)) { + goto loop_end___1; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___0: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break; + } + b[j] += a[i]; + j ++; + } + while_break: /* CIL Label */ ; + } + loop_end___1: ; + } + i ++; + } + loop_continue_0___0: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___1: ; + } + { + { + if (! (j < 5)) { + goto loop_end___2; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___1: ; + } + { + while (1) { + while_continue___0: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___0; + } + b[j] += a[i]; + j ++; + } + while_break___0: /* CIL Label */ ; + } + loop_end___2: ; + } + i ++; + } + loop_continue_1___1: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___3: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___2: ; + } + { + { + if (! (j < 5)) { + goto loop_end___3; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___2: ; + } + { + while (1) { + while_continue___1: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___1; + } + b[j] += a[i]; + j ++; + } + while_break___1: /* CIL Label */ ; + } + loop_end___3: ; + } + i ++; + } + loop_continue_2___2: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___4: ; + } + { + { + if (! (j < 5)) { + goto loop_end___4; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___3: ; + } + { + while (1) { + while_continue___2: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___2; + } + b[j] += a[i]; + j ++; + } + while_break___2: /* CIL Label */ ; + } + loop_end___4: ; + } + i ++; + } + loop_continue_3___3: ; + } + { + { + if (! (i < 5)) { + goto loop_end___0; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_0___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_1___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_2___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_3___5: ; + } + { + { + if (! (j < 5)) { + goto loop_end___5; + } + b[j] += a[i]; + j ++; + } + loop_continue_4___5: ; + } + { + while (1) { + while_continue___3: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___3; + } + b[j] += a[i]; + j ++; + } + while_break___3: /* CIL Label */ ; + } + loop_end___5: ; + } + i ++; + } + loop_continue_4___4: ; + } + { + while (1) { + while_continue___4: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break___4; + } + a[i] = i; + j = 0; + { + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_0: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_1: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_2: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_3: ; + } + { + { + if (! (j < 5)) { + goto loop_end; + } + b[j] += a[i]; + j ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue___5: /* CIL Label */ ; + if (! (j < 5)) { + goto while_break___5; + } + b[j] += a[i]; + j ++; + } + while_break___5: /* CIL Label */ ; + } + loop_end: ; + } + i ++; + } + while_break___4: /* CIL Label */ ; + } + loop_end___0: ; + } + return; + } + } + void example9(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_0: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_1: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_2: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_3: ; + } + { + { + if (! 1) { + goto loop_end; + } + a[i] = i; + i ++; + if (i == 5) { + goto loop_end; + } + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! 1) { + goto while_break; + } + a[i] = i; + i ++; + if (i == 5) { + goto while_break; + } + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + return; + } + } + void example10(void) + { + int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_1: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_2: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_3: ; + } + { + { + if (! (i < 5)) { + goto loop_end; + } + if (i == 3) { + i ++; + goto loop_continue_4; + } + a[i] = i; + i ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 5)) { + goto while_break; + } + if (i == 3) { + i ++; + goto while_continue; + } + a[i] = i; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + return; + } + } diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t new file mode 100644 index 0000000000..022c1c691f --- /dev/null +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -0,0 +1,923 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 07-nested-unroll.c + [Info] unrolling loop at 07-nested-unroll.c:7:9-9:9 with factor 5 + [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5 + [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5 + [Info] unrolling loop at 07-nested-unroll.c:12:5-16:5 with factor 5 + extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int main(void) + { + int arr[10][10] __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i___0 __attribute__((__goblint_array_domain__("unroll"))) ; + int j___0 __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + { + { + { + if (! (i < 10)) { + goto loop_end___0; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end___1; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0___1: ; + } + { + { + if (! (j < 10)) { + goto loop_end___1; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1___0: ; + } + { + { + if (! (j < 10)) { + goto loop_end___1; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2___0: ; + } + { + { + if (! (j < 10)) { + goto loop_end___1; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3___0: ; + } + { + { + if (! (j < 10)) { + goto loop_end___1; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4___0: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break; + } + arr[i][j] = i + j; + j ++; + } + while_break: /* CIL Label */ ; + } + loop_end___1: ; + } + i ++; + } + loop_continue_0___0: ; + } + { + { + if (! (i < 10)) { + goto loop_end___0; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end___2; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0___2: ; + } + { + { + if (! (j < 10)) { + goto loop_end___2; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1___2: ; + } + { + { + if (! (j < 10)) { + goto loop_end___2; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2___1: ; + } + { + { + if (! (j < 10)) { + goto loop_end___2; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3___1: ; + } + { + { + if (! (j < 10)) { + goto loop_end___2; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4___1: ; + } + { + while (1) { + while_continue___0: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break___0; + } + arr[i][j] = i + j; + j ++; + } + while_break___0: /* CIL Label */ ; + } + loop_end___2: ; + } + i ++; + } + loop_continue_1___1: ; + } + { + { + if (! (i < 10)) { + goto loop_end___0; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end___3; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0___3: ; + } + { + { + if (! (j < 10)) { + goto loop_end___3; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1___3: ; + } + { + { + if (! (j < 10)) { + goto loop_end___3; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2___3: ; + } + { + { + if (! (j < 10)) { + goto loop_end___3; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3___2: ; + } + { + { + if (! (j < 10)) { + goto loop_end___3; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4___2: ; + } + { + while (1) { + while_continue___1: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break___1; + } + arr[i][j] = i + j; + j ++; + } + while_break___1: /* CIL Label */ ; + } + loop_end___3: ; + } + i ++; + } + loop_continue_2___2: ; + } + { + { + if (! (i < 10)) { + goto loop_end___0; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end___4; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0___4: ; + } + { + { + if (! (j < 10)) { + goto loop_end___4; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1___4: ; + } + { + { + if (! (j < 10)) { + goto loop_end___4; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2___4: ; + } + { + { + if (! (j < 10)) { + goto loop_end___4; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3___4: ; + } + { + { + if (! (j < 10)) { + goto loop_end___4; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4___3: ; + } + { + while (1) { + while_continue___2: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break___2; + } + arr[i][j] = i + j; + j ++; + } + while_break___2: /* CIL Label */ ; + } + loop_end___4: ; + } + i ++; + } + loop_continue_3___3: ; + } + { + { + if (! (i < 10)) { + goto loop_end___0; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end___5; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0___5: ; + } + { + { + if (! (j < 10)) { + goto loop_end___5; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1___5: ; + } + { + { + if (! (j < 10)) { + goto loop_end___5; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2___5: ; + } + { + { + if (! (j < 10)) { + goto loop_end___5; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3___5: ; + } + { + { + if (! (j < 10)) { + goto loop_end___5; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4___5: ; + } + { + while (1) { + while_continue___3: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break___3; + } + arr[i][j] = i + j; + j ++; + } + while_break___3: /* CIL Label */ ; + } + loop_end___5: ; + } + i ++; + } + loop_continue_4___4: ; + } + { + while (1) { + while_continue___4: /* CIL Label */ ; + if (! (i < 10)) { + goto while_break___4; + } + j = 0; + { + { + { + if (! (j < 10)) { + goto loop_end; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_0: ; + } + { + { + if (! (j < 10)) { + goto loop_end; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_1: ; + } + { + { + if (! (j < 10)) { + goto loop_end; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_2: ; + } + { + { + if (! (j < 10)) { + goto loop_end; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_3: ; + } + { + { + if (! (j < 10)) { + goto loop_end; + } + arr[i][j] = i + j; + j ++; + } + loop_continue_4: ; + } + { + while (1) { + while_continue___5: /* CIL Label */ ; + if (! (j < 10)) { + goto while_break___5; + } + arr[i][j] = i + j; + j ++; + } + while_break___5: /* CIL Label */ ; + } + loop_end: ; + } + i ++; + } + while_break___4: /* CIL Label */ ; + } + loop_end___0: ; + } + i___0 = 0; + { + { + { + if (! (i___0 < 5)) { + goto loop_end___7; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___8: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___7: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___7: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___7: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___7: ; + } + { + while (1) { + while_continue___6: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___6: /* CIL Label */ ; + } + loop_end___8: ; + } + i___0 ++; + } + loop_continue_0___7: ; + } + { + { + if (! (i___0 < 5)) { + goto loop_end___7; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___9: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___9: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___8: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___8: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___8: ; + } + { + while (1) { + while_continue___7: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___7; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___7: /* CIL Label */ ; + } + loop_end___9: ; + } + i___0 ++; + } + loop_continue_1___8: ; + } + { + { + if (! (i___0 < 5)) { + goto loop_end___7; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___10: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___10: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___10: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___9: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___9: ; + } + { + while (1) { + while_continue___8: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___8; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___8: /* CIL Label */ ; + } + loop_end___10: ; + } + i___0 ++; + } + loop_continue_2___9: ; + } + { + { + if (! (i___0 < 5)) { + goto loop_end___7; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___11; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___11: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___11; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___11: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___11; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___11: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___11; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___11: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___11; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___10: ; + } + { + while (1) { + while_continue___9: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___9; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___9: /* CIL Label */ ; + } + loop_end___11: ; + } + i___0 ++; + } + loop_continue_3___10: ; + } + { + { + if (! (i___0 < 5)) { + goto loop_end___7; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___12: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___12: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___12: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___12: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___12: ; + } + { + while (1) { + while_continue___10: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___10; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___10: /* CIL Label */ ; + } + loop_end___12: ; + } + i___0 ++; + } + loop_continue_4___11: ; + } + { + while (1) { + while_continue___11: /* CIL Label */ ; + if (! (i___0 < 5)) { + goto while_break___11; + } + j___0 = 0; + { + { + { + if (! (j___0 < 5)) { + goto loop_end___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_0___6: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_1___6: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_2___6: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_3___6: ; + } + { + { + if (! (j___0 < 5)) { + goto loop_end___6; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + loop_continue_4___6: ; + } + { + while (1) { + while_continue___12: /* CIL Label */ ; + if (! (j___0 < 5)) { + goto while_break___12; + } + __goblint_check(arr[i___0][j___0] == i___0 + j___0); + j___0 ++; + } + while_break___12: /* CIL Label */ ; + } + loop_end___6: ; + } + i___0 ++; + } + while_break___11: /* CIL Label */ ; + } + loop_end___7: ; + } + return (0); + } + } diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t new file mode 100644 index 0000000000..99c7f44c20 --- /dev/null +++ b/tests/regression/55-loop-unrolling/08-bad.t @@ -0,0 +1,58 @@ + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil 08-bad.c + [Info] unrolling loop at 08-bad.c:8:7-8:23 with factor 1 + [Info] unrolling loop at 08-bad.c:14:8-14:24 with factor 1 + int main(void) + { + int m ; + + { + { + goto switch_default; + { + { + { + if (! 0) { + goto loop_end; + } + } + loop_continue_0: ; + } + switch_default: /* CIL Label */ + { + while (1) { + while_continue: /* CIL Label */ ; + if (! 0) { + goto while_break; + } + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + switch_break: /* CIL Label */ ; + } + goto lab; + { + { + { + if (! 0) { + goto loop_end___0; + } + } + loop_continue_0___0: ; + } + lab: + { + while (1) { + while_continue___0: /* CIL Label */ ; + if (! 0) { + goto while_break___0; + } + } + while_break___0: /* CIL Label */ ; + } + loop_end___0: ; + } + return (0); + } + } diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t new file mode 100644 index 0000000000..82ff6d97f4 --- /dev/null +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -0,0 +1,62 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil 09-weird.c + [Info] unrolling loop at 09-weird.c:8:5-11:5 with factor 2 + extern void __goblint_check(int exp ) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + void main(void) + { + int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i __attribute__((__goblint_array_domain__("unroll"))) ; + + { + j = 0; + i = 0; + { + { + { + if (! (i < 50)) { + goto loop_end; + } + goto somelab___0; + somelab___0: + j = 8; + i ++; + } + loop_continue_0: ; + } + { + { + if (! (i < 50)) { + goto loop_end; + } + goto somelab___1; + somelab___1: + j = 8; + i ++; + } + loop_continue_1: ; + } + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i < 50)) { + goto while_break; + } + goto somelab; + somelab: + j = 8; + i ++; + } + while_break: /* CIL Label */ ; + } + loop_end: ; + } + __goblint_check(j == 8); + return; + } + } diff --git a/tests/regression/55-loop-unrolling/dune b/tests/regression/55-loop-unrolling/dune new file mode 100644 index 0000000000..23c0dd3290 --- /dev/null +++ b/tests/regression/55-loop-unrolling/dune @@ -0,0 +1,2 @@ +(cram + (deps (glob_files *.c))) From 933b0f6114fc95bcf379a384ea8bd1c9469f9087 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 20 Feb 2024 17:56:02 +0200 Subject: [PATCH 04/14] Mark unrolled loop labels as not original --- src/util/loopUnrolling.ml | 4 +- .../55-loop-unrolling/01-simple-cases.t | 192 +++++++++--------- tests/regression/55-loop-unrolling/02-break.t | 12 +- .../55-loop-unrolling/03-break-right-place.t | 12 +- .../regression/55-loop-unrolling/04-simple.t | 12 +- .../55-loop-unrolling/05-continue.t | 12 +- .../06-simple-cases-unrolled.t | 192 +++++++++--------- .../55-loop-unrolling/07-nested-unroll.t | 168 +++++++-------- tests/regression/55-loop-unrolling/08-bad.t | 8 +- tests/regression/55-loop-unrolling/09-weird.t | 6 +- 10 files changed, 309 insertions(+), 309 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 55e72ee62a..d1785360f0 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -453,9 +453,9 @@ class loopUnrollingVisitor(func, totalLoops) = object Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor; annotateArrays b; (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) - let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in + let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, false)]} in (* continues should go to the next unrolling *) - let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in + let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) let current_continue_target = ref dummyStmt in let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index 30d393eec2..5eb2e12d1b 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -63,7 +63,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -73,7 +73,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -83,7 +83,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -93,7 +93,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -103,7 +103,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -116,7 +116,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 3); @@ -139,7 +139,7 @@ goto loop_end; } } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -149,7 +149,7 @@ goto loop_end; } } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -159,7 +159,7 @@ goto loop_end; } } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -169,7 +169,7 @@ goto loop_end; } } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -179,7 +179,7 @@ goto loop_end; } } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -192,7 +192,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 3); @@ -215,7 +215,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -225,7 +225,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -235,7 +235,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -245,7 +245,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -255,7 +255,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -268,7 +268,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -301,7 +301,7 @@ a[i] = 0; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -318,7 +318,7 @@ a[i] = 0; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -335,7 +335,7 @@ a[i] = 0; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -352,7 +352,7 @@ a[i] = 0; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -369,7 +369,7 @@ a[i] = 0; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -389,7 +389,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(first_iteration == 0); @@ -420,7 +420,7 @@ } i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -436,7 +436,7 @@ } i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -452,7 +452,7 @@ } i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -468,7 +468,7 @@ } i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -484,7 +484,7 @@ } i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -503,7 +503,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -530,7 +530,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -541,7 +541,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -552,7 +552,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -563,7 +563,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -574,7 +574,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -588,7 +588,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -627,7 +627,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -638,7 +638,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -649,7 +649,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -660,7 +660,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -671,7 +671,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -685,7 +685,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[6] == 0); @@ -723,7 +723,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___1: ; + loop_continue_0___1: /* CIL Label */ ; } { { @@ -733,7 +733,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___0: ; + loop_continue_1___0: /* CIL Label */ ; } { { @@ -743,7 +743,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___0: ; + loop_continue_2___0: /* CIL Label */ ; } { { @@ -753,7 +753,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___0: ; + loop_continue_3___0: /* CIL Label */ ; } { { @@ -763,7 +763,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___0: ; + loop_continue_4___0: /* CIL Label */ ; } { while (1) { @@ -776,11 +776,11 @@ } while_break: /* CIL Label */ ; } - loop_end___1: ; + loop_end___1: /* CIL Label */ ; } i ++; } - loop_continue_0___0: ; + loop_continue_0___0: /* CIL Label */ ; } { { @@ -798,7 +798,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___2: ; + loop_continue_0___2: /* CIL Label */ ; } { { @@ -808,7 +808,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___2: ; + loop_continue_1___2: /* CIL Label */ ; } { { @@ -818,7 +818,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___1: ; + loop_continue_2___1: /* CIL Label */ ; } { { @@ -828,7 +828,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___1: ; + loop_continue_3___1: /* CIL Label */ ; } { { @@ -838,7 +838,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___1: ; + loop_continue_4___1: /* CIL Label */ ; } { while (1) { @@ -851,11 +851,11 @@ } while_break___0: /* CIL Label */ ; } - loop_end___2: ; + loop_end___2: /* CIL Label */ ; } i ++; } - loop_continue_1___1: ; + loop_continue_1___1: /* CIL Label */ ; } { { @@ -873,7 +873,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___3: ; + loop_continue_0___3: /* CIL Label */ ; } { { @@ -883,7 +883,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___3: ; + loop_continue_1___3: /* CIL Label */ ; } { { @@ -893,7 +893,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___3: ; + loop_continue_2___3: /* CIL Label */ ; } { { @@ -903,7 +903,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___2: ; + loop_continue_3___2: /* CIL Label */ ; } { { @@ -913,7 +913,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___2: ; + loop_continue_4___2: /* CIL Label */ ; } { while (1) { @@ -926,11 +926,11 @@ } while_break___1: /* CIL Label */ ; } - loop_end___3: ; + loop_end___3: /* CIL Label */ ; } i ++; } - loop_continue_2___2: ; + loop_continue_2___2: /* CIL Label */ ; } { { @@ -948,7 +948,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___4: ; + loop_continue_0___4: /* CIL Label */ ; } { { @@ -958,7 +958,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___4: ; + loop_continue_1___4: /* CIL Label */ ; } { { @@ -968,7 +968,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___4: ; + loop_continue_2___4: /* CIL Label */ ; } { { @@ -978,7 +978,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___4: ; + loop_continue_3___4: /* CIL Label */ ; } { { @@ -988,7 +988,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___3: ; + loop_continue_4___3: /* CIL Label */ ; } { while (1) { @@ -1001,11 +1001,11 @@ } while_break___2: /* CIL Label */ ; } - loop_end___4: ; + loop_end___4: /* CIL Label */ ; } i ++; } - loop_continue_3___3: ; + loop_continue_3___3: /* CIL Label */ ; } { { @@ -1023,7 +1023,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___5: ; + loop_continue_0___5: /* CIL Label */ ; } { { @@ -1033,7 +1033,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___5: ; + loop_continue_1___5: /* CIL Label */ ; } { { @@ -1043,7 +1043,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___5: ; + loop_continue_2___5: /* CIL Label */ ; } { { @@ -1053,7 +1053,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___5: ; + loop_continue_3___5: /* CIL Label */ ; } { { @@ -1063,7 +1063,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___5: ; + loop_continue_4___5: /* CIL Label */ ; } { while (1) { @@ -1076,11 +1076,11 @@ } while_break___3: /* CIL Label */ ; } - loop_end___5: ; + loop_end___5: /* CIL Label */ ; } i ++; } - loop_continue_4___4: ; + loop_continue_4___4: /* CIL Label */ ; } { while (1) { @@ -1099,7 +1099,7 @@ b[j] += a[i]; j ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1109,7 +1109,7 @@ b[j] += a[i]; j ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1119,7 +1119,7 @@ b[j] += a[i]; j ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1129,7 +1129,7 @@ b[j] += a[i]; j ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1139,7 +1139,7 @@ b[j] += a[i]; j ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1152,13 +1152,13 @@ } while_break___5: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } i ++; } while_break___4: /* CIL Label */ ; } - loop_end___0: ; + loop_end___0: /* CIL Label */ ; } return; } @@ -1182,7 +1182,7 @@ goto loop_end; } } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1195,7 +1195,7 @@ goto loop_end; } } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1208,7 +1208,7 @@ goto loop_end; } } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1221,7 +1221,7 @@ goto loop_end; } } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1234,7 +1234,7 @@ goto loop_end; } } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1250,7 +1250,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } return; } @@ -1275,7 +1275,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1289,7 +1289,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1303,7 +1303,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1317,7 +1317,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1331,7 +1331,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1348,7 +1348,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } return; } diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index fa3aba7f69..eb20ea7a74 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -40,7 +40,7 @@ goto loop_end; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -65,7 +65,7 @@ goto loop_end; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -90,7 +90,7 @@ goto loop_end; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -115,7 +115,7 @@ goto loop_end; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -140,7 +140,7 @@ goto loop_end; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -168,7 +168,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(r == 17); return (0); diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index d6c9f155b5..6da76f5f66 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -28,7 +28,7 @@ } i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -41,7 +41,7 @@ } i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -54,7 +54,7 @@ } i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -67,7 +67,7 @@ } i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -80,7 +80,7 @@ } i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -96,7 +96,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(i == 0); return (0); diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index c951e1b4a2..a6cb9460c4 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -24,7 +24,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -34,7 +34,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -44,7 +44,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -54,7 +54,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -64,7 +64,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -77,7 +77,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 3); diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index b8324b1654..57324a7034 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -32,7 +32,7 @@ __Cont___0: /* CIL Label */ i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -49,7 +49,7 @@ __Cont___1: /* CIL Label */ i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -66,7 +66,7 @@ __Cont___2: /* CIL Label */ i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -83,7 +83,7 @@ __Cont___3: /* CIL Label */ i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -100,7 +100,7 @@ __Cont___4: /* CIL Label */ i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -120,7 +120,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(j == 3); return; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index 1779d03476..9ee8d83334 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -63,7 +63,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -73,7 +73,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -83,7 +83,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -93,7 +93,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -103,7 +103,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -116,7 +116,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 3); @@ -139,7 +139,7 @@ goto loop_end; } } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -149,7 +149,7 @@ goto loop_end; } } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -159,7 +159,7 @@ goto loop_end; } } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -169,7 +169,7 @@ goto loop_end; } } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -179,7 +179,7 @@ goto loop_end; } } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -192,7 +192,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 3); @@ -215,7 +215,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -225,7 +225,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -235,7 +235,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -245,7 +245,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -255,7 +255,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -268,7 +268,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -301,7 +301,7 @@ a[i] = 0; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -318,7 +318,7 @@ a[i] = 0; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -335,7 +335,7 @@ a[i] = 0; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -352,7 +352,7 @@ a[i] = 0; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -369,7 +369,7 @@ a[i] = 0; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -389,7 +389,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(first_iteration == 0); @@ -420,7 +420,7 @@ } i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -436,7 +436,7 @@ } i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -452,7 +452,7 @@ } i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -468,7 +468,7 @@ } i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -484,7 +484,7 @@ } i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -503,7 +503,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -530,7 +530,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -541,7 +541,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -552,7 +552,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -563,7 +563,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -574,7 +574,7 @@ __goblint_check(a[0] == 0); i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -588,7 +588,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[3] == 0); @@ -627,7 +627,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -638,7 +638,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -649,7 +649,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -660,7 +660,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -671,7 +671,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -685,7 +685,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(a[0] == 0); __goblint_check(a[6] == 0); @@ -723,7 +723,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___1: ; + loop_continue_0___1: /* CIL Label */ ; } { { @@ -733,7 +733,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___0: ; + loop_continue_1___0: /* CIL Label */ ; } { { @@ -743,7 +743,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___0: ; + loop_continue_2___0: /* CIL Label */ ; } { { @@ -753,7 +753,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___0: ; + loop_continue_3___0: /* CIL Label */ ; } { { @@ -763,7 +763,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___0: ; + loop_continue_4___0: /* CIL Label */ ; } { while (1) { @@ -776,11 +776,11 @@ } while_break: /* CIL Label */ ; } - loop_end___1: ; + loop_end___1: /* CIL Label */ ; } i ++; } - loop_continue_0___0: ; + loop_continue_0___0: /* CIL Label */ ; } { { @@ -798,7 +798,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___2: ; + loop_continue_0___2: /* CIL Label */ ; } { { @@ -808,7 +808,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___2: ; + loop_continue_1___2: /* CIL Label */ ; } { { @@ -818,7 +818,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___1: ; + loop_continue_2___1: /* CIL Label */ ; } { { @@ -828,7 +828,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___1: ; + loop_continue_3___1: /* CIL Label */ ; } { { @@ -838,7 +838,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___1: ; + loop_continue_4___1: /* CIL Label */ ; } { while (1) { @@ -851,11 +851,11 @@ } while_break___0: /* CIL Label */ ; } - loop_end___2: ; + loop_end___2: /* CIL Label */ ; } i ++; } - loop_continue_1___1: ; + loop_continue_1___1: /* CIL Label */ ; } { { @@ -873,7 +873,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___3: ; + loop_continue_0___3: /* CIL Label */ ; } { { @@ -883,7 +883,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___3: ; + loop_continue_1___3: /* CIL Label */ ; } { { @@ -893,7 +893,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___3: ; + loop_continue_2___3: /* CIL Label */ ; } { { @@ -903,7 +903,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___2: ; + loop_continue_3___2: /* CIL Label */ ; } { { @@ -913,7 +913,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___2: ; + loop_continue_4___2: /* CIL Label */ ; } { while (1) { @@ -926,11 +926,11 @@ } while_break___1: /* CIL Label */ ; } - loop_end___3: ; + loop_end___3: /* CIL Label */ ; } i ++; } - loop_continue_2___2: ; + loop_continue_2___2: /* CIL Label */ ; } { { @@ -948,7 +948,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___4: ; + loop_continue_0___4: /* CIL Label */ ; } { { @@ -958,7 +958,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___4: ; + loop_continue_1___4: /* CIL Label */ ; } { { @@ -968,7 +968,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___4: ; + loop_continue_2___4: /* CIL Label */ ; } { { @@ -978,7 +978,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___4: ; + loop_continue_3___4: /* CIL Label */ ; } { { @@ -988,7 +988,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___3: ; + loop_continue_4___3: /* CIL Label */ ; } { while (1) { @@ -1001,11 +1001,11 @@ } while_break___2: /* CIL Label */ ; } - loop_end___4: ; + loop_end___4: /* CIL Label */ ; } i ++; } - loop_continue_3___3: ; + loop_continue_3___3: /* CIL Label */ ; } { { @@ -1023,7 +1023,7 @@ b[j] += a[i]; j ++; } - loop_continue_0___5: ; + loop_continue_0___5: /* CIL Label */ ; } { { @@ -1033,7 +1033,7 @@ b[j] += a[i]; j ++; } - loop_continue_1___5: ; + loop_continue_1___5: /* CIL Label */ ; } { { @@ -1043,7 +1043,7 @@ b[j] += a[i]; j ++; } - loop_continue_2___5: ; + loop_continue_2___5: /* CIL Label */ ; } { { @@ -1053,7 +1053,7 @@ b[j] += a[i]; j ++; } - loop_continue_3___5: ; + loop_continue_3___5: /* CIL Label */ ; } { { @@ -1063,7 +1063,7 @@ b[j] += a[i]; j ++; } - loop_continue_4___5: ; + loop_continue_4___5: /* CIL Label */ ; } { while (1) { @@ -1076,11 +1076,11 @@ } while_break___3: /* CIL Label */ ; } - loop_end___5: ; + loop_end___5: /* CIL Label */ ; } i ++; } - loop_continue_4___4: ; + loop_continue_4___4: /* CIL Label */ ; } { while (1) { @@ -1099,7 +1099,7 @@ b[j] += a[i]; j ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1109,7 +1109,7 @@ b[j] += a[i]; j ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1119,7 +1119,7 @@ b[j] += a[i]; j ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1129,7 +1129,7 @@ b[j] += a[i]; j ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1139,7 +1139,7 @@ b[j] += a[i]; j ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1152,13 +1152,13 @@ } while_break___5: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } i ++; } while_break___4: /* CIL Label */ ; } - loop_end___0: ; + loop_end___0: /* CIL Label */ ; } return; } @@ -1182,7 +1182,7 @@ goto loop_end; } } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1195,7 +1195,7 @@ goto loop_end; } } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1208,7 +1208,7 @@ goto loop_end; } } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1221,7 +1221,7 @@ goto loop_end; } } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1234,7 +1234,7 @@ goto loop_end; } } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1250,7 +1250,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } return; } @@ -1275,7 +1275,7 @@ a[i] = i; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -1289,7 +1289,7 @@ a[i] = i; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -1303,7 +1303,7 @@ a[i] = i; i ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -1317,7 +1317,7 @@ a[i] = i; i ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -1331,7 +1331,7 @@ a[i] = i; i ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -1348,7 +1348,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } return; } diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index 022c1c691f..d8eae58ee8 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -37,7 +37,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0___1: ; + loop_continue_0___1: /* CIL Label */ ; } { { @@ -47,7 +47,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1___0: ; + loop_continue_1___0: /* CIL Label */ ; } { { @@ -57,7 +57,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2___0: ; + loop_continue_2___0: /* CIL Label */ ; } { { @@ -67,7 +67,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3___0: ; + loop_continue_3___0: /* CIL Label */ ; } { { @@ -77,7 +77,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4___0: ; + loop_continue_4___0: /* CIL Label */ ; } { while (1) { @@ -90,11 +90,11 @@ } while_break: /* CIL Label */ ; } - loop_end___1: ; + loop_end___1: /* CIL Label */ ; } i ++; } - loop_continue_0___0: ; + loop_continue_0___0: /* CIL Label */ ; } { { @@ -111,7 +111,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0___2: ; + loop_continue_0___2: /* CIL Label */ ; } { { @@ -121,7 +121,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1___2: ; + loop_continue_1___2: /* CIL Label */ ; } { { @@ -131,7 +131,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2___1: ; + loop_continue_2___1: /* CIL Label */ ; } { { @@ -141,7 +141,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3___1: ; + loop_continue_3___1: /* CIL Label */ ; } { { @@ -151,7 +151,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4___1: ; + loop_continue_4___1: /* CIL Label */ ; } { while (1) { @@ -164,11 +164,11 @@ } while_break___0: /* CIL Label */ ; } - loop_end___2: ; + loop_end___2: /* CIL Label */ ; } i ++; } - loop_continue_1___1: ; + loop_continue_1___1: /* CIL Label */ ; } { { @@ -185,7 +185,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0___3: ; + loop_continue_0___3: /* CIL Label */ ; } { { @@ -195,7 +195,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1___3: ; + loop_continue_1___3: /* CIL Label */ ; } { { @@ -205,7 +205,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2___3: ; + loop_continue_2___3: /* CIL Label */ ; } { { @@ -215,7 +215,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3___2: ; + loop_continue_3___2: /* CIL Label */ ; } { { @@ -225,7 +225,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4___2: ; + loop_continue_4___2: /* CIL Label */ ; } { while (1) { @@ -238,11 +238,11 @@ } while_break___1: /* CIL Label */ ; } - loop_end___3: ; + loop_end___3: /* CIL Label */ ; } i ++; } - loop_continue_2___2: ; + loop_continue_2___2: /* CIL Label */ ; } { { @@ -259,7 +259,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0___4: ; + loop_continue_0___4: /* CIL Label */ ; } { { @@ -269,7 +269,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1___4: ; + loop_continue_1___4: /* CIL Label */ ; } { { @@ -279,7 +279,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2___4: ; + loop_continue_2___4: /* CIL Label */ ; } { { @@ -289,7 +289,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3___4: ; + loop_continue_3___4: /* CIL Label */ ; } { { @@ -299,7 +299,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4___3: ; + loop_continue_4___3: /* CIL Label */ ; } { while (1) { @@ -312,11 +312,11 @@ } while_break___2: /* CIL Label */ ; } - loop_end___4: ; + loop_end___4: /* CIL Label */ ; } i ++; } - loop_continue_3___3: ; + loop_continue_3___3: /* CIL Label */ ; } { { @@ -333,7 +333,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0___5: ; + loop_continue_0___5: /* CIL Label */ ; } { { @@ -343,7 +343,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1___5: ; + loop_continue_1___5: /* CIL Label */ ; } { { @@ -353,7 +353,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2___5: ; + loop_continue_2___5: /* CIL Label */ ; } { { @@ -363,7 +363,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3___5: ; + loop_continue_3___5: /* CIL Label */ ; } { { @@ -373,7 +373,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4___5: ; + loop_continue_4___5: /* CIL Label */ ; } { while (1) { @@ -386,11 +386,11 @@ } while_break___3: /* CIL Label */ ; } - loop_end___5: ; + loop_end___5: /* CIL Label */ ; } i ++; } - loop_continue_4___4: ; + loop_continue_4___4: /* CIL Label */ ; } { while (1) { @@ -408,7 +408,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -418,7 +418,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { { @@ -428,7 +428,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_2: ; + loop_continue_2: /* CIL Label */ ; } { { @@ -438,7 +438,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_3: ; + loop_continue_3: /* CIL Label */ ; } { { @@ -448,7 +448,7 @@ arr[i][j] = i + j; j ++; } - loop_continue_4: ; + loop_continue_4: /* CIL Label */ ; } { while (1) { @@ -461,13 +461,13 @@ } while_break___5: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } i ++; } while_break___4: /* CIL Label */ ; } - loop_end___0: ; + loop_end___0: /* CIL Label */ ; } i___0 = 0; { @@ -486,7 +486,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___8: ; + loop_continue_0___8: /* CIL Label */ ; } { { @@ -496,7 +496,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___7: ; + loop_continue_1___7: /* CIL Label */ ; } { { @@ -506,7 +506,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___7: ; + loop_continue_2___7: /* CIL Label */ ; } { { @@ -516,7 +516,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___7: ; + loop_continue_3___7: /* CIL Label */ ; } { { @@ -526,7 +526,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___7: ; + loop_continue_4___7: /* CIL Label */ ; } { while (1) { @@ -539,11 +539,11 @@ } while_break___6: /* CIL Label */ ; } - loop_end___8: ; + loop_end___8: /* CIL Label */ ; } i___0 ++; } - loop_continue_0___7: ; + loop_continue_0___7: /* CIL Label */ ; } { { @@ -560,7 +560,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___9: ; + loop_continue_0___9: /* CIL Label */ ; } { { @@ -570,7 +570,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___9: ; + loop_continue_1___9: /* CIL Label */ ; } { { @@ -580,7 +580,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___8: ; + loop_continue_2___8: /* CIL Label */ ; } { { @@ -590,7 +590,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___8: ; + loop_continue_3___8: /* CIL Label */ ; } { { @@ -600,7 +600,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___8: ; + loop_continue_4___8: /* CIL Label */ ; } { while (1) { @@ -613,11 +613,11 @@ } while_break___7: /* CIL Label */ ; } - loop_end___9: ; + loop_end___9: /* CIL Label */ ; } i___0 ++; } - loop_continue_1___8: ; + loop_continue_1___8: /* CIL Label */ ; } { { @@ -634,7 +634,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___10: ; + loop_continue_0___10: /* CIL Label */ ; } { { @@ -644,7 +644,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___10: ; + loop_continue_1___10: /* CIL Label */ ; } { { @@ -654,7 +654,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___10: ; + loop_continue_2___10: /* CIL Label */ ; } { { @@ -664,7 +664,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___9: ; + loop_continue_3___9: /* CIL Label */ ; } { { @@ -674,7 +674,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___9: ; + loop_continue_4___9: /* CIL Label */ ; } { while (1) { @@ -687,11 +687,11 @@ } while_break___8: /* CIL Label */ ; } - loop_end___10: ; + loop_end___10: /* CIL Label */ ; } i___0 ++; } - loop_continue_2___9: ; + loop_continue_2___9: /* CIL Label */ ; } { { @@ -708,7 +708,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___11: ; + loop_continue_0___11: /* CIL Label */ ; } { { @@ -718,7 +718,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___11: ; + loop_continue_1___11: /* CIL Label */ ; } { { @@ -728,7 +728,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___11: ; + loop_continue_2___11: /* CIL Label */ ; } { { @@ -738,7 +738,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___11: ; + loop_continue_3___11: /* CIL Label */ ; } { { @@ -748,7 +748,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___10: ; + loop_continue_4___10: /* CIL Label */ ; } { while (1) { @@ -761,11 +761,11 @@ } while_break___9: /* CIL Label */ ; } - loop_end___11: ; + loop_end___11: /* CIL Label */ ; } i___0 ++; } - loop_continue_3___10: ; + loop_continue_3___10: /* CIL Label */ ; } { { @@ -782,7 +782,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___12: ; + loop_continue_0___12: /* CIL Label */ ; } { { @@ -792,7 +792,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___12: ; + loop_continue_1___12: /* CIL Label */ ; } { { @@ -802,7 +802,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___12: ; + loop_continue_2___12: /* CIL Label */ ; } { { @@ -812,7 +812,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___12: ; + loop_continue_3___12: /* CIL Label */ ; } { { @@ -822,7 +822,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___12: ; + loop_continue_4___12: /* CIL Label */ ; } { while (1) { @@ -835,11 +835,11 @@ } while_break___10: /* CIL Label */ ; } - loop_end___12: ; + loop_end___12: /* CIL Label */ ; } i___0 ++; } - loop_continue_4___11: ; + loop_continue_4___11: /* CIL Label */ ; } { while (1) { @@ -857,7 +857,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_0___6: ; + loop_continue_0___6: /* CIL Label */ ; } { { @@ -867,7 +867,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_1___6: ; + loop_continue_1___6: /* CIL Label */ ; } { { @@ -877,7 +877,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_2___6: ; + loop_continue_2___6: /* CIL Label */ ; } { { @@ -887,7 +887,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_3___6: ; + loop_continue_3___6: /* CIL Label */ ; } { { @@ -897,7 +897,7 @@ __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; } - loop_continue_4___6: ; + loop_continue_4___6: /* CIL Label */ ; } { while (1) { @@ -910,13 +910,13 @@ } while_break___12: /* CIL Label */ ; } - loop_end___6: ; + loop_end___6: /* CIL Label */ ; } i___0 ++; } while_break___11: /* CIL Label */ ; } - loop_end___7: ; + loop_end___7: /* CIL Label */ ; } return (0); } diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t index 99c7f44c20..6f63b31a91 100644 --- a/tests/regression/55-loop-unrolling/08-bad.t +++ b/tests/regression/55-loop-unrolling/08-bad.t @@ -15,7 +15,7 @@ goto loop_end; } } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } switch_default: /* CIL Label */ { @@ -27,7 +27,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } switch_break: /* CIL Label */ ; } @@ -39,7 +39,7 @@ goto loop_end___0; } } - loop_continue_0___0: ; + loop_continue_0___0: /* CIL Label */ ; } lab: { @@ -51,7 +51,7 @@ } while_break___0: /* CIL Label */ ; } - loop_end___0: ; + loop_end___0: /* CIL Label */ ; } return (0); } diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index 82ff6d97f4..c8fe6ec113 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -27,7 +27,7 @@ j = 8; i ++; } - loop_continue_0: ; + loop_continue_0: /* CIL Label */ ; } { { @@ -39,7 +39,7 @@ j = 8; i ++; } - loop_continue_1: ; + loop_continue_1: /* CIL Label */ ; } { while (1) { @@ -54,7 +54,7 @@ } while_break: /* CIL Label */ ; } - loop_end: ; + loop_end: /* CIL Label */ ; } __goblint_check(j == 8); return; From 3f7d1dcf77b4c8033c661cb0e3bbd75080b99e62 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 10:31:06 +0200 Subject: [PATCH 05/14] Fix continue in loop unrolling (Double) reference meant all unrolled bodies continued directly to last unrolled loop, not next unrolled iteration. --- src/util/loopUnrolling.ml | 6 +++--- tests/regression/55-loop-unrolling/01-simple-cases.t | 8 ++++---- .../55-loop-unrolling/06-simple-cases-unrolled.t | 8 ++++---- 3 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index d1785360f0..e0ad753886 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -426,13 +426,13 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object | Continue loc -> if loopNestingDepth = 0 then (* turn top-level continues into gotos to end of current unrolling *) - ChangeDoChildrenPost(rename_labels {s with skind = Goto (!currentIterationEnd, loc)}, after) + ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref !currentIterationEnd, loc)}, after) else ChangeDoChildrenPost(rename_labels s, after) | Break loc -> if loopNestingDepth = 0 then (* turn top-level breaks into gotos to end of current unrolling *) - ChangeDoChildrenPost(rename_labels {s with skind = Goto (loopEnd,loc)}, after) + ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref loopEnd,loc)}, after) else ChangeDoChildrenPost(rename_labels s, after) | Loop _ -> loopNestingDepth <- loopNestingDepth+1; @@ -458,7 +458,7 @@ class loopUnrollingVisitor(func, totalLoops) = object let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) let current_continue_target = ref dummyStmt in - let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in + let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in let copies = List.init (factor) (fun i -> current_continue_target := continue_target i; diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index 5eb2e12d1b..ed70814445 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -1270,7 +1270,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_0; } a[i] = i; i ++; @@ -1284,7 +1284,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_1; } a[i] = i; i ++; @@ -1298,7 +1298,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_2; } a[i] = i; i ++; @@ -1312,7 +1312,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_3; } a[i] = i; i ++; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index 9ee8d83334..cef96f5eaf 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -1270,7 +1270,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_0; } a[i] = i; i ++; @@ -1284,7 +1284,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_1; } a[i] = i; i ++; @@ -1298,7 +1298,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_2; } a[i] = i; i ++; @@ -1312,7 +1312,7 @@ } if (i == 3) { i ++; - goto loop_continue_4; + goto loop_continue_3; } a[i] = i; i ++; From beb779a74f3c2eb9a550c7402505f7f15930fd96 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 10:52:27 +0200 Subject: [PATCH 06/14] Refactor loop unrolling to be functional --- src/util/loopUnrolling.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index e0ad753886..54639465f8 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -456,13 +456,12 @@ class loopUnrollingVisitor(func, totalLoops) = object let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, false)]} in (* continues should go to the next unrolling *) let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in - (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *) - let current_continue_target = ref dummyStmt in - let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in - let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - let copies = List.init (factor) (fun i -> - current_continue_target := continue_target i; - mkStmt (Block (mkBlock [one_copy (); !current_continue_target]))) + let copies = List.init factor (fun i -> + let current_continue_target = continue_target i in + let patcher = new copyandPatchLabelsVisitor (break_target, ref current_continue_target) in (* TODO: remove ref *) + let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in + mkStmt (Block (mkBlock [one_copy (); current_continue_target])) + ) in mkStmt (Block (mkBlock (copies@[s]@[break_target]))) ) else s (*no change*) From 107278c5898b8e67ded16831c3bcb9e3cbe34081 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 10:55:24 +0200 Subject: [PATCH 07/14] Clean up loop unrolling --- src/util/loopUnrolling.ml | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 54639465f8..6ca77e091f 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -426,7 +426,7 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object | Continue loc -> if loopNestingDepth = 0 then (* turn top-level continues into gotos to end of current unrolling *) - ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref !currentIterationEnd, loc)}, after) + ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref currentIterationEnd, loc)}, after) else ChangeDoChildrenPost(rename_labels s, after) | Break loc -> @@ -454,13 +454,12 @@ class loopUnrollingVisitor(func, totalLoops) = object annotateArrays b; (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *) let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, false)]} in - (* continues should go to the next unrolling *) - let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in let copies = List.init factor (fun i -> - let current_continue_target = continue_target i in - let patcher = new copyandPatchLabelsVisitor (break_target, ref current_continue_target) in (* TODO: remove ref *) - let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - mkStmt (Block (mkBlock [one_copy (); current_continue_target])) + (* continues should go to the next unrolling *) + let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in + let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in + let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in + mkStmt (Block (mkBlock [one_copy; current_continue_target])) ) in mkStmt (Block (mkBlock (copies@[s]@[break_target]))) From c2e66e6f5a4294cbf6a8f5f56dcd6dc948c892c6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 11:15:45 +0200 Subject: [PATCH 08/14] Remove one excessive block from loop unrolling --- src/util/loopUnrolling.ml | 6 +- .../55-loop-unrolling/01-simple-cases.t | 160 ------------------ tests/regression/55-loop-unrolling/02-break.t | 10 -- .../55-loop-unrolling/03-break-right-place.t | 10 -- .../regression/55-loop-unrolling/04-simple.t | 10 -- .../55-loop-unrolling/05-continue.t | 10 -- .../06-simple-cases-unrolled.t | 160 ------------------ .../55-loop-unrolling/07-nested-unroll.t | 140 --------------- tests/regression/55-loop-unrolling/08-bad.t | 4 - tests/regression/55-loop-unrolling/09-weird.t | 4 - 10 files changed, 3 insertions(+), 511 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 6ca77e091f..71ab2caa5c 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -458,11 +458,11 @@ class loopUnrollingVisitor(func, totalLoops) = object (* continues should go to the next unrolling *) let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in - let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - mkStmt (Block (mkBlock [one_copy; current_continue_target])) + let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in (* TODO: avoid this block, removing breaks some continue labels for some reason *) + [one_copy; current_continue_target] ) in - mkStmt (Block (mkBlock (copies@[s]@[break_target]))) + mkStmt (Block (mkBlock (List.flatten copies @ [s; break_target]))) ) else s (*no change*) | _ -> s in diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index ed70814445..3c5677086d 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -56,7 +56,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -64,8 +63,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -74,8 +71,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -84,8 +79,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -94,8 +87,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -104,7 +95,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -132,7 +122,6 @@ i = 0; { { - { a[i] = i; i ++; if (! (i <= 5)) { @@ -140,8 +129,6 @@ } } loop_continue_0: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -150,8 +137,6 @@ } } loop_continue_1: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -160,8 +145,6 @@ } } loop_continue_2: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -170,8 +153,6 @@ } } loop_continue_3: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -180,7 +161,6 @@ } } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -208,7 +188,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -216,8 +195,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -226,8 +203,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -236,8 +211,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -246,8 +219,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -256,7 +227,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -287,7 +257,6 @@ first_iteration = 1; { { - { if (! (i < 10)) { goto loop_end; } @@ -302,8 +271,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -319,8 +286,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -336,8 +301,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -353,8 +316,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -370,7 +331,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -407,7 +367,6 @@ top = 0; { { - { if (! (i < 4)) { goto loop_end; } @@ -421,8 +380,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -437,8 +394,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -453,8 +408,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -469,8 +422,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -485,7 +436,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -522,7 +472,6 @@ top = 0; { { - { if (! (i < 3)) { goto loop_end; } @@ -531,8 +480,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -542,8 +489,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -553,8 +498,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -564,8 +507,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -575,7 +516,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -619,7 +559,6 @@ i = 0; { { - { tmp = update(i); if (! tmp) { goto loop_end; @@ -628,8 +567,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -639,8 +576,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -650,8 +585,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -661,8 +594,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -672,7 +603,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -708,7 +638,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end___0; } @@ -716,7 +645,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___1; } @@ -724,8 +652,6 @@ j ++; } loop_continue_0___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -734,8 +660,6 @@ j ++; } loop_continue_1___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -744,8 +668,6 @@ j ++; } loop_continue_2___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -754,8 +676,6 @@ j ++; } loop_continue_3___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -764,7 +684,6 @@ j ++; } loop_continue_4___0: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -781,8 +700,6 @@ i ++; } loop_continue_0___0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -791,7 +708,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___2; } @@ -799,8 +715,6 @@ j ++; } loop_continue_0___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -809,8 +723,6 @@ j ++; } loop_continue_1___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -819,8 +731,6 @@ j ++; } loop_continue_2___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -829,8 +739,6 @@ j ++; } loop_continue_3___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -839,7 +747,6 @@ j ++; } loop_continue_4___1: /* CIL Label */ ; - } { while (1) { while_continue___0: /* CIL Label */ ; @@ -856,8 +763,6 @@ i ++; } loop_continue_1___1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -866,7 +771,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___3; } @@ -874,8 +778,6 @@ j ++; } loop_continue_0___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -884,8 +786,6 @@ j ++; } loop_continue_1___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -894,8 +794,6 @@ j ++; } loop_continue_2___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -904,8 +802,6 @@ j ++; } loop_continue_3___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -914,7 +810,6 @@ j ++; } loop_continue_4___2: /* CIL Label */ ; - } { while (1) { while_continue___1: /* CIL Label */ ; @@ -931,8 +826,6 @@ i ++; } loop_continue_2___2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -941,7 +834,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___4; } @@ -949,8 +841,6 @@ j ++; } loop_continue_0___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -959,8 +849,6 @@ j ++; } loop_continue_1___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -969,8 +857,6 @@ j ++; } loop_continue_2___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -979,8 +865,6 @@ j ++; } loop_continue_3___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -989,7 +873,6 @@ j ++; } loop_continue_4___3: /* CIL Label */ ; - } { while (1) { while_continue___2: /* CIL Label */ ; @@ -1006,8 +889,6 @@ i ++; } loop_continue_3___3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -1016,7 +897,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___5; } @@ -1024,8 +904,6 @@ j ++; } loop_continue_0___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1034,8 +912,6 @@ j ++; } loop_continue_1___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1044,8 +920,6 @@ j ++; } loop_continue_2___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1054,8 +928,6 @@ j ++; } loop_continue_3___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1064,7 +936,6 @@ j ++; } loop_continue_4___5: /* CIL Label */ ; - } { while (1) { while_continue___3: /* CIL Label */ ; @@ -1081,7 +952,6 @@ i ++; } loop_continue_4___4: /* CIL Label */ ; - } { while (1) { while_continue___4: /* CIL Label */ ; @@ -1092,7 +962,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end; } @@ -1100,8 +969,6 @@ j ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1110,8 +977,6 @@ j ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1120,8 +985,6 @@ j ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1130,8 +993,6 @@ j ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1140,7 +1001,6 @@ j ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue___5: /* CIL Label */ ; @@ -1172,7 +1032,6 @@ i = 0; { { - { if (! 1) { goto loop_end; } @@ -1183,8 +1042,6 @@ } } loop_continue_0: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1196,8 +1053,6 @@ } } loop_continue_1: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1209,8 +1064,6 @@ } } loop_continue_2: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1222,8 +1075,6 @@ } } loop_continue_3: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1235,7 +1086,6 @@ } } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -1264,7 +1114,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -1276,8 +1125,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1290,8 +1137,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1304,8 +1149,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1318,8 +1161,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1332,7 +1173,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index eb20ea7a74..b230ae6df9 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -18,7 +18,6 @@ i = 0; { { - { if (! (i < 2)) { goto loop_end; } @@ -41,8 +40,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 2)) { goto loop_end; @@ -66,8 +63,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 2)) { goto loop_end; @@ -91,8 +86,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 2)) { goto loop_end; @@ -116,8 +109,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 2)) { goto loop_end; @@ -141,7 +132,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index 6da76f5f66..8e87e6eebd 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -18,7 +18,6 @@ j = 0; { { - { if (! (i < 17)) { goto loop_end; } @@ -29,8 +28,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 17)) { goto loop_end; @@ -42,8 +39,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 17)) { goto loop_end; @@ -55,8 +50,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 17)) { goto loop_end; @@ -68,8 +61,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 17)) { goto loop_end; @@ -81,7 +72,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index a6cb9460c4..1b0a200477 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -17,7 +17,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -25,8 +24,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -35,8 +32,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -45,8 +40,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -55,8 +48,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -65,7 +56,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index 57324a7034..9835d0f9c5 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -18,7 +18,6 @@ i = 0; { { - { if (! (i < 50)) { goto loop_end; } @@ -33,8 +32,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 50)) { goto loop_end; @@ -50,8 +47,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 50)) { goto loop_end; @@ -67,8 +62,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 50)) { goto loop_end; @@ -84,8 +77,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 50)) { goto loop_end; @@ -101,7 +92,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index cef96f5eaf..ebbbb25ce0 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -56,7 +56,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -64,8 +63,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -74,8 +71,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -84,8 +79,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -94,8 +87,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -104,7 +95,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -132,7 +122,6 @@ i = 0; { { - { a[i] = i; i ++; if (! (i <= 5)) { @@ -140,8 +129,6 @@ } } loop_continue_0: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -150,8 +137,6 @@ } } loop_continue_1: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -160,8 +145,6 @@ } } loop_continue_2: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -170,8 +153,6 @@ } } loop_continue_3: /* CIL Label */ ; - } - { { a[i] = i; i ++; @@ -180,7 +161,6 @@ } } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -208,7 +188,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -216,8 +195,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -226,8 +203,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -236,8 +211,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -246,8 +219,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -256,7 +227,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -287,7 +257,6 @@ first_iteration = 1; { { - { if (! (i < 10)) { goto loop_end; } @@ -302,8 +271,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -319,8 +286,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -336,8 +301,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -353,8 +316,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end; @@ -370,7 +331,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -407,7 +367,6 @@ top = 0; { { - { if (! (i < 4)) { goto loop_end; } @@ -421,8 +380,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -437,8 +394,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -453,8 +408,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -469,8 +422,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 4)) { goto loop_end; @@ -485,7 +436,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -522,7 +472,6 @@ top = 0; { { - { if (! (i < 3)) { goto loop_end; } @@ -531,8 +480,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -542,8 +489,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -553,8 +498,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -564,8 +507,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 3)) { goto loop_end; @@ -575,7 +516,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -619,7 +559,6 @@ i = 0; { { - { tmp = update(i); if (! tmp) { goto loop_end; @@ -628,8 +567,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -639,8 +576,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -650,8 +585,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -661,8 +594,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { tmp = update(i); if (! tmp) { @@ -672,7 +603,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -708,7 +638,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end___0; } @@ -716,7 +645,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___1; } @@ -724,8 +652,6 @@ j ++; } loop_continue_0___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -734,8 +660,6 @@ j ++; } loop_continue_1___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -744,8 +668,6 @@ j ++; } loop_continue_2___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -754,8 +676,6 @@ j ++; } loop_continue_3___0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___1; @@ -764,7 +684,6 @@ j ++; } loop_continue_4___0: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -781,8 +700,6 @@ i ++; } loop_continue_0___0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -791,7 +708,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___2; } @@ -799,8 +715,6 @@ j ++; } loop_continue_0___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -809,8 +723,6 @@ j ++; } loop_continue_1___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -819,8 +731,6 @@ j ++; } loop_continue_2___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -829,8 +739,6 @@ j ++; } loop_continue_3___1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___2; @@ -839,7 +747,6 @@ j ++; } loop_continue_4___1: /* CIL Label */ ; - } { while (1) { while_continue___0: /* CIL Label */ ; @@ -856,8 +763,6 @@ i ++; } loop_continue_1___1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -866,7 +771,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___3; } @@ -874,8 +778,6 @@ j ++; } loop_continue_0___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -884,8 +786,6 @@ j ++; } loop_continue_1___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -894,8 +794,6 @@ j ++; } loop_continue_2___3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -904,8 +802,6 @@ j ++; } loop_continue_3___2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___3; @@ -914,7 +810,6 @@ j ++; } loop_continue_4___2: /* CIL Label */ ; - } { while (1) { while_continue___1: /* CIL Label */ ; @@ -931,8 +826,6 @@ i ++; } loop_continue_2___2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -941,7 +834,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___4; } @@ -949,8 +841,6 @@ j ++; } loop_continue_0___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -959,8 +849,6 @@ j ++; } loop_continue_1___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -969,8 +857,6 @@ j ++; } loop_continue_2___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -979,8 +865,6 @@ j ++; } loop_continue_3___4: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___4; @@ -989,7 +873,6 @@ j ++; } loop_continue_4___3: /* CIL Label */ ; - } { while (1) { while_continue___2: /* CIL Label */ ; @@ -1006,8 +889,6 @@ i ++; } loop_continue_3___3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end___0; @@ -1016,7 +897,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end___5; } @@ -1024,8 +904,6 @@ j ++; } loop_continue_0___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1034,8 +912,6 @@ j ++; } loop_continue_1___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1044,8 +920,6 @@ j ++; } loop_continue_2___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1054,8 +928,6 @@ j ++; } loop_continue_3___5: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end___5; @@ -1064,7 +936,6 @@ j ++; } loop_continue_4___5: /* CIL Label */ ; - } { while (1) { while_continue___3: /* CIL Label */ ; @@ -1081,7 +952,6 @@ i ++; } loop_continue_4___4: /* CIL Label */ ; - } { while (1) { while_continue___4: /* CIL Label */ ; @@ -1092,7 +962,6 @@ j = 0; { { - { if (! (j < 5)) { goto loop_end; } @@ -1100,8 +969,6 @@ j ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1110,8 +977,6 @@ j ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1120,8 +985,6 @@ j ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1130,8 +993,6 @@ j ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (j < 5)) { goto loop_end; @@ -1140,7 +1001,6 @@ j ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue___5: /* CIL Label */ ; @@ -1172,7 +1032,6 @@ i = 0; { { - { if (! 1) { goto loop_end; } @@ -1183,8 +1042,6 @@ } } loop_continue_0: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1196,8 +1053,6 @@ } } loop_continue_1: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1209,8 +1064,6 @@ } } loop_continue_2: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1222,8 +1075,6 @@ } } loop_continue_3: /* CIL Label */ ; - } - { { if (! 1) { goto loop_end; @@ -1235,7 +1086,6 @@ } } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -1264,7 +1114,6 @@ i = 0; { { - { if (! (i < 5)) { goto loop_end; } @@ -1276,8 +1125,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1290,8 +1137,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1304,8 +1149,6 @@ i ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1318,8 +1161,6 @@ i ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (i < 5)) { goto loop_end; @@ -1332,7 +1173,6 @@ i ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index d8eae58ee8..39cf4205c8 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -23,14 +23,12 @@ i = 0; { { - { if (! (i < 10)) { goto loop_end___0; } j = 0; { { - { if (! (j < 10)) { goto loop_end___1; } @@ -38,8 +36,6 @@ j ++; } loop_continue_0___1: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___1; @@ -48,8 +44,6 @@ j ++; } loop_continue_1___0: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___1; @@ -58,8 +52,6 @@ j ++; } loop_continue_2___0: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___1; @@ -68,8 +60,6 @@ j ++; } loop_continue_3___0: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___1; @@ -78,7 +68,6 @@ j ++; } loop_continue_4___0: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; @@ -95,8 +84,6 @@ i ++; } loop_continue_0___0: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end___0; @@ -104,7 +91,6 @@ j = 0; { { - { if (! (j < 10)) { goto loop_end___2; } @@ -112,8 +98,6 @@ j ++; } loop_continue_0___2: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___2; @@ -122,8 +106,6 @@ j ++; } loop_continue_1___2: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___2; @@ -132,8 +114,6 @@ j ++; } loop_continue_2___1: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___2; @@ -142,8 +122,6 @@ j ++; } loop_continue_3___1: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___2; @@ -152,7 +130,6 @@ j ++; } loop_continue_4___1: /* CIL Label */ ; - } { while (1) { while_continue___0: /* CIL Label */ ; @@ -169,8 +146,6 @@ i ++; } loop_continue_1___1: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end___0; @@ -178,7 +153,6 @@ j = 0; { { - { if (! (j < 10)) { goto loop_end___3; } @@ -186,8 +160,6 @@ j ++; } loop_continue_0___3: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___3; @@ -196,8 +168,6 @@ j ++; } loop_continue_1___3: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___3; @@ -206,8 +176,6 @@ j ++; } loop_continue_2___3: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___3; @@ -216,8 +184,6 @@ j ++; } loop_continue_3___2: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___3; @@ -226,7 +192,6 @@ j ++; } loop_continue_4___2: /* CIL Label */ ; - } { while (1) { while_continue___1: /* CIL Label */ ; @@ -243,8 +208,6 @@ i ++; } loop_continue_2___2: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end___0; @@ -252,7 +215,6 @@ j = 0; { { - { if (! (j < 10)) { goto loop_end___4; } @@ -260,8 +222,6 @@ j ++; } loop_continue_0___4: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___4; @@ -270,8 +230,6 @@ j ++; } loop_continue_1___4: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___4; @@ -280,8 +238,6 @@ j ++; } loop_continue_2___4: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___4; @@ -290,8 +246,6 @@ j ++; } loop_continue_3___4: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___4; @@ -300,7 +254,6 @@ j ++; } loop_continue_4___3: /* CIL Label */ ; - } { while (1) { while_continue___2: /* CIL Label */ ; @@ -317,8 +270,6 @@ i ++; } loop_continue_3___3: /* CIL Label */ ; - } - { { if (! (i < 10)) { goto loop_end___0; @@ -326,7 +277,6 @@ j = 0; { { - { if (! (j < 10)) { goto loop_end___5; } @@ -334,8 +284,6 @@ j ++; } loop_continue_0___5: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___5; @@ -344,8 +292,6 @@ j ++; } loop_continue_1___5: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___5; @@ -354,8 +300,6 @@ j ++; } loop_continue_2___5: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___5; @@ -364,8 +308,6 @@ j ++; } loop_continue_3___5: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end___5; @@ -374,7 +316,6 @@ j ++; } loop_continue_4___5: /* CIL Label */ ; - } { while (1) { while_continue___3: /* CIL Label */ ; @@ -391,7 +332,6 @@ i ++; } loop_continue_4___4: /* CIL Label */ ; - } { while (1) { while_continue___4: /* CIL Label */ ; @@ -401,7 +341,6 @@ j = 0; { { - { if (! (j < 10)) { goto loop_end; } @@ -409,8 +348,6 @@ j ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end; @@ -419,8 +356,6 @@ j ++; } loop_continue_1: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end; @@ -429,8 +364,6 @@ j ++; } loop_continue_2: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end; @@ -439,8 +372,6 @@ j ++; } loop_continue_3: /* CIL Label */ ; - } - { { if (! (j < 10)) { goto loop_end; @@ -449,7 +380,6 @@ j ++; } loop_continue_4: /* CIL Label */ ; - } { while (1) { while_continue___5: /* CIL Label */ ; @@ -472,14 +402,12 @@ i___0 = 0; { { - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___8; } @@ -487,8 +415,6 @@ j___0 ++; } loop_continue_0___8: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___8; @@ -497,8 +423,6 @@ j___0 ++; } loop_continue_1___7: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___8; @@ -507,8 +431,6 @@ j___0 ++; } loop_continue_2___7: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___8; @@ -517,8 +439,6 @@ j___0 ++; } loop_continue_3___7: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___8; @@ -527,7 +447,6 @@ j___0 ++; } loop_continue_4___7: /* CIL Label */ ; - } { while (1) { while_continue___6: /* CIL Label */ ; @@ -544,8 +463,6 @@ i___0 ++; } loop_continue_0___7: /* CIL Label */ ; - } - { { if (! (i___0 < 5)) { goto loop_end___7; @@ -553,7 +470,6 @@ j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___9; } @@ -561,8 +477,6 @@ j___0 ++; } loop_continue_0___9: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___9; @@ -571,8 +485,6 @@ j___0 ++; } loop_continue_1___9: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___9; @@ -581,8 +493,6 @@ j___0 ++; } loop_continue_2___8: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___9; @@ -591,8 +501,6 @@ j___0 ++; } loop_continue_3___8: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___9; @@ -601,7 +509,6 @@ j___0 ++; } loop_continue_4___8: /* CIL Label */ ; - } { while (1) { while_continue___7: /* CIL Label */ ; @@ -618,8 +525,6 @@ i___0 ++; } loop_continue_1___8: /* CIL Label */ ; - } - { { if (! (i___0 < 5)) { goto loop_end___7; @@ -627,7 +532,6 @@ j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___10; } @@ -635,8 +539,6 @@ j___0 ++; } loop_continue_0___10: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___10; @@ -645,8 +547,6 @@ j___0 ++; } loop_continue_1___10: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___10; @@ -655,8 +555,6 @@ j___0 ++; } loop_continue_2___10: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___10; @@ -665,8 +563,6 @@ j___0 ++; } loop_continue_3___9: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___10; @@ -675,7 +571,6 @@ j___0 ++; } loop_continue_4___9: /* CIL Label */ ; - } { while (1) { while_continue___8: /* CIL Label */ ; @@ -692,8 +587,6 @@ i___0 ++; } loop_continue_2___9: /* CIL Label */ ; - } - { { if (! (i___0 < 5)) { goto loop_end___7; @@ -701,7 +594,6 @@ j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___11; } @@ -709,8 +601,6 @@ j___0 ++; } loop_continue_0___11: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___11; @@ -719,8 +609,6 @@ j___0 ++; } loop_continue_1___11: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___11; @@ -729,8 +617,6 @@ j___0 ++; } loop_continue_2___11: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___11; @@ -739,8 +625,6 @@ j___0 ++; } loop_continue_3___11: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___11; @@ -749,7 +633,6 @@ j___0 ++; } loop_continue_4___10: /* CIL Label */ ; - } { while (1) { while_continue___9: /* CIL Label */ ; @@ -766,8 +649,6 @@ i___0 ++; } loop_continue_3___10: /* CIL Label */ ; - } - { { if (! (i___0 < 5)) { goto loop_end___7; @@ -775,7 +656,6 @@ j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___12; } @@ -783,8 +663,6 @@ j___0 ++; } loop_continue_0___12: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___12; @@ -793,8 +671,6 @@ j___0 ++; } loop_continue_1___12: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___12; @@ -803,8 +679,6 @@ j___0 ++; } loop_continue_2___12: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___12; @@ -813,8 +687,6 @@ j___0 ++; } loop_continue_3___12: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___12; @@ -823,7 +695,6 @@ j___0 ++; } loop_continue_4___12: /* CIL Label */ ; - } { while (1) { while_continue___10: /* CIL Label */ ; @@ -840,7 +711,6 @@ i___0 ++; } loop_continue_4___11: /* CIL Label */ ; - } { while (1) { while_continue___11: /* CIL Label */ ; @@ -850,7 +720,6 @@ j___0 = 0; { { - { if (! (j___0 < 5)) { goto loop_end___6; } @@ -858,8 +727,6 @@ j___0 ++; } loop_continue_0___6: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___6; @@ -868,8 +735,6 @@ j___0 ++; } loop_continue_1___6: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___6; @@ -878,8 +743,6 @@ j___0 ++; } loop_continue_2___6: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___6; @@ -888,8 +751,6 @@ j___0 ++; } loop_continue_3___6: /* CIL Label */ ; - } - { { if (! (j___0 < 5)) { goto loop_end___6; @@ -898,7 +759,6 @@ j___0 ++; } loop_continue_4___6: /* CIL Label */ ; - } { while (1) { while_continue___12: /* CIL Label */ ; diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t index 6f63b31a91..a57a3cb278 100644 --- a/tests/regression/55-loop-unrolling/08-bad.t +++ b/tests/regression/55-loop-unrolling/08-bad.t @@ -10,13 +10,11 @@ goto switch_default; { { - { if (! 0) { goto loop_end; } } loop_continue_0: /* CIL Label */ ; - } switch_default: /* CIL Label */ { while (1) { @@ -34,13 +32,11 @@ goto lab; { { - { if (! 0) { goto loop_end___0; } } loop_continue_0___0: /* CIL Label */ ; - } lab: { while (1) { diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index c8fe6ec113..19cf16ff08 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -18,7 +18,6 @@ i = 0; { { - { if (! (i < 50)) { goto loop_end; } @@ -28,8 +27,6 @@ i ++; } loop_continue_0: /* CIL Label */ ; - } - { { if (! (i < 50)) { goto loop_end; @@ -40,7 +37,6 @@ i ++; } loop_continue_1: /* CIL Label */ ; - } { while (1) { while_continue: /* CIL Label */ ; From 2bfb5cba92e191fe686efbbe51b86213bdbfa1ab Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 11:25:28 +0200 Subject: [PATCH 09/14] Add option dbg.justcil-printer --- src/common/util/cilfacade.ml | 11 ++++++++--- src/config/options.schema.json | 7 +++++++ tests/regression/55-loop-unrolling/01-simple-cases.t | 2 +- tests/regression/55-loop-unrolling/02-break.t | 2 +- .../55-loop-unrolling/03-break-right-place.t | 2 +- tests/regression/55-loop-unrolling/04-simple.t | 2 +- tests/regression/55-loop-unrolling/05-continue.t | 2 +- .../55-loop-unrolling/06-simple-cases-unrolled.t | 2 +- tests/regression/55-loop-unrolling/07-nested-unroll.t | 2 +- tests/regression/55-loop-unrolling/08-bad.t | 2 +- tests/regression/55-loop-unrolling/09-weird.t | 2 +- 11 files changed, 24 insertions(+), 12 deletions(-) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 3df3a71ae5..04dcfee606 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -66,7 +66,7 @@ let parse fileName = E.s (E.error "There were parsing errors in %s" fileName_str); file -class myCilPrinter = +class cleanCilPrinterClass = object inherit defaultCilPrinterClass as super @@ -79,14 +79,19 @@ object | _ -> super#pGlobal () g end -let dumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file = +let cleanCilPrinter = new cleanCilPrinterClass + +let cleanDumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file = Pretty.printDepth := 99999; Pretty.fastMode := true; iterGlobals file (fun g -> dumpGlobal pp out g); flush out let print (fileAST: file) = - dumpFile (new myCilPrinter) stdout "stdout" fileAST + match GobConfig.get_string "dbg.justcil-printer" with + | "default" -> dumpFile defaultCilPrinter stdout "stdout" fileAST + | "clean" -> cleanDumpFile cleanCilPrinter stdout "stdout" fileAST + | _ -> assert false let rmTemps fileAST = RmUnused.removeUnused fileAST diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 5d69990499..abba08fca9 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1860,6 +1860,13 @@ "type": "string", "default": "" }, + "justcil-printer": { + "title": "dbg.justcil-printer", + "description": "Printer to use for justcil", + "type": "string", + "enum": ["default", "clean"], + "default": "default" + }, "timeout": { "title": "dbg.timeout", "description": diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index 3c5677086d..8539810091 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 01-simple-cases.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 01-simple-cases.c [Info] unrolling loop at 01-simple-cases.c:27:5-30:5 with factor 5 [Info] unrolling loop at 01-simple-cases.c:42:5-45:19 with factor 5 [Info] unrolling loop at 01-simple-cases.c:57:5-60:5 with factor 5 diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index b230ae6df9..125842394b 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 02-break.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 02-break.c [Info] unrolling loop at 02-break.c:6:5-15:2 with factor 5 extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index 8e87e6eebd..dd4d4f658e 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 03-break-right-place.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 03-break-right-place.c [Info] unrolling loop at 03-break-right-place.c:8:5-15:5 with factor 5 extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index 1b0a200477..dab702cc7c 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 04-simple.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 04-simple.c [Info] unrolling loop at 04-simple.c:10:5-13:5 with factor 5 extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index 9835d0f9c5..e8fc6c2a4a 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil 05-continue.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 05-continue.c [Info] unrolling loop at 05-continue.c:9:5-17:5 with factor 5 extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index ebbbb25ce0..8a2a6b5f5e 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 06-simple-cases-unrolled.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 06-simple-cases-unrolled.c [Info] unrolling loop at 06-simple-cases-unrolled.c:27:5-30:5 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:42:5-45:19 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:57:5-60:5 with factor 5 diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index 39cf4205c8..8242d42805 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil 07-nested-unroll.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 07-nested-unroll.c [Info] unrolling loop at 07-nested-unroll.c:7:9-9:9 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5 diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t index a57a3cb278..84724005ed 100644 --- a/tests/regression/55-loop-unrolling/08-bad.t +++ b/tests/regression/55-loop-unrolling/08-bad.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil 08-bad.c + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil --set dbg.justcil-printer clean 08-bad.c [Info] unrolling loop at 08-bad.c:8:7-8:23 with factor 1 [Info] unrolling loop at 08-bad.c:14:8-14:24 with factor 1 int main(void) diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index 19cf16ff08..be6c824ab3 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -1,4 +1,4 @@ - $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil 09-weird.c + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil --set dbg.justcil-printer clean 09-weird.c [Info] unrolling loop at 09-weird.c:8:5-11:5 with factor 2 extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; From bdebd1b922f414ef3e345de070765ccaead7333b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 11:33:49 +0200 Subject: [PATCH 10/14] Remove second excessive block from loop unrolling --- src/util/loopUnrolling.ml | 9 +- .../55-loop-unrolling/01-simple-cases.t | 160 ------------------ tests/regression/55-loop-unrolling/02-break.t | 10 -- .../55-loop-unrolling/03-break-right-place.t | 10 -- .../regression/55-loop-unrolling/04-simple.t | 10 -- .../55-loop-unrolling/05-continue.t | 10 -- .../06-simple-cases-unrolled.t | 160 ------------------ .../55-loop-unrolling/07-nested-unroll.t | 140 --------------- tests/regression/55-loop-unrolling/08-bad.t | 4 - tests/regression/55-loop-unrolling/09-weird.t | 4 - 10 files changed, 7 insertions(+), 510 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 71ab2caa5c..abdff8fa57 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -458,8 +458,13 @@ class loopUnrollingVisitor(func, totalLoops) = object (* continues should go to the next unrolling *) let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in - let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in (* TODO: avoid this block, removing breaks some continue labels for some reason *) - [one_copy; current_continue_target] + let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in + let one_copy_stmts = (* TODO: avoid this nonsense, directly visiting only b.bstmts breaks some continue labels for some reason *) + match one_copy.skind with + | Block b -> b.bstmts + | _ -> assert false + in + one_copy_stmts @ [current_continue_target] ) in mkStmt (Block (mkBlock (List.flatten copies @ [s; break_target]))) diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index 8539810091..a05ee4d010 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -55,45 +55,35 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -121,45 +111,35 @@ { i = 0; { - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_0: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_1: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_2: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_3: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -187,45 +167,35 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -256,7 +226,6 @@ i = 0; first_iteration = 1; { - { if (! (i < 10)) { goto loop_end; } @@ -269,9 +238,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -284,9 +251,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -299,9 +264,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -314,9 +277,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -329,7 +290,6 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -366,7 +326,6 @@ i = 0; top = 0; { - { if (! (i < 4)) { goto loop_end; } @@ -378,9 +337,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -392,9 +349,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -406,9 +361,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -420,9 +373,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -434,7 +385,6 @@ __goblint_check(top == 3); } i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -471,50 +421,40 @@ i = 0; top = 0; { - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -558,50 +498,40 @@ { i = 0; { - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -637,52 +567,41 @@ b[4] = 0; i = 0; { - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_0___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_1___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_2___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_3___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_4___0: /* CIL Label */ ; { while (1) { @@ -698,54 +617,42 @@ loop_end___1: /* CIL Label */ ; } i ++; - } loop_continue_0___0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_0___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_1___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_2___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_3___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_4___1: /* CIL Label */ ; { while (1) { @@ -761,54 +668,42 @@ loop_end___2: /* CIL Label */ ; } i ++; - } loop_continue_1___1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_0___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_1___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_2___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_3___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_4___2: /* CIL Label */ ; { while (1) { @@ -824,54 +719,42 @@ loop_end___3: /* CIL Label */ ; } i ++; - } loop_continue_2___2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_0___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_1___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_2___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_3___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_4___3: /* CIL Label */ ; { while (1) { @@ -887,54 +770,42 @@ loop_end___4: /* CIL Label */ ; } i ++; - } loop_continue_3___3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_0___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_1___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_2___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_3___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_4___5: /* CIL Label */ ; { while (1) { @@ -950,7 +821,6 @@ loop_end___5: /* CIL Label */ ; } i ++; - } loop_continue_4___4: /* CIL Label */ ; { while (1) { @@ -961,45 +831,35 @@ a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -1031,7 +891,6 @@ { i = 0; { - { if (! 1) { goto loop_end; } @@ -1040,9 +899,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_0: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1051,9 +908,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_1: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1062,9 +917,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_2: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1073,9 +926,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_3: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1084,7 +935,6 @@ if (i == 5) { goto loop_end; } - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -1113,7 +963,6 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } @@ -1123,9 +972,7 @@ } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1135,9 +982,7 @@ } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1147,9 +992,7 @@ } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1159,9 +1002,7 @@ } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1171,7 +1012,6 @@ } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index 125842394b..5f6928002a 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -17,7 +17,6 @@ r = 5; i = 0; { - { if (! (i < 2)) { goto loop_end; } @@ -38,9 +37,7 @@ r = 17; goto loop_end; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 2)) { goto loop_end; } @@ -61,9 +58,7 @@ r = 17; goto loop_end; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 2)) { goto loop_end; } @@ -84,9 +79,7 @@ r = 17; goto loop_end; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 2)) { goto loop_end; } @@ -107,9 +100,7 @@ r = 17; goto loop_end; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 2)) { goto loop_end; } @@ -130,7 +121,6 @@ r = 17; goto loop_end; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index dd4d4f658e..bc183b00c1 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -17,7 +17,6 @@ i = 0; j = 0; { - { if (! (i < 17)) { goto loop_end; } @@ -26,9 +25,7 @@ goto loop_end; } i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 17)) { goto loop_end; } @@ -37,9 +34,7 @@ goto loop_end; } i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 17)) { goto loop_end; } @@ -48,9 +43,7 @@ goto loop_end; } i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 17)) { goto loop_end; } @@ -59,9 +52,7 @@ goto loop_end; } i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 17)) { goto loop_end; } @@ -70,7 +61,6 @@ goto loop_end; } i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index dab702cc7c..49f5cc7e46 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -16,45 +16,35 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index e8fc6c2a4a..6b1601c833 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -17,7 +17,6 @@ j = 0; i = 0; { - { if (! (i < 50)) { goto loop_end; } @@ -30,9 +29,7 @@ j ++; __Cont___0: /* CIL Label */ i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 50)) { goto loop_end; } @@ -45,9 +42,7 @@ j ++; __Cont___1: /* CIL Label */ i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 50)) { goto loop_end; } @@ -60,9 +55,7 @@ j ++; __Cont___2: /* CIL Label */ i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 50)) { goto loop_end; } @@ -75,9 +68,7 @@ j ++; __Cont___3: /* CIL Label */ i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 50)) { goto loop_end; } @@ -90,7 +81,6 @@ j ++; __Cont___4: /* CIL Label */ i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index 8a2a6b5f5e..ae6c4ba147 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -55,45 +55,35 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -121,45 +111,35 @@ { i = 0; { - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_0: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_1: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_2: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_3: /* CIL Label */ ; - { a[i] = i; i ++; if (! (i <= 5)) { goto loop_end; } - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -187,45 +167,35 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -256,7 +226,6 @@ i = 0; first_iteration = 1; { - { if (! (i < 10)) { goto loop_end; } @@ -269,9 +238,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -284,9 +251,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -299,9 +264,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -314,9 +277,7 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end; } @@ -329,7 +290,6 @@ first_iteration = 0; a[i] = 0; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -366,7 +326,6 @@ i = 0; top = 0; { - { if (! (i < 4)) { goto loop_end; } @@ -378,9 +337,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -392,9 +349,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -406,9 +361,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -420,9 +373,7 @@ __goblint_check(top == 3); } i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 4)) { goto loop_end; } @@ -434,7 +385,6 @@ __goblint_check(top == 3); } i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -471,50 +421,40 @@ i = 0; top = 0; { - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 3)) { goto loop_end; } a[i] = 0; __goblint_check(a[0] == 0); i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -558,50 +498,40 @@ { i = 0; { - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { tmp = update(i); if (! tmp) { goto loop_end; } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -637,52 +567,41 @@ b[4] = 0; i = 0; { - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_0___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_1___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_2___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_3___0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___1; } b[j] += a[i]; j ++; - } loop_continue_4___0: /* CIL Label */ ; { while (1) { @@ -698,54 +617,42 @@ loop_end___1: /* CIL Label */ ; } i ++; - } loop_continue_0___0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_0___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_1___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_2___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_3___1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___2; } b[j] += a[i]; j ++; - } loop_continue_4___1: /* CIL Label */ ; { while (1) { @@ -761,54 +668,42 @@ loop_end___2: /* CIL Label */ ; } i ++; - } loop_continue_1___1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_0___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_1___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_2___3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_3___2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___3; } b[j] += a[i]; j ++; - } loop_continue_4___2: /* CIL Label */ ; { while (1) { @@ -824,54 +719,42 @@ loop_end___3: /* CIL Label */ ; } i ++; - } loop_continue_2___2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_0___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_1___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_2___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_3___4: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___4; } b[j] += a[i]; j ++; - } loop_continue_4___3: /* CIL Label */ ; { while (1) { @@ -887,54 +770,42 @@ loop_end___4: /* CIL Label */ ; } i ++; - } loop_continue_3___3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end___0; } a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_0___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_1___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_2___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_3___5: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end___5; } b[j] += a[i]; j ++; - } loop_continue_4___5: /* CIL Label */ ; { while (1) { @@ -950,7 +821,6 @@ loop_end___5: /* CIL Label */ ; } i ++; - } loop_continue_4___4: /* CIL Label */ ; { while (1) { @@ -961,45 +831,35 @@ a[i] = i; j = 0; { - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (j < 5)) { goto loop_end; } b[j] += a[i]; j ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -1031,7 +891,6 @@ { i = 0; { - { if (! 1) { goto loop_end; } @@ -1040,9 +899,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_0: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1051,9 +908,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_1: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1062,9 +917,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_2: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1073,9 +926,7 @@ if (i == 5) { goto loop_end; } - } loop_continue_3: /* CIL Label */ ; - { if (! 1) { goto loop_end; } @@ -1084,7 +935,6 @@ if (i == 5) { goto loop_end; } - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -1113,7 +963,6 @@ { i = 0; { - { if (! (i < 5)) { goto loop_end; } @@ -1123,9 +972,7 @@ } a[i] = i; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1135,9 +982,7 @@ } a[i] = i; i ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1147,9 +992,7 @@ } a[i] = i; i ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1159,9 +1002,7 @@ } a[i] = i; i ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (i < 5)) { goto loop_end; } @@ -1171,7 +1012,6 @@ } a[i] = i; i ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index 8242d42805..a5c1c2f590 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -22,51 +22,40 @@ { i = 0; { - { if (! (i < 10)) { goto loop_end___0; } j = 0; { - { if (! (j < 10)) { goto loop_end___1; } arr[i][j] = i + j; j ++; - } loop_continue_0___1: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___1; } arr[i][j] = i + j; j ++; - } loop_continue_1___0: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___1; } arr[i][j] = i + j; j ++; - } loop_continue_2___0: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___1; } arr[i][j] = i + j; j ++; - } loop_continue_3___0: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___1; } arr[i][j] = i + j; j ++; - } loop_continue_4___0: /* CIL Label */ ; { while (1) { @@ -82,53 +71,41 @@ loop_end___1: /* CIL Label */ ; } i ++; - } loop_continue_0___0: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end___0; } j = 0; { - { if (! (j < 10)) { goto loop_end___2; } arr[i][j] = i + j; j ++; - } loop_continue_0___2: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___2; } arr[i][j] = i + j; j ++; - } loop_continue_1___2: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___2; } arr[i][j] = i + j; j ++; - } loop_continue_2___1: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___2; } arr[i][j] = i + j; j ++; - } loop_continue_3___1: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___2; } arr[i][j] = i + j; j ++; - } loop_continue_4___1: /* CIL Label */ ; { while (1) { @@ -144,53 +121,41 @@ loop_end___2: /* CIL Label */ ; } i ++; - } loop_continue_1___1: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end___0; } j = 0; { - { if (! (j < 10)) { goto loop_end___3; } arr[i][j] = i + j; j ++; - } loop_continue_0___3: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___3; } arr[i][j] = i + j; j ++; - } loop_continue_1___3: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___3; } arr[i][j] = i + j; j ++; - } loop_continue_2___3: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___3; } arr[i][j] = i + j; j ++; - } loop_continue_3___2: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___3; } arr[i][j] = i + j; j ++; - } loop_continue_4___2: /* CIL Label */ ; { while (1) { @@ -206,53 +171,41 @@ loop_end___3: /* CIL Label */ ; } i ++; - } loop_continue_2___2: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end___0; } j = 0; { - { if (! (j < 10)) { goto loop_end___4; } arr[i][j] = i + j; j ++; - } loop_continue_0___4: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___4; } arr[i][j] = i + j; j ++; - } loop_continue_1___4: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___4; } arr[i][j] = i + j; j ++; - } loop_continue_2___4: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___4; } arr[i][j] = i + j; j ++; - } loop_continue_3___4: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___4; } arr[i][j] = i + j; j ++; - } loop_continue_4___3: /* CIL Label */ ; { while (1) { @@ -268,53 +221,41 @@ loop_end___4: /* CIL Label */ ; } i ++; - } loop_continue_3___3: /* CIL Label */ ; - { if (! (i < 10)) { goto loop_end___0; } j = 0; { - { if (! (j < 10)) { goto loop_end___5; } arr[i][j] = i + j; j ++; - } loop_continue_0___5: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___5; } arr[i][j] = i + j; j ++; - } loop_continue_1___5: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___5; } arr[i][j] = i + j; j ++; - } loop_continue_2___5: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___5; } arr[i][j] = i + j; j ++; - } loop_continue_3___5: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end___5; } arr[i][j] = i + j; j ++; - } loop_continue_4___5: /* CIL Label */ ; { while (1) { @@ -330,7 +271,6 @@ loop_end___5: /* CIL Label */ ; } i ++; - } loop_continue_4___4: /* CIL Label */ ; { while (1) { @@ -340,45 +280,35 @@ } j = 0; { - { if (! (j < 10)) { goto loop_end; } arr[i][j] = i + j; j ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end; } arr[i][j] = i + j; j ++; - } loop_continue_1: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end; } arr[i][j] = i + j; j ++; - } loop_continue_2: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end; } arr[i][j] = i + j; j ++; - } loop_continue_3: /* CIL Label */ ; - { if (! (j < 10)) { goto loop_end; } arr[i][j] = i + j; j ++; - } loop_continue_4: /* CIL Label */ ; { while (1) { @@ -401,51 +331,40 @@ } i___0 = 0; { - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___8; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___8: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___8; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___7: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___8; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___7: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___8; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___7: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___8; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___7: /* CIL Label */ ; { while (1) { @@ -461,53 +380,41 @@ loop_end___8: /* CIL Label */ ; } i___0 ++; - } loop_continue_0___7: /* CIL Label */ ; - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___9; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___9: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___9; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___9: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___9; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___8: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___9; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___8: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___9; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___8: /* CIL Label */ ; { while (1) { @@ -523,53 +430,41 @@ loop_end___9: /* CIL Label */ ; } i___0 ++; - } loop_continue_1___8: /* CIL Label */ ; - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___10; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___10: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___10; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___10: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___10; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___10: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___10; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___9: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___10; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___9: /* CIL Label */ ; { while (1) { @@ -585,53 +480,41 @@ loop_end___10: /* CIL Label */ ; } i___0 ++; - } loop_continue_2___9: /* CIL Label */ ; - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___11; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___11: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___11; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___11: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___11; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___11: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___11; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___11: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___11; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___10: /* CIL Label */ ; { while (1) { @@ -647,53 +530,41 @@ loop_end___11: /* CIL Label */ ; } i___0 ++; - } loop_continue_3___10: /* CIL Label */ ; - { if (! (i___0 < 5)) { goto loop_end___7; } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___12; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___12: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___12; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___12: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___12; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___12: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___12; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___12: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___12; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___12: /* CIL Label */ ; { while (1) { @@ -709,7 +580,6 @@ loop_end___12: /* CIL Label */ ; } i___0 ++; - } loop_continue_4___11: /* CIL Label */ ; { while (1) { @@ -719,45 +589,35 @@ } j___0 = 0; { - { if (! (j___0 < 5)) { goto loop_end___6; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_0___6: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___6; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_1___6: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___6; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_2___6: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___6; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_3___6: /* CIL Label */ ; - { if (! (j___0 < 5)) { goto loop_end___6; } __goblint_check(arr[i___0][j___0] == i___0 + j___0); j___0 ++; - } loop_continue_4___6: /* CIL Label */ ; { while (1) { diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t index 84724005ed..11cded728f 100644 --- a/tests/regression/55-loop-unrolling/08-bad.t +++ b/tests/regression/55-loop-unrolling/08-bad.t @@ -9,11 +9,9 @@ { goto switch_default; { - { if (! 0) { goto loop_end; } - } loop_continue_0: /* CIL Label */ ; switch_default: /* CIL Label */ { @@ -31,11 +29,9 @@ } goto lab; { - { if (! 0) { goto loop_end___0; } - } loop_continue_0___0: /* CIL Label */ ; lab: { diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index be6c824ab3..606f59acd8 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -17,7 +17,6 @@ j = 0; i = 0; { - { if (! (i < 50)) { goto loop_end; } @@ -25,9 +24,7 @@ somelab___0: j = 8; i ++; - } loop_continue_0: /* CIL Label */ ; - { if (! (i < 50)) { goto loop_end; } @@ -35,7 +32,6 @@ somelab___1: j = 8; i ++; - } loop_continue_1: /* CIL Label */ ; { while (1) { From 2fb6b618ca557122c250178791c2056ae7f178fb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 11:47:54 +0200 Subject: [PATCH 11/14] Refactor statements copying in loop unrolling --- src/util/loopUnrolling.ml | 36 ++++++++++++------------------------ 1 file changed, 12 insertions(+), 24 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index abdff8fa57..d5efd0d937 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -390,27 +390,13 @@ end Also assigns fresh names to all labels and patches gotos for labels appearing in the current fragment to their new name *) -class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object +class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object inherit nopCilVisitor - val mutable depth = 0 val mutable loopNestingDepth = 0 - val gotos = StatementHashTable.create 20 - method! vstmt s = - let after x = - depth <- depth-1; - if depth = 0 then - (* the labels can only be patched once the entire part of the AST we want has been transformed, and *) - (* we know all lables appear in the hash table *) - let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in - let x = visitCilStmt patchLabelsVisitor x in - StatementHashTable.clear gotos; - x - else - x - in + let after x = x in let rename_labels sn = let new_labels = List.map (function Label(str,loc,b) -> Label (Cil.freshLabel str,loc,b) | x -> x) sn.labels in (* this makes new physical copy*) @@ -421,7 +407,6 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object StatementHashTable.add gotos s new_s; new_s in - depth <- depth+1; match s.skind with | Continue loc -> if loopNestingDepth = 0 then @@ -440,6 +425,15 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object | _ -> ChangeDoChildrenPost(rename_labels s, after) end +let copy_and_patch_labels break_target current_continue_target stmts = + let gotos = StatementHashTable.create 20 in + let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target, gotos) in + let stmts' = List.map (visitCilStmt patcher) stmts in + (* the labels can only be patched once the entire part of the AST we want has been transformed, and *) + (* we know all lables appear in the hash table *) + let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in + List.map (visitCilStmt patchLabelsVisitor) stmts' + class loopUnrollingVisitor(func, totalLoops) = object (* Labels are simply handled by giving them a fresh name. Jumps coming from outside will still always go to the original label! *) inherit nopCilVisitor @@ -457,13 +451,7 @@ class loopUnrollingVisitor(func, totalLoops) = object let copies = List.init factor (fun i -> (* continues should go to the next unrolling *) let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in - let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target) in - let one_copy = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in - let one_copy_stmts = (* TODO: avoid this nonsense, directly visiting only b.bstmts breaks some continue labels for some reason *) - match one_copy.skind with - | Block b -> b.bstmts - | _ -> assert false - in + let one_copy_stmts = copy_and_patch_labels break_target current_continue_target b.bstmts in one_copy_stmts @ [current_continue_target] ) in From 7c80a6eae45eb1b2f884e912c92d8f0623f0e4c6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 16:17:50 +0200 Subject: [PATCH 12/14] Add assert test for correct continue unrolling --- .../10-continue-right-place.c | 17 ++ .../10-continue-right-place.t | 173 ++++++++++++++++++ 2 files changed, 190 insertions(+) create mode 100644 tests/regression/55-loop-unrolling/10-continue-right-place.c create mode 100644 tests/regression/55-loop-unrolling/10-continue-right-place.t diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.c b/tests/regression/55-loop-unrolling/10-continue-right-place.c new file mode 100644 index 0000000000..dd31a704c2 --- /dev/null +++ b/tests/regression/55-loop-unrolling/10-continue-right-place.c @@ -0,0 +1,17 @@ +// PARAM: --set lib.activated '["goblint"]' --exp.unrolling-factor 11 +#include + +int main() { + int i = 0; + int j = 10; + while (i <= 10) { + if (i == 5) { + i = 7; + j = 3; + continue; // the continue should jump to the following iteration, not all the way to the unrolled loop + } + __goblint_check(i + j == 10); + i++; j--; + } + return 0; +} diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.t b/tests/regression/55-loop-unrolling/10-continue-right-place.t new file mode 100644 index 0000000000..3313122f03 --- /dev/null +++ b/tests/regression/55-loop-unrolling/10-continue-right-place.t @@ -0,0 +1,173 @@ + $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 11 --enable justcil --set dbg.justcil-printer clean 10-continue-right-place.c + [Info] unrolling loop at 10-continue-right-place.c:7:3-15:3 with factor 11 + extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_assume(int exp ) ; + extern void __goblint_assert(int exp ) ; + extern void __goblint_assume_join() ; + extern void __goblint_globalize(void *ptr ) ; + extern void __goblint_split_begin(int exp ) ; + extern void __goblint_split_end(int exp ) ; + extern void __goblint_bounded(unsigned long long exp ) ; + int main(void) + { + int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j __attribute__((__goblint_array_domain__("unroll"))) ; + + { + i = 0; + j = 10; + { + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_0; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_0: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_1; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_1: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_2; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_2: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_3; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_3: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_4; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_4: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_5; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_5: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_6; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_6: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_7; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_7: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_8; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_8: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_9; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_9: /* CIL Label */ ; + if (! (i <= 10)) { + goto loop_end; + } + if (i == 5) { + i = 7; + j = 3; + goto loop_continue_10; + } + __goblint_check(i + j == 10); + i ++; + j --; + loop_continue_10: /* CIL Label */ ; + { + while (1) { + while_continue: /* CIL Label */ ; + if (! (i <= 10)) { + goto while_break; + } + if (i == 5) { + i = 7; + j = 3; + goto while_continue; + } + __goblint_check(i + j == 10); + i ++; + j --; + } + while_break: /* CIL Label */ ; + } + loop_end: /* CIL Label */ ; + } + return (0); + } + } From 93bfa3b3394625d97fc2d618e9b6814aa0fbdcff Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 16:28:52 +0200 Subject: [PATCH 13/14] Don't add goblint_array_domain attribute to non-array variables --- src/util/loopUnrolling.ml | 2 +- .../55-loop-unrolling/01-simple-cases.t | 31 +++++++++---------- tests/regression/55-loop-unrolling/02-break.t | 4 +-- .../55-loop-unrolling/03-break-right-place.t | 4 +-- .../regression/55-loop-unrolling/04-simple.t | 2 +- .../55-loop-unrolling/05-continue.t | 4 +-- .../06-simple-cases-unrolled.t | 31 +++++++++---------- .../55-loop-unrolling/07-nested-unroll.t | 10 +++--- tests/regression/55-loop-unrolling/09-weird.t | 4 +-- .../10-continue-right-place.t | 6 ++-- 10 files changed, 48 insertions(+), 50 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index d5efd0d937..47f42ca830 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -299,7 +299,7 @@ class arrayVisitor = object inherit nopCilVisitor method! vvrbl info = - if not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then + if Cil.isArrayType info.vtype && not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "unroll"]) ) info.vattr; DoChildren end diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t index a05ee4d010..4baf3c13d4 100644 --- a/tests/regression/55-loop-unrolling/01-simple-cases.t +++ b/tests/regression/55-loop-unrolling/01-simple-cases.t @@ -10,7 +10,7 @@ [Info] unrolling loop at 01-simple-cases.c:157:2-165:2 with factor 5 [Info] unrolling loop at 01-simple-cases.c:174:2-178:2 with factor 5 [Info] unrolling loop at 01-simple-cases.c:187:2-194:2 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -50,7 +50,7 @@ void example1(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -106,7 +106,7 @@ void example2(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -162,7 +162,7 @@ void example3(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -219,8 +219,8 @@ void example4(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int first_iteration ; { i = 0; @@ -319,8 +319,8 @@ void example5(void) { int a[4] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int top __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int top ; { i = 0; @@ -414,7 +414,7 @@ void example6(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; int top ; { @@ -476,7 +476,6 @@ return; } } - int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; int update(int i ) { @@ -492,8 +491,8 @@ void example7(void) { int a[10] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int tmp ; { i = 0; @@ -556,8 +555,8 @@ { int a[5] ; int b[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { b[0] = 0; @@ -886,7 +885,7 @@ void example9(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -958,7 +957,7 @@ void example10(void) { int a[5] ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t index 5f6928002a..cd94f32d6e 100644 --- a/tests/regression/55-loop-unrolling/02-break.t +++ b/tests/regression/55-loop-unrolling/02-break.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int r __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int r ; + int i ; { r = 5; diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t index bc183b00c1..e4d15ae90e 100644 --- a/tests/regression/55-loop-unrolling/03-break-right-place.t +++ b/tests/regression/55-loop-unrolling/03-break-right-place.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t index 49f5cc7e46..da38fd7b13 100644 --- a/tests/regression/55-loop-unrolling/04-simple.t +++ b/tests/regression/55-loop-unrolling/04-simple.t @@ -11,7 +11,7 @@ void main(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t index 6b1601c833..16731ad4e6 100644 --- a/tests/regression/55-loop-unrolling/05-continue.t +++ b/tests/regression/55-loop-unrolling/05-continue.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; void main(void) { - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j ; + int i ; { j = 0; diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t index ae6c4ba147..52fd7d868b 100644 --- a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t +++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t @@ -10,7 +10,7 @@ [Info] unrolling loop at 06-simple-cases-unrolled.c:157:2-165:2 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:174:2-178:2 with factor 5 [Info] unrolling loop at 06-simple-cases-unrolled.c:187:2-194:2 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -50,7 +50,7 @@ void example1(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -106,7 +106,7 @@ void example2(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -162,7 +162,7 @@ void example3(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -219,8 +219,8 @@ void example4(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int first_iteration __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int first_iteration ; { i = 0; @@ -319,8 +319,8 @@ void example5(void) { int a[4] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int top __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int top ; { i = 0; @@ -414,7 +414,7 @@ void example6(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; int top ; { @@ -476,7 +476,6 @@ return; } } - int update(int i ) __attribute__((__goblint_array_domain__("unroll"))) ; int update(int i ) { @@ -492,8 +491,8 @@ void example7(void) { int a[10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int tmp __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int tmp ; { i = 0; @@ -556,8 +555,8 @@ { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; int b[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { b[0] = 0; @@ -886,7 +885,7 @@ void example9(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; @@ -958,7 +957,7 @@ void example10(void) { int a[5] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t index a5c1c2f590..03455b7c8d 100644 --- a/tests/regression/55-loop-unrolling/07-nested-unroll.t +++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t @@ -3,7 +3,7 @@ [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5 [Info] unrolling loop at 07-nested-unroll.c:12:5-16:5 with factor 5 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -14,10 +14,10 @@ int main(void) { int arr[10][10] __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i___0 __attribute__((__goblint_array_domain__("unroll"))) ; - int j___0 __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; + int i___0 ; + int j___0 ; { i = 0; diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t index 606f59acd8..502847c46e 100644 --- a/tests/regression/55-loop-unrolling/09-weird.t +++ b/tests/regression/55-loop-unrolling/09-weird.t @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; void main(void) { - int j __attribute__((__goblint_array_domain__("unroll"))) ; - int i __attribute__((__goblint_array_domain__("unroll"))) ; + int j ; + int i ; { j = 0; diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.t b/tests/regression/55-loop-unrolling/10-continue-right-place.t index 3313122f03..1daab03c52 100644 --- a/tests/regression/55-loop-unrolling/10-continue-right-place.t +++ b/tests/regression/55-loop-unrolling/10-continue-right-place.t @@ -1,6 +1,6 @@ $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 11 --enable justcil --set dbg.justcil-printer clean 10-continue-right-place.c [Info] unrolling loop at 10-continue-right-place.c:7:3-15:3 with factor 11 - extern void __goblint_check(int exp ) __attribute__((__goblint_array_domain__("unroll"))) ; + extern void __goblint_check(int exp ) ; extern void __goblint_assume(int exp ) ; extern void __goblint_assert(int exp ) ; extern void __goblint_assume_join() ; @@ -10,8 +10,8 @@ extern void __goblint_bounded(unsigned long long exp ) ; int main(void) { - int i __attribute__((__goblint_array_domain__("unroll"))) ; - int j __attribute__((__goblint_array_domain__("unroll"))) ; + int i ; + int j ; { i = 0; From ea2f91e3b8e748fc7eccf09d2985467e141c8c35 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 26 Feb 2024 10:34:36 +0200 Subject: [PATCH 14/14] Document clean CIL printer --- src/common/util/cilfacade.ml | 2 ++ src/config/options.schema.json | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 04dcfee606..09aab6088b 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -66,6 +66,8 @@ let parse fileName = E.s (E.error "There were parsing errors in %s" fileName_str); file +(** Version of {!defaultCilPrinterClass} which excludes line directives and builtin signatures (in comments). + Used for [dbg.justcil-printer]. *) class cleanCilPrinterClass = object inherit defaultCilPrinterClass as super diff --git a/src/config/options.schema.json b/src/config/options.schema.json index abba08fca9..14f4530a45 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1862,7 +1862,7 @@ }, "justcil-printer": { "title": "dbg.justcil-printer", - "description": "Printer to use for justcil", + "description": "Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).", "type": "string", "enum": ["default", "clean"], "default": "default"