chc_analyze_file.py: Unable to find function with global vid 111

[bergkvist]

Source code (main.c):

#include <stdlib.h>

int main(int argc, char **argv) {
    return 0;
}

If I remove #include <stdlib.h> include-statement, chc_analyze_file.py works fine.

Command:

chc_parse_file.py main.c && chc_analyze_file.py . main.c && chc_report_file.py . main.c

Logs/Ouput:

Preprocess file: ['gcc', '-fno-inline', '-fno-builtin', '-E', '-g', '-m64', '-o', 'main.i', 'main.c']
Result: 0
Parse file: ['/home/tobias/repos/CodeHawk-C/chc/bin/linux/parseFile', '-projectpath', '/home/tobias/repos/CodeHawk-C/wrapper-test', '-targetdirectory', '/home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts', '-nofilter', '/home/tobias/repos/CodeHawk-C/wrapper-test/main.i']
Parsing /home/tobias/repos/CodeHawk-C/wrapper-test/main.i
[ ; home ; tobias ; repos ; CodeHawk-C ; wrapper-test ; semantics ; chcartifacts]
[/home ; /home/tobias ; /home/tobias/repos ; /home/tobias/repos/CodeHawk-C ; /home/tobias/repos/CodeHawk-C/wrapper-test ; /home/tobias/repos/CodeHawk-C/wrapper-test/semantics ; /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts]
Saving 6 function file(s) ... 
Trying mkdir /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main
Executing mkdir /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main (exitvalue: 0)

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_main_cfun.xml

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_wcstombs_cfun.xml

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_mbstowcs_cfun.xml

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_wctomb_cfun.xml

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_ptsname_r_cfun.xml

Saving function file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main/main_realpath_cfun.xml

Saving cfile file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main_cfile.xml

Saving dictionary file: /home/tobias/repos/CodeHawk-C/wrapper-test/semantics/chcartifacts/main_cdict.xml
 ================================================================ 
 Finished parsing /home/tobias/repos/CodeHawk-C/wrapper-test/main.i
 ================================================================ 

Traceback (most recent call last):
  File "/home/tobias/repos/CodeHawk-C/chc/cmdline/c_file/chc_analyze_file.py", line 157, in <module>
    capp.collect_post_assumes()
  File "/home/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 351, in collect_post_assumes
    self.iter_files(lambda f: f.collect_post_assumes())
  File "/home/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 163, in iter_files
    f(file)
  File "/home/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 351, in <lambda>
    self.iter_files(lambda f: f.collect_post_assumes())
  File "/home/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 128, in collect_post_assumes
    self.iter_functions(lambda fn: fn.collect_post_assumes())
  File "/home/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 214, in iter_functions
    f(fn)
  File "/home/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 128, in <lambda>
    self.iter_functions(lambda fn: fn.collect_post_assumes())
  File "/home/tobias/repos/CodeHawk-C/chc/app/CFunction.py", line 203, in collect_post_assumes
    self.proofs.collect_post_assumes()
  File "/home/tobias/repos/CodeHawk-C/chc/proof/CFunctionProofs.py", line 86, in collect_post_assumes
    self.spos.collect_post_assumes()
  File "/home/tobias/repos/CodeHawk-C/chc/proof/CFunctionSPOs.py", line 68, in collect_post_assumes
    cs.collect_post_assumes()
  File "/home/tobias/repos/CodeHawk-C/chc/proof/CFunctionCallsiteSPOs.py", line 299, in collect_post_assumes
    calleefun = cfile.capp.resolve_vid_function(cfile.index, self.callee.get_vid())
  File "/home/tobias/repos/CodeHawk-C/chc/app/CApplication.py", line 211, in resolve_vid_function
    return self.files[filename].get_function_by_index(tgtvid)
  File "/home/tobias/repos/CodeHawk-C/chc/app/CFile.py", line 202, in get_function_by_index
    raise Exception('Unable to find function with global vid ' + str(index))
Exception: Unable to find function with global vid 111

It seems like pretty much any kind of include-statement with standard Linux libraries will cause this issue. I've tried with:

• #include <stdio.h>
• #include <stdlib.h>
• #include <unistd.h>

---

How to reproduce:

1. Install nixpkgs (on either Linux or macOS)

curl -L https://nixos.org/nix/install | sh

2. Clone this repository:

git clone https://github.com/static-analysis-engineering/CodeHawk-C
cd CodeHawk-C

3. Create a file named shell.nix inside of CodeHawk-C with the following contents:

{ pkgs ? import (fetchTarball "https://github.com/bergkvist/nixpkgs/archive/4b833cc141172f88e563692f2458253212d1cf1a.tar.gz") {} }:

let
  PROJECT_ROOT = toString ./.;
in pkgs.mkShell {
  buildInputs = [
    pkgs.gcc
    pkgs.python39
  ];
  shellHook = ''
    export PYTHONPATH="${PROJECT_ROOT}"
    export PATH="${PROJECT_ROOT}/chc/cmdline/c_file/:$PATH"
  '';
}

4. Create a folder named tmp and add main.c inside with the following contents:

#include <stdlib.h>

int main(int argc, char **argv) {
    return 0;
}

5. Make sure you are in the same folder as shell.nix and run nix-shell (running nix-shell is similar to entering a virtual environment in Python)

nix-shell
[nix-shell]$ cd tmp
[nix-shell]$ chc_parse_file.py main.c && chc_analyze_file.py . main.c && chc_report_file.py . main.c