Bug report - Code properties violations during software vulnerabilities investigation

[janislley]

Hello,

We found some potential code failures that might cause a security vulnerability.
To identify this kind of vulnerabilities I used tool LSVerifier: https://github.com/janislley/LSVerifier

More about the tool: https://ssvlab.github.io/lucasccordeiro/papers/sbseg2023.pdf

Please, check this report for code property violations:

1 - Dereference failure: NULL pointer

[FILE] ext/fts3/fts3_expr.c
[ARGS] ['--unwind', '1', '--no-unwinding-assertions']
[FUNCTION] sqlite3Fts3OpenTokenizer

int sqlite3Fts3OpenTokenizer(
  sqlite3_tokenizer *pTokenizer,
  int iLangid,
  const char *z,
  int n,
  sqlite3_tokenizer_cursor **ppCsr
){
  sqlite3_tokenizer_module const *pModule = pTokenizer->pModule;
  sqlite3_tokenizer_cursor *pCsr = 0;
  int rc;

  rc = pModule->xOpen(pTokenizer, z, n, &pCsr);
  assert( rc==SQLITE_OK || pCsr==0 );
  if( rc==SQLITE_OK ){
    pCsr->pTokenizer = pTokenizer; // line 145
    if( pModule->iVersion>=1 ){
      rc = pModule->xLanguageid(pCsr, iLangid);
      if( rc!=SQLITE_OK ){
        pModule->xClose(pCsr);
        pCsr = 0;
      }
    }
  }
  *ppCsr = pCsr;
  return rc;
}

Counterexample:

State 5 file fts3_expr.c line 145 function sqlite3Fts3OpenTokenizer thread 0

Violated property:
file fts3_expr.c line 145 function sqlite3Fts3OpenTokenizer
dereference failure: NULL pointer
line 145: pCsr->pTokenizer = pTokenizer;

Pre-analysis:

The function pointer xOpen is called, which presumably sets the value of pCsr. The assertion ensures that if the return code is not SQLITE_OK, then pCsr must be null. If the return code is SQLITE_OK, the code dereferences pCsr with pCsr->pTokenizer = pTokenizer;. This is safe because the assertion guarantees that pCsr is not null when rc is SQLITE_OK.

However, there's a potential issue if the function pointer xOpen or any other function pointer in the pModule structure is null. The code doesn't check for this, and if any of these function pointers are null, it would result in a null pointer dereference.