-
Notifications
You must be signed in to change notification settings - Fork 30
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.
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
Allow bounds to be saved to and loaded from files #759
Conversation
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
Signed-off-by: Hernan Ponce de Leon <[email protected]>
} catch (IOException e) { | ||
e.printStackTrace(); | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Are you sure that you just want to print the stack trace and then keep going? The code will just keep running with an incomplete file and will likely trigger the same error a few more times since the file is accessed multiple times (this commenet applies to all the cases where you do this).
I would rather throw a terminating exception or log a warning (only once!) and reset whatever has been computed so far as if no file was provided (e.g., when computing the bounds).
Thanks @ThomasHaas for the clean-up. Unless the CI complains due to the bounds file generation, or times drastically increase, I will merge the code as it. |
I'm still not a fan of all the |
Signed-off-by: Hernan Ponce de Leon <[email protected]>
dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/LoopUnrolling.java
Outdated
Show resolved
Hide resolved
Signed-off-by: Hernan Ponce de Leon <[email protected]>
dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java
Outdated
Show resolved
Hide resolved
Signed-off-by: Hernan Ponce de Leon <[email protected]>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
This feature needs to be used with caution since the information depends on event ids which may not match if the program is changed. However, if used as intended (just run dartagnan several times in a row and let it automatically adapt the bounds until getting PASS), it can boost performance. I have seen improvements up to 3x.