Unintended consequences of wrapping assertions into one single function

[zvonimir]

While discussing the issue with looking for multiple assertion violations with Corral (brought up by @shaobo-he), I realized that SMACK implements assertions in an "interesting" way that introduces a level of indirection.

Basically, we have a procedure that looks as follows:

procedure __SMACK_assert(cond : bool) {
  assert cond;
}

Then, everywhere we have an assertion in the source code, we do not inject assert statement directly, but rather invoke __SMACK_assert, which adds a level of indirection. This clearly causes an issue if we are looking for multiple assertion violations.

However, I've been wondering if this kind of encoding messes up other algorithms that Corral implements. Such as maybe property-directed verification, etc. Thoughts?

Basically, I am wondering if there would be benefits to "inlining" those assertions to remove the indirection, in terms of performance, scalability, etc.

Thoughts?

[akashlal]

@zvonimir It should not matter. Things like stratified inlining are robust to it. In fact, SDV (which has been the main application driving corral) also encodes things in this way. I have experimented with pre-inlining the assert procedure, but it has little effect. I guess it does interfere with syntax-driven flags like /cex, where pre-inlining these procedures would be best.

[akashlal]

There is an attribute, called {:ForceInline} that you can put on procedures. Stratified inlining then immediately inlines them when their call site is exposed. This can be helpful in general. You can try putting it on these assert procedures, but I suspect you won't notice any change in the running times.

[zvonimir]

Thanks Akash! It seems that {:ForceInline} should help with the multiple counterexamples issue that started this thread.

@shaobo-he Can you take a look into this attribute that Akash suggested? I think you should be able to use it to improve you pull request for multiple counterexamples. Thanks!