Skip to content

Improve loop bound detection for loop unrolling by handling casts in loop statements #1599

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Oct 15, 2024
Merged

Improve loop bound detection for loop unrolling by handling casts in loop statements #1599

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f54ce55
Handle casts in loop statements for unrolling
karoliineh Oct 15, 2024
872b159
Refactor: Simplify pattern matching of casts by using Cil.stripCasts
karoliineh Oct 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 11 additions & 7 deletions src/util/loopUnrolling.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -243,23 +243,27 @@ let findBreakComparison loopStatement =
with WrongOrMultiple ->
None

let getLoopVar loopStatement func = function
| BinOp (op, (Const (CInt (goal, _, _) )), Lval ((Var varinfo), NoOffset), (TInt _)) when isCompare op && not varinfo.vglob ->
let findLoopVarAndGoal loopStatement func (op, exp1, exp2) =
match Cil.stripCasts exp1, Cil.stripCasts exp2 with
| Const (CInt (goal, _, _)), Lval (Var varinfo, NoOffset) when 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 ->
| Lval (Var varinfo, NoOffset), Const (CInt (goal, _, _)) when 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 ->
| Lval (Var varinfo, NoOffset), Lval (Var varinfo2, NoOffset) when not varinfo.vglob && not varinfo2.vglob ->
(* 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? *)
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 getLoopVar loopStatement func = function
| BinOp (op, exp1, exp2, TInt _) when isCompare op -> findLoopVarAndGoal loopStatement func (op, exp1, exp2)
| _ -> None

let getsPointedAt var func =
try
let visitor = new isPointedAtVisitor (var) in
Expand Down
Loading