search

PrincetonUniversity / VST

Verified Software Toolchain
https://vst.cs.princeton.edu
Other
436 stars 92 forks source link

forward_call takes a long time #750

Closed rigille closed 7 months ago

rigille commented 7 months ago

Hi I really appreciate this project. I'm attempting to write a library for multiple precision arithmetic in C, starting with a comparison function. Inside the loop there are two function calls, and for some reason this forward_call takes a long time. I haven't observed it terminate yet, even if I have a really simple API specification which has no spatial assertions and just returns the second parameter. Also the previous forward_call for a function with an identical specification succeeds quickly. So I suspect the tactic is trying to figure out what the postcondition should be. Is there a workaround for this?

I'm using Coq 8.17 and VST 2.13 on NixOS. There's a flake.nix at the root of the repository, so it's possible to install nix and run nix develop to get an exact copy of my environment if needed.

Edit: It terminates successfully after 11 minutes

rigille commented 7 months ago

I see there were some improvements to forward_call here https://github.com/PrincetonUniversity/VST/issues/729. I'll check if that inclusion solves the problem.

rigille commented 7 months ago

Even with the latest improvements to performance, the tactic still took several minutes to run. However using semax_seq to specify what the postcondition should be made it faster. Or even better use seq_assoc to isolate the function call statement. I guess the real takeaway from this is that forward_call works best when the function call is not grouped with another assignment.