Skip to content
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

Jump to bottom

Handle loop statement comparison between two variables in loop unrolling #1590

Merged
merged 3 commits into from
Oct 11, 2024
Merged

Handle loop statement comparison between two variables in loop unrolling #1590

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
c439f79
Handle loop statement comparison between two variables in loopUnrolling
karoliineh Oct 2, 2024
881532d
Ignore labels inserted by loopunrolling when finding latest var assigns
karoliineh Oct 10, 2024
13bcf34
Remove commented out code
karoliineh Oct 10, 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
23 changes: 20 additions & 3 deletions src/util/loopUnrolling.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,16 @@ 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
match st.skind with
| Instr list -> (
match lastAssignToVar var list with
Expand Down Expand Up @@ -220,13 +229,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? *)
Comment on lines +239 to +240
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Theoretically it would be possible to lift this from the option monad to the list monad for non-determinism and return both here. Then the following checks getsPointedAt, constBefore, etc would filter it down to the one that meets all the conditions (although I guess both could still pass all of them).
It would automatically achieve backtracking instead of what currently happens: if the first one doesn't pass getPointedAt, we don't retry everything with the second variable.

I don't know if it would be worth the trouble though.

| 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 =
Expand Down Expand Up @@ -273,7 +290,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
Expand Down
Loading