Question about "function never returning"

[adrianherrera]

Hi folks,

I am trying to apply sea-dsa to some codebases where some functions contain only calls to exit or abort (e.g., error-handling functions). I am trying to construct the MemorySSA, which reports a warning about these functions "never returning". This then results in the assert here failing.

What is it about functions not returning that would cause this to assertion to fail? If you have any pointers to help me get around this (and hopefully contribute a patch!) that would be greatly appreciated.

Thanks!

[agurfinkel]

The pointer you have is to mem-ssa that computes memory SSA form of the program. That code might silently assume that a function has a designated exit basic block. Functions that do not return might not have it.

Can you create a small repro for us to debug? Most of our own clients of sea-dsa ensure that functions always terminate by cutting out non-terminating paths. So we have probably missed some case here.

[adrianherrera]

Hey Arie,

Thanks for the reply!

Most of our own clients of sea-dsa ensure that functions always terminate by cutting out non-terminating paths.

Do you mean like what CLAM does (e.g., the RemoveUnreachableBlocksPass)? I guess these blocks are not actually non-terminating, because they explicitly call exit/abort/etc.

Currently, my client code is a relatively straight forward pass:

void MyPass::getAnalysisUsage(AnalysisUsage &AU) const {
  AU.setPreservesCFG();
  AU.addRequired<seadsa::ShadowMemPass>();
}

bool MyPass::runOnModule(Module &M) {
  auto &ShadowMem = getAnalysis<seadsa::ShadowMemPass>().getShadowMem();

  for (auto &F : M) {
    const auto *MemSSA = ShadowMem.getMemorySSA(F);
    outs() << "```";
    MemSSA->print(outs());
    outs() << "```\n";
  }

  // Remove the shadow memory annotations
  auto StripShadowMem = std::make_unique<seadsa::StripShadowMemPass>();
  StripShadowMem->runOnModule(M);

  return false;
}

And my first test program was the AFL fuzzer test program:

int main(int argc, char** argv) {

  char buf[8];

  if (read(0, buf, 8) < 1) {
    printf("Hum?\n");
    exit(1);
  }

  if (buf[0] == '0')
    printf("Looks like a zero to me!\n");
  else
    printf("A non-zero value? How quaint!\n");

  exit(0);

}

I'll have a deeper look at the CLAM source code to get some ideas (this is all pretty new to me!), but any pointers (hah!) would be greatly appreciated :)

~Adrian

[caballa]

@adrianherrera : thanks for the test. I'll look at it. By non-terminating paths, @arie meant that the execution path does not return. You are probably thinking about non-terminating loops. For our clients (e.g., Clam and SeaHorn), we typically do not care if an execution terminates with the LLVM instruction unreachable. If you look at the bitcode generated by your test, you will see an unreachable LLVM instruction after each call to exit. The pass RemoveUnreachableBlockPass removes any block and predecessors that always terminate with an unreachable instruction.

[adrianherrera]

Thanks @caballa!

Given that, does it suffice to generalize HasReturn (as used here) to also allow for UnreachableInsts and then only mark a cell with a mem.out marker here if the terminator isa<ReturnInst> (and just leave it untouched if it's an UnreachableInst, as this indicates program termination anyway)?

[adrianherrera]

Hey @agurfinkel and @caballa,

Just wondering if you had any thoughts on https://github.com/seahorn/sea-dsa/pull/139?

[caballa]

Hi @adrianherrera sorry for being so late. I still need more time to think about it. Sorry about that