-
Notifications
You must be signed in to change notification settings - Fork 75
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Failures on haskell code #995
Comments
I'm similarly having a look at stoke and have run into similar issues in the past, although on gcc. Although I don't have a solution for you, I can perhaps offer some alternative insight. When compiling binaries on gcc 8.2.1, I got a lot of errors of the sort As for the errors regard undefined symbols, I haven't had any luck getting stoke to work with functions that contain calls, with any call to a different functions. If this is possible, I do not know how this is done and would appreciate any pointers. |
Sorry there's nobody who really works on the stoke codebase these days, but I can offer some insights:
|
Yes, STOKE does not support optimizing across calls as far as I know. The paper I wrote used very specialized support for functions, essentially as a way to add "custom" instructions by implementing them as functions (and teaching the verifier to treat these functions specially). It did not have any support for functions in the regular sense of the word. |
I'm just trying out
stoke
for fun/curiosity. I've built latest indevelop
branch, in a 16.04 docker container. I can't run the tests due to this.My
/proc/cpuinfo
:I'm not sure if you're trying to support targets compiled with something other than
gcc
, but I get various errors on a hello-world Haskell binary (happy to provide details to repro, if you want).extract
I see a lot of files in
hello_plain_bins
though.testcase
Trying a few functions haphazardly...
I don't have any particular reason to believe STOKE will be helpful on these functions, I was just curious to see what would happen. Not sure how much help I'll be able to be but let me know.
The text was updated successfully, but these errors were encountered: