From c439f7934ecc50a97a300b280aaa740187ee0aab Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Wed, 2 Oct 2024 22:18:05 +0300
Subject: [PATCH 1/3] Handle loop statement comparison between two variables in
 loopUnrolling

---
 src/util/loopUnrolling.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index c883e121fc..fe9fec6ce8 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -220,13 +220,21 @@ let findBreakComparison loopStatement =
   with WrongOrMultiple ->
     None
 
-let getLoopVar = function
+let getLoopVar loopStatement func = function
   | BinOp (op, (Const (CInt (goal, _, _) )), Lval ((Var varinfo), NoOffset), (TInt _)) when isCompare op && not varinfo.vglob ->
     (* TODO: define isCompare and flip in cilfacade and refactor to use instead of the many separately defined similar functions *)
     let flip = function | Lt -> Gt | Gt -> Lt | Ge -> Le | Le -> Ge | s -> s in
     Some (flip op, varinfo, goal)
   | BinOp (op, Lval ((Var varinfo), NoOffset), (Const (CInt (goal, _, _) )), (TInt _)) when isCompare op && not varinfo.vglob ->
     Some (op, varinfo, goal)
+  (* When loop condition has a comparison between variables, we assume that the left one is the counter and right one is the bound.
+     TODO: can we do something more meaningful instead of this assumption? *)
+  | BinOp (op, Lval ((Var varinfo), NoOffset), Lval ((Var varinfo2), NoOffset), (TInt _)) 
+  | BinOp (op, CastE ((TInt _), (Lval ((Var varinfo), NoOffset))), Lval ((Var varinfo2), NoOffset), (TInt _)) when isCompare op && not varinfo.vglob && not varinfo2.vglob ->
+    begin match constBefore varinfo2 loopStatement func with
+      | Some goal -> Logs.debug "const: %a %a" CilType.Varinfo.pretty varinfo2 GobZ.pretty goal; Some (op, varinfo, goal)
+      | None -> None
+    end;
   | _ -> None
 
 let getsPointedAt var func =
@@ -273,7 +281,7 @@ let loopIterations start diff goal shouldBeExact =
 let fixedLoopSize loopStatement func =
   let open GobOption.Syntax in
   let* comparison = findBreakComparison loopStatement in
-  let* op, var, goal = getLoopVar comparison in
+  let* op, var, goal = getLoopVar loopStatement func comparison in
   if getsPointedAt var func then
     None
   else

From 881532da16ecc8b9b8507f307c4ffdaa07421787 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 10 Oct 2024 12:00:23 +0300
Subject: [PATCH 2/3] Ignore labels inserted by loopunrolling when finding
 latest var assigns

---
 src/util/loopUnrolling.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index fe9fec6ce8..5739fd70e5 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -154,7 +154,17 @@ let constBefore var loop f =
   let targetLocation = loopLocation loop
   in let rec lastAssignmentToVarBeforeLoop (current: (Z.t option)) (statements: stmt list) = match statements with
       | st::stmts -> (
-          let current' = if st.labels <> [] then (Logs.debug "has Label"; (None)) else current in
+          let current' =
+            (* If there exists labels that are not the ones inserted by loop unrolling, forget the found assigned constant value *)
+            if List.exists (function
+                | Label (s,_,_) -> not (String.starts_with ~prefix:"loop_continue" s || String.starts_with ~prefix:"loop_end" s)
+                | _ -> true) st.labels
+            then
+              (Logs.debug "has Label"; (None))
+            else
+              current
+          in
+          (* let current' = current in *)
           match st.skind with
           | Instr list -> (
               match lastAssignToVar var list with

From 13bcf346fb15758de54947e13bfdd747e430d289 Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Thu, 10 Oct 2024 12:02:13 +0300
Subject: [PATCH 3/3] Remove commented out code

---
 src/util/loopUnrolling.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 5739fd70e5..39e17d14d7 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -164,7 +164,6 @@ let constBefore var loop f =
             else
               current
           in
-          (* let current' = current in *)
           match st.skind with
           | Instr list -> (
               match lastAssignToVar var list with