Skip to content

Add a more consistent and sophisticated warning system #466

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
Merged
merged 1 commit into from
Jul 2, 2019
Merged

Add a more consistent and sophisticated warning system #466

merged 1 commit into from
Jul 2, 2019

Conversation

shaobo-he
Copy link
Contributor

No description provided.

@shaobo-he shaobo-he mentioned this pull request Jun 18, 2019
Closed
zvonimir
zvonimir requested changes Jun 18, 2019
View reviewed changes
@shaobo-he shaobo-he added this to the Release 2.0.0 milestone Jun 18, 2019
@zvonimir
Copy link
Member

Are you always printing warnings as comments into bpl file?

@shaobo-he
Copy link
Contributor Author

Are you always printing warnings as comments into bpl file?

No, they are printed only when the warning level is greater than or equal to unsound.

@zvonimir zvonimir removed the request for review from michael-emmi June 28, 2019 20:52
keram88
keram88 requested changes Jun 28, 2019
View reviewed changes
Copy link
Contributor

@keram88 keram88 left a comment

Choose a reason for hiding this comment

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

Looks good to me.
I don't think we handled the color warning as elegantly as we could have, but I can't think of a better way. I suppose it could be reworked if more coloring were done later.

Currently we print out some thing like:
unsoundly ignoring ... try adding flag(s) (bit-precise)
would it be better if we said:
unsoundly ignoring ... try adding flag(s) (--bit-precise)

keram88
keram88 approved these changes Jun 28, 2019
View reviewed changes
Copy link
Contributor

@keram88 keram88 left a comment

Choose a reason for hiding this comment

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

Looks good to me.

@shaobo-he
Copy link
Contributor Author

We need to do some refactoring after the bv intrinsic handling PR is merged.

zvonimir
zvonimir requested changes Jun 29, 2019
View reviewed changes
@zvonimir
Copy link
Member

I have a more high-level concern about this pull request. I know we already discussed this to some extent, but it is still not completely clear to me how come we could not simply use LLVM's DEBUG macro functionality to achieve this.

What is DEBUG missing that you could not implement this using it?

Also, we use DEBUG macros a fair amount in the code. So if this gets merge, we will have a combination of DEBUG macros and calls to SmackWarnings in the code. How should then I think about them? Do they serve a different purpose? Or is the plan to switch to SmackWarnings completely and remove DEBUG macros?

@shaobo-he
Copy link
Contributor Author

shaobo-he commented Jun 30, 2019 •
edited
Loading

I have a more high-level concern about this pull request. I know we already discussed this to some extent, but it is still not completely clear to me how come we could not simply use LLVM's DEBUG macro functionality to achieve this.

What is DEBUG missing that you could not implement this using it?

Also, we use DEBUG macros a fair amount in the code. So if this gets merge, we will have a combination of DEBUG macros and calls to SmackWarnings in the code. How should then I think about them? Do they serve a different purpose? Or is the plan to switch to SmackWarnings completely and remove DEBUG macros?

First of all, the existing DEBUG macros serve a different purpose than SmackWarnings. The former is used to print information used for debugging as its name stands for while the latter is to print warnings messages to the users. From this perspective, we don't have to worry about mixing the two implementations.

Second, when I first implemented this PR, I used LLVM's DEBUG macros, which turned out to be very cumbersome. The current implementation is much cleaner than the one using macros. First, it creates very clear and informative interfaces: arguments passed to llvm2bpl are meaningful such as -warn-type=unsound as opposed to -debug-only=unsound if we use LLVM's macros. Second, handling warning message level is intuitive and simple in the current implementation: we simply compare the enum values as opposed to comparing the macro strings. Of course, both of the two things can be implemented using the DEBUG macros, but why the detours?

zvonimir
zvonimir reviewed Jul 1, 2019
View reviewed changes
zvonimir
zvonimir reviewed Jul 1, 2019
View reviewed changes
zvonimir
zvonimir reviewed Jul 1, 2019
View reviewed changes
zvonimir
zvonimir requested changes Jul 1, 2019
View reviewed changes
@shaobo-he @keram88
Improved SMACK's warning system
96785f1 
This commit changes SMACK's warning system as follows,

1. Added a class (SmackWarnings) to provide APIs that print warning messages
to both the Boogie program and the console.

2. The warning messages are layered: there are three levels, silent (no
messages), unsound (messages about unsoundness such as using uninterpreted
functions to model bitwise operations), and info (messages about unsoundness as
well as translation information such as collapsing DSA nodes). Their relation is
silent ⊂ unsound ⊂ info.

3. The warning messages can be colored, which is controlled by the llvm2bpl
option, `-colored-warnings`.

Co-authored-by: Mark Stanislaw Baranowski <mark.s.baranowski@gmail.com>
Co-authored-by: Shaobo He <polarishehn@gmail.com>
zvonimir
zvonimir approved these changes Jul 2, 2019
View reviewed changes
Copy link
Member

@zvonimir zvonimir left a comment

Choose a reason for hiding this comment

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

Looks good to me.

@zvonimir zvonimir merged commit 5c1c469 into develop Jul 2, 2019
@zvonimir zvonimir deleted the improve-warnings branch July 2, 2019 12:38
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@zvonimir zvonimir zvonimir approved these changes

@keram88 keram88 keram88 approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

Release 2.0.0

Development

Successfully merging this pull request may close these issues.

3 participants

@shaobo-he @zvonimir @keram88