devirtbounce name issues with Swift/OBJC method invocation

[jjgarzella]

Currently, SMACK cannot tell between methods in Objective-C or Swift unless they have different method signatures. Both of these languages use devirtbounce to manage method invocation. Consider the following example:

// @expect verified

#import <Foundation/Foundation.h>
#include "smack.h"

@interface Car : NSObject

- (int)numWheels;

- (int)numHeadlights;

- (int)milageLeft:(int)miles;

@end

@implementation Car

- (int)numWheels
{
    return 4;
}

- (int)numHeadlights
{
    return 2;
}
@end

int main(void) {
    Car *c = [[Car alloc] init];
    
    assert([c numWheels] == 4);
    //assert([c numHeadlights] == 2);
    return 0;
}

Running SMACK on this file fails, because smack things that [c numWheels] could be either 4 or 2. Something about the way that devirtbounce does things doesn't keep track of naming, only method signatures. Swift has the exact same problem as Objective-C.

[jjgarzella]

Upon further inspection, it seems there are two issues, one for Objective-C and one for Swift. In both cases, the argument to devirtbounce is not modeled properly, and so it is nondet.

[jjgarzella]

Update: For Objective-C, the culprit right now is the lack of modeling for the objc_msg_lookup function. We could probably get this to work if we properly modeled that function.