From 25a1aca3e559e954bd45bfdeaa932eefe7728e9e Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Thu, 20 Jun 2024 13:01:59 +0300 Subject: [PATCH 1/2] Assume var is 0 if there was no assign before loop --- src/util/loopUnrolling.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index c883e121fc..7347bca361 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -277,7 +277,8 @@ let fixedLoopSize loopStatement func = if getsPointedAt var func then None else - let* start = constBefore var loopStatement func in + (* Assume var value to be 0 if there was no constant assignment to the var before loop *) + let start = Option.value (constBefore var loopStatement func) ~default:Z.zero in let* diff = assignmentDifference (loopBody loopStatement) var in let* goal = adjustGoal diff goal op in let iterations = loopIterations start diff goal (op=Ne) in From 64b3baaec718a08698c505c052dee1c50e19bfdb Mon Sep 17 00:00:00 2001 From: Karoliine Holter Date: Fri, 27 Sep 2024 15:12:01 +0300 Subject: [PATCH 2/2] Bugfix: do not assume loop start to be 0 in case of decreasing values --- src/util/loopUnrolling.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml index 7347bca361..905cc39e6a 100644 --- a/src/util/loopUnrolling.ml +++ b/src/util/loopUnrolling.ml @@ -277,9 +277,10 @@ let fixedLoopSize loopStatement func = if getsPointedAt var func then None else - (* Assume var value to be 0 if there was no constant assignment to the var before loop *) - let start = Option.value (constBefore var loopStatement func) ~default:Z.zero in - let* diff = assignmentDifference (loopBody loopStatement) var in + let diff = Option.value (assignmentDifference (loopBody loopStatement) var) ~default:Z.one in + (* Assume var start value if there was no constant assignment to the var before loop; + Assume it to be 0, if loop is increasing and 11 (TODO: can we do better than just 11?) if loop is decreasing *) + let start = Option.value (constBefore var loopStatement func) ~default:(if diff < Z.zero then Z.of_int 11 else Z.zero) in let* goal = adjustGoal diff goal op in let iterations = loopIterations start diff goal (op=Ne) in Logs.debug "comparison: %a" CilType.Exp.pretty comparison;