From b010c1654cf4b281af733f49af76b7792d7f59c0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 21 Feb 2024 12:06:56 +0200 Subject: [PATCH 01/14] Add cram test for YAML witness unrolled loop invariant (issue #1225) --- .../10-unrolled-loop-invariant.c | 6 +++++ .../10-unrolled-loop-invariant.t | 25 +++++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c create mode 100644 tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c new file mode 100644 index 0000000000..39e3cbce49 --- /dev/null +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c @@ -0,0 +1,6 @@ +int main() { + int i = 0; + while (i < 10) + i++; + return 0; +} diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t new file mode 100644 index 0000000000..b80d780211 --- /dev/null +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t @@ -0,0 +1,25 @@ + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c + [Info] unrolling loop at 10-unrolled-loop-invariant.c:3:3-4:8 with factor 5 + [Info][Deadcode] Logical lines of code (LLoC) summary: + live: 5 + dead: 0 + total lines: 5 + [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Info][Witness] witness generation summary: + total generation entries: 4 + + $ cat witness.yml | grep -A 1 'value:' + value: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) || + i == 0 + -- + value: i == 10 + format: c_expression + -- + value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) || + i == 0 + + From 598d541a813370c5cd34511e76e89a8d5f1669b7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 15:10:57 +0300 Subject: [PATCH 02/14] Attempt to record statement copies during loop unrolling --- src/util/loopUnrolling.ml | 4 + src/witness/yamlWitness.ml | 10 ++ .../10-unrolled-loop-invariant.t | 121 +++++++++++++++++- 3 files changed, 134 insertions(+), 1 deletion(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index d5efd0d937..c1da3de52b 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -384,6 +384,8 @@ class patchLabelsGotosVisitor(newtarget) = object | _ -> DoChildren end +let copyof = StatementHashTable.create 113 + (* Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with goto currentIterationEnd @@ -401,6 +403,8 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object 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*) let new_s = {sn with labels = new_labels} in + StatementHashTable.replace copyof new_s s; + Logs.debug "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s; if new_s.labels <> [] then (* Use original s, ns might be temporay e.g. if the type of statement changed *) (* record that goto s; appearing in the current fragment should later be patched to goto new_s *) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index d9d39ccee1..89cb877c5a 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -289,6 +289,16 @@ struct LH.fold (fun loc ns acc -> if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( let inv = List.fold_left (fun acc n -> + begin match n with + | Node.Statement s -> + begin match LoopUnrolling.StatementHashTable.find_opt LoopUnrolling.copyof s with + | Some s' -> + Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' + | None -> + Logs.debug "%a is not a copy" Node.pretty n + end + | _ -> () + end; let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t index b80d780211..719e23ddfd 100644 --- a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t @@ -1,5 +1,118 @@ - $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c --set dbg.level debug + [Debug] 2024-04-02 15:10:01 + [Debug] 'goblint' '--set' 'lib.activated' '[]' '--set' 'exp.unrolling-factor' '5' '--enable' 'ana.int.interval' '--enable' 'witness.yaml.enabled' '10-unrolled-loop-invariant.c' '--set' 'dbg.level' 'debug' + [Debug] Custom include dirs: + [Debug] 1. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/include (exists=true) + [Debug] 2. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/runtime/include (exists=true) + [Debug] 3. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/src (exists=true) + [Debug] Preprocessing files. + [Debug] Preprocessor cpp: is_bad=false + [Debug] 'cpp' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/include' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/runtime/include' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/src' '10-unrolled-loop-invariant.c' '-o' '.goblint/preprocessed/10-unrolled-loop-invariant.i' + [Debug] Parsing files. + Frontc is parsing .goblint/preprocessed/10-unrolled-loop-invariant.i + Converting CABS->CIL + [Debug] Constructors: + [Debug] Adding constructors to: main [Info] unrolling loop at 10-unrolled-loop-invariant.c:3:3-4:8 with factor 5 + [Debug] Marking if (! (i < 10)) { + break; + } as copy of if (! (i < 10)) { + break; + } + [Debug] Marking goto loop_end; as copy of break; + [Debug] Marking { + i ++; + } as copy of { + i ++; + } + [Debug] Marking i ++; as copy of i ++; + [Debug] Marking if (! (i < 10)) { + break; + } as copy of if (! (i < 10)) { + break; + } + [Debug] Marking goto loop_end; as copy of break; + [Debug] Marking { + i ++; + } as copy of { + i ++; + } + [Debug] Marking i ++; as copy of i ++; + [Debug] Marking if (! (i < 10)) { + break; + } as copy of if (! (i < 10)) { + break; + } + [Debug] Marking goto loop_end; as copy of break; + [Debug] Marking { + i ++; + } as copy of { + i ++; + } + [Debug] Marking i ++; as copy of i ++; + [Debug] Marking if (! (i < 10)) { + break; + } as copy of if (! (i < 10)) { + break; + } + [Debug] Marking goto loop_end; as copy of break; + [Debug] Marking { + i ++; + } as copy of { + i ++; + } + [Debug] Marking i ++; as copy of i ++; + [Debug] Marking if (! (i < 10)) { + break; + } as copy of if (! (i < 10)) { + break; + } + [Debug] Marking goto loop_end; as copy of break; + [Debug] Marking { + i ++; + } as copy of { + i ++; + } + [Debug] Marking i ++; as copy of i ++; + [Debug] And now... the Goblin! + [Debug] Startfuns: [main] + Exitfuns: [] + Otherfuns: [] + [Debug] Activated analyses: expRelation, base, threadid, threadflag, threadreturn, escape, mutexEvents, mutex, access, race, mallocWrapper, mhp, assert + [Debug] Activated transformations: + [Debug] Generating the control flow graph. + [Debug] cfgF (bindings=16 buckets=128 max_length=1 histo=112,16 load=0.125000), cfgB (bindings=16 buckets=128 max_length=1 histo=112,16 load=0.125000) + [Debug] Initializing 0 globals. + [Debug] Executing 1 assigns. + [Debug] Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1. + + [Debug] Unstable solver start vars in 1. phase: + [Debug] L:call of main (297) on 10-unrolled-loop-invariant.c:1:1-6:1 + + [Debug] Data after solve completed: + [Debug] |rho|=23 + [Debug] |stable|=23 + [Debug] |infl|=23 + [Debug] |wpoint|=0 + [Debug] |sides|=7 + [Debug] |side_dep|=0 + [Debug] |side_infl|=0 + [Debug] |var_messages|=0 + [Debug] |rho_write|=0 + [Debug] |dep|=15 + [Debug] Postsolving + [Debug] Pruning result + [Debug] Data after postsolve: + [Debug] |rho|=24 + [Debug] |stable|=24 + [Debug] |infl|=23 + [Debug] |wpoint|=0 + [Debug] |sides|=7 + [Debug] |side_dep|=8 + [Debug] |side_infl|=9 + [Debug] |var_messages|=0 + [Debug] |rho_write|=8 + [Debug] |dep|=15 [Info][Deadcode] Logical lines of code (LLoC) summary: live: 5 dead: 0 @@ -9,6 +122,12 @@ [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Debug] node 31 "i < 10" is not a copy + [Debug] node 23 "i < 10" is not a copy + [Debug] node 18 "i < 10" is not a copy + [Debug] node 13 "i < 10" is not a copy + [Debug] node 8 "i < 10" is not a copy + [Debug] node 3 "i < 10" is not a copy [Info][Witness] witness generation summary: total generation entries: 4 From 3dd76bd46cc4b704ca36cc64cc83a9d5fdcc0adb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 15:20:45 +0300 Subject: [PATCH 03/14] Add TODO about nested unrolled loops for copyof --- src/witness/yamlWitness.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 89cb877c5a..ed04ab5a23 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -291,6 +291,7 @@ struct let inv = List.fold_left (fun acc n -> begin match n with | Node.Statement s -> + (* TODO: need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) begin match LoopUnrolling.StatementHashTable.find_opt LoopUnrolling.copyof s with | Some s' -> Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' From d823989c971b7fd80d20719eb1d7354c51538c3d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 17:17:54 +0300 Subject: [PATCH 04/14] Use special stmt hash function for LoopUnrolling.copyof --- src/util/loopUnrolling.ml | 13 +++++++++-- src/witness/yamlWitness.ml | 2 +- .../10-unrolled-loop-invariant.t | 23 +++++++++++++------ 3 files changed, 28 insertions(+), 10 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index c1da3de52b..22e982fa15 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -384,7 +384,16 @@ class patchLabelsGotosVisitor(newtarget) = object | _ -> DoChildren end -let copyof = StatementHashTable.create 113 +module CopyOfHashTable = Hashtbl.Make(struct + type t = stmt + (* Identity by physical equality. *) + let equal = (==) + (* Hash only labels and skind (statement itself) because they should remain unchanged between now + and lookup after analysis. + CFG construction modifies sid, succs, preds and fallthrough, which are empty here.*) + let hash (s: stmt) = Hashtbl.hash (s.skind, s.labels) + end) +let copyof = CopyOfHashTable.create 113 (* Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with @@ -403,7 +412,7 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object 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*) let new_s = {sn with labels = new_labels} in - StatementHashTable.replace copyof new_s s; + CopyOfHashTable.replace copyof new_s s; Logs.debug "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s; if new_s.labels <> [] then (* Use original s, ns might be temporay e.g. if the type of statement changed *) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index ed04ab5a23..b51584b37e 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -292,7 +292,7 @@ struct begin match n with | Node.Statement s -> (* TODO: need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) - begin match LoopUnrolling.StatementHashTable.find_opt LoopUnrolling.copyof s with + begin match LoopUnrolling.CopyOfHashTable.find_opt LoopUnrolling.copyof s with | Some s' -> Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' | None -> diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t index 719e23ddfd..a80f955609 100644 --- a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t @@ -1,5 +1,4 @@ - $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c --set dbg.level debug - [Debug] 2024-04-02 15:10:01 + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 10-unrolled-loop-invariant.c --set dbg.level debug 2>&1 | tail -n +2 [Debug] 'goblint' '--set' 'lib.activated' '[]' '--set' 'exp.unrolling-factor' '5' '--enable' 'ana.int.interval' '--enable' 'witness.yaml.enabled' '10-unrolled-loop-invariant.c' '--set' 'dbg.level' 'debug' [Debug] Custom include dirs: [Debug] 1. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/include (exists=true) @@ -123,11 +122,21 @@ [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Debug] node 31 "i < 10" is not a copy - [Debug] node 23 "i < 10" is not a copy - [Debug] node 18 "i < 10" is not a copy - [Debug] node 13 "i < 10" is not a copy - [Debug] node 8 "i < 10" is not a copy - [Debug] node 3 "i < 10" is not a copy + [Debug] node 23 "i < 10" is copy of if (! (i < 10)) { + goto while_break; + } + [Debug] node 18 "i < 10" is copy of if (! (i < 10)) { + goto while_break; + } + [Debug] node 13 "i < 10" is copy of if (! (i < 10)) { + goto while_break; + } + [Debug] node 8 "i < 10" is copy of if (! (i < 10)) { + goto while_break; + } + [Debug] node 3 "i < 10" is copy of if (! (i < 10)) { + goto while_break; + } [Info][Witness] witness generation summary: total generation entries: 4 From 79707e63c8a4b30090e49304354b29f97129d660 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 17:28:21 +0300 Subject: [PATCH 05/14] Add recursive LoopUnrolling.find_original function --- src/util/loopUnrolling.ml | 6 ++++++ src/witness/yamlWitness.ml | 12 +++++------- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 22e982fa15..7778ca756e 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -395,6 +395,12 @@ module CopyOfHashTable = Hashtbl.Make(struct end) let copyof = CopyOfHashTable.create 113 +let rec find_original s = + (* TODO: actually need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) + match CopyOfHashTable.find_opt copyof s with + | None -> s + | Some s' -> (find_original [@tailcall]) s' + (* Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with goto currentIterationEnd diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index b51584b37e..2f5f03c22d 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -291,13 +291,11 @@ struct let inv = List.fold_left (fun acc n -> begin match n with | Node.Statement s -> - (* TODO: need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) - begin match LoopUnrolling.CopyOfHashTable.find_opt LoopUnrolling.copyof s with - | Some s' -> - Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' - | None -> - Logs.debug "%a is not a copy" Node.pretty n - end + let s' = LoopUnrolling.find_original s in + if s != s' then + Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' + else + Logs.debug "%a is not a copy" Node.pretty n | _ -> () end; let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in From 5a59328de95ab4d2b52f1d24a722fbdcfba423d7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 17:28:32 +0300 Subject: [PATCH 06/14] Add interface for LoopUnrolling --- src/util/loopUnrolling.ml | 2 -- src/util/loopUnrolling.mli | 9 +++++++++ 2 files changed, 9 insertions(+), 2 deletions(-) create mode 100644 src/util/loopUnrolling.mli diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 7778ca756e..d9347598cf 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -1,5 +1,3 @@ -(** Syntactic loop unrolling. *) - open GobConfig open GoblintCil diff --git a/src/util/loopUnrolling.mli b/src/util/loopUnrolling.mli new file mode 100644 index 0000000000..ea45688c77 --- /dev/null +++ b/src/util/loopUnrolling.mli @@ -0,0 +1,9 @@ +(** Syntactic loop unrolling. *) + +val unroll_loops: GoblintCil.fundec -> int -> unit +(** Unroll loops in a function. + + @param totalLoops total number of loops from autotuner *) + +val find_original: GoblintCil.stmt -> GoblintCil.stmt +(** Find original un-unrolled instance of the statement. *) From db8f25f9700197150b450acf7148e5040d87707e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 17:41:08 +0300 Subject: [PATCH 07/14] Add sid-s to loop unrolling copy of output --- src/witness/yamlWitness.ml | 2 +- .../55-loop-unrolling/10-unrolled-loop-invariant.t | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 2f5f03c22d..92e09c238d 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -293,7 +293,7 @@ struct | Node.Statement s -> let s' = LoopUnrolling.find_original s in if s != s' then - Logs.debug "%a is copy of %a" Node.pretty n CilType.Stmt.pretty s' + Logs.debug "%a is copy of %a (%d)" Node.pretty n CilType.Stmt.pretty s' s'.sid else Logs.debug "%a is not a copy" Node.pretty n | _ -> () diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t index a80f955609..5cd0c2f449 100644 --- a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t @@ -124,19 +124,19 @@ [Debug] node 31 "i < 10" is not a copy [Debug] node 23 "i < 10" is copy of if (! (i < 10)) { goto while_break; - } + } (31) [Debug] node 18 "i < 10" is copy of if (! (i < 10)) { goto while_break; - } + } (31) [Debug] node 13 "i < 10" is copy of if (! (i < 10)) { goto while_break; - } + } (31) [Debug] node 8 "i < 10" is copy of if (! (i < 10)) { goto while_break; - } + } (31) [Debug] node 3 "i < 10" is copy of if (! (i < 10)) { goto while_break; - } + } (31) [Info][Witness] witness generation summary: total generation entries: 4 From 1434d8191743e789a56bbc556b8cf5dcc406f0f6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 2 Apr 2024 18:01:27 +0300 Subject: [PATCH 08/14] Test LoopUnrolling.find_original on nested loop --- .../10-unrolled-loop-invariant.c | 7 + .../10-unrolled-loop-invariant.t | 1200 ++++++++++++++++- 2 files changed, 1189 insertions(+), 18 deletions(-) diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c index 39e3cbce49..096c031cf1 100644 --- a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.c @@ -2,5 +2,12 @@ int main() { int i = 0; while (i < 10) i++; + + int j = 0, k = 0; + while (j < 10) { + while (k < 100) + k++; + j++; + } return 0; } diff --git a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t index 5cd0c2f449..612158f522 100644 --- a/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/10-unrolled-loop-invariant.t @@ -73,6 +73,988 @@ i ++; } [Debug] Marking i ++; as copy of i ++; + [Info] unrolling loop at 10-unrolled-loop-invariant.c:8:5-9:10 with factor 5 + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking goto loop_end___0; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking goto loop_end___0; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking goto loop_end___0; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking goto loop_end___0; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking goto loop_end___0; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Info] unrolling loop at 10-unrolled-loop-invariant.c:7:3-11:3 with factor 5 + [Debug] Marking if (! (j < 10)) { + break; + } as copy of if (! (j < 10)) { + break; + } + [Debug] Marking goto loop_end___1; as copy of break; + [Debug] Marking { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } as copy of { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_0___2: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_1___1: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_2___1: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_3___1: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_4___1: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; + [Debug] Marking while (k < 100) { + { + k ++; + } + } as copy of while (k < 100) { + { + k ++; + } + } + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking break; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_end___2: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; + [Debug] Marking { + j ++; + } as copy of { + j ++; + } + [Debug] Marking j ++; as copy of j ++; + [Debug] Marking if (! (j < 10)) { + break; + } as copy of if (! (j < 10)) { + break; + } + [Debug] Marking goto loop_end___1; as copy of break; + [Debug] Marking { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } as copy of { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_0___3: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_1___3: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_2___2: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_3___2: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_4___2: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; + [Debug] Marking while (k < 100) { + { + k ++; + } + } as copy of while (k < 100) { + { + k ++; + } + } + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking break; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_end___3: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; + [Debug] Marking { + j ++; + } as copy of { + j ++; + } + [Debug] Marking j ++; as copy of j ++; + [Debug] Marking if (! (j < 10)) { + break; + } as copy of if (! (j < 10)) { + break; + } + [Debug] Marking goto loop_end___1; as copy of break; + [Debug] Marking { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } as copy of { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_0___4: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_1___4: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_2___4: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_3___3: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_4___3: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; + [Debug] Marking while (k < 100) { + { + k ++; + } + } as copy of while (k < 100) { + { + k ++; + } + } + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking break; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_end___4: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; + [Debug] Marking { + j ++; + } as copy of { + j ++; + } + [Debug] Marking j ++; as copy of j ++; + [Debug] Marking if (! (j < 10)) { + break; + } as copy of if (! (j < 10)) { + break; + } + [Debug] Marking goto loop_end___1; as copy of break; + [Debug] Marking { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } as copy of { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_0___5: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_1___5: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_2___5: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_3___5: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_4___4: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; + [Debug] Marking while (k < 100) { + { + k ++; + } + } as copy of while (k < 100) { + { + k ++; + } + } + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking break; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_end___5: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; + [Debug] Marking { + j ++; + } as copy of { + j ++; + } + [Debug] Marking j ++; as copy of j ++; + [Debug] Marking if (! (j < 10)) { + break; + } as copy of if (! (j < 10)) { + break; + } + [Debug] Marking goto loop_end___1; as copy of break; + [Debug] Marking { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } as copy of { + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_0___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_1___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_2___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_3___0: /* CIL Label */ ; + if (! (k < 100)) { + goto loop_end___0; + } + { + k ++; + } + loop_continue_4___0: /* CIL Label */ ; + while (k < 100) { + { + k ++; + } + } + loop_end___0: /* CIL Label */ ; + } + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_0___6: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_1___6: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_2___6: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_3___6: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; + [Debug] Marking if (! (k < 100)) { + goto loop_end___0; + } as copy of if (! (k < 100)) { + goto loop_end___0; + } + [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_continue_4___6: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; + [Debug] Marking while (k < 100) { + { + k ++; + } + } as copy of while (k < 100) { + { + k ++; + } + } + [Debug] Marking if (! (k < 100)) { + break; + } as copy of if (! (k < 100)) { + break; + } + [Debug] Marking break; as copy of break; + [Debug] Marking { + k ++; + } as copy of { + k ++; + } + [Debug] Marking k ++; as copy of k ++; + [Debug] Marking loop_end___6: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; + [Debug] Marking { + j ++; + } as copy of { + j ++; + } + [Debug] Marking j ++; as copy of j ++; [Debug] And now... the Goblin! [Debug] Startfuns: [main] Exitfuns: [] @@ -80,47 +1062,168 @@ [Debug] Activated analyses: expRelation, base, threadid, threadflag, threadreturn, escape, mutexEvents, mutex, access, race, mallocWrapper, mhp, assert [Debug] Activated transformations: [Debug] Generating the control flow graph. - [Debug] cfgF (bindings=16 buckets=128 max_length=1 histo=112,16 load=0.125000), cfgB (bindings=16 buckets=128 max_length=1 histo=112,16 load=0.125000) + [Debug] cfgF (bindings=102 buckets=128 max_length=3 histo=60,37,28,3 load=0.796875), cfgB (bindings=102 buckets=128 max_length=3 histo=59,40,25,4 load=0.796875) [Debug] Initializing 0 globals. [Debug] Executing 1 assigns. [Debug] Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1. [Debug] Unstable solver start vars in 1. phase: - [Debug] L:call of main (297) on 10-unrolled-loop-invariant.c:1:1-6:1 + [Debug] L:call of main (297) on 10-unrolled-loop-invariant.c:1:1-13:1 [Debug] Data after solve completed: - [Debug] |rho|=23 - [Debug] |stable|=23 - [Debug] |infl|=23 + [Debug] |rho|=126 + [Debug] |stable|=126 + [Debug] |infl|=126 [Debug] |wpoint|=0 - [Debug] |sides|=7 + [Debug] |sides|=24 [Debug] |side_dep|=0 [Debug] |side_infl|=0 [Debug] |var_messages|=0 [Debug] |rho_write|=0 - [Debug] |dep|=15 + [Debug] |dep|=101 [Debug] Postsolving [Debug] Pruning result [Debug] Data after postsolve: - [Debug] |rho|=24 - [Debug] |stable|=24 - [Debug] |infl|=23 + [Debug] |rho|=127 + [Debug] |stable|=127 + [Debug] |infl|=126 [Debug] |wpoint|=0 - [Debug] |sides|=7 - [Debug] |side_dep|=8 - [Debug] |side_infl|=9 + [Debug] |sides|=24 + [Debug] |side_dep|=25 + [Debug] |side_infl|=33 [Debug] |var_messages|=0 - [Debug] |rho_write|=8 - [Debug] |dep|=15 + [Debug] |rho_write|=32 + [Debug] |dep|=101 [Info][Deadcode] Logical lines of code (LLoC) summary: - live: 5 + live: 10 dead: 0 - total lines: 5 + total lines: 10 + [Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:7:10-7:16) + [Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:7:10-7:16) + [Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (10-unrolled-loop-invariant.c:8:12-8:19) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) [Warning][Deadcode][CWE-571] condition 'i < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:3:10-3:16) + [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:7:10-7:16) + [Warning][Deadcode][CWE-570] condition 'k < 100' (possibly inserted by CIL) is always false (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:7:10-7:16) + [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:8:12-8:19) + [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (10-unrolled-loop-invariant.c:7:10-7:16) + [Debug] node 124 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 252 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 247 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 112 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 104 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 232 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 99 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 224 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 94 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 219 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 89 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 214 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 84 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 209 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 204 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 72 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 64 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 192 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 59 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 184 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 54 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 179 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 49 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 174 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 44 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 169 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 164 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 152 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 275 "k < 100" is not a copy + [Debug] node 144 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 139 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 267 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 134 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 262 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 129 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) + [Debug] node 257 "k < 100" is copy of if (! (k < 100)) { + goto while_break___6; + } (275) [Debug] node 31 "i < 10" is not a copy [Debug] node 23 "i < 10" is copy of if (! (i < 10)) { goto while_break; @@ -137,17 +1240,78 @@ [Debug] node 3 "i < 10" is copy of if (! (i < 10)) { goto while_break; } (31) + [Debug] node 121 "j < 10" is copy of if (! (j < 10)) { + goto while_break___5; + } (244) + [Debug] node 244 "j < 10" is not a copy + [Debug] node 81 "j < 10" is copy of if (! (j < 10)) { + goto while_break___5; + } (244) + [Debug] node 201 "j < 10" is copy of if (! (j < 10)) { + goto while_break___5; + } (244) + [Debug] node 41 "j < 10" is copy of if (! (j < 10)) { + goto while_break___5; + } (244) + [Debug] node 161 "j < 10" is copy of if (! (j < 10)) { + goto while_break___5; + } (244) [Info][Witness] witness generation summary: - total generation entries: 4 + total generation entries: 19 $ cat witness.yml | grep -A 1 'value:' + value: i == 10 + format: c_expression + -- + value: j == 0 + format: c_expression + -- + value: (((((5 <= k && k <= 99) || k == 4) || k == 3) || k == 2) || k == 1) || + k == 0 + -- + value: i == 10 + format: c_expression + -- + value: j == 10 + format: c_expression + -- + value: k == 100 + format: c_expression + -- value: (((((5 <= i && i <= 9) || i == 4) || i == 3) || i == 2) || i == 1) || i == 0 -- value: i == 10 format: c_expression + -- + value: j == 0 + format: c_expression + -- + value: i == 10 + format: c_expression + -- + value: k == 100 + format: c_expression + -- + value: ((((j == 1 || j == 4) || j == 0) || j == 3) || j == 2) || (5 <= j && + j <= 9) + -- + value: i == 10 + format: c_expression + -- + value: i == 10 + format: c_expression + -- + value: (((((((k == 100 && (((j == 2 || (5 <= j && j <= 9)) || j == 1) || j == + 4)) || ((5 <= k && k <= 100) && j == 0)) || (j == 0 && k == 4)) || (j == 0 -- value: (((((5 <= i && i <= 10) || i == 4) || i == 3) || i == 2) || i == 1) || i == 0 + -- + value: i == 10 + format: c_expression + -- + value: ((k == 100 && (((j == 2 || (5 <= j && j <= 10)) || j == 1) || j == 4)) + || (j == 0 && k == 0)) || (j == 3 && k == 100) From dd51f86021a81310ae2703ea16f7abdbf3033f0c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 Apr 2024 10:39:00 +0300 Subject: [PATCH 09/14] Add option dbg.cfg.loop-unrolling --- src/common/framework/cfgTools.ml | 10 +++++++++- src/common/util/loopUnrolling0.ml | 18 ++++++++++++++++++ src/config/options.schema.json | 6 ++++++ src/util/loopUnrolling.ml | 17 +---------------- 4 files changed, 34 insertions(+), 17 deletions(-) create mode 100644 src/common/util/loopUnrolling0.ml diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index 77460f9f41..c39371c754 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -559,7 +559,15 @@ struct | FunctionEntry _ -> ["shape=box"] in let styles = String.concat "," (label @ shape @ extraNodeStyles n) in - Format.fprintf out ("\t%a [%s];\n") p_node n styles + Format.fprintf out ("\t%a [%s];\n") p_node n styles; + match n with + | Statement s when get_bool "dbg.cfg.loop-unrolling" -> + let s' = LoopUnrolling0.find_original s in + if s != s' then ( + let n' = Statement s' in + Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n' + ) + | _ -> () end let fprint_dot (module CfgPrinters: CfgPrinters) iter_edges out = diff --git a/src/common/util/loopUnrolling0.ml b/src/common/util/loopUnrolling0.ml new file mode 100644 index 0000000000..34b5043f4b --- /dev/null +++ b/src/common/util/loopUnrolling0.ml @@ -0,0 +1,18 @@ +open GoblintCil + +module CopyOfHashTable = Hashtbl.Make(struct + type t = stmt + (* Identity by physical equality. *) + let equal = (==) + (* Hash only labels and skind (statement itself) because they should remain unchanged between now + and lookup after analysis. + CFG construction modifies sid, succs, preds and fallthrough, which are empty here.*) + let hash (s: stmt) = Hashtbl.hash (s.skind, s.labels) + end) +let copyof = CopyOfHashTable.create 113 + +let rec find_original s = + (* TODO: actually need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) + match CopyOfHashTable.find_opt copyof s with + | None -> s + | Some s' -> (find_original [@tailcall]) s' diff --git a/src/config/options.schema.json b/src/config/options.schema.json index abba08fca9..93b766e5ff 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -1984,6 +1984,12 @@ "description": "Add loop SCC clusters to CFG .dot output.", "type": "boolean", "default": false + }, + "loop-unrolling": { + "title": "dbg.cfg.loop-unrolling", + "description": "Add dotted loop unrolling copy-of edges to CFG .dot output.", + "type": "boolean", + "default": false } }, "additionalProperties": false diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index d9347598cf..c16949f0ea 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -382,22 +382,7 @@ class patchLabelsGotosVisitor(newtarget) = object | _ -> DoChildren end -module CopyOfHashTable = Hashtbl.Make(struct - type t = stmt - (* Identity by physical equality. *) - let equal = (==) - (* Hash only labels and skind (statement itself) because they should remain unchanged between now - and lookup after analysis. - CFG construction modifies sid, succs, preds and fallthrough, which are empty here.*) - let hash (s: stmt) = Hashtbl.hash (s.skind, s.labels) - end) -let copyof = CopyOfHashTable.create 113 - -let rec find_original s = - (* TODO: actually need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) - match CopyOfHashTable.find_opt copyof s with - | None -> s - | Some s' -> (find_original [@tailcall]) s' +include LoopUnrolling0 (* Makes a copy, replacing top-level breaks with goto loopEnd and top-level continues with From 55ef8b6fb1f45ac4732e3f6ac43c53fd3ced1405 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 Apr 2024 10:43:28 +0300 Subject: [PATCH 10/14] Make dbg.cfg.loop-unrolling non-recursive This makes the graph simpler and layouting faster. --- src/common/framework/cfgTools.ml | 11 ++++++----- src/common/util/loopUnrolling0.ml | 5 +++-- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index c39371c754..5c59c8c59d 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -562,11 +562,12 @@ struct Format.fprintf out ("\t%a [%s];\n") p_node n styles; match n with | Statement s when get_bool "dbg.cfg.loop-unrolling" -> - let s' = LoopUnrolling0.find_original s in - if s != s' then ( - let n' = Statement s' in - Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n' - ) + begin match LoopUnrolling0.find_copyof s with + | Some s' -> + let n' = Statement s' in + Format.fprintf out "\t%a -> %a [style=dotted];\n" p_node n p_node n' + | None -> () + end | _ -> () end diff --git a/src/common/util/loopUnrolling0.ml b/src/common/util/loopUnrolling0.ml index 34b5043f4b..02e1ae7fdc 100644 --- a/src/common/util/loopUnrolling0.ml +++ b/src/common/util/loopUnrolling0.ml @@ -11,8 +11,9 @@ module CopyOfHashTable = Hashtbl.Make(struct end) let copyof = CopyOfHashTable.create 113 +let find_copyof = CopyOfHashTable.find_opt copyof + let rec find_original s = - (* TODO: actually need to recursively follow copies in case of nested unrolled loops? kind of like union-find *) - match CopyOfHashTable.find_opt copyof s with + match find_copyof s with | None -> s | Some s' -> (find_original [@tailcall]) s' From 215c50c461137f3f9e70512106d854186abbf527 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 Apr 2024 11:26:46 +0300 Subject: [PATCH 11/14] Test unrolled loop CFG --- .../11-unrolled-loop-invariant.t | 141 ++++++++++++++++++ tests/regression/cfg/util/cfgDot.ml | 25 +++- tests/regression/cfg/util/dune | 1 + 3 files changed, 165 insertions(+), 2 deletions(-) diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index 5556706814..7b319f431e 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -1,3 +1,144 @@ + $ cfgDot --unroll 1 11-unrolled-loop-invariant.c + [Info] unrolling loop at 11-unrolled-loop-invariant.c:3:3-4:8 with factor 1 + [Info] unrolling loop at 11-unrolled-loop-invariant.c:8:5-9:10 with factor 1 + [Info] unrolling loop at 11-unrolled-loop-invariant.c:7:3-11:3 with factor 1 + + $ graph-easy --as=boxart main.dot + ┌──────────────────────────────────────────────────────┐ + │ main() │ + └──────────────────────────────────────────────────────┘ + │ + │ (body) + ▼ + ┌──────────────────────────────────────────────────────┐ + │ 11-unrolled-loop-invariant.c:2:7-2:12 │ + │ (11-unrolled-loop-invariant.c:2:7-2:12) │ + └──────────────────────────────────────────────────────┘ + │ + │ i = 0 + ▼ + ┌──────────────────────────────────────────────────────┐ + │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic) │ + ┌───────────── │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ ·┐ + │ └──────────────────────────────────────────────────────┘ : + │ │ : + │ │ Pos(i < 10) : + │ ▼ : + │ ┌──────────────────────────────────────────────────────┐ : + │ │ 11-unrolled-loop-invariant.c:4:5-4:8 │ : + │ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ ·┼··························································┐ + │ └──────────────────────────────────────────────────────┘ : : + │ │ : : + │ Neg(i < 10) │ i = i + 1 : : + │ ▼ ▼ : + │ ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : + │ │ 11-unrolled-loop-invariant.c:3:3-4:8 (synthetic) │ : + │ │ (11-unrolled-loop-invariant.c:3:10-3:16 (synthetic)) │ : + │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : + │ │ │ ▲ : + │ │ Neg(i < 10) │ Pos(i < 10) │ i = i + 1 : + │ ▼ │ │ : + │ ┌──────────────────────────────────────────────────────┐ │ ┌─────────────────────────────────────────┐ : + │ │ 11-unrolled-loop-invariant.c:6:7-6:12 │ │ │ 11-unrolled-loop-invariant.c:4:5-4:8 │ : + └────────────▶ │ (11-unrolled-loop-invariant.c:6:7-6:12) │ └───────────▶ │ (11-unrolled-loop-invariant.c:4:5-4:8) │ ◀┘ + └──────────────────────────────────────────────────────┘ └─────────────────────────────────────────┘ + │ + │ j = 0 + ▼ + ┌──────────────────────────────────────────────────────┐ + │ 11-unrolled-loop-invariant.c:6:14-6:19 │ + │ (11-unrolled-loop-invariant.c:6:14-6:19) │ + └──────────────────────────────────────────────────────┘ + │ + │ k = 0 + ▼ + ┌──────────────────────────────────────────────────────┐ ┌─────────────────────────────────────────┐ ┌──────────────────┐ + │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ Neg(j < 10) │ 11-unrolled-loop-invariant.c:12:3-12:11 │ return 0 │ return of main() │ + ┌············· │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ ─────────────▶ │ (unknown) │ ──────────▶ │ │ + : └──────────────────────────────────────────────────────┘ └─────────────────────────────────────────┘ └──────────────────┘ + : │ ▲ Neg(j < 10) + : │ Pos(j < 10) └────────────────────────────────────────────────────────────────────────────────┐ + : ▼ │ + : ┌──────────────────────────────────────────────────────┐ │ + : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ │ + ┌──────────────────────────┼───────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ····························································┐ │ + │ : └──────────────────────────────────────────────────────┘ : │ + │ : │ : │ + │ : │ Pos(k < 100) : │ + │ : ▼ : │ + │ : ┌──────────────────────────────────────────────────────┐ : │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ + │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ····························································┼············┐ │ + │ : └──────────────────────────────────────────────────────┘ : : │ + │ : │ : : │ + │ : │ k = k + 1 ┌──────────────────────────────────────────┼────────────┼────────────────────────┼─────────────┐ + │ : ▼ │ : : │ │ + │ : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ + │ : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ + │ : │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ : : │ │ + │ : └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ + │ : │ : ▲ : : │ │ + │ : │ Pos(k < 100) : │ k = k + 1 : : │ │ + │ : ▼ : │ : : │ │ + │ : ┌──────────────────────────────────────────────────────┐ : │ : : │ │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ : : │ │ + │ : │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ─┼───────────────┘ : : │ │ + │ : └──────────────────────────────────────────────────────┘ : : : │ │ + │ : : : : : │ │ + ┌────┘ : : : : : │ │ + │ : ▼ : : : │ │ + │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ + │ : │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : : : │ │ + │ ┌··························┼············▶ │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ◀┼───────────────┐ : : │ │ + │ : : └──────────────────────────────────────────────────────┘ : │ : : │ │ + │ : : │ : │ : : │ │ + │ : : │ k = k + 1 : │ Pos(k < 100) : : │ │ + │ : : ▼ ▼ │ : : │ │ + │ : : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : │ │ + │ : k = k + 1 : │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : │ │ + │ : ┌─────────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ◀┼············┼···················┐ │ │ + │ : │ : └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ + │ : │ : │ : : : │ │ + │ : │ : │ Neg(k < 100) : : : │ │ + │ : │ : ▼ : : : │ │ + │ : │ : ┌──────────────────────────────────────────────────────┐ : : : │ │ + │ : │ : │ 11-unrolled-loop-invariant.c:10:5-10:8 │ : : : │ │ + │ : │ ┌────────────────┼────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8) │ ◀···························································┼············┼···················┼····┼·············┼····┐ + │ : │ │ : └──────────────────────────────────────────────────────┘ : : : │ │ : + │ : │ │ : │ : : : │ │ : + │ : │ │ : │ j = j + 1 ┌──────────────────────────────────────────┼────────────┼───────────────────┼────┘ │ : + │ : │ │ : ▼ │ : : : │ : + │ : │ │ : ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ : + │ : │ │ : │ 11-unrolled-loop-invariant.c:7:3-11:3 (synthetic) │ : : : │ : + │ : │ │ Neg(k < 100) └············▶ │ (11-unrolled-loop-invariant.c:7:10-7:16 (synthetic)) │ ◀┼────────────┼───────────────────┼────┐ │ : + │ : │ │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : : │ │ : + │ : │ │ │ : : : │ │ : + │ : │ │ │ Pos(j < 10) : : : │ │ : + │ : │ │ ▼ : : : │ │ : + │ : │ │ ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ : : : │ │ : + │ : │ │ │ 11-unrolled-loop-invariant.c:8:5-9:10 (synthetic) │ : : : │ │ : + │ : │ └────────────────────────────── │ (11-unrolled-loop-invariant.c:8:12-8:19 (synthetic)) │ ◀┘ : : │ j = j + 1 │ : + │ : │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ : : │ │ : + │ : │ │ : : : │ │ : + │ : │ │ Pos(k < 100) └·······················································┼···················┘ │ │ : + │ : │ ▼ : │ │ : + │ : │ ┌──────────────────────────────────────────────────────┐ : │ │ : + │ : │ │ 11-unrolled-loop-invariant.c:9:7-9:10 │ : │ │ : + │ : └─────────────────────────────────── │ (11-unrolled-loop-invariant.c:9:7-9:10) │ ◀········································································┘ ┌····┼·············┼····┘ + │ : └──────────────────────────────────────────────────────┘ : │ │ + │ : : : │ │ + │ └···········································┘ : │ │ + │ : │ │ + │ : │ │ + │ ┌···················································································································································┘ │ │ + │ : │ │ + │ ┌──────────────────────────────────────────────────────┐ │ │ + │ Neg(k < 100) │ 11-unrolled-loop-invariant.c:10:5-10:8 │ │ │ + └────────────────────────────────────────────▶ │ (11-unrolled-loop-invariant.c:10:5-10:8) │ ──────────────────────────────────────────────────────────────────────────────────────────────────┘ │ + └──────────────────────────────────────────────────────┘ │ + ▲ Neg(k < 100) │ + └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c --set dbg.level debug 2>&1 | tail -n +2 [Debug] 'goblint' '--set' 'lib.activated' '[]' '--set' 'exp.unrolling-factor' '5' '--enable' 'ana.int.interval' '--enable' 'witness.yaml.enabled' '11-unrolled-loop-invariant.c' '--set' 'dbg.level' 'debug' [Debug] Custom include dirs: diff --git a/tests/regression/cfg/util/cfgDot.ml b/tests/regression/cfg/util/cfgDot.ml index 8d28933596..7eb7cb27c1 100644 --- a/tests/regression/cfg/util/cfgDot.ml +++ b/tests/regression/cfg/util/cfgDot.ml @@ -1,12 +1,31 @@ +open Goblint_lib + +let usage_msg = "cfgDot [--unroll ] " + +let files = ref [] +let unroll = ref 0 + +let anon_fun filename = + files := filename :: !files + +let speclist = [ + ("--unroll", Arg.Set_int unroll, "Unroll loops"); +] + let main () = Goblint_logs.Logs.Level.current := Info; Cilfacade.init (); + GobConfig.set_bool "dbg.cfg.loop-unrolling" true; + GobConfig.set_int "exp.unrolling-factor" !unroll; - let ast = Cilfacade.getAST (Fpath.v Sys.argv.(1)) in + assert (List.length !files = 1); + let ast = Cilfacade.getAST (Fpath.v (List.hd !files)) in CilCfg0.end_basic_blocks ast; (* Part of CilCfg.createCFG *) GoblintCil.iterGlobals ast (function | GFun (fd, _) -> + if !unroll > 0 then + LoopUnrolling.unroll_loops fd (-1); GoblintCil.prepareCFG fd; GoblintCil.computeCFGInfo fd true | _ -> () @@ -52,4 +71,6 @@ let main () = | _ -> () ) -let () = main () +let () = + Arg.parse speclist anon_fun usage_msg; + main () diff --git a/tests/regression/cfg/util/dune b/tests/regression/cfg/util/dune index 8528aca384..fe03f7a3ec 100644 --- a/tests/regression/cfg/util/dune +++ b/tests/regression/cfg/util/dune @@ -4,6 +4,7 @@ goblint-cil goblint_logs goblint_common + goblint_lib ; TODO: avoid: extract LoopUnrolling from goblint_lib fpath goblint.sites.dune goblint.build-info.dune) From bebf99a30a6a4f303af419c3222808117ceed3a0 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 Apr 2024 11:38:00 +0300 Subject: [PATCH 12/14] Remove debug output from 55-loop-unrolling/11-unrolled-loop-invariant --- .../11-unrolled-loop-invariant.t | 1234 +---------------- 1 file changed, 3 insertions(+), 1231 deletions(-) diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t index 7b319f431e..81244d00f8 100644 --- a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -139,1102 +139,10 @@ ▲ Neg(k < 100) │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ - $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c --set dbg.level debug 2>&1 | tail -n +2 - [Debug] 'goblint' '--set' 'lib.activated' '[]' '--set' 'exp.unrolling-factor' '5' '--enable' 'ana.int.interval' '--enable' 'witness.yaml.enabled' '11-unrolled-loop-invariant.c' '--set' 'dbg.level' 'debug' - [Debug] Custom include dirs: - [Debug] 1. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/include (exists=true) - [Debug] 2. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/runtime/include (exists=true) - [Debug] 3. /home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/src (exists=true) - [Debug] Preprocessing files. - [Debug] Preprocessor cpp: is_bad=false - [Debug] 'cpp' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/include' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/runtime/include' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/_build/install/default/share/goblint/lib/stub/src' '11-unrolled-loop-invariant.c' '-o' '.goblint/preprocessed/11-unrolled-loop-invariant.i' - [Debug] Parsing files. - Frontc is parsing .goblint/preprocessed/11-unrolled-loop-invariant.i - Converting CABS->CIL - [Debug] Constructors: - [Debug] Adding constructors to: main + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled 11-unrolled-loop-invariant.c [Info] unrolling loop at 11-unrolled-loop-invariant.c:3:3-4:8 with factor 5 - [Debug] Marking if (! (i < 10)) { - break; - } as copy of if (! (i < 10)) { - break; - } - [Debug] Marking goto loop_end; as copy of break; - [Debug] Marking { - i ++; - } as copy of { - i ++; - } - [Debug] Marking i ++; as copy of i ++; - [Debug] Marking if (! (i < 10)) { - break; - } as copy of if (! (i < 10)) { - break; - } - [Debug] Marking goto loop_end; as copy of break; - [Debug] Marking { - i ++; - } as copy of { - i ++; - } - [Debug] Marking i ++; as copy of i ++; - [Debug] Marking if (! (i < 10)) { - break; - } as copy of if (! (i < 10)) { - break; - } - [Debug] Marking goto loop_end; as copy of break; - [Debug] Marking { - i ++; - } as copy of { - i ++; - } - [Debug] Marking i ++; as copy of i ++; - [Debug] Marking if (! (i < 10)) { - break; - } as copy of if (! (i < 10)) { - break; - } - [Debug] Marking goto loop_end; as copy of break; - [Debug] Marking { - i ++; - } as copy of { - i ++; - } - [Debug] Marking i ++; as copy of i ++; - [Debug] Marking if (! (i < 10)) { - break; - } as copy of if (! (i < 10)) { - break; - } - [Debug] Marking goto loop_end; as copy of break; - [Debug] Marking { - i ++; - } as copy of { - i ++; - } - [Debug] Marking i ++; as copy of i ++; [Info] unrolling loop at 11-unrolled-loop-invariant.c:8:5-9:10 with factor 5 - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking goto loop_end___0; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking goto loop_end___0; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking goto loop_end___0; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking goto loop_end___0; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking goto loop_end___0; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; [Info] unrolling loop at 11-unrolled-loop-invariant.c:7:3-11:3 with factor 5 - [Debug] Marking if (! (j < 10)) { - break; - } as copy of if (! (j < 10)) { - break; - } - [Debug] Marking goto loop_end___1; as copy of break; - [Debug] Marking { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } as copy of { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_0___2: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_1___1: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_2___1: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_3___1: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_4___1: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; - [Debug] Marking while (k < 100) { - { - k ++; - } - } as copy of while (k < 100) { - { - k ++; - } - } - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking break; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_end___2: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; - [Debug] Marking { - j ++; - } as copy of { - j ++; - } - [Debug] Marking j ++; as copy of j ++; - [Debug] Marking if (! (j < 10)) { - break; - } as copy of if (! (j < 10)) { - break; - } - [Debug] Marking goto loop_end___1; as copy of break; - [Debug] Marking { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } as copy of { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_0___3: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_1___3: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_2___2: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_3___2: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_4___2: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; - [Debug] Marking while (k < 100) { - { - k ++; - } - } as copy of while (k < 100) { - { - k ++; - } - } - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking break; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_end___3: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; - [Debug] Marking { - j ++; - } as copy of { - j ++; - } - [Debug] Marking j ++; as copy of j ++; - [Debug] Marking if (! (j < 10)) { - break; - } as copy of if (! (j < 10)) { - break; - } - [Debug] Marking goto loop_end___1; as copy of break; - [Debug] Marking { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } as copy of { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_0___4: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_1___4: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_2___4: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_3___3: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_4___3: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; - [Debug] Marking while (k < 100) { - { - k ++; - } - } as copy of while (k < 100) { - { - k ++; - } - } - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking break; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_end___4: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; - [Debug] Marking { - j ++; - } as copy of { - j ++; - } - [Debug] Marking j ++; as copy of j ++; - [Debug] Marking if (! (j < 10)) { - break; - } as copy of if (! (j < 10)) { - break; - } - [Debug] Marking goto loop_end___1; as copy of break; - [Debug] Marking { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } as copy of { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_0___5: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_1___5: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_2___5: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_3___5: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_4___4: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; - [Debug] Marking while (k < 100) { - { - k ++; - } - } as copy of while (k < 100) { - { - k ++; - } - } - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking break; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_end___5: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; - [Debug] Marking { - j ++; - } as copy of { - j ++; - } - [Debug] Marking j ++; as copy of j ++; - [Debug] Marking if (! (j < 10)) { - break; - } as copy of if (! (j < 10)) { - break; - } - [Debug] Marking goto loop_end___1; as copy of break; - [Debug] Marking { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } as copy of { - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_0___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_1___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_2___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_3___0: /* CIL Label */ ; - if (! (k < 100)) { - goto loop_end___0; - } - { - k ++; - } - loop_continue_4___0: /* CIL Label */ ; - while (k < 100) { - { - k ++; - } - } - loop_end___0: /* CIL Label */ ; - } - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_0___6: /* CIL Label */ ; as copy of loop_continue_0___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_1___6: /* CIL Label */ ; as copy of loop_continue_1___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_2___6: /* CIL Label */ ; as copy of loop_continue_2___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_3___6: /* CIL Label */ ; as copy of loop_continue_3___0: /* CIL Label */ ; - [Debug] Marking if (! (k < 100)) { - goto loop_end___0; - } as copy of if (! (k < 100)) { - goto loop_end___0; - } - [Debug] Marking goto loop_end___0; as copy of goto loop_end___0; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_continue_4___6: /* CIL Label */ ; as copy of loop_continue_4___0: /* CIL Label */ ; - [Debug] Marking while (k < 100) { - { - k ++; - } - } as copy of while (k < 100) { - { - k ++; - } - } - [Debug] Marking if (! (k < 100)) { - break; - } as copy of if (! (k < 100)) { - break; - } - [Debug] Marking break; as copy of break; - [Debug] Marking { - k ++; - } as copy of { - k ++; - } - [Debug] Marking k ++; as copy of k ++; - [Debug] Marking loop_end___6: /* CIL Label */ ; as copy of loop_end___0: /* CIL Label */ ; - [Debug] Marking { - j ++; - } as copy of { - j ++; - } - [Debug] Marking j ++; as copy of j ++; - [Debug] And now... the Goblin! - [Debug] Startfuns: [main] - Exitfuns: [] - Otherfuns: [] - [Debug] Activated analyses: expRelation, base, threadid, threadflag, threadreturn, escape, mutexEvents, mutex, access, race, mallocWrapper, mhp, assert - [Debug] Activated transformations: - [Debug] Generating the control flow graph. - [Debug] cfgF (bindings=102 buckets=128 max_length=3 histo=60,37,28,3 load=0.796875), cfgB (bindings=102 buckets=128 max_length=3 histo=59,40,25,4 load=0.796875) - [Debug] Initializing 0 globals. - [Debug] Executing 1 assigns. - [Debug] Solving the constraint system with td3. Solver statistics are shown every 10s or by signal sigusr1. - - [Debug] Unstable solver start vars in 1. phase: - [Debug] L:call of main (297) on 11-unrolled-loop-invariant.c:1:1-13:1 - - [Debug] Data after solve completed: - [Debug] |rho|=126 - [Debug] |stable|=126 - [Debug] |infl|=126 - [Debug] |wpoint|=0 - [Debug] |sides|=24 - [Debug] |side_dep|=0 - [Debug] |side_infl|=0 - [Debug] |var_messages|=0 - [Debug] |rho_write|=0 - [Debug] |dep|=101 - [Debug] Postsolving - [Debug] Pruning result - [Debug] Data after postsolve: - [Debug] |rho|=127 - [Debug] |stable|=127 - [Debug] |infl|=126 - [Debug] |wpoint|=0 - [Debug] |sides|=24 - [Debug] |side_dep|=25 - [Debug] |side_infl|=33 - [Debug] |var_messages|=0 - [Debug] |rho_write|=32 - [Debug] |dep|=101 [Info][Deadcode] Logical lines of code (LLoC) summary: live: 10 dead: 0 @@ -1259,147 +167,11 @@ [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:12-8:19) [Warning][Deadcode][CWE-571] condition 'k < 100' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:8:12-8:19) [Warning][Deadcode][CWE-571] condition 'j < 10' (possibly inserted by CIL) is always true (11-unrolled-loop-invariant.c:7:10-7:16) - [Debug] node 31 "i < 10" is not a copy - [Debug] node 23 "i < 10" is copy of if (! (i < 10)) { - goto while_break; - } (31) - [Debug] node 18 "i < 10" is copy of if (! (i < 10)) { - goto while_break; - } (31) - [Debug] node 13 "i < 10" is copy of if (! (i < 10)) { - goto while_break; - } (31) - [Debug] node 8 "i < 10" is copy of if (! (i < 10)) { - goto while_break; - } (31) - [Debug] node 3 "i < 10" is copy of if (! (i < 10)) { - goto while_break; - } (31) - [Debug] node 124 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 252 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 247 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 112 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 104 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 232 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 99 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 224 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 94 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 219 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 89 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 214 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 84 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 209 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 204 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 72 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 64 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 192 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 59 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 184 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 54 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 179 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 49 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 174 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 44 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 169 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 164 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 152 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 275 "k < 100" is not a copy - [Debug] node 144 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 139 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 267 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 134 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 262 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 129 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 257 "k < 100" is copy of if (! (k < 100)) { - goto while_break___6; - } (275) - [Debug] node 121 "j < 10" is copy of if (! (j < 10)) { - goto while_break___5; - } (244) - [Debug] node 244 "j < 10" is not a copy - [Debug] node 81 "j < 10" is copy of if (! (j < 10)) { - goto while_break___5; - } (244) - [Debug] node 201 "j < 10" is copy of if (! (j < 10)) { - goto while_break___5; - } (244) - [Debug] node 41 "j < 10" is copy of if (! (j < 10)) { - goto while_break___5; - } (244) - [Debug] node 161 "j < 10" is copy of if (! (j < 10)) { - goto while_break___5; - } (244) [Info][Witness] witness generation summary: total generation entries: 19 +TODO: use yamlWitnessStrip for this + $ cat witness.yml | grep -A 1 'value:' value: i == 10 format: c_expression From 4a7863d6533bba186d00c90a5d23311130310659 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 3 Apr 2024 11:40:11 +0300 Subject: [PATCH 13/14] Remove some loop unrolling CFG debugging --- src/util/loopUnrolling.ml | 4 +++- src/witness/yamlWitness.ml | 9 --------- 2 files changed, 3 insertions(+), 10 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index e803209594..02cce23f42 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -1,6 +1,8 @@ open GobConfig open GoblintCil +module M = Messages + (*loop unroll heuristics*) (*used if AutoTune is activated*) @@ -402,7 +404,7 @@ class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object (* this makes new physical copy*) let new_s = {sn with labels = new_labels} in CopyOfHashTable.replace copyof new_s s; - Logs.debug "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s; + if M.tracing then M.trace "cfg" "Marking %a as copy of %a" CilType.Stmt.pretty new_s CilType.Stmt.pretty s; if new_s.labels <> [] then (* Use original s, ns might be temporay e.g. if the type of statement changed *) (* record that goto s; appearing in the current fragment should later be patched to goto new_s *) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index 92e09c238d..d9d39ccee1 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -289,15 +289,6 @@ struct LH.fold (fun loc ns acc -> if WitnessInvariant.emit_loop_head && List.exists is_loop_head_node ns then ( let inv = List.fold_left (fun acc n -> - begin match n with - | Node.Statement s -> - let s' = LoopUnrolling.find_original s in - if s != s' then - Logs.debug "%a is copy of %a (%d)" Node.pretty n CilType.Stmt.pretty s' s'.sid - else - Logs.debug "%a is not a copy" Node.pretty n - | _ -> () - end; let local = try NH.find (Lazy.force nh) n with Not_found -> Spec.D.bot () in Invariant.(acc || R.ask_local_node n ~local (Invariant Invariant.default_context)) [@coverage off] (* bisect_ppx cannot handle redefined (||) *) ) (Invariant.bot ()) ns From 41f4a6dd12e69fd36d21762497c9afb399552400 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 4 Apr 2024 10:19:11 +0300 Subject: [PATCH 14/14] Add graph-easy availability condition to 55-loop-unrolling/11-unrolled-loop-invariant --- tests/regression/55-loop-unrolling/dune | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/tests/regression/55-loop-unrolling/dune b/tests/regression/55-loop-unrolling/dune index 23c0dd3290..a2bf9b4515 100644 --- a/tests/regression/55-loop-unrolling/dune +++ b/tests/regression/55-loop-unrolling/dune @@ -1,2 +1,8 @@ (cram (deps (glob_files *.c))) + +(cram + (applies_to 11-unrolled-loop-invariant) + (enabled_if %{bin-available:graph-easy}) + (deps + %{bin:cfgDot}))