Clean up or document SMACK warnings

[zvonimir]

Warnings such as:

• collapsing DSA node
• memory intrinsic length exceeds threshold (0); adding quantifiers
• ignoring inline asm passed as argument

are repeatedly confusing our users. We should think about not printing them out by default maybe, and we should also rethink if they are all really needed.

[zvonimir]

Ok, so let's maybe discuss this a little bit. I think that the warnings I listed below should not be printed by default. We should have some kind of a command line option that you have to enable to see these warnings.

[zvonimir]

Actually, now that I think more about this, maybe we should leave this warning ignoring inline asm passed as argument. Since that one I think can affect soundness and it would be good for users to see it.

[shaobo-he]

I talked to Mark about this. I propose we use multi-level verbose/debug output.

[zvonimir]

Yes, I agree with you guys. Could you please propose an implementation for this functionality?

[shaobo-he]

@keram88 Can you take a look at this?

[shaobo-he]

In light of recent development on handling LLVM intrinsics, we should probably give warnings for over-approximations such as bitwise operations when the --bit-precise flag is not enabled.

[shaobo-he]

In the current develop branch, we have the following warnings printed to the console,

1. inline asm
2. memory intrinsic length
3. those generated by the DSMonitor class such as collapsing DSA node
4. over-approximations in intrinsic handling

I also propose we extend 4. I propose we use a two-tier warning outputs. The first tier includes 1 and 4 which is important due to its influences on soundness. The second tier includes 2 and 3.

@zvonimir @michael-emmi @keram88 what do you think?

[keram88]

I think 4 should be as informative as possible. We could go so far as to say something like (try --bit-precise). This would cut down on surprises for users (and occasional debugging holes for us).

[shaobo-he]

Good point. We should do this.

[keram88]

For the fourth item. I'm thinking of the following:
We create an enum class
enum class Requirements { BitPrecise, Float, Strings, ... };

Then we have a requirements predicate:

bool meetsRequirements(std::initializer_list<Requirements> reqs) {
  bool success = true;
  for (req : reqs) {
    switch(req) {
    case BitPrecise: success &= SmackOptions::BitPrecise; break;
     ...
    }
  }  
}

And a warning generator for instructions that end up unmodeled.
void warnUnModeled(CallInst* ci, std::initializer_list<Requirements> req);
For example, with bit-precise disabled we could have
warning: over-approximate call to : llvm.cttz.i32 (try enabling --bit-precise)

Together, these will allow us to reduce the duplicated code in our assign*Expr functions.

If it makes sense, we could also have it say this isn't modeled (by an empty requirements list), e.g.
warning: over-approximate call to: llvm.foo (this operation is currently unmodeled)

In the end I think this helps in two ways: the error messages are more helpful to users by steering them to ways to cut down on false bugs, and possibly reduce the number of issues we receive from this.

I'm still trying to think of how to extend this into a more comprehensive framework across the whole project.

[keram88]

For Zvonimir's original point: We can introduce a new warn function that takes a warning level.
My very rough idea is to add this:

enum class WarningLevel: unsigned {
Silent=0,
Unsound=10, // Unhandled intrinsics, asm, etc
Info=20, // Memory length, etc.
Debug=30,
Everything=UINT_MAX
};

We record the warn switch given to SMACK in SmackOptions (silent is 0, default would be Unsound, and everything would be UINT_MAX), then add a new warn function:

llvm::raw_ostream &warn(WarningLevel level) {
  if (level <= SmackOptions::WarnLevel)
    return errs();
  else
    return nulls();
}

I think for the non-bpl warnings, this would be fairly straightforward to implement.
It feels wrong to do order comparison on an Enum, but we could create a class with factory methods to create the warn level.