PLSysSec / veriwasm

SFI verifier of Wasm binaries
Other
79 stars 7 forks source link

SPEC 2006 Build Problem #7

Open ya0guang opened 1 year ago

ya0guang commented 1 year ago

Hi,

I want to reproduce the evaluation in VeriWASM. However, I cannot build some tasks of SPEC 2006 which is included in your evaluation. What are the steps to compile the SPEC CPU 2006 tests successfully?

The sphinx3 reports such errors in the compilation:

/opt/lucet/bin/wasm32-wasi-clang -c -o unlimit.o -DSPEC_CPU -DNDEBUG -I. -DSPEC_CPU -DHAVE_CONFIG_H -I. -Ilibutil    -O0       -DSPEC_CPU_LP64         unlimit.c
unlimit.c:67:17: error: variable has incomplete type 'struct rlimit'
  struct rlimit rl;
                ^
unlimit.c:67:10: note: forward declaration of 'struct rlimit'
  struct rlimit rl;
         ^
unlimit.c:69:3: warning: implicit declaration of function 'getrlimit' is invalid in C99 [-Wimplicit-function-declaration]
  getrlimit(RLIMIT_DATA,&rl);
  ^
unlimit.c:69:13: error: use of undeclared identifier 'RLIMIT_DATA'
  getrlimit(RLIMIT_DATA,&rl);
            ^
unlimit.c:71:3: warning: implicit declaration of function 'setrlimit' is invalid in C99 [-Wimplicit-function-declaration]
  setrlimit(RLIMIT_DATA,&rl);
  ^
unlimit.c:71:13: error: use of undeclared identifier 'RLIMIT_DATA'
  setrlimit(RLIMIT_DATA,&rl);
            ^
2 warnings and 3 errors generated.

After I comment these lines in unlimit.c like this, the compiler complains like:

void unlimit ( void )
{
#if ((! SPEC_CPU_WINDOWS) && (! _HPUX_SOURCE))
  // struct rlimit rl;

  // getrlimit(RLIMIT_DATA,&rl);
  // rl.rlim_cur = rl.rlim_max;
  // setrlimit(RLIMIT_DATA,&rl);
#endif
}
/opt/lucet/bin/wasm32-wasi-clang -c -o unlimit.o -DSPEC_CPU -DNDEBUG -I. -DSPEC_CPU -DHAVE_CONFIG_H -I. -Ilibutil    -O0       -DSPEC_CPU_LP64         unlimit.c
/opt/lucet/bin/wasm32-wasi-clang   -O0  -DSPEC_CPU_LP64        spec_main_live_pretend.o parse_args_file.o live.o agc.o approx_cont_mgau.o ascr.o beam.o bio.o case.o ckd_alloc.o cmd_ln.o cmn.o cmn_prior.o cont_mgau.o dict.o dict2pid.o err.o feat.o fillpen.o glist.o gs.o hash.o heap.o hmm.o io.o kb.o kbcore.o lextree.o lm.o lmclass.o logs3.o mdef.o new_fe.o new_fe_sp.o profile.o specrand.o str2words.o subvq.o tmat.o unlimit.o utt.o vector.o vithist.o wid.o             -lm        -o sphinx_livepretend
wasm-ld: error: io.o: undefined symbol: popen
wasm-ld: error: io.o: undefined symbol: popen
wasm-ld: error: io.o: undefined symbol: pclose
wasm-ld: error: utt.o: undefined symbol: getcwd
clang-10: error: linker command failed with exit code 1 (use -v to see invocation)

This is because the symbols are not defined in wasi. (their definitions are avoided).

I also modified the cfg file in SPEC 2006 to use clang(++) shipped with lucet.

CC                 = /opt/lucet/bin/wasm32-wasi-clang
CXX                = /opt/lucet/bin/wasm32-wasi-clang++
FC                 = /usr/bin/false

I'm using the most recent lucet (archived version, d0b358c). The tests soplex, sphinx3, and povray cannot be compiled because of undeclared symbol, and gobmk cannot be verified because of veriwasm believe it's not heap safe.

It would also be helpful if you can tell the specific lucet version used in the evaluation. In your evaluation you mentioned lucet 0.7.0, which is not a stable version and I worry that the version changes may also cause inconsistent result.