search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
427 stars 82 forks source link

Reproduce the paper, but I can't accomplish #800

Closed zoush99 closed 5 months ago

zoush99 commented 6 months ago

Hi, everyone! I would like to reproduce the results of your paper "Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification", do you have the artifact file submitted at that time? I see that there is a paper that mentions it, thanks. Good luck with the work! @ZackPierce @zvonimir

zoush99 commented 6 months ago

The paper "Verifying Fortran Programs with CIVL" said that, "All SMACK executions were conducted on a TACAS 2020 AEVM provided by the authors of [13]; the version of SMACK is 1.9.1." Thank you for your response!

keram88 commented 5 months ago

Hello,

This should be the artifact for the VMCAI paper: https://drive.google.com/file/d/1xun6p7vOkMm-g9ik9hqbDPEV_LQm5SBS/view?usp=drivesdk

Let us know if it works and if your results match.

Best, Mark

On Sat, Apr 13, 2024, 02:06 zoush99 @.***> wrote:

The paper "Verifying Fortran Programs with CIVL" said that, "All SMACK executions were conducted on a TACAS 2020 AEVM provided by the authors of [13]; the version of SMACK is 1.9.1." Thank you for your response!

— Reply to this email directly, view it on GitHub https://github.com/smackers/smack/issues/800#issuecomment-2053566286, or unsubscribe https://github.com/notifications/unsubscribe-auth/ABQSABO6KRT5TZWOHYPUEUDY5DROTAVCNFSM6AAAAABGFIRGXOVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDANJTGU3DMMRYGY . You are receiving this because you are subscribed to this thread.Message ID: @.***>

zoush99 commented 5 months ago

Thank you for your response! I appreciate the guidance and will endeavor to replicate the impressive work achieved by your team. SMACK is truly a remarkable accomplishment, and I wish you continued success with it! Best, zoush

zoush99 commented 5 months ago

When I install it on the TACAS19 image, it reports the following. @keram88 dpkg: error processing package gnustep-back0.27 (--install): dependency problems - leaving unconfigured Processing triggers for gnome-menus (3.13.3-11ubuntu1.1) ... Processing triggers for desktop-file-utils (0.23-1ubuntu3.18.04.1) ... Processing triggers for mime-support (3.60ubuntu1) ... Processing triggers for man-db (2.8.3-2) ... Processing triggers for install-info (6.5.0.dfsg.1-2) ... Processing triggers for ureadahead (0.100.0-20) ... Processing triggers for systemd (237-3ubuntu10.3) ... Processing triggers for libc-bin (2.27-3ubuntu1) ... Errors were encountered while processing: gnustep-gui-runtime gnustep-make gobjc gobjc-8 gorm.app grr.app gworkspace.app helpviewer.app libaddressview0 libgnustep-base1.26 libgnustep-base-dev libgnustep-gui0.27 libgnustep-gui-dev libgorm1 libpantomime1.3 libpopplerkit0 libpreferencepanes1 librenaissance0 librenaissance0-dev librsskit0d libwraster6:amd64 mknfonts.tool price.app projectcenter.app systempreferences.app terminal.app textedit.app viewpdf.app wmaker zipper.app addressmanager.app affiche.app agenda.app charmap.app dictionaryreader.app edenmath.app gnumail.app gnustep gnustep-back0.27-cairo gnustep-back-common gnustep-base-runtime gnustep-core-devel gnustep-devel libaddresses0 libdbuskit0 libwings3:amd64 gnustep-back0.27

keram88 commented 5 months ago

I don't know why that is breaking without seeing the rest of your setup, but if you are only testing Fortran programs, you should be able to skip the install script in the artifact. These files are needed to compile Swift programs. The included flang compiler should be self contained.

Best, Mark

zoush99 commented 5 months ago

Sorry to bother you so much, but I always get an error when I run it on your artifact, maybe you can tell me your runtime environment? Like ubuntu version, is the software pre-installed? Or the version of artifact you provided is not the one that can be executed correctly? Thank you very much! I have tested it on ubuntu19.04 and ubuntu20.04 and neither of them can be executed correctly!

zous@zous-VirtualBox:~/Downloads/artifact-VMCAI/artifact/gandalv$ ./regtest.py --folder fortran
Creating Pool with '1' Workers
Running regression tests...
./fortran/array.f90
./fortran/array_fail.f90
./fortran/basic.f90
./fortran/basic_fail.f90
./fortran/compound.f90
./fortran/compound_fail.f90
./fortran/compound_fail_2.f90
./fortran/compute.f90
./fortran/compute_fail.f90
./fortran/fib.f90
./fortran/fib_fail.f90
./fortran/fib_fail_2.f90
./fortran/forloop.f90
./fortran/forloop_fail.f90
./fortran/function.f90
./fortran/function_fail.f90
./fortran/function_fail_2.f90
./fortran/function_fail_3.f90
./fortran/inout.f90
./fortran/inout_fail.f90
./fortran/pointer.f90
./fortran/pointer_fail.f90
 ./fortran/array.f90
UNKNOWN  [0.19s]

./fortran/array_fail.f90
UNKNOWN  [0.14s]

 ./fortran/basic.f90
UNKNOWN  [0.14s]

./fortran/basic_fail.f90
UNKNOWN  [0.14s]

./fortran/compound.f90
UNKNOWN  [0.14s]

./fortran/compound_fail.f90
UNKNOWN  [0.15s]

./fortran/compound_fail_2.f90
UNKNOWN  [0.15s]

./fortran/compute.f90
UNKNOWN  [0.15s]

./fortran/compute_fail.f90
UNKNOWN  [0.14s]

   ./fortran/fib.f90
UNKNOWN  [0.14s]

./fortran/fib_fail.f90
UNKNOWN  [0.14s]

./fortran/fib_fail_2.f90
UNKNOWN  [0.15s]

./fortran/forloop.f90
UNKNOWN  [0.14s]

./fortran/forloop_fail.f90
UNKNOWN  [0.14s]

./fortran/function.f90
UNKNOWN  [0.20s]

./fortran/function_fail.f90
UNKNOWN  [0.20s]

./fortran/function_fail_2.f90
UNKNOWN  [0.18s]

./fortran/function_fail_3.f90
UNKNOWN  [0.15s]

 ./fortran/inout.f90
UNKNOWN  [0.14s]

./fortran/inout_fail.f90
UNKNOWN  [0.14s]

./fortran/pointer.f90
UNKNOWN  [0.14s]

./fortran/pointer_fail.f90
UNKNOWN  [0.15s]

Quitting normally
 ELAPSED TIME [3.41s]
 PASSED count: 0
 FAILED count: 0
 TIMEOUT count: 0
 UNKNOWN count: 22

================================================================================
fortran results:
================================================================================
array: FAILING
basic: FAILING
compound: FAILING
compute: FAILING
fib: FAILING
forloop: FAILING
function: FAILING
inout: FAILING
pointer: FAILING
zous@zous-VirtualBox:~/Downloads/artifact-VMCAI/artifact/gandalv/fortran$ ./verify.sh array.f90
SMACK program verifier version 1.9.1
Traceback (most recent call last):
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/smack", line 13, in <module>
    smack.top.main()
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/top.py", line 618, in main
    frontend(args)
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/top.py", line 315, in frontend
    bitcode = frontends()[lang](input_file,args) 
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/frontend.py", line 168, in fortran_frontend
    fortran_build_libs(args)
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/frontend.py", line 272, in fortran_build_libs
    bc = fortran_compile_to_bc(c,compile_command,args)
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/frontend.py", line 112, in fortran_compile_to_bc
    try_command(['llvm-as', ll])
  File "/home/zous/Downloads/artifact-VMCAI/artifact/smack/bin/../share/smack/utils.py", line 69, in try_command
    raise Exception(output)
Exception: llvm-as: error while loading shared libraries: libffi.so.6: cannot open shared object file: No such file or directory
zoush99 commented 5 months ago

Oh, I managed to solve it, it's really great! I installed mono and it works! Thank you very much! You guys are doing a fantastic job!

keram88 commented 5 months ago

Should anyone be interested in running the VMCAI 2020 artifact in the future, it is intended to be used inside this virtual machine provided by the conference: https://zenodo.org/records/3533104

I have uploaded a copy of the artifact here: https://zenodo.org/records/10988936

keram88 commented 5 months ago

Where did you get the artifact? Sorry, it's been a while since I've thought about this and noticed we didn't link a copy in the VMCAI publication.

zoush99 commented 5 months ago

Hi, your artifact was mentioned in the experimental section of this article (Verifying Fortran Programs with CIVL) https://link.springer.com/chapter/10.1007/978-3-030-99524-9_6), but we didn't find it, so came to consult you.