[StaticAnalyser] unreachable code false positives when there are multiple returns

Hello!

I am investigating the false positive for this example code:

static int mt(const int i) {
  if (i != 0)
    return 1;
  return 0;
}

void f1(int i) {
  int x = mt(i);
  x && x<10; // <- Clang says that "x<10" is unreachable
}

As far as I see the ExplodedGraph is not constructed correctly.

I think this is wrong:

   ReturnStmt return 1; ReturnStmt return 0;
   Location context stack: Location context stack:
   0. Calling mt 0: Calling mt
   1. Calling f1 1: Calling f1
   Store, 0x0: Store, 0x0:
   Expressions: Expressions:
   mt:&code{mt} mt:&code{mt}
   i:reg_$0<i> i:reg_$0<i>
        > >
        > >
   Edge: (B2,B0) Edge: (B1,B0)
   Location context stack: Location context stack:
   0. Calling mt 0: Calling mt
   1. Calling f1 1: Calling f1
   Store, 0x0: Store, 0x0:
   Expressions: Expressions:
   mt:&code{mt} mt:&code{mt}
   i:reg_$0<i> i:reg_$0<i>
         \ /
      \ /
               CallExitBegin
               Location context stack:
               0. Calling mt
               1. Calling f1
               Store, 0x0:
               Expressions:
               mt:&code{mt}
               i:reg_$0<i>
                    >
                    >
               ReturnStmt return 0;
               Location context stack:
               0. Calling mt
               1. Calling f1
               Store, 0x0:
               Expressions:
               mt:&code{mt}
               mt(i):0 S32
               i:reg_$0<i>

My own conclusion is that somewhere near the CallExitBegin something wrong happens. To me it looks like the mt always returns 0 according to the explodedgraph.

some more info/hints so I can fix this would be appreciated.

Best regards,
Daniel Marjamäki

..................................................................................................................
Daniel Marjamäki Senior Engineer
Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden

Mobile: +46 (0)709 12 42 62
E-mail: Daniel.Marjamaki@evidente.se

www.evidente.se

Hello!

I previously reduced my example code too much. Here is code I hope reproduce the false positive better:

  extern int table[];

  static int mt(const int i) {
    if (table[i] != 0)
      return 1;
    return 0;
  }

  void f1(int i) {
    int x = mt(i);
    x && x<10; // <- clang says that "x<10" is never executed
  }

My conclusions so far:

The condition "table[i] != 0" result is unknown (SVal = Unknown). Therefore in ExprEngine::processBranch() this code is executed:

    // If the condition is still unknown, give up.
    if (X.isUnknownOrUndef()) {
      builder.generateNode(PrevState, true, PredI);
      builder.generateNode(PrevState, false, PredI);
      continue;
    }

So the same state is used for both the true and false branch.

In CoreEngine::enqueueEndOfFunction() the generateCallExitBeginNode() is called. No difference is seen for the exit nodes for "return 1;" and "return 0;" so only the first node is created.

I don't know.. should this "Profile" function (ExplodedGraph.h, line 159) be modified:

  static void Profile(llvm::FoldingSetNodeID &ID,
                      const ProgramPoint &Loc,
                      const ProgramStateRef &state,
                      bool IsSink) {
    ID.Add(Loc);
    ID.AddPointer(state.get());
    ID.AddBoolean(IsSink);
  }

Or should I modify Loc/State/etc so the difference is detected?

Best regards,
Daniel Marjamäki

..................................................................................................................
Daniel Marjamäki Senior Engineer
Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden

Mobile: +46 (0)709 12 42 62
E-mail: Daniel.Marjamaki@evidente.se

www.evidente.se