Unsound points-to results?

[Machiry]

I am trying to find aliases for a pointer, specifically, netibuf.

Target (simplified) source of the program (telnet):

Ring netiring;
unsigned char  netibuf[BUFSIZ];
void init_network (void)
{
 ..
  if (ring_init (&netiring, netibuf, sizeof netibuf) != 1)
    {
      exit (EXIT_FAILURE);
    }
  ..
}

int ring_init (Ring * ring, unsigned char *buffer, int count)
{
  memset ((char *) ring, 0, sizeof *ring);

  ring->size = count;

  ring->supply = ring->consume = ring->bottom = buffer;
  ...
}

I use the following code:

PointerAnalysis* currPta = new AndersenWaveDiffWithType();
currPta->analyze(svfModule);
// get the PAG
PAG *currentPAG = currPta->getPAG();
// Get the top-level variable
GlobalVariable *targetGlobVar = targetModule->getGlobalVariable("netibuf", true);

// get node id
NodeID targetNode = currentPAG->getValueNode(targetGlobVar);

// then I search for aliases
for (NodeBS::iterator nIter = currPta->getAllValidPtrs().begin();
                 nIter != currPta->getAllValidPtrs().end();
                 ++nIter) {
                if (currPta->alias(*nIter, targetNode) != NoAlias) {
                    if (targetAliases.find(*nIter) == targetAliases.end()) {
                       dbgs() << "[+] Alias found:" << *nIter << "\n";
                    }
                }
  }

The above doesn't print any aliases, however, as we can see in the program source above, netibuf has aliases. These results are not sound, Am I missing something here?

Attached is the bc file telnet.0.4.opt.mem2reg.bc.zip, of the telnet, that I am using. The target source code is of telnet is available here: https://ftp.gnu.org/gnu/inetutils/inetutils-1.9.4.tar.gz

[yuleisui]

Is "targetNode" an object node or a value node? What's the points-to set of "targetNode"?

[Machiry]

"targetNode" is a value node and a TL pointer.

It has just one object in its points_to set. The object is a memory object, specifically, FIObjNode.

Got PAG Node: TL:1, Address Taken:0, Kind: 0
[$] It has following points to:

[$] Node id:1038 value:@netibuf = internal dso_local global [8192 x i8] zeroinitializer, align 16, !dbg !524, source loc:Glob ln: 69 fl: network.c

[yuleisui]

It is correct to me. Your problem seems that targetAliases was never updated or initialized in your code.

[Machiry]

targetAliases is a an object of type set<NodeID>.

[yuleisui]

Its value is always empty? How about the getAllValidPtrs()? You may wish to print the points to set of all pointers.

[Machiry]

And do intersection with the points to set of targetNode?

[Machiry]

Still..I do not see the NodeID in the pointsto set of other (except for the once top-level node). However, as I explained, there are clearly other aliases. Any help on this is greatly appreciated!

[yuleisui]

Please print points-to sets of all variables, so that we can have a look. It seems to me only one pointer points to the object. You may not get other aliased pointers.

[yuleisui]

Another way to quickly check aliases is to insert a "MAYALIAS" stub function as an oracle (correct answer), SVF will verify the analysis results against the correct answer based on the "MAYALIAS" calls.

See below:
https://github.com/SVF-tools/PTABen/blob/master/basic_c_tests/CI-global.c

[Machiry]

The bc file telnet.0.4.opt.mem2reg.bc.zip, of the telnet, that I am using. The target source code is of telnet is available here: https://ftp.gnu.org/gnu/inetutils/inetutils-1.9.4.tar.gz

Place where we store the @netibuf to the field consume (first field) of netiring:

In Function @main in the IR:

store <2 x i8*> <i8* getelementptr inbounds ([8192 x i8], [8192 x i8]* @netibuf, i64 0, i64 0), i8* getelementptr inbounds ([8192 x i8], [8192 x i8]* @netibuf, i64 0, i64 0)>, <2 x i8*>* bitcast (%struct.Ring* @netiring to <2 x i8*>*), align 16, !dbg !5456, !tbaa !1477

The store function above looks funky, Does SVF correctly handle this kind of store statements?

In Function telrcv, we retrieve:

%16 = getelementptr %struct.Ring, %struct.Ring* @netiring, i64 0, i32 0
%.pre = load i8*, i8** %16, align 16, !dbg !1490, !tbaa !1462

From the source code (telnet.c):

int
telrcv (void)
{
 ...
 lineno:1832     sbp = netiring.consume;
...

But, I do not see %.pre (or sbp) has netiring in its points to set.

From the attached text file (all_aliases.txt.zip) containing points to information of all nodes, I do not see any points to for the target node:

[+] NodeID:10474, Value:  %.pre = load i8*, i8** %16, align 16, !dbg !1490, !tbaa !1462, Src Loc:ln: 1832 fl: telnet.c
Points To:[]

[yuleisui]

Machiry,

Your bc file and whole project is too large. It would be good for you to abstract a small program. I am happy to resolve the issue together with you from a small program since I usually don't have time to debug such large program for SVF users.

I have gone through your problem. From my understanding %.pre should not point to @netiring, but @netibuf which is the first field of @netiring.

The complicated store instruction will be broken down into a few sub instructions before pointer analysis (see https://github.com/SVF-tools/SVF/blob/master/lib/Util/BreakConstantExpr.cpp). You can try to see the points-to value of @netiring to determine the correctness.

I think first you can try to see which pointer stores its value to @netiring (e.g., store %xx, @netiring ) or the first field of @netiring, so that we can know that %16 actually points to some object(s).

Another way to do is to add some assertion checks to figure out the aliases, e.g., MAYALIAS in the source code level, so that SVF can automatically validate that for you to locate the problem.

[Machiry]

I debugged this. I was right, the BreakConstantExpr doesn't handle vector operands. Although This may be fine, but it impacts soundness when dealing with store instructions.
This is exactly what was happening in this case, where the value operand of the store instruction was a ConstantVector:

store <2 x i8*> <i8* getelementptr inbounds ([8192 x i8], [8192 x i8]* @netibuf, i64 0, i64 0), i8* getelementptr inbounds ([8192 x i8], [8192 x i8]* @netibuf, i64 0, i64 0)>, <2 x i8*>* bitcast (%struct.Ring* @netiring to <2 x i8*>*), align 16, !dbg !5456, !tbaa !1477

I have made the fix and create a pull request for the same.

[yuleisui]

Great! Impressive that you have such good understanding of SVF.

[Machiry]

Pull requests: #73 and #74